feat(lean) turn rejection phase into a transformation phase

CHANGELOG.md

@@ -51,6 +51,7 @@ Changes to the Lean backend:
  - Add support for nonliteral array sizes (#1826)
  - Add `hax_lib::lean::proof` attribute (#1831)
  - Add support for `#[hax_lib::opaque]` (#1846)
+ - Turn rejection phase into a transformation phase (#1840)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)

rust-engine/src/backends/lean.rs

@@ -143,7 +143,7 @@ impl Backend for LeanBackend {
     }
 
     fn phases(&self) -> Vec<Box<dyn Phase>> {
-        vec![Box::new(RejectNotDoLeanDSL), Box::new(ExplicitMonadic)]
+        vec![Box::new(ExplicitMonadic)]
     }
 }
 

rust-engine/src/phase/explicit_monadic.rs

@@ -115,26 +115,22 @@ impl ExplicitMonadicVisitor {
                 [Some(then), else_.as_mut()]
                     .into_iter()
                     .flatten()
-                    // The constraint is propagated on each branch
-                    .for_each(|branch| self.visit_expr_coerce(constraint, branch));
-                // No need to coerce the `If` node itself, the coercion is propagated on branches
-                None
+                    .for_each(|branch| self.visit_expr_coerce(MonadicStatus::Computation, branch));
+                Some(MonadicStatus::Computation)
             }
             ExprKind::Match { scrutinee, arms } => {
                 self.visit_expr_coerce(MonadicStatus::Value, scrutinee);
-                arms.iter_mut()
-                    // The constraint is propagated on each arm
-                    .for_each(|arm| {
-                        if let Some(Guard {
-                            kind: GuardKind::IfLet { rhs, .. },
-                            ..
-                        }) = &mut arm.guard
-                        {
-                            self.visit_expr_coerce(MonadicStatus::Value, rhs);
-                        };
-                        self.visit_expr_coerce(constraint, &mut arm.body)
-                    });
-                None
+                arms.iter_mut().for_each(|arm| {
+                    if let Some(Guard {
+                        kind: GuardKind::IfLet { rhs, .. },
+                        ..
+                    }) = &mut arm.guard
+                    {
+                        self.visit_expr_coerce(MonadicStatus::Value, rhs);
+                    };
+                    self.visit_expr_coerce(MonadicStatus::Computation, &mut arm.body)
+                });
+                Some(MonadicStatus::Computation)
             }
             ExprKind::Block { body, .. } => {
                 self.visit_expr_coerce(constraint, body);

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

@@ -11,7 +11,7 @@ info:
     description: ~
   spec:
     optional: false
-    broken: true
+    broken: false
     issue_id: ~
     positive: true
     snapshot:
@@ -20,61 +20,11 @@ info:
     include_flag: ~
     backend_options: ~
 ---
-exit = 1
-stderr = """
-Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs
-\u001B[1m\u001B[91merror\u001B[0m: \u001B[1m[HAX0008] Explicit rejection by a phase in the Hax engine:
-This interleaving of expression and statements does not fit in Lean's do-notation DSL.
-You may try hoisting out let-bindings and control-flow.
-
-This is discussed in issue https://github.com/hacspec/hax/issues/1741.
-Please upvote or comment this issue if you see this error message.
-Note: the error was labeled with context `Engine phase (RejectNotDoLeanDSL)`.
-\u001B[0m
- \u001B[1m\u001B[94m-->\u001B[0m lean-tests/src/reject_do_dsl.rs:6:18
-  \u001B[1m\u001B[94m|\u001B[0m
-\u001B[1m\u001B[94m6 |\u001B[0m     let x1 = 1 + (if true { 0 } else { 1 });
-  \u001B[1m\u001B[94m|\u001B[0m                  \u001B[1m\u001B[91m^^^^^^^^^^^^^^^^^^^^^^^^^^\u001B[0m
-  \u001B[1m\u001B[94m|\u001B[0m
-\u001B[1m\u001B[91merror\u001B[0m: \u001B[1m[HAX0008] Explicit rejection by a phase in the Hax engine:
-This interleaving of expression and statements does not fit in Lean's do-notation DSL.
-You may try hoisting out let-bindings and control-flow.
-
-This is discussed in issue https://github.com/hacspec/hax/issues/1741.
-Please upvote or comment this issue if you see this error message.
-Note: the error was labeled with context `Engine phase (RejectNotDoLeanDSL)`.
-\u001B[0m
-  \u001B[1m\u001B[94m-->\u001B[0m lean-tests/src/reject_do_dsl.rs:8:11
-   \u001B[1m\u001B[94m|\u001B[0m
-\u001B[1m\u001B[94m 8 |\u001B[0m           + (match (1, 2) {
-   \u001B[1m\u001B[94m|\u001B[0m  \u001B[1m\u001B[91m___________^\u001B[0m
-\u001B[1m\u001B[94m 9 |\u001B[0m \u001B[1m\u001B[91m|\u001B[0m             _ => 0,
-\u001B[1m\u001B[94m10 |\u001B[0m \u001B[1m\u001B[91m|\u001B[0m         });
-   \u001B[1m\u001B[94m|\u001B[0m \u001B[1m\u001B[91m|__________^\u001B[0m
-   \u001B[1m\u001B[94m|\u001B[0m"""
-[[stdout.diagnostics]]
-message = """
-Explicit rejection by a phase in the Hax engine:
-This interleaving of expression and statements does not fit in Lean's do-notation DSL.
-You may try hoisting out let-bindings and control-flow.
-
-This is discussed in issue https://github.com/hacspec/hax/issues/1741.
-Please upvote or comment this issue if you see this error message.
-\u001B[90mNote: the error was labeled with context `Engine phase (RejectNotDoLeanDSL)`.
-\u001B[0m"""
-spans = ['Span { lo: Loc { line: 6, col: 17 }, hi: Loc { line: 6, col: 43 }, filename: Real(LocalPath("lean-tests/src/reject_do_dsl.rs")), rust_span_data: None }']
-
-[[stdout.diagnostics]]
-message = """
-Explicit rejection by a phase in the Hax engine:
-This interleaving of expression and statements does not fit in Lean's do-notation DSL.
-You may try hoisting out let-bindings and control-flow.
-
-This is discussed in issue https://github.com/hacspec/hax/issues/1741.
-Please upvote or comment this issue if you see this error message.
-\u001B[90mNote: the error was labeled with context `Engine phase (RejectNotDoLeanDSL)`.
-\u001B[0m"""
-spans = ['Span { lo: Loc { line: 8, col: 10 }, hi: Loc { line: 10, col: 10 }, filename: Real(LocalPath("lean-tests/src/reject_do_dsl.rs")), rust_span_data: None }']
+exit = 0
+stderr = 'Finished `dev` profile [unoptimized + debuginfo] target(s) in XXs'
+
+[stdout]
+diagnostics = []
 
 [stdout.files]
 "Lean_tests.lean" = '''
@@ -1573,18 +1523,26 @@ abbrev Lean_tests.Types.ESMonad
   (A : Type) (S : Type) (E : Type) : Type :=
   (Rust_primitives.Hax.Tuple2 (Core.Result.Result A E) S)
 
-def Lean_tests.Reject_do_dsl.rejected
+opaque Lean_tests.Opaque.an_opaque_fn
+  (_ : Rust_primitives.Hax.Tuple0)
+  : RustM Rust_primitives.Hax.Tuple0
+
+
+def Lean_tests.Nested_control_flow.nested_control_flow
   (_ : Rust_primitives.Hax.Tuple0)
   : RustM Rust_primitives.Hax.Tuple0
   := do
-  let x1 : i32 ← ((1 : i32) +? sorry);
-  let x2 : i32 ← ((1 : i32) +? sorry);
+  let x1 : i32 ←
+    ((1 : i32) +? (← if true then (pure (0 : i32)) else (pure (1 : i32))));
+  let x2 : i32 ←
+    ((1 : i32)
+      +? (← match (Rust_primitives.Hax.Tuple2.mk (1 : i32) (2 : i32)) with
+        | _ => (pure (0 : i32))));
   let x : i32 := (9 : i32);
   let x3 : i32 ← ((1 : i32) +? (← (x +? (1 : i32))));
   (pure Rust_primitives.Hax.Tuple0.mk)
 
---  Code that should be produced from the rejected code
-def Lean_tests.Reject_do_dsl.accepted
+def Lean_tests.Nested_control_flow.explicit_hoisting
   (_ : Rust_primitives.Hax.Tuple0)
   : RustM Rust_primitives.Hax.Tuple0
   := do
@@ -1599,7 +1557,7 @@ def Lean_tests.Reject_do_dsl.accepted
   let x3 : i32 ← ((1 : i32) +? x3_tmp);
   (pure Rust_primitives.Hax.Tuple0.mk)
 
-def Lean_tests.Reject_do_dsl.test
+def Lean_tests.Nested_control_flow.complex_nesting
   (_ : Rust_primitives.Hax.Tuple0)
   : RustM
   (Rust_primitives.Hax.Tuple2
@@ -1649,11 +1607,6 @@ 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/Cargo.toml

@@ -7,4 +7,4 @@ edition = "2021"
 hax-lib = { path = "../../hax-lib" }
 
 [package.metadata.hax-tests]
-into."lean" = { broken = true }
+into."lean" = { broken = false }

tests/lean-tests/src/lib.rs

@@ -11,8 +11,8 @@ pub mod ite;
 pub mod loops;
 pub mod matching;
 pub mod monadic;
+pub mod nested_control_flow;
 pub mod opaque;
-pub mod reject_do_dsl;
 pub mod specs;
 pub mod structs;
 pub mod traits;

tests/lean-tests/src/reject_do_dsl.rs → tests/lean-tests/src/nested_control_flow.rs

@@ -1,8 +1,8 @@
-//! Tests on patterns rejected by the engine as outside of Lean's do-notation DSL
+//! Tests for nested control flow in expressions
 #![allow(dead_code)]
 #![allow(unused_variables)]
 
-fn rejected() {
+fn nested_control_flow() {
     let x1 = 1 + (if true { 0 } else { 1 });
     let x2 = 1
         + (match (1, 2) {
@@ -14,8 +14,7 @@ fn rejected() {
     };
 }
 
-/// Code that should be produced from the rejected code
-fn accepted() {
+fn explicit_hoisting() {
     let x1_tmp = if true { 0 } else { 1 };
     let x1 = 1 + x1_tmp;
     let x2_tmp = match (1, 2) {
@@ -27,8 +26,7 @@ fn accepted() {
     let x3 = 1 + x3_tmp;
 }
 
-// Other cases that should be accepted
-fn test() {
+fn complex_nesting() {
     let mut x1 = if true {
         let mut y = if false {
             let mut z = match () {