Lean backend [M2] - 2/3 - Examples

examples/Cargo.toml

@@ -1,6 +1,8 @@
 [workspace]
 members = [
     "chacha20",
+    "lean_chacha20",
+    "lean_barrett",
     "limited-order-book",
     "sha256",
     "barrett",
@@ -13,4 +15,3 @@ resolver = "2"
 [workspace.dependencies]
 hax-lib = { path = "../hax-lib" }
 hax-bounded-integers = { path = "../hax-bounded-integers" }
-

examples/Makefile

@@ -6,6 +6,8 @@ default:
 	make -C barrett
 	make -C kyber_compress
 	make -C proverif-psk
+	make -C lean_chacha20
+	make -C lean_barrett
 
 clean:
 	make -C limited-order-book clean
@@ -14,3 +16,5 @@ clean:
 	make -C barrett            clean
 	make -C kyber_compress     clean
 	make -C proverif-psk       clean
+	make -C lean_chacha20      clean
+	make -C lean_barrett       clean

examples/README.md

@@ -12,11 +12,11 @@
 
 <details>
   <summary><b>Requirements</b></summary>
-  
+
   First, make sure to have hax installed in PATH. Then:
-  
+
   * With Nix, `nix develop .#examples` setups a shell automatically for you.
-     
+
   * Without Nix:
     1. install F* `v2025.03.25`<!---FSTAR_VERSION--> manually (see https://github.com/FStarLang/FStar/blob/master/INSTALL.md);
        1. make sure to have `fstar.exe` in PATH;
@@ -39,3 +39,51 @@ Note the generated modules live in the
 
 For those examples, we generated Coq modules without typechecking them.
 The `<EXAMPLE>/proofs/coq/extraction` folders contain the generated Coq modules.
+
+## Lean
+
+Two examples are fine-tuned to showcase the Lean backend: `lean_barrett` and
+`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`). 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.
+
+The proof can be run by doing (requires `lake`):
+
+```sh
+cd lean_barrett/
+make
+```
+
+### Chacha20
+
+The Chacha20 example extracts to Lean, but requires a manual edit to be
+wellformed. It showcases array, vector and slices accesses, as well as loops
+(with loop invariants). For the Lean extracted code, we prove panic freedom,
+which involves arithmetic on size of arrays.
+
+This edit and the proofs of panic freedom can be found in
+`lean_chacha20/proofs/lean/extraction/lean_chacha20_manual_edit.lean`.
+
+The extraction (in `lean_chacha20.lean`) and rerun of the proofs (in
+`lean_chacha20_manual_edit.lean`) can be done by doing (requires `lake`):
+
+```sh
+cd lean_chacha20/
+make
+```

examples/lean_barrett/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "lean_barrett"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+hax-lib.workspace = true

examples/lean_barrett/Makefile

@@ -0,0 +1,8 @@
+.PHONY: default lean clean
+default:
+	cargo hax into lean
+	cd proofs/lean/extraction && lake build
+
+clean:
+	rm -f proofs/lean/extraction/lean_barrett.lean
+	cd proofs/lean/extraction && lake clean

examples/lean_barrett/proofs/lean/extraction/lakefile.toml

@@ -0,0 +1,10 @@
+name = "lean_barrett"
+version = "0.1.0"
+defaultTargets = ["lean_barrett"]
+
+[[lean_lib]]
+name = "lean_barrett"
+
+[[require]]
+name = "Hax"
+path = "../../../../../hax-lib/proof-libs/lean"

examples/lean_barrett/src/lib.rs

@@ -0,0 +1,73 @@
+use hax_lib as hax;
+use hax_lib::lean;
+
+/// Values having this type hold a representative 'x' of the Kyber field.
+/// We use 'fe' as a shorthand for this type.
+pub(crate) type FieldElement = i32;
+
+#[hax_lib::lean::before("@[simp, spec]")]
+const BARRETT_R: i64 = 0x400000; // is 0x4000000 in the normal barrett example
+
+#[hax_lib::lean::before("@[simp, spec]")]
+const BARRETT_SHIFT: i64 = 26;
+
+#[hax_lib::lean::before("@[simp, spec]")]
+const BARRETT_MULTIPLIER: i64 = 20159;
+
+#[hax_lib::lean::before("@[simp, spec]")]
+pub(crate) const FIELD_MODULUS: i32 = 3329;
+
+/// Signed Barrett Reduction
+///
+/// Given an input `value`, `barrett_reduce` outputs a representative `result`
+/// such that:
+///
+/// - result ≡ value (mod FIELD_MODULUS)
+/// - the absolute value of `result` is bound as follows:
+///
+/// `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)
+///
+/// In particular, if `|value| < BARRETT_R`, then `|result| < FIELD_MODULUS`.
+#[hax::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
+#[hax::ensures(|result| {
+  let valid_result = value % FIELD_MODULUS;
+  result > -FIELD_MODULUS
+  && result < FIELD_MODULUS
+  && (result == valid_result ||
+      result == valid_result + FIELD_MODULUS ||
+      result == valid_result - FIELD_MODULUS)
+})]
+#[hax_lib::lean::before("@[simp, spec]")]
+#[hax_lib::lean::after("
+theorem barrett_spec (value: i32) :
+  ⦃ __requires (value) = pure true ⦄
+  (barrett_reduce value)
+  ⦃ ⇓ result => __ensures value result = pure true ⦄
+:= by
+  mvcgen [__requires, __ensures]
+  hax_bv_decide
+  simp [__requires, __ensures] at *
+  rw [Int32.HaxRem_spec_bv_rw] ; simp ;
+  rw [Int32.HaxAdd_spec_bv_rw] ; simp ;
+  rw [Int32.HaxSub_spec_bv_rw] ; simp
+  hax_bv_decide
+  expose_names
+  have ⟨ h1, h2 ⟩ := h; clear h
+  simp [Int32.eq_iff_toBitVec_eq,
+          Int32.lt_iff_toBitVec_slt,
+          Int32.le_iff_toBitVec_sle,
+          Int64.eq_iff_toBitVec_eq,
+          Int64.lt_iff_toBitVec_slt,
+          Int64.le_iff_toBitVec_sle,
+          ] at *
+  generalize Int32.toBitVec value = bv_value at * ; clear value
+  bv_decide (config := {timeout := 120})
+")]
+pub fn barrett_reduce(value: FieldElement) -> FieldElement {
+    let t = i64::from(value) * BARRETT_MULTIPLIER;
+    let t = t + (BARRETT_R >> 1);
+    let quotient = t >> BARRETT_SHIFT;
+    let quotient = quotient as i32;
+    let sub = quotient * FIELD_MODULUS;
+    value - sub
+}

examples/lean_chacha20/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "lean_chacha20"
+version = "0.1.0"
+authors = ["Clement Blaudeau <[email protected]>"]
+edition = "2021"
+
+[dependencies]
+hax-lib.workspace = true
+hax-bounded-integers.workspace = true

examples/lean_chacha20/Makefile

@@ -0,0 +1,7 @@
+.PHONY: default clean
+default:
+	cargo hax into lean
+	cd proofs/lean/extraction && lake build
+
+clean:
+	rm -f proofs/lean/extraction/lean_chacha20.lean

examples/lean_chacha20/proofs/lean/extraction/lakefile.toml

@@ -0,0 +1,13 @@
+name = "lean_chacha20"
+version = "0.1.0"
+defaultTargets = ["lean_chacha20_manual_edit"]
+
+[[lean_lib]]
+name = "lean_chacha20"
+
+[[lean_lib]]
+name = "lean_chacha20_manual_edit"
+
+[[require]]
+name = "Hax"
+path = "../../../../../hax-lib/proof-libs/lean"