Lean migration: typeclass-based parameter passing, as in the Agda original

The port had flattened Agda's instance arguments ({{flA}}, {{evaluator}}, {{latticeInterpretation}}, {{validEvaluator}}) into explicitly threaded values (fhL, E, I, hE). Restore them as typeclasses: - Spa.FiniteHeightLattice: now actually used — Fixedpoint takes the instance instead of a FixedHeight value; FiniteMap gets the missing instance (height = ks.length * height B), so varsFixedHeight / statesFixedHeight / signFixedHeight / constFixedHeight plumbing disappears (instance bottoms are defeq to the old ones) - Spa.Analysis.Forward.Evaluation: StmtEvaluator/ExprEvaluator become classes; the Valid* Props become Prop-classes, as in Agda - Spa.Analysis.Forward.Adapters: the expr→stmt adapter and its validity are instances (Agda: the ExprToStmtAdapter instances) - LatticeInterpretation is a class; sign/const interpretations, evaluators and validity proofs are instances; use sites read like the Agda module applications: result SignLattice prog Proof simplifications (same theorems, proofs factored): - Spa.Lattice.AboveBelow.monotone₂_of_strict: any ⊥-strict/⊤-dominated operation on a flat lattice is monotone — replaces the four near- identical case bashes per analysis (postulates in Agda) - Spa.Lattice.AboveBelow.interp_sup_of/interp_inf_of: the shared flat- lattice interpretation case analysis, making interpSign_sup/inf and interpConst_sup/inf one-liners lake build green with zero warnings; lake exe spa output verified byte-identical (diff) to the previous, Agda-verified output. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Lean migration: final notes — Lean output verified identical to Agda
2026-06-09 23:32:38 -07:00 · 2026-06-09 20:54:59 -07:00 · 2026-06-09 20:52:08 -07:00 · 2026-06-09 20:14:53 -07:00 · 2026-06-09 19:30:42 -07:00 · 2026-06-09 19:12:39 -07:00
35 changed files with 4580 additions and 1221 deletions
--- a/.claude/settings.json
+++ b/.claude/settings.json
@@ -0,0 +1,9 @@
+{
+  "permissions": {
+    "allow": [
+      "Bash(lake build)",
+      "Bash(lake build *)",
+      "Bash(export PATH=\"$HOME/.elan/bin:$PATH\")"
+    ]
+  }
+}
--- a/Equivalence.agda
+++ b/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
+    }
--- a/LEAN_MIGRATION.md
+++ b/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.
--- a/Language/Graphs.agda
+++ b/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
--- a/Lattice.agda
+++ b/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 ⊓ ⊥)
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
--- a/Utils.agda
+++ b/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)
--- a/lean/.gitignore
+++ b/lean/.gitignore
@@ -0,0 +1 @@
+.lake/
--- a/lean/Main.lean
+++ b/lean/Main.lean
@@ -0,0 +1,40 @@
+/-
+Port of `Main.agda`. Prints the constant- and sign-analysis results for the
+test program (Agda: `putStrLn (output-Const ++ "\n" ++ output-Sign)`).
+-/
+import Spa.Analysis.Sign
+import Spa.Analysis.Constant
+
+namespace Spa
+
+/-- Agda: `testCode`. -/
+def testCode : Stmt :=
+  .andThen (.basic (.assign "zero" (.num 0)))
+    (.andThen (.basic (.assign "pos" (.add (.var "zero") (.num 1))))
+      (.andThen (.basic (.assign "neg" (.sub (.var "zero") (.num 1))))
+        (.basic (.assign "unknown" (.add (.var "pos") (.var "neg"))))))
+
+/-- Agda: `testCodeCond₁`. -/
+def testCodeCond₁ : Stmt :=
+  .andThen (.basic (.assign "var" (.num 1)))
+    (.ifElse (.var "var")
+      (.basic (.assign "var" (.add (.var "var") (.num 1))))
+      (.andThen (.basic (.assign "var" (.sub (.var "var") (.num 1))))
+        (.basic (.assign "var" (.num 1)))))
+
+/-- Agda: `testCodeCond₂`. -/
+def testCodeCond₂ : Stmt :=
+  .andThen (.basic (.assign "var" (.num 1)))
+    (.ifElse (.var "var")
+      (.basic (.assign "x" (.num 1)))
+      (.basic .noop))
+
+/-- Agda: `testProgram`. -/
+def testProgram : Program := ⟨testCode⟩
+
+end Spa
+
+/-- Agda: `main`. -/
+def main : IO Unit :=
+  IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
+              Spa.SignAnalysis.output Spa.testProgram)
--- a/lean/Spa.lean
+++ b/lean/Spa.lean
@@ -0,0 +1,22 @@
+import Spa.Lattice
+import Spa.Fixedpoint
+import Spa.Isomorphism
+import Spa.Lattice.Unit
+import Spa.Lattice.Prod
+import Spa.Lattice.AboveBelow
+import Spa.Lattice.IterProd
+import Spa.Lattice.FiniteMap
+import Spa.Language.Base
+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
--- a/lean/Spa/Analysis/Constant.lean
+++ b/lean/Spa/Analysis/Constant.lean
@@ -0,0 +1,228 @@
+/-
+Port of `Analysis/Constant.agda`.
+
+Correspondence:
+  showable, ≡-equiv, ≡-Decidable-ℤ ↦ (mathlib/derived instances)
+  ConstLattice (AboveBelow ℤ)      ↦ ConstLattice
+  AB.Plain (+ 0)                   ↦ the AboveBelow FiniteHeightLattice instance,
+                                     seeded by `Inhabited ℤ` (default `0`)
+  plus, minus                      ↦ plus, minus
+  plus-Monoˡ/ʳ, minus-Monoˡ/ʳ (postulates in Agda!)
+                                   ↦ plus_mono_left/right, minus_mono_left/right
+                                     — now actually proved, via
+                                     AboveBelow.monotone₂_of_strict
+  plus-Mono₂, minus-Mono₂          ↦ plus_mono₂, minus_mono₂
+  ⟦_⟧ᶜ                             ↦ interpConst
+  ⟦⟧ᶜ-respects-≈ᶜ                  ↦ (trivial with `=`)
+  ⟦⟧ᶜ-⊔ᶜ-∨, ⟦⟧ᶜ-⊓ᶜ-∧               ↦ interpConst_sup, interpConst_inf
+  s₁≢s₂⇒¬s₁∧s₂                     ↦ interpConst_mk_disjoint
+  latticeInterpretationᶜ           ↦ constInterpretation
+  WithProg.eval, eval-Monoʳ        ↦ ConstAnalysis.eval, eval_mono
+  ConstEval                        ↦ ConstAnalysis.exprEvaluator
+  plus-valid, minus-valid          ↦ plus_valid, minus_valid
+  eval-valid, ConstEvalValid       ↦ eval_valid
+  output                           ↦ ConstAnalysis.output
+  analyze-correct                  ↦ ConstAnalysis.analyze_correct
+-/
+import Spa.Analysis.Forward
+import Spa.Analysis.Utils
+import Spa.Showable
+
+namespace Spa
+
+abbrev ConstLattice : Type := AboveBelow ℤ
+
+namespace ConstAnalysis
+
+open AboveBelow in
+/-- Agda: `plus`. -/
+def plus : ConstLattice → ConstLattice → ConstLattice
+  | bot, _ => bot
+  | _, bot => bot
+  | top, _ => top
+  | _, top => top
+  | mk z₁, mk z₂ => mk (z₁ + z₂)
+
+open AboveBelow in
+/-- Agda: `minus`. -/
+def minus : ConstLattice → ConstLattice → ConstLattice
+  | bot, _ => bot
+  | _, bot => bot
+  | top, _ => top
+  | _, top => top
+  | mk z₁, mk z₂ => mk (z₁ - z₂)
+
+/-- Agda: `plus-Mono₂` (its components were postulates in Agda; `plus` is a
+strict operation on the flat lattice, so monotonicity holds regardless of the
+constant table). -/
+theorem plus_mono₂ : Monotone₂ plus :=
+  AboveBelow.monotone₂_of_strict plus
+    (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
+    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
+    (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
+
+/-- Agda: `plus-Monoˡ` — a postulate there, a theorem here. -/
+theorem plus_mono_left (s₂ : ConstLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂
+
+/-- Agda: `plus-Monoʳ` — a postulate there, a theorem here. -/
+theorem plus_mono_right (s₁ : ConstLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁
+
+/-- Agda: `minus-Mono₂` (likewise from strictness of `minus`). -/
+theorem minus_mono₂ : Monotone₂ minus :=
+  AboveBelow.monotone₂_of_strict minus
+    (fun y => by cases y <;> rfl) (fun x => by cases x <;> rfl)
+    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
+    (fun x hx => by cases x <;> first | exact absurd rfl hx | rfl)
+
+/-- Agda: `minus-Monoˡ` — a postulate there, a theorem here. -/
+theorem minus_mono_left (s₂ : ConstLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂
+
+/-- Agda: `minus-Monoʳ` — a postulate there, a theorem here. -/
+theorem minus_mono_right (s₁ : ConstLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁
+
+/-- Agda: `⟦_⟧ᶜ`. -/
+def interpConst : ConstLattice → Value → Prop
+  | .bot, _ => False
+  | .top, _ => True
+  | .mk z, v => v = .int z
+
+/-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/
+theorem 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
+
+/-- Agda: `⟦⟧ᶜ-⊔ᶜ-∨` (via the factored flat-lattice lemma). -/
+theorem interpConst_sup {s₁ s₂ : ConstLattice} (v : Value)
+    (h : interpConst s₁ v ∨ interpConst s₂ v) : interpConst (s₁ ⊔ s₂) v :=
+  AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
+
+/-- Agda: `⟦⟧ᶜ-⊓ᶜ-∧` (via the factored flat-lattice lemma). -/
+theorem interpConst_inf {s₁ s₂ : ConstLattice} (v : Value)
+    (h : interpConst s₁ v ∧ interpConst s₂ v) : interpConst (s₁ ⊓ s₂) v :=
+  AboveBelow.interp_inf_of (fun hne _ => interpConst_mk_disjoint hne) v h
+
+/-- Agda: `latticeInterpretationᶜ` (an instance there too). -/
+instance constInterpretation : LatticeInterpretation ConstLattice where
+  interp := interpConst
+  interp_sup := fun {l₁ l₂} v h => interpConst_sup (s₁ := l₁) (s₂ := l₂) v h
+  interp_inf := fun {l₁ l₂} v h => interpConst_inf (s₁ := l₁) (s₂ := l₂) v h
+
+variable (prog : Program)
+
+/-- Agda: `WithProg.eval`. -/
+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
+
+/-- Agda: `WithProg.eval-Monoʳ`. -/
+theorem 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 _
+
+/-- Agda: the `ConstEval` instance. -/
+instance exprEvaluator : ExprEvaluator ConstLattice prog :=
+  ⟨eval prog, eval_mono prog⟩
+
+/-- Agda: `WithProg.result`/`output`. -/
+def output : String :=
+  show' (result ConstLattice prog)
+
+/-- Agda: `plus-valid`. -/
+theorem plus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
+    (h₁ : interpConst g₁ (.int z₁)) (h₂ : interpConst g₂ (.int z₂)) :
+    interpConst (plus g₁ g₂) (.int (z₁ + z₂)) := by
+  rcases g₁ with _ | _ | c₁
+  · exact h₁.elim
+  · rcases g₂ with _ | _ | c₂
+    · exact h₂.elim
+    · exact trivial
+    · exact trivial
+  · rcases g₂ with _ | _ | c₂
+    · exact h₂.elim
+    · exact trivial
+    · injection h₁ with hz₁
+      injection h₂ with hz₂
+      show Value.int (z₁ + z₂) = Value.int (c₁ + c₂)
+      rw [hz₁, hz₂]
+
+/-- Agda: `minus-valid`. -/
+theorem minus_valid {g₁ g₂ : ConstLattice} {z₁ z₂ : ℤ}
+    (h₁ : interpConst g₁ (.int z₁)) (h₂ : interpConst g₂ (.int z₂)) :
+    interpConst (minus g₁ g₂) (.int (z₁ - z₂)) := by
+  rcases g₁ with _ | _ | c₁
+  · exact h₁.elim
+  · rcases g₂ with _ | _ | c₂
+    · exact h₂.elim
+    · exact trivial
+    · exact trivial
+  · rcases g₂ with _ | _ | c₂
+    · exact h₂.elim
+    · exact trivial
+    · injection h₁ with hz₁
+      injection h₂ with hz₂
+      show Value.int (z₁ - z₂) = Value.int (c₁ - c₂)
+      rw [hz₁, hz₂]
+
+/-- Agda: `eval-valid` / the `ConstEvalValid` instance. -/
+instance eval_valid : ValidExprEvaluator ConstLattice prog := by
+  constructor
+  intro vs ρ e v hev
+  induction hev with
+  | num n =>
+    intro _
+    show interpConst (eval prog (.num n) vs) (.int n)
+    rfl
+  | var x v hxv =>
+    intro hvs
+    show interpConst (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₁ : interpConst (eval prog e₁ vs) (.int z₁) := ih₁ hvs
+    have h₂ : interpConst (eval prog e₂ vs) (.int z₂) := ih₂ hvs
+    show interpConst (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₁ : interpConst (eval prog e₁ vs) (.int z₁) := ih₁ hvs
+    have h₂ : interpConst (eval prog e₂ vs) (.int z₂) := ih₂ hvs
+    show interpConst (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂))
+    exact minus_valid h₁ h₂
+
+/-- Agda: `WithProg.analyze-correct`. -/
+theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    interpV (variablesAt prog.finalState (result ConstLattice prog)) ρ :=
+  Spa.analyze_correct ConstLattice prog hrun
+
+end ConstAnalysis
+
+end Spa
--- a/lean/Spa/Analysis/Forward.lean
+++ b/lean/Spa/Analysis/Forward.lean
@@ -0,0 +1,167 @@
+/-
+Port of `Analysis/Forward.agda` (`WithProg`, `WithStmtEvaluator`,
+`WithValidInterpretation`).
+
+As in Agda, the statement evaluator, the lattice interpretation and the
+evaluator's validity proof are instance arguments (`{{evaluator}}`,
+`{{latticeInterpretationˡ}}`, `{{validEvaluator}}`); `result` and
+`analyze_correct` take `L` and `prog` explicitly, mirroring the Agda call
+shape `WithProg.result L prog`.
+
+Correspondence:
+  updateVariablesForState, -Monoʳ   ↦ updateVariablesForState, _mono
+  updateAll, updateAll-Mono,
+  updateAll-k∈ks-≡                  ↦ updateAll, updateAll_mono, updateAll_mem_eq
+  analyze, analyze-Mono             ↦ analyze, analyze_mono
+  result, result≈analyze-result     ↦ result, result_eq
+  variablesAt-updateAll             ↦ variablesAt_updateAll
+  eval-fold-valid                   ↦ eval_fold_valid
+  updateVariablesForState-matches   ↦ updateVariablesForState_matches
+  updateAll-matches                 ↦ updateAll_matches
+  stepTrace                         ↦ stepTrace   (the `subst`/`⟦⟧ᵛ-respects-≈ᵛ`
+                                       plumbing becomes plain rewriting with `=`)
+  walkTrace                         ↦ walkTrace
+  joinForKey-initialState-⊥ᵛ        ↦ joinForKey_initialState
+  ⟦joinAll-initialState⟧ᵛ∅          ↦ interpV_joinForKey_initialState
+  analyze-correct                   ↦ analyze_correct
+-/
+import Spa.Analysis.Forward.Lattices
+import Spa.Analysis.Forward.Evaluation
+import Spa.Analysis.Forward.Adapters
+import Spa.Fixedpoint
+
+namespace Spa
+
+variable {L : Type} [Lattice L] {prog : Program} [E : StmtEvaluator L prog]
+
+/-- Agda: `updateVariablesForState`. -/
+def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
+    VariableValues L prog :=
+  (prog.code s).foldl (fun vs bs => E.eval s bs vs) (variablesAt s sv)
+
+/-- Agda: `updateVariablesForState-Monoʳ`. -/
+theorem updateVariablesForState_mono (s : prog.State) :
+    Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
+  foldl_mono' (prog.code s) _ (fun bs => E.eval_mono s bs) (variablesAt_le hle s)
+
+/-- Agda: `updateAll`. -/
+def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
+  FiniteMap.generalizedUpdate id (fun s sv => updateVariablesForState s sv)
+    prog.states sv
+
+/-- Agda: `updateAll-Mono`. -/
+theorem updateAll_mono : Monotone (updateAll (L := L) (prog := prog)) :=
+  FiniteMap.generalizedUpdate_monotone monotone_id updateVariablesForState_mono
+
+/-- Agda: `updateAll-k∈ks-≡`. -/
+theorem 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
+
+/-- Agda: `variablesAt-updateAll`. -/
+theorem variablesAt_updateAll (s : prog.State) (sv : StateVariables L prog) :
+    variablesAt s (updateAll sv) = updateVariablesForState s sv :=
+  updateAll_mem_eq (variablesAt_mem s (updateAll sv))
+
+variable [FiniteHeightLattice L]
+
+/-- Agda: `analyze`. -/
+def analyze (sv : StateVariables L prog) : StateVariables L prog :=
+  updateAll (joinAll sv)
+
+/-- Agda: `analyze-Mono`. -/
+theorem analyze_mono : Monotone (analyze (L := L) (prog := prog)) := fun _ _ hle =>
+  updateAll_mono (joinAll_mono hle)
+
+variable [DecidableEq L]
+
+variable (L prog) in
+/-- Agda: `result` (the least fixpoint of `analyze`). -/
+def result : StateVariables L prog :=
+  Fixedpoint.aFix analyze analyze_mono
+
+variable (L prog) in
+/-- Agda: `result≈analyze-result`. -/
+theorem result_eq : result L prog = analyze (result L prog) :=
+  Fixedpoint.aFix_eq analyze analyze_mono
+
+/-- Agda: `joinForKey-initialState-⊥ᵛ`. -/
+theorem joinForKey_initialState :
+    joinForKey prog.initialState (result L prog) = botV L prog := by
+  rw [joinForKey, prog.incoming_initialState_eq_nil]
+  rfl
+
+/-! ### Semantic correctness (Agda: `WithValidInterpretation`) -/
+
+variable [I : LatticeInterpretation L] [V : ValidStmtEvaluator L prog]
+
+omit [FiniteHeightLattice L] [DecidableEq L] in
+/-- Agda: `eval-fold-valid`. -/
+theorem eval_fold_valid {s : prog.State} {bss : List BasicStmt}
+    {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
+    (hbss : EvalBasicStmts ρ₁ bss ρ₂) (hvs : interpV vs ρ₁) :
+    interpV (bss.foldl (fun vs bs => E.eval s bs vs) vs) ρ₂ := by
+  induction hbss generalizing vs with
+  | nil => exact hvs
+  | cons hbs _ ih => exact ih (ValidStmtEvaluator.valid hbs hvs)
+
+omit [FiniteHeightLattice L] [DecidableEq L] in
+/-- Agda: `updateVariablesForState-matches`. -/
+theorem updateVariablesForState_matches {s : prog.State}
+    {sv : StateVariables L prog} {ρ₁ ρ₂ : Env}
+    (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
+    (hvs : interpV (variablesAt s sv) ρ₁) :
+    interpV (updateVariablesForState s sv) ρ₂ :=
+  eval_fold_valid hbss hvs
+
+omit [FiniteHeightLattice L] [DecidableEq L] in
+/-- Agda: `updateAll-matches`. -/
+theorem updateAll_matches {s : prog.State} {sv : StateVariables L prog}
+    {ρ₁ ρ₂ : Env} (hbss : EvalBasicStmts ρ₁ (prog.code s) ρ₂)
+    (hvs : interpV (variablesAt s sv) ρ₁) :
+    interpV (variablesAt s (updateAll sv)) ρ₂ := by
+  rw [variablesAt_updateAll]
+  exact updateVariablesForState_matches hbss hvs
+
+/-- Agda: `stepTrace`. -/
+theorem stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env}
+    (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁)
+    (hbss : EvalBasicStmts ρ₁ (prog.code s₁) ρ₂) :
+    interpV (variablesAt s₁ (result L prog)) ρ₂ := by
+  rw [result_eq L prog]
+  refine updateAll_matches hbss ?_
+  rw [variablesAt_joinAll]
+  exact hjoin
+
+/-- Agda: `walkTrace`. -/
+theorem walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env}
+    (hjoin : interpV (joinForKey s₁ (result L prog)) ρ₁)
+    (tr : Trace prog.graph s₁ s₂ ρ₁ ρ₂) :
+    interpV (variablesAt s₂ (result L prog)) ρ₂ := by
+  induction tr with
+  | single hbss => exact stepTrace hjoin hbss
+  | @edge _ ρ' _ i₁ i₂ _ hbss hedge _ ih =>
+    have hstep : interpV (variablesAt i₁ (result L prog)) ρ' :=
+      stepTrace hjoin hbss
+    have hmem : variablesAt i₁ (result L prog)
+        ∈ (result L prog).valuesAt (prog.incoming i₂) :=
+      FiniteMap.mem_valuesAt prog.states_nodup
+        (prog.mem_incoming_of_edge hedge) (variablesAt_mem i₁ (result L prog))
+    exact ih (interpV_foldr hstep hmem)
+
+omit V in
+/-- Agda: `⟦joinAll-initialState⟧ᵛ∅`. -/
+theorem interpV_joinForKey_initialState :
+    interpV (joinForKey prog.initialState (result L prog)) [] := by
+  rw [joinForKey_initialState]
+  exact interpV_botV_nil
+
+variable (L prog) in
+/-- Agda: `analyze-correct` — the analysis result at the final state soundly
+describes every terminating execution of the program. -/
+theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    interpV (variablesAt prog.finalState (result L prog)) ρ :=
+  walkTrace interpV_joinForKey_initialState (prog.trace hrun)
+
+end Spa
--- a/lean/Spa/Analysis/Forward/Adapters.lean
+++ b/lean/Spa/Analysis/Forward/Adapters.lean
@@ -0,0 +1,75 @@
+/-
+Port of `Analysis/Forward/Adapters.agda` (`ExprToStmtAdapter`).
+
+Correspondence:
+  updateVariablesFromExpression           ↦ updateVariablesFromExpression
+  updateVariablesFromExpression-Mono      ↦ updateVariablesFromExpression_mono
+  (the -k∈ks-≡ / -k∉ks-backward renames   ↦ used directly from FiniteMap)
+  evalᵇ, evalᵇ-Monoʳ                      ↦ evalB, evalB_mono
+  stmtEvaluator (instance)                ↦ instance StmtEvaluator L prog
+  evalᵇ-valid, validStmtEvaluator         ↦ instance ValidStmtEvaluator L prog
+                                            (the Agda `k ≟ˢ k'` case split is
+                                            subsumed by `cases` on `Env.Mem`,
+                                            whose `here` case forces `k' = k`)
+-/
+import Spa.Analysis.Forward.Evaluation
+
+namespace Spa
+
+variable {L : Type} [Lattice L] {prog : Program} [E : ExprEvaluator L prog]
+
+/-- Agda: `updateVariablesFromExpression` — set the single key `k` to the
+value of `e` (the `GeneralizedUpdate` with `ks = [k]`). -/
+def updateVariablesFromExpression (k : String) (e : Expr)
+    (vs : VariableValues L prog) : VariableValues L prog :=
+  FiniteMap.generalizedUpdate id (fun _ vs => E.eval e vs) [k] vs
+
+/-- Agda: `updateVariablesFromExpression-Mono`. -/
+theorem updateVariablesFromExpression_mono (k : String) (e : Expr) :
+    Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) :=
+  FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)
+
+/-- Agda: `evalᵇ`. -/
+def evalB (_ : prog.State) (bs : BasicStmt)
+    (vs : VariableValues L prog) : VariableValues L prog :=
+  match bs with
+  | .assign k e => updateVariablesFromExpression k e vs
+  | .noop => vs
+
+/-- Agda: `evalᵇ-Monoʳ`. -/
+theorem evalB_mono (s : prog.State) (bs : BasicStmt) :
+    Monotone (evalB (L := L) (prog := prog) s bs) := by
+  cases bs with
+  | assign k e => exact updateVariablesFromExpression_mono k e
+  | noop => exact monotone_id
+
+/-- Agda: the `stmtEvaluator` instance of `ExprToStmtAdapter`. -/
+instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
+  ⟨evalB, evalB_mono⟩
+
+/-- Agda: `evalᵇ-valid` / the `validStmtEvaluator` instance. -/
+instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
+    [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by
+  constructor
+  intro s vs ρ₁ ρ₂ bs hbs hvs
+  cases hbs with
+  | noop => exact hvs
+  | assign k e v hev =>
+    intro k' l hk'l v' hv'
+    cases hv' with
+    | here =>
+      have hk'l₀ : (k, l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
+          (fun _ vs => E.eval e vs) [k] vs := hk'l
+      have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
+        (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hk'l₀
+      rw [hl]
+      exact ValidExprEvaluator.valid hev hvs
+    | there _ _ _ _ _ hne hmem' =>
+      have hk'l₀ : (k', l) ∈ FiniteMap.generalizedUpdate (ks := prog.vars) id
+          (fun _ vs => E.eval e vs) [k] vs := hk'l
+      have hk'l' : (k', l) ∈ (id vs : VariableValues L prog) :=
+        FiniteMap.generalizedUpdate_not_mem_backward
+          (fun hmem => hne (List.mem_singleton.mp hmem)) hk'l₀
+      exact hvs _ _ hk'l' _ hmem'
+
+end Spa
--- a/lean/Spa/Analysis/Forward/Evaluation.lean
+++ b/lean/Spa/Analysis/Forward/Evaluation.lean
@@ -0,0 +1,43 @@
+/-
+Port of `Analysis/Forward/Evaluation.agda`.
+
+All four records were consumed through Agda instance arguments (`{{evaluator :
+StmtEvaluator}}`, `{{validEvaluator : ValidStmtEvaluator …}}`), so they are
+typeclasses here as well.
+
+Correspondence:
+  StmtEvaluator (eval, eval-Monoʳ)  ↦ StmtEvaluator (eval, eval_mono)
+  ExprEvaluator (eval, eval-Monoʳ)  ↦ ExprEvaluator (eval, eval_mono)
+  ValidExprEvaluator                ↦ ValidExprEvaluator (valid)
+  ValidStmtEvaluator                ↦ ValidStmtEvaluator (valid)
+-/
+import Spa.Analysis.Forward.Lattices
+
+namespace Spa
+
+variable (L : Type) [Lattice L] (prog : Program)
+
+/-- Agda: `StmtEvaluator`. -/
+class StmtEvaluator where
+  eval : prog.State → BasicStmt → VariableValues L prog → VariableValues L prog
+  eval_mono : ∀ s bs, Monotone (eval s bs)
+
+/-- Agda: `ExprEvaluator`. -/
+class ExprEvaluator where
+  eval : Expr → VariableValues L prog → L
+  eval_mono : ∀ e, Monotone (eval e)
+
+/-- Agda: `ValidExprEvaluator`. -/
+class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
+    Prop where
+  valid : ∀ {vs : VariableValues L prog} {ρ : Env} {e : Expr} {v : Value},
+    EvalExpr ρ e v → interpV vs ρ → I.interp (ExprEvaluator.eval e vs) v
+
+/-- Agda: `ValidStmtEvaluator`. -/
+class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
+    Prop where
+  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
+    {bs : BasicStmt},
+    EvalBasicStmt ρ₁ bs ρ₂ → interpV vs ρ₁ → interpV (E.eval s bs vs) ρ₂
+
+end Spa
--- a/lean/Spa/Analysis/Forward/Lattices.lean
+++ b/lean/Spa/Analysis/Forward/Lattices.lean
@@ -0,0 +1,143 @@
+/-
+Port of `Analysis/Forward/Lattices.agda`.
+
+The Agda module instantiates `Lattice.FiniteMap` twice (variables ↦ abstract
+values, states ↦ variable maps) and re-exports everything with ᵛ/ᵐ suffixes.
+In Lean the two instantiations are `abbrev`s and the FiniteMap API is used
+directly; the module parameters (the finite-height lattice `L`, the program)
+become section variables, with the finite-height structure and the lattice
+interpretation arriving by instance resolution as in Agda.
+
+Correspondence:
+  VariableValues, StateVariables  ↦ VariableValues, StateVariables
+  isLatticeᵛ/isLatticeᵐ, ⊔ᵛ, ≼ᵛ … ↦ (the FiniteMap Lattice instances)
+  fixedHeightᵛ, fixedHeightᵐ      ↦ (the FiniteMap FiniteHeightLattice instance)
+  ⊥ᵛ, ⊥ᵛ-contains-bottoms         ↦ botV, FiniteMap.bot_contains_bots
+  states-in-Map                   ↦ states_memKey
+  variablesAt                     ↦ variablesAt
+  variablesAt-∈                   ↦ variablesAt_mem
+  variablesAt-≈                   ↦ (congruence, trivial with `=`)
+  joinForKey, joinForKey-Mono     ↦ joinForKey, joinForKey_mono
+  joinAll, joinAll-Mono,
+  joinAll-k∈ks-≡                  ↦ joinAll, joinAll_mono, joinAll_mem_eq
+  variablesAt-joinAll             ↦ variablesAt_joinAll
+  ⟦_⟧ᵛ                            ↦ interpV
+  ⟦⊥ᵛ⟧ᵛ∅                          ↦ interpV_botV_nil
+  ⟦⟧ᵛ-respects-≈ᵛ                 ↦ (trivial with `=`)
+  ⟦⟧ᵛ-⊔ᵛ-∨                        ↦ interpV_sup
+  ⟦⟧ᵛ-foldr                       ↦ interpV_foldr
+-/
+import Spa.Language
+import Spa.Lattice.FiniteMap
+
+namespace Spa
+
+variable (L : Type) [Lattice L] (prog : Program)
+
+/-- Agda: `VariableValues`. -/
+abbrev VariableValues : Type := FiniteMap String L prog.vars
+
+/-- Agda: `StateVariables`. -/
+abbrev StateVariables : Type := FiniteMap prog.State (VariableValues L prog) prog.states
+
+/-- Agda: `⊥ᵛ` (the bottom of `fixedHeightᵛ`, now found by instance search). -/
+def botV [FiniteHeightLattice L] : VariableValues L prog :=
+  FiniteHeightLattice.bot (VariableValues L prog)
+
+variable {L prog}
+
+omit [Lattice L] in
+/-- Agda: `states-in-Map`. -/
+theorem states_memKey (s : prog.State) (sv : StateVariables L prog) :
+    FiniteMap.MemKey s sv :=
+  FiniteMap.memKey_iff.mpr (prog.states_complete s)
+
+/-- Agda: `variablesAt`. -/
+def variablesAt (s : prog.State) (sv : StateVariables L prog) :
+    VariableValues L prog :=
+  (FiniteMap.locate (states_memKey s sv)).1
+
+omit [Lattice L] in
+/-- Agda: `variablesAt-∈`. -/
+theorem variablesAt_mem (s : prog.State) (sv : StateVariables L prog) :
+    (s, variablesAt s sv) ∈ sv :=
+  (FiniteMap.locate (states_memKey s sv)).2
+
+/-- Agda: `m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ`, specialized the way `Forward.agda` uses it. -/
+theorem 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]
+
+/-- Agda: `joinForKey`. -/
+def joinForKey (k : prog.State) (sv : StateVariables L prog) :
+    VariableValues L prog :=
+  (sv.valuesAt (prog.incoming k)).foldr (· ⊔ ·) (botV L prog)
+
+/-- Agda: `joinForKey-Mono`. -/
+theorem 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)
+
+/-- Agda: `joinAll` (the "Exercise 4.26" generalized update with `f = id`). -/
+def joinAll (sv : StateVariables L prog) : StateVariables L prog :=
+  FiniteMap.generalizedUpdate id joinForKey prog.states sv
+
+/-- Agda: `joinAll-Mono`. -/
+theorem joinAll_mono : Monotone (joinAll (L := L) (prog := prog)) :=
+  FiniteMap.generalizedUpdate_monotone monotone_id joinForKey_mono
+
+/-- Agda: `joinAll-k∈ks-≡`. -/
+theorem 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
+
+/-- Agda: `variablesAt-joinAll`. -/
+theorem variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
+    variablesAt s (joinAll sv) = joinForKey s sv :=
+  joinAll_mem_eq (variablesAt_mem s (joinAll sv))
+
+/-! ### Lifting an interpretation to variable maps -/
+
+variable [I : LatticeInterpretation L]
+
+omit [FiniteHeightLattice L] in
+/-- Agda: `⟦_⟧ᵛ`. -/
+def interpV (vs : VariableValues L prog) (ρ : Env) : Prop :=
+  ∀ (k : String) (l : L), (k, l) ∈ vs →
+    ∀ (v : Value), Env.Mem (k, v) ρ → I.interp l v
+
+/-- Agda: `⟦⊥ᵛ⟧ᵛ∅`. -/
+theorem interpV_botV_nil : interpV (botV L prog) [] := by
+  intro k l _ v hmem
+  cases hmem
+
+omit [FiniteHeightLattice L] in
+/-- Agda: `⟦⟧ᵛ-⊔ᵛ-∨`. -/
+theorem interpV_sup {vs₁ vs₂ : VariableValues L prog} {ρ : Env}
+    (h : interpV vs₁ ρ ∨ interpV vs₂ ρ) : interpV (vs₁ ⊔ vs₂) ρ := by
+  intro 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))
+
+/-- Agda: `⟦⟧ᵛ-foldr`. -/
+theorem interpV_foldr {vs : VariableValues L prog}
+    {vss : List (VariableValues L prog)} {ρ : Env}
+    (hvs : interpV vs ρ) (hmem : vs ∈ vss) :
+    interpV (vss.foldr (· ⊔ ·) (botV L prog)) ρ := by
+  induction vss with
+  | nil => cases hmem
+  | cons vs' vss' ih =>
+    rcases List.mem_cons.mp hmem with rfl | hmem'
+    · exact interpV_sup (Or.inl hvs)
+    · exact interpV_sup (Or.inr (ih hmem'))
+
+end Spa
--- a/lean/Spa/Analysis/Sign.lean
+++ b/lean/Spa/Analysis/Sign.lean
@@ -0,0 +1,335 @@
+/-
+Port of `Analysis/Sign.agda`.
+
+Correspondence:
+  Sign (+ / - / 0ˢ)         ↦ Sign.plus / Sign.minus / Sign.zero
+  _≟ᵍ_, ≡-equiv, ≡-Decidable ↦ deriving DecidableEq
+  SignLattice (AboveBelow)  ↦ SignLattice
+  AB.Plain 0ˢ               ↦ the AboveBelow FiniteHeightLattice instance,
+                              seeded by `Inhabited Sign := ⟨.zero⟩`
+  plus, minus               ↦ plus, minus
+  plus-Monoˡ/ʳ, minus-Monoˡ/ʳ (postulates in Agda!)
+                            ↦ plus_mono_left/right, minus_mono_left/right —
+                              now actually proved, via
+                              AboveBelow.monotone₂_of_strict
+  plus-Mono₂, minus-Mono₂   ↦ plus_mono₂, minus_mono₂
+  ⟦_⟧ᵍ                      ↦ interpSign
+  ⟦⟧ᵍ-respects-≈ᵍ           ↦ (trivial with `=`)
+  ⟦⟧ᵍ-⊔ᵍ-∨, ⟦⟧ᵍ-⊓ᵍ-∧        ↦ interpSign_sup, interpSign_inf
+  s₁≢s₂⇒¬s₁∧s₂              ↦ interpSign_mk_disjoint
+  latticeInterpretationᵍ    ↦ signInterpretation
+  WithProg.eval, eval-Monoʳ ↦ SignAnalysis.eval, eval_mono
+  SignEval (instance)       ↦ SignAnalysis.exprEvaluator
+  plus-valid, minus-valid   ↦ plus_valid, minus_valid
+  eval-valid, SignEvalValid ↦ eval_valid
+  output                    ↦ SignAnalysis.output
+  analyze-correct           ↦ SignAnalysis.analyze_correct
+-/
+import Spa.Analysis.Forward
+import Spa.Analysis.Utils
+import Spa.Showable
+
+namespace Spa
+
+inductive Sign where
+  | plus
+  | minus
+  | zero
+  deriving DecidableEq
+
+instance : Showable Sign :=
+  ⟨fun
+    | .plus => "+"
+    | .minus => "-"
+    | .zero => "0"⟩
+
+/-- Agda: the module parameter `x = 0ˢ` of `AB.Plain` (it seeds the
+`FiniteHeightLattice (AboveBelow Sign)` instance). -/
+instance : Inhabited Sign := ⟨.zero⟩
+
+abbrev SignLattice : Type := AboveBelow Sign
+
+open AboveBelow in
+/-- Agda: `plus`. -/
+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
+/-- Agda: `minus`. -/
+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
+
+/-- Agda: `plus-Mono₂` (its components were postulates in Agda; `plus` is a
+strict operation on the flat lattice, so monotonicity holds regardless of the
+sign table). -/
+theorem plus_mono₂ : Monotone₂ plus :=
+  AboveBelow.monotone₂_of_strict plus
+    (fun y => by cases y <;> rfl)
+    (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
+    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
+    (fun x hx => by
+      rcases x with _ | _ | s <;>
+        first | exact absurd rfl hx | rfl | (cases s <;> rfl))
+
+/-- Agda: `plus-Monoˡ` — a postulate there, a theorem here. -/
+theorem plus_mono_left (s₂ : SignLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂
+
+/-- Agda: `plus-Monoʳ` — a postulate there, a theorem here. -/
+theorem plus_mono_right (s₁ : SignLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁
+
+/-- Agda: `minus-Mono₂` (likewise from strictness of `minus`). -/
+theorem minus_mono₂ : Monotone₂ minus :=
+  AboveBelow.monotone₂_of_strict minus
+    (fun y => by cases y <;> rfl)
+    (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
+    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
+    (fun x hx => by
+      rcases x with _ | _ | s <;>
+        first | exact absurd rfl hx | rfl | (cases s <;> rfl))
+
+/-- Agda: `minus-Monoˡ` — a postulate there, a theorem here. -/
+theorem minus_mono_left (s₂ : SignLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂
+
+/-- Agda: `minus-Monoʳ` — a postulate there, a theorem here. -/
+theorem minus_mono_right (s₁ : SignLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁
+
+/-- Agda: `⟦_⟧ᵍ`. -/
+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))
+
+/-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/
+theorem 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
+
+/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` (via the factored flat-lattice lemma). -/
+theorem interpSign_sup {s₁ s₂ : SignLattice} (v : Value)
+    (h : interpSign s₁ v ∨ interpSign s₂ v) : interpSign (s₁ ⊔ s₂) v :=
+  AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h
+
+/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` (via the factored flat-lattice lemma). -/
+theorem interpSign_inf {s₁ s₂ : SignLattice} (v : Value)
+    (h : interpSign s₁ v ∧ interpSign s₂ v) : interpSign (s₁ ⊓ s₂) v :=
+  AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h
+
+/-- Agda: `latticeInterpretationᵍ` (an instance there too). -/
+instance signInterpretation : LatticeInterpretation SignLattice where
+  interp := interpSign
+  interp_sup := fun {l₁ l₂} v h => interpSign_sup (s₁ := l₁) (s₂ := l₂) v h
+  interp_inf := fun {l₁ l₂} v h => interpSign_inf (s₁ := l₁) (s₂ := l₂) v h
+
+namespace SignAnalysis
+
+/-! Agda: `module WithProg (prog : Program)`. -/
+
+variable (prog : Program)
+
+/-- Agda: `WithProg.eval`. -/
+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
+
+/-- Agda: `WithProg.eval-Monoʳ`. -/
+theorem 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 _
+
+/-- Agda: the `SignEval` instance. -/
+instance exprEvaluator : ExprEvaluator SignLattice prog :=
+  ⟨eval prog, eval_mono prog⟩
+
+/-- Agda: `WithProg.result`/`output` — the analysis result, printed. -/
+def output : String :=
+  show' (result SignLattice prog)
+
+/-- Agda: `plus-valid`. -/
+theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
+    (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) :
+    interpSign (plus g₁ g₂) (.int (z₁ + z₂)) := by
+  rcases g₁ with _ | _ | s₁
+  · exact h₁.elim
+  · rcases g₂ with _ | _ | s₂
+    · exact h₂.elim
+    · exact trivial
+    · exact trivial
+  · rcases g₂ with _ | _ | s₂
+    · exact h₂.elim
+    · rcases s₁ <;> exact trivial
+    · rcases s₁ <;> rcases s₂ <;>
+        simp only [plus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;>
+        try trivial
+      · obtain ⟨n₁, rfl⟩ := h₁
+        obtain ⟨n₂, rfl⟩ := h₂
+        exact ⟨n₁ + n₂ + 1, by omega⟩
+      · obtain ⟨n₁, rfl⟩ := h₁
+        subst h₂
+        exact ⟨n₁, by omega⟩
+      · obtain ⟨n₁, rfl⟩ := h₁
+        obtain ⟨n₂, rfl⟩ := h₂
+        exact ⟨n₁ + n₂ + 1, by omega⟩
+      · obtain ⟨n₁, rfl⟩ := h₁
+        subst h₂
+        exact ⟨n₁, by omega⟩
+      · subst h₁
+        obtain ⟨n₂, rfl⟩ := h₂
+        exact ⟨n₂, by omega⟩
+      · subst h₁
+        obtain ⟨n₂, rfl⟩ := h₂
+        exact ⟨n₂, by omega⟩
+      · subst h₁
+        subst h₂
+        omega
+
+/-- Agda: `minus-valid`. -/
+theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
+    (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) :
+    interpSign (minus g₁ g₂) (.int (z₁ - z₂)) := by
+  rcases g₁ with _ | _ | s₁
+  · exact h₁.elim
+  · rcases g₂ with _ | _ | s₂
+    · exact h₂.elim
+    · exact trivial
+    · exact trivial
+  · rcases g₂ with _ | _ | s₂
+    · exact h₂.elim
+    · rcases s₁ <;> exact trivial
+    · rcases s₁ <;> rcases s₂ <;>
+        simp only [minus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;>
+        try trivial
+      · obtain ⟨n₁, rfl⟩ := h₁
+        obtain ⟨n₂, rfl⟩ := h₂
+        exact ⟨n₁ + n₂ + 1, by omega⟩
+      · obtain ⟨n₁, rfl⟩ := h₁
+        subst h₂
+        exact ⟨n₁, by omega⟩
+      · obtain ⟨n₁, rfl⟩ := h₁
+        obtain ⟨n₂, rfl⟩ := h₂
+        exact ⟨n₁ + n₂ + 1, by omega⟩
+      · obtain ⟨n₁, rfl⟩ := h₁
+        subst h₂
+        exact ⟨n₁, by omega⟩
+      · subst h₁
+        obtain ⟨n₂, rfl⟩ := h₂
+        exact ⟨n₂, by omega⟩
+      · subst h₁
+        obtain ⟨n₂, rfl⟩ := h₂
+        exact ⟨n₂, by omega⟩
+      · subst h₁
+        subst h₂
+        omega
+
+/-- Agda: `eval-valid` / the `SignEvalValid` instance. -/
+instance eval_valid : ValidExprEvaluator SignLattice prog := by
+  constructor
+  intro vs ρ e v hev
+  induction hev with
+  | num n =>
+    intro _
+    show interpSign (eval prog (.num n) vs) (.int n)
+    cases n with
+    | zero => rfl
+    | succ n' => exact ⟨n', congrArg Value.int (by push_cast; ring)⟩
+  | var x v hxv =>
+    intro hvs
+    show interpSign (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₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs
+    have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs
+    show interpSign (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₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs
+    have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs
+    show interpSign (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂))
+    exact minus_valid h₁ h₂
+
+/-- Agda: `WithProg.analyze-correct`. -/
+theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
+    interpV (variablesAt prog.finalState (result SignLattice prog)) ρ :=
+  Spa.analyze_correct SignLattice prog hrun
+
+end SignAnalysis
+
+end Spa
--- a/lean/Spa/Analysis/Utils.lean
+++ b/lean/Spa/Analysis/Utils.lean
@@ -0,0 +1,15 @@
+/-
+Port of `Analysis/Utils.agda`. The `≼ᴼ-trans` module parameter lifts into the
+`Preorder` instance.
+-/
+import Spa.Lattice
+
+namespace Spa
+
+/-- Agda: `eval-combine₂`. -/
+theorem 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
--- a/lean/Spa/Fixedpoint.lean
+++ b/lean/Spa/Fixedpoint.lean
@@ -0,0 +1,82 @@
+/-
+Port of `Fixedpoint.agda`.
+
+Same gas-based algorithm: iterate `f` starting at the chain-bottom `⊥`; since
+the lattice has fixed height `h`, a fixed point must be reached within `h + 1`
+steps, or we would build a `<`-chain longer than the longest one. We
+deliberately do *not* use mathlib's `OrderHom.lfp` (different proof approach,
+and not computable).
+
+As in Agda — where the module took `{{flA : IsFiniteHeightLattice A h …}}` —
+the finite-height structure arrives by instance resolution
+(`[FiniteHeightLattice α]`); only `f` and its monotonicity are explicit.
+
+Correspondence:
+  doStep             ↦ Spa.Fixedpoint.doStep   (the chain argument now carries
+                                                 `a₁ = ⊥` and its length in the
+                                                 `LTSeries` structure itself)
+  fix                ↦ Spa.Fixedpoint.fix
+  aᶠ                 ↦ Spa.Fixedpoint.aFix
+  aᶠ≈faᶠ             ↦ Spa.Fixedpoint.aFix_eq
+  stepPreservesLess  ↦ Spa.Fixedpoint.doStep_le
+  aᶠ≼                ↦ Spa.Fixedpoint.aFix_le
+-/
+import Spa.Lattice
+
+namespace Spa.Fixedpoint
+
+open FiniteHeightLattice (height fixedHeight)
+
+variable {α : Type*} [Lattice α] [DecidableEq α] [FiniteHeightLattice α]
+
+/-- Agda: `doStep`. `g` is gas; the invariant `c.length + g = h + 1` guarantees
+that when gas runs out the chain contradicts boundedness. -/
+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 ((fixedHeight (α := α)).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)
+
+/-- Agda: `fix`. Start iterating from `⊥`. -/
+def fix (f : α → α) (hf : Monotone f) : {a : α // a = f a} :=
+  doStep f hf (height (α := α) + 1) (RelSeries.singleton _ (FiniteHeightLattice.bot α))
+    (by simp)
+    (by simpa [RelSeries.last_singleton]
+          using FiniteHeightLattice.bot_le α (f (FiniteHeightLattice.bot α)))
+
+/-- Agda: `aᶠ`. -/
+def aFix (f : α → α) (hf : Monotone f) : α :=
+  (fix f hf).1
+
+/-- Agda: `aᶠ≈faᶠ`. -/
+theorem aFix_eq (f : α → α) (hf : Monotone f) :
+    aFix f hf = f (aFix f hf) :=
+  (fix f hf).2
+
+/-- Agda: `stepPreservesLess` — iteration stays below any fixed point. -/
+theorem 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 ((fixedHeight (α := α)).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)
+
+/-- Agda: `aᶠ≼` — `aFix` is below every fixed point of `f`. -/
+theorem aFix_le (f : α → α) (hf : Monotone f)
+    {a : α} (ha : a = f a) : aFix f hf ≤ a :=
+  doStep_le f hf ha _ _ _ _ (by simpa using FiniteHeightLattice.bot_le α a)
+
+end Spa.Fixedpoint
--- a/lean/Spa/Isomorphism.lean
+++ b/lean/Spa/Isomorphism.lean
@@ -0,0 +1,58 @@
+/-
+Port of `Isomorphism.agda` (`TransportFiniteHeight`).
+
+With propositional equality this module shrinks dramatically: the Agda
+hypotheses `f-preserves-≈`, `g-preserves-≈` are free, and `f-⊔-distr` /
+`g-⊔-distr` (which in the setoid world encoded monotonicity of `f` and `g`
+w.r.t. the derived order) become plain `Monotone` hypotheses. The chain
+transport `portChain₁` / `portChain₂` is mathlib's `LTSeries.map`, using that
+a monotone injective map between partial orders is strictly monotone.
+
+Correspondence:
+  IsInverseˡ / IsInverseʳ     ↦ explicit inverse hypotheses `hfg` / `hgf`
+  f-Injective / g-Injective   ↦ local `Function.LeftInverse.injective`
+  portChain₁ / portChain₂     ↦ LTSeries.map
+  instance fixedHeight        ↦ Spa.FixedHeight.transport
+  isFiniteHeightLattice,
+  finiteHeightLattice         ↦ Spa.FiniteHeightLattice.transport
+-/
+import Spa.Lattice
+
+namespace Spa
+
+namespace FixedHeight
+
+variable {α β : Type*} [PartialOrder α] [PartialOrder β] {h : ℕ}
+
+/-- Agda: `TransportFiniteHeight.fixedHeight`. Transport a `FixedHeight`
+structure along a monotone inverse pair `f : α → β`, `g : β → α`. -/
+def transport (fh : FixedHeight α h) (f : α → β) (g : β → α)
+    (hf : Monotone f) (hg : Monotone g)
+    (hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
+    FixedHeight β h where
+  bot := f fh.bot
+  top := f fh.top
+  longestChain :=
+    fh.longestChain.map f
+      (hf.strictMono_of_injective (Function.LeftInverse.injective hgf))
+  head_longestChain := by
+    rw [LTSeries.head_map, fh.head_longestChain]
+  last_longestChain := by
+    rw [LTSeries.last_map, fh.last_longestChain]
+  length_longestChain := fh.length_longestChain
+  bounded := fun c =>
+    fh.bounded
+      (c.map g (hg.strictMono_of_injective (Function.LeftInverse.injective hfg)))
+
+end FixedHeight
+
+/-- Agda: `TransportFiniteHeight.finiteHeightLattice`. -/
+def FiniteHeightLattice.transport {α β : Type*} [Lattice α] [Lattice β]
+    (I : FiniteHeightLattice α) (f : α → β) (g : β → α)
+    (hf : Monotone f) (hg : Monotone g)
+    (hgf : ∀ a, g (f a) = a) (hfg : ∀ b, f (g b) = b) :
+    FiniteHeightLattice β where
+  height := I.height
+  fixedHeight := I.fixedHeight.transport f g hf hg hgf hfg
+
+end Spa
--- a/lean/Spa/Language.lean
+++ b/lean/Spa/Language.lean
@@ -0,0 +1,90 @@
+/-
+Port of `Language.agda` (the `Program` record and re-exports).
+
+Correspondence:
+  Program record      ↦ structure Program (defs in the `Program` namespace)
+  graph               ↦ Program.graph
+  State               ↦ Program.State
+  initialState        ↦ Program.initialState
+  finalState          ↦ Program.finalState
+  trace               ↦ Program.trace
+  vars, vars-Unique   ↦ Program.vars, Program.vars_nodup
+                        (Finset.toList + Finset.nodup_toList replace
+                        `to-Listˢ` and the intrinsic MapSet uniqueness)
+  states, states-complete, states-Unique
+                      ↦ Program.states, .states_complete, .states_nodup
+  code                ↦ Program.code
+  _≟_, _≟ᵉ_           ↦ (instances, automatic for Fin/products)
+  incoming            ↦ Program.incoming
+  initialState-pred-∅ ↦ Program.incoming_initialState_eq_nil
+  edge⇒incoming       ↦ Program.mem_incoming_of_edge
+-/
+import Spa.Language.Base
+import Spa.Language.Semantics
+import Spa.Language.Graphs
+import Spa.Language.Traces
+import Spa.Language.Properties
+import Mathlib.Data.Finset.Sort
+import Mathlib.Data.String.Basic
+
+namespace Spa
+
+structure Program where
+  rootStmt : Stmt
+
+namespace Program
+
+variable (p : Program)
+
+def graph : Graph := Graph.wrap (buildCfg p.rootStmt)
+
+abbrev State : Type := p.graph.Index
+
+def initialState : p.State := (buildCfg p.rootStmt).wrapInput
+
+def finalState : p.State := (buildCfg p.rootStmt).wrapOutput
+
+/-- Agda: `Program.trace`. -/
+theorem trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
+    Trace p.graph p.initialState p.finalState [] ρ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (buildCfg_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
+
+/-- Agda: `vars` (via `vars-Set = Stmt-vars rootStmt`). `Finset.toList` is
+noncomputable, so the variables are listed in sorted order instead — this is
+the computable stand-in for MapSet's `to-List`. -/
+def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
+
+/-- Agda: `vars-Unique`. -/
+theorem vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
+
+def states : List p.State := p.graph.indices
+
+/-- Agda: `states-complete`. -/
+theorem states_complete (s : p.State) : s ∈ p.states := p.graph.mem_indices s
+
+/-- Agda: `states-Unique`. -/
+theorem states_nodup : p.states.Nodup := p.graph.nodup_indices
+
+/-- Agda: `code`. -/
+def code (st : p.State) : List BasicStmt := p.graph.nodes st
+
+/-- Agda: `incoming`. -/
+def incoming (s : p.State) : List p.State := p.graph.predecessors s
+
+/-- Agda: `initialState-pred-∅`. -/
+theorem incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
+  Graph.wrap_predecessors_eq_nil (buildCfg p.rootStmt) p.initialState
+    (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
+
+/-- Agda: `edge⇒incoming`. -/
+theorem mem_incoming_of_edge {s₁ s₂ : p.State}
+    (h : (s₁, s₂) ∈ p.graph.edges) : s₁ ∈ p.incoming s₂ :=
+  p.graph.mem_predecessors_of_edge h
+
+end Program
+
+end Spa
--- a/lean/Spa/Language/Base.lean
+++ b/lean/Spa/Language/Base.lean
@@ -0,0 +1,78 @@
+/-
+Port of `Language/Base.agda`.
+
+`StringSet` (built on `Lattice/MapSet.agda`, itself on `Lattice/Map.agda`) is
+lifted to mathlib's `Finset String`: `insertˢ ↦ insert`, `emptyˢ ↦ ∅`,
+`singletonˢ ↦ {·}`, `_⊔ˢ_ ↦ ∪`, `to-List ↦ Finset.toList` (with
+`Finset.nodup_toList` standing in for the intrinsic `Unique` proof).
+
+Constructor renaming (Agda mixfix has no direct Lean counterpart):
+  _+_ ↦ Expr.add      _-_ ↦ Expr.sub     `_ ↦ Expr.var    #_ ↦ Expr.num
+  _←_ ↦ BasicStmt.assign              noop ↦ BasicStmt.noop
+  ⟨_⟩ ↦ Stmt.basic    _then_ ↦ Stmt.andThen
+  if_then_else_ ↦ Stmt.ifElse         while_repeat_ ↦ Stmt.whileLoop
+
+The `_∈ᵉ_` / `_∈ᵇ_` variable-occurrence relations are ported as
+`Expr.HasVar` / `BasicStmt.HasVar`; the commented-out lemmas relating them to
+`Expr-vars` remain unported (they were commented out in the Agda, too).
+-/
+import Mathlib.Data.Finset.Basic
+
+namespace Spa
+
+inductive Expr where
+  | add (e₁ e₂ : Expr)
+  | sub (e₁ e₂ : Expr)
+  | var (x : String)
+  | num (n : ℕ)
+  deriving DecidableEq
+
+inductive BasicStmt where
+  | assign (x : String) (e : Expr)
+  | noop
+  deriving DecidableEq
+
+inductive Stmt where
+  | basic (bs : BasicStmt)
+  | andThen (s₁ s₂ : Stmt)
+  | ifElse (e : Expr) (s₁ s₂ : Stmt)
+  | whileLoop (e : Expr) (s : Stmt)
+  deriving DecidableEq
+
+/-- Agda: `_∈ᵉ_`. -/
+inductive Expr.HasVar : String → Expr → Prop
+  | addLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.add e₁ e₂)
+  | addRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.add e₁ e₂)
+  | subLeft {e₁ e₂ k} : Expr.HasVar k e₁ → Expr.HasVar k (.sub e₁ e₂)
+  | subRight {e₁ e₂ k} : Expr.HasVar k e₂ → Expr.HasVar k (.sub e₁ e₂)
+  | here {k} : Expr.HasVar k (.var k)
+
+/-- Agda: `_∈ᵇ_`. -/
+inductive BasicStmt.HasVar : String → BasicStmt → Prop
+  | assignLeft {k e} : BasicStmt.HasVar k (.assign k e)
+  | assignRight {k k' e} : Expr.HasVar k e → BasicStmt.HasVar k (.assign k' e)
+
+/-- Agda: `Expr-vars`. -/
+def Expr.vars : Expr → Finset String
+  | .add l r => l.vars ∪ r.vars
+  | .sub l r => l.vars ∪ r.vars
+  | .var s => {s}
+  | .num _ => ∅
+
+/-- Agda: `BasicStmt-vars`. -/
+def BasicStmt.vars : BasicStmt → Finset String
+  | .assign x e => {x} ∪ e.vars
+  | .noop => ∅
+
+/-- Agda: `Stmt-vars`. -/
+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
+
+/-- Agda: `Stmts-vars`. -/
+def Stmt.varsList (ss : List Stmt) : Finset String :=
+  ss.foldr (fun s acc => s.vars ∪ acc) ∅
+
+end Spa
--- a/lean/Spa/Language/Graphs.lean
+++ b/lean/Spa/Language/Graphs.lean
@@ -0,0 +1,169 @@
+/-
+Port of `Language/Graphs.agda`.
+
+Representation note: `nodes : Vec (List BasicStmt) size` becomes
+`nodes : Fin size → List BasicStmt`. With that, the `Data.Vec` lookup/append
+lemma stack (`lookup-++ˡ/ʳ`, `cast-is-id`, …) lifts into mathlib's
+`Fin.append` with `Fin.append_left` / `Fin.append_right`.
+
+Correspondence:
+  _↑ˡ_/_↑ʳ_ (on Fin)  ↦ Fin.castAdd / Fin.natAdd (mathlib)
+  _↑ˡⁱ_/_↑ʳⁱ_         ↦ liftIdxL / liftIdxR
+  _↑ˡᵉ_/_↑ʳᵉ_         ↦ liftEdgeL / liftEdgeR
+  _∙_                 ↦ Graph.comp   (scoped notation ∙)
+  _↦_                 ↦ Graph.link   (scoped notation ⤳)
+  loop                ↦ Graph.loop
+  _skipto_            ↦ Graph.skipto
+  _[_]                ↦ Graph.nodes (plain application)
+  singleton, wrap     ↦ Graph.singleton, Graph.wrap
+  buildCfg            ↦ buildCfg
+  indices             ↦ List.finRange (mathlib; `fins` from Utils.agda)
+  indices-complete    ↦ List.mem_finRange
+  indices-Unique      ↦ List.nodup_finRange
+  predecessors        ↦ Graph.predecessors
+  edge⇒predecessor    ↦ Graph.mem_predecessors_of_edge
+  predecessor⇒edge    ↦ Graph.edge_of_mem_predecessors
+-/
+import Spa.Language.Base
+import Mathlib.Data.Fin.Tuple.Basic
+import Mathlib.Data.List.ProdSigma
+import Mathlib.Data.List.FinRange
+
+namespace Spa
+
+structure Graph where
+  size : ℕ
+  nodes : Fin size → List BasicStmt
+  edges : List (Fin size × Fin size)
+  inputs : List (Fin size)
+  outputs : List (Fin size)
+
+namespace Graph
+
+abbrev Index (g : Graph) : Type := Fin g.size
+
+abbrev Edge (g : Graph) : Type := g.Index × g.Index
+
+/-- Agda: `_↑ˡⁱ_`. -/
+def liftIdxL {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) :=
+  l.map (Fin.castAdd m)
+
+/-- Agda: `_↑ʳⁱ_`. -/
+def liftIdxR (n : ℕ) {m : ℕ} (l : List (Fin m)) : List (Fin (n + m)) :=
+  l.map (Fin.natAdd n)
+
+/-- Agda: `_↑ˡᵉ_` (with `_↑ˡ_` on pairs inlined). -/
+def liftEdgeL {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))
+
+/-- Agda: `_↑ʳᵉ_` (with `_↑ʳ_` on pairs inlined). -/
+def liftEdgeR (n : ℕ) {m : ℕ} (l : List (Fin m × Fin m)) :
+    List (Fin (n + m) × Fin (n + m)) :=
+  l.map (fun e => (e.1.natAdd n, e.2.natAdd n))
+
+/-- Agda: `_∙_` — disjoint union. -/
+def comp (g₁ g₂ : Graph) : Graph where
+  size := g₁.size + g₂.size
+  nodes := Fin.append g₁.nodes g₂.nodes
+  edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges
+  inputs := liftIdxL g₁.inputs g₂.size ++ liftIdxR g₁.size g₂.inputs
+  outputs := liftIdxL g₁.outputs g₂.size ++ liftIdxR g₁.size g₂.outputs
+
+@[inherit_doc] scoped infixr:70 " ∙ " => Graph.comp
+
+/-- Agda: `_↦_` — sequencing: all outputs of `g₁` feed all inputs of `g₂`. -/
+def link (g₁ g₂ : Graph) : Graph where
+  size := g₁.size + g₂.size
+  nodes := Fin.append g₁.nodes g₂.nodes
+  edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges ++
+    (liftIdxL g₁.outputs g₂.size).product (liftIdxR g₁.size g₂.inputs)
+  inputs := liftIdxL g₁.inputs g₂.size
+  outputs := liftIdxR g₁.size g₂.outputs
+
+@[inherit_doc] scoped infixr:70 " ⤳ " => Graph.link
+
+/-- The entry node of a `loop` graph. -/
+def loopIn (g : Graph) : Fin (2 + g.size) := (0 : Fin 2).castAdd g.size
+
+/-- The exit node of a `loop` graph. -/
+def loopOut (g : Graph) : Fin (2 + g.size) := (1 : Fin 2).castAdd g.size
+
+/-- Agda: `loop`. -/
+def loop (g : Graph) : Graph where
+  size := 2 + g.size
+  nodes := Fin.append (fun _ : Fin 2 => []) g.nodes
+  edges := liftEdgeR 2 g.edges ++
+    (liftIdxR 2 g.inputs).map (g.loopIn, ·) ++
+    (liftIdxR 2 g.outputs).map (·, g.loopOut) ++
+    [(g.loopOut, g.loopIn), (g.loopIn, g.loopOut)]
+  inputs := [g.loopIn]
+  outputs := [g.loopOut]
+
+@[simp] theorem loop_inputs (g : Graph) : (loop g).inputs = [g.loopIn] := rfl
+
+@[simp] theorem loop_outputs (g : Graph) : (loop g).outputs = [g.loopOut] := rfl
+
+/-- Agda: `_skipto_` (unused by `buildCfg`, ported for parity). -/
+def skipto (g₁ g₂ : Graph) : Graph where
+  size := g₁.size + g₂.size
+  nodes := Fin.append g₁.nodes g₂.nodes
+  edges := liftEdgeL g₁.edges g₂.size ++ liftEdgeR g₁.size g₂.edges ++
+    (liftIdxL g₁.inputs g₂.size).product (liftIdxR g₁.size g₂.inputs)
+  inputs := liftIdxL g₁.inputs g₂.size
+  outputs := liftIdxR g₁.size g₂.inputs
+
+/-- Agda: `singleton`. -/
+def singleton (bss : List BasicStmt) : Graph where
+  size := 1
+  nodes := fun _ => bss
+  edges := []
+  inputs := [0]
+  outputs := [0]
+
+/-- Agda: `wrap`. -/
+def wrap (g : Graph) : Graph :=
+  singleton [] ⤳ g ⤳ singleton []
+
+end Graph
+
+open Graph in
+/-- Agda: `buildCfg`. -/
+def buildCfg : Stmt → Graph
+  | .basic bs => Graph.singleton [bs]
+  | .andThen s₁ s₂ => buildCfg s₁ ⤳ buildCfg s₂
+  | .ifElse _ s₁ s₂ => buildCfg s₁ ∙ buildCfg s₂
+  | .whileLoop _ s => Graph.loop (buildCfg s)
+
+namespace Graph
+
+variable (g : Graph)
+
+/-- Agda: `indices` (`fins` is mathlib's `List.finRange`). -/
+def indices : List g.Index := List.finRange g.size
+
+/-- Agda: `indices-complete`. -/
+theorem mem_indices (idx : g.Index) : idx ∈ g.indices :=
+  List.mem_finRange idx
+
+/-- Agda: `indices-Unique`. -/
+theorem nodup_indices : g.indices.Nodup :=
+  List.nodup_finRange g.size
+
+/-- Agda: `predecessors`. -/
+def predecessors (idx : g.Index) : List g.Index :=
+  g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)
+
+/-- Agda: `edge⇒predecessor`. -/
+theorem 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⟩
+
+/-- Agda: `predecessor⇒edge`. -/
+theorem 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 Graph
+
+end Spa
--- a/lean/Spa/Language/Properties.lean
+++ b/lean/Spa/Language/Properties.lean
@@ -0,0 +1,282 @@
+/-
+Port of `Language/Properties.agda`.
+
+Correspondence:
+  ↑-≢ (and the whole "ugly" Fin-disjointness block:
+    idx→f∉↑ʳᵉ, idx→f∉pair, idx→f∉cart, help, helpAll)
+                          ↦ Fin.castAdd_ne_natAdd + not_mem_edges_castAdd_link
+                            (mathlib `List.mem_append`/`mem_map`/`mem_product`
+                            replace the hand-rolled membership eliminations)
+  wrap-preds-∅            ↦ wrap_predecessors_eq_nil
+  wrap-input, wrap-output ↦ Graph.wrapInput/wrapOutput + wrap_inputs/wrap_outputs
+  Trace-∙ˡ/ʳ              ↦ Trace.comp_left / Trace.comp_right
+  Trace-↦ˡ/ʳ              ↦ Trace.link_left / Trace.link_right
+  Trace-loop              ↦ Trace.loop
+  EndToEndTrace-∙ˡ/ʳ      ↦ EndToEndTrace.comp_left / .comp_right
+  loop-edge-groups,
+  loop-edge-help          ↦ (inlined: the four edge groups are reached through
+                            `List.mem_append` directly)
+  EndToEndTrace-loop      ↦ EndToEndTrace.loop
+  EndToEndTrace-loop²     ↦ EndToEndTrace.loop_concat
+  EndToEndTrace-loop⁰     ↦ EndToEndTrace.loop_empty
+  _++_                    ↦ EndToEndTrace.concat
+  EndToEndTrace-singleton ↦ EndToEndTrace.singleton (+ .singleton_nil)
+  EndToEndTrace-wrap      ↦ EndToEndTrace.wrap
+  buildCfg-sufficient     ↦ buildCfg_sufficient
+-/
+import Spa.Language.Traces
+
+namespace Spa
+
+open Graph
+
+/-- Agda: `↑-≢`. -/
+theorem 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
+
+/-! ### Trace embeddings -/
+
+section Embeddings
+
+variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
+
+/-- Agda: `Trace-∙ˡ`. -/
+theorem Trace.comp_left {idx₁ idx₂ : g₁.Index}
+    (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (g₁ ∙ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
+  induction tr with
+  | single hbs =>
+    exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
+      Fin.append_left])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
+    · exact List.mem_append_left _ (List.mem_map_of_mem _ he)
+
+/-- Agda: `Trace-∙ʳ`. -/
+theorem Trace.comp_right {idx₁ idx₂ : g₂.Index}
+    (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (g₁ ∙ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
+  induction tr with
+  | single hbs =>
+    exact Trace.single (by rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
+      Fin.append_right])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · rwa [show (g₁ ∙ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
+    · exact List.mem_append_right _ (List.mem_map_of_mem _ he)
+
+/-- Agda: `Trace-↦ˡ`. -/
+theorem Trace.link_left {idx₁ idx₂ : g₁.Index}
+    (tr : Trace g₁ idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (g₁ ⤳ g₂) (idx₁.castAdd g₂.size) (idx₂.castAdd g₂.size) ρ₁ ρ₂ := by
+  induction tr with
+  | single hbs =>
+    exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
+      Fin.append_left])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_left]
+    · exact List.mem_append_left _ (List.mem_append_left _ (List.mem_map_of_mem _ he))
+
+/-- Agda: `Trace-↦ʳ`. -/
+theorem Trace.link_right {idx₁ idx₂ : g₂.Index}
+    (tr : Trace g₂ idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (g₁ ⤳ g₂) (idx₁.natAdd g₁.size) (idx₂.natAdd g₁.size) ρ₁ ρ₂ := by
+  induction tr with
+  | single hbs =>
+    exact Trace.single (by rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl,
+      Fin.append_right])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · rwa [show (g₁ ⤳ g₂).nodes = Fin.append g₁.nodes g₂.nodes from rfl, Fin.append_right]
+    · exact List.mem_append_left _
+        (List.mem_append_right _ (List.mem_map_of_mem _ he))
+
+/-- Agda: `EndToEndTrace-∙ˡ`. -/
+theorem EndToEndTrace.comp_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.comp_left⟩
+
+/-- Agda: `EndToEndTrace-∙ʳ`. -/
+theorem EndToEndTrace.comp_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.comp_right⟩
+
+/-- Agda: `_++_` — sequencing end-to-end traces over `⤳`. -/
+theorem 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₂,
+          Trace.concat tr₁.link_left ?_ tr₂.link_right⟩
+  exact List.mem_append_right _
+    (List.mem_product.mpr ⟨List.mem_map_of_mem _ h₂, List.mem_map_of_mem _ k₁⟩)
+
+end Embeddings
+
+/-! ### Loops -/
+
+section Loop
+
+variable {g : Graph} {ρ₁ ρ₂ ρ₃ : Env}
+
+/-- Agda: `Trace-loop`. -/
+theorem Trace.loop {idx₁ idx₂ : g.Index} (tr : Trace g idx₁ idx₂ ρ₁ ρ₂) :
+    Trace (Graph.loop g) (idx₁.natAdd 2) (idx₂.natAdd 2) ρ₁ ρ₂ := by
+  induction tr with
+  | single hbs =>
+    exact Trace.single (by
+      rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl,
+        Fin.append_right])
+  | edge hbs he _ ih =>
+    refine Trace.edge ?_ ?_ ih
+    · rwa [show (Graph.loop g).nodes = Fin.append (fun _ : Fin 2 => []) g.nodes from rfl,
+        Fin.append_right]
+    · exact List.mem_append_left _ (List.mem_append_left _
+        (List.mem_append_left _ (List.mem_map_of_mem _ he)))
+
+private theorem loop_nodes_at_in :
+    (Graph.loop g).nodes g.loopIn = [] :=
+  Fin.append_left (fun _ : Fin 2 => []) g.nodes 0
+
+private theorem loop_nodes_at_out :
+    (Graph.loop g).nodes g.loopOut = [] :=
+  Fin.append_left (fun _ : Fin 2 => []) g.nodes 1
+
+/-- Agda: `EndToEndTrace-loop`. -/
+theorem 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.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hin
+    (Trace.concat tr.loop hout (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil)))
+
+private theorem 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 _ _
+
+/-- Agda: `EndToEndTrace-loop²`. -/
+theorem 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 _,
+    Trace.concat tr₁ loop_edge_out_in tr₂⟩
+
+/-- Agda: `EndToEndTrace-loop⁰`. -/
+theorem 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.concat (Trace.single (loop_nodes_at_in ▸ EvalBasicStmts.nil)) hedge
+      (Trace.single (loop_nodes_at_out ▸ EvalBasicStmts.nil))⟩
+
+end Loop
+
+/-! ### Singletons, wrap, and the main result -/
+
+/-- Agda: `EndToEndTrace-singleton`. -/
+theorem EndToEndTrace.singleton {bss : List BasicStmt} {ρ₁ ρ₂ : Env}
+    (h : EvalBasicStmts ρ₁ bss ρ₂) : EndToEndTrace (Graph.singleton bss) ρ₁ ρ₂ :=
+  ⟨(0 : Fin 1), List.mem_singleton_self _, (0 : Fin 1), List.mem_singleton_self _,
+   Trace.single h⟩
+
+/-- Agda: `EndToEndTrace-singleton[]`. -/
+theorem EndToEndTrace.singleton_nil (ρ : Env) :
+    EndToEndTrace (Graph.singleton []) ρ ρ :=
+  EndToEndTrace.singleton EvalBasicStmts.nil
+
+/-- Agda: `EndToEndTrace-wrap`. -/
+theorem EndToEndTrace.wrap {g : Graph} {ρ₁ ρ₂ : Env}
+    (etr : EndToEndTrace g ρ₁ ρ₂) : EndToEndTrace (Graph.wrap g) ρ₁ ρ₂ :=
+  (EndToEndTrace.singleton_nil ρ₁).concat (etr.concat (EndToEndTrace.singleton_nil ρ₂))
+
+/-- Agda: `buildCfg-sufficient` — every terminating execution is witnessed by
+an end-to-end trace through the control-flow graph. -/
+theorem buildCfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
+    (h : EvalStmt ρ₁ s ρ₂) : EndToEndTrace (buildCfg s) ρ₁ ρ₂ := by
+  induction h with
+  | basic ρ₁ ρ₂ bs hbs =>
+    exact EndToEndTrace.singleton (EvalBasicStmts.cons hbs EvalBasicStmts.nil)
+  | andThen ρ₁ ρ₂ ρ₃ s₁ s₂ _ _ ih₁ ih₂ =>
+    exact ih₁.concat ih₂
+  | ifTrue ρ₁ ρ₂ e z s₁ s₂ _ _ _ ih =>
+    exact ih.comp_left
+  | ifFalse ρ₁ ρ₂ e s₁ s₂ _ _ ih =>
+    exact ih.comp_right
+  | whileTrue ρ₁ ρ₂ ρ₃ e z s _ _ _ _ ih₁ ih₂ =>
+    exact (ih₁.loop).loop_concat ih₂
+  | whileFalse ρ e s _ =>
+    exact EndToEndTrace.loop_empty
+
+/-! ### The wrapped graph's entry has no predecessors (Agda's "ugly" block) -/
+
+/-- The input of `wrap g` (Agda: `wrap-input`). -/
+def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
+  (0 : Fin 1).castAdd ((g ⤳ Graph.singleton []).size)
+
+/-- The output of `wrap g` (Agda: `wrap-output`). -/
+def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
+  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
+
+theorem Graph.wrap_inputs (g : Graph) :
+    (Graph.wrap g).inputs = [g.wrapInput] := rfl
+
+theorem Graph.wrap_outputs (g : Graph) :
+    (Graph.wrap g).outputs = [g.wrapOutput] := rfl
+
+/-- Agda: `help`/`helpAll` — no edge of `singleton [] ⤳ g₂` ends at a
+`castAdd`-injected node (all edge targets are `natAdd`s). -/
+private theorem not_mem_edges_castAdd_link {g₂ : Graph} (i : Fin 1)
+    (idx : (Graph.singleton [] ⤳ g₂).Index) :
+    ((idx, i.castAdd g₂.size) : (Graph.singleton [] ⤳ g₂).Edge)
+      ∉ (Graph.singleton [] ⤳ g₂).edges := by
+  intro h
+  rcases List.mem_append.mp h with h' | h'
+  · rcases List.mem_append.mp h' with h'' | h''
+    · -- lifted edges of `singleton []`: there are none
+      simp [Graph.singleton, Graph.liftEdgeL] 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
+
+/-- Agda: `wrap-preds-∅` — the entry node of a wrapped graph has no
+incoming edges. -/
+theorem Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
+    (h : idx ∈ (Graph.wrap g).inputs) :
+    (Graph.wrap g).predecessors idx = [] := by
+  rw [Graph.wrap_inputs, List.mem_singleton] at h
+  subst h
+  rw [Graph.predecessors, List.filter_eq_nil_iff]
+  intro idx' _
+  simpa using not_mem_edges_castAdd_link (g₂ := g ⤳ Graph.singleton []) 0 idx'
+
+end Spa
--- a/lean/Spa/Language/Semantics.lean
+++ b/lean/Spa/Language/Semantics.lean
@@ -0,0 +1,91 @@
+/-
+Port of `Language/Semantics.agda`.
+
+Correspondence:
+  Value (↑ᶻ)        ↦ Value.int
+  Env               ↦ Env (= List (String × Value))
+  _∈_ (env lookup)  ↦ Env.Mem
+  _,_⇒ᵉ_            ↦ EvalExpr
+  _,_⇒ᵇ_            ↦ EvalBasicStmt
+  _,_⇒ᵇˢ_           ↦ EvalBasicStmts
+  _,_⇒ˢ_            ↦ EvalStmt
+  LatticeInterpretation:
+    ⟦_⟧             ↦ interp
+    ⟦⟧-respects-≈   ↦ (trivial with `=`; field dropped)
+    ⟦⟧-⊔-∨          ↦ interp_sup
+    ⟦⟧-⊓-∧          ↦ interp_inf
+    (the `Utils` combinators `_⇒_`, `_∨_`, `_∧_` are inlined as plain logic)
+-/
+import Spa.Language.Base
+import Spa.Lattice
+
+namespace Spa
+
+inductive Value where
+  | int (z : ℤ)
+  deriving DecidableEq
+
+def Env : Type := List (String × Value)
+
+/-- Agda: `_∈_` on environments — lookup respecting shadowing. -/
+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') :: ρ)
+
+/-- Agda: `_,_⇒ᵉ_`. -/
+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₂))
+
+/-- Agda: `_,_⇒ᵇ_`. -/
+inductive EvalBasicStmt : Env → BasicStmt → Env → Prop
+  | noop (ρ : Env) : EvalBasicStmt ρ .noop ρ
+  | assign (ρ : Env) (x : String) (e : Expr) (v : Value) :
+      EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ)
+
+/-- Agda: `_,_⇒ᵇˢ_`. -/
+inductive EvalBasicStmts : Env → List BasicStmt → Env → Prop
+  | nil {ρ : Env} : EvalBasicStmts ρ [] ρ
+  | cons {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} :
+      EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmts ρ₂ bss ρ₃ →
+      EvalBasicStmts ρ₁ (bs :: bss) ρ₃
+
+/-- Agda: `_,_⇒ˢ_`. -/
+inductive EvalStmt : Env → Stmt → Env → Prop
+  | 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) ρ
+
+/-- Agda: `LatticeInterpretation` (used there as an instance argument `⦃·⦄`,
+hence a typeclass here). -/
+class LatticeInterpretation (L : Type*) [Lattice L] where
+  interp : L → Value → Prop
+  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
--- a/lean/Spa/Language/Traces.lean
+++ b/lean/Spa/Language/Traces.lean
@@ -0,0 +1,38 @@
+/-
+Port of `Language/Traces.agda`.
+
+Correspondence:
+  Trace          ↦ Trace (a `Prop`-valued inductive; only used in proofs)
+  _++⟨_⟩_        ↦ Trace.concat
+  EndToEndTrace  ↦ EndToEndTrace (a `Prop`-valued structure, like `∃`; its
+                   fields are accessed by destructuring inside proofs)
+-/
+import Spa.Language.Semantics
+import Spa.Language.Graphs
+
+namespace Spa
+
+/-- Agda: `Trace`. -/
+inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Prop
+  | single {ρ₁ ρ₂ : Env} {idx : g.Index} :
+      EvalBasicStmts ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
+  | edge {ρ₁ ρ₂ ρ₃ : Env} {idx₁ idx₂ idx₃ : g.Index} :
+      EvalBasicStmts ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
+      Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
+
+/-- Agda: `_++⟨_⟩_`. -/
+theorem Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
+    {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
+    (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
+    Trace g idx₁ idx₄ ρ₁ ρ₃ := by
+  induction tr₁ with
+  | single hbs => exact Trace.edge hbs he tr₂
+  | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)
+
+/-- Agda: `EndToEndTrace` (an existential package, destructured in proofs). -/
+inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Prop
+  | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs)
+      (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs)
+      (trace : Trace g idx₁ idx₂ ρ₁ ρ₂) : EndToEndTrace g ρ₁ ρ₂
+
+end Spa
--- a/lean/Spa/Lattice.lean
+++ b/lean/Spa/Lattice.lean
@@ -0,0 +1,168 @@
+/-
+Port of `Lattice.agda`.
+
+Most of the Agda module is *lifted* into mathlib, since we now work with
+propositional equality instead of a setoid:
+
+  IsSemilattice A _≈_ _⊔_   ↦  SemilatticeSup α
+  IsLattice A _≈_ _⊔_ _⊓_   ↦  Lattice α
+  _≼_ (a ⊔ b ≈ b)           ↦  a ≤ b           (bridge: `sup_eq_right`)
+  _≺_                       ↦  a < b
+  Monotonic                 ↦  Monotone
+  ⊔-assoc/⊔-comm/⊔-idemp    ↦  sup_assoc/sup_comm/sup_idem
+  absorb-⊔-⊓/absorb-⊓-⊔     ↦  sup_inf_self/inf_sup_self
+  ≼-refl/≼-trans/≼-antisym  ↦  le_refl/le_trans/le_antisymm
+  x≼x⊔y                     ↦  le_sup_left
+  ⊔-Monotonicˡ/ʳ            ↦  sup_le_sup_left/sup_le_sup_right
+  id-Mono/const-Mono        ↦  monotone_id/monotone_const
+  IsDecidable               ↦  DecidableEq (kept only where computation needs it)
+  Chain (Chain.agda)        ↦  LTSeries (chains of `<`); concat ↦ RelSeries.smash
+  ChainMapping.Chain-map    ↦  LTSeries.map (Monotone + Injective ⇒ StrictMono)
+
+What remains custom is exactly what mathlib does not have:
+  * monotonicity of folds over pairwise-related lists (foldr-Mono & friends),
+  * the fixed-height machinery (Chain.Height ↦ FixedHeight, Bounded),
+  * the proof that the bottom of the longest chain is a least element (⊥≼).
+-/
+import Mathlib.Order.Lattice
+import Mathlib.Order.RelSeries
+
+namespace Spa
+
+/-! ### Monotonicity helpers (Lattice.agda, `Monotonic₂` and fold lemmas) -/
+
+/-- Agda: `Monotonic₂` (a pair of one-sided monotonicity proofs). -/
+def Monotone₂ {α β γ : Type*} [Preorder α] [Preorder β] [Preorder γ]
+    (f : α → β → γ) : Prop :=
+  (∀ b, Monotone fun a => f a b) ∧ (∀ a, Monotone (f a))
+
+section Folds
+
+variable {α β : Type*} [Preorder α] [Preorder β]
+
+/-- Agda: `foldr-Mono`. `Pairwise _≼₁_` becomes `List.Forall₂ (· ≤ ·)`. -/
+theorem foldr_mono {l₁ l₂ : List α} (f : α → β → β) {b₁ b₂ : β}
+    (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
+    (hf₁ : ∀ b, Monotone fun a => f a 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)
+
+/-- Agda: `foldl-Mono`. -/
+theorem foldl_mono {l₁ l₂ : List α} (f : β → α → β) {b₁ b₂ : β}
+    (hl : List.Forall₂ (· ≤ ·) l₁ l₂) (hb : b₁ ≤ b₂)
+    (hf₁ : ∀ a, Monotone fun b => f b 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
+/-- Agda: `foldr-Mono'` (fixed list, varying accumulator). -/
+theorem foldr_mono' (l : List α) (f : α → β → β)
+    (hf : ∀ a, Monotone (f a)) : Monotone fun b => l.foldr f b := by
+  intro b₁ b₂ hb
+  induction l with
+  | nil => exact hb
+  | cons x xs ih => exact hf x ih
+
+omit [Preorder α] in
+/-- Agda: `foldl-Mono'`. -/
+theorem foldl_mono' (l : List α) (f : β → α → β)
+    (hf : ∀ a, Monotone fun b => f b 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)
+
+end Folds
+
+/-! ### Fixed height (Chain.agda `Bounded`/`Height`, Lattice.agda `FixedHeight`) -/
+
+/-- Agda: `Chain.Bounded`. Every `<`-chain has length at most `n`. -/
+def BoundedChains (α : Type*) [Preorder α] (n : ℕ) : Prop :=
+  ∀ c : LTSeries α, c.length ≤ n
+
+/-- Agda: `Chain.Height` (with `FixedHeight h = Height h` from Lattice.agda).
+A longest chain runs from `⊥` to `⊤` and has length exactly `height`;
+no chain is longer. -/
+structure FixedHeight (α : Type*) [Preorder α] (height : ℕ) where
+  bot : α
+  top : α
+  longestChain : LTSeries α
+  head_longestChain : longestChain.head = bot
+  last_longestChain : longestChain.last = top
+  length_longestChain : longestChain.length = height
+  bounded : BoundedChains α height
+
+/-- Agda: `Chain.Bounded-suc-n` (a bounded order admits no chain one longer). -/
+theorem BoundedChains.no_longer {α : Type*} [Preorder α] {n : ℕ}
+    (h : BoundedChains α n) (c : LTSeries α) : c.length ≠ n + 1 :=
+  fun hc => absurd (h c) (by omega)
+
+/-- Re-index a `FixedHeight` along an equality of heights (used where Agda
+just rewrites with arithmetic identities). -/
+def FixedHeight.cast {α : Type*} [Preorder α] {m n : ℕ} (h : m = n)
+    (fh : FixedHeight α m) : FixedHeight α n where
+  bot := fh.bot
+  top := fh.top
+  longestChain := fh.longestChain
+  head_longestChain := fh.head_longestChain
+  last_longestChain := fh.last_longestChain
+  length_longestChain := h ▸ fh.length_longestChain
+  bounded := h ▸ fh.bounded
+
+@[simp] theorem FixedHeight.cast_bot {α : Type*} [Preorder α] {m n : ℕ}
+    (h : m = n) (fh : FixedHeight α m) : (fh.cast h).bot = fh.bot := rfl
+
+/-- Agda: `IsFiniteHeightLattice` / `FiniteHeightLattice` (bundled). Like the
+Agda code (which took `IsFiniteHeightLattice` as an instance argument `⦃·⦄`),
+this is a typeclass; downstream modules pick it up by instance resolution
+rather than threading a `FixedHeight` value. -/
+class FiniteHeightLattice (α : Type*) [Lattice α] where
+  height : ℕ
+  fixedHeight : FixedHeight α height
+
+namespace FixedHeight
+
+variable {α : Type*} [Lattice α] {h : ℕ}
+
+/-- Agda: `Known-⊥`. -/
+def KnownBot (fh : FixedHeight α h) : Prop := ∀ a : α, fh.bot ≤ a
+
+/-- Agda: `Known-⊤`. -/
+def KnownTop (fh : FixedHeight α h) : Prop := ∀ a : α, a ≤ fh.top
+
+/-- Agda: `⊥≼` — the bottom of the longest chain is a least element.
+Same proof: if `⊥ ⊓ a ≠ ⊥` then `⊥ ⊓ a < ⊥` prepends to the longest chain,
+contradicting boundedness. (The decidability hypothesis of the Agda proof is
+not needed classically.) -/
+theorem bot_le (fh : FixedHeight α h) : fh.KnownBot := by
+  intro a
+  by_cases heq : fh.bot ⊓ a = fh.bot
+  · exact inf_eq_left.mp heq
+  · exfalso
+    have hlt : fh.bot ⊓ a < fh.bot :=
+      lt_of_le_of_ne inf_le_left heq
+    exact fh.bounded.no_longer
+      (fh.longestChain.cons (fh.bot ⊓ a) (fh.head_longestChain ▸ hlt))
+      (by simp [RelSeries.cons, fh.length_longestChain])
+
+end FixedHeight
+
+namespace FiniteHeightLattice
+
+variable (α : Type*) [Lattice α] [FiniteHeightLattice α]
+
+/-- Agda: the `⊥` of `Chain.Height`, with the type explicit. -/
+def bot : α := (fixedHeight (α := α)).bot
+
+/-- Agda: `⊥≼` for the instance bottom. -/
+theorem bot_le (a : α) : bot α ≤ a := FixedHeight.bot_le _ a
+
+end FiniteHeightLattice
+
+end Spa
--- a/lean/Spa/Lattice/AboveBelow.lean
+++ b/lean/Spa/Lattice/AboveBelow.lean
@@ -0,0 +1,289 @@
+/-
+Port of `Lattice/AboveBelow.agda`: the flat lattice obtained by adjoining a
+top and bottom element to an (unordered, decidable-equality) type.
+
+With propositional equality the `_≈_` data type and its equivalence/decidability
+proofs disappear (`deriving DecidableEq`). The lattice itself cannot be lifted:
+mathlib has no "flat lattice on a discrete type". The `Lattice` instance is
+built with `Lattice.mk'`, which — exactly like the Agda module — consumes the
+two semilattices (comm/assoc, idempotence derived) plus the absorption laws,
+and defines `a ≤ b ↔ a ⊔ b = b` (Agda's `_≼_`).
+
+The Agda module's `Plain x` submodule (the witness `x` seeds the longest chain
+`⊥ ≺ [x] ≺ ⊤`) becomes `plainFixedHeight x`; the boundedness proof `isLongest`
+is restated through a rank function since chains are mathlib `LTSeries` rather
+than a pattern-matchable inductive (the `¬-Chain-⊤`-style case analysis lives
+in `rank_strictMono`).
+-/
+import Spa.Lattice
+
+namespace Spa
+
+/-- Agda: `AboveBelow` with constructors `⊥`, `⊤`, `[_]`. -/
+inductive AboveBelow (α : Type*) where
+  | bot
+  | top
+  | mk (x : α)
+  deriving DecidableEq
+
+namespace AboveBelow
+
+/-- Agda: the `Showable` instance. -/
+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
+
+/-! Agda: `⊥⊔x≡x`, `⊤⊔x≡⊤`, `x⊔⊥≡x`, `x⊔⊤≡⊤`, and the `[x]⊔[y]` reductions
+(`x≈y⇒[x]⊔[y]≡[x]` / `x̷≈y⇒[x]⊔[y]≡⊤` are the two branches of `mk_sup_mk`). -/
+
+@[simp] theorem bot_sup (x : AboveBelow α) : bot ⊔ x = x := rfl
+@[simp] theorem top_sup (x : AboveBelow α) : top ⊔ x = top := rfl
+@[simp] theorem sup_bot (x : AboveBelow α) : x ⊔ bot = x := by cases x <;> rfl
+@[simp] theorem sup_top (x : AboveBelow α) : x ⊔ top = top := by cases x <;> rfl
+@[simp] theorem mk_sup_mk (x y : α) :
+    (mk x ⊔ mk y : AboveBelow α) = if x = y then mk x else top := rfl
+
+@[simp] theorem bot_inf (x : AboveBelow α) : bot ⊓ x = bot := rfl
+@[simp] theorem top_inf (x : AboveBelow α) : top ⊓ x = x := rfl
+@[simp] theorem inf_bot (x : AboveBelow α) : x ⊓ bot = bot := by cases x <;> rfl
+@[simp] theorem inf_top (x : AboveBelow α) : x ⊓ top = x := by cases x <;> rfl
+@[simp] theorem mk_inf_mk (x y : α) :
+    (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
+
+/-- Agda: `⊔-comm`. -/
+protected theorem sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
+    [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
+  split_ifs with h₁ h₂ h₂ <;> simp_all
+
+/-- Agda: `⊔-assoc`. -/
+protected theorem sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
+    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk]
+  split_ifs <;> simp_all
+
+/-- Agda: `⊓-comm`. -/
+protected theorem inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp only
+    [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
+  split_ifs with h₁ h₂ h₂ <;> simp_all
+
+/-- Agda: `⊓-assoc`. -/
+protected theorem inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> rcases c with _ | _ | z <;>
+    simp only [bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk]
+  split_ifs <;> simp_all
+
+/-- Agda: `absorb-⊔-⊓`. -/
+protected theorem sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
+    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
+               bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
+    try (split_ifs <;> simp_all)
+
+/-- Agda: `absorb-⊓-⊔`. -/
+protected theorem inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
+    simp only [bot_sup, sup_bot, top_sup, sup_top, mk_sup_mk,
+               bot_inf, inf_bot, top_inf, inf_top, mk_inf_mk] <;>
+    try (split_ifs <;> simp_all)
+
+/-- Agda: `isLattice` (via the two semilattices + absorption, like the Agda
+record; `Lattice.mk'` derives idempotence and sets `a ≤ b ↔ a ⊔ b = b`). -/
+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
+
+theorem le_iff {a b : AboveBelow α} : a ≤ b ↔ a ⊔ b = b := sup_eq_right.symm
+
+/-- Agda: `⊥≺[x]` (the `≤` part; `⊥` is least). -/
+theorem bot_le' (a : AboveBelow α) : (bot : AboveBelow α) ≤ a :=
+  le_iff.mpr (bot_sup a)
+
+/-- Agda: `[x]≺⊤` (the `≤` part; `⊤` is greatest). -/
+theorem le_top' (a : AboveBelow α) : a ≤ (top : AboveBelow α) :=
+  le_iff.mpr (sup_top a)
+
+theorem bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
+  lt_of_le_of_ne (bot_le' _) (by simp)
+
+theorem mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
+  lt_of_le_of_ne (le_top' _) (by simp)
+
+theorem bot_lt_top : (bot : AboveBelow α) < top :=
+  lt_of_le_of_ne (bot_le' _) (by simp)
+
+/-- The order of the flat lattice, by cases (used to discharge the
+monotonicity obligations that were `postulate`d in `Analysis/Sign.agda` and
+`Analysis/Constant.agda`). -/
+theorem le_cases {a b : AboveBelow α} (h : a ≤ b) :
+    a = bot ∨ b = top ∨ a = b := by
+  have hsup := le_iff.mp h
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y
+  · exact Or.inl rfl
+  · exact Or.inr (Or.inl rfl)
+  · exact Or.inl rfl
+  · exact absurd hsup (by simp)
+  · exact Or.inr (Or.inl rfl)
+  · exact absurd hsup (by simp)
+  · exact absurd hsup (by simp)
+  · exact Or.inr (Or.inl rfl)
+  · rw [mk_sup_mk] at hsup
+    by_cases hxy : x = y
+    · exact Or.inr (Or.inr (by rw [hxy]))
+    · rw [if_neg hxy] at hsup
+      exact absurd hsup (by simp)
+
+/-- Monotonicity for *strict* operations on flat lattices: if `f` sends `⊥` to
+`⊥` (in either argument) and `⊤` to `⊤` (against any non-`⊥` argument), it is
+monotone in both arguments — regardless of its values on plain elements.
+`Analysis/Sign.agda` and `Analysis/Constant.agda` postulated exactly these
+monotonicity facts for their `plus`/`minus`, all of which have this shape. -/
+theorem monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
+    (f : AboveBelow α → AboveBelow β → AboveBelow γ)
+    (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
+    (htopl : ∀ y, y ≠ bot → f top y = top)
+    (htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
+  constructor
+  · intro y a b hab
+    show f a y ≤ f b y
+    rcases le_cases hab with rfl | rfl | rfl
+    · rw [hbotl]; exact bot_le' _
+    · rcases eq_or_ne y bot with rfl | hy
+      · rw [hbotr, hbotr]
+      · rw [htopl y hy]; exact le_top' _
+    · exact le_rfl
+  · intro x a b hab
+    rcases le_cases hab with rfl | rfl | rfl
+    · rw [hbotr]; exact bot_le' _
+    · rcases eq_or_ne x bot with rfl | hx
+      · rw [hbotl, hbotl]
+      · rw [htopr x hx]; exact le_top' _
+    · exact le_rfl
+
+/-! ### Interpretations of flat lattices
+
+The `⟦⟧-⊔-∨` / `⟦⟧-⊓-∧` proofs of `Analysis/Sign.agda` and
+`Analysis/Constant.agda` are the same case analysis; only the meaning of the
+plain elements differs. Factored here, they need just `P ⊥ ↦ False`,
+`P ⊤ ↦ True`, and (for `⊓`) disjointness of distinct plain elements. -/
+
+section Interp
+
+variable {V : Type*} {P : AboveBelow α → V → Prop}
+
+/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` / `⟦⟧ᶜ-⊔ᶜ-∨`, generalized. -/
+theorem interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
+  rcases s₁ with _ | _ | x
+  · rw [bot_sup]; exact h.resolve_left (hbot v)
+  · rw [top_sup]; exact htop v
+  · rcases s₂ with _ | _ | y
+    · rw [sup_bot]; exact h.resolve_right (hbot v)
+    · rw [sup_top]; exact htop v
+    · rw [mk_sup_mk]
+      split
+      · next heq => subst heq; exact h.elim id id
+      · exact htop v
+
+/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` / `⟦⟧ᶜ-⊓ᶜ-∧`, generalized. -/
+theorem interp_inf_of
+    (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
+  rcases s₁ with _ | _ | x
+  · rw [bot_inf]; exact h.1
+  · rw [top_inf]; exact h.2
+  · rcases s₂ with _ | _ | y
+    · rw [inf_bot]; exact h.2
+    · rw [inf_top]; exact h.1
+    · rw [mk_inf_mk]
+      split
+      · next heq => subst heq; exact h.1
+      · next hne => exact absurd h (hdisj hne v)
+
+end Interp
+
+/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains
+(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
+def rank : AboveBelow α → ℕ
+  | bot => 0
+  | mk _ => 1
+  | top => 2
+
+/-- Agda: the impossibility of `[x] ≺ [y]` (combines `x≺[y]⇒x≡⊥` and
+`[x]≺y⇒y≡⊤`: the flat middle layer is an antichain). -/
+theorem not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
+  intro h
+  obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
+  have hsup := le_iff.mp hle
+  rw [mk_sup_mk] at hsup
+  by_cases hxy : x = y
+  · rw [if_pos hxy] at hsup
+    exact hne hsup
+  · rw [if_neg hxy] at hsup
+    exact absurd hsup (by simp)
+
+theorem rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
+  intro a b hab
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y
+  · exact absurd hab (lt_irrefl _)
+  · simp [rank]
+  · simp [rank]
+  · exact absurd hab (bot_le' _).not_lt
+  · exact absurd hab (lt_irrefl _)
+  · exact absurd hab (le_top' _).not_lt
+  · exact absurd hab (bot_le' _).not_lt
+  · simp [rank]
+  · exact absurd hab (not_mk_lt_mk x y)
+
+/-- Agda: `isLongest` — no chain is longer than 2. -/
+theorem 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
+
+/-- Agda: `Plain.longestChain` and `Plain.fixedHeight` — the witness `x`
+seeds the chain `⊥ ≺ [x] ≺ ⊤` of length 2. -/
+def plainFixedHeight (x : α) : FixedHeight (AboveBelow α) 2 where
+  bot := bot
+  top := top
+  longestChain :=
+    ((RelSeries.singleton _ bot).snoc (mk x)
+        (by rw [RelSeries.last_singleton]; exact bot_lt_mk x)).snoc top
+      (by rw [RelSeries.last_snoc]; exact mk_lt_top x)
+  head_longestChain := by simp
+  last_longestChain := by simp
+  length_longestChain := by simp [RelSeries.snoc, RelSeries.append]
+  bounded := boundedChains
+
+/-- Agda: `Plain.isFiniteHeightLattice` / `Plain.finiteHeightLattice`
+(`default` plays the role of the Agda module parameter `x`). -/
+instance [Inhabited α] : FiniteHeightLattice (AboveBelow α) where
+  height := 2
+  fixedHeight := plainFixedHeight default
+
+end AboveBelow
+
+end Spa
--- a/lean/Spa/Lattice/FiniteMap.lean
+++ b/lean/Spa/Lattice/FiniteMap.lean
@@ -0,0 +1,672 @@
+/-
+Port of `Lattice/FiniteMap.agda` (and the parts of `Lattice/Map.agda` it was
+built on).
+
+Representation change enabled by dropping the setoid: a finite map over a
+*fixed* key list `ks` is an association list whose key spine is *exactly* `ks`:
+
+    FiniteMap A B ks := { l : List (A × B) // l.map Prod.fst = ks }
+
+Since the spine (including order) is pinned by the type, the representation is
+canonical and propositional equality coincides with the Agda `_≈_` (pointwise
+value equality). The 1100-line `Lattice/Map.agda` — whose unordered-keys
+union/intersection and `Provenance` machinery existed to make `_≈_` workable —
+collapses into the positional `combine` below.
+
+Correspondence (Agda ↦ Lean):
+  FiniteMap, _≈_, ≈-Decidable    ↦ FiniteMap, `=`, DecidableEq instance
+  _⊔_/_⊓_ (via Map union/inter)  ↦ Max/Min via `combine`
+  isUnionSemilattice,
+  isIntersectSemilattice,
+  isLattice, lattice             ↦ instance Lattice (FiniteMap A B ks) (Lattice.mk',
+                                   i.e. the same "two semilattices + absorption" data)
+  _∈_, _∈k_, ∈k-dec, forget      ↦ Membership instance, MemKey (+ Decidable),
+                                   mem_key_of_mem
+  locate                         ↦ locate (computable)
+  all-equal-keys                 ↦ spine_eq
+  ∈k-exclusive                   ↦ immediate from memKey_iff (both sides ↔ k ∈ ks)
+  m₁≼m₂⇒m₁[k]≼m₂[k]              ↦ le_of_mem_mem (takes `ks.Nodup`; the Agda Map
+                                   carried key-uniqueness intrinsically)
+  m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂         ↦ trivial with `=` (congruence)
+  _updating_via_ + Map lemmas:
+    updating-via-keys-≡          ↦ (the `property` field of `updating`)
+    updating-via-∈k-forward      ↦ memKey_updating
+    updating-via-k∈ks            ↦ mem_updating
+    updating-via-k∈ks-≡          ↦ eq_of_mem_updating
+    updating-via-k∉ks-forward    ↦ mem_updating_of_not_mem
+    updating-via-k∉ks-backward   ↦ mem_of_mem_updating
+    f'-Monotonic (Map)           ↦ updating_mono
+  GeneralizedUpdate:
+    f'                           ↦ generalizedUpdate
+    f'-Monotonic                 ↦ generalizedUpdate_monotone
+    f'-∈k-forward                ↦ generalizedUpdate_memKey
+    f'-k∈ks                      ↦ generalizedUpdate_mem
+    f'-k∈ks-≡                    ↦ generalizedUpdate_mem_eq
+    f'-k∉ks-forward, -backward   ↦ generalizedUpdate_not_mem_forward, _backward
+  _[_], []-∈                     ↦ valuesAt, mem_valuesAt (takes `ks.Nodup`)
+  m₁≼m₂⇒m₁[ks]≼m₂[ks]            ↦ valuesAt_le
+  Provenance-union               ↦ mem_sup
+  ⊔-combines                     ↦ (omitted: only used inside the Agda
+                                   isomorphism proofs, which simplified away)
+  IterProdIsomorphism.from/to    ↦ toIter / ofIter — no `Unique ks` needed: the
+                                   spine-pinned representation is already
+                                   canonical, so the isomorphism is exact
+  from/to-preserves-≈, -⊔-distr  ↦ toIter_monotone / ofIter_monotone (with `≼`
+                                   being `≤`, the transport interface consumes
+                                   monotonicity directly)
+  from-to-inverseˡ/ʳ             ↦ toIter_ofIter / ofIter_toIter
+  to-build                       ↦ mem_ofIter_build
+  FixedHeight.fixedHeight        ↦ FiniteMap.fixedHeight (still obtained by
+                                   transport along the IterProd isomorphism)
+  ⊥-contains-bottoms             ↦ bot_contains_bots
+-/
+import Spa.Lattice.IterProd
+import Spa.Isomorphism
+
+namespace Spa
+
+/-- Agda: `FiniteMap = Σ Map (λ m → Map.keys m ≡ ks)`. -/
+def FiniteMap (A B : Type*) (ks : List A) : Type _ :=
+  { l : List (A × B) // l.map Prod.fst = ks }
+
+namespace FiniteMap
+
+variable {A B : Type*} {ks : List A}
+
+instance [DecidableEq A] [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
+  fun a b => decidable_of_iff (a.val = b.val) Subtype.ext_iff.symm
+
+/-- Agda: `all-equal-keys`. -/
+theorem spine_eq (fm₁ fm₂ : FiniteMap A B ks) :
+    fm₁.val.map Prod.fst = fm₂.val.map Prod.fst :=
+  fm₁.property.trans fm₂.property.symm
+
+/-! ### The lattice structure (`combine` replaces Map union/intersection) -/
+
+/-- Positional combination of two maps with equal spines. -/
+def combine (f : B → B → B) (l₁ l₂ : List (A × B)) : List (A × B) :=
+  List.zipWith (fun p q => (p.1, f p.2 q.2)) l₁ l₂
+
+theorem combine_spine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)},
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (combine f l₁ l₂).map Prod.fst = l₁.map Prod.fst
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, List.map_cons]
+    exact congrArg _ (combine_spine f h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
+
+theorem combine_comm (f : B → B → B) (hf : ∀ a b, f a b = f b a) :
+    ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
+      combine f l₁ l₂ = combine f l₂ l₁
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons]
+    rw [h.1, hf]
+    exact congrArg _ (combine_comm f hf h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
+
+theorem combine_assoc (f : B → B → B) (hf : ∀ a b c, f (f a b) c = f a (f b c)) :
+    ∀ {l₁ l₂ l₃ : List (A × B)},
+      l₁.map Prod.fst = l₂.map Prod.fst → l₂.map Prod.fst = l₃.map Prod.fst →
+      combine f (combine f l₁ l₂) l₃ = combine f l₁ (combine f l₂ l₃)
+  | [], [], [], _, _ => rfl
+  | p :: l₁, q :: l₂, r :: l₃, h₁₂, h₂₃ => by
+    simp only [List.map_cons, List.cons.injEq] at h₁₂ h₂₃
+    simp only [combine, List.zipWith_cons_cons]
+    rw [hf]
+    exact congrArg _ (combine_assoc f hf h₁₂.2 h₂₃.2)
+  | [], [], _ :: _, _, h => by simp at h
+  | [], _ :: _, _, h, _ => by simp at h
+  | _ :: _, [], _, h, _ => by simp at h
+  | _ :: _, _ :: _, [], _, h => by simp at h
+
+theorem combine_absorb (f g : B → B → B) (hfg : ∀ a b, f a (g a b) = a) :
+    ∀ {l₁ l₂ : List (A × B)}, l₁.map Prod.fst = l₂.map Prod.fst →
+      combine f l₁ (combine g l₁ l₂) = l₁
+  | [], [], _ => rfl
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, hfg]
+    exact congrArg _ (combine_absorb f g hfg h.2)
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
+
+variable [Lattice B]
+
+instance : Max (FiniteMap A B ks) where
+  max fm₁ fm₂ :=
+    ⟨combine (· ⊔ ·) fm₁.val fm₂.val,
+     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
+
+instance : Min (FiniteMap A B ks) where
+  min fm₁ fm₂ :=
+    ⟨combine (· ⊓ ·) fm₁.val fm₂.val,
+     (combine_spine _ (spine_eq fm₁ fm₂)).trans fm₁.property⟩
+
+@[simp] theorem sup_val (fm₁ fm₂ : FiniteMap A B ks) :
+    (fm₁ ⊔ fm₂).val = combine (· ⊔ ·) fm₁.val fm₂.val := rfl
+
+@[simp] theorem inf_val (fm₁ fm₂ : FiniteMap A B ks) :
+    (fm₁ ⊓ fm₂).val = combine (· ⊓ ·) fm₁.val fm₂.val := rfl
+
+/-- Agda: `isLattice`/`lattice` (built like the Agda record from the two
+semilattices plus absorption; `Lattice.mk'` defines `a ≤ b ↔ a ⊔ b = b`). -/
+instance : Lattice (FiniteMap A B ks) :=
+  Lattice.mk'
+    (fun a b => Subtype.ext (combine_comm _ sup_comm (spine_eq a b)))
+    (fun a b c => Subtype.ext (combine_assoc _ sup_assoc (spine_eq a b) (spine_eq b c)))
+    (fun a b => Subtype.ext (combine_comm _ inf_comm (spine_eq a b)))
+    (fun a b c => Subtype.ext (combine_assoc _ inf_assoc (spine_eq a b) (spine_eq b c)))
+    (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => sup_inf_self) (spine_eq a b)))
+    (fun a b => Subtype.ext (combine_absorb _ _ (fun _ _ => inf_sup_self) (spine_eq a b)))
+
+/-! ### Membership -/
+
+instance : Membership (A × B) (FiniteMap A B ks) :=
+  ⟨fun fm p => p ∈ fm.val⟩
+
+omit [Lattice B] in
+theorem mem_def {p : A × B} {fm : FiniteMap A B ks} : p ∈ fm ↔ p ∈ fm.val :=
+  Iff.rfl
+
+/-- Agda: `_∈k_`. -/
+def MemKey (k : A) (fm : FiniteMap A B ks) : Prop :=
+  k ∈ fm.val.map Prod.fst
+
+omit [Lattice B] in
+/-- A key is in the map iff it is in the (fixed) key list
+(Agda: `∈k-exclusive` becomes a special case). -/
+theorem memKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := by
+  rw [MemKey, fm.property]
+
+/-- Agda: `∈k-dec`. -/
+instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] :
+    Decidable (MemKey k fm) :=
+  decidable_of_iff _ memKey_iff.symm
+
+omit [Lattice B] in
+/-- Agda: `forget`. -/
+theorem mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+    (h : (k, v) ∈ fm) : MemKey k fm :=
+  List.mem_map_of_mem _ h
+
+section Locate
+
+variable [DecidableEq A]
+
+private def locateList (k : A) :
+    (l : List (A × B)) → k ∈ l.map Prod.fst → {v : B // (k, v) ∈ l}
+  | [], h => absurd h (by simp)
+  | p :: l', h =>
+    if heq : p.1 = k then
+      ⟨p.2, by rw [← heq]; exact List.mem_cons_self ..⟩
+    else
+      let ⟨v, hv⟩ := locateList k l' (by
+        rcases List.mem_cons.mp h with h' | h'
+        · exact absurd h'.symm heq
+        · exact h')
+      ⟨v, List.mem_cons_of_mem _ hv⟩
+
+/-- Agda: `locate`. -/
+def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
+    {v : B // (k, v) ∈ fm} :=
+  locateList k fm.val h
+
+end Locate
+
+/-! ### The pointwise order -/
+
+theorem combine_eq_right_iff : ∀ {l₁ l₂ : List (A × B)},
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (combine (· ⊔ ·) l₁ l₂ = l₂ ↔
+      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂)
+  | [], [], _ => by simp [combine]
+  | p :: l₁, q :: l₂, h => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp only [combine, List.zipWith_cons_cons, List.cons.injEq,
+               List.forall₂_cons, Prod.ext_iff]
+    rw [show List.zipWith (fun p q : A × B => (p.1, p.2 ⊔ q.2)) l₁ l₂
+          = combine (· ⊔ ·) l₁ l₂ from rfl,
+        combine_eq_right_iff h.2]
+    constructor
+    · rintro ⟨⟨hk, hv⟩, hrest⟩
+      exact ⟨⟨hk, sup_eq_right.mp hv⟩, hrest⟩
+    · rintro ⟨⟨hk, hv⟩, hrest⟩
+      exact ⟨⟨hk, sup_eq_right.mpr hv⟩, hrest⟩
+  | [], _ :: _, h => by simp at h
+  | _ :: _, [], h => by simp at h
+
+/-- The order on finite maps is the pointwise order on values. -/
+theorem le_iff {fm₁ fm₂ : FiniteMap A B ks} :
+    fm₁ ≤ fm₂ ↔
+      List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) fm₁.val fm₂.val := by
+  rw [← sup_eq_right, ← combine_eq_right_iff (spine_eq fm₁ fm₂), Subtype.ext_iff,
+      sup_val]
+
+private theorem forall₂_spine : ∀ {l₁ l₂ : List (A × B)},
+    List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂ →
+    l₁.map Prod.fst = l₂.map Prod.fst
+  | _, _, List.Forall₂.nil => rfl
+  | _, _, List.Forall₂.cons hpq hrest => by
+    simp [List.map_cons, hpq.1, forall₂_spine hrest]
+
+private theorem forall₂_mem_mem {l₁ l₂ : List (A × B)}
+    (hf : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
+    (l₁.map Prod.fst).Nodup →
+    ∀ {k : A} {v₁ v₂ : B}, (k, v₁) ∈ l₁ → (k, v₂) ∈ l₂ → v₁ ≤ v₂ := by
+  induction hf with
+  | nil =>
+    intro _ k v₁ v₂ h₁ _
+    simp at h₁
+  | @cons p q l₁' l₂' hpq hrest ih =>
+    intro hnd k v₁ v₂ h₁ h₂
+    simp only [List.map_cons, List.nodup_cons] at hnd
+    have hspine := forall₂_spine hrest
+    rcases List.mem_cons.mp h₁ with heq₁ | h₁'
+    · rcases List.mem_cons.mp h₂ with heq₂ | h₂'
+      · rw [← heq₁, ← heq₂] at hpq
+        exact hpq.2
+      · exfalso
+        apply hnd.1
+        rw [show p.1 = k from (congrArg Prod.fst heq₁).symm, hspine]
+        exact List.mem_map_of_mem _ h₂'
+    · rcases List.mem_cons.mp h₂ with heq₂ | h₂'
+      · exfalso
+        apply hnd.1
+        rw [hpq.1, show q.1 = k from (congrArg Prod.fst heq₂).symm]
+        exact List.mem_map_of_mem _ h₁'
+      · exact ih hnd.2 h₁' h₂'
+
+/-- Agda: `m₁≼m₂⇒m₁[k]≼m₂[k]`. The `Nodup` hypothesis was carried inside the
+Agda `Map` type. -/
+theorem le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
+    (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
+    (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ :=
+  forall₂_mem_mem (le_iff.mp hle) (fm₁.property.symm ▸ hks) h₁ h₂
+
+/-! ### Provenance of joined values -/
+
+omit [Lattice B] in
+private theorem mem_combine (f : B → B → B) : ∀ {l₁ l₂ : List (A × B)} {k : A} {v : B},
+    l₁.map Prod.fst = l₂.map Prod.fst →
+    (k, v) ∈ combine f l₁ l₂ →
+    ∃ v₁ v₂, v = f v₁ v₂ ∧ (k, v₁) ∈ l₁ ∧ (k, v₂) ∈ l₂
+  | [], [], _, _, _, h => by simp [combine] at h
+  | p :: l₁, q :: l₂, k, v, hsp, h => by
+    simp only [List.map_cons, List.cons.injEq] at hsp
+    simp only [combine, List.zipWith_cons_cons] at h
+    rcases List.mem_cons.mp h with heq | h'
+    · injection heq with hk hv
+      exact ⟨p.2, q.2, hv,
+        by rw [hk]; simp,
+        by rw [hk, hsp.1]; simp⟩
+    · obtain ⟨v₁, v₂, hv, h₁, h₂⟩ := mem_combine f hsp.2 h'
+      exact ⟨v₁, v₂, hv, List.mem_cons_of_mem _ h₁, List.mem_cons_of_mem _ h₂⟩
+
+/-- Agda: `Provenance-union` — a binding of a join comes from bindings of both
+maps. -/
+theorem mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
+    (h : (k, v) ∈ fm₁ ⊔ fm₂) :
+    ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ :=
+  mem_combine _ (spine_eq fm₁ fm₂) h
+
+/-! ### Updating (Agda: `_updating_via_` and `GeneralizedUpdate`) -/
+
+section Updating
+
+variable [DecidableEq A]
+
+/-- Agda: `_updating_via_` — for each key in `ks'`, replace its value by `g k`. -/
+def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
+    FiniteMap A B ks :=
+  ⟨fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p), by
+    rw [List.map_map,
+        show (Prod.fst ∘ fun p : A × B => if p.1 ∈ ks' then (p.1, g p.1) else p)
+          = Prod.fst from funext fun p => by by_cases h : p.1 ∈ ks' <;> simp [h]]
+    exact fm.property⟩
+
+omit [Lattice B] in
+@[simp] theorem updating_val (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) :
+    (updating fm ks' g).val
+      = fm.val.map (fun p => if p.1 ∈ ks' then (p.1, g p.1) else p) := rfl
+
+omit [Lattice B] in
+/-- Agda: `updating-via-∈k-forward` (strengthened to an iff). -/
+theorem memKey_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B} :
+    MemKey k (updating fm ks' g) ↔ MemKey k fm := by
+  rw [memKey_iff, memKey_iff]
+
+omit [Lattice B] in
+/-- Agda: `updating-via-k∈ks-≡`. -/
+theorem eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∈ ks')
+    (h : (k, v) ∈ updating fm ks' g) : v = g k := by
+  obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
+  by_cases hmem : p.1 ∈ ks'
+  · rw [if_pos hmem] at heq
+    injection heq with h1 h2
+    rw [← h2, h1]
+  · rw [if_neg hmem] at heq
+    rw [heq] at hmem
+    exact absurd hk hmem
+
+omit [Lattice B] in
+/-- Agda: `updating-via-k∈ks`. -/
+theorem mem_updating {k : A} {fm : FiniteMap A B ks} {ks' : List A} {g : A → B}
+    (hk : k ∈ ks') (hmem : MemKey k fm) : (k, g k) ∈ updating fm ks' g := by
+  obtain ⟨v, hv⟩ := locate hmem
+  exact List.mem_map.mpr ⟨(k, v), hv, by simp [hk]⟩
+
+omit [Lattice B] in
+/-- Agda: `updating-via-k∉ks-forward`. -/
+theorem mem_updating_of_not_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∉ ks') (h : (k, v) ∈ fm) :
+    (k, v) ∈ updating fm ks' g :=
+  List.mem_map.mpr ⟨(k, v), h, by simp [hk]⟩
+
+omit [Lattice B] in
+/-- Agda: `updating-via-k∉ks-backward`. -/
+theorem mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
+    {ks' : List A} {g : A → B} (hk : k ∉ ks')
+    (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
+  obtain ⟨p, hp, heq⟩ := List.mem_map.mp h
+  by_cases hmem : p.1 ∈ ks'
+  · rw [if_pos hmem] at heq
+    injection heq with h1 _
+    rw [← h1] at hk
+    exact absurd hmem hk
+  · rw [if_neg hmem] at heq
+    exact heq ▸ hp
+
+private theorem updating_mono_list {ks' : List A} {g₁ g₂ : A → B}
+    (hg : ∀ k, g₁ k ≤ g₂ k) {l₁ l₂ : List (A × B)}
+    (hl : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) :
+    List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2)
+      (l₁.map fun p => if p.1 ∈ ks' then (p.1, g₁ p.1) else p)
+      (l₂.map fun p => if p.1 ∈ ks' then (p.1, g₂ p.1) else p) := by
+  induction hl with
+  | nil => exact List.Forall₂.nil
+  | @cons x y l₁' l₂' hpq hrest ih =>
+    simp only [List.map_cons]
+    refine List.Forall₂.cons ?_ ih
+    obtain ⟨hk, hv⟩ := hpq
+    by_cases h : x.1 ∈ ks'
+    · rw [if_pos h, if_pos (hk ▸ h)]
+      exact ⟨hk, hk ▸ hg x.1⟩
+    · rw [if_neg h, if_neg (fun hy => h (hk.symm ▸ hy))]
+      exact ⟨hk, hv⟩
+
+/-- Agda: `f'-Monotonic` at the `Map` level. -/
+theorem updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
+    {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
+    updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
+  rw [le_iff] at hfm ⊢
+  simp only [updating_val]
+  exact updating_mono_list hg hfm
+
+end Updating
+
+section GeneralizedUpdate
+
+/-! Agda: `GeneralizedUpdate` (the "Exercise 4.26" construction). -/
+
+variable [DecidableEq A] {L : Type*} [Lattice L]
+
+/-- Agda: `GeneralizedUpdate.f'`. -/
+def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
+    (ks' : List A) (l : L) : FiniteMap A B ks :=
+  (f l).updating ks' (fun k => g k l)
+
+variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
+
+/-- Agda: `f'-Monotonic`. -/
+theorem generalizedUpdate_monotone (hf : Monotone f)
+    (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
+  fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-∈k-forward`. -/
+theorem generalizedUpdate_memKey {k : A} {l : L}
+    (h : MemKey k (f l)) : MemKey k (generalizedUpdate f g ks' l) := by
+  unfold generalizedUpdate
+  exact memKey_updating.mpr h
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-k∈ks`. -/
+theorem generalizedUpdate_mem {k : A} {l : L} (hk : k ∈ ks')
+    (h : MemKey k (f l)) : (k, g k l) ∈ generalizedUpdate f g ks' l := by
+  unfold generalizedUpdate
+  exact mem_updating hk h
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-k∈ks-≡`. -/
+theorem generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l := by
+  unfold generalizedUpdate at h
+  exact eq_of_mem_updating (g := fun k => g k l) hk h
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-k∉ks-forward`. -/
+theorem generalizedUpdate_not_mem_forward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+    (h : (k, v) ∈ f l) : (k, v) ∈ generalizedUpdate f g ks' l := by
+  unfold generalizedUpdate
+  exact mem_updating_of_not_mem hk h
+
+omit [Lattice B] [Lattice L] in
+/-- Agda: `f'-k∉ks-backward`. -/
+theorem generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+    (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l := by
+  unfold generalizedUpdate at h
+  exact mem_of_mem_updating hk h
+
+end GeneralizedUpdate
+
+/-! ### Reading off values at a list of keys (Agda: `_[_]`) -/
+
+section ValuesAt
+
+variable [DecidableEq A]
+
+private def lookup? (k : A) : List (A × B) → Option B
+  | [] => none
+  | p :: l' => if p.1 = k then some p.2 else lookup? k l'
+
+/-- Agda: `_[_]`. -/
+def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
+  ks'.filterMap (fun k => lookup? k fm.val)
+
+omit [Lattice B] in
+private theorem lookup?_eq_some_of_mem : ∀ {l : List (A × B)},
+    (l.map Prod.fst).Nodup → ∀ {k : A} {v : B}, (k, v) ∈ l →
+    lookup? k l = some v
+  | [], _, _, _, h => by simp at h
+  | p :: l', hnd, k, v, h => by
+    simp only [List.map_cons, List.nodup_cons] at hnd
+    rcases List.mem_cons.mp h with heq | h'
+    · rw [← heq]
+      simp [lookup?]
+    · rw [lookup?, if_neg ?_]
+      · exact lookup?_eq_some_of_mem hnd.2 h'
+      · intro hpk
+        subst hpk
+        have := List.mem_map_of_mem Prod.fst h'
+        exact hnd.1 this
+
+omit [Lattice B] in
+/-- Agda: `[]-∈`. -/
+theorem mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
+    {ks' : List A} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' :=
+  List.mem_filterMap.mpr
+    ⟨k, hk, lookup?_eq_some_of_mem (fm.property.symm ▸ hks) h⟩
+
+private theorem lookup?_forall₂ {l₁ l₂ : List (A × B)}
+    (h : List.Forall₂ (fun p q : A × B => p.1 = q.1 ∧ p.2 ≤ q.2) l₁ l₂) (k : A) :
+    Option.Rel (· ≤ ·) (lookup? k l₁) (lookup? k l₂) := by
+  induction h with
+  | nil => exact Option.Rel.none
+  | @cons p q l₁ l₂ hpq hrest ih =>
+    rw [lookup?, lookup?]
+    by_cases hc : q.1 = k
+    · rw [if_pos hc, if_pos (hpq.1.trans hc)]
+      exact Option.Rel.some hpq.2
+    · rw [if_neg hc, if_neg (fun hp => hc (hpq.1 ▸ hp))]
+      exact ih
+
+/-- Agda: `m₁≼m₂⇒m₁[ks]≼m₂[ks]`. -/
+theorem valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
+    (ks' : List A) :
+    List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
+  induction ks' with
+  | nil => exact List.Forall₂.nil
+  | cons k ks'' ih =>
+    have hrel := lookup?_forall₂ (le_iff.mp hle) k
+    rw [valuesAt, valuesAt, List.filterMap_cons, List.filterMap_cons]
+    revert hrel
+    generalize lookup? k fm₁.val = o₁
+    generalize lookup? k fm₂.val = 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
+
+/-! ### The isomorphism with `IterProd` and the fixed height -/
+
+section Iso
+
+omit [Lattice B] in
+theorem val_ne_nil {k : A} {ks' : List A} (fm : FiniteMap A B (k :: ks')) :
+    fm.val ≠ [] := fun h => by
+  have hp := fm.property
+  rw [h] at hp
+  simp at hp
+
+def headVal {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → B
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨p :: _, _⟩ => p.2
+
+/-- Agda: `pop`. -/
+def pop {k : A} {ks' : List A} : FiniteMap A B (k :: ks') → FiniteMap A B ks'
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨_ :: l, h⟩ =>
+    ⟨l, by simp only [List.map_cons, List.cons.injEq] at h; exact h.2⟩
+
+omit [Lattice B] in
+theorem val_eq_cons {k : A} {ks' : List A} :
+    ∀ fm : FiniteMap A B (k :: ks'), fm.val = (k, fm.headVal) :: fm.pop.val
+  | ⟨[], h⟩ => absurd h (by simp)
+  | ⟨p :: l, h⟩ => by
+    simp only [List.map_cons, List.cons.injEq] at h
+    simp [headVal, pop, ← h.1]
+
+/-- Agda: `IterProdIsomorphism.from`. -/
+def toIter : {ks : List A} → FiniteMap A B ks → IterProd B PUnit ks.length
+  | [], _ => PUnit.unit
+  | _ :: _, fm => (fm.headVal, toIter fm.pop)
+
+/-- Agda: `IterProdIsomorphism.to` (no `Unique ks` needed: the spine-pinned
+representation is canonical). -/
+def ofIter : (ks : List A) → IterProd B PUnit ks.length → FiniteMap A B ks
+  | [], _ => ⟨[], rfl⟩
+  | k :: ks', ip =>
+    ⟨(k, ip.1) :: (ofIter ks' ip.2).val, by
+      simp [(ofIter ks' ip.2).property]⟩
+
+omit [Lattice B] in
+/-- Agda: `from-to-inverseʳ`. -/
+theorem ofIter_toIter : ∀ {ks : List A} (fm : FiniteMap A B ks),
+    ofIter ks (toIter fm) = fm
+  | [], fm => by
+    obtain ⟨val, hprop⟩ := fm
+    cases val with
+    | nil => rfl
+    | cons p l => exact absurd hprop (by simp)
+  | k :: ks', fm => Subtype.ext (by
+      show (k, fm.headVal) :: (ofIter ks' (toIter fm.pop)).val = fm.val
+      rw [ofIter_toIter fm.pop, ← val_eq_cons fm])
+
+omit [Lattice B] in
+/-- Agda: `from-to-inverseˡ`. -/
+theorem toIter_ofIter : ∀ (ks : List A) (ip : IterProd B PUnit ks.length),
+    toIter (ofIter ks ip) = ip
+  | [], _ => rfl
+  | k :: ks', ip => by
+    show (headVal (ofIter (k :: ks') ip), toIter (pop (ofIter (k :: ks') ip))) = ip
+    rw [show pop (ofIter (k :: ks') ip) = ofIter ks' ip.2 from rfl,
+        toIter_ofIter ks' ip.2]
+    rfl
+
+theorem headVal_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
+    (h : fm₁ ≤ fm₂) : fm₁.headVal ≤ fm₂.headVal := by
+  have h' := le_iff.mp h
+  rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
+  exact (List.forall₂_cons.mp h').1.2
+
+theorem pop_le {k : A} {ks' : List A} {fm₁ fm₂ : FiniteMap A B (k :: ks')}
+    (h : fm₁ ≤ fm₂) : fm₁.pop ≤ fm₂.pop := by
+  rw [le_iff]
+  have h' := le_iff.mp h
+  rw [val_eq_cons fm₁, val_eq_cons fm₂] at h'
+  exact (List.forall₂_cons.mp h').2
+
+/-- Agda: `from-preserves-≈` and `from-⊔-distr` (see header note). -/
+theorem toIter_monotone : ∀ {ks : List A},
+    Monotone (toIter : FiniteMap A B ks → IterProd B PUnit ks.length)
+  | [] => fun _ _ _ => le_refl _
+  | _ :: _ => fun _ _ h =>
+    Prod.mk_le_mk.mpr ⟨headVal_le h, toIter_monotone (pop_le h)⟩
+
+/-- Agda: `to-preserves-≈` and `to-⊔-distr` (see header note). -/
+theorem ofIter_monotone : ∀ (ks : List A), Monotone (ofIter (A := A) (B := B) ks)
+  | [] => fun _ _ _ => le_refl _
+  | k :: ks' => fun ip₁ ip₂ h => by
+    rw [le_iff]
+    show List.Forall₂ _ ((k, ip₁.1) :: (ofIter ks' ip₁.2).val)
+                        ((k, ip₂.1) :: (ofIter ks' ip₂.2).val)
+    exact List.Forall₂.cons ⟨rfl, h.1⟩ (le_iff.mp (ofIter_monotone ks' h.2))
+
+/-- Agda: `FixedHeight.fixedHeight` — a finite map into a lattice of height
+`hB` has height `|ks| · hB`, by transport along the `IterProd` isomorphism. -/
+def fixedHeight {hB : ℕ} (fhB : FixedHeight B hB) (ks : List A) :
+    FixedHeight (FiniteMap A B ks) (ks.length * hB) :=
+  ((IterProd.fixedHeight fhB punitFixedHeight ks.length).transport
+      (ofIter ks) toIter (ofIter_monotone ks) toIter_monotone
+      (toIter_ofIter ks) (fun fm => ofIter_toIter fm)).cast (by ring)
+
+/-- Agda: `isFiniteHeightLattice`/`finiteHeightLattice` of `Lattice/FiniteMap.agda`
+(there instance arguments; here an instance). -/
+instance [IB : FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) where
+  height := ks.length * IB.height
+  fixedHeight := fixedHeight IB.fixedHeight ks
+
+omit [Lattice B] in
+/-- Agda: `to-build`. -/
+theorem mem_ofIter_build {b : B} : ∀ {ks : List A} {k : A} {v : B},
+    (k, v) ∈ ofIter ks (IterProd.build b PUnit.unit ks.length) → v = b
+  | [], _, _, h => by simp [ofIter, mem_def] at h
+  | k' :: ks', k, v, h => by
+    rcases List.mem_cons.mp h with heq | h'
+    · exact (Prod.ext_iff.mp heq).2
+    · exact mem_ofIter_build h'
+
+/-- Agda: `⊥-contains-bottoms`. -/
+theorem bot_contains_bots {hB : ℕ} (fhB : FixedHeight B hB) {k : A} {v : B}
+    (h : (k, v) ∈ (fixedHeight fhB ks).bot) : v = fhB.bot := by
+  have hbot : (fixedHeight fhB ks).bot
+      = ofIter ks (IterProd.build fhB.bot PUnit.unit ks.length) := by
+    show ofIter ks (IterProd.fixedHeight fhB punitFixedHeight ks.length).bot = _
+    rw [IterProd.bot_fixedHeight]
+  rw [hbot] at h
+  exact mem_ofIter_build h
+
+end Iso
+
+end FiniteMap
+
+end Spa
--- a/lean/Spa/Lattice/IterProd.lean
+++ b/lean/Spa/Lattice/IterProd.lean
@@ -0,0 +1,76 @@
+/-
+Port of `Lattice/IterProd.agda`: the `k`-fold product `A × (A × ⋯ × B)`.
+
+With propositional equality and typeclasses, the Agda `Everything` record
+(which threaded the lattice operations and the conditional fixed-height proof
+through one recursion, so that the operations built by separate recursions
+would agree) is no longer needed: the `Lattice` instance is one recursive
+definition, and the fixed-height structure is another recursion over it.
+
+Correspondence:
+  IterProd            ↦ Spa.IterProd
+  build               ↦ Spa.IterProd.build
+  isLattice/lattice   ↦ instance Spa.IterProd.instLattice
+  fixedHeight,
+  isFiniteHeightLattice,
+  finiteHeightLattice ↦ Spa.IterProd.fixedHeight (+ FiniteHeightLattice instance)
+  ⊥-built             ↦ Spa.IterProd.bot_fixedHeight
+-/
+import Spa.Lattice.Prod
+import Spa.Lattice.Unit
+import Mathlib.Tactic.Ring
+
+namespace Spa
+
+universe u
+
+/-- Agda: `IterProd k = iterate k (A × ·) B`. (As in the Agda module, `A` and
+`B` are constrained to the same universe to keep the recursion simple.) -/
+def IterProd (A B : Type u) : ℕ → Type u
+  | 0 => B
+  | k + 1 => A × IterProd A B k
+
+namespace IterProd
+
+variable {A B : Type u}
+
+instance instLattice [Lattice A] [Lattice B] :
+    ∀ k, Lattice (IterProd A B k)
+  | 0 => inferInstanceAs (Lattice B)
+  | k + 1 => @Prod.instLattice A (IterProd A B k) _ (instLattice k)
+
+instance instDecidableEq [DecidableEq A] [DecidableEq B] :
+    ∀ k, DecidableEq (IterProd A B k)
+  | 0 => inferInstanceAs (DecidableEq B)
+  | k + 1 => @instDecidableEqProd A (IterProd A B k) _ (instDecidableEq k)
+
+/-- Agda: `build`. -/
+def build (a : A) (b : B) : (k : ℕ) → IterProd A B k
+  | 0 => b
+  | k + 1 => (a, build a b k)
+
+variable [Lattice A] [Lattice B]
+
+/-- Agda: `fixedHeight` (the `isFiniteHeightIfSupported` recursion). -/
+def fixedHeight {hA hB : ℕ} (fhA : FixedHeight A hA) (fhB : FixedHeight B hB) :
+    (k : ℕ) → FixedHeight (IterProd A B k) (k * hA + hB)
+  | 0 => fhB.cast (by ring)
+  | k + 1 => (fhA.prod (fixedHeight fhA fhB k)).cast (by ring)
+
+/-- Agda: `⊥-built` — the bottom of the iterated product is built from the
+component bottoms. -/
+theorem bot_fixedHeight {hA hB : ℕ} (fhA : FixedHeight A hA) (fhB : FixedHeight B hB) :
+    ∀ k, (fixedHeight fhA fhB k).bot = build fhA.bot fhB.bot k
+  | 0 => rfl
+  | k + 1 => by
+    show (fhA.bot, (fixedHeight fhA fhB k).bot) = (fhA.bot, build fhA.bot fhB.bot k)
+    rw [bot_fixedHeight fhA fhB k]
+
+instance [IA : FiniteHeightLattice A] [IB : FiniteHeightLattice B] (k : ℕ) :
+    FiniteHeightLattice (IterProd A B k) where
+  height := k * IA.height + IB.height
+  fixedHeight := fixedHeight IA.fixedHeight IB.fixedHeight k
+
+end IterProd
+
+end Spa
--- a/lean/Spa/Lattice/Prod.lean
+++ b/lean/Spa/Lattice/Prod.lean
@@ -0,0 +1,113 @@
+/-
+Port of `Lattice/Prod.agda`.
+
+The component-wise lattice structure on `α × β` is lifted into mathlib
+(`Prod.instLattice`), as is decidability of equality. What remains custom is
+the fixed-height content:
+
+  unzip                      ↦ LTSeries.exists_unzip
+  a,∙-Monotonic/∙,b-Monotonic ↦ Prod.mk_lt_mk_iff_right/left (strict mono of
+                                the two injections, used to map the chains)
+  fixedHeight (h₁ + h₂)      ↦ FixedHeight.prod
+  isFiniteHeightLattice      ↦ instance FiniteHeightLattice (α × β)
+-/
+import Spa.Lattice
+
+namespace Spa
+
+section Unzip
+
+variable {α β : Type*} [PartialOrder α] [PartialOrder β]
+
+/-- Agda: `unzip` — a chain in the product splits into chains of the
+components whose lengths sum to at least the original length. -/
+theorem LTSeries.exists_unzip (c : LTSeries (α × β)) :
+    ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
+      c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
+      c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
+      c.length ≤ c₁.length + c₂.length := by
+  suffices H : ∀ (n : ℕ) (c : LTSeries (α × β)), c.length = n →
+      ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
+        c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
+        c₂.head = c.head.2 ∧ c₂.last = c.last.2 ∧
+        c.length ≤ c₁.length + c₂.length from H c.length c rfl
+  intro n
+  induction n with
+  | zero =>
+    intro c hn
+    refine ⟨RelSeries.singleton _ c.head.1, RelSeries.singleton _ c.head.2,
+      rfl, ?_, rfl, ?_, by simp [hn]⟩ <;>
+    · have hlast : Fin.last c.length = 0 := by ext; simp [hn]
+      simp [RelSeries.last, RelSeries.head, hlast]
+  | succ n ih =>
+    intro c hn
+    have h0 : c.length ≠ 0 := by omega
+    obtain ⟨c₁, c₂, hh₁, hl₁, hh₂, hl₂, hlen⟩ :=
+      ih (c.tail h0) (by simp [RelSeries.tail_length, hn])
+    rw [RelSeries.last_tail] at hl₁ hl₂
+    rw [RelSeries.head_tail] at hh₁ hh₂
+    rw [RelSeries.tail_length] at hlen
+    have hstep : c.head < c 1 := by
+      have h := c.step ⟨0, by omega⟩
+      have h1 : (⟨0, by omega⟩ : Fin c.length).succ = 1 := by
+        ext; simp [Fin.val_one, Nat.mod_eq_of_lt (by omega : 1 < c.length + 1)]
+      rwa [h1] at h
+    obtain ⟨hle1, hle2⟩ := Prod.le_def.mp hstep.le
+    rcases eq_or_lt_of_le hle1 with heq1 | hlt1 <;>
+      rcases eq_or_lt_of_le hle2 with heq2 | hlt2
+    · exact absurd (Prod.ext heq1 heq2) hstep.ne
+    · refine ⟨c₁, c₂.cons c.head.2 (hh₂ ▸ hlt2),
+        hh₁.trans heq1.symm, hl₁, RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+    · refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂,
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₁,
+        hh₂.trans heq2.symm, hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+    · refine ⟨c₁.cons c.head.1 (hh₁ ▸ hlt1), c₂.cons c.head.2 (hh₂ ▸ hlt2),
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₁,
+        RelSeries.head_cons .., by
+          rw [RelSeries.last_cons]; exact hl₂, by
+          simp only [RelSeries.cons_length]; omega⟩
+
+end Unzip
+
+section FixedHeight
+
+variable {α β : Type*} [Lattice α] [Lattice β]
+
+/-- Agda: `Lattice/Prod.agda`'s `fixedHeight` — the product of lattices of
+heights `h₁` and `h₂` has height `h₁ + h₂`. The longest chain climbs the first
+component (at `⊥₂`), then the second component (at `⊤₁`). -/
+def FixedHeight.prod {h₁ h₂ : ℕ} (fhA : FixedHeight α h₁) (fhB : FixedHeight β h₂) :
+    FixedHeight (α × β) (h₁ + h₂) where
+  bot := (fhA.bot, fhB.bot)
+  top := (fhA.top, fhB.top)
+  longestChain :=
+    RelSeries.smash
+      (fhA.longestChain.map (fun a => (a, fhB.bot))
+        (fun _ _ h => Prod.mk_lt_mk_iff_left.mpr h))
+      (fhB.longestChain.map (fun b => (fhA.top, b))
+        (fun _ _ h => Prod.mk_lt_mk_iff_right.mpr h))
+      (by simp [fhA.last_longestChain, fhB.head_longestChain])
+  head_longestChain := by simp [fhA.head_longestChain]
+  last_longestChain := by simp [fhB.last_longestChain]
+  length_longestChain := by
+    simp [fhA.length_longestChain, fhB.length_longestChain]
+  bounded := fun c => by
+    obtain ⟨c₁, c₂, -, -, -, -, hlen⟩ := LTSeries.exists_unzip c
+    have h₁ := fhA.bounded c₁
+    have h₂ := fhB.bounded c₂
+    omega
+
+/-- Agda: `Lattice/Prod.agda`'s `isFiniteHeightLattice`/`finiteHeightLattice`. -/
+instance [IA : FiniteHeightLattice α] [IB : FiniteHeightLattice β] :
+    FiniteHeightLattice (α × β) where
+  height := IA.height + IB.height
+  fixedHeight := IA.fixedHeight.prod IB.fixedHeight
+
+end FixedHeight
+
+end Spa
--- a/lean/Spa/Lattice/Unit.lean
+++ b/lean/Spa/Lattice/Unit.lean
@@ -0,0 +1,35 @@
+/-
+Port of `Lattice/Unit.agda`.
+
+The lattice structure itself (`_⊔_`, `_⊓_`, all semilattice/lattice laws) is
+lifted into mathlib: `PUnit.instLinearOrder` provides `Lattice PUnit`.
+What remains is the fixed-height structure: the unit lattice has height 0.
+-/
+import Spa.Lattice
+
+namespace Spa
+
+/-- Chains in a subsingleton order are bounded by any `n` (Agda: the `bounded`
+field of `Lattice/Unit.agda`'s `fixedHeight`, generalized). -/
+theorem 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 _ _)
+
+/-- Agda: `Lattice/Unit.agda`'s `fixedHeight`. -/
+def punitFixedHeight : FixedHeight PUnit 0 where
+  bot := PUnit.unit
+  top := PUnit.unit
+  longestChain := RelSeries.singleton _ PUnit.unit
+  head_longestChain := rfl
+  last_longestChain := rfl
+  length_longestChain := rfl
+  bounded := boundedChains_of_subsingleton PUnit 0
+
+/-- Agda: `Lattice/Unit.agda`'s `isFiniteHeightLattice`. -/
+instance : FiniteHeightLattice PUnit where
+  height := 0
+  fixedHeight := punitFixedHeight
+
+end Spa
--- a/lean/Spa/Showable.lean
+++ b/lean/Spa/Showable.lean
@@ -0,0 +1,47 @@
+/-
+Port of `Showable.agda` (plus the `Showable` instances that lived on
+`Lattice/Map.agda` and `Lattice/AboveBelow.agda`).
+
+Lean has `ToString`, but its `String` instance does not quote (the Agda one
+does), so to reproduce the Agda output exactly we port the class as-is.
+-/
+import Spa.Lattice.FiniteMap
+import Spa.Lattice.AboveBelow
+
+namespace Spa
+
+/-- Agda: `Showable` (`show` is a Lean keyword, hence `show'`). -/
+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 _ => "()"⟩
+
+/-- Agda: the `Showable` instance of `Lattice/AboveBelow.agda`. -/
+instance {α : Type*} [Showable α] : Showable (AboveBelow α) :=
+  ⟨fun
+    | .bot => "⊥"
+    | .top => "⊤"
+    | .mk x => show' x⟩
+
+/-- Agda: the `Showable` instance of `Lattice/Map.agda` (inherited by
+`FiniteMap`). -/
+instance {α β : Type*} {ks : List α} [Showable α] [Showable β] :
+    Showable (FiniteMap α β ks) :=
+  ⟨fun fm =>
+    "{" ++ fm.val.foldr (fun p rest => show' p.1 ++ " ↦ " ++ show' p.2 ++ ", " ++ rest) ""
+        ++ "}"⟩
+
+end Spa
--- a/lean/lake-manifest.json
+++ b/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"}
--- a/lean/lakefile.toml
+++ b/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"
--- a/lean/lean-toolchain
+++ b/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.17.0
Author	SHA1	Message	Date
Danila Fedorin	b16f14fdfd	Lean migration: typeclass-based parameter passing, as in the Agda original The port had flattened Agda's instance arguments ({{flA}}, {{evaluator}}, {{latticeInterpretation}}, {{validEvaluator}}) into explicitly threaded values (fhL, E, I, hE). Restore them as typeclasses: - Spa.FiniteHeightLattice: now actually used — Fixedpoint takes the instance instead of a FixedHeight value; FiniteMap gets the missing instance (height = ks.length * height B), so varsFixedHeight / statesFixedHeight / signFixedHeight / constFixedHeight plumbing disappears (instance bottoms are defeq to the old ones) - Spa.Analysis.Forward.Evaluation: StmtEvaluator/ExprEvaluator become classes; the Valid* Props become Prop-classes, as in Agda - Spa.Analysis.Forward.Adapters: the expr→stmt adapter and its validity are instances (Agda: the ExprToStmtAdapter instances) - LatticeInterpretation is a class; sign/const interpretations, evaluators and validity proofs are instances; use sites read like the Agda module applications: result SignLattice prog Proof simplifications (same theorems, proofs factored): - Spa.Lattice.AboveBelow.monotone₂_of_strict: any ⊥-strict/⊤-dominated operation on a flat lattice is monotone — replaces the four near- identical case bashes per analysis (postulates in Agda) - Spa.Lattice.AboveBelow.interp_sup_of/interp_inf_of: the shared flat- lattice interpretation case analysis, making interpSign_sup/inf and interpConst_sup/inf one-liners lake build green with zero warnings; lake exe spa output verified byte-identical (diff) to the previous, Agda-verified output. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-06-09 23:32:38 -07:00
Danila Fedorin	b26d6b5acd	Lean migration: final notes — Lean output verified identical to Agda Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-06-09 20:54:59 -07:00
Danila Fedorin	a82d54666a	Lean migration: Phase 7 (Sign + Constant analyses, executable) - Spa.Showable: port of Showable.agda (quoted strings, map format) for output parity - Spa.Analysis.Utils: eval_combine₂ - Spa.Lattice.AboveBelow.le_cases: order of the flat lattice by cases - Spa.Analysis.Sign / Spa.Analysis.Constant: the four monotonicity POSTULATES from the Agda files are now proved theorems (via le_cases); interpretations, evaluator validity, analyze_correct per analysis - Main + lake exe spa: runs both analyses on the Agda test program; constant analysis folds unknown=0, sign analysis gives unknown=⊤ Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-06-09 20:52:08 -07:00
Danila Fedorin	739fbb503c	Lean migration: Phase 6 (forward analysis framework) - Spa.Analysis.Forward.Lattices: VariableValues/StateVariables (FiniteMap instantiations), fixed heights, variablesAt, joinForKey/joinAll, interpV and its sup/foldr lemmas - Spa.Analysis.Forward.Evaluation: StmtEvaluator/ExprEvaluator + validity (the Agda Valid* instance records become plain Props) - Spa.Analysis.Forward.Adapters: expr-to-stmt evaluator adapter + validity - Spa.Analysis.Forward: updateAll, analyze, result (least fixpoint via the gas-based Fixedpoint), walkTrace, analyze_correct — the framework's main soundness theorem Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-06-09 20:14:53 -07:00
Danila Fedorin	2cfd0a2fb7	Lean migration: Phase 5 (language, CFGs, traces, Program) - Spa.Language.Base: Expr/BasicStmt/Stmt + HasVar relations; StringSet lifts to Finset String - Spa.Language.Semantics: Value/Env/Env.Mem, big-step relations, LatticeInterpretation (respects-≈ field drops out with =) - Spa.Language.Graphs: Graph with nodes : Fin size → List BasicStmt (Vec lookup lemmas lift to Fin.append_left/right), comp/link/loop/ skipto/singleton/wrap/buildCfg, predecessors via List.finRange - Spa.Language.Traces: Trace + EndToEndTrace (Prop-valued) - Spa.Language.Properties: trace embeddings, loop lemmas, buildCfg_sufficient; the 80-line Fin-disjointness block reduces to castAdd_ne_natAdd + mathlib list lemmas - Spa.Language: Program (vars via Finset.sort — toList is noncomputable) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-06-09 19:30:42 -07:00
Danila Fedorin	781d7947e0	Lean migration: Phase 4 (IterProd + FiniteMap lattices) - Spa.Lattice.IterProd: k-fold product, recursive Lattice instance, fixed height khA + hB, bot = build of bottoms - Spa.Lattice.FiniteMap: spine-pinned assoc lists ({l // l.map fst = ks}); with = the 1100-line Map.agda collapses into positional 'combine'. Same lemma inventory (membership, locate, updating, GeneralizedUpdate, valuesAt, Provenance-union, le_of_mem_mem) — Nodup is now an explicit hypothesis where the Agda Map carried it intrinsically. Fixed height \|ks\|hB still via transport along the IterProd isomorphism, which no longer needs Unique ks (representation is canonical). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-06-09 19:12:39 -07:00
Danila Fedorin	4c337afa9c	Lean migration: Phase 3 (Unit, Prod, AboveBelow lattices) - Spa.Lattice.Unit: PUnit fixed height 0 (lattice lifted from mathlib) - Spa.Lattice.Prod: chain unzip + FixedHeight (h1+h2) on products (componentwise lattice lifted from mathlib's Prod.instLattice) - Spa.Lattice.AboveBelow: flat lattice via Lattice.mk' (mirrors the Agda semilattices+absorption construction), boundedness via rank into Nat, Plain x ↦ plainFixedHeight x, height 2 Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-06-09 18:48:02 -07:00
Danila Fedorin	ae030386b4	Lean migration: Phases 0-2 (core lattice/chain, fixpoint, transport) - lean/ lake project pinned to Lean v4.17.0 + mathlib v4.17.0 - Spa.Lattice: fold monotonicity, FixedHeight/BoundedChains (LTSeries-based), FiniteHeightLattice, chain-bottom-is-least; the rest of Lattice.agda, Chain.agda and Equivalence.agda lift into mathlib (see LEAN_MIGRATION.md) - Spa.Fixedpoint: gas-based least-fixpoint computation (doStep/fix/aFix) - Spa.Isomorphism: FixedHeight transport along monotone inverse pairs Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>	2026-06-09 18:36:43 -07:00
Danila Fedorin	1c2bcc2d92	Require bottom element to actually be bottom; finish proof Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-16 20:15:10 -08:00
Danila Fedorin	da2b6dd5c6	Make code less brittle for when \McL changes Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-16 19:43:10 -08:00
Danila Fedorin	c64504b819	Fix broken code by moving fins to utils Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-16 19:33:56 -08:00
Danila Fedorin	4a9e7492f4	Prove the other direction for associativity Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-16 19:31:39 -08:00
Danila Fedorin	ba57e2558d	Add more cases for associativity lemma	2026-02-16 17:43:07 -08:00
Danila Fedorin	1c37141234	Add more properties about lattices Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-16 17:43:07 -08:00
Danila Fedorin	9072da4ab6	Add some cases for associativity lemma	2026-02-16 17:42:59 -08:00
Danila Fedorin	3f923c2d7d	Clean up some definitions Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-16 12:57:59 -08:00
Danila Fedorin	01555ee203	Make progress on properties of the dependent product Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-16 01:08:34 -08:00
Danila Fedorin	a083f2f4ae	Construct proofs of 'basic' lattices Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-14 14:40:15 -08:00
Danila Fedorin	27f65c10f7	Prove absroption laws Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-14 14:22:27 -08:00
Danila Fedorin	c6e525ad7c	Add associativity proofs Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-14 13:47:39 -08:00
Danila Fedorin	ccc3c7d5c7	Add meet/join operation and some properties Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-12 20:16:02 -08:00
Danila Fedorin	05c55498ce	Extend proofs to meet as well as join Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-12 17:12:01 -08:00
Danila Fedorin	6b462f1a83	Prove that having a total join function is decidable Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-05 16:54:22 -08:00
Danila Fedorin	7382c632bc	Add some proofs about predecessors Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2026-02-05 16:16:12 -08:00
Danila Fedorin	aa32706120	Fix typo Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-23 14:07:45 -08:00
Danila Fedorin	4b0541caf5	Use "top" instead of T Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-23 14:06:28 -08:00
Danila Fedorin	299938d97e	Add decidability proofs for properties Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-07 22:25:47 -08:00
Danila Fedorin	927030c337	Prove that having a top and bottom element is decidable Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-07 19:28:56 -08:00
Danila Fedorin	ef3c351bb0	Add some utility proofs about uniqueness etc. Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-12-07 19:28:27 -08:00
Danila Fedorin	84c4ea6936	Prove final postulate about cycles in graphs Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-29 22:46:49 -08:00
Danila Fedorin	a277c8f969	Prove walk splitting Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-29 21:34:39 -08:00
Danila Fedorin	d1700f23fa	Add some helpers Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-29 13:24:27 -08:00
Danila Fedorin	eb2d64f3b5	Properly state all-paths property using simple walks Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 21:31:54 -08:00
Danila Fedorin	14214ab5e7	Reorder definitions to be in the order the graph is built up Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 17:09:57 -08:00
Danila Fedorin	baece236d3	Re-define 'interior' Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 17:09:14 -08:00
Danila Fedorin	6f642d85e0	Put self-paths into the adjacency graph Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 17:08:56 -08:00
Danila Fedorin	25fa0140f0	Switch to a path definition that allows trivial self-loops Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 16:30:10 -08:00
Danila Fedorin	27621992ad	Rename a helper Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 16:25:46 -08:00
Danila Fedorin	e409cceae5	Start on an initial implementation of DAG-based builder Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 16:24:48 -08:00
Danila Fedorin	8cb082e3c5	Delete original builder (lol) Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 16:24:29 -08:00
Danila Fedorin	c199e9616f	Factor some code out into Utils Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2025-11-28 16:22:17 -08:00