From c4d5be0c8ec4a8219301902588806c0804be6abc Mon Sep 17 00:00:00 2001 From: Siddharth Date: Tue, 27 Aug 2024 22:02:37 -0500 Subject: [PATCH] chore: Memory Tactic now solves in a loop and throws error if failed to make progress (#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 --- Arm/Memory/SeparateAutomation.lean | 120 ++++++++++++++++--------- Proofs/Experiments/MemoryAliasing.lean | 38 +++++++- 2 files changed, 115 insertions(+), 43 deletions(-) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 3bc77c8e..57ed0231 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/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 /-- diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index 4a073007..8794291e 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/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