From 80bf039368ad3ded64ded55a685bd77bc20e5987 Mon Sep 17 00:00:00 2001
From: Jacopo Moretti <quartztz@proton.me>
Date: Thu, 6 Aug 2026 17:29:02 +0200
Subject: [PATCH 1/6] feat(CFG): CFG + Kildall with termination

---
 Cslib/Analysis/Dataflow/CFG.lean     |  67 +++++++++++++++++
 Cslib/Analysis/Dataflow/Kildall.lean | 104 +++++++++++++++++++++++++++
 2 files changed, 171 insertions(+)
 create mode 100644 Cslib/Analysis/Dataflow/CFG.lean
 create mode 100644 Cslib/Analysis/Dataflow/Kildall.lean

diff --git a/Cslib/Analysis/Dataflow/CFG.lean b/Cslib/Analysis/Dataflow/CFG.lean
new file mode 100644
index 000000000..4c0dd71d0
--- /dev/null
+++ b/Cslib/Analysis/Dataflow/CFG.lean
@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Jacopo Moretti. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacopo Moretti
+-/
+
+import Cslib.Init
+import Mathlib.Data.Fintype.List
+import Mathlib.Data.DFinsupp.WellFounded
+
+
+/-!
+# Control flow graphs
+
+## Main definitions
+
+- `CFG` is a structure representing Control Flow Graphs on which the dataflow
+  algorithm defined in Kildall.lean runs.
+-/
+
+variable {Node Edge : Type} [DecidableEq Node] [DecidableEq Edge]
+
+class CFG (Node Edge : Type) [DecidableEq Node] [DecidableEq Edge] where
+  /-- All of the nodes in the CFG. -/
+  nodes : List Node
+  /-- All of the edges in the CFG. -/
+  edges : List Edge
+  /-- A distinguished entry node in the CFG. -/
+  entry : Node
+  /-- A proof that the entry node is part of the graph's nodes. -/
+  entry_mem : entry ∈ nodes
+  /-- Extractor function for an edge's source node. -/
+  _srcOf : Edge -> Node
+  /-- Proof of correctness for the source extractor. -/
+  srcOf_mem : ∀ e ∈ edges, _srcOf e ∈ nodes
+  /-- Extractor function for an edge's destination node. -/
+  _dstOf : Edge -> Node
+  /-- Proof of correctness for the destination extractor. -/
+  dstOf_mem : ∀ e ∈ edges, _dstOf e ∈ nodes
+
+abbrev NodeOf (g : CFG Node Edge) : Type := {n // n ∈ g.nodes}
+abbrev EdgeOf (g : CFG Node Edge) : Type := {e // e ∈ g.edges}
+
+namespace CFG
+
+/-- `g.nodes`, presented as `NodeOf g`. -/
+def nodesOf (g : CFG Node Edge) : List (NodeOf g) := g.nodes.attach
+
+def edgesOf (g : CFG Node Edge) : List (EdgeOf g) := g.edges.attach
+
+def dstOf (g : CFG Node Edge) (e : EdgeOf g) : NodeOf g :=
+  ⟨g._dstOf e, g.dstOf_mem e e.property⟩
+
+def srcOf (g : CFG Node Edge) (e : EdgeOf g) : NodeOf g :=
+  ⟨g._srcOf e, g.srcOf_mem e e.property⟩
+
+/-- All in-edges of a given node -/
+def inEdges (g : CFG Node Edge) (n : NodeOf g) : List (EdgeOf g) :=
+  g.edgesOf.filter (g.dstOf · = n)
+
+def succOf (g : CFG Node Edge) (n : NodeOf g) : List (NodeOf g) :=
+  g.nodesOf.filter (fun m => (g.inEdges m).any (g.srcOf · = n))
+
+instance {g : CFG Node Edge} : Fintype (NodeOf g) :=
+  List.Subtype.fintype g.nodes
+
+end CFG
diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean
new file mode 100644
index 000000000..5f072d4cc
--- /dev/null
+++ b/Cslib/Analysis/Dataflow/Kildall.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Jacopo Moretti. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacopo Moretti
+-/
+
+import Cslib.Analysis.Dataflow.CFG
+import Mathlib.Order.Lattice
+import Mathlib.Data.DFinsupp.WellFounded
+
+/-!
+# Forward Worklist dataflow algorithm
+
+Implementation of Kildall's worklist algorithm for solving dataflow equations,
+as described in @Kildall73.
+
+## Main definitions
+
+- `DFState` represents the result of a dataflow analysis algorithm, a mapping
+  between CFG nodes and abstract states
+
+## Main theorems
+
+- Termination of the worklist algorithm
+
+## References
+
+* [G. Kildall, *A Unified Approach to Global Program Optimization*][Kildall73]
+* [R. LaSpina, *Formal Verification of WTO-based Dataflow Solvers*][LaSpina25]
+-/
+
+variable {Node Edge : Type} [DecidableEq Node] [DecidableEq Edge]
+
+/-- The state of a dataflow analysis on graph `g` is a mapping from nodes `n`
+    of `g` to elements of the abstract domain `L`. -/
+abbrev DFState (g : CFG Node Edge) (L : Type) : Type := NodeOf g -> L
+
+namespace DFState
+
+variable {L : Type} [SemilatticeSup L]
+
+/-- The empty dataflow result, a function mapping every node to `⊥`. -/
+def empty {g : CFG Node Edge} [Bot L] : DFState g L := fun _ => ⊥
+
+/-- Update `ρ`'s value at node `n`, to new value `v`. -/
+def update {g : CFG Node Edge} (ρ : DFState g L) (n : NodeOf g) (v : L) : DFState g L :=
+  fun m => if m = n then v else ρ m
+
+/-- Updating `ρ` at `n` with a value smaller than `ρ n` yields a smaller `ρ` -/
+theorem lt_update {g : CFG Node Edge} (ρ : DFState g L) (n : NodeOf g) (v : L) (hlt : ρ n < v) :
+    ρ < ρ.update n v := by
+  rw [Pi.lt_def]
+  refine ⟨fun m => ?_, n, ?_⟩ <;> grind [DFState.update]
+
+end DFState
+
+section Kildall
+
+variable {L : Type} [SemilatticeSup L] [DecidableEq L] [Bot L]
+
+/-- if there's no ascending chains in `L`, there are no ascending chains in `DFState g L` either -/
+instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedGT (DFState g L) :=
+  -- since Mathlib only defines LT wellfoundedness for functions, we need to do some flips
+  inferInstanceAs (WellFoundedLT (NodeOf g → Lᵒᵈ))
+
+/-- Instance of wellfoundedness for the ordering on states. -/
+local instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedRelation (DFState g L) :=
+  ⟨(· > ·), IsWellFounded.wf⟩
+
+-- abstract shape of transfer function
+abbrev Transfer (α L : Type) := α -> L -> L
+
+def joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (s : DFState g L) (n : NodeOf g) : L :=
+  (g.inEdges n).foldl (fun acc e =>
+    let src : NodeOf g := g.srcOf e
+    acc ⊔ eT e (s src)
+  ) ⊥
+
+/-- Kildall's worklist algorithm, propagating updates to the worklist based on new information.
+    The termination proof uses wellfoundedness of · < · on `L`, i.e. the fact that the lattice
+    is of finite height. -/
+def kildall [WellFoundedGT L]
+    (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L)
+    (init : L) (acc : DFState g L := DFState.empty)
+    (wl : List (NodeOf g) := g.nodesOf) : DFState g L :=
+  match wl with
+  | [] => acc
+  | n :: rest =>
+      let newIn := joinPred g eT acc n
+      let newOut := (acc n) ⊔ (nT n newIn)
+      if _h : newOut = (acc n) then
+        kildall g nT eT init acc rest
+      else
+        let acc' := DFState.update acc n newOut
+        let wl' := rest ++ g.succOf n
+        kildall g nT eT init acc' wl'
+termination_by (acc, wl.length)
+decreasing_by
+  · exact Prod.Lex.right acc (by simp)
+  · refine Prod.Lex.left _ _ ?_
+    apply DFState.lt_update
+    apply le_sup_left.lt_of_ne; grind
+
+end Kildall

From d092b6210d70a75a77164ffa944d0b2cdd48a96a Mon Sep 17 00:00:00 2001
From: Jacopo Moretti <quartztz@proton.me>
Date: Fri, 7 Aug 2026 16:28:34 +0200
Subject: [PATCH 2/6] feat(CFG): Correctnesses!

---
 Cslib/Analysis/Dataflow/Kildall.lean | 223 ++++++++++++++++++++++++---
 1 file changed, 202 insertions(+), 21 deletions(-)

diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean
index 5f072d4cc..f6bb04797 100644
--- a/Cslib/Analysis/Dataflow/Kildall.lean
+++ b/Cslib/Analysis/Dataflow/Kildall.lean
@@ -11,21 +11,28 @@ import Mathlib.Data.DFinsupp.WellFounded
 /-!
 # Forward Worklist dataflow algorithm
 
-Implementation of Kildall's worklist algorithm for solving dataflow equations,
-as described in @Kildall73.
+Implementation of Kildall's worklist algorithm for solving dataflow equations, as described in
+@Kildall73. Correctness follows an argument similar to the one found in @Nielson99, with a proof
+technique borrowed from @LaSpina25.
 
 ## Main definitions
 
-- `DFState` represents the result of a dataflow analysis algorithm, a mapping
-  between CFG nodes and abstract states
+- `DFState` represents the result of a dataflow analysis algorithm, a mapping between CFG nodes and
+  abstract states.
+- Definitions of correctness (soundness + completeness) for the analysis result, as `Fixpoint`s over
+  the analysis result `ρ`.
+-
 
 ## Main theorems
 
 - Termination of the worklist algorithm
+- Correctness of the algorithm : computation of a postfixpoint.
+- Correctness of the algorithm : computation of a fixpoint in the monotone transfer case.
 
 ## References
 
 * [G. Kildall, *A Unified Approach to Global Program Optimization*][Kildall73]
+* [F. Nielson, H.R. Nielson, C. Hankin, *Principles of Program Analysis*][Nielson99]
 * [R. LaSpina, *Formal Verification of WTO-based Dataflow Solvers*][LaSpina25]
 -/
 
@@ -40,7 +47,7 @@ namespace DFState
 variable {L : Type} [SemilatticeSup L]
 
 /-- The empty dataflow result, a function mapping every node to `⊥`. -/
-def empty {g : CFG Node Edge} [Bot L] : DFState g L := fun _ => ⊥
+def empty {g : CFG Node Edge} [OrderBot L] : DFState g L := fun _ => ⊥
 
 /-- Update `ρ`'s value at node `n`, to new value `v`. -/
 def update {g : CFG Node Edge} (ρ : DFState g L) (n : NodeOf g) (v : L) : DFState g L :=
@@ -56,7 +63,7 @@ end DFState
 
 section Kildall
 
-variable {L : Type} [SemilatticeSup L] [DecidableEq L] [Bot L]
+variable {L : Type} [SemilatticeSup L] [DecidableEq L] [OrderBot L]
 
 /-- if there's no ascending chains in `L`, there are no ascending chains in `DFState g L` either -/
 instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedGT (DFState g L) :=
@@ -70,35 +77,209 @@ local instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedRelation (DFSt
 -- abstract shape of transfer function
 abbrev Transfer (α L : Type) := α -> L -> L
 
-def joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (s : DFState g L) (n : NodeOf g) : L :=
-  (g.inEdges n).foldl (fun acc e =>
-    let src : NodeOf g := g.srcOf e
-    acc ⊔ eT e (s src)
-  ) ⊥
+def joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L) (ρ : DFState g L)
+    (n : NodeOf g) : L :=
+  (g.inEdges n).foldl (fun acc (e : EdgeOf g) =>
+    acc ⊔ eT e (ρ (g.srcOf e))
+  ) (if n.val = g.entry then init else ⊥)
 
 /-- Kildall's worklist algorithm, propagating updates to the worklist based on new information.
     The termination proof uses wellfoundedness of · < · on `L`, i.e. the fact that the lattice
     is of finite height. -/
 def kildall [WellFoundedGT L]
     (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L)
-    (init : L) (acc : DFState g L := DFState.empty)
+    (init : L) (ρ : DFState g L := DFState.empty)
     (wl : List (NodeOf g) := g.nodesOf) : DFState g L :=
   match wl with
-  | [] => acc
+  | [] => ρ
   | n :: rest =>
-      let newIn := joinPred g eT acc n
-      let newOut := (acc n) ⊔ (nT n newIn)
-      if _h : newOut = (acc n) then
-        kildall g nT eT init acc rest
+      let newIn := joinPred g eT init ρ n
+      let newOut := (ρ n) ⊔ (nT n newIn)
+      if _h : newOut = (ρ n) then
+        kildall g nT eT init ρ rest
       else
-        let acc' := DFState.update acc n newOut
+        let ρ' := DFState.update ρ n newOut
         let wl' := rest ++ g.succOf n
-        kildall g nT eT init acc' wl'
-termination_by (acc, wl.length)
+        kildall g nT eT init ρ' wl'
+termination_by (ρ, wl.length)
 decreasing_by
-  · exact Prod.Lex.right acc (by simp)
+  · exact Prod.Lex.right ρ (by simp)
   · refine Prod.Lex.left _ _ ?_
     apply DFState.lt_update
     apply le_sup_left.lt_of_ne; grind
 
 end Kildall
+
+section Properties
+
+variable {L : Type} [SemilatticeSup L] [WellFoundedGT L] [OrderBot L]
+
+omit [WellFoundedGT L] in
+/-- Updating the abstract state at node `m` doesn't impact the incoming state at node `n` if `m` is
+    not a predecessor of `n`. -/
+lemma joinPred_neq_of_nonpred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L)
+    (ρ : DFState g L) (n m : NodeOf g) (v : L) (hm : n ∉ g.succOf m) :
+    joinPred g eT init (ρ.update m v) n = joinPred g eT init ρ n := by
+  simp only [joinPred]
+  apply List.foldl_ext
+  intro acc e he
+  simp only [DFState.update]
+  split
+  case isFalse hneq => rfl
+  case isTrue heq =>
+    exfalso
+    apply hm
+    simp only [CFG.succOf, CFG.nodesOf, List.mem_filter, List.mem_attach, List.any_eq_true,
+      decide_eq_true_eq, Subtype.exists, true_and]
+    use e, e.property
+
+omit [WellFoundedGT L] in
+/-- Incoming states are monotone when every edge transfer is monotone. -/
+lemma monotone_joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L)
+    (heT : ∀ e, Monotone (eT e)) : Monotone (joinPred g eT init) := by
+  intro ρ₁ ρ₂ hle
+  apply Pi.le_def.2
+  intro n
+  simp only [joinPred]
+  suffices ∀ init₁ init₂, init₁ <= init₂ →
+    List.foldl _ init₁ (g.inEdges n) ≤ List.foldl _ init₂ (g.inEdges n) by
+    apply Std.IsPreorder.le_refl _ |> this _ _
+  induction g.inEdges n with
+  | nil => simp
+  | cons e t ih =>
+    intros i₁ i₂ hlei
+    simp only [List.foldl_cons]
+    refine sup_le_sup hlei ?_ |> ih _ _
+    exact heT e (hle _)
+
+/- To prove properties on this algorithm, we adapt a technique from @LaSpina25 to exploit the
+inductive structure of the algorithm's execution. -/
+
+/-- The result of the worklist algorithm satisfies any invariant preserved through the
+    algorithm's run. -/
+lemma kildall_invariant [DecidableEq L]
+    (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L)
+    (init : L) (ρ : DFState g L) (wl : List (NodeOf g))
+    (P : DFState g L → List (NodeOf g) → Prop)
+    (hinit : P ρ wl)
+    (hstep_same : ∀ {ρ n rest}, P ρ (n :: rest) →
+      let newOut := ρ n ⊔ nT n (joinPred g eT init ρ n)
+      newOut = ρ n →
+        P ρ rest)
+    (hstep_changed : ∀ {ρ n rest}, P ρ (n :: rest) →
+      let newOut := ρ n ⊔ nT n (joinPred g eT init ρ n)
+      newOut ≠ ρ n →
+        P (ρ.update n newOut) (rest ++ g.succOf n)) :
+      P (kildall g nT eT init ρ wl) [] := by
+  induction ρ, wl using kildall.induct g nT eT init with
+  | case1 o => simpa [kildall]
+  | case2 acc n rest nin nout heq ih =>
+      simp only [kildall, dite_eq_ite]
+      rw [if_pos heq]
+      exact ih (hstep_same hinit heq)
+  | case3 acc n r nin nout hnout acc' wl' ih =>
+      simp only [kildall, dite_eq_ite]
+      rw [if_neg hnout]
+      exact ih (hstep_changed hinit hnout)
+
+/-- An analysis result `ρ` on `g` is a postfixpoint if, at every node of `g`, computing the
+    transfers of the incoming facts remains within the outgoing facts. -/
+def ForwardPostFixpoint
+    (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
+    (ρ : DFState g L) (wl : List (NodeOf g)) : Prop :=
+  ∀ n ∉ wl, nT n (joinPred g eT init ρ n) ≤ ρ n
+
+/-- An analysis result `ρ` on `g` is a fixpoint if, at every node of `g`, the `ForwardPostFixpoint`
+    bound is tight. -/
+def ForwardFixpoint
+    (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
+    (ρ : DFState g L) (wl : List (NodeOf g)) : Prop :=
+  ∀ n ∉ wl, nT n (joinPred g eT init ρ n) = ρ n
+
+/-- The result of the worklist algorithm is a `ForwardPostfixpoint`. -/
+theorem kildall_forwardPostFixpoint [DecidableEq L] (g : CFG Node Edge)
+    (nT : Transfer Node L) (eT : Transfer Edge L) (init : L) (ρ : DFState g L)
+    (wl : List (NodeOf g))
+    (hinv0 : ∀ m : NodeOf g, m ∉ wl → nT m (joinPred g eT init ρ m) ≤ ρ m) :
+    let res := kildall g nT eT init ρ wl
+    ForwardPostFixpoint g nT eT init res [] := by
+  refine kildall_invariant g nT eT init ρ wl (ForwardPostFixpoint g nT eT init) ?_ ?_ ?_
+  · exact hinv0
+  · intro ρ n rest hfp newOut heq m hm
+    by_cases hmn : m = n
+    · subst m
+      exact le_sup_right.trans_eq heq
+    · exact hfp m (by simp_all)
+  · intro ρ n rest hfp newOut hnout m hm
+    have hsucc : m ∉ g.succOf n := fun hin => (List.mem_append_right _ hin) |> hm
+    rw [joinPred_neq_of_nonpred g eT init ρ m n newOut hsucc, DFState.update]
+    split -- m ?= n
+    case isTrue heq =>
+      grind [le_sup_right]
+    case isFalse hneq =>
+      apply hfp; grind
+
+/-- An analysis result `ρ` on `g` is a prefixpoint if every outgoing fact remains within the
+    result of transferring its incoming facts. -/
+def ForwardPreFixpoint (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
+    (ρ : DFState g L) : Prop :=
+  ∀ n, ρ n ≤ nT n (joinPred g eT init ρ n)
+
+/-- The worklist algorithm preserves forward pre-fixpoints when all transfers are monotone. -/
+lemma kildall_forwardPreFixpoint [DecidableEq L] (g : CFG Node Edge)
+    (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
+    (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
+    (init : L) (ρ : DFState g L) (wl : List (NodeOf g))
+    (hinv0 : ForwardPreFixpoint g nT eT init ρ) :
+    let res := kildall g nT eT init ρ wl
+    ForwardPreFixpoint g nT eT init res := by
+  refine kildall_invariant g nT eT init ρ wl
+    (fun ρ _ => ForwardPreFixpoint g nT eT init ρ) hinv0 ?_ ?_
+  · exact fun hfp _ => hfp
+  · intro ρ n rest hfp newOut hnout m
+    have hle : ρ ≤ ρ.update n newOut := by
+      intro k
+      simp only [DFState.update]
+      split <;> grind [le_refl, le_sup_left]
+    have htransfer : nT m (joinPred g eT init ρ m) ≤
+        nT m (joinPred g eT init (ρ.update n newOut) m) :=
+      hnT m (monotone_joinPred g eT init heT hle m)
+    grind [DFState.update, sup_le, hfp m]
+
+/-- If the transfer functions are monotone, the result of the worklist algorithm is a
+    `ForwardFixpoint`. -/
+theorem kildall_forwardFixpoint [DecidableEq L] (g : CFG Node Edge)
+    (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
+    (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
+    (init : L) (ρ : DFState g L) (wl : List (NodeOf g))
+    (hpost0 : ∀ m ∉ wl, nT m (joinPred g eT init ρ m) ≤ ρ m)
+    (hpre0 : ForwardPreFixpoint g nT eT init ρ) :
+    let res := kildall g nT eT init ρ wl
+    ForwardFixpoint g nT eT init res [] := by
+  intro res
+  have hpost : ForwardPostFixpoint g nT eT init res [] :=
+    kildall_forwardPostFixpoint g nT eT init ρ wl hpost0
+  have hpre : ForwardPreFixpoint g nT eT init res :=
+    kildall_forwardPreFixpoint g nT hnT eT heT init ρ wl hpre0
+  intro n hn
+  exact le_antisymm (hpost n hn) (hpre n)
+
+/-- Final theorem: the result of a full run of the algorithm with the default arguments is the least
+    fixpoint of the equations induced by the transfer functions and the initial state. -/
+theorem kildall_correct [DecidableEq L] (g : CFG Node Edge)
+    (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
+    (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
+    (init : L) :
+    let res := kildall g nT eT init
+    ForwardFixpoint g nT eT init res [] := by
+  apply kildall_forwardFixpoint g nT hnT eT heT init DFState.empty g.nodesOf
+  case hpost0 => -- ≤
+    -- `∀ m ∉ g.nodesOf, ...`
+    -- since every `m` is in `g.nodesOf` this is vacuously true
+    grind [CFG.nodesOf]
+  case hpre0 => -- ≥
+    -- `∀ m ∈ g.nodesOf, DFState.empty m ≤ ...`
+    -- since `DFState.empty` is `λ _. ⊥`, it's ≤ anything, thanks to `OrderBot`.
+    simp [ForwardPreFixpoint, DFState.empty]
+
+end Properties

From f9581735f26f61ae7581f34b2cd01723e8202e49 Mon Sep 17 00:00:00 2001
From: Jacopo Moretti <quartztz@proton.me>
Date: Fri, 7 Aug 2026 16:28:43 +0200
Subject: [PATCH 3/6] chore(CFG): cleanup

---
 Cslib/Analysis/Dataflow/CFG.lean     | 4 ++--
 Cslib/Analysis/Dataflow/Kildall.lean | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Analysis/Dataflow/CFG.lean b/Cslib/Analysis/Dataflow/CFG.lean
index 4c0dd71d0..7eb85bcc7 100644
--- a/Cslib/Analysis/Dataflow/CFG.lean
+++ b/Cslib/Analysis/Dataflow/CFG.lean
@@ -30,11 +30,11 @@ class CFG (Node Edge : Type) [DecidableEq Node] [DecidableEq Edge] where
   /-- A proof that the entry node is part of the graph's nodes. -/
   entry_mem : entry ∈ nodes
   /-- Extractor function for an edge's source node. -/
-  _srcOf : Edge -> Node
+  _srcOf : Edge → Node
   /-- Proof of correctness for the source extractor. -/
   srcOf_mem : ∀ e ∈ edges, _srcOf e ∈ nodes
   /-- Extractor function for an edge's destination node. -/
-  _dstOf : Edge -> Node
+  _dstOf : Edge → Node
   /-- Proof of correctness for the destination extractor. -/
   dstOf_mem : ∀ e ∈ edges, _dstOf e ∈ nodes
 
diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean
index f6bb04797..1bcd59ef7 100644
--- a/Cslib/Analysis/Dataflow/Kildall.lean
+++ b/Cslib/Analysis/Dataflow/Kildall.lean
@@ -40,7 +40,7 @@ variable {Node Edge : Type} [DecidableEq Node] [DecidableEq Edge]
 
 /-- The state of a dataflow analysis on graph `g` is a mapping from nodes `n`
     of `g` to elements of the abstract domain `L`. -/
-abbrev DFState (g : CFG Node Edge) (L : Type) : Type := NodeOf g -> L
+abbrev DFState (g : CFG Node Edge) (L : Type) : Type := NodeOf g → L
 
 namespace DFState
 
@@ -75,7 +75,7 @@ local instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedRelation (DFSt
   ⟨(· > ·), IsWellFounded.wf⟩
 
 -- abstract shape of transfer function
-abbrev Transfer (α L : Type) := α -> L -> L
+abbrev Transfer (α L : Type) := α → L → L
 
 def joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L) (ρ : DFState g L)
     (n : NodeOf g) : L :=

From ccd675c8a8b51ec75cfdae1c21803043b32c4e4d Mon Sep 17 00:00:00 2001
From: Jacopo Moretti <quartztz@proton.me>
Date: Fri, 7 Aug 2026 17:11:56 +0200
Subject: [PATCH 4/6] chore(CFG): refactor

---
 Cslib/Analysis/Dataflow/CFG.lean     |   3 +-
 Cslib/Analysis/Dataflow/Kildall.lean | 159 ++++++++++++++-------------
 2 files changed, 83 insertions(+), 79 deletions(-)

diff --git a/Cslib/Analysis/Dataflow/CFG.lean b/Cslib/Analysis/Dataflow/CFG.lean
index 7eb85bcc7..cd14816ae 100644
--- a/Cslib/Analysis/Dataflow/CFG.lean
+++ b/Cslib/Analysis/Dataflow/CFG.lean
@@ -15,11 +15,12 @@ import Mathlib.Data.DFinsupp.WellFounded
 ## Main definitions
 
 - `CFG` is a structure representing Control Flow Graphs on which the dataflow
-  algorithm defined in Kildall.lean runs.
+  algorithm defined in `Kildall.lean` runs.
 -/
 
 variable {Node Edge : Type} [DecidableEq Node] [DecidableEq Edge]
 
+/-- Abstract structure defining the necessary operations on a CFG to define a Control Flow Graph. -/
 class CFG (Node Edge : Type) [DecidableEq Node] [DecidableEq Edge] where
   /-- All of the nodes in the CFG. -/
   nodes : List Node
diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean
index 1bcd59ef7..d8d43e61f 100644
--- a/Cslib/Analysis/Dataflow/Kildall.lean
+++ b/Cslib/Analysis/Dataflow/Kildall.lean
@@ -26,8 +26,9 @@ technique borrowed from @LaSpina25.
 ## Main theorems
 
 - Termination of the worklist algorithm
-- Correctness of the algorithm : computation of a postfixpoint.
-- Correctness of the algorithm : computation of a fixpoint in the monotone transfer case.
+- Correctness of the algorithm : The algorithm computes a postfixpoint.
+- Correctness of the algorithm : The algorithm computes a fixpoint if the transfer functions are
+  monotone.
 
 ## References
 
@@ -49,11 +50,11 @@ variable {L : Type} [SemilatticeSup L]
 /-- The empty dataflow result, a function mapping every node to `⊥`. -/
 def empty {g : CFG Node Edge} [OrderBot L] : DFState g L := fun _ => ⊥
 
-/-- Update `ρ`'s value at node `n`, to new value `v`. -/
+/-- Update the value of `ρ` at node `n`, to new value `v`. -/
 def update {g : CFG Node Edge} (ρ : DFState g L) (n : NodeOf g) (v : L) : DFState g L :=
   fun m => if m = n then v else ρ m
 
-/-- Updating `ρ` at `n` with a value smaller than `ρ n` yields a smaller `ρ` -/
+/-- Updating `ρ` at `n` with a value bigger than `ρ n` yields a bigger `ρ` -/
 theorem lt_update {g : CFG Node Edge} (ρ : DFState g L) (n : NodeOf g) (v : L) (hlt : ρ n < v) :
     ρ < ρ.update n v := by
   rw [Pi.lt_def]
@@ -64,20 +65,21 @@ end DFState
 section Kildall
 
 variable {L : Type} [SemilatticeSup L] [DecidableEq L] [OrderBot L]
+variable {g : CFG Node Edge}
 
-/-- if there's no ascending chains in `L`, there are no ascending chains in `DFState g L` either -/
-instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedGT (DFState g L) :=
+/-- If there's no ascending chains in `L`, there are no ascending chains in `DFState g L` either -/
+local instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedGT (DFState g L) :=
   -- since Mathlib only defines LT wellfoundedness for functions, we need to do some flips
   inferInstanceAs (WellFoundedLT (NodeOf g → Lᵒᵈ))
 
-/-- Instance of wellfoundedness for the ordering on states. -/
+/-- Wellfoundedness of state ordering based on WellFoundedGT. -/
 local instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedRelation (DFState g L) :=
   ⟨(· > ·), IsWellFounded.wf⟩
 
--- abstract shape of transfer function
+/-- The type of a transfer function over α. -/
 abbrev Transfer (α L : Type) := α → L → L
 
-def joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L) (ρ : DFState g L)
+def joinPred {g : CFG Node Edge} (eT : Transfer Edge L) (init : L) (ρ : DFState g L)
     (n : NodeOf g) : L :=
   (g.inEdges n).foldl (fun acc (e : EdgeOf g) =>
     acc ⊔ eT e (ρ (g.srcOf e))
@@ -86,21 +88,22 @@ def joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L) (ρ : DFState
 /-- Kildall's worklist algorithm, propagating updates to the worklist based on new information.
     The termination proof uses wellfoundedness of · < · on `L`, i.e. the fact that the lattice
     is of finite height. -/
-def kildall [WellFoundedGT L]
-    (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L)
+@[simp]
+def kildall [WellFoundedGT L] {g : CFG Node Edge}
+    (nT : Transfer Node L) (eT : Transfer Edge L)
     (init : L) (ρ : DFState g L := DFState.empty)
     (wl : List (NodeOf g) := g.nodesOf) : DFState g L :=
   match wl with
   | [] => ρ
   | n :: rest =>
-      let newIn := joinPred g eT init ρ n
+      let newIn := joinPred eT init ρ n
       let newOut := (ρ n) ⊔ (nT n newIn)
       if _h : newOut = (ρ n) then
-        kildall g nT eT init ρ rest
+        kildall nT eT init ρ rest
       else
         let ρ' := DFState.update ρ n newOut
         let wl' := rest ++ g.succOf n
-        kildall g nT eT init ρ' wl'
+        kildall nT eT init ρ' wl'
 termination_by (ρ, wl.length)
 decreasing_by
   · exact Prod.Lex.right ρ (by simp)
@@ -110,16 +113,39 @@ decreasing_by
 
 end Kildall
 
-section Properties
-
+-- Our analysis lattice.
 variable {L : Type} [SemilatticeSup L] [WellFoundedGT L] [OrderBot L]
 
+/- ### Definitions -/
+
+/-- An analysis result `ρ` on `g` is a postfixpoint if, at every node of `g`, computing the
+    transfers of the incoming facts remains within the outgoing facts. -/
+def ForwardPostFixpoint
+    {g : CFG Node Edge} (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
+    (ρ : DFState g L) (wl : List (NodeOf g)) : Prop :=
+  ∀ n ∉ wl, nT n (joinPred eT init ρ n) ≤ ρ n
+
+/-- An analysis result `ρ` on `g` is a fixpoint if, at every node of `g`, the `ForwardPostFixpoint`
+    bound is tight. -/
+def ForwardFixpoint
+    {g : CFG Node Edge} (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
+    (ρ : DFState g L) (wl : List (NodeOf g)) : Prop :=
+  ∀ n ∉ wl, nT n (joinPred eT init ρ n) = ρ n
+
+/-- An analysis result `ρ` on `g` is a prefixpoint if every outgoing fact remains within the
+    result of transferring its incoming facts. -/
+def ForwardPreFixpoint {g : CFG Node Edge} (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
+    (ρ : DFState g L) : Prop :=
+  ∀ n, ρ n ≤ nT n (joinPred eT init ρ n)
+
+/- ### Helpers -/
+
 omit [WellFoundedGT L] in
 /-- Updating the abstract state at node `m` doesn't impact the incoming state at node `n` if `m` is
     not a predecessor of `n`. -/
-lemma joinPred_neq_of_nonpred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L)
+lemma joinPred_neq_of_nonpred {g : CFG Node Edge} (eT : Transfer Edge L) (init : L)
     (ρ : DFState g L) (n m : NodeOf g) (v : L) (hm : n ∉ g.succOf m) :
-    joinPred g eT init (ρ.update m v) n = joinPred g eT init ρ n := by
+    joinPred eT init (ρ.update m v) n = joinPred eT init ρ n := by
   simp only [joinPred]
   apply List.foldl_ext
   intro acc e he
@@ -135,8 +161,8 @@ lemma joinPred_neq_of_nonpred (g : CFG Node Edge) (eT : Transfer Edge L) (init :
 
 omit [WellFoundedGT L] in
 /-- Incoming states are monotone when every edge transfer is monotone. -/
-lemma monotone_joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L)
-    (heT : ∀ e, Monotone (eT e)) : Monotone (joinPred g eT init) := by
+lemma monotone_joinPred {g : CFG Node Edge} (eT : Transfer Edge L) (init : L)
+    (heT : ∀ e, Monotone (eT e)) : Monotone (joinPred (g := g) eT init) := by
   intro ρ₁ ρ₂ hle
   apply Pi.le_def.2
   intro n
@@ -152,27 +178,24 @@ lemma monotone_joinPred (g : CFG Node Edge) (eT : Transfer Edge L) (init : L)
     refine sup_le_sup hlei ?_ |> ih _ _
     exact heT e (hle _)
 
-/- To prove properties on this algorithm, we adapt a technique from @LaSpina25 to exploit the
-inductive structure of the algorithm's execution. -/
-
 /-- The result of the worklist algorithm satisfies any invariant preserved through the
-    algorithm's run. -/
+    algorithm's run. Technique borrowed from @LaSpina25 -/
 lemma kildall_invariant [DecidableEq L]
-    (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L)
+    {g : CFG Node Edge} (nT : Transfer Node L) (eT : Transfer Edge L)
     (init : L) (ρ : DFState g L) (wl : List (NodeOf g))
     (P : DFState g L → List (NodeOf g) → Prop)
     (hinit : P ρ wl)
     (hstep_same : ∀ {ρ n rest}, P ρ (n :: rest) →
-      let newOut := ρ n ⊔ nT n (joinPred g eT init ρ n)
+      let newOut := ρ n ⊔ nT n (joinPred eT init ρ n)
       newOut = ρ n →
         P ρ rest)
     (hstep_changed : ∀ {ρ n rest}, P ρ (n :: rest) →
-      let newOut := ρ n ⊔ nT n (joinPred g eT init ρ n)
+      let newOut := ρ n ⊔ nT n (joinPred eT init ρ n)
       newOut ≠ ρ n →
         P (ρ.update n newOut) (rest ++ g.succOf n)) :
-      P (kildall g nT eT init ρ wl) [] := by
-  induction ρ, wl using kildall.induct g nT eT init with
-  | case1 o => simpa [kildall]
+      P (kildall nT eT init ρ wl) [] := by
+  induction ρ, wl using kildall.induct nT eT init with
+  | case1 o => simpa
   | case2 acc n rest nin nout heq ih =>
       simp only [kildall, dite_eq_ite]
       rw [if_pos heq]
@@ -182,28 +205,16 @@ lemma kildall_invariant [DecidableEq L]
       rw [if_neg hnout]
       exact ih (hstep_changed hinit hnout)
 
-/-- An analysis result `ρ` on `g` is a postfixpoint if, at every node of `g`, computing the
-    transfers of the incoming facts remains within the outgoing facts. -/
-def ForwardPostFixpoint
-    (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
-    (ρ : DFState g L) (wl : List (NodeOf g)) : Prop :=
-  ∀ n ∉ wl, nT n (joinPred g eT init ρ n) ≤ ρ n
-
-/-- An analysis result `ρ` on `g` is a fixpoint if, at every node of `g`, the `ForwardPostFixpoint`
-    bound is tight. -/
-def ForwardFixpoint
-    (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
-    (ρ : DFState g L) (wl : List (NodeOf g)) : Prop :=
-  ∀ n ∉ wl, nT n (joinPred g eT init ρ n) = ρ n
+/- ### Theorems -/
 
 /-- The result of the worklist algorithm is a `ForwardPostfixpoint`. -/
-theorem kildall_forwardPostFixpoint [DecidableEq L] (g : CFG Node Edge)
+theorem kildall_forwardPostFixpoint [DecidableEq L] {g : CFG Node Edge}
     (nT : Transfer Node L) (eT : Transfer Edge L) (init : L) (ρ : DFState g L)
     (wl : List (NodeOf g))
-    (hinv0 : ∀ m : NodeOf g, m ∉ wl → nT m (joinPred g eT init ρ m) ≤ ρ m) :
-    let res := kildall g nT eT init ρ wl
-    ForwardPostFixpoint g nT eT init res [] := by
-  refine kildall_invariant g nT eT init ρ wl (ForwardPostFixpoint g nT eT init) ?_ ?_ ?_
+    (hinv0 : ∀ m : NodeOf g, m ∉ wl → nT m (joinPred eT init ρ m) ≤ ρ m) :
+    let res := kildall nT eT init ρ wl
+    ForwardPostFixpoint nT eT init res [] := by
+  refine kildall_invariant nT eT init ρ wl (ForwardPostFixpoint nT eT init) ?_ ?_ ?_
   · exact hinv0
   · intro ρ n rest hfp newOut heq m hm
     by_cases hmn : m = n
@@ -212,55 +223,49 @@ theorem kildall_forwardPostFixpoint [DecidableEq L] (g : CFG Node Edge)
     · exact hfp m (by simp_all)
   · intro ρ n rest hfp newOut hnout m hm
     have hsucc : m ∉ g.succOf n := fun hin => (List.mem_append_right _ hin) |> hm
-    rw [joinPred_neq_of_nonpred g eT init ρ m n newOut hsucc, DFState.update]
+    rw [joinPred_neq_of_nonpred eT init ρ m n newOut hsucc, DFState.update]
     split -- m ?= n
     case isTrue heq =>
       grind [le_sup_right]
     case isFalse hneq =>
       apply hfp; grind
 
-/-- An analysis result `ρ` on `g` is a prefixpoint if every outgoing fact remains within the
-    result of transferring its incoming facts. -/
-def ForwardPreFixpoint (g : CFG Node Edge) (nT : Transfer Node L) (eT : Transfer Edge L) (init : L)
-    (ρ : DFState g L) : Prop :=
-  ∀ n, ρ n ≤ nT n (joinPred g eT init ρ n)
-
 /-- The worklist algorithm preserves forward pre-fixpoints when all transfers are monotone. -/
-lemma kildall_forwardPreFixpoint [DecidableEq L] (g : CFG Node Edge)
+lemma kildall_forwardPreFixpoint [DecidableEq L] {g : CFG Node Edge}
     (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
     (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
     (init : L) (ρ : DFState g L) (wl : List (NodeOf g))
-    (hinv0 : ForwardPreFixpoint g nT eT init ρ) :
-    let res := kildall g nT eT init ρ wl
-    ForwardPreFixpoint g nT eT init res := by
-  refine kildall_invariant g nT eT init ρ wl
-    (fun ρ _ => ForwardPreFixpoint g nT eT init ρ) hinv0 ?_ ?_
+    (hinv0 : ForwardPreFixpoint nT eT init ρ) :
+    let res := kildall nT eT init ρ wl
+    ForwardPreFixpoint nT eT init res := by
+  refine kildall_invariant nT eT init ρ wl
+    (fun ρ _ => ForwardPreFixpoint nT eT init ρ) hinv0 ?_ ?_
   · exact fun hfp _ => hfp
   · intro ρ n rest hfp newOut hnout m
     have hle : ρ ≤ ρ.update n newOut := by
       intro k
       simp only [DFState.update]
       split <;> grind [le_refl, le_sup_left]
-    have htransfer : nT m (joinPred g eT init ρ m) ≤
-        nT m (joinPred g eT init (ρ.update n newOut) m) :=
-      hnT m (monotone_joinPred g eT init heT hle m)
+    have htransfer : nT m (joinPred eT init ρ m) ≤
+        nT m (joinPred eT init (ρ.update n newOut) m) :=
+      hnT m (monotone_joinPred eT init heT hle m)
     grind [DFState.update, sup_le, hfp m]
 
 /-- If the transfer functions are monotone, the result of the worklist algorithm is a
     `ForwardFixpoint`. -/
-theorem kildall_forwardFixpoint [DecidableEq L] (g : CFG Node Edge)
+theorem kildall_forwardFixpoint [DecidableEq L] {g : CFG Node Edge}
     (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
     (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
     (init : L) (ρ : DFState g L) (wl : List (NodeOf g))
-    (hpost0 : ∀ m ∉ wl, nT m (joinPred g eT init ρ m) ≤ ρ m)
-    (hpre0 : ForwardPreFixpoint g nT eT init ρ) :
-    let res := kildall g nT eT init ρ wl
-    ForwardFixpoint g nT eT init res [] := by
+    (hpost0 : ∀ m ∉ wl, nT m (joinPred eT init ρ m) ≤ ρ m)
+    (hpre0 : ForwardPreFixpoint nT eT init ρ) :
+    let res := kildall nT eT init ρ wl
+    ForwardFixpoint nT eT init res [] := by
   intro res
-  have hpost : ForwardPostFixpoint g nT eT init res [] :=
-    kildall_forwardPostFixpoint g nT eT init ρ wl hpost0
-  have hpre : ForwardPreFixpoint g nT eT init res :=
-    kildall_forwardPreFixpoint g nT hnT eT heT init ρ wl hpre0
+  have hpost :=
+    kildall_forwardPostFixpoint nT eT init ρ wl hpost0
+  have hpre :=
+    kildall_forwardPreFixpoint nT hnT eT heT init ρ wl hpre0
   intro n hn
   exact le_antisymm (hpost n hn) (hpre n)
 
@@ -270,9 +275,9 @@ theorem kildall_correct [DecidableEq L] (g : CFG Node Edge)
     (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
     (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
     (init : L) :
-    let res := kildall g nT eT init
-    ForwardFixpoint g nT eT init res [] := by
-  apply kildall_forwardFixpoint g nT hnT eT heT init DFState.empty g.nodesOf
+    let res := kildall (g := g) nT eT init
+    ForwardFixpoint (g := g) nT eT init res [] := by
+  apply kildall_forwardFixpoint nT hnT eT heT init DFState.empty g.nodesOf
   case hpost0 => -- ≤
     -- `∀ m ∉ g.nodesOf, ...`
     -- since every `m` is in `g.nodesOf` this is vacuously true
@@ -281,5 +286,3 @@ theorem kildall_correct [DecidableEq L] (g : CFG Node Edge)
     -- `∀ m ∈ g.nodesOf, DFState.empty m ≤ ...`
     -- since `DFState.empty` is `λ _. ⊥`, it's ≤ anything, thanks to `OrderBot`.
     simp [ForwardPreFixpoint, DFState.empty]
-
-end Properties

From b6969dbe351ad0f936c58a06f7058d8f71c944e4 Mon Sep 17 00:00:00 2001
From: Jacopo Moretti <quartztz@proton.me>
Date: Fri, 7 Aug 2026 17:58:43 +0200
Subject: [PATCH 5/6] feat(CFG): add minimality

---
 Cslib/Analysis/Dataflow/Kildall.lean | 67 ++++++++++++++++++++++------
 1 file changed, 54 insertions(+), 13 deletions(-)

diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean
index d8d43e61f..dad755b7b 100644
--- a/Cslib/Analysis/Dataflow/Kildall.lean
+++ b/Cslib/Analysis/Dataflow/Kildall.lean
@@ -21,12 +21,13 @@ technique borrowed from @LaSpina25.
   abstract states.
 - Definitions of correctness (soundness + completeness) for the analysis result, as `Fixpoint`s over
   the analysis result `ρ`.
--
 
 ## Main theorems
 
 - Termination of the worklist algorithm
 - Correctness of the algorithm : The algorithm computes a postfixpoint.
+- Minimality of the algorithm : The algorithm computes the least solution if the transfer functions
+  are monotone.
 - Correctness of the algorithm : The algorithm computes a fixpoint if the transfer functions are
   monotone.
 
@@ -207,8 +208,9 @@ lemma kildall_invariant [DecidableEq L]
 
 /- ### Theorems -/
 
-/-- The result of the worklist algorithm is a `ForwardPostfixpoint`. -/
-theorem kildall_forwardPostFixpoint [DecidableEq L] {g : CFG Node Edge}
+/-- The result of the worklist algorithm on appropriate intermediate state is a
+    `ForwardPostFixpoint`. -/
+theorem kildall_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG Node Edge}
     (nT : Transfer Node L) (eT : Transfer Edge L) (init : L) (ρ : DFState g L)
     (wl : List (NodeOf g))
     (hinv0 : ∀ m : NodeOf g, m ∉ wl → nT m (joinPred eT init ρ m) ≤ ρ m) :
@@ -230,8 +232,29 @@ theorem kildall_forwardPostFixpoint [DecidableEq L] {g : CFG Node Edge}
     case isFalse hneq =>
       apply hfp; grind
 
+/-- The result of the worklist algorithm on appropriate intermediate state is the least
+    `ForwardPostFixpoint`. -/
+theorem kildall_least_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG Node Edge}
+    (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
+    (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
+    (init : L) (ρ σ : DFState g L) (wl : List (NodeOf g))
+    (hρ : ρ ≤ σ) (hσ : ForwardPostFixpoint nT eT init σ []) :
+    kildall nT eT init ρ wl ≤ σ := by
+  refine kildall_invariant nT eT init ρ wl
+    (fun ρ _ => ρ ≤ σ) hρ ?_ ?_
+  · exact fun hle _ => hle
+  · intro ρ n rest hle newOut hnout m
+    simp only [DFState.update]
+    split
+    case isTrue heq =>
+      subst m
+      apply sup_le (hle n)
+      refine (hnT n (monotone_joinPred eT init heT hle n)).trans ?_
+      apply hσ n (by simp)
+    case isFalse hneq => exact hle m
+
 /-- The worklist algorithm preserves forward pre-fixpoints when all transfers are monotone. -/
-lemma kildall_forwardPreFixpoint [DecidableEq L] {g : CFG Node Edge}
+lemma kildall_forwardPreFixpoint_of_init [DecidableEq L] {g : CFG Node Edge}
     (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
     (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
     (init : L) (ρ : DFState g L) (wl : List (NodeOf g))
@@ -251,9 +274,9 @@ lemma kildall_forwardPreFixpoint [DecidableEq L] {g : CFG Node Edge}
       hnT m (monotone_joinPred eT init heT hle m)
     grind [DFState.update, sup_le, hfp m]
 
-/-- If the transfer functions are monotone, the result of the worklist algorithm is a
-    `ForwardFixpoint`. -/
-theorem kildall_forwardFixpoint [DecidableEq L] {g : CFG Node Edge}
+/-- If the transfer functions are monotone, the result of the worklist algorithm on appropriate
+    intermediate state is a `ForwardFixpoint`. -/
+theorem kildall_forwardFixpoint_of_init [DecidableEq L] {g : CFG Node Edge}
     (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
     (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
     (init : L) (ρ : DFState g L) (wl : List (NodeOf g))
@@ -263,21 +286,39 @@ theorem kildall_forwardFixpoint [DecidableEq L] {g : CFG Node Edge}
     ForwardFixpoint nT eT init res [] := by
   intro res
   have hpost :=
-    kildall_forwardPostFixpoint nT eT init ρ wl hpost0
+    kildall_forwardPostFixpoint_of_init nT eT init ρ wl hpost0
   have hpre :=
-    kildall_forwardPreFixpoint nT hnT eT heT init ρ wl hpre0
+    kildall_forwardPreFixpoint_of_init nT hnT eT heT init ρ wl hpre0
   intro n hn
   exact le_antisymm (hpost n hn) (hpre n)
 
-/-- Final theorem: the result of a full run of the algorithm with the default arguments is the least
-    fixpoint of the equations induced by the transfer functions and the initial state. -/
-theorem kildall_correct [DecidableEq L] (g : CFG Node Edge)
+/-- Running Kildall's algorithm yields a postfixpoint of the forward dataflow constraints. -/
+theorem kildall_forwardPostFixpoint [DecidableEq L] (g : CFG Node Edge)
+    (nT : Transfer Node L) (eT : Transfer Edge L) (init : L) :
+    let res := kildall (g := g) nT eT init
+    ForwardPostFixpoint (g := g) nT eT init res [] := by
+  apply kildall_forwardPostFixpoint_of_init nT eT init
+  -- `∀ m ∉ g.nodesOf, ...`
+  -- since every `m` is in `g.nodesOf` this is vacuously true
+  grind [CFG.nodesOf]
+
+theorem kildall_least_forwardPostFixpoint [DecidableEq L] (g : CFG Node Edge)
+    (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
+    (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
+    (init : L) (σ : DFState g L) (hfpf : ForwardPostFixpoint nT eT init σ []) :
+    kildall (g := g) nT eT init ≤ σ := by
+  apply kildall_least_forwardPostFixpoint_of_init nT hnT eT heT init DFState.empty σ g.nodesOf
+    <;> simp [Pi.le_def, DFState.empty, hfpf]
+
+/-- If all transfer functions are monotone, running Kildall's algorithm yields a fixpoint of the
+     forward dataflow equations. -/
+theorem kildall_forwardFixpoint [DecidableEq L] (g : CFG Node Edge)
     (nT : Transfer Node L) (hnT : ∀ n, Monotone (nT n))
     (eT : Transfer Edge L) (heT : ∀ e, Monotone (eT e))
     (init : L) :
     let res := kildall (g := g) nT eT init
     ForwardFixpoint (g := g) nT eT init res [] := by
-  apply kildall_forwardFixpoint nT hnT eT heT init DFState.empty g.nodesOf
+  apply kildall_forwardFixpoint_of_init nT hnT eT heT init DFState.empty g.nodesOf
   case hpost0 => -- ≤
     -- `∀ m ∉ g.nodesOf, ...`
     -- since every `m` is in `g.nodesOf` this is vacuously true

From 85af5c0e710b7f9a5f9bce7e6e98dc2da61547d1 Mon Sep 17 00:00:00 2001
From: Jacopo Moretti <quartztz@proton.me>
Date: Fri, 7 Aug 2026 20:04:11 +0200
Subject: [PATCH 6/6] chore(CFG): fix lints

---
 Cslib.lean                           |  2 ++
 Cslib/Analysis/Dataflow/CFG.lean     | 10 +++++++---
 Cslib/Analysis/Dataflow/Kildall.lean | 10 +++++++---
 3 files changed, 16 insertions(+), 6 deletions(-)

diff --git a/Cslib.lean b/Cslib.lean
index d74457919..79e8f3142 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -2,6 +2,8 @@ module  -- shake: keep-all --deprecated_module: ignore
 
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.Analysis.Dataflow.CFG
+public import Cslib.Analysis.Dataflow.Kildall
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
 public import Cslib.Computability.Automata.DA.Basic
diff --git a/Cslib/Analysis/Dataflow/CFG.lean b/Cslib/Analysis/Dataflow/CFG.lean
index cd14816ae..97093a528 100644
--- a/Cslib/Analysis/Dataflow/CFG.lean
+++ b/Cslib/Analysis/Dataflow/CFG.lean
@@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jacopo Moretti
 -/
 
-import Cslib.Init
-import Mathlib.Data.Fintype.List
-import Mathlib.Data.DFinsupp.WellFounded
+module
+
+public import Cslib.Init
+public import Mathlib.Data.Fintype.List
+public import Mathlib.Data.DFinsupp.WellFounded
 
 
 /-!
@@ -18,6 +20,8 @@ import Mathlib.Data.DFinsupp.WellFounded
   algorithm defined in `Kildall.lean` runs.
 -/
 
+@[expose] public section
+
 variable {Node Edge : Type} [DecidableEq Node] [DecidableEq Edge]
 
 /-- Abstract structure defining the necessary operations on a CFG to define a Control Flow Graph. -/
diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean
index dad755b7b..accbe2b51 100644
--- a/Cslib/Analysis/Dataflow/Kildall.lean
+++ b/Cslib/Analysis/Dataflow/Kildall.lean
@@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jacopo Moretti
 -/
 
-import Cslib.Analysis.Dataflow.CFG
-import Mathlib.Order.Lattice
-import Mathlib.Data.DFinsupp.WellFounded
+module
+
+public import Cslib.Analysis.Dataflow.CFG
+public import Mathlib.Order.Lattice
+public import Mathlib.Data.DFinsupp.WellFounded
 
 /-!
 # Forward Worklist dataflow algorithm
@@ -38,6 +40,8 @@ technique borrowed from @LaSpina25.
 * [R. LaSpina, *Formal Verification of WTO-based Dataflow Solvers*][LaSpina25]
 -/
 
+@[expose] public section
+
 variable {Node Edge : Type} [DecidableEq Node] [DecidableEq Edge]
 
 /-- The state of a dataflow analysis on graph `g` is a mapping from nodes `n`