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/Forward.lean

@@ -131,6 +131,15 @@ def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
   | .edge hnode hedge rest =>
     let ⟨ρin, r'⟩ := reaches_final rest; ⟨ρin, .edge_there hnode hedge _ r'⟩
 
+omit [DecidableEq L] in
+/-- Reaching the final node covers the whole trace. -/
+@[simp] lemma reaches_final_post {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
+    (reaches_final tr).2.post = tr := by
+  induction tr with
+  | single hnode => rfl
+  | edge hnode hedge rest ih => simp [reaches_final, Reaches.post, ih]
+
 variable (L prog) in
 /-- Soundness at every program point reached during execution: for any node `s` visited
     by the run `hrun` (witnessed by `hr`), the analysis result over-approximates both the
@@ -148,11 +157,9 @@ theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
 variable (L prog) in
 theorem analyze_correct'
     {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (reaches_final (prog.trace hrun)).2.post) := by
+    ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (prog.trace hrun)) := by
-  let idk₀ := prog.trace hrun
+  have h := (analyze_correct_at L prog hrun (reaches_final (prog.trace hrun)).2).2
-  have ⟨_, idk₁⟩ := reaches_final idk₀
+  rwa [reaches_final_post] at h
-  have ⟨_, idk₂⟩ := analyze_correct_at L prog hrun idk₁
-  assumption
 
 end
 

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
+/-- The statements a trace executed, paired with the state each executed at,
-  | nil : Run prog
+    most recent first (matching `LastAssign`, which scans for the most recent
-  | cons (s : prog.State) (bs : BasicStmt)
+    assignment). This is `Trace.steps` (chronological) reversed, so facts about
-      (rest : Run prog) : Run prog
+    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
+  Proj := Run prog
-  init := Run.nil
+  Pre := @runOfTraceₗ prog
-  interp vs _ run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
+  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
+  post_pre := by
-  | .none, rest => rest
+    intro vs s₁ s₂ s₃ ρ₁ ρ₂ tr hedge hvs
-  | .some (bs := bs) _, rest => Run.cons s bs rest
+    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₁ s₂ ρ₁ ρ₂ ρ₃ vs tr hbs hvs
-    intro s ρ₁ ρ₂ vs; generalize prog.code s = obs; intro hst hbs hvs
+    show ⟦eval prog s₂ vs⟧ (runOfTrace prog (tr ++ hbs))
-    rcases hbs with _ | @⟨_, bs, hbs⟩; try (simpa [stepAt])
+    simpa [runOfTrace, runOfTraceₗ] using valid_step prog s₂ rfl hbs hvs
-    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
   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) ⟧ ρ
+    ⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧
-      (stepTraceState (prog.trace hrun) (stateInterp prog).init) :=
+      (runOfTrace prog (prog.trace hrun)) :=
-  Forward.analyze_correct_state (DefSet prog) prog 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}
+    {s : prog.State} {ρin ρout : Env}
-    (hr : Reaches (prog.trace hrun) (stateInterp prog).init s ρin ρout stin stout) :
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
-    ⟦ joinForKey s (result (DefSet prog) prog) ⟧ ρin stin
+    ⟦ joinForKey s (result (DefSet prog) prog) ⟧ (runOfTraceₗ prog hr.pre)
-      ∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ ρout stout :=
+      ∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ (runOfTrace prog hr.post) :=
   Forward.analyze_correct_at (DefSet prog) prog hrun hr
 
 end ReachingAnalysis

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/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
+    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
-  | 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)
 
 /-- 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
+    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.overlayRight g₁ g₂)
-  | 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)
 
 /-- 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
+    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
-  | 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))
 
 /-- 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
+    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.sequenceRight g₁ g₂)
-  | 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))
 
 /-- 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
+    Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.loop g)
-  | 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)))
 
 /-- The beginning node of a loop graph is empty. -/
 private lemma loop_nodes_at_in :

lean/Spa/Language/Traces.lean

@@ -136,6 +136,61 @@ instance instHAppendTraceTraceR {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ
     HAppend (Trace g idx₁ idx₂ ρ₁ ρ₂) (Traceᵣ g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where
   hAppend := Trace.appendRight
 
+/-!
+
+## Trace Steps
+
+Analyses that care about *which statements executed* (e.g. reaching
+definitions) need to project a trace down to its list of executed statements.
+Defining that projection here, once, as a chronological mathlib `List` means
+all the re-association facts about concatenating traces come for free from
+`List.append_assoc` and friends, instead of being re-proven per analysis. -/
+
+/-- The (index, statement) pairs executed by a single optional-statement step:
+    none if the node is empty, and the node's statement otherwise. -/
+def EvalBasicStmtOpt.steps {α : Type*} (idx : α) {ρ₁ ρ₂ : Env} {obs : Option BasicStmt} :
+    EvalBasicStmtOpt ρ₁ obs ρ₂ → List (α × BasicStmt)
+  | .none => []
+  | .some (bs := bs) _ => [(idx, bs)]
+
+/-- The statements executed by a left-open trace, in chronological order. -/
+def Traceₗ.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
+    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
+  | .nil => []
+  | .cons (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
+
+/-- The statements executed by a trace, in chronological order. -/
+def Trace.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
+    Trace g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
+  | .single (idx := idx) hnode => hnode.steps idx
+  | .edge (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
+
+@[simp] lemma Traceₗ.steps_append {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
+    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
+    (tr₂ : Traceₗ g idx₂ idx₃ ρ₂ ρ₃) :
+    (tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
+  show (tr₁.append tr₂).steps = _
+  induction tr₁ <;> simp [Traceₗ.append, Traceₗ.steps, *]
+
+@[simp] lemma Traceₗ.steps_appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
+    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
+    (tr₂ : Trace g idx₂ idx₃ ρ₂ ρ₃) :
+    (tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
+  show (tr₁.appendTrace tr₂).steps = _
+  induction tr₁ <;> simp [Traceₗ.appendTrace, Traceₗ.steps, Trace.steps, *]
+
+@[simp] lemma Traceₗ.steps_appendStep {g : Graph} {idx₁ idx₂ : g.Index}
+    {ρ₁ ρ₂ ρ₃ : Env} (tr : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
+    (hbs : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) :
+    (tr ++ hbs).steps = tr.steps ++ hbs.steps idx₂ :=
+  Traceₗ.steps_appendTrace tr (Trace.single hbs)
+
+@[simp] lemma Trace.steps_addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
+    {ρ₁ ρ₂ : Env} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂)
+    (hedge : (idx₂, idx₃) ∈ g.edges) :
+    (tr.addEdge hedge).steps = tr.steps := by
+  induction tr <;> simp [Trace.addEdge, Trace.steps, Traceₗ.steps, *]
+
 @[simp] lemma Traceₗ.append_addEdge {g : Graph}
     {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env}
     (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)