Revert "Simplifying loop unrolling using sym_aggregate"

This reverts commit 31efd7c.
pennyannn · Sep 9, 2024 · da24d63 · da24d63
1 parent 385222d
commit da24d63
Showing 1 changed file with 23 additions and 13 deletions.
diff --git a/Proofs/AES-GCM/AESHWEncryptSym.lean b/Proofs/AES-GCM/AESHWEncryptSym.lean
@@ -6,7 +6,6 @@ Author(s): Yan Peng
 import Tests.«AES-GCM».AESHWEncryptProgram
 import Tactics.Sym
 import Tactics.StepThms
-import Tactics.Aggregate
 import Correctness.ArmSpec
 
 namespace AESHWEncryptProgram
@@ -41,26 +40,37 @@ theorem aes_hw_encrypt_program_run_60 (s0 sf : ArmState)
   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
-  sym_aggregate at h_step_13
   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
-  -- -- This is an aggregated result
-  -- have h_s13_x3 : read_gpr 32 3#5 s13 = 10#32 := by
-  --   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_x3, h_s10_non_effects,
-  --              h_s11_non_effects, h_s12_non_effects, h_step_13,
-  --              state_simp_rules, bitvec_rules, minimal_theory]
-  --   simp (config := {ground := true}) only [h_rounds.symm, minimal_theory]
+  -- Add hypotheses that are needed for next loop iteration
+  -- This is an aggregated result
+  have h_s13_x3 : read_gpr 32 3#5 s13 = 10#32 := by
+    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_x3, h_s10_non_effects,
+               h_s11_non_effects, h_s12_non_effects, h_step_13,
+               state_simp_rules, bitvec_rules, minimal_theory]
+    simp (config := {ground := true}) only [h_rounds.symm, minimal_theory]
   --
   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
-  sym_aggregate at h_step_21
+  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