refactor: rephrase the register frame-condition precondition as non-membership in a list of modified registers

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

@@ -203,7 +203,7 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
   -- Split conjunction
   repeat' apply And.intro
   · simp_mem; rfl
-  · 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

Proofs/Popcount32.lean

@@ -100,7 +100,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

@@ -85,7 +85,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

Tactics/Common.lean

@@ -284,6 +284,50 @@ def mkMemory : Expr := mkConst ``Memory
 def mkEqReflMemory (x : Expr) : Expr :=
   mkApp2 (.const ``Eq.refl [1]) mkMemory x
 
+/-- Return `<x> ∈ <xs>`, given expressions `α : Type u`, `x : α`
+and `xs : List α` -/
+def mkListMem (u : Level) (α x xs : Expr) : Expr :=
+  let list := mkApp (.const ``List [u]) α
+  let inst := mkApp (.const ``List.instMembership [u]) α
+  mkApp5 (.const ``Membership.mem [u,u]) α list inst xs x
+
+/-- Return `<f> ∈ <fs>`, given expressions `f : StateField`
+and `fs : List StateField` -/
+def mkStateFieldListMem (f fs : Expr) : Expr :=
+  mkListMem 0 (mkConst ``StateField) f fs
+
+/-- Return a proof of type `<x> ∈ <xs>`, given expressions `α : Type u`, `x : α`
+and `xs : List α`, assuming that `xs` is of the form `[x₁, x₂, ⋯, xₙ]` and that
+`x` is *syntactically* equal to one of the elements `xᵢ`.
+
+Returns `none` if the proof could not be constructed  -/
+partial def mkListMemProof (u : Level) (α x xs : Expr) : Option Expr := do
+  let_expr List.cons _α hd tl := xs | none
+  if hd == x then
+    mkApp3 (.const ``List.Mem.head [u]) α x tl
+  else
+    mkApp5 (.const ``List.Mem.tail [u]) α x hd tl (← mkListMemProof u α x tl)
+
+/-- auxiliary lemma for use in `mkNeProofOfMemAndNotMem` -/
+private theorem mkNeProofOfNotMemAndMem.aux.{u}
+    {α : Type u} {x y : α} {xs : List α}
+    (h_not_mem : x ∉ xs) (h_mem : y ∈ xs)  :
+    x ≠ y := by
+  rintro rfl; contradiction
+
+/-- Return a proof of type `<x> ≠ <y>`, given proofs
+`nonMemProof : <x> ∉ <xs>` and `memProof : <y> ∈ <xs>`, assuming that
+`α : Type u`, `x y : α`, and `xs : List α` -/
+@[inline] def mkNeProofOfNotMemAndMem (u : Level) (α x y xs nonMemProof memProof : Expr) :
+    Expr :=
+  mkApp6 (.const ``mkNeProofOfNotMemAndMem.aux [u]) α x y xs
+    nonMemProof memProof
+
+/-- Return a proof of `<x> ∉ <xs>`, given `notMemProof : <x> ∉ <y> :: xs`,
+assuming that `α : Type u`, `x y : α`, and `xs : List α` -/
+@[inline] def mkNotMemOfNotMemCons (u : Level) (α x y xs notMemProof : Expr) : Expr :=
+  mkApp5 (.const ``List.not_mem_of_not_mem_cons [u]) α x y xs notMemProof
+
 /-! ## Expr Helpers -/
 
 /-- Throw an error if `e` is not of type `expectedType` -/