Remove 'prog.code s = some bs' argument to eval

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

lean/Main.lean

@@ -1,5 +1,6 @@
 import Spa.Analysis.Sign
 import Spa.Analysis.Constant
+import Spa.Analysis.Reaching
 import Spa.Language.Notation
 
 namespace Spa
@@ -26,10 +27,11 @@ def testCodeCond₂ : Stmt := [obj_stmt|
   if var { x := 1 } else { noop }
 ]
 
-def testProgram : Program := ⟨testCode⟩
+def testProgram : Program := { rootStmt := testCode }
 
 end Spa
 
 def main : IO Unit :=
   IO.println (Spa.ConstAnalysis.output Spa.testProgram ++ "\n" ++
-              Spa.SignAnalysis.output Spa.testProgram)
+              Spa.SignAnalysis.output Spa.testProgram ++ "\n" ++
+              Spa.ReachingAnalysis.output Spa.testProgram)

lean/Spa/Analysis/Constant.lean

@@ -137,6 +137,13 @@ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     ⟦ variablesAt prog.finalState (result ConstLattice prog) ⟧ ρ () :=
   Forward.analyze_correct ConstLattice prog hrun
 
+theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
+    {s : prog.State} {ρin ρout : Env} {stin stout : PUnit}
+    (hr : Reaches (L := ConstLattice) (prog.trace hrun) PUnit.unit s ρin ρout stin stout) :
+    ⟦ joinForKey s (result ConstLattice prog) ⟧ ρin stin
+      ∧ ⟦ variablesAt s (result ConstLattice prog) ⟧ ρout stout :=
+  Forward.analyze_correct_at ConstLattice prog hrun hr
+
 end ConstAnalysis
 
 end Spa

lean/Spa/Analysis/Forward.lean

@@ -9,22 +9,12 @@ namespace Forward
 
 variable {L : Type} [FiniteHeightLattice L] {prog : Program} [E : StmtEvaluator L prog]
 
-def evalStmtOrNone (s : prog.State) (o : Option BasicStmt) (hco : prog.code s = o)
-    (vs : VariableValues L prog) : VariableValues L prog :=
-  o.elimEq vs (fun bs h => E.eval s bs (hco.trans h))
-
-lemma evalStmtOrNone_mono (s : prog.State) (o : Option BasicStmt)
-    (hco : prog.code s = o) : Monotone (evalStmtOrNone (L := L) s o hco) :=
-  elimEq_self_mono o (fun bs h vs => E.eval s bs (hco.trans h) vs)
-    (fun bs h => E.eval_mono s bs (hco.trans h))
-
 def updateVariablesForState (s : prog.State) (sv : StateVariables L prog) :
-    VariableValues L prog :=
-  evalStmtOrNone s (prog.code s) rfl (variablesAt s sv)
+    VariableValues L prog := E.eval s (variablesAt s sv)
 
 lemma updateVariablesForState_mono (s : prog.State) :
     Monotone (updateVariablesForState (L := L) s) := fun _ _ hle =>
-  evalStmtOrNone_mono s (prog.code s) rfl (variablesAt_le hle s)
+  E.eval_mono s (variablesAt_le hle s)
 
 def updateAll (sv : StateVariables L prog) : StateVariables L prog :=
   FiniteMap.generalizedUpdate id updateVariablesForState
@@ -64,33 +54,26 @@ lemma joinForKey_initialState :
   rfl
 
 class ValidStateEvaluator (L : Type) [FiniteHeightLattice L] (prog : Program)
-    [E : StmtEvaluator L prog] [S : StateInterp L prog] where
-  step : (s : prog.State) → {ρ₁ ρ₂ : Env} → {bs : BasicStmt} →
-    prog.code s = some bs → EvalBasicStmt ρ₁ bs ρ₂ → S.St ρ₁ → S.St ρ₂
-  valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env} {bs : BasicStmt}
+    [E : StmtEvaluator L prog] [S : StateInterpretation L prog] where
+  step : (s : prog.State) → {ρ₁ ρ₂ : Env} → EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → S.St ρ₁ → S.St ρ₂
+  valid : ∀ (s : prog.State) {ρ₁ ρ₂ : Env}
     {vs : VariableValues L prog} {st : S.St ρ₁},
-    (hcode : prog.code s = some bs) → (hbs : EvalBasicStmt ρ₁ bs ρ₂) → ⟦ vs ⟧ ρ₁ st →
-    ⟦ E.eval s bs hcode vs ⟧ ρ₂ (step s hcode hbs st)
+    (hbs : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) → ⟦ vs ⟧ ρ₁ st →
+    ⟦ E.eval s vs ⟧ ρ₂ (step s hbs st)
   botV_init : ⟦ botV L prog ⟧ [] S.init
 
 instance [LatticeInterpretation L] [ValidStmtEvaluator L prog] :
     ValidStateEvaluator L prog where
-  step := by intro _ _ _ _ _ _ _; exact PUnit.unit
-  valid := by intro _ _ _ _ _ _ hcode hbs hvs; exact ValidStmtEvaluator.valid hcode hbs hvs
+  step := by intro _ _ _ _ _; exact PUnit.unit
+  valid := by intro _ _ _ _ _ hbs hvs; exact ValidStmtEvaluator.valid hbs hvs
   botV_init := by intro k l _ v hmem; cases hmem
 
 section
-variable [S : StateInterp L prog] [V : ValidStateEvaluator L prog]
-
-noncomputable def stepStmtOrNone (s : prog.State) {ρ₁ ρ₂ : Env} :
-    (o : Option BasicStmt) → prog.code s = o → EvalBasicStmtOpt ρ₁ o ρ₂ →
-    S.St ρ₁ → S.St ρ₂
-  | none, _, .none, st => st
-  | some _, hco, .some hbs, st => V.step s hco hbs st
+variable [S : StateInterpretation L prog] [V : ValidStateEvaluator L prog]
 
 noncomputable def stepNode (s : prog.State) {ρ₁ ρ₂ : Env}
     (h : EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂) (st : S.St ρ₁) : S.St ρ₂ :=
-  stepStmtOrNone s (prog.code s) rfl h st
+  V.step s h st
 
 noncomputable def stepTraceState :
     {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
@@ -99,14 +82,27 @@ noncomputable def stepTraceState :
   | s₁, _, _, _, .edge hnode _ subtr, st =>
       stepTraceState subtr (stepNode s₁ hnode st)
 
-omit [DecidableEq L] in
-lemma evalStmtOrNone_valid {s : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
-    {vs : VariableValues L prog} (o : Option BasicStmt) (hco : prog.code s = o)
-    (he : EvalBasicStmtOpt ρ₁ o ρ₂) (hvs : ⟦ vs ⟧ ρ₁ st) :
-    ⟦ evalStmtOrNone s o hco vs ⟧ ρ₂ (stepStmtOrNone s o hco he st) := by
-  cases he with
-  | none => exact hvs
-  | some hbs => exact V.valid s hco hbs hvs
+/-- `Reaches tr st₁ s ρin ρout stin stout` witnesses that, when the trace `tr`
+    (starting at state `st₁`) is executed, node `s` is visited at some point: `ρin`
+    and `ρout` are the concrete environments just before and after `s`'s basic block
+    runs, and `stin`/`stout` are the corresponding abstract execution states. A node
+    inside a loop is reached once per iteration, each with its own environments. -/
+inductive Reaches : {s₁ s₂ : prog.State} → {ρ₁ ρ₂ : Env} →
+    Trace prog.cfg s₁ s₂ ρ₁ ρ₂ → S.St ρ₁ →
+    (s : prog.State) → (ρin ρout : Env) → S.St ρin → S.St ρout → Prop
+  | single_here {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂) :
+      Reaches (.single hnode) st₁ s₁ ρ₁ ρ₂ st₁ (stepNode s₁ hnode st₁)
+  | edge_here {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} {st₁ : S.St ρ₁}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
+      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃) :
+      Reaches (.edge hnode hedge rest) st₁ s₁ ρ₁ ρ₂ st₁ (stepNode s₁ hnode st₁)
+  | edge_there {s₁ s₂ s₃ : prog.State} {ρ₁ ρ₂ ρ₃ : Env} {st₁ : S.St ρ₁}
+      (hnode : EvalBasicStmtOpt ρ₁ (prog.code s₁) ρ₂)
+      (hedge : (s₁, s₂) ∈ prog.cfg.edges) (rest : Trace prog.cfg s₂ s₃ ρ₂ ρ₃)
+      {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout} :
+      Reaches rest (stepNode s₁ hnode st₁) s ρin ρout stin stout →
+      Reaches (.edge hnode hedge rest) st₁ s ρin ρout stin stout
 
 omit [DecidableEq L] in
 lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog}
@@ -115,7 +111,7 @@ lemma updateAll_matches {s : prog.State} {sv : StateVariables L prog}
     (hvs : ⟦ variablesAt s sv ⟧ ρ₁ st) :
     ⟦ variablesAt s (updateAll sv) ⟧ ρ₂ (stepNode s hnode st) := by
   rw [variablesAt_updateAll]
-  exact evalStmtOrNone_valid (prog.code s) rfl hnode hvs
+  exact V.valid s hnode hvs
 
 lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
     (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st)
@@ -126,20 +122,46 @@ lemma stepTrace {s₁ : prog.State} {ρ₁ ρ₂ : Env} {st : S.St ρ₁}
   rw [variablesAt_joinAll]
   exact hjoin
 
+/-- Soundness at *every* visited node: if the analysis result over-approximates the
+    incoming environment at the start of the trace, then at each node reached along the
+    way it over-approximates both the environment entering that node (via `joinForKey`)
+    and the environment leaving it (via `variablesAt`). The intermediate `variablesAt`
+    evidence used to be computed and discarded inside `walkTrace`; here it is returned. -/
+lemma walkTrace_reaches {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
+    {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout}
+    {tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂}
+    (hr : Reaches tr st₁ s ρin ρout stin stout)
+    (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁) :
+    ⟦ joinForKey s (result L prog) ⟧ ρin stin
+      ∧ ⟦ variablesAt s (result L prog) ⟧ ρout stout := by
+  induction hr with
+  | single_here hnode => exact ⟨hjoin, stepTrace hjoin hnode⟩
+  | edge_here hnode hedge rest => exact ⟨hjoin, stepTrace hjoin hnode⟩
+  | edge_there hnode hedge rest hr' ih =>
+    have hstep := stepTrace hjoin hnode
+    have hmem := FiniteMap.mem_valuesAt prog.states_nodup
+      (prog.mem_incoming_of_edge hedge) (variablesAt_mem _ (result L prog))
+    exact ih (interp_foldr hstep hmem)
+
+omit [DecidableEq L] in
+/-- The final node of a trace is always reached, with the environment/state the trace
+    ends in. Used to recover the final-state soundness theorem from `walkTrace_reaches`. -/
+lemma reaches_final {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} (st₁ : S.St ρ₁)
+    (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
+    ∃ ρin, ∃ stin : S.St ρin,
+      Reaches tr st₁ s₂ ρin ρ₂ stin (stepTraceState tr st₁) := by
+  induction tr with
+  | single hnode => exact ⟨_, _, .single_here hnode⟩
+  | edge hnode hedge rest ih =>
+    obtain ⟨ρin, stin, hr⟩ := ih (stepNode _ hnode st₁)
+    exact ⟨ρin, stin, .edge_there hnode hedge rest hr⟩
+
 lemma walkTrace {s₁ s₂ : prog.State} {ρ₁ ρ₂ : Env} {st₁ : S.St ρ₁}
     (hjoin : ⟦ joinForKey s₁ (result L prog) ⟧ ρ₁ st₁)
     (tr : Trace prog.cfg s₁ s₂ ρ₁ ρ₂) :
     ⟦ variablesAt s₂ (result L prog) ⟧ ρ₂ (stepTraceState tr st₁) := by
-  induction tr with
-  | single hnode => exact stepTrace hjoin hnode
-  | @edge _ ρ' _ i₁ i₂ _ hnode hedge _ ih =>
-    have hstep : ⟦ variablesAt i₁ (result L prog) ⟧ ρ' (stepNode i₁ hnode st₁) :=
-      stepTrace hjoin hnode
-    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 (interp_foldr hstep hmem)
+  obtain ⟨_, _, hr⟩ := reaches_final st₁ tr
+  exact (walkTrace_reaches hr hjoin).2
 
 variable (L prog) in
 theorem analyze_correct_state {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
@@ -149,6 +171,20 @@ theorem analyze_correct_state {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
   rw [joinForKey_initialState]
   exact ValidStateEvaluator.botV_init
 
+variable (L prog) in
+/-- Soundness at every program point reached during execution: for any node `s` visited
+    by the run `hrun` (witnessed by `hr`), the analysis result over-approximates both the
+    environment entering `s` and the one leaving it. The final-state theorem
+    `analyze_correct_state` is the special case where `s` is `prog.finalState`. -/
+theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
+    {s : prog.State} {ρin ρout : Env} {stin : S.St ρin} {stout : S.St ρout}
+    (hr : Reaches (prog.trace hrun) S.init s ρin ρout stin stout) :
+    ⟦ joinForKey s (result L prog) ⟧ ρin stin
+      ∧ ⟦ variablesAt s (result L prog) ⟧ ρout stout := by
+  refine walkTrace_reaches hr ?_
+  rw [joinForKey_initialState]
+  exact ValidStateEvaluator.botV_init
+
 end
 
 variable (L prog) in

lean/Spa/Analysis/Forward/Adapters.lean

@@ -14,44 +14,50 @@ lemma updateVariablesFromExpression_mono (k : String) (e : Expr) :
     Monotone (updateVariablesFromExpression (L := L) (prog := prog) k e) :=
   FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => E.eval_mono e)
 
-def evalBasicStmt (s : prog.State) (bs : BasicStmt) (_h : prog.code s = some bs)
+def evalBasicStmt (bs : BasicStmt)
     (vs : VariableValues L prog) : VariableValues L prog :=
   match bs with
   | .assign k e => updateVariablesFromExpression k e vs
   | .noop => vs
 
-lemma evalBasicStmt_mono (s : prog.State) (bs : BasicStmt) (h : prog.code s = some bs) :
-    Monotone (evalBasicStmt (L := L) (prog := prog) s bs h) := by
+lemma evalBasicStmt_mono (bs : BasicStmt) :
+    Monotone (evalBasicStmt (L := L) (prog := prog) bs) := by
   cases bs with
   | assign k e => exact updateVariablesFromExpression_mono k e
   | noop => exact monotone_id
 
+def evalBasicStmtOpt (obs : Option BasicStmt)
+    (vs : VariableValues L prog) : VariableValues L prog :=
+  match obs with
+  | none => vs
+  | some bs => evalBasicStmt bs vs
+
+lemma evalBasicStmtOpt_mono (obs : Option BasicStmt) :
+    Monotone (evalBasicStmtOpt (L := L) (prog := prog) obs) := by
+  cases obs <;> unfold evalBasicStmtOpt
+  · exact monotone_id
+  · apply evalBasicStmt_mono
+
 instance ExprEvaluator.toStmtEvaluator : StmtEvaluator L prog :=
-  ⟨evalBasicStmt, evalBasicStmt_mono⟩
+  ⟨evalBasicStmtOpt ∘ prog.code,
+   by intro s; simp; exact (evalBasicStmtOpt_mono (prog.code s))⟩
 
 instance ExprEvaluator.toStmtEvaluator_valid [LatticeInterpretation L]
     [ValidExprEvaluator L prog] : ValidStmtEvaluator L prog := by
   constructor
-  intro s vs ρ₁ ρ₂ bs hcode hbs hvs
-  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]
+  simp [StmtEvaluator.eval, evalBasicStmtOpt]
+  intro s vs ρ₁ ρ₂; generalize prog.code s = obs; intro hev hvs
+  rcases hev with _ | @⟨_,bs,hev⟩ <;> try simpa
+  rcases hev with _ | @⟨k, e, v, hev⟩ <;> try simpa
+  intros k' l' hkl' v' hρ
+  rcases hρ with _ | ⟨_,_,_,_,_,hne,hmem⟩ <;> simp [evalBasicStmt] at hkl'
+  · have hl := FiniteMap.generalizedUpdate_mem_eq (f := id)
+        (g := fun _ vs => E.eval e vs) (List.mem_singleton_self k) hkl'
+    rewrite [hl]; simp
     exact ValidExprEvaluator.valid hev hvs
-    | 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'
+  · have hl := FiniteMap.generalizedUpdate_not_mem_backward
+        (fun hmem => hne (List.mem_singleton.mp hmem)) hkl'
+    apply hvs _ _ hl _ hmem
 
 end Forward
 

lean/Spa/Analysis/Forward/Evaluation.lean

@@ -7,9 +7,8 @@ namespace Forward
 variable (L : Type) [Lattice L] (prog : Program)
 
 class StmtEvaluator where
-  eval : (s : prog.State) → (bs : BasicStmt) → prog.code s = some bs →
-    VariableValues L prog → VariableValues L prog
-  eval_mono : ∀ s bs h, Monotone (eval s bs h)
+  eval : prog.State → VariableValues L prog → VariableValues L prog
+  eval_mono : ∀ s, Monotone (eval s)
 
 class ExprEvaluator where
   eval : Expr → VariableValues L prog → L
@@ -22,9 +21,8 @@ class ValidExprEvaluator [ExprEvaluator L prog] [I : LatticeInterpretation L] :
 
 class ValidStmtEvaluator [E : StmtEvaluator L prog] [LatticeInterpretation L] :
     Prop where
-  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env}
-    {bs : BasicStmt} (hcode : prog.code s = some bs),
-    EvalBasicStmt ρ₁ bs ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s bs hcode vs ⟧ ρ₂ ()
+  valid : ∀ {s : prog.State} {vs : VariableValues L prog} {ρ₁ ρ₂ : Env},
+    EvalBasicStmtOpt ρ₁ (prog.code s) ρ₂ → ⟦ vs ⟧ ρ₁ () → ⟦ E.eval s vs ⟧ ρ₂ ()
 
 end Forward
 

lean/Spa/Analysis/Forward/Lattices.lean

@@ -64,7 +64,7 @@ lemma variablesAt_joinAll (s : prog.State) (sv : StateVariables L prog) :
     variablesAt s (joinAll sv) = joinForKey s sv :=
   joinAll_mem_eq (variablesAt_mem s (joinAll sv))
 
-class StateInterp (L : Type) [Lattice L] (prog : Program) where
+class StateInterpretation (L : Type) [Lattice L] (prog : Program) where
   St : Env → Type
   init : St []
   interp : VariableValues L prog → (ρ : Env) → St ρ → Prop
@@ -73,11 +73,11 @@ class StateInterp (L : Type) [Lattice L] (prog : Program) where
   interp_inf : ∀ {vs₁ vs₂ : VariableValues L prog} {ρ : Env} {st : St ρ},
     interp vs₁ ρ st ∧ interp vs₂ ρ st → interp (vs₁ ⊓ vs₂) ρ st
 
-instance [S : StateInterp L prog] :
+instance [S : StateInterpretation L prog] :
     Interp (VariableValues L prog) ((ρ : Env) → S.St ρ → Prop) :=
   ⟨S.interp⟩
 
-lemma interp_foldr [S : StateInterp L prog]
+lemma interp_foldr [S : StateInterpretation L prog]
     {vs : VariableValues L prog} {vss : List (VariableValues L prog)}
     {ρ : Env} {st : S.St ρ} (hvs : ⟦ vs ⟧ ρ st) (hmem : vs ∈ vss) :
     ⟦ vss.foldr (· ⊔ ·) (botV L prog) ⟧ ρ st := by
@@ -90,7 +90,7 @@ lemma interp_foldr [S : StateInterp L prog]
 
 variable [I : LatticeInterpretation L]
 
-instance : StateInterp L prog where
+instance : StateInterpretation L prog where
   St := fun _ => PUnit
   init := PUnit.unit
   interp vs ρ _ := ∀ (k : String) (l : L), (k, l) ∈ vs →

lean/Spa/Analysis/Reaching.lean

@@ -1,6 +1,5 @@
 import Spa.Analysis.Forward
-import Spa.Lattice.Bool
-import Spa.Lattice.Tuple
+import Spa.Lattice.Finset
 import Spa.Language.Tagged.Graphs
 import Spa.Showable
 
@@ -8,37 +7,35 @@ namespace Spa
 
 open Forward
 
-instance : Showable Bool := ⟨fun b => if b then "true" else "false"⟩
-
-instance {n : ℕ} {β : Type*} [Showable β] : Showable (Fin n → β) :=
-  ⟨fun f =>
+instance {n : ℕ} : Showable (Finset (Fin n)) :=
+  ⟨fun s =>
     "{" ++ (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
 
 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
+def genSet (s : prog.State) : DefSet prog := (prog.nodeIdOf s).elim {} (fun x => {x})
 
-def eval (s : prog.State) :
-    (bs : BasicStmt) → prog.code s = some bs →
-    VariableValues (DefSet prog) prog → VariableValues (DefSet prog) prog
-  | .assign k _, h, vs =>
-    FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s h) [k] vs
-  | .noop, _, vs => vs
+def eval (s : prog.State) (vs : VariableValues (DefSet prog) prog) : VariableValues (DefSet prog) prog :=
+  match prog.code s with
+  | none => vs
+  | some bs =>
+    match bs with
+    | .assign k _ => FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s) [k] vs
+    | .noop => vs
 
-lemma eval_mono (s : prog.State) (bs : BasicStmt) (h : prog.code s = some bs) :
-    Monotone (eval prog s bs h) := by
-  cases bs with
-  | assign k e =>
-    exact FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
-  | noop => exact monotone_id
+lemma eval_mono (s : prog.State) :
+    Monotone (eval prog s) := by
+  intros vs₁ vs₂ hle
+  unfold eval; split <;> try simpa
+  split <;> try simpa
+  apply FiniteMap.generalizedUpdate_monotone monotone_id (fun _ => monotone_const)
+  assumption
 
 instance stmtEvaluator : StmtEvaluator (DefSet prog) prog :=
   ⟨eval prog, eval_mono prog⟩
@@ -48,49 +45,54 @@ def output : String :=
 
 inductive Run (prog : Program) where
   | nil : Run prog
-  | cons (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
+  | cons (s : prog.State) (bs : BasicStmt)
       (rest : Run prog) : Run prog
 
 @[aesop unsafe cases]
 inductive LastAssign (prog : Program) (x : String) : Run prog → prog.NodeId → Prop
   | here (s : prog.State) (e : Expr) (hc : prog.code s = some (.assign x e))
       (rest : Run prog) :
-      LastAssign prog x (Run.cons s (.assign x e) hc rest) (prog.nodeIdOfNonempty s hc)
+      LastAssign prog x (Run.cons s (.assign x e) rest) (prog.nodeIdOfNonempty s hc)
   | there (s : prog.State) (bs : BasicStmt) (hc : prog.code s = some bs)
       (rest : Run prog) {n : prog.NodeId} :
       (∀ e, bs ≠ .assign x e) → LastAssign prog x rest n →
-      LastAssign prog x (Run.cons s bs hc rest) n
+      LastAssign prog x (Run.cons s bs rest) n
 
-instance stateInterp : StateInterp (DefSet prog) prog where
+instance stateInterp : StateInterpretation (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)
+
+private def stepAt (s : prog.State) (obs : Option BasicStmt) { ρ₁ ρ₂ : Env} : EvalBasicStmtOpt ρ₁ obs ρ₂ → Run prog → Run prog
+  | .none, rest => rest
+  | .some (bs := bs) _, rest => Run.cons s bs rest
 
 instance validStateEvaluator : ValidStateEvaluator (DefSet prog) prog where
-  step := by intro s _ _ bs hcode _ rest; exact Run.cons s bs hcode rest
+  step := fun s ρ₁ ρ₂ => stepAt prog s (prog.code s)
   valid := by
-    intro s ρ₁ ρ₂ bs vs st hcode hbs hvs
+    simp [StmtEvaluator.eval, eval];
+    intro s ρ₁ ρ₂ vs; generalize prog.code s = obs; intro hst hbs hvs
+    rcases hbs with _ | @⟨_, bs, hbs⟩; try (simpa [stepAt])
     cases hbs with
     | noop => intro x assigners hmem n hla; aesop
     | assign x e v hev =>
-      intro k assigners hmem n hla
-      have hmem2 : (k, assigners) ∈
-          FiniteMap.generalizedUpdate id (fun _ _ => genSet prog s hcode) [x] vs := hmem
+      simp; intro k assigners hmem n hla
       by_cases hx : k = x
       · subst hx
-        have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem2
-        aesop (add simp genSet)
+        have hd := FiniteMap.generalizedUpdate_mem_eq (List.mem_singleton.mpr rfl) hmem
+        rcases hla
+          <;> simp [Program.nodeIdOfNonempty, hd, genSet, Option.get] <;> aesop
       · have hmem' := FiniteMap.generalizedUpdate_not_mem_backward
-          (fun hc => hx (List.mem_singleton.mp hc)) hmem2
+          (fun hc => hx (List.mem_singleton.mp hc)) hmem
         aesop
   botV_init := by intro x assigners _ n hla; cases hla
 
@@ -99,6 +101,13 @@ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
       (stepTraceState (prog.trace hrun) (stateInterp prog).init) :=
   Forward.analyze_correct_state (DefSet prog) prog hrun
 
+theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
+    {s : prog.State} {ρin ρout : Env} {stin : Run prog} {stout : Run prog}
+    (hr : Reaches (prog.trace hrun) (stateInterp prog).init s ρin ρout stin stout) :
+    ⟦ joinForKey s (result (DefSet prog) prog) ⟧ ρin stin
+      ∧ ⟦ variablesAt s (result (DefSet prog) prog) ⟧ ρout stout :=
+  Forward.analyze_correct_at (DefSet prog) prog hrun hr
+
 end ReachingAnalysis
 
 end Spa

lean/Spa/Analysis/Sign.lean

@@ -213,6 +213,13 @@ theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
     ⟦ variablesAt prog.finalState (result SignLattice prog) ⟧ ρ () :=
   Forward.analyze_correct SignLattice prog hrun
 
+theorem analyze_correct_at {ρf : Env} (hrun : EvalStmt [] prog.rootStmt ρf)
+    {s : prog.State} {ρin ρout : Env} {stin stout : PUnit}
+    (hr : Reaches (L := SignLattice) (prog.trace hrun) PUnit.unit s ρin ρout stin stout) :
+    ⟦ joinForKey s (result SignLattice prog) ⟧ ρin stin
+      ∧ ⟦ variablesAt s (result SignLattice prog) ⟧ ρout stout :=
+  Forward.analyze_correct_at SignLattice prog hrun hr
+
 end SignAnalysis
 
 end Spa

lean/Spa/Language.lean

@@ -3,56 +3,4 @@ import Spa.Language.Semantics
 import Spa.Language.Graphs
 import Spa.Language.Traces
 import Spa.Language.Properties
-import Mathlib.Data.Finset.Sort
-import Mathlib.Data.String.Basic
-
-namespace Spa
-
-structure Program where
-  rootStmt : Stmt
-
-namespace Program
-
-variable (p : Program)
-
-def cfg : Graph := Graph.wrap p.rootStmt.cfg
-
-abbrev State : Type := p.cfg.Index
-
-def initialState : p.State := p.rootStmt.cfg.wrapInput
-
-def finalState : p.State := p.rootStmt.cfg.wrapOutput
-
-noncomputable def trace {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
-    Trace p.cfg p.initialState p.finalState [] ρ := by
-  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h)
-  rw [Graph.wrap_inputs, List.mem_singleton] at h₁
-  rw [Graph.wrap_outputs, List.mem_singleton] at h₂
-  subst h₁; subst h₂
-  exact tr
-
-def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
-
-lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
-
-def states : List p.State := p.cfg.indices
-
-lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
-
-lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
-
-def code (st : p.State) : Option BasicStmt := p.cfg.nodes st
-
-def incoming (s : p.State) : List p.State := p.cfg.predecessors s
-
-lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
-  Graph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
-    (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
-
-lemma mem_incoming_of_edge {s₁ s₂ : p.State}
-    (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ :=
-  p.cfg.mem_predecessors_of_edge h
-
-end Program
-
-end Spa
+import Spa.Language.Program

lean/Spa/Language/Graphs.lean

@@ -25,6 +25,15 @@ indexing into a list.
 
 -/
 
+/-- Logically, when combining `Fin`s from two distinct pools,
+    the combination is disjoint. -/
+lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
+    Fin.castAdd m i ≠ Fin.natAdd n j := by
+  intro h
+  have := congrArg Fin.val h
+  simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
+  omega
+
 /-- Bump the upper bound of a list of `Fin`s without changing their value. -/
 def List.finCastAdd {n : ℕ} (l : List (Fin n)) (m : ℕ) : List (Fin (n + m)) :=
   l.map (Fin.castAdd m)
@@ -157,6 +166,22 @@ def singleton (a : α) : GGraph α where
 def wrap (g : GGraph (Option β)) : GGraph (Option β) :=
   singleton none ⤳ g ⤳ singleton none
 
+/-- The input / entry node generated by `GGraph.wrap`. -/
+def wrapInput (g : GGraph (Option β)) : (wrap g).Index :=
+  (0 : Fin 1).castAdd ((g ⤳ singleton none).size)
+
+/-- The output / exit node generated by `GGraph.wrap`. -/
+def wrapOutput (g : GGraph (Option β)) : (wrap g).Index :=
+  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
+
+/-- The `wrapInput` is, indeed, the graph's only input after `wrap`. -/
+lemma wrap_inputs (g : GGraph (Option β)) :
+    (wrap g).inputs = [g.wrapInput] := rfl
+
+/-- The `wrapInput` is, indeed, the graph's only output after `wrap`. -/
+lemma wrap_outputs (g : GGraph (Option β)) :
+    (wrap g).outputs = [g.wrapOutput] := rfl
+
 @[simp] lemma map_singleton (f : α → β) (a : α) :
     f <$> singleton a = singleton (f a) := rfl
 
@@ -205,6 +230,35 @@ lemma nodup_indices : g.indices.Nodup :=
 def predecessors (idx : g.Index) : List g.Index :=
   g.indices.filter (fun idx' => (idx', idx) ∈ g.edges)
 
+/-- When sequencing (proven here with `Graph.singleton` on the left), no edges
+    exist from the right-hand graph back to the left. -/
+private lemma not_mem_edges_castAdd_sequence {g₂ : GGraph (Option β)} (i : Fin 1)
+    (idx : (singleton none ⤳ g₂).Index) :
+    ((idx, i.castAdd g₂.size) : (singleton none ⤳ g₂).Edge)
+      ∉ (singleton none ⤳ g₂).edges := by
+  intro h
+  rcases List.mem_append.mp h with h' | h'
+  · rcases List.mem_append.mp h' with h'' | h''
+    · -- lifted edges of `singleton []`: there are none
+      simp [singleton, List.finCastAddProd] at h''
+    · -- lifted edges of g₂: targets are natAdd
+      obtain ⟨e, _, heq⟩ := List.mem_map.mp h''
+      exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm
+  · -- product edges: targets are natAdd'd inputs of g₂
+    obtain ⟨-, hb⟩ := List.mem_product.mp h'
+    obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
+    exact Fin.castAdd_ne_natAdd i j heq.symm
+
+/-- The input node of a graph after `Graph.wrap` has no predecessors. -/
+lemma wrap_predecessors_eq_nil (g : GGraph (Option β)) (idx : (wrap g).Index)
+    (h : idx ∈ (wrap g).inputs) :
+    (wrap g).predecessors idx = [] := by
+  rw [wrap_inputs, List.mem_singleton] at h
+  subst h
+  rw [GGraph.predecessors, List.filter_eq_nil_iff]
+  intro idx' _
+  simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ singleton none) 0 idx'
+
 /-- There's there's an edge between two nodes `idx₁` and `idx₂`,
     then `idx₁` is the predecessor of `idx₂`. -/
 lemma mem_predecessors_of_edge {idx₁ idx₂ : g.Index}
@@ -225,7 +279,7 @@ abbrev Graph : Type := GGraph (Option BasicStmt)
 
 namespace Graph
 
-export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs)
+export GGraph (overlay sequence loop singleton wrap loop_inputs loop_outputs wrapInput wrapOutput wrap_inputs wrap_outputs)
 
 @[inherit_doc] scoped infixr:70 " ∙ " => GGraph.overlay
 @[inherit_doc] scoped infixr:70 " ⤳ " => GGraph.sequence

lean/Spa/Language/Program.lean

@@ -0,0 +1,76 @@
+import Spa.Language.Base
+import Spa.Language.Semantics
+import Spa.Language.Graphs
+import Mathlib.Data.Finset.Sort
+import Mathlib.Data.String.Basic
+
+namespace Spa
+
+/-- A self-contained program to be evaluated, analyzed, and transformed. -/
+structure Program where
+  /-- The statement at the top level of the program. Since `Spa.Stmt` contains
+      sequencing via `Spa.Stmt.andThen`, this can encode any number of
+      statements. -/
+  rootStmt : Stmt
+  /-- A memoized copy of the control-flow graph. This field is an
+      implementation detail to avoid re-computing `Spa.GGraph.wrap` and `Spa.Stmt.cfg`
+      every time the program's control flow graph is needed -/
+  cfgCache : Thunk Graph := Thunk.mk fun _ => Graph.wrap rootStmt.cfg
+
+namespace Program
+
+variable (p : Program)
+
+-- Runtime implementation of `cfg`: read the memoized graph.
+private def cfgImpl : Graph := p.cfgCache.get
+
+/-- The control flow graph corresponding to this graph. -/
+@[implemented_by cfgImpl]
+def cfg : Graph := Graph.wrap p.rootStmt.cfg
+
+/-- A state in the control flow `Spa.Graph` of this program. -/
+abbrev State : Type := p.cfg.Index
+
+/-- Variables mentioned or defined in this program. -/
+def vars : List String := p.rootStmt.vars.sort (· ≤ ·)
+
+/-- `vars` has no duplicates. -/
+lemma vars_nodup : p.vars.Nodup := Finset.sort_nodup _ _
+
+/-- All the states in the program's control flow `Spa.Graph`. -/
+def states : List p.State := p.cfg.indices
+
+/-- All states in the CFG are contained in `states`. -/
+lemma states_complete (s : p.State) : s ∈ p.states := p.cfg.mem_indices s
+
+/-- `states` has no duplicates. -/
+lemma states_nodup : p.states.Nodup := p.cfg.nodup_indices
+
+/-- Given a node of the program's CFG, return the code at that node.
+    At this time, for convenience of proofs, the CFGs have at most
+    one basic statement, and multi-statement basic blocks are encoded
+    as chains of blocks. Thus, this returns at most one `Spa.BasicStmt`. -/
+def code (st : p.State) : Option BasicStmt := p.cfg.nodes st
+
+/-- Get the predecessors of a particular CFG node / program state. -/
+def incoming (s : p.State) : List p.State := p.cfg.predecessors s
+
+/-- The entry point of the program's CFG. -/
+def initialState : p.State := Graph.wrapInput p.rootStmt.cfg
+
+/-- The exit point of the program's CFG. -/
+def finalState : p.State := Graph.wrapOutput p.rootStmt.cfg
+
+/-- `incoming` is a faithful representation of edges in the CFG. -/
+lemma mem_incoming_of_edge {s₁ s₂ : p.State}
+    (h : (s₁, s₂) ∈ p.cfg.edges) : s₁ ∈ p.incoming s₂ :=
+  p.cfg.mem_predecessors_of_edge h
+
+/-- The `initialState` has no incoming edges (it's the program start). -/
+lemma incoming_initialState_eq_nil : p.incoming p.initialState = [] :=
+  GGraph.wrap_predecessors_eq_nil p.rootStmt.cfg p.initialState
+    (by rw [Graph.wrap_inputs]; exact List.mem_singleton_self _)
+
+end Program
+
+end Spa

lean/Spa/Language/Properties.lean

@@ -23,13 +23,6 @@ namespace Spa
 
 open Graph
 
-lemma Fin.castAdd_ne_natAdd {n m : ℕ} (i : Fin n) (j : Fin m) :
-    Fin.castAdd m i ≠ Fin.natAdd n j := by
-  intro h
-  have := congrArg Fin.val h
-  simp only [Fin.coe_castAdd, Fin.coe_natAdd] at this
-  omega
-
 section Embeddings
 
 variable {g₁ g₂ : Graph} {ρ₁ ρ₂ : Env}
@@ -246,49 +239,17 @@ noncomputable def Stmt.cfg_sufficient {s : Stmt} {ρ₁ ρ₂ : Env}
   | whileFalse ρ e s _ =>
     exact EndToEndTrace.loop_empty
 
-/-- The input / entry node generated by `Graph.wrap`. -/
-def Graph.wrapInput (g : Graph) : (Graph.wrap g).Index :=
-  (0 : Fin 1).castAdd ((g ⤳ Graph.singleton none).size)
+namespace Program
 
-/-- The output / exit node generated by `Graph.wrap`. -/
-def Graph.wrapOutput (g : Graph) : (Graph.wrap g).Index :=
-  Fin.natAdd 1 ((Fin.natAdd g.size (0 : Fin 1)))
+noncomputable def trace (p : Program) {ρ : Env} (h : EvalStmt [] p.rootStmt ρ) :
+    Trace p.cfg p.initialState p.finalState [] ρ := by
+  obtain ⟨i₁, h₁, i₂, h₂, tr⟩ := EndToEndTrace.wrap (Stmt.cfg_sufficient h)
+  rw [Graph.wrap_inputs, List.mem_singleton] at h₁
+  rw [Graph.wrap_outputs, List.mem_singleton] at h₂
+  subst h₁; subst h₂
+  exact tr
 
-/-- The `Graph.wrapInput` is, indeed, the graph's only input after `Graph.wrap`. -/
-lemma Graph.wrap_inputs (g : Graph) :
-    (Graph.wrap g).inputs = [g.wrapInput] := rfl
+end Program
 
-/-- The `Graph.wrapInput` is, indeed, the graph's only output after `Graph.wrap`. -/
-lemma Graph.wrap_outputs (g : Graph) :
-    (Graph.wrap g).outputs = [g.wrapOutput] := rfl
-
-/-- When sequencing (proven here with `Graph.singleton` on the left), no edges
-    exist from the right-hand graph back to the left. -/
-private lemma not_mem_edges_castAdd_sequence {g₂ : Graph} (i : Fin 1)
-    (idx : (Graph.singleton none ⤳ g₂).Index) :
-    ((idx, i.castAdd g₂.size) : (Graph.singleton none ⤳ g₂).Edge)
-      ∉ (Graph.singleton none ⤳ g₂).edges := by
-  intro h
-  rcases List.mem_append.mp h with h' | h'
-  · rcases List.mem_append.mp h' with h'' | h''
-    · -- lifted edges of `singleton []`: there are none
-      simp [Graph.singleton, List.finCastAddProd] at h''
-    · -- lifted edges of g₂: targets are natAdd
-      obtain ⟨e, _, heq⟩ := List.mem_map.mp h''
-      exact Fin.castAdd_ne_natAdd i e.2 (congrArg Prod.snd heq).symm
-  · -- product edges: targets are natAdd'd inputs of g₂
-    obtain ⟨-, hb⟩ := List.mem_product.mp h'
-    obtain ⟨j, -, heq⟩ := List.mem_map.mp hb
-    exact Fin.castAdd_ne_natAdd i j heq.symm
-
-/-- The input node of a graph after `Graph.wrap` has no predecessors. -/
-lemma Graph.wrap_predecessors_eq_nil (g : Graph) (idx : (Graph.wrap g).Index)
-    (h : idx ∈ (Graph.wrap g).inputs) :
-    (Graph.wrap g).predecessors idx = [] := by
-  rw [Graph.wrap_inputs, List.mem_singleton] at h
-  subst h
-  rw [GGraph.predecessors, List.filter_eq_nil_iff]
-  intro idx' _
-  simpa using not_mem_edges_castAdd_sequence (g₂ := g ⤳ Graph.singleton none) 0 idx'
 
 end Spa

lean/Spa/Language/Traces.lean

@@ -1,5 +1,6 @@
 import Spa.Language.Semantics
 import Spa.Language.Graphs
+import Spa.Language.Program
 
 /-!
 

lean/Spa/Lattice/AboveBelow.lean

@@ -1,7 +1,38 @@
 import Spa.Lattice
 
+/-!
+
+# The Above-Below Lattice
+
+This file defines the `AboveBelow` lattice, which takes a flat domain
+$a_1, \ldots, a_n \in \alpha$ and lifts it into a lattice bounded
+above by a synthetic $\top$ element, and below by a synthetic $\bot$
+element.
+
+$$
+\begin{array}{ccccc}
+  && \top && \\
+  & \swarrow & \downarrow & \searrow & \\
+  a_1 & & … & & a_n \\
+  & \searrow & \downarrow & \swarrow & \\
+  && \bot &&
+\end{array}
+$$
+
+This lattice is also a `Spa.FiniteHeightLattice`, because no chain can
+exceed the bottom-to-top chain $\bot < a_i < \top$.
+
+The above-below lattice is helpful for for analyses such as
+`Spa/Analysis/Sign.lean` and `Spa/Analysis/Constant.lean`, whose
+classifications of values (by sign or by exact value) do not have
+any inherent structure beyond "matching exactly".
+
+-/
+
 namespace Spa
 
+/-- The above-below lattice, with bottom element `bot` and top element `top`. -/
+@[aesop safe cases]
 inductive AboveBelow (α : Type*) where
   | bot
   | top
@@ -10,8 +41,6 @@ inductive AboveBelow (α : Type*) where
 
 namespace AboveBelow
 
-attribute [aesop safe cases] AboveBelow
-
 instance {α : Type*} [ToString α] : ToString (AboveBelow α) where
   toString
     | bot => "⊥"
@@ -50,23 +79,12 @@ instance : Min (AboveBelow α) where
 @[simp] lemma mk_inf_mk (x y : α) :
     (mk x ⊓ mk y : AboveBelow α) = if x = y then mk x else bot := rfl
 
-protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by
-  aesop
-
-protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by
-  aesop
-
-protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by
-  aesop
-
-protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by
-  aesop
-
-protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by
-  aesop
-
-protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by
-  aesop
+protected lemma sup_comm (a b : AboveBelow α) : a ⊔ b = b ⊔ a := by aesop
+protected lemma sup_assoc (a b c : AboveBelow α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c) := by aesop
+protected lemma inf_comm (a b : AboveBelow α) : a ⊓ b = b ⊓ a := by aesop
+protected lemma inf_assoc (a b c : AboveBelow α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) := by aesop
+protected lemma sup_inf_self (a b : AboveBelow α) : a ⊔ a ⊓ b = a := by aesop
+protected lemma inf_sup_self (a b : AboveBelow α) : a ⊓ (a ⊔ b) = a := by aesop
 
 instance : Lattice (AboveBelow α) :=
   Lattice.mk' AboveBelow.sup_comm AboveBelow.sup_assoc
@@ -89,123 +107,72 @@ instance : OrderTop (AboveBelow α) where
   top := top
   le_top := le_top'
 
-lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x :=
-  lt_of_le_of_ne (bot_le' _) (by simp)
-
-lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top :=
-  lt_of_le_of_ne (le_top' _) (by simp)
-
-lemma bot_lt_top : (bot : AboveBelow α) < top :=
-  lt_of_le_of_ne (bot_le' _) (by simp)
+lemma bot_lt_mk (x : α) : (bot : AboveBelow α) < mk x := lt_of_le_of_ne (bot_le' _) (by simp)
+lemma mk_lt_top (x : α) : (mk x : AboveBelow α) < top := lt_of_le_of_ne (le_top' _) (by simp)
+lemma bot_lt_top : (bot : AboveBelow α) < top := lt_of_le_of_ne (bot_le' _) (by simp)
 
 lemma le_cases {a b : AboveBelow α} (h : a ≤ b) :
     a = bot ∨ b = top ∨ a = b := by
-  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)
+  rw [le_iff] at h
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;> simp_all
 
-/-- 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. -/
+/-- If `f` sends `⊥` to `⊥` (in both arguments) and `⊤` to `⊤`
+    (against any non-`⊥` argument), it is monotone in both arguments.
+    The values of the the elements in `α` are irrelevant since they
+    are always incomparable. This makes it easy to prove monotonicity
+    for operations that "just" combine their flat elements, or give up. -/
 lemma monotone₂_of_strict {β γ : Type*} [DecidableEq β] [DecidableEq γ]
     (f : AboveBelow α → AboveBelow β → AboveBelow γ)
     (hbotl : ∀ y, f bot y = bot) (hbotr : ∀ x, f x bot = bot)
     (htopl : ∀ y, y ≠ bot → f top y = top)
     (htopr : ∀ x, x ≠ bot → f x top = top) : Monotone₂ f := by
-  constructor
-  · intro 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
-    show f x a ≤ f x b
-    rcases le_cases hab with rfl | rfl | rfl
-    · rw [hbotr]; exact bot_le' _
-    · rcases eq_or_ne x bot with rfl | hx
-      · rw [hbotl, hbotl]
-      · rw [htopr x hx]; exact le_top' _
-    · exact le_rfl
-
-/-! ### Interpretations of flat lattices -/
+  constructor <;> intro c a b hab <;>
+    rcases eq_or_ne c bot with rfl | hc <;>
+    rcases le_cases hab with rfl | rfl | rfl <;>
+    simp [hbotl, hbotr, htopl, htopr, bot_le', le_top', *]
 
 section Interp
 
 variable {V : Type*} {P : AboveBelow α → V → Prop}
 
+/-- As long as the interpretation of a the above-below lattice respects the
+    fact that `bot` means "impossible", interpreting the above-below
+    lattice agrees with its `⊔`. -/
 lemma interp_sup_of (hbot : ∀ v, ¬P bot v) (htop : ∀ v, P top v)
-    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by
-  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
+    {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∨ P s₂ v) : P (s₁ ⊔ s₂) v := by aesop
 
+/-- As long as two distinct values in the flat domain don't overlap,
+    interpreting the above-below lattice agrees with its `⊔` -/
 lemma interp_inf_of
     (hdisj : ∀ {x y : α}, x ≠ y → ∀ v, ¬(P (mk x) v ∧ P (mk y) v))
     {s₁ s₂ : AboveBelow α} (v : V) (h : P s₁ v ∧ P s₂ v) : P (s₁ ⊓ s₂) v := by
-  rcases s₁ with _ | _ | x
-  · 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]
+  rcases s₁ with _ | _ | x <;> rcases s₂ with _ | _ | y <;> simp_all
   split
-      · next heq => subst heq; exact h.1
-      · next hne => exact absurd h (hdisj hne v)
+  · exact h.2
+  · next hne => exact (hdisj hne v h.1 h.2).elim
 
 end Interp
 
-/-- Rank of an element: `⊥ ↦ 0`, `[x] ↦ 1`, `⊤ ↦ 2`. Used to bound chains
-(Agda's `isLongest` / `x≺[y]⇒x≡⊥` / `[x]≺y⇒y≡⊤` case analysis lives here). -/
-def rank : AboveBelow α → ℕ
+/-- synthetic rank of an element, used to prove chain bounds. -/
+private 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). -/
+/-- It's not possible for any two lifted flat-domain elements to be less
+    than one another. -/
 lemma not_mk_lt_mk (x y : α) : ¬(mk x : AboveBelow α) < mk y := by
   intro h
   obtain ⟨hle, hne⟩ := lt_iff_le_and_ne.mp h
   rcases le_cases hle with h | h | h <;> simp_all
 
+/-- The rank of elements is strictly monotonic. -/
 lemma rank_strictMono : StrictMono (rank : AboveBelow α → ℕ) := by
   intro a b hab
-  rcases a with _ | _ | x <;> rcases b with _ | _ | y
-  · 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)
+  rcases a with _ | _ | x <;> rcases b with _ | _ | y <;>
+    simp_all [rank, not_mk_lt_mk, (bot_le' _).not_lt, (le_top' _).not_lt]
 
+/-- All chains in the above-below lattice have at most 2 comparisons. -/
 lemma boundedChains : BoundedChains (AboveBelow α) 2 := fun c => by
   have h := LTSeries.head_add_length_le_nat (c.map rank rank_strictMono)
   rw [LTSeries.head_map, LTSeries.last_map, LTSeries.map_length] at h

lean/Spa/Lattice/FiniteMap.lean

@@ -1,64 +1,79 @@
 import Spa.Lattice.Tuple
 import Mathlib.Data.List.Nodup
 
+/-!
+
+# Finite Maps
+
+This file defines _finite maps_, or key-value maps with a finite domain. This
+is encoded as a map from `Fin` into the value type. Finite maps form a
+lattice from pointwise composition: $(f \land g) k = f k \land g k$,
+and, provided the domain `\beta` is of finite height, so is the map
+lattice as a whole.
+
+In fact, the isomorphism is described and proven in `Spa/Lattice/Tuple.lean`.
+
+-/
+
 namespace Spa
 
-def FiniteMap (A B : Type*) (ks : List A) : Type _ := Fin ks.length → B
+/-- Key-value map with domain `α` and codomain `β`, with possible keys $\textit{ks} \subseteq \alpha$. -/
+def FiniteMap (α β : Type*) (ks : List α) : Type _ := Fin ks.length → β
 
 namespace FiniteMap
 
-variable {A B : Type*} {ks : List A}
+variable {α β : Type*} {ks : List α}
 
-instance [Lattice B] : Lattice (FiniteMap A B ks) :=
-  inferInstanceAs (Lattice (Fin ks.length → B))
+instance [Lattice β] : Lattice (FiniteMap α β ks) :=
+  inferInstanceAs (Lattice (Fin ks.length → β))
 
-instance [FiniteHeightLattice B] : FiniteHeightLattice (FiniteMap A B ks) :=
-  inferInstanceAs (FiniteHeightLattice (Fin ks.length → B))
+instance [FiniteHeightLattice β] : FiniteHeightLattice (FiniteMap α β ks) :=
+  inferInstanceAs (FiniteHeightLattice (Fin ks.length → β))
 
-instance [DecidableEq B] : DecidableEq (FiniteMap A B ks) :=
-  inferInstanceAs (DecidableEq (Fin ks.length → B))
+instance [DecidableEq β] : DecidableEq (FiniteMap α β ks) :=
+  inferInstanceAs (DecidableEq (Fin ks.length → β))
 
-instance : Membership (A × B) (FiniteMap A B ks) :=
+instance : Membership (α × β) (FiniteMap α β ks) :=
   ⟨fun fm p => ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2⟩
 
-lemma mem_iff {fm : FiniteMap A B ks} {p : A × B} :
+lemma mem_iff {fm : FiniteMap α β ks} {p : α × β} :
     p ∈ fm ↔ ∃ i : Fin ks.length, ks.get i = p.1 ∧ fm i = p.2 := Iff.rfl
 
-def MemKey (k : A) (_fm : FiniteMap A B ks) : Prop := k ∈ ks
+def MemKey (k : α) (_fm : FiniteMap α β ks) : Prop := k ∈ ks
 
-lemma MemKey_iff {k : A} {fm : FiniteMap A B ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
+lemma MemKey_iff {k : α} {fm : FiniteMap α β ks} : MemKey k fm ↔ k ∈ ks := Iff.rfl
 
-instance {k : A} {fm : FiniteMap A B ks} [DecidableEq A] : Decidable (MemKey k fm) :=
+instance {k : α} {fm : FiniteMap α β ks} [DecidableEq α] : Decidable (MemKey k fm) :=
   decidable_of_iff _ MemKey_iff.symm
 
-lemma mem_key_of_mem {k : A} {v : B} {fm : FiniteMap A B ks}
+lemma mem_key_of_mem {k : α} {v : β} {fm : FiniteMap α β ks}
     (h : (k, v) ∈ fm) : MemKey k fm := by
   obtain ⟨i, hi, _⟩ := h
   have hik : ks.get i = k := hi
   exact hik ▸ ks.get_mem i
 
-def toList (fm : FiniteMap A B ks) : List (A × B) :=
+def toList (fm : FiniteMap α β ks) : List (α × β) :=
   (List.finRange ks.length).map fun i => (ks.get i, fm i)
 
-lemma le_def [Lattice B] {fm₁ fm₂ : FiniteMap A B ks} :
+lemma le_def [Lattice β] {fm₁ fm₂ : FiniteMap α β ks} :
     fm₁ ≤ fm₂ ↔ ∀ i, fm₁ i ≤ fm₂ i := Iff.rfl
 
 section Locate
 
-variable [DecidableEq A]
+variable [DecidableEq α]
 
 /-- Recover the value stored under a present key. -/
-def locate {k : A} {fm : FiniteMap A B ks} (h : MemKey k fm) :
-    {v : B // (k, v) ∈ fm} :=
+def locate {k : α} {fm : FiniteMap α β ks} (h : MemKey k fm) :
+    {v : β // (k, v) ∈ fm} :=
   let i : Fin ks.length := ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩
   ⟨fm i, i, List.idxOf_get _, rfl⟩
 
 end Locate
 
-variable [Lattice B]
+variable [Lattice β]
 
-lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
-    (hle : fm₁ ≤ fm₂) {k : A} {v₁ v₂ : B}
+lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap α β ks}
+    (hle : fm₁ ≤ fm₂) {k : α} {v₁ v₂ : β}
     (h₁ : (k, v₁) ∈ fm₁) (h₂ : (k, v₂) ∈ fm₂) : v₁ ≤ v₂ := by
   obtain ⟨i, hi, rfl⟩ := h₁
   obtain ⟨j, hj, rfl⟩ := h₂
@@ -66,13 +81,13 @@ lemma le_of_mem_mem (hks : ks.Nodup) {fm₁ fm₂ : FiniteMap A B ks}
   subst hij
   exact le_def.mp hle i
 
-lemma mem_sup {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
+lemma mem_sup {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
     (h : (k, v) ∈ fm₁ ⊔ fm₂) :
     ∃ v₁ v₂, v = v₁ ⊔ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
   obtain ⟨i, hi, rfl⟩ := h
   exact ⟨fm₁ i, fm₂ i, rfl, ⟨i, hi, rfl⟩, ⟨i, hi, rfl⟩⟩
 
-lemma mem_inf {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
+lemma mem_inf {fm₁ fm₂ : FiniteMap α β ks} {k : α} {v : β}
     (h : (k, v) ∈ fm₁ ⊓ fm₂) :
     ∃ v₁ v₂, v = v₁ ⊓ v₂ ∧ (k, v₁) ∈ fm₁ ∧ (k, v₂) ∈ fm₂ := by
   obtain ⟨i, hi, rfl⟩ := h
@@ -80,30 +95,30 @@ lemma mem_inf {fm₁ fm₂ : FiniteMap A B ks} {k : A} {v : B}
 
 section Updating
 
-variable [DecidableEq A]
+variable [DecidableEq α]
 
-def updating (fm : FiniteMap A B ks) (ks' : List A) (g : A → B) : FiniteMap A B ks :=
+def updating (fm : FiniteMap α β ks) (ks' : List α) (g : α → β) : FiniteMap α β ks :=
   fun i => if ks.get i ∈ ks' then g (ks.get i) else fm i
 
-omit [Lattice B] in
-lemma eq_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
-    {ks' : List A} {g : A → B} (hk : k ∈ ks')
+omit [Lattice β] in
+lemma eq_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
+    {ks' : List α} {g : α → β} (hk : k ∈ ks')
     (h : (k, v) ∈ updating fm ks' g) : v = g k := by
   obtain ⟨i, hi, rfl⟩ := h
   show (if ks.get i ∈ ks' then g (ks.get i) else fm i) = g k
   rw [if_pos (by rw [hi]; exact hk), hi]
 
-omit [Lattice B] in
-lemma mem_of_mem_updating {k : A} {v : B} {fm : FiniteMap A B ks}
-    {ks' : List A} {g : A → B} (hk : k ∉ ks')
+omit [Lattice β] in
+lemma mem_of_mem_updating {k : α} {v : β} {fm : FiniteMap α β ks}
+    {ks' : List α} {g : α → β} (hk : k ∉ ks')
     (h : (k, v) ∈ updating fm ks' g) : (k, v) ∈ fm := by
   obtain ⟨i, hi, rfl⟩ := h
   refine ⟨i, hi, ?_⟩
   show fm i = (if ks.get i ∈ ks' then g (ks.get i) else fm i)
   rw [if_neg (by rw [hi]; exact hk)]
 
-lemma updating_mono {fm₁ fm₂ : FiniteMap A B ks} {ks' : List A}
-    {g₁ g₂ : A → B} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
+lemma updating_mono {fm₁ fm₂ : FiniteMap α β ks} {ks' : List α}
+    {g₁ g₂ : α → β} (hfm : fm₁ ≤ fm₂) (hg : ∀ k, g₁ k ≤ g₂ k) :
     updating fm₁ ks' g₁ ≤ updating fm₂ ks' g₂ := by
   rw [le_def]
   intro i
@@ -117,25 +132,25 @@ end Updating
 
 section GeneralizedUpdate
 
-variable [DecidableEq A] {L : Type*} [Lattice L]
+variable [DecidableEq α] {L : Type*} [Lattice L]
 
-def generalizedUpdate (f : L → FiniteMap A B ks) (g : A → L → B)
-    (ks' : List A) : L → FiniteMap A B ks := fun l =>
+def generalizedUpdate (f : L → FiniteMap α β ks) (g : α → L → β)
+    (ks' : List α) : L → FiniteMap α β ks := fun l =>
   (f l).updating ks' (fun k => g k l)
 
-variable {f : L → FiniteMap A B ks} {g : A → L → B} {ks' : List A}
+variable {f : L → FiniteMap α β ks} {g : α → L → β} {ks' : List α}
 
 lemma generalizedUpdate_monotone (hf : Monotone f)
     (hg : ∀ k, Monotone (g k)) : Monotone (generalizedUpdate f g ks') :=
   fun _ _ hl => updating_mono (hf hl) (fun k => hg k hl)
 
-omit [Lattice B] [Lattice L] in
-lemma generalizedUpdate_mem_eq {k : A} {v : B} {l : L} (hk : k ∈ ks')
+omit [Lattice β] [Lattice L] in
+lemma generalizedUpdate_mem_eq {k : α} {v : β} {l : L} (hk : k ∈ ks')
     (h : (k, v) ∈ generalizedUpdate f g ks' l) : v = g k l :=
   eq_of_mem_updating (g := fun k => g k l) hk h
 
-omit [Lattice B] [Lattice L] in
-lemma generalizedUpdate_not_mem_backward {k : A} {v : B} {l : L} (hk : k ∉ ks')
+omit [Lattice β] [Lattice L] in
+lemma generalizedUpdate_not_mem_backward {k : α} {v : β} {l : L} (hk : k ∉ ks')
     (h : (k, v) ∈ generalizedUpdate f g ks' l) : (k, v) ∈ f l :=
   mem_of_mem_updating hk h
 
@@ -143,19 +158,19 @@ end GeneralizedUpdate
 
 section ValuesAt
 
-variable [DecidableEq A]
+variable [DecidableEq α]
 
 /-- The value stored under `k`, if `k` is a key. -/
-private def lookup (fm : FiniteMap A B ks) (k : A) : Option B :=
+private def lookup (fm : FiniteMap α β ks) (k : α) : Option β :=
   if h : k ∈ ks then some (fm ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none
 
 /-- The values stored under the keys `ks'` (skipping any that are not keys). -/
-def valuesAt (fm : FiniteMap A B ks) (ks' : List A) : List B :=
+def valuesAt (fm : FiniteMap α β ks) (ks' : List α) : List β :=
   ks'.filterMap fm.lookup
 
-omit [Lattice B] in
-lemma 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' := by
+omit [Lattice β] in
+lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap α β ks} {k : α} {v : β}
+    {ks' : List α} (hk : k ∈ ks') (h : (k, v) ∈ fm) : v ∈ valuesAt fm ks' := by
   refine List.mem_filterMap.mpr ⟨k, hk, ?_⟩
   obtain ⟨i, hi, rfl⟩ := h
   have hik : ks.get i = k := hi
@@ -167,7 +182,7 @@ lemma mem_valuesAt (hks : ks.Nodup) {fm : FiniteMap A B ks} {k : A} {v : B}
     hks.get_inj_iff.mp (by rw [List.idxOf_get, hi])
   rw [this]
 
-private lemma lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂) (k : A) :
+private lemma lookup_rel {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂) (k : α) :
     Option.Rel (· ≤ ·) (fm₁.lookup k) (fm₂.lookup k) := by
   show Option.Rel _
     (if h : k ∈ ks then some (fm₁ ⟨ks.idxOf k, List.idxOf_lt_length_iff.mpr h⟩) else none)
@@ -176,8 +191,8 @@ private lemma lookup_rel {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂
   · rw [dif_pos hk, dif_pos hk]; exact Option.Rel.some (le_def.mp hle _)
   · rw [dif_neg hk, dif_neg hk]; exact Option.Rel.none
 
-lemma valuesAt_le {fm₁ fm₂ : FiniteMap A B ks} (hle : fm₁ ≤ fm₂)
-    (ks' : List A) :
+lemma valuesAt_le {fm₁ fm₂ : FiniteMap α β ks} (hle : fm₁ ≤ fm₂)
+    (ks' : List α) :
     List.Forall₂ (· ≤ ·) (valuesAt fm₁ ks') (valuesAt fm₂ ks') := by
   induction ks' with
   | nil => exact List.Forall₂.nil

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
-`true`). With the AST-id-keyed lattice these are recovered directly. -/
+/-- The AST node ids marked as definition sites in a `DefSet`. With the
+`Finset`-of-AST-ids lattice these are just the elements of the set. -/
 def defSites (prog : Program) (d : DefSet prog) : List prog.NodeId :=
-  (List.finRange prog.size).filter (fun i => 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