feat(lean): Use FunctionsToConstants

CHANGELOG.md

@@ -16,6 +16,7 @@ Change to cargo-hax:
 Changes to hax-lib:
 
 Changes to the Lean backend:
+- Support for constants with arbitrary computation (#1738)
 
 Miscellaneous:
 

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

@@ -65,6 +65,14 @@ def ofOption {α} (x:Option α) (e: Error) : Result α := match x with
   | .some v => pure v
   | .none => .fail e
 
+@[reducible]
+def isOk {α : Type} (x: Result α) : Bool := match x with
+| .ok _ => true
+| _ => false
+
+def of_isOk {α : Type} (x: Result α) (h: Result.isOk x): α :=
+by cases x <;> try simp_all <;> assumption
+
 @[simp]
 instance instMonad : Monad Result where
   pure := pure
@@ -118,7 +126,6 @@ instance instWPMonad : WPMonad Result (.except Error .pure) where
 instance instCoe {α} : Coe α (Result α) where
   coe x := pure x
 
-
 @[simp, spec, default_instance]
 instance {α} : Coe (Result (Result α)) (Result α) where
   coe x := match x with

rust-engine/src/backends/lean.rs

@@ -97,19 +97,22 @@ impl RenderView for LeanPrinter {
 
 impl Printer for LeanPrinter {
     fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
-        vec![Box::new(BinOp::new(&[
-            binops::add,
-            binops::sub,
-            binops::mul,
-            binops::rem,
-            binops::div,
-            binops::shr,
-            binops::bitand,
-            binops::bitxor,
-            binops::logical_op_and,
-            binops::logical_op_or,
-            binops::Index::index,
-        ]))]
+        vec![
+            Box::new(BinOp::new(&[
+                binops::add,
+                binops::sub,
+                binops::mul,
+                binops::rem,
+                binops::div,
+                binops::shr,
+                binops::bitand,
+                binops::bitxor,
+                binops::logical_op_and,
+                binops::logical_op_or,
+                binops::Index::index,
+            ])),
+            Box::new(FunctionsToConstants),
+        ]
     }
 }
 
@@ -139,6 +142,11 @@ impl LeanPrinter {
                 params: _,
                 safety: _,
             } if name.is_anonymous_const() => false,
+            ItemKind::Resugared(ResugaredItemKind::Constant {
+                name,
+                body: _,
+                generics: _,
+            }) if name.is_anonymous_const() => false,
             // Other unprintable items
             ItemKind::Error(_) | ItemKind::NotImplementedYet | ItemKind::Use { .. } => false,
             // Printable items
@@ -847,29 +855,23 @@ set_option linter.unusedVariables false
                     body,
                     params,
                     safety: _,
-                } => match &*body.kind {
-                    // TODO: Literal consts. This should be done by a resugaring, see
-                    // https://github.com/cryspen/hax/issues/1614
-                    ExprKind::Literal(l) if params.is_empty() => {
-                        docs!["def ", name, reflow!(" : "), &body.ty, reflow!(" := "), l].group()
-                    }
-                    _ => docs![
-                        docs![
-                            docs!["def", line!(), name].group(),
-                            line!(),
-                            generics,
-                            params,
-                            docs![": Result", line!(), &body.ty].group(),
-                            line!(),
-                            ":= do"
-                        ]
-                        .group(),
+                } => docs![
+                    docs![
+                        docs!["def", line!(), name].group(),
+                        line!(),
+                        generics,
+                        params,
+                        docs![": Result", line!(), &body.ty].group(),
                         line!(),
-                        body
+                        ":= do"
                     ]
-                    .group()
-                    .nest(INDENT),
-                },
+                    .group(),
+                    line!(),
+                    body
+                ]
+                .group()
+                .nest(INDENT),
+
                 ItemKind::TyAlias {
                     name,
                     generics: _,
@@ -1017,9 +1019,33 @@ set_option linter.unusedVariables false
                     .nest(INDENT),
                 ],
                 ItemKind::Resugared(resugared_item_kind) => match resugared_item_kind {
-                    ResugaredItemKind::Constant { .. } => {
-                        unreachable!("This backend does not use constant resugaring")
-                    }
+                    ResugaredItemKind::Constant {
+                        name,
+                        body,
+                        generics,
+                    } => docs![
+                        docs![
+                            docs!["def", line!(), name].group(),
+                            line!(),
+                            generics,
+                            docs![":", line!(), &body.ty].group(),
+                            line!(),
+                            ":="
+                        ]
+                        .group(),
+                        line!(),
+                        docs![
+                            "Result.of_isOk",
+                            line!(),
+                            docs!["do ", body].group().parens(),
+                            line!(),
+                            "(by rfl)"
+                        ]
+                        .group()
+                        .nest(INDENT)
+                    ]
+                    .group()
+                    .nest(INDENT),
                 },
                 ItemKind::Alias { .. } => {
                     // aliases are introduced when creating bundles. Those should not appear in

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

@@ -538,9 +538,38 @@ def Lean_tests.Enums.enums
     | (Lean_tests.Enums.E.V6 (f1 := f1) (f2 := other_name_for_f2))
       => do Rust_primitives.Hax.Tuple0.mk)
 
-def Lean_tests.FORTYTWO : usize := 42
+def Lean_tests.Constants.C1 : u32 := Result.of_isOk (do (5678 : u32)) (by rfl)
 
-def Lean_tests.MINUS_FORTYTWO : isize := -42
+def Lean_tests.Constants.C2 : u32 :=
+  Result.of_isOk (do (← Lean_tests.Constants.C1 +? (1 : u32))) (by rfl)
+
+def Lean_tests.Constants.C3 : u32 :=
+  Result.of_isOk
+    (do (← if true then do (890 : u32) else do (← (9 : u32) /? (0 : u32))))
+    (by rfl)
+
+def Lean_tests.Constants.computation (x : u32) : Result u32 := do
+  (← (← x +? x) +? (1 : u32))
+
+def Lean_tests.Constants.C4 : u32 :=
+  Result.of_isOk
+    (do (← (← Lean_tests.Constants.computation Lean_tests.Constants.C1)
+      +? Lean_tests.Constants.C2))
+    (by rfl)
+
+def Lean_tests.Constants.test
+  (_ : Rust_primitives.Hax.Tuple0)
+  : Result Rust_primitives.Hax.Tuple0
+  := do
+  let x : u32 ← (pure (← Lean_tests.Constants.C1 +? (1 : u32)));
+  let y : u32 ← (pure (← Lean_tests.Constants.C2 +? Lean_tests.Constants.C3));
+  let z : u32 ← (pure (← Lean_tests.Constants.C4 -? Lean_tests.Constants.C3));
+  Rust_primitives.Hax.Tuple0.mk
+
+def Lean_tests.FORTYTWO : usize := Result.of_isOk (do (42 : usize)) (by rfl)
+
+def Lean_tests.MINUS_FORTYTWO : isize :=
+  Result.of_isOk (do (-42 : isize)) (by rfl)
 
 def Lean_tests.returns42 (_ : Rust_primitives.Hax.Tuple0) : Result usize := do
   Lean_tests.FORTYTWO

tests/lean-tests/src/constants.rs

@@ -0,0 +1,19 @@
+// Tests on constants
+#![allow(dead_code)]
+#![allow(unused_variables)]
+
+const C1: u32 = 5678;
+const C2: u32 = C1 + 1;
+const C3: u32 = if true { 890 } else { 9 / 0 };
+
+const fn computation(x: u32) -> u32 {
+    x + x + 1
+}
+
+const C4: u32 = computation(C1) + C2;
+
+fn test() {
+    let x = C1 + 1;
+    let y = C2 + C3;
+    let z = C4 - C3;
+}

tests/lean-tests/src/lib.rs

@@ -2,6 +2,7 @@
 #![allow(unused_variables)]
 
 pub mod comments;
+pub mod constants;
 pub mod enums;
 pub mod ite;
 pub mod loops;