feat(lean): Add support for #[hax_lib::opaque]

CHANGELOG.md

@@ -48,6 +48,7 @@ Changes to the Lean backend:
  - Add generation of specs from requires/ensures-annotations (#1815)
  - Add support for nonliteral array sizes (#1826)
  - Add `hax_lib::lean::proof` attribute (#1831)
+ - Add support for `#[hax_lib::opaque]` (#1846)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)

hax-lib/proof-libs/lean/Hax/Lib.lean

@@ -50,7 +50,7 @@ inductive RustM.{u} (α : Type u) where
   | ok (v: α): RustM α
   | fail (e: Error): RustM α
   | div
-deriving Repr, BEq, DecidableEq
+deriving Repr, BEq, DecidableEq, Inhabited
 
 namespace RustM
 

rust-engine/src/ast.rs

@@ -1483,6 +1483,18 @@ pub struct Item {
     pub meta: Metadata,
 }
 
+impl Item {
+    /// Checks whether the item was marked opaque using `hax_lib::opaque`
+    pub fn is_opaque(&self) -> bool {
+        self.meta.attributes.iter().any(|a| {
+            matches!(
+                a.kind,
+                AttributeKind::Hax(hax_lib_macros_types::AttrPayload::Erased)
+            )
+        })
+    }
+}
+
 /// A "flat" module: this contains only non-module items.
 #[derive_group_for_ast]
 pub struct Module {

rust-engine/src/backends/lean.rs

@@ -1161,20 +1161,20 @@ set_option linter.unusedVariables false
                     params,
                     safety: _,
                 } => {
+                    let opaque = item.is_opaque();
                     docs![
                         docs![
                             docs![
-                                docs!["def", line!(), name].group(),
+                                docs![if opaque { "opaque" } else { "def" }, line!(), name].group(),
                                 line!(),
                                 generics,
                                 params,
                                 docs![": RustM", line!(), &body.ty].group(),
                                 line!(),
-                                ":= do"
+                                if opaque { nil!() } else { docs![":= do"] }
                             ]
                             .group(),
-                            line!(),
-                            body
+                            if opaque { nil!() } else { docs![line!(), body] }
                         ]
                         .group()
                         .nest(INDENT),

test-harness/src/snapshots/toolchain__lean-tests into-lean.snap

@@ -1490,6 +1490,11 @@ def Lean_tests.Reject_do_dsl.test
   (pure (Rust_primitives.Hax.Tuple2.mk
     Rust_primitives.Hax.Tuple0.mk Rust_primitives.Hax.Tuple0.mk))
 
+opaque Lean_tests.Opaque.an_opaque_fn
+  (_ : Rust_primitives.Hax.Tuple0)
+  : RustM Rust_primitives.Hax.Tuple0
+
+
 def Lean_tests.Matching.test_const_matching
   (x : u32)
   (c : Char)

tests/lean-tests/src/lib.rs

@@ -11,6 +11,7 @@ pub mod ite;
 pub mod loops;
 pub mod matching;
 pub mod monadic;
+pub mod opaque;
 pub mod reject_do_dsl;
 pub mod specs;
 pub mod structs;

tests/lean-tests/src/opaque.rs

@@ -0,0 +1,2 @@
+#[hax_lib::opaque]
+pub fn an_opaque_fn() {}