feat(lean): support for const parameters

CHANGELOG.md

@@ -36,6 +36,7 @@ Changes to the Lean backend:
  - Add support for pattern matching on constant literals (#1789)
  - Add support for binding subpatterns in match constructs (#1790)
  - Add error when using patterns in function parameters (#1792)
+ - Add support for constant parameters to functions and traits (#1797)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)

rust-engine/src/backends/lean.rs

@@ -335,6 +335,30 @@ const _: () = {
         ) -> String {
             format!("_constr_{}_{}", associated_type_name, constraint.name)
         }
+
+        /// Turns an expression of type `RustM T` into one of type `T` (out of the monad), providing
+        /// reflexivity as a proof witness.
+        fn monad_extract<A: 'static + Clone>(&self, expr: &Expr) -> DocBuilder<A> {
+            match *expr.kind() {
+                ExprKind::Literal(_) | ExprKind::GlobalId(_) | ExprKind::LocalId(_) => {
+                    // Pure values are displayed directly. Note that constructors, while pure, may
+                    // contain sub-expressions that are not, so they must be wrapped in a do-block
+                    docs![expr]
+                }
+                _ => {
+                    // All other expressions are wrapped in a do-block, and extracted out of the monad
+                    docs![
+                        "RustM.of_isOk",
+                        line!(),
+                        self.do_block(expr).parens(),
+                        line!(),
+                        "(by rfl)"
+                    ]
+                    .group()
+                    .nest(INDENT)
+                }
+            }
+        }
     }
 
     impl<A: 'static + Clone> PrettyAst<A> for LeanPrinter {
@@ -423,9 +447,17 @@ set_option linter.unusedVariables false
                     .parens()
                     .group(),
                 GenericParamKind::Lifetime => unreachable_by_invariant!(Drop_references),
-                GenericParamKind::Const { .. } => {
-                    emit_error!(issue 1711, "Const parameters are not yet supported")
-                }
+                GenericParamKind::Const { ty } => docs![&generic_param.ident, reflow!(" : "), ty]
+                    .parens()
+                    .group(),
+            }
+        }
+
+        fn generic_value(&self, generic_value: &GenericValue) -> DocBuilder<A> {
+            match generic_value {
+                GenericValue::Ty(ty) => docs![ty],
+                GenericValue::Expr(expr) => docs![self.monad_extract(expr)].parens(),
+                GenericValue::Lifetime => unreachable_by_invariant!(Drop_references),
             }
         }
 
@@ -463,15 +495,14 @@ set_option linter.unusedVariables false
                         }
                         _ => {
                             // Fallback for any application
-                            let generic_args = (!generic_args.is_empty()).then_some(
-                                docs![line!(), intersperse!(generic_args, line!())].group(),
-                            );
-                            let args = (!args.is_empty())
-                                .then_some(docs![line!(), intersperse!(args, line!())].group());
-                            docs![head, generic_args, args]
-                                .parens()
-                                .nest(INDENT)
-                                .group()
+                            docs![
+                                head,
+                                zip_left!(line!(), generic_args).group(),
+                                zip_left!(line!(), args).group(),
+                            ]
+                            .parens()
+                            .nest(INDENT)
+                            .group()
                         }
                     }
                 }
@@ -840,14 +871,6 @@ set_option linter.unusedVariables false
             }]
         }
 
-        fn generic_value(&self, generic_value: &GenericValue) -> DocBuilder<A> {
-            match generic_value {
-                GenericValue::Ty(ty) => docs![ty],
-                GenericValue::Expr(expr) => docs![expr],
-                GenericValue::Lifetime => unreachable_by_invariant!(Drop_references),
-            }
-        }
-
         fn quote_content(&self, quote_content: &QuoteContent) -> DocBuilder<A> {
             match quote_content {
                 QuoteContent::Verbatim(s) => {
@@ -1065,15 +1088,7 @@ set_option linter.unusedVariables false
                         ]
                         .group(),
                         line!(),
-                        docs![
-                            "RustM.of_isOk",
-                            line!(),
-                            self.do_block(body).parens(),
-                            line!(),
-                            "(by rfl)"
-                        ]
-                        .group()
-                        .nest(INDENT)
+                        self.monad_extract(body),
                     ]
                     .group()
                     .nest(INDENT),

rust-engine/src/phase/explicit_monadic.rs

@@ -233,4 +233,10 @@ impl AstVisitorMut for ExplicitMonadicVisitor {
             self.visit_expr_coerce(MonadicStatus::Value, length);
         };
     }
+
+    fn visit_generic_value(&mut self, x: &mut GenericValue) {
+        if let GenericValue::Expr(expr) = x {
+            self.visit_expr_coerce(MonadicStatus::Value, expr);
+        };
+    }
 }

rustfmt.toml

@@ -1 +1,2 @@
 style_edition = "2024"
+edition="2024"

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

@@ -91,6 +91,68 @@ open Std.Tactic
 set_option mvcgen.warning false
 set_option linter.unusedVariables false
 
+class Lean_tests.Traits.Trait_level_args.T1
+  (Self : Type) (A : Type) (B : Type)
+  where
+  f1 (C : Type) (D : Type) : (Self -> RustM Rust_primitives.Hax.Tuple0)
+  f2 (C : Type) (D : Type) : (Self -> A -> RustM Rust_primitives.Hax.Tuple0)
+  f3 (C : Type) (D : Type) :
+    (Self -> A -> B -> RustM Rust_primitives.Hax.Tuple0)
+
+instance Lean_tests.Traits.Trait_level_args.Impl :
+  Lean_tests.Traits.Trait_level_args.T1 usize u32 u64
+  where
+  f1 (C : Type) (D : Type) (self : usize) := do
+    (pure Rust_primitives.Hax.Tuple0.mk)
+  f2 (C : Type) (D : Type) (self : usize) (x : u32) := do
+    (pure Rust_primitives.Hax.Tuple0.mk)
+  f3 (C : Type) (D : Type) (self : usize) (x : u32) (y : u64) := do
+    (pure Rust_primitives.Hax.Tuple0.mk)
+
+
+/--
+error: Application type mismatch: The argument
+  x
+has type
+  U
+of sort `Type` but is expected to have type
+  Type
+of sort `Type 1` in the application
+  T1.f1 C D x
+---
+error: Application type mismatch: The argument
+  x
+has type
+  U
+of sort `Type` but is expected to have type
+  Type
+of sort `Type 1` in the application
+  T1.f2 C D x
+---
+error: failed to synthesize
+  T1 A ?m.19 C
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+
+def Lean_tests.Traits.Trait_level_args.test
+  (A : Type)
+  (B : Type)
+  (C : Type)
+  (D : Type)
+  (U : Type)
+  [(Lean_tests.Traits.Trait_level_args.T1 U A B)]
+  (x : U)
+  (a : A)
+  (b : B)
+  : RustM Rust_primitives.Hax.Tuple0
+  := do
+  let _ ← (Lean_tests.Traits.Trait_level_args.T1.f1 C D x);
+  let _ ← (Lean_tests.Traits.Trait_level_args.T1.f2 C D x a);
+  let _ ← (Lean_tests.Traits.Trait_level_args.T1.f3 C D x a b);
+  (pure Rust_primitives.Hax.Tuple0.mk)
+
 class Lean_tests.Traits.Overlapping_methods.T1 (Self : Type) where
   f : (Self -> RustM usize)
 
@@ -717,6 +779,96 @@ def Lean_tests.Enums.enums
     | (Lean_tests.Enums.E.V6 (f1 := f1) (f2 := other_name_for_f2))
       => (pure Rust_primitives.Hax.Tuple0.mk)
 
+--  Function with const parameter
+def Lean_tests.Constants.Const_parameters.f
+  (N : usize) (_ : Rust_primitives.Hax.Tuple0)
+  : RustM usize
+  := do
+  (pure N)
+
+def Lean_tests.Constants.Const_parameters.N0 : usize :=
+  RustM.of_isOk (do (pure (1 : usize))) (by rfl)
+
+def Lean_tests.Constants.Const_parameters.N1 : usize :=
+  RustM.of_isOk (do (pure (10 : usize))) (by rfl)
+
+def Lean_tests.Constants.Const_parameters.test
+  (_ : Rust_primitives.Hax.Tuple0)
+  : RustM Rust_primitives.Hax.Tuple0
+  := do
+  let _ ←
+    ((← (Lean_tests.Constants.Const_parameters.f ((9 : usize))
+        Rust_primitives.Hax.Tuple0.mk))
+      +? (← (Lean_tests.Constants.Const_parameters.f ((10 : usize))
+        Rust_primitives.Hax.Tuple0.mk)));
+  (pure Rust_primitives.Hax.Tuple0.mk)
+
+--  Trait definition
+class Lean_tests.Constants.Const_parameters.T
+  (Self : Type) (N_TRAIT : usize)
+  where
+  f (N_FIELD : usize) : (Self -> RustM usize)
+
+--  Struct definition
+structure Lean_tests.Constants.Const_parameters.S (N : usize) where
+  _0 : u32
+
+instance Lean_tests.Constants.Const_parameters.Impl (N_TRAIT : usize) :
+  Lean_tests.Constants.Const_parameters.T
+  (Lean_tests.Constants.Const_parameters.S (N_TRAIT))
+  (N_TRAIT)
+  where
+  f (N_FIELD : usize) (self :
+    (Lean_tests.Constants.Const_parameters.S (N_TRAIT)))
+    := do
+    (N_TRAIT -? N_FIELD)
+
+
+/--
+error: Application type mismatch: The argument
+  s
+has type
+  S 10
+but is expected to have type
+  usize
+in the application
+  T.f 1 s
+---
+error: Application type mismatch: The argument
+  x
+has type
+  A
+but is expected to have type
+  usize
+in the application
+  T.f 11 x
+---
+error: Application type mismatch: The argument
+  x
+has type
+  A
+but is expected to have type
+  usize
+in the application
+  T.f 4 x
+-/
+#guard_msgs in
+
+def Lean_tests.Constants.Const_parameters.test2
+  (N2 : usize) (A : Type) [(Lean_tests.Constants.Const_parameters.T A (N2))] (x
+  :
+  A)
+  : RustM usize
+  := do
+  let s : (Lean_tests.Constants.Const_parameters.S ((10 : usize))) :=
+    (Lean_tests.Constants.Const_parameters.S.mk (9 : u32));
+  let _ ←
+    ((← (Lean_tests.Constants.Const_parameters.T.f ((1 : usize)) s))
+      +? (← (Lean_tests.Constants.Const_parameters.T.f ((11 : usize)) x)));
+  let s : (Lean_tests.Constants.Const_parameters.S ((3 : usize))) :=
+    (Lean_tests.Constants.Const_parameters.S.mk (9 : u32));
+  (Lean_tests.Constants.Const_parameters.T.f ((4 : usize)) x)
+
 def Lean_tests.Constants.C1 : u32 :=
   RustM.of_isOk (do (pure (5678 : u32))) (by rfl)
 

tests/lean-tests/src/constants.rs

@@ -17,3 +17,71 @@ fn test() {
     let y = C2 + C3;
     let z = C4 - C3;
 }
+
+mod const_parameters {
+
+    /// Function with const parameter
+    fn f<const N: usize>() -> usize {
+        N
+    }
+
+    const N0: usize = 1;
+    const N1: usize = 10;
+
+    fn test() {
+        let _ = f::<9>() + f::<N1>();
+    }
+
+    /// Trait definition
+    trait T<const N_TRAIT: usize> {
+        fn f<const N_FIELD: usize>(&self) -> usize;
+    }
+
+    /// Struct definition
+    struct S<const N: usize>(u32);
+
+    impl<const N_TRAIT: usize> T<N_TRAIT> for S<N_TRAIT> {
+        fn f<const N_FIELD: usize>(&self) -> usize {
+            N_TRAIT - N_FIELD
+        }
+    }
+
+    #[hax_lib::lean::before(
+        "
+/--
+error: Application type mismatch: The argument
+  s
+has type
+  S 10
+but is expected to have type
+  usize
+in the application
+  T.f 1 s
+---
+error: Application type mismatch: The argument
+  x
+has type
+  A
+but is expected to have type
+  usize
+in the application
+  T.f 11 x
+---
+error: Application type mismatch: The argument
+  x
+has type
+  A
+but is expected to have type
+  usize
+in the application
+  T.f 4 x
+-/
+#guard_msgs in"
+    )]
+    fn test2<const N2: usize, A: T<N2>>(x: A) -> usize {
+        let s = S::<N1>(9);
+        let _ = s.f::<1>() + x.f::<{ 1 + N1 }>();
+        let s = S::<{ 1 + 2 }>(9);
+        x.f::<{ 2 + 2 }>()
+    }
+}