Trying out

Proofs/AES-GCM/GCMInitV8Sym.lean

@@ -38,7 +38,7 @@ theorem gcm_init_v8_program_run_152 (s0 sf : ArmState)
 set_option maxRecDepth 100000 in
 set_option maxHeartbeats 500000 in
 set_option sat.timeout 120 in
-set_option trace.profiler true in
+-- set_option trace.profiler true in
 -- set_option pp.deepTerms true in
 -- set_option pp.maxSteps 10000 in
 -- set_option trace.profiler true in
@@ -111,11 +111,15 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
       GCMV8.reduce, GCMV8.degree, GCMV8.degree.degreeTR]
     simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.reduceExtracLsb',
       BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.ofNat_eq_ofNat,
-      BitVec.reduceEq, ↓reduceIte, BitVec.zero_eq, Nat.sub_self, BitVec.ushiftRight_zero_eq,
+      BitVec.reduceEq, ↓reduceIte, Nat.sub_self, BitVec.ushiftRight_zero_eq, Nat.reduceMul,
       BitVec.reduceAnd, BitVec.toNat_ofNat, Nat.pow_one, Nat.reduceMod, Nat.mul_zero, Nat.add_zero,
       Nat.zero_mod, Nat.zero_add, Nat.sub_zero, Nat.mul_one, Nat.zero_mul, Nat.one_mul,
-      Nat.reduceSub, BitVec.reduceMul, BitVec.reduceXOr, BitVec.mul_one, Nat.add_one_sub_one,
-      BitVec.one_mul]
+      Nat.reduceSub, BitVec.and_self, BitVec.getLsbD_one, Nat.zero_lt_succ, decide_True,
+      reduceCtorEq, decide_False, Bool.and_false, BitVec.ofBool_false, BitVec.replicate_succ_eq,
+      BitVec.replicate_zero_eq, BitVec.append_zero_width, BitVec.cast_eq, BitVec.reduceXOr,
+      BitVec.zero_and, BitVec.not_zero, BitVec.reduceAllOnes, BitVec.zero_or, BitVec.mul_one,
+      BitVec.zero_xor, BitVec.reduceGetLsb, Nat.add_one_sub_one, BitVec.ofBool_true,
+      BitVec.reduceNot, BitVec.or_zero]
     bv_decide
     -- bv_check "lrat_files/GCMInitV8Sym.lean-GCMInitV8Program.gcm_init_v8_program_correct-117-4.lrat"
     -- TODO: proof works in vscode but timeout in the CI -- need to investigate further

Specs/GCMV8.lean

@@ -71,8 +71,10 @@ example: GCMV8.degree 0b1101#4 = 3 := rfl
 /-- Subtract x from y if y's x-degree-th bit is 1.
     Defined using non-ite statements. -/
 def reduce (x : BitVec n) (y : BitVec n) : BitVec n :=
-  let is_one := (y >>> (GCMV8.degree x)) &&& 1#n
-  y ^^^ (is_one * x)
+  let is_one := ofBool $ getLsbD y (GCMV8.degree x)
+  have h : 1 * n = n := by omega
+  let dup := BitVec.cast h $ replicate n is_one
+  (dup &&& (y ^^^ x) ||| (~~~dup) &&& y)
 
 /-- Performs division of polynomials over GF(2). -/
 def pdiv (x: BitVec n) (y : BitVec m): BitVec n :=
@@ -104,8 +106,10 @@ def pmod (x : BitVec n) (y : BitVec (m + 1)) (H : 0 < m) : BitVec m :=
       -- let xi := getLsbD x (n - i)
       -- let tmp :=
       --     if xi then extractLsb' 0 m p else 0#m
-      let is_one := extractLsb' 0 m ((x >>> (n - i)) &&& 1)
-      let tmp := is_one * extractLsb' 0 m p
+      let is_one := ofBool $ getLsbD x (n - i)
+      have h : 1 * m = m := by omega
+      let dup := BitVec.cast h (replicate m is_one)
+      let tmp := dup &&& (extractLsb' 0 m p)
       let r := r ^^^ tmp
       pmodTR x y (GCMV8.reduce y (p <<< 1)) j r H
   if y = 0 then 0 else pmodTR x y (GCMV8.reduce y 1) n (0#m) H
@@ -189,7 +193,7 @@ def GCMInitV8 (H : BitVec 128) : (List (BitVec 128)) :=
   [H0_rev, H1, H2_rev, H3_rev, H4, H5_rev, H6_rev,
    H7, H8_rev, H9_rev, H10, H11_rev]
 
-set_option maxRecDepth 8000 in
+set_option maxRecDepth 12000 in
 example :  GCMInitV8 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 ==
   [ 0x1099f4b39468565ccdd297a9df145877#128,
     0x62d81a7fe5da3296dd4b631a4b7c0e2b#128,