Revert "Exposing the bv_decide problem"

This reverts commit e7e3cf6.
pennyannn · Dec 2, 2024 · 42ae5e1 · 42ae5e1
1 parent e7e3cf6
commit 42ae5e1
Showing 1 changed file with 11 additions and 17 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,13 +202,6 @@ 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
@@ -542,16 +535,17 @@ 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]
-    simp only [hi, lo] at *
-    -- simp only [mwe]
-    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]
+    -- 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
   have h_H3 : r (StateField.SFP 23#5) s77 =
     let x_rev := (lo x1) ++ (hi x1)
     let H0 := gcm_init_H_asm x_rev