From ae0d4c0b6e1d1544d365ab207c75a933ffd7875d Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 2 Oct 2024 15:04:12 -0500 Subject: [PATCH 01/11] feat: package up logic that writes cutpoint assertions in terms of run. --- Correctness/Correctness.lean | 37 ++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/Correctness/Correctness.lean b/Correctness/Correctness.lean index 1ec8b9c9..cb384a2f 100644 --- a/Correctness/Correctness.lean +++ b/Correctness/Correctness.lean @@ -216,6 +216,43 @@ theorem partial_correctness_from_verification_conditions [Sys σ] [Spec' σ] ⟨n, Nat.le_refl _, hexit, hpost⟩ find 0 (v1 s0 hp) (Nat.zero_le ..) + +/-- +Prove partial correctness using inductive assertions and functions +`csteps` and `nextc`. + +We use `s0`, `si`, and `sf` to refer to initial, intermediate, and +final (exit) states respectively. + +This is Theorem 1 from page 5 of the paper. This proof method is more +convenient to use than `partial_correctness_by_stepwise_invariants` +because we need only attach assertions at certain cutpoints. However, +it may still be tedious to use from the point of view of automation +because it is difficult to both symbolically simulate an instruction +and unwind `csteps` in tandem. So far, we have found that it is +easiest to determine what concrete value `csteps` yields (via symbolic +simulation), and then perform symbolic simulation -- however, then we +end up doing simulation twice, which is expensive. + +Also see `partial_correctness_from_assertions`. +-/ +theorem partial_correctness_from_verification_conditions_concrete_num_steps [Sys σ] [Spec' σ] + (csteps' : σ → Nat) -- a computable function that tells us the number of steps. + (hnsteps : ∀ (s0 si : σ), (hs : assert s0 si) → + run si (csteps' si) = (nextc (run si 1))) -- csteps' si is the steps till the next cutpoint. + (v1 : ∀ s0 : σ, pre s0 → assert s0 s0) + (v2 : ∀ sf : σ, exit sf → cut sf) + (v3 : ∀ s0 sf : σ, assert s0 sf → exit sf → post s0 sf) + -- We use `run` since it plays well with `sym_n` proof automation. + (v4 : ∀ s0 si : σ, assert s0 si → ¬ exit si → assert s0 (run si (csteps' si))) + : PartialCorrectness σ := by + intro s0 n hp hexit + apply partial_correctness_from_verification_conditions <;> try assumption + intros s0' si' hassert' hexit' + specialize (v4 s0' si' hassert' hexit') + rw [← hnsteps s0' si' hassert'] + exact v4 + ---------------------------------------------------------------------- /-! From a065c9e407278b67972ffb95c26f3f2db0dc108c Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 2 Oct 2024 15:11:20 -0500 Subject: [PATCH 02/11] chore: add ability to trace a single simp_mem --- Arm/Memory/SeparateAutomation.lean | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 88b3c8da..419cfcfb 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -101,6 +101,8 @@ end BvOmega namespace SeparateAutomation structure SimpMemConfig where + /-- Locally turn on tracing for this particular invocation of 'simp_mem'. -/ + trace : Bool := false /-- number of times rewrites must be performed. -/ rewriteFuel : Nat := 1000 /-- whether an error should be thrown if the tactic makes no progress. -/ @@ -349,8 +351,11 @@ def State.init (cfg : SimpMemConfig) : State := abbrev SimpMemM := StateRefT State (ReaderT Context TacticM) -def SimpMemM.run (m : SimpMemM α) (cfg : SimpMemConfig) : TacticM α := - m.run' (State.init cfg) |>.run (Context.init cfg) +def SimpMemM.run (m : SimpMemM α) (cfg : SimpMemConfig) : TacticM α := do + let insertTraceIfEnabled := fun (opts : Options) => + if cfg.trace then opts.insert `simp_mem.trace.info true else opts + withOptions insertTraceIfEnabled do + m.run' (State.init cfg) |>.run (Context.init cfg) /-- Add a `Hypothesis` to our hypothesis cache. -/ def SimpMemM.addHypothesis (h : Hypothesis) : SimpMemM Unit := From b0a63a255017554b01bf87acb6b7bc6232efa717 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 2 Oct 2024 15:16:51 -0500 Subject: [PATCH 03/11] add syntax categories for finer grained simp_mem usage --- Arm/Memory/SeparateAutomation.lean | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 419cfcfb..a4ecb5b5 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -1082,14 +1082,32 @@ Allow elaboration of `SimpMemConfig` arguments to tactics. -/ declare_config_elab elabSimpMemConfig SeparateAutomation.SimpMemConfig +/-- +Direct `simp_mem` to assume certain memory relationships when trying to rewrite the context. +· ⟂w direct `simp_mem` to assume that the write is separated from the read. +· ⊆w directs `simp_mem` to assume that the read is a subset of a write. +· ⊆r directs `simp_mem` to assume that the read is a subset of a read in the hypothesis. +-/ +syntax simpMemTarget := "⟂w" <|> "⊆w" <|> "⊆r" + /-- Implement the simp_mem tactic frontend. -/ -syntax (name := simp_mem) "simp_mem" (Lean.Parser.Tactic.config)? : tactic +syntax (name := simp_mem) "simp_mem" (Lean.Parser.Tactic.config)? (simpMemTarget)? : tactic + @[tactic simp_mem] def evalSimpMem : Tactic := fun | `(tactic| simp_mem $[$cfg]?) => do let cfg ← elabSimpMemConfig (mkOptionalNode cfg) SeparateAutomation.simpMemTactic cfg + | `(tactic| simp_mem $[$cfg]? ⟂w) => do + let cfg ← elabSimpMemConfig (mkOptionalNode cfg) + SeparateAutomation.simpMemTactic cfg + | `(tactic| simp_mem $[$cfg]? ⊆w) => do + let cfg ← elabSimpMemConfig (mkOptionalNode cfg) + SeparateAutomation.simpMemTactic cfg + | `(tactic| simp_mem $[$cfg]? ⊆r) => do + let cfg ← elabSimpMemConfig (mkOptionalNode cfg) + SeparateAutomation.simpMemTactic cfg | _ => throwUnsupportedSyntax From 73e9d7f345fd28d685cab62cebabc5d488f7ccb8 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 2 Oct 2024 15:33:12 -0500 Subject: [PATCH 04/11] chore: introduce mem_omega to dispatch purely omega-based closing reasoning --- Arm/Memory/SeparateAutomation.lean | 62 ++++++++++++------------ Proofs/AES-GCM/GCMGmultV8Sym.lean | 2 +- Proofs/Experiments/Memcpy/MemCpyVCG.lean | 2 +- Proofs/Experiments/MemoryAliasing.lean | 6 +-- Proofs/Popcount32.lean | 2 +- Proofs/SHA512/SHA512Prelude.lean | 2 +- 6 files changed, 39 insertions(+), 37 deletions(-) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index a4ecb5b5..d7bd40ac 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -107,18 +107,6 @@ structure SimpMemConfig where rewriteFuel : Nat := 1000 /-- whether an error should be thrown if the tactic makes no progress. -/ failIfUnchanged : Bool := true - /-- whether `simp_mem` should always try to use `omega` to close the goal, - even if goal state is not recognized as one of the blessed states. - This is useful when one is trying to establish some numerical invariant - about addresses based on knowledge of memory. - e.g. - ``` - h : mem_separate' a 10 b 10 - hab : a < b - ⊢ a + 5 < b - ``` - -/ - useOmegaToClose : Bool := false /-- Context for the `SimpMemM` monad, containing the user configurable options. -/ structure Context where @@ -988,24 +976,6 @@ partial def SimpMemM.closeGoal (g : MVarId) (hyps : Array Hypothesis) : SimpMemM withTraceNode m!"Matched on ⊢ {e}. Proving..." do if let .some proof ← proveWithOmega? e hyps then g.assign proof.h - - if (← getConfig).useOmegaToClose then - withTraceNode m!"Unknown memory expression ⊢ {gt}. Trying reduction to omega (`config.useOmegaToClose = true`):" do - let oldGoals := (← getGoals) - try - let gproof ← mkFreshExprMVar (type? := gt) - setGoals (gproof.mvarId! :: (← getGoals)) - SimpMemM.withMainContext do - let _ ← Hypothesis.addOmegaFactsOfHyps hyps.toList #[] - trace[simp_mem.info] m!"Executing `omega` to close {gt}" - SimpMemM.withTraceNode m!"goal (Note: can be large)" do - trace[simp_mem.info] "{← getMainGoal}" - omega - trace[simp_mem.info] "{checkEmoji} `omega` succeeded." - g.assign gproof - catch e => - trace[simp_mem.info] "{crossEmoji} `omega` failed with error:\n{e.toMessageData}" - setGoals oldGoals return ← g.isAssigned @@ -1075,6 +1045,27 @@ def simpMem (cfg : SimpMemConfig := {}) : TacticM Unit := do /-- The `simp_mem` tactic, for simplifying away statements about memory. -/ def simpMemTactic (cfg : SimpMemConfig) : TacticM Unit := simpMem cfg +/-- The `mem_omega` finishing tactic, to close arithmetic related goals about memory addresses. -/ +def memOmegaTactic : TacticM Unit := do + SimpMemM.run (cfg := {}) do + let g ← getMainGoal + g.withContext do + let hyps := (← getLocalHyps) + let foundHyps ← SimpMemM.withTraceNode m!"Searching for Hypotheses" do + let mut foundHyps : Array Hypothesis := #[] + for h in hyps do + foundHyps ← hypothesisOfExpr h foundHyps + pure foundHyps + + SimpMemM.withMainContext do + let _ ← Hypothesis.addOmegaFactsOfHyps foundHyps.toList #[] + trace[simp_mem.info] m!"Executing `omega` to close goal." + SimpMemM.withTraceNode m!"goal (Note: can be large)" do + trace[simp_mem.info] "{← getMainGoal}" + omega + trace[simp_mem.info] "{checkEmoji} `omega` succeeded." + return () + end SeparateAutomation /-- @@ -1095,6 +1086,11 @@ Implement the simp_mem tactic frontend. -/ syntax (name := simp_mem) "simp_mem" (Lean.Parser.Tactic.config)? (simpMemTarget)? : tactic +/-- +Use the `simp_mem` preprocessing to automatically close goals that involve +reasoning about addresses in memory. +-/ +syntax (name := mem_omega) "mem_omega" : tactic @[tactic simp_mem] def evalSimpMem : Tactic := fun @@ -1111,3 +1107,9 @@ def evalSimpMem : Tactic := fun let cfg ← elabSimpMemConfig (mkOptionalNode cfg) SeparateAutomation.simpMemTactic cfg | _ => throwUnsupportedSyntax + +@[tactic mem_omega] +def evalMemOmega : Tactic := fun +| `(tactic| mem_omega) => + SeparateAutomation.memOmegaTactic +| _ => throwUnsupportedSyntax diff --git a/Proofs/AES-GCM/GCMGmultV8Sym.lean b/Proofs/AES-GCM/GCMGmultV8Sym.lean index 6a5ecc7a..57ee57a5 100644 --- a/Proofs/AES-GCM/GCMGmultV8Sym.lean +++ b/Proofs/AES-GCM/GCMGmultV8Sym.lean @@ -91,7 +91,7 @@ theorem gcm_gmult_v8_program_run_27 (s0 sf : ArmState) · simp only [List.mem_cons, List.mem_singleton, not_or, and_imp] sym_aggregate · intro n addr h_separate - simp_mem (config := { useOmegaToClose := false }) + simp_mem -- Aggregate the memory (non)effects. simp only [*] done diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean index 76eeff7e..f990ca32 100644 --- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean +++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean @@ -471,7 +471,7 @@ theorem Memcpy.extracted_2 (s0 si : ArmState) have h_upper_bound := hsep.hb.omega_def have h_upper_bound₂ := h_pre_1.hb.omega_def have h_upper_bound₃ := hsep.ha.omega_def - have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by simp_mem (config := {useOmegaToClose := true}) + have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by mem_omega rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] · rw [h_assert_6] skip_proof simp_mem diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index a357172c..4a252d0e 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -47,7 +47,7 @@ theorem subset_3 (l : mem_subset' a 16 b 16) : mem_subset' (a+6) 10 b 16 := by /-- Show that we can perform address arithmetic based on subset constraints. -/ theorem subset_4 (l : mem_subset' a 16 b 16) : a = b := by - simp_mem (config := {useOmegaToClose := true}) + mem_omega /-- Show that we can perform address arithmetic based on subset constraints. Only two configurations possible: @@ -59,7 +59,7 @@ a0 a1 a2 .. b0 b1 b2 b3 -/ theorem subset_5 (l : mem_subset' a 3 b 4) : a ≤ b + 1 := by - simp_mem (config := {useOmegaToClose := true}) + mem_omega end MemSubset @@ -135,7 +135,7 @@ us to exploit memory separateness properties. -/ theorem mem_separate_9 (h : mem_separate' a 100 b 100) (hab : a < b) : a + 50 ≤ b := by - simp_mem (config := {useOmegaToClose := true}) + mem_omega end MemSeparate diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean index a00aa992..10ef79a4 100644 --- a/Proofs/Popcount32.lean +++ b/Proofs/Popcount32.lean @@ -103,7 +103,7 @@ theorem popcount32_sym_meets_spec (s0 sf : ArmState) · -- Memory Frame Condition intro n addr h_separate simp only [memory_rules] at * - repeat (simp_mem (config := { useOmegaToClose := false }); sym_aggregate) + repeat (simp_mem; sym_aggregate) done /-- diff --git a/Proofs/SHA512/SHA512Prelude.lean b/Proofs/SHA512/SHA512Prelude.lean index 78a10f98..3a30429d 100644 --- a/Proofs/SHA512/SHA512Prelude.lean +++ b/Proofs/SHA512/SHA512Prelude.lean @@ -182,7 +182,7 @@ theorem sha512_block_armv8_prelude (s0 sf : ArmState) · constructor · -- (TODO @bollu) Think about whether `simp_mem` should be powerful enough to solve this goal. -- Also, `mem_omega` name suggestion from Alex for the already souped up `simp_mem`. - simp_mem (config := { useOmegaToClose := false } ) + simp_mem simp only [h_s0_ctx_base, Nat.sub_self, minimal_theory, bitvec_rules] · constructor · -- (FIXME @bollu) simp_mem doesn't make progress here. :-( From c592dfbca6a16644bd485fe4ba4efba72ab570b0 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 2 Oct 2024 16:21:22 -0500 Subject: [PATCH 05/11] chore: cleanup simplifyExpr in simp_mem to allow for targeted usage --- Arm/Memory/SeparateAutomation.lean | 175 +++++++++++++++++++++-------- 1 file changed, 128 insertions(+), 47 deletions(-) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index d7bd40ac..2dffa418 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -15,6 +15,8 @@ import Arm.BitVec import Arm.Memory.Attr import Arm.Memory.AddressNormalization import Lean +import Lean.Meta.ForEachExpr +import Lean.Meta.ExprTraverse import Lean.Meta.Tactic.Rewrite import Lean.Meta.Tactic.Rewrites import Lean.Elab.Tactic.Conv @@ -333,6 +335,7 @@ instance : ToMessageData Hypothesis where structure State where hypotheses : Array Hypothesis := #[] rewriteFuel : Nat + changed : Bool := false def State.init (cfg : SimpMemConfig) : State := { rewriteFuel := cfg.rewriteFuel} @@ -806,6 +809,53 @@ def SimpMemM.rewriteWithEquality (rw : Expr) (msg : MessageData) : SimpMemM Unit throwError m!"{crossEmoji} internal error: expected rewrite to produce no side conditions. Produced {result.mvarIds}" replaceMainGoal [mvarId'] +/-- +Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`. + +Rewrites with a fresh metavariable as the ambient goal. +Fails if the rewrite produces any subgoals. +-/ +-- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477 +private def rewrite (e eq : Expr) : MetaM Expr := do + let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq + | throwError "Expr.rewrite may not produce subgoals." + return eq' + +/-- +Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`. + +Rewrites with a fresh metavariable as the ambient goal. +Fails if the rewrite produces any subgoals. +-/ +-- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477 +private def rewriteType (e eq : Expr) : MetaM Expr := do + mkEqMP (← rewrite (← inferType e) eq) e + +-- def ppExprWithInfos (ctx : PPContext) (e : Expr) (msg : MessageData) : MetaM FormatWithInfos := do +-- let out : FormatWithInfos := { +-- fmt := format (toString e), +-- infos := RBMap.empty.insert 0 (.ofTermInfo { expr := e, lctx := ← getLCtx }) +-- } +-- return out + +-- def mkExprTraceNode (e : Expr) (msg : MessageData) : MessageData := +-- MessageData.ofLazy +-- (fun ctx? => do +-- let msg ← MessageData.ofFormatWithInfos <$> match ctx? with +-- | .none => pure (format (toString e)) +-- | .some ctx => ppExprWithInfos ctx e msg +-- return Dynamic.mk msg) +-- (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry) + +def SimpMemM.rewriteWithEqualityAtTarget (rw : Expr) (targetExpr : Expr) (msg : MessageData) : SimpMemM Expr := do + withTraceNode msg do + withMainContext do + withTraceNode m!"rewrite (Note: can be large)" do + trace[simp_mem.info] "{← inferType rw}" + let targetExpr' ← rewriteType targetExpr rw + return targetExpr' + + /-- info: Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate' {x : BitVec 64} {xn : Nat} {y : BitVec 64} {yn : Nat} {mem : Memory} (hsep : mem_separate' x xn y yn) (val : BitVec (yn * 8)) : @@ -865,6 +915,11 @@ def SimpMemM.rewriteReadOfSubsetWrite ew.val] SimpMemM.rewriteWithEquality call m!"rewriting read({er})⊆write({ew})" + +structure SimplifyExprResult where + e : Expr + changed : Bool + mutual /-- @@ -872,7 +927,13 @@ 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 Bool := do +partial def SimpMemM.simplifyExpr + (e : Expr) + (hyps : Array Hypothesis) + (useSeparate : Bool := false) + (useSubset : Bool := false) + (useOverlappingRead : Bool := false) + : SimpMemM Bool := do consumeRewriteFuel if ← outofRewriteFuel? then trace[simp_mem.info] "out of fuel for rewriting, stopping." @@ -883,75 +944,71 @@ partial def SimpMemM.simplifyExpr (e : Expr) (hyps : Array Hypothesis) : SimpMem return false if let .some er := ReadBytesExpr.ofExpr? e then + trace[simp_mem.info] "{checkEmoji} Found read {er.span}." if let .some ew := WriteBytesExpr.ofExpr? er.mem then - trace[simp_mem.info] "{checkEmoji} Found read of write." - trace[simp_mem.info] "read: {er}" - trace[simp_mem.info] "write: {ew}" + trace[simp_mem.info] "{checkEmoji} Found read({er.span}) of write ({ew.span})." trace[simp_mem.info] "{processingEmoji} read({er.span})⟂/⊆write({ew.span})" let separate := MemSeparateProp.mk er.span ew.span let subset := MemSubsetProp.mk er.span ew.span - if let .some separateProof ← proveWithOmega? separate hyps then do - trace[simp_mem.info] "{checkEmoji} {separate}" - rewriteReadOfSeparatedWrite er ew separateProof - 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 false - else - -- read - trace[simp_mem.info] "{checkEmoji} Found read {er}." + if useSeparate then + if let .some separateProof ← proveWithOmega? separate hyps then do + trace[simp_mem.info] "{checkEmoji} {separate}" + rewriteReadOfSeparatedWrite er ew separateProof + return true + else + trace[simp_mem.info] "{crossEmoji} {separate}" + + if useSubset then + 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} {separate}" + + if useOverlappingRead then -- 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. - 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 - 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? + trace[simp_mem.info] m!"Searching for overlapping read {er.span}." + for hyp in hyps do + if let Hypothesis.read_eq hReadEq := hyp then do + trace[simp_mem.info] "{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 true + return false else if e.isForall then Lean.Meta.forallTelescope e fun xs b => do let mut changedInCurrentIter? := false for x in xs do - changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps) + changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps useSeparate useSubset useOverlappingRead) -- we may have a hypothesis like -- ∀ (x : read_mem (read_mem_bytes ...) ... = out). -- we want to simplify the *type* of x. - changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps) - changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps) + changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps useSeparate useSubset useOverlappingRead) + changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps useSeparate useSubset useOverlappingRead) return changedInCurrentIter? else if e.isLambda then Lean.Meta.lambdaTelescope e fun xs b => do let mut changedInCurrentIter? := false for x in xs do - changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps) - changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps) - changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps) + changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps useSeparate useSubset useOverlappingRead) + changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr (← inferType x) hyps useSeparate useSubset useOverlappingRead) + changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr b hyps useSeparate useSubset useOverlappingRead) return changedInCurrentIter? else -- check if we have expressions. match e with | .app f x => let mut changedInCurrentIter? := false - changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr f hyps) - changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps) + changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr f hyps useSeparate useSubset useOverlappingRead) + changedInCurrentIter? := changedInCurrentIter? || (← SimpMemM.simplifyExpr x hyps useSeparate useSubset useOverlappingRead) return changedInCurrentIter? | _ => return false @@ -989,7 +1046,7 @@ partial def SimpMemM.simplifyGoal (g : MVarId) (hyps : Array Hypothesis) : SimpM SimpMemM.withContext g do let gt ← g.getType let changedInCurrentIter? ← withTraceNode m!"Simplifying goal." do - SimpMemM.simplifyExpr (← whnf gt) hyps + SimpMemM.simplifyExpr (← whnf gt) hyps (useSeparate := true) (useSubset := true) (useOverlappingRead := true) return changedInCurrentIter? end @@ -1031,6 +1088,30 @@ partial def SimpMemM.simplifyLoop : SimpMemM Unit := do /- we haven't changed ever.. -/ if !changedInAnyIter? && (← getConfig).failIfUnchanged then throwError "{crossEmoji} simp_mem failed to make any progress." + +def simpMemSpecialized (useSeparate : Bool) (useSubset : Bool) (useOverlappingRead : Bool) : SimpMemM Unit := do + let g ← getMainGoal + let gt ← getMainTarget + g.withContext do + let hyps := (← getLocalHyps) + let foundHyps : Array Hypothesis ← SimpMemM.withTraceNode m!"Searching for Hypotheses" do + let mut foundHyps : Array Hypothesis := #[] + for h in hyps do + foundHyps ← hypothesisOfExpr h foundHyps + pure foundHyps + + SimpMemM.withTraceNode m!"Summary: Found {foundHyps.size} hypotheses" do + for (i, h) in foundHyps.toList.enum do + trace[simp_mem.info] m!"{i+1}) {h}" + + let changed? ← SimpMemM.simplifyExpr (← whnf gt) foundHyps (useSeparate := useSeparate) (useSubset := useSubset) (useOverlappingRead := useOverlappingRead) + if !changed? then + throwError "{crossEmoji} simp_mem failed to make any progress." + + def simpMemSeparate : SimpMemM Unit := simpMemSpecialized (useSeparate := true) (useSubset := false) (useOverlappingRead := false) + def simpMemSubset : SimpMemM Unit := simpMemSpecialized (useSeparate := false) (useSubset := true) (useOverlappingRead := false) + def simpMemOverlappingRead : SimpMemM Unit := simpMemSpecialized (useSeparate := false) (useSubset := false) (useOverlappingRead := true) + end Simplify /-- @@ -1099,13 +1180,13 @@ def evalSimpMem : Tactic := fun SeparateAutomation.simpMemTactic cfg | `(tactic| simp_mem $[$cfg]? ⟂w) => do let cfg ← elabSimpMemConfig (mkOptionalNode cfg) - SeparateAutomation.simpMemTactic cfg + SeparateAutomation.SimpMemM.run SeparateAutomation.simpMemSeparate cfg | `(tactic| simp_mem $[$cfg]? ⊆w) => do let cfg ← elabSimpMemConfig (mkOptionalNode cfg) - SeparateAutomation.simpMemTactic cfg + SeparateAutomation.SimpMemM.run SeparateAutomation.simpMemSubset cfg | `(tactic| simp_mem $[$cfg]? ⊆r) => do let cfg ← elabSimpMemConfig (mkOptionalNode cfg) - SeparateAutomation.simpMemTactic cfg + SeparateAutomation.SimpMemM.run SeparateAutomation.simpMemOverlappingRead cfg | _ => throwUnsupportedSyntax @[tactic mem_omega] From 3cbf022f3ff6fba4fa419d3655dc6a813d331e59 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 2 Oct 2024 16:46:46 -0500 Subject: [PATCH 06/11] chore: bench WTF is happening. Next step: write extensions to simp_mem to fail if omega is taking too long. --- Arm/Memory/SeparateAutomation.lean | 4 +- Proofs/Experiments/Memcpy/MemCpyVCG.lean | 60 +++++++++++++++++++++++- Proofs/Experiments/MemoryAliasing.lean | 9 ++-- Proofs/Popcount32.lean | 2 + 4 files changed, 67 insertions(+), 8 deletions(-) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 2dffa418..b25ee7e3 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -1160,7 +1160,7 @@ Direct `simp_mem` to assume certain memory relationships when trying to rewrite · ⊆w directs `simp_mem` to assume that the read is a subset of a write. · ⊆r directs `simp_mem` to assume that the read is a subset of a read in the hypothesis. -/ -syntax simpMemTarget := "⟂w" <|> "⊆w" <|> "⊆r" +syntax simpMemTarget := "⟂" <|> "⊆w" <|> "⊆r" /-- Implement the simp_mem tactic frontend. @@ -1178,7 +1178,7 @@ def evalSimpMem : Tactic := fun | `(tactic| simp_mem $[$cfg]?) => do let cfg ← elabSimpMemConfig (mkOptionalNode cfg) SeparateAutomation.simpMemTactic cfg - | `(tactic| simp_mem $[$cfg]? ⟂w) => do + | `(tactic| simp_mem $[$cfg]? ⟂) => do let cfg ← elabSimpMemConfig (mkOptionalNode cfg) SeparateAutomation.SimpMemM.run SeparateAutomation.simpMemSeparate cfg | `(tactic| simp_mem $[$cfg]? ⊆w) => do diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean index f990ca32..a4c74ac8 100644 --- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean +++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean @@ -440,9 +440,24 @@ end CutTheorems section PartialCorrectness +/- +tactic execution of Lean.Parser.Tactic.omega took 290ms +tactic execution of Lean.Parser.Tactic.omega took 1.81s +tactic execution of simp_mem took 751ms +tactic execution of Lean.Parser.Tactic.omega took 1.11s +tactic execution of Lean.Parser.Tactic.omega took 664ms +tactic execution of Lean.Parser.Tactic.omega took 676ms +instantiate metavars took 7.15s +share common exprs took 3.9s +type checking took 1.47s +process pre-definitions took 440ms +-/ -- set_option skip_proof.skip true in +set_option maxHeartbeats 0 in -- set_option trace.profiler true in -- set_option profiler true in +set_option trace.profiler true in +set_option profiler true in set_option maxHeartbeats 0 in theorem Memcpy.extracted_2 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) @@ -471,7 +486,8 @@ theorem Memcpy.extracted_2 (s0 si : ArmState) have h_upper_bound := hsep.hb.omega_def have h_upper_bound₂ := h_pre_1.hb.omega_def have h_upper_bound₃ := hsep.ha.omega_def - have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by mem_omega + have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by + mem_omega rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] · rw [h_assert_6] skip_proof simp_mem @@ -482,10 +498,37 @@ theorem Memcpy.extracted_2 (s0 si : ArmState) skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega · apply mem_subset'_refl hsep.hb + +/- +tactic execution of Lean.Parser.Tactic.omega took 1.54s +tactic execution of simp_mem took 274ms +tactic execution of Lean.Parser.Tactic.omega took 1.11s +tactic execution of simp_mem took 403ms +tactic execution of Lean.Parser.Tactic.omega took 302ms +tactic execution of Lean.Parser.Tactic.omega took 284ms +tactic execution of Lean.Parser.Tactic.omega took 4.25s +tactic execution of simp_mem took 1.96s +tactic execution of Lean.Parser.Tactic.omega took 8.95s +tactic execution of simp_mem took 1.68s +tactic execution of Lean.Parser.Tactic.omega took 102ms +tactic execution of Lean.Parser.Tactic.omega took 1.9s +tactic execution of simp_mem took 318ms +tactic execution of Lean.Parser.Tactic.omega took 322ms +tactic execution of Lean.Parser.Tactic.omega took 115ms +tactic execution of Lean.Parser.Tactic.omega took 101ms +instantiate metavars took 30s +share common exprs took 16.7s +fix level params took 118ms +type checking took 4.37s +process pre-definitions took 5.44s +-/ -- set_option skip_proof.skip true in set_option maxHeartbeats 0 in -- set_option trace.profiler true in -- set_option profiler true in +set_option trace.profiler true in +set_option profiler true in +set_option maxHeartbeats 0 in theorem Memcpy.extracted_0 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) @@ -554,9 +597,22 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) } · intros n addr hsep apply Memcpy.extracted_2 <;> assumption - +/- +tactic execution of Lean.Parser.Tactic.omega took 616ms +tactic execution of Lean.Parser.Tactic.omega took 1.1s +tactic execution of Lean.Parser.Tactic.assumption took 114ms +instantiate metavars took 14.7s +share common exprs took 1.94s +type checking took 988ms +-/ -- set_option trace.profiler true in -- set_option profiler true in +set_option maxHeartbeats 0 in +-- set_option trace.profiler true in +-- set_option profiler true in +set_option trace.profiler true in +set_option profiler true in +set_option maxHeartbeats 0 in theorem partial_correctness : PartialCorrectness ArmState := by apply Correctness.partial_correctness_from_assertions diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean index 4a252d0e..b601d1f0 100644 --- a/Proofs/Experiments/MemoryAliasing.lean +++ b/Proofs/Experiments/MemoryAliasing.lean @@ -161,7 +161,7 @@ theorem mem_automation_test_2 read_mem_bytes 16 src_addr (write_mem_bytes 16 dest_addr blah s0) = read_mem_bytes 16 src_addr s0 := by simp only [memory_rules] - simp_mem + simp_mem ⟂ rfl @@ -179,7 +179,7 @@ theorem mem_automation_test_3 read_mem_bytes 10 (src_addr + 1) (write_mem_bytes ignore_n ignore_addr blah s0) = read_mem_bytes 10 (src_addr + 1) s0 := by simp only [memory_rules] - simp_mem + simp_mem ⟂ rfl @@ -198,7 +198,8 @@ 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 ⟂ + simp_mem ⊆w congr 1 bv_omega -- TODO: address normalization. @@ -226,7 +227,7 @@ theorem overlapping_read_test_2 {out : BitVec (16 * 8)} (h : read_mem_bytes 16 src_addr s = out) : read_mem_bytes 10 (src_addr + 6) s = out.extractLsBytes 6 10 := by simp only [memory_rules] at h ⊢ - simp_mem + simp_mem ⊆r · congr -- ⊢ (src_addr + 6).toNat - src_addr.toNat = 6 bv_omega diff --git a/Proofs/Popcount32.lean b/Proofs/Popcount32.lean index 10ef79a4..1fdbd872 100644 --- a/Proofs/Popcount32.lean +++ b/Proofs/Popcount32.lean @@ -70,6 +70,8 @@ def popcount32_program : Program := #genStepEqTheorems popcount32_program +-- raw `simp_mem`: time: 4786ms +-- `simp_mem ⟂`: time: 4887ms theorem popcount32_sym_meets_spec (s0 sf : ArmState) (h_s0_pc : read_pc s0 = 0x4005b4#64) (h_s0_program : s0.program = popcount32_program) From 895bc0592dd5116fb05e13735bea77850e1c2b2f Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 2 Oct 2024 17:10:02 -0500 Subject: [PATCH 07/11] chore: extract out benchmark from omega slowdown --- Arm/Memory/SeparateAutomation.lean | 86 ++++++++++++++--------- Proofs/Experiments/Memcpy/MemCpyVCG.lean | 15 ++-- Proofs/Experiments/Memcpy/OmegaBench.lean | 55 +++++++++++++++ 3 files changed, 112 insertions(+), 44 deletions(-) create mode 100644 Proofs/Experiments/Memcpy/OmegaBench.lean diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index b25ee7e3..98bcec74 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -109,6 +109,14 @@ structure SimpMemConfig where rewriteFuel : Nat := 1000 /-- whether an error should be thrown if the tactic makes no progress. -/ failIfUnchanged : Bool := true + /-- Time that omega is allowed to take (in `ms`), before we raise a failure from `simp_mem`. -/ + omegaCutoffMs : Option Nat := .some 1000 + /-- In the sequence of `omega` calls made by `simp_mem`, if the `i`th omega call times out, + it will only throw an error if it's not in the "permitted failures" list. + This is useful to make progress on a proof while still permitting debugging of + omega timeouts. + -/ + omegaFailurePermittedOccs : Array Nat := #[] /-- Context for the `SimpMemM` monad, containing the user configurable options. -/ structure Context where @@ -336,6 +344,8 @@ structure State where hypotheses : Array Hypothesis := #[] rewriteFuel : Nat changed : Bool := false + -- Times taken by the `omega` tactic. + omegaTimingsMs : Array Nat := #[] def State.init (cfg : SimpMemConfig) : State := { rewriteFuel := cfg.rewriteFuel} @@ -422,12 +432,27 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId := do replaceMainGoal [goal] return fvar +def pushOmegaTiming (target : Expr) (ms : Nat) : SimpMemM Unit := do + let s ← get + let ix := s.omegaTimingsMs.size + if ms ≥ (← getConfig).omegaCutoffMs.get! then + if ix ∈ (← getConfig).omegaFailurePermittedOccs then + trace[simp_mem.info] m!"[simp_mem] omega tactic took too long ({ms}ms) to run, but this is a permitted failure at index '{ix}'." + throwError m!"[simp_mem] omega tactic took too long ({ms}ms) at index {ix}.{indentD target}" + + modify fun s => { s with omegaTimingsMs := s.omegaTimingsMs.push ms } + /-- SimpMemM's omega invoker -/ def omega : SimpMemM Unit := do + let target ← getMainTarget -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280 -- @bollu: TODO: understand what precisely we are recovering from. + let startTime ← IO.monoMsNow withoutRecover do + -- TODO: replace this with filling in an MVar, sure, but not like this. evalTactic (← `(tactic| bv_omega)) + let endTime ← IO.monoMsNow + pushOmegaTiming target (endTime - startTime) section Hypotheses @@ -789,7 +814,7 @@ def proveWithOmega? {α : Type} [ToMessageData α] [OmegaReducible α] (e : α) trace[simp_mem.info] "{checkEmoji} `omega` succeeded." return (.some <| Proof.mk (← instantiateMVars factProof)) catch e => - trace[simp_mem.info] "{crossEmoji} `omega` failed with error:\n{e.toMessageData}" + trace[simp_mem.info] "{crossEmoji} `omega` failed with error:{indentD e.toMessageData}" setGoals oldGoals return none end ReductionToOmega @@ -809,27 +834,27 @@ def SimpMemM.rewriteWithEquality (rw : Expr) (msg : MessageData) : SimpMemM Unit throwError m!"{crossEmoji} internal error: expected rewrite to produce no side conditions. Produced {result.mvarIds}" replaceMainGoal [mvarId'] -/-- -Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`. +-- /-- +-- Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`. -Rewrites with a fresh metavariable as the ambient goal. -Fails if the rewrite produces any subgoals. --/ --- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477 -private def rewrite (e eq : Expr) : MetaM Expr := do - let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq - | throwError "Expr.rewrite may not produce subgoals." - return eq' +-- Rewrites with a fresh metavariable as the ambient goal. +-- Fails if the rewrite produces any subgoals. +-- -/ +-- -- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477 +-- private def rewrite (e eq : Expr) : MetaM Expr := do +-- let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq +-- | throwError "Expr.rewrite may not produce subgoals." +-- return eq' -/-- -Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`. +-- /-- +-- Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`. -Rewrites with a fresh metavariable as the ambient goal. -Fails if the rewrite produces any subgoals. --/ --- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477 -private def rewriteType (e eq : Expr) : MetaM Expr := do - mkEqMP (← rewrite (← inferType e) eq) e +-- Rewrites with a fresh metavariable as the ambient goal. +-- Fails if the rewrite produces any subgoals. +-- -/ +-- -- source: https://github.com/leanprover-community/mathlib4/blob/b35703fe5a80f1fa74b82a2adc22f3631316a5b3/Mathlib/Lean/Expr/Basic.lean#L476-L477 +-- private def rewriteType (e eq : Expr) : MetaM Expr := do +-- mkEqMP (← rewrite (← inferType e) eq) e -- def ppExprWithInfos (ctx : PPContext) (e : Expr) (msg : MessageData) : MetaM FormatWithInfos := do -- let out : FormatWithInfos := { @@ -838,22 +863,13 @@ private def rewriteType (e eq : Expr) : MetaM Expr := do -- } -- return out --- def mkExprTraceNode (e : Expr) (msg : MessageData) : MessageData := --- MessageData.ofLazy --- (fun ctx? => do --- let msg ← MessageData.ofFormatWithInfos <$> match ctx? with --- | .none => pure (format (toString e)) --- | .some ctx => ppExprWithInfos ctx e msg --- return Dynamic.mk msg) --- (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry) - -def SimpMemM.rewriteWithEqualityAtTarget (rw : Expr) (targetExpr : Expr) (msg : MessageData) : SimpMemM Expr := do - withTraceNode msg do - withMainContext do - withTraceNode m!"rewrite (Note: can be large)" do - trace[simp_mem.info] "{← inferType rw}" - let targetExpr' ← rewriteType targetExpr rw - return targetExpr' +-- def SimpMemM.rewriteWithEqualityAtTarget (rw : Expr) (targetExpr : Expr) (msg : MessageData) : SimpMemM Expr := do +-- withTraceNode msg do +-- withMainContext do +-- withTraceNode m!"rewrite (Note: can be large)" do +-- trace[simp_mem.info] "{← inferType rw}" +-- let targetExpr' ← rewriteType targetExpr rw +-- return targetExpr' /-- diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean index a4c74ac8..7bd919a2 100644 --- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean +++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean @@ -456,9 +456,8 @@ process pre-definitions took 440ms set_option maxHeartbeats 0 in -- set_option trace.profiler true in -- set_option profiler true in -set_option trace.profiler true in -set_option profiler true in -set_option maxHeartbeats 0 in +-- set_option trace.profiler true in +-- set_option profiler true in theorem Memcpy.extracted_2 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) @@ -526,9 +525,8 @@ process pre-definitions took 5.44s set_option maxHeartbeats 0 in -- set_option trace.profiler true in -- set_option profiler true in -set_option trace.profiler true in -set_option profiler true in -set_option maxHeartbeats 0 in +-- set_option trace.profiler true in +-- set_option profiler true in theorem Memcpy.extracted_0 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) @@ -610,9 +608,8 @@ type checking took 988ms set_option maxHeartbeats 0 in -- set_option trace.profiler true in -- set_option profiler true in -set_option trace.profiler true in -set_option profiler true in -set_option maxHeartbeats 0 in +-- set_option trace.profiler true in +-- set_option profiler true in theorem partial_correctness : PartialCorrectness ArmState := by apply Correctness.partial_correctness_from_assertions diff --git a/Proofs/Experiments/Memcpy/OmegaBench.lean b/Proofs/Experiments/Memcpy/OmegaBench.lean new file mode 100644 index 00000000..9b441a32 --- /dev/null +++ b/Proofs/Experiments/Memcpy/OmegaBench.lean @@ -0,0 +1,55 @@ +import Arm +import Arm.Memory.SeparateAutomation + +/- +tactic execution of Lean.Parser.Tactic.omega took 6.04s +instantiate metavars took 31.6s +share common exprs took 5.61s +type checking took 1.36s +process pre-definitions took 1.02s +-/ +set_option maxHeartbeats 0 in +set_option trace.profiler true in +set_option profiler true in +theorem foo +(s0 si : ArmState) +(h_si_x0_nonzero : si.x0 ≠ 0) +(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) +(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) +(h_assert_1 : si.x0 ≤ s0.x0) +(h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0)) +(h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0)) +(h_assert_6 : ∀ (n : Nat) (addr : BitVec 64), + mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n → + Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem) +(h_assert_5 : ∀ (i : BitVec 64), + i < s0.x0 - si.x0 → + Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem) +(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16)) +(n : Nat) +(addr : BitVec 64) +(hsep : mem_separate' s0.x2 (0x10#64 * (s0.x0 - (si.x0 - 0x1#64))).toNat addr n) +(h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat) +(h_upper_bound : addr.toNat + n ≤ 2 ^ 64) +(h_upper_bound₂ : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(h_upper_bound₃ : s0.x2.toNat + (0x10#64 * (s0.x0 - (si.x0 - 0x1#64))).toNat ≤ 2 ^ 64) +(h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64) +(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16)) +(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemSeparate_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + si.x0.toNat) % 2 ^ 64 + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ + 2 ^ 64 ∧ + addr.toNat + n ≤ 2 ^ 64 ∧ + (s0.x2.toNat + + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + si.x0.toNat) % 2 ^ 64 + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ + addr.toNat ∨ + s0.x2.toNat ≥ addr.toNat + n)) +(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + si.x0.toNat) % 2 ^ 64 + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ + 2 ^ 64) +(hmemLegal_omega : addr.toNat + n ≤ 2 ^ 64) : + s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ 2 ^ 64 ∧ + addr.toNat + n ≤ 2 ^ 64 ∧ + (s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ addr.toNat ∨ s0.x2.toNat ≥ addr.toNat + n) := by + bv_omega From 2cb756ba9011e1148090a0c8d113a44a09caed2c Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Wed, 2 Oct 2024 18:23:51 -0500 Subject: [PATCH 08/11] chore: add slow examples, also see that instantiateMVars is uber slow --- Arm/Memory/Attr.lean | 17 +++++ Arm/Memory/SeparateAutomation.lean | 34 +++++----- Proofs/Experiments/Memcpy/MemCpyVCG.lean | 22 +++++-- .../OmegaBench/MemcpyExtracted0Line583.lean | 63 +++++++++++++++++++ .../OmegaBench/MemcpyExtracted0Line586.lean | 63 +++++++++++++++++++ .../MemcpyExtracted2.lean} | 13 ++-- 6 files changed, 185 insertions(+), 27 deletions(-) create mode 100644 Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean create mode 100644 Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line586.lean rename Proofs/Experiments/Memcpy/{OmegaBench.lean => OmegaBench/MemcpyExtracted2.lean} (92%) diff --git a/Arm/Memory/Attr.lean b/Arm/Memory/Attr.lean index b95cd9c4..810a65ec 100644 --- a/Arm/Memory/Attr.lean +++ b/Arm/Memory/Attr.lean @@ -23,3 +23,20 @@ register_simp_attr memory_omega -- Simprocs for address normalization register_simp_attr address_normalization + +register_option simp_mem.omegaTimeoutMs : Nat := { + defValue := 1000 + descr := "maximum amount of time per omega invocation in milliseconds before `simp_mem` times out. `0` for no timeout." +} + +register_option simp_mem.omegaNumIgnoredTimeouts: Nat := { + defValue := 0 + descr := "number of times omega is allowed to timeout before an error is thrown." +} + + +def getOmegaTimeoutMs [Monad m] [MonadOptions m] : m Nat := do + return simp_mem.omegaTimeoutMs.get (← getOptions) + +def getOmegaNumIgnoredTimeouts [Monad m] [MonadOptions m] : m Nat := do + return simp_mem.omegaNumIgnoredTimeouts.get (← getOptions) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 98bcec74..2a37e6fe 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -109,14 +109,6 @@ structure SimpMemConfig where rewriteFuel : Nat := 1000 /-- whether an error should be thrown if the tactic makes no progress. -/ failIfUnchanged : Bool := true - /-- Time that omega is allowed to take (in `ms`), before we raise a failure from `simp_mem`. -/ - omegaCutoffMs : Option Nat := .some 1000 - /-- In the sequence of `omega` calls made by `simp_mem`, if the `i`th omega call times out, - it will only throw an error if it's not in the "permitted failures" list. - This is useful to make progress on a proof while still permitting debugging of - omega timeouts. - -/ - omegaFailurePermittedOccs : Array Nat := #[] /-- Context for the `SimpMemM` monad, containing the user configurable options. -/ structure Context where @@ -344,8 +336,10 @@ structure State where hypotheses : Array Hypothesis := #[] rewriteFuel : Nat changed : Bool := false - -- Times taken by the `omega` tactic. + /-- Times taken by the `omega` tactic. -/ omegaTimingsMs : Array Nat := #[] + /-- Number of times omega has timed out. -/ + omegaNumTimeouts : Nat := 0 def State.init (cfg : SimpMemConfig) : State := { rewriteFuel := cfg.rewriteFuel} @@ -427,24 +421,26 @@ def simpAndIntroDef (name : String) (hdefVal : Expr) : SimpMemM FVarId := do let hdefVal ← simpResult.mkCast hdefVal let hdefTy ← inferType hdefVal - let goal ← goal.define name hdefTy hdefVal + let goal ← goal.assert name hdefTy hdefVal let (fvar, goal) ← goal.intro1P replaceMainGoal [goal] return fvar -def pushOmegaTiming (target : Expr) (ms : Nat) : SimpMemM Unit := do +def pushOmegaTiming (goal : MVarId) (ms : Nat) : SimpMemM Unit := do let s ← get - let ix := s.omegaTimingsMs.size - if ms ≥ (← getConfig).omegaCutoffMs.get! then - if ix ∈ (← getConfig).omegaFailurePermittedOccs then - trace[simp_mem.info] m!"[simp_mem] omega tactic took too long ({ms}ms) to run, but this is a permitted failure at index '{ix}'." - throwError m!"[simp_mem] omega tactic took too long ({ms}ms) at index {ix}.{indentD target}" + modify fun s => { s with omegaTimingsMs := s.omegaTimingsMs.push ms } + if ms ≥ (← getOmegaTimeoutMs) then + let numTimeouts := s.omegaNumTimeouts + 1 + modify fun s => { s with omegaNumTimeouts := numTimeouts } + if numTimeouts ≤ (← getOmegaNumIgnoredTimeouts) then + trace[simp_mem.info] m!"[simp_mem] 🚫 omega tactic took too long ({ms}ms) to run, but this is a permitted failure at occurrence {numTimeouts}. Goal: {indentD goal}" + else + throwError m!"[simp_mem] omega tactic took too long ({ms}ms) at occurrence {numTimeouts}. Goal: {indentD goal}" - modify fun s => { s with omegaTimingsMs := s.omegaTimingsMs.push ms } /-- SimpMemM's omega invoker -/ def omega : SimpMemM Unit := do - let target ← getMainTarget + let g ← getMainGoal -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280 -- @bollu: TODO: understand what precisely we are recovering from. let startTime ← IO.monoMsNow @@ -452,7 +448,7 @@ def omega : SimpMemM Unit := do -- TODO: replace this with filling in an MVar, sure, but not like this. evalTactic (← `(tactic| bv_omega)) let endTime ← IO.monoMsNow - pushOmegaTiming target (endTime - startTime) + pushOmegaTiming g (endTime - startTime) section Hypotheses diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean index 7bd919a2..172f1616 100644 --- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean +++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean @@ -458,6 +458,10 @@ set_option maxHeartbeats 0 in -- set_option profiler true in -- set_option trace.profiler true in -- set_option profiler true in +set_option trace.simp_mem true +set_option trace.simp_mem.info true +set_option simp_mem.omegaNumIgnoredTimeouts 0 in +set_option simp_mem.omegaTimeoutMs 1000 in theorem Memcpy.extracted_2 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) @@ -486,7 +490,7 @@ theorem Memcpy.extracted_2 (s0 si : ArmState) have h_upper_bound₂ := h_pre_1.hb.omega_def have h_upper_bound₃ := hsep.ha.omega_def have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by - mem_omega + sorry rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] · rw [h_assert_6] skip_proof simp_mem @@ -521,12 +525,17 @@ fix level params took 118ms type checking took 4.37s process pre-definitions took 5.44s -/ + +set_option maxHeartbeats 0 -- set_option skip_proof.skip true in set_option maxHeartbeats 0 in -- set_option trace.profiler true in -- set_option profiler true in -- set_option trace.profiler true in -- set_option profiler true in +set_option trace.simp_mem.info true +set_option simp_mem.omegaNumIgnoredTimeouts 9999 in +-- set_option simp_mem.omegaTimeoutMs 1000 in theorem Memcpy.extracted_0 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) @@ -595,6 +604,7 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) } · intros n addr hsep apply Memcpy.extracted_2 <;> assumption + /- tactic execution of Lean.Parser.Tactic.omega took 616ms tactic execution of Lean.Parser.Tactic.omega took 1.1s @@ -603,9 +613,13 @@ instantiate metavars took 14.7s share common exprs took 1.94s type checking took 988ms -/ --- set_option trace.profiler true in --- set_option profiler true in + +set_option maxHeartbeats 0 in +set_option trace.profiler true in +set_option profiler true in set_option maxHeartbeats 0 in +set_option trace.simp_mem.info true in +set_option simp_mem.omegaNumIgnoredTimeouts 9999 in -- set_option trace.profiler true in -- set_option profiler true in -- set_option trace.profiler true in @@ -726,7 +740,7 @@ theorem partial_correctness : simp only [memory_rules] at h_si_read_sep rw [h_si_read_sep] rw [h_si_x0_eq_zero] - skip_proof simp_mem -- nice! + skip_proof sorry -- nice! · simp only [step.h_err, step.h_program, step.h_sp_aligned, and_self] · have step_8f4_8e4 := program.step_8f4_8e4_of_wellformed_of_z_eq_0 si s1 si_well_formed diff --git a/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean new file mode 100644 index 00000000..7b012825 --- /dev/null +++ b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean @@ -0,0 +1,63 @@ +import Arm +import Arm.Memory.SeparateAutomation + +set_option maxHeartbeats 0 +set_option trace.profiler true +set_option profiler true + +/- +tactic execution of Lean.Parser.Tactic.omega took 3.67s +instantiate metavars took 15.3s +share common exprs took 3.28s +type checking took 742ms +process pre-definitions took 475ms +linting took 262ms +elaboration took 2.07s +-/ +theorem memcpy_extracted_0_line_585 +(s0 si : ArmState) +(h_si_x0_nonzero : si.x0 ≠ 0) +(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) +(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) +(h_assert_1 : si.x0 ≤ s0.x0) +(h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0)) +(h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0)) +(h_assert_6 : ∀ (n : Nat) (addr : BitVec 64), + mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n → + Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem) +(h_assert_5 : ∀ (i : BitVec 64), + i < s0.x0 - si.x0 → + Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem) +(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16)) +(h_pre_2 : r StateField.PC s0 = 0x8e0#64) +(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64) +(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16)) +(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16)) +(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hi : s0.x0 - si.x0 < s0.x0 - (si.x0 - 0x1#64)) +(i_sub_x0_mul_16 : 16 * (s0.x0 - si.x0).toNat < 16 * s0.x0.toNat) +(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16)) +(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧ + s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ + s0.x2.toNat + s0.x0.toNat * 16) +(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧ + s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧ + (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ + s0.x1.toNat + s0.x0.toNat * 16) +(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +: s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ 2 ^ 64 ∧ + (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧ + (s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat ∨ + s0.x2.toNat ≥ (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16) := by + bv_omega + + diff --git a/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line586.lean b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line586.lean new file mode 100644 index 00000000..00663e2b --- /dev/null +++ b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line586.lean @@ -0,0 +1,63 @@ +import Arm +import Arm.Memory.SeparateAutomation + +set_option maxHeartbeats 0 +set_option trace.profiler true +set_option profiler true + + +/- +tactic execution of Lean.Parser.Tactic.omega took 5.47s +instantiate metavars took 7.69s +share common exprs took 4.82s +type checking took 860ms +process pre-definitions took 1.59s +linting took 353ms +elaboration took 2.91s +-/ +theorem memcpy +(s0 si : ArmState) +(h_si_x0_nonzero : si.x0 ≠ 0) +(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) +(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) +(h_assert_1 : si.x0 ≤ s0.x0) +(h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0)) +(h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0)) +(h_assert_6 : ∀ (n : Nat) (addr : BitVec 64), + mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n → + Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem) +(h_assert_5 : ∀ (i : BitVec 64), + i < s0.x0 - si.x0 → + Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem) +(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16)) +(h_pre_2 : r StateField.PC s0 = 0x8e0#64) +(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64) +(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16)) +(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16)) +(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hi : s0.x0 - si.x0 < s0.x0 - (si.x0 - 0x1#64)) +(i_sub_x0_mul_16 : 16 * (s0.x0 - si.x0).toNat < 16 * s0.x0.toNat) +(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16)) +(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧ + s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ + s0.x2.toNat + s0.x0.toNat * 16) +(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64) +(hmemLegal_omega: s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧ + s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧ + (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ + s0.x1.toNat + s0.x0.toNat * 16) +(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - si.x0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) : + (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧ + (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ 2 ^ 64 ∧ + (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat ≤ (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat ∧ + (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 ≤ (s0.x2 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16 := by + bv_omega + diff --git a/Proofs/Experiments/Memcpy/OmegaBench.lean b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted2.lean similarity index 92% rename from Proofs/Experiments/Memcpy/OmegaBench.lean rename to Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted2.lean index 9b441a32..60a299f1 100644 --- a/Proofs/Experiments/Memcpy/OmegaBench.lean +++ b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted2.lean @@ -1,6 +1,11 @@ import Arm import Arm.Memory.SeparateAutomation +set_option maxHeartbeats 0 +set_option trace.profiler true +set_option profiler true + + /- tactic execution of Lean.Parser.Tactic.omega took 6.04s instantiate metavars took 31.6s @@ -8,10 +13,10 @@ share common exprs took 5.61s type checking took 1.36s process pre-definitions took 1.02s -/ -set_option maxHeartbeats 0 in -set_option trace.profiler true in -set_option profiler true in -theorem foo +set_option maxHeartbeats 0 +set_option trace.profiler true +set_option profiler true +theorem memcpy_extracted_2 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) From 6bc0404ecda509789229b2c3add7e8385561bd12 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 3 Oct 2024 10:22:25 -0500 Subject: [PATCH 09/11] chore: add another omega bench --- .../OmegaBench/MemcpyExtracted0Line583.lean | 56 +++++++++++++++++-- 1 file changed, 52 insertions(+), 4 deletions(-) diff --git a/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean index 7b012825..26482195 100644 --- a/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean +++ b/Proofs/Experiments/Memcpy/OmegaBench/MemcpyExtracted0Line583.lean @@ -1,10 +1,60 @@ -import Arm import Arm.Memory.SeparateAutomation +set_option linter.all false set_option maxHeartbeats 0 -set_option trace.profiler true +set_option trace.profiler true set_option profiler true +/- +tactic execution of Lean.Parser.Tactic.omega took 3.71s +instantiate metavars took 16.5s +share common exprs took 3.59s +type checking took 936ms +process pre-definitions took 376ms +elaboration took 2.32s +-/ +theorem memcpy_extracted_0_line_585 +(h_si_x0_nonzero : six0 ≠ 0) +(h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - six0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (six0 - 0x1#64))) +(h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - six0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (six0 - 0x1#64))) +(h_assert_1 : six0 ≤ s0.x0) +(h_assert_3 : six1 = s0.x1 + 0x10#64 * (s0.x0 - six0)) +(h_assert_4 : six2 = s0.x2 + 0x10#64 * (s0.x0 - six0)) +(h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16)) +(h_pre_2 : r StateField.PC s0 = 0x8e0#64) +(h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64) +(h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - six0)).toNat s0.x2 (s0.x0.toNat * 16)) +(h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - six0)) 16 s0.x1 (s0.x0.toNat * 16)) +(s2_sum_inbounds : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hi : s0.x0 - six0 < s0.x0 - (six0 - 0x1#64)) +(i_sub_x0_mul_16 : 16 * (s0.x0 - six0).toNat < 16 * s0.x0.toNat) +(hmemSeparate_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + (s0.x1.toNat + s0.x0.toNat * 16 ≤ s0.x2.toNat ∨ s0.x1.toNat ≥ s0.x2.toNat + s0.x0.toNat * 16)) +(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemSubset_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64 ∧ + s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ + s0.x2.toNat + s0.x0.toNat * 16) +(hmemLegal_omega : s0.x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x2.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +(hmemSubset_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64 ∧ + s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64 ∧ + s0.x1.toNat ≤ (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 ∧ + (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ + s0.x1.toNat + s0.x0.toNat * 16) +(hmemLegal_omega : (s0.x1.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - six0.toNat + s0.x0.toNat) % 2 ^ 64) % 2 ^ 64) % 2 ^ 64 + 16 ≤ 2 ^ 64) +(hmemLegal_omega : s0.x1.toNat + s0.x0.toNat * 16 ≤ 2 ^ 64) +: s0.x2.toNat + (0x10#64 * (s0.x0 - six0)).toNat ≤ 2 ^ 64 ∧ + (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat + 16 ≤ 2 ^ 64 ∧ + (s0.x2.toNat + (0x10#64 * (s0.x0 - six0)).toNat ≤ (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat ∨ + s0.x2.toNat ≥ (s0.x1 + 0x10#64 * (s0.x0 - six0)).toNat + 16) := by + bv_omega + + +#exit + /- tactic execution of Lean.Parser.Tactic.omega took 3.67s instantiate metavars took 15.3s @@ -59,5 +109,3 @@ theorem memcpy_extracted_0_line_585 (s0.x2.toNat + (0x10#64 * (s0.x0 - si.x0)).toNat ≤ (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat ∨ s0.x2.toNat ≥ (s0.x1 + 0x10#64 * (s0.x0 - si.x0)).toNat + 16) := by bv_omega - - From 01f5cde666d57b169af44e4235c1829d7a5a74e4 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 3 Oct 2024 13:48:43 -0500 Subject: [PATCH 10/11] chore: try to refactor to not use 'evalTactic', and fail to do so. Back away from this change --- Arm/Memory/Separate.lean | 12 ++ Arm/Memory/SeparateAutomation.lean | 20 +-- Proofs/Experiments/Memcpy/MemCpyVCG.lean | 187 ++++++++--------------- Tactics/Simp.lean | 28 +++- 4 files changed, 110 insertions(+), 137 deletions(-) diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean index a05cc413..22f47e98 100644 --- a/Arm/Memory/Separate.lean +++ b/Arm/Memory/Separate.lean @@ -237,6 +237,10 @@ theorem mem_legal'.iff_omega (a : BitVec 64) (n : Nat) : · intros h apply h.omega_def +@[bv_toNat] +theorem mem_legal'.iff_omega' (a : BitVec 64) (n : Nat) : + mem_legal' a n ↔ (a.toNat + n ≤ 2^64) := mem_legal'.iff_omega a n |>.symm + instance : Decidable (mem_legal' a n) := if h : a.toNat + n ≤ 2^64 then isTrue (mem_legal'.of_omega h) @@ -350,6 +354,10 @@ theorem mem_separate'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : · intros h apply h.omega_def +@[bv_toNat] + theorem mem_separate'.iff_omega' (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) : + mem_separate' a an b bn ↔ (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) := mem_separate'.iff_omega a an b bn |>.symm + instance : Decidable (mem_separate' a an b bn) := if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) then isTrue (mem_separate'.of_omega h) @@ -434,6 +442,10 @@ theorem mem_subset'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : N · intros h apply h.omega_def +@[bv_toNat] +theorem mem_subset'.iff_omega' (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) : + mem_subset' a an b bn ↔ (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) := mem_subset'.iff_omega a an b bn |>.symm + instance : Decidable (mem_subset' a an b bn) := if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) then isTrue (mem_subset'.of_omega h) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index 2a37e6fe..f2224a0f 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -444,9 +444,17 @@ def omega : SimpMemM Unit := do -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280 -- @bollu: TODO: understand what precisely we are recovering from. let startTime ← IO.monoMsNow - withoutRecover do -- TODO: replace this with filling in an MVar, sure, but not like this. - evalTactic (← `(tactic| bv_omega)) + let (ctx, simprocs) ← LNSymSimpContext (config := { failIfUnchanged := false }) + (simp_attrs := #[`bv_toNat]) + (simprocs := #[]) + (useDefaultSimprocs := false) + if let .some goal ← LNSymSimpAtStar (← getMainGoal) ctx simprocs then + replaceMainGoal [goal] + withoutRecover do + evalTactic (← `(tactic| omega)) + else + trace[simp_mem.info] m!"{checkEmoji} bv_omega preprocessing automatically solved goal." let endTime ← IO.monoMsNow pushOmegaTiming g (endTime - startTime) @@ -1143,15 +1151,7 @@ def memOmegaTactic : TacticM Unit := do SimpMemM.run (cfg := {}) do let g ← getMainGoal g.withContext do - let hyps := (← getLocalHyps) - let foundHyps ← SimpMemM.withTraceNode m!"Searching for Hypotheses" do - let mut foundHyps : Array Hypothesis := #[] - for h in hyps do - foundHyps ← hypothesisOfExpr h foundHyps - pure foundHyps - SimpMemM.withMainContext do - let _ ← Hypothesis.addOmegaFactsOfHyps foundHyps.toList #[] trace[simp_mem.info] m!"Executing `omega` to close goal." SimpMemM.withTraceNode m!"goal (Note: can be large)" do trace[simp_mem.info] "{← getMainGoal}" diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean index 172f1616..da97e8fa 100644 --- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean +++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean @@ -268,11 +268,10 @@ theorem program.step_8e4_8e8_of_wellformed_of_stepped (scur snext : ArmState) obtain h_sp_aligned := hscur.h_sp_aligned have := program.stepi_eq_0x8e4 h_program h_pc h_err - simp [BitVec.extractLsb] at this obtain ⟨h_step⟩ := hstep subst h_step constructor <;> simp only [*, cut, state_simp_rules, minimal_theory, bitvec_rules] - · constructor <;> simp [*, state_simp_rules, minimal_theory, BitVec.extractLsb] + · constructor <;> simp [*, state_simp_rules, minimal_theory] -- 3/7 (0x8e8#64, 0x3c810444#32), /- str q4, [x2], #16 -/ structure Step_8e8_8ec (scur : ArmState) (snext : ArmState) extends WellFormedAtPc snext 0x8ec : Prop where @@ -296,7 +295,6 @@ theorem program.step_8e8_8ec_of_wellformed (scur snext : ArmState) obtain h_sp_aligned := hscur.h_sp_aligned have := program.stepi_eq_0x8e8 h_program h_pc h_err - simp [BitVec.extractLsb] at this obtain ⟨h_step⟩ := hstep subst h_step constructor @@ -335,11 +333,10 @@ theorem program.step_8ec_8f0_of_wellformed (scur snext : ArmState) obtain h_sp_aligned := hs.h_sp_aligned have := program.stepi_eq_0x8ec h_program h_pc h_err - simp [BitVec.extractLsb] at this obtain ⟨h_step⟩ := hstep subst h_step constructor <;> simp (config := { ground := true, decide := true}) [*, - state_simp_rules, minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, memory_rules] + state_simp_rules, minimal_theory, fst_AddWithCarry_eq_sub_neg, memory_rules] · constructor <;> simp [*, state_simp_rules, minimal_theory, bitvec_rules, memory_rules] -- 5/7 (0x8f0#64, 0xf100001f#32), /- cmp x0, #0x0 -/ @@ -364,7 +361,7 @@ theorem program.step_8f0_8f4_of_wellformed (scur snext : ArmState) obtain h_sp_aligned := hs.h_sp_aligned have := program.stepi_eq_0x8f0 h_program h_pc h_err - simp (config := { ground := true, decide := true}) [BitVec.extractLsb, + simp (config := { ground := true, decide := true}) [ fst_AddWithCarry_eq_sub_neg, fst_AddWithCarry_eq_add] at this obtain ⟨h_step⟩ := hstep @@ -396,14 +393,14 @@ theorem program.step_8f4_8e4_of_wellformed_of_z_eq_0 (scur snext : ArmState) obtain h_sp_aligned := hs.h_sp_aligned have := program.stepi_eq_0x8f4 h_program h_pc h_err - simp (config := { ground := true, decide := true}) [BitVec.extractLsb, + simp (config := { ground := true, decide := true}) [ fst_AddWithCarry_eq_sub_neg, fst_AddWithCarry_eq_add] at this obtain ⟨h_step⟩ := hstep subst h_step constructor <;> solve | simp (config := { ground := true, decide := true}) [*, - state_simp_rules, minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg] + state_simp_rules, minimal_theory, fst_AddWithCarry_eq_sub_neg] · constructor <;> simp [*, state_simp_rules, minimal_theory, bitvec_rules] -- 6/7 (0x8f4#64, 0x54ffff81#32), /- b.ne 8e4 -/ @@ -426,116 +423,73 @@ theorem program.step_8f4_8f8_of_wellformed_of_z_eq_1 (scur snext : ArmState) obtain h_sp_aligned := hs.h_sp_aligned have := program.stepi_eq_0x8f4 h_program h_pc h_err - simp (config := { ground := true, decide := true}) [BitVec.extractLsb, + simp (config := { ground := true, decide := true}) [ fst_AddWithCarry_eq_sub_neg, fst_AddWithCarry_eq_add] at this obtain ⟨h_step⟩ := hstep subst h_step constructor <;> simp (config := { ground := true, decide := true}) [*, state_simp_rules, h_z, - minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, cut] + minimal_theory, fst_AddWithCarry_eq_sub_neg, cut] · constructor <;> simp [*, h_z, state_simp_rules, minimal_theory, bitvec_rules, cut] end CutTheorems section PartialCorrectness -/- -tactic execution of Lean.Parser.Tactic.omega took 290ms -tactic execution of Lean.Parser.Tactic.omega took 1.81s -tactic execution of simp_mem took 751ms -tactic execution of Lean.Parser.Tactic.omega took 1.11s -tactic execution of Lean.Parser.Tactic.omega took 664ms -tactic execution of Lean.Parser.Tactic.omega took 676ms -instantiate metavars took 7.15s -share common exprs took 3.9s -type checking took 1.47s -process pre-definitions took 440ms --/ --- set_option skip_proof.skip true in -set_option maxHeartbeats 0 in --- set_option trace.profiler true in --- set_option profiler true in --- set_option trace.profiler true in --- set_option profiler true in -set_option trace.simp_mem true -set_option trace.simp_mem.info true -set_option simp_mem.omegaNumIgnoredTimeouts 0 in -set_option simp_mem.omegaTimeoutMs 1000 in -theorem Memcpy.extracted_2 (s0 si : ArmState) - (h_si_x0_nonzero : si.x0 ≠ 0) - (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) - (h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) - (h_assert_1 : si.x0 ≤ s0.x0) (h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0)) - (h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0)) - (h_assert_6 : - ∀ (n : Nat) (addr : BitVec 64), - mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n → - Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem) - (h_assert_5 : - ∀ (i : BitVec 64), - i < s0.x0 - si.x0 → - Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem) - (h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16)) - -- (h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64) - (n : Nat) - (addr : BitVec 64) - (hsep : mem_separate' s0.x2 (0x10#64 * (s0.x0 - (si.x0 - 0x1#64))).toNat addr n) : - Memory.read_bytes n addr - (Memory.write_bytes 16 (s0.x2 + 0x10#64 * (s0.x0 - si.x0)) - (Memory.read_bytes 16 (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) si.mem) si.mem) = - Memory.read_bytes n addr s0.mem := by - have h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat := by bv_omega - have h_upper_bound := hsep.hb.omega_def - have h_upper_bound₂ := h_pre_1.hb.omega_def - have h_upper_bound₃ := hsep.ha.omega_def - have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by - sorry - rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] - · rw [h_assert_6] - skip_proof simp_mem - · -- @bollu: TODO: figure out why this is so slow! - apply mem_separate'.symm - apply mem_separate'.of_subset'_of_subset' hsep - · apply mem_subset'.of_omega - skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega - · apply mem_subset'_refl hsep.hb - +-- -- set_option skip_proof.skip true in +-- -- set_option trace.profiler true in +-- -- set_option profiler true in +-- set_option maxHeartbeats 0 in +-- theorem Memcpy.extracted_2 (s0 si : ArmState) +-- (h_si_x0_nonzero : si.x0 ≠ 0) +-- (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) +-- (h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) +-- (h_assert_1 : si.x0 ≤ s0.x0) (h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0)) +-- (h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0)) +-- (h_assert_6 : +-- ∀ (n : Nat) (addr : BitVec 64), +-- mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n → +-- Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem) +-- (h_assert_5 : +-- ∀ (i : BitVec 64), +-- i < s0.x0 - si.x0 → +-- Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem) +-- (h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16)) +-- -- (h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64) +-- (n : Nat) +-- (addr : BitVec 64) +-- (hsep : mem_separate' s0.x2 (0x10#64 * (s0.x0 - (si.x0 - 0x1#64))).toNat addr n) : +-- Memory.read_bytes n addr +-- (Memory.write_bytes 16 (s0.x2 + 0x10#64 * (s0.x0 - si.x0)) +-- (Memory.read_bytes 16 (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) si.mem) si.mem) = +-- Memory.read_bytes n addr s0.mem := by +-- -- have h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat := by mem_omega +-- have h_upper_bound := hsep.hb.omega_def +-- have h_upper_bound₂ := h_pre_1.hb.omega_def +-- have h_upper_bound₃ := hsep.ha.omega_def +-- -- have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by +-- -- mem_omega +-- rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] +-- · rw [h_assert_6] +-- sorry +-- -- bv_omega +-- -- skip_proof mem_omega +-- · -- @bollu: TODO: figure out why this is so slow! +-- apply mem_separate'.symm +-- apply mem_separate'.of_subset'_of_subset' hsep +-- · apply mem_subset'.of_omega +-- skip_proof refine ⟨?_, ?_, ?_, ?_⟩ +-- · sorry +-- · sorry +-- · sorry +-- · sorry +-- · apply mem_subset'_refl hsep.hb -/- -tactic execution of Lean.Parser.Tactic.omega took 1.54s -tactic execution of simp_mem took 274ms -tactic execution of Lean.Parser.Tactic.omega took 1.11s -tactic execution of simp_mem took 403ms -tactic execution of Lean.Parser.Tactic.omega took 302ms -tactic execution of Lean.Parser.Tactic.omega took 284ms -tactic execution of Lean.Parser.Tactic.omega took 4.25s -tactic execution of simp_mem took 1.96s -tactic execution of Lean.Parser.Tactic.omega took 8.95s -tactic execution of simp_mem took 1.68s -tactic execution of Lean.Parser.Tactic.omega took 102ms -tactic execution of Lean.Parser.Tactic.omega took 1.9s -tactic execution of simp_mem took 318ms -tactic execution of Lean.Parser.Tactic.omega took 322ms -tactic execution of Lean.Parser.Tactic.omega took 115ms -tactic execution of Lean.Parser.Tactic.omega took 101ms -instantiate metavars took 30s -share common exprs took 16.7s -fix level params took 118ms -type checking took 4.37s -process pre-definitions took 5.44s --/ - -set_option maxHeartbeats 0 -- set_option skip_proof.skip true in set_option maxHeartbeats 0 in -- set_option trace.profiler true in -- set_option profiler true in --- set_option trace.profiler true in --- set_option profiler true in -set_option trace.simp_mem.info true -set_option simp_mem.omegaNumIgnoredTimeouts 9999 in --- set_option simp_mem.omegaTimeoutMs 1000 in theorem Memcpy.extracted_0 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) @@ -569,9 +523,9 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) apply And.intro · intros i hi have h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16) := by - skip_proof simp_mem + skip_proof mem_omega have h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16) := by - skip_proof simp_mem + skip_proof mem_omega have icases : i = s0.x0 - si.x0 ∨ i < s0.x0 - si.x0 := by skip_proof bv_omega have s2_sum_inbounds := h_pre_1.hb.omega_def have i_sub_x0_mul_16 : 16 * i.toNat < 16 * s0.x0.toNat := by skip_proof bv_omega @@ -582,13 +536,13 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) · simp only [Nat.reduceMul, BitVec.toNat_add, BitVec.toNat_mul, BitVec.toNat_ofNat, Nat.reducePow, Nat.reduceMod, BitVec.toNat_sub, Nat.add_mod_mod, Nat.sub_self, BitVec.extractLsBytes_eq_self, BitVec.cast_eq] - rw [h_assert_6 _ _ (by simp_mem)] - · skip_proof simp_mem + rw [h_assert_6 _ _ (by mem_omega)] + · skip_proof mem_omega · rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] · apply h_assert_5 _ hi · constructor - · skip_proof simp_mem - · skip_proof simp_mem + · skip_proof mem_omega + · skip_proof mem_omega · left -- @bollu: TODO, see if `simp_mem` can figure this out given less aggressive -- proof states. @@ -605,23 +559,6 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) · intros n addr hsep apply Memcpy.extracted_2 <;> assumption -/- -tactic execution of Lean.Parser.Tactic.omega took 616ms -tactic execution of Lean.Parser.Tactic.omega took 1.1s -tactic execution of Lean.Parser.Tactic.assumption took 114ms -instantiate metavars took 14.7s -share common exprs took 1.94s -type checking took 988ms --/ - -set_option maxHeartbeats 0 in -set_option trace.profiler true in -set_option profiler true in -set_option maxHeartbeats 0 in -set_option trace.simp_mem.info true in -set_option simp_mem.omegaNumIgnoredTimeouts 9999 in --- set_option trace.profiler true in --- set_option profiler true in -- set_option trace.profiler true in -- set_option profiler true in theorem partial_correctness : @@ -740,7 +677,7 @@ theorem partial_correctness : simp only [memory_rules] at h_si_read_sep rw [h_si_read_sep] rw [h_si_x0_eq_zero] - skip_proof sorry -- nice! + skip_proof simp_mem -- nice! · simp only [step.h_err, step.h_program, step.h_sp_aligned, and_self] · have step_8f4_8e4 := program.step_8f4_8e4_of_wellformed_of_z_eq_0 si s1 si_well_formed diff --git a/Tactics/Simp.lean b/Tactics/Simp.lean index c4b716fc..72a2278f 100644 --- a/Tactics/Simp.lean +++ b/Tactics/Simp.lean @@ -37,6 +37,7 @@ def fixSimpTheoremKey (thm : SimpTheorem) : MetaM SimpTheorem := do let keys ← mkPath lhs simpDtConfig (noIndexAtArgs := false) pure { thm with keys } + /- Create a context for using the `simp` tactic during symbolic simulation in LNSym proofs. -/ def LNSymSimpContext @@ -54,10 +55,16 @@ def LNSymSimpContext (simprocs : Array Name := #[]) -- argument to `DiscrTree.mkPath` (noIndexAtArgs : Bool := true) + (useDefaultSimprocs : Bool := true) : MetaM (Simp.Context × Array Simp.Simprocs) := do let mut ext_simpTheorems := #[] - let default_simprocs ← Simp.getSimprocs - let mut all_simprocs := (#[default_simprocs] : Simp.SimprocsArray) + let all_simprocs : Array Simp.Simprocs ← do + if useDefaultSimprocs then + pure #[(← Simp.getSimprocs)] + else + pure #[] + /- For whatever reason, can't have the `all_simprocs` be `mut`. -/ + let mut all_simprocs := all_simprocs for a in simp_attrs do let some ext ← (getSimpExtension? a) | @@ -113,4 +120,21 @@ def LNSymSimp (goal : MVarId) | none => return none | some (_, goal') => return goal' +/-- +Invoke `simp [..] at *` at the given goal `g` with +simp context `ctx` and simprocs `simprocs`. +-/ +def LNSymSimpAtStar (g : MVarId) + (ctx : Simp.Context) + (simprocs : Array Simp.Simprocs) + : MetaM (Option MVarId) := do + g.withContext do + let fvars : Array FVarId := + (← getLCtx).foldl (init := #[]) fun fvars d => fvars.push d.fvarId + let (result, _stats) ← simpGoal g ctx simprocs (fvarIdsToSimp := fvars) + (simplifyTarget := true) (discharge? := none) + match result with + | none => return none + | some (_newHyps, g') => pure g' + ---------------------------------------------------------------------- From bf9074c4a8887c74dc6f51ab9355ccf6b2ddc0f3 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 3 Oct 2024 13:48:46 -0500 Subject: [PATCH 11/11] Revert "chore: try to refactor to not use 'evalTactic', and fail to do so. Back away from this change" This reverts commit 01f5cde666d57b169af44e4235c1829d7a5a74e4. --- Arm/Memory/Separate.lean | 12 -- Arm/Memory/SeparateAutomation.lean | 20 +-- Proofs/Experiments/Memcpy/MemCpyVCG.lean | 187 +++++++++++++++-------- Tactics/Simp.lean | 28 +--- 4 files changed, 137 insertions(+), 110 deletions(-) diff --git a/Arm/Memory/Separate.lean b/Arm/Memory/Separate.lean index 22f47e98..a05cc413 100644 --- a/Arm/Memory/Separate.lean +++ b/Arm/Memory/Separate.lean @@ -237,10 +237,6 @@ theorem mem_legal'.iff_omega (a : BitVec 64) (n : Nat) : · intros h apply h.omega_def -@[bv_toNat] -theorem mem_legal'.iff_omega' (a : BitVec 64) (n : Nat) : - mem_legal' a n ↔ (a.toNat + n ≤ 2^64) := mem_legal'.iff_omega a n |>.symm - instance : Decidable (mem_legal' a n) := if h : a.toNat + n ≤ 2^64 then isTrue (mem_legal'.of_omega h) @@ -354,10 +350,6 @@ theorem mem_separate'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : · intros h apply h.omega_def -@[bv_toNat] - theorem mem_separate'.iff_omega' (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) : - mem_separate' a an b bn ↔ (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) := mem_separate'.iff_omega a an b bn |>.symm - instance : Decidable (mem_separate' a an b bn) := if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ (a.toNat + an ≤ b.toNat ∨ a.toNat ≥ b.toNat + bn)) then isTrue (mem_separate'.of_omega h) @@ -442,10 +434,6 @@ theorem mem_subset'.iff_omega (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : N · intros h apply h.omega_def -@[bv_toNat] -theorem mem_subset'.iff_omega' (a : BitVec 64) (an : Nat) (b : BitVec 64) (bn : Nat) : - mem_subset' a an b bn ↔ (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) := mem_subset'.iff_omega a an b bn |>.symm - instance : Decidable (mem_subset' a an b bn) := if h : (a.toNat + an ≤ 2^64 ∧ b.toNat + bn ≤ 2^64 ∧ b.toNat ≤ a.toNat ∧ a.toNat + an ≤ b.toNat + bn) then isTrue (mem_subset'.of_omega h) diff --git a/Arm/Memory/SeparateAutomation.lean b/Arm/Memory/SeparateAutomation.lean index f2224a0f..2a37e6fe 100644 --- a/Arm/Memory/SeparateAutomation.lean +++ b/Arm/Memory/SeparateAutomation.lean @@ -444,17 +444,9 @@ def omega : SimpMemM Unit := do -- https://leanprover.zulipchat.com/#narrow/stream/326056-ICERM22-after-party/topic/Regression.20tests/near/290131280 -- @bollu: TODO: understand what precisely we are recovering from. let startTime ← IO.monoMsNow + withoutRecover do -- TODO: replace this with filling in an MVar, sure, but not like this. - let (ctx, simprocs) ← LNSymSimpContext (config := { failIfUnchanged := false }) - (simp_attrs := #[`bv_toNat]) - (simprocs := #[]) - (useDefaultSimprocs := false) - if let .some goal ← LNSymSimpAtStar (← getMainGoal) ctx simprocs then - replaceMainGoal [goal] - withoutRecover do - evalTactic (← `(tactic| omega)) - else - trace[simp_mem.info] m!"{checkEmoji} bv_omega preprocessing automatically solved goal." + evalTactic (← `(tactic| bv_omega)) let endTime ← IO.monoMsNow pushOmegaTiming g (endTime - startTime) @@ -1151,7 +1143,15 @@ def memOmegaTactic : TacticM Unit := do SimpMemM.run (cfg := {}) do let g ← getMainGoal g.withContext do + let hyps := (← getLocalHyps) + let foundHyps ← SimpMemM.withTraceNode m!"Searching for Hypotheses" do + let mut foundHyps : Array Hypothesis := #[] + for h in hyps do + foundHyps ← hypothesisOfExpr h foundHyps + pure foundHyps + SimpMemM.withMainContext do + let _ ← Hypothesis.addOmegaFactsOfHyps foundHyps.toList #[] trace[simp_mem.info] m!"Executing `omega` to close goal." SimpMemM.withTraceNode m!"goal (Note: can be large)" do trace[simp_mem.info] "{← getMainGoal}" diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean index da97e8fa..172f1616 100644 --- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean +++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean @@ -268,10 +268,11 @@ theorem program.step_8e4_8e8_of_wellformed_of_stepped (scur snext : ArmState) obtain h_sp_aligned := hscur.h_sp_aligned have := program.stepi_eq_0x8e4 h_program h_pc h_err + simp [BitVec.extractLsb] at this obtain ⟨h_step⟩ := hstep subst h_step constructor <;> simp only [*, cut, state_simp_rules, minimal_theory, bitvec_rules] - · constructor <;> simp [*, state_simp_rules, minimal_theory] + · constructor <;> simp [*, state_simp_rules, minimal_theory, BitVec.extractLsb] -- 3/7 (0x8e8#64, 0x3c810444#32), /- str q4, [x2], #16 -/ structure Step_8e8_8ec (scur : ArmState) (snext : ArmState) extends WellFormedAtPc snext 0x8ec : Prop where @@ -295,6 +296,7 @@ theorem program.step_8e8_8ec_of_wellformed (scur snext : ArmState) obtain h_sp_aligned := hscur.h_sp_aligned have := program.stepi_eq_0x8e8 h_program h_pc h_err + simp [BitVec.extractLsb] at this obtain ⟨h_step⟩ := hstep subst h_step constructor @@ -333,10 +335,11 @@ theorem program.step_8ec_8f0_of_wellformed (scur snext : ArmState) obtain h_sp_aligned := hs.h_sp_aligned have := program.stepi_eq_0x8ec h_program h_pc h_err + simp [BitVec.extractLsb] at this obtain ⟨h_step⟩ := hstep subst h_step constructor <;> simp (config := { ground := true, decide := true}) [*, - state_simp_rules, minimal_theory, fst_AddWithCarry_eq_sub_neg, memory_rules] + state_simp_rules, minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, memory_rules] · constructor <;> simp [*, state_simp_rules, minimal_theory, bitvec_rules, memory_rules] -- 5/7 (0x8f0#64, 0xf100001f#32), /- cmp x0, #0x0 -/ @@ -361,7 +364,7 @@ theorem program.step_8f0_8f4_of_wellformed (scur snext : ArmState) obtain h_sp_aligned := hs.h_sp_aligned have := program.stepi_eq_0x8f0 h_program h_pc h_err - simp (config := { ground := true, decide := true}) [ + simp (config := { ground := true, decide := true}) [BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, fst_AddWithCarry_eq_add] at this obtain ⟨h_step⟩ := hstep @@ -393,14 +396,14 @@ theorem program.step_8f4_8e4_of_wellformed_of_z_eq_0 (scur snext : ArmState) obtain h_sp_aligned := hs.h_sp_aligned have := program.stepi_eq_0x8f4 h_program h_pc h_err - simp (config := { ground := true, decide := true}) [ + simp (config := { ground := true, decide := true}) [BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, fst_AddWithCarry_eq_add] at this obtain ⟨h_step⟩ := hstep subst h_step constructor <;> solve | simp (config := { ground := true, decide := true}) [*, - state_simp_rules, minimal_theory, fst_AddWithCarry_eq_sub_neg] + state_simp_rules, minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg] · constructor <;> simp [*, state_simp_rules, minimal_theory, bitvec_rules] -- 6/7 (0x8f4#64, 0x54ffff81#32), /- b.ne 8e4 -/ @@ -423,73 +426,116 @@ theorem program.step_8f4_8f8_of_wellformed_of_z_eq_1 (scur snext : ArmState) obtain h_sp_aligned := hs.h_sp_aligned have := program.stepi_eq_0x8f4 h_program h_pc h_err - simp (config := { ground := true, decide := true}) [ + simp (config := { ground := true, decide := true}) [BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, fst_AddWithCarry_eq_add] at this obtain ⟨h_step⟩ := hstep subst h_step constructor <;> simp (config := { ground := true, decide := true}) [*, state_simp_rules, h_z, - minimal_theory, fst_AddWithCarry_eq_sub_neg, cut] + minimal_theory, BitVec.extractLsb, fst_AddWithCarry_eq_sub_neg, cut] · constructor <;> simp [*, h_z, state_simp_rules, minimal_theory, bitvec_rules, cut] end CutTheorems section PartialCorrectness --- -- set_option skip_proof.skip true in --- -- set_option trace.profiler true in --- -- set_option profiler true in --- set_option maxHeartbeats 0 in --- theorem Memcpy.extracted_2 (s0 si : ArmState) --- (h_si_x0_nonzero : si.x0 ≠ 0) --- (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) --- (h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) --- (h_assert_1 : si.x0 ≤ s0.x0) (h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0)) --- (h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0)) --- (h_assert_6 : --- ∀ (n : Nat) (addr : BitVec 64), --- mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n → --- Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem) --- (h_assert_5 : --- ∀ (i : BitVec 64), --- i < s0.x0 - si.x0 → --- Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem) --- (h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16)) --- -- (h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64) --- (n : Nat) --- (addr : BitVec 64) --- (hsep : mem_separate' s0.x2 (0x10#64 * (s0.x0 - (si.x0 - 0x1#64))).toNat addr n) : --- Memory.read_bytes n addr --- (Memory.write_bytes 16 (s0.x2 + 0x10#64 * (s0.x0 - si.x0)) --- (Memory.read_bytes 16 (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) si.mem) si.mem) = --- Memory.read_bytes n addr s0.mem := by --- -- have h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat := by mem_omega --- have h_upper_bound := hsep.hb.omega_def --- have h_upper_bound₂ := h_pre_1.hb.omega_def --- have h_upper_bound₃ := hsep.ha.omega_def --- -- have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by --- -- mem_omega --- rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] --- · rw [h_assert_6] --- sorry --- -- bv_omega --- -- skip_proof mem_omega --- · -- @bollu: TODO: figure out why this is so slow! --- apply mem_separate'.symm --- apply mem_separate'.of_subset'_of_subset' hsep --- · apply mem_subset'.of_omega --- skip_proof refine ⟨?_, ?_, ?_, ?_⟩ --- · sorry --- · sorry --- · sorry --- · sorry --- · apply mem_subset'_refl hsep.hb +/- +tactic execution of Lean.Parser.Tactic.omega took 290ms +tactic execution of Lean.Parser.Tactic.omega took 1.81s +tactic execution of simp_mem took 751ms +tactic execution of Lean.Parser.Tactic.omega took 1.11s +tactic execution of Lean.Parser.Tactic.omega took 664ms +tactic execution of Lean.Parser.Tactic.omega took 676ms +instantiate metavars took 7.15s +share common exprs took 3.9s +type checking took 1.47s +process pre-definitions took 440ms +-/ +-- set_option skip_proof.skip true in +set_option maxHeartbeats 0 in +-- set_option trace.profiler true in +-- set_option profiler true in +-- set_option trace.profiler true in +-- set_option profiler true in +set_option trace.simp_mem true +set_option trace.simp_mem.info true +set_option simp_mem.omegaNumIgnoredTimeouts 0 in +set_option simp_mem.omegaTimeoutMs 1000 in +theorem Memcpy.extracted_2 (s0 si : ArmState) + (h_si_x0_nonzero : si.x0 ≠ 0) + (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) + (h_s0_x2 : s0.x2 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x2 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) + (h_assert_1 : si.x0 ≤ s0.x0) (h_assert_3 : si.x1 = s0.x1 + 0x10#64 * (s0.x0 - si.x0)) + (h_assert_4 : si.x2 = s0.x2 + 0x10#64 * (s0.x0 - si.x0)) + (h_assert_6 : + ∀ (n : Nat) (addr : BitVec 64), + mem_separate' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat addr n → + Memory.read_bytes n addr si.mem = Memory.read_bytes n addr s0.mem) + (h_assert_5 : + ∀ (i : BitVec 64), + i < s0.x0 - si.x0 → + Memory.read_bytes 16 (s0.x2 + 0x10#64 * i) si.mem = Memory.read_bytes 16 (s0.x1 + 0x10#64 * i) s0.mem) + (h_pre_1 : mem_separate' s0.x1 (s0.x0.toNat * 16) s0.x2 (s0.x0.toNat * 16)) + -- (h_pre_6 : 16 * s0.x0.toNat < 2 ^ 64) + (n : Nat) + (addr : BitVec 64) + (hsep : mem_separate' s0.x2 (0x10#64 * (s0.x0 - (si.x0 - 0x1#64))).toNat addr n) : + Memory.read_bytes n addr + (Memory.write_bytes 16 (s0.x2 + 0x10#64 * (s0.x0 - si.x0)) + (Memory.read_bytes 16 (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) si.mem) si.mem) = + Memory.read_bytes n addr s0.mem := by + have h_le : (s0.x0 - (si.x0 - 0x1#64)).toNat ≤ s0.x0.toNat := by bv_omega + have h_upper_bound := hsep.hb.omega_def + have h_upper_bound₂ := h_pre_1.hb.omega_def + have h_upper_bound₃ := hsep.ha.omega_def + have h_width_lt : (0x10#64).toNat * (s0.x0 - (si.x0 - 0x1#64)).toNat < 2 ^ 64 := by + sorry + rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] + · rw [h_assert_6] + skip_proof simp_mem + · -- @bollu: TODO: figure out why this is so slow! + apply mem_separate'.symm + apply mem_separate'.of_subset'_of_subset' hsep + · apply mem_subset'.of_omega + skip_proof refine ⟨?_, ?_, ?_, ?_⟩ <;> skip_proof bv_omega + · apply mem_subset'_refl hsep.hb + +/- +tactic execution of Lean.Parser.Tactic.omega took 1.54s +tactic execution of simp_mem took 274ms +tactic execution of Lean.Parser.Tactic.omega took 1.11s +tactic execution of simp_mem took 403ms +tactic execution of Lean.Parser.Tactic.omega took 302ms +tactic execution of Lean.Parser.Tactic.omega took 284ms +tactic execution of Lean.Parser.Tactic.omega took 4.25s +tactic execution of simp_mem took 1.96s +tactic execution of Lean.Parser.Tactic.omega took 8.95s +tactic execution of simp_mem took 1.68s +tactic execution of Lean.Parser.Tactic.omega took 102ms +tactic execution of Lean.Parser.Tactic.omega took 1.9s +tactic execution of simp_mem took 318ms +tactic execution of Lean.Parser.Tactic.omega took 322ms +tactic execution of Lean.Parser.Tactic.omega took 115ms +tactic execution of Lean.Parser.Tactic.omega took 101ms +instantiate metavars took 30s +share common exprs took 16.7s +fix level params took 118ms +type checking took 4.37s +process pre-definitions took 5.44s +-/ + +set_option maxHeartbeats 0 -- set_option skip_proof.skip true in set_option maxHeartbeats 0 in -- set_option trace.profiler true in -- set_option profiler true in +-- set_option trace.profiler true in +-- set_option profiler true in +set_option trace.simp_mem.info true +set_option simp_mem.omegaNumIgnoredTimeouts 9999 in +-- set_option simp_mem.omegaTimeoutMs 1000 in theorem Memcpy.extracted_0 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) @@ -523,9 +569,9 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) apply And.intro · intros i hi have h_subset_2 : mem_subset' s0.x2 (0x10#64 * (s0.x0 - si.x0)).toNat s0.x2 (s0.x0.toNat * 16) := by - skip_proof mem_omega + skip_proof simp_mem have h_subset_1 : mem_subset' (s0.x1 + 0x10#64 * (s0.x0 - si.x0)) 16 s0.x1 (s0.x0.toNat * 16) := by - skip_proof mem_omega + skip_proof simp_mem have icases : i = s0.x0 - si.x0 ∨ i < s0.x0 - si.x0 := by skip_proof bv_omega have s2_sum_inbounds := h_pre_1.hb.omega_def have i_sub_x0_mul_16 : 16 * i.toNat < 16 * s0.x0.toNat := by skip_proof bv_omega @@ -536,13 +582,13 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) · simp only [Nat.reduceMul, BitVec.toNat_add, BitVec.toNat_mul, BitVec.toNat_ofNat, Nat.reducePow, Nat.reduceMod, BitVec.toNat_sub, Nat.add_mod_mod, Nat.sub_self, BitVec.extractLsBytes_eq_self, BitVec.cast_eq] - rw [h_assert_6 _ _ (by mem_omega)] - · skip_proof mem_omega + rw [h_assert_6 _ _ (by simp_mem)] + · skip_proof simp_mem · rw [Memory.read_bytes_write_bytes_eq_read_bytes_of_mem_separate'] · apply h_assert_5 _ hi · constructor - · skip_proof mem_omega - · skip_proof mem_omega + · skip_proof simp_mem + · skip_proof simp_mem · left -- @bollu: TODO, see if `simp_mem` can figure this out given less aggressive -- proof states. @@ -559,6 +605,23 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) · intros n addr hsep apply Memcpy.extracted_2 <;> assumption +/- +tactic execution of Lean.Parser.Tactic.omega took 616ms +tactic execution of Lean.Parser.Tactic.omega took 1.1s +tactic execution of Lean.Parser.Tactic.assumption took 114ms +instantiate metavars took 14.7s +share common exprs took 1.94s +type checking took 988ms +-/ + +set_option maxHeartbeats 0 in +set_option trace.profiler true in +set_option profiler true in +set_option maxHeartbeats 0 in +set_option trace.simp_mem.info true in +set_option simp_mem.omegaNumIgnoredTimeouts 9999 in +-- set_option trace.profiler true in +-- set_option profiler true in -- set_option trace.profiler true in -- set_option profiler true in theorem partial_correctness : @@ -677,7 +740,7 @@ theorem partial_correctness : simp only [memory_rules] at h_si_read_sep rw [h_si_read_sep] rw [h_si_x0_eq_zero] - skip_proof simp_mem -- nice! + skip_proof sorry -- nice! · simp only [step.h_err, step.h_program, step.h_sp_aligned, and_self] · have step_8f4_8e4 := program.step_8f4_8e4_of_wellformed_of_z_eq_0 si s1 si_well_formed diff --git a/Tactics/Simp.lean b/Tactics/Simp.lean index 72a2278f..c4b716fc 100644 --- a/Tactics/Simp.lean +++ b/Tactics/Simp.lean @@ -37,7 +37,6 @@ def fixSimpTheoremKey (thm : SimpTheorem) : MetaM SimpTheorem := do let keys ← mkPath lhs simpDtConfig (noIndexAtArgs := false) pure { thm with keys } - /- Create a context for using the `simp` tactic during symbolic simulation in LNSym proofs. -/ def LNSymSimpContext @@ -55,16 +54,10 @@ def LNSymSimpContext (simprocs : Array Name := #[]) -- argument to `DiscrTree.mkPath` (noIndexAtArgs : Bool := true) - (useDefaultSimprocs : Bool := true) : MetaM (Simp.Context × Array Simp.Simprocs) := do let mut ext_simpTheorems := #[] - let all_simprocs : Array Simp.Simprocs ← do - if useDefaultSimprocs then - pure #[(← Simp.getSimprocs)] - else - pure #[] - /- For whatever reason, can't have the `all_simprocs` be `mut`. -/ - let mut all_simprocs := all_simprocs + let default_simprocs ← Simp.getSimprocs + let mut all_simprocs := (#[default_simprocs] : Simp.SimprocsArray) for a in simp_attrs do let some ext ← (getSimpExtension? a) | @@ -120,21 +113,4 @@ def LNSymSimp (goal : MVarId) | none => return none | some (_, goal') => return goal' -/-- -Invoke `simp [..] at *` at the given goal `g` with -simp context `ctx` and simprocs `simprocs`. --/ -def LNSymSimpAtStar (g : MVarId) - (ctx : Simp.Context) - (simprocs : Array Simp.Simprocs) - : MetaM (Option MVarId) := do - g.withContext do - let fvars : Array FVarId := - (← getLCtx).foldl (init := #[]) fun fvars d => fvars.push d.fvarId - let (result, _stats) ← simpGoal g ctx simprocs (fvarIdsToSimp := fvars) - (simplifyTarget := true) (discharge? := none) - match result with - | none => return none - | some (_newHyps, g') => pure g' - ----------------------------------------------------------------------