Add function back in to Embedding

Remove trace suffix from Reaching type
Clean up comments in Graphs.lean and Program.lean
2026-08-09 21:43:20 -05:00 · 2026-08-09 21:23:21 -05:00 · 2026-08-09 18:17:02 -05:00 · 2026-08-09 17:51:58 -05:00 · 2026-08-09 17:38:56 -05:00 · 2026-08-09 17:35:30 -05:00
25 changed files with 969 additions and 1243 deletions
--- a/lean/Main.lean
+++ b/lean/Main.lean
@@ -1,5 +1,6 @@
 import Spa.Analysis.Sign
 import Spa.Analysis.Constant
+import Spa.Analysis.Reaching
 import Spa.Language.Notation

 namespace Spa
@@ -26,10 +27,11 @@ def testCodeCond₂ : Stmt := [obj_stmt|
  if var { x := 1 } else { noop }
 ]

-def testProgram : Program := ⟨testCode⟩
+def testProgram : Program := { rootStmt := testCode }

 end Spa

 def main : IO Unit :=
  IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
-              Spa.SignAnalysis.output Spa.testProgram)
+              Spa.SignAnalysis.output Spa.testProgram ++ "\n" ++
+              Spa.ReachingAnalysis.output Spa.testProgram)
--- a/lean/Spa.lean
+++ b/lean/Spa.lean
@@ -19,10 +19,5 @@ import Spa.Showable
 import Spa.Analysis.Utils
 import Spa.Analysis.Sign
 import Spa.Analysis.Constant
-import Spa.Language.Tagged.Id
-import Spa.Language.Tagged.Derive
-import Spa.Language.Tagged.Basic
-import Spa.Language.Tagged.Properties
-import Spa.Language.Tagged.Graphs
 import Spa.Analysis.Reaching
 import Spa.Transformation.Licm
--- a/lean/Spa/Analysis/Constant.lean
+++ b/lean/Spa/Analysis/Constant.lean
@@ -134,9 +134,15 @@ 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 {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches s ρin ρout) :
+    ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin
+      ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout :=
+  Forward.analyze_correct_at ConstLattice prog hr
+
 end ConstAnalysis

 end Spa
--- a/lean/Spa/Analysis/Forward.lean
+++ b/lean/Spa/Analysis/Forward.lean
@@ -9,22 +9,12 @@ namespace Forward

 variable {L : Type} [FiniteHeightLattice L] {prog : Program} [E : StmtEvaluator L prog]

-def evalStmtOrNone (s : prog.State) (o : Option BasicStmt) (hco : prog.code s = o)
-    (vs : VariableValues L prog) : VariableValues L prog :=
-  o.elimEq vs (fun bs h => E.eval s bs (hco.trans h))
-
-lemma evalStmtOrNone_mono (s : prog.State) (o : Option BasicStmt)
-    (hco : prog.code s = o) : Monotone (evalStmtOrNone (L := L) s o hco) :=
-  elimEq_self_mono o (fun bs h vs => E.eval s bs (hco.trans h) vs)
-    (fun bs h => E.eval_mono s bs (hco.trans h))
-
 def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
-    VariableValues L prog :=
-  evalStmtOrNone s (prog.code s) rfl (variablesAt s sv)
+    VariableValues L prog := E.eval s (variablesAt s sv)

 lemma updateVariablesForState_mono (s : prog.State) :
    Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
-  evalStmtOrNone_mono s (prog.code s) rfl (variablesAt_le hle s)
+  E.eval_mono s (variablesAt_le hle s)

 def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
  FiniteMap.generalizedUpdate id updateVariablesForState
@@ -64,98 +54,99 @@ lemma joinForKey_initialState :
  rfl

 class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
-    [E : StmtEvaluator L prog] [S : StateInterp L prog] where
-  step : (s : prog.State) → {ρ₁ ρ₂ : Env} → {bs : BasicStmt} →
-    prog.code s = some bs → EvalBasicStmt ρ₁ bs ρ₂ → S.St ρ₁ → S.St ρ₂
-  valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} {bs : BasicStmt}
-    {vs : VariableValues L prog} {st : S.St ρ₁},
-    (hcode : prog.code s = some bs) → (hbs : EvalBasicStmt ρ₁ bs ρ₂) → ⟦ vs ⟧ ρ₁ st →
-    ⟦ E.eval s bs hcode vs ⟧ ρ₂ (step s hcode hbs st)
-  botV_init : ⟦ botV L prog ⟧ [] S.init
+    [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
+  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 _ _ _ _ _ _ hcode hbs hvs; exact ValidStmtEvaluator.valid hcode 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 : StateInterp L prog] [V : ValidStateEvaluator L prog]
-
-noncomputable def stepStmtOrNone (s : prog.State) {ρ₁ ρ₂ : Env} :
-    (o : Option BasicStmt) → prog.code s = o → EvalBasicStmtOpt ρ₁ o ρ₂ →
-    S.St ρ₁ → S.St ρ₂
-  | none, _, .none, st => st
-  | some _, hco, .some hbs, st => V.step s hco hbs st
-
-noncomputable def stepNode (s : prog.State) {ρ₁ ρ₂ : Env}
-    (h : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) (st : S.St ρ₁) : S.St ρ₂ :=
-  stepStmtOrNone s (prog.code s) rfl 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)
+variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]

 omit [DecidableEq L] in
-lemma evalStmtOrNone_valid {s : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
-    {vs : VariableValues L prog} (o : Option BasicStmt) (hco : prog.code s = o)
-    (he : EvalBasicStmtOpt ρ₁ o ρ₂) (hvs : ⟦ vs ⟧ ρ₁ st) :
-    ⟦ evalStmtOrNone s o hco vs ⟧ ρ₂ (stepStmtOrNone s o hco he st) := by
-  cases he with
-  | none => exact hvs
-  | some hbs => exact V.valid s hco hbs hvs
-
-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 evalStmtOrNone_valid (prog.code s) rfl 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

-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
-  induction tr with
-  | single hnode => exact stepTrace hjoin hnode
-  | @edge _ ρ' _ i₁ i₂ _ hnode hedge _ ih =>
-    have hstep : ⟦ variablesAt i₁ (result L prog) ⟧ ρ' (stepNode i₁ hnode st₁) :=
-      stepTrace hjoin hnode
-    have hmem : variablesAt i₁ (result L prog)
-        ∈ (result L prog).valuesAt (prog.incoming i₂) :=
-      FiniteMap.mem_valuesAt prog.states_nodup
-        (prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog))
-    exact ih (interp_foldr hstep hmem)
+/-- Soundness propagates along an execution prefix: if the analysis is sound at
+    `s₂` for the run so far (`trₗ`), then it is sound wherever the further prefix
+    `mid` ends up. -/
+lemma walkPrefix : ∀ {s₂ s : prog.State} {ρ₂ ρin : Env}
+    (mid : Traceₗ prog.cfg s₂ s ρ₂ ρin) {s₁ : prog.State} {ρ₁ : Env}
+    (trₗ : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂),
+    ⟦ 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 =>
+      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)
+          (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 `walkPrefix`. -/
+def reaches_final {s : prog.State} {ρ : Env}
+    (tr : Trace prog.cfg prog.initialState s [] ρ) : Σ ρin, Reaches s ρin ρ :=
+  ⟨_, ⟨tr.split.2.1, tr.split.2.2⟩⟩
+
+omit [DecidableEq L] in
+@[simp] lemma reaches_final_post {s : prog.State} {ρ : Env}
+    (tr : Trace prog.cfg prog.initialState s [] ρ) :
+    (reaches_final tr).2.post = tr := Trace.split_append tr

 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
+/-- Soundness at every program point an execution actually visits: the analysis
+    over-approximates both the environment entering that point and the one leaving
+    it. -/
+theorem analyze_correct_at {s : prog.State} {ρin ρout : Env} (hr : Reaches s ρin ρout) :
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre hr.pre)
+      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post hr.post) :=
+  have hpre := walkPrefix hr.pre Traceₗ.nil
+    (by rw [joinForKey_initialState]; exact ValidStateEvaluator.botV_init)
+  ⟨hpre, stepTrace hr.pre hpre hr.step⟩
+
+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 (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

--- a/lean/Spa/Analysis/Forward/Adapters.lean
+++ b/lean/Spa/Analysis/Forward/Adapters.lean
@@ -14,44 +14,50 @@ lemma updateVariablesFromExpression_mono (k : String) (e : Expr) :
    Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) :=
  FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)

-def evalBasicStmt (s : prog.State) (bs : BasicStmt) (_h : prog.code s = some bs)
+def evalBasicStmt (bs : BasicStmt)
    (vs : VariableValues L prog) : VariableValues L prog :=
  match bs with
  | .assign k e => updateVariablesFromExpression k e vs
  | .noop => vs

-lemma evalBasicStmt_mono (s : prog.State) (bs : BasicStmt) (h : prog.code s = some bs) :
-    Monotone (evalBasicStmt (L := L) (prog := prog) s bs h) := by
+lemma evalBasicStmt_mono (bs : BasicStmt) :
+    Monotone (evalBasicStmt (L := L) (prog := prog) bs) := by
  cases bs with
  | assign k e => exact updateVariablesFromExpression_mono k e
  | noop => exact monotone_id

+def evalBasicStmtOpt (obs : Option BasicStmt)
+    (vs : VariableValues L prog) : VariableValues L prog :=
+  match obs with
+  | none => vs
+  | some bs => evalBasicStmt bs vs
+
+lemma evalBasicStmtOpt_mono (obs : Option BasicStmt) :
+    Monotone (evalBasicStmtOpt (L := L) (prog := prog) obs) := by
+  cases obs <;> unfold evalBasicStmtOpt
+  · exact monotone_id
+  · apply evalBasicStmt_mono
+
 instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
-  ⟨evalBasicStmt, evalBasicStmt_mono⟩
+  ⟨evalBasicStmtOpt ∘ prog.code,
+   by intro s; simp; exact (evalBasicStmtOpt_mono (prog.code s))⟩

 instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
    [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by
  constructor
-  intro s vs ρ₁ ρ₂ bs hcode hbs hvs
-  cases hbs with
-  | noop => exact hvs
-  | assign k e v hev =>
-    intro k' l hk'l v' hv'
-    cases hv' with
-    | here =>
-      have hk'l₀ : (k, l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
-          (fun _ vs => E.eval e vs) [k] vs := hk'l
-      have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
-        (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hk'l₀
-      rw [hl]
-      exact ValidExprEvaluator.valid hev hvs
-    | there _ _ _ _ _ hne hmem' =>
-      have hk'l₀ : (k', l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
-          (fun _ vs => E.eval e vs) [k] vs := hk'l
-      have hk'l' : (k', l) ∈ (id vs : VariableValues L prog) :=
-        FiniteMap.generalizedUpdate_not_mem_backward
-          (fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀
-      exact hvs _ _ hk'l' _ hmem'
+  simp [StmtEvaluator.eval, evalBasicStmtOpt]
+  intro s vs ρ₁ ρ₂; generalize prog.code s = obs; intro hev hvs
+  rcases hev with _ | @⟨_,bs,hev⟩ <;> try simpa
+  rcases hev with _ | @⟨k, e, v, hev⟩ <;> try simpa
+  intros k' l' hkl' v' hρ
+  rcases hρ with _ | ⟨_,_,_,_,_,hne,hmem⟩ <;> simp [evalBasicStmt] at hkl'
+  · have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
+        (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hkl'
+    rewrite [hl]; simp
+    exact ValidExprEvaluator.valid hev hvs
+  · have hl := FiniteMap.generalizedUpdate_not_mem_backward
+        (fun hmem => hne (List.mem_singleton.mp hmem)) hkl'
+    apply hvs _ _ hl _ hmem

 end Forward

--- a/lean/Spa/Analysis/Forward/Evaluation.lean
+++ b/lean/Spa/Analysis/Forward/Evaluation.lean
@@ -7,9 +7,8 @@ namespace Forward
 variable (L : Type) [Lattice L] (prog : Program)

 class StmtEvaluator where
-  eval : (s : prog.State) → (bs : BasicStmt) → prog.code s = some bs →
-    VariableValues L prog → VariableValues L prog
-  eval_mono : ∀ s bs h, Monotone (eval s bs h)
+  eval : prog.State → VariableValues L prog → VariableValues L prog
+  eval_mono : ∀ s, Monotone (eval s)

 class ExprEvaluator where
  eval : Expr → VariableValues L prog → L
@@ -18,13 +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}
-    {bs : BasicStmt} (hcode : prog.code s = some bs),
-    EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s bs hcode vs ⟧ ρ₂ ()
+  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env},
+    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s vs ⟧ ρ₂

 end Forward

--- a/lean/Spa/Analysis/Forward/Lattices.lean
+++ b/lean/Spa/Analysis/Forward/Lattices.lean
@@ -64,23 +64,29 @@ lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
    variablesAt s (joinAll sv) = joinForKey s sv :=
  joinAll_mem_eq (variablesAt_mem s (joinAll sv))

-class StateInterp (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
+class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
+  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

-instance [S : StateInterp L prog] :
-    Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → Prop) :=
+  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) (S.Proj → Prop) :=
  ⟨S.interp⟩

-lemma interp_foldr [S : StateInterp L prog]
+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 =>
@@ -90,21 +96,25 @@ lemma interp_foldr [S : StateInterp L prog]

 variable [I : LatticeInterpretation L]

-instance : StateInterp L prog where
-  St := fun _ => PUnit
-  init := PUnit.unit
-  interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs →
+instance : StateInterpretation L prog where
+  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

--- a/lean/Spa/Analysis/Reaching.lean
+++ b/lean/Spa/Analysis/Reaching.lean
@@ -1,44 +1,38 @@
 import Spa.Analysis.Forward
-import Spa.Lattice.Bool
-import Spa.Lattice.Tuple
-import Spa.Language.Tagged.Graphs
+import Spa.Lattice.Finset
 import Spa.Showable

 namespace Spa

 open Forward

-instance : Showable Bool := ⟨fun b => if b then "true" else "false"⟩
-
-instance {n : ℕ} {β : Type*} [Showable β] : Showable (Fin n → β) :=
-  ⟨fun f =>
+instance {n : ℕ} : Showable (Finset (Fin n)) :=
+  ⟨fun s =>
    "{" ++ (List.finRange n).foldr
-        (fun i rest => show' i ++ " ↦ " ++ show' (f i) ++ ", " ++ rest) ""
+        (fun i rest => if i ∈ s then show' i ++ ", " ++ rest else rest) ""
        ++ "}"⟩

-abbrev DefSet (prog : Program) : Type := prog.NodeId → Bool
+abbrev DefSet (prog : Program) : Type := Finset prog.State

 namespace ReachingAnalysis

 variable (prog : Program)

-def genSet (s : prog.State) {bs : BasicStmt} (h : prog.code s = some bs) :
-    DefSet prog :=
-  Function.update (⊥ : DefSet prog) (prog.nodeIdOfNonempty s h) true
+def eval (s : prog.State) (vs : VariableValues (DefSet prog) prog) : VariableValues (DefSet prog) prog :=
+  match prog.code s with
+  | none => vs
+  | some bs =>
+    match bs with
+    | .assign k _ => FiniteMap.generalizedUpdate id (fun _ _ => {s}) [k] vs
+    | .noop => vs

-def eval (s : prog.State) :
-    (bs : BasicStmt) → prog.code s = some bs →
-    VariableValues (DefSet prog) prog → VariableValues (DefSet prog) prog
-  | .assign k _, h, vs =>
-    FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s h) [k] vs
-  | .noop, _, vs => vs
-
-lemma eval_mono (s : prog.State) (bs : BasicStmt) (h : prog.code s = some bs) :
-    Monotone (eval prog s bs h) := by
-  cases bs with
-  | assign k e =>
-    exact FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
-  | noop => exact monotone_id
+lemma eval_mono (s : prog.State) :
+    Monotone (eval prog s) := by
+  intros vs₁ vs₂ hle
+  unfold eval; split <;> try simpa
+  split <;> try simpa
+  apply FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
+  assumption

 instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
  ⟨eval prog, eval_mono prog⟩
@@ -46,58 +40,89 @@ 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) (hc : prog.code s = some bs)
-      (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) hc rest) (prog.nodeIdOfNonempty s hc)
+inductive LastAssign (prog : Program) (x : String) : Run prog → prog.State → Prop
+  | here (s : prog.State) (e : Expr) (rest : Run prog) :
+      LastAssign prog x ((s, .assign x e) :: rest) s
  | there (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
-      (rest : Run prog) {n : prog.NodeId} :
+      (rest : Run prog) {n : prog.State} :
      (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
-      LastAssign prog x (Run.cons s bs hc rest) n
+      LastAssign prog x ((s, bs) :: rest) n

-instance stateInterp : StateInterp (DefSet prog) prog where
-  St := fun _ => Run prog
-  init := Run.nil
-  interp vs _ run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
-    ∀ (n : prog.NodeId), LastAssign prog x run n → assigners n = true
+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
+  Proj := Run prog
+  Pre := @runOfTraceₗ prog
+  Post := @runOfTrace prog
+
+  interp vs run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
+    ∀ (n : prog.State), 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
+    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
+    aesop (add simp Finset.mem_inter)
+
+  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 [hd] <;> 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 := by intro s _ _ bs hcode _ rest; exact Run.cons s bs hcode rest
  valid := by
-    intro s ρ₁ ρ₂ bs vs st hcode hbs hvs
-    cases hbs with
-    | noop => intro x assigners hmem n hla; aesop
-    | assign x e v hev =>
-      intro k assigners hmem n hla
-      have hmem2 : (k, assigners) ∈
-          FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s hcode) [x] vs := hmem
-      by_cases hx : k = x
-      · subst hx
-        have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem2
-        aesop (add simp genSet)
-      · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
-          (fun hc => hx (List.mem_singleton.mp hc)) hmem2
-        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 {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches 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 hr

 end ReachingAnalysis

--- a/lean/Spa/Analysis/Sign.lean
+++ b/lean/Spa/Analysis/Sign.lean
@@ -111,13 +111,16 @@ namespace SignAnalysis

 variable (prog : Program)

+/-- The sign of an integer literal. -/
+def signOf (z : ℤ) : SignLattice :=
+  if z = 0 then .mk .zero else if 0 < z then .mk .plus else .mk .minus
+
 def eval : Expr → VariableValues SignLattice prog → SignLattice
  | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs)
  | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs)
  | .var k, vs =>
    if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
-  | .num 0, _ => .mk .zero
-  | .num (_ + 1), _ => .mk .plus
+  | .num z, _ => signOf z

 lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
  induction e with
@@ -139,7 +142,7 @@ lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
          dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
  | num n =>
    intro vs₁ vs₂ _
-    cases n <;> exact le_refl _
+    exact le_refl _

 instance exprEvaluator : ExprEvaluator SignLattice prog :=
  ⟨eval prog, eval_mono prog⟩
@@ -159,6 +162,20 @@ private lemma int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z
  · rintro ⟨n, rfl⟩; omega
  · intro h; exact ⟨(-z - 1).toNat, by omega⟩

+/-- `signOf` really does describe the literal it was computed from. -/
+lemma interp_signOf (z : ℤ) : ⟦signOf z⟧ (Value.int z) := by
+  unfold signOf
+  split
+  · case isTrue h => subst h; rfl
+  · rename_i hne
+    split
+    · case isTrue hpos =>
+        simp only [signInterpretation, interpSign, Value.int.injEq, int_pos_iff]
+        exact hpos
+    · case isFalse hnpos =>
+        simp only [signInterpretation, interpSign, Value.int.injEq, int_neg_iff]
+        omega
+
 lemma plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
    ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
@@ -184,9 +201,7 @@ instance eval_valid : ValidExprEvaluator SignLattice prog := by
  | num n =>
    intro _
    show ⟦eval prog (.num n) vs⟧ (.int n)
-    cases n with
-    | zero => rfl
-    | succ n' => exact ⟨n', congrArg Value.int (by norm_cast)⟩
+    exact interp_signOf n
  | var x v hxv =>
    intro hvs
    show ⟦eval prog (.var x) vs⟧ v
@@ -210,9 +225,15 @@ 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 {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches s ρin ρout) :
+    ⟦ joinForKey s (result SignLattice prog) ⟧ ρin
+      ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout :=
+  Forward.analyze_correct_at SignLattice prog hr
+
 end SignAnalysis

 end Spa
--- a/lean/Spa/Language.lean
+++ b/lean/Spa/Language.lean
@@ -3,56 +3,4 @@ import Spa.Language.Semantics
 import Spa.Language.Graphs
 import Spa.Language.Traces
 import Spa.Language.Properties
-import Mathlib.Data.Finset.Sort
-import Mathlib.Data.String.Basic
-
-namespace Spa
-
-structure Program where
-  rootStmt : Stmt
-
-namespace Program
-
-variable (p : Program)
-
-def cfg : Graph := Graph.wrap p.rootStmt.cfg
-
-abbrev State : Type := p.cfg.Index
-
-def initialState : p.State := p.rootStmt.cfg.wrapInput
-
-def finalState : p.State := p.rootStmt.cfg.wrapOutput
-
-noncomputable def trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
-    Trace p.cfg p.initialState p.finalState [] ρ := by
-  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h)
-  rw [Graph.wrap_inputs, List.mem_singleton] at h₁
-  rw [Graph.wrap_outputs, List.mem_singleton] at h₂
-  subst h₁; subst h₂
-  exact tr
-
-def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
-
-lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
-
-def states : List p.State := p.cfg.indices
-
-lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
-
-lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
-
-def code (st : p.State) : Option BasicStmt := p.cfg.nodes st
-
-def incoming (s : p.State) : List p.State := p.cfg.predecessors s
-
-lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
-  Graph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
-    (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
-
-lemma mem_incoming_of_edge {s₁ s₂ : p.State}
-    (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ :=
-  p.cfg.mem_predecessors_of_edge h
-
-end Program
-
-end Spa
+import Spa.Language.Program
--- a/lean/Spa/Language/Base.lean
+++ b/lean/Spa/Language/Base.lean
@@ -5,9 +5,13 @@ import Mathlib.Data.Finset.Basic
 # Base Language

 This file defines the core object language for the program analysis and
-transformation. It's a very basic imperative language. The `Spa/Language/Tagged/Basic.lean`
-file provides an auto-derived version of the `Expr`, `BasicStmt`, and `Stmt` data
-types with unique IDs per condtructor, enabling in-AST pointers.
+transformation. It's a very basic imperative language.
+
+Program points are identified by their node in the control flow graph rather than
+by an identifier stored in the AST: a recursion over a `Stmt` threads a
+`Spa.GGraph.Embed` of the subtree's CFG into the whole program's (starting from
+`Spa.Program.rootEmbed`), which yields the CFG index of each basic statement
+along with a proof that the node carries it.

 -/

@@ -18,7 +22,7 @@ inductive Expr where
  | add (e₁ e₂ : Expr)
  | sub (e₁ e₂ : Expr)
  | var (x : String)
-  | num (n : ℕ)
+  | num (z : ℤ)
  deriving DecidableEq

 /-- A statement that cannot alter control flow (and thus, can be part of a basic block).
--- a/lean/Spa/Language/Graphs.lean
+++ b/lean/Spa/Language/Graphs.lean
@@ -25,6 +25,15 @@ indexing into a list.

 -/

+/-- Logically, when combining `Fin`s from two distinct pools,
+    the combination is disjoint. -/
+lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
+    Fin.castAdd m i ≠ Fin.natAdd n j := by
+  intro h
+  have := congrArg Fin.val h
+  simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
+  omega
+
 /-- Bump the upper bound of a list of `Fin`s without changing their value. -/
 def List.finCastAdd {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) :=
  l.map (Fin.castAdd m)
@@ -157,6 +166,22 @@ def singleton (a : α) : GGraph α where
 def wrap (g : GGraph (Option β)) : GGraph (Option β) :=
  singleton none ⤳ g ⤳ singleton none

+/-- The input / entry node generated by `GGraph.wrap`. -/
+def wrapInput (g : GGraph (Option β)) : (wrap g).Index :=
+  (0 : Fin 1).castAdd ((g ⤳ singleton none).size)
+
+/-- The output / exit node generated by `GGraph.wrap`. -/
+def wrapOutput (g : GGraph (Option β)) : (wrap g).Index :=
+  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
+
+/-- The `wrapInput` is, indeed, the graph's only input after `wrap`. -/
+lemma wrap_inputs (g : GGraph (Option β)) :
+    (wrap g).inputs = [g.wrapInput] := rfl
+
+/-- The `wrapInput` is, indeed, the graph's only output after `wrap`. -/
+lemma wrap_outputs (g : GGraph (Option β)) :
+    (wrap g).outputs = [g.wrapOutput] := rfl
+
@[simp] lemma map_singleton (f : α → β) (a : α) :
    f <$> singleton a = singleton (f a) := rfl

@@ -188,6 +213,106 @@ def wrap (g : GGraph (Option β)) : GGraph (Option β) :=
    (Option.map h) <$> wrap g = wrap (Option.map h <$> g) := by
  simp [GGraph.wrap, GGraph.map_sequence, GGraph.map_singleton]

+/-! ### Embeddings
+
+To be able to reason compositionally about traces through the graphs,
+we need to be able to reason about how a trace within a sub-graph maps
+to the full graph. Fortunately, graphs are built using composition operators,
+and these composition operators always include their arguments as embedded
+subgraphs in the full result. Moreover, each embedding "just" offsets the
+existing node IDs by a given amount.
+
+This section formalizes this fact by providing an `Embed` type that
+represents an offset-based embedding, and showing that such an embedding
+exists for all arguments given to graph composition operators. Furthermore,
+because of the offset-based embedding, we can determine whether a node
+came from a particular subgraph simply by examining its offset and sub-graph
+size. This is captured by `Embed.mem_range_iff`. -/
+
+/-- A special-case embedding of `g` into `h` in which all edges and nodes
+    of `g` are present in `h` at a given offset `off`. -/
+structure Embed (g h : GGraph α) where
+  f : g.Index → h.Index
+  off : ℕ
+  f_val : ∀ i, (f i).val = off + i.val
+  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
+
+lemma Embed.f_inj {g h : GGraph α} (e : Embed g h) : Function.Injective e.f := by
+  intro i j hij
+  have := congrArg Fin.val hij
+  rw [e.f_val, e.f_val] at this
+  exact Fin.ext (by omega)
+
+/-- An embedding's range is the interval `[off, off + g.size)`. -/
+lemma Embed.mem_range_iff {g h : GGraph α} (e : Embed g h) (j : h.Index) :
+    (∃ i, e.f i = j) ↔ e.off ≤ j.val ∧ j.val < e.off + g.size := by
+  constructor
+  · rintro ⟨i, rfl⟩; have := i.isLt; rw [e.f_val]; omega
+  · rintro ⟨hlo, hhi⟩
+    refine ⟨⟨j.val - e.off, by omega⟩, Fin.ext ?_⟩
+    rw [e.f_val]
+    show e.off + (j.val - e.off) = j.val
+    omega
+
+/-- Build an embedding from an index map that is pointwise the shift.  The five
+    inclusions below are naturally written with `Fin.castAdd`/`Fin.natAdd` — the form
+    the `Fin.append` lemmas are stated in — so this lets them keep those proofs
+    verbatim.  The trailing argument is boilerplate at every call site and defaults
+    to discharging itself. -/
+private def Embed.ofIndexMap {g h : GGraph α} (off : ℕ) (k : g.Index → h.Index)
+    (hn : ∀ i, h.nodes (k i) = g.nodes i)
+    (hem : ∀ {e : g.Edge}, e ∈ g.edges → (k e.1, k e.2) ∈ h.edges)
+    (hk : ∀ i, (k i).val = off + i.val := by intro i; simp) :
+    Embed g h where
+  f := k
+  off := off
+  f_val := hk
+  nodes_eq := hn
+  edges_mem := hem
+
+/-- Embeddings compose (offsets add). -/
+def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Embed g₂ g₃) :
+    Embed g₁ g₃ :=
+  ofIndexMap (e₂.off + e₁.off) (fun i => e₂.f (e₁.f i))
+    (fun i => (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i))
+    (fun he => e₂.edges_mem (e₁.edges_mem he))
+    (hk := fun i => by rw [e₂.f_val, e₁.f_val]; omega)
+
+/-- The left operand's inclusion into a sequenced graph. -/
+def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) :=
+  ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes)
+    (fun 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₂) :=
+  ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes)
+    (fun 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₂) :=
+  ofIndexMap 0 (fun i => i.castAdd g₂.size) (Fin.append_left g₁.nodes g₂.nodes)
+    (fun 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₂) :=
+  ofIndexMap g₁.size (fun i => i.natAdd g₁.size) (Fin.append_right g₁.nodes g₂.nodes)
+    (fun 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 (GGraph.loop g) :=
+  ofIndexMap 2 (fun i => i.natAdd 2) (Fin.append_right (fun _ : Fin 2 => none) g.nodes)
+    (fun he => List.mem_append_left _ (List.mem_append_left _
+      (List.mem_append_left _ (List.mem_map_of_mem _ he))))
+
+/-- A `singleton` subgraph has exactly one node; this is where it sits in the ambient graph. -/
+def Embed.singletonIndex {a : α} {h : GGraph α} (e : Embed (singleton a) h) : h.Index :=
+  e.f ⟨0, Nat.zero_lt_one⟩
+
+@[simp] lemma Embed.nodes_singletonIndex {a : α} {h : GGraph α}
+    (e : Embed (singleton a) h) : h.nodes e.singletonIndex = a :=
+  e.nodes_eq ⟨0, Nat.zero_lt_one⟩
+
 variable (g : GGraph α)

 /-- All the nodes in the graph. -/
@@ -205,6 +330,35 @@ lemma nodup_indices : g.indices.Nodup :=
 def predecessors (idx : g.Index) : List g.Index :=
  g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)

+/-- When sequencing (proven here with `Graph.singleton` on the left), no edges
+    exist from the right-hand graph back to the left. -/
+private lemma not_mem_edges_castAdd_sequence {g₂ : GGraph (Option β)} (i : Fin 1)
+    (idx : (singleton none ⤳ g₂).Index) :
+    ((idx, i.castAdd g₂.size) : (singleton none ⤳ g₂).Edge)
+      ∉ (singleton none ⤳ g₂).edges := by
+  intro h
+  rcases List.mem_append.mp h with h' | h'
+  · rcases List.mem_append.mp h' with h'' | h''
+    · -- lifted edges of `singleton []`: there are none
+      simp [singleton, List.finCastAddProd] at h''
+    · -- lifted edges of g₂: targets are natAdd
+      obtain ⟨e, _, heq⟩ := List.mem_map.mp h''
+      exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm
+  · -- product edges: targets are natAdd'd inputs of g₂
+    obtain ⟨-, hb⟩ := List.mem_product.mp h'
+    obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
+    exact Fin.castAdd_ne_natAdd i j heq.symm
+
+/-- The input node of a graph after `Graph.wrap` has no predecessors. -/
+lemma wrap_predecessors_eq_nil (g : GGraph (Option β)) (idx : (wrap g).Index)
+    (h : idx ∈ (wrap g).inputs) :
+    (wrap g).predecessors idx = [] := by
+  rw [wrap_inputs, List.mem_singleton] at h
+  subst h
+  rw [GGraph.predecessors, List.filter_eq_nil_iff]
+  intro idx' _
+  simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ singleton none) 0 idx'
+
 /-- There's there's an edge between two nodes `idx₁` and `idx₂`,
    then `idx₁` is the predecessor of `idx₂`. -/
 lemma mem_predecessors_of_edge {idx₁ idx₂ : g.Index}
@@ -225,7 +379,7 @@ abbrev Graph : Type := GGraph (Option BasicStmt)

 namespace Graph

-export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs)
+export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs wrapInput wrapOutput wrap_inputs wrap_outputs)

@[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay
@[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence
--- a/lean/Spa/Language/Program.lean
+++ b/lean/Spa/Language/Program.lean
@@ -0,0 +1,82 @@
+import Spa.Language.Base
+import Spa.Language.Semantics
+import Spa.Language.Graphs
+import Mathlib.Data.Finset.Sort
+import Mathlib.Data.String.Basic
+
+namespace Spa
+
+/-- A self-contained program to be evaluated, analyzed, and transformed. -/
+structure Program where
+  /-- The statement at the top level of the program. Since `Spa.Stmt` contains
+      sequencing via `Spa.Stmt.andThen`, this can encode any number of
+      statements. -/
+  rootStmt : Stmt
+  /-- A memoized copy of the control-flow graph. This field is an
+      implementation detail to avoid re-computing `Spa.GGraph.wrap` and `Spa.Stmt.cfg`
+      every time the program's control flow graph is needed -/
+  cfgCache : Thunk Graph := Thunk.mk fun _ => Graph.wrap rootStmt.cfg
+
+namespace Program
+
+variable (p : Program)
+
+-- Runtime implementation of `cfg`: read the memoized graph.
+private def cfgImpl : Graph := p.cfgCache.get
+
+/-- The control flow graph corresponding to this graph. -/
+@[implemented_by cfgImpl]
+def cfg : Graph := Graph.wrap p.rootStmt.cfg
+
+/-- A state in the control flow `Spa.Graph` of this program. -/
+abbrev State : Type := p.cfg.Index
+
+/-- The root statement's CFG sits inside the program's CFG. -/
+def rootEmbed : GGraph.Embed p.rootStmt.cfg p.cfg :=
+  (GGraph.Embed.sequenceLeft p.rootStmt.cfg (Graph.singleton none)).trans
+    (GGraph.Embed.sequenceRight (Graph.singleton none) _)
+
+/-- Variables mentioned or defined in this program. -/
+def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
+
+/-- `vars` has no duplicates. -/
+lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
+
+/-- All the states in the program's control flow `Spa.Graph`. -/
+def states : List p.State := p.cfg.indices
+
+/-- All states in the CFG are contained in `states`. -/
+lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
+
+/-- `states` has no duplicates. -/
+lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
+
+/-- Given a node of the program's CFG, return the code at that node.
+    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. -/
+def incoming (s : p.State) : List p.State := p.cfg.predecessors s
+
+/-- The entry point of the program's CFG. -/
+def initialState : p.State := Graph.wrapInput p.rootStmt.cfg
+
+/-- The exit point of the program's CFG. -/
+def finalState : p.State := Graph.wrapOutput p.rootStmt.cfg
+
+/-- `incoming` is a faithful representation of edges in the CFG. -/
+lemma mem_incoming_of_edge {s₁ s₂ : p.State}
+    (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ :=
+  p.cfg.mem_predecessors_of_edge h
+
+/-- The `initialState` has no incoming edges (it's the program start). -/
+lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
+  GGraph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
+    (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
+
+end Program
+
+end Spa
--- a/lean/Spa/Language/Properties.lean
+++ b/lean/Spa/Language/Properties.lean
@@ -23,73 +23,47 @@ namespace Spa

 open Graph

-lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
-    Fin.castAdd m i ≠ Fin.natAdd n j := by
-  intro h
-  have := congrArg Fin.val h
-  simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
-  omega
-
 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₁ ρ₁ ρ₂) :
@@ -132,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 :
@@ -246,49 +210,17 @@ noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
  | whileFalse ρ e s _ =>
    exact EndToEndTrace.loop_empty

-/-- The input / entry node generated by `Graph.wrap`. -/
-def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
-  (0 : Fin 1).castAdd ((g ⤳ Graph.singleton none).size)
+namespace Program

-/-- The output / exit node generated by `Graph.wrap`. -/
-def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
-  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
+noncomputable def trace (p : Program) {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
+    Trace p.cfg p.initialState p.finalState [] ρ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h)
+  rw [Graph.wrap_inputs, List.mem_singleton] at h₁
+  rw [Graph.wrap_outputs, List.mem_singleton] at h₂
+  subst h₁; subst h₂
+  exact tr

-/-- The `Graph.wrapInput` is, indeed, the graph's only input after `Graph.wrap`. -/
-lemma Graph.wrap_inputs (g : Graph) :
-    (Graph.wrap g).inputs = [g.wrapInput] := rfl
+end Program

-/-- The `Graph.wrapInput` is, indeed, the graph's only output after `Graph.wrap`. -/
-lemma Graph.wrap_outputs (g : Graph) :
-    (Graph.wrap g).outputs = [g.wrapOutput] := rfl
-
-/-- When sequencing (proven here with `Graph.singleton` on the left), no edges
-    exist from the right-hand graph back to the left. -/
-private lemma not_mem_edges_castAdd_sequence {g₂ : Graph} (i : Fin 1)
-    (idx : (Graph.singleton none ⤳ g₂).Index) :
-    ((idx, i.castAdd g₂.size) : (Graph.singleton none ⤳ g₂).Edge)
-      ∉ (Graph.singleton none ⤳ g₂).edges := by
-  intro h
-  rcases List.mem_append.mp h with h' | h'
-  · rcases List.mem_append.mp h' with h'' | h''
-    · -- lifted edges of `singleton []`: there are none
-      simp [Graph.singleton, List.finCastAddProd] at h''
-    · -- lifted edges of g₂: targets are natAdd
-      obtain ⟨e, _, heq⟩ := List.mem_map.mp h''
-      exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm
-  · -- product edges: targets are natAdd'd inputs of g₂
-    obtain ⟨-, hb⟩ := List.mem_product.mp h'
-    obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
-    exact Fin.castAdd_ne_natAdd i j heq.symm
-
-/-- The input node of a graph after `Graph.wrap` has no predecessors. -/
-lemma Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
-    (h : idx ∈ (Graph.wrap g).inputs) :
-    (Graph.wrap g).predecessors idx = [] := by
-  rw [Graph.wrap_inputs, List.mem_singleton] at h
-  subst h
-  rw [GGraph.predecessors, List.filter_eq_nil_iff]
-  intro idx' _
-  simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ Graph.singleton none) 0 idx'

 end Spa
--- a/lean/Spa/Language/Semantics.lean
+++ b/lean/Spa/Language/Semantics.lean
@@ -33,7 +33,7 @@ inductive Env.Mem : String × Value → Env → Prop
 /-- Inference rules for evaluating an expression (`Spa.Expr`) in a given
    environment. Pretty standard big-step expression evaluation. -/
 inductive EvalExpr : Env → Expr → Value → Prop
-  | num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n)
+  | num (ρ : Env) (z : ℤ) : EvalExpr ρ (.num z) (.int z)
  | var (ρ : Env) (x : String) (v : Value) :
      Env.Mem (x, v) ρ → EvalExpr ρ (.var x) v
  | add (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) :
--- a/lean/Spa/Language/Tagged/Basic.lean
+++ b/lean/Spa/Language/Tagged/Basic.lean
@@ -1,18 +0,0 @@
-import Spa.Language.Base
-import Spa.Language.Tagged.Id
-import Spa.Language.Tagged.Derive
-
-derive_tagged Spa.Expr Spa.BasicStmt Spa.Stmt
-
-namespace Spa
-
-def tagStmt (s : Stmt) : Stmt.Tagged RawId := (s.tag 0).1
-
-def Stmt.Tagged.subtreeIds {τ : Type} (s : Stmt.Tagged τ) : List τ :=
-  s.foldTags (· :: ·) []
-
-def Stmt.Tagged.isInLoopBody {τ : Type} [DecidableEq τ]
-    (body : Stmt.Tagged τ) (id : τ) : Bool :=
-  decide (id ∈ body.subtreeIds)
-
-end Spa
--- a/lean/Spa/Language/Tagged/Derive.lean
+++ b/lean/Spa/Language/Tagged/Derive.lean
@@ -1,509 +0,0 @@
-import Lean
-import Mathlib.Tactic.DeriveTraversable
-import Spa.Language.Base
-import Spa.Language.Tagged.Id
-
-/-!
-# The `derive_tagged` command
-
-`derive_tagged T₁ T₂ … Tₙ` takes a family of (possibly mutually recursive)
-inductive types and generates, for each `Tᵢ`:
-
-* a *tagged* mirror inductive `Tᵢ.Tagged (τ : Type)`, in which every constructor
-  carries a leading `tag : τ` field and every field whose type is a family
-  member is retyped to its `.Tagged τ` counterpart;
-* `Tᵢ.Tagged.erase : Tᵢ.Tagged τ → Tᵢ`, forgetting all tags;
-* `Tᵢ.tag : Tᵢ → ℕ → Tᵢ.Tagged RawId × ℕ`, assigning every node a unique
-  `RawId` (its postorder index) by a single unified traversal that threads a
-  counter; the whole family shares one counter, so identifiers are unique across
-  types.
-
-The generated declarations have exactly the shape of the hand-written reference;
-see `Spa/Language/Tagged/Basic.lean` (which invokes this command) and the proofs
-in `Spa/Language/Tagged/Properties.lean`.
-
-Scope: the generator handles non-indexed inductives whose constructor fields are
-either scalars or *direct* references to a family member (which covers the object
-language).  Nested occurrences such as `List Tᵢ` are not supported.
-/
-
-open Lean Elab Command Meta
-
-namespace Spa.DeriveTagged
-
-/-- One constructor field, classified as a recursive family reference or a scalar
-(whose type syntax we keep verbatim for the mirror inductive). -/
-structure FieldData where
-  isRec : Bool
-  recType : Name
-  typeStx : Term
-
-/-- A constructor: its original (full) name, short name, and fields. -/
-structure CtorData where
-  origName : Name
-  shortName : Name
-  fields : Array FieldData
-
-/-- A family member together with its constructors. -/
-structure TypeData where
-  name : Name
-  ctors : Array CtorData
-
-def taggedOf (n : Name) : Name := n ++ `Tagged
-def eraseOf (n : Name) : Name := n ++ `Tagged ++ `erase
-def rootTagOf (n : Name) : Name := n ++ `Tagged ++ `rootTag
-def tagOf (n : Name) : Name := n ++ `tag
-def foldTagsOf (n : Name) : Name := n ++ `Tagged ++ `foldTags
-def wfOf (n : Name) : Name := n ++ `Tagged ++ `WF
-def narrowOf (n : Name) : Name := n ++ `Tagged ++ `narrow
-def narrowEraseOf (n : Name) : Name := n ++ `Tagged ++ `narrow_erase
-def tagLeOf (n : Name) : Name := n ++ `tag_le
-def tagRootTagPostOf (n : Name) : Name := n ++ `tag_rootTag_post
-def tagWfOf (n : Name) : Name := n ++ `tag_wf
-
-/-- Project the `i`-th conjunct (1-based) out of `hyp`, which has type a
-right-nested `And` of `total` conjuncts, e.g. `hyp |>.2 |>.2 |>.1`. -/
-def projAnd {m : Type → Type} [Monad m] [MonadQuotation m]
-    (hyp : Term) (i total : Nat) : m Term := do
-  let mut t := hyp
-  for _ in [0:i-1] do
-    t ← `($t |>.2)
-  if i < total then
-    t ← `($t |>.1)
-  return t
-
-/-- Combine a non-empty array of propositions into a right-nested conjunction. -/
-def mkAndR {m : Type → Type} [Monad m] [MonadQuotation m]
-    (cs : Array Term) : m Term := do
-  let mut t := cs.back!
-  for c in cs.pop.reverse do
-    t ← `($c ∧ $t)
-  return t
-
-/-- For a constructor, return one entry per *recursive* field: its argument
-identifier, the family member it references, and the start-counter expression at
-which it is tagged (`n`, then `(a.tag n).2`, …) — the same threading `mkTag`
-uses. -/
-def recChildren (cd : CtorData) (argNames : Array Ident) (nStart : Term) :
-    CommandElabM (Array (Ident × Name × Term)) := do
-  let mut res : Array (Ident × Name × Term) := #[]
-  let mut cur := nStart
-  for (f, a) in cd.fields.zip argNames do
-    if f.isRec then
-      res := res.push (a, f.recType, cur)
-      cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
-  return res
-
-/-- Inspect the family, classifying each constructor field. -/
-def gather (family : Array Name) (τ : Ident) : TermElabM (Array TypeData) := do
-  let famSet : NameSet := family.foldl (·.insert ·) {}
-  family.mapM fun tn => do
-    let iv ← getConstInfoInduct tn
-    let ctors ← iv.ctors.toArray.mapM fun cn => do
-      let cv ← getConstInfoCtor cn
-      let fields ← forallTelescopeReducing cv.type fun args _ => do
-        let fieldArgs := args.extract iv.numParams args.size
-        fieldArgs.mapM fun a => do
-          let ty ← inferType a
-          match ty.getAppFn.constName? with
-          | some hn =>
-            if famSet.contains hn then
-              return { isRec := true, recType := hn, typeStx := ← `($(mkIdent (taggedOf hn)) $τ) }
-            else
-              return { isRec := false, recType := default, typeStx := ← Lean.PrettyPrinter.delab ty }
-          | none =>
-            return { isRec := false, recType := default, typeStx := ← Lean.PrettyPrinter.delab ty }
-      return { origName := cn, shortName := cn.componentsRev.head!, fields }
-    return { name := tn, ctors }
-
-/-- The arrow type `τ → <fields…> → Self τ` of a tagged constructor. -/
-def ctorArrow (cd : CtorData) (self : Term) (τ : Ident) : TermElabM Term := do
-  let mut t := self
-  for f in cd.fields.reverse do
-    t ← `($(f.typeStx) → $t)
-  `($τ → $t)
-
-/-- The tagged mirror inductives, one per family member.  The family is a DAG
-(`Expr ← BasicStmt ← Stmt`), not genuinely mutual, so they are emitted as
-separate inductives in dependency order rather than a `mutual` block.
-
-`Functor`/`Traversable` instances are derived separately by `mkDeriveInstances`
-below rather than via an inline `deriving` clause. -/
-def mkInductives (tds : Array TypeData) (τ : Ident) :
-    CommandElabM (Array (TSyntax `command)) := do
-  tds.mapM fun td => do
-    let self ← `($(mkIdent (taggedOf td.name)) $τ)
-    let ctors ← td.ctors.mapM fun cd => do
-      let aty ← Command.liftTermElabM (ctorArrow cd self τ)
-      `(Lean.Parser.Command.ctor| | $(mkIdent cd.shortName):ident : $aty)
-    `(command| inductive $(mkIdent (taggedOf td.name)):ident ($τ : Type) where $ctors*)
-
-/-- A `deriving instance Functor, Traversable for Tᵢ.Tagged` command per family
-member.  Since every tagged type is a single-parameter, direct-recursive
-inductive in `τ`, Mathlib's deriving handler produces clean (`sorry`-free)
-instances, giving `map`, `traverse`, and the `Traversable.foldr`/`toList` folds
-for free.
-
-These are emitted as *separate* commands in dependency order (rather than an
-inline `deriving` clause on each inductive) for two reasons: deriving
-`Stmt.Tagged` needs the `Expr.Tagged`/`BasicStmt.Tagged` instances already in
-scope, and — because every member's type name ends in `.Tagged` — the handler's
-auto-generated instance name (`instFunctorTagged`, built from the type's last
-component) collides across the family unless each derive sees the environment
-the previous one updated; separate commands give it that, so the names
-disambiguate to `instFunctorTagged`, `instFunctorTagged_1`, ….
-
-The hand-written `foldTags` is retained alongside these: it is a
-structural-recursion fold that `simp`/`decide` reduce cleanly, unlike the
-abstract `Traversable.foldr` (defined via the `FreeMonoid`/`Const` applicative),
-which reduces under `decide`/`rfl` but not naive `simp` unfolding. -/
-def mkDeriveInstances (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  tds.mapM fun td =>
-    `(command| deriving instance Functor, Traversable for $(mkIdent (taggedOf td.name)))
-
-/-- The `erase` functions, one per family member (separate defs in dependency
-order — each calls only already-defined lower members). -/
-def mkErase (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
-      let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) _ $argNames*)
-      let eraseArgs ← (cd.fields.zip argNames).mapM fun (f, a) =>
-        if f.isRec then `($(mkIdent (eraseOf f.recType)) $a) else pure a
-      let rhs ← `($(mkIdent cd.origName) $eraseArgs*)
-      pats := pats.push pat
-      rhss := rhss.push rhs
-    `(command| def $(mkIdent (eraseOf td.name)) {τ : Type} :
-        $(mkIdent (taggedOf td.name)) τ → $(mkIdent td.name) :=
-        fun x => match x with $[| $pats => $rhss]*)
-
-/-- The `rootTag` accessors (one non-recursive `def` per type). -/
-def mkRootTag (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let tIdent := mkIdent `t
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let hole ← `(_)
-      let wilds := Array.mkArray cd.fields.size hole
-      pats := pats.push (← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tIdent $wilds*))
-      rhss := rhss.push tIdent
-    `(command| def $(mkIdent (rootTagOf td.name)) {τ : Type} :
-        $(mkIdent (taggedOf td.name)) τ → τ :=
-        fun x => match x with $[| $pats => $rhss]*)
-
-/-- The postorder `tag` functions, one per family member (separate defs in
-dependency order). -/
-def mkTag (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let nId := mkIdent ``Spa.RawId
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
-      let pat ← `($(mkIdent cd.origName) $argNames*)
-      let mut cur : Term ← `(n)
-      let mut lets : Array (Ident × Term) := #[]
-      let mut taggedArgs : Array Term := #[]
-      let mut ri := 0
-      for (f, a) in cd.fields.zip argNames do
-        if f.isRec then
-          let rName := mkIdent (.mkSimple s!"r{ri}")
-          let rhsCall ← `($(mkIdent (tagOf f.recType)) $a $cur)
-          lets := lets.push (rName, rhsCall)
-          taggedArgs := taggedArgs.push (← `($rName |>.1))
-          cur ← `($rName |>.2)
-          ri := ri + 1
-        else
-          taggedArgs := taggedArgs.push a
-      let last := cur
-      let tagged ← `($(mkIdent (taggedOf td.name ++ cd.shortName))
-          (⟨$last⟩ : $nId) $taggedArgs*)
-      let mut body ← `(($tagged, $last + 1))
-      for (rName, rhs) in lets.reverse do
-        body ← `(let $rName := $rhs; $body)
-      pats := pats.push pat
-      rhss := rhss.push body
-    `(command| def $(mkIdent (tagOf td.name)) :
-        $(mkIdent td.name) → Nat → $(mkIdent (taggedOf td.name)) $nId × Nat :=
-        fun e n => match e with $[| $pats => $rhss]*)
-
-/-- The tag-fold functions: `foldTags f acc t` applies `f` to every tag in `t`,
-right-to-left, threading `acc`.  This is the `Foldable`/`foldr`-over-tags the
-hand-written collectors (e.g. `subtreeIds`) reduce to.  One separate def per
-family member (the family is a DAG, so no `mutual` block is needed). -/
-def mkFoldTags (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let τ := mkIdent `τ
-  let m := mkIdent `M
-  let fId := mkIdent `f
-  let accId := mkIdent `acc
-  let tagId := mkIdent `t
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map (fun i => mkIdent (.mkSimple s!"a{i}"))
-      let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tagId $argNames*)
-      let mut body : Term := accId
-      for (fld, a) in (cd.fields.zip argNames).reverse do
-        if fld.isRec then
-          body ← `($(mkIdent (foldTagsOf fld.recType)) $fId $body $a)
-      body ← `($fId $tagId $body)
-      pats := pats.push pat
-      rhss := rhss.push body
-    `(command| def $(mkIdent (foldTagsOf td.name)) {$τ:ident : Type} {$m:ident : Type}
-        ($fId : $τ → $m → $m) ($accId : $m) :
-        $(mkIdent (taggedOf td.name)) $τ → $m :=
-        fun x => match x with $[| $pats => $rhss]*)
-
-/-- The well-formedness predicate `T.Tagged.WF : T.Tagged RawId → Prop`: every
-recursive child's root tag has a strictly smaller postorder index than the node's
-own tag, and each child is itself well-formed.  Leaf constructors are `True`. -/
-def mkWF (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let tId := mkIdent `t
-  let rawId := mkIdent ``Spa.RawId
-  tds.mapM fun td => do
-    let mut pats : Array Term := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let hasRec := cd.fields.any (·.isRec)
-      let mut patArgs : Array Term := #[]
-      let mut recArgs : Array Ident := #[]
-      let mut i := 0
-      for f in cd.fields do
-        if f.isRec then
-          let a := mkIdent (.mkSimple s!"a{i}")
-          patArgs := patArgs.push a
-          recArgs := recArgs.push a
-        else
-          patArgs := patArgs.push (← `(_))
-        i := i + 1
-      let tagBind : Term ← if hasRec then `($tId) else `(_)
-      let pat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tagBind $patArgs*)
-      let rhs ← if recArgs.isEmpty then `(True) else do
-        let bounds ← recArgs.mapM fun a => `($(a).rootTag.post < $(tId).post)
-        let wfs ← recArgs.mapM fun a => `($(a).WF)
-        mkAndR (bounds ++ wfs)
-      pats := pats.push pat
-      rhss := rhss.push rhs
-    `(command| def $(mkIdent (wfOf td.name)) :
-        $(mkIdent (taggedOf td.name)) $rawId → Prop :=
-        fun x => match x with $[| $pats => $rhss]*)
-
-/-- The `narrow` coercion `T.Tagged RawId → T.Tagged (Fin N)`, given a bound on
-the root tag and a well-formedness proof.  Each node's tag becomes the `Fin N`
-built from its postorder index, and recursion threads the bound through `lt_trans`
-and the (definitionally unfolded) `WF` conjunction. -/
-def mkNarrow (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let rawId := mkIdent ``Spa.RawId
-  let tId := mkIdent `t
-  let nId := mkIdent `N
-  let hId := mkIdent `h
-  let hwfId := mkIdent `hwf
-  let tgId := mkIdent `tg
-  tds.mapM fun td => do
-    let self ← `($(mkIdent (taggedOf td.name)) $rawId)
-    let mut patss : Array (Array Term) := #[]
-    let mut rhss : Array Term := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-      let ctorPat ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) $tgId $argNames*)
-      let k := (cd.fields.filter (·.isRec)).size
-      let mut newArgs : Array Term := #[]
-      let mut ri := 0
-      for (f, a) in cd.fields.zip argNames do
-        if f.isRec then
-          let bound ← projAnd hwfId (ri + 1) (2 * k)
-          let wf ← projAnd hwfId (k + ri + 1) (2 * k)
-          newArgs := newArgs.push (← `($(a).narrow (lt_trans $bound $hId) $wf))
-          ri := ri + 1
-        else
-          newArgs := newArgs.push a
-      let built ← `($(mkIdent (taggedOf td.name ++ cd.shortName)) ⟨$(tgId).post, $hId⟩ $newArgs*)
-      let nPat ← `(_)
-      let hPat ← `($hId)
-      let hwfPat : Term ← if k == 0 then `(_) else `($hwfId)
-      patss := patss.push #[ctorPat, nPat, hPat, hwfPat]
-      rhss := rhss.push built
-    `(command| def $(mkIdent (narrowOf td.name)) : ($tId : $self) → {$nId : ℕ} →
-        $(tId).rootTag.post < $nId → $(tId).WF → $(mkIdent (taggedOf td.name)) (Fin $nId)
-        $[| $[$patss],* => $rhss]*)
-
-/-- `T.tag_rootTag_post`: the root tag of a freshly tagged node is exactly one
-below the threaded-out counter, i.e. the node itself is numbered last (postorder).
-A uniform `cases <;> simp` discharges every constructor. -/
-def mkTagRootTagPost (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let eId := mkIdent `e
-  let nId := mkIdent `n
-  tds.mapM fun td =>
-    `(command| theorem $(mkIdent (tagRootTagPostOf td.name))
-        ($eId : $(mkIdent td.name)) ($nId : ℕ) :
-        ($(eId).tag $nId).1.rootTag.post + 1 = ($(eId).tag $nId).2 := by
-        cases $eId:ident <;>
-          simp [$(mkIdent (tagOf td.name)):ident, $(mkIdent (rootTagOf td.name)):ident])
-
-/-- `T.tag_le`: tagging only ever advances the counter (`n ≤ (e.tag n).2`).
-Proved by induction; each arm threads the counter through its recursive children
-(using the relevant `tag_le`/induction hypothesis) and closes with `omega`. -/
-def mkTagLe (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let eId := mkIdent `e
-  let nId := mkIdent `n
-  tds.mapM fun td => do
-    let mut ctorLabels : Array Ident := #[]
-    let mut binderss : Array (Array Ident) := #[]
-    let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-      let mut ihBinders : Array Ident := #[]
-      let mut haveTacs : Array (TSyntax `tactic) := #[]
-      let mut cur : Term ← `($nId)
-      let mut i := 0
-      for (f, a) in cd.fields.zip argNames do
-        if f.isRec then
-          let fact ← if f.recType == td.name then
-              `($(mkIdent (.mkSimple s!"ih{i}")) $cur)
-            else
-              `($(mkIdent (tagLeOf f.recType)) $a $cur)
-          if f.recType == td.name then
-            ihBinders := ihBinders.push (mkIdent (.mkSimple s!"ih{i}"))
-          haveTacs := haveTacs.push (← `(tactic| have := $fact))
-          cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
-        i := i + 1
-      let simpTac ← `(tactic| simp only [$(mkIdent (tagOf td.name)):ident])
-      let omegaTac ← `(tactic| omega)
-      let allTacs := #[simpTac] ++ haveTacs ++ #[omegaTac]
-      ctorLabels := ctorLabels.push (mkIdent cd.shortName)
-      binderss := binderss.push (argNames ++ ihBinders)
-      tacs := tacs.push (← `(tacticSeq| $[$allTacs]*))
-    `(command| theorem $(mkIdent (tagLeOf td.name)) ($eId : $(mkIdent td.name)) ($nId : ℕ) :
-        $nId ≤ ($(eId).tag $nId).2 := by
-        induction $eId:ident generalizing $nId:ident with
-          $[| $ctorLabels:ident $binderss* => $tacs]*)
-
-/-- `T.tag_wf`: a freshly tagged term is well-formed.  Each recursive child's
-bound conjunct is closed by `omega` from that child's `tag_rootTag_post` plus the
-`tag_le` of every later child (which bounds the threaded-out counter), and each
-well-formedness conjunct is the child's induction hypothesis / `tag_wf`. -/
-def mkTagWf (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let eId := mkIdent `e
-  let nId := mkIdent `n
-  tds.mapM fun td => do
-    let mut ctorLabels : Array Ident := #[]
-    let mut binderss : Array (Array Ident) := #[]
-    let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-      -- recursive children: (arg, recType, startCounter, sameType?, fieldIndex)
-      let mut recs : Array (Ident × Name × Term × Bool × Nat) := #[]
-      let mut cur : Term ← `($nId)
-      let mut i := 0
-      for (f, a) in cd.fields.zip argNames do
-        if f.isRec then
-          recs := recs.push (a, f.recType, cur, f.recType == td.name, i)
-          cur ← `(($(mkIdent (tagOf f.recType)) $a $cur) |>.2)
-        i := i + 1
-      let k := recs.size
-      let ihBinders := (recs.filter (·.2.2.2.1)).map fun r => mkIdent (.mkSimple s!"ih{r.2.2.2.2}")
-      let tac : TSyntax ``Lean.Parser.Tactic.tacticSeq ← if k == 0 then
-          `(tacticSeq| exact True.intro)
-        else do
-          let mut comps : Array Term := #[]
-          -- bound conjuncts
-          for idx in [0:k] do
-            let (a, rt, s, _, _) := recs[idx]!
-            let mut bHaves : Array (TSyntax `tactic) :=
-              #[← `(tactic| have := $(mkIdent (tagRootTagPostOf rt)) $a $s)]
-            for j in [idx+1:k] do
-              let (aj, rtj, sj, _, _) := recs[j]!
-              bHaves := bHaves.push (← `(tactic| have := $(mkIdent (tagLeOf rtj)) $aj $sj))
-            bHaves := bHaves.push (← `(tactic| omega))
-            comps := comps.push (← `(by $(← `(tacticSeq| $[$bHaves]*))))
-          -- well-formedness conjuncts
-          for idx in [0:k] do
-            let (a, rt, s, same, fi) := recs[idx]!
-            comps := comps.push <| ← if same then `($(mkIdent (.mkSimple s!"ih{fi}")) $s)
-              else `($(mkIdent (tagWfOf rt)) $a $s)
-          let simpTac ← `(tactic| simp only
-            [$(mkIdent (tagOf td.name)):ident, $(mkIdent (wfOf td.name)):ident])
-          let exactTac ← `(tactic| exact ⟨$comps,*⟩)
-          `(tacticSeq| $[$(#[simpTac, exactTac])]*)
-      ctorLabels := ctorLabels.push (mkIdent cd.shortName)
-      binderss := binderss.push (argNames ++ ihBinders)
-      tacs := tacs.push tac
-    `(command| theorem $(mkIdent (tagWfOf td.name)) ($eId : $(mkIdent td.name)) ($nId : ℕ) :
-        ($(eId).tag $nId).1.WF := by
-        induction $eId:ident generalizing $nId:ident with
-          $[| $ctorLabels:ident $binderss* => $tacs]*)
-
-/-- `T.Tagged.narrow_erase`: narrowing the tag type does not change the erased
-(untagged) term.  A per-constructor `simp` with the local `narrow`/`erase`
-equations, the lower members' `narrow_erase`, and the induction hypotheses. -/
-def mkNarrowErase (tds : Array TypeData) : CommandElabM (Array (TSyntax `command)) := do
-  let rawId := mkIdent ``Spa.RawId
-  let tId := mkIdent `t
-  let nId := mkIdent `N
-  let hId := mkIdent `h
-  let hwfId := mkIdent `hwf
-  let tgId := mkIdent `tg
-  tds.mapM fun td => do
-    let mut ctorLabels : Array Ident := #[]
-    let mut binderss : Array (Array Ident) := #[]
-    let mut tacs : Array (TSyntax ``Lean.Parser.Tactic.tacticSeq) := #[]
-    for cd in td.ctors do
-      let argNames := (Array.range cd.fields.size).map fun i => mkIdent (.mkSimple s!"a{i}")
-      let mut lemmas : Array Term :=
-        #[← `($(mkIdent (narrowOf td.name))), ← `($(mkIdent (eraseOf td.name)))]
-      let mut ihBinders : Array Ident := #[]
-      let mut seenLower : Array Name := #[]
-      let mut i := 0
-      for f in cd.fields do
-        if f.isRec then
-          if f.recType == td.name then
-            let ih := mkIdent (.mkSimple s!"ih{i}")
-            ihBinders := ihBinders.push ih
-            lemmas := lemmas.push (← `($ih))
-          else if !seenLower.contains f.recType then
-            seenLower := seenLower.push f.recType
-            lemmas := lemmas.push (← `($(mkIdent (narrowEraseOf f.recType))))
-        i := i + 1
-      let introTac ← `(tactic| intro $nId $hId $hwfId)
-      let simpTac ← `(tactic| simp [$[$lemmas:term],*])
-      ctorLabels := ctorLabels.push (mkIdent cd.shortName)
-      binderss := binderss.push (#[tgId] ++ argNames ++ ihBinders)
-      tacs := tacs.push (← `(tacticSeq| $[$(#[introTac, simpTac])]*))
-    `(command| theorem $(mkIdent (narrowEraseOf td.name)) :
-        ($tId : $(mkIdent (taggedOf td.name)) $rawId) → ∀ {$nId : ℕ}
-          ($hId : $(tId).rootTag.post < $nId) ($hwfId : $(tId).WF),
-          ($(tId).narrow $hId $hwfId).erase = $(tId).erase := by
-        intro $tId:ident
-        induction $tId:ident with
-          $[| $ctorLabels:ident $binderss* => $tacs]*)
-
-/-- `derive_tagged T₁ … Tₙ` — generate tagged mirrors, `erase`, and `tag` for the
-given family of inductives. -/
-syntax (name := deriveTaggedCmd) "derive_tagged " ident+ : command
-
-@[command_elab deriveTaggedCmd]
-def elabDeriveTagged : CommandElab := fun stx => do
-  match stx with
-  | `(derive_tagged $ids*) =>
-    let family ← ids.mapM fun i => Command.liftCoreM (realizeGlobalConstNoOverload i)
-    let τ := mkIdent `τ
-    let tds ← Command.liftTermElabM (gather family τ)
-    for d in (← mkInductives tds τ) do elabCommand d
-    for d in (← mkDeriveInstances tds) do elabCommand d
-    for d in (← mkRootTag tds) do elabCommand d
-    for d in (← mkErase tds) do elabCommand d
-    for d in (← mkTag tds) do elabCommand d
-    for d in (← mkFoldTags tds) do elabCommand d
-    for d in (← mkWF tds) do elabCommand d
-    for d in (← mkNarrow tds) do elabCommand d
-    for d in (← mkTagRootTagPost tds) do elabCommand d
-    for d in (← mkTagLe tds) do elabCommand d
-    for d in (← mkTagWf tds) do elabCommand d
-    for d in (← mkNarrowErase tds) do elabCommand d
-  | _ => throwUnsupportedSyntax
-
-end Spa.DeriveTagged
--- a/lean/Spa/Language/Tagged/Graphs.lean
+++ b/lean/Spa/Language/Tagged/Graphs.lean
@@ -1,104 +0,0 @@
-import Spa.Language
-import Spa.Language.Graphs
-import Spa.Language.Tagged.Basic
-import Spa.Language.Tagged.Properties
-
-namespace Spa
-
-open GGraph
-
-def Stmt.Tagged.cfg {τ : Type} : Stmt.Tagged τ → GGraph (Option (BasicStmt.Tagged τ))
-  | .basic _ bs => GGraph.singleton (some bs)
-  | .andThen _ s₁ s₂ => s₁.cfg ⤳  s₂.cfg
-  | .ifElse _ _ s₁ s₂ => s₁.cfg ∙ s₂.cfg
-  | .whileLoop _ _ s => GGraph.loop s.cfg
-
-theorem Stmt.Tagged.cfg_graph {τ : Type} : ∀ (t : Stmt.Tagged τ),
-    (Option.map BasicStmt.Tagged.erase) <$> t.cfg = t.erase.cfg
-  | .basic _ bs => by simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, BasicStmt.Tagged.erase]
-  | .andThen _ s₁ s₂ => by
-      simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s₁, Stmt.Tagged.cfg_graph s₂]
-  | .ifElse _ _ s₁ s₂ => by
-      simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s₁, Stmt.Tagged.cfg_graph s₂]
-  | .whileLoop _ _ s => by
-      simp [Stmt.Tagged.cfg, Stmt.cfg, Stmt.Tagged.erase, Stmt.Tagged.cfg_graph s]
-
-def GGraph.nodeLabel {τ : Type} (g : GGraph (Option (BasicStmt.Tagged τ))) (i : g.Index) :
-    Option τ :=
-  (g.nodes i).map BasicStmt.Tagged.rootTag
-
-def GGraph.stateOf {τ : Type} [DecidableEq τ] (g : GGraph (Option (BasicStmt.Tagged τ)))
-    (id : τ) : Option g.Index :=
-  g.indices.find? (fun i => decide (g.nodeLabel i = some id))
-
-theorem GGraph.stateOf_label {τ : Type} [DecidableEq τ]
-    {g : GGraph (Option (BasicStmt.Tagged τ))} {id : τ}
-    {i : g.Index} (h : g.stateOf id = some i) : g.nodeLabel i = some id := by
-  rw [GGraph.stateOf] at h
-  simpa using List.find?_some h
-
-namespace Program
-
-variable (p : Program)
-
-def tagged : Stmt.Tagged RawId := tagStmt p.rootStmt
-
-def size : ℕ := p.tagged.rootTag.post + 1
-
-theorem size_pos : 0 < p.size := Nat.succ_pos _
-
-abbrev NodeId : Type := Fin p.size
-
-theorem tagged_wf : p.tagged.WF := Stmt.tag_wf p.rootStmt 0
-
-def taggedFin : Stmt.Tagged p.NodeId :=
-  p.tagged.narrow (Nat.lt_succ_self _) p.tagged_wf
-
-def taggedCfg : GGraph (Option (BasicStmt.Tagged p.NodeId)) :=
-  GGraph.wrap p.taggedFin.cfg
-
-theorem taggedCfg_erase :
-    (Option.map BasicStmt.Tagged.erase) <$> p.taggedCfg = p.cfg := by
-  rw [taggedCfg, GGraph.map_wrap, Stmt.Tagged.cfg_graph, taggedFin,
-    Stmt.Tagged.narrow_erase, tagged, erase_tagStmt]
-  rfl
-
-theorem taggedCfg_size : p.taggedCfg.size = p.cfg.size := by
-  conv_rhs => rw [← p.taggedCfg_erase]
-  rfl
-
-def nodeIdOf (s : p.State) : Option p.NodeId :=
-  p.taggedCfg.nodeLabel (Fin.cast p.taggedCfg_size.symm s)
-
-def stateOfNodeId (id : p.NodeId) : Option p.State :=
-  (p.taggedCfg.stateOf id).map (Fin.cast p.taggedCfg_size)
-
-theorem cfg_nodes_eq (s : p.State) :
-    p.cfg.nodes s = Option.map BasicStmt.Tagged.erase
-      (p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s)) := by
-  have key : ∀ (g : Graph) (hsz : p.taggedCfg.size = g.size),
-      (Option.map BasicStmt.Tagged.erase) <$> p.taggedCfg = g →
-      ∀ i : Fin g.size,
-        g.nodes i = Option.map BasicStmt.Tagged.erase
-          (p.taggedCfg.nodes (Fin.cast hsz.symm i)) := by
-    intro g hsz hg i
-    subst hg
-    rfl
-  exact key p.cfg p.taggedCfg_size p.taggedCfg_erase s
-
-theorem nodeIdOf_isSome_of_code {s : p.State} {bs : BasicStmt}
-    (h : p.code s = some bs) : (p.nodeIdOf s).isSome = true := by
-  have hc : Option.map BasicStmt.Tagged.erase
-      (p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s)) = some bs := by
-    rw [← p.cfg_nodes_eq s]; exact h
-  unfold Program.nodeIdOf GGraph.nodeLabel
-  cases hcase : p.taggedCfg.nodes (Fin.cast p.taggedCfg_size.symm s) with
-  | none => rw [hcase] at hc; simp at hc
-  | some tbs => simp
-
-def nodeIdOfNonempty (s : p.State) {bs : BasicStmt} (h : p.code s = some bs) : p.NodeId :=
-  (p.nodeIdOf s).get (p.nodeIdOf_isSome_of_code h)
-
-end Program
-
-end Spa
--- a/lean/Spa/Language/Tagged/Id.lean
+++ b/lean/Spa/Language/Tagged/Id.lean
@@ -1,9 +0,0 @@
-import Mathlib.Data.Nat.Notation
-
-namespace Spa
-
-structure RawId where
-  post : ℕ
-  deriving DecidableEq, Repr
-
-end Spa
--- a/lean/Spa/Language/Tagged/Properties.lean
+++ b/lean/Spa/Language/Tagged/Properties.lean
@@ -1,29 +0,0 @@
-import Spa.Language.Tagged.Basic
-
-namespace Spa
-
-@[simp] theorem Expr.erase_tag (e : Expr) (n : ℕ) : (e.tag n).1.erase = e := by
-  induction e generalizing n with
-  | add a b iha ihb => simp [Expr.tag, Expr.Tagged.erase, iha, ihb]
-  | sub a b iha ihb => simp [Expr.tag, Expr.Tagged.erase, iha, ihb]
-  | var x => simp [Expr.tag, Expr.Tagged.erase]
-  | num k => simp [Expr.tag, Expr.Tagged.erase]
-
-@[simp] theorem BasicStmt.erase_tag (bs : BasicStmt) (n : ℕ) :
-    (bs.tag n).1.erase = bs := by
-  cases bs with
-  | assign x e => simp [BasicStmt.tag, BasicStmt.Tagged.erase]
-  | noop => simp [BasicStmt.tag, BasicStmt.Tagged.erase]
-
-@[simp] theorem Stmt.erase_tag (s : Stmt) (n : ℕ) : (s.tag n).1.erase = s := by
-  induction s generalizing n with
-  | basic bs => simp [Stmt.tag, Stmt.Tagged.erase]
-  | andThen a b iha ihb => simp [Stmt.tag, Stmt.Tagged.erase, iha, ihb]
-  | ifElse e a b iha ihb => simp [Stmt.tag, Stmt.Tagged.erase, iha, ihb]
-  | whileLoop e s ih => simp [Stmt.tag, Stmt.Tagged.erase, ih]
-
-/-- Erasing a freshly tagged program recovers it. -/
-theorem erase_tagStmt (s : Stmt) : (tagStmt s).erase = s := by
-  simp [tagStmt]
-
-end Spa
--- a/lean/Spa/Language/Traces.lean
+++ b/lean/Spa/Language/Traces.lean
@@ -1,5 +1,6 @@
 import Spa.Language.Semantics
 import Spa.Language.Graphs
+import Spa.Language.Program

 /-!

@@ -36,24 +37,210 @@ 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 ρ₁ ρ₂

+/-- Every trace splits into the prefix that arrives at its last node and that node's own step. -/
+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 =>
+      let ⟨ρ, pre, step⟩ := rest.split
+      ⟨ρ, .cons hnode hedge 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
+
+structure Reaches {prog : Program} (s : prog.State) (ρin ρout : Env) : Type where
+  pre : Traceₗ prog.cfg prog.initialState s [] ρin
+  step : EvalBasicStmtOpt ρin (prog.code s) ρout
+
+/-- Forget the environment before the last evaluated state. -/
+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
--- a/lean/Spa/Lattice/AboveBelow.lean
+++ b/lean/Spa/Lattice/AboveBelow.lean
@@ -1,7 +1,38 @@
 import Spa.Lattice

+/-!
+
+# The Above-Below Lattice
+
+This file defines the `AboveBelow` lattice, which takes a flat domain
+$a_1, \ldots, a_n \in \alpha$ and lifts it into a lattice bounded
+above by a synthetic $\top$ element, and below by a synthetic $\bot$
+element.
+
+$$
+\begin{array}{ccccc}
+  && \top && \\
+  & \swarrow & \downarrow & \searrow & \\
+  a_1 & & … & & a_n \\
+  & \searrow & \downarrow & \swarrow & \\
+  && \bot &&
+\end{array}
+$$
+
+This lattice is also a `Spa.FiniteHeightLattice`, because no chain can
+exceed the bottom-to-top chain $\bot < a_i < \top$.
+
+The above-below lattice is helpful for for analyses such as
+`Spa/Analysis/Sign.lean` and `Spa/Analysis/Constant.lean`, whose
+classifications of values (by sign or by exact value) do not have
+any inherent structure beyond "matching exactly".
+
+-/
+
 namespace Spa

+/-- The above-below lattice, with bottom element `bot` and top element `top`. -/
+@[aesop safe cases]
 inductive AboveBelow (α : Type*) where
  | bot
  | top
@@ -10,8 +41,6 @@ inductive AboveBelow (α : Type*) where

 namespace AboveBelow

-attribute [aesop safe cases] AboveBelow
-
 instance {α : Type*} [ToString α] : ToString (AboveBelow α) where
  toString
    | bot => "⊥"
@@ -50,23 +79,12 @@ instance : Min (AboveBelow α) where
@[simp] lemma mk_inf_mk (x y : α) :
    (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl

-protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
-  aesop
-
-protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
-  aesop
-
-protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
-  aesop
-
-protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
-  aesop
-
-protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
-  aesop
-
-protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
-  aesop
+protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by aesop
+protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by aesop
+protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by aesop
+protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by aesop
+protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by aesop
+protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by aesop

 instance : Lattice (AboveBelow α) :=
  Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc
@@ -89,123 +107,72 @@ instance : OrderTop (AboveBelow α) where
  top := top
  le_top := le_top'

-lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
-  lt_of_le_of_ne (bot_le' _) (by simp)
-
-lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
-  lt_of_le_of_ne (le_top' _) (by simp)
-
-lemma bot_lt_top : (bot : AboveBelow α) < top :=
-  lt_of_le_of_ne (bot_le' _) (by simp)
+lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lt_of_le_of_ne (bot_le' _) (by simp)
+lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top := lt_of_le_of_ne (le_top' _) (by simp)
+lemma bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp)

 lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
    a = bot ∨ b = top ∨ a = b := by
-  have hsup := le_iff.mp h
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y
-  · exact Or.inl rfl
-  · exact Or.inr (Or.inl rfl)
-  · exact Or.inl rfl
-  · exact absurd hsup (by simp)
-  · exact Or.inr (Or.inl rfl)
-  · exact absurd hsup (by simp)
-  · exact absurd hsup (by simp)
-  · exact Or.inr (Or.inl rfl)
-  · rw [mk_sup_mk] at hsup
-    by_cases hxy : x = y
-    · exact Or.inr (Or.inr (by rw [hxy]))
-    · rw [if_neg hxy] at hsup
-      exact absurd hsup (by simp)
+  rw [le_iff] at h
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp_all

-/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to
-`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is
-monotone in both arguments — regardless of its values on plain elements.
-`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
-monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
+/-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤`
+    (against any non-`⊥` argument), it is monotone in both arguments.
+    The values of the the elements in `α` are irrelevant since they
+    are always incomparable. This makes it easy to prove monotonicity
+    for operations that "just" combine their flat elements, or give up. -/
 lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
    (f : AboveBelow α → AboveBelow β → AboveBelow γ)
    (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
    (htopl : ∀ y, y ≠ bot → f top y = top)
    (htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
-  constructor
-  · intro y a b hab
-    show f a y ≤ f b y
-    rcases le_cases hab with rfl | rfl | rfl
-    · rw [hbotl]; exact bot_le' _
-    · rcases eq_or_ne y bot with rfl | hy
-      · rw [hbotr, hbotr]
-      · rw [htopl y hy]; exact le_top' _
-    · exact le_rfl
-  · intro x a b hab
-    show f x a ≤ f x b
-    rcases le_cases hab with rfl | rfl | rfl
-    · rw [hbotr]; exact bot_le' _
-    · rcases eq_or_ne x bot with rfl | hx
-      · rw [hbotl, hbotl]
-      · rw [htopr x hx]; exact le_top' _
-    · exact le_rfl
-
-/-! ### Interpretations of flat lattices -/
+  constructor <;> intro c a b hab <;>
+    rcases eq_or_ne c bot with rfl | hc <;>
+    rcases le_cases hab with rfl | rfl | rfl <;>
+    simp [hbotl, hbotr, htopl, htopr, bot_le', le_top', *]

 section Interp

 variable {V : Type*} {P : AboveBelow α → V → Prop}

+/-- As long as the interpretation of a the above-below lattice respects the
+    fact that `bot` means "impossible", interpreting the above-below
+    lattice agrees with its `⊔`. -/
 lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
-    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
-  rcases s₁ with _ | _ | x
-  · rw [bot_sup]; exact h.resolve_left (hbot v)
-  · rw [top_sup]; exact htop v
-  · rcases s₂ with _ | _ | y
-    · rw [sup_bot]; exact h.resolve_right (hbot v)
-    · rw [sup_top]; exact htop v
-    · rw [mk_sup_mk]
-      split
-      · next heq => subst heq; exact h.elim id id
-      · exact htop v
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by aesop

+/-- As long as two distinct values in the flat domain don't overlap,
+    interpreting the above-below lattice agrees with its `⊔` -/
 lemma interp_inf_of
    (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
-  rcases s₁ with _ | _ | x
-  · rw [bot_inf]; exact h.1
-  · rw [top_inf]; exact h.2
-  · rcases s₂ with _ | _ | y
-    · rw [inf_bot]; exact h.2
-    · rw [inf_top]; exact h.1
-    · rw [mk_inf_mk]
-      split
-      · next heq => subst heq; exact h.1
-      · next hne => exact absurd h (hdisj hne v)
+  rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> simp_all
+  split
+  · exact h.2
+  · next hne => exact (hdisj hne v h.1 h.2).elim

 end Interp

-/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains
-(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
-def rank : AboveBelow α → ℕ
+/-- synthetic rank of an element, used to prove chain bounds. -/
+private def rank : AboveBelow α → ℕ
  | bot => 0
  | mk _ => 1
  | top => 2

-/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
-`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
+/-- It's not possible for any two lifted flat-domain elements to be less
+    than one another. -/
 lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
  intro h
  obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
  rcases le_cases hle with h | h | h <;> simp_all

+/-- The rank of elements is strictly monotonic. -/
 lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
  intro a b hab
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y
-  · exact absurd hab (lt_irrefl _)
-  · simp [rank]
-  · simp [rank]
-  · exact absurd hab (bot_le' _).not_lt
-  · exact absurd hab (lt_irrefl _)
-  · exact absurd hab (le_top' _).not_lt
-  · exact absurd hab (bot_le' _).not_lt
-  · simp [rank]
-  · exact absurd hab (not_mk_lt_mk x y)
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
+    simp_all [rank, not_mk_lt_mk, (bot_le' _).not_lt, (le_top' _).not_lt]

+/-- All chains in the above-below lattice have at most 2 comparisons. -/
 lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
  have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
  rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
--- a/lean/Spa/Lattice/FiniteMap.lean
+++ b/lean/Spa/Lattice/FiniteMap.lean
@@ -1,64 +1,79 @@
 import Spa.Lattice.Tuple
 import Mathlib.Data.List.Nodup

+/-!
+
+# Finite Maps
+
+This file defines _finite maps_, or key-value maps with a finite domain. This
+is encoded as a map from `Fin` into the value type. Finite maps form a
+lattice from pointwise composition: $(f \land g) k = f k \land g k$,
+and, provided the domain `\beta` is of finite height, so is the map
+lattice as a whole.
+
+In fact, the isomorphism is described and proven in `Spa/Lattice/Tuple.lean`.
+
+-/
+
 namespace Spa

-def FiniteMap (A B : Type*) (ks : List A) : Type _ := Fin ks.length → B
+/-- Key-value map with domain `α` and codomain `β`, with possible keys $\textit{ks} \subseteq \alpha$. -/
+def FiniteMap (α β : Type*) (ks : List α) : Type _ := Fin ks.length → β

 namespace FiniteMap

-variable {A B : Type*} {ks : List A}
+variable {α β : Type*} {ks : List α}

-instance [Lattice B] : Lattice (FiniteMap A B ks) :=
-  inferInstanceAs (Lattice (Fin ks.length → B))
+instance [Lattice β] : Lattice (FiniteMap α β ks) :=
+  inferInstanceAs (Lattice (Fin ks.length → β))

-instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
-  inferInstanceAs (FiniteHeightLattice (Fin ks.length → B))
+instance [FiniteHeightLattice β] : FiniteHeightLattice (FiniteMap α β ks) :=
+  inferInstanceAs (FiniteHeightLattice (Fin ks.length → β))

-instance [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
-  inferInstanceAs (DecidableEq (Fin ks.length → B))
+instance [DecidableEq β] : DecidableEq (FiniteMap α β ks) :=
+  inferInstanceAs (DecidableEq (Fin ks.length → β))

-instance : Membership (A × B) (FiniteMap A B ks) :=
+instance : Membership (α × β) (FiniteMap α β ks) :=
  ⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩

-lemma mem_iff {fm : FiniteMap A B ks} {p : A × B} :
+lemma mem_iff {fm : FiniteMap α β ks} {p : α × β} :
    p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl

-def MemKey (k : A) (_fm : FiniteMap A B ks) : Prop := k ∈ ks
+def MemKey (k : α) (_fm : FiniteMap α β ks) : Prop := k ∈ ks

-lemma MemKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
+lemma MemKey_iff {k : α} {fm : FiniteMap α β ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl

-instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] : Decidable (MemKey k fm) :=
+instance {k : α} {fm : FiniteMap α β ks} [DecidableEq α] : Decidable (MemKey k fm) :=
  decidable_of_iff _ MemKey_iff.symm

-lemma mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+lemma mem_key_of_mem {k : α} {v : β} {fm : FiniteMap α β ks}
    (h : (k, v) ∈ fm) : MemKey k fm := by
  obtain ⟨i, hi, _⟩ := h
  have hik : ks.get i = k := hi
  exact hik ▸ ks.get_mem i

-def toList (fm : FiniteMap A B ks) : List (A × B) :=
+def toList (fm : FiniteMap α β ks) : List (α × β) :=
  (List.finRange ks.length).map fun i => (ks.get i, fm i)

-lemma le_def [Lattice B] {fm₁ fm₂ : FiniteMap A B ks} :
+lemma le_def [Lattice β] {fm₁ fm₂ : FiniteMap α β ks} :
    fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl

 section Locate

-variable [DecidableEq A]
+variable [DecidableEq α]

 /-- Recover the value stored under a present key. -/
-def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
-    {v : B // (k, v) ∈ fm} :=
+def locate {k : α} {fm : FiniteMap α β ks} (h : MemKey k fm) :
+    {v : β // (k, v) ∈ fm} :=
  let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩
  ⟨fm i, i, List.idxOf_get _, rfl⟩

 end Locate

-variable [Lattice B]
+variable [Lattice β]

-lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
-    (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
+lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap α β ks}
+    (hle : fm₁ ≤ fm₂) {k : α} {v₁ v₂ : β}
    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
  obtain ⟨i, hi, rfl⟩ := h₁
  obtain ⟨j, hj, rfl⟩ := h₂
@@ -66,13 +81,13 @@ lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
  subst hij
  exact le_def.mp hle i

-lemma mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
+lemma mem_sup {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
    (h : (k, v) ∈ fm₁ ⊔ fm₂) :
    ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
  obtain ⟨i, hi, rfl⟩ := h
  exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩

-lemma mem_inf {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
+lemma mem_inf {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
    (h : (k, v) ∈ fm₁ ⊓ fm₂) :
    ∃ v₁ v₂, v = v₁ ⊓ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
  obtain ⟨i, hi, rfl⟩ := h
@@ -80,30 +95,30 @@ lemma mem_inf {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}

 section Updating

-variable [DecidableEq A]
+variable [DecidableEq α]

-def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : FiniteMap A B ks :=
+def updating (fm : FiniteMap α β ks) (ks' : List α) (g : α → β) : FiniteMap α β ks :=
  fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i

-omit [Lattice B] in
-lemma eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
-    {ks' : List A} {g : A → B} (hk : k ∈ ks')
+omit [Lattice β] in
+lemma eq_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
+    {ks' : List α} {g : α → β} (hk : k ∈ ks')
    (h : (k, v) ∈ updating fm ks' g) : v = g k := by
  obtain ⟨i, hi, rfl⟩ := h
  show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k
  rw [if_pos (by rw [hi]; exact hk), hi]

-omit [Lattice B] in
-lemma mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
-    {ks' : List A} {g : A → B} (hk : k ∉ ks')
+omit [Lattice β] in
+lemma mem_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
+    {ks' : List α} {g : α → β} (hk : k ∉ ks')
    (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
  obtain ⟨i, hi, rfl⟩ := h
  refine ⟨i, hi, ?_⟩
  show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
  rw [if_neg (by rw [hi]; exact hk)]

-lemma updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
-    {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
+lemma updating_mono {fm₁ fm₂ : FiniteMap α β ks} {ks' : List α}
+    {g₁ g₂ : α → β} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
    updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
  rw [le_def]
  intro i
@@ -117,25 +132,25 @@ end Updating

 section GeneralizedUpdate

-variable [DecidableEq A] {L : Type*} [Lattice L]
+variable [DecidableEq α] {L : Type*} [Lattice L]

-def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
-    (ks' : List A) : L → FiniteMap A B ks := fun l =>
+def generalizedUpdate (f : L → FiniteMap α β ks) (g : α → L → β)
+    (ks' : List α) : L → FiniteMap α β ks := fun l =>
  (f l).updating ks' (fun k => g k l)

-variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
+variable {f : L → FiniteMap α β ks} {g : α → L → β} {ks' : List α}

 lemma generalizedUpdate_monotone (hf : Monotone f)
    (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
  fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)

-omit [Lattice B] [Lattice L] in
-lemma generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
+omit [Lattice β] [Lattice L] in
+lemma generalizedUpdate_mem_eq {k : α} {v : β} {l : L} (hk : k ∈ ks')
    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
  eq_of_mem_updating (g := fun k => g k l) hk h

-omit [Lattice B] [Lattice L] in
-lemma generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+omit [Lattice β] [Lattice L] in
+lemma generalizedUpdate_not_mem_backward {k : α} {v : β} {l : L} (hk : k ∉ ks')
    (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l :=
  mem_of_mem_updating hk h

@@ -143,19 +158,19 @@ end GeneralizedUpdate

 section ValuesAt

-variable [DecidableEq A]
+variable [DecidableEq α]

 /-- The value stored under `k`, if `k` is a key. -/
-private def lookup (fm : FiniteMap A B ks) (k : A) : Option B :=
+private def lookup (fm : FiniteMap α β ks) (k : α) : Option β :=
  if h : k ∈ ks then some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none

 /-- The values stored under the keys `ks'` (skipping any that are not keys). -/
-def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
+def valuesAt (fm : FiniteMap α β ks) (ks' : List α) : List β :=
  ks'.filterMap fm.lookup

-omit [Lattice B] in
-lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
-    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
+omit [Lattice β] in
+lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap α β ks} {k : α} {v : β}
+    {ks' : List α} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
  refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
  obtain ⟨i, hi, rfl⟩ := h
  have hik : ks.get i = k := hi
@@ -167,7 +182,7 @@ lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
    hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
  rw [this]

-private lemma lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (k : A) :
+private lemma lookup_rel {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂) (k : α) :
    Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by
  show Option.Rel _
    (if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
@@ -176,8 +191,8 @@ private lemma lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂
  · rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _)
  · rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none

-lemma valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
-    (ks' : List A) :
+lemma valuesAt_le {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂)
+    (ks' : List α) :
    List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
  induction ks' with
  | nil => exact List.Forall₂.nil
--- a/lean/Spa/Lattice/Finset.lean
+++ b/lean/Spa/Lattice/Finset.lean
@@ -0,0 +1,38 @@
+import Spa.Lattice
+import Mathlib.Data.Finset.Lattice.Basic
+import Mathlib.Data.Fintype.Lattice
+import Mathlib.Data.Fintype.Card
+
+/-! # Power Sets of Finite Type
+
+For a `Fintype α`, `Finset α` is the power-set lattice: `⊔` is union, `⊓` is
+intersection, `⊥ = ∅`, `⊤ = univ`. This lattice also has a finite height.
+
+The `Finset α` representation s isomorphic to `Fin α → Bool`, but far more
+efficient because it avoids building up stacks of layered closures. -/
+
+namespace Spa
+
+variable {α : Type*} [Fintype α] [DecidableEq α]
+
+omit [Fintype α] [DecidableEq α] in
+private lemma finset_card_strictMono : StrictMono (Finset.card : Finset α → ℕ) :=
+  fun _ _ h => Finset.card_lt_card h
+
+omit [DecidableEq α] in
+/-- A strictly increasing chain of finsets grows its cardinality by at least one
+    each step, and cardinality is capped by `Fintype.card α`. -/
+lemma finset_boundedChains : BoundedChains (Finset α) (Fintype.card α) := fun c => by
+  have h := LTSeries.head_add_length_le_nat (c.map Finset.card finset_card_strictMono)
+  rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
+  have h2 : c.last.card ≤ Fintype.card α := Finset.card_le_univ _
+  omega
+
+instance instFiniteHeightFinset : FiniteHeightLattice (Finset α) where
+  toLattice := inferInstance
+  toOrderBot := inferInstance
+  toOrderTop := inferInstance
+  height := Fintype.card α
+  chains_bounded := finset_boundedChains
+
+end Spa
--- a/lean/Spa/Transformation/Licm.lean
+++ b/lean/Spa/Transformation/Licm.lean
@@ -1,26 +1,30 @@
 import Spa.Analysis.Reaching
-import Spa.Language.Tagged.Graphs

 /-!
 # Finding loop-invariant assignments (LICM groundwork)

 This wires the **reaching-definitions** analysis (`Spa/Analysis/Reaching.lean`)
-to the **tagged AST** to *find* — not yet move — assignments inside a `while`
-loop whose right-hand side depends only on definitions made *outside* the loop.
-These are the candidates a later LICM pass could hoist.
+to the AST to *find* — not yet move — assignments inside a `while` loop whose
+right-hand side depends only on definitions made *outside* the loop. These are
+the candidates a later LICM pass could hoist.

-The pipeline, for each assignment immediately enclosed by a loop:
+The traversal recurses over the plain `Stmt`, threading a `GGraph.Embed` of the
+current subtree's CFG into the program's (`Program.rootEmbed`, then one
+`Embed.trans` per descent). That embedding is what supplies program states:

-1. locate its CFG state via the tagged-graph bridge (`Program.stateOfNodeId`);
-2. read the reaching definitions at the assignment's *entry*
-   (`joinForKey s result` — the join over predecessors, i.e. before the
-   assignment itself runs);
+1. at an assignment, its CFG state is `Embed.singletonIndex` — the subtree's CFG
+   is a `singleton`, so its sole node is the state, and `nodes_eq` proves it
+   holds that very statement;
+2. read the reaching definitions at the assignment's *entry* (`joinForKey s
+   result` — the join over predecessors, i.e. before the assignment runs);
 3. union the definition sets of the RHS variables;
-4. map each definition site back to its `RawId` (`Program.nodeIdOf`) and check
-   it is **not** inside the loop body (structural `subtreeIds` membership).
+4. check no definition site lies in the loop body's CFG range. Every embedding is
+   a constant index shift, so the body occupies the interval
+   `[off, off + size)` (`GGraph.Embed.mem_range_iff`) and the test is two
+   comparisons.

 If every reaching definition of every RHS variable lies outside the loop, the
-assignment is reported as loop-invariant.  This is the first-order check ("all
+assignment is reported as loop-invariant. This is the first-order check ("all
 reaching definitions outside the loop"); transitive/iterated invariance and the
 actual hoisting are out of scope here.
 -/
@@ -29,64 +33,74 @@ namespace Spa

 namespace LicmTransformation

-open Forward
+open Forward GGraph
+
+/-- The CFG footprint of an enclosing loop: its entry node (for reporting) and
+the index interval its body occupies. -/
+structure Enclosing (prog : Program) where
+  /-- The loop's entry node, i.e. `GGraph.loopIn` embedded into the program. -/
+  loopState : prog.State
+  /-- Start of the body's index range. -/
+  bodyOff : ℕ
+  /-- Length of the body's index range. -/
+  bodySize : ℕ
+
+/-- Is this definition site inside the loop body's CFG range? -/
+def Enclosing.covers {prog : Program} (l : Enclosing prog) (d : prog.State) : Bool :=
+  decide (l.bodyOff ≤ d.val ∧ d.val < l.bodyOff + l.bodySize)

 /-- An assignment found inside a loop, paired with the data needed to test its
 invariance against that (immediately enclosing) loop. -/
 structure Candidate (prog : Program) where
-  /-- The enclosing `whileLoop`'s tag (for reporting). -/
-  loopId : prog.NodeId
-  /-- Every node id inside the loop body (the "is-child-of-loop" set). -/
-  bodyIds : List prog.NodeId
-  /-- The assignment `BasicStmt`'s tag — what labels its CFG node. -/
-  assignId : prog.NodeId
+  /-- The enclosing loop. -/
+  encl : Enclosing prog
+  /-- The assignment's CFG state. -/
+  assignState : prog.State
  /-- The variables read by the assignment's RHS. -/
  rhsVars : List String

 /-- Collect every assignment together with its *immediately enclosing* loop.
-`enclosing` carries the current loop's tag and body id-set, or `none` outside any
-loop (in which case assignments are skipped — only in-loop assignments are
-candidates). -/
-def collectCandidates (prog : Program) (enc : Option (prog.NodeId × List prog.NodeId)) :
-    Stmt.Tagged prog.NodeId → List (Candidate prog)
-  | .basic _ bs =>
+`enc` is `none` outside any loop, in which case assignments are skipped — only
+in-loop assignments are candidates. -/
+def collectCandidates (prog : Program) (enc : Option (Enclosing prog)) :
+    (s : Stmt) → Embed s.cfg prog.cfg → List (Candidate prog)
+  | .basic bs, e =>
      match bs, enc with
-      | .assign t _ e, some (loopId, bodyIds) =>
-          [{ loopId := loopId, bodyIds := bodyIds, assignId := t,
-             rhsVars := e.erase.vars.sort (· ≤ ·) }]
+      | .assign _ ex, some l =>
+          [{ encl := l, assignState := e.singletonIndex,
+             rhsVars := ex.vars.sort (· ≤ ·) }]
      | _, _ => []
-  | .andThen _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
-  | .ifElse _ _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
-  | .whileLoop loopT _ body =>
-      collectCandidates prog (some (loopT, body.subtreeIds)) body
+  | .andThen s₁ s₂, e =>
+      collectCandidates prog enc s₁ ((Embed.sequenceLeft s₁.cfg s₂.cfg).trans e) ++
+      collectCandidates prog enc s₂ ((Embed.sequenceRight s₁.cfg s₂.cfg).trans e)
+  | .ifElse _ s₁ s₂, e =>
+      collectCandidates prog enc s₁ ((Embed.overlayLeft s₁.cfg s₂.cfg).trans e) ++
+      collectCandidates prog enc s₂ ((Embed.overlayRight s₁.cfg s₂.cfg).trans e)
+  | .whileLoop _ body, e =>
+      let be := (Embed.loop body.cfg).trans e
+      collectCandidates prog
+        (some { loopState := e.f body.cfg.loopIn, bodyOff := be.off,
+                bodySize := body.cfg.size }) body be

 /-- Read the definition set assigned to variable `k`, or `⊥` if absent. -/
 def lookupDef (prog : Program) (vs : VariableValues (DefSet prog) prog)
    (k : String) : DefSet prog :=
  if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else ⊥

-/-- The AST node ids marked as definition sites in a `DefSet` (those mapped to
-`true`). With the AST-id-keyed lattice these are recovered directly. -/
-def defSites (prog : Program) (d : DefSet prog) : List prog.NodeId :=
-  (List.finRange prog.size).filter (fun i => d i)
-
 /-- Is the candidate assignment loop-invariant: do all reaching definitions of
-its RHS variables lie outside the loop body? Reaching sets are now keyed by AST
-node id, so we compare against the loop-body ids directly (embedding the raw
-body ids into `p.NodeId`). -/
+its RHS variables lie outside the loop body? -/
 def isInvariant (prog : Program) (c : Candidate prog) : Bool :=
-  match prog.stateOfNodeId c.assignId with
-  | none => false
-  | some s =>
-      let entry := joinForKey s (result (DefSet prog) prog)
-      let combined : DefSet prog :=
-        c.rhsVars.foldl (fun acc k => acc ⊔ lookupDef prog entry k) ⊥
-      (defSites prog combined).all (fun nid => ! decide (nid ∈ c.bodyIds))
+  let entry := joinForKey c.assignState (result (DefSet prog) prog)
+  let combined : DefSet prog :=
+    c.rhsVars.foldl (fun acc k => acc ⊔ lookupDef prog entry k) ⊥
+  -- `Finset.toList` is noncomputable; the decidable bounded-∀ folds over the
+  -- underlying multiset and keeps `lake exe` working.
+  decide (∀ d ∈ combined, c.encl.covers d = false)

-/-- The loop-invariant assignments of `prog`, as `(loopId, assignId)` pairs. -/
-def licmCandidates (prog : Program) : List (prog.NodeId × prog.NodeId) :=
-  (collectCandidates prog none prog.taggedFin).filterMap (fun c =>
-    if isInvariant prog c then some (c.loopId, c.assignId) else none)
+/-- The loop-invariant assignments of `prog`, as `(loop, assignment)` state pairs. -/
+def licmCandidates (prog : Program) : List (prog.State × prog.State) :=
+  (collectCandidates prog none prog.rootStmt prog.rootEmbed).filterMap (fun c =>
+    if isInvariant prog c then some (c.encl.loopState, c.assignState) else none)

 /-- A human-readable report of the loop-invariant assignments. -/
 def output (prog : Program) : String :=
Author	SHA1	Message	Date
Danila Fedorin	53f8bd47dc	Add function back in to Embedding	2026-08-09 21:43:20 -05:00
Danila Fedorin	fd371ba175	Remove trace suffix from Reaching type	2026-08-09 21:23:21 -05:00
Danila Fedorin	df4d072f22	Clean up comments in Graphs.lean and Program.lean	2026-08-09 18:17:02 -05:00
Danila Fedorin	c0542d0811	Allow negative numbers in expressions	2026-08-09 17:51:58 -05:00
Danila Fedorin	a19f9fa148	Get rid of Tagged	2026-08-09 17:38:56 -05:00
Danila Fedorin	269906871f	Update LICM/Reaching to node use NodeId	2026-08-09 17:35:30 -05:00
Danila Fedorin	1eecf45c0f	Add more machinery to use embeddings as "proofs of child-ship"	2026-08-09 17:30:38 -05:00
Danila Fedorin	827d55c6b6	Switch embeddings to index-offset. This is a special case of an embedding, but it has the nice property for checking inclusion.	2026-08-09 17:23:46 -05:00
Danila Fedorin	904f6375be	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>	2026-07-02 15:06:40 -05:00
Danila Fedorin	8cd053a242	Migrate Reaching.lean to projections via a generic Trace.steps Finish the projection migration for reaching definitions by replacing the accumulator-style runOfTrace*From definitions and their hand-rolled re-association lemmas with a single analysis-agnostic projection: Trace.steps / Traceₗ.steps, the chronological List of executed (index, statement) pairs. Its four simp lemmas are one-line inductions, with all re-association falling out of mathlib's List.append_assoc and List.reverse_append. Run is now an abbrev for List (State × BasicStmt) (latest-first, so LastAssign keeps its first-match structure) and runOfTrace is just steps.reverse. Also hoist the generic reaches_final_post into Forward.lean, letting analyze_correct' be stated directly about S.Post (prog.trace hrun). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-07-02 09:01:09 -05:00
Danila Fedorin	0e6976f9b4	Migrate most of the codebase (sans Reaching.lean / LICM left) to projections	2026-07-01 22:56:29 -05:00
Danila Fedorin	10b8fa97ca	Add left-and-right open traces to help formalization Co-Authored-By: OpenAI Codex <codex@openai.com>	2026-07-01 19:27:06 -05:00
Danila Fedorin	8ed48cf444	Add non-state parameterized 'Reaches' relation	2026-07-01 13:02:39 -05:00
Danila Fedorin	37d88f070a	Remove 'prog.code s = some bs' argument to `eval`	2026-06-30 23:21:00 -05:00
Danila Fedorin	6c05e401c1	Document Program.lean	2026-06-29 10:42:01 -05:00
Danila Fedorin	fe5098095a	Reorganize proofs to make 'Program' accessible to files in Language/	2026-06-29 10:41:40 -05:00
Danila Fedorin	59afbdaf71	Rename StateInterp to match the style of the rest of the codebase	2026-06-29 10:00:01 -05:00
Danila Fedorin	490c472d22	Start documenting FiniteMap.lean	2026-06-29 08:59:51 -05:00
Danila Fedorin	d1a11a9b2c	Use alpha and beta for FiniteMap type variables	2026-06-29 08:59:37 -05:00
Danila Fedorin	2598df690c	Slightly tweak AboveBelow proofs	2026-06-29 08:16:55 -05:00
Danila Fedorin	47d54f5b4b	Further simplify proofs in AboveBelow Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-06-28 15:01:24 -05:00
Danila Fedorin	8fa822b2e6	Improve performance by caching CFG building Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-06-28 14:39:14 -05:00
Danila Fedorin	d66a7d0e3e	Clean up and document AboveBelow	2026-06-28 14:38:12 -05:00
Danila Fedorin	778e974dfb	Prove that analysis results apply to all states, not just the final one Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-06-28 14:24:46 -05:00
Danila Fedorin	319fa272ac	Switch Reaching analysis to use Finset for more efficiency Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-06-28 09:46:54 -05:00