From f55ff94bdc2661d3839cc9ab02ab228fb30797e6 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Mon, 26 Aug 2024 20:43:42 -0500
Subject: [PATCH 01/14] chore: add defn for List.pairwise mem_separate xs

---
 Arm/Memory/SeparateAutomation.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 3bc77c8e..fb9bbd90 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -181,6 +181,12 @@ abbrev MemLegalProof := Proof MemLegalProp
 def MemLegalProof.mk {e : MemLegalProp} (h : Expr) : MemLegalProof e :=
   { h }
 
+/--
+A proposition List.pairwise mem_separate' [x1, x2, ..., xn].
+-/
+structure MemPairwiseSeparateProp where
+  xs : Array Expr
+
 /-- info: Memory.read_bytes (n : Nat) (addr : BitVec 64) (m : Memory) : BitVec (n * 8) -/
 #guard_msgs in #check Memory.read_bytes
 
@@ -257,6 +263,7 @@ inductive Hypothesis
 | separate (proof : MemSeparateProof e)
 | subset (proof : MemSubsetProof e)
 | legal (proof : MemLegalProof e)
+| pairwise_separate (proof : MemPairwiseSeparateProof e)
 | read_eq (proof : ReadBytesEqProof)
 
 def Hypothesis.proof : Hypothesis → Expr

From 3e7ba478966d6091fcaa80458b634785ce21c849 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 11:08:35 -0500
Subject: [PATCH 02/14] chore: completely untested code for separation

---
 Arm/Memory/Separate.lean           |  52 ++++++++++++
 Arm/Memory/SeparateAutomation.lean | 129 ++++++++++++++++++++++++++++-
 2 files changed, 177 insertions(+), 4 deletions(-)

diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
index f1ecfd58..441caee2 100644
--- a/Arm/Memory/Separate.lean
+++ b/Arm/Memory/Separate.lean
@@ -328,6 +328,12 @@ theorem BitVec.not_le_eq_lt {a b : BitVec w₁} : (¬ (a ≤ b)) ↔ b < a := by
   rw [BitVec.le_def, BitVec.lt_def]
   omega
 
+theorem mem_separate'_comm (h : mem_separate' a an b bn) :
+    mem_separate' b bn a an := by
+  have := h.omega_def
+  apply mem_separate'.of_omega
+  omega
+
 /-#
 This is a theorem we ought to prove, which establishes the equivalence
 between the old and new defintions of 'mem_separate'.
@@ -560,4 +566,50 @@ theorem Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset'
       bv_omega
     · simp only [h, ↓reduceIte]
 
+/-- A region of memory, given by (base pointer, length) -/
+abbrev Memory.Region := BitVec 64 × Nat
+
+def Memory.Region.mk (a : BitVec 64) (n : Nat) : Memory.Region := (a, n)
+
+def Memory.Region.separate (a b : Memory.Region) : Prop :=
+  mem_separate' a.fst a.snd b.fst b.snd
+
+
+/-- A list of memory regions, that are known to be pairwise disjoint. -/
+def Memory.Region.pairwiseSeparate (mems : List Memory.Region) : Prop :=
+  mems.Pairwise Memory.Region.separate
+
+def Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem
+  (h : Memory.Region.pairwiseSeparate mems)
+  (i j : Nat)
+  (hij : i ≠ j)
+  (a b : Memory.Region)
+  (ha : mems.get? i = some a) (hb :mems.get? j = some b) :
+    mem_separate' a.fst a.snd b.fst b.snd := by
+  induction h generalizing a b i j
+  case nil => simp at ha
+  case cons x xs ihx _ihxs ihxs' =>
+    simp at ha hb
+    rcases i with rfl | i'
+    · simp at ha
+      · rcases j with rfl | j'
+        · simp at hij
+        · clear hij
+          subst ha
+          simp at hb
+          apply ihx
+          exact List.getElem?_mem hb
+    · rcases j with rfl | j'
+      · simp at hb
+        · subst hb
+          simp at ha
+          apply mem_separate'_comm
+          apply ihx
+          exact List.getElem?_mem ha
+      · simp at ha hb
+        apply ihxs' i' j'
+        · omega
+        · simp [ha]
+        · simp [hb]
+
 end NewDefinitions
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index fb9bbd90..cd26d454 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -121,6 +121,13 @@ instance [ToMessageData α] : ToMessageData (Proof α e) where
 structure MemSpanExpr where
   base : Expr
   n : Expr
+deriving Inhabited
+
+/-- info: Memory.Region.mk (a : BitVec 64) (n : Nat) : Memory.Region -/
+#guard_msgs in #check Memory.Region.mk
+
+def MemSpanExpr.toExpr (span : MemSpanExpr) : Expr :=
+  mkAppN (Expr.const ``Memory.Region.mk []) #[span.base, span.n]
 
 instance : ToMessageData MemSpanExpr where
   toMessageData span := m! "[{span.base}..{span.n})"
@@ -181,11 +188,37 @@ abbrev MemLegalProof := Proof MemLegalProp
 def MemLegalProof.mk {e : MemLegalProp} (h : Expr) : MemLegalProof e :=
   { h }
 
+
+/-- info: Memory.Region.pairwiseSeparate (mems : List Memory.Region) : Prop -/
+#guard_msgs in #check Memory.Region.pairwiseSeparate
+
 /--
-A proposition List.pairwise mem_separate' [x1, x2, ..., xn].
+A proposition `Memory.Region.pairwiseSeparate [x1, x2, ..., xn]`.
 -/
 structure MemPairwiseSeparateProp where
-  xs : Array Expr
+  xs : Array MemSpanExpr
+
+/-- info: List.nil.{u} {α : Type u} : List α -/
+#guard_msgs in #check List.nil
+
+/-- info: List.cons.{u} {α : Type u} (head : α) (tail : List α) : List α -/
+#guard_msgs in #check List.cons
+
+instance : ToExpr MemPairwiseSeparateProp where
+  toTypeExpr := mkConst ``Memory.Region.pairwiseSeparate
+
+  toExpr e := Id.run do
+    let memoryRegionTy : Expr := mkConst ``Memory.Region
+    let mut out := mkApp (mkConst  ``List.nil) memoryRegionTy
+    for x in e.xs do
+      out := mkAppN (mkConst ``List.cons) #[memoryRegionTy, x.toExpr, out]
+    let ty := mkConst ``Memory.Region.pairwiseSeparate
+    return (mkApp ty out)
+
+instance : ToMessageData MemPairwiseSeparateProp where
+  toMessageData e := m!"pairwiseSeparate {e.xs.toList}"
+
+abbrev MemPairwiseSeparateProof := Proof MemPairwiseSeparateProp
 
 /-- info: Memory.read_bytes (n : Nat) (addr : BitVec 64) (m : Memory) : BitVec (n * 8) -/
 #guard_msgs in #check Memory.read_bytes
@@ -263,11 +296,12 @@ inductive Hypothesis
 | separate (proof : MemSeparateProof e)
 | subset (proof : MemSubsetProof e)
 | legal (proof : MemLegalProof e)
-| pairwise_separate (proof : MemPairwiseSeparateProof e)
+| pairwiseSeparate (proof : MemPairwiseSeparateProof e)
 | read_eq (proof : ReadBytesEqProof)
 
 def Hypothesis.proof : Hypothesis → Expr
-| .separate proof  => proof.h
+| .pairwiseSeparate proof  => proof.h
+| .separate proof => proof.h
 | .subset proof => proof.h
 | .legal proof => proof.h
 | .read_eq proof => proof.h
@@ -278,6 +312,7 @@ instance : ToMessageData Hypothesis where
   | .separate proof => toMessageData proof
   | .legal proof => toMessageData proof
   | .read_eq proof => toMessageData proof
+  | .pairwiseSeparate proof => toMessageData proof
 
 /-- The internal state for the `SimpMemM` monad, recording previously encountered atoms. -/
 structure State where
@@ -404,6 +439,35 @@ def MemSeparateProp.ofExpr? (e : Expr) : Option MemSeparateProp :=
     .some { sa, sb }
   | _ => none
 
+/-- info: Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β -/
+#guard_msgs in #check Prod.mk
+
+/-- info: List.cons.{u} {α : Type u} (head : α) (tail : List α) : List α -/
+#guard_msgs in #check List.cons
+
+/-- info: List.nil.{u} {α : Type u} : List α -/
+#guard_msgs in #check List.nil
+
+/-- match an expression `e` to a `Memory.Region.pairwiseSeparate`. -/
+partial def MemPairwiseSeparateProof.ofExpr? (e : Expr) : Option MemPairwiseSeparateProp :=
+  match_expr e with
+  | Memory.Region.pairwiseSeparate xs => do
+      let .some xs := go xs #[] | none
+      some { xs := xs }
+  | _ => none
+  where
+    go (e : Expr) (xs : Array MemSpanExpr) : Option (Array MemSpanExpr) :=
+      match_expr e with
+      | List.cons _α ex exs =>
+        match_expr ex with
+        | Prod.mk _ta a _tn n =>
+          let x : MemSpanExpr := ⟨a, n⟩
+          go exs (xs.push x)
+        | _ => none
+      | List.nil _α => some xs
+      | _ => none
+
+
 /-- Match an expression `h` to see if it's a useful hypothesis. -/
 def hypothesisOfExpr (h : Expr) (hyps : Array Hypothesis) : MetaM (Array Hypothesis) := do
   let ht ← inferType h
@@ -424,6 +488,10 @@ def hypothesisOfExpr (h : Expr) (hyps : Array Hypothesis) : MetaM (Array Hypothe
     let proof : MemLegalProof legal := ⟨h⟩
     let hyps := hyps.push (.legal proof)
     return hyps
+  else if let .some pairwiseSep := MemPairwiseSeparateProof.ofExpr? ht then
+    let proof : MemPairwiseSeparateProof pairwiseSep := ⟨h⟩
+    let hyps := hyps.push (.pairwiseSeparate proof)
+    return hyps
   else
     let mut hyps := hyps
     for eqProof in ReadBytesEqProof.ofExpr? h ht do
@@ -487,6 +555,58 @@ def MemSeparateProof.addOmegaFacts (h : MemSeparateProof e) (args : Array Expr)
     trace[simp_mem.info]  "{h}: added omega fact ({h.omega_def})"
     return args.push (Expr.fvar fvar)
 
+
+/--
+info: Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem {mems : List Memory.Region}
+  (h : Memory.Region.pairwiseSeparate mems) (i j : Nat) (hij : i ≠ j) (a b : Memory.Region) (ha : mems.get? i = some a)
+  (hb : mems.get? j = some b) : mem_separate' a.fst a.snd b.fst b.snd
+-/
+#guard_msgs in #check Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem
+
+/-- info: Ne.{u} {α : Sort u} (a b : α) : Prop -/
+#guard_msgs in #check Ne
+
+/-- info: List.get?.{u} {α : Type u} (as : List α) (i : Nat) : Option α -/
+#guard_msgs in #check List.get?
+
+def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem
+    (self : MemPairwiseSeparateProof e) (i j : Nat) (a b : MemSpanExpr)  :
+    SimpMemM <| MemSeparateProof ⟨a, b⟩ := do
+  let iexpr := mkNatLit i
+  let jexpr := mkNatLit j
+
+    -- i ≠ j
+  let hijTy := mkAppN (mkConst ``Ne [0]) #[(mkConst ``Nat), mkNatLit i, mkNatLit j]
+  -- mems.get? i = some a
+  let haTy ← mkFreshExprMVar (type? := .none)
+  let hbTy ← mkFreshExprMVar (type? := .none)
+
+  let hijVal ← mkDecideProof hijTy
+  let haVal ← mkDecideProof haTy
+  let hbVal ← mkDecideProof hbTy
+  let a := e.xs[i]!
+
+  let h := mkAppN (Expr.const ``Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem [])
+    #[toExpr e, self.h, iexpr, jexpr, hijVal, a.toExpr, b.toExpr, haVal, hbVal]
+
+  return ⟨h⟩
+/--
+Currently, if the list is syntacticaly of the form [x1, ..., xn],
+ we create hypotheses of the form `mem_separate' xi xj` for all i, j..
+This can (and should) be generalized to pairwise separation given hypotheses x ∈ xs, x' ∈ xs.
+-/
+def MemPairwiseSeparateProof.addOmegaFacts (h : MemPairwiseSeparateProof e) (args : Array Expr) :
+    SimpMemM (Array Expr) := do
+  -- We need to loop over i, j where i < j and extract hypotheses.
+  -- We need to find the length of the list, and return an `Array MemRegion`.
+  let mut args := args
+  for i in [0:e.xs.size] do
+    for j in [i+1:e.xs.size] do
+      let a := e.xs[i]!
+      let b := e.xs[j]!
+      let proof ← h.mem_separate'_of_pairwiseSeparate_of_mem_of_mem i j a b
+      args ← proof.addOmegaFacts args
+  return args
 /--
 Given a hypothesis, add declarations that would be useful for omega-blasting
 -/
@@ -495,6 +615,7 @@ def Hypothesis.addOmegaFactsOfHyp (h : Hypothesis) (args : Array Expr) : SimpMem
   | Hypothesis.legal h => h.addOmegaFacts args
   | Hypothesis.subset h => h.addOmegaFacts args
   | Hypothesis.separate h => h.addOmegaFacts args
+  | Hypothesis.pairwiseSeparate h => h.addOmegaFacts args
   | Hypothesis.read_eq _h => return args -- read has no extra `omega` facts.
 
 /--

From 35f5e6c9d64b04be9776d35fb14a32a65572785b Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 11:38:14 -0500
Subject: [PATCH 03/14] chore: don't use decideProof in ways that don't work

---
 Arm/Memory/SeparateAutomation.lean     | 20 +++++++++++++++-----
 Proofs/Experiments/MemoryAliasing.lean |  4 ++++
 2 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index cd26d454..7f0d2595 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -129,6 +129,9 @@ deriving Inhabited
 def MemSpanExpr.toExpr (span : MemSpanExpr) : Expr :=
   mkAppN (Expr.const ``Memory.Region.mk []) #[span.base, span.n]
 
+def MemSpanExpr.toTypeExpr  : Expr :=
+    (Expr.const ``Memory.Region [])
+
 instance : ToMessageData MemSpanExpr where
   toMessageData span := m! "[{span.base}..{span.n})"
 
@@ -204,6 +207,9 @@ structure MemPairwiseSeparateProp where
 /-- info: List.cons.{u} {α : Type u} (head : α) (tail : List α) : List α -/
 #guard_msgs in #check List.cons
 
+def MemPairwiseSeparateProp.getMemSpanListExpr (h : MemPairwiseSeparateProp) : MetaM Expr :=
+  mkListLit (type := mkConst ``Memory.Region) <| (h.xs.map MemSpanExpr.toExpr).toList
+
 instance : ToExpr MemPairwiseSeparateProp where
   toTypeExpr := mkConst ``Memory.Region.pairwiseSeparate
 
@@ -569,8 +575,13 @@ info: Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem {mems : List Memo
 /-- info: List.get?.{u} {α : Type u} (as : List α) (i : Nat) : Option α -/
 #guard_msgs in #check List.get?
 
+def mkListGetEqSomeTy (mems : MemPairwiseSeparateProp) (i : Nat) (a : MemSpanExpr) : SimpMemM Expr := do
+  let lhs ← mkAppOptM ``List.get? #[.none, ← mems.getMemSpanListExpr, mkNatLit i]
+  let rhs ← mkSome MemSpanExpr.toTypeExpr a.toExpr
+  mkEq lhs rhs
+
 def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem
-    (self : MemPairwiseSeparateProof e) (i j : Nat) (a b : MemSpanExpr)  :
+    (self : MemPairwiseSeparateProof mems) (i j : Nat) (a b : MemSpanExpr)  :
     SimpMemM <| MemSeparateProof ⟨a, b⟩ := do
   let iexpr := mkNatLit i
   let jexpr := mkNatLit j
@@ -578,16 +589,15 @@ def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem
     -- i ≠ j
   let hijTy := mkAppN (mkConst ``Ne [0]) #[(mkConst ``Nat), mkNatLit i, mkNatLit j]
   -- mems.get? i = some a
-  let haTy ← mkFreshExprMVar (type? := .none)
-  let hbTy ← mkFreshExprMVar (type? := .none)
+  let haTy ← (mkListGetEqSomeTy mems i a)
+  let hbTy ← (mkListGetEqSomeTy mems j a)
 
   let hijVal ← mkDecideProof hijTy
   let haVal ← mkDecideProof haTy
   let hbVal ← mkDecideProof hbTy
-  let a := e.xs[i]!
 
   let h := mkAppN (Expr.const ``Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem [])
-    #[toExpr e, self.h, iexpr, jexpr, hijVal, a.toExpr, b.toExpr, haVal, hbVal]
+    #[← mems.getMemSpanListExpr, self.h, iexpr, jexpr, hijVal, a.toExpr, b.toExpr, haVal, hbVal]
 
   return ⟨h⟩
 /--
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 4a073007..6bb040dd 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -365,3 +365,7 @@ theorem mem_separate_move_of_lt_of_le  (h : mem_separate' a an b bn)
   (hlegal : a' ≤ a) : mem_separate' a' (an + (a - a').toNat) b bn := by simp_mem
 
 end MathProperties
+
+
+section PairwiseSeparate
+end PairwiseSeparate

From 80454dadb634d31e57d68a13e65b88384a09dd3d Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 13:22:33 -0500
Subject: [PATCH 04/14] chore: I don't understand this failure

---
 Arm/Memory/SeparateAutomation.lean     | 40 ++++++++++++++++++++------
 Proofs/Experiments/MemoryAliasing.lean | 11 +++++++
 2 files changed, 43 insertions(+), 8 deletions(-)

diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 7f0d2595..ff9663f6 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -354,6 +354,14 @@ def consumeRewriteFuel : SimpMemM Unit :=
 
 def outofRewriteFuel? : SimpMemM Bool := do
   return (← get).rewriteFuel == 0
+
+/-- Create a trace note that folds `header` with `(NOTE: can be large)`,
+and prints `msg` under such a trace node.
+-/
+def SimpMemM.traceLargeMsg (header : MessageData) (msg : MessageData) : SimpMemM Unit :=
+    withTraceNode m!"{header} (NOTE: can be large)" do
+      trace[simp_mem.info] msg
+
 /-
 Introduce a new definition into the local context,
 and return the FVarId of the new definition in the goal.
@@ -466,7 +474,7 @@ partial def MemPairwiseSeparateProof.ofExpr? (e : Expr) : Option MemPairwiseSepa
       match_expr e with
       | List.cons _α ex exs =>
         match_expr ex with
-        | Prod.mk _ta a _tn n =>
+        | Prod.mk _ta _tb a n =>
           let x : MemSpanExpr := ⟨a, n⟩
           go exs (xs.push x)
         | _ => none
@@ -575,6 +583,7 @@ info: Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem {mems : List Memo
 /-- info: List.get?.{u} {α : Type u} (as : List α) (i : Nat) : Option α -/
 #guard_msgs in #check List.get?
 
+/-- Make the expression `mems.get? i = some a`. -/
 def mkListGetEqSomeTy (mems : MemPairwiseSeparateProp) (i : Nat) (a : MemSpanExpr) : SimpMemM Expr := do
   let lhs ← mkAppOptM ``List.get? #[.none, ← mems.getMemSpanListExpr, mkNatLit i]
   let rhs ← mkSome MemSpanExpr.toTypeExpr a.toExpr
@@ -587,17 +596,30 @@ def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem
   let jexpr := mkNatLit j
 
     -- i ≠ j
-  let hijTy := mkAppN (mkConst ``Ne [0]) #[(mkConst ``Nat), mkNatLit i, mkNatLit j]
+  let hijTy := mkAppN (mkConst ``Ne [1]) #[(mkConst ``Nat), mkNatLit i, mkNatLit j]
+  _ ← inferType hijTy
+
   -- mems.get? i = some a
   let haTy ← (mkListGetEqSomeTy mems i a)
-  let hbTy ← (mkListGetEqSomeTy mems j a)
+  let hbTy ← (mkListGetEqSomeTy mems j b)
+
+  _ ← inferType haTy
+  _ ← inferType hbTy
 
   let hijVal ← mkDecideProof hijTy
-  let haVal ← mkDecideProof haTy
-  let hbVal ← mkDecideProof hbTy
+  let haVal ← mkEqRefl haTy
+  let hbVal ← mkEqRefl hbTy
 
   let h := mkAppN (Expr.const ``Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem [])
-    #[← mems.getMemSpanListExpr, self.h, iexpr, jexpr, hijVal, a.toExpr, b.toExpr, haVal, hbVal]
+    #[← mems.getMemSpanListExpr,
+      self.h,
+      iexpr,
+      jexpr,
+      hijVal,
+      a.toExpr,
+      b.toExpr,
+      haVal,
+      hbVal]
 
   return ⟨h⟩
 /--
@@ -614,8 +636,10 @@ def MemPairwiseSeparateProof.addOmegaFacts (h : MemPairwiseSeparateProof e) (arg
     for j in [i+1:e.xs.size] do
       let a := e.xs[i]!
       let b := e.xs[j]!
-      let proof ← h.mem_separate'_of_pairwiseSeparate_of_mem_of_mem i j a b
-      args ← proof.addOmegaFacts args
+      args ← SimpMemM.withTraceNode m!"Exploiting ({i}, {j}) : {a} ⟂ {b}" do
+        let proof ← h.mem_separate'_of_pairwiseSeparate_of_mem_of_mem i j a b
+        SimpMemM.traceLargeMsg m!"added {← inferType proof.h}" m!"{proof.h}"
+        proof.addOmegaFacts args
   return args
 /--
 Given a hypothesis, add declarations that would be useful for omega-blasting
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 6bb040dd..39d25945 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -367,5 +367,16 @@ theorem mem_separate_move_of_lt_of_le  (h : mem_separate' a an b bn)
 end MathProperties
 
 
+
 section PairwiseSeparate
+  theorem foo (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
+    mem_separate' a 100 b 200 := by
+
+    -- have : mem_separate' (a, 100).fst (a, 100).snd (d, 400).fst (d, 400).snd := by
+    --   apply Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem h 0 3
+    --   · decide
+    --   · rfl
+    --   · rfl
+    simp_mem
+
 end PairwiseSeparate

From f2877b9878bb2d26d5341b92a239381c767aeb04 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 13:27:46 -0500
Subject: [PATCH 05/14] chore: add separate example

---
 Arm/Memory/SeparateAutomation.lean     | 6 ++++--
 Proofs/Experiments/MemoryAliasing.lean | 7 +------
 2 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index ff9663f6..635ba963 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -607,8 +607,8 @@ def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem
   _ ← inferType hbTy
 
   let hijVal ← mkDecideProof hijTy
-  let haVal ← mkEqRefl haTy
-  let hbVal ← mkEqRefl hbTy
+  let haVal ← mkEqRefl <| ← mkSome MemSpanExpr.toTypeExpr a.toExpr
+  let hbVal ← mkEqRefl <| ← mkSome MemSpanExpr.toTypeExpr b.toExpr
 
   let h := mkAppN (Expr.const ``Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem [])
     #[← mems.getMemSpanListExpr,
@@ -621,6 +621,8 @@ def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem
       haVal,
       hbVal]
 
+  _ ← inferType h
+
   return ⟨h⟩
 /--
 Currently, if the list is syntacticaly of the form [x1, ..., xn],
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 39d25945..bcc0079f 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -371,12 +371,7 @@ end MathProperties
 section PairwiseSeparate
   theorem foo (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
     mem_separate' a 100 b 200 := by
-
-    -- have : mem_separate' (a, 100).fst (a, 100).snd (d, 400).fst (d, 400).snd := by
-    --   apply Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem h 0 3
-    --   · decide
-    --   · rfl
-    --   · rfl
     simp_mem
 
+
 end PairwiseSeparate

From 13e12ef05780ccef63f9219a37cd9015ec8f80ac Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 13:46:10 -0500
Subject: [PATCH 06/14] chore: add examples for pairwise

---
 Proofs/Experiments/MemoryAliasing.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index bcc0079f..472f1470 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -369,9 +369,15 @@ end MathProperties
 
 
 section PairwiseSeparate
-  theorem foo (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
+  /- Check that a direct implication of the pairwise separation is proven. -/
+  theorem pairwise_direct (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
     mem_separate' a 100 b 200 := by
     simp_mem
 
+  /- Check that a direct implication of the pairwise separation is proven. -/
+  theorem separate_of_pairwise (h : Memory.Region.pairwiseSeparate [⟨a, n⟩, ⟨b, m⟩, ⟨c, o⟩])
+    (hn' : n' < n) (hm' : m' < m) :
+    (mem_separate' a n' b m') := by
+  simp_mem
 
 end PairwiseSeparate

From 16ec26c511fdb13da911483b606f09be4844174f Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 14:10:17 -0500
Subject: [PATCH 07/14] chore: show example where better address normalization
 is needed

---
 Arm/Memory/SeparateAutomation.lean     | 20 ++++++++++++++-----
 Proofs/Experiments/MemoryAliasing.lean | 27 ++++++++++++++++++++++----
 2 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 635ba963..0831fd2c 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -18,6 +18,7 @@ import Lean.Meta.Tactic.Rewrite
 import Lean.Meta.Tactic.Rewrites
 import Lean.Elab.Tactic.Conv
 import Lean.Elab.Tactic.Conv.Basic
+import Tactics.Simp
 
 open Lean Meta Elab Tactic
 
@@ -363,14 +364,22 @@ def SimpMemM.traceLargeMsg (header : MessageData) (msg : MessageData) : SimpMemM
       trace[simp_mem.info] msg
 
 /-
-Introduce a new definition into the local context,
+Introduce a new definition into the local context, simplify it using `simp`,
 and return the FVarId of the new definition in the goal.
 -/
-def introDef (name : String) (hdefVal : Expr) : SimpMemM FVarId  := do
+def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId  := do
   SimpMemM.withMainContext do
+
     let name ← mkFreshUserName <| .mkSimple name
     let goal ← getMainGoal
     let hdefTy ← inferType hdefVal
+
+    let (simpCtx, simprocs) ← LNSymSimpContext (config := { decide := true, failIfUnchanged := false})
+    let (simpResult, _stats) ← simp hdefTy simpCtx simprocs
+    let hdefVal ← simpResult.mkCast hdefVal
+    let hdefTy ← inferType hdefVal
+    trace[simp_mem.info] "{processingEmoji} Simplified {hdefTy} to {hdefTy}"
+
     let goal ← goal.define name hdefTy hdefVal
     let (fvar, goal) ← goal.intro1P
     replaceMainGoal [goal]
@@ -527,7 +536,7 @@ def MemLegalProof.omega_def (h : MemLegalProof e) : Expr :=
 def MemLegalProof.addOmegaFacts (h : MemLegalProof e) (args : Array Expr) :
     SimpMemM (Array Expr) := do
   SimpMemM.withMainContext do
-    let fvar ← introDef "hmemLegal_omega" h.omega_def
+    let fvar ← simpAndIntroDef "hmemLegal_omega" h.omega_def
     trace[simp_mem.info]  "{h}: added omega fact ({h.omega_def})"
     return args.push (Expr.fvar fvar)
 
@@ -549,7 +558,7 @@ def MemSubsetProof.omega_def (h : MemSubsetProof e) : Expr :=
 def MemSubsetProof.addOmegaFacts (h : MemSubsetProof e) (args : Array Expr) :
     SimpMemM (Array Expr) := do
   SimpMemM.withMainContext do
-    let fvar ← introDef "hmemSubset_omega" h.omega_def
+    let fvar ← simpAndIntroDef "hmemSubset_omega" h.omega_def
     trace[simp_mem.info]  "{h}: added omega fact ({h.omega_def})"
     return args.push (Expr.fvar fvar)
 
@@ -565,7 +574,8 @@ def MemSeparateProof.omega_def (h : MemSeparateProof e) : Expr :=
 def MemSeparateProof.addOmegaFacts (h : MemSeparateProof e) (args : Array Expr) :
     SimpMemM (Array Expr) := do
   SimpMemM.withMainContext do
-    let fvar ← introDef "hmemSeparate_omega" h.omega_def
+    -- simp only [bitvec_rules] (failIfUnchanged := false)
+    let fvar ← simpAndIntroDef "hmemSeparate_omega" h.omega_def
     trace[simp_mem.info]  "{h}: added omega fact ({h.omega_def})"
     return args.push (Expr.fvar fvar)
 
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 472f1470..2ae23cfe 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -98,6 +98,26 @@ theorem separate_6 {n : Nat} (hn : n ≠ 0)
 /-- info: 'MemSeparate.separate_6' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms separate_6
 
+/-- constant shift for base pointer. -/
+theorem separate_7 (hm : m ≠ 0)
+    (l : mem_separate' a 100 b m)
+    (l : mem_separate' (a+100) 100 b m)  :
+    mem_separate' a 200 b m := by
+  simp_mem
+  sorry /- Need better address normalization. -/
+
+/-- symbolic shift for base pointer. -/
+theorem separate_8 {n : Nat} (hn : n ≠ 0) (hm : m ≠ 0)
+    (l : mem_separate' a n b m)
+    (l : mem_separate' (a+n) n b m)  :
+    mem_separate' a (2*n) b m := by
+  simp_mem
+  sorry  /- Need better address normalization. -/
+
+/-- info: 'MemSeparate.separate_6' depends on axioms: [propext, Classical.choice, Quot.sound] -/
+#guard_msgs in #print axioms separate_6
+
+
 end MemSeparate
 
 
@@ -375,9 +395,8 @@ section PairwiseSeparate
     simp_mem
 
   /- Check that a direct implication of the pairwise separation is proven. -/
-  theorem separate_of_pairwise (h : Memory.Region.pairwiseSeparate [⟨a, n⟩, ⟨b, m⟩, ⟨c, o⟩])
-    (hn' : n' < n) (hm' : m' < m) :
-    (mem_separate' a n' b m') := by
-  simp_mem
+  theorem pairwise_subset (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) :
+    mem_separate' a 80 b 100 := by
+    simp_mem
 
 end PairwiseSeparate

From f9d879a98797fae7d567d18d3d257363c6930324 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 14:47:19 -0500
Subject: [PATCH 08/14] chore: cleanup

---
 Arm/Memory/Separate.lean           | 27 +++++++------
 Arm/Memory/SeparateAutomation.lean | 62 +++++++++++++-----------------
 2 files changed, 41 insertions(+), 48 deletions(-)

diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
index 441caee2..69d62358 100644
--- a/Arm/Memory/Separate.lean
+++ b/Arm/Memory/Separate.lean
@@ -579,37 +579,40 @@ def Memory.Region.separate (a b : Memory.Region) : Prop :=
 def Memory.Region.pairwiseSeparate (mems : List Memory.Region) : Prop :=
   mems.Pairwise Memory.Region.separate
 
+/-- If `i ≠ j`, then prove that `mems[i] ⟂ mems[j]`.
+The theorem is stated in mildly awkward fashion for ease of use during proof automation.
+-/
 def Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem
   (h : Memory.Region.pairwiseSeparate mems)
   (i j : Nat)
   (hij : i ≠ j)
   (a b : Memory.Region)
-  (ha : mems.get? i = some a) (hb :mems.get? j = some b) :
+  (ha : mems.get? i = some a) (hb : mems.get? j = some b) :
     mem_separate' a.fst a.snd b.fst b.snd := by
   induction h generalizing a b i j
-  case nil => simp at ha
+  case nil => simp only [List.get?_eq_getElem?, List.getElem?_nil] at ha
   case cons x xs ihx _ihxs ihxs' =>
-    simp at ha hb
+    simp only [List.get?_eq_getElem?] at ha hb
     rcases i with rfl | i'
     · simp at ha
       · rcases j with rfl | j'
-        · simp at hij
-        · clear hij
-          subst ha
-          simp at hb
+        · simp only [ne_eq, not_true_eq_false] at hij
+        · subst ha
+          simp only [List.getElem?_cons_succ] at hb
           apply ihx
           exact List.getElem?_mem hb
     · rcases j with rfl | j'
-      · simp at hb
+      · simp only [List.length_cons, Nat.zero_lt_succ, List.getElem?_eq_getElem,
+        List.getElem_cons_zero, Option.some.injEq] at hb
         · subst hb
-          simp at ha
+          simp only [List.getElem?_cons_succ] at ha
           apply mem_separate'_comm
           apply ihx
           exact List.getElem?_mem ha
-      · simp at ha hb
+      · simp only [List.getElem?_cons_succ] at ha hb
         apply ihxs' i' j'
         · omega
-        · simp [ha]
-        · simp [hb]
+        · simp only [List.get?_eq_getElem?, ha]
+        · simp only [List.get?_eq_getElem?, hb]
 
 end NewDefinitions
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 0831fd2c..4d4a8ed9 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -208,19 +208,19 @@ structure MemPairwiseSeparateProp where
 /-- info: List.cons.{u} {α : Type u} (head : α) (tail : List α) : List α -/
 #guard_msgs in #check List.cons
 
-def MemPairwiseSeparateProp.getMemSpanListExpr (h : MemPairwiseSeparateProp) : MetaM Expr :=
-  mkListLit (type := mkConst ``Memory.Region) <| (h.xs.map MemSpanExpr.toExpr).toList
-
-instance : ToExpr MemPairwiseSeparateProp where
-  toTypeExpr := mkConst ``Memory.Region.pairwiseSeparate
+/-- Given `Memory.Region.pairwiseSeparate [x1, ..., xn]`,
+get the expression corresponding `[x1, ..., xn]`. -/
+def MemPairwiseSeparateProp.getMemSpanListExpr
+    (e : MemPairwiseSeparateProp) : Expr := Id.run do
+  let memoryRegionTy : Expr := mkConst ``Memory.Region
+  let mut out := mkApp (mkConst  ``List.nil) memoryRegionTy
+  for x in e.xs do
+    out := mkAppN (mkConst ``List.cons) #[memoryRegionTy, x.toExpr, out]
+  return out
 
-  toExpr e := Id.run do
-    let memoryRegionTy : Expr := mkConst ``Memory.Region
-    let mut out := mkApp (mkConst  ``List.nil) memoryRegionTy
-    for x in e.xs do
-      out := mkAppN (mkConst ``List.cons) #[memoryRegionTy, x.toExpr, out]
-    let ty := mkConst ``Memory.Region.pairwiseSeparate
-    return (mkApp ty out)
+/-- Get the expression `Memory.Region.pairwiseSeparate [x1, ..., xn]` -/
+def MemPairwiseSeparateProp.toExpr (e : MemPairwiseSeparateProp) : Expr :=
+  mkApp (mkConst ``Memory.Region.pairwiseSeparate) e.getMemSpanListExpr
 
 instance : ToMessageData MemPairwiseSeparateProp where
   toMessageData e := m!"pairwiseSeparate {e.xs.toList}"
@@ -374,11 +374,12 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId  := do
     let goal ← getMainGoal
     let hdefTy ← inferType hdefVal
 
-    let (simpCtx, simprocs) ← LNSymSimpContext (config := { decide := true, failIfUnchanged := false})
+    /- Simp to gain some more juice out of the defn.. -/
+    let (simpCtx, simprocs) ← LNSymSimpContext
+      (config := { decide := false, failIfUnchanged := false })
     let (simpResult, _stats) ← simp hdefTy simpCtx simprocs
     let hdefVal ← simpResult.mkCast hdefVal
     let hdefTy ← inferType hdefVal
-    trace[simp_mem.info] "{processingEmoji} Simplified {hdefTy} to {hdefTy}"
 
     let goal ← goal.define name hdefTy hdefVal
     let (fvar, goal) ← goal.intro1P
@@ -580,12 +581,6 @@ def MemSeparateProof.addOmegaFacts (h : MemSeparateProof e) (args : Array Expr)
     return args.push (Expr.fvar fvar)
 
 
-/--
-info: Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem {mems : List Memory.Region}
-  (h : Memory.Region.pairwiseSeparate mems) (i j : Nat) (hij : i ≠ j) (a b : Memory.Region) (ha : mems.get? i = some a)
-  (hb : mems.get? j = some b) : mem_separate' a.fst a.snd b.fst b.snd
--/
-#guard_msgs in #check Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem
 
 /-- info: Ne.{u} {α : Sort u} (a b : α) : Prop -/
 #guard_msgs in #check Ne
@@ -595,33 +590,31 @@ info: Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem {mems : List Memo
 
 /-- Make the expression `mems.get? i = some a`. -/
 def mkListGetEqSomeTy (mems : MemPairwiseSeparateProp) (i : Nat) (a : MemSpanExpr) : SimpMemM Expr := do
-  let lhs ← mkAppOptM ``List.get? #[.none, ← mems.getMemSpanListExpr, mkNatLit i]
+  let lhs ← mkAppOptM ``List.get? #[.none, mems.getMemSpanListExpr, mkNatLit i]
   let rhs ← mkSome MemSpanExpr.toTypeExpr a.toExpr
   mkEq lhs rhs
 
+/--
+info: Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem {mems : List Memory.Region}
+  (h : Memory.Region.pairwiseSeparate mems) (i j : Nat) (hij : i ≠ j) (a b : Memory.Region) (ha : mems.get? i = some a)
+  (hb : mems.get? j = some b) : mem_separate' a.fst a.snd b.fst b.snd
+-/
+#guard_msgs in #check Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem
+
+/-- make `Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem i j (by decide) a b rfl rfl`. -/
 def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem
     (self : MemPairwiseSeparateProof mems) (i j : Nat) (a b : MemSpanExpr)  :
     SimpMemM <| MemSeparateProof ⟨a, b⟩ := do
   let iexpr := mkNatLit i
   let jexpr := mkNatLit j
-
     -- i ≠ j
   let hijTy := mkAppN (mkConst ``Ne [1]) #[(mkConst ``Nat), mkNatLit i, mkNatLit j]
-  _ ← inferType hijTy
-
   -- mems.get? i = some a
-  let haTy ← (mkListGetEqSomeTy mems i a)
-  let hbTy ← (mkListGetEqSomeTy mems j b)
-
-  _ ← inferType haTy
-  _ ← inferType hbTy
-
   let hijVal ← mkDecideProof hijTy
   let haVal ← mkEqRefl <| ← mkSome MemSpanExpr.toTypeExpr a.toExpr
   let hbVal ← mkEqRefl <| ← mkSome MemSpanExpr.toTypeExpr b.toExpr
-
   let h := mkAppN (Expr.const ``Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem [])
-    #[← mems.getMemSpanListExpr,
+    #[mems.getMemSpanListExpr,
       self.h,
       iexpr,
       jexpr,
@@ -630,14 +623,11 @@ def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem
       b.toExpr,
       haVal,
       hbVal]
-
-  _ ← inferType h
-
   return ⟨h⟩
 /--
 Currently, if the list is syntacticaly of the form [x1, ..., xn],
  we create hypotheses of the form `mem_separate' xi xj` for all i, j..
-This can (and should) be generalized to pairwise separation given hypotheses x ∈ xs, x' ∈ xs.
+This can be generalized to pairwise separation given hypotheses x ∈ xs, x' ∈ xs.
 -/
 def MemPairwiseSeparateProof.addOmegaFacts (h : MemPairwiseSeparateProof e) (args : Array Expr) :
     SimpMemM (Array Expr) := do

From a8a8f642102eea8a890c096ecdccc60d81dc6d4b Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 14:47:45 -0500
Subject: [PATCH 09/14] chore: touchup

---
 Arm/Memory/Separate.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
index 69d62358..3e7386b9 100644
--- a/Arm/Memory/Separate.lean
+++ b/Arm/Memory/Separate.lean
@@ -571,10 +571,10 @@ abbrev Memory.Region := BitVec 64 × Nat
 
 def Memory.Region.mk (a : BitVec 64) (n : Nat) : Memory.Region := (a, n)
 
+/-- A hypothesis that memory regions `a` and `b` are separate. -/
 def Memory.Region.separate (a b : Memory.Region) : Prop :=
   mem_separate' a.fst a.snd b.fst b.snd
 
-
 /-- A list of memory regions, that are known to be pairwise disjoint. -/
 def Memory.Region.pairwiseSeparate (mems : List Memory.Region) : Prop :=
   mems.Pairwise Memory.Region.separate

From 75c343593ecb53f4e34a3544e527526c964c139e Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 27 Aug 2024 14:50:46 -0500
Subject: [PATCH 10/14] metaprogramming nits

---
 Arm/Memory/SeparateAutomation.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index 4d4a8ed9..ddff4c9e 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -213,9 +213,10 @@ get the expression corresponding `[x1, ..., xn]`. -/
 def MemPairwiseSeparateProp.getMemSpanListExpr
     (e : MemPairwiseSeparateProp) : Expr := Id.run do
   let memoryRegionTy : Expr := mkConst ``Memory.Region
-  let mut out := mkApp (mkConst  ``List.nil) memoryRegionTy
-  for x in e.xs do
-    out := mkAppN (mkConst ``List.cons) #[memoryRegionTy, x.toExpr, out]
+  let mut out := mkApp (mkConst  ``List.nil [0]) memoryRegionTy
+  for i in [0:e.xs.size] do
+    let x := e.xs[e.xs.size - i - 1]!
+    out := mkAppN (mkConst ``List.cons [0]) #[memoryRegionTy, x.toExpr, out]
   return out
 
 /-- Get the expression `Memory.Region.pairwiseSeparate [x1, ..., xn]` -/

From 56d5154ce6f77db2fe29355c5c81a0cb5373e692 Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Tue, 3 Sep 2024 21:47:35 -0500
Subject: [PATCH 11/14] Update Proofs/Experiments/MemoryAliasing.lean

Co-authored-by: Shilpi Goel <shigoel@gmail.com>
---
 Proofs/Experiments/MemoryAliasing.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 15a80f74..78cbe88a 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -175,7 +175,7 @@ theorem mem_automation_test_4
       (write_mem_bytes 48 src_addr val s0)) =
    val.extractLsBytes 1 10 := by
   simp only [memory_rules]
-  simp_mem -- TODO: repeat on change.
+  simp_mem
   congr 1
   bv_omega' -- TODO: address normalization.
 

From d38e1a50f6418ac4d8db2c18a76d20e2d7ebc0aa Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 4 Sep 2024 09:11:05 -0500
Subject: [PATCH 12/14] chore: scope trace enablement

---
 Proofs/Experiments/MemoryAliasing.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index 15a80f74..21c98c2c 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -399,10 +399,8 @@ end PairwiseSeparate
 
 namespace MemOptions
 
-set_option trace.simp_mem true
-set_option trace.simp_mem.info true
-
-
+set_option trace.simp_mem true in
+set_option trace.simp_mem.info true in
 /--
 error: unsolved goals
 ⊢ False
@@ -420,6 +418,8 @@ info: ⊢ False
   simp_mem (config := { failIfUnchanged := false })
   trace_state
 
+set_option trace.simp_mem true in
+set_option trace.simp_mem.info true in
 /--
 error: ❌️ simp_mem failed to make any progress.
 ---

From 34ded47cbed348e50422d9bb26cf78d4b3ab79bf Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 4 Sep 2024 16:31:16 -0500
Subject: [PATCH 13/14] chore: simp only

---
 Arm/Memory/Separate.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean
index a131b90a..c35b1da4 100644
--- a/Arm/Memory/Separate.lean
+++ b/Arm/Memory/Separate.lean
@@ -498,7 +498,7 @@ theorem Memory.read_bytes_write_bytes_eq_of_mem_subset'
   · subst hxn
     exfalso
     have h := i.isLt
-    simp at h
+    simp only [Nat.reduceMul, Nat.zero_mul, Nat.not_lt_zero] at h
   · by_cases h₁ : ↑i < xn * 8
     · simp only [h₁]
       simp only [decide_True, Bool.true_and]

From dd24b6dd0f2c6d7fd8ab0cde42ccd1e75b0838df Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Wed, 4 Sep 2024 16:49:54 -0500
Subject: [PATCH 14/14] chore: use custom simp set

---
 Arm/Memory/SeparateAutomation.lean | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index a361cede..e73ebd68 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -373,6 +373,9 @@ def getConfig : SimpMemM SimpMemConfig := do
   let ctx ← read
   return ctx.cfg
 
+/-- info: state_value (fld : StateField) : Type -/
+#guard_msgs in #check state_value
+
 /-
 Introduce a new definition into the local context, simplify it using `simp`,
 and return the FVarId of the new definition in the goal.
@@ -385,9 +388,20 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId  := do
     let hdefTy ← inferType hdefVal
 
     /- Simp to gain some more juice out of the defn.. -/
-    let (simpCtx, simprocs) ← LNSymSimpContext
-      (config := { decide := false, failIfUnchanged := false })
-    let (simpResult, _stats) ← simp hdefTy simpCtx simprocs
+    let mut simpTheorems : Array SimpTheorems := #[]
+    for a in #[`minimal_theory, `bitvec_rules] do
+      let some ext ← (getSimpExtension? a)
+        | throwError m!"[simp_mem] Internal error: simp attribute {a} not found!"
+      simpTheorems := simpTheorems.push (← ext.getTheorems)
+
+    -- unfold `state_value.
+    simpTheorems := simpTheorems.push <| ← ({} : SimpTheorems).addDeclToUnfold `state_value
+    let simpCtx : Simp.Context := { 
+      simpTheorems,
+      config := { decide := true, failIfUnchanged := false },
+      congrTheorems := (← Meta.getSimpCongrTheorems)
+    }
+    let (simpResult, _stats) ← simp hdefTy simpCtx (simprocs := #[])
     let hdefVal ← simpResult.mkCast hdefVal
     let hdefTy ← inferType hdefVal