From cfcd3948a34e6c31305c2f0b6a556be874639c78 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 6 Oct 2026 20:09:08 -0500 Subject: [PATCH] Proof step and variable lemmas 1. no writes = save value 2. embedding commutation with steps 3. all variables in code end up in the set of vars --- lean/Spa.lean | 1 + lean/Spa/Analysis/Reaching.lean | 42 +++++---- lean/Spa/Language/TraceProperties.lean | 114 +++++++++++++++++++++++++ lean/Spa/Language/Traces.lean | 14 ++- 4 files changed, 141 insertions(+), 30 deletions(-) create mode 100644 lean/Spa/Language/TraceProperties.lean diff --git a/lean/Spa.lean b/lean/Spa.lean index ac762cb..9aa3513 100644 --- a/lean/Spa.lean +++ b/lean/Spa.lean @@ -11,6 +11,7 @@ import Spa.Language.Equivalence import Spa.Language.Graphs import Spa.Language.Traces import Spa.Language.Properties +import Spa.Language.TraceProperties import Spa.Language import Spa.Analysis.Forward.Lattices import Spa.Analysis.Forward.Evaluation diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean index 02bff45..6ed485c 100644 --- a/lean/Spa/Analysis/Reaching.lean +++ b/lean/Spa/Analysis/Reaching.lean @@ -85,36 +85,34 @@ instance stateInterp : StateInterpretation (DefSet prog) prog where simpa only [runOfPath, Trace.addEdge, Path.steps_append, Path.single, Path.steps, Step.steps, List.append_nil] using hvs -private lemma valid_step (s : prog.State) {ρ₁ ρ₂ : Env} - {obs : Option BasicStmt} (hcode : prog.code s = obs) - (hbs : EvalBasicStmtOpt ρ₁ obs ρ₂) +private lemma valid_step (s : prog.State) {vs : VariableValues (DefSet prog) prog} {run : Run prog} (hvs : ⟦vs⟧ run) : - ⟦eval prog s vs⟧ ((hbs.steps s).reverse ++ run) := by - cases hbs with - | none => simpa [eval, hcode, EvalBasicStmtOpt.steps] using hvs - | some hbs => - cases hbs with - | noop => - simp [eval, hcode, EvalBasicStmtOpt.steps] - intro x assigners hmem n hla; aesop (add simp hcode) - | assign x e v hev => - simp [eval, hcode, EvalBasicStmtOpt.steps]; intro k assigners hmem n hla - by_cases hx : k = x - · subst hx - have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem - rcases hla <;> simp [hd] <;> aesop (add simp hcode) - · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward - (fun hc => hx (List.mem_singleton.mp hc)) hmem - aesop (add simp hcode) + ⟦eval prog s vs⟧ ((match prog.code s with | none => [] | some _ => [s]) ++ run) := by + cases hcode : prog.code s with + | none => simpa [eval, hcode] using hvs + | some bs => + cases bs with + | noop => + simp [eval, hcode] + intro x assigners hmem n hla; aesop (add simp hcode) + | assign x e => + simp [eval, hcode]; intro k assigners hmem n hla + by_cases hx : k = x + · subst hx + have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem + rcases hla <;> simp [hd] <;> aesop (add simp hcode) + · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward + (fun hc => hx (List.mem_singleton.mp hc)) hmem + aesop (add simp hcode) instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where valid := by intro s₁ s₂ ρ₁ ρ₂ ρ₃ vs tr hbs hvs change ⟦vs⟧ (runOfPath prog tr) at hvs change ⟦eval prog s₂ vs⟧ (runOfPath prog (Path.append tr (.single (.execute hbs)))) - simpa only [runOfPath, Path.steps_append, Path.single, Path.steps, Step.steps, - List.append_nil, List.reverse_append] using valid_step prog s₂ rfl hbs hvs + cases hcode : prog.code s₂ <;> + simpa [runOfPath, Path.single, Path.steps, Step.steps, hcode] using valid_step prog s₂ hvs botV_init := by intro x assigners _ n hla; cases hla theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : diff --git a/lean/Spa/Language/TraceProperties.lean b/lean/Spa/Language/TraceProperties.lean new file mode 100644 index 0000000..c30d0e4 --- /dev/null +++ b/lean/Spa/Language/TraceProperties.lean @@ -0,0 +1,114 @@ +import Spa.Language.Properties +import Spa.Language.Equivalence + +namespace Spa +open GGraph + +/-- Recorded nodes contain instructions; empty CFG nodes are omitted from the history. -/ +lemma Path.steps_nonempty {g : Graph} {a b : Configuration g} (p : Path g a b) + {d : g.Index} (hm : d ∈ p.steps) : g.nodes d ≠ none := by + induction p with + | nil => simp [Path.steps] at hm + | cons st p ih => + rcases List.mem_append.mp hm with hs | hp + · cases st with + | edge => simp [Step.steps] at hs + | @execute i ρ σ h => + cases hc : g.nodes i <;> aesop (add simp [Step.steps, hc]) + · exact ih hp + +private lemma optional_preserves_unwritten {ρ σ : Env} {obs : Option BasicStmt} + (h : EvalBasicStmtOpt ρ obs σ) (x : String) + (hn : ∀ rhs, obs ≠ some (.assign x rhs)) : + ∀ v, Env.Mem (x, v) ρ ↔ Env.Mem (x, v) σ := by + cases h with + | none => exact fun _ => Iff.rfl + | some h => + cases h with + | noop => exact fun _ => Iff.rfl + | assign y rhs w hv => + have hxy : x ≠ y := by + rintro rfl + exact hn rhs rfl + intro v; simp [Env.mem_cons, hxy] + +/-- A path whose executed nodes do not assign `x` preserves its binding. -/ +lemma Path.preserves_unwritten {g : Graph} {a b : Configuration g} (p : Path g a b) + {x : String} (hn : ∀ d ∈ p.steps, ∀ rhs, g.nodes d ≠ some (.assign x rhs)) : + ∀ v, Env.Mem (x, v) a.2 ↔ Env.Mem (x, v) b.2 := by + induction p with + | nil => exact fun _ => Iff.rfl + | cons st p ih => + have ht := ih (fun d hm => hn d (List.mem_append_right _ hm)) + suffices hs : ∀ v, Env.Mem (x, v) _ ↔ Env.Mem (x, v) _ from + fun v => (hs v).trans (ht v) + cases st with + | edge => exact fun _ => Iff.rfl + | execute h => + apply optional_preserves_unwritten h x + intro rhs hc + exact hn _ (List.mem_append_left _ (by simp [Step.steps, hc])) rhs hc + +lemma Step.steps_embed {g h : Graph} (e : Embed g h) {a b : Configuration g} + (s : Step g a b) : + (s.embed e).steps = s.steps.map e.f := by + cases s with + | edge => rfl + | @execute i ρ σ h => + simp only [Step.embed, Step.steps, e.nodes_eq] + cases g.nodes i <;> rfl + +lemma Path.steps_embed {g h : Graph} (e : Embed g h) {a b : Configuration g} + (p : Path g a b) : + (p.embed e).steps = p.steps.map e.f := by + induction p <;> aesop (add simp [Path.embed, Path.steps, Step.steps_embed]) + +/-- Every nonempty node in a loop belongs to its body. -/ +lemma GGraph.loop_node_in_body {g : Graph} {i : (Graph.loop g).Index} {bs : BasicStmt} + (hc : (Graph.loop g).nodes i = some bs) : ∃ j, (Embed.loop g).f j = i := by + refine Fin.addCases ?_ ?_ i hc + · intro j hj + simp [Graph.loop, Fin.append_left] at hj + · intro j _; exact ⟨j, rfl⟩ + +/-- Variables at any CFG statement occur in its source statement. -/ +lemma Stmt.cfg_node_vars {s : Stmt} {i : s.cfg.Index} {bs : BasicStmt} + (hc : s.cfg.nodes i = some bs) : bs.vars ⊆ s.vars := by + induction s with + | basic b => + have : b = bs := Option.some.inj hc + subst bs; exact Finset.Subset.refl _ + | andThen a b iha ihb => + refine Fin.addCases ?_ ?_ i hc + · intro j hj; have hv := iha (by simpa [Stmt.cfg, Graph.sequence] using hj) + exact fun x hx => Finset.mem_union_left _ (hv hx) + · intro j hj; have hv := ihb (by simpa [Stmt.cfg, Graph.sequence] using hj) + exact fun x hx => Finset.mem_union_right _ (hv hx) + | ifElse cond a b iha ihb => + refine Fin.addCases ?_ ?_ i hc + · intro j hj; have hv := iha (by simpa [Stmt.cfg, Graph.overlay] using hj) + exact fun x hx => Finset.mem_union_left _ (Finset.mem_union_right _ (hv hx)) + · intro j hj; have hv := ihb (by simpa [Stmt.cfg, Graph.overlay] using hj) + exact fun x hx => Finset.mem_union_right _ (hv hx) + | whileLoop cond body ih => + obtain ⟨j, rfl⟩ := GGraph.loop_node_in_body hc + have hv := ih (((Embed.loop body.cfg).nodes_eq j).symm.trans hc) + exact fun x hx => Finset.mem_union_right _ (hv hx) + +lemma Program.code_vars {prog : Program} {i : prog.State} {bs : BasicStmt} + (hc : prog.code i = some bs) : ∀ x ∈ bs.vars, x ∈ prog.vars := by + have hroot : ∃ j, prog.rootStmt.cfg.nodes j = some bs := by + unfold Program.code Program.cfg Graph.wrap at hc + revert hc + refine Fin.addCases ?_ ?_ i + · intro j hj; simp [Graph.sequence, Graph.singleton] at hj + · intro j + refine Fin.addCases ?_ ?_ j + · intro k hk + exact ⟨k, by simpa [Graph.sequence] using hk⟩ + · intro k hk; simp [Graph.sequence, Graph.singleton] at hk + obtain ⟨j, hj⟩ := hroot + intro x hx + simpa [Program.vars] using Stmt.cfg_node_vars hj hx + +end Spa diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index 878cf14..a73fc4e 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -186,14 +186,12 @@ instance {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) (Trace g idx₁ idx₂ ρ₁ ρ₃) := ⟨Traceₗ.appendStep⟩ -/-- The node executed by an optional-statement step; empty nodes are omitted. -/ -def EvalBasicStmtOpt.steps {α : Type*} (idx : α) {ρ₁ ρ₂ : Env} {obs : Option BasicStmt} : - EvalBasicStmtOpt ρ₁ obs ρ₂ → List α - | .none => [] - | .some _ => [idx] - +/-- The nonempty node executed by this step; edges and empty nodes are omitted. -/ def Step.steps {g : Graph} {a b : Configuration g} : Step g a b → List g.Index - | .execute (i := i) h => h.steps i + | .execute (i := i) _ => + match g.nodes i with + | none => [] + | some _ => [i] | .edge _ => [] /-- Executed nodes in chronological order; edges and empty nodes contribute nothing. @@ -217,7 +215,7 @@ abbrev Traceᵣ.steps {g : Graph} {i j : g.Index} {ρ₁ ρ₂ : Env} @[simp] lemma Traceₗ.steps_appendStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} (tr : Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (hbs : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) : - (tr ++ hbs).steps = tr.steps ++ hbs.steps idx₂ := by + (tr ++ hbs).steps = tr.steps ++ (Step.execute hbs).steps := by change Path.steps (Path.append tr (Path.single (.execute hbs))) = _ aesop (add simp [Trace.steps, Traceₗ.steps, Path.single, Path.steps, Step.steps])