From d2b6bf5af7088252d1fe12416a75f54457aaab98 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 4 Oct 2026 09:58:39 -0500 Subject: [PATCH] Use a unified representation for all trace types --- lean/Spa/Analysis/Forward.lean | 13 +- lean/Spa/Analysis/Reaching.lean | 28 ++- lean/Spa/Language/Properties.lean | 10 - lean/Spa/Language/Traces.lean | 356 ++++++++++++++++-------------- 4 files changed, 211 insertions(+), 196 deletions(-) diff --git a/lean/Spa/Analysis/Forward.lean b/lean/Spa/Analysis/Forward.lean index 81cbdd2..885a3fd 100644 --- a/lean/Spa/Analysis/Forward.lean +++ b/lean/Spa/Analysis/Forward.lean @@ -99,15 +99,18 @@ lemma walkPrefix : ∀ {s₂ s : prog.State} {ρ₂ ρin : Env} ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre trₗ) → ⟦ joinForKey s (result L prog) ⟧ (S.Pre (trₗ ++ mid)) := by intro s₂ s ρ₂ ρin mid - induction mid with - | nil => intro s₁ ρ₁ trₗ hjoin; simpa [HAppend.hAppend, Traceₗ.append] using hjoin - | cons hnode hedge rest ih => + match mid with + | Traceₗ.nil => + intro s₁ ρ₁ trₗ hjoin + simpa only [HAppend.hAppend, Path.append_nil] using hjoin + | Traceₗ.cons hnode hedge rest => intro s₁ ρ₁ trₗ hjoin have hstep := stepTrace trₗ hjoin hnode have hmem := FiniteMap.mem_valuesAt prog.states_nodup (prog.mem_incoming_of_edge hedge) (variablesAt_mem _ (result L prog)) - simpa [HAppend.hAppend, Traceₗ.append] using - ih ((trₗ ++ hnode).addEdge hedge) + simpa only [HAppend.hAppend, Traceₗ.appendStep, Trace.addEdge, + Path.append_assoc, Path.single, Path.append] using + walkPrefix rest ((trₗ ++ hnode).addEdge hedge) (interp_foldr (S.post_pre (trₗ ++ hnode) hedge hstep) hmem) omit [DecidableEq L] in diff --git a/lean/Spa/Analysis/Reaching.lean b/lean/Spa/Analysis/Reaching.lean index 1a43354..323e878 100644 --- a/lean/Spa/Analysis/Reaching.lean +++ b/lean/Spa/Analysis/Reaching.lean @@ -42,7 +42,7 @@ def output : String := /-- 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 + assignment). This is `Path.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) @@ -55,18 +55,19 @@ inductive LastAssign (prog : Program) (x : String) : Run prog → prog.State → (∀ e, bs ≠ .assign x e) → LastAssign prog x 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 runOfPath {a b : Configuration prog.cfg} (p : Path prog.cfg a b) : Run prog := + p.steps.reverse -def runOfTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} - (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog := - tr.steps.reverse +abbrev runOfTraceₗ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} + (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog := runOfPath prog tr + +abbrev runOfTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} + (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog := runOfPath prog tr instance stateInterp : StateInterpretation (DefSet prog) prog where Proj := Run prog - Pre := @runOfTraceₗ prog - Post := @runOfTrace prog + Pre := fun tr => runOfPath prog tr + Post := fun tr => runOfPath prog tr interp vs run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs → ∀ (n : prog.State), LastAssign prog x run n → n ∈ assigners @@ -81,7 +82,8 @@ instance stateInterp : StateInterpretation (DefSet prog) prog where post_pre := by intro vs s₁ s₂ s₃ ρ₁ ρ₂ tr hedge hvs - simpa [runOfTrace, runOfTraceₗ] using hvs + 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) @@ -109,8 +111,10 @@ private lemma valid_step (s : prog.State) {ρ₁ ρ₂ : Env} instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where valid := by 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 + 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 botV_init := by intro x assigners _ n hla; cases hla theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) : diff --git a/lean/Spa/Language/Properties.lean b/lean/Spa/Language/Properties.lean index 08caeb6..9902f3a 100644 --- a/lean/Spa/Language/Properties.lean +++ b/lean/Spa/Language/Properties.lean @@ -27,16 +27,6 @@ section Embeddings variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env} -/-- Transport a trace along a graph embedding: an embedding preserves node - payloads and edges, which is everything a trace is made of. This is the - single induction behind all the per-operator lifting corollaries below. -/ -noncomputable def Trace.embed {g h : Graph} (e : GGraph.Embed g h) - {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) : - Trace h (e.f idx₁) (e.f idx₂) ρ₁ ρ₂ := by - induction tr with - | single hbs => exact Trace.single (by rwa [e.nodes_eq]) - | edge hbs he _ ih => exact Trace.edge (by rwa [e.nodes_eq]) (e.edges_mem he) ih - /-- When two graphs are overlaid, for each trace in the left graph, a corresponding trace exists in the combined graph. -/ noncomputable def Trace.overlay_left {idx₁ idx₂ : g₁.Index} diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean index 2c8e779..409dc10 100644 --- a/lean/Spa/Language/Traces.lean +++ b/lean/Spa/Language/Traces.lean @@ -1,21 +1,22 @@ -import Spa.Language.Semantics import Spa.Language.Graphs import Spa.Language.Program +import Spa.Language.Semantics /-! # Program Traces This module defines program traces tied to Control Flow Graphs, or CFGs -(see `Spa.GGraph` and `Spa.Graph`). These traces boil town to sequences of +(see `Spa.GGraph` and `Spa.Graph`). These traces boil down to sequences of basic-block executions (really, `Spa.BasicStmt` executions), each of which must have an actual basic block in the graph _and_ be connected to the previous basic block by an edge. In this way, traces encode executions admitted by the CFG. -While the regular `Trace` is just _any_ path through the graph, an -`EndToEndTrace` is a path from the entry node to the exit node, denoting -full program execution. +`Path` interleaves execution and edge steps, with endpoints recording whether +we are before or after a node. `Trace`, `Traceₗ`, and `Traceᵣ` are endpoint +specializations of this one type. An `EndToEndTrace` runs from a graph input +to a graph output, denoting full program execution. Properties about graphs and language semantics (especially, the fact that the graph contains the proper basic block and edges @@ -27,211 +28,229 @@ in `Spa/Language/Properties.lean`. namespace Spa -/-- A partial trace through a graph `g`, starting right before - the execution of the basic block at the first index, and - ending right after the execution of the basic block at the last index. -/ -inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type - | single {ρ₁ ρ₂ : Env} {idx : g.Index} : - EvalBasicStmtOpt ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂ - | edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} : - EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges → - Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃ +/-- A node together with the phase of its execution. -/ +inductive Position (α : Type) where + | before : α → Position α + | after : α → Position α + deriving DecidableEq -/-! +abbrev Configuration (g : Graph) := Position g.Index × Env -## Open Traces +/-- Executing a node changes the environment; following an edge preserves it. -/ +inductive Step (g : Graph) : Configuration g → Configuration g → Type where + | execute {i : g.Index} {ρ ρ' : Env} + (h : EvalBasicStmtOpt ρ (g.nodes i) ρ') : + Step g (.before i, ρ) (.after i, ρ') + | edge {i j : g.Index} {ρ : Env} (h : (i, j) ∈ g.edges) : + Step g (.after i, ρ) (.before j, ρ) -A normal `Trace` starts right before one state, and ends right after another. -This is convenient for inductively proving correctness / sufficience, but -awkward because 1) no empty traces exist and 2) concatenation requires an extra -edge. +/-- A concrete CFG path, including executions of statement-less nodes. -/ +inductive Path (g : Graph) : Configuration g → Configuration g → Type where + | nil {a} : Path g a a + | cons {a b c} : Step g a b → Path g b c → Path g a c -However, when attempting an "empty" trace, two types are equally possible: -traces that end _right before_ executing a state (`Traceₗ`) and -traces that begin _right after_ executing a state (`Traceᵣ`). They -are symmetric and can be concatenated with full traces on the left -and right, respectively. -/ +namespace Path -/-- Left-open trace, representing execution that ends right before `idx₂`. -/ -inductive Traceₗ (g : Graph) : g.Index → g.Index → Env → Env → Type where - | nil {idx : g.Index} {ρ : Env} : Traceₗ g idx idx ρ ρ - | cons {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → - (idx₁, idx₂) ∈ g.edges → - Traceₗ g idx₂ idx₃ ρ₂ ρ₃ → Traceₗ g idx₁ idx₃ ρ₁ ρ₃ +variable {g : Graph} {a b c d : Configuration g} -def Traceₗ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceₗ g idx idx ρ ρ := .nil +@[match_pattern] def single (s : Step g a b) : Path g a b := .cons s .nil -/-- Right-open trace, representing execution that starts right after `idx₁`. -/ -inductive Traceᵣ (g : Graph) : g.Index → g.Index → Env → Env → Type where - | nil {idx : g.Index} {ρ : Env} : Traceᵣ g idx idx ρ ρ - | cons {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - Traceᵣ g idx₁ idx₂ ρ₁ ρ₂ → - (idx₂, idx₃) ∈ g.edges → - EvalBasicStmtOpt ρ₂ (g.nodes idx₃) ρ₃ → Traceᵣ g idx₁ idx₃ ρ₁ ρ₃ +def append {a b c : Configuration g} : Path g a b → Path g b c → Path g a c + | .nil, q => q + | .cons s p, q => .cons s (p.append q) -def Traceᵣ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceᵣ g idx idx ρ ρ := .nil +instance : HAppend (Path g a b) (Path g b c) (Path g a c) := ⟨append⟩ -/-- Sequence two traces together. Since the endpoint of the first trace - is _after_ its last basic block's execution, and the beginning of - the next trace is _before_ its first basic block's execution, - there must be an edge to connect the two. -/ -def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index} - {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂) - (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) : - Trace g idx₁ idx₄ ρ₁ ρ₃ := - match tr₁ with - | single hbs => edge hbs he tr₂ - | edge hbs he' tr₁' => edge hbs he' (tr₁'.concat he tr₂) +@[simp] lemma nil_append (p : Path g a b) : Path.nil.append p = p := rfl + +@[simp] lemma append_nil (p : Path g a b) : p.append Path.nil = p := by + induction p <;> aesop (add simp append) + +lemma append_assoc (p : Path g a b) (q : Path g b c) (r : Path g c d) : + (p.append q).append r = p.append (q.append r) := by + induction p <;> aesop (add simp append) + +end Path + +def GGraph.Embed.mapConfiguration {g h : Graph} (e : GGraph.Embed g h) : + Configuration g → Configuration h + | (.before i, ρ) => (.before (e.f i), ρ) + | (.after i, ρ) => (.after (e.f i), ρ) + +lemma GGraph.Embed.mapConfiguration_trans {g h k : Graph} + (e : GGraph.Embed g h) (f : GGraph.Embed h k) (a : Configuration g) : + f.mapConfiguration (e.mapConfiguration a) = (e.trans f).mapConfiguration a := by + rcases a with ⟨_ | _, ρ⟩ <;> rfl + +noncomputable def Step.embed {g h : Graph} (e : GGraph.Embed g h) + {a b : Configuration g} : Step g a b → Step h (e.mapConfiguration a) (e.mapConfiguration b) + | .execute h => .execute (_root_.cast (congrArg (EvalBasicStmtOpt _ · _) (e.nodes_eq _).symm) h) + | .edge h => .edge (e.edges_mem h) + +noncomputable def Path.embed {g h : Graph} (e : GGraph.Embed g h) + {a b : Configuration g} : Path g a b → Path h (e.mapConfiguration a) (e.mapConfiguration b) + | .nil => .nil + | .cons s p => .cons (s.embed e) (p.embed e) + +lemma Path.embed_append {g h : Graph} (e : GGraph.Embed g h) + {a b c : Configuration g} (p : Path g a b) (q : Path g b c) : + (p.append q).embed e = (p.embed e).append (q.embed e) := by + induction p <;> aesop (add simp [append, embed]) + +/-- Transport endpoints without changing the path. -/ +def Path.cast {g : Graph} {a b a' b' : Configuration g} + (ha : a = a') (hb : b = b') (p : Path g a b) : Path g a' b' := ha ▸ hb ▸ p + +lemma Path.embed_trans {g h k : Graph} (e : GGraph.Embed g h) (f : GGraph.Embed h k) + {a b : Configuration g} (p : Path g a b) : + ((p.embed e).embed f).cast (e.mapConfiguration_trans f a) + (e.mapConfiguration_trans f b) = p.embed (e.trans f) := by + induction p with + | @nil a => rcases a with ⟨_ | _, ρ⟩ <;> rfl + | @cons a b c s p ih => + rcases c with ⟨_ | _, ρ⟩ <;> cases s <;> + aesop (add simp [embed, Step.embed, cast, GGraph.Embed.mapConfiguration, cast_cast]) + +/-- A trace includes the executions of both endpoint nodes. -/ +abbrev Trace (g : Graph) (i j : g.Index) (ρ ρ' : Env) := + Path g (.before i, ρ) (.after j, ρ') + +/-- A prefix ending before execution of its final node. -/ +abbrev Traceₗ (g : Graph) (i j : g.Index) (ρ ρ' : Env) := + Path g (.before i, ρ) (.before j, ρ') + +/-- A suffix starting after execution of its initial node. -/ +abbrev Traceᵣ (g : Graph) (i j : g.Index) (ρ ρ' : Env) := + Path g (.after i, ρ) (.after j, ρ') + +/-- Compatibility patterns for an execution and an execution-edge pair. -/ +@[match_pattern] abbrev Trace.single {g : Graph} {ρ₁ ρ₂ : Env} {idx : g.Index} + (h : EvalBasicStmtOpt ρ₁ (g.nodes idx) ρ₂) : Trace g idx idx ρ₁ ρ₂ := + .cons (.execute h) .nil + +@[match_pattern] abbrev Trace.edge {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} + {idx₁ idx₂ idx₃ : g.Index} (h : EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂) + (he : (idx₁, idx₂) ∈ g.edges) (p : Trace g idx₂ idx₃ ρ₂ ρ₃) : + Trace g idx₁ idx₃ ρ₁ ρ₃ := Path.cons (.execute h) (.cons (.edge he) p) + +@[match_pattern] abbrev Traceₗ.nil {g : Graph} {idx : g.Index} {ρ : Env} : + Traceₗ g idx idx ρ ρ := Path.nil + +@[match_pattern] abbrev Traceₗ.cons {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} + {idx₁ idx₂ idx₃ : g.Index} (h : EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂) + (he : (idx₁, idx₂) ∈ g.edges) (p : Traceₗ g idx₂ idx₃ ρ₂ ρ₃) : + Traceₗ g idx₁ idx₃ ρ₁ ρ₃ := Path.cons (.execute h) (.cons (.edge he) p) + +@[match_pattern] abbrev Traceᵣ.nil {g : Graph} {idx : g.Index} {ρ : Env} : Traceᵣ g idx idx ρ ρ := Path.nil + +abbrev Traceᵣ.cons {g : Graph} {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} + (p : Traceᵣ g idx₁ idx₂ ρ₁ ρ₂) (he : (idx₂, idx₃) ∈ g.edges) + (h : EvalBasicStmtOpt ρ₂ (g.nodes idx₃) ρ₃) : Traceᵣ g idx₁ idx₃ ρ₁ ρ₃ := + p.append (.cons (.edge he) (.single (.execute h))) + +abbrev Traceₗ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceₗ g idx idx ρ ρ := .nil +abbrev Traceᵣ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceᵣ g idx idx ρ ρ := .nil + +abbrev Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} + (p : Trace g idx₁ idx₂ ρ₁ ρ₂) (he : (idx₂, idx₃) ∈ g.edges) + (q : Trace g idx₃ idx₄ ρ₂ ρ₃) : Trace g idx₁ idx₄ ρ₁ ρ₃ := + (p.append (.single (.edge he))).append q scoped notation:65 tr₁:66 " ++< " he " >++ " tr₂:65 => Trace.concat tr₁ he tr₂ -def Trace.addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ : Env} : - Trace g idx₁ idx₂ ρ₁ ρ₂ → - (idx₂, idx₃) ∈ g.edges → - Traceₗ g idx₁ idx₃ ρ₁ ρ₂ - | .single hnode, hedge => .cons hnode hedge .nil - | .edge hnode hedge' rest, hedge => .cons hnode hedge' (rest.addEdge hedge) +abbrev Trace.addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ : Env} + (p : Trace g idx₁ idx₂ ρ₁ ρ₂) (he : (idx₂, idx₃) ∈ g.edges) : + Traceₗ g idx₁ idx₃ ρ₁ ρ₂ := p.append (.single (.edge he)) -@[aesop simp] -def Traceₗ.append {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → Traceₗ g idx₂ idx₃ ρ₂ ρ₃ → - Traceₗ g idx₁ idx₃ ρ₁ ρ₃ - | .nil, rhs => rhs - | .cons hnode hedge rest, rhs => .cons hnode hedge (rest.append rhs) +abbrev Traceₗ.append {g : Graph} {i j k : g.Index} {ρ₁ ρ₂ ρ₃ : Env} + (p : Traceₗ g i j ρ₁ ρ₂) (q : Traceₗ g j k ρ₂ ρ₃) : Traceₗ g i k ρ₁ ρ₃ := + Path.append p q -@[simp] def traceₗ_append_nil {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} - {trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂} : trₗ.append Traceₗ.nil = trₗ := by - induction trₗ <;> aesop +abbrev Traceₗ.appendTrace {g : Graph} {i j k : g.Index} {ρ₁ ρ₂ ρ₃ : Env} + (p : Traceₗ g i j ρ₁ ρ₂) (q : Trace g j k ρ₂ ρ₃) : Trace g i k ρ₁ ρ₃ := + Path.append p q -def Traceₗ.appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → Trace g idx₂ idx₃ ρ₂ ρ₃ → - Trace g idx₁ idx₃ ρ₁ ρ₃ - | .nil, rhs => rhs - | .cons hnode hedge rest, rhs => .edge hnode hedge (rest.appendTrace rhs) +abbrev Trace.appendRight {g : Graph} {i j k : g.Index} {ρ₁ ρ₂ ρ₃ : Env} + (p : Trace g i j ρ₁ ρ₂) (q : Traceᵣ g j k ρ₂ ρ₃) : Trace g i k ρ₁ ρ₃ := + Path.append p q -def Traceₗ.appendStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃ → - Trace g idx₁ idx₂ ρ₁ ρ₃ := fun trₗ hbs => trₗ.appendTrace (Trace.single hbs) +noncomputable abbrev Trace.embed {g h : Graph} (e : GGraph.Embed g h) + {i j : g.Index} {ρ₁ ρ₂ : Env} (p : Trace g i j ρ₁ ρ₂) : + Trace h (e.f i) (e.f j) ρ₁ ρ₂ := Path.embed e p -def Trace.appendRight {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - Trace g idx₁ idx₂ ρ₁ ρ₂ → Traceᵣ g idx₂ idx₃ ρ₂ ρ₃ → - Trace g idx₁ idx₃ ρ₁ ρ₃ - | lhs, .nil => lhs - | lhs, .cons rest hedge hnode => Trace.concat (lhs.appendRight rest) hedge (.single hnode) +abbrev Traceₗ.appendStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} + (p : Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (h : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) : + Trace g idx₁ idx₂ ρ₁ ρ₃ := Path.append p (.single (.execute h)) -instance instHAppendTraceLTraceL {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (Traceₗ g idx₂ idx₃ ρ₂ ρ₃) (Traceₗ g idx₁ idx₃ ρ₁ ρ₃) where - hAppend := Traceₗ.append +instance {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : + HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) + (Trace g idx₁ idx₂ ρ₁ ρ₃) := ⟨Traceₗ.appendStep⟩ -instance instHAppendTraceLTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (Trace g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where - hAppend := Traceₗ.appendTrace - -instance instHAppendTraceLStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) (Trace g idx₁ idx₂ ρ₁ ρ₃) where - hAppend := Traceₗ.appendStep - -instance instHAppendTraceTraceR {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} : - 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. -/ +/-- The (index, statement) pairs executed by a single optional-statement step. -/ 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) +def Step.steps {g : Graph} {a b : Configuration g} : Step g a b → List (g.Index × BasicStmt) + | .execute (i := i) h => h.steps i + | .edge _ => [] + +/-- Executed statements in chronological order; edges and empty nodes contribute nothing. -/ +def Path.steps {g : Graph} {a b : Configuration g} : Path g a b → List (g.Index × BasicStmt) | .nil => [] - | .cons (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps + | .cons s p => s.steps ++ p.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 +abbrev Trace.steps {g : Graph} {i j : g.Index} {ρ₁ ρ₂ : Env} + (p : Trace g i j ρ₁ ρ₂) : List (g.Index × BasicStmt) := Path.steps p +abbrev Traceₗ.steps {g : Graph} {i j : g.Index} {ρ₁ ρ₂ : Env} + (p : Traceₗ g i j ρ₁ ρ₂) : List (g.Index × BasicStmt) := Path.steps p +abbrev Traceᵣ.steps {g : Graph} {i j : g.Index} {ρ₁ ρ₂ : Env} + (p : Traceᵣ g i j ρ₁ ρ₂) : List (g.Index × BasicStmt) := Path.steps p -@[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 Path.steps_append {g : Graph} {a b c : Configuration g} + (p : Path g a b) (q : Path g b c) : + (p.append q).steps = p.steps ++ q.steps := by + induction p <;> aesop (add simp [append, steps, List.append_assoc]) @[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) + (tr ++ hbs).steps = tr.steps ++ hbs.steps idx₂ := by + change Path.steps (Path.append tr (Path.single (.execute hbs))) = _ + aesop (add simp [Trace.steps, Traceₗ.steps, Path.single, Path.steps, Step.steps]) @[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₂ ρ₁ ρ₂) - (hnode : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) - (hedge : (idx₂, idx₃) ∈ g.edges) - (rest : Traceₗ g idx₃ idx₄ ρ₃ ρ₄) : - trₗ.append (Traceₗ.cons hnode hedge rest) = - (Trace.addEdge (trₗ.appendStep hnode) hedge).append rest := by - induction trₗ <;> simp [Traceₗ.append, Traceₗ.appendStep, Traceₗ.appendTrace, Trace.addEdge, *] - -@[simp] lemma Traceₗ.appendTrace_addEdge {g : Graph} - {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env} - (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂) - (hnode : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) - (hedge : (idx₂, idx₃) ∈ g.edges) - (rest : Trace g idx₃ idx₄ ρ₃ ρ₄) : - trₗ.appendTrace (Trace.edge hnode hedge rest) = - (Trace.addEdge (trₗ.appendStep hnode) hedge).appendTrace rest := by - induction trₗ <;> simp [Traceₗ.appendTrace, Traceₗ.appendStep, Trace.addEdge, *] + {ρ₁ ρ₂ : Env} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) (he : (idx₂, idx₃) ∈ g.edges) : + (tr.addEdge he).steps = tr.steps := by + change Path.steps (Path.append tr (Path.single (.edge he))) = _ + aesop (add simp [Trace.steps, Traceₗ.steps, Path.single, Path.steps, Step.steps]) /-- A beginning-to-end trace corresponding to the CFG `g`. -/ -inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type - | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs) - (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs) - (trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂ +structure EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type where + intro :: + entry : g.Index + entry_mem : entry ∈ g.inputs + exit : g.Index + exit_mem : exit ∈ g.outputs + trace : Trace g entry exit ρ₁ ρ₂ -/-- Every trace splits into the prefix that arrives at its last node and that node's own step. -/ +/-- Every trace splits into the prefix arriving at its last node and that node's execution. -/ def Trace.split {g : Graph} {i₁ i₂ : g.Index} {ρ₁ ρ₂ : Env} : Trace g i₁ i₂ ρ₁ ρ₂ → Σ ρ, Traceₗ g i₁ i₂ ρ₁ ρ × EvalBasicStmtOpt ρ (g.nodes i₂) ρ₂ - | .single hnode => ⟨_, .nil, hnode⟩ - | .edge hnode hedge rest => + | Trace.single h => ⟨_, .nil, h⟩ + | Trace.edge h he rest => let ⟨ρ, pre, step⟩ := rest.split - ⟨ρ, .cons hnode hedge pre, step⟩ + ⟨ρ, Traceₗ.cons h he pre, step⟩ @[simp] lemma Trace.split_append {g : Graph} {i₁ i₂ : g.Index} {ρ₁ ρ₂ : Env} (tr : Trace g i₁ i₂ ρ₁ ρ₂) : tr.split.2.1 ++ tr.split.2.2 = tr := by - induction tr with - | single hnode => rfl - | edge hnode hedge rest ih => - show Traceₗ.appendStep _ _ = _ - simpa [Trace.split, Traceₗ.appendStep, Traceₗ.appendTrace] using ih + match tr with + | Trace.single h => rw [Trace.split.eq_1]; rfl + | Trace.edge h he rest => + have ih := Trace.split_append rest + rw [Trace.split.eq_2] + aesop (add simp [HAppend.hAppend, Traceₗ.appendStep, Path.append]) structure Reaches {prog : Program} (s : prog.State) (ρin ρout : Env) : Type where pre : Traceₗ prog.cfg prog.initialState s [] ρin @@ -242,5 +261,4 @@ def Reaches.post {prog : Program} {s : prog.State} {ρin ρout : Env} (r : Reaches s ρin ρout) : Trace prog.cfg prog.initialState s [] ρout := r.pre ++ r.step - end Spa