chore: Memory Tactic now solves in a loop and throws error if failed …

…to make progress (leanprover#122)

This removed the need for repeated calls for `simp_mem`, and also uses
the information in the state to throw an error if the tactic was unable
to make *any* progress whatsoever. We mimic the `simp` API, and allow
this to be changed by setting `failIfUnchanged? := false`.

---------

Co-authored-by: Shilpi Goel <shigoel@gmail.com>

Arm/Memory/SeparateAutomation.lean

@@ -98,7 +98,8 @@ namespace SeparateAutomation
 structure SimpMemConfig where
   /-- number of times rewrites must be performed. -/
   rewriteFuel : Nat := 1000
-
+  /-- whether an error should be thrown if the tactic makes no progress. -/
+  failIfUnchanged : Bool := true
 
 /-- Context for the `SimpMemM` monad, containing the user configurable options. -/
 structure Context where
@@ -306,6 +307,11 @@ def consumeRewriteFuel : SimpMemM Unit :=
 
 def outofRewriteFuel? : SimpMemM Bool := do
   return (← get).rewriteFuel == 0
+
+def getConfig : SimpMemM SimpMemConfig := do
+  let ctx ← read
+  return ctx.cfg
+
 /-
 Introduce a new definition into the local context,
 and return the FVarId of the new definition in the goal.
@@ -674,16 +680,17 @@ mutual
 /--
 Pattern match for memory patterns, and simplify them.
 Close memory side conditions with `simplifyGoal`.
+Returns if progress was made.
 -/
-partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Hypothesis) : SimpMemM Unit := do
+partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Hypothesis) : SimpMemM Bool := do
   consumeRewriteFuel
   if ← outofRewriteFuel? then
     trace[simp_mem.info] "out of fuel for rewriting, stopping."
-    return ()
+    return false
 
   if e.isSort then
     trace[simp_mem.info] "skipping sort '{e}'."
-    return ()
+    return false
 
   if let .some er := ReadBytesExpr.ofExpr? e then
     if let .some ew := WriteBytesExpr.ofExpr? er.mem then
@@ -697,99 +704,130 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Hypothesis) : SimpMem
       if let .some separateProof ← proveWithOmega? separate hyps then do
         trace[simp_mem.info] "{checkEmoji} {separate}"
         rewriteReadOfSeparatedWrite er ew separateProof
-        return ()
+        return true
       else if let .some subsetProof ← proveWithOmega? subset hyps then do
         trace[simp_mem.info] "{checkEmoji} {subset}"
         rewriteReadOfSubsetWrite er ew subsetProof
+        return true
       else
         trace[simp_mem.info] "{crossEmoji} Could not prove {er.span} ⟂/⊆ {ew.span}"
-        return ()
+        return false
     else
       -- read
       trace[simp_mem.info] "{checkEmoji} Found read {er}."
       -- TODO: we don't need a separate `subset` branch for the writes: instead, for the write,
       -- 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 changedInCurrentIter? ← withTraceNode m!"Searching for overlapping read {er.span}." do
+        let mut changedInCurrentIter? := false
         for hyp in hyps do
           if let Hypothesis.read_eq hReadEq := hyp then 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)
-            if let some hSubsetProof ← proveWithOmega? subset hyps then
-              trace[simp_mem.info] "{checkEmoji}  ... ⊆ {hReadEq.read.span}"
-              rewriteReadOfSubsetRead er hReadEq hSubsetProof
-              return ()
-            else
-              trace[simp_mem.info] "{crossEmoji}  ... ⊊ {hReadEq.read.span}"
+            changedInCurrentIter? := changedInCurrentIter? ||
+              (← 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)
+                if let some hSubsetProof ← proveWithOmega? subset hyps then
+                  trace[simp_mem.info] "{checkEmoji}  ... ⊆ {hReadEq.read.span}"
+                  rewriteReadOfSubsetRead er hReadEq hSubsetProof
+                  pure true
+                else
+                  trace[simp_mem.info] "{crossEmoji}  ... ⊊ {hReadEq.read.span}"
+                  pure false)
+        pure changedInCurrentIter?
+      return changedInCurrentIter?
   else
     if e.isForall then
       Lean.Meta.forallTelescope e fun xs b => do
+        let mut changedInCurrentIter? := false
         for x in xs do
-          SimpMemM.simplifyExpr x hyps
+          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps)
           -- we may have a hypothesis like
           -- ∀ (x : read_mem (read_mem_bytes ...) ... = out).
           -- we want to simplify the *type* of x.
-          SimpMemM.simplifyExpr (← inferType x) hyps
-        SimpMemM.simplifyExpr b hyps
+          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps)
+        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps)
+        return changedInCurrentIter?
     else if e.isLambda then
       Lean.Meta.lambdaTelescope e fun xs b => do
+        let mut changedInCurrentIter? := false
         for x in xs do
-          SimpMemM.simplifyExpr x hyps
-          SimpMemM.simplifyExpr (← inferType x) hyps
-        SimpMemM.simplifyExpr b hyps
+          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps)
+          changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps)
+        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps)
+        return changedInCurrentIter?
     else
       -- check if we have expressions.
       match e with
       | .app f x =>
-        SimpMemM.simplifyExpr f hyps
-        SimpMemM.simplifyExpr x hyps
-      | _ => return ()
+        let mut changedInCurrentIter? := false
+        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr f hyps)
+        changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps)
+        return changedInCurrentIter?
+      | _ => return false
+
 
 /--
 simplify the goal state, closing legality, subset, and separation goals,
 and simplifying all other expressions.
 -/
-partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM Unit := do
+partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM Bool := do
   SimpMemM.withMainContext do
     trace[simp_mem.info] "{processingEmoji} Matching on ⊢ {← g.getType}"
     let gt ← g.getType
-    if let .some e := MemLegalProp.ofExpr? gt then do
+    if let .some e := MemLegalProp.ofExpr? gt then
       withTraceNode m!"Matched on ⊢ {e}. Proving..." do
-      if let .some proof ← proveWithOmega? e hyps then do
-        (← getMainGoal).assign proof.h
-    if let .some e := MemSubsetProp.ofExpr? gt then do
+        if let .some proof ← proveWithOmega? e hyps then
+          (← getMainGoal).assign proof.h
+      return true
+
+    if let .some e := MemSubsetProp.ofExpr? gt then
       withTraceNode m!"Matched on ⊢ {e}. Proving..." do
-      if let .some proof ←  proveWithOmega? e hyps then do
-        (← getMainGoal).assign proof.h
-    if let .some e := MemSeparateProp.ofExpr? gt then do
+        if let .some proof ←  proveWithOmega? e hyps then
+          (← getMainGoal).assign proof.h
+      return true
+    if let .some e := MemSeparateProp.ofExpr? gt then
       withTraceNode m!"Matched on ⊢ {e}. Proving..." do
-      if let .some proof ←  proveWithOmega? e hyps then do
-        (← getMainGoal).assign proof.h
-    withTraceNode m!"Simplifying goal." do
-      SimpMemM.simplifyExpr (← whnf gt) hyps
-
+        if let .some proof ←  proveWithOmega? e hyps then
+          (← getMainGoal).assign proof.h
+      return true
+    else
+      let changedInCurrentIter? ← withTraceNode m!"Simplifying goal." do
+          SimpMemM.simplifyExpr (← whnf gt) hyps
+      return changedInCurrentIter?
 end
 
 /--
 The core simplification loop.
 We look for appropriate hypotheses, and simplify (often closing) the main goal using them.
 -/
-def SimpMemM.simplifyLoop : SimpMemM Unit := do
-    (← getMainGoal).withContext do
+partial def SimpMemM.simplifyLoop : SimpMemM Unit := do
+  (← getMainGoal).withContext do
+    let mut madeAnyProgress? := false -- whether we ever make any progress. Used to throw `failIfUnchanged` error.
+    let mut changedInCurrentIter? := true
+    while ! (← outofRewriteFuel?) && changedInCurrentIter? do
+      consumeRewriteFuel
       let hyps := (← getLocalHyps)
       let foundHyps ← withTraceNode m!"Searching for Hypotheses" do
         let mut foundHyps : Array Hypothesis := #[]
         for h in hyps do
           foundHyps ← hypothesisOfExpr h foundHyps
         pure foundHyps
+
       withTraceNode m!"Summary: Found {foundHyps.size} hypotheses" do
         for (i, h) in foundHyps.toList.enum do
           trace[simp_mem.info] m!"{i+1}) {h}"
 
-      withTraceNode m!"Performing Rewrite At Main Goal" do
+      if (← getUnsolvedGoals).isEmpty then
+        trace[simp_mem.info] "{checkEmoji} All goals solved."
+        break
+
+      changedInCurrentIter? ← withTraceNode m!"Performing Rewrite At Main Goal" do
         SimpMemM.simplifyGoal (← getMainGoal) foundHyps
+      madeAnyProgress? := madeAnyProgress? || changedInCurrentIter?
 
+    /- we haven't changed ever, nor in the current iteration.. -/
+    if !madeAnyProgress? && (← getConfig).failIfUnchanged then
+        throwError "{crossEmoji} simp_mem failed to make progress."
 end Simplify
 
 /--

Proofs/Experiments/MemoryAliasing.lean

@@ -159,7 +159,7 @@ theorem mem_automation_test_4
       (write_mem_bytes 48 src_addr val s0)) =
    val.extractLsBytes 1 10 := by
   simp only [memory_rules]
-  simp_mem; simp_mem -- TODO: repeat on change.
+  simp_mem; -- TODO: repeat on change.
   congr 1
   bv_omega' -- TODO: address normalization.
 
@@ -264,7 +264,7 @@ theorem test_write_zero (hlegalw : mem_legal' write_addr 0)
     (hlegalr : mem_legal' read_addr read_n) :
     Memory.read_bytes read_n read_addr (Memory.write_bytes 0 write_addr write_val mem) =
     mem.read_bytes read_n read_addr := by
-  simp_mem
+  try simp_mem
   sorry
 
 end ReadOverlappingWrite
@@ -365,3 +365,37 @@ theorem mem_separate_move_of_lt_of_le  (h : mem_separate' a an b bn)
   (hlegal : a' ≤ a) : mem_separate' a' (an + (a - a').toNat) b bn := by simp_mem
 
 end MathProperties
+
+namespace MemOptions
+
+/--
+error: unsolved goals
+⊢ False
+---
+info: [simp_mem.info] Searching for Hypotheses
+[simp_mem.info] Summary: Found 0 hypotheses
+[simp_mem.info] Performing Rewrite At Main Goal
+  [simp_mem.info] ⚙️ Matching on ⊢ False
+  [simp_mem.info] Simplifying goal.
+---
+info: ⊢ False
+-/
+#guard_msgs in theorem test_no_fail_if_unchanged : False := by
+  simp_mem (config := { failIfUnchanged := false })
+  trace_state
+
+/--
+error: ❌ simp_mem failed to make progress.
+---
+info: [simp_mem.info] Searching for Hypotheses
+[simp_mem.info] Summary: Found 0 hypotheses
+[simp_mem.info] Performing Rewrite At Main Goal
+  [simp_mem.info] ⚙️ Matching on ⊢ False
+  [simp_mem.info] Simplifying goal.
+-/
+#guard_msgs in theorem test_fail_if_unchanged : False := by
+  simp_mem
+  trace_state
+
+
+end MemOptions