[Lean Backend] Add basic support for traits

CHANGELOG.md

@@ -17,6 +17,7 @@ Changes to the Rust Engine:
  - Printers now emit proper diagnostics (PR #1669)
  - Global identifiers are now interned (#1689)
  - Global identifiers are encapsulated properly, and provide easy destructuring as tuple identifiers (#1693)
+ - Add basic support for traits and impls in the Lean backend (#1679)
 
 Changes to the frontend:
 - Add an explicit `Self: Trait` clause to trait methods and consts (#1559)

rust-engine/src/ast.rs

@@ -1531,7 +1531,7 @@ pub mod traits {
     );
     derive_has_kind!(
         Item => ItemKind, Expr => ExprKind, Pat => PatKind, Guard => GuardKind,
-        GenericParam => GenericParamKind, ImplItem => ImplItemKind, TraitItem => TraitItemKind
+        GenericParam => GenericParamKind, ImplItem => ImplItemKind, TraitItem => TraitItemKind, ImplExpr => ImplExprKind
     );
 
     impl HasSpan for Attribute {

rust-engine/src/ast/identifiers/global_id.rs

@@ -323,6 +323,18 @@ impl GlobalId {
         self.0.get().is_projector()
     }
 
+    /// Returns true if the underlying identifier is a precondition (trait/impl item)
+    /// Should be removed once https://github.com/cryspen/hax/issues/1646 has been fixed
+    pub fn is_precondition(self) -> bool {
+        self.0.get().is_precondition()
+    }
+
+    /// Returns true if the underlying identifier is a postcondition (trait/impl item)
+    /// Should be removed once https://github.com/cryspen/hax/issues/1646 has been fixed
+    pub fn is_postcondition(self) -> bool {
+        self.0.get().is_postcondition()
+    }
+
     /// Renders a view of the concrete identifier.
     pub fn view(self) -> view::View {
         ConcreteId::from_global_id(self).view()
@@ -380,6 +392,18 @@ impl GlobalIdInner {
             _ => false,
         }
     }
+
+    /// Returns true if the underlying identifier has the precondition suffix
+    /// Should be removed once https://github.com/cryspen/hax/issues/1646 has been fixed
+    pub fn is_precondition(&self) -> bool {
+        matches!(self, GlobalIdInner::Concrete(concrete_id) if matches!(concrete_id.suffix, Some(ReservedSuffix::Pre)))
+    }
+
+    /// Returns true if the underlying identifier has the postcondition suffix
+    /// Should be removed once https://github.com/cryspen/hax/issues/1646 has been fixed
+    pub fn is_postcondition(&self) -> bool {
+        matches!(self, GlobalIdInner::Concrete(concrete_id) if matches!(concrete_id.suffix, Some(ReservedSuffix::Post)))
+    }
 }
 
 impl ConcreteId {