feat: enable simp_mem to be used in ITP style [8/?] (leanprover#240)

### Description:

This adapts changes made in leanprover#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 leanprover#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

@@ -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,40 +801,20 @@ 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 =>
     trace[simp_mem.info]  "{crossEmoji} `omega` failed with error:\n{e.toMessageData}"
     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)
 
 
 

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