From e37d50f6d72fb4c4150a6dd3f21240539984c425 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Tue, 12 Nov 2024 18:44:34 +0000 Subject: [PATCH 01/27] More gcm_init_v8 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 48 ++++++++++++++++++++++++-------- 1 file changed, 36 insertions(+), 12 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index c5edc1b6..973737b5 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -16,8 +16,24 @@ set_option bv.ac_nf false abbrev H_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 1#5) s abbrev Htable_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 0#5) s -set_option maxRecDepth 2000 in -set_option maxHeartbeats 500000 in +-- Taken from gcm_gmult_v8 +theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : + DPSFP.pmull_op 0 64 1 x y 0#128 = + DPSFP.polynomial_mult x y := by + unfold DPSFP.pmull_op + simp (config := {ground := true}) only [minimal_theory] + unfold DPSFP.pmull_op + simp (config := {ground := true}) only [minimal_theory] + simp only [state_simp_rules, bitvec_rules] + done + +-- (TODO) Should we simply replace one function by the other here? +theorem gcm_polyval_mul_eq_polynomial_mult {x y : BitVec 128} : + GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by + sorry + +set_option maxRecDepth 10000 in +set_option maxHeartbeats 4000000 in set_option sat.timeout 120 in -- set_option pp.deepTerms true in -- set_option pp.maxSteps 10000 in @@ -47,9 +63,12 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) -- H_addr ptr stays the same ∧ H_addr sf = H_addr s0 -- v20 - v31 stores results of Htable + -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + -- read_sfp 128 20#5 sf = + -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 0 ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) - read_sfp 128 20#5 sf = - (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 0 + read_sfp 128 21#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 1 -- -- TODO: Commenting out memory related conjuncts since it seems -- to make symbolic execution stuck @@ -86,14 +105,19 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) generalize Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = Hinit -- change the type of Hinit to be BitVec 128, assuming that's def-eq change BitVec 128 at Hinit + simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq] simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi, GCMV8.gcm_init_H, GCMV8.refpoly, GCMV8.pmod, GCMV8.pmod.pmodTR, - GCMV8.reduce, GCMV8.degree, GCMV8.degree.degreeTR] - simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.reduceExtracLsb', - BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.ofNat_eq_ofNat, - BitVec.reduceEq, ↓reduceIte, Nat.sub_self, BitVec.ushiftRight_zero_eq, BitVec.reduceAnd, - BitVec.toNat_ofNat, Nat.pow_one, Nat.reduceMod, Nat.mul_zero, Nat.add_zero, Nat.zero_mod, - Nat.zero_add, Nat.sub_zero, Nat.mul_one, Nat.zero_mul, Nat.one_mul, Nat.reduceSub, - BitVec.and_self, BitVec.zero_and, BitVec.reduceMul, BitVec.xor_zero, BitVec.mul_one, - BitVec.zero_xor, Nat.add_one_sub_one, BitVec.one_mul, BitVec.reduceXOr] + GCMV8.reduce, GCMV8.degree, GCMV8.degree.degreeTR, + GCMV8.gcm_polyval, GCMV8.gcm_polyval_red, GCMV8.irrepoly, + BitVec.reverse, BitVec.reverse.reverseTR, BitVec.partInstall + ] + simp only [gcm_polyval_mul_eq_polynomial_mult] + simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.reduceExtracLsb', BitVec.reduceHShiftLeft, + BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, + BitVec.reduceSetWidth, BitVec.reduceNot, BitVec.shiftLeft_zero_eq, BitVec.zero_eq, Nat.sub_self, BitVec.zero_and, + Nat.add_one_sub_one, BitVec.ofNat_eq_ofNat, BitVec.reduceEq, ↓reduceIte, BitVec.ushiftRight_zero_eq, BitVec.reduceAnd, + BitVec.toNat_ofNat, Nat.pow_one, Nat.reduceMod, Nat.mul_zero, Nat.add_zero, Nat.zero_mod, Nat.zero_add, Nat.sub_zero, + Nat.mul_one, Nat.zero_mul, Nat.one_mul, Nat.reduceSub, BitVec.and_self, BitVec.reduceMul, BitVec.xor_zero, + BitVec.mul_one, BitVec.zero_xor, BitVec.one_mul, BitVec.reduceXOr, BitVec.zero_or] bv_decide From 4410723dbc11fd9dbf3d8ad83bb46c0b4d977889 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 13 Nov 2024 00:19:41 +0000 Subject: [PATCH 02/27] Add an important lemma --- Proofs/AES-GCM/GCMInitV8Sym.lean | 101 ++++++++++++++++++++++++++----- Specs/GCMV8.lean | 2 + 2 files changed, 87 insertions(+), 16 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 973737b5..765e7dd3 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -16,6 +16,40 @@ set_option bv.ac_nf false abbrev H_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 1#5) s abbrev Htable_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 0#5) s +abbrev lo (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 0 64 x +abbrev hi (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 64 64 x + +-- The following represents the assembly version of gcm_polyval +def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := + let v19 := 0xe1#128 + let v19 := BitVec.shiftLeft (hi v19) 57 ++ BitVec.shiftLeft (lo v19) 57 + let v16 := ((lo x) ^^^ (hi x)) ++ ((hi x) ^^^ (lo x)) + let v17 := ((lo y) ^^^ (hi y)) ++ ((hi y) ^^^ (lo y)) + let x := (lo x) ++ (hi x) + let y := (lo y) ++ (hi y) + let v0 := DPSFP.polynomial_mult (hi x) (hi y) + let v2 := DPSFP.polynomial_mult (lo x) (lo y) + let v1 := DPSFP.polynomial_mult (lo v16) (lo v17) + let v16 := (lo v2) ++ (hi v0) + let v18 := v0 ^^^ v2 + let v1 := v1 ^^^ v16 + let v1 := v1 ^^^ v18 + let v18 := DPSFP.polynomial_mult (lo v0) (lo v19) + let v2 := BitVec.partInstall 0 64 (hi v1) v2 + let v1 := BitVec.partInstall 64 64 (lo v0) v1 + let v0 := v1 ^^^ v18 + let v18 := (lo v0) ++ (hi v0) + let v0 := DPSFP.polynomial_mult (lo v0) (lo v19) + let v18 := v18 ^^^ v2 + let v16 := v0 ^^^ v18 + let v23 := (hi v16) ++ (lo v16) + v23 + +#eval gcm_polyval_asm 0xcdd297a9df1458771099f4b39468565c#128 0x88d320376963120dea0b3a488cb9209b#128 + +theorem gcm_polyval_asm_gcm_polyval_equiv (x : BitVec 128) (y : BitVec 128) : + GCMV8.gcm_polyval x y = gcm_polyval_asm x y := by sorry + -- Taken from gcm_gmult_v8 theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : DPSFP.pmull_op 0 64 1 x y 0#128 = @@ -28,10 +62,38 @@ theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : done -- (TODO) Should we simply replace one function by the other here? -theorem gcm_polyval_mul_eq_polynomial_mult {x y : BitVec 128} : +theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by sorry +theorem extractLsb'_of_append_mid (x : BitVec 128) : + BitVec.extractLsb' 64 128 (x ++ x) + = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x := by + sorry + +theorem extractLsb'_of_append_hi (x y : BitVec 64) : + BitVec.extractLsb' 64 64 (x ++ y) = x := by + sorry + +theorem extractLsb'_of_append_lo (x y : BitVec 64) : + BitVec.extractLsb' 0 64 (x ++ y) = y := by + sorry + +theorem crock3 (x : BitVec 32) : + (BitVec.extractLsb' 0 32 (x ++ x ++ x ++ x)) = x := by sorry + +theorem crock4 (x : BitVec 32) : + (BitVec.extractLsb' 32 32 (x ++ x ++ x ++ x)) = x := by sorry + +theorem crock5 (x : BitVec 32) : + (BitVec.extractLsb' 64 32 (x ++ x ++ x ++ x)) = x := by sorry + +theorem crock6 (x : BitVec 32) : + (BitVec.extractLsb' 96 32 (x ++ x ++ x ++ x)) = x := by sorry + +theorem crock7 (x : BitVec 128) : + (BitVec.setWidth 64 x) = BitVec.extractLsb' 0 64 x := by sorry + set_option maxRecDepth 10000 in set_option maxHeartbeats 4000000 in set_option sat.timeout 120 in @@ -101,23 +163,30 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) , shift_right_common_aux_64_2_tff , shift_right_common_aux_32_4_fff , DPSFP.AdvSIMDExpandImm - , DPSFP.dup_aux_0_4_32] + , DPSFP.dup_aux_0_4_32 + , BitVec.partInstall] generalize Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = Hinit -- change the type of Hinit to be BitVec 128, assuming that's def-eq change BitVec 128 at Hinit + -- simplifying LHS + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, + extractLsb'_of_append_lo, crock3, crock4, crock5, crock6, crock7] + simp (config := {ground := true}) only + generalize h_Hinit_lo : BitVec.extractLsb' 0 64 Hinit = Hinit_lo + generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq] - simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi, - GCMV8.gcm_init_H, GCMV8.refpoly, GCMV8.pmod, GCMV8.pmod.pmodTR, - GCMV8.reduce, GCMV8.degree, GCMV8.degree.degreeTR, - GCMV8.gcm_polyval, GCMV8.gcm_polyval_red, GCMV8.irrepoly, - BitVec.reverse, BitVec.reverse.reverseTR, BitVec.partInstall - ] - simp only [gcm_polyval_mul_eq_polynomial_mult] - simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.reduceExtracLsb', BitVec.reduceHShiftLeft, - BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, - BitVec.reduceSetWidth, BitVec.reduceNot, BitVec.shiftLeft_zero_eq, BitVec.zero_eq, Nat.sub_self, BitVec.zero_and, - Nat.add_one_sub_one, BitVec.ofNat_eq_ofNat, BitVec.reduceEq, ↓reduceIte, BitVec.ushiftRight_zero_eq, BitVec.reduceAnd, - BitVec.toNat_ofNat, Nat.pow_one, Nat.reduceMod, Nat.mul_zero, Nat.add_zero, Nat.zero_mod, Nat.zero_add, Nat.sub_zero, - Nat.mul_one, Nat.zero_mul, Nat.one_mul, Nat.reduceSub, BitVec.and_self, BitVec.reduceMul, BitVec.xor_zero, - BitVec.mul_one, BitVec.zero_xor, BitVec.one_mul, BitVec.reduceXOr, BitVec.zero_or] + -- simplifying RHS + simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi, GCMV8.gcm_init_H] + simp only [gcm_polyval_asm_gcm_polyval_equiv] + simp only [gcm_polyval_asm, GCMV8.refpoly, GCMV8.pmod, GCMV8.pmod.pmodTR, + GCMV8.reduce, GCMV8.degree, GCMV8.degree.degreeTR, lo, hi, BitVec.partInstall] + simp only [Nat.reduceAdd, BitVec.shiftLeft_zero_eq, BitVec.ofNat_eq_ofNat, BitVec.reduceEq, + ↓reduceIte, Nat.sub_self, BitVec.ushiftRight_zero_eq, BitVec.reduceAnd, + BitVec.reduceExtracLsb', BitVec.toNat_ofNat, Nat.pow_one, Nat.reduceMod, Nat.mul_zero, + Nat.add_zero, BitVec.reduceHShiftRight, Nat.zero_mod, Nat.zero_add, Nat.sub_zero, Nat.mul_one, + Nat.zero_mul, Nat.one_mul, Nat.reduceSub, BitVec.and_self, BitVec.zero_and, BitVec.reduceMul, + BitVec.xor_zero, BitVec.mul_one, BitVec.zero_xor, BitVec.reduceHShiftLeft, + Nat.add_one_sub_one, BitVec.one_mul, BitVec.reduceXOr, BitVec.reduceAllOnes, + BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceNot, BitVec.shiftLeft_eq, + BitVec.zero_shiftLeft, BitVec.reduceAppend] bv_decide diff --git a/Specs/GCMV8.lean b/Specs/GCMV8.lean index a491f1ff..66514dca 100644 --- a/Specs/GCMV8.lean +++ b/Specs/GCMV8.lean @@ -160,6 +160,8 @@ def gcm_polyval_red (x : BitVec 256) : BitVec 128 := def gcm_polyval (x : BitVec 128) (y : BitVec 128) : BitVec 128 := GCMV8.gcm_polyval_red $ GCMV8.gcm_polyval_mul x y +#eval gcm_polyval 0xcdd297a9df1458771099f4b39468565c#128 0x88d320376963120dea0b3a488cb9209b#128 + /-- GCMInitV8 specification: H : [128] -- initial H input output : [12][128] -- precomputed Htable values From 4a9ca4d3d37cb045fcf47d3e1376c8da763e1fc8 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 13 Nov 2024 18:47:12 +0000 Subject: [PATCH 03/27] Add another lemma for gcm_init_H_asm --- Proofs/AES-GCM/GCMInitV8Sym.lean | 45 +++++++++++++++++++++++--------- Specs/GCMV8.lean | 2 ++ 2 files changed, 34 insertions(+), 13 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 765e7dd3..c595702e 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -19,6 +19,31 @@ abbrev Htable_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 0#5) s abbrev lo (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 0 64 x abbrev hi (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 64 64 x +-- define a function that represents gcm_init_H in the assembly +def gcm_init_H_asm (H : BitVec 128) : BitVec 128 := + let v17 := (lo H) ++ (hi H) + let v19 := 0xe1#128 + let v19 := BitVec.shiftLeft (hi v19) 57 ++ BitVec.shiftLeft (lo v19) 57 + let v3 := (lo v17) ++ (hi v17) + let v18 := BitVec.ushiftRight v19 63 + let v17_1 := BitVec.extractLsb' 32 32 v17 + let v17 := v17_1 ++ v17_1 ++ v17_1 ++ v17_1 + let v16 := (lo v19) ++ (hi v18) + let v18 := BitVec.ushiftRight v3 63 + let v17 := BitVec.sshiftRight v17 31 + let v18 := v18 &&& v16 + let v3 := v3 <<< 1 + let v18 := (lo v18) ++ (hi v18) + let v16 := v16 &&& v17 + let v3 := v3 ||| v18 + let v20 := v3 ^^^ v16 + v20 + +#eval gcm_init_H_asm 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 + +theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : + GCMV8.gcm_init_H x = gcm_init_H_asm x := by sorry + -- The following represents the assembly version of gcm_polyval def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := let v19 := 0xe1#128 @@ -176,17 +201,11 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq] -- simplifying RHS - simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi, GCMV8.gcm_init_H] - simp only [gcm_polyval_asm_gcm_polyval_equiv] - simp only [gcm_polyval_asm, GCMV8.refpoly, GCMV8.pmod, GCMV8.pmod.pmodTR, - GCMV8.reduce, GCMV8.degree, GCMV8.degree.degreeTR, lo, hi, BitVec.partInstall] - simp only [Nat.reduceAdd, BitVec.shiftLeft_zero_eq, BitVec.ofNat_eq_ofNat, BitVec.reduceEq, - ↓reduceIte, Nat.sub_self, BitVec.ushiftRight_zero_eq, BitVec.reduceAnd, - BitVec.reduceExtracLsb', BitVec.toNat_ofNat, Nat.pow_one, Nat.reduceMod, Nat.mul_zero, - Nat.add_zero, BitVec.reduceHShiftRight, Nat.zero_mod, Nat.zero_add, Nat.sub_zero, Nat.mul_one, - Nat.zero_mul, Nat.one_mul, Nat.reduceSub, BitVec.and_self, BitVec.zero_and, BitVec.reduceMul, - BitVec.xor_zero, BitVec.mul_one, BitVec.zero_xor, BitVec.reduceHShiftLeft, - Nat.add_one_sub_one, BitVec.one_mul, BitVec.reduceXOr, BitVec.reduceAllOnes, - BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceNot, BitVec.shiftLeft_eq, - BitVec.zero_shiftLeft, BitVec.reduceAppend] + simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi] + simp only [gcm_polyval_asm_gcm_polyval_equiv, gcm_init_H_asm_gcm_int_H_equiv] + simp only [gcm_polyval_asm, gcm_init_H_asm, hi, lo, BitVec.partInstall] + simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.shiftLeft_zero_eq, + BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.zero_shiftLeft, BitVec.reduceHShiftLeft, + BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.reduceAllOnes, + BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceNot] bv_decide diff --git a/Specs/GCMV8.lean b/Specs/GCMV8.lean index 66514dca..3e258594 100644 --- a/Specs/GCMV8.lean +++ b/Specs/GCMV8.lean @@ -145,6 +145,8 @@ example : reverse irrepoly = refpoly := by native_decide def gcm_init_H (H : BitVec 128) : BitVec 128 := pmod (H ++ 0b0#1) refpoly (by omega) +#eval gcm_init_H 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 + def gcm_polyval_red (x : BitVec 256) : BitVec 128 := reverse $ pmod (reverse x) irrepoly (by omega) From 3b012541d8e4f0d2a45c2ee8938fa077edf320cb Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 14 Nov 2024 00:47:30 +0000 Subject: [PATCH 04/27] Identified a set of lemmas for simplifying the goal --- Proofs/AES-GCM/GCMInitV8Sym.lean | 57 ++++++++++++++++++++++++-------- 1 file changed, 44 insertions(+), 13 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index c595702e..1b6a3943 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -8,6 +8,7 @@ import Proofs.«AES-GCM».GCMInitV8Pre import Tactics.Sym import Tactics.Aggregate import Specs.GCMV8 +import Tactics.ExtractGoal namespace GCMInitV8Program @@ -21,18 +22,16 @@ abbrev hi (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 64 64 x -- define a function that represents gcm_init_H in the assembly def gcm_init_H_asm (H : BitVec 128) : BitVec 128 := - let v17 := (lo H) ++ (hi H) - let v19 := 0xe1#128 + let v19 := 0xe1e1e1e1e1e1e1e1e1e1e1e1e1e1e1e1#128 let v19 := BitVec.shiftLeft (hi v19) 57 ++ BitVec.shiftLeft (lo v19) 57 - let v3 := (lo v17) ++ (hi v17) - let v18 := BitVec.ushiftRight v19 63 - let v17_1 := BitVec.extractLsb' 32 32 v17 - let v17 := v17_1 ++ v17_1 ++ v17_1 ++ v17_1 + let v18 := BitVec.ushiftRight (hi v19) 63 ++ BitVec.ushiftRight (lo v19) 63 + let v17_1 := BitVec.extractLsb' 32 32 (hi H) let v16 := (lo v19) ++ (hi v18) - let v18 := BitVec.ushiftRight v3 63 - let v17 := BitVec.sshiftRight v17 31 + let v18 := BitVec.ushiftRight (hi H) 63 ++ BitVec.ushiftRight (lo H) 63 + let v17 := BitVec.sshiftRight v17_1 31 ++ BitVec.sshiftRight v17_1 31 ++ + BitVec.sshiftRight v17_1 31 ++ BitVec.sshiftRight v17_1 31 let v18 := v18 &&& v16 - let v3 := v3 <<< 1 + let v3 := (hi H) <<< 1 ++ (lo H) <<< 1 let v18 := (lo v18) ++ (hi v18) let v16 := v16 &&& v17 let v3 := v3 ||| v18 @@ -46,7 +45,7 @@ theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : -- The following represents the assembly version of gcm_polyval def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := - let v19 := 0xe1#128 + let v19 := 0xe1e1e1e1e1e1e1e1e1e1e1e1e1e1e1e1#128 let v19 := BitVec.shiftLeft (hi v19) 57 ++ BitVec.shiftLeft (lo v19) 57 let v16 := ((lo x) ^^^ (hi x)) ++ ((hi x) ^^^ (lo x)) let v17 := ((lo y) ^^^ (hi y)) ++ ((hi y) ^^^ (lo y)) @@ -119,11 +118,29 @@ theorem crock6 (x : BitVec 32) : theorem crock7 (x : BitVec 128) : (BitVec.setWidth 64 x) = BitVec.extractLsb' 0 64 x := by sorry +theorem crock8 (x : BitVec 64) (y : BitVec 64) : + (BitVec.extractLsb' 0 64 (x ++ y)) ++ (BitVec.extractLsb' 64 64 (x ++ y)) + = y ++ x := by sorry + +theorem crock9 (x : BitVec 64) (y : BitVec 64) : + (x ++ y) >>> 63 = (x >>> 63) ++ (y >>> 63) := by sorry + +theorem crock10 (x : BitVec 64) (y : BitVec 64) : + (x ++ y) <<< 1 = (x <<< 1) ++ (y >>> 63) := by sorry + +theorem crock11 (x : BitVec 64) (y : BitVec 64) : + (BitVec.extractLsb' 0 64 ((x ++ y) ^^^ (y ++ x))) + = (x ^^^ y) := by sorry + +theorem crock12 (x : BitVec 128) (y : BitVec 128) : + BitVec.extractLsb' 64 128 (x ++ y) + = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 y := by sorry + set_option maxRecDepth 10000 in set_option maxHeartbeats 4000000 in set_option sat.timeout 120 in --- set_option pp.deepTerms true in --- set_option pp.maxSteps 10000 in +set_option pp.deepTerms true in +set_option pp.maxSteps 10000 in -- set_option trace.profiler true in -- set_option linter.unusedVariables false in -- set_option profiler true in @@ -195,7 +212,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) change BitVec 128 at Hinit -- simplifying LHS simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, crock3, crock4, crock5, crock6, crock7] + extractLsb'_of_append_lo, crock3, crock4, crock5, crock6, crock7, crock11, crock12] simp (config := {ground := true}) only generalize h_Hinit_lo : BitVec.extractLsb' 0 64 Hinit = Hinit_lo generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi @@ -208,4 +225,18 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.zero_shiftLeft, BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceNot] + simp only [crock8, extractLsb'_of_append_hi, extractLsb'_of_append_lo] + -- more simplification + generalize h_term1 : ((Hinit_lo <<< 1 ++ Hinit_hi <<< 1 ||| + BitVec.extractLsb' 0 64 + (Hinit_lo >>> 63 ++ Hinit_hi >>> 63 &&& + 257870231182273679343338569694386847745#128) ++ + BitVec.extractLsb' 64 64 + (Hinit_lo >>> 63 ++ Hinit_hi >>> 63 &&& + 257870231182273679343338569694386847745#128)) ^^^ + 257870231182273679343338569694386847745#128 &&& + (BitVec.extractLsb' 32 32 Hinit_lo).sshiftRight 31 ++ + (BitVec.extractLsb' 32 32 Hinit_lo).sshiftRight 31 ++ + (BitVec.extractLsb' 32 32 Hinit_lo).sshiftRight 31 ++ + (BitVec.extractLsb' 32 32 Hinit_lo).sshiftRight 31) = term1 bv_decide From 2ffd8d78e4348cf7e8dc595b749d5e1f680d17b2 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 14 Nov 2024 01:42:15 +0000 Subject: [PATCH 05/27] Need to look into RME to prove gcm_polyval_asm_gcm_polyval_equiv --- Proofs/AES-GCM/GCMInitV8Sym.lean | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 1b6a3943..24d58683 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -43,6 +43,11 @@ def gcm_init_H_asm (H : BitVec 128) : BitVec 128 := theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : GCMV8.gcm_init_H x = gcm_init_H_asm x := by sorry +-- (TODO) Should we simply replace one function by the other here? +theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : + GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by + sorry + -- The following represents the assembly version of gcm_polyval def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := let v19 := 0xe1e1e1e1e1e1e1e1e1e1e1e1e1e1e1e1#128 @@ -71,8 +76,14 @@ def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := #eval gcm_polyval_asm 0xcdd297a9df1458771099f4b39468565c#128 0x88d320376963120dea0b3a488cb9209b#128 +-- TODO: RME look into https://github.com/GaloisInc/saw-script/tree/master/rme +-- https://github.com/GaloisInc/aws-lc-verification/blob/0efc892de9a4d2660067ab02fdcef5993ff5184a/SAW/proof/AES/goal-rewrites.saw#L200-L214 +set_option maxRecDepth 10000 in +set_option maxHeartbeats 1000000 in theorem gcm_polyval_asm_gcm_polyval_equiv (x : BitVec 128) (y : BitVec 128) : - GCMV8.gcm_polyval x y = gcm_polyval_asm x y := by sorry + GCMV8.gcm_polyval x y = gcm_polyval_asm x y := by + simp only [GCMV8.gcm_polyval, gcm_polyval_asm] + sorry -- Taken from gcm_gmult_v8 theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : @@ -85,11 +96,6 @@ theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : simp only [state_simp_rules, bitvec_rules] done --- (TODO) Should we simply replace one function by the other here? -theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : - GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by - sorry - theorem extractLsb'_of_append_mid (x : BitVec 128) : BitVec.extractLsb' 64 128 (x ++ x) = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x := by From 557856a087c39554852b15586788987fda694d23 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 14 Nov 2024 17:35:18 +0000 Subject: [PATCH 06/27] Prove a couple more lemmas --- Proofs/AES-GCM/GCMInitV8Sym.lean | 55 ++++++++++++++++++-------------- 1 file changed, 31 insertions(+), 24 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 24d58683..8dfbac75 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -8,7 +8,6 @@ import Proofs.«AES-GCM».GCMInitV8Pre import Tactics.Sym import Tactics.Aggregate import Specs.GCMV8 -import Tactics.ExtractGoal namespace GCMInitV8Program @@ -40,13 +39,27 @@ def gcm_init_H_asm (H : BitVec 128) : BitVec 128 := #eval gcm_init_H_asm 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 +set_option maxRecDepth 3000 in +set_option maxHeartbeats 1000000 in +set_option sat.timeout 120 in theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : - GCMV8.gcm_init_H x = gcm_init_H_asm x := by sorry - --- (TODO) Should we simply replace one function by the other here? -theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : - GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by - sorry + GCMV8.gcm_init_H x = gcm_init_H_asm x := by + simp only [GCMV8.gcm_init_H, gcm_init_H_asm, hi, lo, + GCMV8.pmod, GCMV8.refpoly, GCMV8.pmod.pmodTR, + GCMV8.reduce, GCMV8.degree, GCMV8.degree.degreeTR] + simp only [Nat.reduceAdd, BitVec.ofNat_eq_ofNat, BitVec.reduceEq, ↓reduceIte, Nat.sub_self, + BitVec.ushiftRight_zero_eq, BitVec.reduceAnd, BitVec.reduceExtracLsb', BitVec.toNat_ofNat, + Nat.pow_one, Nat.reduceMod, Nat.mul_zero, Nat.add_zero, BitVec.reduceHShiftRight, Nat.zero_mod, + Nat.zero_add, Nat.sub_zero, Nat.mul_one, Nat.zero_mul, Nat.one_mul, Nat.reduceSub, + BitVec.and_self, BitVec.zero_and, BitVec.reduceMul, BitVec.xor_zero, BitVec.mul_one, + BitVec.zero_xor, BitVec.reduceHShiftLeft, Nat.add_one_sub_one, BitVec.one_mul, BitVec.reduceXOr, + BitVec.ushiftRight_eq, BitVec.shiftLeft_eq, BitVec.reduceAppend] + bv_decide + +-- -- (TODO) Should we simply replace one function by the other here? +-- theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : +-- GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by +-- sorry -- The following represents the assembly version of gcm_polyval def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := @@ -99,48 +112,42 @@ theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : theorem extractLsb'_of_append_mid (x : BitVec 128) : BitVec.extractLsb' 64 128 (x ++ x) = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x := by - sorry + bv_decide theorem extractLsb'_of_append_hi (x y : BitVec 64) : BitVec.extractLsb' 64 64 (x ++ y) = x := by - sorry + bv_decide theorem extractLsb'_of_append_lo (x y : BitVec 64) : BitVec.extractLsb' 0 64 (x ++ y) = y := by - sorry + bv_decide theorem crock3 (x : BitVec 32) : - (BitVec.extractLsb' 0 32 (x ++ x ++ x ++ x)) = x := by sorry + (BitVec.extractLsb' 0 32 (x ++ x ++ x ++ x)) = x := by bv_decide theorem crock4 (x : BitVec 32) : - (BitVec.extractLsb' 32 32 (x ++ x ++ x ++ x)) = x := by sorry + (BitVec.extractLsb' 32 32 (x ++ x ++ x ++ x)) = x := by bv_decide theorem crock5 (x : BitVec 32) : - (BitVec.extractLsb' 64 32 (x ++ x ++ x ++ x)) = x := by sorry + (BitVec.extractLsb' 64 32 (x ++ x ++ x ++ x)) = x := by bv_decide theorem crock6 (x : BitVec 32) : - (BitVec.extractLsb' 96 32 (x ++ x ++ x ++ x)) = x := by sorry + (BitVec.extractLsb' 96 32 (x ++ x ++ x ++ x)) = x := by bv_decide theorem crock7 (x : BitVec 128) : - (BitVec.setWidth 64 x) = BitVec.extractLsb' 0 64 x := by sorry + (BitVec.setWidth 64 x) = BitVec.extractLsb' 0 64 x := by bv_decide theorem crock8 (x : BitVec 64) (y : BitVec 64) : (BitVec.extractLsb' 0 64 (x ++ y)) ++ (BitVec.extractLsb' 64 64 (x ++ y)) - = y ++ x := by sorry - -theorem crock9 (x : BitVec 64) (y : BitVec 64) : - (x ++ y) >>> 63 = (x >>> 63) ++ (y >>> 63) := by sorry - -theorem crock10 (x : BitVec 64) (y : BitVec 64) : - (x ++ y) <<< 1 = (x <<< 1) ++ (y >>> 63) := by sorry + = y ++ x := by bv_decide theorem crock11 (x : BitVec 64) (y : BitVec 64) : (BitVec.extractLsb' 0 64 ((x ++ y) ^^^ (y ++ x))) - = (x ^^^ y) := by sorry + = (x ^^^ y) := by bv_decide theorem crock12 (x : BitVec 128) (y : BitVec 128) : BitVec.extractLsb' 64 128 (x ++ y) - = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 y := by sorry + = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 y := by bv_decide set_option maxRecDepth 10000 in set_option maxHeartbeats 4000000 in From 5b14ee289a42c5af9988e6b73228b41b074959c5 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 14 Nov 2024 18:04:36 +0000 Subject: [PATCH 07/27] Renaming and simplifying theorems --- Proofs/AES-GCM/GCMInitV8Sym.lean | 54 +++++++++++++------------------- 1 file changed, 21 insertions(+), 33 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 8dfbac75..bafcee6c 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -42,6 +42,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 theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : GCMV8.gcm_init_H x = gcm_init_H_asm x := by simp only [GCMV8.gcm_init_H, gcm_init_H_asm, hi, lo, @@ -109,9 +110,9 @@ theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : simp only [state_simp_rules, bitvec_rules] done -theorem extractLsb'_of_append_mid (x : BitVec 128) : - BitVec.extractLsb' 64 128 (x ++ x) - = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x := by +theorem extractLsb'_of_append_mid (x : BitVec 128) (y : BitVec 128): + BitVec.extractLsb' 64 128 (x ++ y) + = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 y := by bv_decide theorem extractLsb'_of_append_hi (x y : BitVec 64) : @@ -122,38 +123,34 @@ theorem extractLsb'_of_append_lo (x y : BitVec 64) : BitVec.extractLsb' 0 64 (x ++ y) = y := by bv_decide -theorem crock3 (x : BitVec 32) : +theorem extractLsb'_append4_1 (x : BitVec 32) : (BitVec.extractLsb' 0 32 (x ++ x ++ x ++ x)) = x := by bv_decide -theorem crock4 (x : BitVec 32) : +theorem extractLsb'_append4_2 (x : BitVec 32) : (BitVec.extractLsb' 32 32 (x ++ x ++ x ++ x)) = x := by bv_decide -theorem crock5 (x : BitVec 32) : +theorem extractLsb'_append4_3 (x : BitVec 32) : (BitVec.extractLsb' 64 32 (x ++ x ++ x ++ x)) = x := by bv_decide -theorem crock6 (x : BitVec 32) : +theorem extractLsb'_append4_4 (x : BitVec 32) : (BitVec.extractLsb' 96 32 (x ++ x ++ x ++ x)) = x := by bv_decide -theorem crock7 (x : BitVec 128) : +theorem setWidth_extractLsb'_equiv_64_128 (x : BitVec 128) : (BitVec.setWidth 64 x) = BitVec.extractLsb' 0 64 x := by bv_decide -theorem crock8 (x : BitVec 64) (y : BitVec 64) : +theorem append_of_extractLsb'_of_append (x : BitVec 64) (y : BitVec 64) : (BitVec.extractLsb' 0 64 (x ++ y)) ++ (BitVec.extractLsb' 64 64 (x ++ y)) = y ++ x := by bv_decide -theorem crock11 (x : BitVec 64) (y : BitVec 64) : +theorem extractLsb'_of_xor_of_append (x : BitVec 64) (y : BitVec 64) : (BitVec.extractLsb' 0 64 ((x ++ y) ^^^ (y ++ x))) = (x ^^^ y) := by bv_decide -theorem crock12 (x : BitVec 128) (y : BitVec 128) : - BitVec.extractLsb' 64 128 (x ++ y) - = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 y := by bv_decide - set_option maxRecDepth 10000 in set_option maxHeartbeats 4000000 in set_option sat.timeout 120 in -set_option pp.deepTerms true in -set_option pp.maxSteps 10000 in +-- set_option pp.deepTerms true in +-- set_option pp.maxSteps 10000 in -- set_option trace.profiler true in -- set_option linter.unusedVariables false in -- set_option profiler true in @@ -224,12 +221,14 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) -- change the type of Hinit to be BitVec 128, assuming that's def-eq change BitVec 128 at Hinit -- simplifying LHS - simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, crock3, crock4, crock5, crock6, crock7, crock11, crock12] + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, extractLsb'_of_append_lo, + extractLsb'_append4_1, extractLsb'_append4_2, extractLsb'_append4_3, extractLsb'_append4_4, + setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append] simp (config := {ground := true}) only + simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq] + -- generalize hi and lo of Hinit generalize h_Hinit_lo : BitVec.extractLsb' 0 64 Hinit = Hinit_lo generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq] -- simplifying RHS simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi] simp only [gcm_polyval_asm_gcm_polyval_equiv, gcm_init_H_asm_gcm_int_H_equiv] @@ -238,18 +237,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.zero_shiftLeft, BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceNot] - simp only [crock8, extractLsb'_of_append_hi, extractLsb'_of_append_lo] - -- more simplification - generalize h_term1 : ((Hinit_lo <<< 1 ++ Hinit_hi <<< 1 ||| - BitVec.extractLsb' 0 64 - (Hinit_lo >>> 63 ++ Hinit_hi >>> 63 &&& - 257870231182273679343338569694386847745#128) ++ - BitVec.extractLsb' 64 64 - (Hinit_lo >>> 63 ++ Hinit_hi >>> 63 &&& - 257870231182273679343338569694386847745#128)) ^^^ - 257870231182273679343338569694386847745#128 &&& - (BitVec.extractLsb' 32 32 Hinit_lo).sshiftRight 31 ++ - (BitVec.extractLsb' 32 32 Hinit_lo).sshiftRight 31 ++ - (BitVec.extractLsb' 32 32 Hinit_lo).sshiftRight 31 ++ - (BitVec.extractLsb' 32 32 Hinit_lo).sshiftRight 31) = term1 + simp only [append_of_extractLsb'_of_append, extractLsb'_of_append_hi, extractLsb'_of_append_lo] + -- TODO: a lot of the lemmas here are for reducing the arguments on DPSFP.polynomial_mul to be the same + -- It should be unnecessary after theory of uninterpreted functions are built into bv_decide bv_decide From 64483b79d493ca3e26a207e86cf80bcff2463cce Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Fri, 15 Nov 2024 01:17:52 +0000 Subject: [PATCH 08/27] Some more experiments --- Proofs/AES-GCM/GCMInitV8Sym.lean | 198 ++++++++++++++++++++++--------- 1 file changed, 143 insertions(+), 55 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index bafcee6c..e8a2acb7 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -8,6 +8,7 @@ import Proofs.«AES-GCM».GCMInitV8Pre import Tactics.Sym import Tactics.Aggregate import Specs.GCMV8 +import Tactics.ExtractGoal namespace GCMInitV8Program @@ -37,8 +38,6 @@ def gcm_init_H_asm (H : BitVec 128) : BitVec 128 := let v20 := v3 ^^^ v16 v20 -#eval gcm_init_H_asm 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 - set_option maxRecDepth 3000 in set_option maxHeartbeats 1000000 in set_option sat.timeout 120 in @@ -57,10 +56,11 @@ theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : BitVec.ushiftRight_eq, BitVec.shiftLeft_eq, BitVec.reduceAppend] bv_decide --- -- (TODO) Should we simply replace one function by the other here? --- theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : --- GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by --- sorry +set_option maxRecDepth 10000 in +set_option maxHeartbeats 1000000 in +theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : + GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by + sorry -- The following represents the assembly version of gcm_polyval def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := @@ -88,15 +88,54 @@ def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := let v23 := (hi v16) ++ (lo v16) v23 -#eval gcm_polyval_asm 0xcdd297a9df1458771099f4b39468565c#128 0x88d320376963120dea0b3a488cb9209b#128 +theorem extractLsb'_of_append_hi (x y : BitVec 64) : + BitVec.extractLsb' 64 64 (x ++ y) = x := by + bv_decide + +theorem extractLsb'_of_append_lo (x y : BitVec 64) : + BitVec.extractLsb' 0 64 (x ++ y) = y := by + bv_decide --- TODO: RME look into https://github.com/GaloisInc/saw-script/tree/master/rme +-- https://kib.kiev.ua/x86docs/Intel/WhitePapers/323640-001.pdf +def karatsuba_multiplication (x : BitVec 128) (y : BitVec 128) : BitVec 256 := + let A1 := hi x + let A0 := lo x + let B1 := hi y + let B0 := lo y + let A1B1 := DPSFP.polynomial_mult A1 B1 + let C1 := hi A1B1 + let C0 := lo A1B1 + let A0B0 := DPSFP.polynomial_mult A0 B0 + let D1 := hi A0B0 + let D0 := lo A0B0 + let A1A0B1B0 := DPSFP.polynomial_mult (A1 ^^^ A0) (B1 ^^^ B0) + let E1 := hi A1A0B1B0 + let E0 := lo A1A0B1B0 + C1 ++ (C0 ^^^ C1 ^^^ D1 ^^^ E1) ++ (D1 ^^^ C0 ^^^ D0 ^^^ E0) ++ D0 + +theorem karatsuba_multiplication_equiv (x : BitVec 128) (y : BitVec 128) : + DPSFP.polynomial_mult x y = karatsuba_multiplication x y := by sorry + +-- TODO: look into https://github.com/GaloisInc/saw-script/tree/master/rme for RME -- https://github.com/GaloisInc/aws-lc-verification/blob/0efc892de9a4d2660067ab02fdcef5993ff5184a/SAW/proof/AES/goal-rewrites.saw#L200-L214 set_option maxRecDepth 10000 in -set_option maxHeartbeats 1000000 in +set_option maxHeartbeats 5000000 in theorem gcm_polyval_asm_gcm_polyval_equiv (x : BitVec 128) (y : BitVec 128) : GCMV8.gcm_polyval x y = gcm_polyval_asm x y := by - simp only [GCMV8.gcm_polyval, gcm_polyval_asm] + simp only [GCMV8.gcm_polyval, gcm_polyval_asm, hi, lo, + extractLsb'_of_append_hi, extractLsb'_of_append_lo, BitVec.partInstall, + gcm_polyval_mul_eq_polynomial_mult] + simp only [Nat.reduceAdd, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, + BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, BitVec.reduceExtracLsb', + BitVec.shiftLeft_eq, BitVec.shiftLeft_zero_eq] + simp only [karatsuba_multiplication_equiv, karatsuba_multiplication, hi, lo] + generalize h_A1 : BitVec.extractLsb' 64 64 x = A1 + generalize h_A0 : BitVec.extractLsb' 0 64 x = A0 + generalize h_B1 : BitVec.extractLsb' 64 64 y = B1 + generalize h_B0 : BitVec.extractLsb' 0 64 y = B0 + generalize h_A1A0B1B0 : DPSFP.polynomial_mult (A1 ^^^ A0) (B1 ^^^ B0) = A1A0B1B0 + generalize h_A1B1 : DPSFP.polynomial_mult A1 B1 = A1B1 + generalize h_A0B0 : DPSFP.polynomial_mult A0 B0 = A0B0 sorry -- Taken from gcm_gmult_v8 @@ -115,14 +154,6 @@ theorem extractLsb'_of_append_mid (x : BitVec 128) (y : BitVec 128): = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 y := by bv_decide -theorem extractLsb'_of_append_hi (x y : BitVec 64) : - BitVec.extractLsb' 64 64 (x ++ y) = x := by - bv_decide - -theorem extractLsb'_of_append_lo (x y : BitVec 64) : - BitVec.extractLsb' 0 64 (x ++ y) = y := by - bv_decide - theorem extractLsb'_append4_1 (x : BitVec 32) : (BitVec.extractLsb' 0 32 (x ++ x ++ x ++ x)) = x := by bv_decide @@ -146,11 +177,53 @@ theorem extractLsb'_of_xor_of_append (x : BitVec 64) (y : BitVec 64) : (BitVec.extractLsb' 0 64 ((x ++ y) ^^^ (y ++ x))) = (x ^^^ y) := by bv_decide + +syntax "gcm_init_v8_tac" : tactic + +macro_rules + | `(tactic| gcm_init_v8_tac) => + `(tactic| + (simp only + [shift_left_common_aux_64_2 + , shift_right_common_aux_64_2_tff + , shift_right_common_aux_32_4_fff + , DPSFP.AdvSIMDExpandImm + , DPSFP.dup_aux_0_4_32 + , BitVec.partInstall]; + generalize Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = Hinit; + -- change the type of Hinit to be BitVec 128, assuming that's def-eq + change BitVec 128 at Hinit; + -- simplifying LHS + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, + extractLsb'_of_append_lo, extractLsb'_append4_1, extractLsb'_append4_2, + extractLsb'_append4_3, extractLsb'_append4_4, + setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append]; + simp (config := {ground := true}) only; + simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq]; + -- generalize hi and lo of Hinit + generalize h_Hinit_lo : BitVec.extractLsb' 0 64 Hinit = Hinit_lo; + generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi; + -- simplifying RHS + simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi]; + simp only [gcm_polyval_asm_gcm_polyval_equiv, gcm_init_H_asm_gcm_int_H_equiv]; + simp only [gcm_polyval_asm, gcm_init_H_asm, hi, lo, BitVec.partInstall]; + simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.shiftLeft_zero_eq, + BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.zero_shiftLeft, + BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, + BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, + BitVec.reduceNot]; + simp only [append_of_extractLsb'_of_append, extractLsb'_of_append_hi, + extractLsb'_of_append_lo]; + -- TODO: a lot of the lemmas here are for reducing the arguments on + -- DPSFP.polynomial_mul to be the same. It should be unnecessary after + -- theory of uninterpreted functions are built into bv_decide + (try bv_decide))) + set_option maxRecDepth 10000 in set_option maxHeartbeats 4000000 in set_option sat.timeout 120 in --- set_option pp.deepTerms true in --- set_option pp.maxSteps 10000 in +set_option pp.deepTerms true in +set_option pp.maxSteps 1000000 in -- set_option trace.profiler true in -- set_option linter.unusedVariables false in -- set_option profiler true in @@ -180,9 +253,15 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) -- read_sfp 128 20#5 sf = -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 0 + -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + -- read_sfp 128 21#5 sf = + -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 1 + -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + -- read_sfp 128 22#5 sf = + -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 2 ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) - read_sfp 128 21#5 sf = - (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 1 + read_sfp 128 23#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 3 -- -- TODO: Commenting out memory related conjuncts since it seems -- to make symbolic execution stuck @@ -208,36 +287,45 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) -- unable to be reflected sym_n 152 simp only [Htable_addr, state_value] -- TODO: state_value is needed, why - apply And.intro - · bv_decide - · simp only - [shift_left_common_aux_64_2 - , shift_right_common_aux_64_2_tff - , shift_right_common_aux_32_4_fff - , DPSFP.AdvSIMDExpandImm - , DPSFP.dup_aux_0_4_32 - , BitVec.partInstall] - generalize Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = Hinit - -- change the type of Hinit to be BitVec 128, assuming that's def-eq - change BitVec 128 at Hinit - -- simplifying LHS - simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, extractLsb'_of_append_lo, - extractLsb'_append4_1, extractLsb'_append4_2, extractLsb'_append4_3, extractLsb'_append4_4, - setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append] - simp (config := {ground := true}) only - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq] - -- generalize hi and lo of Hinit - generalize h_Hinit_lo : BitVec.extractLsb' 0 64 Hinit = Hinit_lo - generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi - -- simplifying RHS - simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi] - simp only [gcm_polyval_asm_gcm_polyval_equiv, gcm_init_H_asm_gcm_int_H_equiv] - simp only [gcm_polyval_asm, gcm_init_H_asm, hi, lo, BitVec.partInstall] - simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.shiftLeft_zero_eq, - BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.zero_shiftLeft, BitVec.reduceHShiftLeft, - BitVec.reduceAppend, BitVec.reduceHShiftRight, BitVec.reduceAllOnes, - BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceNot] - simp only [append_of_extractLsb'_of_append, extractLsb'_of_append_hi, extractLsb'_of_append_lo] - -- TODO: a lot of the lemmas here are for reducing the arguments on DPSFP.polynomial_mul to be the same - -- It should be unnecessary after theory of uninterpreted functions are built into bv_decide - bv_decide + repeat' apply And.intro + · first | bv_decide | gcm_init_v8_tac + · first | bv_decide | + (simp only + [shift_left_common_aux_64_2 + , shift_right_common_aux_64_2_tff + , shift_right_common_aux_32_4_fff + , DPSFP.AdvSIMDExpandImm + , DPSFP.dup_aux_0_4_32 + , BitVec.partInstall]; + generalize Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = Hinit; + -- change the type of Hinit to be BitVec 128, assuming that's def-eq + change BitVec 128 at Hinit; + -- simplifying LHS + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, + extractLsb'_of_append_lo, extractLsb'_append4_1, extractLsb'_append4_2, + extractLsb'_append4_3, extractLsb'_append4_4, + setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append]; + simp (config := {ground := true}) only; + simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq]; + -- generalize hi and lo of Hinit + generalize h_Hinit_lo : BitVec.extractLsb' 0 64 Hinit = Hinit_lo; + generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi; + -- simplifying RHS + simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi]; + simp only [gcm_polyval_asm_gcm_polyval_equiv, gcm_init_H_asm_gcm_int_H_equiv]; + simp only [gcm_polyval_asm, gcm_init_H_asm, hi, lo, BitVec.partInstall]; + simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.shiftLeft_zero_eq, + BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.zero_shiftLeft, + BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, + BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, + BitVec.reduceNot]; + simp only [append_of_extractLsb'_of_append, extractLsb'_of_append_hi, + extractLsb'_of_append_lo]; + -- TODO: a lot of the lemmas here are for reducing the arguments on + -- DPSFP.polynomial_mul to be the same. It should be unnecessary after + -- theory of uninterpreted functions are built into bv_decide + -- extract_goal + -- TODO: later terms in Htable gets larger because it depends on previous term + -- Need to simplify the term along the way, maybe do some simulation, simplify, + -- then do some more, then simplify more? + bv_decide) From 8950f38fc6d823fd3d36b7899a38e9db87000275 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Mon, 18 Nov 2024 23:40:37 +0000 Subject: [PATCH 09/27] Incremental proof for gcm_init_v8 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 204 ++++++++++++++++++++++--------- 1 file changed, 146 insertions(+), 58 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index e8a2acb7..eb1de083 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -222,8 +222,8 @@ macro_rules set_option maxRecDepth 10000 in set_option maxHeartbeats 4000000 in set_option sat.timeout 120 in -set_option pp.deepTerms true in -set_option pp.maxSteps 1000000 in +-- set_option pp.deepTerms true in +-- set_option pp.maxSteps 1000000 in -- set_option trace.profiler true in -- set_option linter.unusedVariables false in -- set_option profiler true in @@ -232,7 +232,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) (h_s0_err : read_err s0 = .None) (h_s0_pc : read_pc s0 = gcm_init_v8_program.min) (h_s0_sp_aligned : CheckSPAlignment s0) - (h_run : sf = run gcm_init_v8_program.length s0) + -- (h_run : sf = run gcm_init_v8_program.length s0) + (h_run : sf = run 78 s0) (h_mem : Memory.Region.pairwiseSeparate [ ⟨(H_addr s0), 128⟩, ⟨(Htable_addr s0), 2048⟩ ]) @@ -244,24 +245,30 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) -- SP is still aligned ∧ CheckSPAlignment sf -- PC is updated - ∧ read_pc sf = read_gpr 64 30#5 s0 + -- ∧ read_pc sf = read_gpr 64 30#5 s0 -- Htable_addr ptr is moved to the start of the 10th element - ∧ Htable_addr sf = Htable_addr s0 + (9 * 16#64) + -- ∧ Htable_addr sf = Htable_addr s0 + (9 * 16#64) -- H_addr ptr stays the same ∧ H_addr sf = H_addr s0 -- v20 - v31 stores results of Htable - -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) - -- read_sfp 128 20#5 sf = - -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 0 - -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) - -- read_sfp 128 21#5 sf = - -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 1 - -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) - -- read_sfp 128 22#5 sf = - -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 2 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 20#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 0 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 21#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 1 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 22#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 2 ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) read_sfp 128 23#5 sf = (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 3 + -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + -- read_sfp 128 24#5 sf = + -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 4 + -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + -- read_sfp 128 25#5 sf = + -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 5 -- -- TODO: Commenting out memory related conjuncts since it seems -- to make symbolic execution stuck @@ -285,47 +292,128 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp (config := {ground := true}) only at h_s0_pc -- ^^ Still needed, because `gcm_init_v8_program.min` is somehow -- unable to be reflected - sym_n 152 - simp only [Htable_addr, state_value] -- TODO: state_value is needed, why - repeat' apply And.intro - · first | bv_decide | gcm_init_v8_tac - · first | bv_decide | - (simp only - [shift_left_common_aux_64_2 - , shift_right_common_aux_64_2_tff - , shift_right_common_aux_32_4_fff - , DPSFP.AdvSIMDExpandImm - , DPSFP.dup_aux_0_4_32 - , BitVec.partInstall]; - generalize Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = Hinit; - -- change the type of Hinit to be BitVec 128, assuming that's def-eq - change BitVec 128 at Hinit; - -- simplifying LHS - simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, extractLsb'_append4_1, extractLsb'_append4_2, - extractLsb'_append4_3, extractLsb'_append4_4, - setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append]; - simp (config := {ground := true}) only; - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq]; - -- generalize hi and lo of Hinit - generalize h_Hinit_lo : BitVec.extractLsb' 0 64 Hinit = Hinit_lo; - generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi; - -- simplifying RHS - simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi]; - simp only [gcm_polyval_asm_gcm_polyval_equiv, gcm_init_H_asm_gcm_int_H_equiv]; - simp only [gcm_polyval_asm, gcm_init_H_asm, hi, lo, BitVec.partInstall]; - simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.shiftLeft_zero_eq, - BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.zero_shiftLeft, - BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, - BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, - BitVec.reduceNot]; - simp only [append_of_extractLsb'_of_append, extractLsb'_of_append_hi, - extractLsb'_of_append_lo]; - -- TODO: a lot of the lemmas here are for reducing the arguments on - -- DPSFP.polynomial_mul to be the same. It should be unnecessary after - -- theory of uninterpreted functions are built into bv_decide - -- extract_goal - -- TODO: later terms in Htable gets larger because it depends on previous term - -- Need to simplify the term along the way, maybe do some simulation, simplify, - -- then do some more, then simplify more? - bv_decide) + -- Step 1: simulate up to the instruction that saves the value for H0_rev + -- Verify that v20 stores H0_rev + sym_n 17 + -- simp only [Htable_addr, state_value] -- TODO: state_value is needed, why + generalize x1_h: (Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem) = x1 at * + change BitVec 128 at x1 + -- value of q19 + have h_e1 : (r (StateField.SFP 19#5) s17) = + let tmp := 0xe1e1e1e1e1e1e1e1e1e1e1e1e1e1e1e1#128 + BitVec.shiftLeft (hi tmp) 57 ++ BitVec.shiftLeft (lo tmp) 57 := by + have q0 : (r (StateField.SFP 19#5) s17) = (r (StateField.SFP 19#5) s3) := by sym_aggregate + simp only [q0, h_s3_q19, h_s3_non_effects, h_s2_q19, shift_left_common_aux_64_2] + simp only [Nat.reduceAdd, BitVec.reduceExtracLsb', BitVec.reduceHShiftLeft, + BitVec.reduceAppend, BitVec.shiftLeft_eq, hi, lo] + -- value of H0 + have h0 : r (StateField.SFP 20#5) s17 = + let x_rev := (lo x1) ++ (hi x1) + lo (gcm_init_H_asm x_rev) ++ hi (gcm_init_H_asm x_rev) := by + sym_aggregate + have q0: (read_mem_bytes 16 (r (StateField.GPR 1#5) s0) s0) = + (Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem) := by rfl + simp only [q0, x1_h] + simp only [shift_left_common_aux_64_2, shift_right_common_aux_64_2_tff, + shift_right_common_aux_32_4_fff, DPSFP.AdvSIMDExpandImm, + DPSFP.dup_aux_0_4_32, BitVec.partInstall] + -- simplifying LHS + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, + extractLsb'_of_append_lo, extractLsb'_append4_1, extractLsb'_append4_2, + extractLsb'_append4_3, extractLsb'_append4_4, + setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append] + -- simplifying RHS + simp only [lo, hi, gcm_init_H_asm, BitVec.partInstall, + extractLsb'_of_append_hi, extractLsb'_of_append_lo] + simp (config := {ground := true}) only + -- Step 2: simulate up to H1 and H2_rev and verify + sym_n 20 + -- value of H1 + have h1 : r (StateField.SFP 21#5) s37 = + 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 H0) ^^^ (lo H0)) := by + simp only [h_s37_q21, h_s37_non_effects, ] + sorry + have h2 : r (StateField.SFP 22#5) s37 = + let x_rev := (lo x1) ++ (hi x1) + let H0 := gcm_init_H_asm x_rev + let H2 := gcm_polyval_asm H0 H0 + (lo H2) ++ (hi H2) := by sorry + -- Step 3: simulate up to H3_rev, H4 and H5_rev and verify + sym_n 40 + have h3 : r (StateField.SFP 23#5) s77 = + let x_rev := (lo x1) ++ (hi x1) + let H0 := gcm_init_H_asm x_rev + let H2 := gcm_polyval_asm H0 H0 + let H3 := GCMV8.gcm_polyval H0 H2 + (lo H3) ++ (hi H3) := by + -- TODO: I want to sym_aggregate, but only aggregate to last step, + -- instead of all the way to the top + -- sym_aggregate + simp (config := {decide := true}) only [ + h_s77_non_effects, h_s76_non_effects, h_s75_non_effects, + h_s74_non_effects, h_s73_non_effects, h_s72_non_effects, + h_s71_non_effects, h_s70_q23, h_s70_non_effects, + h_s69_non_effects, h_s68_q16, h_s68_non_effects, + h_s67_non_effects, h_s66_q18, h_s66_non_effects, + h_s65_non_effects, h_s64_q0, h_s64_non_effects, + h_s63_non_effects, h_s62_q18, h_s62_non_effects, + h_s61_non_effects, h_s60_q0, h_s60_non_effects, + h_s59_non_effects, h_s58_q1, h_s58_non_effects, + h_s57_non_effects, h_s56_q2, h_s56_non_effects, + h_s55_non_effects, h_s54_non_effects, + h_s53_q18, h_s53_non_effects, + h_s52_q1, h_s52_non_effects, + h_s51_non_effects, h_s50_non_effects, + h_s49_q1, h_s49_non_effects, + h_s48_q18, h_s48_non_effects, + h_s47_non_effects, h_s46_q16, h_s46_non_effects, + h_s45_non_effects, h_s44_q1, h_s44_non_effects, + h_s43_non_effects, h_s42_q2, h_s42_non_effects, + h_s41_non_effects, h_s40_q0] + have q0 : r (StateField.SFP 20#5) s39 = r (StateField.SFP 20#5) s17 := by sym_aggregate + have q1 : r (StateField.SFP 20#5) s40 = r (StateField.SFP 20#5) s17 := by sym_aggregate + have q2 : r (StateField.SFP 22#5) s39 = r (StateField.SFP 22#5) s37 := by sym_aggregate + have q3 : r (StateField.SFP 22#5) s40 = r (StateField.SFP 22#5) s37 := by sym_aggregate + have q4_1 : r (StateField.SFP 16#5) s40 = r (StateField.SFP 16#5) s20 := by sym_aggregate + have q4 : BitVec.extractLsb' 0 64 (r (StateField.SFP 16#5) s40) = + let x_rev := (lo x1) ++ (hi x1) + let H0 := gcm_init_H_asm x_rev + (hi H0) ^^^ (lo H0) := by + simp (config := {decide := true}) only [ q4_1, + h_s20_q16, h_s20_non_effects, h_s19_non_effects, + h_s18_q16, h_s18_non_effects, h0 ] + simp only [hi, lo] + bv_decide + have q5 : BitVec.extractLsb' 0 64 (r (StateField.SFP 17#5) s40) = + 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) := by + sorry + have q6 : (r (StateField.SFP 19#5) s40) = (r (StateField.SFP 19#5) s17) := by sym_aggregate + simp only [q0, q1, h0, q2, q3, h2, q4, q5, q6, h_e1] + -- 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] + generalize (gcm_init_H_asm (BitVec.extractLsb' 0 64 x1 ++ BitVec.extractLsb' 64 64 x1)) = H0 + generalize (gcm_polyval_asm H0 H0) = H2 + simp (config := {ground := true}) only + -- simplifying RHS + 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] + -- simplify all + simp only [Nat.reduceAdd, BitVec.shiftLeft_zero_eq, BitVec.reduceAllOnes, + BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, + BitVec.reduceExtracLsb', BitVec.shiftLeft_eq] + sym_n 1 + sorry From 9f74fc158269759e86a9c6c6be432a19005f5e01 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Tue, 19 Nov 2024 00:02:30 +0000 Subject: [PATCH 10/27] Bug in h_s36_non_effects --- Proofs/AES-GCM/GCMInitV8Sym.lean | 36 ++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 11 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index eb1de083..8d9949e8 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -334,7 +334,23 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) let H0 := gcm_init_H_asm x_rev let H2 := gcm_polyval_asm H0 H0 ((hi H2) ^^^ (lo H2)) ++ ((hi H0) ^^^ (lo H0)) := by - simp only [h_s37_q21, h_s37_non_effects, ] + -- FIXME: there is a weird bug that h_s36_non_effects wouldn't apply + simp only [ + h_s37_q21, h_s37_non_effects, + h_s36_non_effects + -- h_s35_q22, h_s35_non_effects, + -- h_s34_q17, h_s34_non_effects, + -- h_s33_q18, h_s33_non_effects, + -- h_s32_q0, h_s32_non_effects, + -- h_s31_q18, h_s31_non_effects, h_s30_q0, h_s30_non_effects, + -- h_s29_q1, h_s29_non_effects, h_s28_q2, h_s28_non_effects, + -- h_s27_q18, h_s27_non_effects, h_s26_q1, h_s26_non_effects, + -- h_s25_q1, h_s25_non_effects, h_s24_q18, h_s24_non_effects, + -- h_s23_q17, h_s23_non_effects, h_s22_q1, h_s22_non_effects, + -- h_s21_q2, h_s21_non_effects, h_s20_q16, h_s20_non_effects, + -- h_s19_q0, h_s19_non_effects, h_s18_q16, h_s18_non_effects, + ] + sorry have h2 : r (StateField.SFP 22#5) s37 = let x_rev := (lo x1) ++ (hi x1) @@ -372,29 +388,27 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s47_non_effects, h_s46_q16, h_s46_non_effects, h_s45_non_effects, h_s44_q1, h_s44_non_effects, h_s43_non_effects, h_s42_q2, h_s42_non_effects, - h_s41_non_effects, h_s40_q0] + h_s41_non_effects, h_s40_q0, h_s40_non_effects] have q0 : r (StateField.SFP 20#5) s39 = r (StateField.SFP 20#5) s17 := by sym_aggregate - have q1 : r (StateField.SFP 20#5) s40 = r (StateField.SFP 20#5) s17 := by sym_aggregate - have q2 : r (StateField.SFP 22#5) s39 = r (StateField.SFP 22#5) s37 := by sym_aggregate - have q3 : r (StateField.SFP 22#5) s40 = r (StateField.SFP 22#5) s37 := by sym_aggregate - have q4_1 : r (StateField.SFP 16#5) s40 = r (StateField.SFP 16#5) s20 := by sym_aggregate - have q4 : BitVec.extractLsb' 0 64 (r (StateField.SFP 16#5) s40) = + have q1 : r (StateField.SFP 22#5) s39 = r (StateField.SFP 22#5) s37 := by sym_aggregate + have q2_1 : r (StateField.SFP 16#5) s39 = r (StateField.SFP 16#5) s20 := by sym_aggregate + have q2 : BitVec.extractLsb' 0 64 (r (StateField.SFP 16#5) s39) = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev (hi H0) ^^^ (lo H0) := by - simp (config := {decide := true}) only [ q4_1, + simp (config := {decide := true}) only [ q2_1, h_s20_q16, h_s20_non_effects, h_s19_non_effects, h_s18_q16, h_s18_non_effects, h0 ] simp only [hi, lo] bv_decide - have q5 : BitVec.extractLsb' 0 64 (r (StateField.SFP 17#5) s40) = + have q3 : BitVec.extractLsb' 0 64 (r (StateField.SFP 17#5) s39) = 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) := by sorry - have q6 : (r (StateField.SFP 19#5) s40) = (r (StateField.SFP 19#5) s17) := by sym_aggregate - simp only [q0, q1, h0, q2, q3, h2, q4, q5, q6, h_e1] + have q4 : (r (StateField.SFP 19#5) s39) = (r (StateField.SFP 19#5) s17) := by sym_aggregate + simp only [q0, h0, q1, h2, q2, q3, q4, h_e1] -- simplifying LHS simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, gcm_polyval_asm_gcm_polyval_equiv, From 6b0c2208755ae7a23551a50c00137eb610cca889 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Tue, 19 Nov 2024 01:23:28 +0000 Subject: [PATCH 11/27] Proving sorry'ed lemmas --- Proofs/AES-GCM/GCMInitV8Sym.lean | 186 ++++++++++++++++++------------- 1 file changed, 110 insertions(+), 76 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 8d9949e8..92caecc2 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -85,7 +85,7 @@ def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := let v0 := DPSFP.polynomial_mult (lo v0) (lo v19) let v18 := v18 ^^^ v2 let v16 := v0 ^^^ v18 - let v23 := (hi v16) ++ (lo v16) + let v23 := v16 v23 theorem extractLsb'_of_append_hi (x y : BitVec 64) : @@ -177,47 +177,22 @@ theorem extractLsb'_of_xor_of_append (x : BitVec 64) (y : BitVec 64) : (BitVec.extractLsb' 0 64 ((x ++ y) ^^^ (y ++ x))) = (x ^^^ y) := by bv_decide +theorem extractLsb'_of_xor_of_append_hi (x : BitVec 64) (y : BitVec 64) : + (BitVec.extractLsb' 64 64 ((x ++ y) ^^^ (y ++ x))) + = (x ^^^ y) := by bv_decide + +theorem extractLsb'_of_xor_of_extractLsb' (x : BitVec 128): + (BitVec.extractLsb' 0 64 + (x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x))) + = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by + bv_decide syntax "gcm_init_v8_tac" : tactic macro_rules | `(tactic| gcm_init_v8_tac) => `(tactic| - (simp only - [shift_left_common_aux_64_2 - , shift_right_common_aux_64_2_tff - , shift_right_common_aux_32_4_fff - , DPSFP.AdvSIMDExpandImm - , DPSFP.dup_aux_0_4_32 - , BitVec.partInstall]; - generalize Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = Hinit; - -- change the type of Hinit to be BitVec 128, assuming that's def-eq - change BitVec 128 at Hinit; - -- simplifying LHS - simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, extractLsb'_append4_1, extractLsb'_append4_2, - extractLsb'_append4_3, extractLsb'_append4_4, - setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append]; - simp (config := {ground := true}) only; - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq]; - -- generalize hi and lo of Hinit - generalize h_Hinit_lo : BitVec.extractLsb' 0 64 Hinit = Hinit_lo; - generalize h_Hinit_hi : BitVec.extractLsb' 64 64 Hinit = Hinit_hi; - -- simplifying RHS - simp only [GCMV8.GCMInitV8, GCMV8.lo, List.get!, GCMV8.hi]; - simp only [gcm_polyval_asm_gcm_polyval_equiv, gcm_init_H_asm_gcm_int_H_equiv]; - simp only [gcm_polyval_asm, gcm_init_H_asm, hi, lo, BitVec.partInstall]; - simp only [Nat.reduceAdd, BitVec.ushiftRight_eq, BitVec.shiftLeft_zero_eq, - BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.zero_shiftLeft, - BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.reduceHShiftRight, - BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, - BitVec.reduceNot]; - simp only [append_of_extractLsb'_of_append, extractLsb'_of_append_hi, - extractLsb'_of_append_lo]; - -- TODO: a lot of the lemmas here are for reducing the arguments on - -- DPSFP.polynomial_mul to be the same. It should be unnecessary after - -- theory of uninterpreted functions are built into bv_decide - (try bv_decide))) + (sorry)) set_option maxRecDepth 10000 in set_option maxHeartbeats 4000000 in @@ -307,7 +282,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [Nat.reduceAdd, BitVec.reduceExtracLsb', BitVec.reduceHShiftLeft, BitVec.reduceAppend, BitVec.shiftLeft_eq, hi, lo] -- value of H0 - have h0 : r (StateField.SFP 20#5) s17 = + have h_H0 : r (StateField.SFP 20#5) s17 = let x_rev := (lo x1) ++ (hi x1) lo (gcm_init_H_asm x_rev) ++ hi (gcm_init_H_asm x_rev) := by sym_aggregate @@ -328,38 +303,104 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp (config := {ground := true}) only -- Step 2: simulate up to H1 and H2_rev and verify sym_n 20 + have h_v16_s20_hi : BitVec.extractLsb' 64 64 (r (StateField.SFP 16#5) s20) = + let x_rev := (lo x1) ++ (hi x1) + hi (gcm_init_H_asm x_rev) ^^^ lo (gcm_init_H_asm x_rev) := by + simp (config := {decide := true}) only [ + h_s20_q16, h_s20_non_effects, + h_s19_non_effects, h_s18_q16, h_s18_non_effects, + extractLsb'_of_append_mid] + simp only [h_H0] + bv_decide + have h_v16_s20_lo : BitVec.extractLsb' 0 64 (r (StateField.SFP 16#5) s20) = + let x_rev := (lo x1) ++ (hi x1) + lo (gcm_init_H_asm x_rev) ^^^ hi (gcm_init_H_asm x_rev):= by + simp (config := {decide := true}) only [ + h_s20_q16, h_s20_non_effects, + h_s19_non_effects, h_s18_q16, h_s18_non_effects, + extractLsb'_of_append_mid] + simp only [h_H0] + bv_decide + have h_v17_s34 : (r (StateField.SFP 17#5) s34) = + let x_rev := (lo x1) ++ (hi x1) + let H0 := gcm_init_H_asm x_rev + gcm_polyval_asm H0 H0 := by + simp (config := {decide := true}) only [ + extractLsb'_of_append_mid, + h_s34_q17, h_s34_non_effects, + h_s33_q18, h_s33_non_effects, + h_s32_q0, h_s32_non_effects, + h_s31_q18, h_s31_non_effects, + h_s30_q0, h_s30_non_effects, + h_s29_q1, h_s29_non_effects, + h_s28_q2, h_s28_non_effects, + h_s27_q18, h_s27_non_effects, + h_s26_q1, h_s26_non_effects, + h_s25_q1, h_s25_non_effects, + h_s24_q18, h_s24_non_effects, + h_s23_q17, h_s23_non_effects, + h_s22_q1, h_s22_non_effects, + h_s21_q2, h_s21_non_effects, + h_s20_q16, h_s20_non_effects, + h_s19_q0, h_s19_non_effects, + h_s18_q16, h_s18_non_effects, + ] + simp only [h_H0, h_e1] + generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 + -- simplify LHS + simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, + BitVec.partInstall, lo, hi] + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, + extractLsb'_of_xor_of_append, extractLsb'_of_xor_of_append_hi] + simp only [Nat.reduceAdd, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, + BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, + BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.shiftLeft_zero_eq] + -- simplify RHS + simp only [gcm_polyval_asm, BitVec.partInstall, hi, lo] + simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, + extractLsb'_of_xor_of_append] + simp only [Nat.reduceAdd, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, + BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, + BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.shiftLeft_zero_eq] + have h_v17_s36 : BitVec.extractLsb' 0 64 (r (StateField.SFP 17#5) s36) = + 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) := by + simp (config := {decide := true}) only [ + extractLsb'_of_append_mid, + h_s36_q17, h_s36_non_effects, + h_s35_q22, h_s35_non_effects, + extractLsb'_of_xor_of_extractLsb', ] + simp only [h_v17_s34, h_e1] -- value of H1 - have h1 : r (StateField.SFP 21#5) s37 = + have h_H1 : r (StateField.SFP 21#5) s37 = 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 H0) ^^^ (lo H0)) := by - -- FIXME: there is a weird bug that h_s36_non_effects wouldn't apply - simp only [ - h_s37_q21, h_s37_non_effects, - h_s36_non_effects - -- h_s35_q22, h_s35_non_effects, - -- h_s34_q17, h_s34_non_effects, - -- h_s33_q18, h_s33_non_effects, - -- h_s32_q0, h_s32_non_effects, - -- h_s31_q18, h_s31_non_effects, h_s30_q0, h_s30_non_effects, - -- h_s29_q1, h_s29_non_effects, h_s28_q2, h_s28_non_effects, - -- h_s27_q18, h_s27_non_effects, h_s26_q1, h_s26_non_effects, - -- h_s25_q1, h_s25_non_effects, h_s24_q18, h_s24_non_effects, - -- h_s23_q17, h_s23_non_effects, h_s22_q1, h_s22_non_effects, - -- h_s21_q2, h_s21_non_effects, h_s20_q16, h_s20_non_effects, - -- h_s19_q0, h_s19_non_effects, h_s18_q16, h_s18_non_effects, - ] - - sorry - have h2 : r (StateField.SFP 22#5) s37 = + simp (config := {decide := true}) only [ + h_s37_q21, + h_s37_non_effects, + extractLsb'_of_append_mid, ] + have q: r (StateField.SFP 16#5) s36 = r (StateField.SFP 16#5) s20 := by sym_aggregate + simp only [q, h_v17_s36, h_v16_s20_hi] + have h_H2 : r (StateField.SFP 22#5) s37 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev let H2 := gcm_polyval_asm H0 H0 - (lo H2) ++ (hi H2) := by sorry + (lo H2) ++ (hi H2) := by + simp (config := {decide := true}) only [ + h_s37_non_effects, h_s36_non_effects, + h_s35_q22, h_s35_non_effects, + extractLsb'_of_append_mid, ] + simp only [h_v17_s34, hi, lo, + extractLsb'_of_append_hi, extractLsb'_of_append_lo] -- Step 3: simulate up to H3_rev, H4 and H5_rev and verify sym_n 40 - have h3 : r (StateField.SFP 23#5) s77 = + have h_H3 : r (StateField.SFP 23#5) s77 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev let H2 := gcm_polyval_asm H0 H0 @@ -388,27 +429,21 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s47_non_effects, h_s46_q16, h_s46_non_effects, h_s45_non_effects, h_s44_q1, h_s44_non_effects, h_s43_non_effects, h_s42_q2, h_s42_non_effects, - h_s41_non_effects, h_s40_q0, h_s40_non_effects] - have q0 : r (StateField.SFP 20#5) s39 = r (StateField.SFP 20#5) s17 := by sym_aggregate - have q1 : r (StateField.SFP 22#5) s39 = r (StateField.SFP 22#5) s37 := by sym_aggregate - have q2_1 : r (StateField.SFP 16#5) s39 = r (StateField.SFP 16#5) s20 := by sym_aggregate - have q2 : BitVec.extractLsb' 0 64 (r (StateField.SFP 16#5) s39) = + h_s41_non_effects, h_s40_q0, h_s40_non_effects, + h_s39_non_effects, h_s38_non_effects, h_s37_non_effects] + have q0 : r (StateField.SFP 20#5) s36 = r (StateField.SFP 20#5) s17 := by sym_aggregate + have q1 : r (StateField.SFP 22#5) s36 = r (StateField.SFP 22#5) s37 := by sym_aggregate + have q2_1 : r (StateField.SFP 16#5) s36 = r (StateField.SFP 16#5) s20 := by sym_aggregate + have q2 : BitVec.extractLsb' 0 64 (r (StateField.SFP 16#5) s36) = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev (hi H0) ^^^ (lo H0) := by - simp (config := {decide := true}) only [ q2_1, - h_s20_q16, h_s20_non_effects, h_s19_non_effects, - h_s18_q16, h_s18_non_effects, h0 ] + simp [ q2_1, h_v16_s20_lo ] simp only [hi, lo] bv_decide - have q3 : BitVec.extractLsb' 0 64 (r (StateField.SFP 17#5) s39) = - 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) := by - sorry - have q4 : (r (StateField.SFP 19#5) s39) = (r (StateField.SFP 19#5) s17) := by sym_aggregate - simp only [q0, h0, q1, h2, q2, q3, q4, h_e1] + have q4 : (r (StateField.SFP 19#5) s36) = (r (StateField.SFP 19#5) s17) := by sym_aggregate + simp only [q0, h_H0, q1, h_H2, q2, h_v17_s36, q4, h_e1] + generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 -- simplifying LHS simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, gcm_polyval_asm_gcm_polyval_equiv, @@ -416,7 +451,6 @@ 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] - generalize (gcm_init_H_asm (BitVec.extractLsb' 0 64 x1 ++ BitVec.extractLsb' 64 64 x1)) = H0 generalize (gcm_polyval_asm H0 H0) = H2 simp (config := {ground := true}) only -- simplifying RHS From 3a68c555ed92ab0435110b843173ef52a7db9a16 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 20 Nov 2024 00:07:38 +0000 Subject: [PATCH 12/27] Proving h_H3, h_H4, h_H5 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 118 ++++++++++++++++++++++++++++--- 1 file changed, 109 insertions(+), 9 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 92caecc2..3fd16b31 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -138,6 +138,10 @@ theorem gcm_polyval_asm_gcm_polyval_equiv (x : BitVec 128) (y : BitVec 128) : generalize h_A0B0 : DPSFP.polynomial_mult A0 B0 = A0B0 sorry +theorem gcm_polyval_asm_associativity (x : BitVec 128) (y : BitVec 128) (z : BitVec 128) : + gcm_polyval_asm x (gcm_polyval_asm y z) = gcm_polyval_asm (gcm_polyval_asm x y) z := by + sorry + -- Taken from gcm_gmult_v8 theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : DPSFP.pmull_op 0 64 1 x y 0#128 = @@ -181,12 +185,18 @@ theorem extractLsb'_of_xor_of_append_hi (x : BitVec 64) (y : BitVec 64) : (BitVec.extractLsb' 64 64 ((x ++ y) ^^^ (y ++ x))) = (x ^^^ y) := by bv_decide -theorem extractLsb'_of_xor_of_extractLsb' (x : BitVec 128): +theorem extractLsb'_of_xor_of_extractLsb'_lo (x : BitVec 128): (BitVec.extractLsb' 0 64 (x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x))) = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by bv_decide +theorem extractLsb'_of_xor_of_extractLsb'_hi (x : BitVec 128): + (BitVec.extractLsb' 64 64 + (x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x))) + = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by + bv_decide + syntax "gcm_init_v8_tac" : tactic macro_rules @@ -373,7 +383,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) extractLsb'_of_append_mid, h_s36_q17, h_s36_non_effects, h_s35_q22, h_s35_non_effects, - extractLsb'_of_xor_of_extractLsb', ] + extractLsb'_of_xor_of_extractLsb'_lo, ] simp only [h_v17_s34, h_e1] -- value of H1 have h_H1 : r (StateField.SFP 21#5) s37 = @@ -400,20 +410,16 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) extractLsb'_of_append_hi, extractLsb'_of_append_lo] -- Step 3: simulate up to H3_rev, H4 and H5_rev and verify sym_n 40 - have h_H3 : r (StateField.SFP 23#5) s77 = + have h_v16_s68 : r (StateField.SFP 16#5) s68 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev let H2 := gcm_polyval_asm H0 H0 - let H3 := GCMV8.gcm_polyval H0 H2 - (lo H3) ++ (hi H3) := by + gcm_polyval_asm H0 H2 := by -- TODO: I want to sym_aggregate, but only aggregate to last step, -- instead of all the way to the top -- sym_aggregate simp (config := {decide := true}) only [ - h_s77_non_effects, h_s76_non_effects, h_s75_non_effects, - h_s74_non_effects, h_s73_non_effects, h_s72_non_effects, - h_s71_non_effects, h_s70_q23, h_s70_non_effects, - h_s69_non_effects, h_s68_q16, h_s68_non_effects, + h_s68_q16, h_s68_non_effects, h_s67_non_effects, h_s66_q18, h_s66_non_effects, h_s65_non_effects, h_s64_q0, h_s64_non_effects, h_s63_non_effects, h_s62_q18, h_s62_non_effects, @@ -463,5 +469,99 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [Nat.reduceAdd, BitVec.shiftLeft_zero_eq, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, BitVec.reduceExtracLsb', BitVec.shiftLeft_eq] + have h_v17_s69 : r (StateField.SFP 17#5) s69 = + let x_rev := (lo x1) ++ (hi x1) + let H0 := gcm_init_H_asm x_rev + let H2 := gcm_polyval_asm H0 H0 + gcm_polyval_asm H2 H2 := by + simp (config := {decide := true}) only [ + h_s69_q17, h_s69_non_effects, h_s68_non_effects, + h_s67_q4, h_s67_non_effects, + h_s66_non_effects, h_s65_q5, h_s65_non_effects, + h_s64_non_effects, h_s63_q4, h_s63_non_effects, + h_s62_non_effects, h_s61_q5, h_s61_non_effects, + h_s60_non_effects, h_s59_q6, h_s59_non_effects, + h_s58_non_effects, h_s57_q7, h_s57_non_effects, + h_s56_non_effects, h_s55_q4, h_s55_non_effects, + h_s54_q6, h_s54_non_effects, + h_s53_non_effects, h_s52_non_effects, + h_s51_q6, h_s51_non_effects, + h_s50_q4, h_s50_non_effects, + h_s49_non_effects, h_s48_non_effects, + h_s47_q17, h_s47_non_effects, + h_s46_non_effects, h_s45_q6, h_s45_non_effects, + h_s44_non_effects, h_s43_q7, h_s43_non_effects, + h_s42_non_effects, h_s41_q5, h_s41_non_effects, + h_s40_non_effects, h_s39_non_effects, h_s38_non_effects, + ] + have q0 : (r (StateField.SFP 19#5) s37) = (r (StateField.SFP 19#5) s17) := by sym_aggregate + have q1 : (r (StateField.SFP 17#5) s37) = (r (StateField.SFP 17#5) s36) := by sym_aggregate + simp only [q0, h_H2, h_e1, q1, h_v17_s36] + -- 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] + simp (config := {ground := true}) only + -- simplifying RHS + 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] + -- simplify all + simp only [Nat.reduceAdd, BitVec.shiftLeft_zero_eq, BitVec.reduceAllOnes, + BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, + BitVec.reduceNot, BitVec.reduceExtracLsb', BitVec.shiftLeft_eq] + have h_H3 : r (StateField.SFP 23#5) s77 = + 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 + (lo H3) ++ (hi H3) := by + simp (config := {decide := true}) only [ + h_s77_non_effects, h_s76_non_effects, h_s75_non_effects, + h_s74_non_effects, h_s73_non_effects, h_s72_non_effects, + h_s71_non_effects, h_s70_q23, h_s70_non_effects, + h_s69_non_effects, extractLsb'_of_append_mid ] + simp only [h_v16_s68] + have h_H5 : r (StateField.SFP 25#5) s77 = + 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 + (lo H5) ++ (hi H5) := by + simp (config := {decide := true}) only [ + h_s77_non_effects, h_s76_non_effects, + h_s75_non_effects, h_s74_non_effects, + h_s73_non_effects, h_s72_non_effects, + h_s71_q25, h_s71_non_effects, + extractLsb'_of_append_mid,] + have q : r (StateField.SFP 17#5) s70 = r (StateField.SFP 17#5) s69 := by sym_aggregate + simp only [q, h_v17_s69, gcm_polyval_asm_associativity] + have h_H4 : r (StateField.SFP 24#5) s77 = + 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 + ((hi H5) ^^^ (lo H5)) ++ ((hi H3) ^^^ (lo H3)) := by + simp (config := {decide := true}) only [ + h_s77_non_effects, h_s76_q24, h_s76_non_effects, + h_s75_non_effects, h_s74_q17, h_s74_non_effects, + h_s73_q16, h_s73_non_effects, + h_s72_non_effects, + extractLsb'_of_append_mid] + have q0 : r (StateField.SFP 17#5) s71 = r (StateField.SFP 17#5) s69 := by sym_aggregate + have q1 : r (StateField.SFP 16#5) s71 = r (StateField.SFP 16#5) s68 := by sym_aggregate + have q2 : r (StateField.SFP 25#5) s71 = r (StateField.SFP 25#5) s77 := by sym_aggregate + have q3 : r (StateField.SFP 23#5) s71 = r (StateField.SFP 23#5) s77 := by sym_aggregate + simp only [q0, q1, q2, q3, h_v16_s68, h_v17_s69, h_H3, h_H5] + simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, + extractLsb'_of_xor_of_extractLsb'_lo, + gcm_polyval_asm_associativity] sym_n 1 sorry From c5c3d40851be77f7ec12b93385091f61703bde1f Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 20 Nov 2024 00:22:50 +0000 Subject: [PATCH 13/27] Proving h_H6, h_H7, h_H8 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 83 ++++++++++++++++++++++++++++++-- 1 file changed, 78 insertions(+), 5 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 3fd16b31..4238b98f 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -218,7 +218,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) (h_s0_pc : read_pc s0 = gcm_init_v8_program.min) (h_s0_sp_aligned : CheckSPAlignment s0) -- (h_run : sf = run gcm_init_v8_program.length s0) - (h_run : sf = run 78 s0) + (h_run : sf = run 116 s0) (h_mem : Memory.Region.pairwiseSeparate [ ⟨(H_addr s0), 128⟩, ⟨(Htable_addr s0), 2048⟩ ]) @@ -312,7 +312,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) extractLsb'_of_append_hi, extractLsb'_of_append_lo] simp (config := {ground := true}) only -- Step 2: simulate up to H1 and H2_rev and verify - sym_n 20 + sym_n 22 have h_v16_s20_hi : BitVec.extractLsb' 64 64 (r (StateField.SFP 16#5) s20) = let x_rev := (lo x1) ++ (hi x1) hi (gcm_init_H_asm x_rev) ^^^ lo (gcm_init_H_asm x_rev) := by @@ -409,7 +409,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [h_v17_s34, hi, lo, extractLsb'_of_append_hi, extractLsb'_of_append_lo] -- Step 3: simulate up to H3_rev, H4 and H5_rev and verify - sym_n 40 + sym_n 38 have h_v16_s68 : r (StateField.SFP 16#5) s68 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -539,9 +539,9 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s75_non_effects, h_s74_non_effects, h_s73_non_effects, h_s72_non_effects, h_s71_q25, h_s71_non_effects, + h_s70_non_effects, extractLsb'_of_append_mid,] - have q : r (StateField.SFP 17#5) s70 = r (StateField.SFP 17#5) s69 := by sym_aggregate - simp only [q, h_v17_s69, gcm_polyval_asm_associativity] + simp only [h_v17_s69, gcm_polyval_asm_associativity] have h_H4 : r (StateField.SFP 24#5) s77 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -563,5 +563,78 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, extractLsb'_of_xor_of_extractLsb'_lo, gcm_polyval_asm_associativity] + -- Step 4: simulate up to H6_rev, H7, and H8_rev and verify + sym_n 38 + have h_v16_s106 : r (StateField.SFP 16#5) s106 = + 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 + gcm_polyval_asm H0 H5 := by + sorry + have h_v17_s107 : r (StateField.SFP 17#5) s107 = + 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 + gcm_polyval_asm H0 H6 := 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 + 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 + lo H6 ++ hi H6 := by + simp (config := {decide := true}) only [ + h_s115_non_effects, h_s114_non_effects, h_s113_non_effects, + h_s112_non_effects, h_s111_non_effects, h_s110_non_effects, + h_s109_non_effects, h_s108_q26, h_s108_non_effects, + h_s107_non_effects, extractLsb'_of_append_mid ] + simp only [h_v16_s106] + have h_H8 : r (StateField.SFP 28#5) s115 = + 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 + let H8 := gcm_polyval_asm H0 H6 + lo H8 ++ hi H8 := by + simp (config := {decide := true}) only [ + h_s115_non_effects, h_s114_non_effects, + h_s113_non_effects, h_s112_non_effects, + h_s111_non_effects, h_s110_non_effects, + h_s109_q28, h_s109_non_effects, + h_s108_non_effects, + extractLsb'_of_append_mid,] + simp only [h_v17_s107, gcm_polyval_asm_associativity] + have h_H7 : r (StateField.SFP 27#5) s115 = + 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 + let H8 := gcm_polyval_asm H0 H6 + ((hi H8) ^^^ (lo H8)) ++ ((hi H6) ^^^ (lo H6)) := by + simp (config := {decide := true}) only [ + h_s115_non_effects, h_s114_q27, h_s113_non_effects, + h_s112_q17, h_s112_non_effects, + h_s111_q16, h_s111_non_effects, + h_s110_non_effects, + extractLsb'_of_append_mid] + have q0 : r (StateField.SFP 17#5) s109 = r (StateField.SFP 17#5) s107 := by sym_aggregate + have q1 : r (StateField.SFP 16#5) s109 = r (StateField.SFP 16#5) s106 := by sym_aggregate + have q2 : r (StateField.SFP 26#5) s109 = r (StateField.SFP 26#5) s115 := by sym_aggregate + have q3 : r (StateField.SFP 28#5) s109 = r (StateField.SFP 28#5) s115 := by sym_aggregate + simp only [q0, q1, q2, q3, h_v16_s106, h_v17_s107, h_H6, h_H8] + simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, + extractLsb'_of_xor_of_extractLsb'_lo, + gcm_polyval_asm_associativity] sym_n 1 sorry From e855c82e92ddd2409f17083f586b485eae7e6376 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 20 Nov 2024 01:37:11 +0000 Subject: [PATCH 14/27] Proving h_H9, h_H10 and h_H11 and finish the rest of the proof --- Proofs/AES-GCM/GCMInitV8Sym.lean | 205 ++++++++++++++++++++++++++++--- 1 file changed, 186 insertions(+), 19 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 4238b98f..1a8d32c2 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -218,7 +218,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) (h_s0_pc : read_pc s0 = gcm_init_v8_program.min) (h_s0_sp_aligned : CheckSPAlignment s0) -- (h_run : sf = run gcm_init_v8_program.length s0) - (h_run : sf = run 116 s0) + (h_run : sf = run 152 s0) (h_mem : Memory.Region.pairwiseSeparate [ ⟨(H_addr s0), 128⟩, ⟨(Htable_addr s0), 2048⟩ ]) @@ -230,9 +230,9 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) -- SP is still aligned ∧ CheckSPAlignment sf -- PC is updated - -- ∧ read_pc sf = read_gpr 64 30#5 s0 + ∧ read_pc sf = read_gpr 64 30#5 s0 -- Htable_addr ptr is moved to the start of the 10th element - -- ∧ Htable_addr sf = Htable_addr s0 + (9 * 16#64) + ∧ Htable_addr sf = Htable_addr s0 + (9 * 16#64) -- H_addr ptr stays the same ∧ H_addr sf = H_addr s0 -- v20 - v31 stores results of Htable @@ -248,12 +248,30 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) read_sfp 128 23#5 sf = (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 3 - -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) - -- read_sfp 128 24#5 sf = - -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 4 - -- ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) - -- read_sfp 128 25#5 sf = - -- (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 5 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 24#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 4 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 25#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 5 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 26#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 6 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 27#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 7 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 28#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 8 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 29#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 9 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 30#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 10 + ∧ let Hinit := (read_mem_bytes 16 (H_addr s0) s0) + read_sfp 128 31#5 sf = + (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 11 -- -- TODO: Commenting out memory related conjuncts since it seems -- to make symbolic execution stuck @@ -277,10 +295,10 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp (config := {ground := true}) only at h_s0_pc -- ^^ Still needed, because `gcm_init_v8_program.min` is somehow -- unable to be reflected + ------------------------------------------------ -- Step 1: simulate up to the instruction that saves the value for H0_rev -- Verify that v20 stores H0_rev sym_n 17 - -- simp only [Htable_addr, state_value] -- TODO: state_value is needed, why generalize x1_h: (Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem) = x1 at * change BitVec 128 at x1 -- value of q19 @@ -311,6 +329,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [lo, hi, gcm_init_H_asm, BitVec.partInstall, extractLsb'_of_append_hi, extractLsb'_of_append_lo] simp (config := {ground := true}) only + ------------------------------------------------ -- Step 2: simulate up to H1 and H2_rev and verify sym_n 22 have h_v16_s20_hi : BitVec.extractLsb' 64 64 (r (StateField.SFP 16#5) s20) = @@ -408,6 +427,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) extractLsb'_of_append_mid, ] simp only [h_v17_s34, hi, lo, extractLsb'_of_append_hi, extractLsb'_of_append_lo] + ------------------------------------------------ -- Step 3: simulate up to H3_rev, H4 and H5_rev and verify sym_n 38 have h_v16_s68 : r (StateField.SFP 16#5) s68 = @@ -555,14 +575,15 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s73_q16, h_s73_non_effects, h_s72_non_effects, extractLsb'_of_append_mid] - have q0 : r (StateField.SFP 17#5) s71 = r (StateField.SFP 17#5) s69 := by sym_aggregate - have q1 : r (StateField.SFP 16#5) s71 = r (StateField.SFP 16#5) s68 := by sym_aggregate - have q2 : r (StateField.SFP 25#5) s71 = r (StateField.SFP 25#5) s77 := by sym_aggregate - have q3 : r (StateField.SFP 23#5) s71 = r (StateField.SFP 23#5) s77 := by sym_aggregate + have q0 : r (StateField.SFP 17#5) s71 = r (StateField.SFP 17#5) s69 := by sorry + have q1 : r (StateField.SFP 16#5) s71 = r (StateField.SFP 16#5) s68 := by sorry + have q2 : r (StateField.SFP 25#5) s71 = r (StateField.SFP 25#5) s77 := by sorry + have q3 : r (StateField.SFP 23#5) s71 = r (StateField.SFP 23#5) s77 := by sorry simp only [q0, q1, q2, q3, h_v16_s68, h_v17_s69, h_H3, h_H5] simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, extractLsb'_of_xor_of_extractLsb'_lo, gcm_polyval_asm_associativity] + ------------------------------------------------ -- Step 4: simulate up to H6_rev, H7, and H8_rev and verify sym_n 38 have h_v16_s106 : r (StateField.SFP 16#5) s106 = @@ -628,13 +649,159 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s111_q16, h_s111_non_effects, h_s110_non_effects, extractLsb'_of_append_mid] - have q0 : r (StateField.SFP 17#5) s109 = r (StateField.SFP 17#5) s107 := by sym_aggregate - have q1 : r (StateField.SFP 16#5) s109 = r (StateField.SFP 16#5) s106 := by sym_aggregate - have q2 : r (StateField.SFP 26#5) s109 = r (StateField.SFP 26#5) s115 := by sym_aggregate - have q3 : r (StateField.SFP 28#5) s109 = r (StateField.SFP 28#5) s115 := by sym_aggregate + have q0 : r (StateField.SFP 17#5) s109 = r (StateField.SFP 17#5) s107 := by sorry + have q1 : r (StateField.SFP 16#5) s109 = r (StateField.SFP 16#5) s106 := by sorry + have q2 : r (StateField.SFP 26#5) s109 = r (StateField.SFP 26#5) s115 := by sorry + have q3 : r (StateField.SFP 28#5) s109 = r (StateField.SFP 28#5) s115 := by sorry simp only [q0, q1, q2, q3, h_v16_s106, h_v17_s107, h_H6, h_H8] simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, extractLsb'_of_xor_of_extractLsb'_lo, gcm_polyval_asm_associativity] + ------------------------------------------------ + -- Step 5: simulate up to H9_rev, H10, and H11_rev and verify + sym_n 36 + have h_v16_s144 : r (StateField.SFP 16#5) s144 = + 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 + let H8 := gcm_polyval_asm H0 H6 + gcm_polyval_asm H0 H8 := by + sorry + 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 + 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 + let H8 := gcm_polyval_asm H0 H6 + let H9 := gcm_polyval_asm H0 H8 + gcm_polyval_asm H0 H9 := by + sorry + have h_H9 : r (StateField.SFP 29#5) s151 = + 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 + let H8 := gcm_polyval_asm H0 H6 + let H9 := gcm_polyval_asm H0 H8 + lo H9 ++ hi H9 := by + simp (config := {decide := true}) only [ + h_s151_non_effects, h_s150_non_effects, h_s149_non_effects, + h_s148_non_effects, h_s147_non_effects, + h_s146_q29, h_s146_non_effects, + h_s145_non_effects, extractLsb'_of_append_mid ] + simp only [h_v16_s144, gcm_polyval_asm_associativity] + have h_H11 : r (StateField.SFP 31#5) s151 = + 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 + let H8 := gcm_polyval_asm H0 H6 + let H9 := gcm_polyval_asm H0 H8 + let H11 := gcm_polyval_asm H0 H9 + lo H11 ++ hi H11 := by + simp (config := {decide := true}) only [ + h_s151_non_effects, h_s150_non_effects, + h_s149_non_effects, h_s148_non_effects, + h_s147_q31, h_s147_non_effects, h_s146_non_effects, + extractLsb'_of_append_mid,] + simp only [h_v17_s145, gcm_polyval_asm_associativity] + have h_H10 : r (StateField.SFP 30#5) s151 = + 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 + let H8 := gcm_polyval_asm H0 H6 + let H9 := gcm_polyval_asm H0 H8 + let H11 := gcm_polyval_asm H0 H9 + ((hi H11) ^^^ (lo H11)) ++ ((hi H9) ^^^ (lo H9)) := by + simp (config := {decide := true}) only [ + h_s151_non_effects, h_s150_q30, h_s150_non_effects, + h_s149_q17, h_s149_non_effects, + h_s148_q16, h_s148_non_effects, + extractLsb'_of_append_mid] + have q0 : r (StateField.SFP 17#5) s147 = r (StateField.SFP 17#5) s145 := by sorry + have q1 : r (StateField.SFP 16#5) s147 = r (StateField.SFP 16#5) s144 := by sorry + have q2 : r (StateField.SFP 29#5) s147 = r (StateField.SFP 29#5) s151 := by sorry + have q3 : r (StateField.SFP 31#5) s147 = r (StateField.SFP 31#5) s151 := by sorry + simp only [q0, q1, q2, q3, h_v16_s144, h_v17_s145, h_H9, h_H11] + simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, + extractLsb'_of_xor_of_extractLsb'_lo, + gcm_polyval_asm_associativity] sym_n 1 - sorry + repeat' apply And.intro + · sym_aggregate + · simp only [Htable_addr, state_value] -- TODO: state_value is needed, why + sym_aggregate + bv_decide + · sym_aggregate + · have q : r (StateField.SFP 20#5) s151 = r (StateField.SFP 20#5) s17 := by sym_aggregate + 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 + 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 + 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 + 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 + 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 + 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 + 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 + 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 + 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 + 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 + simp only [q, h_H10, + 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 31#5) s151 = r (StateField.SFP 31#5) s151 := by sym_aggregate + simp only [q, h_H11, + GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, + gcm_init_H_asm_gcm_int_H_equiv, + gcm_polyval_asm_gcm_polyval_equiv] From eb0e911c91293bc27aa29a442e9f70fdc8a00b66 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 20 Nov 2024 04:51:12 +0000 Subject: [PATCH 15/27] Fix an import issue --- Proofs/AES-GCM/GCMInitV8Sym.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 1a8d32c2..ad810490 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -8,7 +8,6 @@ import Proofs.«AES-GCM».GCMInitV8Pre import Tactics.Sym import Tactics.Aggregate import Specs.GCMV8 -import Tactics.ExtractGoal namespace GCMInitV8Program From 263b643fef5afb09d4514aafd7610f742fdaf69b Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 20 Nov 2024 19:55:45 +0000 Subject: [PATCH 16/27] Clean up comments and proved some sorry'ed lemmas --- Proofs/AES-GCM/GCMInitV8Sym.lean | 96 +++++++++++++++++++++++--------- 1 file changed, 70 insertions(+), 26 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index ad810490..5e7eeaaf 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -19,7 +19,7 @@ abbrev Htable_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 0#5) s abbrev lo (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 0 64 x abbrev hi (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 64 64 x --- define a function that represents gcm_init_H in the assembly +-- Define a function that represents gcm_init_H in the assembly def gcm_init_H_asm (H : BitVec 128) : BitVec 128 := let v19 := 0xe1e1e1e1e1e1e1e1e1e1e1e1e1e1e1e1#128 let v19 := BitVec.shiftLeft (hi v19) 57 ++ BitVec.shiftLeft (lo v19) 57 @@ -37,10 +37,15 @@ def gcm_init_H_asm (H : BitVec 128) : BitVec 128 := let v20 := v3 ^^^ v16 v20 +-- FIXME: This proof takes a non-trivial amount of time in bv_decide +-- The bulk of time is spent in bitblasting because bitblasting +-- doesn't have cache for common subterms +-- See discussion in https://leanprover.zulipchat.com/#narrow/channel/424609-lean-at-aws/topic/.E2.9C.94.20stack.20overflow.20in.20bv_decide set_option maxRecDepth 3000 in set_option maxHeartbeats 1000000 in set_option sat.timeout 120 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 simp only [GCMV8.gcm_init_H, gcm_init_H_asm, hi, lo, @@ -55,6 +60,7 @@ theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : BitVec.ushiftRight_eq, BitVec.shiftLeft_eq, BitVec.reduceAppend] bv_decide +-- FIXME: prove the following lemma set_option maxRecDepth 10000 in set_option maxHeartbeats 1000000 in theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : @@ -141,7 +147,7 @@ theorem gcm_polyval_asm_associativity (x : BitVec 128) (y : BitVec 128) (z : Bit gcm_polyval_asm x (gcm_polyval_asm y z) = gcm_polyval_asm (gcm_polyval_asm x y) z := by sorry --- Taken from gcm_gmult_v8 +-- FIXME: Taken from gcm_gmult_v8 theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : DPSFP.pmull_op 0 64 1 x y 0#128 = DPSFP.polynomial_mult x y := by @@ -196,16 +202,8 @@ theorem extractLsb'_of_xor_of_extractLsb'_hi (x : BitVec 128): = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by bv_decide -syntax "gcm_init_v8_tac" : tactic - -macro_rules - | `(tactic| gcm_init_v8_tac) => - `(tactic| - (sorry)) - -set_option maxRecDepth 10000 in -set_option maxHeartbeats 4000000 in -set_option sat.timeout 120 in +set_option maxRecDepth 5000 in +set_option maxHeartbeats 1000000 in -- set_option pp.deepTerms true in -- set_option pp.maxSteps 1000000 in -- set_option trace.profiler true in @@ -216,8 +214,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) (h_s0_err : read_err s0 = .None) (h_s0_pc : read_pc s0 = gcm_init_v8_program.min) (h_s0_sp_aligned : CheckSPAlignment s0) - -- (h_run : sf = run gcm_init_v8_program.length s0) - (h_run : sf = run 152 s0) + (h_run : sf = run gcm_init_v8_program.length s0) (h_mem : Memory.Region.pairwiseSeparate [ ⟨(H_addr s0), 128⟩, ⟨(Htable_addr s0), 2048⟩ ]) @@ -574,10 +571,27 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s73_q16, h_s73_non_effects, h_s72_non_effects, extractLsb'_of_append_mid] - have q0 : r (StateField.SFP 17#5) s71 = r (StateField.SFP 17#5) s69 := by sorry - have q1 : r (StateField.SFP 16#5) s71 = r (StateField.SFP 16#5) s68 := by sorry - have q2 : r (StateField.SFP 25#5) s71 = r (StateField.SFP 25#5) s77 := by sorry - have q3 : r (StateField.SFP 23#5) s71 = r (StateField.SFP 23#5) s77 := by sorry + have q0 : r (StateField.SFP 17#5) s71 = r (StateField.SFP 17#5) s69 := by + -- FIXME: one could also use sym_aggregate, but it takes longer + simp (config := {decide := true}) only [ + h_s71_non_effects, h_s70_non_effects + ] + have q1 : r (StateField.SFP 16#5) s71 = r (StateField.SFP 16#5) s68 := by + simp (config := {decide := true}) only [ + h_s71_non_effects, h_s70_non_effects, h_s69_non_effects + ] + have q2 : r (StateField.SFP 25#5) s71 = r (StateField.SFP 25#5) s77 := by + simp (config := {decide := true}) only [ + h_s71_non_effects, h_s72_non_effects, h_s73_non_effects, + h_s74_non_effects, h_s75_non_effects, h_s76_non_effects, + h_s77_non_effects + ] + have q3 : r (StateField.SFP 23#5) s71 = r (StateField.SFP 23#5) s77 := by + simp (config := {decide := true}) only [ + h_s71_non_effects, h_s72_non_effects, h_s73_non_effects, + h_s74_non_effects, h_s75_non_effects, h_s76_non_effects, + h_s77_non_effects + ] simp only [q0, q1, q2, q3, h_v16_s68, h_v17_s69, h_H3, h_H5] simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, extractLsb'_of_xor_of_extractLsb'_lo, @@ -648,10 +662,26 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s111_q16, h_s111_non_effects, h_s110_non_effects, extractLsb'_of_append_mid] - have q0 : r (StateField.SFP 17#5) s109 = r (StateField.SFP 17#5) s107 := by sorry - have q1 : r (StateField.SFP 16#5) s109 = r (StateField.SFP 16#5) s106 := by sorry - have q2 : r (StateField.SFP 26#5) s109 = r (StateField.SFP 26#5) s115 := by sorry - have q3 : r (StateField.SFP 28#5) s109 = r (StateField.SFP 28#5) s115 := by sorry + have q0 : r (StateField.SFP 17#5) s109 = r (StateField.SFP 17#5) s107 := by + simp (config := {decide := true}) only [ + h_s109_non_effects, h_s108_non_effects + ] + have q1 : r (StateField.SFP 16#5) s109 = r (StateField.SFP 16#5) s106 := by + simp (config := {decide := true}) only [ + h_s109_non_effects, h_s108_non_effects, h_s107_non_effects + ] + have q2 : r (StateField.SFP 26#5) s109 = r (StateField.SFP 26#5) s115 := by + simp (config := {decide := true}) only [ + h_s109_non_effects, h_s110_non_effects, h_s111_non_effects, + h_s112_non_effects, h_s113_non_effects, h_s114_non_effects, + h_s115_non_effects + ] + have q3 : r (StateField.SFP 28#5) s109 = r (StateField.SFP 28#5) s115 := by + simp (config := {decide := true}) only [ + h_s109_non_effects, h_s110_non_effects, h_s111_non_effects, + h_s112_non_effects, h_s113_non_effects, h_s114_non_effects, + h_s115_non_effects + ] simp only [q0, q1, q2, q3, h_v16_s106, h_v17_s107, h_H6, h_H8] simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, extractLsb'_of_xor_of_extractLsb'_lo, @@ -729,10 +759,24 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s149_q17, h_s149_non_effects, h_s148_q16, h_s148_non_effects, extractLsb'_of_append_mid] - have q0 : r (StateField.SFP 17#5) s147 = r (StateField.SFP 17#5) s145 := by sorry - have q1 : r (StateField.SFP 16#5) s147 = r (StateField.SFP 16#5) s144 := by sorry - have q2 : r (StateField.SFP 29#5) s147 = r (StateField.SFP 29#5) s151 := by sorry - have q3 : r (StateField.SFP 31#5) s147 = r (StateField.SFP 31#5) s151 := by sorry + have q0 : r (StateField.SFP 17#5) s147 = r (StateField.SFP 17#5) s145 := by + simp (config := {decide := true}) only [ + h_s147_non_effects, h_s146_non_effects, + ] + have q1 : r (StateField.SFP 16#5) s147 = r (StateField.SFP 16#5) s144 := by + simp (config := {decide := true}) only [ + h_s147_non_effects, h_s146_non_effects, h_s145_non_effects + ] + have q2 : r (StateField.SFP 29#5) s147 = r (StateField.SFP 29#5) s151 := by + simp (config := {decide := true}) only [ + h_s147_non_effects, h_s148_non_effects, h_s149_non_effects, + h_s150_non_effects, h_s151_non_effects + ] + have q3 : r (StateField.SFP 31#5) s147 = r (StateField.SFP 31#5) s151 := by + simp (config := {decide := true}) only [ + h_s147_non_effects, h_s148_non_effects, h_s149_non_effects, + h_s150_non_effects, h_s151_non_effects + ] simp only [q0, q1, q2, q3, h_v16_s144, h_v17_s145, h_H9, h_H11] simp only [lo, hi, extractLsb'_of_xor_of_extractLsb'_hi, extractLsb'_of_xor_of_extractLsb'_lo, From 4fd2eb98ac26ae618aa1a8c41a1eb3da44e79317 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 21 Nov 2024 00:00:36 +0000 Subject: [PATCH 17/27] Proving h_v16_s106 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 69 +++++++++++++++++++++++++++++--- 1 file changed, 64 insertions(+), 5 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 5e7eeaaf..288e5d8e 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -61,11 +61,12 @@ theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : bv_decide -- FIXME: prove the following lemma -set_option maxRecDepth 10000 in -set_option maxHeartbeats 1000000 in theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : - GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by - sorry + GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by sorry + +-- FIXME: prove the following lemma +theorem polynomial_mult_commutativity (x y : BitVec 64) : + DPSFP.polynomial_mult x y = DPSFP.polynomial_mult y x := by sorry -- The following represents the assembly version of gcm_polyval def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := @@ -147,6 +148,10 @@ theorem gcm_polyval_asm_associativity (x : BitVec 128) (y : BitVec 128) (z : Bit gcm_polyval_asm x (gcm_polyval_asm y z) = gcm_polyval_asm (gcm_polyval_asm x y) z := by sorry +-- FIXME: prove the following lemma +theorem gcm_polyval_asm_commutativity (x y : BitVec 128) : + gcm_polyval_asm x y = gcm_polyval_asm y x := by sorry + -- FIXME: Taken from gcm_gmult_v8 theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : DPSFP.pmull_op 0 64 1 x y 0#128 = @@ -531,6 +536,17 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [Nat.reduceAdd, BitVec.shiftLeft_zero_eq, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, BitVec.reduceExtracLsb', BitVec.shiftLeft_eq] + have h_v16_s73 : r (StateField.SFP 16#5) s73 = + 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 + ((hi H3) ^^^ (lo H3)) ++ ((hi H3) ^^^ (lo H3)) := by sorry + have h_v18_s75 : r (StateField.SFP 18#5) s75 = + 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_H3 : r (StateField.SFP 23#5) s77 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -606,7 +622,50 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) let H3 := gcm_polyval_asm H0 H2 let H5 := gcm_polyval_asm H0 H3 gcm_polyval_asm H0 H5 := by - sorry + simp (config := {decide := true}) only [ + h_s106_q16, h_s106_non_effects, h_s105_non_effects, + h_s104_q18, h_s104_non_effects, h_s103_non_effects, + h_s102_q0, h_s102_non_effects, h_s101_non_effects, + h_s100_q18, h_s100_non_effects, h_s99_non_effects, + h_s98_q0, h_s98_non_effects, h_s97_non_effects, + h_s96_q1, h_s96_non_effects, h_s95_non_effects, + h_s94_q2, h_s94_non_effects, h_s93_non_effects, + h_s92_non_effects, h_s91_q18, h_s91_non_effects, + h_s90_q1, h_s90_non_effects, h_s89_non_effects, + h_s88_non_effects, h_s87_q1, h_s87_non_effects, + h_s86_q18, h_s86_non_effects, h_s85_non_effects, + h_s84_q16, h_s84_non_effects, h_s83_non_effects, + h_s82_q1, h_s82_non_effects, h_s81_non_effects, + h_s80_q2, h_s80_non_effects, h_s79_non_effects, + h_s78_q0, h_s78_non_effects + ] + have q0 : r (StateField.SFP 16#5) s77 = r (StateField.SFP 16#5) s73 := by sorry + have q1 : r (StateField.SFP 18#5) s77 = r (StateField.SFP 18#5) s75 := by sorry + have q2 : r (StateField.SFP 22#5) s77 = r (StateField.SFP 22#5) s37 := by sorry + have q3 : r (StateField.SFP 19#5) s77 = r (StateField.SFP 19#5) s17 := by sorry + simp only [q0, q1, q2, q3, h_v16_s73, h_v18_s75, h_H2, h_H3, h_e1] + generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 + -- 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] + generalize h_H2_var : (gcm_polyval_asm H0 H0) = H2 + generalize (gcm_polyval_asm H0 H2) = H3 + -- 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 H3)] + rw [polynomial_mult_commutativity (BitVec.extractLsb' 0 64 H2) (BitVec.extractLsb' 0 64 H3)] have h_v17_s107 : r (StateField.SFP 17#5) s107 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev From 03e57d9730105eeea9bd0e59d16452027b6d2a6f Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 21 Nov 2024 00:32:53 +0000 Subject: [PATCH 18/27] Proving h_v17_s107 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 43 +++++++++++++++++++++++++++++++- 1 file changed, 42 insertions(+), 1 deletion(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 288e5d8e..87b5e859 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -674,7 +674,48 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) let H5 := gcm_polyval_asm H0 H3 let H6 := gcm_polyval_asm H0 H5 gcm_polyval_asm H0 H6 := by - sorry + simp (config := {decide := true}) only [ + h_s107_q17, h_s107_non_effects, + h_s106_non_effects, h_s105_q4, h_s105_non_effects, + h_s104_non_effects, h_s103_q5, h_s103_non_effects, + h_s102_non_effects, h_s101_q4, h_s101_non_effects, + h_s100_non_effects, h_s99_q5, h_s99_non_effects, + h_s98_non_effects, h_s97_q6, h_s97_non_effects, + h_s96_non_effects, h_s95_q7, h_s95_non_effects, + h_s94_non_effects, h_s93_q4, h_s93_non_effects, + h_s92_q6, h_s92_non_effects, h_s91_non_effects, + h_s90_non_effects, h_s89_q6, h_s89_non_effects, + h_s88_q4, h_s88_non_effects, h_s87_non_effects, + h_s86_non_effects, h_s85_q17, h_s85_non_effects, + h_s84_non_effects, h_s83_q6, h_s83_non_effects, + h_s82_non_effects, h_s81_q7, h_s81_non_effects, + h_s80_non_effects, h_s79_q5, h_s79_non_effects, + h_s78_non_effects + ] + have q0 : r (StateField.SFP 16#5) s77 = r (StateField.SFP 16#5) s73 := by sorry + have q1 : r (StateField.SFP 19#5) s77 = r (StateField.SFP 19#5) s17 := by sorry + simp only [q0, q1, h_e1, h_H3, h_v16_s73] + generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 + generalize h_H3_var : (gcm_polyval_asm H0 (gcm_polyval_asm H0 H0)) = H3 + -- 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 + have q3 : (gcm_polyval_asm (gcm_polyval_asm H0 H0) H0) = H3 := by + rw [gcm_polyval_asm_commutativity (gcm_polyval_asm H0 H0) H0] + simp only [h_H3_var] + conv => + rhs + simp only [gcm_polyval_asm_associativity, q3] + 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] have h_H6 : r (StateField.SFP 26#5) s115 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev From 71d054da180cf3e14e6b9ed23fc88fafda15dee5 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 21 Nov 2024 00:46:05 +0000 Subject: [PATCH 19/27] Proving h_v16_s73 and h_v18_s75 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 87b5e859..edff150a 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -207,6 +207,11 @@ theorem extractLsb'_of_xor_of_extractLsb'_hi (x : BitVec 128): = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by bv_decide +theorem crock (x : BitVec 128) : + x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x) = + ((BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x) ++ + (BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x)) := by bv_decide + set_option maxRecDepth 5000 in set_option maxHeartbeats 1000000 in -- set_option pp.deepTerms true in @@ -541,7 +546,13 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) let H0 := gcm_init_H_asm x_rev let H2 := gcm_polyval_asm H0 H0 let H3 := gcm_polyval_asm H0 H2 - ((hi H3) ^^^ (lo H3)) ++ ((hi H3) ^^^ (lo H3)) := by sorry + ((hi H3) ^^^ (lo H3)) ++ ((hi H3) ^^^ (lo H3)) := by + simp (config := {decide := true}) only [ + h_s73_q16, h_s73_non_effects, + h_s72_non_effects, h_s71_non_effects, + h_s70_q23, h_s70_non_effects, h_s69_non_effects + ] + simp only [h_v16_s68, extractLsb'_of_append_mid, crock] have h_v18_s75 : r (StateField.SFP 18#5) s75 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev From da3b43475e6e97b3c81b68d69f83abafb14dc89b Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 21 Nov 2024 20:03:43 +0000 Subject: [PATCH 20/27] 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, From b708c6c00876df8af256dd4a1b3109a1eb07414a Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 21 Nov 2024 20:29:49 +0000 Subject: [PATCH 21/27] Proving h_v17_s145 --- Proofs/AES-GCM/GCMInitV8Sym.lean | 59 ++++++++++++++++++++++++++++++-- 1 file changed, 56 insertions(+), 3 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 0da95767..9a26bf5c 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -735,7 +735,16 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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 = + have h_v17_s112 : r (StateField.SFP 17#5) s112 = + 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 + let H8 := gcm_polyval_asm H0 H6 + (hi H8 ^^^ lo H8) ++ (hi H8 ^^^ lo H8) := by sorry + have h_v18_s113 : 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 @@ -843,7 +852,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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] + simp only [q0, q1, q2, q3, h_H6, h_H2, h_v16_s111, h_v18_s113, 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 @@ -876,7 +885,51 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) let H8 := gcm_polyval_asm H0 H6 let H9 := gcm_polyval_asm H0 H8 gcm_polyval_asm H0 H9 := by - sorry + simp (config := {decide := true}) only [ + h_s145_q17, h_s145_non_effects, + h_s144_non_effects, h_s143_q4, h_s143_non_effects, + h_s142_non_effects, h_s141_q5, h_s141_non_effects, + h_s140_non_effects, h_s139_q4, h_s139_non_effects, + h_s138_non_effects, h_s137_q5, h_s137_non_effects, + h_s136_non_effects, h_s135_q6, h_s135_non_effects, + h_s134_non_effects, h_s133_q7, h_s133_non_effects, + h_s132_non_effects, h_s131_q4, h_s131_non_effects, + h_s130_q6, h_s130_non_effects, h_s129_non_effects, + h_s128_non_effects, h_s127_q6, h_s127_non_effects, + h_s126_q4, h_s126_non_effects, h_s125_non_effects, + h_s124_non_effects, h_s123_q17, h_s123_non_effects, + h_s122_non_effects, h_s121_q6, h_s121_non_effects, + h_s120_non_effects, h_s119_q7, h_s119_non_effects, + h_s118_non_effects, h_s117_q5, h_s117_non_effects, + 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 17#5) s115 = r (StateField.SFP 17#5) s112 := 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_e1, h_H8, h_H2, h_v18_s113, h_v17_s112] + 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 (gcm_polyval_asm H0 H2)))) = H6 + -- 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 H6)] + rw [polynomial_mult_commutativity (BitVec.extractLsb' 0 64 H2) (BitVec.extractLsb' 0 64 H6)] have h_H9 : r (StateField.SFP 29#5) s151 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev From 0e35e5784e388f02d8f843ad34426c39bbf6b38b Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 21 Nov 2024 22:01:17 +0000 Subject: [PATCH 22/27] Proving all intermediate lemmas in the theorem --- Proofs/AES-GCM/GCMInitV8Sym.lean | 111 ++++++++++++++++++++++--------- 1 file changed, 80 insertions(+), 31 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 9a26bf5c..65bd65f5 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -212,6 +212,12 @@ theorem crock (x : BitVec 128) : ((BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x) ++ (BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x)) := by bv_decide + +theorem crock2 (x : BitVec 128) : + (BitVec.extractLsb' 64 64 x ++ BitVec.extractLsb' 0 64 x) ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x) = + ((BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x) ++ + (BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x)) := by bv_decide + set_option maxRecDepth 5000 in set_option maxHeartbeats 1000000 in -- set_option pp.deepTerms true in @@ -464,7 +470,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s41_non_effects, h_s40_q0, h_s40_non_effects, h_s39_non_effects, h_s38_non_effects, h_s37_non_effects] have q0 : r (StateField.SFP 20#5) s36 = r (StateField.SFP 20#5) s17 := by sym_aggregate - have q1 : r (StateField.SFP 22#5) s36 = r (StateField.SFP 22#5) s37 := by sym_aggregate + have q1 : r (StateField.SFP 22#5) s36 = r (StateField.SFP 22#5) s37 := by + simp (config := {decide := true}) only [ h_s37_non_effects ] have q2_1 : r (StateField.SFP 16#5) s36 = r (StateField.SFP 16#5) s20 := by sym_aggregate have q2 : BitVec.extractLsb' 0 64 (r (StateField.SFP 16#5) s36) = let x_rev := (lo x1) ++ (hi x1) @@ -521,7 +528,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s40_non_effects, h_s39_non_effects, h_s38_non_effects, ] have q0 : (r (StateField.SFP 19#5) s37) = (r (StateField.SFP 19#5) s17) := by sym_aggregate - have q1 : (r (StateField.SFP 17#5) s37) = (r (StateField.SFP 17#5) s36) := by sym_aggregate + have q1 : (r (StateField.SFP 17#5) s37) = (r (StateField.SFP 17#5) s36) := by + simp (config := {decide := true}) only [ h_s37_non_effects ] simp only [q0, h_H2, h_e1, q1, h_v17_s36] -- simplifying LHS simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, @@ -557,7 +565,14 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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 + ((hi H2) ^^^ (lo H2)) ++ ((hi H2) ^^^ (lo H2)) := by + simp (config := {decide := true}) only [ + h_s75_q18, h_s75_non_effects, h_s74_non_effects, + 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, crock2] have h_H3 : r (StateField.SFP 23#5) s77 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -650,10 +665,11 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s80_q2, h_s80_non_effects, h_s79_non_effects, h_s78_q0, h_s78_non_effects ] - have q0 : r (StateField.SFP 16#5) s77 = r (StateField.SFP 16#5) s73 := by sorry - have q1 : r (StateField.SFP 18#5) s77 = r (StateField.SFP 18#5) s75 := by sorry - have q2 : r (StateField.SFP 22#5) s77 = r (StateField.SFP 22#5) s37 := by sorry - have q3 : r (StateField.SFP 19#5) s77 = r (StateField.SFP 19#5) s17 := by sorry + have q0 : r (StateField.SFP 16#5) s77 = r (StateField.SFP 16#5) s73 := by sym_aggregate + have q1 : r (StateField.SFP 18#5) s77 = r (StateField.SFP 18#5) s75 := by + simp (config := {decide := true}) only [ h_s77_non_effects, h_s76_non_effects ] + have q2 : r (StateField.SFP 22#5) s77 = r (StateField.SFP 22#5) s37 := by sym_aggregate + have q3 : r (StateField.SFP 19#5) s77 = r (StateField.SFP 19#5) s17 := by sym_aggregate simp only [q0, q1, q2, q3, h_v16_s73, h_v18_s75, h_H2, h_H3, h_e1] generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 -- simplifying LHS @@ -703,8 +719,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s80_non_effects, h_s79_q5, h_s79_non_effects, h_s78_non_effects ] - have q0 : r (StateField.SFP 16#5) s77 = r (StateField.SFP 16#5) s73 := by sorry - have q1 : r (StateField.SFP 19#5) s77 = r (StateField.SFP 19#5) s17 := by sorry + have q0 : r (StateField.SFP 16#5) s77 = r (StateField.SFP 16#5) s73 := by sym_aggregate + have q1 : r (StateField.SFP 19#5) s77 = r (StateField.SFP 19#5) s17 := by sym_aggregate simp only [q0, q1, h_e1, h_H3, h_v16_s73] generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 generalize h_H3_var : (gcm_polyval_asm H0 (gcm_polyval_asm H0 H0)) = H3 @@ -734,7 +750,15 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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 + (hi H6 ^^^ lo H6) ++ (hi H6 ^^^ lo H6) := by + simp (config := {decide := true}) only [ + h_s111_q16, h_s111_non_effects, h_s110_non_effects, + h_s109_non_effects, h_s108_q26, h_s108_non_effects, + h_s107_non_effects, + ] + simp only [h_v16_s106, hi, lo, extractLsb'_of_append_mid, + extractLsb'_of_append_hi, + extractLsb'_of_append_lo, crock] have h_v17_s112 : r (StateField.SFP 17#5) s112 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -743,12 +767,30 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) let H5 := gcm_polyval_asm H0 H3 let H6 := gcm_polyval_asm H0 H5 let H8 := gcm_polyval_asm H0 H6 - (hi H8 ^^^ lo H8) ++ (hi H8 ^^^ lo H8) := by sorry + (hi H8 ^^^ lo H8) ++ (hi H8 ^^^ lo H8) := by + simp (config := {decide := true}) only [ + h_s112_q17, h_s112_non_effects, + h_s111_non_effects, h_s110_non_effects, + h_s109_q28, h_s109_non_effects, + h_s108_non_effects, + ] + simp only [h_v17_s107, hi, lo, extractLsb'_of_append_mid, + extractLsb'_of_append_hi, + extractLsb'_of_append_lo, crock] have h_v18_s113 : 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 + (hi H2 ^^^ lo H2) ++ (hi H2 ^^^ lo H2) := by + simp (config := {decide := true}) only [ + h_s113_q18, h_s113_non_effects, + h_s112_non_effects, h_s111_non_effects, + h_s110_q18, h_s110_non_effects, + ] + have q: r (StateField.SFP 22#5) s109 = r (StateField.SFP 22#5) s37 := by sym_aggregate + simp only [q, h_H2, hi, lo, extractLsb'_of_append_mid, + extractLsb'_of_append_hi, + extractLsb'_of_append_lo, crock2] have h_H6 : r (StateField.SFP 26#5) s115 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -848,10 +890,11 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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 + have q0 : r (StateField.SFP 22#5) s115 = r (StateField.SFP 22#5) s37 := by sym_aggregate + have q1 : r (StateField.SFP 16#5) s115 = r (StateField.SFP 16#5) s111 := by sym_aggregate + have q2 : r (StateField.SFP 18#5) s115 = r (StateField.SFP 18#5) s113 := by + simp (config := {decide := true}) only [ h_s115_non_effects, h_s114_non_effects ] + have q3 : r (StateField.SFP 19#5) s115 = r (StateField.SFP 19#5) s17 := by sym_aggregate simp only [q0, q1, q2, q3, h_H6, h_H2, h_v16_s111, h_v18_s113, h_e1] generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 generalize h_H2_var : (gcm_polyval_asm H0 H0) = H2 @@ -903,10 +946,16 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s118_non_effects, h_s117_q5, h_s117_non_effects, 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 17#5) s115 = r (StateField.SFP 17#5) s112 := 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 + have q0 : r (StateField.SFP 22#5) s115 = r (StateField.SFP 22#5) s37 := by sym_aggregate + have q1 : r (StateField.SFP 17#5) s115 = r (StateField.SFP 17#5) s112 := by + simp (config := {decide := true}) only [ + h_s115_non_effects, h_s114_non_effects, h_s113_non_effects + ] + have q2 : r (StateField.SFP 18#5) s115 = r (StateField.SFP 18#5) s113 := by + simp (config := {decide := true}) only [ + h_s115_non_effects, h_s114_non_effects + ] + have q3 : r (StateField.SFP 19#5) s115 = r (StateField.SFP 19#5) s17 := by sym_aggregate simp only [q0, q1, q2, q3, h_e1, h_H8, h_H2, h_v18_s113, h_v17_s112] generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 generalize h_H2_var : (gcm_polyval_asm H0 H0) = H2 @@ -1008,57 +1057,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 sorry + · have q : r (StateField.SFP 20#5) s151 = r (StateField.SFP 20#5) s17 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 21#5) s151 = r (StateField.SFP 21#5) s37 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 22#5) s151 = r (StateField.SFP 22#5) s37 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 23#5) s151 = r (StateField.SFP 23#5) s77 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 24#5) s151 = r (StateField.SFP 24#5) s77 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 25#5) s151 = r (StateField.SFP 25#5) s77 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 26#5) s151 = r (StateField.SFP 26#5) s115 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 27#5) s151 = r (StateField.SFP 27#5) s115 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 28#5) s151 = r (StateField.SFP 28#5) s115 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 29#5) s151 = r (StateField.SFP 29#5) s151 := by sym_aggregate 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 sorry + · have q : r (StateField.SFP 30#5) s151 = r (StateField.SFP 30#5) s151 := by sym_aggregate simp only [q, h_H10, GCMV8.GCMInitV8, List.get!, GCMV8.lo, GCMV8.hi, gcm_init_H_asm_gcm_int_H_equiv, From df846b7ccfa8ed1536dee8671811f82f85227f35 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Thu, 21 Nov 2024 22:54:45 +0000 Subject: [PATCH 23/27] Clarify bv lemmas and cleanup --- .../DPSFP/Advanced_simd_three_different.lean | 10 + Proofs/AES-GCM/GCMInitV8Sym.lean | 266 ++++++++---------- 2 files changed, 123 insertions(+), 153 deletions(-) diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean index c1cd5765..8887eb14 100644 --- a/Arm/Insts/DPSFP/Advanced_simd_three_different.lean +++ b/Arm/Insts/DPSFP/Advanced_simd_three_different.lean @@ -63,6 +63,16 @@ def pmull_op (e : Nat) (esize : Nat) (elements : Nat) (x : BitVec n) pmull_op (e + 1) esize elements x y result termination_by (elements - e) +theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : + DPSFP.pmull_op 0 64 1 x y 0#128 = + DPSFP.polynomial_mult x y := by + unfold DPSFP.pmull_op + simp (config := {ground := true}) only [minimal_theory] + unfold DPSFP.pmull_op + simp (config := {ground := true}) only [minimal_theory] + simp only [state_simp_rules, bitvec_rules] + done + @[state_simp_rules] def exec_pmull (inst : Advanced_simd_three_different_cls) (s : ArmState) : ArmState := -- This function assumes IsFeatureImplemented(FEAT_PMULL) is true diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 65bd65f5..19e2cddb 100644 --- a/Proofs/AES-GCM/GCMInitV8Sym.lean +++ b/Proofs/AES-GCM/GCMInitV8Sym.lean @@ -13,12 +13,74 @@ namespace GCMInitV8Program set_option bv.ac_nf false +------------------------------------ +-- Definitions + abbrev H_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 1#5) s abbrev Htable_addr (s : ArmState) : BitVec 64 := r (StateField.GPR 0#5) s abbrev lo (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 0 64 x abbrev hi (x : BitVec 128) : BitVec 64 := BitVec.extractLsb' 64 64 x +------------------------------------ +-- bv lemmas + +theorem extractLsb'_of_append_hi (x y : BitVec 64) : + BitVec.extractLsb' 64 64 (x ++ y) = x := by + bv_decide + +theorem extractLsb'_of_append_lo (x y : BitVec 64) : + BitVec.extractLsb' 0 64 (x ++ y) = y := by + bv_decide + +theorem extractLsb'_of_append_mid (x : BitVec 128) (y : BitVec 128): + BitVec.extractLsb' 64 128 (x ++ y) + = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 y := by + bv_decide + +theorem extractLsb'_append4_1 (x : BitVec 32) : + (BitVec.extractLsb' 0 32 (x ++ x ++ x ++ x)) = x := by bv_decide + +theorem extractLsb'_append4_2 (x : BitVec 32) : + (BitVec.extractLsb' 32 32 (x ++ x ++ x ++ x)) = x := by bv_decide + +theorem extractLsb'_append4_3 (x : BitVec 32) : + (BitVec.extractLsb' 64 32 (x ++ x ++ x ++ x)) = x := by bv_decide + +theorem extractLsb'_append4_4 (x : BitVec 32) : + (BitVec.extractLsb' 96 32 (x ++ x ++ x ++ x)) = x := by bv_decide + +theorem setWidth_extractLsb'_equiv_64_128 (x : BitVec 128) : + (BitVec.setWidth 64 x) = BitVec.extractLsb' 0 64 x := by bv_decide + +theorem xor_of_append_append_of_xor_equiv (x : BitVec 64) (y : BitVec 64) : + (x ++ y) ^^^ (y ++ x) =(x ^^^ y) ++ (x ^^^ y) := by bv_decide + +theorem bv_append_64_128 (x : BitVec 128) : + BitVec.extractLsb' 64 64 x ++ BitVec.extractLsb' 0 64 x = x := by bv_decide + +theorem extractLsb'_of_xor_of_extractLsb'_lo (x : BitVec 128): + (BitVec.extractLsb' 0 64 + (x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x))) + = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by + bv_decide + +theorem extractLsb'_of_xor_of_extractLsb'_hi (x : BitVec 128): + (BitVec.extractLsb' 64 64 + (x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x))) + = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by + bv_decide + +------------------------------------ + +-- FIXME: prove the following lemma +theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : + GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by sorry + +-- FIXME: prove the following lemma +theorem polynomial_mult_commutativity (x y : BitVec 64) : + DPSFP.polynomial_mult x y = DPSFP.polynomial_mult y x := by sorry + -- Define a function that represents gcm_init_H in the assembly def gcm_init_H_asm (H : BitVec 128) : BitVec 128 := let v19 := 0xe1e1e1e1e1e1e1e1e1e1e1e1e1e1e1e1#128 @@ -44,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 @@ -60,14 +122,6 @@ theorem gcm_init_H_asm_gcm_int_H_equiv (x : BitVec 128) : BitVec.ushiftRight_eq, BitVec.shiftLeft_eq, BitVec.reduceAppend] bv_decide --- FIXME: prove the following lemma -theorem gcm_polyval_mul_eq_polynomial_mult (x y : BitVec 128) : - GCMV8.gcm_polyval_mul x y = DPSFP.polynomial_mult x y := by sorry - --- FIXME: prove the following lemma -theorem polynomial_mult_commutativity (x y : BitVec 64) : - DPSFP.polynomial_mult x y = DPSFP.polynomial_mult y x := by sorry - -- The following represents the assembly version of gcm_polyval def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := let v19 := 0xe1e1e1e1e1e1e1e1e1e1e1e1e1e1e1e1#128 @@ -94,14 +148,6 @@ def gcm_polyval_asm (x : BitVec 128) (y : BitVec 128) : BitVec 128 := let v23 := v16 v23 -theorem extractLsb'_of_append_hi (x y : BitVec 64) : - BitVec.extractLsb' 64 64 (x ++ y) = x := by - bv_decide - -theorem extractLsb'_of_append_lo (x y : BitVec 64) : - BitVec.extractLsb' 0 64 (x ++ y) = y := by - bv_decide - -- https://kib.kiev.ua/x86docs/Intel/WhitePapers/323640-001.pdf def karatsuba_multiplication (x : BitVec 128) (y : BitVec 128) : BitVec 256 := let A1 := hi x @@ -122,7 +168,7 @@ def karatsuba_multiplication (x : BitVec 128) (y : BitVec 128) : BitVec 256 := theorem karatsuba_multiplication_equiv (x : BitVec 128) (y : BitVec 128) : DPSFP.polynomial_mult x y = karatsuba_multiplication x y := by sorry --- TODO: look into https://github.com/GaloisInc/saw-script/tree/master/rme for RME +-- FIXME: look into https://github.com/GaloisInc/saw-script/tree/master/rme for RME -- https://github.com/GaloisInc/aws-lc-verification/blob/0efc892de9a4d2660067ab02fdcef5993ff5184a/SAW/proof/AES/goal-rewrites.saw#L200-L214 set_option maxRecDepth 10000 in set_option maxHeartbeats 5000000 in @@ -144,82 +190,22 @@ theorem gcm_polyval_asm_gcm_polyval_equiv (x : BitVec 128) (y : BitVec 128) : generalize h_A0B0 : DPSFP.polynomial_mult A0 B0 = A0B0 sorry -theorem gcm_polyval_asm_associativity (x : BitVec 128) (y : BitVec 128) (z : BitVec 128) : - gcm_polyval_asm x (gcm_polyval_asm y z) = gcm_polyval_asm (gcm_polyval_asm x y) z := by - sorry - --- FIXME: prove the following lemma theorem gcm_polyval_asm_commutativity (x y : BitVec 128) : - gcm_polyval_asm x y = gcm_polyval_asm y x := by sorry - --- FIXME: Taken from gcm_gmult_v8 -theorem pmull_op_e_0_eize_64_elements_1_size_128_eq (x y : BitVec 64) : - DPSFP.pmull_op 0 64 1 x y 0#128 = - DPSFP.polynomial_mult x y := by - unfold DPSFP.pmull_op - simp (config := {ground := true}) only [minimal_theory] - unfold DPSFP.pmull_op - simp (config := {ground := true}) only [minimal_theory] - simp only [state_simp_rules, bitvec_rules] - done - -theorem extractLsb'_of_append_mid (x : BitVec 128) (y : BitVec 128): - BitVec.extractLsb' 64 128 (x ++ y) - = BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 y := by - bv_decide - -theorem extractLsb'_append4_1 (x : BitVec 32) : - (BitVec.extractLsb' 0 32 (x ++ x ++ x ++ x)) = x := by bv_decide - -theorem extractLsb'_append4_2 (x : BitVec 32) : - (BitVec.extractLsb' 32 32 (x ++ x ++ x ++ x)) = x := by bv_decide - -theorem extractLsb'_append4_3 (x : BitVec 32) : - (BitVec.extractLsb' 64 32 (x ++ x ++ x ++ x)) = x := by bv_decide - -theorem extractLsb'_append4_4 (x : BitVec 32) : - (BitVec.extractLsb' 96 32 (x ++ x ++ x ++ x)) = x := by bv_decide - -theorem setWidth_extractLsb'_equiv_64_128 (x : BitVec 128) : - (BitVec.setWidth 64 x) = BitVec.extractLsb' 0 64 x := by bv_decide - -theorem append_of_extractLsb'_of_append (x : BitVec 64) (y : BitVec 64) : - (BitVec.extractLsb' 0 64 (x ++ y)) ++ (BitVec.extractLsb' 64 64 (x ++ y)) - = y ++ x := by bv_decide - -theorem extractLsb'_of_xor_of_append (x : BitVec 64) (y : BitVec 64) : - (BitVec.extractLsb' 0 64 ((x ++ y) ^^^ (y ++ x))) - = (x ^^^ y) := by bv_decide - -theorem extractLsb'_of_xor_of_append_hi (x : BitVec 64) (y : BitVec 64) : - (BitVec.extractLsb' 64 64 ((x ++ y) ^^^ (y ++ x))) - = (x ^^^ y) := by bv_decide - -theorem extractLsb'_of_xor_of_extractLsb'_lo (x : BitVec 128): - (BitVec.extractLsb' 0 64 - (x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x))) - = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by - bv_decide - -theorem extractLsb'_of_xor_of_extractLsb'_hi (x : BitVec 128): - (BitVec.extractLsb' 64 64 - (x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x))) - = BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x := by - bv_decide - -theorem crock (x : BitVec 128) : - x ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x) = - ((BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x) ++ - (BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x)) := by bv_decide + gcm_polyval_asm x y = gcm_polyval_asm y x := by + simp only [gcm_polyval_asm, BitVec.partInstall, + lo, hi, polynomial_mult_commutativity] +-- FIXME: Prove the following lemma +theorem gcm_polyval_asm_associativity + (x : BitVec 128) (y : BitVec 128) (z : BitVec 128) : + gcm_polyval_asm x (gcm_polyval_asm y z) = + gcm_polyval_asm (gcm_polyval_asm x y) z := by + sorry -theorem crock2 (x : BitVec 128) : - (BitVec.extractLsb' 64 64 x ++ BitVec.extractLsb' 0 64 x) ^^^ (BitVec.extractLsb' 0 64 x ++ BitVec.extractLsb' 64 64 x) = - ((BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x) ++ - (BitVec.extractLsb' 64 64 x ^^^ BitVec.extractLsb' 0 64 x)) := by bv_decide +------------------------------------ set_option maxRecDepth 5000 in -set_option maxHeartbeats 1000000 in +set_option maxHeartbeats 2000000 in -- set_option pp.deepTerms true in -- set_option pp.maxSteps 1000000 in -- set_option trace.profiler true in @@ -285,12 +271,12 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) read_sfp 128 31#5 sf = (GCMV8.GCMInitV8 ((BitVec.extractLsb' 0 64 Hinit) ++ (BitVec.extractLsb' 64 64 Hinit))).get! 11 -- - -- TODO: Commenting out memory related conjuncts since it seems + -- FIXME: Commenting out memory related conjuncts since it seems -- to make symbolic execution stuck -- -- First 12 elements in Htable is correct -- ∧ read_mem_bytes 192 (Htable_addr s0) sf -- = revflat (GCMV8.GCMInitV8 (read_mem_bytes 16 (H_addr s0) s0)) - -- + -- ----------------------------------------- -- non-effects -- State values that shouldn't change do not change -- TODO: figure out all registers that are used ... @@ -336,7 +322,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, extractLsb'_of_append_lo, extractLsb'_append4_1, extractLsb'_append4_2, extractLsb'_append4_3, extractLsb'_append4_4, - setWidth_extractLsb'_equiv_64_128, extractLsb'_of_xor_of_append] + setWidth_extractLsb'_equiv_64_128] -- simplifying RHS simp only [lo, hi, gcm_init_H_asm, BitVec.partInstall, extractLsb'_of_append_hi, extractLsb'_of_append_lo] @@ -389,22 +375,15 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [h_H0, h_e1] generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 -- simplify LHS - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, + simp only [DPSFP.pmull_op_e_0_eize_64_elements_1_size_128_eq, BitVec.partInstall, lo, hi] simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, - extractLsb'_of_xor_of_append, extractLsb'_of_xor_of_append_hi] - simp only [Nat.reduceAdd, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, - BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, - BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.shiftLeft_zero_eq] + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128] -- simplify RHS simp only [gcm_polyval_asm, BitVec.partInstall, hi, lo] simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, - extractLsb'_of_xor_of_append] - simp only [Nat.reduceAdd, BitVec.reduceAllOnes, BitVec.truncate_eq_setWidth, - BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, - BitVec.reduceExtracLsb', BitVec.shiftLeft_eq, BitVec.shiftLeft_zero_eq] + xor_of_append_append_of_xor_equiv] have h_v17_s36 : BitVec.extractLsb' 0 64 (r (StateField.SFP 17#5) s36) = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -447,7 +426,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) let H0 := gcm_init_H_asm x_rev let H2 := gcm_polyval_asm H0 H0 gcm_polyval_asm H0 H2 := by - -- TODO: I want to sym_aggregate, but only aggregate to last step, + -- FIXME: I want to sym_aggregate, but only aggregate to last step, -- instead of all the way to the top -- sym_aggregate simp (config := {decide := true}) only [ @@ -484,24 +463,16 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [q0, h_H0, q1, h_H2, q2, h_v17_s36, q4, h_e1] generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 -- simplifying LHS - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, + simp only [DPSFP.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] + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128] generalize (gcm_polyval_asm H0 H0) = H2 - simp (config := {ground := true}) only -- simplifying RHS - simp only [gcm_polyval_asm, BitVec.partInstall] - simp only [hi, lo] at * + simp only [gcm_polyval_asm, BitVec.partInstall, hi, lo] simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, - extractLsb'_of_xor_of_append] - -- simplify all - simp only [Nat.reduceAdd, BitVec.shiftLeft_zero_eq, BitVec.reduceAllOnes, - BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, BitVec.reduceNot, - BitVec.reduceExtracLsb', BitVec.shiftLeft_eq] + extractLsb'_of_append_lo, xor_of_append_append_of_xor_equiv] have h_v17_s69 : r (StateField.SFP 17#5) s69 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -532,23 +503,15 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp (config := {decide := true}) only [ h_s37_non_effects ] simp only [q0, h_H2, h_e1, q1, h_v17_s36] -- simplifying LHS - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, + simp only [DPSFP.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] - simp (config := {ground := true}) only + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128] -- simplifying RHS - simp only [gcm_polyval_asm, BitVec.partInstall] - simp only [hi, lo] at * + simp only [gcm_polyval_asm, BitVec.partInstall, hi, lo] simp only [extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128, - extractLsb'_of_xor_of_append] - -- simplify all - simp only [Nat.reduceAdd, BitVec.shiftLeft_zero_eq, BitVec.reduceAllOnes, - BitVec.truncate_eq_setWidth, BitVec.reduceSetWidth, BitVec.reduceHShiftLeft, - BitVec.reduceNot, BitVec.reduceExtracLsb', BitVec.shiftLeft_eq] + extractLsb'_of_append_lo, xor_of_append_append_of_xor_equiv] have h_v16_s73 : r (StateField.SFP 16#5) s73 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -560,7 +523,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) h_s72_non_effects, h_s71_non_effects, h_s70_q23, h_s70_non_effects, h_s69_non_effects ] - simp only [h_v16_s68, extractLsb'_of_append_mid, crock] + simp only [h_v16_s68, extractLsb'_of_append_mid, + hi, lo, bv_append_64_128, ←xor_of_append_append_of_xor_equiv] have h_v18_s75 : r (StateField.SFP 18#5) s75 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -572,7 +536,8 @@ 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, crock2] + extractLsb'_of_append_hi, extractLsb'_of_append_lo, + bv_append_64_128, ←xor_of_append_append_of_xor_equiv] have h_H3 : r (StateField.SFP 23#5) s77 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -673,12 +638,11 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) simp only [q0, q1, q2, q3, h_v16_s73, h_v18_s75, h_H2, h_H3, h_e1] generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 -- simplifying LHS - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, + simp only [DPSFP.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] + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128] generalize h_H2_var : (gcm_polyval_asm H0 H0) = H2 generalize (gcm_polyval_asm H0 H2) = H3 -- simplifying RHS @@ -689,8 +653,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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] + extractLsb'_of_append_lo, xor_of_append_append_of_xor_equiv] rw [polynomial_mult_commutativity (BitVec.extractLsb' 64 64 H2) (BitVec.extractLsb' 64 64 H3)] rw [polynomial_mult_commutativity (BitVec.extractLsb' 0 64 H2) (BitVec.extractLsb' 0 64 H3)] have h_v17_s107 : r (StateField.SFP 17#5) s107 = @@ -725,12 +688,11 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) generalize (gcm_init_H_asm (lo x1 ++ hi x1)) = H0 generalize h_H3_var : (gcm_polyval_asm H0 (gcm_polyval_asm H0 H0)) = H3 -- simplifying LHS - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, + simp only [DPSFP.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] + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128] -- simplifying RHS have q3 : (gcm_polyval_asm (gcm_polyval_asm H0 H0) H0) = H3 := by rw [gcm_polyval_asm_commutativity (gcm_polyval_asm H0 H0) H0] @@ -741,8 +703,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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] + extractLsb'_of_append_lo, xor_of_append_append_of_xor_equiv] 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 @@ -758,7 +719,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) ] simp only [h_v16_s106, hi, lo, extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, crock] + extractLsb'_of_append_lo, + bv_append_64_128, ←xor_of_append_append_of_xor_equiv] have h_v17_s112 : r (StateField.SFP 17#5) s112 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -776,7 +738,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) ] simp only [h_v17_s107, hi, lo, extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, crock] + extractLsb'_of_append_lo, + bv_append_64_128, ←xor_of_append_append_of_xor_equiv] have h_v18_s113 : r (StateField.SFP 18#5) s113 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -790,7 +753,8 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) have q: r (StateField.SFP 22#5) s109 = r (StateField.SFP 22#5) s37 := by sym_aggregate simp only [q, h_H2, hi, lo, extractLsb'_of_append_mid, extractLsb'_of_append_hi, - extractLsb'_of_append_lo, crock2] + extractLsb'_of_append_lo, + xor_of_append_append_of_xor_equiv] have h_H6 : r (StateField.SFP 26#5) s115 = let x_rev := (lo x1) ++ (hi x1) let H0 := gcm_init_H_asm x_rev @@ -900,12 +864,11 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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, + simp only [DPSFP.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] + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128] -- simplifying RHS conv => rhs @@ -914,8 +877,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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] + extractLsb'_of_append_lo, xor_of_append_append_of_xor_equiv] 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 = @@ -961,12 +923,11 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) generalize h_H2_var : (gcm_polyval_asm H0 H0) = H2 generalize (gcm_polyval_asm H0 (gcm_polyval_asm H0 (gcm_polyval_asm H0 (gcm_polyval_asm H0 H2)))) = H6 -- simplifying LHS - simp only [pmull_op_e_0_eize_64_elements_1_size_128_eq, + simp only [DPSFP.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] + extractLsb'_of_append_lo, setWidth_extractLsb'_equiv_64_128] -- simplifying RHS conv => rhs @@ -975,8 +936,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) 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] + extractLsb'_of_append_lo, xor_of_append_append_of_xor_equiv] rw [polynomial_mult_commutativity (BitVec.extractLsb' 64 64 H2) (BitVec.extractLsb' 64 64 H6)] rw [polynomial_mult_commutativity (BitVec.extractLsb' 0 64 H2) (BitVec.extractLsb' 0 64 H6)] have h_H9 : r (StateField.SFP 29#5) s151 = @@ -1053,7 +1013,7 @@ theorem gcm_init_v8_program_correct (s0 sf : ArmState) sym_n 1 repeat' apply And.intro · sym_aggregate - · simp only [Htable_addr, state_value] -- TODO: state_value is needed, why + · simp only [Htable_addr, state_value] -- FIXME: state_value is needed, why sym_aggregate bv_decide · sym_aggregate From a54bfd09140e1f6ba50ec75bdba8ff1f22472baf Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Fri, 22 Nov 2024 01:02:52 +0000 Subject: [PATCH 24/27] 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 From e7e3cf63ce0ad1960f55d8abc08cbe625bb04efa Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Fri, 22 Nov 2024 19:00:34 +0000 Subject: [PATCH 25/27] Exposing the bv_decide problem --- Proofs/AES-GCM/GCMInitV8Sym.lean | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index e298b854..1c52c61e 100644 --- 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 From 42ae5e14e5786a880b933a1ba22d0da6651a4a9e Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Mon, 2 Dec 2024 18:54:57 +0000 Subject: [PATCH 26/27] Revert "Exposing the bv_decide problem" This reverts commit e7e3cf63ce0ad1960f55d8abc08cbe625bb04efa. --- Proofs/AES-GCM/GCMInitV8Sym.lean | 28 +++++++++++----------------- 1 file changed, 11 insertions(+), 17 deletions(-) diff --git a/Proofs/AES-GCM/GCMInitV8Sym.lean b/Proofs/AES-GCM/GCMInitV8Sym.lean index 1c52c61e..e298b854 100644 --- 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 From 2976e95ca0e05da4a72dbf9fe99cc853fb6353ff Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Mon, 2 Dec 2024 18:57:34 +0000 Subject: [PATCH 27/27] Removing debugging tests --- Specs/GCMV8.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Specs/GCMV8.lean b/Specs/GCMV8.lean index 3e258594..a491f1ff 100644 --- a/Specs/GCMV8.lean +++ b/Specs/GCMV8.lean @@ -145,8 +145,6 @@ example : reverse irrepoly = refpoly := by native_decide def gcm_init_H (H : BitVec 128) : BitVec 128 := pmod (H ++ 0b0#1) refpoly (by omega) -#eval gcm_init_H 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 - def gcm_polyval_red (x : BitVec 256) : BitVec 128 := reverse $ pmod (reverse x) irrepoly (by omega) @@ -162,8 +160,6 @@ def gcm_polyval_red (x : BitVec 256) : BitVec 128 := def gcm_polyval (x : BitVec 128) (y : BitVec 128) : BitVec 128 := GCMV8.gcm_polyval_red $ GCMV8.gcm_polyval_mul x y -#eval gcm_polyval 0xcdd297a9df1458771099f4b39468565c#128 0x88d320376963120dea0b3a488cb9209b#128 - /-- GCMInitV8 specification: H : [128] -- initial H input output : [12][128] -- precomputed Htable values