From f7534ae58ae0684776d167cafb08d267a565e521 Mon Sep 17 00:00:00 2001
From: Siddharth Bhat <siddu.druid@gmail.com>
Date: Tue, 15 Oct 2024 14:40:25 -0500
Subject: [PATCH] feat: add new syntax for guided simp_mem

chore: add subgoals for targets we could not close automatically

chore: iron out bugs, bench perf on small examples

chore: conv mode interacts poorly with clear :(

chore: checkpoint

Revert "chore: checkpoint"

This reverts commit 26f7b852feb297c6d11cc6bf17e4c0ced9ee3e96.

Revert "chore: conv mode interacts poorly with clear :("

This reverts commit 472a9ae653524a7afd478c1bb4ac809b50b07b9e.

chore: add TDD test case

chore: plumb through state for omega hypothesis filtering

chore: start plumbing in infra to filter out user hyps

chore: cleanup API to build keep hyps

feat: working conv + simp_mem with goal state filtering

chore: updateSHA512Prelude to use simp_mem with targeted rewrite

chore: time SHA512 memor aliasing

feat: add sha512 memory aliasing simp_mem DSL based version.

chore: add speedups from GCMGmultV8Sym and MaxTandem

chore: add pretty simp_mem conv based proof of memcpy

chore: fixup commit
---
 Arm/Memory/Common.lean                       |  53 ++--
 Arm/Memory/MemOmega.lean                     | 103 +++++---
 Arm/Memory/SeparateAutomation.lean           | 251 +++++++++++++++++--
 Proofs/AES-GCM/GCMGmultV8Sym.lean            |  17 +-
 Proofs/Experiments/Max/MaxTandem.lean        |   7 +-
 Proofs/Experiments/Memcpy/MemCpyVCG.lean     |  21 +-
 Proofs/Experiments/MemoryAliasing.lean       | 175 ++++++++++++-
 Proofs/Experiments/SHA512MemoryAliasing.lean |   6 +-
 Proofs/SHA512/SHA512Prelude.lean             |  20 +-
 Tactics/BvOmegaBench.lean                    |  64 ++---
 10 files changed, 559 insertions(+), 158 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 4c68fc8e..3885b990 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}"
@@ -168,7 +203,7 @@ syntax (name := mem_omega) "mem_omega" (Lean.Parser.Tactic.config)? (memOmegaWit
 /--
 Implement the `mem_omega` tactic frontend.
 -/
-syntax (name := mem_omega_bang) "mem_omega!" (memOmegaWith)?  : tactic
+syntax (name := mem_omega_bang) "mem_omega!" (Lean.Parser.Tactic.config)? (memOmegaWith)?  : tactic
 
 -- /-- Since we have
 -- syntax memOmegaRule := term
@@ -179,7 +214,6 @@ syntax (name := mem_omega_bang) "mem_omega!" (memOmegaWith)?  : tactic
 --   TSyntax.mk t.raw
   
 
-  
 /--
 build a `UserHyp` from the raw syntax.
 This supports using fars, using CDot notation to partially apply theorems, and to use terms.
@@ -229,15 +263,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 e3d83c17..92cd8baf 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
@@ -257,12 +274,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
@@ -277,7 +294,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
@@ -321,19 +338,28 @@ partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Memory.Hypothesis)
         -- let out ← SimpMemM.simplifyExpr (← whnf gt) hyps
         let some out ← SimpMemM.simplifyExpr gt hyps
           | return ()
+        -- TODO: remove the `check` to make this faster?
         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 := #[]
@@ -365,17 +391,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
 
@@ -384,22 +515,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,
@@ -430,11 +568,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 05461b5f..dd81f79b 100644
--- a/Proofs/AES-GCM/GCMGmultV8Sym.lean
+++ b/Proofs/AES-GCM/GCMGmultV8Sym.lean
@@ -49,7 +49,7 @@ theorem extractLsb'_extractLsb'_zero_of_le (h : start + len1 ≤ len2):
 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)
@@ -100,12 +100,15 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
     -- (FIXME) This will be tackled by `sym_aggregate` when `sym_n` and `simp_mem`
     -- are merged.
     simp only [*]
-    simp_mem
-    rfl
+    conv =>
+      lhs 
+      simp_mem sep with [h_mem_sep]
   · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp]
     sym_aggregate
   · intro n addr h_separate
-    simp_mem
+    conv =>
+      lhs
+      simp_mem sep with [h_separate]
     -- Aggregate the memory (non)effects.
     simp only [*]
   · clear_named [h_s, stepi_]
@@ -114,6 +117,9 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState)
     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]
@@ -128,6 +134,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/Max/MaxTandem.lean b/Proofs/Experiments/Max/MaxTandem.lean
index 48264ca1..3dc6bec2 100644
--- a/Proofs/Experiments/Max/MaxTandem.lean
+++ b/Proofs/Experiments/Max/MaxTandem.lean
@@ -174,7 +174,7 @@ info: 'MaxTandem.program.stepi_0x894_cut' depends on axioms: [propext, Classical
 
 -- 2/15: str  w0, [sp, #12]  ; sp[12] = w0_a
 set_option trace.simp_mem.info true in
-theorem program.stepi_0x898_cut (s sn : ArmState)
+#time theorem program.stepi_0x898_cut (s sn : ArmState)
   (h_program : s.program = program)
   (h_pc : r StateField.PC s = 0x898#64)
   (h_err : r StateField.ERR s = StateError.None)
@@ -198,8 +198,9 @@ theorem program.stepi_0x898_cut (s sn : ArmState)
   simp only [pcs, List.mem_cons, BitVec.reduceEq, List.mem_singleton, or_self, not_false_eq_true,
     true_and, List.not_mem_nil, or_self, not_false_eq_true, true_and]
   simp only [memory_rules, state_simp_rules]
-  simp_mem
-  rfl
+  conv =>
+    lhs
+    simp_mem sep with [h_legal]
 
 /--
 info: 'MaxTandem.program.stepi_0x898_cut' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]
diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
index bf02cbf6..4aa3f615 100644
--- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean
+++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean
@@ -440,7 +440,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)))
@@ -464,21 +463,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 7af16753..7d543803 100644
--- a/Proofs/SHA512/SHA512Prelude.lean
+++ b/Proofs/SHA512/SHA512Prelude.lean
@@ -101,9 +101,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
-set_option trace.simp_mem.info true in
-set_option trace.simp_mem.expr_walk_trace true 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)
@@ -184,7 +182,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. :-(
@@ -205,7 +207,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):
@@ -218,7 +222,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