From b42093cd54b64d85dbc35c5b2da6e7b7b77f380e Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Sun, 18 Aug 2024 21:46:50 -0500 Subject: [PATCH] add mem_separate examples --- Arm/Memory/Separate.lean | 2 +- Arm/Memory/SeparateAutomation.lean | 90 +++++++++++++++++++++++--- Proofs/Experiments/MemoryAliasing.lean | 46 ++++++++++++- 3 files changed, 127 insertions(+), 11 deletions(-) diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean index d3c5d3c3..422cfbcc 100644 --- a/Arm/Memory/Separate.lean +++ b/Arm/Memory/Separate.lean @@ -378,7 +378,7 @@ theorem mem_separate'.omega_def (h : mem_separate' a an b bn) : theorem mem_separate'.of_omega (h :a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ - (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn) := by omega) : + (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) : mem_separate' a an b bn := by constructor · unfold mem_legal'; omega diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 4df160b2..a9df1435 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -150,6 +150,9 @@ instance : ToMessageData MemSeparateExpr where abbrev MemSeparateProof := WithWitness MemSeparateExpr +def MemSeparateProof.mk {e : MemSeparateExpr} (h : Expr) : MemSeparateProof e := + { h } + abbrev MemLegalProof := WithWitness MemLegalExpr @@ -334,7 +337,7 @@ def MemLegalProof.def (h : MemLegalProof e) : Expr := def MemLegalProof.addOmegaFacts (h : MemLegalProof e) (args : Array Expr) : SimpMemM (Array Expr) := do SimpMemM.withMainContext do - let fvar ← introDef "memLegal_omegaH" h.def + let fvar ← introDef "hmemLegal_omega" h.def trace[simp_mem.info] "{h}: added omega fact ({h.def})" return args.push (Expr.fvar fvar) @@ -356,7 +359,23 @@ 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 "memSubset_omegaH" h.omega_def + let fvar ← introDef "hmemSubset_omega" h.omega_def + trace[simp_mem.info] "{h}: added omega fact ({h.omega_def})" + return args.push (Expr.fvar fvar) + +/-- +Build a term corresponding to `mem_separate'.omega_def` which has facts written +in a style that is exploitable by omega. +-/ +def MemSeparateProof.omega_def (h : MemSeparateProof e) : Expr := + mkAppN (Expr.const ``mem_separate'.omega_def []) + #[e.sa.base, e.sa.n, e.sb.base, e.sb.n, h.h] + +/-- Add the omega fact from `mem_legal'.def` and run the rest of the continuation. -/ +def MemSeparateProof.addOmegaFacts (h : MemSeparateProof e) (args : Array Expr) : + SimpMemM (Array Expr) := do + SimpMemM.withMainContext do + let fvar ← introDef "hmemSeparate_omega" h.omega_def trace[simp_mem.info] "{h}: added omega fact ({h.omega_def})" return args.push (Expr.fvar fvar) @@ -367,7 +386,7 @@ def Hypothesis.addOmegaFactsOfHyp (h : Hypothesis) (args : Array Expr) : SimpMem match h with | Hypothesis.legal h => h.addOmegaFacts args | Hypothesis.subset h => h.addOmegaFacts args - | _ => return args + | Hypothesis.separate h => h.addOmegaFacts args /-- Accumulate all omega defs in `args` and finally call the continuation `k` @@ -465,10 +484,59 @@ def proveMemSubsetWithOmega? (subset : MemSubsetExpr) trace[simp_mem.info] "{checkEmoji} `omega` succeeded." return (.some <| MemSubsetProof.mk (← instantiateMVars ofOmegaVal)) catch e => + -- | TODO: raise `e`. trace[simp_mem.info] "{crossEmoji} `omega` failed with error:\n{e.toMessageData}" return none end MemSubset + +section MemSeparate + +/-- +info: mem_subset'.of_omega {an bn : Nat} {a b : BitVec 64} + (h : a.toNat + an ≤ 2 ^ 64 ∧ b.toNat + bn ≤ 2 ^ 64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) : + mem_subset' a an b bn +-/ +#guard_msgs in #check mem_subset'.of_omega + + +/-- +Try to prove that the memory subset is legal by reducing the problem to `omega`. +Eventually, this will be supplemented by heuristics. +-/ +def proveMemSeparateWithOmega? (e : MemSeparateExpr) + (hyps : Array Hypothesis) : SimpMemM (Option (MemSeparateProof e)) := do + -- [a..n) + let a := e.sa.base + let an := e.sa.n + let b := e.sb.base + let bn := e.sb.n + let ofOmegaVal := mkAppN (Expr.const ``mem_separate'.of_omega []) #[an, bn, a, b] + let ofOmegaTy ← inferType ofOmegaVal + trace[simp_mem.info] "partially applied: '{ofOmegaVal} : {ofOmegaTy}'" + let omegaObligationTy ← do + match ofOmegaTy with + | Expr.forallE _argName argTy _body _binderInfo => pure argTy + | _ => throwError "expected '{ofOmegaTy}' to a ∀" + trace[simp_mem.info] "omega obligation '{omegaObligationTy}'" + let omegaGoal ← mkFreshExprMVar (type? := omegaObligationTy) + let ofOmegaVal := mkAppN ofOmegaVal #[omegaGoal] + + try + setGoals (omegaGoal.mvarId! :: (← getGoals)) + SimpMemM.withMainContext do + let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[] + trace[simp_mem.info] "Executing `omega` to close {e}" + trace[simp_mem.info] "{← getMainGoal}" + omega + trace[simp_mem.info] "{checkEmoji} `omega` succeeded." + return (.some <| MemSeparateProof.mk (← instantiateMVars ofOmegaVal)) + catch e => + trace[simp_mem.info] "{crossEmoji} `omega` failed with error:\n{e.toMessageData}" + return none + +end MemSeparate + -- /-- info: mem_legal' (a : BitVec 64) (n : Nat) : Prop -/ -- #guard_msgs in #check mem_legal' @@ -476,13 +544,17 @@ partial def SimpMemM.improveGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMe SimpMemM.withMainContext do trace[simp_mem.info] "{processingEmoji} Matching on ⊢ {← g.getType}" let gt ← g.getType - if let .some legal := MemLegalExpr.match? gt then do - withTraceNode `simp_mem.info (fun _ => return m!"Matched on ⊢ {legal}. Proving...") do - if let .some proof ← proveMemLegalWithOmega? legal hyps then do + if let .some e := MemLegalExpr.match? gt then do + withTraceNode `simp_mem.info (fun _ => return m!"Matched on ⊢ {e}. Proving...") do + if let .some proof ← proveMemLegalWithOmega? e hyps then do + (← getMainGoal).assign proof.h + if let .some e := MemSubsetExpr.match? gt then do + withTraceNode `simp_mem.info (fun _ => return m!"Matched on ⊢ {e}. Proving...") do + if let .some proof ← proveMemSubsetWithOmega? e hyps then do (← getMainGoal).assign proof.h - if let .some legal := MemSubsetExpr.match? gt then do - withTraceNode `simp_mem.info (fun _ => return m!"Matched on ⊢ {legal}. Proving...") do - if let .some proof ← proveMemSubsetWithOmega? legal hyps then do + if let .some e := MemSeparateExpr.match? gt then do + 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 -- let some (_, _lhs, _rhs) ← matchEq? (← g.getType) | throwError "invalid goal, expected 'lhs = rhs'." diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index 5e2a9d4c..3b8fd459 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -24,7 +24,7 @@ theorem legal_1 (l : mem_legal' a 16) : mem_legal' a 16 := by end MemLegal namespace MemSubset -/-- Show reflexivity of subset. -/ +/-- Reflexivity. -/ theorem subset_1 (l : mem_subset' a 16 b 16) : mem_subset' a 16 b 16 := by simp_mem @@ -47,6 +47,50 @@ theorem subset_3 (l : mem_subset' a 16 b 16) : mem_subset' (a+6) 10 b 16 := by end MemSubset +namespace MemSeparate + +/-- Reflexivity. -/ +theorem separate_1 (l : mem_separate' a 16 b 16) : mem_separate' a 16 b 16 := by + simp_mem + +/-- info: 'MemSeparate.separate_1' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in #print axioms separate_1 + + +/-- Symmetry. -/ +theorem separate_2 (l : mem_separate' a 16 b 16) : mem_separate' b 16 a 16 := by + simp_mem + +/-- info: 'MemSeparate.separate_2' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in #print axioms separate_2 + +/-- Smaller subsets. -/ +theorem separate_3 (l : mem_separate' a 16 b 16) : mem_separate' b 10 a 10 := by + simp_mem + +/-- sliding subset to the right. -/ +theorem separate_4 (l : mem_separate' a 16 b 16) (hab : a < b) : + mem_separate' a 17 (b+1) 15 := by + simp_mem + +/-- shifts inside the arithmetic. -/ +theorem separate_5 {n : Nat} (hn : n ≠ 0) + (l : mem_separate' a (n <<< 4) b (n <<< 4)) : + mem_separate' a 16 b 16 := by + simp_mem + +/-- shifts inside the arithmetic. -/ +theorem separate_6 {n : Nat} (hn : n ≠ 0) + (l : mem_separate' a (n <<< 4) b (n <<< 4)) : + mem_separate' a (n <<< 3 + 8) b (n <<< 4) := by + simp_mem + +/-- info: 'MemSeparate.separate_2' depends on axioms: [propext, Classical.choice, Quot.sound] -/ +#guard_msgs in #print axioms separate_2 + + +end MemSeparate + namespace MemSeparate end MemSeparate