feat: replace use of (evalTactic bv_omega) with a manual run of simp followed by (evalTactic omega)

Arm/Memory/SeparateAutomation.lean

@@ -122,9 +122,18 @@ structure SimpMemConfig where
 structure Context where
   /-- User configurable options for `simp_mem`. -/
   cfg : SimpMemConfig
-
-def Context.init (cfg : SimpMemConfig) : Context where
-  cfg := cfg
+  /-- Cache of `bv_toNat` simp context. -/
+  bvToNatSimpCtx : Simp.Context
+  /-- Cache of `bv_toNat` simprocs. -/
+  bvToNatSimprocs : Array Simp.Simprocs
+
+def Context.init (cfg : SimpMemConfig) : MetaM Context := do
+  let (bvToNatSimpCtx, bvToNatSimprocs) ←
+    LNSymSimpContext
+      (config := {failIfUnchanged := false})
+      (simp_attrs := #[`bv_toNat])
+      (useDefaultSimprocs := false)
+  return {cfg, bvToNatSimpCtx, bvToNatSimprocs}
 
 /-- a Proof of `e : α`, where `α` is a type such as `MemLegalProp`. -/
 structure Proof (α : Type) (e : α) where
@@ -349,8 +358,8 @@ def State.init (cfg : SimpMemConfig) : State :=
 
 abbrev SimpMemM := StateRefT State (ReaderT Context TacticM)
 
-def SimpMemM.run (m : SimpMemM α) (cfg : SimpMemConfig) : TacticM α :=
-  m.run' (State.init cfg) |>.run (Context.init cfg)
+def SimpMemM.run (m : SimpMemM α) (cfg : SimpMemConfig) : TacticM α := do
+  m.run' (State.init cfg) |>.run (← Context.init cfg)
 
 /-- Add a `Hypothesis` to our hypothesis cache. -/
 def SimpMemM.addHypothesis (h : Hypothesis) : SimpMemM Unit :=
@@ -369,6 +378,14 @@ def SimpMemM.withTraceNode (header : MessageData) (k : SimpMemM α)
     (traceClass : Name := `simp_mem.info) : SimpMemM α :=
   Lean.withTraceNode traceClass (fun _ => return header) k (collapsed := collapsed)
 
+/-- Get the cached simp context for bv_toNat -/
+def SimpMemM.getBvToNatSimpCtx : SimpMemM Simp.Context := do
+  return (← read).bvToNatSimpCtx
+
+/-- Get the cached simpprocs for bv_toNat -/
+def SimpMemM.getBvToNatSimprocs : SimpMemM (Array Simp.Simprocs) := do
+  return (← read).bvToNatSimprocs
+
 def processingEmoji : String := "⚙️"
 
 def consumeRewriteFuel : SimpMemM Unit :=
@@ -428,9 +445,17 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId  := do
 
 /-- SimpMemM's omega invoker -/
 def omega : SimpMemM Unit := do
-  -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280
-  -- @bollu: TODO: understand what precisely we are recovering from.
-  withoutRecover do
+  SimpMemM.withMainContext do
+    -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280
+    let bvToNatSimpCtx ← SimpMemM.getBvToNatSimpCtx
+    let bvToNatSimprocs ← SimpMemM.getBvToNatSimprocs
+    let .some goal ← LNSymSimpAtStar (← getMainGoal) bvToNatSimpCtx bvToNatSimprocs
+      | trace[simp_mem.info] "simp [bv_toNat] at * managed to close goal."
+    replaceMainGoal [goal]
+    SimpMemM.withTraceNode m!"goal post `bv_toNat` reductions (Note: can be large)" do
+      trace[simp_mem.info] "{goal}"
+    -- @bollu: TODO: understand what precisely we are recovering from.
+    withoutRecover do
     evalTactic (← `(tactic| bv_omega_bench))
 
 section Hypotheses
@@ -787,8 +812,6 @@ def proveWithOmega?  {α : Type} [ToMessageData α] [OmegaReducible α] (e : α)
     SimpMemM.withMainContext do
     let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[]
     trace[simp_mem.info] m!"Executing `omega` to close {e}"
-    SimpMemM.withTraceNode m!"goal (Note: can be large)" do
-      trace[simp_mem.info] "{← getMainGoal}"
     omega
     trace[simp_mem.info] "{checkEmoji} `omega` succeeded."
     return (.some <| Proof.mk (← instantiateMVars factProof))

Proofs/Experiments/MemoryAliasing.lean

@@ -12,6 +12,7 @@ import Arm.Memory.SeparateAutomation
 
 -- set_option trace.simp_mem true
 -- set_option trace.simp_mem.info true
+-- set_option trace.Meta.Tactic.simp true
 
 namespace MemLegal
 /-- Show reflexivity of legality. -/

Tactics/Simp.lean

@@ -52,12 +52,18 @@ def LNSymSimpContext
   (exprs : Array Expr := #[])
   -- Simprocs to add to the default set.
   (simprocs : Array Name := #[])
+  -- Whether the default simprocs should be used.
+  (useDefaultSimprocs : Bool := true)
   -- argument to `DiscrTree.mkPath`
   (noIndexAtArgs : Bool := true)
   : MetaM (Simp.Context ×  Array Simp.Simprocs) := do
   let mut ext_simpTheorems := #[]
-  let default_simprocs ← Simp.getSimprocs
-  let mut all_simprocs := (#[default_simprocs] : Simp.SimprocsArray)
+  /- Workaround for https://github.com/leanprover/lean4/issues/5607: Elaboration failure with let mut whose RHS is a do notation -/
+  let all_simprocs ← do
+    if useDefaultSimprocs then
+      pure #[← Simp.getSimprocs]
+    else pure #[]
+  let mut all_simprocs := all_simprocs
 
   for a in simp_attrs do
     let some ext ← (getSimpExtension? a) |
@@ -113,4 +119,21 @@ def LNSymSimp (goal : MVarId)
     | none => return none
     | some (_, goal') => return goal'
 
+/--
+Invoke `simp [..] at *` at the given goal `g` with
+simp context `ctx` and simprocs `simprocs`.
+-/
+def LNSymSimpAtStar (g : MVarId)
+    (ctx : Simp.Context)
+    (simprocs : Array Simp.Simprocs)
+    : MetaM (Option MVarId) := do
+   g.withContext do
+    let fvars : Array FVarId :=
+      (← getLCtx).foldl (init := #[]) fun fvars d => fvars.push d.fvarId
+    let (result, _stats) ← simpGoal g ctx simprocs (fvarIdsToSimp := fvars)
+      (simplifyTarget := true) (discharge? := none)
+    match result with
+    | none => return none
+    | some (_newHyps, g') => pure g'
+
 ----------------------------------------------------------------------