Use a unified representation for all trace types

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

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 ρ) :

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}

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