Consolidate per-operator trace lifting into GGraph.Embed + Trace.embed

Each graph-composition operator includes its operands via an index
translation preserving node payloads and edges. Capture that once as
GGraph.Embed (a structure, not a class: for g ; g both inclusions share
the type Embed g (g <~> g), so instance resolution could pick the wrong
copy) with five named witnesses, and replace the five structurally
identical trace-lifting inductions in Properties.lean with a single
generic Trace.embed plus one-line corollaries.

The same witnesses' nodes_eq fields will back the upcoming AST-id/CFG
label bijection, so the per-operator content is stated exactly once.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

lean/Spa/Analysis/Constant.lean

@@ -134,14 +134,14 @@ instance eval_valid : ValidExprEvaluator ConstLattice prog := by
     exact minus_valid h₁ h₂
 
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ () :=
+    ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ :=
   Forward.analyze_correct ConstLattice prog hrun
 
 theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env} {stin stout : PUnit}
-    (hr : Reaches (L := ConstLattice) (prog.trace hrun) PUnit.unit s ρin ρout stin stout) :
-    ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin stin
-      ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout stout :=
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin
+      ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout :=
   Forward.analyze_correct_at ConstLattice prog hrun hr
 
 end ConstAnalysis

lean/Spa/Analysis/Forward.lean

@@ -55,70 +55,38 @@ lemma joinForKey_initialState :
 
 class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
     [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
-  step : (s : prog.State) → {ρ₁ ρ₂ : Env} → EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → S.St ρ₁ → S.St ρ₂
-  valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env}
-    {vs : VariableValues L prog} {st : S.St ρ₁},
-    (hbs : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) → ⟦ vs ⟧ ρ₁ st →
-    ⟦ E.eval s vs ⟧ ρ₂ (step s hbs st)
-  botV_init : ⟦ botV L prog ⟧ [] S.init
+  valid : ∀ (s₁ s₂ : prog.State) {ρ₁ ρ₂ ρ₃: Env}
+    {vs : VariableValues L prog},
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) →
+    (hbs : EvalBasicStmtOpt ρ₂ (prog.cfg.nodes s₂) ρ₃) → ⟦ vs ⟧ (S.Pre tr) →
+    ⟦ E.eval s₂ vs ⟧ (S.Post (tr ++ hbs))
+  botV_init : ⟦ botV L prog ⟧ (S.Pre (Traceₗ.single prog.cfg prog.initialState []))
 
 instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
     ValidStateEvaluator L prog where
-  step := by intro _ _ _ _ _; exact PUnit.unit
-  valid := by intro _ _ _ _ _ hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
+  valid := by intro _ _ _ _ _ _ tr hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
   botV_init := by intro k l _ v hmem; cases hmem
 
 section
 variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]
 
-noncomputable def stepNode (s : prog.State) {ρ₁ ρ₂ : Env}
-    (h : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) (st : S.St ρ₁) : S.St ρ₂ :=
-  V.step s h st
-
-noncomputable def stepTraceState :
-    {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
-    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → S.St ρ₁ → S.St ρ₂
-  | s₁, _, _, _, .single hnode, st => stepNode s₁ hnode st
-  | s₁, _, _, _, .edge hnode _ subtr, st =>
-      stepTraceState subtr (stepNode s₁ hnode st)
-
-/-- `Reaches tr st₁ s ρin ρout stin stout` witnesses that, when the trace `tr`
-    (starting at state `st₁`) is executed, node `s` is visited at some point: `ρin`
-    and `ρout` are the concrete environments just before and after `s`'s basic block
-    runs, and `stin`/`stout` are the corresponding abstract execution states. A node
-    inside a loop is reached once per iteration, each with its own environments. -/
-inductive Reaches : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
-    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → S.St ρ₁ →
-    (s : prog.State) → (ρin ρout : Env) → S.St ρin → S.St ρout → Prop
-  | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
-      Reaches (.single hnode) st₁ s₁ ρ₁ ρ₂ st₁ (stepNode s₁ hnode st₁)
-  | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} {st₁ : S.St ρ₁}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
-      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) :
-      Reaches (.edge hnode hedge rest) st₁ s₁ ρ₁ ρ₂ st₁ (stepNode s₁ hnode st₁)
-  | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} {st₁ : S.St ρ₁}
-      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
-      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃)
-      {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout} :
-      Reaches rest (stepNode s₁ hnode st₁) s ρin ρout stin stout →
-      Reaches (.edge hnode hedge rest) st₁ s ρin ρout stin stout
-
 omit [DecidableEq L] in
-lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog}
-    {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
-    (hnode : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂)
-    (hvs : ⟦ variablesAt s sv ⟧ ρ₁ st) :
-    ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ (stepNode s hnode st) := by
+lemma updateAll_matches {s₁ s₂ : prog.State} {sv : StateVariables L prog}
+    {ρ₁ ρ₂ ρ₃ : Env}
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃)
+    (hvs : ⟦ variablesAt s₂ sv ⟧ (S.Pre tr)) :
+    ⟦ variablesAt s₂ (updateAll sv) ⟧ (S.Post (tr ++ hnode)) := by
   rw [variablesAt_updateAll]
-  exact V.valid s hnode hvs
+  exact V.valid s₁ s₂ tr hnode hvs
 
-lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
-    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st)
-    (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
-    ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ (stepNode s₁ hnode st) := by
+lemma stepTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre tr))
+    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃) :
+    ⟦ variablesAt s₂ (result L prog) ⟧ (S.Post (tr ++ hnode)) := by
   rw [result_eq L prog]
-  refine updateAll_matches hnode ?_
+  refine updateAll_matches tr hnode ?_
   rw [variablesAt_joinAll]
   exact hjoin
 
@@ -127,49 +95,50 @@ lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
     way it over-approximates both the environment entering that node (via `joinForKey`)
     and the environment leaving it (via `variablesAt`). The intermediate `variablesAt`
     evidence used to be computed and discarded inside `walkTrace`; here it is returned. -/
-lemma walkTrace_reaches {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
-    {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout}
-    {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂}
-    (hr : Reaches tr st₁ s ρin ρout stin stout)
-    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁) :
-    ⟦ joinForKey s (result L prog) ⟧ ρin stin
-      ∧ ⟦ variablesAt s (result L prog) ⟧ ρout stout := by
+lemma walkTrace_reaches {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ ρ₃: Env}
+    {s : prog.State} {ρin ρout : Env}
+    {tr : Trace prog.cfg s₂ s₃ ρ₂ ρ₃}
+    (hr : Reaches tr s ρin ρout)
+    (trₗ : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre trₗ)) :
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre (trₗ ++ hr.pre))
+      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post (trₗ ++ hr.post)) := by
   induction hr with
-  | single_here hnode => exact ⟨hjoin, stepTrace hjoin hnode⟩
-  | edge_here hnode hedge rest => exact ⟨hjoin, stepTrace hjoin hnode⟩
+  | single_here hnode =>
+    simp [Reaches.pre, Reaches.post]
+    refine ⟨?_, ?_⟩ <;> try simpa [HAppend.hAppend]
+    exact stepTrace trₗ hjoin hnode
+  | edge_here hnode hedge rest =>
+    simp [Reaches.pre, Reaches.post]
+    refine ⟨?_, ?_⟩ <;> try simpa [HAppend.hAppend]
+    exact stepTrace trₗ hjoin hnode
   | edge_there hnode hedge rest hr' ih =>
-    have hstep := stepTrace hjoin hnode
+    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))
-    exact ih (interp_foldr hstep hmem)
+    simpa [Reaches.pre, Reaches.post, HAppend.hAppend] using
+      ih ((trₗ ++ hnode).addEdge hedge)
+        (interp_foldr (S.post_pre (trₗ ++ hnode) hedge hstep) hmem)
 
 omit [DecidableEq L] in
 /-- The final node of a trace is always reached, with the environment/state the trace
     ends in. Used to recover the final-state soundness theorem from `walkTrace_reaches`. -/
-lemma reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} (st₁ : S.St ρ₁)
+def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
     (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
-    ∃ ρin, ∃ stin : S.St ρin,
-      Reaches tr st₁ s₂ ρin ρ₂ stin (stepTraceState tr st₁) := by
+    Σ ρin, Reaches tr s₂ ρin ρ₂ :=
+  match tr with
+  | .single hnode => ⟨_, .single_here hnode⟩
+  | .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 => exact ⟨_, _, .single_here hnode⟩
-  | edge hnode hedge rest ih =>
-    obtain ⟨ρin, stin, hr⟩ := ih (stepNode _ hnode st₁)
-    exact ⟨ρin, stin, .edge_there hnode hedge rest hr⟩
-
-lemma walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
-    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁)
-    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
-    ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ (stepTraceState tr st₁) := by
-  obtain ⟨_, _, hr⟩ := reaches_final st₁ tr
-  exact (walkTrace_reaches hr hjoin).2
-
-variable (L prog) in
-theorem analyze_correct_state {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ
-      (stepTraceState (prog.trace hrun) S.init) := by
-  refine walkTrace ?_ (prog.trace hrun)
-  rw [joinForKey_initialState]
-  exact ValidStateEvaluator.botV_init
+  | 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
@@ -177,21 +146,28 @@ variable (L prog) in
     environment entering `s` and the one leaving it. The final-state theorem
     `analyze_correct_state` is the special case where `s` is `prog.finalState`. -/
 theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout}
-    (hr : Reaches (prog.trace hrun) S.init s ρin ρout stin stout) :
-    ⟦ joinForKey s (result L prog) ⟧ ρin stin
-      ∧ ⟦ variablesAt s (result L prog) ⟧ ρout stout := by
-  refine walkTrace_reaches hr ?_
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre hr.pre)
+      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post hr.post) := by
+  refine walkTrace_reaches hr (Traceₗ.single _ _ []) ?_
   rw [joinForKey_initialState]
   exact ValidStateEvaluator.botV_init
 
+variable (L prog) in
+theorem analyze_correct'
+    {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    ⟦ 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
 
 variable (L prog) in
 theorem analyze_correct [LatticeInterpretation L] [ValidStmtEvaluator L prog]
     {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ () :=
-  analyze_correct_state L prog hrun
+    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
+  analyze_correct' L prog hrun
 
 end Forward
 

lean/Spa/Analysis/Forward/Evaluation.lean

@@ -17,12 +17,12 @@ class ExprEvaluator where
 class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
     Prop where
   valid : ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value},
-    EvalExpr ρ e v → ⟦ vs ⟧ ρ () → I.interp (ExprEvaluator.eval e vs) v
+    EvalExpr ρ e v → ⟦ vs ⟧ ρ → I.interp (ExprEvaluator.eval e vs) v
 
 class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
     Prop where
   valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env},
-    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s vs ⟧ ρ₂ ()
+    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s vs ⟧ ρ₂
 
 end Forward
 

lean/Spa/Analysis/Forward/Lattices.lean

@@ -65,22 +65,28 @@ lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
   joinAll_mem_eq (variablesAt_mem s (joinAll sv))
 
 class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
-  St : Env → Type
-  init : St []
-  interp : VariableValues L prog → (ρ : Env) → St ρ → Prop
-  interp_sup : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ},
-    interp vs₁ ρ st ∨ interp vs₂ ρ st → interp (vs₁ ⊔ vs₂) ρ st
-  interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ},
-    interp vs₁ ρ st ∧ interp vs₂ ρ st → interp (vs₁ ⊓ vs₂) ρ st
+  Proj : Type
+  Pre : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
+  Post : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
+
+  interp : VariableValues L prog → (p : Proj) → Prop
+  interp_sup : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj},
+    interp vs₁ p ∨ interp vs₂ p → interp (vs₁ ⊔ vs₂) p
+  interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj},
+    interp vs₁ p ∧ interp vs₂ p → interp (vs₁ ⊓ vs₂) p
+
+  post_pre : ∀ {vs} {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) (hedge : (s₂, s₃) ∈ prog.cfg.edges),
+    interp vs (Post tr) → interp vs (Pre (tr.addEdge hedge))
 
 instance [S : StateInterpretation L prog] :
-    Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → Prop) :=
+    Interp (VariableValues L prog) (S.Proj → Prop) :=
   ⟨S.interp⟩
 
 lemma interp_foldr [S : StateInterpretation L prog]
     {vs : VariableValues L prog} {vss : List (VariableValues L prog)}
-    {ρ : Env} {st : S.St ρ} (hvs : ⟦ vs ⟧ ρ st) (hmem : vs ∈ vss) :
-    ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ st := by
+    {p : S.Proj} (hvs : ⟦ vs ⟧ p) (hmem : vs ∈ vss) :
+    ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ p := by
   induction vss with
   | nil => cases hmem
   | cons vs' vss' ih =>
@@ -91,20 +97,24 @@ lemma interp_foldr [S : StateInterpretation L prog]
 variable [I : LatticeInterpretation L]
 
 instance : StateInterpretation L prog where
-  St := fun _ => PUnit
-  init := PUnit.unit
-  interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs →
+  Proj := Env
+  Pre := fun {_ _ _ ρ₂} _ => ρ₂
+  Post := fun {_ _ _ ρ₂} _ => ρ₂
+
+  interp vs ρ := ∀ (k : String) (l : L), (k, l) ∈ vs →
     ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
   interp_sup := by
-    intro vs₁ vs₂ ρ st h k l hmem v hv
+    intro vs₁ vs₂ ρ h k l hmem v hv
     obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
     rcases h with h | h
     · exact I.interp_sup v (Or.inl (h _ _ h₁ _ hv))
     · exact I.interp_sup v (Or.inr (h _ _ h₂ _ hv))
   interp_inf := by
-    intro vs₁ vs₂ ρ st h k l hmem v hv
+    intro vs₁ vs₂ ρ h k l hmem v hv
     obtain ⟨l₁, l₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem
     exact I.interp_inf v ⟨h.1 _ _ h₁ _ hv, h.2 _ _ h₂ _ hv⟩
+  post_pre := by simp
+
 
 end Forward
 

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

lean/Spa/Analysis/Sign.lean

@@ -210,14 +210,14 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
     exact minus_valid h₁ h₂
 
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ () :=
+    ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ :=
   Forward.analyze_correct SignLattice prog hrun
 
 theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
-    {s : prog.State} {ρin ρout : Env} {stin stout : PUnit}
-    (hr : Reaches (L := SignLattice) (prog.trace hrun) PUnit.unit s ρin ρout stin stout) :
-    ⟦ joinForKey s (result SignLattice prog) ⟧ ρin stin
-      ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout stout :=
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result SignLattice prog) ⟧ ρin
+      ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout :=
   Forward.analyze_correct_at SignLattice prog hrun hr
 
 end SignAnalysis

lean/Spa/Language/Graphs.lean

@@ -213,6 +213,65 @@ lemma wrap_outputs (g : GGraph (Option β)) :
     (Option.map h) <$> wrap g = wrap (Option.map h <$> g) := by
   simp [GGraph.wrap, GGraph.map_sequence, GGraph.map_singleton]
 
+/-! ### Embeddings
+
+Each composition operator includes its operands into the result via an index
+translation that preserves node payloads and edges. `Embed` captures exactly
+those two facts, so anything defined from `nodes` and `edges` (traces, node
+labels, …) can be transported along an embedding once, instead of once per
+operator.
+
+`Embed` is deliberately a structure rather than a class: for `g ⤳ g`, both the
+left and the right inclusion inhabit the same type `Embed g (g ⤳ g)`, so
+instance resolution could silently pick the wrong copy. Embeddings into a
+composed graph are non-canonical by design; a named witness says which
+inclusion is meant. -/
+
+/-- An embedding of graph `g` into graph `h`: an index translation that
+    preserves node payloads and edges. -/
+structure Embed (g h : GGraph α) where
+  f : g.Index → h.Index
+  nodes_eq : ∀ i, h.nodes (f i) = g.nodes i
+  edges_mem : ∀ {e : g.Edge}, e ∈ g.edges → (f e.1, f e.2) ∈ h.edges
+
+/-- Embeddings compose. -/
+def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Embed g₂ g₃) :
+    Embed g₁ g₃ where
+  f := e₂.f ∘ e₁.f
+  nodes_eq i := (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i)
+  edges_mem he := e₂.edges_mem (e₁.edges_mem he)
+
+/-- The left operand's inclusion into a sequenced graph. -/
+def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) where
+  f i := i.castAdd g₂.size
+  nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
+  edges_mem he := List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
+
+/-- The right operand's inclusion into a sequenced graph. -/
+def Embed.sequenceRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ⤳ g₂) where
+  f i := i.natAdd g₁.size
+  nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
+  edges_mem he := List.mem_append_left _ (List.mem_append_right _ (List.mem_map_of_mem _ he))
+
+/-- The left operand's inclusion into an overlaid graph. -/
+def Embed.overlayLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ∙ g₂) where
+  f i := i.castAdd g₂.size
+  nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
+  edges_mem he := List.mem_append_left _ (List.mem_map_of_mem _ he)
+
+/-- The right operand's inclusion into an overlaid graph. -/
+def Embed.overlayRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ∙ g₂) where
+  f i := i.natAdd g₁.size
+  nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
+  edges_mem he := List.mem_append_right _ (List.mem_map_of_mem _ he)
+
+/-- The body's inclusion into a `loop` graph. -/
+def Embed.loop (g : GGraph (Option β)) : Embed g (loop g) where
+  f i := i.natAdd 2
+  nodes_eq i := Fin.append_right (fun _ : Fin 2 => none) g.nodes i
+  edges_mem he := List.mem_append_left _ (List.mem_append_left _
+    (List.mem_append_left _ (List.mem_map_of_mem _ he)))
+
 variable (g : GGraph α)
 
 /-- All the nodes in the graph. -/

lean/Spa/Language/Program.lean

@@ -50,6 +50,7 @@ lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
     At this time, for convenience of proofs, the CFGs have at most
     one basic statement, and multi-statement basic blocks are encoded
     as chains of blocks. Thus, this returns at most one `Spa.BasicStmt`. -/
+@[reducible]
 def code (st : p.State) : Option BasicStmt := p.cfg.nodes st
 
 /-- Get the predecessors of a particular CFG node / program state. -/

lean/Spa/Language/Properties.lean

@@ -27,62 +27,43 @@ 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}
     (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
-  induction tr with
-  | single hbs =>
-    exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
-      Fin.append_left])
-  | edge hbs he _ ih =>
-    refine Trace.edge ?_ ?_ ih
-    · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
-    · exact List.mem_append_left _ (List.mem_map_of_mem _ he)
+    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
 
 /-- When two graphs are overlaid, for each trace in the right graph,
     a corresponding trace exists in the combined graph. -/
 noncomputable def Trace.overlay_right {idx₁ idx₂ : g₂.Index}
     (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
-  induction tr with
-  | single hbs =>
-    exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
-      Fin.append_right])
-  | edge hbs he _ ih =>
-    refine Trace.edge ?_ ?_ ih
-    · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
-    · exact List.mem_append_right _ (List.mem_map_of_mem _ he)
+    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.overlayRight g₁ g₂)
 
 /-- When two graphs are sequenced, for each trace in the first graph,
     a corresponding trace exists in the combined graph. -/
 noncomputable def Trace.sequence_left {idx₁ idx₂ : g₁.Index}
     (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
-  induction tr with
-  | single hbs =>
-    exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
-      Fin.append_left])
-  | edge hbs he _ ih =>
-    refine Trace.edge ?_ ?_ ih
-    · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
-    · exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
+    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
 
 /-- When two graphs are sequenced, for each trace in the second graph,
    a corresponding trace exists in the combined graph. -/
 noncomputable def Trace.sequence_right {idx₁ idx₂ : g₂.Index}
     (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
-  induction tr with
-  | single hbs =>
-    exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
-      Fin.append_right])
-  | edge hbs he _ ih =>
-    refine Trace.edge ?_ ?_ ih
-    · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
-    · exact List.mem_append_left _
-        (List.mem_append_right _ (List.mem_map_of_mem _ he))
+    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.sequenceRight g₁ g₂)
 
 /-- Equivalent of `Trace.overlay_left` for end-to-end traces. -/
 noncomputable def EndToEndTrace.overlay_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
@@ -125,18 +106,8 @@ variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env}
 
 /-- A trace through a body CFG still exists (up to reindexing) in a zero-or-more loop CFG. -/
 noncomputable def Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by
-  induction tr with
-  | single hbs =>
-    exact Trace.single (by
-      rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => none) g.nodes from rfl,
-        Fin.append_right])
-  | edge hbs he _ ih =>
-    refine Trace.edge ?_ ?_ ih
-    · rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => none) g.nodes from rfl,
-        Fin.append_right]
-    · exact List.mem_append_left _ (List.mem_append_left _
-        (List.mem_append_left _ (List.mem_map_of_mem _ he)))
+    Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.loop g)
 
 /-- The beginning node of a loop graph is empty. -/
 private lemma loop_nodes_at_in :

lean/Spa/Language/Traces.lean

@@ -37,24 +37,230 @@ inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type
       EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
       Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
 
+/-!
+
+## Open Traces
+
+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.
+
+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. -/
+
+/-- 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₃ ρ₁ ρ₃
+
+def Traceₗ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceₗ g idx idx ρ ρ := .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 Traceᵣ.single (g : Graph) (idx : g.Index) (ρ : Env) : Traceᵣ g idx idx ρ ρ := .nil
+
 /-- 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. -/
-noncomputable def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
+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₄ ρ₁ ρ₃ := by
-  induction tr₁ with
-  | single hbs => exact Trace.edge hbs he tr₂
-  | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)
+    Trace g idx₁ idx₄ ρ₁ ρ₃ :=
+  match tr₁ with
+  | single hbs => edge hbs he tr₂
+  | edge hbs he' tr₁' => edge hbs he' (tr₁'.concat he tr₂)
 
 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)
+
+@[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)
+
+@[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
+
+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)
+
+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)
+
+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)
+
+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 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. -/
+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₂ ρ₁ ρ₂)
+    (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, *]
+
 /-- 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 ρ₁ ρ₂
 
+inductive Reaches {prog : Program} : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
+    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ →
+    (s : prog.State) → (ρin ρout : Env) → Type
+  | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
+      Reaches (.single hnode) s₁ ρ₁ ρ₂
+  | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
+      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) :
+      Reaches (.edge hnode hedge rest) s₁ ρ₁ ρ₂
+  | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
+      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃)
+      {s : prog.State} {ρin ρout : Env} :
+      Reaches rest s ρin ρout →
+      Reaches (.edge hnode hedge rest) s ρin ρout
+
+def Reaches.pre {prog : Program} {s₁ s₂ s: prog.State}
+    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
+    (r : Reaches tr s ρin ρout) → Traceₗ prog.cfg s₁ s ρ₁ ρin
+  | .single_here _ => .nil
+  | .edge_here _ _ _ => .nil
+  | .edge_there hnode hedge _ r => .cons hnode hedge r.pre
+
+def Reaches.post {prog : Program} {s₁ s₂ s: prog.State}
+    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
+    (r : Reaches tr s ρin ρout) → Trace prog.cfg s₁ s ρ₁ ρout
+  | .single_here hnode => .single hnode
+  | .edge_here hnode _ _ => .single hnode
+  | .edge_there hnode hedge _ r => .edge hnode hedge r.post
+
+def Reaches.first {prog : Program} {s₁ s₂ s: prog.State}
+    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
+    (r : Reaches tr s ρin ρout) → Σ ρ₁', Reaches tr s₁ ρ₁ ρ₁'
+  | .single_here hnode => ⟨_, .single_here hnode⟩
+  | .edge_here hnode hedge hrest => ⟨_, .edge_here hnode hedge hrest⟩
+  | .edge_there hnode hedge hrest tmp' => ⟨_, .edge_here hnode hedge hrest⟩
+
+def Reaches.step {prog : Program} {s₁ s₂ s: prog.State}
+    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
+    (r : Reaches tr s ρin ρout) → EvalBasicStmtOpt ρin (prog.code s) ρout
+  | .single_here hnode => hnode
+  | .edge_here hnode hedge hrest => hnode
+  | .edge_there hnode hedge hrest tmp' => tmp'.step
+
+
 end Spa