Manually unroll the aes_hw_encrypt loop

pennyannn · Sep 5, 2024 · 4de6598 · 4de6598
1 parent 8e8a133
commit 4de6598
Show file tree

Hide file tree

Showing 2 changed files with 156 additions and 19 deletions.
diff --git a/Proofs/AES-GCM/AESHWEncryptSym.lean b/Proofs/AES-GCM/AESHWEncryptSym.lean
@@ -86,7 +86,6 @@ theorem AESHWEncrypt.csteps_eq (s : ArmState) (i : Nat) :
 
 #genStepEqTheorems aes_hw_encrypt_program
 
-
 theorem partial_correctness :
   PartialCorrectness ArmState := by
   apply Correctness.partial_correctness_from_verification_conditions
@@ -116,21 +115,158 @@ theorem termination :
   sorry
 
 
--- theorem aes_hw_encrypt_program_run_60 (s0 sf : ArmState)
---     (h_s0_program : s0.program = aes_hw_encrypt_program)
---     (h_s0_err : read_err s0 = .None)
---     (h_s0_pc : read_pc s0 = aes_hw_encrypt_program.min)
---     (h_s0_sp_aligned : CheckSPAlignment s0)
---     (h_run : sf = run 60 s0)
---     -- AES256 rounds = 14, the address of rounds is stored in x2
---     (h_rounds : 14 = read_mem_bytes 8 (read_gpr 64 2#5 s0) s0) :
---     read_err sf = .None := by
---   simp (config := {ground := true}) only at h_s0_pc
---   -- ^^ Still needed, because `aes_hw_encrypt_program.min` is somehow
---   --    unable to be reflected
---   -- TODO: branching condition currently not supported
---   sorry
---   -- sym_n 60
---   -- subst h_run
---   -- assumption
---   -- done
+-------------------------------------------------------------------------------
+
+abbrev in_addr   (s : ArmState) : BitVec 64 := r (StateField.GPR 0#5) s
+abbrev key_addr   (s : ArmState) : BitVec 64 := r (StateField.GPR 2#5) s
+abbrev round_addr   (s : ArmState) : BitVec 64 := (r (StateField.GPR 2#5) s) + 240#64
+abbrev out_addr   (s : ArmState) : BitVec 64 := r (StateField.GPR 1#5) s
+
+theorem aes_hw_encrypt_program_run_60 (s0 sf : ArmState)
+    (h_s0_program : s0.program = aes_hw_encrypt_program)
+    (h_s0_err : read_err s0 = .None)
+    (h_s0_pc : read_pc s0 = aes_hw_encrypt_program.min)
+    (h_s0_sp_aligned : CheckSPAlignment s0)
+    (h_run : sf = run 28 s0)
+    -- AES256 rounds = 14, the address of rounds is stored in x2
+    (h_rounds : 6 = read_mem_bytes 4 (round_addr s0) s0)
+    -- memory separation
+    (h_s0_in_key_separate :
+      mem_separate' (in_addr s0) 128 (key_addr s0) 304)
+    (h_s0_out_key_separate :
+      mem_separate' (out_addr s0) 128 (key_addr s0) 304)
+    (h_s0_in_out_separate :
+      mem_separate' (in_addr s0) 128 (out_addr s0) 128)
+     :
+    read_err sf = .None := by
+  simp (config := {ground := true}) only at h_s0_pc
+  -- ^^ Still needed, because `aes_hw_encrypt_program.min` is somehow
+  --    unable to be reflected
+  -- TODO: branching condition currently not supported so manually unroll loops
+  -- sym_n 13 fails with "tactic 'rewrite' failed, motive is not type correct"
+  sym_n 12
+  init_next_step h_run h_step_13 s13
+  replace h_step_13 := h_step_13.symm
+  rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_13<;> try assumption
+  simp only [h_s1_x3, h_s2_non_effects, h_s3_non_effects, h_s4_x3,
+             h_s5_non_effects, h_s6_non_effects, h_s7_non_effects,
+             h_s8_non_effects, h_s9_flagN, h_s9_flagV, h_s9_flagZ,
+             h_s9_flagC, h_s10_non_effects, h_s11_non_effects,
+             h_s12_non_effects, state_simp_rules, bitvec_rules,
+             minimal_theory] at h_step_13
+  simp only [round_addr] at h_rounds
+  simp (config := {ground := true}) only [h_rounds.symm, minimal_theory] at h_step_13
+  (intro_fetch_decode_lemmas h_step_13 h_s12_program "h_s12")
+  -- Add hypotheses that are needed for next loop iteration
+  have h_s13_non_effects : ∀ (f : StateField), f ≠ StateField.SFP 0x1#5 → f ≠ StateField.GPR 0x2#5 → f ≠ StateField.PC → r f s13 = r f s12 := by sorry
+  have h_s13_x3 : read_gpr 32 3#5 s13 = 2#32 := by sorry
+  --
+  -- sym_n 7 at s13
+  -- init_next_step h_run h_step_21 s21
+  -- replace h_step_21 := h_step_21.symm
+  -- rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_21<;> try assumption
+  -- simp only [state_simp_rules] at h_s13_x3
+  -- simp only [h_s20_non_effects, h_s19_non_effects, h_s18_non_effects,
+  --            h_s17_flagN, h_s17_flagV, h_s17_flagZ,
+  --            h_s17_flagC, h_s16_non_effects, h_s15_non_effects,
+  --            h_s14_non_effects, state_simp_rules, bitvec_rules,
+  --            minimal_theory,
+  --            -- hypothesis that states x3's value
+  --            h_s13_x3] at h_step_21
+  -- simp (config := {ground := true}) only [minimal_theory] at h_step_21
+  -- (intro_fetch_decode_lemmas h_step_21 h_s20_program "h_s20")
+  -- -- Add hypotheses that are needed for next loop iteration
+  -- have h_s21_non_effects : ∀ (f : StateField), f ≠ StateField.SFP 0x1#5 → f ≠ StateField.GPR 0x2#5 → f ≠ StateField.PC → r f s21 = r f s20 := by sorry
+  -- have h_s21_x3 : read_gpr 32 3#5 s21 = 0#32 := by sorry
+  -- --
+  -- sym_n 7 at s21
+  -- init_next_step h_run h_step_29 s29
+  -- replace h_step_29 := h_step_29.symm
+  -- rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_29<;> try assumption
+  -- simp only [state_simp_rules] at h_s21_x3
+  -- simp only [h_s28_non_effects, h_s27_non_effects, h_s26_non_effects,
+  --            h_s25_flagN, h_s25_flagV, h_s25_flagZ,
+  --            h_s25_flagC, h_s24_non_effects, h_s23_non_effects,
+  --            h_s22_non_effects, state_simp_rules, bitvec_rules,
+  --            minimal_theory,
+  --            -- hypothesis that states x3's value
+  --            h_s21_x3] at h_step_29
+  -- simp (config := {ground := true}) only [minimal_theory] at h_step_29
+  -- (intro_fetch_decode_lemmas h_step_29 h_s28_program "h_s28")
+  -- -- Add hypotheses that are needed for next loop iteration
+  -- have h_s29_non_effects : ∀ (f : StateField), f ≠ StateField.SFP 0x1#5 → f ≠ StateField.GPR 0x2#5 → f ≠ StateField.PC → r f s29 = r f s28 := by sorry
+  -- have h_s29_x3 : read_gpr 32 3#5 s29 = 6#32 := by sorry
+  -- --
+  -- sym_n 7 at s29
+  -- init_next_step h_run h_step_37 s37
+  -- replace h_step_37 := h_step_37.symm
+  -- rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_37<;> try assumption
+  -- simp only [state_simp_rules] at h_s29_x3
+  -- simp only [h_s36_non_effects, h_s35_non_effects, h_s34_non_effects,
+  --            h_s33_flagN, h_s33_flagV, h_s33_flagZ,
+  --            h_s33_flagC, h_s32_non_effects, h_s31_non_effects,
+  --            h_s30_non_effects, state_simp_rules, bitvec_rules,
+  --            minimal_theory,
+  --            -- hypothesis that states x3's value
+  --            h_s29_x3] at h_step_37
+  -- simp (config := {ground := true}) only [minimal_theory] at h_step_37
+  -- (intro_fetch_decode_lemmas h_step_37 h_s36_program "h_s36")
+  -- -- Add hypotheses that are needed for next loop iteration
+  -- have h_s37_non_effects : ∀ (f : StateField), f ≠ StateField.SFP 0x1#5 → f ≠ StateField.GPR 0x2#5 → f ≠ StateField.PC → r f s37 = r f s36 := by sorry
+  -- have h_s37_x3 : read_gpr 32 3#5 s37 = 4#32 := by sorry
+  -- --
+  -- sym_n 7 at s37
+  -- init_next_step h_run h_step_45 s45
+  -- replace h_step_45 := h_step_45.symm
+  -- rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_45<;> try assumption
+  -- simp only [state_simp_rules] at h_s37_x3
+  -- simp only [h_s44_non_effects, h_s43_non_effects, h_s42_non_effects,
+  --            h_s41_flagN, h_s41_flagV, h_s41_flagZ,
+  --            h_s41_flagC, h_s40_non_effects, h_s39_non_effects,
+  --            h_s38_non_effects, state_simp_rules, bitvec_rules,
+  --            minimal_theory,
+  --            -- hypothesis that states x3's value
+  --            h_s37_x3] at h_step_45
+  -- simp (config := {ground := true}) only [minimal_theory] at h_step_45
+  -- (intro_fetch_decode_lemmas h_step_45 h_s44_program "h_s36")
+  -- -- Add hypotheses that are needed for next loop iteration
+  -- have h_s45_non_effects : ∀ (f : StateField), f ≠ StateField.SFP 0x1#5 → f ≠ StateField.GPR 0x2#5 → f ≠ StateField.PC → r f s45 = r f s44 := by sorry
+  -- have h_s45_x3 : read_gpr 32 3#5 s45 = 2#32 := by sorry
+  -- --
+  -- sym_n 7 at s45
+  -- init_next_step h_run h_step_53 s53
+  -- replace h_step_53 := h_step_53.symm
+  -- rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_53<;> try assumption
+  -- simp only [state_simp_rules] at h_s45_x3
+  -- simp only [h_s52_non_effects, h_s51_non_effects, h_s50_non_effects,
+  --            h_s49_flagN, h_s49_flagV, h_s49_flagZ,
+  --            h_s49_flagC, h_s48_non_effects, h_s47_non_effects,
+  --            h_s46_non_effects, state_simp_rules, bitvec_rules,
+  --            minimal_theory,
+  --            -- hypothesis that states x3's value
+  --            h_s45_x3] at h_step_53
+  -- simp (config := {ground := true}) only [minimal_theory] at h_step_53
+  -- (intro_fetch_decode_lemmas h_step_53 h_s52_program "h_s36")
+  -- -- Add hypotheses that are needed for next loop iteration
+  -- have h_s53_non_effects : ∀ (f : StateField), f ≠ StateField.SFP 0x1#5 → f ≠ StateField.GPR 0x2#5 → f ≠ StateField.PC → r f s53 = r f s52 := by sorry
+  -- have h_s53_x3 : read_gpr 32 3#5 s53 = 0#32 := by sorry
+  --
+  sym_n 7 at s13
+  init_next_step h_run h_step_21 s21
+  replace h_step_21 := h_step_21.symm
+  rw [aes_hw_encrypt_program.stepi_eq_0x79f5d0] at h_step_21<;> try assumption
+  simp only [state_simp_rules] at h_s13_x3
+  simp only [h_s20_non_effects, h_s19_non_effects, h_s18_non_effects,
+             h_s17_flagN, h_s17_flagV, h_s17_flagZ,
+             h_s17_flagC, h_s16_non_effects, h_s15_non_effects,
+             h_s14_non_effects, state_simp_rules, bitvec_rules,
+             minimal_theory,
+             -- hypothesis that states x3's value
+             h_s13_x3] at h_step_21
+  simp (config := {ground := true}) only [minimal_theory] at h_step_21
+  (intro_fetch_decode_lemmas h_step_21 h_s20_program "h_s20")
+  --
+  sym_n 7 at s21
+  subst h_run
+  assumption
+  done
diff --git a/Proofs/AES-GCM/GCM.lean b/Proofs/AES-GCM/GCM.lean
@@ -5,3 +5,4 @@ Author(s): Alex Keizer
 -/
 import Proofs.«AES-GCM».GCMGmultV8Sym
 import Proofs.«AES-GCM».GCMInitV8Sym
+import Proofs.«AES-GCM».AESHWEncryptSym