From e397f57e3d860c7a9e1f9bb99405f2afb0f402de Mon Sep 17 00:00:00 2001
From: Siddharth <siddu.druid@gmail.com>
Date: Fri, 1 Nov 2024 10:43:34 -0500
Subject: [PATCH] feat: enable simp_mem to be used in ITP style [8/?] (#240)

### Description:

This adapts changes made in #238 for `mem_omega` into `simp_mem`. This
adds a ITP style mode into `simp_mem`, which receives user guidance and
attempts to proceed according to user input. It throws errors if the
goal state does not match the expected goal state. If the goal state
matches, it tries to dischange side conditions automatically. Failing
this, it creates new goals for the user to discharge these side
conditions. In total, this converts `simp_mem` into a tactic that's
usable for making incremental, interactive progress in simplifying
memory non-interference.

### Testing:

No semantics changed. Conformance succeeds.
---

Stacked on top of #238
What tests have been run? Did `make all` succeed for your changes? Was
conformance testing successful on an Aarch64 machine?

### License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.
---
 Arm/Memory/Common.lean                       |  53 ++--
 Arm/Memory/MemOmega.lean                     | 103 +++++---
 Arm/Memory/SeparateAutomation.lean           | 251 +++++++++++++++++--
 Proofs/AES-GCM/GCMGmultV8Sym.lean            |  14 +-
 Proofs/Experiments/Memcpy/MemCpyVCG.lean     |  21 +-
 Proofs/Experiments/MemoryAliasing.lean       | 175 ++++++++++++-
 Proofs/Experiments/SHA512MemoryAliasing.lean |   6 +-
 Proofs/SHA512/SHA512Prelude.lean             |  18 +-
 Tactics/BvOmegaBench.lean                    |  64 ++---
 9 files changed, 551 insertions(+), 154 deletions(-)

diff --git a/Arm/Memory/Common.lean b/Arm/Memory/Common.lean
index 41f909b9..2ee68e26 100644
--- a/Arm/Memory/Common.lean
+++ b/Arm/Memory/Common.lean
@@ -281,8 +281,8 @@ def TacticM.traceLargeMsg
 
 
 /-- TacticM's omega invoker -/
-def omega (g : MVarId) (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs) : MetaM Unit := do
-    BvOmegaBench.run g bvToNatSimpCtx bvToNatSimprocs
+def omega (g : MVarId) (hyps : Array Expr) (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs) : MetaM Unit := do
+    BvOmegaBench.run g hyps bvToNatSimpCtx bvToNatSimprocs
 
 /-
 Introduce a new definition into the local context, simplify it using `simp`,
@@ -757,6 +757,23 @@ instance : OmegaReducible MemSeparateProp where
     let bn := separate.sb.n
     mkAppN (Expr.const ``mem_separate'.of_omega []) #[an, bn, a, b]
 
+
+/-- For a goal that is reducible to `Omega`, make a new goal to be presented to the user -/
+def mkProofGoalForOmega {α : Type} [ToMessageData α] [OmegaReducible α] (e : α) : MetaM (Proof α e × MVarId) := do
+  let proofFromOmegaVal := (OmegaReducible.reduceToOmega e)
+  -- (h : a.toNat + n ≤ 2 ^ 64) → mem_legal' a n
+  let proofFromOmegaTy ← inferType (OmegaReducible.reduceToOmega e)
+  -- trace[simp_mem.info] "partially applied: '{proofFromOmegaVal} : {proofFromOmegaTy}'"
+  let omegaObligationTy ← do -- (h : a.toNat + n ≤ 2 ^ 64)
+    match proofFromOmegaTy with
+    | Expr.forallE _argName argTy _body _binderInfo => pure argTy
+    | _ => throwError "expected '{proofFromOmegaTy}' to a ∀"
+  trace[simp_mem.info] "omega obligation '{omegaObligationTy}'"
+  let omegaObligationVal ← mkFreshExprMVar (type? := omegaObligationTy)
+  let factProof := mkAppN proofFromOmegaVal #[omegaObligationVal]
+  let g := omegaObligationVal.mvarId!
+  return (Proof.mk (← instantiateMVars factProof), g)
+
 /--
 `OmegaReducible` is a value whose type is `omegaFact → desiredFact`.
 An example is `mem_lega'.of_omega n a`, which has type:
@@ -766,8 +783,10 @@ An example is `mem_lega'.of_omega n a`, which has type:
   a way to convert `e : α` into the `omegaToDesiredFactFnVal`.
 -/
 def proveWithOmega?  {α : Type} [ToMessageData α] [OmegaReducible α] (e : α)
+    (extraOmegaAssumptions : Array Expr)
     (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs)
     (hyps : Array Memory.Hypothesis) : MetaM (Option (Proof α e)) := do
+  -- TODO: refactor to use mkProofGoalForOmega
   let proofFromOmegaVal := (OmegaReducible.reduceToOmega e)
   -- (h : a.toNat + n ≤ 2 ^ 64) → mem_legal' a n
   let proofFromOmegaTy ← inferType (OmegaReducible.reduceToOmega e)
@@ -782,9 +801,9 @@ def proveWithOmega?  {α : Type} [ToMessageData α] [OmegaReducible α] (e : α)
   let g := omegaObligationVal.mvarId!
   g.withContext do
   try
-    let (_, g) ← Hypothesis.addOmegaFactsOfHyps g hyps.toList #[]
+    let (omegaAssumptions, g) ← Hypothesis.addOmegaFactsOfHyps g hyps.toList #[]
     trace[simp_mem.info] m!"Executing `omega` to close {e}"
-    omega g bvToNatSimpCtx bvToNatSimprocs
+    omega g (omegaAssumptions ++ extraOmegaAssumptions) bvToNatSimpCtx bvToNatSimprocs
     trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
     return (.some <| Proof.mk (← instantiateMVars factProof))
   catch e =>
@@ -792,30 +811,10 @@ def proveWithOmega?  {α : Type} [ToMessageData α] [OmegaReducible α] (e : α)
     return none
   end ReductionToOmega
 
-/--
-simplify the goal state, closing legality, subset, and separation goals,
-and simplifying all other expressions. return `true` if goal has been closed, and `false` otherwise.
--/
-partial def closeMemSideCondition (g : MVarId)
-    (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs)
-    (hyps : Array Memory.Hypothesis) : MetaM Bool := do
-  g.withContext do
-    trace[simp_mem.info] "{processingEmoji} Matching on ⊢ {← g.getType}"
-    let gt ← g.getType
-    if let .some e := MemLegalProp.ofExpr? gt then
-      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
-        if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then
-          g.assign proof.h
-    if let .some e := MemSubsetProp.ofExpr? gt then
-      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
-        if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then
-          g.assign proof.h
-    if let .some e := MemSeparateProp.ofExpr? gt then
-      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
-        if let .some proof ← proveWithOmega? e bvToNatSimpCtx bvToNatSimprocs hyps then
-          g.assign proof.h
-  return ← g.isAssigned
 
+/-- Collect nondependent hypotheses that are propositions. -/
+def _root_.Lean.MVarId.getNondepPropExprs (g : MVarId) : MetaM (Array Expr) := do
+  return ((← g.getNondepPropHyps).map Expr.fvar)
 
 
 
diff --git a/Arm/Memory/MemOmega.lean b/Arm/Memory/MemOmega.lean
index d44fff04..30840e51 100644
--- a/Arm/Memory/MemOmega.lean
+++ b/Arm/Memory/MemOmega.lean
@@ -39,6 +39,11 @@ inductive UserHyp
 | expr : Expr → UserHyp
 
 namespace UserHyp
+def ofExpr (e : Expr) : UserHyp := 
+  if e.isFVar then
+    .hyp e.fvarId!
+  else 
+    .expr e
 end UserHyp
 
 
@@ -88,6 +93,33 @@ namespace MemOmegaM
   def run (ctx : Context) (x : MemOmegaM α) : MetaM α := ReaderT.run x ctx
 end MemOmegaM
 
+/--
+simplify the goal state, closing legality, subset, and separation goals,
+and simplifying all other expressions. return `true` if goal has been closed, and `false` otherwise.
+-/
+private def closeMemSideCondition (g : MVarId) (extraHyps : Array Expr)
+    (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs)
+    (hyps : Array Memory.Hypothesis) : MetaM Bool := do
+  -- TODO: take user selected hyps.
+  g.withContext do
+    trace[simp_mem.info] "{processingEmoji} Matching on ⊢ {← g.getType}"
+    let gt ← g.getType
+    if let .some e := MemLegalProp.ofExpr? gt then
+      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
+        if let .some proof ← proveWithOmega? e  extraHyps bvToNatSimpCtx bvToNatSimprocs hyps then
+          g.assign proof.h
+    if let .some e := MemSubsetProp.ofExpr? gt then
+      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
+        if let .some proof ← proveWithOmega? e extraHyps  bvToNatSimpCtx bvToNatSimprocs hyps then
+          g.assign proof.h
+    if let .some e := MemSeparateProp.ofExpr? gt then
+      TacticM.withTraceNode' m!"Matched on ⊢ {e}. Proving..." do
+        if let .some proof ← proveWithOmega? e extraHyps bvToNatSimpCtx bvToNatSimprocs hyps then
+          g.assign proof.h
+  return ← g.isAssigned
+
+
+
 /-- Modify the set of hypotheses `hyp` based on the user hyp `hyp`. -/
 def mkKeepHypsOfUserHyp (g : MVarId) (set : Std.HashSet FVarId) (hyp : UserHyp) : MetaM <| Std.HashSet FVarId :=
   match hyp with 
@@ -99,42 +131,45 @@ def mkKeepHypsOfUserHyp (g : MVarId) (set : Std.HashSet FVarId) (hyp : UserHyp)
   | .expr _e => return set
 
 /--
-Given the user hypotheses, build a more focusedd MVarId that contains only those hypotheses.
-This makes `omega` focus only on those hypotheses, since omega by default crawls the entire goal state.
-
-This is arguably a workaround to having to plumb the hypotheses through the full layers of code, but it works,
-and should be a cheap solution.
+Fold over the array of `UserHyps`, build tracking `FVarId`s for the ones that we use.
+if the array is `.none`, then we keep everything. 
 -/
-def mkGoalWithOnlyUserHyps (g : MVarId) (userHyps? : Option (Array UserHyp)) : MetaM <| MVarId :=
+private def mkKeepHypsOfUserHyps (g : MVarId) (userHyps? : Option (Array UserHyp)) : MetaM <| Std.HashSet FVarId :=
   match userHyps? with
-  | none => pure g
-  | some userHyps => do
-    g.withContext do 
-      let mut keepHyps : Std.HashSet FVarId ← userHyps.foldlM
-        (init := ∅)
-        (mkKeepHypsOfUserHyp g)
-      let hyps ← g.getNondepPropHyps
-      let mut g := g
-      for h in hyps do
-        if !keepHyps.contains h then
-          g ← g.withContext <| g.clear h
-      return g
-
-def memOmega (g : MVarId) : MemOmegaM Unit := do
-    let g ← mkGoalWithOnlyUserHyps g (← readThe Context).userHyps? 
+  | none => return Std.HashSet.ofList (← g.getNondepPropHyps).toList
+  | some hyps => hyps.foldlM (init := ∅) (MemOmega.mkKeepHypsOfUserHyp g)
+
+/-- Fold over the array of `UserHyps`, build tracking `FVarId`s for the ones that we use.
+if the array is `.none`, then we keep everything. 
+This partitions `userHyps` into the ones that create `Memory.Hypothesis`, and the ones that we leave as `FVarId`s,
+which may contain memory assumptions that we cannot translate (eg. bounds like `b - a ≤ 200`.)
+-/
+def mkMemoryAndKeepHypsOfUserHyps (g : MVarId) (userHyps? : Option (Array UserHyp)) : MetaM <| Array Memory.Hypothesis × Array FVarId := do 
+  let keepHyps : Std.HashSet FVarId ← mkKeepHypsOfUserHyps g userHyps?
+  g.withContext do
+    let mut foundHyps : Array Memory.Hypothesis := #[]
+    let mut nonmem := #[]
+    for h in keepHyps do
+      let sz := foundHyps.size
+      foundHyps ← hypothesisOfExpr (Expr.fvar h) foundHyps
+      if foundHyps.size == sz then 
+        -- size did not change, so that was a non memory hyp.
+        nonmem := nonmem.push h
+    return (foundHyps, nonmem)
+
+  
+private def Bool.implies (p q : Bool) : Bool := !p || q
+
+def memOmega (g : MVarId) (userHyps? : Option (Array UserHyp)) : MemOmegaM Unit := do
     g.withContext do
-      let rawHyps ← getLocalHyps
-      let mut hyps := #[]
-      -- extract out structed values for all hyps.
-      for h in rawHyps do
-        hyps ← hypothesisOfExpr h hyps
+      let (hyps, extraHyps) ← mkMemoryAndKeepHypsOfUserHyps g userHyps?
 
       -- only enable pairwise constraints if it is enabled.
       let isPairwiseEnabled := (← readThe Context).cfg.explodePairwiseSeparate
-      hyps := hyps.filter (!·.isPairwiseSeparate || isPairwiseEnabled)
+      let hyps := hyps.filter (fun hyp => Bool.implies hyp.isPairwiseSeparate isPairwiseEnabled)
 
       -- used specialized procedure that doesn't unfold everything for the easy case.
-      if ← closeMemSideCondition g (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs hyps then
+      if ← closeMemSideCondition g (extraHyps.map .fvar) (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs hyps then
         return ()
       else
         -- in the bad case, just rip through everything.
@@ -143,7 +178,7 @@ def memOmega (g : MVarId) : MemOmegaM Unit := do
         TacticM.withTraceNode' m!"Reducion to omega" do
           try
             TacticM.traceLargeMsg m!"goal (Note: can be large)"  m!"{g}"
-            omega g (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs
+            omega g (extraHyps.map .fvar) (← readThe Context).bvToNatSimpCtx (← readThe Context).bvToNatSimprocs
             trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
           catch e =>
             trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
@@ -170,8 +205,7 @@ syntax (name := mem_omega) "mem_omega" (Lean.Parser.Tactic.config)? (memOmegaWit
 /--
 The `mem_omega!` tactic is a finishing tactic, that is a more aggressive variant of `mem_omega`.
 -/
-syntax (name := mem_omega_bang) "mem_omega!" (memOmegaWith)?  : tactic
-  
+syntax (name := mem_omega_bang) "mem_omega!" (Lean.Parser.Tactic.config)? (memOmegaWith)?  : tactic
 /--
 build a `UserHyp` from the raw syntax.
 This supports using fars, using CDot notation to partially apply theorems, and to use terms.
@@ -222,15 +256,16 @@ def evalMemOmega : Tactic := fun
     let cfg ← elabMemOmegaConfig (mkOptionalNode cfg)
     let memOmegaRules? := ← v.mapM elabMemOmegaWith
     liftMetaFinishingTactic fun g => do
-      memOmega g |>.run (← Context.init cfg memOmegaRules?)
+      memOmega g memOmegaRules? |>.run (← Context.init cfg memOmegaRules?)
   | _ => throwUnsupportedSyntax
 
 @[tactic mem_omega_bang]
 def evalMemOmegaBang : Tactic := fun
-  | `(tactic| mem_omega! $[$cfg]?) => do
+  | `(tactic| mem_omega! $[$cfg]? $[ $v:memOmegaWith ]?) => do
     let cfg ← elabMemOmegaConfig (mkOptionalNode cfg)
+    let memOmegaRules? := ← v.mapM elabMemOmegaWith
     liftMetaFinishingTactic fun g => do
-      memOmega g |>.run (← Context.init cfg.mkBang .none)
+      memOmega g memOmegaRules? |>.run (← Context.init cfg.mkBang .none)
   | _ => throwUnsupportedSyntax
 
 end MemOmega
diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean
index a4d174a1..3a466509 100644
--- a/Arm/Memory/SeparateAutomation.lean
+++ b/Arm/Memory/SeparateAutomation.lean
@@ -22,6 +22,7 @@ import Lean.Elab.Tactic.Conv
 import Lean.Elab.Tactic.Conv.Basic
 import Tactics.Simp
 import Tactics.BvOmegaBench
+import Arm.Memory.MemOmega
 import Arm.Memory.Common
 import Arm.Memory.MemOmega
 import Lean.Elab.Tactic.Location
@@ -105,6 +106,22 @@ end BvOmega
 
 namespace SeparateAutomation
 
+
+/-- User given instructions of what kind of simplification we must perform -/
+inductive Guidance.Kind
+/-- write is a subset of the write -/
+| subsetWrite
+/-- write is separate from the write (no-alias) -/
+| separateWrite
+/-- write is a susbet a known read from the same memory, where the known read is given by an optional `e : readFrom`. -/
+| subsetRead (readFrom : Option Expr)
+
+structure Guidance where
+  /-- The kind of rewrite we must perform -/
+  kind : Guidance.Kind
+  /-- The user given hypotheses. If the user has given no such guidance, then it is `.none`. -/
+  userHyps? : Option (Array MemOmega.UserHyp)
+
 structure SimpMemConfig where
   /-- number of times rewrites must be performed. -/
   rewriteFuel : Nat := 1000
@@ -194,21 +211,21 @@ def getConfig : SimpMemM SimpMemConfig := do
 #guard_msgs in #check state_value
 
 
-def SimpMemM.findOverlappingReadHypAux (hyps : Array Memory.Hypothesis) (er : ReadBytesExpr)  (hReadEq : ReadBytesEqProof) :
+def SimpMemM.findOverlappingReadHypAux (extraOmegaHyps : Array Expr) (hyps : Array Memory.Hypothesis) (er : ReadBytesExpr)  (hReadEq : ReadBytesEqProof) :
     SimpMemM <| Option (MemSubsetProof { sa := er.span, sb := hReadEq.read.span }) := do
   withTraceNode m!"{processingEmoji} ... ⊆ {hReadEq.read.span} ? " do
     -- the read we are analyzing should be a subset of the hypothesis
     let subset := (MemSubsetProp.mk er.span hReadEq.read.span)
-    let some hSubsetProof ← proveWithOmega? subset (← getBvToNatSimpCtx) (← getBvToNatSimprocs)  hyps
+    let some hSubsetProof ← proveWithOmega? subset extraOmegaHyps (← getBvToNatSimpCtx) (← getBvToNatSimprocs)  hyps
       | return none
     return some (hSubsetProof)
 
-def SimpMemM.findOverlappingReadHyp (hyps : Array Memory.Hypothesis) (er : ReadBytesExpr) :
+def SimpMemM.findOverlappingReadHyp (extraOmegaHyps : Array Expr) (hyps : Array Memory.Hypothesis) (er : ReadBytesExpr) :
     SimpMemM <| Option (Σ (hread : ReadBytesEqProof),  MemSubsetProof { sa := er.span, sb := hread.read.span }) := do
   for hyp in hyps do
     let Hypothesis.read_eq hReadEq := hyp
       | continue
-    let some subsetProof ← SimpMemM.findOverlappingReadHypAux hyps er hReadEq
+    let some subsetProof ← SimpMemM.findOverlappingReadHypAux extraOmegaHyps hyps er hReadEq
       | continue
     return some ⟨hReadEq, subsetProof⟩
   return none
@@ -242,12 +259,12 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Memory.Hypothesis) :
 
     let separate := MemSeparateProp.mk er.span ew.span
     let subset := MemSubsetProp.mk er.span ew.span
-    if let .some separateProof ← proveWithOmega? separate (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then do
+    if let .some separateProof ← proveWithOmega? separate (← (← getMainGoal).getNondepPropExprs) (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then do
       trace[simp_mem.info] "{checkEmoji} {separate}"
       let result ← MemSeparateProof.rewriteReadOfSeparatedWrite er ew separateProof e
       setChanged
       return result
-    else if let .some subsetProof ← proveWithOmega? subset (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then do
+    else if let .some subsetProof ← proveWithOmega? subset  (← (← getMainGoal).getNondepPropExprs) (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps then do
       trace[simp_mem.info] "{checkEmoji} {subset}"
       let result ← MemSubsetProof.rewriteReadOfSubsetWrite er ew subsetProof e
       setChanged
@@ -262,7 +279,7 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Memory.Hypothesis) :
     -- we can add the theorem that `(write region).read = write val`.
     -- Then this generic theory will take care of it.
     withTraceNode m!"Searching for overlapping read {er.span}." do
-      let some ⟨hReadEq, hSubsetProof⟩ ← findOverlappingReadHyp hyps er
+      let some ⟨hReadEq, hSubsetProof⟩ ← findOverlappingReadHyp (← (← getMainGoal).getNondepPropExprs) hyps er
         | SimpMemM.walkExpr e hyps
       let out ← MemSubsetProof.rewriteReadOfSubsetRead er hReadEq hSubsetProof e
       setChanged
@@ -304,20 +321,27 @@ partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Memory.Hypothesis)
     withTraceNode m!"Simplifying goal." do
         let some out ← SimpMemM.simplifyExpr gt hyps
           | return ()
-        -- Note: this could impact performance, so delete this if it turns out to be a resource hog.
         check out.eNew
         check out.eqProof
         let newGoal ←  (← getMainGoal).replaceTargetEq out.eNew out.eqProof
         replaceMainGoal [newGoal]
 end
 
+def SimpMemM.mkMemoryHypsFrom (g : MVarId) (hyps : (Array Expr))  : SimpMemM <| Array Memory.Hypothesis := do
+  g.withContext do
+    withTraceNode m!"Searching for Hypotheses" do
+      let mut foundHyps : Array Memory.Hypothesis := #[]
+      for h in hyps do
+        foundHyps ← hypothesisOfExpr h foundHyps
+      return foundHyps
 /--
 The core simplification loop.
 We look for appropriate hypotheses, and simplify (often closing) the main goal using them.
 -/
-partial def SimpMemM.simplifyLoop : SimpMemM Unit := do
+partial def SimpMemM.simpifyLoopUnsupervised : SimpMemM Unit := do
   let g ← getMainGoal
   g.withContext do
+    -- TODO: refactor to use 'findMemoryHyps'
     let hyps := (← getLocalHyps)
     let foundHyps ← withTraceNode m!"Searching for Hypotheses" do
       let mut foundHyps : Array Memory.Hypothesis := #[]
@@ -349,17 +373,122 @@ partial def SimpMemM.simplifyLoop : SimpMemM Unit := do
     if !everChanged && (← getConfig).failIfUnchanged then
         throwError "{crossEmoji} simp_mem failed to make any progress."
 
+
+
+/-- Make this an auxiliary definition because lean was taking way too long inferring this typeclass -/
+private def Meta.logWarning (msgData : Lean.MessageData) : MetaM Unit := Lean.logWarning msgData
+
+def SimpMemM.simplifySupervisedCore (g : MVarId) (e : Expr) (guidance : Guidance) : SimpMemM (SimplifyResult × Array MVarId) := do
+  withContext g do
+    let e := e.consumeMData
+    let e ← instantiateMVars e
+
+    let .some er := ReadBytesExpr.ofExpr? e
+      | throwError "{crossEmoji} expected to find 'Memory.read ...', but found {indentD e}"
+
+    match guidance.kind with
+    | .subsetWrite => do
+        -- TODO: unify code with other branch.
+        let .some ew := WriteBytesExpr.ofExpr? er.mem 
+          | throwError "{crossEmoji} expected to find read of write based on '⊂' guidance, but found read of '{er.mem}'"
+        let subset := MemSubsetProp.mk er.span ew.span
+        let (hyps, keepHyps) ← MemOmega.mkMemoryAndKeepHypsOfUserHyps g guidance.userHyps?
+        withContext g do
+          match ← proveWithOmega? subset (keepHyps.map .fvar) (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps with
+          | .some p => 
+              return (← MemSubsetProof.rewriteReadOfSubsetWrite er ew p e, #[])
+          | .none => do 
+             Meta.logWarning m!"simp_mem: Unable to prove subset {subset}, creating user obligation."
+             let (p, g') ← mkProofGoalForOmega subset
+             return (← MemSubsetProof.rewriteReadOfSubsetWrite er ew p e, #[g'])
+    | .separateWrite => 
+        -- TODO: unify code with other branch.
+        let .some ew := WriteBytesExpr.ofExpr? er.mem 
+          | throwError "{crossEmoji} expected to find read of write based on '⟂' guidance, but found read of '{er.mem}'"
+        let separate := MemSeparateProp.mk er.span ew.span
+        let (hyps, keepHyps) ← MemOmega.mkMemoryAndKeepHypsOfUserHyps g guidance.userHyps?
+          /- TODO: replace the use of throwError with telling the user to prove the goals if enabled. -/
+        withContext g do
+            match ← proveWithOmega? separate (keepHyps.map .fvar) (← getBvToNatSimpCtx) (← getBvToNatSimprocs) hyps with
+            | .some p =>
+              return (← MemSeparateProof.rewriteReadOfSeparatedWrite er ew p e, #[])
+            | .none => do
+              Meta.logWarning m!"simp_mem: Unable to prove separate {separate}, creating user obligation."
+              let (p, g') ← mkProofGoalForOmega separate
+              return (← MemSeparateProof.rewriteReadOfSeparatedWrite er ew p e, #[g'])
+    | .subsetRead hread? => do
+        -- If the user has provided guidance hypotheses, add the user hypothesis to this list.
+        -- If the user has not provided guidance hypotheses, then we don't filter the list, so 
+        -- we don't add it
+        let userHyps? : Option (Array MemOmega.UserHyp) := 
+          match (guidance.userHyps?, hread?) with
+          | (.none, _) => .none -- nothing to filter, just keep everything.
+          | (.some userHyps, .none) => .some userHyps
+          -- -- User wants filtering, and wants this read hypothesis to be used.
+          -- -- Add it into the set of user provided hypotheses.
+          |  (.some userHyps, .some readHyp) => .some <| userHyps.push (MemOmega.UserHyp.ofExpr readHyp)
+        let (hyps, keepHyps) ← MemOmega.mkMemoryAndKeepHypsOfUserHyps g userHyps?
+        match hread? with
+        | .none => do 
+          /-
+          User hasn't given us a read, so find a read. No recovery possible,
+          Because the expression we want to rewrite into depends on knowing what the read was.
+          -/
+          let .some ⟨hreadEq, proof⟩ ← findOverlappingReadHyp (keepHyps.map .fvar) hyps er
+            | throwError "{crossEmoji} unable to find overlapping read for {er}"
+          return (←  MemSubsetProof.rewriteReadOfSubsetRead er hreadEq proof e, #[])
+        | .some hyp => do
+          /- 
+          User has given us a read, prove that it works.
+          TODO: replace the use of throwError with telling the user to prove the goals if enabled.
+          -/
+          let .some hReadEq := (← ReadBytesEqProof.ofExpr? hyp (← inferType hyp)).get? 0
+            | throwError "{crossEmoji} expected user provided read hypohesis {hyp} to be a read"
+          let subset := (MemSubsetProp.mk er.span hReadEq.read.span)
+          match ← proveWithOmega? subset (keepHyps.map .fvar) (← getBvToNatSimpCtx) (← getBvToNatSimprocs)  hyps with
+          | .some p => do 
+              let result ← MemSubsetProof.rewriteReadOfSubsetRead er hReadEq p e
+              return (result, #[])
+          | .none => do
+              Meta.logWarning m!"simp_mem: Unable to prove read subset {subset}, creating user obligation."
+              let (p, g') ← mkProofGoalForOmega subset
+              let result ← MemSubsetProof.rewriteReadOfSubsetRead er hReadEq p e
+              return (result, #[g'])
+
+
+partial def SimpMemM.simplifySupervised (g : MVarId) (guidances : Array Guidance) : SimpMemM Unit := do
+  let mut g := g
+  let mut sideGoals : Array MVarId := #[]
+  for guidance in guidances do
+    let (outProof, newGoals) ← simplifySupervisedCore g (← g.getType) guidance
+    sideGoals := sideGoals.append newGoals
+    check outProof.eqProof
+    g ←  g.replaceTargetEq outProof.eNew outProof.eqProof
+  appendGoals sideGoals.toList
+  return ()
+
+partial def SimpMemM.simplifySupervisedConv (guidances : Array Guidance) : SimpMemM Unit := do
+  withMainContext do
+    let mut gs := #[]
+    for guidance in guidances do
+      let lhs ← Conv.getLhs
+      let (result, newGoals) ← withMainContext do SimpMemM.simplifySupervisedCore (← getMainGoal) lhs guidance
+      withMainContext do Conv.updateLhs result.eNew result.eqProof
+      gs := gs.append newGoals
+    appendGoals gs.toList -- append oblgations.
+
 /--
 Given a collection of facts, try prove `False` using the omega algorithm,
 and close the goal using that.
 -/
-def simpMem (cfg : SimpMemConfig := {}) : TacticM Unit := do
-  -- evalTactic (← `(simp (config := {failIfUnchanged := false}) only [memory_rules]))
-  SimpMemM.run SimpMemM.simplifyLoop cfg
+def simpMemUnsupervisedTac (cfg : SimpMemConfig := {}) : TacticM Unit := do
+    SimpMemM.run SimpMemM.simpifyLoopUnsupervised  cfg
 
+def simpMemSupervisedTac (cfg : SimpMemConfig := {}) (guidances: Array Guidance) : TacticM Unit := do
+    SimpMemM.run (SimpMemM.simplifySupervised (← getMainGoal) guidances) cfg 
 
-/-- The `simp_mem` tactic, for simplifying away statements about memory. -/
-def simpMemTactic (cfg : SimpMemConfig) : TacticM Unit := simpMem cfg
+def simpMemSupervisedConvTac (cfg : SimpMemConfig := {}) (guidances: Array Guidance) : TacticM Unit := do
+    SimpMemM.run (SimpMemM.simplifySupervisedConv  guidances) cfg 
 
 end SeparateAutomation
 
@@ -368,22 +497,29 @@ Allow elaboration of `SimpMemConfig` arguments to tactics.
 -/
 declare_config_elab elabSimpMemConfig SeparateAutomation.SimpMemConfig
 
+namespace SimpMem.Syntax
+open MemOmega
 
-/-
-This allows users to supply a list of hypotheses that simp_mem should use.
-Modeled after `rwRule`.
--/
-syntax simpMemRule := term
 
 /-
 The kind of simplification that must be performed. If we are told
 that we must simplify a separation, a subset, or a read of a write,
 we perform this kind of simplification.
 -/
-syntax simpMemSimplificationKind := "⟂" <|> "⊂w" <|> "⊂r" (term)?
+syntax guidanceKindSeparate := &"sep" <|> &"⟂" 
+syntax guidanceKindSubset := &"sub" <|> &"⊂" <|> &"⊆"-- &"⊂"
+syntax guidanceKindSubsetRead := &"r" -- &"⊂"
+syntax guidanceKind := guidanceKindSeparate <|> guidanceKindSubset (guidanceKindSubsetRead ("at" term)?)? 
+
+/--
+User driven guidance for `simp_mem`, which is of the form `⟂` | `⊂` | `⊂ r hyp?`
+-/
+syntax guidance := guidanceKind (memOmegaWith)?
 
+end SimpMem.Syntax
 
-open Lean.Parser.Tactic in
+
+open Lean.Parser.Tactic SimpMem.Syntax in
 /--
 The simp_mem tactic allows simplifying expressions of the form `Memory.read_bytes rbase rn (mem')`.
 `simp_mem` attempts to discover the result of the expression by various heuristics,
@@ -414,11 +550,74 @@ which hypotheses are at play. `simp_mem` can be controlled along multiple axes:
    + `simp_mem at h₁, h₂, ⊢`
 
 -/
-syntax (name := simp_mem) "simp_mem" (Lean.Parser.Tactic.config)? (simpMemSimplificationKind)? ("using" "[" withoutPosition(simpMemRule,*,?) "]")? (location)? : tactic
-
-@[tactic simp_mem]
+syntax (name := simpMem) "simp_mem" (Lean.Parser.Tactic.config)? guidance,*  : tactic
+
+
+open Lean.Parser.Tactic SimpMem.Syntax in
+/-- Executes the given conv block without converting regular goal into a `conv` goal. -/
+syntax (name := convSimpMem) "simp_mem" (Lean.Parser.Tactic.config)? guidance,+ : conv
+
+open SimpMem.Syntax MemOmega in
+def elabGuidanceKind (stx : TSyntax `SimpMem.Syntax.guidanceKind) : TacticM (SeparateAutomation.Guidance.Kind) := do
+  match stx with
+  | `(guidanceKind| $_:guidanceKindSeparate) => do
+      return SeparateAutomation.Guidance.Kind.separateWrite
+  | `(guidanceKind| $_:guidanceKindSubset $_:guidanceKindSubsetRead) => do
+      return SeparateAutomation.Guidance.Kind.subsetRead .none
+  | `(guidanceKind| $_:guidanceKindSubset $_:guidanceKindSubsetRead at $t:term) => do
+     withMainContext do
+       /-
+       Adapted from Lean.Elab.Tactic.Rw.WithRWRulesSeq,
+       Lean.Elab.Tactic.Simp.resolveSimpIdTheorem,
+       Lean.Elab.Tactic.Simp.addSimpTheorem 
+       -/
+       let te : Expr ← do
+         if let .some fvarId ← optional <| getFVarId t then
+           pure <| Expr.fvar fvarId
+         else 
+           let e ← Term.elabTerm t none
+           Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
+           let e ← instantiateMVars e
+           let e := e.eta
+           if e.hasMVar then
+             throwErrorAt t "found metavariables when elaborating user guidance '{t}', giving up."
+           pure e
+        return SeparateAutomation.Guidance.Kind.subsetRead <| some te
+  | `(guidanceKind| $_:guidanceKindSubset) => do
+      return SeparateAutomation.Guidance.Kind.subsetWrite
+  | _ => throwUnsupportedSyntax 
+
+--   trace[simp_mem.info] m!"raw syntax: {toString stx}"
+--   throwError "unknown simp_mem guidance kind: {stx}"
+
+open SimpMem.Syntax MemOmega in
+def elabGuidance : TSyntax `SimpMem.Syntax.guidance → TacticM (SeparateAutomation.Guidance) 
+| `(guidance| $kindStx:guidanceKind $[ $userHypsStx:memOmegaWith ]?) => do
+    let kind ← elabGuidanceKind kindStx
+    let userHyps? ← userHypsStx.mapM MemOmega.elabMemOmegaWith
+    return { kind, userHyps? }
+| _ => throwUnsupportedSyntax
+
+
+@[tactic simpMem]
 def evalSimpMem : Tactic := fun
-  | `(tactic| simp_mem $[$cfg]?) => do
+  -- | `(tactic| simp_mem $[$cfg]?) => do
+  --   let cfg ← elabSimpMemConfig (mkOptionalNode cfg)
+  --   SeparateAutomation.simpMemUnsupervisedTac cfg 
+  | `(tactic| simp_mem $[$cfg]? $[ $guidancesStx:guidance ],* ) => do
     let cfg ← elabSimpMemConfig (mkOptionalNode cfg)
-    SeparateAutomation.simpMemTactic cfg
+    let guidances ← guidancesStx.mapM elabGuidance
+    if guidances.isEmpty then
+      SeparateAutomation.simpMemUnsupervisedTac cfg 
+    else 
+      SeparateAutomation.simpMemSupervisedTac cfg  guidances
+  | _ => throwUnsupportedSyntax
+
+
+@[tactic convSimpMem]
+def evalConvSimpMem : Tactic := fun
+  | `(conv| simp_mem $[$cfg]? $[ $guidancesStx:guidance ],* ) => do
+      let cfg ← elabSimpMemConfig (mkOptionalNode cfg)
+      let guidances ← guidancesStx.mapM elabGuidance
+      SeparateAutomation.simpMemSupervisedConvTac cfg  guidances
   | _ => throwUnsupportedSyntax
diff --git a/Proofs/AES-GCM/GCMGmultV8Sym.lean b/Proofs/AES-GCM/GCMGmultV8Sym.lean
index 1c707de3..a6f5dcf5 100644
--- a/Proofs/AES-GCM/GCMGmultV8Sym.lean
+++ b/Proofs/AES-GCM/GCMGmultV8Sym.lean
@@ -149,7 +149,7 @@ example :
 set_option pp.deepTerms false in
 set_option pp.deepTerms.threshold 50 in
 -- set_option trace.simp_mem.info true in
-theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
+#time theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
     (h_s0_program : s0.program = gcm_gmult_v8_program)
     (h_s0_err : read_err s0 = .None)
     (h_s0_pc : read_pc s0 = gcm_gmult_v8_program.min)
@@ -206,15 +206,18 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
   · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp] at *
     sym_aggregate
   · intro n addr h_separate
-    simp_mem
-    -- Aggregate the memory (non)effects.
-    simp only [*]
+    conv =>
+      lhs
+      simp_mem sep with [h_separate]
   · clear_named [h_s, stepi_]
     clear s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 s16 s17 s18 s19 s20 s21 s22 s23 s24 s25 s26
     -- Simplifying the LHS
     have h_HTable_low :
       Memory.read_bytes 16 (r (StateField.GPR 1#5) s0) s0.mem = HTable.extractLsb' 0 128 := by
       -- (FIXME @bollu) use `simp_mem` instead of the rw below.
+      -- conv => 
+      --   lhs
+      --   simp_mem sub r 
       rw [@Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset'
            32 (r (StateField.GPR 1#5) s0) HTable (r (StateField.GPR 1#5) s0) 16 _ h_HTable.symm]
       · simp only [Nat.reduceMul, BitVec.extractLsBytes, Nat.sub_self, Nat.zero_mul]
@@ -222,6 +225,9 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
     have h_HTable_high :
       (Memory.read_bytes 16 (r (StateField.GPR 1#5) s0 + 16#64) s0.mem) = HTable.extractLsb' 128 128 := by
       -- (FIXME @bollu) use `simp_mem` instead of the rw below.
+      -- conv => 
+      --   lhs
+      --   simp_mem sub r 
       rw [@Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset'
           32 (r (StateField.GPR 1#5) s0) HTable (r (StateField.GPR 1#5) s0 + 16#64) 16 _ h_HTable.symm]
       repeat sorry
diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
index b5b0f0dd..c288d22b 100644
--- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean
+++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
@@ -442,7 +442,6 @@ section PartialCorrectness
 -- set_option skip_proof.skip true in
 -- set_option trace.profiler true in
 -- set_option profiler true in
-#time set_option maxHeartbeats 0 in
 theorem Memcpy.extracted_2 (s0 si : ArmState)
   (h_si_x0_nonzero : si.x0 ≠ 0)
   (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64)))
@@ -466,21 +465,11 @@ theorem Memcpy.extracted_2 (s0 si : ArmState)
       (Memory.write_bytes 16 (s0.x2 + 0x10#64 * (s0.x0 - si.x0))
         (Memory.read_bytes 16 (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) si.mem) si.mem) =
     Memory.read_bytes n addr s0.mem := by
-  have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by 
-    mem_omega with [h_assert_1, h_pre_1]
-  rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate']
-  · rw [h_assert_6]
-    skip_proof mem_omega with [h_assert_1, h_pre_1, hsep]
-  · -- @bollu: TODO: figure out why this is so slow!/
-    apply mem_separate'.symm
-    apply mem_separate'.of_subset'_of_subset' hsep
-    · apply mem_subset'.of_omega
-      skip_proof refine ⟨?_, ?_, ?_, ?_⟩
-      · mem_omega with [h_si_x0_nonzero, h_assert_1, h_pre_1] -- TODO: add support for patterns like *, -<hyp1>, ... -<hypN>
-      · mem_omega with [h_si_x0_nonzero, h_assert_1, h_pre_1]
-      · mem_omega with [h_si_x0_nonzero, h_assert_1, h_pre_1]
-      · mem_omega with [h_si_x0_nonzero, h_assert_1, h_pre_1] -- , hsep] -- adding `hsep` makes this way slower.
-    · apply mem_subset'_refl hsep.hb
+  conv =>
+    lhs
+    simp_mem sep with [h_si_x0_nonzero, h_assert_1, h_pre_1, h_assert_1, hsep]
+  rw [h_assert_6]
+  mem_omega with [hsep, h_pre_1, h_assert_1, h_assert_4]
 
 -- set_option skip_proof.skip true in
 set_option maxHeartbeats 0 in
diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
index eea843b4..002dde0d 100644
--- a/Proofs/Experiments/MemoryAliasing.lean
+++ b/Proofs/Experiments/MemoryAliasing.lean
@@ -170,6 +170,7 @@ set_option linter.all false in
   mem_omega
 
 set_option linter.all false in
+set_option trace.simp_mem.info true in
 #time theorem mem_separate_11  (h : mem_separate' a 100 b 100)
   (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1)
   (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1) (h' : a < b + 1)
@@ -208,9 +209,8 @@ section HypothesisSelectors
 set_option linter.all false in
 set_option trace.simp_mem.info true in
 /--
-info: [simp_mem.info] ⚙️ Processing 'a' : 'Nat'
+info: [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1'
 [simp_mem.info] ⚙️ Processing 'h'' : 'a ≤ 100'
-[simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1'
 [simp_mem.info] ⚙️ Matching on ⊢ a ≤ a + 1
 [simp_mem.info] Adding omega facts from hypotheses
 [simp_mem.info] Reducion to omega
@@ -226,13 +226,13 @@ info: [simp_mem.info] ⚙️ Processing 'a' : 'Nat'
   mem_omega  -- by default, process all hyps
 
 /--
-info: [simp_mem.info] ⚙️ Processing 'a' : 'Nat'
-[simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1'
+info: [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1'
 [simp_mem.info] ⚙️ Matching on ⊢ a ≤ a + 1
 [simp_mem.info] Adding omega facts from hypotheses
 [simp_mem.info] Reducion to omega
   [simp_mem.info] goal (Note: can be large) (NOTE: can be large)
     [simp_mem.info] a : Nat
+        h' : a ≤ 100
         hab : a ≤ a + 1
         ⊢ a ≤ a + 1
   [simp_mem.info] ✅️ `omega` succeeded.
@@ -247,18 +247,18 @@ example (h' : a ≤ 100) (hab : a ≤ a + 1) : a ≤ a + 1 := by
 warning: unused variable `hab`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 ---
-info: [simp_mem.info] ⚙️ Processing 'a' : 'Nat'
-[simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1'
+info: [simp_mem.info] ⚙️ Processing 'hab' : 'a ≤ a + 1'
 [simp_mem.info] ⚙️ Matching on ⊢ a ≤ a + 1
 [simp_mem.info] Adding omega facts from hypotheses
 [simp_mem.info] Reducion to omega
   [simp_mem.info] goal (Note: can be large) (NOTE: can be large)
     [simp_mem.info] a : Nat
+        h' : a ≤ 100
         hab : a ≤ a + 1
         ⊢ a ≤ a + 1
   [simp_mem.info] ✅️ `omega` succeeded.
 -/
-#guard_msgs in
+#guard_msgs in -- TODO: fix this, we shouldn't process h!
 set_option trace.simp_mem.info true in
 example (h' : a ≤ 100) (hab : a ≤ a + 1) : a ≤ a + 1 := by
   mem_omega with [*, -h'] -- correctly exclude h' and include hab, so processing should not mention h'.
@@ -267,6 +267,7 @@ example (h' : a ≤ 100) (hab : a ≤ a + 1) : a ≤ a + 1 := by
 end HypothesisSelectors
 
 
+#time
 theorem mem_automation_test_1
   (h_s0_src_dest_separate : mem_separate' src_addr  16 dest_addr 16) :
   read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) =
@@ -276,11 +277,29 @@ theorem mem_automation_test_1
   rfl
 
 
-  -- rfl
+theorem mem_automation_test_1_conv_all_hyps
+  (h_s0_src_dest_separate : mem_separate' src_addr  16 dest_addr 16) :
+  read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) =
+  read_mem_bytes 16 src_addr s0 := by
+  simp only [memory_rules]
+  conv =>
+    lhs
+    simp_mem sep with [*]
+
+#time
+theorem mem_automation_test_1_conv_focused_hyp
+  (h_s0_src_dest_separate : mem_separate' src_addr  16 dest_addr 16) :
+  read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) =
+  read_mem_bytes 16 src_addr s0 := by
+  simp only [memory_rules]
+  conv =>
+    lhs
+    simp_mem sep with [h_s0_src_dest_separate]
 
 /-- info: 'mem_automation_test_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_1
 
+#time
 theorem mem_automation_test_2
   (h_n0 : n0 ≠ 0)
   (h_no_wrap_src_region : mem_legal' src_addr (n0 <<< 4))
@@ -295,9 +314,40 @@ theorem mem_automation_test_2
   rfl
 
 
+#time
+theorem mem_automation_test_2_conv
+  (h_n0 : n0 ≠ 0)
+  (h_no_wrap_src_region : mem_legal' src_addr (n0 <<< 4))
+  (h_no_wrap_dest_region : mem_legal' dest_addr (n0 <<< 4))
+  (h_s0_src_dest_separate :
+    mem_separate' src_addr  (n0 <<< 4)
+                  dest_addr (n0 <<< 4)) :
+  read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) =
+  read_mem_bytes 16 src_addr s0 := by
+  simp only [memory_rules]
+  conv =>
+    lhs 
+    simp_mem sep with [*]
+
+theorem mem_automation_test_2_conv_focus
+  (h_n0 : n0 ≠ 0)
+  (h_no_wrap_src_region : mem_legal' src_addr (n0 <<< 4))
+  (h_no_wrap_dest_region : mem_legal' dest_addr (n0 <<< 4))
+  (h_s0_src_dest_separate :
+    mem_separate' src_addr  (n0 <<< 4)
+                  dest_addr (n0 <<< 4)) :
+  read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) =
+  read_mem_bytes 16 src_addr s0 := by
+  simp only [memory_rules]
+  conv =>
+    lhs 
+    simp_mem sep with [h_s0_src_dest_separate]
+
+
 /-- info: 'mem_automation_test_2' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_2
 
+#time
 /-- reading from a region `[src_addr+1..10] ⊆ [src_addr..16]` with an
 interleaved write `[ignore_addr..ignore_addr+ignore_n)`
 -/
@@ -312,11 +362,26 @@ theorem mem_automation_test_3
   simp_mem
   rfl
 
-
+#time
+/-- reading from a region `[src_addr+1..10] ⊆ [src_addr..16]` with an
+interleaved write `[ignore_addr..ignore_addr+ignore_n)`
+-/
+theorem mem_automation_test_3_conv
+  (h_no_wrap_src_region : mem_legal' src_addr 16)
+  (h_s0_src_ignore_disjoint :
+    mem_separate' src_addr  16
+                  ignore_addr ignore_n) :
+  read_mem_bytes 10 (src_addr + 1) (write_mem_bytes ignore_n ignore_addr blah s0) =
+   read_mem_bytes 10 (src_addr + 1) s0 := by
+  simp only [memory_rules]
+  conv =>
+    lhs
+    simp_mem sep with [h_s0_src_ignore_disjoint]
 
 /-- info: 'mem_automation_test_3' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_3
 
+#time
 /-- TODO: make simp_mem repeat on change. -/
 theorem mem_automation_test_4
   (h_no_wrap_src_region : mem_legal' src_addr 48)
@@ -332,12 +397,49 @@ theorem mem_automation_test_4
   congr 1
   bv_omega_bench -- TODO: address normalization.
 
+#time
+/-- TODO: make simp_mem repeat on change. -/
+theorem mem_automation_test_4_conv
+  (h_no_wrap_src_region : mem_legal' src_addr 48)
+  (h_s0_src_ignore_disjoint :
+    mem_separate' src_addr  48
+                  ignore_addr ignore_n) :
+  read_mem_bytes 10 (1 + src_addr)
+    (write_mem_bytes ignore_n ignore_addr blah
+      (write_mem_bytes 48 src_addr val s0)) =
+   val.extractLsBytes 1 10 := by
+  simp only [memory_rules]
+  conv =>
+    lhs
+    simp_mem sep with [*], sub with [*]
+  congr 1
+  bv_omega_bench -- TODO: address normalization.
+
 /-- info: 'mem_automation_test_4' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms mem_automation_test_4
 
+#time
+/-- TODO: make simp_mem repeat on change. -/
+theorem mem_automation_test_4_conv_focused
+  (h_no_wrap_src_region : mem_legal' src_addr 48)
+  (h_s0_src_ignore_disjoint :
+    mem_separate' src_addr  48
+                  ignore_addr ignore_n) :
+  read_mem_bytes 10 (1 + src_addr)
+    (write_mem_bytes ignore_n ignore_addr blah
+      (write_mem_bytes 48 src_addr val s0)) =
+   val.extractLsBytes 1 10 := by
+  simp only [memory_rules]
+  conv =>
+    lhs
+    simp_mem sep with [h_no_wrap_src_region, h_s0_src_ignore_disjoint], sub with [*]
+  congr 1
+  bv_omega_bench -- TODO: address normalization.
+
 
 namespace ReadOverlappingRead
 
+#time
 /-- A read overlapping with another read. -/
 theorem overlapping_read_test_1 {out : BitVec (16 * 8)}
     (hlegal : mem_legal' src_addr 16)
@@ -347,9 +449,34 @@ theorem overlapping_read_test_1 {out : BitVec (16 * 8)}
   simp_mem
   simp only [Nat.reduceMul, Nat.sub_self, BitVec.extractLsBytes_eq_self, BitVec.cast_eq]
 
+
+#time
+/-- A read overlapping with another read. -/
+theorem overlapping_read_test_1_conv {out : BitVec (16 * 8)}
+    (hlegal : mem_legal' src_addr 16)
+    (h : read_mem_bytes 16 src_addr s = out) :
+    read_mem_bytes 16 src_addr s = out := by
+  simp only [memory_rules] at h ⊢
+  conv =>
+    lhs
+    simp_mem ⊆r at h with [*]
+  simp only [Nat.reduceMul, Nat.sub_self, BitVec.extractLsBytes_eq_self, BitVec.cast_eq]
+
+/-- A read overlapping with another read. -/
+theorem overlapping_read_test_1_conv_search_read {out : BitVec (16 * 8)}
+    (hlegal : mem_legal' src_addr 16)
+    (h : read_mem_bytes 16 src_addr s = out) :
+    read_mem_bytes 16 src_addr s = out := by
+  simp only [memory_rules] at h ⊢
+  conv =>
+    lhs
+    simp_mem ⊆r with [*]
+  simp only [Nat.reduceMul, Nat.sub_self, BitVec.extractLsBytes_eq_self, BitVec.cast_eq]
+
 /-- info: 'ReadOverlappingRead.overlapping_read_test_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
 #guard_msgs in #print axioms overlapping_read_test_1
 
+#time
 /-- A read overlapping with another read. -/
 theorem overlapping_read_test_2 {out : BitVec (16 * 8)}
     (hlegal : mem_legal' src_addr 16)
@@ -365,6 +492,20 @@ info: 'ReadOverlappingRead.overlapping_read_test_2' depends on axioms: [propext,
 -/
 #guard_msgs in #print axioms overlapping_read_test_2
 
+#time
+/-- A read overlapping with another read. -/
+theorem overlapping_read_test_2_conv {out : BitVec (16 * 8)}
+    (hlegal : mem_legal' src_addr 16)
+    (h : read_mem_bytes 16 src_addr s = out) :
+    read_mem_bytes 10 (src_addr + 6) s = out.extractLsBytes 6 10 := by
+  simp only [memory_rules] at h ⊢
+  conv =>
+    lhs
+    simp_mem ⊆r at h with [*]
+  · congr
+    -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6
+    bv_omega_bench
+
 /-- A read in the goal state overlaps with a read in the
 left hand side of the hypotheis `h`.
 -/
@@ -497,6 +638,22 @@ theorem test_quantified_app_2 {val : BitVec (16 * 8)}
 end ExprVisitor
 -/
 
+
+namespace SimpMemConv
+
+#time
+theorem irrelvant_hyps
+  (h_irrelevant: mem_subset' src_addr 10 src_addr 30)
+  (h_s0_src_dest_separate : mem_separate' src_addr  16 dest_addr 16) :
+  read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) =
+  read_mem_bytes 16 src_addr s0 := by
+  simp only [memory_rules]
+  conv => 
+    lhs
+    simp_mem sep with [h_s0_src_dest_separate]
+  -- rfl
+end SimpMemConv
+
 namespace MathProperties
 
 /-
diff --git a/Proofs/Experiments/SHA512MemoryAliasing.lean b/Proofs/Experiments/SHA512MemoryAliasing.lean
index 4d9c2657..12841f3a 100644
--- a/Proofs/Experiments/SHA512MemoryAliasing.lean
+++ b/Proofs/Experiments/SHA512MemoryAliasing.lean
@@ -122,7 +122,7 @@ work for `16#64 + ktbl_addr`?
 -/
 -- set_option trace.simp_mem true in
 -- set_option trace.simp_mem.info true in
-theorem sha512_block_armv8_loop_sym_ktbl_access (s1 : ArmState)
+#time theorem sha512_block_armv8_loop_sym_ktbl_access (s1 : ArmState)
   (_h_s1_err : read_err s1 = StateError.None)
   (_h_s1_sp_aligned : CheckSPAlignment s1)
   (h_s1_pc : read_pc s1 = 0x126500#64)
@@ -150,7 +150,9 @@ theorem sha512_block_armv8_loop_sym_ktbl_access (s1 : ArmState)
   -- @bollu: we need 'hSHA2_k512_length' to allow omega to reason about
   -- SHA2.k_512.length, which is otherwise treated as an unintepreted constant.
   have hSHA2_k512_length : SHA2.k_512.length = 80 := rfl
-  simp_mem -- It should fail if it makes no progress. Also, make small examples that demonstrate such failures.
+  conv =>
+    lhs
+    simp_mem ⊂ r at h_s1_ktbl with [] -- It should fail if it makes no progress. Also, make small examples that demonstrate such failures.
   rfl
 
 /--
diff --git a/Proofs/SHA512/SHA512Prelude.lean b/Proofs/SHA512/SHA512Prelude.lean
index ed1d1383..27eaaa1a 100644
--- a/Proofs/SHA512/SHA512Prelude.lean
+++ b/Proofs/SHA512/SHA512Prelude.lean
@@ -115,7 +115,7 @@ in this proof. This will hopefully go down, once we optimize `sym_aggregate`.
 -/
 set_option maxRecDepth 8000 in
 set_option linter.unusedVariables false in
-theorem sha512_block_armv8_prelude (s0 sf : ArmState)
+#time theorem sha512_block_armv8_prelude (s0 sf : ArmState)
   -- We fix the number of blocks to hash to 1.
   (h_N : N = 1#64)
   (h_s0_init : precondition 0x1264c0#64 N SP CtxBase InputBase s0)
@@ -194,7 +194,11 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState)
   · constructor
     · -- (TODO @bollu) Think about whether `simp_mem` should be powerful enough to solve this goal.
       -- Also, `mem_omega` name suggestion from Alex for the already souped up `simp_mem`.
-      simp_mem
+      -- simp_mem
+      conv =>
+        lhs
+        simp_mem sep with [h_s0_mem_sep, h_s0_sp]
+        simp_mem sub r with [h_s0_ctx, h_s0_ctx_base, h_s0_mem_sep]
       simp only [h_s0_ctx_base, Nat.sub_self, minimal_theory, bitvec_rules]
     · constructor
       · -- (FIXME @bollu) simp_mem doesn't make progress here. :-(
@@ -214,7 +218,9 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState)
   · intro n addr h
     simp only [←h_s0_sp] at h
     clear_named [h_, stepi]
-    simp_mem
+    conv =>
+      lhs
+      simp_mem sep with [h]
     /-
     (NOTE @bollu): Without the `clear_named...` above, we run into the following
     error(s):
@@ -227,7 +233,11 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState)
     `(deterministic) timeout at elaborator, maximum number of heartbeats
      (200000) has been reached...`
     -/
-    rfl
   done
 
+/--
+info: 'SHA512.sha512_block_armv8_prelude' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]
+-/
+#guard_msgs in #print axioms sha512_block_armv8_prelude 
+
 end SHA512
diff --git a/Tactics/BvOmegaBench.lean b/Tactics/BvOmegaBench.lean
index 4224998f..c197c13b 100644
--- a/Tactics/BvOmegaBench.lean
+++ b/Tactics/BvOmegaBench.lean
@@ -49,42 +49,41 @@ Code adapted from:
 - https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Simp.lean#L406
 - https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Tactic/Omega/Frontend.lean#L685
 -/
-def run (g : MVarId)  (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs) : MetaM Unit := do
+def run (g : MVarId) (hyps : Array Expr) (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array Simp.Simprocs) : MetaM Unit := do
   let minMs ← getBvOmegaBenchMinMs
   let goalStr ← ppGoal g
   let startTime ← IO.monoMsNow
   let filePath ← getBvOmegaBenchFilePath
+  let mut g := g
+  let mut hypFVars : Array FVarId := hyps.filterMap (fun e => if e.isFVar then some e.fvarId! else none)
   try
-      g.withContext do
-        let nonDepHyps ← g.getNondepPropHyps
-        let mut g := g
-
-        try
-          let (result?, _stats) ← 
-            simpGoal g bvToNatSimpCtx bvToNatSimprocs
-              (simplifyTarget := true) (discharge? := .none) nonDepHyps
-          let .some (_, g') := result? | return ()
-          g := g'
-        catch e => 
-          trace[simp_mem.info] "in BvOmega, ran `simp only [bv_toNat]` and got error: {indentD e.toMessageData}"
-          throw e
-
-        g.withContext do 
-          let some g ← g.falseOrByContra | return ()
-          g.withContext do
-            let hyps := (← getLocalHyps).toList
-            omega hyps g {}
-            let endTime ← IO.monoMsNow
-            let delta := endTime - startTime
-            if (← getBvOmegaBenchIsEnabled) && delta ≥ minMs then 
-              IO.FS.withFile filePath IO.FS.Mode.append fun h => do
-                  h.putStrLn "\n---\n"
-                  h.putStrLn s!"goal"
-                  h.putStrLn goalStr.pretty
-                  h.putStrLn s!"endgoal"
-                  h.putStrLn s!"time"
-                  h.putStrLn s!"{delta}"
-                  h.putStrLn s!"endtime"
+     /- Wow, this is gross. I need to filter out the fvars, and keep track of which ones I use for simplification. -/
+     try
+       let (result?, _stats) ← g.withContext <| simpGoal g bvToNatSimpCtx bvToNatSimprocs (simplifyTarget := true) (discharge? := .none) hypFVars
+       let .some (hypFVars', g') := result? | return ()
+       g := g'
+       let hypsOldRetained ← g.withContext <| pure (← getLCtx).getFVarIds
+       let hypsOldRetained := hypsOldRetained.filter (fun fvar => hypFVars.contains fvar)
+       -- hypFVars := hypFVars'
+     catch e => 
+       trace[simp_mem.info] "in BvOmega, ran `simp only [bv_toNat]` and got error: {indentD e.toMessageData}"
+       throw e
+     let some g' ← g.withContext <| g.falseOrByContra | return ()
+     g := g'
+     g.withContext do
+       -- omega (hypExprs ++ hypFVars.map (Expr.fvar)).toList g {}
+       omega (← getLocalHyps).toList g {}
+       let endTime ← IO.monoMsNow
+       let delta := endTime - startTime
+       if (← getBvOmegaBenchIsEnabled) && delta ≥ minMs then 
+         IO.FS.withFile filePath IO.FS.Mode.append fun h => do
+           h.putStrLn "\n---\n"
+           h.putStrLn s!"goal"
+           h.putStrLn goalStr.pretty
+           h.putStrLn s!"endgoal"
+           h.putStrLn s!"time"
+           h.putStrLn s!"{delta}"
+           h.putStrLn s!"endtime"
   catch e =>
     let endTime ← IO.monoMsNow
     let delta := endTime - startTime
@@ -105,7 +104,8 @@ def run (g : MVarId)  (bvToNatSimpCtx : Simp.Context) (bvToNatSimprocs : Array S
 /-- Build the default simp context (bv_toNat) and run omega -/
 def runWithDefaultSimpContext (g : MVarId) : MetaM Unit := do
   let (bvToNatSimpCtx, bvToNatSimprocs) ← bvOmegaSimpCtx
-  run g bvToNatSimpCtx bvToNatSimprocs
+  g.withContext do
+    run g ((← g.getNondepPropHyps).map Expr.fvar) bvToNatSimpCtx bvToNatSimprocs
 
 end BvOmegaBench