Turn bv_decide into bv_check

leanprover · Oct 11, 2024 · 1fdd2f5 · 1fdd2f5
1 parent 1b5df7c
commit 1fdd2f5
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean
@@ -114,4 +114,4 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState)
       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]
-    bv_decide
+    bv_check "GCMInitV8Sym.lean-GCMInitV8Program.gcm_init_v8_program_correct-117-4.lrat"
diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean-GCMInitV8Program.gcm_init_v8_program_correct-117-4.lrat b/Proofs/AES-GCM/GCMInitV8Sym.lean-GCMInitV8Program.gcm_init_v8_program_correct-117-4.lrat