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 :=
+    VariableValues L prog := E.eval s (variablesAt s sv)
  evalStmtOrNone s (prog.code s) rfl (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
+    [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
-  step : (s : prog.State) → {ρ₁ ρ₂ : Env} → {bs : BasicStmt} →
+  valid : ∀ (s₁ s₂ : prog.State) {ρ₁ ρ₂ ρ₃: Env}
-    prog.code s = some bs → EvalBasicStmt ρ₁ bs ρ₂ → S.St ρ₁ → S.St ρ₂
+    {vs : VariableValues L prog},
-  valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} {bs : BasicStmt}
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) →
-    {vs : VariableValues L prog} {st : S.St ρ₁},
+    (hbs : EvalBasicStmtOpt ρ₂ (prog.cfg.nodes s₂) ρ₃) → ⟦ vs ⟧ (S.Pre tr) →
-    (hcode : prog.code s = some bs) → (hbs : EvalBasicStmt ρ₁ bs ρ₂) → ⟦ vs ⟧ ρ₁ st →
+    ⟦ E.eval s₂ vs ⟧ (S.Post (tr ++ hbs))
-    ⟦ E.eval s bs hcode vs ⟧ ρ₂ (step s hcode hbs st)
+  botV_init : ⟦ botV L prog ⟧ (S.Pre (Traceₗ.single prog.cfg prog.initialState []))
  botV_init : ⟦ botV L prog ⟧ [] S.init
 instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
    ValidStateEvaluator L prog where
-  step := by intro _ _ _ _ _ _ _; exact PUnit.unit
+  valid := by intro _ _ _ _ _ _ tr hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
  valid := by intro _ _ _ _ _ _ hcode hbs hvs; exact ValidStmtEvaluator.valid hcode hbs hvs
  botV_init := by intro k l _ v hmem; cases hmem
 section
-variable [S : StateInterp L prog] [V : ValidStateEvaluator L prog]
+variable [S : StateInterpretation 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)
 omit [DecidableEq L] in
-lemma evalStmtOrNone_valid {s : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
+lemma updateAll_matches {s₁ s₂ : prog.State} {sv : StateVariables L prog}
-    {vs : VariableValues L prog} (o : Option BasicStmt) (hco : prog.code s = o)
+    {ρ₁ ρ₂ ρ₃ : Env}
-    (he : EvalBasicStmtOpt ρ₁ o ρ₂) (hvs : ⟦ vs ⟧ ρ₁ st) :
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
-    ⟦ evalStmtOrNone s o hco vs ⟧ ρ₂ (stepStmtOrNone s o hco he st) := by
+    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃)
-  cases he with
+    (hvs : ⟦ variablesAt s₂ sv ⟧ (S.Pre tr)) :
-  | none => exact hvs
+    ⟦ variablesAt s₂ (updateAll sv) ⟧ (S.Post (tr ++ hnode)) := by
  | 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
  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 ρ₁}
+lemma stepTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
-    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st)
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
-    (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
+    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre tr))
-    ⟦ variablesAt s₁ (result L prog) ⟧ ρ₂ (stepNode s₁ hnode st) := by
+    (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 ρ₁}
+/-- Soundness propagates along an execution prefix: if the analysis is sound at
-    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁)
+    `s₂` for the run so far (`trₗ`), then it is sound wherever the further prefix
-    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
+    `mid` ends up. -/
-    ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ (stepTraceState tr st₁) := by
+lemma walkPrefix : ∀ {s₂ s : prog.State} {ρ₂ ρin : Env}
-  induction tr with
+    (mid : Traceₗ prog.cfg s₂ s ρ₂ ρin) {s₁ : prog.State} {ρ₁ : Env}
-  | single hnode => exact stepTrace hjoin hnode
+    (trₗ : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂),
-  | @edge _ ρ' _ i₁ i₂ _ hnode hedge _ ih =>
+    ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre trₗ) →
-    have hstep : ⟦ variablesAt i₁ (result L prog) ⟧ ρ' (stepNode i₁ hnode st₁) :=
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre (trₗ ++ mid)) := by
-      stepTrace hjoin hnode
+  intro s₂ s ρ₂ ρin mid
-    have hmem : variablesAt i₁ (result L prog)
+  induction mid with
-        ∈ (result L prog).valuesAt (prog.incoming i₂) :=
+  | nil => intro s₁ ρ₁ trₗ hjoin; simpa [HAppend.hAppend, Traceₗ.append] using hjoin
-      FiniteMap.mem_valuesAt prog.states_nodup
+  | cons hnode hedge rest ih =>
-        (prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog))
+      intro s₁ ρ₁ trₗ hjoin
-    exact ih (interp_foldr hstep hmem)
+      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 ρ) :
+/-- Soundness at every program point an execution actually visits: the analysis
-    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ
+    over-approximates both the environment entering that point and the one leaving
-      (stepTraceState (prog.trace hrun) S.init) := by
+    it. -/
-  refine walkTrace ?_ (prog.trace hrun)
+theorem analyze_correct_at {s : prog.State} {ρin ρout : Env} (hr : Reaches s ρin ρout) :
-  rw [joinForKey_initialState]
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre hr.pre)
-  exact ValidStateEvaluator.botV_init
+      ∧ ⟦ 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) ⟧ ρ () :=
+    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
-  analyze_correct_state L prog hrun
+  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) :
+lemma evalBasicStmt_mono (bs : BasicStmt) :
-    Monotone (evalBasicStmt (L := L) (prog := prog) s bs h) := by
+    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
+  simp [StmtEvaluator.eval, evalBasicStmtOpt]
-  cases hbs with
+  intro s vs ρ₁ ρ₂; generalize prog.code s = obs; intro hev hvs
-  | noop => exact hvs
+  rcases hev with _ | @⟨_,bs,hev⟩ <;> try simpa
-  | assign k e v hev =>
+  rcases hev with _ | @⟨k, e, v, hev⟩ <;> try simpa
-    intro k' l hk'l v' hv'
+  intros k' l' hkl' v' hρ
-    cases hv' with
+  rcases hρ with _ | ⟨_,_,_,_,_,hne,hmem⟩ <;> simp [evalBasicStmt] at hkl'
-    | here =>
+  · have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
-      have hk'l₀ : (k, l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
+        (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hkl'
-          (fun _ vs => E.eval e vs) [k] vs := hk'l
+    rewrite [hl]; simp
      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 hl := FiniteMap.generalizedUpdate_not_mem_backward
-      have hk'l₀ : (k', l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
+        (fun hmem => hne (List.mem_singleton.mp hmem)) hkl'
-          (fun _ vs => E.eval e vs) [k] vs := hk'l
+    apply hvs _ _ hl _ hmem
      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'
 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 →
+  eval : prog.State → VariableValues L prog → VariableValues L prog
-    VariableValues L prog → VariableValues L prog
+  eval_mono : ∀ s, Monotone (eval s)
  eval_mono : ∀ s bs h, Monotone (eval s bs h)
 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}
+  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env},
-    {bs : BasicStmt} (hcode : prog.code s = some bs),
+    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s vs ⟧ ρ₂
    EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s bs hcode 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
+class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
-  St : Env → Type
+  Proj : Type
-  init : St []
+  Pre : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
-  interp : VariableValues L prog → (ρ : Env) → St ρ → Prop
+  Post : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
  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
-instance [S : StateInterp L prog] :
+  interp : VariableValues L prog → (p : Proj) → Prop
-    Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → 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) :
+    {p : S.Proj} (hvs : ⟦ vs ⟧ p) (hmem : vs ∈ vss) :
-    ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ st := by
+    ⟦ 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
+instance : StateInterpretation L prog where
-  St := fun _ => PUnit
+  Proj := Env
-  init := PUnit.unit
+  Pre := fun {_ _ _ ρ₂} _ => ρ₂
-  interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs →
+  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.Finset
 import Spa.Lattice.Tuple
 import Spa.Language.Tagged.Graphs
 import Spa.Showable
 namespace Spa
 open Forward
-instance : Showable Bool := ⟨fun b => if b then "true" else "false"⟩
+instance {n : ℕ} : Showable (Finset (Fin n)) :=
-
+  ⟨fun s =>
 instance {n : ℕ} {β : Type*} [Showable β] : Showable (Fin n → β) :=
  ⟨fun f =>
    "{" ++ (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) :
+def eval (s : prog.State) (vs : VariableValues (DefSet prog) prog) : VariableValues (DefSet prog) prog :=
-    DefSet prog :=
+  match prog.code s with
-  Function.update (⊥ : DefSet prog) (prog.nodeIdOfNonempty s h) true
+  | none => vs
  | some bs =>
    match bs with
    | .assign k _ => FiniteMap.generalizedUpdate id (fun _ _ => {s}) [k] vs
    | .noop => vs
-def eval (s : prog.State) :
+lemma eval_mono (s : prog.State) :
-    (bs : BasicStmt) → prog.code s = some bs →
+    Monotone (eval prog s) := by
-    VariableValues (DefSet prog) prog → VariableValues (DefSet prog) prog
+  intros vs₁ vs₂ hle
-  | .assign k _, h, vs =>
+  unfold eval; split <;> try simpa
-    FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s h) [k] vs
+  split <;> try simpa
-  | .noop, _, vs => vs
+  apply FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
-
+  assumption
 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
 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
+/-- The statements a trace executed, paired with the state each executed at,
-  | nil : Run prog
+    most recent first (matching `LastAssign`, which scans for the most recent
-  | cons (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
+    assignment). This is `Trace.steps` (chronological) reversed, so facts about
-      (rest : Run prog) : Run prog
+    concatenating traces reduce to mathlib's `List.append`/`List.reverse` lemmas. -/
 abbrev Run (prog : Program) : Type := List (prog.State × BasicStmt)
@[aesop unsafe cases]
-inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId → Prop
+inductive LastAssign (prog : Program) (x : String) : Run prog → prog.State → Prop
-  | here (s : prog.State) (e : Expr) (hc : prog.code s = some (.assign x e))
+  | here (s : prog.State) (e : Expr) (rest : Run prog) :
-      (rest : Run prog) :
+      LastAssign prog x ((s, .assign x e) :: rest) s
      LastAssign prog x (Run.cons s (.assign x e) hc rest) (prog.nodeIdOfNonempty s hc)
  | 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
+def runOfTraceₗ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
-  St := fun _ => Run prog
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
-  init := Run.nil
+  tr.steps.reverse
-  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
 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 (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
+    intro s₁ s₂ ρ₁ ρ₂ ρ₃ vs tr hbs hvs
-    cases hbs with
+    show ⟦eval prog s₂ vs⟧ (runOfTrace prog (tr ++ hbs))
-    | noop => intro x assigners hmem n hla; aesop
+    simpa [runOfTrace, runOfTraceₗ] using valid_step prog s₂ rfl hbs hvs
    | 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
  botV_init := by intro x assigners _ n hla; cases hla
 theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
-    ⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧ ρ
+    ⟦ variablesAt prog.finalState (result (DefSet prog) prog) ⟧
-      (stepTraceState (prog.trace hrun) (stateInterp prog).init) :=
+      (runOfTrace prog (prog.trace hrun)) :=
-  Forward.analyze_correct_state (DefSet prog) prog hrun
+  Forward.analyze_correct' (DefSet prog) prog hrun
 theorem analyze_correct_at {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 z, _ => signOf z
  | .num (_ + 1), _ => .mk .plus
 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
+    exact interp_signOf n
    | zero => rfl
    | succ n' => exact ⟨n', congrArg Value.int (by norm_cast)⟩
  | 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 Spa.Language.Program
 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
--- 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`
+transformation. It's a very basic imperative language.
-file provides an auto-derived version of the `Expr`, `BasicStmt`, and `Stmt` data
+
-types with unique IDs per condtructor, enabling in-AST pointers.
+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
+    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
  | single hbs =>
    exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
      Fin.append_left])
  | edge hbs he _ ih =>
    refine Trace.edge ?_ ?_ ih
    · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
    · exact List.mem_append_left _ (List.mem_map_of_mem _ he)
 /-- When two graphs are overlaid, for each trace in the right graph,
    a corresponding trace exists in the combined graph. -/
 noncomputable def Trace.overlay_right {idx₁ idx₂ : g₂.Index}
    (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
+    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.overlayRight g₁ g₂)
  | single hbs =>
    exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
      Fin.append_right])
  | edge hbs he _ ih =>
    refine Trace.edge ?_ ?_ ih
    · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
    · exact List.mem_append_right _ (List.mem_map_of_mem _ he)
 /-- When two graphs are sequenced, for each trace in the first graph,
    a corresponding trace exists in the combined graph. -/
 noncomputable def Trace.sequence_left {idx₁ idx₂ : g₁.Index}
    (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
+    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
  | single hbs =>
    exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
      Fin.append_left])
  | edge hbs he _ ih =>
    refine Trace.edge ?_ ?_ ih
    · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
    · exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
 /-- When two graphs are sequenced, for each trace in the second graph,
   a corresponding trace exists in the combined graph. -/
 noncomputable def Trace.sequence_right {idx₁ idx₂ : g₂.Index}
    (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
-    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
+    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.sequenceRight g₁ g₂)
  | single hbs =>
    exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
      Fin.append_right])
  | edge hbs he _ ih =>
    refine Trace.edge ?_ ?_ ih
    · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
    · exact List.mem_append_left _
        (List.mem_append_right _ (List.mem_map_of_mem _ he))
 /-- Equivalent of `Trace.overlay_left` for end-to-end traces. -/
 noncomputable def EndToEndTrace.overlay_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
@@ -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
+    Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ :=
-  induction tr with
+  tr.embed (GGraph.Embed.loop g)
  | single hbs =>
    exact Trace.single (by
      rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => none) g.nodes from rfl,
        Fin.append_right])
  | edge hbs he _ ih =>
    refine Trace.edge ?_ ?_ ih
    · rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => none) g.nodes from rfl,
        Fin.append_right]
    · exact List.mem_append_left _ (List.mem_append_left _
        (List.mem_append_left _ (List.mem_map_of_mem _ he)))
 /-- The beginning node of a loop graph is empty. -/
 private lemma loop_nodes_at_in :
@@ -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`. -/
+namespace Program
 def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
  (0 : Fin 1).castAdd ((g ⤳ Graph.singleton none).size)
-/-- The output / exit node generated by `Graph.wrap`. -/
+noncomputable def trace (p : Program) {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
-def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
+    Trace p.cfg p.initialState p.finalState [] ρ := by
-  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
+  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`. -/
+end Program
 lemma Graph.wrap_inputs (g : Graph) :
    (Graph.wrap g).inputs = [g.wrapInput] := rfl
 /-- 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
+    Trace g idx₁ idx₄ ρ₁ ρ₃ :=
-  induction tr₁ with
+  match tr₁ with
-  | single hbs => exact Trace.edge hbs he tr₂
+  | single hbs => edge hbs he tr₂
-  | edge hbs he' _ ih => exact Trace.edge hbs he' (ih 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
+protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by aesop
-  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 sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
+protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by aesop
-  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 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 :=
+lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lt_of_le_of_ne (bot_le' _) (by simp)
-  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 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
+  rw [le_iff] at h
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp_all
  · 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)
-/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to
+/-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤`
-`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is
+    (against any non-`⊥` argument), it is monotone in both arguments.
-monotone in both arguments — regardless of its values on plain elements.
+    The values of the the elements in `α` are irrelevant since they
-`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
+    are always incomparable. This makes it easy to prove monotonicity
-monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
+    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
+  constructor <;> intro c a b hab <;>
-  · intro y a b hab
+    rcases eq_or_ne c bot with rfl | hc <;>
-    show f a y ≤ f b y
+    rcases le_cases hab with rfl | rfl | rfl <;>
-    rcases le_cases hab with rfl | rfl | rfl
+    simp [hbotl, hbotr, htopl, htopr, bot_le', le_top', *]
    · 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 -/
 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
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by aesop
  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
 /-- 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
+  rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> simp_all
  · 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
+  · exact h.2
-      · next hne => exact absurd h (hdisj hne v)
+  · 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
+/-- synthetic rank of an element, used to prove chain bounds. -/
-(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
+private def rank : AboveBelow α → ℕ
 def rank : AboveBelow α → ℕ
  | bot => 0
  | mk _ => 1
  | top => 2
-/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
+/-- It's not possible for any two lifted flat-domain elements to be less
-`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
+    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
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
-  · exact absurd hab (lt_irrefl _)
+    simp_all [rank, not_mk_lt_mk, (bot_le' _).not_lt, (le_top' _).not_lt]
  · 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)
 /-- 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) :=
+instance [Lattice β] : Lattice (FiniteMap α β ks) :=
-  inferInstanceAs (Lattice (Fin ks.length → B))
+  inferInstanceAs (Lattice (Fin ks.length → β))
-instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
+instance [FiniteHeightLattice β] : FiniteHeightLattice (FiniteMap α β ks) :=
-  inferInstanceAs (FiniteHeightLattice (Fin ks.length → B))
+  inferInstanceAs (FiniteHeightLattice (Fin ks.length → β))
-instance [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
+instance [DecidableEq β] : DecidableEq (FiniteMap α β ks) :=
-  inferInstanceAs (DecidableEq (Fin ks.length → B))
+  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) :
+def locate {k : α} {fm : FiniteMap α β ks} (h : MemKey k fm) :
-    {v : B // (k, v) ∈ 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}
+lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap α β ks}
-    (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
+    (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
+omit [Lattice β] in
-lemma eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
+lemma eq_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
-    {ks' : List A} {g : A → B} (hk : k ∈ 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
+omit [Lattice β] in
-lemma mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
+lemma mem_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
-    {ks' : List A} {g : A → B} (hk : k ∉ 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}
+lemma updating_mono {fm₁ fm₂ : FiniteMap α β ks} {ks' : List α}
-    {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
+    {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)
+def generalizedUpdate (f : L → FiniteMap α β ks) (g : α → L → β)
-    (ks' : List A) : L → FiniteMap A B ks := fun 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
+omit [Lattice β] [Lattice L] in
-lemma generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
+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
+omit [Lattice β] [Lattice L] in
-lemma generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+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
+omit [Lattice β] in
-lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
+lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap α β ks} {k : α} {v : β}
-    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
+    {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₂)
+lemma valuesAt_le {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂)
-    (ks' : List A) :
+    (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,23 +1,27 @@
 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`
+to the AST to *find* — not yet move — assignments inside a `while` loop whose
-loop whose right-hand side depends only on definitions made *outside* the loop.
+right-hand side depends only on definitions made *outside* the loop. These are
-These are the candidates a later LICM pass could hoist.
+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`);
+1. at an assignment, its CFG state is `Embed.singletonIndex` — the subtree's CFG
-2. read the reaching definitions at the assignment's *entry*
+   is a `singleton`, so its sole node is the state, and `nodes_eq` proves it
-   (`joinForKey s result` — the join over predecessors, i.e. before the
+   holds that very statement;
-   assignment itself runs);
+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
+4. check no definition site lies in the loop body's CFG range. Every embedding is
-   it is **not** inside the loop body (structural `subtreeIds` membership).
+   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
@@ -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). -/
+  /-- The enclosing loop. -/
-  loopId : prog.NodeId
+  encl : Enclosing prog
-  /-- Every node id inside the loop body (the "is-child-of-loop" set). -/
+  /-- The assignment's CFG state. -/
-  bodyIds : List prog.NodeId
+  assignState : prog.State
  /-- The assignment `BasicStmt`'s tag — what labels its CFG node. -/
  assignId : prog.NodeId
  /-- 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
+`enc` is `none` outside any loop, in which case assignments are skipped — only
-loop (in which case assignments are skipped — only in-loop assignments are
+in-loop assignments are candidates. -/
-candidates). -/
+def collectCandidates (prog : Program) (enc : Option (Enclosing prog)) :
-def collectCandidates (prog : Program) (enc : Option (prog.NodeId × List prog.NodeId)) :
+    (s : Stmt) → Embed s.cfg prog.cfg → List (Candidate prog)
-    Stmt.Tagged prog.NodeId → List (Candidate prog)
+  | .basic bs, e =>
  | .basic _ bs =>
      match bs, enc with
-      | .assign t _ e, some (loopId, bodyIds) =>
+      | .assign _ ex, some l =>
-          [{ loopId := loopId, bodyIds := bodyIds, assignId := t,
+          [{ encl := l, assignState := e.singletonIndex,
-             rhsVars := e.erase.vars.sort (· ≤ ·) }]
+             rhsVars := ex.vars.sort (· ≤ ·) }]
      | _, _ => []
-  | .andThen _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
+  | .andThen s₁ s₂, e =>
-  | .ifElse _ _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
+      collectCandidates prog enc s₁ ((Embed.sequenceLeft s₁.cfg s₂.cfg).trans e) ++
-  | .whileLoop loopT _ body =>
+      collectCandidates prog enc s₂ ((Embed.sequenceRight s₁.cfg s₂.cfg).trans e)
-      collectCandidates prog (some (loopT, body.subtreeIds)) body
+  | .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
+its RHS variables lie outside the loop body? -/
 node id, so we compare against the loop-body ids directly (embedding the raw
 body ids into `p.NodeId`). -/
 def isInvariant (prog : Program) (c : Candidate prog) : Bool :=
-  match prog.stateOfNodeId c.assignId with
+  let entry := joinForKey c.assignState (result (DefSet prog) prog)
  | 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))
+  -- `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. -/
+/-- The loop-invariant assignments of `prog`, as `(loop, assignment)` state pairs. -/
-def licmCandidates (prog : Program) : List (prog.NodeId × prog.NodeId) :=
+def licmCandidates (prog : Program) : List (prog.State × prog.State) :=
-  (collectCandidates prog none prog.taggedFin).filterMap (fun c =>
+  (collectCandidates prog none prog.rootStmt prog.rootEmbed).filterMap (fun c =>
-    if isInvariant prog c then some (c.loopId, c.assignId) else none)
+    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