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>

.claude/settings.json

@@ -0,0 +1,9 @@
+{
+  "permissions": {
+    "allow": [
+      "Bash(lake build)",
+      "Bash(lake build *)",
+      "Bash(export PATH=\"$HOME/.elan/bin:$PATH\")"
+    ]
+  }
+}

Equivalence.agda

@@ -2,7 +2,7 @@ module Equivalence where
 
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Relation.Binary.Definitions
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans)
 
 module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
     IsReflexive : Set a
@@ -19,3 +19,10 @@ module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
             ≈-refl : IsReflexive
             ≈-sym : IsSymmetric
             ≈-trans : IsTransitive
+
+isEquivalence-≡ : ∀ {a} {A : Set a} → IsEquivalence A _≡_
+isEquivalence-≡ = record
+    { ≈-refl = refl
+    ; ≈-sym = sym
+    ; ≈-trans = trans
+    }

LEAN_MIGRATION.md

@@ -0,0 +1,117 @@
+# Agda → Lean 4 (mathlib) migration plan
+
+Goal: port the static-analysis framework to Lean 4 + mathlib, preserving the
+overall structure and **the same theorems/lemmas** (modulo language details),
+while lifting custom machinery into mathlib wherever a standard counterpart
+exists. Per discussion, the setoid equality (`_≈_`) is **dropped in favor of
+propositional `=`** — it existed mainly so that unordered key-value maps could
+be "equal"; representations below are chosen to be canonical so `=` works.
+
+The Lean project lives in `lean/` (library root `Spa`). Each phase ends with a
+green `lake build` and a correspondence table appended to this file, so you can
+validate phase by phase.
+
+## Design mapping
+
+| Agda | Lean | Notes |
+|---|---|---|
+| `Equivalence.agda` | *lifted*: `Eq`, `Equivalence` | module disappears |
+| `IsDecidable` | *lifted*: `DecidableEq` / `DecidableRel` | mathlib is classical; decidability kept only where functions compute (e.g. the fixpoint iteration) |
+| `Showable.agda` | *lifted*: `ToString` | |
+| `Lattice.agda` `IsSemilattice` (`⊔-assoc/comm/idemp`, `≼`, `≼-refl/trans/antisym`, `x≼x⊔y`, `⊔-Monotonicˡ/ʳ`) | *lifted*: `SemilatticeSup` (`sup_assoc`, `sup_comm`, `sup_idem`, `≤` with `sup_eq_right`, `le_refl`, `le_trans`, `le_antisymm`, `le_sup_left`, `sup_le_sup_left/right`) | `a ≼ b := a ⊔ b ≈ b` becomes `a ≤ b` with bridge lemma `sup_eq_right` |
+| `IsLattice` (`absorb-⊔-⊓`, `absorb-⊓-⊔`) | *lifted*: `Lattice` (`sup_inf_self`, `inf_sup_self`) | |
+| `Monotonic`, `Monotonicˡ/ʳ/₂` | *lifted*: `Monotone` (+ tiny aliases) | |
+| `foldr-Mono`, `foldl-Mono`, `foldr-Mono'`, `foldl-Mono'` | custom, `Spa/Lattice.lean` | stated with `List.Forall₂` (≙ `Utils.Pairwise`) |
+| `Chain.agda` (`Chain`, `concat`, `Chain-map` in `ChainMapping`) | *lifted*: `LTSeries` (`RelSeries.smash`, `LTSeries.map` + `Monotone.strictMono_of_injective`) | with `=`, the ≈-congruence steps in chains vanish |
+| `Chain.Height`, `Bounded`, `Bounded-suc-n` | custom: `Spa.FixedHeight` structure (`⊥`, `⊤`, longest `LTSeries`, `bounded`) | |
+| `IsFiniteHeightLattice`, `FiniteHeightLattice` | custom class `Spa.FiniteHeightLattice` | |
+| `⊥≼` (chain bottom is least, given decidable eq) | custom, same proof shape (prepend `⊥⊓a ≺ ⊥` to longest chain) | decidability hypothesis dropped (classical) |
+| `Fixedpoint.agda` (`doStep` with gas, `aᶠ`, `aᶠ≈faᶠ`, `aᶠ≼`) | custom, `Spa/Fixedpoint.lean`, same gas-based algorithm | **not** replaced by mathlib `lfp` (would change the proof approach and lose computability) |
+| `Isomorphism.agda` (`TransportFiniteHeight`) | custom, `Spa/Isomorphism.lean` | much smaller: with `=`, f/g monotone inverse pair transports `FixedHeight` via `LTSeries.map` |
+| `Lattice/Unit.agda` | *lifted*: mathlib `Lattice PUnit`; custom `FixedHeight PUnit 0` | |
+| `Lattice/Nat.agda` (max/min lattice) | *lifted*: mathlib `Lattice ℕ` (`Nat.instLattice`) | kept only as a remark; file had no fixed-height content |
+| `Lattice/Prod.agda` | instance *lifted* (`Prod.instLattice`); custom: `unzip` + `FixedHeight (A×B) (h₁+h₂)` | same proof: split a product chain into component chains |
+| `Lattice/AboveBelow.agda` (flat lattice ⊥/[x]/⊤) | custom, same datatype; `Plain` module ⇒ `FixedHeight 2` | mathlib has no flat-lattice-on-discrete-type |
+| `Lattice/ExtendBelow.agda` | *lifted*: `WithBot A` lattice instance; custom `FixedHeight (h+1)` | unused by the pipeline; ported for parity (optional) |
+| `Lattice/IterProd.agda` | custom, same induction (`IterProd k = A × … × B`), lattice + height-sum by recursion | the `Everything` record trick survives as a recursive definition of bundled instances |
+| `Lattice/Map.agda` (assoc list with `Unique` keys, setoid) | **deleted**: only existed to support setoid map equality | its consumers move to `Finset` / spine-fixed `FiniteMap` |
+| `Lattice/MapSet.agda` (`StringSet`) | *lifted*: `Finset String` (`∪`, `{·}`, `∅`, `.toList`, `nodup_toList`) | |
+| `Lattice/FiniteMap.agda` | custom: `{ l : List (A × B) // l.map Prod.fst = ks }` — key spine fixed ⇒ `=` is pointwise value equality | same API: `locate`, `_[_]`, `GeneralizedUpdate` (`f'`, `f'-Monotonic`, `f'-k∈ks-≡`, `f'-k∉ks-backward`), `m₁≼m₂⇒m₁[k]≼m₂[k]`, `Provenance-union` analog; fixed height **still via isomorphism to `IterProd`** (same approach) |
+| `Lattice/Builder.agda` | **skipped** — not imported by anything in the repo | flag if you want it |
+| `Utils.agda` | *lifted*: `Unique`→`List.Nodup`, `Pairwise`→`List.Forall₂`, `fins`→`List.finRange`, `∈-cartesianProduct`→`List.product`/`pair_mem_product`, `x∈xs⇒fx∈fxs`→`List.mem_map_of_mem`, `filter-++`→`List.filter_append`, `iterate`→`f^[n]`, `concat-∈`→`List.mem_join`, `All¬-¬Any` etc. → `List.All`/`Any` API | leftovers (if any) in `Spa/Utils.lean` |
+| `Language/Base.agda` | custom; `Expr-vars`/`Stmt-vars : Finset String` | commented-out `∈-vars` lemmas stay omitted |
+| `Language/Semantics.agda` | custom, same big-step relations; `Value`, `Env = List (String × Value)`, custom `∈` | `ℤ` → `Int` |
+| `Language/Graphs.agda` | custom; `Vec` → `Vector` (mathlib `List.Vector`), `Fin._↑ˡ/_↑ʳ` → `Fin.castAdd`/`Fin.natAdd` | same `Graph` record, `∙`/`↦`/`loop`/`skipto`/`singleton`/`wrap`/`buildCfg`, `predecessors` + edge lemmas |
+| `Language/Traces.agda` | custom, same `Trace`/`EndToEndTrace`/`++⟨_⟩` | |
+| `Language/Properties.agda` | custom, same lemma inventory (`Trace-∙ˡ/ʳ`, `Trace-↦ˡ/ʳ`, `Trace-loop`, `EndToEndTrace-*`, `wrap-preds-∅`, `buildCfg-sufficient`) | the "ugly" `↑-≢` Fin-disjointness block should shrink via `Fin.castAdd_ne_natAdd`-style mathlib lemmas |
+| `Language.agda` (`Program` record) | custom, same fields/lemmas (`trace`, `vars`, `states`, `incoming`, `initialState-pred-∅`, …) | |
+| `Analysis/Forward/{Lattices,Evaluation,Adapters}.agda`, `Analysis/Forward.agda` | custom, same structure: `VariableValues`, `StateVariables`, `joinForKey`/`joinAll`, `StmtEvaluator`/`ExprEvaluator` + validity, expr→stmt adapter, `analyze`, `result`, `analyze-correct` | section variables instead of parameterized modules; everything Agda passed as an instance argument (`IsFiniteHeightLattice`, the evaluators, `LatticeInterpretation`, the validity records) is a typeclass resolved by instance search |
+| `Analysis/Sign.agda`, `Analysis/Constant.agda` | custom, same definitions | the four monotonicity **postulates** become real proofs (any `⊥`-strict/`⊤`-dominating operation on a flat lattice is monotone: `AboveBelow.monotone₂_of_strict`) |
+| `Main.agda` | `lake exe spa` | same test programs, same printed output |
+
+## Phases & checkpoints
+
+- **Phase 0 — scaffold.** `lean/` lake project, mathlib pinned to toolchain
+  v4.17.0 (already installed). ✅ checkpoint: `lake build` green on empty lib.
+- **Phase 1 — core order theory.** `Spa/Lattice.lean` (Monotone aliases, fold
+  monotonicity, `FixedHeight`, `Bounded`, `FiniteHeightLattice`, chain-bottom-
+  is-least). ✅ checkpoint: build + table below.
+- **Phase 2 — fixpoint & transport.** `Spa/Fixedpoint.lean`,
+  `Spa/Isomorphism.lean`. ✅ checkpoint: `fix`, `fix_eq`, `fix_le`,
+  `TransportFiniteHeight`.
+- **Phase 3 — basic lattice instances.** Unit, Prod (+height), AboveBelow
+  (+`Plain`, height 2), ExtendBelow. ✅ checkpoint.
+- **Phase 4 — map lattices.** IterProd, FiniteMap (+fixed height via IterProd
+  isomorphism), MapSet→`Finset` shims. ✅ checkpoint.
+- **Phase 5 — language.** Base, Semantics, Graphs, Traces, Properties,
+  `Program`. ✅ checkpoint: `buildCfg_sufficient`, `Program.trace`.
+- **Phase 6 — forward analysis framework.** Lattices/Evaluation/Adapters/
+  Forward. ✅ checkpoint: `analyze_correct`.
+- **Phase 7 — concrete analyses + executable.** Sign, Constant, Main.
+  ✅ checkpoint: `lake exe spa` output vs Agda `Main` output; postulates now
+  proved.
+
+## Status
+
+- [x] Phase 0
+- [x] Phase 1
+- [x] Phase 2
+- [x] Phase 3
+- [x] Phase 4
+- [x] Phase 5
+- [x] Phase 6
+- [x] Phase 7
+
+All phases complete: `lake build` is green with zero warnings, zero `sorry`s
+and zero axioms, and `lake exe spa` prints output **byte-for-byte identical**
+to the compiled Agda `Main` (verified with `diff`). Per-file `Agda ↦ Lean`
+correspondence tables live in the header comment of each Lean file.
+
+## Wins from the migration
+
+- The four monotonicity **postulates** in `Analysis/Sign.agda` and
+  `Analysis/Constant.agda` are now proved theorems (via
+  `AboveBelow.monotone₂_of_strict`: any operation on the flat lattice that
+  is strict in `⊥` and dominated by `⊤` is monotone, whatever its table),
+  so the Lean development is postulate-free.
+- ~2200 lines of map machinery (`Lattice/Map.agda`, `Lattice/MapSet.agda`,
+  much of `Lattice/FiniteMap.agda`) collapse into the spine-pinned
+  `FiniteMap` + `Finset`; the `IterProd` isomorphism no longer needs
+  `Unique ks` (the representation is canonical).
+- `Equivalence.agda`, `Chain.agda`, the `IsSemilattice`/`IsLattice`
+  hierarchy, and most of `Utils.agda` lift into mathlib.
+
+## Deviations & deferred items
+
+- `Lattice/Builder.agda`: not ported (nothing in the repo imports it).
+- `Lattice/ExtendBelow.agda`, `Lattice/Nat.agda`: not ported (unused by the
+  pipeline; `Nat`'s lattice is mathlib's, `ExtendBelow` would be `WithBot` +
+  a small height proof). Say the word if you want them for parity.
+- `Program.vars` lists variables in **sorted** order (`Finset.sort`, since
+  `Finset.toList` is noncomputable). For the test program this coincides
+  with the Agda MapSet order.
+- Chains are mathlib `LTSeries`, so chain-manipulating proofs
+  (`Prod` `unzip`, `AboveBelow`'s `isLongest` → a `rank`-based bound) are
+  restated against that API rather than pattern-matching a custom `Chain`
+  inductive.
+- `Trace`/`EndToEndTrace` are `Prop`-valued and destructured in proofs.

Language/Graphs.agda

@@ -18,7 +18,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl;
 open import Relation.Nullary using (¬_)
 
 open import Lattice
-open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
+open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct; fins; fins-complete)
 
 record Graph : Set where
     constructor MkGraph
@@ -124,28 +124,6 @@ buildCfg (s₁ then s₂) = buildCfg s₁ ↦ buildCfg s₂
 buildCfg (if _ then s₁ else s₂) = buildCfg s₁ ∙ buildCfg s₂
 buildCfg (while _ repeat s) = loop (buildCfg s)
 
-private
-    z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (zero ≡ suc f)
-    z≢sf f ()
-
-    z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (List.map suc fs)
-    z≢mapsfs [] = []
-    z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
-
-    finValues : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
-    finValues 0 = ([] , Utils.empty)
-    finValues (suc n') =
-        let
-            (inds' , unids') = finValues n'
-        in
-            ( zero ∷ List.map suc inds'
-            , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
-            )
-
-    finValues-complete : ∀ (n : ℕ) (f : Fin n) → f ListMem.∈ (proj₁ (finValues n))
-    finValues-complete (suc n') zero = RelAny.here refl
-    finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
-
 module _ (g : Graph) where
     open import Data.Product.Properties as ProdProp using ()
     private _≟_ = ProdProp.≡-dec (FinProp._≟_ {Graph.size g})
@@ -154,13 +132,13 @@ module _ (g : Graph) where
     open import Data.List.Membership.DecPropositional (_≟_) using (_∈?_)
 
     indices : List (Graph.Index g)
-    indices = proj₁ (finValues (Graph.size g))
+    indices = proj₁ (fins (Graph.size g))
 
     indices-complete : ∀ (idx : (Graph.Index g)) → idx ListMem.∈ indices
-    indices-complete = finValues-complete (Graph.size g)
+    indices-complete = fins-complete (Graph.size g)
 
     indices-Unique : Unique indices
-    indices-Unique = proj₂ (finValues (Graph.size g))
+    indices-Unique = proj₂ (fins (Graph.size g))
 
     predecessors : (Graph.Index g) → List (Graph.Index g)
     predecessors idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges g)) indices

Lattice.agda

@@ -96,6 +96,12 @@ record IsSemilattice {a} (A : Set a)
                     (a₁ ⊔ a) ⊔ (a₂ ⊔ a)
                 ∎
 
+    -- need to show: a₁ ⊔ (a₁ ⊔ a₂) ≈ a₁ ⊔ a₂
+    -- (a₁ ⊔ a₁) ⊔ a₂ ≈ a₁ ⊔ (a₁ ⊔ a₂)
+
+    x≼x⊔y : ∀ (a₁ a₂ : A) → a₁ ≼ (a₁ ⊔ a₂)
+    x≼x⊔y a₁ a₂ = ≈-sym (≈-trans (≈-⊔-cong (≈-sym (⊔-idemp a₁)) (≈-refl {a₂})) (⊔-assoc a₁ a₁ a₂))
+
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
@@ -113,6 +119,18 @@ record IsSemilattice {a} (A : Set a)
             a₃
         ∎
 
+    ≼-antisym : ∀ {a₁ a₂ : A} → a₁ ≼ a₂ → a₂ ≼ a₁ → a₁ ≈ a₂
+    ≼-antisym {a₁} {a₂} a₁⊔a₂≈a₂ a₂⊔a₁≈a₁ =
+        begin
+            a₁
+        ∼⟨ ≈-sym a₂⊔a₁≈a₁ ⟩
+            a₂ ⊔ a₁
+        ∼⟨ ⊔-comm _ _ ⟩
+            a₁ ⊔ a₂
+        ∼⟨ a₁⊔a₂≈a₂ ⟩
+            a₂
+        ∎
+
     ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
     ≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
         begin
@@ -237,16 +255,25 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         {{fixedHeight}} : FixedHeight h
 
+    private
+        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
+
+    open MyChain.Height fixedHeight using (⊥; ⊤) public
+
+    Known-⊥ : Set a
+    Known-⊥ = ∀ (a : A) → ⊥ ≼ a
+
+    Known-⊤ : Set a
+    Known-⊤ = ∀ (a : A) → a ≼ ⊤
+
     -- If the equality is decidable, we can prove that the top and bottom
     -- elements of the chain are least and greatest elements of the lattice
     module _ {{≈-Decidable : IsDecidable _≈_}} where
         open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
 
-        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
-        open MyChain.Height fixedHeight using (⊥; ⊤) public
         open MyChain.Height fixedHeight using (bounded; longestChain)
 
-        ⊥≼ : ∀ (a : A) → ⊥ ≼ a
+        ⊥≼ : Known-⊥
         ⊥≼ a with ≈-dec a ⊥
         ...   | yes a≈⊥ = ≼-cong a≈⊥ ≈-refl (≼-refl a)
         ...   | no a̷≈⊥ with ≈-dec ⊥ (a ⊓ ⊥)

Utils.agda

@@ -1,19 +1,32 @@
 module Utils where
 
 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
-open import Data.Product as Prod using (_×_)
+open import Data.Product as Prod using (Σ; _×_; _,_; proj₁; proj₂)
+open import Data.Empty using (⊥-elim)
 open import Data.Nat using (ℕ; suc)
+open import Data.Fin as Fin using (Fin; suc; zero)
+open import Data.Fin.Properties using (suc-injective)
 open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; filter) renaming (map to mapˡ)
-open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Membership.Propositional using (_∈_; lose)
 open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
-open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
-open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
+open import Data.List.Relation.Unary.All using (All; []; _∷_; map; all?; lookup)
+open import Data.List.Relation.Unary.All.Properties using (++⁻ˡ; ++⁻ʳ)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there; any?) -- TODO: re-export these with nicer names from map
 open import Data.Sum using (_⊎_)
 open import Function.Definitions using (Injective)
+open import Relation.Binary using (Antisymmetric) renaming (Decidable to Decidable²)
 open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong)
-open import Relation.Nullary using (¬_; yes; no)
+open import Relation.Nullary using (¬_; yes; no; Dec)
+open import Relation.Nullary.Decidable using (¬?)
 open import Relation.Unary using (Decidable)
 
+All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
+All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
+All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+
+Decidable-¬ : ∀ {p c} {C : Set c} {P : C → Set p} → Decidable P → Decidable (λ x → ¬ P x)
+Decidable-¬ Decidable-P x = ¬? (Decidable-P x)
+
 data Unique {c} {C : Set c} : List C → Set c where
     empty : Unique []
     push : ∀ {x : C} {xs : List C}
@@ -34,6 +47,24 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
         help {[]} _ = x'≢x ∷ []
         help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
 
+Unique-++⁻ˡ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique xs
+Unique-++⁻ˡ [] Unique-ys = empty
+Unique-++⁻ˡ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = push (++⁻ˡ xs {ys = ys} x≢xs++ys) (Unique-++⁻ˡ xs Unique-xs++ys)
+
+Unique-++⁻ʳ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique ys
+Unique-++⁻ʳ [] Unique-ys = Unique-ys
+Unique-++⁻ʳ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = Unique-++⁻ʳ xs Unique-xs++ys
+
+Unique-∈-++ˡ : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} →  Unique (xs ++ ys) → x ∈ xs → ¬ x ∈ ys
+Unique-∈-++ˡ [] _ ()
+Unique-∈-++ˡ {x = x} (x' ∷ xs) (push x≢xs++ys _) (here refl) = All¬-¬Any (++⁻ʳ xs x≢xs++ys)
+Unique-∈-++ˡ {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-∈-++ˡ xs Unique-xs++ys x̷∈xs
+
+Unique-narrow : ∀ {c} {C : Set c} {x : C} (xs : List C) {ys : List C} →  Unique (xs ++ ys) → x ∈ xs →  Unique (x ∷ ys)
+Unique-narrow [] _ ()
+Unique-narrow {x = x} (x' ∷ xs) (push x≢xs++ys Unique-xs++ys) (here refl) = push (++⁻ʳ xs x≢xs++ys) (Unique-++⁻ʳ xs Unique-xs++ys)
+Unique-narrow {x = x} (x' ∷ xs) (push _ Unique-xs++ys) (there x̷∈xs) = Unique-narrow xs Unique-xs++ys x̷∈xs
+
 All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
             Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
             All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
@@ -46,9 +77,8 @@ Unique-map : ∀ {c d} {C : Set c} {D : Set d} {l : List C} (f : C → D) →
 Unique-map {l = []} _ _ _ = empty
 Unique-map {l = x ∷ xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)
 
-All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
-All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
-All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
+¬Any-map : ∀ {p₁ p₂ c} {C : Set c} {P₁ : C → Set p₁} {P₂ : C → Set p₂} {l : List C} → (∀ {x} → P₁ x → P₂ x) → ¬ Any P₂ l → ¬ Any P₁ l
+¬Any-map f ¬Any-P₂ Any-P₁ = ¬Any-P₂ (Any.map f Any-P₁)
 
 All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
 All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
@@ -106,3 +136,42 @@ _∧_ P Q a = P a × Q a
 
 it : ∀ {a} {A : Set a} {{_ : A}} → A
 it {{x}} = x
+
+z≢sf : ∀ {n : ℕ} (f : Fin n) → ¬ (Fin.zero ≡ Fin.suc f)
+z≢sf f ()
+
+z≢mapsfs : ∀ {n : ℕ} (fs : List (Fin n)) → All (λ sf → ¬ zero ≡ sf) (mapˡ suc fs)
+z≢mapsfs [] = []
+z≢mapsfs (f ∷ fs') = z≢sf f ∷ z≢mapsfs fs'
+
+fins : ∀ (n : ℕ) → Σ (List (Fin n)) Unique
+fins 0 = ([] , empty)
+fins (suc n') =
+    let
+        (inds' , unids') = fins n'
+    in
+        ( zero ∷ mapˡ suc inds'
+        , push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
+        )
+
+fins-complete : ∀ (n : ℕ) (f : Fin n) → f ∈ (proj₁ (fins n))
+fins-complete (suc n') zero = here refl
+fins-complete (suc n') (suc f') = there (x∈xs⇒fx∈fxs suc (fins-complete n' f'))
+
+findUniversal : ∀ {p c} {C : Set c} {R : C → C → Set p} (l : List C) →  Decidable² R →
+                Dec (Any (λ x → All (R x) l) l)
+findUniversal l Rdec = any? (λ x → all? (Rdec x) l) l
+
+findUniversal-unique : ∀ {p c} {C : Set c} (R : C → C → Set p) (l : List C) →
+                       Antisymmetric _≡_ R →
+                       ∀ x₁ x₂ → x₁ ∈ l → x₂ ∈ l → All (R x₁) l → All (R x₂) l →
+                       x₁ ≡ x₂
+findUniversal-unique R l Rantisym x₁ x₂ x₁∈l x₂∈l Allx₁ Allx₂ = Rantisym (lookup Allx₁ x₂∈l) (lookup Allx₂ x₁∈l)
+
+x∷xs≢[] : ∀ {a} {A : Set a} (x : A) (xs : List A) → ¬ (x ∷ xs ≡ [])
+x∷xs≢[] x xs ()
+
+foldr₁ : ∀ {a} {A : Set a} {l : List A} → ¬ (l ≡ []) → (A → A → A) → A
+foldr₁ {l = x ∷ []} _ _ = x
+foldr₁ {l = x ∷ x' ∷ xs} _ f = f x (foldr₁ {l = x' ∷ xs} (x∷xs≢[] x' xs) f)
+foldr₁ {l = []} l≢[] _ = ⊥-elim (l≢[] refl)

lean/.gitignore

@@ -0,0 +1 @@
+.lake/

lean/Main.lean

@@ -0,0 +1,37 @@
+import Spa.Analysis.Sign
+import Spa.Analysis.Constant
+import Spa.Analysis.Reaching
+import Spa.Language.Notation
+
+namespace Spa
+
+def testCode : Stmt := [obj_stmt|
+  zero    := 0;
+  pos     := zero + 1;
+  neg     := zero - 1;
+  unknown := pos + neg
+]
+
+def testCodeCond₁ : Stmt := [obj_stmt|
+  var := 1;
+  if var {
+    var := var + 1
+  } else {
+    var := var - 1;
+    var := 1
+  }
+]
+
+def testCodeCond₂ : Stmt := [obj_stmt|
+  var := 1;
+  if var { x := 1 } else { noop }
+]
+
+def testProgram : Program := { rootStmt := testCode }
+
+end Spa
+
+def main : IO Unit :=
+  IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
+              Spa.SignAnalysis.output Spa.testProgram ++ "\n" ++
+              Spa.ReachingAnalysis.output Spa.testProgram)

lean/Spa.lean

@@ -0,0 +1,28 @@
+import Spa.Lattice
+import Spa.Fixedpoint
+import Spa.Lattice.Unit
+import Spa.Lattice.AboveBelow
+import Spa.Lattice.FiniteMap
+import Spa.Lattice.Bool
+import Spa.Language.Base
+import Spa.Language.Notation
+import Spa.Language.Semantics
+import Spa.Language.Graphs
+import Spa.Language.Traces
+import Spa.Language.Properties
+import Spa.Language
+import Spa.Analysis.Forward.Lattices
+import Spa.Analysis.Forward.Evaluation
+import Spa.Analysis.Forward.Adapters
+import Spa.Analysis.Forward
+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

lean/Spa/Analysis/Constant.lean

@@ -0,0 +1,149 @@
+import Spa.Analysis.Forward
+import Spa.Analysis.Utils
+import Spa.Interp
+import Spa.Showable
+
+namespace Spa
+
+open Forward
+
+abbrev ConstLattice : Type := AboveBelow ℤ
+
+namespace ConstAnalysis
+
+open AboveBelow in
+def plus : ConstLattice → ConstLattice → ConstLattice
+  | bot, _ => bot
+  | _, bot => bot
+  | top, _ => top
+  | _, top => top
+  | mk z₁, mk z₂ => mk (z₁ + z₂)
+
+open AboveBelow in
+def minus : ConstLattice → ConstLattice → ConstLattice
+  | bot, _ => bot
+  | _, bot => bot
+  | top, _ => top
+  | _, top => top
+  | mk z₁, mk z₂ => mk (z₁ - z₂)
+
+lemma plus_mono₂ : Monotone₂ plus :=
+  AboveBelow.monotone₂_of_strict plus
+    (fun y => by aesop) (fun x => by aesop)
+    (fun y hy => by aesop) (fun x hx => by aesop)
+
+lemma minus_mono₂ : Monotone₂ minus :=
+  AboveBelow.monotone₂_of_strict minus
+    (fun y => by aesop) (fun x => by aesop)
+    (fun y hy => by aesop) (fun x hx => by aesop)
+
+def interpConst : ConstLattice → Value → Prop
+  | .bot, _ => False
+  | .top, _ => True
+  | .mk z, v => v = .int z
+
+lemma interpConst_mk_disjoint {z₁ z₂ : ℤ} (hne : z₁ ≠ z₂) {v : Value} :
+    ¬(interpConst (.mk z₁) v ∧ interpConst (.mk z₂) v) := by
+  rintro ⟨h₁, h₂⟩
+  rw [h₁] at h₂
+  injection h₂ with hz
+  exact hne hz
+
+instance constInterpretation : LatticeInterpretation ConstLattice where
+  interp := interpConst
+  interp_sup := fun v h => AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
+  interp_inf := fun v h => AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h
+
+variable (prog : Program)
+
+def eval : Expr → VariableValues ConstLattice prog → ConstLattice
+  | .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 n, _ => .mk n
+
+lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
+  induction e with
+  | add e₁ e₂ ih₁ ih₂ =>
+    intro vs₁ vs₂ h
+    exact eval_combine₂ plus_mono₂ (ih₁ h) (ih₂ h)
+  | sub e₁ e₂ ih₁ ih₂ =>
+    intro vs₁ vs₂ h
+    exact eval_combine₂ minus_mono₂ (ih₁ h) (ih₂ h)
+  | var k =>
+    intro vs₁ vs₂ h
+    simp only [eval]
+    by_cases hk : k ∈ prog.vars
+    · rw [dif_pos (FiniteMap.MemKey_iff.mpr hk),
+          dif_pos (FiniteMap.MemKey_iff.mpr hk)]
+      exact FiniteMap.le_of_mem_mem prog.vars_nodup h
+        (FiniteMap.locate _).2 (FiniteMap.locate _).2
+    · rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)),
+          dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
+  | num n =>
+    intro vs₁ vs₂ _
+    exact le_refl _
+
+instance exprEvaluator : ExprEvaluator ConstLattice prog :=
+  ⟨eval prog, eval_mono prog⟩
+
+def output : String :=
+  show' (result ConstLattice prog)
+
+lemma plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
+    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
+    ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
+  rcases g₁ with _ | _ | c₁ <;> rcases g₂ with _ | _ | c₂ <;>
+    simp_all [plus, constInterpretation, interpConst]
+
+lemma minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
+    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
+    ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
+  rcases g₁ with _ | _ | c₁ <;> rcases g₂ with _ | _ | c₂ <;>
+    simp_all [minus, constInterpretation, interpConst]
+
+instance eval_valid : ValidExprEvaluator ConstLattice prog := by
+  constructor
+  intro vs ρ e v hev
+  induction hev with
+  | num n =>
+    intro _
+    show ⟦eval prog (.num n) vs⟧ (.int n)
+    rfl
+  | var x v hxv =>
+    intro hvs
+    show ⟦eval prog (.var x) vs⟧ v
+    simp only [eval]
+    by_cases hk : FiniteMap.MemKey x vs
+    · rw [dif_pos hk]
+      exact hvs _ _ (FiniteMap.locate hk).2 _ hxv
+    · rw [dif_neg hk]
+      exact trivial
+  | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
+    intro hvs
+    have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
+    have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
+    show ⟦eval prog (.add e₁ e₂) vs⟧ (.int (z₁ + z₂))
+    exact plus_valid h₁ h₂
+  | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
+    intro hvs
+    have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
+    have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
+    show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂))
+    exact minus_valid h₁ h₂
+
+theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ :=
+  Forward.analyze_correct ConstLattice prog hrun
+
+theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin
+      ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout :=
+  Forward.analyze_correct_at ConstLattice prog hrun hr
+
+end ConstAnalysis
+
+end Spa

lean/Spa/Analysis/Forward.lean

@@ -0,0 +1,174 @@
+import Spa.Analysis.Forward.Lattices
+import Spa.Analysis.Forward.Evaluation
+import Spa.Analysis.Forward.Adapters
+import Spa.Fixedpoint
+
+namespace Spa
+
+namespace Forward
+
+variable {L : Type} [FiniteHeightLattice L] {prog : Program} [E : StmtEvaluator L prog]
+
+def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
+    VariableValues L prog := E.eval s (variablesAt s sv)
+
+lemma updateVariablesForState_mono (s : prog.State) :
+    Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
+  E.eval_mono s (variablesAt_le hle s)
+
+def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
+  FiniteMap.generalizedUpdate id updateVariablesForState
+    prog.states sv
+
+lemma updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
+  FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono
+
+lemma updateAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
+    {sv : StateVariables L prog} (hmem : (s, vs) ∈ updateAll sv) :
+    vs = updateVariablesForState s sv :=
+  FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) hmem
+
+lemma variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
+    variablesAt s (updateAll sv) = updateVariablesForState s sv :=
+  updateAll_mem_eq (variablesAt_mem s (updateAll sv))
+
+def analyze (sv : StateVariables L prog) : StateVariables L prog :=
+  updateAll (joinAll sv)
+
+lemma analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
+  updateAll_mono (joinAll_mono hle)
+
+variable [DecidableEq L]
+
+variable (L prog) in
+def result : StateVariables L prog :=
+  Fixedpoint.aFix analyze analyze_mono
+
+variable (L prog) in
+lemma result_eq : result L prog = analyze (result L prog) :=
+  Fixedpoint.aFix_eq analyze analyze_mono
+
+lemma joinForKey_initialState :
+    joinForKey prog.initialState (result L prog) = botV L prog := by
+  rw [joinForKey, prog.incoming_initialState_eq_nil]
+  rfl
+
+class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
+    [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
+  valid : ∀ (s₁ s₂ : prog.State) {ρ₁ ρ₂ ρ₃: Env}
+    {vs : VariableValues L prog},
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) →
+    (hbs : EvalBasicStmtOpt ρ₂ (prog.cfg.nodes s₂) ρ₃) → ⟦ vs ⟧ (S.Pre tr) →
+    ⟦ E.eval s₂ vs ⟧ (S.Post (tr ++ hbs))
+  botV_init : ⟦ botV L prog ⟧ (S.Pre (Traceₗ.single prog.cfg prog.initialState []))
+
+instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
+    ValidStateEvaluator L prog where
+  valid := by intro _ _ _ _ _ _ tr hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
+  botV_init := by intro k l _ v hmem; cases hmem
+
+section
+variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]
+
+omit [DecidableEq L] in
+lemma updateAll_matches {s₁ s₂ : prog.State} {sv : StateVariables L prog}
+    {ρ₁ ρ₂ ρ₃ : Env}
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃)
+    (hvs : ⟦ variablesAt s₂ sv ⟧ (S.Pre tr)) :
+    ⟦ variablesAt s₂ (updateAll sv) ⟧ (S.Post (tr ++ hnode)) := by
+  rw [variablesAt_updateAll]
+  exact V.valid s₁ s₂ tr hnode hvs
+
+lemma stepTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre tr))
+    (hnode : EvalBasicStmtOpt ρ₂ (prog.code s₂) ρ₃) :
+    ⟦ variablesAt s₂ (result L prog) ⟧ (S.Post (tr ++ hnode)) := by
+  rw [result_eq L prog]
+  refine updateAll_matches tr hnode ?_
+  rw [variablesAt_joinAll]
+  exact hjoin
+
+/-- Soundness at *every* visited node: if the analysis result over-approximates the
+    incoming environment at the start of the trace, then at each node reached along the
+    way it over-approximates both the environment entering that node (via `joinForKey`)
+    and the environment leaving it (via `variablesAt`). The intermediate `variablesAt`
+    evidence used to be computed and discarded inside `walkTrace`; here it is returned. -/
+lemma walkTrace_reaches {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ ρ₃: Env}
+    {s : prog.State} {ρin ρout : Env}
+    {tr : Trace prog.cfg s₂ s₃ ρ₂ ρ₃}
+    (hr : Reaches tr s ρin ρout)
+    (trₗ : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂)
+    (hjoin : ⟦ joinForKey s₂ (result L prog) ⟧ (S.Pre trₗ)) :
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre (trₗ ++ hr.pre))
+      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post (trₗ ++ hr.post)) := by
+  induction hr with
+  | single_here hnode =>
+    simp [Reaches.pre, Reaches.post]
+    refine ⟨?_, ?_⟩ <;> try simpa [HAppend.hAppend]
+    exact stepTrace trₗ hjoin hnode
+  | edge_here hnode hedge rest =>
+    simp [Reaches.pre, Reaches.post]
+    refine ⟨?_, ?_⟩ <;> try simpa [HAppend.hAppend]
+    exact stepTrace trₗ hjoin hnode
+  | edge_there hnode hedge rest hr' ih =>
+    have hstep := stepTrace trₗ hjoin hnode
+    have hmem := FiniteMap.mem_valuesAt prog.states_nodup
+      (prog.mem_incoming_of_edge hedge) (variablesAt_mem _ (result L prog))
+    simpa [Reaches.pre, Reaches.post, HAppend.hAppend] using
+      ih ((trₗ ++ hnode).addEdge hedge)
+        (interp_foldr (S.post_pre (trₗ ++ hnode) hedge hstep) hmem)
+
+omit [DecidableEq L] in
+/-- The final node of a trace is always reached, with the environment/state the trace
+    ends in. Used to recover the final-state soundness theorem from `walkTrace_reaches`. -/
+def reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
+    Σ ρin, Reaches tr s₂ ρin ρ₂ :=
+  match tr with
+  | .single hnode => ⟨_, .single_here hnode⟩
+  | .edge hnode hedge rest =>
+    let ⟨ρin, r'⟩ := reaches_final rest; ⟨ρin, .edge_there hnode hedge _ r'⟩
+
+omit [DecidableEq L] in
+/-- Reaching the final node covers the whole trace. -/
+@[simp] lemma reaches_final_post {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
+    (reaches_final tr).2.post = tr := by
+  induction tr with
+  | single hnode => rfl
+  | edge hnode hedge rest ih => simp [reaches_final, Reaches.post, ih]
+
+variable (L prog) in
+/-- Soundness at every program point reached during execution: for any node `s` visited
+    by the run `hrun` (witnessed by `hr`), the analysis result over-approximates both the
+    environment entering `s` and the one leaving it. The final-state theorem
+    `analyze_correct_state` is the special case where `s` is `prog.finalState`. -/
+theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result L prog) ⟧ (S.Pre hr.pre)
+      ∧ ⟦ variablesAt s (result L prog) ⟧ (S.Post hr.post) := by
+  refine walkTrace_reaches hr (Traceₗ.single _ _ []) ?_
+  rw [joinForKey_initialState]
+  exact ValidStateEvaluator.botV_init
+
+variable (L prog) in
+theorem analyze_correct'
+    {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    ⟦ variablesAt prog.finalState (result L prog) ⟧ (S.Post (prog.trace hrun)) := by
+  have h := (analyze_correct_at L prog hrun (reaches_final (prog.trace hrun)).2).2
+  rwa [reaches_final_post] at h
+
+end
+
+variable (L prog) in
+theorem analyze_correct [LatticeInterpretation L] [ValidStmtEvaluator L prog]
+    {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    ⟦ variablesAt prog.finalState (result L prog) ⟧ ρ :=
+  analyze_correct' L prog hrun
+
+end Forward
+
+end Spa

lean/Spa/Analysis/Forward/Adapters.lean

@@ -0,0 +1,64 @@
+import Spa.Analysis.Forward.Evaluation
+
+namespace Spa
+
+namespace Forward
+
+variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog]
+
+def updateVariablesFromExpression (k : String) (e : Expr)
+    (vs : VariableValues L prog) : VariableValues L prog :=
+  FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs
+
+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 (bs : BasicStmt)
+    (vs : VariableValues L prog) : VariableValues L prog :=
+  match bs with
+  | .assign k e => updateVariablesFromExpression k e vs
+  | .noop => vs
+
+lemma evalBasicStmt_mono (bs : BasicStmt) :
+    Monotone (evalBasicStmt (L := L) (prog := prog) bs) := by
+  cases bs with
+  | assign k e => exact updateVariablesFromExpression_mono k e
+  | noop => exact monotone_id
+
+def evalBasicStmtOpt (obs : Option BasicStmt)
+    (vs : VariableValues L prog) : VariableValues L prog :=
+  match obs with
+  | none => vs
+  | some bs => evalBasicStmt bs vs
+
+lemma evalBasicStmtOpt_mono (obs : Option BasicStmt) :
+    Monotone (evalBasicStmtOpt (L := L) (prog := prog) obs) := by
+  cases obs <;> unfold evalBasicStmtOpt
+  · exact monotone_id
+  · apply evalBasicStmt_mono
+
+instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
+  ⟨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
+  simp [StmtEvaluator.eval, evalBasicStmtOpt]
+  intro s vs ρ₁ ρ₂; generalize prog.code s = obs; intro hev hvs
+  rcases hev with _ | @⟨_,bs,hev⟩ <;> try simpa
+  rcases hev with _ | @⟨k, e, v, hev⟩ <;> try simpa
+  intros k' l' hkl' v' hρ
+  rcases hρ with _ | ⟨_,_,_,_,_,hne,hmem⟩ <;> simp [evalBasicStmt] at hkl'
+  · have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
+        (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hkl'
+    rewrite [hl]; simp
+    exact ValidExprEvaluator.valid hev hvs
+  · have hl := FiniteMap.generalizedUpdate_not_mem_backward
+        (fun hmem => hne (List.mem_singleton.mp hmem)) hkl'
+    apply hvs _ _ hl _ hmem
+
+end Forward
+
+end Spa

lean/Spa/Analysis/Forward/Evaluation.lean

@@ -0,0 +1,29 @@
+import Spa.Analysis.Forward.Lattices
+
+namespace Spa
+
+namespace Forward
+
+variable (L : Type) [Lattice L] (prog : Program)
+
+class StmtEvaluator where
+  eval : prog.State → VariableValues L prog → VariableValues L prog
+  eval_mono : ∀ s, Monotone (eval s)
+
+class ExprEvaluator where
+  eval : Expr → VariableValues L prog → L
+  eval_mono : ∀ e, Monotone (eval e)
+
+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
+
+class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
+    Prop where
+  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env},
+    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ → ⟦ E.eval s vs ⟧ ρ₂
+
+end Forward
+
+end Spa

lean/Spa/Analysis/Forward/Lattices.lean

@@ -0,0 +1,121 @@
+import Spa.Language
+import Spa.Lattice.FiniteMap
+import Spa.Interp
+
+namespace Spa
+
+namespace Forward
+
+variable (L : Type) [Lattice L] (prog : Program)
+
+abbrev VariableValues : Type := FiniteMap String L prog.vars
+
+abbrev StateVariables : Type := FiniteMap prog.State (VariableValues L prog) prog.states
+
+def botV [FiniteHeightLattice L] : VariableValues L prog :=
+  (⊥ : VariableValues L prog)
+
+variable {L prog}
+
+omit [Lattice L] in
+lemma states_memKey (s : prog.State) (sv : StateVariables L prog) :
+    FiniteMap.MemKey s sv :=
+  FiniteMap.MemKey_iff.mpr (prog.states_complete s)
+
+def variablesAt (s : prog.State) (sv : StateVariables L prog) :
+    VariableValues L prog :=
+  (FiniteMap.locate (states_memKey s sv)).1
+
+omit [Lattice L] in
+lemma variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
+    (s, variablesAt s sv) ∈ sv :=
+  (FiniteMap.locate (states_memKey s sv)).2
+
+lemma variablesAt_le {sv₁ sv₂ : StateVariables L prog} (hle : sv₁ ≤ sv₂)
+    (s : prog.State) : variablesAt s sv₁ ≤ variablesAt s sv₂ :=
+  FiniteMap.le_of_mem_mem prog.states_nodup hle
+    (variablesAt_mem s sv₁) (variablesAt_mem s sv₂)
+
+variable [FiniteHeightLattice L]
+
+def joinForKey (k : prog.State) (sv : StateVariables L prog) :
+    VariableValues L prog :=
+  (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog)
+
+lemma joinForKey_mono (k : prog.State) :
+    Monotone (joinForKey (L := L) k) := by
+  intro sv₁ sv₂ hle
+  exact foldr_mono _ (FiniteMap.valuesAt_le hle (prog.incoming k)) (le_refl _)
+    (fun b _ _ hab => sup_le_sup_right hab b)
+    (fun a _ _ hab => sup_le_sup_left hab a)
+
+def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
+  FiniteMap.generalizedUpdate id joinForKey prog.states sv
+
+lemma joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
+  FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono
+
+lemma joinAll_mem_eq {s : prog.State} {vs : VariableValues L prog}
+    {sv : StateVariables L prog} (h : (s, vs) ∈ joinAll sv) :
+    vs = joinForKey s sv :=
+  FiniteMap.generalizedUpdate_mem_eq (prog.states_complete s) h
+
+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 StateInterpretation (L : Type) [Lattice L] (prog : Program) where
+  Proj : Type
+  Pre : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
+  Post : ∀ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}, Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → Proj
+
+  interp : VariableValues L prog → (p : Proj) → Prop
+  interp_sup : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj},
+    interp vs₁ p ∨ interp vs₂ p → interp (vs₁ ⊔ vs₂) p
+  interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {p : Proj},
+    interp vs₁ p ∧ interp vs₂ p → interp (vs₁ ⊓ vs₂) p
+
+  post_pre : ∀ {vs} {s₁ s₂ s₃: prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) (hedge : (s₂, s₃) ∈ prog.cfg.edges),
+    interp vs (Post tr) → interp vs (Pre (tr.addEdge hedge))
+
+instance [S : StateInterpretation L prog] :
+    Interp (VariableValues L prog) (S.Proj → Prop) :=
+  ⟨S.interp⟩
+
+lemma interp_foldr [S : StateInterpretation L prog]
+    {vs : VariableValues L prog} {vss : List (VariableValues L prog)}
+    {p : S.Proj} (hvs : ⟦ vs ⟧ p) (hmem : vs ∈ vss) :
+    ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ p := by
+  induction vss with
+  | nil => cases hmem
+  | cons vs' vss' ih =>
+    rcases List.mem_cons.mp hmem with rfl | hmem'
+    · exact S.interp_sup (Or.inl hvs)
+    · exact S.interp_sup (Or.inr (ih hmem'))
+
+variable [I : LatticeInterpretation L]
+
+instance : StateInterpretation L prog where
+  Proj := Env
+  Pre := fun {_ _ _ ρ₂} _ => ρ₂
+  Post := fun {_ _ _ ρ₂} _ => ρ₂
+
+  interp vs ρ := ∀ (k : String) (l : L), (k, l) ∈ vs →
+    ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
+  interp_sup := by
+    intro vs₁ vs₂ ρ 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₂ ρ 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
+
+end Spa

lean/Spa/Analysis/Reaching.lean

@@ -0,0 +1,135 @@
+import Spa.Analysis.Forward
+import Spa.Lattice.Finset
+import Spa.Language.Tagged.Graphs
+import Spa.Showable
+
+namespace Spa
+
+open Forward
+
+instance {n : ℕ} : Showable (Finset (Fin n)) :=
+  ⟨fun s =>
+    "{" ++ (List.finRange n).foldr
+        (fun i rest => if i ∈ s then show' i ++ ", " ++ rest else rest) ""
+        ++ "}"⟩
+
+abbrev DefSet (prog : Program) : Type := Finset prog.NodeId
+
+namespace ReachingAnalysis
+
+variable (prog : Program)
+
+def genSet (s : prog.State) : DefSet prog := (prog.nodeIdOf s).elim {} (fun x => {x})
+
+def eval (s : prog.State) (vs : VariableValues (DefSet prog) prog) : VariableValues (DefSet prog) prog :=
+  match prog.code s with
+  | none => vs
+  | some bs =>
+    match bs with
+    | .assign k _ => FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs
+    | .noop => vs
+
+lemma eval_mono (s : prog.State) :
+    Monotone (eval prog s) := by
+  intros vs₁ vs₂ hle
+  unfold eval; split <;> try simpa
+  split <;> try simpa
+  apply FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
+  assumption
+
+instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
+  ⟨eval prog, eval_mono prog⟩
+
+def output : String :=
+  show' (result (DefSet prog) prog)
+
+/-- The statements a trace executed, paired with the state each executed at,
+    most recent first (matching `LastAssign`, which scans for the most recent
+    assignment). This is `Trace.steps` (chronological) reversed, so facts about
+    concatenating traces reduce to mathlib's `List.append`/`List.reverse` lemmas. -/
+abbrev Run (prog : Program) : Type := List (prog.State × BasicStmt)
+
+@[aesop unsafe cases]
+inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId → Prop
+  | here (s : prog.State) (e : Expr) (hc : prog.code s = some (.assign x e))
+      (rest : Run prog) :
+      LastAssign prog x ((s, .assign x e) :: rest) (prog.nodeIdOfNonempty s hc)
+  | there (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
+      (rest : Run prog) {n : prog.NodeId} :
+      (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
+      LastAssign prog x ((s, bs) :: rest) n
+
+def runOfTraceₗ {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Traceₗ prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
+  tr.steps.reverse
+
+def runOfTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) : Run prog :=
+  tr.steps.reverse
+
+instance stateInterp : StateInterpretation (DefSet prog) prog where
+  Proj := Run prog
+  Pre := @runOfTraceₗ prog
+  Post := @runOfTrace prog
+
+  interp vs run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
+    ∀ (n : prog.NodeId), LastAssign prog x run n → n ∈ assigners
+  interp_sup := by
+    intro vs₁ vs₂ run h x assigners hmem n hla
+    obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
+    aesop (add simp Finset.mem_union)
+  interp_inf := by
+    intro vs₁ vs₂ run h x assigners hmem n hla
+    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 [Program.nodeIdOfNonempty, hd, genSet, Option.get] <;> aesop
+    · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
+        (fun hc => hx (List.mem_singleton.mp hc)) hmem
+      aesop
+
+instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
+  valid := by
+    intro s₁ s₂ ρ₁ ρ₂ ρ₃ vs tr hbs hvs
+    show ⟦eval prog s₂ vs⟧ (runOfTrace prog (tr ++ hbs))
+    simpa [runOfTrace, runOfTraceₗ] using valid_step prog s₂ rfl hbs hvs
+  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) ⟧
+      (runOfTrace prog (prog.trace hrun)) :=
+  Forward.analyze_correct' (DefSet prog) prog hrun
+
+theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result (DefSet prog) prog) ⟧ (runOfTraceₗ prog hr.pre)
+      ∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ (runOfTrace prog hr.post) :=
+  Forward.analyze_correct_at (DefSet prog) prog hrun hr
+
+end ReachingAnalysis
+
+end Spa

lean/Spa/Analysis/Sign.lean

@@ -0,0 +1,225 @@
+import Spa.Analysis.Forward
+import Spa.Analysis.Utils
+import Spa.Interp
+import Spa.Showable
+
+namespace Spa
+
+open Forward
+
+inductive Sign where
+  | plus
+  | minus
+  | zero
+  deriving DecidableEq
+
+attribute [aesop safe cases] Sign
+
+instance : Showable Sign :=
+  ⟨fun
+    | .plus => "+"
+    | .minus => "-"
+    | .zero => "0"⟩
+
+instance : Inhabited Sign := ⟨.zero⟩
+
+abbrev SignLattice : Type := AboveBelow Sign
+
+open AboveBelow in
+def plus : SignLattice → SignLattice → SignLattice
+  | bot, _ => bot
+  | _, bot => bot
+  | top, _ => top
+  | _, top => top
+  | mk .plus, mk .plus => mk .plus
+  | mk .plus, mk .minus => top
+  | mk .plus, mk .zero => mk .plus
+  | mk .minus, mk .plus => top
+  | mk .minus, mk .minus => mk .minus
+  | mk .minus, mk .zero => mk .minus
+  | mk .zero, mk .plus => mk .plus
+  | mk .zero, mk .minus => mk .minus
+  | mk .zero, mk .zero => mk .zero
+
+open AboveBelow in
+def minus : SignLattice → SignLattice → SignLattice
+  | bot, _ => bot
+  | _, bot => bot
+  | top, _ => top
+  | _, top => top
+  | mk .plus, mk .plus => top
+  | mk .plus, mk .minus => mk .plus
+  | mk .plus, mk .zero => mk .plus
+  | mk .minus, mk .plus => mk .minus
+  | mk .minus, mk .minus => top
+  | mk .minus, mk .zero => mk .minus
+  | mk .zero, mk .plus => mk .minus
+  | mk .zero, mk .minus => mk .plus
+  | mk .zero, mk .zero => mk .zero
+
+lemma plus_mono₂ : Monotone₂ plus :=
+  AboveBelow.monotone₂_of_strict plus
+    (fun y => by aesop) (fun x => by aesop)
+    (fun y hy => by aesop) (fun x hx => by aesop)
+
+lemma minus_mono₂ : Monotone₂ minus :=
+  AboveBelow.monotone₂_of_strict minus
+    (fun y => by aesop) (fun x => by aesop)
+    (fun y hy => by aesop) (fun x hx => by aesop)
+
+def interpSign : SignLattice → Value → Prop
+  | .bot, _ => False
+  | .top, _ => True
+  | .mk .plus, v => ∃ n : ℕ, v = .int (n + 1)
+  | .mk .zero, v => v = .int 0
+  | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))
+
+lemma interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
+    ¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by
+  rintro ⟨h₁, h₂⟩
+  rcases s₁ <;> rcases s₂ <;> try exact hne rfl
+  all_goals simp only [interpSign] at h₁ h₂
+  · obtain ⟨n₁, rfl⟩ := h₁
+    obtain ⟨n₂, hv⟩ := h₂
+    injection hv with hz
+    omega
+  · obtain ⟨n₁, rfl⟩ := h₁
+    injection h₂ with hz
+    omega
+  · obtain ⟨n₁, rfl⟩ := h₁
+    obtain ⟨n₂, hv⟩ := h₂
+    injection hv with hz
+    omega
+  · obtain ⟨n₁, rfl⟩ := h₁
+    injection h₂ with hz
+    omega
+  · subst h₁
+    obtain ⟨n₂, hv⟩ := h₂
+    injection hv with hz
+    omega
+  · subst h₁
+    obtain ⟨n₂, hv⟩ := h₂
+    injection hv with hz
+    omega
+
+instance signInterpretation : LatticeInterpretation SignLattice where
+  interp := interpSign
+  interp_sup := fun v h => AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
+  interp_inf := fun v h => AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h
+
+namespace SignAnalysis
+
+variable (prog : Program)
+
+def eval : Expr → VariableValues SignLattice prog → SignLattice
+  | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs)
+  | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs)
+  | .var k, vs =>
+    if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
+  | .num 0, _ => .mk .zero
+  | .num (_ + 1), _ => .mk .plus
+
+lemma eval_mono (e : Expr) : Monotone (eval prog e) := by
+  induction e with
+  | add e₁ e₂ ih₁ ih₂ =>
+    intro vs₁ vs₂ h
+    exact eval_combine₂ plus_mono₂ (ih₁ h) (ih₂ h)
+  | sub e₁ e₂ ih₁ ih₂ =>
+    intro vs₁ vs₂ h
+    exact eval_combine₂ minus_mono₂ (ih₁ h) (ih₂ h)
+  | var k =>
+    intro vs₁ vs₂ h
+    simp only [eval]
+    by_cases hk : k ∈ prog.vars
+    · rw [dif_pos (FiniteMap.MemKey_iff.mpr hk),
+          dif_pos (FiniteMap.MemKey_iff.mpr hk)]
+      exact FiniteMap.le_of_mem_mem prog.vars_nodup h
+        (FiniteMap.locate _).2 (FiniteMap.locate _).2
+    · rw [dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm)),
+          dif_neg (fun hm => hk (FiniteMap.MemKey_iff.mp hm))]
+  | num n =>
+    intro vs₁ vs₂ _
+    cases n <;> exact le_refl _
+
+instance exprEvaluator : ExprEvaluator SignLattice prog :=
+  ⟨eval prog, eval_mono prog⟩
+
+def output : String :=
+  show' (result SignLattice prog)
+
+/-- A nonneg-shifted interpretation `∃ n : ℕ, z = n + 1` just means `z` is positive. -/
+private lemma int_pos_iff (z : ℤ) : (∃ n : ℕ, z = (n : ℤ) + 1) ↔ 0 < z := by
+  constructor
+  · rintro ⟨n, rfl⟩; omega
+  · intro h; exact ⟨(z - 1).toNat, by omega⟩
+
+/-- Dually, `∃ n : ℕ, z = -(n + 1)` just means `z` is negative. -/
+private lemma int_neg_iff (z : ℤ) : (∃ n : ℕ, z = -((n : ℤ) + 1)) ↔ z < 0 := by
+  constructor
+  · rintro ⟨n, rfl⟩; omega
+  · intro h; exact ⟨(-z - 1).toNat, by omega⟩
+
+lemma plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
+    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
+    ⟦plus g₁ g₂⟧ (.int (z₁ + z₂)) := by
+  rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
+    (try rcases s₁) <;> (try rcases s₂) <;>
+    simp only [plus, signInterpretation, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
+      at h₁ h₂ ⊢ <;>
+    omega
+
+lemma minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
+    (h₁ : ⟦g₁⟧ (.int z₁)) (h₂ : ⟦g₂⟧ (.int z₂)) :
+    ⟦minus g₁ g₂⟧ (.int (z₁ - z₂)) := by
+  rcases g₁ with _ | _ | s₁ <;> rcases g₂ with _ | _ | s₂ <;>
+    (try rcases s₁) <;> (try rcases s₂) <;>
+    simp only [minus, signInterpretation, interpSign, Value.int.injEq, int_pos_iff, int_neg_iff]
+      at h₁ h₂ ⊢ <;>
+    omega
+
+instance eval_valid : ValidExprEvaluator SignLattice prog := by
+  constructor
+  intro vs ρ e v hev
+  induction hev with
+  | num n =>
+    intro _
+    show ⟦eval prog (.num n) vs⟧ (.int n)
+    cases n with
+    | zero => rfl
+    | succ n' => exact ⟨n', congrArg Value.int (by norm_cast)⟩
+  | var x v hxv =>
+    intro hvs
+    show ⟦eval prog (.var x) vs⟧ v
+    simp only [eval]
+    by_cases hk : FiniteMap.MemKey x vs
+    · rw [dif_pos hk]
+      exact hvs _ _ (FiniteMap.locate hk).2 _ hxv
+    · rw [dif_neg hk]
+      exact trivial
+  | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
+    intro hvs
+    have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
+    have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
+    show ⟦eval prog (.add e₁ e₂) vs⟧ (.int (z₁ + z₂))
+    exact plus_valid h₁ h₂
+  | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
+    intro hvs
+    have h₁ : ⟦eval prog e₁ vs⟧ (.int z₁) := ih₁ hvs
+    have h₂ : ⟦eval prog e₂ vs⟧ (.int z₂) := ih₂ hvs
+    show ⟦eval prog (.sub e₁ e₂) vs⟧ (.int (z₁ - z₂))
+    exact minus_valid h₁ h₂
+
+theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ :=
+  Forward.analyze_correct SignLattice prog hrun
+
+theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
+    {s : prog.State} {ρin ρout : Env}
+    (hr : Reaches (prog.trace hrun) s ρin ρout) :
+    ⟦ joinForKey s (result SignLattice prog) ⟧ ρin
+      ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout :=
+  Forward.analyze_correct_at SignLattice prog hrun hr
+
+end SignAnalysis
+
+end Spa

lean/Spa/Analysis/Utils.lean

@@ -0,0 +1,10 @@
+import Spa.Lattice
+
+namespace Spa
+
+lemma eval_combine₂ {O : Type*} [Preorder O] {combine : O → O → O}
+    (hmono : Monotone₂ combine) {o₁ o₂ o₃ o₄ : O}
+    (h₁ : o₁ ≤ o₃) (h₂ : o₂ ≤ o₄) : combine o₁ o₂ ≤ combine o₃ o₄ :=
+  le_trans (hmono.1 o₂ h₁) (hmono.2 o₃ h₂)
+
+end Spa

lean/Spa/Fixedpoint.lean

@@ -0,0 +1,56 @@
+import Spa.Lattice
+
+namespace Spa
+
+namespace Fixedpoint
+
+open FiniteHeightLattice (height)
+
+variable {α : Type*} [DecidableEq α] [FiniteHeightLattice α]
+
+def doStep (f : α → α) (hf : Monotone f) :
+    ∀ (g : ℕ) (c : LTSeries α), c.length + g = height (α := α) + 1 →
+      c.last ≤ f c.last → {a : α // a = f a}
+  | 0, c, hlen, _ =>
+    absurd (FiniteHeightLattice.chains_bounded c) (by omega)
+  | g + 1, c, hlen, hle =>
+    if heq : c.last = f c.last then
+      ⟨c.last, heq⟩
+    else
+      doStep f hf g (c.snoc (f c.last) (lt_of_le_of_ne hle heq))
+        (by simp [RelSeries.snoc]; omega)
+        (by rw [RelSeries.last_snoc]; exact hf hle)
+
+def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
+  doStep f hf (height (α := α) + 1) (RelSeries.singleton _ ⊥)
+    (by simp)
+    (by simp)
+
+def aFix (f : α → α) (hf : Monotone f) : α :=
+  (fix f hf).1
+
+theorem aFix_eq (f : α → α) (hf : Monotone f) :
+    aFix f hf = f (aFix f hf) :=
+  (fix f hf).2
+
+lemma doStep_le (f : α → α) (hf : Monotone f)
+    {b : α} (hb : b = f b) :
+    ∀ (g : ℕ) (c : LTSeries α) (hlen : c.length + g = height (α := α) + 1)
+      (hle : c.last ≤ f c.last), c.last ≤ b →
+      (doStep f hf g c hlen hle : α) ≤ b
+  | 0, c, hlen, _ => fun _ =>
+    absurd (FiniteHeightLattice.chains_bounded c) (by omega)
+  | g + 1, c, hlen, hle => fun hcb => by
+    rw [doStep]
+    split
+    · exact hcb
+    · exact doStep_le f hf hb g _ _ _
+        (by rw [RelSeries.last_snoc]; exact le_of_le_of_eq (hf hcb) hb.symm)
+
+theorem aFix_le (f : α → α) (hf : Monotone f)
+    {a : α} (ha : a = f a) : aFix f hf ≤ a :=
+  doStep_le f hf ha _ _ _ _ (by simp)
+
+end Fixedpoint
+
+end Spa

lean/Spa/Interp.lean

@@ -0,0 +1,20 @@
+import Mathlib.Tactic.TypeStar
+
+/-!
+
+# Interpretation to a Semantic Domain
+
+This file serves to introduce the double-angle-bracket "denotation"
+notation by prodiving a class instance `Interp`, whose single
+method `interp` is what the double brackets map to. -/
+
+namespace Spa
+
+/-- A type `α` that implements this class has denotation / meaning
+   in the semantic domain `dom`. -/
+class Interp (α : Type*) (dom : outParam Type*) where
+  interp : α → dom
+
+notation:max (priority := high) "⟦" v "⟧" => Interp.interp v
+
+end Spa

lean/Spa/Language.lean

@@ -0,0 +1,6 @@
+import Spa.Language.Base
+import Spa.Language.Semantics
+import Spa.Language.Graphs
+import Spa.Language.Traces
+import Spa.Language.Properties
+import Spa.Language.Program

lean/Spa/Language/Base.lean

@@ -0,0 +1,59 @@
+import Mathlib.Data.Finset.Basic
+
+/-!
+
+# Base Language
+
+This file defines the core object language for the program analysis and
+transformation. It's a very basic imperative language. The `Spa/Language/Tagged/Basic.lean`
+file provides an auto-derived version of the `Expr`, `BasicStmt`, and `Stmt` data
+types with unique IDs per condtructor, enabling in-AST pointers.
+
+-/
+
+namespace Spa
+
+/-- A value-producing expression. Currently, this cannot have side effects. -/
+inductive Expr where
+  | add (e₁ e₂ : Expr)
+  | sub (e₁ e₂ : Expr)
+  | var (x : String)
+  | num (n : ℕ)
+  deriving DecidableEq
+
+/-- A statement that cannot alter control flow (and thus, can be part of a basic block).
+
+    This differs from, e.g., a loop, which can cause execution to jump to its top several times. -/
+inductive BasicStmt where
+  | assign (x : String) (e : Expr)
+  | noop
+  deriving DecidableEq
+
+/-- Any statements, which may or may not change program state (variable assignments). -/
+inductive Stmt where
+  | basic (bs : BasicStmt)
+  | andThen (s₁ s₂ : Stmt)
+  | ifElse (e : Expr) (s₁ s₂ : Stmt)
+  | whileLoop (e : Expr) (s : Stmt)
+  deriving DecidableEq
+
+/-- Variables mentioned in this expression. -/
+def Expr.vars : Expr → Finset String
+  | .add l r => l.vars ∪ r.vars
+  | .sub l r => l.vars ∪ r.vars
+  | .var s => {s}
+  | .num _ => ∅
+
+/-- Variables assigned or mentioned in this basic statement. -/
+def BasicStmt.vars : BasicStmt → Finset String
+  | .assign x e => {x} ∪ e.vars
+  | .noop => ∅
+
+/-- Variables assigned or mentioned in this statement. -/
+def Stmt.vars : Stmt → Finset String
+  | .basic bs => bs.vars
+  | .andThen s₁ s₂ => s₁.vars ∪ s₂.vars
+  | .ifElse e s₁ s₂ => (e.vars ∪ s₁.vars) ∪ s₂.vars
+  | .whileLoop e s => e.vars ∪ s.vars
+
+end Spa

lean/Spa/Language/Graphs.lean

@@ -0,0 +1,360 @@
+import Spa.Language.Base
+import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Data.List.ProdSigma
+import Mathlib.Data.List.FinRange
+
+/-!
+
+# Algebraic Control Flow Graphs
+
+This file defines control flow graphs and operations to naturally compose them,
+making it possible to inductively covnert a program in the object language
+(see `Spa.Stmt` in `Spa/Language/Base.lean`) into its corresponding graph.
+
+Graphs are, in general, parameterized by their "payload" (the per-node data); see `GGraph`.
+This is useful because other operations, such as finding the CFG node corresponding
+to an AST node, are performed by embellishing a graph's basic blocks with their AST
+identifiers.
+
+The operations are deliberately a little bit sloppy here, creating empty / statement-less
+CFG nodes. Additionally, the current CFG construction algorithm doesn't group
+consecutive statements in a single notional basic block into one node.
+This makes graph construction much easier to define, and might save us the
+trouble of (when trying to find the CFG node for an AST node) doing
+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)
+
+/-- Bump the upper bound of a list of `Fin`s by adding the amount to their value. -/
+def List.finNatAdd {m : ℕ} (l : List (Fin m)) (n : ℕ) : List (Fin (n + m)) :=
+  l.map (Fin.natAdd n)
+
+/-- Bump the upper bound of a list of `Fin` pairs without changing their value. -/
+def List.finCastAddProd {n : ℕ} (l : List (Fin n × Fin n)) (m : ℕ) :
+    List (Fin (n + m) × Fin (n + m)) :=
+  l.map (fun e => (e.1.castAdd m, e.2.castAdd m))
+
+/-- Bump the upper bound of a list of `Fin` pairs by adding the amount to their value. -/
+def List.finNatAddProd {m : ℕ} (l : List (Fin m × Fin m)) (n : ℕ) :
+    List (Fin (n + m) × Fin (n + m)) :=
+  l.map (fun e => (e.1.natAdd n, e.2.natAdd n))
+
+namespace Spa
+
+/-- Graph with general (`α`-labeled) nodes. By using a tuple `Fin size → α`
+    and writing `edges` over the `Fin size`, guarantees all edges are between real nodes.
+
+    To make graph composition via operations not force a
+    [`alga`](https://hackage.haskell.org/package/algebraic-graphs)-style "connect"-based
+    algebra, explicitly defines `inputs` and `outputs`, which are the only nodes that
+    get connected when graphs are sequenced. This makes the graph construction
+    operations more naturally fit with how CFGs are created from `Stmt`s. -/
+structure GGraph (α : Type) where
+  size : ℕ
+  nodes : Fin size → α
+  edges : List (Fin size × Fin size)
+  inputs : List (Fin size)
+  outputs : List (Fin size)
+
+namespace GGraph
+
+variable {α β : Type}
+
+/-- An index (node) in the CFG. -/
+abbrev Index (g : GGraph α) : Type := Fin g.size
+
+/-- An edge in the CFG. -/
+abbrev Edge (g : GGraph α) : Type := g.Index × g.Index
+
+instance : Functor GGraph where
+  map {α β : Type} (f : α → β) (g : GGraph α) : GGraph β :=
+    { size := g.size,
+      nodes := f ∘ g.nodes
+      edges := g.edges,
+      inputs := g.inputs,
+      outputs := g.outputs }
+
+@[simp] lemma map_size (f : α → β) (g : GGraph α) : (f <$> g).size = g.size := rfl
+@[simp] lemma map_edges (f : α → β) (g : GGraph α) : (f <$> g).edges = g.edges := rfl
+@[simp] lemma map_inputs (f : α → β) (g : GGraph α) : (f <$> g).inputs = g.inputs := rfl
+@[simp] lemma map_outputs (f : α → β) (g : GGraph α) : (f <$> g).outputs = g.outputs := rfl
+
+/-- Overlay two graphs: create a new graph whose nodes and edges come from two
+    sub-graphs, without inserting any additional edges. Also combines the
+    input and output node sets. -/
+def overlay (g₁ g₂ : GGraph α) : GGraph α where
+  size := g₁.size + g₂.size
+  nodes := Fin.append g₁.nodes g₂.nodes
+  edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size
+  inputs := g₁.inputs.finCastAdd g₂.size ++ g₂.inputs.finNatAdd g₁.size
+  outputs := g₁.outputs.finCastAdd g₂.size ++ g₂.outputs.finNatAdd g₁.size
+
+@[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay
+
+/-- Sequence two CFGs: create a combined graph whose nodes and edges come
+    from two subgraphs, __and__ make all the outputs of the left graph have edges to
+    all the inputs of the right graph. By the semantics of CFGs, this
+    encodes the fact that code first traverses the basic blocks in theleft
+    graph, and does the same for the right graph. -/
+def sequence (g₁ g₂ : GGraph α) : GGraph α where
+  size := g₁.size + g₂.size
+  nodes := Fin.append g₁.nodes g₂.nodes
+  edges := g₁.edges.finCastAddProd g₂.size ++ g₂.edges.finNatAddProd g₁.size ++
+    (g₁.outputs.finCastAdd g₂.size).product (g₂.inputs.finNatAdd g₁.size)
+  inputs := g₁.inputs.finCastAdd g₂.size
+  outputs := g₂.outputs.finNatAdd g₁.size
+
+@[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence
+
+/-- When a graph `g` is wrapped in a `loop`, the index / node corresponding
+    to the input of the new loop. -/
+def loopIn (g : GGraph α) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
+
+/-- When a graph `g` is wrapped in a `loop`, the index / node corresponding
+    to the output of the new loop. -/
+def loopOut (g : GGraph α) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size
+
+/-- Creates a zero-or-more loop loop in the CFG: connects all the output
+    nodes of the CFG back to the graph's beginning, and also introduces a path
+    to a new ending node (see `loopOut`) which bypasses the entire graph.
+
+    Notably, both the new input (`loopIn`) and new output (`loopOut`)
+    nodes are necessary for correctness: adding a path from inputs to a
+    hypothetical no-op end node encodes something like "just the first statement is executed".
+    Similarly, just adding a path from a a hypothetical no-op beginning node
+    to the outputs encodes "just the last statement is executed".
+
+    This is technically sloppy (see module comment), but it's simple.
+-/
+def loop (g : GGraph (Option β)) : GGraph (Option β) where
+  size := 2 + g.size
+  nodes := Fin.append (fun _ : Fin 2 => none) g.nodes
+  edges := g.edges.finNatAddProd 2 ++
+    ((g.loopIn, ·) <$> g.inputs.finNatAdd 2)  ++
+    ((·, g.loopOut) <$> g.outputs.finNatAdd 2) ++
+    [(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)]
+  inputs := [g.loopIn]
+  outputs := [g.loopOut]
+
+@[simp] lemma loop_inputs (g : GGraph (Option β)) : (loop g).inputs = [g.loopIn] := rfl
+
+@[simp] lemma loop_outputs (g : GGraph (Option β)) : (loop g).outputs = [g.loopOut] := rfl
+
+/-- Creates a single-node graph whose node contains the given value. -/
+def singleton (a : α) : GGraph α where
+  size := 1
+  nodes := fun _ => a
+  edges := []
+  inputs := [0]
+  outputs := [0]
+
+/-- Creates a new graph with a single input and single output node. Useful to ensure there's
+    a single point of entry and single point of exit. -/
+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
+
+@[simp] lemma map_overlay (f : α → β) (g₁ g₂ : GGraph α) :
+    f<$> (g₁ ∙ g₂) = f <$> g₁ ∙ f <$> g₂ := by
+  rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
+  simp only [Functor.map, GGraph.overlay]
+  congr 1
+  funext i
+  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
+
+@[simp] lemma map_sequence (f : α → β) (g₁ g₂ : GGraph α) :
+    f <$> (g₁ ⤳ g₂) = (f <$> g₁) ⤳  (f <$> g₂) := by
+  rcases g₁ with ⟨n₁, nd₁, e₁, i₁, o₁⟩; rcases g₂ with ⟨n₂, nd₂, e₂, i₂, o₂⟩
+  simp only [Functor.map, GGraph.sequence]
+  congr 1
+  funext i
+  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
+
+@[simp] lemma map_loop (h : β → γ) (g : GGraph (Option β)) :
+    (Option.map h) <$> (loop g) = loop (Option.map h <$> g) := by
+  rcases g with ⟨n, nd, e, i, o⟩
+  simp only [Functor.map, GGraph.loop]
+  congr 1
+  funext i
+  refine Fin.addCases ?_ ?_ i <;> intro j <;> simp [Fin.append_left, Fin.append_right]
+
+@[simp] lemma map_wrap (h : β → γ) (g : GGraph (Option β)) :
+    (Option.map h) <$> wrap g = wrap (Option.map h <$> g) := by
+  simp [GGraph.wrap, GGraph.map_sequence, GGraph.map_singleton]
+
+/-! ### Embeddings
+
+Each composition operator includes its operands into the result via an index
+translation that preserves node payloads and edges. `Embed` captures exactly
+those two facts, so anything defined from `nodes` and `edges` (traces, node
+labels, …) can be transported along an embedding once, instead of once per
+operator.
+
+`Embed` is deliberately a structure rather than a class: for `g ⤳ g`, both the
+left and the right inclusion inhabit the same type `Embed g (g ⤳ g)`, so
+instance resolution could silently pick the wrong copy. Embeddings into a
+composed graph are non-canonical by design; a named witness says which
+inclusion is meant. -/
+
+/-- An embedding of graph `g` into graph `h`: an index translation that
+    preserves node payloads and edges. -/
+structure Embed (g h : GGraph α) where
+  f : g.Index → h.Index
+  nodes_eq : ∀ i, h.nodes (f i) = g.nodes i
+  edges_mem : ∀ {e : g.Edge}, e ∈ g.edges → (f e.1, f e.2) ∈ h.edges
+
+/-- Embeddings compose. -/
+def Embed.trans {g₁ g₂ g₃ : GGraph α} (e₁ : Embed g₁ g₂) (e₂ : Embed g₂ g₃) :
+    Embed g₁ g₃ where
+  f := e₂.f ∘ e₁.f
+  nodes_eq i := (e₂.nodes_eq (e₁.f i)).trans (e₁.nodes_eq i)
+  edges_mem he := e₂.edges_mem (e₁.edges_mem he)
+
+/-- The left operand's inclusion into a sequenced graph. -/
+def Embed.sequenceLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ⤳ g₂) where
+  f i := i.castAdd g₂.size
+  nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
+  edges_mem he := List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
+
+/-- The right operand's inclusion into a sequenced graph. -/
+def Embed.sequenceRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ⤳ g₂) where
+  f i := i.natAdd g₁.size
+  nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
+  edges_mem he := List.mem_append_left _ (List.mem_append_right _ (List.mem_map_of_mem _ he))
+
+/-- The left operand's inclusion into an overlaid graph. -/
+def Embed.overlayLeft (g₁ g₂ : GGraph α) : Embed g₁ (g₁ ∙ g₂) where
+  f i := i.castAdd g₂.size
+  nodes_eq i := Fin.append_left g₁.nodes g₂.nodes i
+  edges_mem he := List.mem_append_left _ (List.mem_map_of_mem _ he)
+
+/-- The right operand's inclusion into an overlaid graph. -/
+def Embed.overlayRight (g₁ g₂ : GGraph α) : Embed g₂ (g₁ ∙ g₂) where
+  f i := i.natAdd g₁.size
+  nodes_eq i := Fin.append_right g₁.nodes g₂.nodes i
+  edges_mem he := List.mem_append_right _ (List.mem_map_of_mem _ he)
+
+/-- The body's inclusion into a `loop` graph. -/
+def Embed.loop (g : GGraph (Option β)) : Embed g (loop g) where
+  f i := i.natAdd 2
+  nodes_eq i := Fin.append_right (fun _ : Fin 2 => none) g.nodes i
+  edges_mem he := List.mem_append_left _ (List.mem_append_left _
+    (List.mem_append_left _ (List.mem_map_of_mem _ he)))
+
+variable (g : GGraph α)
+
+/-- All the nodes in the graph. -/
+def indices : List g.Index := List.finRange g.size
+
+/-- All of the graph's indices are listed in `indices`. -/
+lemma mem_indices (idx : g.Index) : idx ∈ g.indices :=
+  List.mem_finRange idx
+
+/-- `indices` does not have duplicates. -/
+lemma nodup_indices : g.indices.Nodup :=
+  List.nodup_finRange g.size
+
+/-- Predecessors of a particular node in the graph. --/
+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}
+    (h : (idx₁, idx₂) ∈ g.edges) : idx₁ ∈ g.predecessors idx₂ :=
+  List.mem_filter.mpr ⟨g.mem_indices idx₁, by simpa using h⟩
+
+/-- A node is a predecessor of another node only if there's an
+    edge between them. -/
+lemma edge_of_mem_predecessors {idx₁ idx₂ : g.Index}
+    (h : idx₁ ∈ g.predecessors idx₂) : (idx₁, idx₂) ∈ g.edges := by
+  simpa using (List.mem_filter.mp h).2
+
+end GGraph
+
+/-- "Normal" graphs, for the purposes of the analyses in this
+    framework, have basic statements in their nodes, and nothing else. -/
+abbrev Graph : Type := GGraph (Option BasicStmt)
+
+namespace Graph
+
+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
+
+end Graph
+
+open Graph in
+def Stmt.cfg : Stmt → Graph
+  -- A basic statement goes into a single basic block
+  | .basic bs => singleton (some bs)
+  -- Sequencing of statements corresponds naturally to CFG sequencing
+  | .andThen s₁ s₂ => s₁.cfg ⤳  s₂.cfg
+  -- An if can execute either one branch or the other; overlap them.
+  -- Subsequent sequencing (etc.) will end up creating the forks and joins.
+  | .ifElse _ s₁ s₂ => s₁.cfg ∙ s₂.cfg
+  -- The `loop` construct was developed specifically for zero-or-more loops like this.
+  | .whileLoop _ s => loop s.cfg
+
+end Spa

lean/Spa/Language/Notation.lean

@@ -0,0 +1,60 @@
+import Spa.Language.Base
+
+namespace Spa
+
+/-!
+Scoped quotation syntax for writing object-language programs.
+
+`[obj_expr| … ]` builds an `Expr`, `[obj_stmt| … ]` builds a `Stmt`.
+
+Example:
+```
+[obj_stmt|
+  zero := 0;
+  pos  := zero + 1;
+  if pos { x := 1 } else { noop };
+  while x { x := x - 1 }
+]
+```
+-/
+
+/-- Expressions of the object language. -/
+declare_syntax_cat obj_expr
+
+syntax num                              : obj_expr
+syntax ident                           : obj_expr
+syntax:65 obj_expr:65 " + " obj_expr:66 : obj_expr
+syntax:65 obj_expr:65 " - " obj_expr:66 : obj_expr
+syntax "(" obj_expr ")"                 : obj_expr
+
+/-- Statements of the object language. -/
+declare_syntax_cat obj_stmt
+
+syntax "noop"                                          : obj_stmt
+syntax ident " := " obj_expr                           : obj_stmt
+syntax "if " obj_expr " { " obj_stmt " } " "else" " { " obj_stmt " } " : obj_stmt
+syntax "while " obj_expr " { " obj_stmt " } "          : obj_stmt
+syntax:50 obj_stmt:51 "; " obj_stmt:50                 : obj_stmt
+syntax "(" obj_stmt ")"                                : obj_stmt
+
+scoped syntax "[obj_expr| " obj_expr " ]" : term
+scoped syntax "[obj_stmt| " obj_stmt " ]" : term
+
+scoped macro_rules
+  | `([obj_expr| $n:num])        => `(Expr.num $n)
+  | `([obj_expr| $x:ident])      => `(Expr.var $(Lean.quote x.getId.toString))
+  | `([obj_expr| $a + $b])       => `(Expr.add [obj_expr| $a] [obj_expr| $b])
+  | `([obj_expr| $a - $b])       => `(Expr.sub [obj_expr| $a] [obj_expr| $b])
+  | `([obj_expr| ($e:obj_expr)]) => `([obj_expr| $e])
+
+scoped macro_rules
+  | `([obj_stmt| noop])           => `(Stmt.basic .noop)
+  | `([obj_stmt| $x:ident := $e]) =>
+      `(Stmt.basic (.assign $(Lean.quote x.getId.toString) [obj_expr| $e]))
+  | `([obj_stmt| $s₁ ; $s₂])      => `(Stmt.andThen [obj_stmt| $s₁] [obj_stmt| $s₂])
+  | `([obj_stmt| if $e { $s₁ } else { $s₂ }]) =>
+      `(Stmt.ifElse [obj_expr| $e] [obj_stmt| $s₁] [obj_stmt| $s₂])
+  | `([obj_stmt| while $e { $s }]) => `(Stmt.whileLoop [obj_expr| $e] [obj_stmt| $s])
+  | `([obj_stmt| ($s:obj_stmt)])  => `([obj_stmt| $s])
+
+end Spa

lean/Spa/Language/Program.lean

@@ -0,0 +1,77 @@
+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
+
+/-- 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

lean/Spa/Language/Properties.lean

@@ -0,0 +1,226 @@
+import Spa.Language.Traces
+
+/-!
+
+# Properties of the Object Language, CFGs, and Traces
+
+This module encodes some properties of the language, mostly those having to do
+with connecting the computational view (the `Spa.Graph`s, on which static
+analyses are executed) to the semantic view (such as `EvalStmt`, which
+encodes the expected formal behavior of the language). In particular,
+to prove that our computationally-implemented static analyses are correct,
+we need to show that our computational model of their execution (the CFG)
+matches the formal description. Thus, the key result `cfg_sufficient`.
+
+Many lemmas and definitions here aim are used to prove that result,
+by allowing inductive proofs on the construction of the CFG:
+the bits where we _build up_ the trace corresponding to each
+proof tree are exactly those when we have two graphs (through
+which traces exist) and we want to combine these graphs, while
+showing also that a combined trace exists as well. -/
+
+namespace Spa
+
+open Graph
+
+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) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.overlayLeft g₁ g₂)
+
+/-- When two graphs are overlaid, for each trace in the right graph,
+    a corresponding trace exists in the combined graph. -/
+noncomputable def Trace.overlay_right {idx₁ idx₂ : g₂.Index}
+    (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.overlayRight g₁ g₂)
+
+/-- When two graphs are sequenced, for each trace in the first graph,
+    a corresponding trace exists in the combined graph. -/
+noncomputable def Trace.sequence_left {idx₁ idx₂ : g₁.Index}
+    (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.sequenceLeft g₁ g₂)
+
+/-- When two graphs are sequenced, for each trace in the second graph,
+   a corresponding trace exists in the combined graph. -/
+noncomputable def Trace.sequence_right {idx₁ idx₂ : g₂.Index}
+    (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.sequenceRight g₁ g₂)
+
+/-- Equivalent of `Trace.overlay_left` for end-to-end traces. -/
+noncomputable def EndToEndTrace.overlay_left (etr : EndToEndTrace g₁ ρ₁ ρ₂) :
+    EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
+  exact ⟨i₁.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₁),
+         i₂.castAdd g₂.size, List.mem_append_left _ (List.mem_map_of_mem _ h₂),
+         tr.overlay_left⟩
+
+/-- Equivalent of `Trace.overlay_right` for end-to-end traces. -/
+noncomputable def EndToEndTrace.overlay_right (etr : EndToEndTrace g₂ ρ₁ ρ₂) :
+    EndToEndTrace (g₁ ∙ g₂) ρ₁ ρ₂ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
+  exact ⟨i₁.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₁),
+         i₂.natAdd g₁.size, List.mem_append_right _ (List.mem_map_of_mem _ h₂),
+         tr.overlay_right⟩
+
+/-- When two graphs are sequenced, two end-to-end traces through the respective
+    graphs can be sequenced to create an end-to-end trace in the combined
+    graph. This is only possible for end-to-end traces and not for general
+    `Trace`s, because sequencing only introduces edges from the output nodes
+    of one graph to the input nodes of another graph. A non-end-to-end trace
+    need to conclude at the output node, so it cannot necessarily be sequenced
+    with a trace in another graph. -/
+noncomputable def EndToEndTrace.concat {ρ₃ : Env} (etr₁ : EndToEndTrace g₁ ρ₁ ρ₂)
+    (etr₂ : EndToEndTrace g₂ ρ₂ ρ₃) : EndToEndTrace (g₁ ⤳ g₂) ρ₁ ρ₃ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
+  obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂
+  refine ⟨i₁.castAdd g₂.size, List.mem_map_of_mem _ h₁,
+          j₂.natAdd g₁.size, List.mem_map_of_mem _ k₂,
+          tr₁.sequence_left ++< ?_ >++ tr₂.sequence_right⟩
+  exact List.mem_append_right _
+    (List.mem_product.mpr ⟨List.mem_map_of_mem _ h₂, List.mem_map_of_mem _ k₁⟩)
+
+end Embeddings
+
+section Loop
+
+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) ρ₁ ρ₂ :=
+  tr.embed (GGraph.Embed.loop g)
+
+/-- The beginning node of a loop graph is empty. -/
+private lemma loop_nodes_at_in :
+    (Graph.loop g).nodes g.loopIn = none :=
+  Fin.append_left (fun _ : Fin 2 => none) g.nodes 0
+
+/-- The ending node of a loop graph is empty. -/
+private lemma loop_nodes_at_out :
+    (Graph.loop g).nodes g.loopOut = none :=
+  Fin.append_left (fun _ : Fin 2 => none) g.nodes 1
+
+/-- Equivlaent of `Trace.loop` for end-to-end traces. -/
+noncomputable def EndToEndTrace.loop (etr : EndToEndTrace g ρ₁ ρ₂) :
+    EndToEndTrace (Graph.loop g) ρ₁ ρ₂ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := etr
+  -- the edge in → (2 ↑ʳ i₁), reached through the second edge group
+  have hin : (g.loopIn, i₁.natAdd 2) ∈ (Graph.loop g).edges := by
+    refine List.mem_append_left _ (List.mem_append_left _ (List.mem_append_right _ ?_))
+    exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₁)
+  -- the edge (2 ↑ʳ i₂) → out, reached through the third edge group
+  have hout : (i₂.natAdd 2, g.loopOut) ∈ (Graph.loop g).edges := by
+    refine List.mem_append_left _ (List.mem_append_right _ ?_)
+    exact List.mem_map_of_mem _ (List.mem_map_of_mem _ h₂)
+  refine ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _, ?_⟩
+  exact Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none) ++< hin >++
+    tr.loop ++< hout >++ Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none)
+
+/-- The zero-or-more times loop has an edge to return back to the top, to continue after an iteration. -/
+private lemma loop_edge_out_in :
+    ((g.loopOut, g.loopIn) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges := by
+  refine List.mem_append_right _ ?_
+  exact List.mem_cons_self _ _
+
+/-- Two traces through a loop can be combined, since a loop can be executed any number of times. -/
+noncomputable def EndToEndTrace.loop_concat (etr₁ : EndToEndTrace (Graph.loop g) ρ₁ ρ₂)
+    (etr₂ : EndToEndTrace (Graph.loop g) ρ₂ ρ₃) :
+    EndToEndTrace (Graph.loop g) ρ₁ ρ₃ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr₁⟩ := etr₁
+  obtain ⟨j₁, k₁, j₂, k₂, tr₂⟩ := etr₂
+  simp only [Graph.loop_inputs, Graph.loop_outputs, List.mem_singleton] at h₁ h₂ k₁ k₂
+  subst h₁; subst h₂; subst k₁; subst k₂
+  exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
+    tr₁ ++< loop_edge_out_in >++ tr₂⟩
+
+/-- A loop can be executed zero times. -/
+noncomputable def EndToEndTrace.loop_empty {ρ : Env} : EndToEndTrace (Graph.loop g) ρ ρ := by
+  have hedge : ((g.loopIn, g.loopOut) : (Graph.loop g).Edge) ∈ (Graph.loop g).edges :=
+    List.mem_append_right _ (List.mem_cons_of_mem _ (List.mem_cons_self _ _))
+  exact ⟨g.loopIn, List.mem_singleton_self _, g.loopOut, List.mem_singleton_self _,
+    Trace.single (loop_nodes_at_in ▸ EvalBasicStmtOpt.none) ++< hedge >++
+      Trace.single (loop_nodes_at_out ▸ EvalBasicStmtOpt.none)⟩
+
+end Loop
+
+/-- A CFG consisting of only a single node has a trace through it corresponding to that node. -/
+noncomputable def EndToEndTrace.singleton {o : Option BasicStmt} {ρ₁ ρ₂ : Env}
+    (h : EvalBasicStmtOpt ρ₁ o ρ₂) : EndToEndTrace (Graph.singleton o) ρ₁ ρ₂ :=
+  ⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _,
+   Trace.single h⟩
+
+/-- If a CFG's only node is empty, the no-op trace exists through it. -/
+noncomputable def EndToEndTrace.singleton_nil (ρ : Env) :
+    EndToEndTrace (Graph.singleton none) ρ ρ :=
+  EndToEndTrace.singleton EvalBasicStmtOpt.none
+
+/-- Invoking 'Graph.wrap` (which ensures a single entry and exit node for a CFG)
+    does not invalidate traces in the original graph. -/
+noncomputable def EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
+    (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
+  (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
+
+/-- Key result: the control flow graph admits every execution that's made
+    possible by a language's semantics. Thus, the CFG encodes _at least_ all
+    semantically-possible executions. Informally, we can conclude from this
+    that if we compute a result that using the graph's edges to determine
+    what's possible, this result will not disagree with the semantics.
+
+    Note that a CFG like $K_4$ (where the nodes are basic blocks) is
+    technically also a sufficient graph, but is very likely meaningless in that
+    it grossly overestimates the possible execution paths in the language, and
+    thus is bound to produce less-than-specific results. There is as yet no
+    result in this framework that the CFG we produce is _minimal_: loosely,
+    posessing only edges for things that are admitted by the semantics.
+    This is difficult to state (in its strongest form, this would
+    require the CFG to be able to detect something like `while (alwaysFalse)`,
+    and so remains a TODO. -/
+noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
+    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace s.cfg ρ₁ ρ₂ := by
+  induction h with
+  | basic ρ₁ ρ₂ bs hbs =>
+    exact EndToEndTrace.singleton (EvalBasicStmtOpt.some hbs)
+  | andThen ρ₁ ρ₂ ρ₃ s₁ s₂ _ _ ih₁ ih₂ =>
+    exact ih₁.concat ih₂
+  | ifTrue ρ₁ ρ₂ e z s₁ s₂ _ _ _ ih =>
+    exact ih.overlay_left
+  | ifFalse ρ₁ ρ₂ e s₁ s₂ _ _ ih =>
+    exact ih.overlay_right
+  | whileTrue ρ₁ ρ₂ ρ₃ e z s _ _ _ _ ih₁ ih₂ =>
+    exact (ih₁.loop).loop_concat ih₂
+  | whileFalse ρ e s _ =>
+    exact EndToEndTrace.loop_empty
+
+namespace Program
+
+noncomputable def trace (p : Program) {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
+    Trace p.cfg p.initialState p.finalState [] ρ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h)
+  rw [Graph.wrap_inputs, List.mem_singleton] at h₁
+  rw [Graph.wrap_outputs, List.mem_singleton] at h₂
+  subst h₁; subst h₂
+  exact tr
+
+end Program
+
+
+end Spa

lean/Spa/Language/Semantics.lean

@@ -0,0 +1,99 @@
+import Spa.Language.Base
+import Spa.Lattice
+import Spa.Interp
+
+/-!
+
+# Operational Semantics
+
+This file contains the operational semantics for the object language defined in
+`Spa.Language.Base`. Right now, all values in the language are integers.
+The semantics are big-step, and lead to a fully constructed proof tree
+containing the derivation connecting the initial and final states.
+All pretty standard.
+
+-/
+
+namespace Spa
+
+/-- A value in the object language. Currently, the only possible case is
+    an integer. -/
+inductive Value where
+  | int (z : ℤ)
+  deriving DecidableEq
+
+/-- An environment mapping variables to their values. -/
+def Env : Type := List (String × Value)
+
+inductive Env.Mem : String × Value → Env → Prop
+  | here (s : String) (v : Value) (ρ : Env) : Env.Mem (s, v) ((s, v) :: ρ)
+  | there (s s' : String) (v v' : Value) (ρ : Env) :
+      ¬(s = s') → Env.Mem (s, v) ρ → Env.Mem (s, v) ((s', v') :: ρ)
+
+/-- 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)
+  | var (ρ : Env) (x : String) (v : Value) :
+      Env.Mem (x, v) ρ → EvalExpr ρ (.var x) v
+  | add (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) :
+      EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) →
+      EvalExpr ρ (.add e₁ e₂) (.int (z₁ + z₂))
+  | sub (ρ : Env) (e₁ e₂ : Expr) (z₁ z₂ : ℤ) :
+      EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) →
+      EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂))
+
+/-- Inference rules for evaluating a basic statement (`Spa.BasicStmt`) in
+    a given environment, potentially changing the environment.
+    Pretty standard big-step evaluation. -/
+inductive EvalBasicStmt : Env → BasicStmt → Env → Type
+  | noop (ρ : Env) : EvalBasicStmt ρ .noop ρ
+  | assign (ρ : Env) (x : String) (e : Expr) (v : Value) :
+      EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ)
+
+/-- Inference rules for evaluating a basic-statement-or-nothing,
+    which is the current representation of CFGs nodes. -/
+inductive EvalBasicStmtOpt : Env → Option BasicStmt → Env → Type
+  | none {ρ : Env} : EvalBasicStmtOpt ρ Option.none ρ
+  | some {ρ₁ ρ₂ : Env} {bs : BasicStmt} :
+      EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmtOpt ρ₁ (Option.some bs) ρ₂
+
+/-- Inference rules for evaluating statements (`Spa.Stmt`) in a given
+    environment, potentially changing the environment.
+    Pretty standard big-step evaluation. -/
+inductive EvalStmt : Env → Stmt → Env → Type
+  | basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) :
+      EvalBasicStmt ρ₁ bs ρ₂ → EvalStmt ρ₁ (.basic bs) ρ₂
+  | andThen (ρ₁ ρ₂ ρ₃ : Env) (s₁ s₂ : Stmt) :
+      EvalStmt ρ₁ s₁ ρ₂ → EvalStmt ρ₂ s₂ ρ₃ →
+      EvalStmt ρ₁ (.andThen s₁ s₂) ρ₃
+  | ifTrue (ρ₁ ρ₂ : Env) (e : Expr) (z : ℤ) (s₁ s₂ : Stmt) :
+      EvalExpr ρ₁ e (.int z) → ¬(z = 0) → EvalStmt ρ₁ s₁ ρ₂ →
+      EvalStmt ρ₁ (.ifElse e s₁ s₂) ρ₂
+  | ifFalse (ρ₁ ρ₂ : Env) (e : Expr) (s₁ s₂ : Stmt) :
+      EvalExpr ρ₁ e (.int 0) → EvalStmt ρ₁ s₂ ρ₂ →
+      EvalStmt ρ₁ (.ifElse e s₁ s₂) ρ₂
+  | whileTrue (ρ₁ ρ₂ ρ₃ : Env) (e : Expr) (z : ℤ) (s : Stmt) :
+      EvalExpr ρ₁ e (.int z) → ¬(z = 0) → EvalStmt ρ₁ s ρ₂ →
+      EvalStmt ρ₂ (.whileLoop e s) ρ₃ →
+      EvalStmt ρ₁ (.whileLoop e s) ρ₃
+  | whileFalse (ρ : Env) (e : Expr) (s : Stmt) :
+      EvalExpr ρ e (.int 0) →
+      EvalStmt ρ (.whileLoop e s) ρ
+
+/-- For the purpose of static analysis, lattices we define describe program
+    state, or better yet, they describe _values_ in the program.
+    This class should be provided by each analysis' lattice (see also `Spa/Analysis/Forward.lean`)
+    to describe what each lattice value means in terms of the language.
+
+    In addition to providing the interpretation (`Spa.Interp`), the lattice
+    combinators `⊔` and `⊓` must respect disjunction and conjunction respectively.
+    This is because possible paths through a control flow graph (`Spa/Language/Graphs.lean`),
+    are tied to lattice operations used by the analysis engine. -/
+class LatticeInterpretation (L : Type*) [Lattice L] extends Interp L (Value → Prop) where
+  interp_sup : ∀ {l₁ l₂ : L} (v : Value),
+    interp l₁ v ∨ interp l₂ v → interp (l₁ ⊔ l₂) v
+  interp_inf : ∀ {l₁ l₂ : L} (v : Value),
+    interp l₁ v ∧ interp l₂ v → interp (l₁ ⊓ l₂) v
+
+end Spa

lean/Spa/Language/Tagged/Basic.lean

@@ -0,0 +1,18 @@
+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

lean/Spa/Language/Tagged/DESCENDANT-TRACKING.md

@@ -0,0 +1,417 @@
+# Descendant tracking (parked)
+
+This is the formally-verified **interval-labeling / descendant** machinery that
+used to live in `Id.lean` and `Properties.lean`. It let you decide "is node `a`
+a descendant of node `b`?" with two integer comparisons on their identifiers,
+and *proved* that numeric test equivalent to structural subtree containment.
+
+It was removed because the descendant test is a *computational optimization*:
+the same question can be answered by walking the AST, and nothing in the current
+pipeline needs the fast test yet. The proofs (a rose-tree flattening + a
+postorder `Good` invariant) are a real mechanization cost to carry. Parked here
+so it can be restored verbatim when LICM actually wants it.
+
+## What stays in the live code
+
+- `NodeId` collapses to a single unique index (`{ post : ℕ }`); `tag` still
+  assigns each node a distinct postorder number.
+- The bidirectional mapping (`erase`/`tag` + `erase_tagStmt`) stays in
+  `Properties.lean`.
+- The labelled-CFG id↔state mapping (`Cfg.lean`) is independent of this and is
+  unaffected.
+
+## Revival checklist
+
+1. In `Id.lean`, give `NodeId` back its descendant-count field and the test:
+
+   ```lean
+   structure NodeId where
+     post : ℕ
+     desc : ℕ          -- number of proper descendants (subtree size − 1); leaf = 0
+     deriving DecidableEq, Repr
+
+   namespace NodeId
+
+   /-- Left endpoint of the node's postorder interval `[lo, post]`. -/
+   def lo (a : NodeId) : ℕ := a.post - a.desc
+
+   /-- `a` is a descendant-or-self of `b`: `a.post` lies in `b`'s interval. -/
+   def DescendantOf (a b : NodeId) : Prop := b.lo ≤ a.post ∧ a.post ≤ b.post
+
+   instance (a b : NodeId) : Decidable (DescendantOf a b) := by
+     unfold DescendantOf; infer_instance
+
+   end NodeId
+   ```
+
+2. In `Derive.lean`, make the generated `tag` store the descendant count again:
+   change the emitted identifier in `mkTag` from `(⟨$last⟩ : $nId)` back to
+   `(⟨$last, $last - n⟩ : $nId)`.
+
+3. Paste the Lean block below back into `Properties.lean` (after the round-trip
+   theorems). It builds against the `id.lo = lo`-premise form of `Good` and the
+   childcount (`desc`) identifier. The headline result is
+   `descendant_iff_tagStmt`; everything else is supporting machinery.
+
+## The parked proofs
+
+```lean
+/-- A rose tree of identifiers: the uniform shape underlying all three tagged
+AST types, used to reason about the postorder labeling generically. -/
+inductive IdTree where
+  | node (id : NodeId) (children : List IdTree)
+
+namespace IdTree
+
+def rootId : IdTree → NodeId
+  | .node id _ => id
+
+@[simp] theorem rootId_node (id : NodeId) (cs : List IdTree) :
+    (IdTree.node id cs).rootId = id := rfl
+
+mutual
+def subtrees : IdTree → List IdTree
+  | .node id cs => .node id cs :: subtreesList cs
+def subtreesList : List IdTree → List IdTree
+  | [] => []
+  | c :: cs => subtrees c ++ subtreesList cs
+end
+
+@[simp] theorem subtrees_node (id : NodeId) (cs : List IdTree) :
+    subtrees (.node id cs) = .node id cs :: subtreesList cs := rfl
+
+@[simp] theorem subtreesList_nil : subtreesList [] = [] := rfl
+
+@[simp] theorem subtreesList_cons (c : IdTree) (cs : List IdTree) :
+    subtreesList (c :: cs) = subtrees c ++ subtreesList cs := rfl
+
+def posts (t : IdTree) : List ℕ := (subtrees t).map (fun s => s.rootId.post)
+
+def postsList (cs : List IdTree) : List ℕ := (subtreesList cs).map (fun s => s.rootId.post)
+
+@[simp] theorem posts_node (id : NodeId) (cs : List IdTree) :
+    posts (.node id cs) = id.post :: postsList cs := rfl
+
+@[simp] theorem postsList_nil : postsList [] = [] := rfl
+
+@[simp] theorem postsList_cons (c : IdTree) (cs : List IdTree) :
+    postsList (c :: cs) = posts c ++ postsList cs := by
+  simp [posts, postsList]
+
+end IdTree
+
+def Expr.Tagged.toIdTree : Expr.Tagged NodeId → IdTree
+  | .add t a b => .node t [a.toIdTree, b.toIdTree]
+  | .sub t a b => .node t [a.toIdTree, b.toIdTree]
+  | .var t _ => .node t []
+  | .num t _ => .node t []
+
+def BasicStmt.Tagged.toIdTree : BasicStmt.Tagged NodeId → IdTree
+  | .assign t _ e => .node t [e.toIdTree]
+  | .noop t => .node t []
+
+def Stmt.Tagged.toIdTree : Stmt.Tagged NodeId → IdTree
+  | .basic t bs => .node t [bs.toIdTree]
+  | .andThen t a b => .node t [a.toIdTree, b.toIdTree]
+  | .ifElse t e a b => .node t [e.toIdTree, a.toIdTree, b.toIdTree]
+  | .whileLoop t e s => .node t [e.toIdTree, s.toIdTree]
+
+mutual
+inductive Good : ℕ → IdTree → Prop
+  | mk {lo : ℕ} {id : NodeId} {cs : List IdTree} :
+      id.lo = lo → GoodChildren lo cs id.post →
+      Good lo (.node id cs)
+inductive GoodChildren : ℕ → List IdTree → ℕ → Prop
+  | nil {pos : ℕ} : GoodChildren pos [] pos
+  | cons {cur : ℕ} {c : IdTree} {cs : List IdTree} {pos : ℕ} :
+      Good cur c → GoodChildren (c.rootId.post + 1) cs pos →
+      GoodChildren cur (c :: cs) pos
+end
+
+theorem Good.lo_le_post {lo : ℕ} {t : IdTree} (h : Good lo t) : lo ≤ t.rootId.post := by
+  cases h with
+  | mk hlo _ => simp only [NodeId.lo] at hlo; simp only [IdTree.rootId_node]; omega
+
+theorem GoodChildren.cur_le_pos : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
+    GoodChildren cur cs pos → cur ≤ pos
+  | _, [], _, h => by cases h; exact le_rfl
+  | _, c :: cs, _, h => by
+      cases h with
+      | cons hc hcs =>
+        have := hc.lo_le_post
+        have := GoodChildren.cur_le_pos cs hcs
+        omega
+
+mutual
+theorem Good.mem_posts : ∀ {lo : ℕ} (t : IdTree), Good lo t →
+    ∀ x, x ∈ IdTree.posts t ↔ lo ≤ x ∧ x ≤ t.rootId.post
+  | _, .node id cs, h, x => by
+      cases h with
+      | mk hlo hch =>
+        simp only [IdTree.posts_node, List.mem_cons, IdTree.rootId_node]
+        rw [GoodChildren.mem_postsList cs hch x]
+        simp only [NodeId.lo] at hlo
+        omega
+theorem GoodChildren.mem_postsList : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
+    GoodChildren cur cs pos → ∀ x, x ∈ IdTree.postsList cs ↔ cur ≤ x ∧ x < pos
+  | _, [], _, h, x => by
+      cases h
+      simp only [IdTree.postsList_nil]
+      constructor
+      · intro hx; exact absurd hx (List.not_mem_nil x)
+      · rintro ⟨h1, h2⟩; exfalso; omega
+  | _, c :: cs, _, h, x => by
+      cases h with
+      | cons hc hcs =>
+        simp only [IdTree.postsList_cons, List.mem_append]
+        rw [Good.mem_posts c hc x, GoodChildren.mem_postsList cs hcs x]
+        have := hc.lo_le_post
+        have := GoodChildren.cur_le_pos cs hcs
+        omega
+end
+
+mutual
+theorem Good.nodup_posts : ∀ {lo : ℕ} (t : IdTree), Good lo t → (IdTree.posts t).Nodup
+  | _, .node id cs, h => by
+      cases h with
+      | mk hlo hch =>
+        simp only [IdTree.posts_node, List.nodup_cons]
+        refine ⟨?_, GoodChildren.nodup_postsList cs hch⟩
+        intro hmem
+        rw [GoodChildren.mem_postsList cs hch id.post] at hmem
+        omega
+theorem GoodChildren.nodup_postsList : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
+    GoodChildren cur cs pos → (IdTree.postsList cs).Nodup
+  | _, [], _, h => by cases h; simp only [IdTree.postsList_nil, List.nodup_nil]
+  | _, c :: cs, _, h => by
+      cases h with
+      | cons hc hcs =>
+        simp only [IdTree.postsList_cons, List.nodup_append]
+        refine ⟨Good.nodup_posts c hc, GoodChildren.nodup_postsList cs hcs, ?_⟩
+        intro x hx1 hx2
+        rw [Good.mem_posts c hc x] at hx1
+        rw [GoodChildren.mem_postsList cs hcs x] at hx2
+        omega
+end
+
+mutual
+theorem Good.subtree_good : ∀ {lo : ℕ} (t : IdTree), Good lo t →
+    ∀ s ∈ IdTree.subtrees t, Good s.rootId.lo s
+  | _, .node id cs, h, s, hs => by
+      cases h with
+      | mk hlo hch =>
+        rw [IdTree.subtrees_node, List.mem_cons] at hs
+        rcases hs with rfl | hs
+        · simp only [IdTree.rootId_node]; rw [hlo]; exact Good.mk hlo hch
+        · exact GoodChildren.subtree_good cs hch s hs
+theorem GoodChildren.subtree_good : ∀ {cur : ℕ} (cs : List IdTree) {pos : ℕ},
+    GoodChildren cur cs pos → ∀ s ∈ IdTree.subtreesList cs, Good s.rootId.lo s
+  | _, [], _, _, s, hs => by simp only [IdTree.subtreesList_nil, List.not_mem_nil] at hs
+  | _, c :: cs, _, h, s, hs => by
+      cases h with
+      | cons hc hcs =>
+        rw [IdTree.subtreesList_cons, List.mem_append] at hs
+        rcases hs with hs | hs
+        · exact Good.subtree_good c hc s hs
+        · exact GoodChildren.subtree_good cs hcs s hs
+end
+
+mutual
+theorem IdTree.subtrees_subset : ∀ (t : IdTree) {b : IdTree},
+    b ∈ subtrees t → subtrees b ⊆ subtrees t
+  | .node id cs, b, hb => by
+      rw [subtrees_node, List.mem_cons] at hb
+      rcases hb with rfl | hb
+      · exact fun _ h => h
+      · intro x hx
+        rw [subtrees_node, List.mem_cons]
+        exact Or.inr (IdTree.subtreesList_subset cs hb hx)
+theorem IdTree.subtreesList_subset : ∀ (cs : List IdTree) {b : IdTree},
+    b ∈ subtreesList cs → subtrees b ⊆ subtreesList cs
+  | [], b, hb => by simp only [subtreesList_nil, List.not_mem_nil] at hb
+  | c :: cs, b, hb => by
+      rw [subtreesList_cons, List.mem_append] at hb
+      intro x hx
+      rw [subtreesList_cons, List.mem_append]
+      rcases hb with hb | hb
+      · exact Or.inl (IdTree.subtrees_subset c hb hx)
+      · exact Or.inr (IdTree.subtreesList_subset cs hb hx)
+end
+
+theorem IdTree.eq_of_post_eq {l : List IdTree}
+    (h : (l.map (fun s => s.rootId.post)).Nodup) {a c : IdTree}
+    (ha : a ∈ l) (hc : c ∈ l) (hpost : a.rootId.post = c.rootId.post) : a = c := by
+  induction l with
+  | nil => exact absurd ha (List.not_mem_nil a)
+  | cons d ds ih =>
+    simp only [List.map_cons, List.nodup_cons] at h
+    obtain ⟨hd, htl⟩ := h
+    simp only [List.mem_cons] at ha hc
+    rcases ha with rfl | ha <;> rcases hc with rfl | hc
+    · rfl
+    · exfalso; apply hd; rw [hpost]; exact List.mem_map_of_mem _ hc
+    · exfalso; apply hd; rw [← hpost]; exact List.mem_map_of_mem _ ha
+    · exact ih htl ha hc
+
+theorem descendant_iff_of_good {lo : ℕ} {t : IdTree} (hg : Good lo t)
+    {a b : IdTree} (ha : a ∈ IdTree.subtrees t) (hb : b ∈ IdTree.subtrees t) :
+    a.rootId.DescendantOf b.rootId ↔ a ∈ IdTree.subtrees b := by
+  have hgb : Good b.rootId.lo b := Good.subtree_good t hg b hb
+  constructor
+  · rintro ⟨h1, h2⟩
+    have hmem : a.rootId.post ∈ IdTree.posts b := by
+      rw [Good.mem_posts b hgb a.rootId.post]; exact ⟨h1, h2⟩
+    rw [IdTree.posts, List.mem_map] at hmem
+    obtain ⟨c, hc_mem, hc_post⟩ := hmem
+    have hc_t : c ∈ IdTree.subtrees t := IdTree.subtrees_subset t hb hc_mem
+    have hac : a = c :=
+      IdTree.eq_of_post_eq (hg.nodup_posts t) ha hc_t hc_post.symm
+    rw [hac]; exact hc_mem
+  · intro hsub
+    have hmem : a.rootId.post ∈ IdTree.posts b := by
+      rw [IdTree.posts, List.mem_map]; exact ⟨a, hsub, rfl⟩
+    rw [Good.mem_posts b hgb a.rootId.post] at hmem
+    exact hmem
+
+/-! ### Tagging produces a good tree
+
+We bridge from the `tag` traversal to the abstract `Good` invariant, by induction
+on the plain AST.  Each lemma also records that the returned counter is one past
+the root's postorder index. -/
+
+theorem Expr.tag_spec : ∀ (e : Expr) (n : ℕ),
+    Good n (e.tag n).1.toIdTree ∧ (e.tag n).1.toIdTree.rootId.post + 1 = (e.tag n).2 := by
+  intro e
+  induction e with
+  | num k =>
+      intro n
+      refine ⟨?_, ?_⟩
+      · simp only [Expr.tag, Expr.Tagged.toIdTree]
+        exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
+      · simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
+  | var x =>
+      intro n
+      refine ⟨?_, ?_⟩
+      · simp only [Expr.tag, Expr.Tagged.toIdTree]
+        exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
+      · simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
+  | add a b iha ihb =>
+      intro n
+      obtain ⟨gA, pA⟩ := iha n
+      obtain ⟨gB, pB⟩ := ihb (a.tag n).2
+      have lA := gA.lo_le_post
+      have lB := gB.lo_le_post
+      refine ⟨?_, ?_⟩
+      · simp only [Expr.tag, Expr.Tagged.toIdTree]
+        refine Good.mk ?_ ?_
+        · simp only [NodeId.lo]; omega
+        · refine GoodChildren.cons gA ?_
+          rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
+      · simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
+  | sub a b iha ihb =>
+      intro n
+      obtain ⟨gA, pA⟩ := iha n
+      obtain ⟨gB, pB⟩ := ihb (a.tag n).2
+      have lA := gA.lo_le_post
+      have lB := gB.lo_le_post
+      refine ⟨?_, ?_⟩
+      · simp only [Expr.tag, Expr.Tagged.toIdTree]
+        refine Good.mk ?_ ?_
+        · simp only [NodeId.lo]; omega
+        · refine GoodChildren.cons gA ?_
+          rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
+      · simp only [Expr.tag, Expr.Tagged.toIdTree, IdTree.rootId_node]
+
+theorem BasicStmt.tag_spec : ∀ (bs : BasicStmt) (n : ℕ),
+    Good n (bs.tag n).1.toIdTree ∧ (bs.tag n).1.toIdTree.rootId.post + 1 = (bs.tag n).2 := by
+  intro bs
+  cases bs with
+  | noop =>
+      intro n
+      refine ⟨?_, ?_⟩
+      · simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree]
+        exact Good.mk (by simp only [NodeId.lo]; omega) GoodChildren.nil
+      · simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree, IdTree.rootId_node]
+  | assign x e =>
+      intro n
+      obtain ⟨gE, pE⟩ := Expr.tag_spec e n
+      have lE := gE.lo_le_post
+      refine ⟨?_, ?_⟩
+      · simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree]
+        refine Good.mk ?_ ?_
+        · simp only [NodeId.lo]; omega
+        · refine GoodChildren.cons gE ?_
+          rw [pE]; exact GoodChildren.nil
+      · simp only [BasicStmt.tag, BasicStmt.Tagged.toIdTree, IdTree.rootId_node]
+
+theorem Stmt.tag_spec : ∀ (s : Stmt) (n : ℕ),
+    Good n (s.tag n).1.toIdTree ∧ (s.tag n).1.toIdTree.rootId.post + 1 = (s.tag n).2 := by
+  intro s
+  induction s with
+  | basic bs =>
+      intro n
+      obtain ⟨gBs, pBs⟩ := BasicStmt.tag_spec bs n
+      have lBs := gBs.lo_le_post
+      refine ⟨?_, ?_⟩
+      · simp only [Stmt.tag, Stmt.Tagged.toIdTree]
+        refine Good.mk ?_ ?_
+        · simp only [NodeId.lo]; omega
+        · refine GoodChildren.cons gBs ?_
+          rw [pBs]; exact GoodChildren.nil
+      · simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
+  | andThen a b iha ihb =>
+      intro n
+      obtain ⟨gA, pA⟩ := iha n
+      obtain ⟨gB, pB⟩ := ihb (a.tag n).2
+      have lA := gA.lo_le_post
+      have lB := gB.lo_le_post
+      refine ⟨?_, ?_⟩
+      · simp only [Stmt.tag, Stmt.Tagged.toIdTree]
+        refine Good.mk ?_ ?_
+        · simp only [NodeId.lo]; omega
+        · refine GoodChildren.cons gA ?_
+          rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
+      · simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
+  | ifElse e a b iha ihb =>
+      intro n
+      obtain ⟨gE, pE⟩ := Expr.tag_spec e n
+      obtain ⟨gA, pA⟩ := iha (e.tag n).2
+      obtain ⟨gB, pB⟩ := ihb (a.tag (e.tag n).2).2
+      have lE := gE.lo_le_post
+      have lA := gA.lo_le_post
+      have lB := gB.lo_le_post
+      refine ⟨?_, ?_⟩
+      · simp only [Stmt.tag, Stmt.Tagged.toIdTree]
+        refine Good.mk ?_ ?_
+        · simp only [NodeId.lo]; omega
+        · refine GoodChildren.cons gE ?_
+          rw [pE]; refine GoodChildren.cons gA ?_
+          rw [pA]; refine GoodChildren.cons gB ?_; rw [pB]; exact GoodChildren.nil
+      · simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
+  | whileLoop e s ih =>
+      intro n
+      obtain ⟨gE, pE⟩ := Expr.tag_spec e n
+      obtain ⟨gS, pS⟩ := ih (e.tag n).2
+      have lE := gE.lo_le_post
+      have lS := gS.lo_le_post
+      refine ⟨?_, ?_⟩
+      · simp only [Stmt.tag, Stmt.Tagged.toIdTree]
+        refine Good.mk ?_ ?_
+        · simp only [NodeId.lo]; omega
+        · refine GoodChildren.cons gE ?_
+          rw [pE]; refine GoodChildren.cons gS ?_; rw [pS]; exact GoodChildren.nil
+      · simp only [Stmt.tag, Stmt.Tagged.toIdTree, IdTree.rootId_node]
+
+/-- A freshly tagged program is a well-tagged tree (rooted at postorder start `0`). -/
+theorem good_tagStmt (s : Stmt) : Good 0 (tagStmt s).toIdTree :=
+  (Stmt.tag_spec s 0).1
+
+/-- **Descendant characterization.** The numeric `NodeId.DescendantOf` relation on
+two nodes of a tagged program holds exactly when one is structurally contained in
+the other's subtree. -/
+theorem descendant_iff_tagStmt (s : Stmt) {a b : IdTree}
+    (ha : a ∈ IdTree.subtrees (tagStmt s).toIdTree)
+    (hb : b ∈ IdTree.subtrees (tagStmt s).toIdTree) :
+    a.rootId.DescendantOf b.rootId ↔ a ∈ IdTree.subtrees b :=
+  descendant_iff_of_good (good_tagStmt s) ha hb
+```

lean/Spa/Language/Tagged/Derive.lean

@@ -0,0 +1,509 @@
+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

lean/Spa/Language/Tagged/Graphs.lean

@@ -0,0 +1,104 @@
+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

lean/Spa/Language/Tagged/Id.lean

@@ -0,0 +1,9 @@
+import Mathlib.Data.Nat.Notation
+
+namespace Spa
+
+structure RawId where
+  post : ℕ
+  deriving DecidableEq, Repr
+
+end Spa

lean/Spa/Language/Tagged/Properties.lean

@@ -0,0 +1,29 @@
+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

lean/Spa/Language/Tagged/TODO.md

@@ -0,0 +1,46 @@
+# Tagged AST — follow-ups
+
+## Descendant tracking — parked
+
+The interval-labeling descendant test and its correctness proof
+(`descendant_iff_tagStmt` and supporting rose-tree/`Good` machinery) have been
+removed from the live code and parked in `DESCENDANT-TRACKING.md`, with a revival
+checklist. It's a computational optimization not yet needed; revive it (and the
+`NodeId.desc` field) when LICM wants fast ancestor queries.
+
+## ID → CFG-state mapping — plan part B — DONE
+
+`Graphs.lean` now defines a payload-generic `GGraph α` (with `Graph := GGraph
+(List BasicStmt)` as the concrete CFG), so the labelled CFG **reuses** the graph
+combinators instead of mirroring them. In `Cfg.lean`:
+`buildCfgL : Stmt.Tagged NodeId → GGraph (List (BasicStmt.Tagged NodeId))` is just
+`buildCfg` at the tagged payload; `buildCfgL_graph :
+(buildCfgL t).map (List.map erase) = buildCfg t.erase` connects it to the real
+CFG; and `GGraph.nodeLabel`/`GGraph.stateOf` read a node's id straight from its
+payload (`stateOf_label` is the soundness). No `LGraph`, no separate `label`
+field, no duplicated combinators.
+
+## ID → CFG-state mapping — totality — DONE
+
+The `Option`-valued `nodeIdOf`/`stateOfNodeId` are now proven total on the inputs
+that matter (`Graphs.lean`), via a payload-list characterization of the CFG:
+
+- `GGraph.nodeList` flattens `nodes` into the list of payloads, with combinator
+  lemmas (`nodeList_comp/link/loop/wrap`) reducing it through the CFG builders.
+- `Stmt.Tagged.basics` lists a program's basic statements; the master lemma
+  `Stmt.Tagged.cfg_nodeList_filter` (and its program-level
+  `taggedCfg_nodeList_filter`) shows the non-empty CFG nodes are *exactly* the
+  singletons `[bs]` for `bs ∈ basics`.
+- AST ⇒ CFG: `exists_state_of_mem_basics` (a state with payload `[bs]`) and
+  `stateOfNodeId_isSome` (the search succeeds).
+- CFG ⇒ AST: `exists_basic_of_code_ne_nil` (a non-empty node is `[bs]`, with
+  `code = [bs.erase]` and `nodeIdOf = some bs.rootTag`) and `nodeIdOf_isSome`.
+
+All `propext`/`Quot.sound`-only (no `sorry`, no choice).
+
+Remaining nice-to-have:
+- Injectivity: distinct basic-statement ids map to distinct states, giving a
+  two-sided id ↔ state correspondence (upgrading the existence results above to a
+  genuine bijection, and pinning `stateOfNodeId (bs.rootTag)` to *the* state
+  holding `bs`). The `tag`-uniqueness fact this needs (`Nodup` of postorder tags)
+  was part of the parked descendant machinery in `DESCENDANT-TRACKING.md`.

lean/Spa/Language/Traces.lean

@@ -0,0 +1,266 @@
+import Spa.Language.Semantics
+import Spa.Language.Graphs
+import Spa.Language.Program
+
+/-!
+
+# Program Traces
+
+This module defines program traces tied to Control Flow Graphs, or CFGs
+(see `Spa.GGraph` and `Spa.Graph`). These traces boil town to sequences of
+basic-block executions (really, `Spa.BasicStmt` executions), each of which must
+have an actual basic block in the graph _and_ be connected to the previous
+basic block by an edge. In this way, traces encode executions admitted
+by the CFG.
+
+While the regular `Trace` is just _any_ path through the graph, an
+`EndToEndTrace` is a path from the entry node to the exit node, denoting
+full program execution.
+
+Properties about graphs and language semantics (especially,
+the fact that the graph contains the proper basic block and edges
+to represent any program execution according to the
+language's big-step semantics `EvalStmt`) is found
+in `Spa/Language/Properties.lean`.
+
+-/
+
+namespace Spa
+
+/-- A partial trace through a graph `g`, starting right before
+    the execution of the basic block at the first index, and
+    ending right after the execution of the basic block at the last index. -/
+inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type
+  | single {ρ₁ ρ₂ : Env} {idx : g.Index} :
+      EvalBasicStmtOpt ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
+  | edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} :
+      EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
+      Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
+
+/-!
+
+## 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. -/
+def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
+    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
+    (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
+    Trace g idx₁ idx₄ ρ₁ ρ₃ :=
+  match tr₁ with
+  | single hbs => edge hbs he tr₂
+  | edge hbs he' tr₁' => edge hbs he' (tr₁'.concat he tr₂)
+
+scoped notation:65 tr₁:66 " ++< " he " >++ " tr₂:65 => Trace.concat tr₁ he tr₂
+
+def Trace.addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ : Env} :
+    Trace g idx₁ idx₂ ρ₁ ρ₂ →
+    (idx₂, idx₃) ∈ g.edges →
+    Traceₗ g idx₁ idx₃ ρ₁ ρ₂
+  | .single hnode, hedge => .cons hnode hedge .nil
+  | .edge hnode hedge' rest, hedge => .cons hnode hedge' (rest.addEdge hedge)
+
+@[aesop simp]
+def Traceₗ.append {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
+    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → Traceₗ g idx₂ idx₃ ρ₂ ρ₃ →
+    Traceₗ g idx₁ idx₃ ρ₁ ρ₃
+  | .nil, rhs => rhs
+  | .cons hnode hedge rest, rhs => .cons hnode hedge (rest.append rhs)
+
+@[simp] def traceₗ_append_nil {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env}
+    {trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂} : trₗ.append Traceₗ.nil = trₗ := by
+  induction trₗ <;> aesop
+
+def Traceₗ.appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
+    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → Trace g idx₂ idx₃ ρ₂ ρ₃ →
+    Trace g idx₁ idx₃ ρ₁ ρ₃
+  | .nil, rhs => rhs
+  | .cons hnode hedge rest, rhs => .edge hnode hedge (rest.appendTrace rhs)
+
+def Traceₗ.appendStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
+    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃ →
+    Trace g idx₁ idx₂ ρ₁ ρ₃ := fun trₗ hbs => trₗ.appendTrace (Trace.single hbs)
+
+def Trace.appendRight {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
+    Trace g idx₁ idx₂ ρ₁ ρ₂ → Traceᵣ g idx₂ idx₃ ρ₂ ρ₃ →
+    Trace g idx₁ idx₃ ρ₁ ρ₃
+  | lhs, .nil => lhs
+  | lhs, .cons rest hedge hnode => Trace.concat (lhs.appendRight rest) hedge (.single hnode)
+
+instance instHAppendTraceLTraceL {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
+    HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (Traceₗ g idx₂ idx₃ ρ₂ ρ₃) (Traceₗ g idx₁ idx₃ ρ₁ ρ₃) where
+  hAppend := Traceₗ.append
+
+instance instHAppendTraceLTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
+    HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (Trace g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where
+  hAppend := Traceₗ.appendTrace
+
+instance instHAppendTraceLStep {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
+    HAppend (Traceₗ g idx₁ idx₂ ρ₁ ρ₂) (EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) (Trace g idx₁ idx₂ ρ₁ ρ₃) where
+  hAppend := Traceₗ.appendStep
+
+instance instHAppendTraceTraceR {g : Graph} {idx₁ idx₂ idx₃ : g.Index} {ρ₁ ρ₂ ρ₃ : Env} :
+    HAppend (Trace g idx₁ idx₂ ρ₁ ρ₂) (Traceᵣ g idx₂ idx₃ ρ₂ ρ₃) (Trace g idx₁ idx₃ ρ₁ ρ₃) where
+  hAppend := Trace.appendRight
+
+/-!
+
+## Trace Steps
+
+Analyses that care about *which statements executed* (e.g. reaching
+definitions) need to project a trace down to its list of executed statements.
+Defining that projection here, once, as a chronological mathlib `List` means
+all the re-association facts about concatenating traces come for free from
+`List.append_assoc` and friends, instead of being re-proven per analysis. -/
+
+/-- The (index, statement) pairs executed by a single optional-statement step:
+    none if the node is empty, and the node's statement otherwise. -/
+def EvalBasicStmtOpt.steps {α : Type*} (idx : α) {ρ₁ ρ₂ : Env} {obs : Option BasicStmt} :
+    EvalBasicStmtOpt ρ₁ obs ρ₂ → List (α × BasicStmt)
+  | .none => []
+  | .some (bs := bs) _ => [(idx, bs)]
+
+/-- The statements executed by a left-open trace, in chronological order. -/
+def Traceₗ.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
+    Traceₗ g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
+  | .nil => []
+  | .cons (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
+
+/-- The statements executed by a trace, in chronological order. -/
+def Trace.steps {g : Graph} {idx₁ idx₂ : g.Index} {ρ₁ ρ₂ : Env} :
+    Trace g idx₁ idx₂ ρ₁ ρ₂ → List (g.Index × BasicStmt)
+  | .single (idx := idx) hnode => hnode.steps idx
+  | .edge (idx₁ := idx) hnode _ rest => hnode.steps idx ++ rest.steps
+
+@[simp] lemma Traceₗ.steps_append {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
+    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
+    (tr₂ : Traceₗ g idx₂ idx₃ ρ₂ ρ₃) :
+    (tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
+  show (tr₁.append tr₂).steps = _
+  induction tr₁ <;> simp [Traceₗ.append, Traceₗ.steps, *]
+
+@[simp] lemma Traceₗ.steps_appendTrace {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
+    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
+    (tr₂ : Trace g idx₂ idx₃ ρ₂ ρ₃) :
+    (tr₁ ++ tr₂).steps = tr₁.steps ++ tr₂.steps := by
+  show (tr₁.appendTrace tr₂).steps = _
+  induction tr₁ <;> simp [Traceₗ.appendTrace, Traceₗ.steps, Trace.steps, *]
+
+@[simp] lemma Traceₗ.steps_appendStep {g : Graph} {idx₁ idx₂ : g.Index}
+    {ρ₁ ρ₂ ρ₃ : Env} (tr : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
+    (hbs : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃) :
+    (tr ++ hbs).steps = tr.steps ++ hbs.steps idx₂ :=
+  Traceₗ.steps_appendTrace tr (Trace.single hbs)
+
+@[simp] lemma Trace.steps_addEdge {g : Graph} {idx₁ idx₂ idx₃ : g.Index}
+    {ρ₁ ρ₂ : Env} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂)
+    (hedge : (idx₂, idx₃) ∈ g.edges) :
+    (tr.addEdge hedge).steps = tr.steps := by
+  induction tr <;> simp [Trace.addEdge, Trace.steps, Traceₗ.steps, *]
+
+@[simp] lemma Traceₗ.append_addEdge {g : Graph}
+    {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env}
+    (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
+    (hnode : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃)
+    (hedge : (idx₂, idx₃) ∈ g.edges)
+    (rest : Traceₗ g idx₃ idx₄ ρ₃ ρ₄) :
+    trₗ.append (Traceₗ.cons hnode hedge rest) =
+      (Trace.addEdge (trₗ.appendStep hnode) hedge).append rest := by
+  induction trₗ <;> simp [Traceₗ.append, Traceₗ.appendStep, Traceₗ.appendTrace, Trace.addEdge, *]
+
+@[simp] lemma Traceₗ.appendTrace_addEdge {g : Graph}
+    {idx₁ idx₂ idx₃ idx₄ : g.Index} {ρ₁ ρ₂ ρ₃ ρ₄ : Env}
+    (trₗ : Traceₗ g idx₁ idx₂ ρ₁ ρ₂)
+    (hnode : EvalBasicStmtOpt ρ₂ (g.nodes idx₂) ρ₃)
+    (hedge : (idx₂, idx₃) ∈ g.edges)
+    (rest : Trace g idx₃ idx₄ ρ₃ ρ₄) :
+    trₗ.appendTrace (Trace.edge hnode hedge rest) =
+      (Trace.addEdge (trₗ.appendStep hnode) hedge).appendTrace rest := by
+  induction trₗ <;> simp [Traceₗ.appendTrace, Traceₗ.appendStep, Trace.addEdge, *]
+
+/-- A beginning-to-end trace corresponding to the CFG `g`. -/
+inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type
+  | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs)
+      (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs)
+      (trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂
+
+inductive Reaches {prog : Program} : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
+    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ →
+    (s : prog.State) → (ρin ρout : Env) → Type
+  | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
+      Reaches (.single hnode) s₁ ρ₁ ρ₂
+  | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
+      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) :
+      Reaches (.edge hnode hedge rest) s₁ ρ₁ ρ₂
+  | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
+      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃)
+      {s : prog.State} {ρin ρout : Env} :
+      Reaches rest s ρin ρout →
+      Reaches (.edge hnode hedge rest) s ρin ρout
+
+def Reaches.pre {prog : Program} {s₁ s₂ s: prog.State}
+    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
+    (r : Reaches tr s ρin ρout) → Traceₗ prog.cfg s₁ s ρ₁ ρin
+  | .single_here _ => .nil
+  | .edge_here _ _ _ => .nil
+  | .edge_there hnode hedge _ r => .cons hnode hedge r.pre
+
+def Reaches.post {prog : Program} {s₁ s₂ s: prog.State}
+    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
+    (r : Reaches tr s ρin ρout) → Trace prog.cfg s₁ s ρ₁ ρout
+  | .single_here hnode => .single hnode
+  | .edge_here hnode _ _ => .single hnode
+  | .edge_there hnode hedge _ r => .edge hnode hedge r.post
+
+def Reaches.first {prog : Program} {s₁ s₂ s: prog.State}
+    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
+    (r : Reaches tr s ρin ρout) → Σ ρ₁', Reaches tr s₁ ρ₁ ρ₁'
+  | .single_here hnode => ⟨_, .single_here hnode⟩
+  | .edge_here hnode hedge hrest => ⟨_, .edge_here hnode hedge hrest⟩
+  | .edge_there hnode hedge hrest tmp' => ⟨_, .edge_here hnode hedge hrest⟩
+
+def Reaches.step {prog : Program} {s₁ s₂ s: prog.State}
+    {ρ₁ ρ₂ ρin ρout : Env} {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂} :
+    (r : Reaches tr s ρin ρout) → EvalBasicStmtOpt ρin (prog.code s) ρout
+  | .single_here hnode => hnode
+  | .edge_here hnode hedge hrest => hnode
+  | .edge_there hnode hedge hrest tmp' => tmp'.step
+
+
+end Spa

lean/Spa/Lattice.lean

@@ -0,0 +1,152 @@
+import Mathlib.Order.Lattice
+import Mathlib.Order.RelSeries
+
+/-!
+
+# Lattice Definitions
+
+This file provides some definitions for lattices. It used to be more critical
+when this was an Agda project, since it defined (semi)lattices, the ordering
+relation, etc. However, these have been lifted into `Mathlib.Order.Lattice`
+etc.. What remains are a couple of theorems about folds, as well
+as `FiniteHeightLattice`, the core concept of lattice-based static
+program analyses. See the documentation on that class for more information. -/
+
+namespace Option
+
+/-- Equality-sensitive eliminator for options in which the `some` case
+    is sensitive to the base `β`. This makes it mirror a one-element fold
+    more closely. -/
+def elimEq {α : Type*} {β : Sort*} :
+    (o : Option α) → β → ((a : α) → o = some a → β → β) → β
+  | none, b, _ => b
+  | some a, b, f => f a rfl b
+
+end Option
+
+namespace Spa
+
+/-- Predicate for binary functions independently monotone in both their arguments. -/
+def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
+    (f : α → β → γ) : Prop :=
+  (∀ b, Monotone (f · b)) ∧ (∀ a, Monotone (f a ·))
+
+section Folds
+
+variable {α β : Type*} [Preorder α] [Preorder β]
+
+/-- (right) folds are monotonic in both their arguments if the underlying accumulator function is. -/
+lemma foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
+    (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
+    (hf₁ : ∀ b, Monotone (f · b)) (hf₂ : ∀ a, Monotone (f a ·)) :
+    l₁.foldr f b₁ ≤ l₂.foldr f b₂ := by
+  induction hl with
+  | nil => exact hb
+  | cons hxy _ ih =>
+    exact le_trans (hf₁ _ hxy) (hf₂ _ ih)
+
+/-- (left) folds are monotinic in both their arguments if the underlying accumulator function is. -/
+lemma foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
+    (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
+    (hf₁ : ∀ a, Monotone (f · a)) (hf₂ : ∀ b, Monotone (f b ·)) :
+    l₁.foldl f b₁ ≤ l₂.foldl f b₂ := by
+  induction hl generalizing b₁ b₂ with
+  | nil => exact hb
+  | cons hxy _ ih =>
+    exact ih (le_trans (hf₁ _ hb) (hf₂ _ hxy))
+
+omit [Preorder α] in
+/-- (right) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
+lemma foldr_mono' (l : List α) (f : α → β → β)
+    (hf : ∀ a, Monotone (f a ·)) : Monotone (l.foldr f ·) := by
+  intro b₁ b₂ hb
+  induction l with
+  | nil => exact hb
+  | cons x xs ih => exact hf x ih
+
+omit [Preorder α] in
+/-- (left) folds on a particular list are monotonic if the underlying accumulator is monotonic in its accumulator argument. -/
+lemma foldl_mono' (l : List α) (f : β → α → β)
+    (hf : ∀ a, Monotone (f · a)) : Monotone fun b => l.foldl f b := by
+  intro b₁ b₂ hb
+  induction l generalizing b₁ b₂ with
+  | nil => exact hb
+  | cons x xs ih => exact ih (hf x hb)
+
+omit [Preorder α] in
+/-- The equality-aware eliminator (that also alters its behavior dependent on base case)
+    for option is monotonic. -/
+lemma elimEq_self_mono (o : Option α) (g : (a : α) → o = some a → β → β)
+    (hg : ∀ a h, Monotone (g a h)) :
+    Monotone (o.elimEq · g) := by
+  cases o with
+  | none => exact monotone_id
+  | some a => exact hg a rfl
+
+end Folds
+
+/-- Predicate on types with `Preorder` that claims all $<$ chains in the type have at most `n` comparisons. -/
+def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
+  ∀ c : LTSeries α, c.length ≤ n
+
+/-- Since a singleton type's preorder has no nonempty `<` chains,
+    they are vacuously bounded by any minimum height. -/
+lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
+    (n : ℕ) : BoundedChains α n := fun c => by
+  by_contra hc
+  push_neg at hc
+  exact (c.step ⟨0, by omega⟩).ne (Subsingleton.elim _ _)
+
+/-- A finite height lattice is a lattice in which all chains $a < \ldots < z$ have a maximum height `height`. -/
+class FiniteHeightLattice (α : Type*) extends Lattice α, OrderBot α, OrderTop α where
+  height : ℕ
+  chains_bounded : BoundedChains α height
+
+-- a < ... < z
+-- ----------- length <= height
+
+namespace FiniteHeightLattice
+
+/-- This is something like a lemma about isomorphic types having the same height.
+    Given a finite-height lattice `α`, lattice `β`, and a `Monotone` bijection
+    between the two, we can show that lattice `β` also has a finite height.
+
+    The proof is fairly trivial: any chain in `β` can be transported to a chain in `α`,
+    and must be bounded by the same height by `FiniteHeightLattice.chains_bounded`. -/
+def transport {α β : Type*} [Lattice β]
+    [I : FiniteHeightLattice α] (f : α → β) (g : β → α)
+    (hf : Monotone f) (hg : Monotone g)
+    (hfg : Function.LeftInverse f g) :
+    FiniteHeightLattice β where
+  toLattice := inferInstance
+  toOrderBot := {
+    bot := f (⊥ : α)
+    bot_le := fun b => by
+      rw [← hfg b]
+      exact hf (_root_.bot_le : (⊥ : α) ≤ g b) }
+  toOrderTop := {
+    top := f (⊤ : α)
+    le_top := fun b => by
+      rw [← hfg b]
+      exact hf (_root_.le_top : g b ≤ (⊤ : α)) }
+  height := I.height
+  chains_bounded := fun c =>
+    I.chains_bounded (c.map g (hg.strictMono_of_injective hfg.injective))
+
+/-- A `Unique` lattice trivially has finite height: its only chain is the singleton
+    `[default]`, and there are no nontrivial `<` chains in a subsingleton. -/
+def ofUnique (α : Type*) [Lattice α] [Unique α] :
+    FiniteHeightLattice α where
+  toLattice := inferInstance
+  toOrderBot := {
+    bot := default
+    bot_le := fun _ => le_of_eq (Subsingleton.elim _ _) }
+  toOrderTop := {
+    top := default
+    le_top := fun _ => le_of_eq (Subsingleton.elim _ _) }
+  height := 0
+  chains_bounded := boundedChains_of_subsingleton α 0
+
+end FiniteHeightLattice
+
+end Spa

lean/Spa/Lattice/AboveBelow.lean

@@ -0,0 +1,191 @@
+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
+  | mk (x : α)
+  deriving DecidableEq
+
+namespace AboveBelow
+
+instance {α : Type*} [ToString α] : ToString (AboveBelow α) where
+  toString
+    | bot => "⊥"
+    | top => "⊤"
+    | mk x => toString x
+
+variable {α : Type*} [DecidableEq α]
+
+instance : Max (AboveBelow α) where
+  max
+    | bot, x => x
+    | top, _ => top
+    | mk x, mk y => if x = y then mk x else top
+    | mk x, bot => mk x
+    | mk _, top => top
+
+instance : Min (AboveBelow α) where
+  min
+    | bot, _ => bot
+    | top, x => x
+    | mk x, mk y => if x = y then mk x else bot
+    | mk _, bot => bot
+    | mk x, top => mk x
+
+@[simp] lemma bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
+@[simp] lemma top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
+@[simp] lemma sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
+@[simp] lemma sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
+@[simp] lemma mk_sup_mk (x y : α) :
+    (mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl
+
+@[simp] lemma bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
+@[simp] lemma top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
+@[simp] lemma inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
+@[simp] lemma inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
+@[simp] lemma mk_inf_mk (x y : α) :
+    (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
+
+protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by aesop
+protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by aesop
+protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by aesop
+protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by aesop
+protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by aesop
+protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by aesop
+
+instance : Lattice (AboveBelow α) :=
+  Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc
+    AboveBelow.inf_comm AboveBelow.inf_assoc
+    AboveBelow.sup_inf_self AboveBelow.inf_sup_self
+
+lemma le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
+
+lemma bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
+  le_iff.mpr (bot_sup a)
+
+lemma le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
+  le_iff.mpr (sup_top a)
+
+instance : OrderBot (AboveBelow α) where
+  bot := bot
+  bot_le := bot_le'
+
+instance : OrderTop (AboveBelow α) where
+  top := top
+  le_top := le_top'
+
+lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lt_of_le_of_ne (bot_le' _) (by simp)
+lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top := lt_of_le_of_ne (le_top' _) (by simp)
+lemma bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp)
+
+lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
+    a = bot ∨ b = top ∨ a = b := by
+  rw [le_iff] at h
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp_all
+
+/-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤`
+    (against any non-`⊥` argument), it is monotone in both arguments.
+    The values of the the elements in `α` are irrelevant since they
+    are always incomparable. This makes it easy to prove monotonicity
+    for operations that "just" combine their flat elements, or give up. -/
+lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
+    (f : AboveBelow α → AboveBelow β → AboveBelow γ)
+    (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
+    (htopl : ∀ y, y ≠ bot → f top y = top)
+    (htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
+  constructor <;> intro c a b hab <;>
+    rcases eq_or_ne c bot with rfl | hc <;>
+    rcases le_cases hab with rfl | rfl | rfl <;>
+    simp [hbotl, hbotr, htopl, htopr, bot_le', le_top', *]
+
+section Interp
+
+variable {V : Type*} {P : AboveBelow α → V → Prop}
+
+/-- As long as the interpretation of a the above-below lattice respects the
+    fact that `bot` means "impossible", interpreting the above-below
+    lattice agrees with its `⊔`. -/
+lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by aesop
+
+/-- As long as two distinct values in the flat domain don't overlap,
+    interpreting the above-below lattice agrees with its `⊔` -/
+lemma interp_inf_of
+    (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
+  rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> simp_all
+  split
+  · exact h.2
+  · next hne => exact (hdisj hne v h.1 h.2).elim
+
+end Interp
+
+/-- synthetic rank of an element, used to prove chain bounds. -/
+private def rank : AboveBelow α → ℕ
+  | bot => 0
+  | mk _ => 1
+  | top => 2
+
+/-- It's not possible for any two lifted flat-domain elements to be less
+    than one another. -/
+lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
+  intro h
+  obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
+  rcases le_cases hle with h | h | h <;> simp_all
+
+/-- The rank of elements is strictly monotonic. -/
+lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
+  intro a b hab
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
+    simp_all [rank, not_mk_lt_mk, (bot_le' _).not_lt, (le_top' _).not_lt]
+
+/-- All chains in the above-below lattice have at most 2 comparisons. -/
+lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
+  have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
+  rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
+  have h2 : rank c.last ≤ 2 := by cases c.last <;> simp [rank]
+  omega
+
+instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
+  toLattice := inferInstance
+  toOrderBot := inferInstance
+  toOrderTop := inferInstance
+  height := 2
+  chains_bounded := boundedChains
+
+end AboveBelow
+
+end Spa

lean/Spa/Lattice/Bool.lean

@@ -0,0 +1,39 @@
+import Spa.Lattice
+import Mathlib.Order.BooleanAlgebra
+
+namespace Spa
+
+/-! ### `Bool` as a finite-height lattice
+
+`Bool` is the two-element lattice `false ≤ true` (with `⊥ = false`, `⊤ = true`).
+It is the building block of the "power set" lattice `FiniteMap A Bool ks`, used by
+the reaching-definitions analysis to represent sets of definition sites. -/
+
+namespace Bool
+
+/-- Rank of a boolean: `false ↦ 0`, `true ↦ 1`. Used to bound chains, mirroring
+`AboveBelow.rank`. -/
+def rank : Bool → ℕ
+  | false => 0
+  | true => 1
+
+lemma rank_strictMono : StrictMono rank := by
+  intro a b hab
+  cases a <;> cases b <;> revert hab <;> decide
+
+lemma boundedChains : BoundedChains Bool 1 := 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
+  have h2 : rank c.last ≤ 1 := by cases c.last <;> simp [rank]
+  omega
+
+instance : FiniteHeightLattice Bool where
+  toLattice := inferInstance
+  toOrderBot := inferInstance
+  toOrderTop := inferInstance
+  height := 1
+  chains_bounded := boundedChains
+
+end Bool
+
+end Spa

lean/Spa/Lattice/FiniteMap.lean

@@ -0,0 +1,214 @@
+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
+
+/-- 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 {α β : Type*} {ks : List α}
+
+instance [Lattice β] : Lattice (FiniteMap α β ks) :=
+  inferInstanceAs (Lattice (Fin ks.length → β))
+
+instance [FiniteHeightLattice β] : FiniteHeightLattice (FiniteMap α β ks) :=
+  inferInstanceAs (FiniteHeightLattice (Fin ks.length → β))
+
+instance [DecidableEq β] : DecidableEq (FiniteMap α β ks) :=
+  inferInstanceAs (DecidableEq (Fin ks.length → β))
+
+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 α β ks} {p : α × β} :
+    p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl
+
+def MemKey (k : α) (_fm : FiniteMap α β ks) : Prop := k ∈ ks
+
+lemma MemKey_iff {k : α} {fm : FiniteMap α β ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
+
+instance {k : α} {fm : FiniteMap α β ks} [DecidableEq α] : Decidable (MemKey k fm) :=
+  decidable_of_iff _ MemKey_iff.symm
+
+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 α β ks) : List (α × β) :=
+  (List.finRange ks.length).map fun i => (ks.get i, fm i)
+
+lemma le_def [Lattice β] {fm₁ fm₂ : FiniteMap α β ks} :
+    fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl
+
+section Locate
+
+variable [DecidableEq α]
+
+/-- Recover the value stored under a present key. -/
+def locate {k : α} {fm : FiniteMap α β ks} (h : MemKey k fm) :
+    {v : β // (k, v) ∈ fm} :=
+  let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩
+  ⟨fm i, i, List.idxOf_get _, rfl⟩
+
+end Locate
+
+variable [Lattice β]
+
+lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap α β ks}
+    (hle : fm₁ ≤ fm₂) {k : α} {v₁ v₂ : β}
+    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
+  obtain ⟨i, hi, rfl⟩ := h₁
+  obtain ⟨j, hj, rfl⟩ := h₂
+  have hij : i = j := hks.get_inj_iff.mp (hi.trans hj.symm)
+  subst hij
+  exact le_def.mp hle i
+
+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 α β 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⟩⟩
+
+section Updating
+
+variable [DecidableEq α]
+
+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 β] in
+lemma eq_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
+    {ks' : List α} {g : α → β} (hk : k ∈ ks')
+    (h : (k, v) ∈ updating fm ks' g) : v = g k := by
+  obtain ⟨i, hi, rfl⟩ := h
+  show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k
+  rw [if_pos (by rw [hi]; exact hk), hi]
+
+omit [Lattice β] in
+lemma mem_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
+    {ks' : List α} {g : α → β} (hk : k ∉ ks')
+    (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
+  obtain ⟨i, hi, rfl⟩ := h
+  refine ⟨i, hi, ?_⟩
+  show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
+  rw [if_neg (by rw [hi]; exact hk)]
+
+lemma updating_mono {fm₁ fm₂ : FiniteMap α β ks} {ks' : List α}
+    {g₁ g₂ : α → β} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
+    updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
+  rw [le_def]
+  intro i
+  show (if ks.get i ∈ ks' then g₁ (ks.get i) else fm₁ i)
+     ≤ (if ks.get i ∈ ks' then g₂ (ks.get i) else fm₂ i)
+  split
+  · exact hg (ks.get i)
+  · exact le_def.mp hfm i
+
+end Updating
+
+section GeneralizedUpdate
+
+variable [DecidableEq α] {L : Type*} [Lattice L]
+
+def generalizedUpdate (f : L → FiniteMap α β ks) (g : α → L → β)
+    (ks' : List α) : L → FiniteMap α β ks := fun l =>
+  (f l).updating ks' (fun k => g k l)
+
+variable {f : L → FiniteMap α β 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 β] [Lattice L] in
+lemma generalizedUpdate_mem_eq {k : α} {v : β} {l : L} (hk : k ∈ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
+  eq_of_mem_updating (g := fun k => g k l) hk h
+
+omit [Lattice β] [Lattice L] in
+lemma generalizedUpdate_not_mem_backward {k : α} {v : β} {l : L} (hk : k ∉ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l :=
+  mem_of_mem_updating hk h
+
+end GeneralizedUpdate
+
+section ValuesAt
+
+variable [DecidableEq α]
+
+/-- The value stored under `k`, if `k` is a key. -/
+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 α β ks) (ks' : List α) : List β :=
+  ks'.filterMap fm.lookup
+
+omit [Lattice β] in
+lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap α β ks} {k : α} {v : β}
+    {ks' : List α} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
+  refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
+  obtain ⟨i, hi, rfl⟩ := h
+  have hik : ks.get i = k := hi
+  have hmem : k ∈ ks := hik ▸ ks.get_mem i
+  show (if h : k ∈ ks then
+          some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none) = some (fm i)
+  rw [dif_pos hmem]
+  have : (⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr hmem⟩ : Fin ks.length) = i :=
+    hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
+  rw [this]
+
+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)
+    (if h : k ∈ ks then some (fm₂ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
+  by_cases hk : k ∈ ks
+  · 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 α β ks} (hle : fm₁ ≤ fm₂)
+    (ks' : List α) :
+    List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
+  induction ks' with
+  | nil => exact List.Forall₂.nil
+  | cons k ks'' ih =>
+    have hrel := lookup_rel hle k
+    rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
+    revert hrel
+    generalize fm₁.lookup k = o₁
+    generalize fm₂.lookup k = o₂
+    intro hrel
+    cases hrel with
+    | none => simpa [valuesAt] using ih
+    | some hv => exact List.Forall₂.cons hv (by simpa [valuesAt] using ih)
+
+end ValuesAt
+
+end FiniteMap
+
+end Spa

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

lean/Spa/Lattice/Tuple.lean

@@ -0,0 +1,128 @@
+import Spa.Lattice
+import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
+/-!
+
+# Finite Tuple Lattices
+
+This file provides a proof that, in addition to being a lattice, the function
+space `Fin n → β` is itself a `Spa.FiniteHeightLattice` if the element type
+`β` is a lattice.
+
+Finite tuple lattices are the workhorse behind `FiniteMap`, whose carrier is
+`Fin ks.length → β`.
+
+The proof proceeds by "unzipping" a chain (`LTSeries`):
+
+$$
+(a_1, b_1, c_1) < \ldots < (a_1, b_1, c_o) < \ldots < (a_1, b_m, c_o) <
+  \ldots < (a_n, b_m, c_o)
+$$
+
+In which, at each step, at least one of the components must have increased
+(otherwise, the chain is not striclty increasing), into `n` chains
+(`LTSeries`).
+
+$$
+\begin{aligned}
+a_1 < \ldots < a_n \\
+b_1 < \ldots < b_m \
+c_1 < \ldots < c_o \
+\end{aligned}
+$$
+
+Because at least one of the two "unzipped" chains grows with each element of
+the product chain, the full chain length can't exceed the sum of the
+components. By the definition of finite height, these two chains are bounded,
+and therefore, the product chain is bounded too. -/
+
+namespace Spa
+
+namespace Tuple
+
+variable {β : Type*}
+
+section Unzip
+
+variable [PartialOrder β]
+
+open Classical in -- chain bounds are in Prop, so classical helps here.
+/-- The generalized unzip: any chain in `Fin n → β` decomposes into a family of
+    per-tuple-coordinate chains in `β`, agreeing with the original at each end, whose
+    lengths sum to an upper bound on the original chain's length. -/
+lemma exists_unzip {n : ℕ} (c : LTSeries (Fin n → β)) :
+    ∃ cs : Fin n → LTSeries β,
+      (∀ i, (cs i).head = c.head i) ∧ (∀ i, (cs i).last = c.last i) ∧
+      c.length ≤ ∑ i, (cs i).length := by
+  suffices H : ∀ (m : ℕ) (c : LTSeries (Fin n → β)), c.length = m →
+      ∃ cs : Fin n → LTSeries β,
+        (∀ i, (cs i).head = c.head i) ∧ (∀ i, (cs i).last = c.last i) ∧
+        c.length ≤ ∑ i, (cs i).length from H c.length c rfl
+  intro m
+  induction m with
+  | zero =>
+    intro c hn
+    have hlast : (Fin.last c.length) = 0 := by ext; simp [hn]
+    have hhl : c.last = c.head := by rw [RelSeries.last, RelSeries.head, hlast]
+    refine ⟨fun i => RelSeries.singleton _ (c.head i), fun i => ?_, fun i => ?_, ?_⟩
+    · exact RelSeries.head_singleton _
+    · rw [RelSeries.last_singleton, hhl]
+    · simp [hn, RelSeries.singleton]
+  | succ m ih =>
+    intro c hn
+    have h0 : c.length ≠ 0 := by omega
+    haveI : NeZero c.length := ⟨h0⟩
+    obtain ⟨cs', hh', hl', hlen'⟩ := ih (c.tail h0) (by rw [RelSeries.tail_length]; omega)
+    have hstep : c.head < c 1 := c.strictMono Fin.one_pos'
+    obtain ⟨hle, j, hjlt⟩ := Pi.lt_def.mp hstep
+    have hh'1 : ∀ i, (cs' i).head = c 1 i := fun i => by rw [hh' i, RelSeries.head_tail]
+    refine ⟨fun i =>
+        if hlt : c.head i < c 1 i then
+          (cs' i).cons (c.head i) (by rw [hh'1 i]; exact hlt)
+        else cs' i,
+      fun i => ?_, fun i => ?_, ?_⟩
+    · by_cases hlt : c.head i < c 1 i
+      · simp only [dif_pos hlt, RelSeries.head_cons]
+      · simp only [dif_neg hlt]
+        rw [hh'1 i]
+        exact ((lt_or_eq_of_le (hle i)).resolve_left hlt).symm
+    · by_cases hlt : c.head i < c 1 i
+      · simp only [dif_pos hlt, RelSeries.last_cons, hl' i, RelSeries.last_tail]
+      · simp only [dif_neg hlt, hl' i, RelSeries.last_tail]
+    · calc c.length
+          = (c.tail h0).length + 1 := by rw [RelSeries.tail_length]; omega
+        _ ≤ (∑ i, (cs' i).length) + 1 := Nat.add_le_add_right hlen' 1
+        _ ≤ ∑ i, (if hlt : c.head i < c 1 i then
+              (cs' i).cons (c.head i) (by rw [hh'1 i]; exact hlt) else cs' i).length :=
+          Nat.succ_le_of_lt (Finset.sum_lt_sum (fun i _ => by
+              split
+              · rw [RelSeries.cons_length]; omega
+              · exact le_rfl)
+            ⟨j, Finset.mem_univ j, by rw [dif_pos hjlt, RelSeries.cons_length]; omega⟩)
+
+end Unzip
+
+section FiniteHeight
+
+variable [FiniteHeightLattice β]
+
+instance instFiniteHeight {n : ℕ} : FiniteHeightLattice (Fin n → β) where
+  toLattice := inferInstance
+  toOrderBot := inferInstance
+  toOrderTop := inferInstance
+  height := n * FiniteHeightLattice.height (α := β)
+  chains_bounded := fun c => by
+    obtain ⟨cs, _, _, hbound⟩ := exists_unzip c
+    refine hbound.trans ?_
+    calc ∑ i, (cs i).length
+        ≤ ∑ _i : Fin n, FiniteHeightLattice.height (α := β) :=
+          Finset.sum_le_sum (fun i _ => FiniteHeightLattice.chains_bounded (cs i))
+      _ = n * FiniteHeightLattice.height (α := β) := by
+          simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin]
+
+end FiniteHeight
+
+end Tuple
+
+end Spa

lean/Spa/Lattice/Unit.lean

@@ -0,0 +1,14 @@
+import Spa.Lattice
+
+/-!
+
+# Unit Lattice
+
+This file provides a proof that in addition to being a lattice,
+`PUnit` is a `Spa.FiniteHeightLattice`. This is a fairly trivial result. -/
+
+namespace Spa
+
+instance : FiniteHeightLattice PUnit := FiniteHeightLattice.ofUnique PUnit
+
+end Spa

lean/Spa/Showable.lean

@@ -0,0 +1,37 @@
+import Spa.Lattice.FiniteMap
+import Spa.Lattice.AboveBelow
+
+namespace Spa
+
+class Showable (α : Type*) where
+  show' : α → String
+
+export Showable (show')
+
+instance : Showable String := ⟨fun s => "\"" ++ s ++ "\""⟩
+
+instance : Showable ℕ := ⟨toString⟩
+
+instance : Showable ℤ := ⟨toString⟩
+
+instance {n : ℕ} : Showable (Fin n) := ⟨fun i => toString i.val⟩
+
+instance {α β : Type*} [Showable α] [Showable β] : Showable (α × β) :=
+  ⟨fun p => "(" ++ show' p.1 ++ ", " ++ show' p.2 ++ ")"⟩
+
+instance : Showable PUnit := ⟨fun _ => "()"⟩
+
+instance {α : Type*} [Showable α] : Showable (AboveBelow α) :=
+  ⟨fun
+    | .bot => "⊥"
+    | .top => "⊤"
+    | .mk x => show' x⟩
+
+instance {α β : Type*} {ks : List α} [Showable α] [Showable β] :
+    Showable (FiniteMap α β ks) :=
+  ⟨fun fm =>
+    "{" ++ (FiniteMap.toList fm).foldr
+        (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
+        ++ "}"⟩
+
+end Spa

lean/Spa/Transformation/Licm.lean

@@ -0,0 +1,102 @@
+import Spa.Analysis.Reaching
+import Spa.Language.Tagged.Graphs
+
+/-!
+# Finding loop-invariant assignments (LICM groundwork)
+
+This wires the **reaching-definitions** analysis (`Spa/Analysis/Reaching.lean`)
+to the **tagged AST** to *find* — not yet move — assignments inside a `while`
+loop whose right-hand side depends only on definitions made *outside* the loop.
+These are the candidates a later LICM pass could hoist.
+
+The pipeline, for each assignment immediately enclosed by a loop:
+
+1. locate its CFG state via the tagged-graph bridge (`Program.stateOfNodeId`);
+2. read the reaching definitions at the assignment's *entry*
+   (`joinForKey s result` — the join over predecessors, i.e. before the
+   assignment itself runs);
+3. union the definition sets of the RHS variables;
+4. map each definition site back to its `RawId` (`Program.nodeIdOf`) and check
+   it is **not** inside the loop body (structural `subtreeIds` membership).
+
+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
+reaching definitions outside the loop"); transitive/iterated invariance and the
+actual hoisting are out of scope here.
+-/
+
+namespace Spa
+
+namespace LicmTransformation
+
+open Forward
+
+/-- An assignment found inside a loop, paired with the data needed to test its
+invariance against that (immediately enclosing) loop. -/
+structure Candidate (prog : Program) where
+  /-- The enclosing `whileLoop`'s tag (for reporting). -/
+  loopId : prog.NodeId
+  /-- Every node id inside the loop body (the "is-child-of-loop" set). -/
+  bodyIds : List prog.NodeId
+  /-- The assignment `BasicStmt`'s tag — what labels its CFG node. -/
+  assignId : prog.NodeId
+  /-- The variables read by the assignment's RHS. -/
+  rhsVars : List String
+
+/-- Collect every assignment together with its *immediately enclosing* loop.
+`enclosing` carries the current loop's tag and body id-set, or `none` outside any
+loop (in which case assignments are skipped — only in-loop assignments are
+candidates). -/
+def collectCandidates (prog : Program) (enc : Option (prog.NodeId × List prog.NodeId)) :
+    Stmt.Tagged prog.NodeId → List (Candidate prog)
+  | .basic _ bs =>
+      match bs, enc with
+      | .assign t _ e, some (loopId, bodyIds) =>
+          [{ loopId := loopId, bodyIds := bodyIds, assignId := t,
+             rhsVars := e.erase.vars.sort (· ≤ ·) }]
+      | _, _ => []
+  | .andThen _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
+  | .ifElse _ _ a b => collectCandidates prog enc a ++ collectCandidates prog enc b
+  | .whileLoop loopT _ body =>
+      collectCandidates prog (some (loopT, body.subtreeIds)) body
+
+/-- 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`. With the
+`Finset`-of-AST-ids lattice these are just the elements of the set. -/
+def defSites (prog : Program) (d : DefSet prog) : List prog.NodeId :=
+  (List.finRange prog.size).filter (fun i => decide (i ∈ d))
+
+/-- Is the candidate assignment loop-invariant: do all reaching definitions of
+its RHS variables lie outside the loop body? Reaching sets are now keyed by AST
+node id, so we compare against the loop-body ids directly (embedding the raw
+body ids into `p.NodeId`). -/
+def isInvariant (prog : Program) (c : Candidate prog) : Bool :=
+  match prog.stateOfNodeId c.assignId with
+  | none => false
+  | some s =>
+      let entry := joinForKey s (result (DefSet prog) prog)
+      let combined : DefSet prog :=
+        c.rhsVars.foldl (fun acc k => acc ⊔ lookupDef prog entry k) ⊥
+      (defSites prog combined).all (fun nid => ! decide (nid ∈ c.bodyIds))
+
+/-- The loop-invariant assignments of `prog`, as `(loopId, assignId)` pairs. -/
+def licmCandidates (prog : Program) : List (prog.NodeId × prog.NodeId) :=
+  (collectCandidates prog none prog.taggedFin).filterMap (fun c =>
+    if isInvariant prog c then some (c.loopId, c.assignId) else none)
+
+/-- A human-readable report of the loop-invariant assignments. -/
+def output (prog : Program) : String :=
+  match licmCandidates prog with
+  | [] => "no loop-invariant assignments found"
+  | cands =>
+      "loop-invariant assignments (loop ↦ assignment):\n" ++
+        String.intercalate "\n"
+          (cands.map (fun p => s!"  loop #{p.1.val}: assignment #{p.2.val}"))
+
+end LicmTransformation
+
+end Spa

lean/lake-manifest.json

@@ -0,0 +1,95 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5269898d6a51d047931107c8d72d934d8d5d3753",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.17.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c708be04267e3e995a14ac0d08b1530579c1525a",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.52",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "e7fd1a415c80985ade02a021172834ca2139b0ca",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "spa",
+ "lakeDir": ".lake"}

lean/lakefile.toml

@@ -0,0 +1,14 @@
+name = "spa"
+defaultTargets = ["Spa"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.17.0"
+
+[[lean_lib]]
+name = "Spa"
+
+[[lean_exe]]
+name = "spa"
+root = "Main"

lean/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.17.0