Lean backend [M2] - 2/3 - Examples

[clementblaudeau]

This PR is a follow-up of #1590. It introduces two specific examples to showcase the lean backend in examples/lean_barrett and example/lean_chacha20. For both, the lean extraction can be obtained by running cargo hax into lean

Barrett

The Barrett reduction allows to compute remainders without using divisions. It showcases arithmetic operations, conversions between integer types (namely i32 and i64). Specifically, the Lean backend provides panicking arithmetic operations +?, -?, etc, that panic on overflows.

For the Lean extracted code, we prove panic freedom with regards to those arithmetic operations, and then we prove that the result is indeed the modulus (as long as the absolute value of the input is lower than the bound BARRETT_R). The proof is made via bit-blasting (using Lean's bv_decide). To limit the computation time, the bound BARRETT_R was lowered compared to the normal example in the barrett folder.

The proofs are backported in the rust code (in lean_barrett/src/lib.rs): doing cargo hax into lean extracts a valid lean file that contains the proof.

Chacha20

The Chacha20 example extracts to Lean, but requires a manual edit to be wellformed (will be removed via resugarings #1591). It showcases array, vector and slices accesses, as well as loops (with loop invariants).

For the Lean extracted code, we prove panic freedom. It is not backported in rust yet.

This edit and the proofs of panic freedom can be found in lean_chacha20/proofs/lean/extraction/lean_chacha20_manual_edit.lean.

[karthikbhargavan]

We reviewed the proofs together last week and they look great.
This is mainly a Lean PR and shouldn't require much Rust review.

[W95Psp]

I'm looking into the nix issue

Edit: I got no much time to look at it, let's postpone this.

[W95Psp]

Thanks! I've been the code, it looks nice to me!
I checked the lean_barrett example, it works fine on my laptop :)

[W95Psp]

🎉 CI is happy

[clementblaudeau]

I've rebased to squash the commits about CI, and will merge as soon as it passes.