From a54bfd09140e1f6ba50ec75bdba8ff1f22472baf Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Fri, 22 Nov 2024 01:02:52 +0000 Subject: [PATCH] Add an example for problem with bv_decide --- Proofs/AES-GCM/GCMInitV8Sym.lean | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 19e2cddb..e298b854 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -537,7 +537,15 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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] + 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