Add computational reaching-definitions analysis

Introduce a finite-height lattice instance for Bool, then build the
reaching-definitions analysis on top of the forward framework:

* Spa/Lattice/Bool.lean: FiniteHeightLattice Bool (the two-element
  lattice false ≤ true), making FiniteMap A Bool ks a finite-height
  "power set" lattice for free.
* Spa/Analysis/Reaching.lean: DefSet prog = FiniteMap prog.State Bool
  prog.states as the per-variable lattice of definition sites, with a
  StmtEvaluator whose transfer function performs a strong update
  (assignment to k at node s sets k's def-set to {s}).

The analysis computes a least fixed point and produces correct
reaching-definitions sets. Soundness (relating def-sets to actual
execution provenance) is deferred; not yet exposed in Spa.lean.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

lean/Spa.lean

@@ -6,6 +6,7 @@ import Spa.Lattice.Prod
 import Spa.Lattice.AboveBelow
 import Spa.Lattice.IterProd
 import Spa.Lattice.FiniteMap
+import Spa.Lattice.Bool
 import Spa.Language.Base
 import Spa.Language.Notation
 import Spa.Language.Semantics

lean/Spa/Analysis/Reaching.lean

@@ -0,0 +1,41 @@
+import Spa.Analysis.Forward
+import Spa.Lattice.Bool
+import Spa.Showable
+
+namespace Spa
+
+open Forward
+
+instance : Showable Bool := ⟨fun b => if b then "true" else "false"⟩
+
+abbrev DefSet (prog : Program) : Type := FiniteMap prog.State Bool prog.states
+
+namespace ReachingAnalysis
+
+variable (prog : Program)
+
+def genSet (s : prog.State) : DefSet prog :=
+  FiniteMap.updating (⊥ : DefSet prog) [s] (fun _ => true)
+
+def eval (s : prog.State) :
+    BasicStmt → VariableValues (DefSet prog) prog → VariableValues (DefSet prog) prog
+  | .assign k _, vs =>
+    FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs
+  | .noop, vs => vs
+
+theorem eval_mono (s : prog.State) (bs : BasicStmt) :
+    Monotone (eval prog s bs) := by
+  cases bs with
+  | assign k e =>
+    exact FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
+  | noop => exact monotone_id
+
+instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
+  ⟨eval prog, eval_mono prog⟩
+
+def output : String :=
+  show' (result (DefSet prog) prog)
+
+end ReachingAnalysis
+
+end Spa

lean/Spa/Lattice/Bool.lean

@@ -0,0 +1,42 @@
+import Spa.Lattice
+import Mathlib.Order.BooleanAlgebra
+
+namespace Spa
+
+/-! ### `Bool` as a finite-height lattice
+
+`Bool` is the two-element lattice `false ≤ true` (with `⊥ = false`, `⊤ = true`).
+It is the building block of the "power set" lattice `FiniteMap A Bool ks`, used by
+the reaching-definitions analysis to represent sets of definition sites. -/
+
+namespace Bool
+
+/-- Rank of a boolean: `false ↦ 0`, `true ↦ 1`. Used to bound chains, mirroring
+`AboveBelow.rank`. -/
+def rank : Bool → ℕ
+  | false => 0
+  | true => 1
+
+theorem rank_strictMono : StrictMono rank := by
+  intro a b hab
+  cases a <;> cases b <;> revert hab <;> decide
+
+theorem boundedChains : BoundedChains Bool 1 := fun c => by
+  have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
+  rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h
+  have h2 : rank c.last ≤ 1 := by cases c.last <;> simp [rank]
+  omega
+
+instance : FiniteHeightLattice Bool where
+  height := 1
+  longestChain :=
+    { series := (RelSeries.singleton _ (⊥ : Bool)).snoc (⊤ : Bool)
+        (by rw [RelSeries.last_singleton]; exact bot_lt_top)
+      head_series := by simp
+      last_series := by simp
+      length_series := by simp [RelSeries.snoc, RelSeries.append] }
+  chains_bounded := boundedChains
+
+end Bool
+
+end Spa