Merge pull request #1696 from cryspen/lean-lib-update

proof-libs/lean Library update and refactor

Author: clementblaudeau

CHANGELOG.md

@@ -55,6 +55,7 @@ Changes to hax-lib:
 - New behavior for `hax_lib::include`: it now forces inclusion when in contradiction with `-i` flag.
 - hax-lib requires edition 2021 instead of 2024 (#1726)
 - Improved `VecDeque` model in F* proof lib (#1728)
+- Split the Lean library into several files, update to lean 4.23.0 (#1696)
 
 Changes to the Lean backend:
 - Improve support for functionalized loops (#1695)

examples/lean_barrett/proofs/lean/extraction/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.22.0
+leanprover/lean4:v4.23.0

examples/lean_barrett/src/lib.rs

@@ -40,27 +40,22 @@ pub(crate) const FIELD_MODULUS: i32 = 3329;
 #[hax_lib::lean::before("@[simp, spec]")]
 #[hax_lib::lean::after(
     "
+set_option maxHeartbeats 1000000 in
+-- quite computation intensive
 theorem barrett_spec (value: i32) :
-  ⦃ Lean_barrett.__4.requires (value) = pure true ⦄
-  (Lean_barrett.barrett_reduce value)
-  ⦃ ⇓ result => Lean_barrett.__5.ensures value result = pure true ⦄
+  ⦃ ⌜ Lean_barrett.__4.requires (value) = pure true ⌝ ⦄
+  (do
+    let result ← Lean_barrett.barrett_reduce value;
+    Lean_barrett.__5.ensures value result)
+  ⦃ ⇓ post => ⌜post = true⌝ ⦄
 := by
-  mvcgen
+  open Spec.BV in mvcgen [Lean_barrett.__5.ensures] <;> simp at *
   hax_bv_decide
-  simp [Lean_barrett.__5.ensures] at *
-  rw [i32.HaxRem_spec_bv_rw] ; simp ;
-  rw [i32.HaxAdd_spec_bv_rw] ; simp ;
-  rw [i32.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 *
+        Int32.lt_iff_toBitVec_slt,
+        Int64.le_iff_toBitVec_sle,
+        ] at *
+  expose_names; have ⟨ _ , _ ⟩ := h_1 ; clear h_1
   generalize Int32.toBitVec value = bv_value at * ; clear value
   bv_decide (config := {timeout := 120})
 "

examples/lean_chacha20/Makefile

@@ -7,3 +7,4 @@ default:
 
 clean:
 	-rm -f proofs/lean/extraction/lean_chacha20.lean
+	-cd proofs/lean/extraction && lake clean