From c6c48a01bffb15dc2a75c80e5c168c7d174b2f44 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Fri, 6 Sep 2024 11:04:56 -0500 Subject: [PATCH] feat: add automation support for pairwise memory separation (#126) This is stacked on top of #123 , since we want to state this, for a given `ms : List MemoryRegion`, `ms.pairwise MemoryRegion.Separate`. This, of course, needs us to have the `MemoryRegion` abstraction in the first place. --------- Co-authored-by: Shilpi Goel --- Arm/Memory/Separate.lean | 57 ++++- Arm/Memory/SeparateAutomation.lean | 285 +++++++++++++++++++++---- Proofs/Experiments/MemoryAliasing.lean | 49 ++++- 3 files changed, 339 insertions(+), 52 deletions(-) diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean index f1ecfd58..c35b1da4 100644 --- a/Arm/Memory/Separate.lean +++ b/Arm/Memory/Separate.lean @@ -328,6 +328,12 @@ theorem BitVec.not_le_eq_lt {a b : BitVec w₁} : (¬ (a ≤ b)) ↔ b < a := by rw [BitVec.le_def, BitVec.lt_def] omega +theorem mem_separate'_comm (h : mem_separate' a an b bn) : + mem_separate' b bn a an := by + have := h.omega_def + apply mem_separate'.of_omega + omega + /-# This is a theorem we ought to prove, which establishes the equivalence between the old and new defintions of 'mem_separate'. @@ -492,7 +498,7 @@ theorem Memory.read_bytes_write_bytes_eq_of_mem_subset' · subst hxn exfalso have h := i.isLt - simp at h + simp only [Nat.reduceMul, Nat.zero_mul, Nat.not_lt_zero] at h · by_cases h₁ : ↑i < xn * 8 · simp only [h₁] simp only [decide_True, Bool.true_and] @@ -560,4 +566,53 @@ theorem Memory.read_bytes_eq_extractLsBytes_sub_of_mem_subset' bv_omega · simp only [h, ↓reduceIte] +/-- A region of memory, given by (base pointer, length) -/ +abbrev Memory.Region := BitVec 64 × Nat + +def Memory.Region.mk (a : BitVec 64) (n : Nat) : Memory.Region := (a, n) + +/-- A hypothesis that memory regions `a` and `b` are separate. -/ +def Memory.Region.separate (a b : Memory.Region) : Prop := + mem_separate' a.fst a.snd b.fst b.snd + +/-- A list of memory regions, that are known to be pairwise disjoint. -/ +def Memory.Region.pairwiseSeparate (mems : List Memory.Region) : Prop := + mems.Pairwise Memory.Region.separate + +/-- If `i ≠ j`, then prove that `mems[i] ⟂ mems[j]`. +The theorem is stated in mildly awkward fashion for ease of use during proof automation. +-/ +def Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem + (h : Memory.Region.pairwiseSeparate mems) + (i j : Nat) + (hij : i ≠ j) + (a b : Memory.Region) + (ha : mems.get? i = some a) (hb : mems.get? j = some b) : + mem_separate' a.fst a.snd b.fst b.snd := by + induction h generalizing a b i j + case nil => simp only [List.get?_eq_getElem?, List.getElem?_nil, reduceCtorEq] at ha + case cons x xs ihx _ihxs ihxs' => + simp only [List.get?_eq_getElem?] at ha hb + rcases i with rfl | i' + · simp at ha + · rcases j with rfl | j' + · simp only [ne_eq, not_true_eq_false] at hij + · subst ha + simp only [List.getElem?_cons_succ] at hb + apply ihx + exact List.getElem?_mem hb + · rcases j with rfl | j' + · simp only [List.length_cons, Nat.zero_lt_succ, List.getElem?_eq_getElem, + List.getElem_cons_zero, Option.some.injEq] at hb + · subst hb + simp only [List.getElem?_cons_succ] at ha + apply mem_separate'_comm + apply ihx + exact List.getElem?_mem ha + · simp only [List.getElem?_cons_succ] at ha hb + apply ihxs' i' j' + · omega + · simp only [List.get?_eq_getElem?, ha] + · simp only [List.get?_eq_getElem?, hb] + end NewDefinitions diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 57ed0231..e73ebd68 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -18,6 +18,7 @@ import Lean.Meta.Tactic.Rewrite import Lean.Meta.Tactic.Rewrites import Lean.Elab.Tactic.Conv import Lean.Elab.Tactic.Conv.Basic +import Tactics.Simp open Lean Meta Elab Tactic @@ -122,6 +123,16 @@ instance [ToMessageData α] : ToMessageData (Proof α e) where structure MemSpanExpr where base : Expr n : Expr +deriving Inhabited + +/-- info: Memory.Region.mk (a : BitVec 64) (n : Nat) : Memory.Region -/ +#guard_msgs in #check Memory.Region.mk + +def MemSpanExpr.toExpr (span : MemSpanExpr) : Expr := + mkAppN (Expr.const ``Memory.Region.mk []) #[span.base, span.n] + +def MemSpanExpr.toTypeExpr : Expr := + (Expr.const ``Memory.Region []) instance : ToMessageData MemSpanExpr where toMessageData span := m! "[{span.base}..{span.n})" @@ -182,6 +193,42 @@ abbrev MemLegalProof := Proof MemLegalProp def MemLegalProof.mk {e : MemLegalProp} (h : Expr) : MemLegalProof e := { h } + +/-- info: Memory.Region.pairwiseSeparate (mems : List Memory.Region) : Prop -/ +#guard_msgs in #check Memory.Region.pairwiseSeparate + +/-- +A proposition `Memory.Region.pairwiseSeparate [x1, x2, ..., xn]`. +-/ +structure MemPairwiseSeparateProp where + xs : Array MemSpanExpr + +/-- info: List.nil.{u} {α : Type u} : List α -/ +#guard_msgs in #check List.nil + +/-- info: List.cons.{u} {α : Type u} (head : α) (tail : List α) : List α -/ +#guard_msgs in #check List.cons + +/-- Given `Memory.Region.pairwiseSeparate [x1, ..., xn]`, +get the expression corresponding `[x1, ..., xn]`. -/ +def MemPairwiseSeparateProp.getMemSpanListExpr + (e : MemPairwiseSeparateProp) : Expr := Id.run do + let memoryRegionTy : Expr := mkConst ``Memory.Region + let mut out := mkApp (mkConst ``List.nil [0]) memoryRegionTy + for i in [0:e.xs.size] do + let x := e.xs[e.xs.size - i - 1]! + out := mkAppN (mkConst ``List.cons [0]) #[memoryRegionTy, x.toExpr, out] + return out + +/-- Get the expression `Memory.Region.pairwiseSeparate [x1, ..., xn]` -/ +def MemPairwiseSeparateProp.toExpr (e : MemPairwiseSeparateProp) : Expr := + mkApp (mkConst ``Memory.Region.pairwiseSeparate) e.getMemSpanListExpr + +instance : ToMessageData MemPairwiseSeparateProp where + toMessageData e := m!"pairwiseSeparate {e.xs.toList}" + +abbrev MemPairwiseSeparateProof := Proof MemPairwiseSeparateProp + /-- info: Memory.read_bytes (n : Nat) (addr : BitVec 64) (m : Memory) : BitVec (n * 8) -/ #guard_msgs in #check Memory.read_bytes @@ -258,10 +305,12 @@ inductive Hypothesis | separate (proof : MemSeparateProof e) | subset (proof : MemSubsetProof e) | legal (proof : MemLegalProof e) +| pairwiseSeparate (proof : MemPairwiseSeparateProof e) | read_eq (proof : ReadBytesEqProof) def Hypothesis.proof : Hypothesis → Expr -| .separate proof => proof.h +| .pairwiseSeparate proof => proof.h +| .separate proof => proof.h | .subset proof => proof.h | .legal proof => proof.h | .read_eq proof => proof.h @@ -272,6 +321,7 @@ instance : ToMessageData Hypothesis where | .separate proof => toMessageData proof | .legal proof => toMessageData proof | .read_eq proof => toMessageData proof + | .pairwiseSeparate proof => toMessageData proof /-- The internal state for the `SimpMemM` monad, recording previously encountered atoms. -/ structure State where @@ -293,6 +343,9 @@ def SimpMemM.addHypothesis (h : Hypothesis) : SimpMemM Unit := def SimpMemM.withMainContext (ma : SimpMemM α) : SimpMemM α := do (← getMainGoal).withContext ma +def SimpMemM.withContext (g : MVarId) (ma : SimpMemM α) : SimpMemM α := do + g.withContext ma + /-- create a trace node in trace class (i.e. `set_option traceClass true`), with header `header`, whose default collapsed state is `collapsed`. -/ def SimpMemM.withTraceNode (header : MessageData) (k : SimpMemM α) @@ -308,19 +361,50 @@ def consumeRewriteFuel : SimpMemM Unit := def outofRewriteFuel? : SimpMemM Bool := do return (← get).rewriteFuel == 0 +/-- Create a trace note that folds `header` with `(NOTE: can be large)`, +and prints `msg` under such a trace node. +-/ +def SimpMemM.traceLargeMsg (header : MessageData) (msg : MessageData) : SimpMemM Unit := + withTraceNode m!"{header} (NOTE: can be large)" do + trace[simp_mem.info] msg + + def getConfig : SimpMemM SimpMemConfig := do let ctx ← read return ctx.cfg +/-- info: state_value (fld : StateField) : Type -/ +#guard_msgs in #check state_value + /- -Introduce a new definition into the local context, +Introduce a new definition into the local context, simplify it using `simp`, and return the FVarId of the new definition in the goal. -/ -def introDef (name : String) (hdefVal : Expr) : SimpMemM FVarId := do +def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId := do SimpMemM.withMainContext do + let name ← mkFreshUserName <| .mkSimple name let goal ← getMainGoal let hdefTy ← inferType hdefVal + + /- Simp to gain some more juice out of the defn.. -/ + let mut simpTheorems : Array SimpTheorems := #[] + for a in #[`minimal_theory, `bitvec_rules] do + let some ext ← (getSimpExtension? a) + | throwError m!"[simp_mem] Internal error: simp attribute {a} not found!" + simpTheorems := simpTheorems.push (← ext.getTheorems) + + -- unfold `state_value. + simpTheorems := simpTheorems.push <| ← ({} : SimpTheorems).addDeclToUnfold `state_value + let simpCtx : Simp.Context := { + simpTheorems, + config := { decide := true, failIfUnchanged := false }, + congrTheorems := (← Meta.getSimpCongrTheorems) + } + let (simpResult, _stats) ← simp hdefTy simpCtx (simprocs := #[]) + let hdefVal ← simpResult.mkCast hdefVal + let hdefTy ← inferType hdefVal + let goal ← goal.define name hdefTy hdefVal let (fvar, goal) ← goal.intro1P replaceMainGoal [goal] @@ -403,6 +487,35 @@ def MemSeparateProp.ofExpr? (e : Expr) : Option MemSeparateProp := .some { sa, sb } | _ => none +/-- info: Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β -/ +#guard_msgs in #check Prod.mk + +/-- info: List.cons.{u} {α : Type u} (head : α) (tail : List α) : List α -/ +#guard_msgs in #check List.cons + +/-- info: List.nil.{u} {α : Type u} : List α -/ +#guard_msgs in #check List.nil + +/-- match an expression `e` to a `Memory.Region.pairwiseSeparate`. -/ +partial def MemPairwiseSeparateProof.ofExpr? (e : Expr) : Option MemPairwiseSeparateProp := + match_expr e with + | Memory.Region.pairwiseSeparate xs => do + let .some xs := go xs #[] | none + some { xs := xs } + | _ => none + where + go (e : Expr) (xs : Array MemSpanExpr) : Option (Array MemSpanExpr) := + match_expr e with + | List.cons _α ex exs => + match_expr ex with + | Prod.mk _ta _tb a n => + let x : MemSpanExpr := ⟨a, n⟩ + go exs (xs.push x) + | _ => none + | List.nil _α => some xs + | _ => none + + /-- Match an expression `h` to see if it's a useful hypothesis. -/ def hypothesisOfExpr (h : Expr) (hyps : Array Hypothesis) : MetaM (Array Hypothesis) := do let ht ← inferType h @@ -423,6 +536,10 @@ def hypothesisOfExpr (h : Expr) (hyps : Array Hypothesis) : MetaM (Array Hypothe let proof : MemLegalProof legal := ⟨h⟩ let hyps := hyps.push (.legal proof) return hyps + else if let .some pairwiseSep := MemPairwiseSeparateProof.ofExpr? ht then + let proof : MemPairwiseSeparateProof pairwiseSep := ⟨h⟩ + let hyps := hyps.push (.pairwiseSeparate proof) + return hyps else let mut hyps := hyps for eqProof in ReadBytesEqProof.ofExpr? h ht do @@ -444,7 +561,7 @@ def MemLegalProof.omega_def (h : MemLegalProof e) : Expr := def MemLegalProof.addOmegaFacts (h : MemLegalProof e) (args : Array Expr) : SimpMemM (Array Expr) := do SimpMemM.withMainContext do - let fvar ← introDef "hmemLegal_omega" h.omega_def + let fvar ← simpAndIntroDef "hmemLegal_omega" h.omega_def trace[simp_mem.info] "{h}: added omega fact ({h.omega_def})" return args.push (Expr.fvar fvar) @@ -466,7 +583,7 @@ def MemSubsetProof.omega_def (h : MemSubsetProof e) : Expr := def MemSubsetProof.addOmegaFacts (h : MemSubsetProof e) (args : Array Expr) : SimpMemM (Array Expr) := do SimpMemM.withMainContext do - let fvar ← introDef "hmemSubset_omega" h.omega_def + let fvar ← simpAndIntroDef "hmemSubset_omega" h.omega_def trace[simp_mem.info] "{h}: added omega fact ({h.omega_def})" return args.push (Expr.fvar fvar) @@ -482,10 +599,74 @@ def MemSeparateProof.omega_def (h : MemSeparateProof e) : Expr := def MemSeparateProof.addOmegaFacts (h : MemSeparateProof e) (args : Array Expr) : SimpMemM (Array Expr) := do SimpMemM.withMainContext do - let fvar ← introDef "hmemSeparate_omega" h.omega_def + -- simp only [bitvec_rules] (failIfUnchanged := false) + let fvar ← simpAndIntroDef "hmemSeparate_omega" h.omega_def trace[simp_mem.info] "{h}: added omega fact ({h.omega_def})" return args.push (Expr.fvar fvar) + + +/-- info: Ne.{u} {α : Sort u} (a b : α) : Prop -/ +#guard_msgs in #check Ne + +/-- info: List.get?.{u} {α : Type u} (as : List α) (i : Nat) : Option α -/ +#guard_msgs in #check List.get? + +/-- Make the expression `mems.get? i = some a`. -/ +def mkListGetEqSomeTy (mems : MemPairwiseSeparateProp) (i : Nat) (a : MemSpanExpr) : SimpMemM Expr := do + let lhs ← mkAppOptM ``List.get? #[.none, mems.getMemSpanListExpr, mkNatLit i] + let rhs ← mkSome MemSpanExpr.toTypeExpr a.toExpr + mkEq lhs rhs + +/-- +info: Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem {mems : List Memory.Region} + (h : Memory.Region.pairwiseSeparate mems) (i j : Nat) (hij : i ≠ j) (a b : Memory.Region) (ha : mems.get? i = some a) + (hb : mems.get? j = some b) : mem_separate' a.fst a.snd b.fst b.snd +-/ +#guard_msgs in #check Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem + +/-- make `Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem i j (by decide) a b rfl rfl`. -/ +def MemPairwiseSeparateProof.mem_separate'_of_pairwiseSeparate_of_mem_of_mem + (self : MemPairwiseSeparateProof mems) (i j : Nat) (a b : MemSpanExpr) : + SimpMemM <| MemSeparateProof ⟨a, b⟩ := do + let iexpr := mkNatLit i + let jexpr := mkNatLit j + -- i ≠ j + let hijTy := mkAppN (mkConst ``Ne [1]) #[(mkConst ``Nat), mkNatLit i, mkNatLit j] + -- mems.get? i = some a + let hijVal ← mkDecideProof hijTy + let haVal ← mkEqRefl <| ← mkSome MemSpanExpr.toTypeExpr a.toExpr + let hbVal ← mkEqRefl <| ← mkSome MemSpanExpr.toTypeExpr b.toExpr + let h := mkAppN (Expr.const ``Memory.Region.separate'_of_pairwiseSeprate_of_mem_of_mem []) + #[mems.getMemSpanListExpr, + self.h, + iexpr, + jexpr, + hijVal, + a.toExpr, + b.toExpr, + haVal, + hbVal] + return ⟨h⟩ +/-- +Currently, if the list is syntacticaly of the form [x1, ..., xn], + we create hypotheses of the form `mem_separate' xi xj` for all i, j.. +This can be generalized to pairwise separation given hypotheses x ∈ xs, x' ∈ xs. +-/ +def MemPairwiseSeparateProof.addOmegaFacts (h : MemPairwiseSeparateProof e) (args : Array Expr) : + SimpMemM (Array Expr) := do + -- We need to loop over i, j where i < j and extract hypotheses. + -- We need to find the length of the list, and return an `Array MemRegion`. + let mut args := args + for i in [0:e.xs.size] do + for j in [i+1:e.xs.size] do + let a := e.xs[i]! + let b := e.xs[j]! + args ← SimpMemM.withTraceNode m!"Exploiting ({i}, {j}) : {a} ⟂ {b}" do + let proof ← h.mem_separate'_of_pairwiseSeparate_of_mem_of_mem i j a b + SimpMemM.traceLargeMsg m!"added {← inferType proof.h}" m!"{proof.h}" + proof.addOmegaFacts args + return args /-- Given a hypothesis, add declarations that would be useful for omega-blasting -/ @@ -494,6 +675,7 @@ def Hypothesis.addOmegaFactsOfHyp (h : Hypothesis) (args : Array Expr) : SimpMem | Hypothesis.legal h => h.addOmegaFacts args | Hypothesis.subset h => h.addOmegaFacts args | Hypothesis.separate h => h.addOmegaFacts args + | Hypothesis.pairwiseSeparate h => h.addOmegaFacts args | Hypothesis.read_eq _h => return args -- read has no extra `omega` facts. /-- @@ -768,32 +950,39 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Hypothesis) : SimpMem /-- simplify the goal state, closing legality, subset, and separation goals, -and simplifying all other expressions. +and simplifying all other expressions. return `true` if goal has been closed, and `false` otherwise. -/ -partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM Bool := do - SimpMemM.withMainContext do +partial def SimpMemM.closeGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM Bool := do + SimpMemM.withContext g do trace[simp_mem.info] "{processingEmoji} Matching on ⊢ {← g.getType}" let gt ← g.getType if let .some e := MemLegalProp.ofExpr? gt then withTraceNode m!"Matched on ⊢ {e}. Proving..." do if let .some proof ← proveWithOmega? e hyps then - (← getMainGoal).assign proof.h - return true - + g.assign proof.h if let .some e := MemSubsetProp.ofExpr? gt then withTraceNode m!"Matched on ⊢ {e}. Proving..." do if let .some proof ← proveWithOmega? e hyps then - (← getMainGoal).assign proof.h - return true + g.assign proof.h if let .some e := MemSeparateProp.ofExpr? gt then withTraceNode m!"Matched on ⊢ {e}. Proving..." do 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? + g.assign proof.h + return ← g.isAssigned + + + +/-- +simplify the goal state, closing legality, subset, and separation goals, +and simplifying all other expressions. Returns `true` if an improvement has been made +in the current iteration. +-/ +partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM Bool := do + SimpMemM.withContext g do + let gt ← g.getType + let changedInCurrentIter? ← withTraceNode m!"Simplifying goal." do + SimpMemM.simplifyExpr (← whnf gt) hyps + return changedInCurrentIter? end /-- @@ -801,33 +990,39 @@ The core simplification loop. We look for appropriate hypotheses, and simplify (often closing) the main goal using them. -/ 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}" - - if (← getUnsolvedGoals).isEmpty then - trace[simp_mem.info] "{checkEmoji} All goals solved." - break - - changedInCurrentIter? ← withTraceNode m!"Performing Rewrite At Main Goal" do + let g ← getMainGoal + g.withContext do + 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}" + + if ← SimpMemM.closeGoal g foundHyps then + trace[simp_mem.info] "{checkEmoji} goal closed." + return () + + -- goal was not closed, try and improve. + let mut changedInAnyIter? := false + while true do + if (← outofRewriteFuel?) then break + + let changedInCurrentIter? ← withTraceNode m!"Performing Rewrite At Main Goal" do SimpMemM.simplifyGoal (← getMainGoal) foundHyps - madeAnyProgress? := madeAnyProgress? || changedInCurrentIter? + changedInAnyIter? := changedInAnyIter? || changedInCurrentIter? + + if !changedInCurrentIter? then + trace[simp_mem.info] "{crossEmoji} No progress made in this iteration. halting." + break - /- we haven't changed ever, nor in the current iteration.. -/ - if !madeAnyProgress? && (← getConfig).failIfUnchanged then - throwError "{crossEmoji} simp_mem failed to make progress." + /- we haven't changed ever.. -/ + if !changedInAnyIter? && (← getConfig).failIfUnchanged then + throwError "{crossEmoji} simp_mem failed to make any progress." end Simplify /-- diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index cd7e8854..a27c7aa7 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -10,8 +10,8 @@ import Arm.Memory.MemoryProofs import Arm.BitVec import Arm.Memory.SeparateAutomation -set_option trace.simp_mem true -set_option trace.simp_mem.info true +-- set_option trace.simp_mem true +-- set_option trace.simp_mem.info true namespace MemLegal /-- Show reflexivity of legality. -/ @@ -98,6 +98,22 @@ theorem separate_6 {n : Nat} (hn : n ≠ 0) /-- info: 'MemSeparate.separate_6' depends on axioms: [propext, Classical.choice, Quot.sound] -/ #guard_msgs in #print axioms separate_6 +/-- error: ❌️ simp_mem failed to make any progress. -/ +#guard_msgs in theorem separate_7 (hm : m ≠ 0) + (l : mem_separate' a 100 b m) + (l : mem_separate' (a+100) 100 b m) : + mem_separate' a 200 b m := by + simp_mem /- Need better address normalization. -/ + trace_state + +/-- error: ❌️ simp_mem failed to make any progress. -/ +#guard_msgs in theorem separate_8 {n : Nat} (hn : n ≠ 0) (hm : m ≠ 0) + (l : mem_separate' a n b m) + (l : mem_separate' (a+n) n b m) : + mem_separate' a (2*n) b m := by + simp_mem /- Need better address normalization. -/ + trace_state + end MemSeparate @@ -159,7 +175,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; -- TODO: repeat on change. + simp_mem congr 1 bv_omega' -- TODO: address normalization. @@ -366,17 +382,35 @@ theorem mem_separate_move_of_lt_of_le (h : mem_separate' a an b bn) end MathProperties + + +section PairwiseSeparate + /- Check that a direct implication of the pairwise separation is proven. -/ + theorem pairwise_direct (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) : + mem_separate' a 100 b 200 := by + simp_mem + + /- Check that a direct implication of the pairwise separation is proven. -/ + theorem pairwise_subset (h : Memory.Region.pairwiseSeparate [⟨a, 100⟩, ⟨b, 200⟩, ⟨c, 300⟩, ⟨d, 400⟩]) : + mem_separate' a 80 b 100 := by + simp_mem + +end PairwiseSeparate + namespace MemOptions +set_option trace.simp_mem true in +set_option trace.simp_mem.info true in /-- error: unsolved goals ⊢ False --- info: [simp_mem.info] Searching for Hypotheses [simp_mem.info] Summary: Found 0 hypotheses +[simp_mem.info] ⚙️ Matching on ⊢ False [simp_mem.info] Performing Rewrite At Main Goal - [simp_mem.info] ⚙️ Matching on ⊢ False [simp_mem.info] Simplifying goal. +[simp_mem.info] ❌️ No progress made in this iteration. halting. --- info: ⊢ False -/ @@ -384,14 +418,17 @@ info: ⊢ False simp_mem (config := { failIfUnchanged := false }) trace_state +set_option trace.simp_mem true in +set_option trace.simp_mem.info true in /-- -error: ❌️ simp_mem failed to make progress. +error: ❌️ simp_mem failed to make any progress. --- info: [simp_mem.info] Searching for Hypotheses [simp_mem.info] Summary: Found 0 hypotheses +[simp_mem.info] ⚙️ Matching on ⊢ False [simp_mem.info] Performing Rewrite At Main Goal - [simp_mem.info] ⚙️ Matching on ⊢ False [simp_mem.info] Simplifying goal. +[simp_mem.info] ❌️ No progress made in this iteration. halting. -/ #guard_msgs in theorem test_fail_if_unchanged : False := by simp_mem