From ea439011613cb91f47f3dd76b279d0a0df34ccc4 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 19 Aug 2024 18:03:59 -0500 Subject: [PATCH] chore: add fuel --- Arm/Memory/SeparateAutomation.lean | 59 +++++++++++++++++++++----- Proofs/Experiments/MemoryAliasing.lean | 29 ++++++++++++- 2 files changed, 76 insertions(+), 12 deletions(-) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index f25551d4..34baf736 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/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 diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index 1a6c73dc..b7ed1520 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -253,6 +253,11 @@ 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) : @@ -260,8 +265,13 @@ theorem test_app_1 {val : BitVec (16 * 8)} 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)) = @@ -269,4 +279,21 @@ theorem test_quantified_app_1 {val : BitVec (16 * 8)} 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