Switch Reaching analysis to use Finset for more efficiency

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

lean/Spa/Analysis/Reaching.lean

@@ -1,6 +1,5 @@
 import Spa.Analysis.Forward
-import Spa.Lattice.Bool
+import Spa.Lattice.Finset
-import Spa.Lattice.Tuple
 import Spa.Language.Tagged.Graphs
 import Spa.Showable
 
@@ -8,15 +7,13 @@ namespace Spa
 
 open Forward
 
-instance : Showable Bool := ⟨fun b => if b then "true" else "false"⟩
+instance {n : ℕ} : Showable (Finset (Fin n)) :=
-
+  ⟨fun s =>
-instance {n : ℕ} {β : Type*} [Showable β] : Showable (Fin n → β) :=
-  ⟨fun f =>
     "{" ++ (List.finRange n).foldr
-        (fun i rest => show' i ++ " ↦ " ++ show' (f i) ++ ", " ++ rest) ""
+        (fun i rest => if i ∈ s then show' i ++ ", " ++ rest else rest) ""
         ++ "}"⟩
 
-abbrev DefSet (prog : Program) : Type := prog.NodeId → Bool
+abbrev DefSet (prog : Program) : Type := Finset prog.NodeId
 
 namespace ReachingAnalysis
 
@@ -24,7 +21,7 @@ variable (prog : Program)
 
 def genSet (s : prog.State) {bs : BasicStmt} (h : prog.code s = some bs) :
     DefSet prog :=
-  Function.update (⊥ : DefSet prog) (prog.nodeIdOfNonempty s h) true
+  {prog.nodeIdOfNonempty s h}
 
 def eval (s : prog.State) :
     (bs : BasicStmt) → prog.code s = some bs →
@@ -65,15 +62,15 @@ instance stateInterp : StateInterp (DefSet prog) prog where
   St := fun _ => Run prog
   init := Run.nil
   interp vs _ run := ∀ (x : String) (assigners : DefSet prog), (x, assigners) ∈ vs →
-    ∀ (n : prog.NodeId), LastAssign prog x run n → assigners n = true
+    ∀ (n : prog.NodeId), LastAssign prog x run n → n ∈ assigners
   interp_sup := by
     intro vs₁ vs₂ ρ run h x assigners hmem n hla
     obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_sup hmem
-    aesop
+    aesop (add simp Finset.mem_union)
   interp_inf := by
     intro vs₁ vs₂ ρ run h x assigners hmem n hla
     obtain ⟨a₁, a₂, rfl, h₁, h₂⟩ := FiniteMap.mem_inf hmem
-    aesop
+    aesop (add simp Finset.mem_inter)
 
 instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
   step := by intro s _ _ bs hcode _ rest; exact Run.cons s bs hcode rest
@@ -88,7 +85,7 @@ instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
       by_cases hx : k = x
       · subst hx
         have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem2
-        aesop (add simp genSet)
+        aesop (add simp [genSet, Finset.mem_singleton])
       · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
           (fun hc => hx (List.mem_singleton.mp hc)) hmem2
         aesop

lean/Spa/Lattice/Finset.lean

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

lean/Spa/Transformation/Licm.lean

@@ -65,10 +65,10 @@ def lookupDef (prog : Program) (vs : VariableValues (DefSet prog) prog)
     (k : String) : DefSet prog :=
   if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else ⊥
 
-/-- The AST node ids marked as definition sites in a `DefSet` (those mapped to
+/-- The AST node ids marked as definition sites in a `DefSet`. With the
-`true`). With the AST-id-keyed lattice these are recovered directly. -/
+`Finset`-of-AST-ids lattice these are just the elements of the set. -/
 def defSites (prog : Program) (d : DefSet prog) : List prog.NodeId :=
-  (List.finRange prog.size).filter (fun i => d i)
+  (List.finRange prog.size).filter (fun i => decide (i ∈ d))
 
 /-- Is the candidate assignment loop-invariant: do all reaching definitions of
 its RHS variables lie outside the loop body? Reaching sets are now keyed by AST