From 8cd053a2425f041c6ed06047914810a874bdd8f7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 2 Jul 2026 09:01:09 -0500 Subject: [PATCH] Migrate Reaching.lean to projections via a generic Trace.steps MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Finish the projection migration for reaching definitions by replacing the accumulator-style runOfTrace*From definitions and their hand-rolled re-association lemmas with a single analysis-agnostic projection: Trace.steps / Traceₗ.steps, the chronological List of executed (index, statement) pairs. Its four simp lemmas are one-line inductions, with all re-association falling out of mathlib's List.append_assoc and List.reverse_append. Run is now an abbrev for List (State × BasicStmt) (latest-first, so LastAssign keeps its first-match structure) and runOfTrace is just steps.reverse. Also hoist the generic reaches_final_post into Forward.lean, letting analyze_correct' be stated directly about S.Post (prog.trace hrun). Co-Authored-By: Claude Fable 5 --- lean/Spa/Analysis/Forward.lean | 17 ++++-- lean/Spa/Analysis/Reaching.lean | 96 ++++++++++++++++++++------------- lean/Spa/Language/Traces.lean | 55 +++++++++++++++++++ 3 files changed, 126 insertions(+), 42 deletions(-) diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index 63efeb8..69c7984 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -131,6 +131,15 @@ def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} | .edge hnode hedge rest => let ⟨ρin, r'⟩ := reaches_final rest; ⟨ρin, .edge_there hnode hedge _ r'⟩ +omit [DecidableEq L] in +/-- Reaching the final node covers the whole trace. -/ +@[simp] lemma reaches_final_post {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} + (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : + (reaches_final tr).2.post = tr := by + induction tr with + | single hnode => rfl + | edge hnode hedge rest ih => simp [reaches_final, Reaches.post, ih] + variable (L prog) in /-- Soundness at every program point reached during execution: for any node `s` visited by the run `hrun` (witnessed by `hr`), the analysis result over-approximates both the @@ -148,11 +157,9 @@ theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf) variable (L prog) in theorem analyze_correct' {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (reaches_final (prog.trace hrun)).2.post) := by - let idk₀ := prog.trace hrun - have ⟨_, idk₁⟩ := reaches_final idk₀ - have ⟨_, idk₂⟩ := analyze_correct_at L prog hrun idk₁ - assumption + ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (prog.trace hrun)) := by + have h := (analyze_correct_at L prog hrun (reaches_final (prog.trace hrun)).2).2 + rwa [reaches_final_post] at h end diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean index cc87122..190bf9a 100644 --- a/lean/Spa/Analysis/Reaching.lean +++ b/lean/Spa/Analysis/Reaching.lean @@ -43,69 +43,91 @@ instance stmtEvaluator : StmtEvaluator (DefSet prog) prog := def output : String := show' (result (DefSet prog) prog) -inductive Run (prog : Program) where - | nil : Run prog - | cons (s : prog.State) (bs : BasicStmt) - (rest : Run prog) : Run prog +/-- The statements a trace executed, paired with the state each executed at, + most recent first (matching `LastAssign`, which scans for the most recent + assignment). This is `Trace.steps` (chronological) reversed, so facts about + concatenating traces reduce to mathlib's `List.append`/`List.reverse` lemmas. -/ +abbrev Run (prog : Program) : Type := List (prog.State × BasicStmt) @[aesop unsafe cases] inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId → Prop | here (s : prog.State) (e : Expr) (hc : prog.code s = some (.assign x e)) (rest : Run prog) : - LastAssign prog x (Run.cons s (.assign x e) rest) (prog.nodeIdOfNonempty s hc) + LastAssign prog x ((s, .assign x e) :: rest) (prog.nodeIdOfNonempty s hc) | there (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs) (rest : Run prog) {n : prog.NodeId} : (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n → - LastAssign prog x (Run.cons s bs rest) n + LastAssign prog x ((s, bs) :: rest) n + +def runOfTraceₗ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} + (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog := + tr.steps.reverse + +def runOfTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} + (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog := + tr.steps.reverse instance stateInterp : StateInterpretation (DefSet prog) prog where - St := fun _ => Run prog - init := Run.nil - interp vs _ run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs → + Proj := Run prog + Pre := @runOfTraceₗ prog + Post := @runOfTrace prog + + interp vs run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs → ∀ (n : prog.NodeId), LastAssign prog x run n → n ∈ assigners interp_sup := by - intro vs₁ vs₂ ρ run h x assigners hmem n hla + intro vs₁ vs₂ run h x assigners hmem n hla obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem aesop (add simp Finset.mem_union) interp_inf := by - intro vs₁ vs₂ ρ run h x assigners hmem n hla + intro vs₁ vs₂ run h x assigners hmem n hla obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem aesop (add simp Finset.mem_inter) -private def stepAt (s : prog.State) (obs : Option BasicStmt) { ρ₁ ρ₂ : Env} : EvalBasicStmtOpt ρ₁ obs ρ₂ → Run prog → Run prog - | .none, rest => rest - | .some (bs := bs) _, rest => Run.cons s bs rest + post_pre := by + intro vs s₁ s₂ s₃ ρ₁ ρ₂ tr hedge hvs + simpa [runOfTrace, runOfTraceₗ] using hvs + +private lemma valid_step (s : prog.State) {ρ₁ ρ₂ : Env} + {obs : Option BasicStmt} (hcode : prog.code s = obs) + (hbs : EvalBasicStmtOpt ρ₁ obs ρ₂) + {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 + | 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 [Program.nodeIdOfNonempty, hd, genSet, Option.get] <;> aesop + · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward + (fun hc => hx (List.mem_singleton.mp hc)) hmem + aesop instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where - step := fun s ρ₁ ρ₂ => stepAt prog s (prog.code s) valid := by - simp [StmtEvaluator.eval, eval]; - intro s ρ₁ ρ₂ vs; generalize prog.code s = obs; intro hst hbs hvs - rcases hbs with _ | @⟨_, bs, hbs⟩; try (simpa [stepAt]) - cases hbs with - | noop => intro x assigners hmem n hla; aesop - | assign x e v hev => - simp; 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 [Program.nodeIdOfNonempty, hd, genSet, Option.get] <;> aesop - · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward - (fun hc => hx (List.mem_singleton.mp hc)) hmem - aesop + intro s₁ s₂ ρ₁ ρ₂ ρ₃ vs tr hbs hvs + show ⟦eval prog s₂ vs⟧ (runOfTrace prog (tr ++ hbs)) + simpa [runOfTrace, runOfTraceₗ] using valid_step prog s₂ rfl hbs hvs botV_init := by intro x assigners _ n hla; cases hla theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : - ⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧ ρ - (stepTraceState (prog.trace hrun) (stateInterp prog).init) := - Forward.analyze_correct_state (DefSet prog) prog hrun + ⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧ + (runOfTrace prog (prog.trace hrun)) := + Forward.analyze_correct' (DefSet prog) prog hrun theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf) - {s : prog.State} {ρin ρout : Env} {stin : Run prog} {stout : Run prog} - (hr : Reaches (prog.trace hrun) (stateInterp prog).init s ρin ρout stin stout) : - ⟦ joinForKey s (result (DefSet prog) prog) ⟧ ρin stin - ∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ ρout stout := + {s : prog.State} {ρin ρout : Env} + (hr : Reaches (prog.trace hrun) s ρin ρout) : + ⟦ joinForKey s (result (DefSet prog) prog) ⟧ (runOfTraceₗ prog hr.pre) + ∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ (runOfTrace prog hr.post) := Forward.analyze_correct_at (DefSet prog) prog hrun hr end ReachingAnalysis diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index 69008e8..c2a68f7 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -136,6 +136,61 @@ instance instHAppendTraceTraceR {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ HAppend (Trace g idx₁ idx₂ ρ₁ ρ₂) (Traceᵣ g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where hAppend := Trace.appendRight +/-! + +## Trace Steps + +Analyses that care about *which statements executed* (e.g. reaching +definitions) need to project a trace down to its list of executed statements. +Defining that projection here, once, as a chronological mathlib `List` means +all the re-association facts about concatenating traces come for free from +`List.append_assoc` and friends, instead of being re-proven per analysis. -/ + +/-- The (index, statement) pairs executed by a single optional-statement step: + none if the node is empty, and the node's statement otherwise. -/ +def EvalBasicStmtOpt.steps {α : Type*} (idx : α) {ρ₁ ρ₂ : Env} {obs : Option BasicStmt} : + EvalBasicStmtOpt ρ₁ obs ρ₂ → List (α × BasicStmt) + | .none => [] + | .some (bs := bs) _ => [(idx, bs)] + +/-- The statements executed by a left-open trace, in chronological order. -/ +def Traceₗ.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} : + Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt) + | .nil => [] + | .cons (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps + +/-- The statements executed by a trace, in chronological order. -/ +def Trace.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} : + Trace g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt) + | .single (idx := idx) hnode => hnode.steps idx + | .edge (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps + +@[simp] lemma Traceₗ.steps_append {g : Graph} {idx₁ idx₂ idx₃ : g.Index} + {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂) + (tr₂ : Traceₗ g idx₂ idx₃ ρ₂ ρ₃) : + (tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by + show (tr₁.append tr₂).steps = _ + induction tr₁ <;> simp [Traceₗ.append, Traceₗ.steps, *] + +@[simp] lemma Traceₗ.steps_appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} + {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂) + (tr₂ : Trace g idx₂ idx₃ ρ₂ ρ₃) : + (tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by + show (tr₁.appendTrace tr₂).steps = _ + induction tr₁ <;> simp [Traceₗ.appendTrace, Traceₗ.steps, Trace.steps, *] + +@[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₂ := + Traceₗ.steps_appendTrace tr (Trace.single hbs) + +@[simp] lemma Trace.steps_addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index} + {ρ₁ ρ₂ : Env} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) + (hedge : (idx₂, idx₃) ∈ g.edges) : + (tr.addEdge hedge).steps = tr.steps := by + induction tr <;> simp [Trace.addEdge, Trace.steps, Traceₗ.steps, *] + @[simp] lemma Traceₗ.append_addEdge {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env} (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)