From da3b43475e6e97b3c81b68d69f83abafb14dc89b Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 21 Nov 2024 20:03:43 +0000 Subject: [PATCH] Proving h_v16_s144 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 80 +++++++++++++++++++++++++++----- 1 file changed, 68 insertions(+), 12 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index edff150a..0da95767 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -727,6 +727,19 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append] + have h_v16_s111 : r (StateField.SFP 16#5) s111 = + let x_rev := (lo x1) ++ (hi x1) + let H0 := gcm_init_H_asm x_rev + let H2 := gcm_polyval_asm H0 H0 + let H3 := gcm_polyval_asm H0 H2 + let H5 := gcm_polyval_asm H0 H3 + let H6 := gcm_polyval_asm H0 H5 + (hi H6 ^^^ lo H6) ++ (hi H6 ^^^ lo H6) := by sorry + have h_v18_113 : r (StateField.SFP 18#5) s113 = + let x_rev := (lo x1) ++ (hi x1) + let H0 := gcm_init_H_asm x_rev + let H2 := gcm_polyval_asm H0 H0 + (hi H2 ^^^ lo H2) ++ (hi H2 ^^^ lo H2) := by sorry have h_H6 : r (StateField.SFP 26#5) s115 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -809,7 +822,50 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) let H6 := gcm_polyval_asm H0 H5 let H8 := gcm_polyval_asm H0 H6 gcm_polyval_asm H0 H8 := by - sorry + simp (config := {decide := true}) only [ + h_s144_q16, h_s144_non_effects, h_s143_non_effects, + h_s142_q18, h_s142_non_effects, h_s141_non_effects, + h_s140_q0, h_s140_non_effects, h_s139_non_effects, + h_s138_q18, h_s138_non_effects, h_s137_non_effects, + h_s136_q0, h_s136_non_effects, h_s135_non_effects, + h_s134_q1, h_s134_non_effects, h_s133_non_effects, + h_s132_q2, h_s132_non_effects, h_s131_non_effects, + h_s130_non_effects, h_s129_q18, h_s129_non_effects, + h_s128_q1, h_s128_non_effects, h_s127_non_effects, + h_s126_non_effects, h_s125_q1, h_s125_non_effects, + h_s124_q18, h_s124_non_effects, h_s123_non_effects, + h_s122_q16, h_s122_non_effects, h_s121_non_effects, + h_s120_q1, h_s120_non_effects, h_s119_non_effects, + h_s118_q2, h_s118_non_effects, h_s117_non_effects, + h_s116_q0, h_s116_non_effects + ] + have q0 : r (StateField.SFP 22#5) s115 = r (StateField.SFP 22#5) s37 := by sorry + have q1 : r (StateField.SFP 16#5) s115 = r (StateField.SFP 16#5) s111 := by sorry + have q2 : r (StateField.SFP 18#5) s115 = r (StateField.SFP 18#5) s113 := by sorry + have q3 : r (StateField.SFP 19#5) s115 = r (StateField.SFP 19#5) s17 := by sorry + simp only [q0, q1, q2, q3, h_H6, h_H2, h_v16_s111, h_v18_113, h_e1] + generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 + generalize h_H2_var : (gcm_polyval_asm H0 H0) = H2 + generalize (gcm_polyval_asm H0 (gcm_polyval_asm H0 (gcm_polyval_asm H0 H2))) = H5 + -- simplifying LHS + simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, + gcm_polyval_asm_gcm_polyval_equiv, + hi, lo, BitVec.partInstall] + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, + extractLsb'_of_xor_of_append] + -- simplifying RHS + conv => + rhs + simp only [gcm_polyval_asm_associativity, h_H2_var] + rw [gcm_polyval_asm_commutativity] + simp only [gcm_polyval_asm, BitVec.partInstall] + simp only [hi, lo] at * + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, + extractLsb'_of_xor_of_append] + rw [polynomial_mult_commutativity (BitVec.extractLsb' 64 64 H2) (BitVec.extractLsb' 64 64 H5)] + rw [polynomial_mult_commutativity (BitVec.extractLsb' 0 64 H2) (BitVec.extractLsb' 0 64 H5)] have h_v17_s145 : r (StateField.SFP 17#5) s145 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -899,57 +955,57 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) sym_aggregate bv_decide · sym_aggregate - · have q : r (StateField.SFP 20#5) s151 = r (StateField.SFP 20#5) s17 := by sym_aggregate + · have q : r (StateField.SFP 20#5) s151 = r (StateField.SFP 20#5) s17 := by sorry simp only [q, h_H0, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 21#5) s151 = r (StateField.SFP 21#5) s37 := by sym_aggregate + · have q : r (StateField.SFP 21#5) s151 = r (StateField.SFP 21#5) s37 := by sorry simp only [q, h_H1, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 22#5) s151 = r (StateField.SFP 22#5) s37 := by sym_aggregate + · have q : r (StateField.SFP 22#5) s151 = r (StateField.SFP 22#5) s37 := by sorry simp only [q, h_H2, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 23#5) s151 = r (StateField.SFP 23#5) s77 := by sym_aggregate + · have q : r (StateField.SFP 23#5) s151 = r (StateField.SFP 23#5) s77 := by sorry simp only [q, h_H3, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 24#5) s151 = r (StateField.SFP 24#5) s77 := by sym_aggregate + · have q : r (StateField.SFP 24#5) s151 = r (StateField.SFP 24#5) s77 := by sorry simp only [q, h_H4, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 25#5) s151 = r (StateField.SFP 25#5) s77 := by sym_aggregate + · have q : r (StateField.SFP 25#5) s151 = r (StateField.SFP 25#5) s77 := by sorry simp only [q, h_H5, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 26#5) s151 = r (StateField.SFP 26#5) s115 := by sym_aggregate + · have q : r (StateField.SFP 26#5) s151 = r (StateField.SFP 26#5) s115 := by sorry simp only [q, h_H6, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 27#5) s151 = r (StateField.SFP 27#5) s115 := by sym_aggregate + · have q : r (StateField.SFP 27#5) s151 = r (StateField.SFP 27#5) s115 := by sorry simp only [q, h_H7, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 28#5) s151 = r (StateField.SFP 28#5) s115 := by sym_aggregate + · have q : r (StateField.SFP 28#5) s151 = r (StateField.SFP 28#5) s115 := by sorry simp only [q, h_H8, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 29#5) s151 = r (StateField.SFP 29#5) s151 := by sym_aggregate + · have q : r (StateField.SFP 29#5) s151 = r (StateField.SFP 29#5) s151 := by sorry simp only [q, h_H9, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, gcm_polyval_asm_gcm_polyval_equiv] - · have q : r (StateField.SFP 30#5) s151 = r (StateField.SFP 30#5) s151 := by sym_aggregate + · have q : r (StateField.SFP 30#5) s151 = r (StateField.SFP 30#5) s151 := by sorry simp only [q, h_H10, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv,