feat(rust-engine/lean): monadic phase

[clementblaudeau]

This PR adds a new phase to the rust-engine (and use it in the Lean backend) to handle the monadic encoding.

Overview

• Add a phase to insert pure (for values when a computation is expected) and lift nodes (for computations when a value is expected)
• Add a resugaring for let x ← pure .. into let x := ..
• Update Chacha example to remove all manual edits

Example

The following rust code (from the tests/lean-tests/src/monadic.rs file) displays interleaving of computations and values. Bellow is the extracted Lean code.

struct S {
    f: u32,
}

fn test() {
    let _ = 9; // value
    let _ = 9 + 9; // computation
    let _ = S { f: 9 }; // constructors are values
    let _ = S { f: 9 + 9 }; // computation within a value
    let _ = (S { f: 9 + 9 }).f; // projections are values
    let _ = (S { f: 9 + 9 }).f + 9; // projections are values
    let _ = if true { 3 + 4 } else { 3 - 4 }; // ite expects value for condition
    let _ = if (9 + 9 == 0) { 3 + 4 } else { 3 - 4 }; // ite expects value for condition
    let _ = if true {
        let x = 9;
        3 + x;
    } else {
        let y = 19;
        3 + y - 4;
    };
}

structure S where
  f : u32

def test (_ : Rust_primitives.Hax.Tuple0) : Result Rust_primitives.Hax.Tuple0 := do
  let _ := (9 : i32); -- value, use `let _ := `
  let _ ← ((9 : i32) +? (9 : i32)); -- computation, use `let _ ←`
  let _ := (S.mk (f := (9 : u32)));
  let _ := (S.mk (f := (← ((9 : u32) +? (9 : u32)))));
  let _ := (S.f (S.mk (f := (← ((9 : u32) +? (9 : u32))))));
  let _ ← ((S.f (S.mk (f := (← ((9 : u32) +? (9 : u32)))))) +? (9 : u32));
  let _ ← if true then ((3 : i32) +? (4 : i32)) else ((3 : i32) -? (4 : i32));
  let _ ←
    if (← (Rust_primitives.Hax.Machine_int.eq (← ((9 : i32) +? (9 : i32))) (0 : i32))) then
      ((3 : i32) +? (4 : i32))
    else
      ((3 : i32) -? (4 : i32));
  let _ ←
    if true then
      let x : i32 := (9 : i32);
      let _ ← ((3 : i32) +? x);
      (pure Rust_primitives.Hax.Tuple0.mk)
    else
      let y : i32 := (19 : i32);
      let _ ← ((← ((3 : i32) +? y)) -? (4 : i32));
      (pure Rust_primitives.Hax.Tuple0.mk);
  (pure Rust_primitives.Hax.Tuple0.mk)

Context

Monadic phase

The Lean backend translates rust programs in a monadic style, where each rust computation that could panic is wrapped inside a Result monad : a function fn f(x:u32) -> u32 will be extracted to def f (x:u32) : Result u32. There are two challenges in this encoding :

1. Some expressions cannot panic (literals, consts, constructors for enums, etc) and should be wrapped in the monad. This phase inserts explicit calls to a new Hax primitive pure. The Lean backend translates it directly to the pure operator. While lean also has coercions that could be inserted implicitely, they could badly interact with inference, so making them explicit is more robust.

2. Language constructs (if-then-else, match, etc.) and rust functions, when translated in Lean, still expect rust values as input, not monadic computations. This phase inserts explicit calls to lift to materialize the sub-expressions that return a monadic result where a value is expected. The Lean backend turns them into explicit lifts (← ..), which introduces a monadic bind.

Resugaring

Let-bindings of the form let x = pure e (after the monadic phase) are not extracted as let x ← pure e, but shortened into let x := e. The subexpression e was already outside the do-dsl.

Chacha example

The example has been revisited to remove the manually edited file. To circumvent a bug with quotes attached to macro items, and as i32 loops are not supported yet, a couple of manual edits were also made to the rust files (besides the backport of the proofs).

[maximebuyse]

Looks good! I added a few comments about rust style but the documentation looks good and this phase is a great improvement!

[jschneider-bensch]

Looks good overall, I think 👍
Just some comments

[clementblaudeau]

Thank you for the reviews! Let's merge.