Lean backend [M2] - 1/3 - First proofs

[clementblaudeau]

This PR contains a first set of improvements of the Lean backend, made towards the proof of the barrett and chacha20 examples. The second set of improvements relies on visitors and is separated #1591. The example proofs are in #1593

Context

This PR follows #1509 and improves the Lean backend for Hax. It should still be considered experimental, and might be subjected to change in the future. The effort of this PR was mainly focused on improving the Lean prelude library for proofs, rather than extending the subset of rust supported by the Lean backend.

While the F* backend of Hax relies on an intrinsic proof style (via the pervasive use of the SMT), the Lean backend uses (1) an extrinsic style, achieved via (2) a monadic encoding. In other words, (1) the proofs are written separately from the definitions and (2) the extracted rust code is wrapped in a Result monad to represent the fact that rust computations are actually partial (they can panic), unlike Lean ones.

Example

Barrett reduction

The Barrett reduce function is extracted as :

@[simp, spec]
def barrett_reduce (value : i32) : Result i32 := do
  let (t : i64) ← (← hax_machine_int_mul
    (← convert_From_from value)
      BARRETT_MULTIPLIER);
  let (t : i64) ← (← t +? (← hax_machine_int_shr BARRETT_R 1));
  let (quotient : i64) ← (← hax_machine_int_shr t BARRETT_SHIFT);
  let (quotient : i32) ← (← hax_cast_op quotient);
  let (sub : i32) ← (← hax_machine_int_mul quotient FIELD_MODULUS);
  (← hax_machine_int_sub value sub)

Its specification can be written as the following Hoare triple:

theorem barrett_spec (value: i32) :
  ⦃ __requires (value) = pure true ⦄
  (barrett_reduce value)
  ⦃ ⇓ result => __ensures value result = pure true ⦄

where __requires and __ensures are extracted from the hax attributes in the rust code.

Details

1. The Result monad and error cases are borrowed from the Aeneas project
2. The specifications are written using Hoare triples as defined is the Lean standard library (Std.Do.Triple). See this discussion for details on the monadic encoding and mvcgen tactic, recently added to Lean

Goals

• Lean prelude
  • Panicking arithmetic operations with bitvec specifications
  • Exectuable model for Arrays and Vectors
  • Specification for hax folds (for loops)
  • General documentation of the Lean.lib file
• [ ] Examples Moved to Lean backend [M2] - 2/3 - Examples #1593
• Backend
  • Demo the resugaring on addition: hax_machine_int_add is replaced by +? (other resugaring will be done with visitors)
  • Print disambiguators for trait implementations
  • Support #[hax_lib::lean::..] attributes in Rust
• Other
  • Update changelog
  • Extend lean tests

[maximebuyse]

Generally looks good. I added a couple of comments. Didn't look too deeply into the lean code but it seems nice and well-documented.

[karthikbhargavan]

I reviewed the library and the proofs, they look good.
There is a small amount of Rust changes here, worth a quick look.

[jschneider-bensch]

I've left some comments, mostly questions for my understanding.

[clementblaudeau]

Thank you for the review. I've answered to your comments @jschneider-bensch: I've left some unresolved so you can confirm that it works for you.

[jschneider-bensch]

With the changes coming in the follow up PRs, this looks good to me.

A small request for the future: If there's a chain of PRs with earlier ones introducing temporary fixes or constructs, it would help me if there were comments referencing the work/issues that will address the temporary things. That would make it easier for me to review the PRs on their own.