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 26f7b85.

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

This reverts commit 472a9ae.

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

@@ -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