From acdc047c2978d953528dc7003c547047285cb991 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 5 Sep 2023 22:40:35 -0400
Subject: [PATCH 1/8] chore: bump Lean

---
 lake-manifest.json            | 33 +++++++++++++++++++++++++++++++++
 lakefile.lean                 |  8 +++-----
 lean-toolchain                |  2 +-
 lib/Crypto/Array.lean         | 25 ++++---------------------
 lib/Crypto/BitVec.lean        |  6 +++---
 lib/Crypto/Bool.lean          | 15 +++------------
 lib/Crypto/ByteArray.lean     | 23 ++++-------------------
 lib/Crypto/GF2BV.lean         |  8 ++++----
 lib/Crypto/Nat.lean           |  2 +-
 lib/Crypto/ToMathlib.lean     | 28 ++++------------------------
 lib/Crypto/Vector.lean        |  7 +------
 tests/mceliece/GF4096Mul.lean | 28 ++++++++++++++--------------
 12 files changed, 75 insertions(+), 110 deletions(-)
 create mode 100644 lake-manifest.json

diff --git a/lake-manifest.json b/lake-manifest.json
new file mode 100644
index 0000000..5116a2b
--- /dev/null
+++ b/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"}}]}
diff --git a/lakefile.lean b/lakefile.lean
index e60f625..ed843f5 100644
--- a/lakefile.lean
+++ b/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],
diff --git a/lean-toolchain b/lean-toolchain
index f62cade..03ae79e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-08-09
+leanprover/lean4:nightly-2023-04-20
diff --git a/lib/Crypto/Array.lean b/lib/Crypto/Array.lean
index c33f6cd..bbefdd2 100644
--- a/lib/Crypto/Array.lean
+++ b/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
diff --git a/lib/Crypto/BitVec.lean b/lib/Crypto/BitVec.lean
index 0076019..a62af89 100644
--- a/lib/Crypto/BitVec.lean
+++ b/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⟩
diff --git a/lib/Crypto/Bool.lean b/lib/Crypto/Bool.lean
index 7c9b2fa..a79c066 100644
--- a/lib/Crypto/Bool.lean
+++ b/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.
diff --git a/lib/Crypto/ByteArray.lean b/lib/Crypto/ByteArray.lean
index 168853e..5d7b506 100644
--- a/lib/Crypto/ByteArray.lean
+++ b/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,16 +125,9 @@ 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 =>
@@ -143,20 +135,13 @@ theorem size_extract : ∀(a:ByteArray) (s e : Nat), (a.extract s e).size = min
     | 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]
diff --git a/lib/Crypto/GF2BV.lean b/lib/Crypto/GF2BV.lean
index 8bafacc..b47f107 100644
--- a/lib/Crypto/GF2BV.lean
+++ b/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)
 
diff --git a/lib/Crypto/Nat.lean b/lib/Crypto/Nat.lean
index 285c631..5ee8b6f 100644
--- a/lib/Crypto/Nat.lean
+++ b/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
diff --git a/lib/Crypto/ToMathlib.lean b/lib/Crypto/ToMathlib.lean
index 2edb43e..9cd7e6d 100644
--- a/lib/Crypto/ToMathlib.lean
+++ b/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 _)
diff --git a/lib/Crypto/Vector.lean b/lib/Crypto/Vector.lean
index 9b03661..fc17140 100644
--- a/lib/Crypto/Vector.lean
+++ b/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⟩
 
diff --git a/tests/mceliece/GF4096Mul.lean b/tests/mceliece/GF4096Mul.lean
index 8baf92f..7ecf02d 100644
--- a/tests/mceliece/GF4096Mul.lean
+++ b/tests/mceliece/GF4096Mul.lean
@@ -87,24 +87,24 @@ example (x y : GF) : GF4096.ofGF (x * y) = (GF4096.ofGF x) * (GF4096.ofGF y) :=
   show (GF4096.ofGF (GF.mul x y)) = GaloisField2k.mul (GF4096.ofGF x) (GF4096.ofGF y)
 
   extract_def GF4096.ofGF
-    specialize_def GF4096.ofGF [] blocking [@Subtype.val, UInt16.val]
-    rw [GF4096.ofGF.specialization]
-    rw [GF4096.ofGF.specialization]
-    rw [GF4096.ofGF.specialization]
-    save
+  specialize_def Mceliece.Ref348864.GF4096.ofGF [] blocking [@Subtype.val, UInt16.val]
+  rw [Mceliece.Ref348864.GF4096.ofGF.specialization]
+  rw [Mceliece.Ref348864.GF4096.ofGF.specialization]
+  rw [Mceliece.Ref348864.GF4096.ofGF.specialization]
+  save
 
   extract_def GF.mul
-    specialize_def Mceliece348864Ref.GF.mul [] blocking [
-      @Subtype.val,
-      UInt16.toUInt32,
-      GF.red
-    ]
-    save
+  specialize_def Mceliece.Ref348864.GF.mul [] blocking [
+    @Subtype.val,
+    UInt16.toUInt32,
+    GF.red
+  ]
+  save
 
   extract_def GaloisField2k.mul
-    specialize_def GaloisField2k.mul [GF4096] blocking [@polyMod, @polyMul]
-      rw [GaloisField2k.mul.GF4096.specialization]
-      save
+  specialize_def GaloisField2k.mul [GF4096] blocking [@polyMod, @polyMul]
+  rw [GaloisField2k.mul.GF4096.specialization]
+  save
 
   smt_show [
     GF4096.ofGF,

From 3d24bed8ee568c87a501d0629c26bbf3e2e96ef8 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 5 Sep 2023 22:52:43 -0400
Subject: [PATCH 2/8] chore: fix tests

---
 lib/McEliece.lean       | 4 ++--
 tests/aes/GF256Pow.lean | 9 +++++----
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/lib/McEliece.lean b/lib/McEliece.lean
index 98559a3..6d0298d 100644
--- a/lib/McEliece.lean
+++ b/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) ←
diff --git a/tests/aes/GF256Pow.lean b/tests/aes/GF256Pow.lean
index e0a70ad..276aade 100644
--- a/tests/aes/GF256Pow.lean
+++ b/tests/aes/GF256Pow.lean
@@ -13,15 +13,16 @@ example (x : GF256) : GF256.pow2 8 x = x := by
   conv at GF256.pow2.def =>
     intro k x
     rw [ GaloisField2k.mul.GF256.specialization ]
-  save
+  -- TODO: breaks mvar context
+  -- save
 
   extract_def polyMod
   specialize_def GF2BVPoly.polyMod [16, 8]
-  save
+  -- save
 
   extract_def polyMul
   specialize_def GF2BVPoly.polyMul [8, 8]
-  save
+  -- save
 
   conv at GaloisField2k.mul.GF256.def =>
     intro a b
@@ -34,5 +35,5 @@ example (x : GF256) : GF256.pow2 8 x = x := by
     GF2BVPoly.polyMul.«8».«8»,
     GF2BVPoly.polyMod.«16».«8»
   ] 
-    
+
   sorry

From 77e297d17fadf579b263f343b1c8341937ae878c Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 5 Sep 2023 22:56:32 -0400
Subject: [PATCH 3/8] chore: fetch mathlib cache

---
 .github/workflows/ci.yaml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index c1fc14c..38456a2 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -45,6 +45,8 @@ jobs:
       run: brew install elan
     - name: Checkout
       uses: actions/checkout@v2
+    - name: Retrieve mathlib cache
+      run: lake exe cache get
     - name: Cache build
       uses: actions/cache@v2
       with:

From b1106d216802b8cdb0d306181ae3da74ac96b37f Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 5 Sep 2023 22:58:23 -0400
Subject: [PATCH 4/8] chore: lean_packages -> lake-packages

---
 .github/workflows/ci.yaml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index 38456a2..eb8ab92 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -52,10 +52,10 @@ 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: Run tests
       run: ./scripts/test.sh

From a4b517cc7f0060726c989c8e093b81d5025f0f8e Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 5 Sep 2023 23:04:51 -0400
Subject: [PATCH 5/8] chore: ci action order

---
 .github/workflows/ci.yaml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml
index eb8ab92..04c7b6a 100644
--- a/.github/workflows/ci.yaml
+++ b/.github/workflows/ci.yaml
@@ -45,8 +45,6 @@ jobs:
       run: brew install elan
     - name: Checkout
       uses: actions/checkout@v2
-    - name: Retrieve mathlib cache
-      run: lake exe cache get
     - name: Cache build
       uses: actions/cache@v2
       with:
@@ -57,5 +55,7 @@ jobs:
       with:
         path: lake-packages
         key: ${{ matrix.name }}-lake-packages
+    - name: Retrieve mathlib cache
+      run: lake exe cache get
     - name: Run tests
       run: ./scripts/test.sh

From 6a2c8014cb194cc9dab832a908765d87301dba75 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 5 Sep 2023 23:35:33 -0400
Subject: [PATCH 6/8] chore: load more dylibs to fix test

---
 lakefile.lean               | 14 +++++++++++---
 lean_packages/manifest.json | 10 ----------
 tests/aes/GF256Pow.expected |  4 ++--
 3 files changed, 13 insertions(+), 15 deletions(-)
 delete mode 100644 lean_packages/manifest.json

diff --git a/lakefile.lean b/lakefile.lean
index ed843f5..f5ec3fa 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -110,11 +110,19 @@ lean_exe mceliece where
 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 some smtDynlib := (← findModule? `Smt).map Module.dynlibFile
-    | throwThe IO.Error "cannot find module Smt"
+  let getDynlib nm : ScriptM FilePath := do
+    let some ret := (← findModule? nm).map Module.dynlibFile
+      | throwThe IO.Error "cannot find module Smt"
+    return ret
+  let dynlibs := #[
+    ← getDynlib `Std,
+    ← getDynlib `Qq,
+    ← getDynlib `Aesop,
+    ← getDynlib `Smt    
+  ]
   IO.Process.output {
     cmd := (← getLean).toString
-    args := #[s!"--load-dynlib={smtDynlib}", fname.toString],
+    args := dynlibs.map (s!"--load-dynlib={·}") ++ #[fname.toString],
     env := (← getAugmentedEnv)
   }
 
diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json
deleted file mode 100644
index 3991b38..0000000
--- a/lean_packages/manifest.json
+++ /dev/null
@@ -1,10 +0,0 @@
-{"version": 2,
- "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4",
-   "rev": "cf2e683c25eba2d798b2460d5703a63db72272c0",
-   "name": "mathlib",
-   "inputRev": "cf2e683c25eba2d798b2460d5703a63db72272c0"},
-  {"url": "https://github.com/ufmg-smite/lean-smt",
-   "rev": "219fffdf8d850fcb29c46e226d623def13848618",
-   "name": "smt",
-   "inputRev": "main"}]}
diff --git a/tests/aes/GF256Pow.expected b/tests/aes/GF256Pow.expected
index cd0e0d5..fe54c85 100644
--- a/tests/aes/GF256Pow.expected
+++ b/tests/aes/GF256Pow.expected
@@ -3,9 +3,9 @@ goal: GF256.pow2 8 x = x
 query:
 (define-sort Nat () Int)
 (define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y)))
-(assert (forall ((_uniq.7863 Nat)) (=> (>= _uniq.7863 0) (forall ((_uniq.7864 Nat)) (=> (>= _uniq.7864 0) (>= (Nat.sub _uniq.7863 _uniq.7864) 0))))))
+(assert (forall ((_uniq.7776 Nat)) (=> (>= _uniq.7776 0) (forall ((_uniq.7777 Nat)) (=> (>= _uniq.7777 0) (>= (Nat.sub _uniq.7776 _uniq.7777) 0))))))
 (define-fun |GF2BVPoly.polyMod.«16».«8»| ((x (_ BitVec 16)) (y (_ BitVec 9))) (_ BitVec 8) (let ((ret #b00000000)) (let ((pow (ite (= (not (= ((_ extract 8 8) #b000000001) #b0)) true) (bvxor #b000000001 y) #b000000001))) (let ((ret_1 (ite (= (not (= ((_ extract 0 0) x) #b0)) true) (bvxor ret (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow) #b00000000)) ret))) (let ((pow_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow #b000000001)) #b0)) true) (bvxor (bvshl pow #b000000001) y) (bvshl pow #b000000001)))) (let ((ret_2 (ite (= (not (= ((_ extract 1 1) x) #b0)) true) (bvxor ret_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_1) #b00000000)) ret_1))) (let ((pow_2 (ite (= (not (= ((_ extract 8 8) (bvshl pow_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_1 #b000000001) y) (bvshl pow_1 #b000000001)))) (let ((ret_3 (ite (= (not (= ((_ extract 2 2) x) #b0)) true) (bvxor ret_2 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_2) #b00000000)) ret_2))) (let ((pow_3 (ite (= (not (= ((_ extract 8 8) (bvshl pow_2 #b000000001)) #b0)) true) (bvxor (bvshl pow_2 #b000000001) y) (bvshl pow_2 #b000000001)))) (let ((ret_4 (ite (= (not (= ((_ extract 3 3) x) #b0)) true) (bvxor ret_3 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_3) #b00000000)) ret_3))) (let ((pow_4 (ite (= (not (= ((_ extract 8 8) (bvshl pow_3 #b000000001)) #b0)) true) (bvxor (bvshl pow_3 #b000000001) y) (bvshl pow_3 #b000000001)))) (let ((ret_5_1 (ite (= (not (= ((_ extract 4 4) x) #b0)) true) (bvxor ret_4 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_4) #b00000000)) ret_4))) (let ((pow_5_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_4 #b000000001)) #b0)) true) (bvxor (bvshl pow_4 #b000000001) y) (bvshl pow_4 #b000000001)))) (let ((ret_6 (ite (= (not (= ((_ extract 5 5) x) #b0)) true) (bvxor ret_5_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5_1) #b00000000)) ret_5_1))) (let ((pow_6 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_5_1 #b000000001) y) (bvshl pow_5_1 #b000000001)))) (let ((ret_6_1 (ite (= (not (= ((_ extract 5 5) x) #b0)) true) (bvxor ret_5_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5_1) #b00000000)) ret_5_1))) (let ((pow_6_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_5_1 #b000000001) y) (bvshl pow_5_1 #b000000001)))) (let ((ret_7 (ite (= (not (= ((_ extract 6 6) x) #b0)) true) (bvxor ret_6 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_6) #b00000000)) ret_6))) (let ((pow_7 (ite (= (not (= ((_ extract 8 8) (bvshl pow_6 #b000000001)) #b0)) true) (bvxor (bvshl pow_6 #b000000001) y) (bvshl pow_6 #b000000001)))) (let ((ret_7_1 (ite (= (not (= ((_ extract 6 6) x) #b0)) true) (bvxor ret_6_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_6_1) #b00000000)) ret_6_1))) (let ((pow_7_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_6_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_6_1 #b000000001) y) (bvshl pow_6_1 #b000000001)))) (let ((ret_8 (ite (= (not (= ((_ extract 7 7) x) #b0)) true) (bvxor ret_7 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_7) #b00000000)) ret_7))) (let ((pow_8 (ite (= (not (= ((_ extract 8 8) (bvshl pow_7 #b000000001)) #b0)) true) (bvxor (bvshl pow_7 #b000000001) y) (bvshl pow_7 #b000000001)))) (let ((ret_8_1 (ite (= (not (= ((_ extract 7 7) x) #b0)) true) (bvxor ret_7_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_7_1) #b00000000)) ret_7_1))) (let ((pow_8_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_7_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_7_1 #b000000001) y) (bvshl pow_7_1 #b000000001)))) (let ((ret_9 (ite (= (not (= ((_ extract 8 8) x) #b0)) true) (bvxor ret_8 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_8) #b00000000)) ret_8))) (let ((pow_9 (ite (= (not (= ((_ extract 8 8) (bvshl pow_8 #b000000001)) #b0)) true) (bvxor (bvshl pow_8 #b000000001) y) (bvshl pow_8 #b000000001)))) (let ((ret_9_1 (ite (= (not (= ((_ extract 8 8) x) #b0)) true) (bvxor ret_8_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_8_1) #b00000000)) ret_8_1))) (let ((pow_9_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_8_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_8_1 #b000000001) y) (bvshl pow_8_1 #b000000001)))) (let ((ret_5 (ite (= (not (= ((_ extract 9 9) x) #b0)) true) (bvxor ret_9_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_9_1) #b00000000)) ret_9_1))) (let ((pow_5 (ite (= (not (= ((_ extract 8 8) (bvshl pow_9_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_9_1 #b000000001) y) (bvshl pow_9_1 #b000000001)))) (let ((ret_10 (ite (= (not (= ((_ extract 10 10) x) #b0)) true) (bvxor ret_5 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5) #b00000000)) ret_5))) (let ((pow_10 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5 #b000000001)) #b0)) true) (bvxor (bvshl pow_5 #b000000001) y) (bvshl pow_5 #b000000001)))) (let ((ret_11 (ite (= (not (= ((_ extract 11 11) x) #b0)) true) (bvxor ret_10 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_10) #b00000000)) ret_10))) (let ((pow_11 (ite (= (not (= ((_ extract 8 8) (bvshl pow_10 #b000000001)) #b0)) true) (bvxor (bvshl pow_10 #b000000001) y) (bvshl pow_10 #b000000001)))) (let ((ret_12 (ite (= (not (= ((_ extract 12 12) x) #b0)) true) (bvxor ret_11 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_11) #b00000000)) ret_11))) (let ((pow_12 (ite (= (not (= ((_ extract 8 8) (bvshl pow_11 #b000000001)) #b0)) true) (bvxor (bvshl pow_11 #b000000001) y) (bvshl pow_11 #b000000001)))) (let ((ret_13 (ite (= (not (= ((_ extract 13 13) x) #b0)) true) (bvxor ret_12 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_12) #b00000000)) ret_12))) (let ((pow_13 (ite (= (not (= ((_ extract 8 8) (bvshl pow_12 #b000000001)) #b0)) true) (bvxor (bvshl pow_12 #b000000001) y) (bvshl pow_12 #b000000001)))) (let ((ret_14 (ite (= (not (= ((_ extract 14 14) x) #b0)) true) (bvxor ret_13 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_13) #b00000000)) ret_13))) (let ((pow_14 (ite (= (not (= ((_ extract 8 8) (bvshl pow_13 #b000000001)) #b0)) true) (bvxor (bvshl pow_13 #b000000001) y) (bvshl pow_13 #b000000001)))) (let ((ret_15 (ite (= (not (= ((_ extract 15 15) x) #b0)) true) (bvxor ret_14 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_14) #b00000000)) ret_14))) (let ((pow_15 (ite (= (not (= ((_ extract 8 8) (bvshl pow_14 #b000000001)) #b0)) true) (bvxor (bvshl pow_14 #b000000001) y) (bvshl pow_14 #b000000001)))) (ite (= y #b000000000) #b00000000 ret_15))))))))))))))))))))))))))))))))))))))))))))
-(define-fun |GF2BVPoly.polyMul.«8».«8»| ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) (let ((v (let ((v_1 (bvshl #b0000000000000000 #b0000000000000001))) (let ((v_1_1 (concat #b00000000 a))) (let ((v_1_1_1 (bvshl #b0000000000000000 #b0000000000000001))) (ite (= (not (= ((_ extract 7 7) b) #b0)) true) (bvxor v_1_1_1 v_1_1) v_1)))))) (let ((v_1 (let ((v_1_1 (bvshl v #b0000000000000001))) (let ((v_1_1_1 (concat #b00000000 a))) (let ((v_1_1_1_1 (bvshl v #b0000000000000001))) (ite (= (not (= ((_ extract 6 6) b) #b0)) true) (bvxor v_1_1_1_1 v_1_1_1) v_1_1)))))) (let ((v_2 (let ((v_2_1 (bvshl v_1 #b0000000000000001))) (let ((v_2_1_1 (concat #b00000000 a))) (let ((v_2_1_1_1 (bvshl v_1 #b0000000000000001))) (ite (= (not (= ((_ extract 5 5) b) #b0)) true) (bvxor v_2_1_1_1 v_2_1_1) v_2_1)))))) (let ((v_3 (let ((v_3_1 (bvshl v_2 #b0000000000000001))) (let ((v_3_1_1 (concat #b00000000 a))) (let ((v_3_1_1_1 (bvshl v_2 #b0000000000000001))) (ite (= (not (= ((_ extract 4 4) b) #b0)) true) (bvxor v_3_1_1_1 v_3_1_1) v_3_1)))))) (let ((v_4 (let ((v_4_1 (bvshl v_3 #b0000000000000001))) (let ((v_4_1_1 (concat #b00000000 a))) (let ((v_4_1_1_1 (bvshl v_3 #b0000000000000001))) (ite (= (not (= ((_ extract 3 3) b) #b0)) true) (bvxor v_4_1_1_1 v_4_1_1) v_4_1)))))) (let ((v_5 (let ((v_5_1 (bvshl v_4 #b0000000000000001))) (let ((v_5_1_1 (concat #b00000000 a))) (let ((v_5_1_1_1 (bvshl v_4 #b0000000000000001))) (ite (= (not (= ((_ extract 2 2) b) #b0)) true) (bvxor v_5_1_1_1 v_5_1_1) v_5_1)))))) (let ((v_6 (let ((v_6_1 (bvshl v_5 #b0000000000000001))) (let ((v_6_1_1 (concat #b00000000 a))) (let ((v_6_1_1_1 (bvshl v_5 #b0000000000000001))) (ite (= (not (= ((_ extract 1 1) b) #b0)) true) (bvxor v_6_1_1_1 v_6_1_1) v_6_1)))))) (let ((v_7 (let ((v_7_1 (bvshl v_6 #b0000000000000001))) (let ((v_7_1_1 (concat #b00000000 a))) (let ((v_7_1_1_1 (bvshl v_6 #b0000000000000001))) (ite (= (not (= ((_ extract 0 0) b) #b0)) true) (bvxor v_7_1_1_1 v_7_1_1) v_7_1)))))) v_7)))))))))
+(define-fun |GF2BVPoly.polyMul.«8».«8»| ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) (let ((ret (let ((tmp (bvshl #b0000000000000000 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl #b0000000000000000 #b0000000000000001))) (ite (= (not (= ((_ extract 7 7) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_1 (let ((tmp (bvshl ret #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret #b0000000000000001))) (ite (= (not (= ((_ extract 6 6) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_2 (let ((tmp (bvshl ret_1 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_1 #b0000000000000001))) (ite (= (not (= ((_ extract 5 5) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_3 (let ((tmp (bvshl ret_2 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_2 #b0000000000000001))) (ite (= (not (= ((_ extract 4 4) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_4 (let ((tmp (bvshl ret_3 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_3 #b0000000000000001))) (ite (= (not (= ((_ extract 3 3) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_5 (let ((tmp (bvshl ret_4 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_4 #b0000000000000001))) (ite (= (not (= ((_ extract 2 2) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_6 (let ((tmp (bvshl ret_5 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_5 #b0000000000000001))) (ite (= (not (= ((_ extract 1 1) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_7 (let ((tmp (bvshl ret_6 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_6 #b0000000000000001))) (ite (= (not (= ((_ extract 0 0) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) ret_7)))))))))
 (define-fun GaloisField2k.mul.GF256 ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8) (|GF2BVPoly.polyMod.«16».«8»| (|GF2BVPoly.polyMul.«8».«8»| a b) (bvor #b100000000 (concat #b0 #b00011011))))
 (define-fun-rec GF256.pow2 ((k Nat) (x (_ BitVec 8))) (_ BitVec 8) (ite (= k 0) x (GaloisField2k.mul.GF256 (GF256.pow2 (Nat.sub k 1) x) (GF256.pow2 (Nat.sub k 1) x))))
 (declare-const x (_ BitVec 8))

From 1440f06e80f711f9dfea0514f3212ce0f624ca95 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 5 Sep 2023 23:48:53 -0400
Subject: [PATCH 7/8] Revert "chore: load more dylibs to fix test"

This reverts commit 6a2c8014cb194cc9dab832a908765d87301dba75.
---
 lakefile.lean               | 14 +++-----------
 lean_packages/manifest.json | 10 ++++++++++
 tests/aes/GF256Pow.expected |  4 ++--
 3 files changed, 15 insertions(+), 13 deletions(-)
 create mode 100644 lean_packages/manifest.json

diff --git a/lakefile.lean b/lakefile.lean
index f5ec3fa..ed843f5 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -110,19 +110,11 @@ lean_exe mceliece where
 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 getDynlib nm : ScriptM FilePath := do
-    let some ret := (← findModule? nm).map Module.dynlibFile
-      | throwThe IO.Error "cannot find module Smt"
-    return ret
-  let dynlibs := #[
-    ← getDynlib `Std,
-    ← getDynlib `Qq,
-    ← getDynlib `Aesop,
-    ← getDynlib `Smt    
-  ]
+  let some smtDynlib := (← findModule? `Smt).map Module.dynlibFile
+    | throwThe IO.Error "cannot find module Smt"
   IO.Process.output {
     cmd := (← getLean).toString
-    args := dynlibs.map (s!"--load-dynlib={·}") ++ #[fname.toString],
+    args := #[s!"--load-dynlib={smtDynlib}", fname.toString],
     env := (← getAugmentedEnv)
   }
 
diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json
new file mode 100644
index 0000000..3991b38
--- /dev/null
+++ b/lean_packages/manifest.json
@@ -0,0 +1,10 @@
+{"version": 2,
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "rev": "cf2e683c25eba2d798b2460d5703a63db72272c0",
+   "name": "mathlib",
+   "inputRev": "cf2e683c25eba2d798b2460d5703a63db72272c0"},
+  {"url": "https://github.com/ufmg-smite/lean-smt",
+   "rev": "219fffdf8d850fcb29c46e226d623def13848618",
+   "name": "smt",
+   "inputRev": "main"}]}
diff --git a/tests/aes/GF256Pow.expected b/tests/aes/GF256Pow.expected
index fe54c85..cd0e0d5 100644
--- a/tests/aes/GF256Pow.expected
+++ b/tests/aes/GF256Pow.expected
@@ -3,9 +3,9 @@ goal: GF256.pow2 8 x = x
 query:
 (define-sort Nat () Int)
 (define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y)))
-(assert (forall ((_uniq.7776 Nat)) (=> (>= _uniq.7776 0) (forall ((_uniq.7777 Nat)) (=> (>= _uniq.7777 0) (>= (Nat.sub _uniq.7776 _uniq.7777) 0))))))
+(assert (forall ((_uniq.7863 Nat)) (=> (>= _uniq.7863 0) (forall ((_uniq.7864 Nat)) (=> (>= _uniq.7864 0) (>= (Nat.sub _uniq.7863 _uniq.7864) 0))))))
 (define-fun |GF2BVPoly.polyMod.«16».«8»| ((x (_ BitVec 16)) (y (_ BitVec 9))) (_ BitVec 8) (let ((ret #b00000000)) (let ((pow (ite (= (not (= ((_ extract 8 8) #b000000001) #b0)) true) (bvxor #b000000001 y) #b000000001))) (let ((ret_1 (ite (= (not (= ((_ extract 0 0) x) #b0)) true) (bvxor ret (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow) #b00000000)) ret))) (let ((pow_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow #b000000001)) #b0)) true) (bvxor (bvshl pow #b000000001) y) (bvshl pow #b000000001)))) (let ((ret_2 (ite (= (not (= ((_ extract 1 1) x) #b0)) true) (bvxor ret_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_1) #b00000000)) ret_1))) (let ((pow_2 (ite (= (not (= ((_ extract 8 8) (bvshl pow_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_1 #b000000001) y) (bvshl pow_1 #b000000001)))) (let ((ret_3 (ite (= (not (= ((_ extract 2 2) x) #b0)) true) (bvxor ret_2 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_2) #b00000000)) ret_2))) (let ((pow_3 (ite (= (not (= ((_ extract 8 8) (bvshl pow_2 #b000000001)) #b0)) true) (bvxor (bvshl pow_2 #b000000001) y) (bvshl pow_2 #b000000001)))) (let ((ret_4 (ite (= (not (= ((_ extract 3 3) x) #b0)) true) (bvxor ret_3 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_3) #b00000000)) ret_3))) (let ((pow_4 (ite (= (not (= ((_ extract 8 8) (bvshl pow_3 #b000000001)) #b0)) true) (bvxor (bvshl pow_3 #b000000001) y) (bvshl pow_3 #b000000001)))) (let ((ret_5_1 (ite (= (not (= ((_ extract 4 4) x) #b0)) true) (bvxor ret_4 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_4) #b00000000)) ret_4))) (let ((pow_5_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_4 #b000000001)) #b0)) true) (bvxor (bvshl pow_4 #b000000001) y) (bvshl pow_4 #b000000001)))) (let ((ret_6 (ite (= (not (= ((_ extract 5 5) x) #b0)) true) (bvxor ret_5_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5_1) #b00000000)) ret_5_1))) (let ((pow_6 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_5_1 #b000000001) y) (bvshl pow_5_1 #b000000001)))) (let ((ret_6_1 (ite (= (not (= ((_ extract 5 5) x) #b0)) true) (bvxor ret_5_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5_1) #b00000000)) ret_5_1))) (let ((pow_6_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_5_1 #b000000001) y) (bvshl pow_5_1 #b000000001)))) (let ((ret_7 (ite (= (not (= ((_ extract 6 6) x) #b0)) true) (bvxor ret_6 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_6) #b00000000)) ret_6))) (let ((pow_7 (ite (= (not (= ((_ extract 8 8) (bvshl pow_6 #b000000001)) #b0)) true) (bvxor (bvshl pow_6 #b000000001) y) (bvshl pow_6 #b000000001)))) (let ((ret_7_1 (ite (= (not (= ((_ extract 6 6) x) #b0)) true) (bvxor ret_6_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_6_1) #b00000000)) ret_6_1))) (let ((pow_7_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_6_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_6_1 #b000000001) y) (bvshl pow_6_1 #b000000001)))) (let ((ret_8 (ite (= (not (= ((_ extract 7 7) x) #b0)) true) (bvxor ret_7 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_7) #b00000000)) ret_7))) (let ((pow_8 (ite (= (not (= ((_ extract 8 8) (bvshl pow_7 #b000000001)) #b0)) true) (bvxor (bvshl pow_7 #b000000001) y) (bvshl pow_7 #b000000001)))) (let ((ret_8_1 (ite (= (not (= ((_ extract 7 7) x) #b0)) true) (bvxor ret_7_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_7_1) #b00000000)) ret_7_1))) (let ((pow_8_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_7_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_7_1 #b000000001) y) (bvshl pow_7_1 #b000000001)))) (let ((ret_9 (ite (= (not (= ((_ extract 8 8) x) #b0)) true) (bvxor ret_8 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_8) #b00000000)) ret_8))) (let ((pow_9 (ite (= (not (= ((_ extract 8 8) (bvshl pow_8 #b000000001)) #b0)) true) (bvxor (bvshl pow_8 #b000000001) y) (bvshl pow_8 #b000000001)))) (let ((ret_9_1 (ite (= (not (= ((_ extract 8 8) x) #b0)) true) (bvxor ret_8_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_8_1) #b00000000)) ret_8_1))) (let ((pow_9_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_8_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_8_1 #b000000001) y) (bvshl pow_8_1 #b000000001)))) (let ((ret_5 (ite (= (not (= ((_ extract 9 9) x) #b0)) true) (bvxor ret_9_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_9_1) #b00000000)) ret_9_1))) (let ((pow_5 (ite (= (not (= ((_ extract 8 8) (bvshl pow_9_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_9_1 #b000000001) y) (bvshl pow_9_1 #b000000001)))) (let ((ret_10 (ite (= (not (= ((_ extract 10 10) x) #b0)) true) (bvxor ret_5 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5) #b00000000)) ret_5))) (let ((pow_10 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5 #b000000001)) #b0)) true) (bvxor (bvshl pow_5 #b000000001) y) (bvshl pow_5 #b000000001)))) (let ((ret_11 (ite (= (not (= ((_ extract 11 11) x) #b0)) true) (bvxor ret_10 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_10) #b00000000)) ret_10))) (let ((pow_11 (ite (= (not (= ((_ extract 8 8) (bvshl pow_10 #b000000001)) #b0)) true) (bvxor (bvshl pow_10 #b000000001) y) (bvshl pow_10 #b000000001)))) (let ((ret_12 (ite (= (not (= ((_ extract 12 12) x) #b0)) true) (bvxor ret_11 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_11) #b00000000)) ret_11))) (let ((pow_12 (ite (= (not (= ((_ extract 8 8) (bvshl pow_11 #b000000001)) #b0)) true) (bvxor (bvshl pow_11 #b000000001) y) (bvshl pow_11 #b000000001)))) (let ((ret_13 (ite (= (not (= ((_ extract 13 13) x) #b0)) true) (bvxor ret_12 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_12) #b00000000)) ret_12))) (let ((pow_13 (ite (= (not (= ((_ extract 8 8) (bvshl pow_12 #b000000001)) #b0)) true) (bvxor (bvshl pow_12 #b000000001) y) (bvshl pow_12 #b000000001)))) (let ((ret_14 (ite (= (not (= ((_ extract 14 14) x) #b0)) true) (bvxor ret_13 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_13) #b00000000)) ret_13))) (let ((pow_14 (ite (= (not (= ((_ extract 8 8) (bvshl pow_13 #b000000001)) #b0)) true) (bvxor (bvshl pow_13 #b000000001) y) (bvshl pow_13 #b000000001)))) (let ((ret_15 (ite (= (not (= ((_ extract 15 15) x) #b0)) true) (bvxor ret_14 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_14) #b00000000)) ret_14))) (let ((pow_15 (ite (= (not (= ((_ extract 8 8) (bvshl pow_14 #b000000001)) #b0)) true) (bvxor (bvshl pow_14 #b000000001) y) (bvshl pow_14 #b000000001)))) (ite (= y #b000000000) #b00000000 ret_15))))))))))))))))))))))))))))))))))))))))))))
-(define-fun |GF2BVPoly.polyMul.«8».«8»| ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) (let ((ret (let ((tmp (bvshl #b0000000000000000 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl #b0000000000000000 #b0000000000000001))) (ite (= (not (= ((_ extract 7 7) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_1 (let ((tmp (bvshl ret #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret #b0000000000000001))) (ite (= (not (= ((_ extract 6 6) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_2 (let ((tmp (bvshl ret_1 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_1 #b0000000000000001))) (ite (= (not (= ((_ extract 5 5) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_3 (let ((tmp (bvshl ret_2 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_2 #b0000000000000001))) (ite (= (not (= ((_ extract 4 4) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_4 (let ((tmp (bvshl ret_3 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_3 #b0000000000000001))) (ite (= (not (= ((_ extract 3 3) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_5 (let ((tmp (bvshl ret_4 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_4 #b0000000000000001))) (ite (= (not (= ((_ extract 2 2) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_6 (let ((tmp (bvshl ret_5 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_5 #b0000000000000001))) (ite (= (not (= ((_ extract 1 1) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_7 (let ((tmp (bvshl ret_6 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_6 #b0000000000000001))) (ite (= (not (= ((_ extract 0 0) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) ret_7)))))))))
+(define-fun |GF2BVPoly.polyMul.«8».«8»| ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) (let ((v (let ((v_1 (bvshl #b0000000000000000 #b0000000000000001))) (let ((v_1_1 (concat #b00000000 a))) (let ((v_1_1_1 (bvshl #b0000000000000000 #b0000000000000001))) (ite (= (not (= ((_ extract 7 7) b) #b0)) true) (bvxor v_1_1_1 v_1_1) v_1)))))) (let ((v_1 (let ((v_1_1 (bvshl v #b0000000000000001))) (let ((v_1_1_1 (concat #b00000000 a))) (let ((v_1_1_1_1 (bvshl v #b0000000000000001))) (ite (= (not (= ((_ extract 6 6) b) #b0)) true) (bvxor v_1_1_1_1 v_1_1_1) v_1_1)))))) (let ((v_2 (let ((v_2_1 (bvshl v_1 #b0000000000000001))) (let ((v_2_1_1 (concat #b00000000 a))) (let ((v_2_1_1_1 (bvshl v_1 #b0000000000000001))) (ite (= (not (= ((_ extract 5 5) b) #b0)) true) (bvxor v_2_1_1_1 v_2_1_1) v_2_1)))))) (let ((v_3 (let ((v_3_1 (bvshl v_2 #b0000000000000001))) (let ((v_3_1_1 (concat #b00000000 a))) (let ((v_3_1_1_1 (bvshl v_2 #b0000000000000001))) (ite (= (not (= ((_ extract 4 4) b) #b0)) true) (bvxor v_3_1_1_1 v_3_1_1) v_3_1)))))) (let ((v_4 (let ((v_4_1 (bvshl v_3 #b0000000000000001))) (let ((v_4_1_1 (concat #b00000000 a))) (let ((v_4_1_1_1 (bvshl v_3 #b0000000000000001))) (ite (= (not (= ((_ extract 3 3) b) #b0)) true) (bvxor v_4_1_1_1 v_4_1_1) v_4_1)))))) (let ((v_5 (let ((v_5_1 (bvshl v_4 #b0000000000000001))) (let ((v_5_1_1 (concat #b00000000 a))) (let ((v_5_1_1_1 (bvshl v_4 #b0000000000000001))) (ite (= (not (= ((_ extract 2 2) b) #b0)) true) (bvxor v_5_1_1_1 v_5_1_1) v_5_1)))))) (let ((v_6 (let ((v_6_1 (bvshl v_5 #b0000000000000001))) (let ((v_6_1_1 (concat #b00000000 a))) (let ((v_6_1_1_1 (bvshl v_5 #b0000000000000001))) (ite (= (not (= ((_ extract 1 1) b) #b0)) true) (bvxor v_6_1_1_1 v_6_1_1) v_6_1)))))) (let ((v_7 (let ((v_7_1 (bvshl v_6 #b0000000000000001))) (let ((v_7_1_1 (concat #b00000000 a))) (let ((v_7_1_1_1 (bvshl v_6 #b0000000000000001))) (ite (= (not (= ((_ extract 0 0) b) #b0)) true) (bvxor v_7_1_1_1 v_7_1_1) v_7_1)))))) v_7)))))))))
 (define-fun GaloisField2k.mul.GF256 ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8) (|GF2BVPoly.polyMod.«16».«8»| (|GF2BVPoly.polyMul.«8».«8»| a b) (bvor #b100000000 (concat #b0 #b00011011))))
 (define-fun-rec GF256.pow2 ((k Nat) (x (_ BitVec 8))) (_ BitVec 8) (ite (= k 0) x (GaloisField2k.mul.GF256 (GF256.pow2 (Nat.sub k 1) x) (GF256.pow2 (Nat.sub k 1) x))))
 (declare-const x (_ BitVec 8))

From 7c988814ae090169e94828b65dd165369f9a4bb7 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 5 Sep 2023 23:50:20 -0400
Subject: [PATCH 8/8] chore: use dylib facet for shared library

---
 lean_packages/manifest.json | 10 ----------
 scripts/test.sh             |  2 +-
 tests/aes/GF256Pow.expected |  4 ++--
 3 files changed, 3 insertions(+), 13 deletions(-)
 delete mode 100644 lean_packages/manifest.json

diff --git a/lean_packages/manifest.json b/lean_packages/manifest.json
deleted file mode 100644
index 3991b38..0000000
--- a/lean_packages/manifest.json
+++ /dev/null
@@ -1,10 +0,0 @@
-{"version": 2,
- "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4",
-   "rev": "cf2e683c25eba2d798b2460d5703a63db72272c0",
-   "name": "mathlib",
-   "inputRev": "cf2e683c25eba2d798b2460d5703a63db72272c0"},
-  {"url": "https://github.com/ufmg-smite/lean-smt",
-   "rev": "219fffdf8d850fcb29c46e226d623def13848618",
-   "name": "smt",
-   "inputRev": "main"}]}
diff --git a/scripts/test.sh b/scripts/test.sh
index ef81f0d..7cb3c6f 100755
--- a/scripts/test.sh
+++ b/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
diff --git a/tests/aes/GF256Pow.expected b/tests/aes/GF256Pow.expected
index cd0e0d5..fe54c85 100644
--- a/tests/aes/GF256Pow.expected
+++ b/tests/aes/GF256Pow.expected
@@ -3,9 +3,9 @@ goal: GF256.pow2 8 x = x
 query:
 (define-sort Nat () Int)
 (define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y)))
-(assert (forall ((_uniq.7863 Nat)) (=> (>= _uniq.7863 0) (forall ((_uniq.7864 Nat)) (=> (>= _uniq.7864 0) (>= (Nat.sub _uniq.7863 _uniq.7864) 0))))))
+(assert (forall ((_uniq.7776 Nat)) (=> (>= _uniq.7776 0) (forall ((_uniq.7777 Nat)) (=> (>= _uniq.7777 0) (>= (Nat.sub _uniq.7776 _uniq.7777) 0))))))
 (define-fun |GF2BVPoly.polyMod.«16».«8»| ((x (_ BitVec 16)) (y (_ BitVec 9))) (_ BitVec 8) (let ((ret #b00000000)) (let ((pow (ite (= (not (= ((_ extract 8 8) #b000000001) #b0)) true) (bvxor #b000000001 y) #b000000001))) (let ((ret_1 (ite (= (not (= ((_ extract 0 0) x) #b0)) true) (bvxor ret (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow) #b00000000)) ret))) (let ((pow_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow #b000000001)) #b0)) true) (bvxor (bvshl pow #b000000001) y) (bvshl pow #b000000001)))) (let ((ret_2 (ite (= (not (= ((_ extract 1 1) x) #b0)) true) (bvxor ret_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_1) #b00000000)) ret_1))) (let ((pow_2 (ite (= (not (= ((_ extract 8 8) (bvshl pow_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_1 #b000000001) y) (bvshl pow_1 #b000000001)))) (let ((ret_3 (ite (= (not (= ((_ extract 2 2) x) #b0)) true) (bvxor ret_2 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_2) #b00000000)) ret_2))) (let ((pow_3 (ite (= (not (= ((_ extract 8 8) (bvshl pow_2 #b000000001)) #b0)) true) (bvxor (bvshl pow_2 #b000000001) y) (bvshl pow_2 #b000000001)))) (let ((ret_4 (ite (= (not (= ((_ extract 3 3) x) #b0)) true) (bvxor ret_3 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_3) #b00000000)) ret_3))) (let ((pow_4 (ite (= (not (= ((_ extract 8 8) (bvshl pow_3 #b000000001)) #b0)) true) (bvxor (bvshl pow_3 #b000000001) y) (bvshl pow_3 #b000000001)))) (let ((ret_5_1 (ite (= (not (= ((_ extract 4 4) x) #b0)) true) (bvxor ret_4 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_4) #b00000000)) ret_4))) (let ((pow_5_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_4 #b000000001)) #b0)) true) (bvxor (bvshl pow_4 #b000000001) y) (bvshl pow_4 #b000000001)))) (let ((ret_6 (ite (= (not (= ((_ extract 5 5) x) #b0)) true) (bvxor ret_5_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5_1) #b00000000)) ret_5_1))) (let ((pow_6 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_5_1 #b000000001) y) (bvshl pow_5_1 #b000000001)))) (let ((ret_6_1 (ite (= (not (= ((_ extract 5 5) x) #b0)) true) (bvxor ret_5_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5_1) #b00000000)) ret_5_1))) (let ((pow_6_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_5_1 #b000000001) y) (bvshl pow_5_1 #b000000001)))) (let ((ret_7 (ite (= (not (= ((_ extract 6 6) x) #b0)) true) (bvxor ret_6 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_6) #b00000000)) ret_6))) (let ((pow_7 (ite (= (not (= ((_ extract 8 8) (bvshl pow_6 #b000000001)) #b0)) true) (bvxor (bvshl pow_6 #b000000001) y) (bvshl pow_6 #b000000001)))) (let ((ret_7_1 (ite (= (not (= ((_ extract 6 6) x) #b0)) true) (bvxor ret_6_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_6_1) #b00000000)) ret_6_1))) (let ((pow_7_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_6_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_6_1 #b000000001) y) (bvshl pow_6_1 #b000000001)))) (let ((ret_8 (ite (= (not (= ((_ extract 7 7) x) #b0)) true) (bvxor ret_7 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_7) #b00000000)) ret_7))) (let ((pow_8 (ite (= (not (= ((_ extract 8 8) (bvshl pow_7 #b000000001)) #b0)) true) (bvxor (bvshl pow_7 #b000000001) y) (bvshl pow_7 #b000000001)))) (let ((ret_8_1 (ite (= (not (= ((_ extract 7 7) x) #b0)) true) (bvxor ret_7_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_7_1) #b00000000)) ret_7_1))) (let ((pow_8_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_7_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_7_1 #b000000001) y) (bvshl pow_7_1 #b000000001)))) (let ((ret_9 (ite (= (not (= ((_ extract 8 8) x) #b0)) true) (bvxor ret_8 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_8) #b00000000)) ret_8))) (let ((pow_9 (ite (= (not (= ((_ extract 8 8) (bvshl pow_8 #b000000001)) #b0)) true) (bvxor (bvshl pow_8 #b000000001) y) (bvshl pow_8 #b000000001)))) (let ((ret_9_1 (ite (= (not (= ((_ extract 8 8) x) #b0)) true) (bvxor ret_8_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_8_1) #b00000000)) ret_8_1))) (let ((pow_9_1 (ite (= (not (= ((_ extract 8 8) (bvshl pow_8_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_8_1 #b000000001) y) (bvshl pow_8_1 #b000000001)))) (let ((ret_5 (ite (= (not (= ((_ extract 9 9) x) #b0)) true) (bvxor ret_9_1 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_9_1) #b00000000)) ret_9_1))) (let ((pow_5 (ite (= (not (= ((_ extract 8 8) (bvshl pow_9_1 #b000000001)) #b0)) true) (bvxor (bvshl pow_9_1 #b000000001) y) (bvshl pow_9_1 #b000000001)))) (let ((ret_10 (ite (= (not (= ((_ extract 10 10) x) #b0)) true) (bvxor ret_5 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_5) #b00000000)) ret_5))) (let ((pow_10 (ite (= (not (= ((_ extract 8 8) (bvshl pow_5 #b000000001)) #b0)) true) (bvxor (bvshl pow_5 #b000000001) y) (bvshl pow_5 #b000000001)))) (let ((ret_11 (ite (= (not (= ((_ extract 11 11) x) #b0)) true) (bvxor ret_10 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_10) #b00000000)) ret_10))) (let ((pow_11 (ite (= (not (= ((_ extract 8 8) (bvshl pow_10 #b000000001)) #b0)) true) (bvxor (bvshl pow_10 #b000000001) y) (bvshl pow_10 #b000000001)))) (let ((ret_12 (ite (= (not (= ((_ extract 12 12) x) #b0)) true) (bvxor ret_11 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_11) #b00000000)) ret_11))) (let ((pow_12 (ite (= (not (= ((_ extract 8 8) (bvshl pow_11 #b000000001)) #b0)) true) (bvxor (bvshl pow_11 #b000000001) y) (bvshl pow_11 #b000000001)))) (let ((ret_13 (ite (= (not (= ((_ extract 13 13) x) #b0)) true) (bvxor ret_12 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_12) #b00000000)) ret_12))) (let ((pow_13 (ite (= (not (= ((_ extract 8 8) (bvshl pow_12 #b000000001)) #b0)) true) (bvxor (bvshl pow_12 #b000000001) y) (bvshl pow_12 #b000000001)))) (let ((ret_14 (ite (= (not (= ((_ extract 14 14) x) #b0)) true) (bvxor ret_13 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_13) #b00000000)) ret_13))) (let ((pow_14 (ite (= (not (= ((_ extract 8 8) (bvshl pow_13 #b000000001)) #b0)) true) (bvxor (bvshl pow_13 #b000000001) y) (bvshl pow_13 #b000000001)))) (let ((ret_15 (ite (= (not (= ((_ extract 15 15) x) #b0)) true) (bvxor ret_14 (ite (<= (+ 0 1) 8) ((_ extract 7 0) pow_14) #b00000000)) ret_14))) (let ((pow_15 (ite (= (not (= ((_ extract 8 8) (bvshl pow_14 #b000000001)) #b0)) true) (bvxor (bvshl pow_14 #b000000001) y) (bvshl pow_14 #b000000001)))) (ite (= y #b000000000) #b00000000 ret_15))))))))))))))))))))))))))))))))))))))))))))
-(define-fun |GF2BVPoly.polyMul.«8».«8»| ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) (let ((v (let ((v_1 (bvshl #b0000000000000000 #b0000000000000001))) (let ((v_1_1 (concat #b00000000 a))) (let ((v_1_1_1 (bvshl #b0000000000000000 #b0000000000000001))) (ite (= (not (= ((_ extract 7 7) b) #b0)) true) (bvxor v_1_1_1 v_1_1) v_1)))))) (let ((v_1 (let ((v_1_1 (bvshl v #b0000000000000001))) (let ((v_1_1_1 (concat #b00000000 a))) (let ((v_1_1_1_1 (bvshl v #b0000000000000001))) (ite (= (not (= ((_ extract 6 6) b) #b0)) true) (bvxor v_1_1_1_1 v_1_1_1) v_1_1)))))) (let ((v_2 (let ((v_2_1 (bvshl v_1 #b0000000000000001))) (let ((v_2_1_1 (concat #b00000000 a))) (let ((v_2_1_1_1 (bvshl v_1 #b0000000000000001))) (ite (= (not (= ((_ extract 5 5) b) #b0)) true) (bvxor v_2_1_1_1 v_2_1_1) v_2_1)))))) (let ((v_3 (let ((v_3_1 (bvshl v_2 #b0000000000000001))) (let ((v_3_1_1 (concat #b00000000 a))) (let ((v_3_1_1_1 (bvshl v_2 #b0000000000000001))) (ite (= (not (= ((_ extract 4 4) b) #b0)) true) (bvxor v_3_1_1_1 v_3_1_1) v_3_1)))))) (let ((v_4 (let ((v_4_1 (bvshl v_3 #b0000000000000001))) (let ((v_4_1_1 (concat #b00000000 a))) (let ((v_4_1_1_1 (bvshl v_3 #b0000000000000001))) (ite (= (not (= ((_ extract 3 3) b) #b0)) true) (bvxor v_4_1_1_1 v_4_1_1) v_4_1)))))) (let ((v_5 (let ((v_5_1 (bvshl v_4 #b0000000000000001))) (let ((v_5_1_1 (concat #b00000000 a))) (let ((v_5_1_1_1 (bvshl v_4 #b0000000000000001))) (ite (= (not (= ((_ extract 2 2) b) #b0)) true) (bvxor v_5_1_1_1 v_5_1_1) v_5_1)))))) (let ((v_6 (let ((v_6_1 (bvshl v_5 #b0000000000000001))) (let ((v_6_1_1 (concat #b00000000 a))) (let ((v_6_1_1_1 (bvshl v_5 #b0000000000000001))) (ite (= (not (= ((_ extract 1 1) b) #b0)) true) (bvxor v_6_1_1_1 v_6_1_1) v_6_1)))))) (let ((v_7 (let ((v_7_1 (bvshl v_6 #b0000000000000001))) (let ((v_7_1_1 (concat #b00000000 a))) (let ((v_7_1_1_1 (bvshl v_6 #b0000000000000001))) (ite (= (not (= ((_ extract 0 0) b) #b0)) true) (bvxor v_7_1_1_1 v_7_1_1) v_7_1)))))) v_7)))))))))
+(define-fun |GF2BVPoly.polyMul.«8».«8»| ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 16) (let ((ret (let ((tmp (bvshl #b0000000000000000 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl #b0000000000000000 #b0000000000000001))) (ite (= (not (= ((_ extract 7 7) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_1 (let ((tmp (bvshl ret #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret #b0000000000000001))) (ite (= (not (= ((_ extract 6 6) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_2 (let ((tmp (bvshl ret_1 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_1 #b0000000000000001))) (ite (= (not (= ((_ extract 5 5) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_3 (let ((tmp (bvshl ret_2 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_2 #b0000000000000001))) (ite (= (not (= ((_ extract 4 4) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_4 (let ((tmp (bvshl ret_3 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_3 #b0000000000000001))) (ite (= (not (= ((_ extract 3 3) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_5 (let ((tmp (bvshl ret_4 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_4 #b0000000000000001))) (ite (= (not (= ((_ extract 2 2) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_6 (let ((tmp (bvshl ret_5 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_5 #b0000000000000001))) (ite (= (not (= ((_ extract 1 1) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) (let ((ret_7 (let ((tmp (bvshl ret_6 #b0000000000000001))) (let ((r (concat #b00000000 a))) (let ((tmp_1 (bvshl ret_6 #b0000000000000001))) (ite (= (not (= ((_ extract 0 0) b) #b0)) true) (bvxor tmp_1 r) tmp)))))) ret_7)))))))))
 (define-fun GaloisField2k.mul.GF256 ((a (_ BitVec 8)) (b (_ BitVec 8))) (_ BitVec 8) (|GF2BVPoly.polyMod.«16».«8»| (|GF2BVPoly.polyMul.«8».«8»| a b) (bvor #b100000000 (concat #b0 #b00011011))))
 (define-fun-rec GF256.pow2 ((k Nat) (x (_ BitVec 8))) (_ BitVec 8) (ite (= k 0) x (GaloisField2k.mul.GF256 (GF256.pow2 (Nat.sub k 1) x) (GF256.pow2 (Nat.sub k 1) x))))
 (declare-const x (_ BitVec 8))