Exposing the bv_decide problem

leanprover · Nov 22, 2024 · e7e3cf6 · e7e3cf6
1 parent a54bfd0
commit e7e3cf6
Showing 1 changed file with 17 additions and 11 deletions.
diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean
@@ -106,7 +106,7 @@ def gcm_init_H_asm (H : BitVec 128) : BitVec 128 :=
 set_option maxRecDepth 3000 in
 set_option maxHeartbeats 1000000 in
 set_option sat.timeout 120 in
--- set_option debug.byAsSorry true in
+set_option debug.byAsSorry true in
 -- set_option trace.profiler true in
 theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) :
   GCMV8.gcm_init_H x = gcm_init_H_asm x := by
@@ -202,6 +202,13 @@ theorem gcm_polyval_asm_associativity
   gcm_polyval_asm (gcm_polyval_asm x y) z := by
   sorry
 
+theorem mwe (x1 : BitVec 128):
+  let p := gcm_polyval_asm (gcm_init_H_asm (BitVec.extractLsb' 0 64 x1 ++ BitVec.extractLsb' 64 64 x1))
+      (gcm_init_H_asm (BitVec.extractLsb' 0 64 x1 ++ BitVec.extractLsb' 64 64 x1))
+  BitVec.extractLsb' 64 64 p ++ BitVec.extractLsb' 0 64 p ^^^ BitVec.extractLsb' 0 64 p ++ BitVec.extractLsb' 64 64 p =
+  (BitVec.extractLsb' 64 64 p ^^^ BitVec.extractLsb' 0 64 p) ++
+    (BitVec.extractLsb' 64 64 p ^^^ BitVec.extractLsb' 0 64 p) := by bv_decide
+
 ------------------------------------
 
 set_option maxRecDepth 5000 in
@@ -535,17 +542,16 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
       h_s73_non_effects, h_s72_q18, h_s72_non_effects,
     ]
     have q0 : (r (StateField.SFP 22#5) s71) = (r (StateField.SFP 22#5) s37) := by sym_aggregate
-    simp only [q0, h_H2, hi, lo, extractLsb'_of_append_mid,
-      extractLsb'_of_append_hi, extractLsb'_of_append_lo,
-      bv_append_64_128, ←xor_of_append_append_of_xor_equiv
-      ]
-    -- FIXME: The following wouldn't work
     -- simp only [q0, h_H2, hi, lo, extractLsb'_of_append_mid,
-    --   extractLsb'_of_append_hi, extractLsb'_of_append_lo]
-    -- generalize gcm_polyval_asm
-    --   (gcm_init_H_asm (BitVec.extractLsb' 0 64 x1 ++ BitVec.extractLsb' 64 64 x1))
-    --   (gcm_init_H_asm (BitVec.extractLsb' 0 64 x1 ++ BitVec.extractLsb' 64 64 x1)) = p
-    -- bv_decide
+    --   extractLsb'_of_append_hi, extractLsb'_of_append_lo,
+    --   bv_append_64_128, ←xor_of_append_append_of_xor_equiv
+    --   ]
+    -- FIXME: The following wouldn't work
+    simp only [q0, h_H2, hi, lo, extractLsb'_of_append_mid,
+      extractLsb'_of_append_hi, extractLsb'_of_append_lo]
+    simp only [hi, lo] at *
+    -- simp only [mwe]
+    bv_decide
   have h_H3 : r (StateField.SFP 23#5) s77 =
     let x_rev := (lo x1) ++ (hi x1)
     let H0 := gcm_init_H_asm x_rev