Skip to content

Commit

Permalink
Proving h_v16_s144
Browse files Browse the repository at this point in the history
  • Loading branch information
pennyannn committed Nov 21, 2024
1 parent 71d054d commit da3b434
Showing 1 changed file with 68 additions and 12 deletions.
80 changes: 68 additions & 12 deletions Proofs/AES-GCM/GCMInitV8Sym.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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,
Expand Down

0 comments on commit da3b434

Please sign in to comment.