Merge pull request #14 from joehendrix/bump-04-30

Bump Lean to 2023-04-20 and LeanSMT to newest version

.github/workflows/ci.yaml

@@ -50,10 +50,12 @@ jobs:
       with:
         path: build
         key: ${{ matrix.name }}-build
-    - name: Cache lean_packages
+    - name: Cache lake-packages
       uses: actions/cache@v2
       with:
-        path: lean_packages
-        key: ${{ matrix.name }}-lean_packages
+        path: lake-packages
+        key: ${{ matrix.name }}-lake-packages
+    - name: Retrieve mathlib cache
+      run: lake exe cache get
     - name: Run tests
       run: ./scripts/test.sh

lake-manifest.json

@@ -0,0 +1,33 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "d8de9b777d16d2c287569a684b0404df900583c9",
+    "name": "mathlib",
+    "inputRev?": "d8de9b777d16d2c287569a684b0404df900583c9"}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "cdc00b640d0179910ebaa9c931e3b733a04b881c",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "6006307d2ceb8743fea7e00ba0036af8654d0347",
+    "name": "std",
+    "inputRev?": "main"}},
+  {"git":
+   {"url": "https://github.com/ufmg-smite/lean-smt",
+    "subDir?": null,
+    "rev": "8cb2f2287fd891800dc38178c8d4e62b496f52a2",
+    "name": "smt",
+    "inputRev?": "main"}}]}

lakefile.lean

@@ -97,23 +97,21 @@ extern_lib libcrypto := do
   let dependencies ← opensslFiles.mapM opensslTarget
   buildStaticLib libFile dependencies
 
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4"@"cf2e683c25eba2d798b2460d5703a63db72272c0"
-
 require smt from git
   "https://github.com/ufmg-smite/lean-smt"@"main"
 
 lean_lib LeanCrypto where
   roots := #[`Crypto]
 
-@[defaultTarget]
+@[default_target]
 lean_exe mceliece where
   root := `McEliece
 
 def getTestOutput (fname : FilePath) : ScriptM IO.Process.Output := do
   -- Note: this only works on Unix since it needs the shared library `libSmt`
   -- to also load its transitive dependencies.
-  let smtDynlib := (← findModule? `Smt).get!.dynlibFile
+  let some smtDynlib := (← findModule? `Smt).map Module.dynlibFile
+    | throwThe IO.Error "cannot find module Smt"
   IO.Process.output {
     cmd := (← getLean).toString
     args := #[s!"--load-dynlib={smtDynlib}", fname.toString],

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-08-09
+leanprover/lean4:nightly-2023-04-20

lib/Crypto/Array.lean

@@ -1,3 +1,4 @@
+import Mathlib.Tactic.Linarith
 import Crypto.Fin
 
 theorem ite_same {α:Type} (p:Prop) [h:Decidable p] (a:α) : (if p then a else a) = a := by
@@ -131,23 +132,9 @@ theorem size_empty {α:Type _} : Array.size (#[] : Array α) = 0 := by rfl
 @[simp]
 theorem size_extract {α:Type} (src: Array α) (start stop : Nat)
 : (src.extract start stop).size = min stop src.size - start := by
-  simp [extract, toSubarray]
-  cases Decidable.em (stop ≤ size src) with
-  | inl g =>
-    simp [g, min]
-    cases Decidable.em (start ≤ stop) with
-    | inl h => simp [h]
-    | inr h =>
-      have q := Nat.gt_of_not_le h
-      simp [h, Nat.sub_self, Nat.lt_implies_zero_sub q]
-  | inr g =>
-    simp [g, min]
-    cases Decidable.em (start ≤ size src) with
-    | inl h =>
-      simp [h]
-    | inr h =>
-      have q := Nat.gt_of_not_le h
-      simp [h, Nat.sub_self, Nat.lt_implies_zero_sub q]
+  -- TODO: This definition has changed in core so the lemmas above
+  -- no longer easily prove it.
+  sorry
 
 theorem extract_all (a:Array α)
   : (a.extract 0 a.size) = a := by
@@ -157,13 +144,9 @@ theorem extract_end_empty {a:Array α} {i : Nat} (p : i ≥ a.size) (j : Nat)
   :(a.extract i j) = Array.empty := by
     admit
 
-
 theorem append_empty {α} (a:Array α) : a ++ empty = a := by
   admit
 
-theorem append_data {α} (a b:Array α) : (a ++ b).data = a.data ++ b.data := by
-  admit
-
 theorem size_qsort {α} [Inhabited α] (a:Array α) (lt : α → α → Bool)
   : Array.size (Array.qsort a lt) = a.size := by
   admit

lib/Crypto/BitVec.lean

@@ -12,7 +12,7 @@ def get_lsb (x : BitVec m) (i : Fin m) : Bool :=
 def lsb_getAux (x : BitVec m) (i : Nat) : Bool :=
   (x.val &&& (1 <<< i)) ≠ 0
 
-@[implementedBy lsb_getAux]
+@[implemented_by lsb_getAux]
 def lsb_get! (x : BitVec m) (i : Nat) : Bool :=
   BitVec.lsbGet x i
 
@@ -124,11 +124,11 @@ protected def generate_msb (n : Nat) (f : Fin n → Bool) : BitVec n := Id.run d
   protected def toString {n:Nat} (x:BitVec n) : String :=
     if n % 16 = 0 then
       let s := (Nat.toDigits 16 x.val).asString
-      let t := (List.repeat' '0' (n / 16 - s.length)).asString
+      let t := (List.replicate (n / 16 - s.length) '0').asString
       "0x" ++ t ++ s
     else
       let s := (Nat.toDigits 2 x.val).asString
-      let t := (List.repeat' '0' (n - s.length)).asString
+      let t := (List.replicate (n - s.length) '0').asString
       "0b" ++ t ++ s
 
   instance : ToString (BitVec n) := ⟨BitVec.toString⟩

lib/Crypto/Bool.lean

@@ -1,17 +1,8 @@
-namespace Bool
-
-instance : Xor Bool := ⟨bne⟩
+import Mathlib.Data.Bool.Basic
 
-@[simp] theorem false_xor (a : Bool) : false ^^^ a = a := by cases a <;> rfl
-@[simp] theorem xor_false (a : Bool) : a ^^^ false = a := by cases a <;> rfl
-@[simp] theorem true_xor (a : Bool) : true ^^^ a = !a := by cases a <;> rfl
-@[simp] theorem xor_true (a : Bool) : a ^^^ true = !a := by cases a <;> rfl
-
-theorem xor_comm (a b : Bool) : a ^^^ b = b ^^^ a :=
-  by cases a <;> simp
+namespace Bool
 
-theorem xor_assoc (a b c : Bool) : a ^^^ b ^^^ c = a ^^^ (b ^^^ c) :=
-  by cases a <;> cases b <;> simp
+instance : Xor Bool := ⟨xor⟩
 
 -- TODO(WN): Should these be in the Lean namespace? And probably Mathlib classes
 -- should imply them.

lib/Crypto/ByteArray.lean

@@ -32,7 +32,6 @@ theorem append_data : ∀(x y:ByteArray), (x ++ y).data = x.data ++ y.data
   simp [ByteArray.append, copySlice]
   have p : a.size + b.size ≥ a.size := Nat.le_add_right a.size b.size
   simp [size, Array.extract_all, Array.extract_end_empty p, Array.append_empty (a++b) ]
-  trivial
 
 theorem size_append : ∀(x y:ByteArray), (x ++ y).size = x.size + y.size := by
   intro x y
@@ -42,7 +41,7 @@ theorem size_append : ∀(x y:ByteArray), (x ++ y).size = x.size + y.size := by
   simp only [q]
   apply Array.size_append
 
-@[inline, matchPattern]
+@[inline, match_pattern]
 protected def fromList (l : List UInt8) : ByteArray := { data := { data := l } }
 
 instance : IsList ByteArray where
@@ -60,11 +59,11 @@ def replicateAux : ByteArray → Nat → UInt8 → ByteArray
 
 def replicateNoList (n:Nat) (c:UInt8) : ByteArray := replicateAux (ByteArray.mkEmpty n) n c
 
-@[implementedBy replicateNoList]
+@[implemented_by replicateNoList]
 def replicate (n:Nat) (c:UInt8) : ByteArray := fromList (List.replicate n c)
 
 theorem replicateAuxAsList (a:ByteArray) (j: Nat) (c:UInt8)
-    : replicateAux a j c = a ++ fromList (List.replicate j c) := by
+    : replicateAux a j c = a ++ fromList (α := ByteArray) (List.replicate j c) := by
   revert a
   induction j with
   | zero =>
@@ -126,37 +125,23 @@ theorem size_extract : ∀(a:ByteArray) (s e : Nat), (a.extract s e).size = min
               simp only [Nat.add_sub_of_le h2]
               exact h1
       simp [h3]
-      simp only [Nat.add_sub_cancel_left]
     | inr h2 =>
       have s3 := Nat.le_of_lt (Nat.gt_of_not_le h2)
       simp [h1, Nat.le_implies_zero_sub, s3]
-      cases Decidable.em (s ≤ a.size) with
-      | inl h3 =>
-        simp [h3]
-      | inr h3 =>
-        have s3 := Nat.le_of_lt (Nat.gt_of_not_le h3)
-        simp [Nat.le_implies_zero_sub, s3, h3]
   | inr h1 =>
     cases Decidable.em (s ≤ e) with
     | inl h2 =>
       simp [h1, Nat.add_sub_of_le h2]
     | inr h2 =>
       have n_le_s : e ≤ s := Nat.le_of_lt (Nat.gt_of_not_le h2)
       simp [h1, Nat.le_implies_zero_sub, n_le_s]
-      cases Decidable.em (s ≤ a.size) with
-      | inl h3 =>
-        have h11 : a.size ≤ e := Nat.le_of_lt (Nat.gt_of_not_le h1)
-        have h31 : a.size ≤ s := Nat.le_trans h11 n_le_s
-        simp [h3, Nat.le_implies_zero_sub, h31]
-      | inr h3 =>
-        simp [h3]
 
 def extractN (a:ByteArray) (s n : Nat) : ByteArray :=
   let b := a.extract s (s+n)
   b ++ replicate (n-b.size) 0
 
 theorem size_extractN (a:ByteArray) (s n : Nat) : (a.extractN s n).size = n := by
-  simp [extractN, size_append, size_extract, size_replicate, min]
+  simp [extractN, size_append, size_extract, size_replicate, Nat.min_def]
   cases Decidable.em (s + n ≤ a.size) with
   | inl h1 =>
     simp [h1, Nat.add_sub_self_left]

lib/Crypto/GF2BV.lean

@@ -28,12 +28,12 @@ pmult x y = last zs
 ``` -/
 def polyMul (a : BitVec w) (b : BitVec v) : BitVec (w+v) := Id.run do
   let wOut := w + v
-  let_opaque a := a.zeroExtend wOut (Nat.le_add_right _ _)
+  let a := (let_opaque r := a.zeroExtend v; r)
   let mut ret : BitVec wOut := 0
   -- fold over the bits of b starting at MSB
   for i in List.range v |>.reverse do
-    let_opaque tmp := ret <<< 1
-    opaque ret := if b.lsbGet i then polyAdd tmp a else tmp
+    let tmp := (let_opaque tmp := ret <<< 1; tmp)
+    ret := (let_opaque ret := if b.lsbGet i then polyAdd tmp a else tmp; ret)
   return ret
 
 /-- Modulo operation in GF(2)[x] translated from Cryptol reference.
@@ -144,7 +144,7 @@ def addMany (as : Array F) : F :=
 
 -- TODO: use specialized polyMod instead
 def irredFull (F : GaloisField2k) :=
-  BitVec.ofNat (F.k+1) (1 <<< F.k) ||| F.irred.zeroExtend (F.k+1) (Nat.le_succ _)
+  BitVec.ofNat (F.k+1) (1 <<< F.k) ||| F.irred.zeroExtend 1
 
 def mul (a b : F) : F := polyMod (polyMul a b) (irredFull F)
 

lib/Crypto/Nat.lean

@@ -4,7 +4,7 @@ namespace Nat
 @[simp]
 theorem min_same (n : Nat) : min n n = n := by
   have h : n ≤ n := Nat.le.refl
-  simp [min, h]
+  simp [Nat.min_def, h]
 
 @[simp]
 theorem le_implies_zero_sub {m n:Nat} (p : m ≤ n): m - n = 0 := by

lib/Crypto/ToMathlib.lean

@@ -79,12 +79,6 @@ end Nat
 
 /-! Permutations -/
 
-theorem List.perm_append_singleton {a : α} {l : List α} : l ++ [a] ~ a :: l := by
-  suffices l ++ [a] ~ a :: (l ++ []) by
-    rw [List.append_nil] at this
-    assumption
-  apply perm_middle
-
 theorem List.perm_reverse {l : List α} : l.reverse ~ l := by
   induction l with
   | nil => exact .refl []
@@ -102,7 +96,7 @@ def List.rangeModel : Nat → List Nat
 
 @[csimp]
 theorem List.rangeModel_eq_range : @rangeModel = @range :=
-  have aux (n : Nat) (r : List Nat) : rangeAux n r = rangeModel n ++ r := by
+  have aux (n : Nat) (r : List Nat) : range.loop n r = rangeModel n ++ r := by
     induction n generalizing r with
     | zero => simp [rangeModel]
     | succ n ih => simp [rangeModel, ih, append_assoc]
@@ -128,16 +122,6 @@ theorem List.rangeModel_succ {n : Nat} : rangeModel (n+1) = rangeModel n ++ [n]
 @[simp] theorem List.getD_cons : List.getD (x :: xs) i d = if i = 0 then x else List.getD xs (i-1) d :=
   sorry
 
-lemma List.foldl_ext (f g : α → β → α) (a : α)
-  {l : List β} (H : ∀ a : α, ∀ b ∈ l, f a b = g a b) :
-  l.foldl f a = l.foldl g a :=
-by
-  induction l generalizing a with
-  | nil => rfl
-  | cons x xs ih =>
-    unfold foldl
-    rw [ih (f a x) (fun a b hB => H a b <| mem_cons_of_mem x hB), H a x <| mem_cons_self x xs]
-
 -- by Mario
 def List.withPred (P : α → Prop) : (as : List α) → (h : (a : α) → a ∈ as → P a) → List { x : α // P x }
   | [], _ => []
@@ -173,12 +157,6 @@ theorem List.foldl_eq_of_comm_of_perm {l₁ l₂ : List β} (f : α → β → 
   | swap => simp [foldl, H]
   | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂]
 
-@[simp]
-theorem List.foldl_append (f : α → β → α) :
-    ∀ (a : α) (l₁ l₂ : List β), foldl f a (l₁ ++ l₂) = foldl f (foldl f a l₁) l₂
-  | a, []     , l₂ => rfl
-  | a, (b::l₁), l₂ => by simp [cons_append, foldl, foldl_append f (f a b) l₁ l₂]
-
 /-! Fin and Fin ranges -/
 
 theorem Fin.induction {n : ℕ}
@@ -218,7 +196,9 @@ theorem List.rangeFinUpTo_complete (m : Nat) (i : Fin m) (h : m ≤ n)
     | isTrue hEq => simp [rangeFinUpTo, hEq]
     | isFalse hNeq => 
       let i' : Fin m := ⟨i, Nat.lt_of_le_of_ne (Nat.le_of_lt_succ i.isLt) hNeq⟩
-      simp [rangeFinUpTo, ih i' (Nat.le_of_succ_le h)]
+      have := ih i' (Nat.le_of_succ_le h)
+      simp [rangeFinUpTo]
+      exact Or.inl this
 
 theorem List.rangeFin_complete (n : Nat) (i : Fin n) : i ∈ rangeFin n :=
   rangeFinUpTo_complete n i (Nat.le_refl _)

lib/Crypto/Vector.lean

@@ -109,12 +109,7 @@ def extractN! [Inhabited α] (a : Vector n α) (s m:Nat) : Vector m α :=
         have p : min (s + m) (Array.size a.data) - s ≤ m := by
               apply Nat.sub_le_of_le_add
               simp only [Nat.add_comm s m, min]
-              cases Decidable.em (m + s ≤ a.data.size) with
-              | inl h =>
-                simp [h]
-              | inr h =>
-                simp [h]
-                exact Nat.le_of_lt (Nat.gt_of_not_le h)
+              cases Decidable.em (m + s ≤ a.data.size) <;> next h => simp [h]
         simp [Nat.add_sub_of_le p]
   ⟨b ++ e, pr⟩
 

lib/McEliece.lean

@@ -9,7 +9,7 @@ def main (args:List String): IO Unit := do
   | [reqPath, rspPath] => do
       let mut drbg0 := randombytesInit (byteSequence 48);
       let mut seedArray : Array Seed := #[]
-      let fpReq ← IO.FS.Handle.mk reqPath IO.FS.Mode.write false
+      let fpReq ← IO.FS.Handle.mk reqPath IO.FS.Mode.write
       for i in [0:10] do
         let (seed, drbg2) := PRNG.randombytes drbg0 48
         drbg0 := drbg2
@@ -20,7 +20,7 @@ def main (args:List String): IO Unit := do
         fpReq.putStrLn "ct ="
         fpReq.putStrLn "ss =\n"
         seedArray := seedArray.push seed
-      let fpRsp ← IO.FS.Handle.mk rspPath IO.FS.Mode.write false
+      let fpRsp ← IO.FS.Handle.mk rspPath IO.FS.Mode.write
       fpRsp.putStrLn $ s!"# kem/{Mceliece.Ref348864.name}\n"
       for i in [0:10], seed in seedArray do
         let (key, drbg) ←

scripts/test.sh

@@ -8,7 +8,7 @@ lake build mceliece
 cmp --silent tests/mceliece/kat_kem.req.golden tmp/kat_kem.req || echo "Req files are different"
 cmp --silent tests/mceliece/kat_kem.rsp.golden tmp/kat_kem.rsp || echo "Rsp files are different"
 
-lake build Smt:shared
+lake build +Smt:dynlib
 lake run runTest tests/aes/GF256Pow.lean
 # TODO: times out
 # lake run runTest tests/aes/SBox.lean