chore: add fuel

Arm/Memory/SeparateAutomation.lean

@@ -91,6 +91,9 @@ end BvOmega
 namespace SeparateAutomation
 
 structure SimpMemConfig where
+  /-- number of times rewrites must be performed. -/
+  rewriteFuel : Nat := 100
+
 
 /-- Context for the `SimpMemM` monad, containing the user configurable options. -/
 structure Context where
@@ -254,13 +257,15 @@ instance : ToMessageData Hypothesis where
 /-- The internal state for the `SimpMemM` monad, recording previously encountered atoms. -/
 structure State where
   hypotheses : Array Hypothesis := #[]
+  rewriteFuel : Nat
 
-def State.init : State := {}
+def State.init (cfg : SimpMemConfig) : State :=
+  { rewriteFuel := cfg.rewriteFuel}
 
 abbrev SimpMemM := StateRefT State (ReaderT Context TacticM)
 
 def SimpMemM.run (m : SimpMemM α) (cfg : SimpMemConfig) : TacticM α :=
-  m.run' State.init |>.run (Context.init cfg)
+  m.run' (State.init cfg) |>.run (Context.init cfg)
 
 /-- Add a `Hypothesis` to our hypothesis cache. -/
 def SimpMemM.addHypothesis (h : Hypothesis) : SimpMemM Unit :=
@@ -271,6 +276,12 @@ def SimpMemM.withMainContext (ma : SimpMemM α) : SimpMemM α := do
 
 def processingEmoji : String := "⚙️"
 
+def consumeRewriteFuel : SimpMemM Unit :=
+  modify fun s => { s with rewriteFuel := s.rewriteFuel - 1 }
+
+def outofRewriteFuel? : SimpMemM Bool := do
+  return (← get).rewriteFuel == 0
+
 /--
 info: mem_separate'.ha {a : BitVec 64} {an : Nat} {b : BitVec 64} {bn : Nat} (self : mem_separate' a an b bn) :
   mem_legal' a an
@@ -713,6 +724,15 @@ mutual
 
 
 partial def SimpMemM.improveExpr (e : Expr) (hyps : Array Hypothesis) : SimpMemM Unit := do
+  consumeRewriteFuel
+  if ← outofRewriteFuel? then
+    trace[simp_mem.info] "out of fuel for rewriting, stopping."
+    return ()
+  -- withTraceNode `simp_mem.info (fun _ => return "improving expression (NOTE: can be large)") do
+  --   trace[simp_mem.info] "{e}"
+  --   if e.isSort then trace[simp_mem.info] "{crossEmoji} skipping sorts."
+  if e.isSort then return ()
+
   if let .some er := ReadBytesExpr.match? e then
     if let .some ew := WriteBytesExpr.match? er.mem then
       trace[simp_mem.info] "{checkEmoji} Found read of write."
@@ -751,8 +771,24 @@ partial def SimpMemM.improveExpr (e : Expr) (hyps : Array Hypothesis) : SimpMemM
             else
               trace[simp_mem.info] "{crossEmoji}  ... ⊊ {hReadEq.read.span}"
       -- trace[simp_mem.info] "{crossEmoji} {er.span} ⊊ any read."
-  return ()
-
+  else
+    if e.isForall then
+      Lean.Meta.forallTelescope e fun xs b => do
+        for x in xs do
+          improveExpr x hyps
+        improveExpr b hyps
+    else if e.isLambda then
+      Lean.Meta.lambdaTelescope e fun xs b => do
+        for x in xs do
+          improveExpr x hyps
+        improveExpr b hyps
+    else
+      -- check if we have expressions.
+      match e with
+      | .app f x =>
+        improveExpr f hyps
+        improveExpr x hyps
+      | _ => return ()
 -- /-- info: mem_legal' (a : BitVec 64) (n : Nat) : Prop -/
 -- #guard_msgs in #check mem_legal'
 
@@ -772,13 +808,14 @@ partial def SimpMemM.improveGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMe
       withTraceNode `simp_mem.info (fun _ => return m!"Matched on ⊢ {e}. Proving...") do
       if let .some proof ←  proveMemSeparateWithOmega? e hyps then do
         (← getMainGoal).assign proof.h
-
-    if let some (_, lhs, rhs) ← matchEq? gt then
-      withTraceNode `simp_mem.info (fun _ => return m!"Matched on equality. Simplifying") do
-        withTraceNode `simp_mem.info (fun _ => return m!"⊢ Simplifying LHS") do
-          improveExpr lhs hyps
-        withTraceNode `simp_mem.info (fun _ => return m!"⊢ Simplifying RHS") do
-          improveExpr rhs hyps
+    withTraceNode `simp_mem.info (fun _ => return m!"Simplifying goal.") do
+      improveExpr gt hyps
+    -- if let some (_, lhs, rhs) ← matchEq? gt then
+    --   withTraceNode `simp_mem.info (fun _ => return m!"Matched on equality. Simplifying") do
+    --     withTraceNode `simp_mem.info (fun _ => return m!"⊢ Simplifying LHS") do
+    --       improveExpr lhs hyps
+    --     withTraceNode `simp_mem.info (fun _ => return m!"⊢ Simplifying RHS") do
+    --       improveExpr rhs hyps
     -- -- TODO: do this till fixpoint.
     -- for h in (← get).hypotheses do
     --   let x ← mkFreshExprMVar .none

Proofs/Experiments/MemoryAliasing.lean

@@ -253,20 +253,47 @@ theorem test_quantified_1 {val : BitVec (16 * 8)}
   simp_mem
   simp
 
+/--
+info: 'ExprVisitor.test_quantified_1' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in #print axioms test_quantified_1
+
 /-- Check that we correctly walk under applications. -/
 theorem test_app_1 {val : BitVec (16 * 8)}
     (hlegal : mem_legal' 0 16) (f : BitVec _ → Nat) :
     f (Memory.read_bytes 16 0 (Memory.write_bytes 16 0 val mem)) =
     f (val.extractLsBytes 0 16)  := by
   simp_mem
   simp
+/-- info: 'ExprVisitor.test_app_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/
+#guard_msgs in #print axioms test_app_1
 
-/-- Check that we correctly walk under applications and binders simultaneously. -/
+/--
+Check that we correctly walk under applications
+and binders simultaneously.
+-/
 theorem test_quantified_app_1 {val : BitVec (16 * 8)}
     (hlegal : mem_legal' 0 16) : ∀ (f : BitVec _ → Nat),
     f (Memory.read_bytes 16 0 (Memory.write_bytes 16 0 val mem)) =
     f (val.extractLsBytes 0 16)  := by
   simp_mem
   simp
 
+/--
+info: 'ExprVisitor.test_quantified_app_1' depends on axioms: [propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs in #print axioms test_quantified_app_1
+
+/--
+Check that we correctly simplify hypotheses as well,
+where the hypotheses are universally quantified variables
+-/
+theorem test_quantified_app_2 {val : BitVec (16 * 8)}
+    (hlegal : ∀ (addr : Nat), mem_legal' addr 16)
+    (f : _ → Nat) :
+    f (∀ (P : Memory.read_bytes 16 0 (Memory.write_bytes 16 0 val mem) = irrelevant), Nat) =
+    f (∀ (P : val.extractLsBytes 0 16 = irrelevant), Nat) := by
+  simp_mem
+  simp
+
 end ExprVisitor