fix proofs

Proofs/AES-GCM/AESHWEncryptSym.lean

@@ -39,7 +39,8 @@ 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,
+  simp (config := {decide := true}) 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,
@@ -51,7 +52,8 @@ theorem aes_hw_encrypt_program_run_60 (s0 sf : ArmState)
   -- 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,
+    simp (config := { decide := true }) 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,
@@ -63,106 +65,106 @@ theorem aes_hw_encrypt_program_run_60 (s0 sf : ArmState)
   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,
+  simp (config := { decide := true }) 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
   -- This is an aggregated result
   have h_s21_x3 : read_gpr 32 3#5 s21 = 8#32 := by
-    simp only [h_s20_non_effects, h_s19_non_effects, h_s18_non_effects,
+    simp (config := {decide := true}) only [
+               h_s20_non_effects, h_s19_non_effects, h_s18_non_effects,
                h_s17_x3, h_s16_non_effects, h_s15_non_effects,
-               h_s14_non_effects, h_step_21,
+               h_s14_non_effects, h_step_21, h_s13_x3,
                state_simp_rules, bitvec_rules, minimal_theory]
-    simp (config := {ground := true}) only [h_s13_x3, minimal_theory]
   --
   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,
+  simp (config := { decide := true }) 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
   -- This is an aggregated result
   have h_s29_x3 : read_gpr 32 3#5 s29 = 6#32 := by
-    simp only [h_s28_non_effects, h_s27_non_effects, h_s26_non_effects,
+    simp (config := { decide := true }) only [
+               h_s28_non_effects, h_s27_non_effects, h_s26_non_effects,
                h_s25_x3, h_s24_non_effects, h_s23_non_effects,
-               h_s22_non_effects, h_step_29,
+               h_s22_non_effects, h_step_29, h_s21_x3,
                state_simp_rules, bitvec_rules, minimal_theory]
-    simp (config := {ground := true}) only [h_s21_x3, minimal_theory]
   --
   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,
+  simp (config := { decide := true }) 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
   -- This is an aggregated result
   have h_s37_x3 : read_gpr 32 3#5 s37 = 4#32 := by
-    simp only [h_s36_non_effects, h_s35_non_effects, h_s34_non_effects,
+    simp (config := { decide := true }) only [
+               h_s36_non_effects, h_s35_non_effects, h_s34_non_effects,
                h_s33_x3, h_s32_non_effects, h_s31_non_effects,
-               h_s30_non_effects, h_step_37,
+               h_s30_non_effects, h_step_37, h_s29_x3,
                state_simp_rules, bitvec_rules, minimal_theory]
-    simp (config := {ground := true}) only [h_s29_x3, minimal_theory]
   --
   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,
+  simp (config := { decide := true }) 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_s44")
   -- Add hypotheses that are needed for next loop iteration
   -- This is an aggregated result
   have h_s45_x3 : read_gpr 32 3#5 s45 = 2#32 := by
-    simp only [h_s44_non_effects, h_s43_non_effects, h_s42_non_effects,
+    simp (config := { decide := true }) only [
+               h_s44_non_effects, h_s43_non_effects, h_s42_non_effects,
                h_s41_x3, h_s40_non_effects, h_s39_non_effects,
-               h_s38_non_effects, h_step_45,
+               h_s38_non_effects, h_step_45, h_s37_x3,
                state_simp_rules, bitvec_rules, minimal_theory]
-    simp (config := {ground := true}) only [h_s37_x3, minimal_theory]
   --
   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,
+  simp (config := { decide := true }) 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_s52")
   --
   sym_n 7 at s53

Proofs/AES-GCM/GCMGmultV8Sym.lean

@@ -120,7 +120,7 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
     -/
     rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
     simp_mem
-  · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp]
+  · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp] at *
     sym_aggregate
   · intro n addr h_separate
     simp_mem (config := { useOmegaToClose := false })

Proofs/Popcount32.lean

@@ -99,7 +99,9 @@ theorem popcount32_sym_meets_spec (s0 sf : ArmState)
     simp only [popcount32_spec, popcount32_spec_rec]
     bv_decide
   · -- Register Frame Condition
-    simp only [List.mem_cons, List.mem_singleton, not_or, and_imp]; sym_aggregate
+    simp only [List.mem_cons, List.mem_singleton, not_or, and_imp,
+      List.not_mem_nil, not_false_eq_true, true_implies] at *
+    sym_aggregate
   · -- Memory Frame Condition
     intro n addr h_separate
     simp only [memory_rules] at *

Tactics/Aggregate.lean

@@ -82,7 +82,7 @@ elab "sym_aggregate" simpConfig?:(config)? loc?:(location)? : tactic => withMain
         searchLCtxFor (whenFound := whenFound)
           /- By matching under binders, this also matches for non-effect
           hypotheses, which look like:
-            `∀ f, f ≠ _ → r f ?state = ?rhs`
+            `∀ f, f ∉ […] → r f ?state = ?rhs`
           -/
           (matchUnderBinders := true)
           (expectedType := do