From 80bf039368ad3ded64ded55a685bd77bc20e5987 Mon Sep 17 00:00:00 2001 From: Jacopo Moretti Date: Thu, 6 Aug 2026 17:29:02 +0200 Subject: [PATCH 01/10] 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 Date: Fri, 7 Aug 2026 16:28:34 +0200 Subject: [PATCH 02/10] 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 Date: Fri, 7 Aug 2026 16:28:43 +0200 Subject: [PATCH 03/10] 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 Date: Fri, 7 Aug 2026 17:11:56 +0200 Subject: [PATCH 04/10] 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 Date: Fri, 7 Aug 2026 17:58:43 +0200 Subject: [PATCH 05/10] 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 Date: Fri, 7 Aug 2026 20:04:11 +0200 Subject: [PATCH 06/10] 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` From d3e1e381b23a9b5b5156bc73ea88bab05aa0b0ec Mon Sep 17 00:00:00 2001 From: Jacopo Moretti Date: Sat, 8 Aug 2026 11:54:14 +0200 Subject: [PATCH 07/10] chore(CFG): update references.bib --- references.bib | 851 ++++++++++++++++++++++++++----------------------- 1 file changed, 448 insertions(+), 403 deletions(-) diff --git a/references.bib b/references.bib index 6af9dafc4..5211fa9fc 100644 --- a/references.bib +++ b/references.bib @@ -1,110 +1,110 @@ @misc{Acclavio2026, - title={Choreographic Programming: a Semantic Approach}, - author={Matteo Acclavio and Giulia Manara and Fabrizio Montesi and Xueying Qin}, - year={2026}, - eprint={2607.23793}, - archivePrefix={arXiv}, - primaryClass={cs.PL}, - url={https://arxiv.org/abs/2607.23793}, + title = {Choreographic Programming: a Semantic Approach}, + author = {Matteo Acclavio and Giulia Manara and Fabrizio Montesi and Xueying Qin}, + year = {2026}, + eprint = {2607.23793}, + archiveprefix = {arXiv}, + primaryclass = {cs.PL}, + url = {https://arxiv.org/abs/2607.23793} } @inproceedings{Aceto1999, - author = {Luca Aceto and - Anna Ing{\'{o}}lfsd{\'{o}}ttir}, - editor = {Wolfgang Thomas}, - title = {Testing Hennessy-Milner Logic with Recursion}, - booktitle = {Foundations of Software Science and Computation Structure, Second - International Conference, FoSSaCS'99, Held as Part of the European - Joint Conferences on the Theory and Practice of Software, ETAPS'99, - Amsterdam, The Netherlands, March 22-28, 1999, Proceedings}, - series = {Lecture Notes in Computer Science}, - volume = {1578}, - pages = {41--55}, - publisher = {Springer}, - year = {1999}, - url = {https://doi.org/10.1007/3-540-49019-1\_4}, - doi = {10.1007/3-540-49019-1\_4}, - timestamp = {Tue, 14 May 2019 10:00:55 +0200}, - biburl = {https://dblp.org/rec/conf/fossacs/AcetoI99.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} + author = {Luca Aceto and + Anna Ing{\'{o}}lfsd{\'{o}}ttir}, + editor = {Wolfgang Thomas}, + title = {Testing Hennessy-Milner Logic with Recursion}, + booktitle = {Foundations of Software Science and Computation Structure, Second + International Conference, FoSSaCS'99, Held as Part of the European + Joint Conferences on the Theory and Practice of Software, ETAPS'99, + Amsterdam, The Netherlands, March 22-28, 1999, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {1578}, + pages = {41--55}, + publisher = {Springer}, + year = {1999}, + url = {https://doi.org/10.1007/3-540-49019-1\_4}, + doi = {10.1007/3-540-49019-1\_4}, + timestamp = {Tue, 14 May 2019 10:00:55 +0200}, + biburl = {https://dblp.org/rec/conf/fossacs/AcetoI99.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} } @article{AngluinLaird1988, - author = {Angluin, Dana and Laird, Philip}, - title = {Learning from Noisy Examples}, - journal = {Machine Learning}, - volume = {2}, - number = {4}, - pages = {343--370}, - year = {1988}, - doi = {10.1007/BF00116829} + author = {Angluin, Dana and Laird, Philip}, + title = {Learning from Noisy Examples}, + journal = {Machine Learning}, + volume = {2}, + number = {4}, + pages = {343--370}, + year = {1988}, + doi = {10.1007/BF00116829} } @book{Baader1998, -author = {Baader, Franz and Nipkow, Tobias}, -title = {Term rewriting and all that}, -year = {1998}, -isbn = {0521455200}, -publisher = {Cambridge University Press}, -address = {USA} + author = {Baader, Franz and Nipkow, Tobias}, + title = {Term rewriting and all that}, + year = {1998}, + isbn = {0521455200}, + publisher = {Cambridge University Press}, + address = {USA} } @book{Blackburn2001, - place={Cambridge}, - series={Cambridge Tracts in Theoretical Computer Science}, - title={Modal Logic}, - publisher={Cambridge University Press}, - author={Blackburn, Patrick and Rijke, Maarten de and Venema, Yde}, - year={2001}, - collection={Cambridge Tracts in Theoretical Computer Science} + place = {Cambridge}, + series = {Cambridge Tracts in Theoretical Computer Science}, + title = {Modal Logic}, + publisher = {Cambridge University Press}, + author = {Blackburn, Patrick and Rijke, Maarten de and Venema, Yde}, + year = {2001}, + collection = {Cambridge Tracts in Theoretical Computer Science} } @misc{Burghardt2018, - title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}}, - url = {https://arxiv.org/abs/1806.05036v2}, - abstract = {We checked each binary relation on a 5-element set for a given set of properties, including usual ones like asymmetry and less known ones like Euclideanness. Using a poor man's Quine-McCluskey algorithm, we computed prime implicants of non-occurring property combinations, like "not irreflexive, but asymmetric". We considered the non-trivial laws obtained this way, and manually proved them true for binary relations on arbitrary sets, thus contributing to the encyclopedic knowledge about less known properties.}, - language = {en}, - urldate = {2026-05-19}, - journal = {arXiv.org}, - author = {Burghardt, Jochen}, - month = jun, - year = {2018}, + title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}}, + url = {https://arxiv.org/abs/1806.05036v2}, + abstract = {We checked each binary relation on a 5-element set for a given set of properties, including usual ones like asymmetry and less known ones like Euclideanness. Using a poor man's Quine-McCluskey algorithm, we computed prime implicants of non-occurring property combinations, like "not irreflexive, but asymmetric". We considered the non-trivial laws obtained this way, and manually proved them true for binary relations on arbitrary sets, thus contributing to the encyclopedic knowledge about less known properties.}, + language = {en}, + urldate = {2026-05-19}, + journal = {arXiv.org}, + author = {Burghardt, Jochen}, + month = jun, + year = {2018} } @inproceedings{Danielsson2008, -author = {Danielsson, Nils Anders}, -title = {Lightweight semiformal time complexity analysis for purely functional data structures}, -year = {2008}, -isbn = {9781595936899}, -publisher = {Association for Computing Machinery}, -address = {New York, NY, USA}, -url = {https://doi.org/10.1145/1328438.1328457}, -doi = {10.1145/1328438.1328457}, -abstract = {Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.}, -booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, -pages = {133–144}, -numpages = {12}, -keywords = {purely functional data structures, lazy evaluation, dependent types, amortised time complexity}, -location = {San Francisco, California, USA}, -series = {POPL '08} -} - - -@article{ Barendregt1984, - title={Introduction to Lambda Calculus}, - year={1984} -} - -@book{ Hopcroft2006, -author = {Hopcroft, John E. and Motwani, Rajeev and Ullman, Jeffrey D.}, -title = {Introduction to Automata Theory, Languages, and Computation (3rd Edition)}, -year = {2006}, -isbn = {0321455363}, -publisher = {Addison-Wesley Longman Publishing Co., Inc.}, -address = {USA} -} - -@misc{ Malkin2024, + author = {Danielsson, Nils Anders}, + title = {Lightweight semiformal time complexity analysis for purely functional data structures}, + year = {2008}, + isbn = {9781595936899}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/1328438.1328457}, + doi = {10.1145/1328438.1328457}, + abstract = {Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.}, + booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + pages = {133–144}, + numpages = {12}, + keywords = {purely functional data structures, lazy evaluation, dependent types, amortised time complexity}, + location = {San Francisco, California, USA}, + series = {POPL '08} +} + + +@article{Barendregt1984, + title = {Introduction to Lambda Calculus}, + year = {1984} +} + +@book{Hopcroft2006, + author = {Hopcroft, John E. and Motwani, Rajeev and Ullman, Jeffrey D.}, + title = {Introduction to Automata Theory, Languages, and Computation (3rd Edition)}, + year = {2006}, + isbn = {0321455363}, + publisher = {Addison-Wesley Longman Publishing Co., Inc.}, + address = {USA} +} + +@misc{Malkin2024, author = {Tal Malkin}, title = {{COMS W3261: Computer Science Theory, Handout 3: The Myhill-Nerode Theorem and Implications}}, howpublished = {Columbia University Course Handout}, @@ -113,7 +113,7 @@ @misc{ Malkin2024 url = {https://www.cs.columbia.edu/~tal/3261/fall24/Handouts/3_Myhill_Nerode.pdf} } -@misc{ WikipediaMyhillNerode2026, +@misc{WikipediaMyhillNerode2026, author = {{Wikipedia contributors}}, title = {{Myhill--Nerode theorem}}, howpublished = {Wikipedia, The Free Encyclopedia}, @@ -122,122 +122,122 @@ @misc{ WikipediaMyhillNerode2026 note = {[Online; accessed 9-April-2026]} } -@article{ Chargueraud2012, - title = {The {Locally} {Nameless} {Representation}}, - volume = {49}, - issn = {1573-0670}, - url = {https://doi.org/10.1007/s10817-011-9225-2}, - doi = {10.1007/s10817-011-9225-2}, - abstract = {This paper provides an introduction to the locally nameless approach to the representation of syntax with variable binding, focusing in particular on the use of this technique in formal proofs. First, we explain the benefits of representing bound variables with de Bruijn indices while retaining names for free variables. Then, we explain how to describe and manipulate syntax in that form, and show how to define and reason about judgments on locally nameless terms.}, - language = {en}, - number = {3}, - urldate = {2025-07-13}, - journal = {Journal of Automated Reasoning}, - author = {Charguéraud, Arthur}, - month = oct, - year = {2012}, - keywords = {Binders, C++, Cofinite quantification, Convention Theory, Data Structures, Formal proofs, Functions of a Complex Variable, Lisp, Locally nameless, Metatheory, Syntax}, - pages = {363--408}, - file = {Full Text PDF:/home/chenson/mount/Zotero/storage/WBJWAZGI/Charguéraud - 2012 - The Locally Nameless Representation.pdf:application/pdf}, -} - -@article{ FLP1985, - author = {Fischer, Michael J. and Lynch, Nancy A. and Paterson, Michael S.}, - title = {Impossibility of Distributed Consensus with One Faulty Process}, - year = {1985}, +@article{Chargueraud2012, + title = {The {Locally} {Nameless} {Representation}}, + volume = {49}, + issn = {1573-0670}, + url = {https://doi.org/10.1007/s10817-011-9225-2}, + doi = {10.1007/s10817-011-9225-2}, + abstract = {This paper provides an introduction to the locally nameless approach to the representation of syntax with variable binding, focusing in particular on the use of this technique in formal proofs. First, we explain the benefits of representing bound variables with de Bruijn indices while retaining names for free variables. Then, we explain how to describe and manipulate syntax in that form, and show how to define and reason about judgments on locally nameless terms.}, + language = {en}, + number = {3}, + urldate = {2025-07-13}, + journal = {Journal of Automated Reasoning}, + author = {Charguéraud, Arthur}, + month = oct, + year = {2012}, + keywords = {Binders, C++, Cofinite quantification, Convention Theory, Data Structures, Formal proofs, Functions of a Complex Variable, Lisp, Locally nameless, Metatheory, Syntax}, + pages = {363--408}, + file = {Full Text PDF:/home/chenson/mount/Zotero/storage/WBJWAZGI/Charguéraud - 2012 - The Locally Nameless Representation.pdf:application/pdf} +} + +@article{FLP1985, + author = {Fischer, Michael J. and Lynch, Nancy A. and Paterson, Michael S.}, + title = {Impossibility of Distributed Consensus with One Faulty Process}, + year = {1985}, issue_date = {April 1985}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - volume = {32}, - number = {2}, - issn = {0004-5411}, - url = {https://doi.org/10.1145/3149.214121}, - doi = {10.1145/3149.214121}, - journal = {J. ACM}, - month = {apr}, - pages = {374–382}, - numpages = {9} -} - -@article{ Girard1987, - title={Linear logic}, - author={Girard, Jean-Yves}, - journal={Theoretical Computer Science}, - volume={50}, - number={1}, - year={1987}, - pages={1--101}, - issn={0304-3975}, - doi={10.1016/0304-3975(87)90045-4}, - url={https://www.sciencedirect.com/science/article/pii/0304397587900454}, - abstract={The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality "of course" which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.} -} - -@inbook{ Girard1995, - place={Cambridge}, - series={London Mathematical Society Lecture Note Series}, - title={Linear Logic: its syntax and semantics}, - booktitle={Advances in Linear Logic}, - publisher={Cambridge University Press}, - author={Girard, J.-Y.}, - editor={Girard, Jean-Yves and Lafont, Yves and Regnier, LaurentEditors}, - year={1995}, - pages={1–42}, - collection={London Mathematical Society Lecture Note Series} + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + volume = {32}, + number = {2}, + issn = {0004-5411}, + url = {https://doi.org/10.1145/3149.214121}, + doi = {10.1145/3149.214121}, + journal = {J. ACM}, + month = {apr}, + pages = {374–382}, + numpages = {9} +} + +@article{Girard1987, + title = {Linear logic}, + author = {Girard, Jean-Yves}, + journal = {Theoretical Computer Science}, + volume = {50}, + number = {1}, + year = {1987}, + pages = {1--101}, + issn = {0304-3975}, + doi = {10.1016/0304-3975(87)90045-4}, + url = {https://www.sciencedirect.com/science/article/pii/0304397587900454}, + abstract = {The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality "of course" which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.} +} + +@inbook{Girard1995, + place = {Cambridge}, + series = {London Mathematical Society Lecture Note Series}, + title = {Linear Logic: its syntax and semantics}, + booktitle = {Advances in Linear Logic}, + publisher = {Cambridge University Press}, + author = {Girard, J.-Y.}, + editor = {Girard, Jean-Yves and Lafont, Yves and Regnier, LaurentEditors}, + year = {1995}, + pages = {1–42}, + collection = {London Mathematical Society Lecture Note Series} } @article{Haussler1992, - author = {Haussler, David}, - title = {Decision Theoretic Generalizations of the {PAC} Model for Neural Net and Other Learning Applications}, - journal = {Information and Computation}, - volume = {100}, - number = {1}, - pages = {78--150}, - year = {1992}, - issn = {0890-5401}, - doi = {10.1016/0890-5401(92)90010-D} -} - -@article{ Hennessy1985, - author = {Matthew Hennessy and - Robin Milner}, - title = {Algebraic Laws for Nondeterminism and Concurrency}, - journal = {J. {ACM}}, - volume = {32}, - number = {1}, - pages = {137--161}, - year = {1985}, - url = {https://doi.org/10.1145/2455.2460}, - doi = {10.1145/2455.2460}, - timestamp = {Tue, 06 Nov 2018 12:51:45 +0100}, - biburl = {https://dblp.org/rec/journals/jacm/HennessyM85.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} - -@book{ KatzLindell2020, - author = {Jonathan Katz and - Yehuda Lindell}, - title = {Introduction to Modern Cryptography}, - edition = {3rd}, - publisher = {CRC Press}, - year = {2020}, - isbn = {9780815354369} -} - -@article{ Shamir1979, - author = {Adi Shamir}, - title = {How to Share a Secret}, - journal = {Communications of the ACM}, - volume = {22}, - number = {11}, - pages = {612--613}, - year = {1979}, - month = nov, - url = {https://doi.org/10.1145/359168.359176}, - doi = {10.1145/359168.359176} -} - -@inproceedings{ Kiselyov2015, + author = {Haussler, David}, + title = {Decision Theoretic Generalizations of the {PAC} Model for Neural Net and Other Learning Applications}, + journal = {Information and Computation}, + volume = {100}, + number = {1}, + pages = {78--150}, + year = {1992}, + issn = {0890-5401}, + doi = {10.1016/0890-5401(92)90010-D} +} + +@article{Hennessy1985, + author = {Matthew Hennessy and + Robin Milner}, + title = {Algebraic Laws for Nondeterminism and Concurrency}, + journal = {J. {ACM}}, + volume = {32}, + number = {1}, + pages = {137--161}, + year = {1985}, + url = {https://doi.org/10.1145/2455.2460}, + doi = {10.1145/2455.2460}, + timestamp = {Tue, 06 Nov 2018 12:51:45 +0100}, + biburl = {https://dblp.org/rec/journals/jacm/HennessyM85.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book{KatzLindell2020, + author = {Jonathan Katz and + Yehuda Lindell}, + title = {Introduction to Modern Cryptography}, + edition = {3rd}, + publisher = {CRC Press}, + year = {2020}, + isbn = {9780815354369} +} + +@article{Shamir1979, + author = {Adi Shamir}, + title = {How to Share a Secret}, + journal = {Communications of the ACM}, + volume = {22}, + number = {11}, + pages = {612--613}, + year = {1979}, + month = nov, + url = {https://doi.org/10.1145/359168.359176}, + doi = {10.1145/359168.359176} +} + +@inproceedings{Kiselyov2015, author = {Kiselyov, Oleg and Ishii, Hiromi}, title = {Freer Monads, More Extensible Effects}, booktitle = {Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell}, @@ -251,172 +251,172 @@ @inproceedings{ Kiselyov2015 isbn = {978-1-4503-3808-0} } -@book{ MilewskiDao, +@book{MilewskiDao, author = {Milewski, Bartosz}, title = {The Dao of Functional Programming}, publisher = {Self-published}, year = {2018}, - note = {Available online at \url{https://bartoszmilewski.com}}, -} - -@book{ Milner80, - author = {Robin Milner}, - title = {A Calculus of Communicating Systems}, - series = {Lecture Notes in Computer Science}, - volume = {92}, - publisher = {Springer}, - year = {1980}, - url = {https://doi.org/10.1007/3-540-10235-3}, - doi = {10.1007/3-540-10235-3}, - isbn = {3-540-10235-3}, - timestamp = {Tue, 14 May 2019 10:00:35 +0200}, - biburl = {https://dblp.org/rec/books/sp/Milner80.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} - -@Book{ Montesi2023, - title = {Introduction to {Choreographies}}, - author = {Montesi, Fabrizio}, - year = {2023}, - publisher = {Cambridge University Press}, - address = {Cambridge}, - url = {https://www.cambridge.org/core/books/introduction-to-choreographies/65D3DA3CFF11AB835452CBC97FAE4830}, - urldate = {2023-02-02}, - doi = {10.1017/9781108981491}, - abstract = {In concurrent and distributed systems, processes can - complete tasks together by playing their parts in a joint - plan. The plan, or protocol, can be written as a - choreography: a formal description of overall behaviour - that processes should collaborate to implement, like - authenticating a user or purchasing an item online. - Formality brings clarity, but not only that: choreographies - can contribute to important safety and liveness properties. - This book is an ideal introduction to theory of - choreographies for students, researchers, and professionals - in computer science and applied mathematics. It covers - languages for writing choreographies, their semantics, and - principles for implementing choreographies correctly. The - text treats the study of choreographies as a discipline in - its own right, following a systematic approach that starts - from simple foundations and proceeds to more advanced - features in incremental steps. Each chapter includes - examples and exercises aimed at helping with understanding - the theory and its relation to practice.}, - isbn = {978-1-108-83376-9}, - keywords = {choreographic-programming,choreographic-language,choreography,concurrency-theory} -} - -@article{ Nipkow2001, - title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, - author = {Nipkow, Tobias}, - journal = {Journal of Automated Reasoning}, - volume = {26}, - pages = {51--66}, - year = {2001}, - publisher = {Kluwer Academic Publishers} -} - -@Book{ Sangiorgi2011, - location = {Cambridge}, - title = {Introduction to Bisimulation and Coinduction}, - isbn = {978-1-107-00363-7}, - url = {https://www.cambridge.org/core/books/introduction-to-bisimulation-and-coinduction/8B54001CB763BAE9C4BA602C0A341D60}, - abstract = {Induction is a pervasive tool in computer science and - mathematics for defining objects and reasoning on them. - Coinduction is the dual of induction and as such it brings - in quite different tools. Today, it is widely used in - computer science, but also in other fields, including - artificial intelligence, cognitive science, mathematics, - modal logics, philosophy and physics. The best known - instance of coinduction is bisimulation, mainly employed to - define and prove equalities among potentially infinite - objects: processes, streams, non-well-founded sets, etc. - This book presents bisimulation and coinduction: the - fundamental concepts and techniques and the duality with - induction. Each chapter contains exercises and selected - solutions, enabling students to connect theory with - practice. A special emphasis is placed on bisimulation as a - behavioural equivalence for processes. Thus the book serves - as an introduction to models for expressing processes (such - as process calculi) and to the associated techniques of - operational and algebraic analysis.}, - publisher = {Cambridge University Press}, - author = {Sangiorgi, Davide}, - urldate = {2025-06-16}, - date = {2011}, - doi = {10.1017/CBO9780511777110} -} - -@incollection{ Thomas1990, - author = {Wolfgang Thomas}, - editor = {Jan van Leeuwen}, - title = {Automata on Infinite Objects}, - booktitle = {Handbook of Theoretical Computer Science, Volume {B:} Formal Models and Semantics}, - pages = {133--191}, - publisher = {Elsevier and {MIT} Press}, - year = {1990} -} - -@book{ Cutland1980, - author = {Cutland, Nigel J.}, - title = {Computability: An Introduction to Recursive Function Theory}, - year = {1980}, - publisher = {Cambridge University Press}, - address = {Cambridge}, - isbn = {978-0-521-29465-2} -} - -@article{ ShepherdsonSturgis1963, - author = {Shepherdson, J. C. and Sturgis, H. E.}, - title = {Computability of Recursive Functions}, - journal = {Journal of the ACM}, - volume = {10}, - number = {2}, - year = {1963}, - pages = {217--255}, - doi = {10.1145/321160.321170}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA} + note = {Available online at \url{https://bartoszmilewski.com}} +} + +@book{Milner80, + author = {Robin Milner}, + title = {A Calculus of Communicating Systems}, + series = {Lecture Notes in Computer Science}, + volume = {92}, + publisher = {Springer}, + year = {1980}, + url = {https://doi.org/10.1007/3-540-10235-3}, + doi = {10.1007/3-540-10235-3}, + isbn = {3-540-10235-3}, + timestamp = {Tue, 14 May 2019 10:00:35 +0200}, + biburl = {https://dblp.org/rec/books/sp/Milner80.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book{Montesi2023, + title = {Introduction to {Choreographies}}, + author = {Montesi, Fabrizio}, + year = {2023}, + publisher = {Cambridge University Press}, + address = {Cambridge}, + url = {https://www.cambridge.org/core/books/introduction-to-choreographies/65D3DA3CFF11AB835452CBC97FAE4830}, + urldate = {2023-02-02}, + doi = {10.1017/9781108981491}, + abstract = {In concurrent and distributed systems, processes can + complete tasks together by playing their parts in a joint + plan. The plan, or protocol, can be written as a + choreography: a formal description of overall behaviour + that processes should collaborate to implement, like + authenticating a user or purchasing an item online. + Formality brings clarity, but not only that: choreographies + can contribute to important safety and liveness properties. + This book is an ideal introduction to theory of + choreographies for students, researchers, and professionals + in computer science and applied mathematics. It covers + languages for writing choreographies, their semantics, and + principles for implementing choreographies correctly. The + text treats the study of choreographies as a discipline in + its own right, following a systematic approach that starts + from simple foundations and proceeds to more advanced + features in incremental steps. Each chapter includes + examples and exercises aimed at helping with understanding + the theory and its relation to practice.}, + isbn = {978-1-108-83376-9}, + keywords = {choreographic-programming,choreographic-language,choreography,concurrency-theory} +} + +@article{Nipkow2001, + title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, + author = {Nipkow, Tobias}, + journal = {Journal of Automated Reasoning}, + volume = {26}, + pages = {51--66}, + year = {2001}, + publisher = {Kluwer Academic Publishers} +} + +@book{Sangiorgi2011, + location = {Cambridge}, + title = {Introduction to Bisimulation and Coinduction}, + isbn = {978-1-107-00363-7}, + url = {https://www.cambridge.org/core/books/introduction-to-bisimulation-and-coinduction/8B54001CB763BAE9C4BA602C0A341D60}, + abstract = {Induction is a pervasive tool in computer science and + mathematics for defining objects and reasoning on them. + Coinduction is the dual of induction and as such it brings + in quite different tools. Today, it is widely used in + computer science, but also in other fields, including + artificial intelligence, cognitive science, mathematics, + modal logics, philosophy and physics. The best known + instance of coinduction is bisimulation, mainly employed to + define and prove equalities among potentially infinite + objects: processes, streams, non-well-founded sets, etc. + This book presents bisimulation and coinduction: the + fundamental concepts and techniques and the duality with + induction. Each chapter contains exercises and selected + solutions, enabling students to connect theory with + practice. A special emphasis is placed on bisimulation as a + behavioural equivalence for processes. Thus the book serves + as an introduction to models for expressing processes (such + as process calculi) and to the associated techniques of + operational and algebraic analysis.}, + publisher = {Cambridge University Press}, + author = {Sangiorgi, Davide}, + urldate = {2025-06-16}, + date = {2011}, + doi = {10.1017/CBO9780511777110} +} + +@incollection{Thomas1990, + author = {Wolfgang Thomas}, + editor = {Jan van Leeuwen}, + title = {Automata on Infinite Objects}, + booktitle = {Handbook of Theoretical Computer Science, Volume {B:} Formal Models and Semantics}, + pages = {133--191}, + publisher = {Elsevier and {MIT} Press}, + year = {1990} +} + +@book{Cutland1980, + author = {Cutland, Nigel J.}, + title = {Computability: An Introduction to Recursive Function Theory}, + year = {1980}, + publisher = {Cambridge University Press}, + address = {Cambridge}, + isbn = {978-0-521-29465-2} +} + +@article{ShepherdsonSturgis1963, + author = {Shepherdson, J. C. and Sturgis, H. E.}, + title = {Computability of Recursive Functions}, + journal = {Journal of the ACM}, + volume = {10}, + number = {2}, + year = {1963}, + pages = {217--255}, + doi = {10.1145/321160.321170}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA} } @inproceedings{Valiant1984, - author = {Valiant, L. G.}, - title = {A Theory of the Learnable}, - year = {1984}, - isbn = {0-89791-133-4}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - url = {https://doi.org/10.1145/800057.808710}, - doi = {10.1145/800057.808710}, - booktitle = {Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing}, - pages = {436--445}, - series = {STOC '84} + author = {Valiant, L. G.}, + title = {A Theory of the Learnable}, + year = {1984}, + isbn = {0-89791-133-4}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/800057.808710}, + doi = {10.1145/800057.808710}, + booktitle = {Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing}, + pages = {436--445}, + series = {STOC '84} } @article{EHKV1989, - author = {Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie}, - title = {A General Lower Bound on the Number of Examples Needed for Learning}, - journal = {Information and Computation}, - volume = {82}, - number = {3}, - pages = {247--261}, - year = {1989}, - issn = {0890-5401}, - url = {https://doi.org/10.1016/0890-5401(89)90002-3}, - doi = {10.1016/0890-5401(89)90002-3}, - publisher = {Academic Press} + author = {Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie}, + title = {A General Lower Bound on the Number of Examples Needed for Learning}, + journal = {Information and Computation}, + volume = {82}, + number = {3}, + pages = {247--261}, + year = {1989}, + issn = {0890-5401}, + url = {https://doi.org/10.1016/0890-5401(89)90002-3}, + doi = {10.1016/0890-5401(89)90002-3}, + publisher = {Academic Press} } @book{KearnsVazirani1994, - author = {Kearns, Michael J. and Vazirani, Umesh V.}, - title = {An Introduction to Computational Learning Theory}, - year = {1994}, - isbn = {978-0-262-11193-5}, - publisher = {MIT Press}, - address = {Cambridge, MA, USA} + author = {Kearns, Michael J. and Vazirani, Umesh V.}, + title = {An Introduction to Computational Learning Theory}, + year = {1994}, + isbn = {978-0-262-11193-5}, + publisher = {MIT Press}, + address = {Cambridge, MA, USA} } -@article{ Volzer2004, +@article{Volzer2004, title = {A constructive proof for {FLP}}, author = {V{\"o}lzer, Hagen}, journal = {Information Processing Letters}, @@ -430,61 +430,61 @@ @article{ Volzer2004 } @incollection{WinskelNielsen1995, - author = {Winskel, Glynn and Nielsen, Mogens}, - isbn = {9780198537809}, - title = {Models for concurrency}, - booktitle = {Handbook of Logic in Computer Science}, - publisher = {Oxford University Press}, - year = {1995}, - month = {05}, - doi = {10.1093/oso/9780198537809.003.0001}, - url = {https://doi.org/10.1093/oso/9780198537809.003.0001}, - eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf}, + author = {Winskel, Glynn and Nielsen, Mogens}, + isbn = {9780198537809}, + title = {Models for concurrency}, + booktitle = {Handbook of Logic in Computer Science}, + publisher = {Oxford University Press}, + year = {1995}, + month = {05}, + doi = {10.1093/oso/9780198537809.003.0001}, + url = {https://doi.org/10.1093/oso/9780198537809.003.0001}, + eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf} } @inproceedings{Mitchell1977, - author = {Mitchell, Tom M.}, - title = {Version Spaces: A Candidate Elimination Approach to Rule Learning}, - booktitle = {Proceedings of the 5th International Joint Conference on Artificial Intelligence}, - volume = {1}, - pages = {305--310}, - year = {1977} + author = {Mitchell, Tom M.}, + title = {Version Spaces: A Candidate Elimination Approach to Rule Learning}, + booktitle = {Proceedings of the 5th International Joint Conference on Artificial Intelligence}, + volume = {1}, + pages = {305--310}, + year = {1977} } @article{Mitchell1982, - author = {Mitchell, Tom M.}, - title = {Generalization as Search}, - journal = {Artificial Intelligence}, - volume = {18}, - number = {2}, - pages = {203--226}, - year = {1982}, - doi = {10.1016/0004-3702(82)90040-6} + author = {Mitchell, Tom M.}, + title = {Generalization as Search}, + journal = {Artificial Intelligence}, + volume = {18}, + number = {2}, + pages = {203--226}, + year = {1982}, + doi = {10.1016/0004-3702(82)90040-6} } @article{Angluin1980, - author = {Angluin, Dana}, - title = {Inductive Inference of Formal Languages from Positive Data}, - journal = {Information and Control}, - volume = {45}, - number = {2}, - pages = {117--135}, - year = {1980}, - doi = {10.1016/S0019-9958(80)90285-5} + author = {Angluin, Dana}, + title = {Inductive Inference of Formal Languages from Positive Data}, + journal = {Information and Control}, + volume = {45}, + number = {2}, + pages = {117--135}, + year = {1980}, + doi = {10.1016/S0019-9958(80)90285-5} } @book{Mitchell1997, - author = {Mitchell, Tom M.}, - title = {Machine Learning}, - year = {1997}, - publisher = {McGraw-Hill}, - isbn = {0070428077} + author = {Mitchell, Tom M.}, + title = {Machine Learning}, + year = {1997}, + publisher = {McGraw-Hill}, + isbn = {0070428077} } @mastersthesis{Calisto2022, - author = {Calisto, Bruna}, - title = {Formalization in {Coq} of the {Standardization Theorem} for {$\lambda$}-calculus}, - school = {Universidade do Minho}, - year = {2022} + author = {Calisto, Bruna}, + title = {Formalization in {Coq} of the {Standardization Theorem} for {$\lambda$}-calculus}, + school = {Universidade do Minho}, + year = {2022} } @book{Sipser2013, @@ -495,17 +495,62 @@ @book{Sipser2013 year = {2013} } @book{AroraBarak09, - author = {Sanjeev Arora and - Boaz Barak}, - title = {Computational Complexity - {A} Modern Approach}, - publisher = {Cambridge University Press}, - year = {2009}, + author = {Sanjeev Arora and + Boaz Barak}, + title = {Computational Complexity - {A} Modern Approach}, + publisher = {Cambridge University Press}, + year = {2009} } @book{Papadimitriou94, - title={Computational Complexity}, - author={Papadimitriou, Christos H.}, - year={1994}, - publisher={Addison-Wesley}, - address={Reading, Massachusetts} + title = {Computational Complexity}, + author = {Papadimitriou, Christos H.}, + year = {1994}, + publisher = {Addison-Wesley}, + address = {Reading, Massachusetts} +} + +@inproceedings{Kildall73, + author = {Kildall, Gary A.}, + title = {A unified approach to global program optimization}, + year = {1973}, + isbn = {9781450373494}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/512927.512945}, + doi = {10.1145/512927.512945}, + abstract = {A technique is presented for global analysis of program structure in order to perform compile time optimization of object code generated for expressions. The global expression optimization presented includes constant propagation, common subexpression elimination, elimination of redundant register load operations, and live expression analysis. A general purpose program flow analysis algorithm is developed which depends upon the existence of an "optimizing function." The algorithm is defined formally using a directed graph model of program flow structure, and is shown to be correct. Several optimizing functions are defined which, when used in conjunction with the flow analysis algorithm, provide the various forms of code optimization. The flow analysis algorithm is sufficiently general that additional functions can easily be defined for other forms of global code optimization.}, + booktitle = {Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages}, + pages = {194-206}, + numpages = {13}, + location = {Boston, Massachusetts}, + series = {POPL '73} +} + +@book{Nielson99, + address = {Berlin, Heidelberg}, + title = {Principles of Program Analysis}, + rights = {http://www.springer.com/tdm}, + isbn = {978-3-642-08474-4}, + url = {http://link.springer.com/10.1007/978-3-662-03811-6}, + doi = {10.1007/978-3-662-03811-6}, + publisher = {Springer Berlin Heidelberg}, + author = {Nielson, Flemming and Nielson, Hanne Riis and Hankin, Chris}, + year = {1999}, + language = {en} +} + +@inproceedings{LaSpina25, + title = {{Formal Verification of WTO-based Dataflow Solvers}}, + author = {La Spina, Rom{\'e}o and Demange, Delphine and Blazy, Sandrine}, + url = {https://hal.science/hal-04851724}, + booktitle = {{Programming Languages and Systems}}, + address = {Hamilton, Canada}, + pages = {1-27}, + year = {2025}, + month = May, + keywords = {compiler optimization ; verified compilation ; static analysis}, + pdf = {https://hal.science/hal-04851724v1/file/paper.pdf}, + hal_id = {hal-04851724}, + hal_version = {v1} } From 5be94bdb4f7f1e005b77475e4784dadecb7cdf15 Mon Sep 17 00:00:00 2001 From: Jacopo Moretti Date: Mon, 10 Aug 2026 12:01:11 +0200 Subject: [PATCH 08/10] feat(CFG): recharacterize based on quivers and finsets --- Cslib/Analysis/Dataflow/CFG.lean | 77 +++++++------ Cslib/Analysis/Dataflow/Kildall.lean | 161 ++++++++++++++------------- 2 files changed, 129 insertions(+), 109 deletions(-) diff --git a/Cslib/Analysis/Dataflow/CFG.lean b/Cslib/Analysis/Dataflow/CFG.lean index 97093a528..7e1ba01d9 100644 --- a/Cslib/Analysis/Dataflow/CFG.lean +++ b/Cslib/Analysis/Dataflow/CFG.lean @@ -8,7 +8,11 @@ module public import Cslib.Init public import Mathlib.Data.Fintype.List +public import Mathlib.Data.Fintype.Sigma +public import Mathlib.Data.Finset.Sort public import Mathlib.Data.DFinsupp.WellFounded +public import Mathlib.Combinatorics.Quiver.Basic +public import Mathlib.Combinatorics.Quiver.Covering /-! @@ -22,51 +26,56 @@ public import Mathlib.Data.DFinsupp.WellFounded @[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. -/ -class CFG (Node Edge : Type) [DecidableEq Node] [DecidableEq Edge] where +structure CFG 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. -/ + Node : Type u + [fintypeNode : Fintype Node] + [orderNode : LinearOrder Node] + [dEqNode : DecidableEq Node] + /-- Quiver structure for the edges of the CFG. -/ + quiver : Quiver Node + [fintypeHom : ∀ a b, Fintype (@Quiver.Hom Node quiver a b)] + /-- 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 +instance {g : CFG} : Fintype (g.Node) := + g.fintypeNode + +instance {g : CFG} : LinearOrder (g.Node) := + g.orderNode + +def nodesOf (g : CFG) : Finset g.Node := g.fintypeNode.elems -def edgesOf (g : CFG Node Edge) : List (EdgeOf g) := g.edges.attach +def nodeList (g : CFG) : List g.Node := g.nodesOf.sort -def dstOf (g : CFG Node Edge) (e : EdgeOf g) : NodeOf g := - ⟨g._dstOf e, g.dstOf_mem e e.property⟩ +@[simp] theorem mem_nodeList (g : CFG) (n : g.Node) : n ∈ g.nodeList := by + rw [nodeList] + apply (Finset.mem_sort (· ≤ ·)).mpr + exact @Fintype.complete _ g.fintypeNode n -def srcOf (g : CFG Node Edge) (e : EdgeOf g) : NodeOf g := - ⟨g._srcOf e, g.srcOf_mem e e.property⟩ +abbrev Edge {g : CFG} (src dst : g.Node) := @Quiver.Hom g.Node g.quiver src dst +abbrev inEdge {g : CFG} (n : g.Node) := @Quiver.Costar g.Node g.quiver n +abbrev outEdge {g : CFG} (n : g.Node) := @Quiver.Star g.Node g.quiver n -/-- 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) +/-- All incoming edges of a given node, bundled with their source nodes. -/ +def inEdges {g : CFG} (n : g.Node) : Finset (inEdge n) := by + letI := g.quiver + letI := g.fintypeNode + letI := g.orderNode + letI (src dst : g.Node) := g.fintypeHom src dst + exact Finset.univ -def succOf (g : CFG Node Edge) (n : NodeOf g) : List (NodeOf g) := - g.nodesOf.filter (fun m => (g.inEdges m).any (g.srcOf · = n)) +def outEdges {g : CFG} (n : g.Node) : Finset (outEdge n) := by + letI := g.quiver + letI := g.fintypeNode + letI (src dst : g.Node) := g.fintypeHom src dst + exact Finset.univ -instance {g : CFG Node Edge} : Fintype (NodeOf g) := - List.Subtype.fintype g.nodes +def succOf {g : CFG} (n : g.Node) : Finset g.Node := + letI := g.dEqNode + (outEdges n).image Sigma.fst end CFG diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean index accbe2b51..fcd1535d0 100644 --- a/Cslib/Analysis/Dataflow/Kildall.lean +++ b/Cslib/Analysis/Dataflow/Kildall.lean @@ -9,6 +9,7 @@ module public import Cslib.Analysis.Dataflow.CFG public import Mathlib.Order.Lattice public import Mathlib.Data.DFinsupp.WellFounded +public import Mathlib.Data.Finset.Sort /-! # Forward Worklist dataflow algorithm @@ -42,25 +43,24 @@ technique borrowed from @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` 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) (L : Type) : Type := g.Node → L namespace DFState 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 _ => ⊥ +def empty {g : CFG} [OrderBot L] : DFState g L := fun _ => ⊥ /-- 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 := +def update {g : CFG} (ρ : DFState g L) (n : g.Node) (v : L) : DFState g L := + letI := g.dEqNode fun m => if m = n then v else ρ m /-- 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) : +theorem lt_update {g : CFG} (ρ : DFState g L) (n : g.Node) (v : L) (hlt : ρ n < v) : ρ < ρ.update n v := by rw [Pi.lt_def] refine ⟨fun m => ?_, n, ?_⟩ <;> grind [DFState.update] @@ -70,34 +70,36 @@ end DFState section Kildall variable {L : Type} [SemilatticeSup L] [DecidableEq L] [OrderBot L] -variable {g : CFG Node Edge} +variable {g : CFG} /-- 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) := +local instance {g : CFG} [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ᵒᵈ)) + inferInstanceAs (WellFoundedLT (g.Node → Lᵒᵈ)) /-- Wellfoundedness of state ordering based on WellFoundedGT. -/ -local instance {g : CFG Node Edge} [WellFoundedGT L] : WellFoundedRelation (DFState g L) := +local instance {g : CFG} [WellFoundedGT L] : WellFoundedRelation (DFState g L) := ⟨(· > ·), IsWellFounded.wf⟩ -/-- The type of a transfer function over α. -/ -abbrev Transfer (α L : Type) := α → L → L +abbrev NodeTransfer (g : CFG) (L : Type) := g.Node -> L -> L +abbrev EdgeTransfer (g : CFG) (L : Type) := ∀ {src dst : g.Node}, + g.Edge src dst -> L -> 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)) - ) (if n.val = g.entry then init else ⊥) +def joinPred {g : CFG} (eT : EdgeTransfer g L) (init : L) (ρ : DFState g L) (n : g.Node) : L := + letI := g.dEqNode + (g.inEdges n).fold (· ⊔ ·) + (if n = g.entry then init else ⊥) + (fun e => eT e.2 (ρ e.1)) /-- 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. -/ @[simp] -def kildall [WellFoundedGT L] {g : CFG Node Edge} - (nT : Transfer Node L) (eT : Transfer Edge L) +def kildall [WellFoundedGT L] {g : CFG} + (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L) (ρ : DFState g L := DFState.empty) - (wl : List (NodeOf g) := g.nodesOf) : DFState g L := + (wl : List (g.Node) := g.nodeList) : DFState g L := + letI := g.orderNode match wl with | [] => ρ | n :: rest => @@ -107,7 +109,7 @@ def kildall [WellFoundedGT L] {g : CFG Node Edge} kildall nT eT init ρ rest else let ρ' := DFState.update ρ n newOut - let wl' := rest ++ g.succOf n + let wl' := rest ++ (g.succOf n).sort kildall nT eT init ρ' wl' termination_by (ρ, wl.length) decreasing_by @@ -126,20 +128,20 @@ variable {L : Type} [SemilatticeSup L] [WellFoundedGT L] [OrderBot L] /-- 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 := + {g : CFG} (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L) + (ρ : DFState g L) (wl : List (g.Node)) : 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 := + {g : CFG} (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L) + (ρ : DFState g L) (wl : List (g.Node)) : 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) +def ForwardPreFixpoint {g : CFG} (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L) (ρ : DFState g L) : Prop := ∀ n, ρ n ≤ nT n (joinPred eT init ρ n) @@ -148,47 +150,48 @@ def ForwardPreFixpoint {g : CFG Node Edge} (nT : Transfer Node L) (eT : Transfer 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) : +lemma joinPred_neq_of_nonpred {g : CFG} (eT : EdgeTransfer g L) (init : L) + (ρ : DFState g L) (n m : g.Node) (v : L) (hm : n ∉ g.succOf m) : joinPred eT init (ρ.update m v) n = joinPred eT init ρ n := by simp only [joinPred] - apply List.foldl_ext - intro acc e he + apply Finset.fold_congr + intro e _ simp only [DFState.update] split case isFalse hneq => rfl case isTrue heq => + subst m 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 + apply (@Finset.mem_image _ _ g.dEqNode).mpr + exact ⟨⟨n, e.2⟩, by simp [CFG.outEdges], rfl⟩ 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 := g) eT init) := by +lemma monotone_joinPred {g : CFG} (eT : EdgeTransfer g L) (init : L) + (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e)) : + Monotone (joinPred (g := 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 + (g.inEdges n).fold (fun x y : L => x ⊔ y) init₁ (fun e => eT e.2 (ρ₁ e.1)) ≤ + (g.inEdges n).fold (fun x y : L => x ⊔ y) init₂ (fun e => eT e.2 (ρ₂ e.1)) by apply Std.IsPreorder.le_refl _ |> this _ _ - induction g.inEdges n with - | nil => simp - | cons e t ih => + induction g.inEdges n using Finset.cons_induction with + | empty => simp + | cons e s hnmem ih => intros i₁ i₂ hlei - simp only [List.foldl_cons] - refine sup_le_sup hlei ?_ |> ih _ _ - exact heT e (hle _) + rw [Finset.fold_cons hnmem, Finset.fold_cons hnmem] + exact sup_le_sup (heT e.2 (hle e.1)) (ih _ _ hlei) /-- The result of the worklist algorithm satisfies any invariant preserved through the algorithm's run. Technique borrowed from @LaSpina25 -/ 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) + {g : CFG} (nT : NodeTransfer g L) (eT : EdgeTransfer g L) + (init : L) (ρ : DFState g L) (wl : List (g.Node)) + (P : DFState g L → List (g.Node) → Prop) (hinit : P ρ wl) (hstep_same : ∀ {ρ n rest}, P ρ (n :: rest) → let newOut := ρ n ⊔ nT n (joinPred eT init ρ n) @@ -197,7 +200,7 @@ lemma kildall_invariant [DecidableEq L] (hstep_changed : ∀ {ρ n rest}, P ρ (n :: rest) → let newOut := ρ n ⊔ nT n (joinPred eT init ρ n) newOut ≠ ρ n → - P (ρ.update n newOut) (rest ++ g.succOf n)) : + P (ρ.update n newOut) (rest ++ (g.succOf n).sort)) : P (kildall nT eT init ρ wl) [] := by induction ρ, wl using kildall.induct nT eT init with | case1 o => simpa @@ -214,10 +217,10 @@ lemma kildall_invariant [DecidableEq L] /-- 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) : +theorem kildall_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG} + (nT : NodeTransfer g L) (eT : EdgeTransfer g L) (init : L) (ρ : DFState g L) + (wl : List (g.Node)) + (hinv0 : ∀ m : g.Node, 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) ?_ ?_ ?_ @@ -228,7 +231,8 @@ theorem kildall_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG Node Edge} 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 + have hsucc : m ∉ g.succOf n := fun hin => + hm (List.mem_append_right _ ((g.succOf n).mem_sort (· ≤ ·) |>.mpr hin)) rw [joinPred_neq_of_nonpred eT init ρ m n newOut hsucc, DFState.update] split -- m ?= n case isTrue heq => @@ -238,10 +242,11 @@ theorem kildall_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG Node Edge} /-- 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)) +theorem kildall_least_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG} + (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n)) + (eT : EdgeTransfer g L) + (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e)) + (init : L) (ρ σ : DFState g L) (wl : List (g.Node)) (hρ : ρ ≤ σ) (hσ : ForwardPostFixpoint nT eT init σ []) : kildall nT eT init ρ wl ≤ σ := by refine kildall_invariant nT eT init ρ wl @@ -258,10 +263,11 @@ theorem kildall_least_forwardPostFixpoint_of_init [DecidableEq L] {g : CFG Node case isFalse hneq => exact hle m /-- The worklist algorithm preserves forward pre-fixpoints when all transfers are monotone. -/ -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)) +lemma kildall_forwardPreFixpoint_of_init [DecidableEq L] {g : CFG} + (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n)) + (eT : EdgeTransfer g L) + (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e)) + (init : L) (ρ : DFState g L) (wl : List (g.Node)) (hinv0 : ForwardPreFixpoint nT eT init ρ) : let res := kildall nT eT init ρ wl ForwardPreFixpoint nT eT init res := by @@ -280,10 +286,11 @@ lemma kildall_forwardPreFixpoint_of_init [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)) +theorem kildall_forwardFixpoint_of_init [DecidableEq L] {g : CFG} + (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n)) + (eT : EdgeTransfer g L) + (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e)) + (init : L) (ρ : DFState g L) (wl : List (g.Node)) (hpost0 : ∀ m ∉ wl, nT m (joinPred eT init ρ m) ≤ ρ m) (hpre0 : ForwardPreFixpoint nT eT init ρ) : let res := kildall nT eT init ρ wl @@ -297,36 +304,40 @@ theorem kildall_forwardFixpoint_of_init [DecidableEq L] {g : CFG Node Edge} exact le_antisymm (hpost n hn) (hpre n) /-- 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) : +theorem kildall_forwardPostFixpoint [DecidableEq L] (g : CFG) + (nT : NodeTransfer g L) (eT : EdgeTransfer g 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] + intro m hm + exact (hm (g.mem_nodeList m)).elim -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)) +theorem kildall_least_forwardPostFixpoint [DecidableEq L] (g : CFG) + (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n)) + (eT : EdgeTransfer g L) + (heT : ∀ {src dst} (e : g.Edge src dst), 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 + apply kildall_least_forwardPostFixpoint_of_init nT hnT eT heT init DFState.empty σ g.nodeList <;> 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)) +theorem kildall_forwardFixpoint [DecidableEq L] (g : CFG) + (nT : NodeTransfer g L) (hnT : ∀ n, Monotone (nT n)) + (eT : EdgeTransfer g L) + (heT : ∀ {src dst} (e : g.Edge src dst), Monotone (eT e)) (init : L) : let res := kildall (g := g) nT eT init ForwardFixpoint (g := g) nT eT init res [] := by - apply kildall_forwardFixpoint_of_init nT hnT eT heT init DFState.empty g.nodesOf + apply kildall_forwardFixpoint_of_init nT hnT eT heT init DFState.empty g.nodeList case hpost0 => -- ≤ -- `∀ m ∉ g.nodesOf, ...` -- since every `m` is in `g.nodesOf` this is vacuously true - grind [CFG.nodesOf] + intro m hm + exact (hm (g.mem_nodeList m)).elim case hpre0 => -- ≥ -- `∀ m ∈ g.nodesOf, DFState.empty m ≤ ...` -- since `DFState.empty` is `λ _. ⊥`, it's ≤ anything, thanks to `OrderBot`. From 0237dc8950948c91103bbe566117762f87f6b4f2 Mon Sep 17 00:00:00 2001 From: Jacopo Moretti Date: Mon, 10 Aug 2026 15:48:34 +0200 Subject: [PATCH 09/10] chore(CFG): fix lints --- Cslib/Analysis/Dataflow/CFG.lean | 20 +++++++++++++++++--- Cslib/Analysis/Dataflow/Kildall.lean | 14 +++++++++++--- 2 files changed, 28 insertions(+), 6 deletions(-) diff --git a/Cslib/Analysis/Dataflow/CFG.lean b/Cslib/Analysis/Dataflow/CFG.lean index 7e1ba01d9..317076e09 100644 --- a/Cslib/Analysis/Dataflow/CFG.lean +++ b/Cslib/Analysis/Dataflow/CFG.lean @@ -30,12 +30,16 @@ public import Mathlib.Combinatorics.Quiver.Covering structure CFG where /-- All of the nodes in the CFG. -/ Node : Type u + /-- A CFG contains a finite amount of nodes. -/ [fintypeNode : Fintype Node] + /-- An ordering of nodes, to make the conversion to lists computable. -/ [orderNode : LinearOrder Node] + /-- Decidable equality on nodes. -/ [dEqNode : DecidableEq Node] /-- Quiver structure for the edges of the CFG. -/ quiver : Quiver Node - [fintypeHom : ∀ a b, Fintype (@Quiver.Hom Node quiver a b)] + /-- A CFG contains a finite amount of edges. -/ + [fintypeEdges : ∀ a b, Fintype (@Quiver.Hom Node quiver a b)] /-- Distinguished entry node in the CFG. -/ entry : Node @@ -47,17 +51,25 @@ instance {g : CFG} : Fintype (g.Node) := instance {g : CFG} : LinearOrder (g.Node) := g.orderNode +/-- Finite set of all of the nodes of `g` -/ def nodesOf (g : CFG) : Finset g.Node := g.fintypeNode.elems +/-- List of all of the nodes of `g`, ordered by the ordering on `g.Node` -/ def nodeList (g : CFG) : List g.Node := g.nodesOf.sort +/-- Any node of `g` is in `g.nodeList`. -/ @[simp] theorem mem_nodeList (g : CFG) (n : g.Node) : n ∈ g.nodeList := by rw [nodeList] apply (Finset.mem_sort (· ≤ ·)).mpr exact @Fintype.complete _ g.fintypeNode n +/-- Convenience type for edges of `g`: `Edge src dst` represents an edge between src and dst. -/ abbrev Edge {g : CFG} (src dst : g.Node) := @Quiver.Hom g.Node g.quiver src dst +/-- Convenience type for incoming edges of `n` in `g`: `inEdge n` represents the type of edges + entering n. -/ abbrev inEdge {g : CFG} (n : g.Node) := @Quiver.Costar g.Node g.quiver n +/-- Convenience type for outgoing edges of `n` in `g`: `outEdge n` represents the type of edges + entering n. -/ abbrev outEdge {g : CFG} (n : g.Node) := @Quiver.Star g.Node g.quiver n /-- All incoming edges of a given node, bundled with their source nodes. -/ @@ -65,15 +77,17 @@ def inEdges {g : CFG} (n : g.Node) : Finset (inEdge n) := by letI := g.quiver letI := g.fintypeNode letI := g.orderNode - letI (src dst : g.Node) := g.fintypeHom src dst + letI (src dst : g.Node) := g.fintypeEdges src dst exact Finset.univ +/-- All outgoing edges of a given node, bundled with their source nodes. -/ def outEdges {g : CFG} (n : g.Node) : Finset (outEdge n) := by letI := g.quiver letI := g.fintypeNode - letI (src dst : g.Node) := g.fintypeHom src dst + letI (src dst : g.Node) := g.fintypeEdges src dst exact Finset.univ +/-- The set of successor nodes of node `n` in `g`. -/ def succOf {g : CFG} (n : g.Node) : Finset g.Node := letI := g.dEqNode (outEdges n).image Sigma.fst diff --git a/Cslib/Analysis/Dataflow/Kildall.lean b/Cslib/Analysis/Dataflow/Kildall.lean index fcd1535d0..1f81de052 100644 --- a/Cslib/Analysis/Dataflow/Kildall.lean +++ b/Cslib/Analysis/Dataflow/Kildall.lean @@ -43,6 +43,8 @@ technique borrowed from @LaSpina25. @[expose] public section +namespace Kildall + /-- 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) (L : Type) : Type := g.Node → L @@ -81,15 +83,19 @@ local instance {g : CFG} [WellFoundedGT L] : WellFoundedGT (DFState g L) := local instance {g : CFG} [WellFoundedGT L] : WellFoundedRelation (DFState g L) := ⟨(· > ·), IsWellFounded.wf⟩ +/-- Convenience type for a transfer function over nodes. -/ abbrev NodeTransfer (g : CFG) (L : Type) := g.Node -> L -> L -abbrev EdgeTransfer (g : CFG) (L : Type) := ∀ {src dst : g.Node}, - g.Edge src dst -> L -> L +/-- Convenience type for a transfer function over edges. -/ +abbrev EdgeTransfer (g : CFG) (L : Type) := ∀ {src dst : g.Node}, g.Edge src dst -> L -> L +/-- For a given CFG `g`, at node `n`, computes the join operation of all states incoming from + predecessor nodes through their relative edge transfers. Accounts for initialization at the + entry node. -/ def joinPred {g : CFG} (eT : EdgeTransfer g L) (init : L) (ρ : DFState g L) (n : g.Node) : L := letI := g.dEqNode (g.inEdges n).fold (· ⊔ ·) (if n = g.entry then init else ⊥) - (fun e => eT e.2 (ρ e.1)) + (fun ⟨n, e⟩ => eT e (ρ n)) /-- 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 @@ -342,3 +348,5 @@ theorem kildall_forwardFixpoint [DecidableEq L] (g : CFG) -- `∀ m ∈ g.nodesOf, DFState.empty m ≤ ...` -- since `DFState.empty` is `λ _. ⊥`, it's ≤ anything, thanks to `OrderBot`. simp [ForwardPreFixpoint, DFState.empty] + +end Kildall From 9e8c302361a27cb1818d0413f899aaccec946924 Mon Sep 17 00:00:00 2001 From: Jacopo Moretti Date: Mon, 10 Aug 2026 18:27:07 +0200 Subject: [PATCH 10/10] chore(CFG): fix references.bib --- references.bib | 806 ++++++++++++++++++++++++------------------------- 1 file changed, 403 insertions(+), 403 deletions(-) diff --git a/references.bib b/references.bib index 5211fa9fc..b6b3dff36 100644 --- a/references.bib +++ b/references.bib @@ -1,110 +1,110 @@ @misc{Acclavio2026, - title = {Choreographic Programming: a Semantic Approach}, - author = {Matteo Acclavio and Giulia Manara and Fabrizio Montesi and Xueying Qin}, - year = {2026}, - eprint = {2607.23793}, - archiveprefix = {arXiv}, - primaryclass = {cs.PL}, - url = {https://arxiv.org/abs/2607.23793} + title={Choreographic Programming: a Semantic Approach}, + author={Matteo Acclavio and Giulia Manara and Fabrizio Montesi and Xueying Qin}, + year={2026}, + eprint={2607.23793}, + archivePrefix={arXiv}, + primaryClass={cs.PL}, + url={https://arxiv.org/abs/2607.23793}, } @inproceedings{Aceto1999, - author = {Luca Aceto and - Anna Ing{\'{o}}lfsd{\'{o}}ttir}, - editor = {Wolfgang Thomas}, - title = {Testing Hennessy-Milner Logic with Recursion}, - booktitle = {Foundations of Software Science and Computation Structure, Second - International Conference, FoSSaCS'99, Held as Part of the European - Joint Conferences on the Theory and Practice of Software, ETAPS'99, - Amsterdam, The Netherlands, March 22-28, 1999, Proceedings}, - series = {Lecture Notes in Computer Science}, - volume = {1578}, - pages = {41--55}, - publisher = {Springer}, - year = {1999}, - url = {https://doi.org/10.1007/3-540-49019-1\_4}, - doi = {10.1007/3-540-49019-1\_4}, - timestamp = {Tue, 14 May 2019 10:00:55 +0200}, - biburl = {https://dblp.org/rec/conf/fossacs/AcetoI99.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} + author = {Luca Aceto and + Anna Ing{\'{o}}lfsd{\'{o}}ttir}, + editor = {Wolfgang Thomas}, + title = {Testing Hennessy-Milner Logic with Recursion}, + booktitle = {Foundations of Software Science and Computation Structure, Second + International Conference, FoSSaCS'99, Held as Part of the European + Joint Conferences on the Theory and Practice of Software, ETAPS'99, + Amsterdam, The Netherlands, March 22-28, 1999, Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {1578}, + pages = {41--55}, + publisher = {Springer}, + year = {1999}, + url = {https://doi.org/10.1007/3-540-49019-1\_4}, + doi = {10.1007/3-540-49019-1\_4}, + timestamp = {Tue, 14 May 2019 10:00:55 +0200}, + biburl = {https://dblp.org/rec/conf/fossacs/AcetoI99.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} } @article{AngluinLaird1988, - author = {Angluin, Dana and Laird, Philip}, - title = {Learning from Noisy Examples}, - journal = {Machine Learning}, - volume = {2}, - number = {4}, - pages = {343--370}, - year = {1988}, - doi = {10.1007/BF00116829} + author = {Angluin, Dana and Laird, Philip}, + title = {Learning from Noisy Examples}, + journal = {Machine Learning}, + volume = {2}, + number = {4}, + pages = {343--370}, + year = {1988}, + doi = {10.1007/BF00116829} } @book{Baader1998, - author = {Baader, Franz and Nipkow, Tobias}, - title = {Term rewriting and all that}, - year = {1998}, - isbn = {0521455200}, - publisher = {Cambridge University Press}, - address = {USA} +author = {Baader, Franz and Nipkow, Tobias}, +title = {Term rewriting and all that}, +year = {1998}, +isbn = {0521455200}, +publisher = {Cambridge University Press}, +address = {USA} } @book{Blackburn2001, - place = {Cambridge}, - series = {Cambridge Tracts in Theoretical Computer Science}, - title = {Modal Logic}, - publisher = {Cambridge University Press}, - author = {Blackburn, Patrick and Rijke, Maarten de and Venema, Yde}, - year = {2001}, - collection = {Cambridge Tracts in Theoretical Computer Science} + place={Cambridge}, + series={Cambridge Tracts in Theoretical Computer Science}, + title={Modal Logic}, + publisher={Cambridge University Press}, + author={Blackburn, Patrick and Rijke, Maarten de and Venema, Yde}, + year={2001}, + collection={Cambridge Tracts in Theoretical Computer Science} } @misc{Burghardt2018, - title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}}, - url = {https://arxiv.org/abs/1806.05036v2}, - abstract = {We checked each binary relation on a 5-element set for a given set of properties, including usual ones like asymmetry and less known ones like Euclideanness. Using a poor man's Quine-McCluskey algorithm, we computed prime implicants of non-occurring property combinations, like "not irreflexive, but asymmetric". We considered the non-trivial laws obtained this way, and manually proved them true for binary relations on arbitrary sets, thus contributing to the encyclopedic knowledge about less known properties.}, - language = {en}, - urldate = {2026-05-19}, - journal = {arXiv.org}, - author = {Burghardt, Jochen}, - month = jun, - year = {2018} + title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}}, + url = {https://arxiv.org/abs/1806.05036v2}, + abstract = {We checked each binary relation on a 5-element set for a given set of properties, including usual ones like asymmetry and less known ones like Euclideanness. Using a poor man's Quine-McCluskey algorithm, we computed prime implicants of non-occurring property combinations, like "not irreflexive, but asymmetric". We considered the non-trivial laws obtained this way, and manually proved them true for binary relations on arbitrary sets, thus contributing to the encyclopedic knowledge about less known properties.}, + language = {en}, + urldate = {2026-05-19}, + journal = {arXiv.org}, + author = {Burghardt, Jochen}, + month = jun, + year = {2018}, } @inproceedings{Danielsson2008, - author = {Danielsson, Nils Anders}, - title = {Lightweight semiformal time complexity analysis for purely functional data structures}, - year = {2008}, - isbn = {9781595936899}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - url = {https://doi.org/10.1145/1328438.1328457}, - doi = {10.1145/1328438.1328457}, - abstract = {Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.}, - booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, - pages = {133–144}, - numpages = {12}, - keywords = {purely functional data structures, lazy evaluation, dependent types, amortised time complexity}, - location = {San Francisco, California, USA}, - series = {POPL '08} -} - - -@article{Barendregt1984, - title = {Introduction to Lambda Calculus}, - year = {1984} -} - -@book{Hopcroft2006, - author = {Hopcroft, John E. and Motwani, Rajeev and Ullman, Jeffrey D.}, - title = {Introduction to Automata Theory, Languages, and Computation (3rd Edition)}, - year = {2006}, - isbn = {0321455363}, - publisher = {Addison-Wesley Longman Publishing Co., Inc.}, - address = {USA} -} - -@misc{Malkin2024, +author = {Danielsson, Nils Anders}, +title = {Lightweight semiformal time complexity analysis for purely functional data structures}, +year = {2008}, +isbn = {9781595936899}, +publisher = {Association for Computing Machinery}, +address = {New York, NY, USA}, +url = {https://doi.org/10.1145/1328438.1328457}, +doi = {10.1145/1328438.1328457}, +abstract = {Okasaki and others have demonstrated how purely functional data structures that are efficient even in the presence of persistence can be constructed. To achieve good time bounds essential use is often made of laziness. The associated complexity analysis is frequently subtle, requiring careful attention to detail, and hence formalising it is valuable. This paper describes a simple library which can be used to make the analysis of a class of purely functional data structures and algorithms almost fully formal. The basic idea is to use the type system to annotate every function with the time required to compute its result. An annotated monad is used to combine time complexity annotations. The library has been used to analyse some existing data structures, for instance the deque operations of Hinze and Paterson's finger trees.}, +booktitle = {Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, +pages = {133–144}, +numpages = {12}, +keywords = {purely functional data structures, lazy evaluation, dependent types, amortised time complexity}, +location = {San Francisco, California, USA}, +series = {POPL '08} +} + + +@article{ Barendregt1984, + title={Introduction to Lambda Calculus}, + year={1984} +} + +@book{ Hopcroft2006, +author = {Hopcroft, John E. and Motwani, Rajeev and Ullman, Jeffrey D.}, +title = {Introduction to Automata Theory, Languages, and Computation (3rd Edition)}, +year = {2006}, +isbn = {0321455363}, +publisher = {Addison-Wesley Longman Publishing Co., Inc.}, +address = {USA} +} + +@misc{ Malkin2024, author = {Tal Malkin}, title = {{COMS W3261: Computer Science Theory, Handout 3: The Myhill-Nerode Theorem and Implications}}, howpublished = {Columbia University Course Handout}, @@ -113,7 +113,7 @@ @misc{Malkin2024 url = {https://www.cs.columbia.edu/~tal/3261/fall24/Handouts/3_Myhill_Nerode.pdf} } -@misc{WikipediaMyhillNerode2026, +@misc{ WikipediaMyhillNerode2026, author = {{Wikipedia contributors}}, title = {{Myhill--Nerode theorem}}, howpublished = {Wikipedia, The Free Encyclopedia}, @@ -122,122 +122,122 @@ @misc{WikipediaMyhillNerode2026 note = {[Online; accessed 9-April-2026]} } -@article{Chargueraud2012, - title = {The {Locally} {Nameless} {Representation}}, - volume = {49}, - issn = {1573-0670}, - url = {https://doi.org/10.1007/s10817-011-9225-2}, - doi = {10.1007/s10817-011-9225-2}, - abstract = {This paper provides an introduction to the locally nameless approach to the representation of syntax with variable binding, focusing in particular on the use of this technique in formal proofs. First, we explain the benefits of representing bound variables with de Bruijn indices while retaining names for free variables. Then, we explain how to describe and manipulate syntax in that form, and show how to define and reason about judgments on locally nameless terms.}, - language = {en}, - number = {3}, - urldate = {2025-07-13}, - journal = {Journal of Automated Reasoning}, - author = {Charguéraud, Arthur}, - month = oct, - year = {2012}, - keywords = {Binders, C++, Cofinite quantification, Convention Theory, Data Structures, Formal proofs, Functions of a Complex Variable, Lisp, Locally nameless, Metatheory, Syntax}, - pages = {363--408}, - file = {Full Text PDF:/home/chenson/mount/Zotero/storage/WBJWAZGI/Charguéraud - 2012 - The Locally Nameless Representation.pdf:application/pdf} -} - -@article{FLP1985, - author = {Fischer, Michael J. and Lynch, Nancy A. and Paterson, Michael S.}, - title = {Impossibility of Distributed Consensus with One Faulty Process}, - year = {1985}, +@article{ Chargueraud2012, + title = {The {Locally} {Nameless} {Representation}}, + volume = {49}, + issn = {1573-0670}, + url = {https://doi.org/10.1007/s10817-011-9225-2}, + doi = {10.1007/s10817-011-9225-2}, + abstract = {This paper provides an introduction to the locally nameless approach to the representation of syntax with variable binding, focusing in particular on the use of this technique in formal proofs. First, we explain the benefits of representing bound variables with de Bruijn indices while retaining names for free variables. Then, we explain how to describe and manipulate syntax in that form, and show how to define and reason about judgments on locally nameless terms.}, + language = {en}, + number = {3}, + urldate = {2025-07-13}, + journal = {Journal of Automated Reasoning}, + author = {Charguéraud, Arthur}, + month = oct, + year = {2012}, + keywords = {Binders, C++, Cofinite quantification, Convention Theory, Data Structures, Formal proofs, Functions of a Complex Variable, Lisp, Locally nameless, Metatheory, Syntax}, + pages = {363--408}, + file = {Full Text PDF:/home/chenson/mount/Zotero/storage/WBJWAZGI/Charguéraud - 2012 - The Locally Nameless Representation.pdf:application/pdf}, +} + +@article{ FLP1985, + author = {Fischer, Michael J. and Lynch, Nancy A. and Paterson, Michael S.}, + title = {Impossibility of Distributed Consensus with One Faulty Process}, + year = {1985}, issue_date = {April 1985}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - volume = {32}, - number = {2}, - issn = {0004-5411}, - url = {https://doi.org/10.1145/3149.214121}, - doi = {10.1145/3149.214121}, - journal = {J. ACM}, - month = {apr}, - pages = {374–382}, - numpages = {9} -} - -@article{Girard1987, - title = {Linear logic}, - author = {Girard, Jean-Yves}, - journal = {Theoretical Computer Science}, - volume = {50}, - number = {1}, - year = {1987}, - pages = {1--101}, - issn = {0304-3975}, - doi = {10.1016/0304-3975(87)90045-4}, - url = {https://www.sciencedirect.com/science/article/pii/0304397587900454}, - abstract = {The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality "of course" which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.} -} - -@inbook{Girard1995, - place = {Cambridge}, - series = {London Mathematical Society Lecture Note Series}, - title = {Linear Logic: its syntax and semantics}, - booktitle = {Advances in Linear Logic}, - publisher = {Cambridge University Press}, - author = {Girard, J.-Y.}, - editor = {Girard, Jean-Yves and Lafont, Yves and Regnier, LaurentEditors}, - year = {1995}, - pages = {1–42}, - collection = {London Mathematical Society Lecture Note Series} -} - -@article{Haussler1992, - author = {Haussler, David}, - title = {Decision Theoretic Generalizations of the {PAC} Model for Neural Net and Other Learning Applications}, - journal = {Information and Computation}, - volume = {100}, - number = {1}, - pages = {78--150}, - year = {1992}, - issn = {0890-5401}, - doi = {10.1016/0890-5401(92)90010-D} -} - -@article{Hennessy1985, - author = {Matthew Hennessy and - Robin Milner}, - title = {Algebraic Laws for Nondeterminism and Concurrency}, - journal = {J. {ACM}}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, volume = {32}, - number = {1}, - pages = {137--161}, - year = {1985}, - url = {https://doi.org/10.1145/2455.2460}, - doi = {10.1145/2455.2460}, - timestamp = {Tue, 06 Nov 2018 12:51:45 +0100}, - biburl = {https://dblp.org/rec/journals/jacm/HennessyM85.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} - -@book{KatzLindell2020, - author = {Jonathan Katz and - Yehuda Lindell}, - title = {Introduction to Modern Cryptography}, - edition = {3rd}, - publisher = {CRC Press}, - year = {2020}, - isbn = {9780815354369} -} - -@article{Shamir1979, - author = {Adi Shamir}, - title = {How to Share a Secret}, - journal = {Communications of the ACM}, - volume = {22}, - number = {11}, - pages = {612--613}, - year = {1979}, - month = nov, - url = {https://doi.org/10.1145/359168.359176}, - doi = {10.1145/359168.359176} + number = {2}, + issn = {0004-5411}, + url = {https://doi.org/10.1145/3149.214121}, + doi = {10.1145/3149.214121}, + journal = {J. ACM}, + month = {apr}, + pages = {374–382}, + numpages = {9} +} + +@article{ Girard1987, + title={Linear logic}, + author={Girard, Jean-Yves}, + journal={Theoretical Computer Science}, + volume={50}, + number={1}, + year={1987}, + pages={1--101}, + issn={0304-3975}, + doi={10.1016/0304-3975(87)90045-4}, + url={https://www.sciencedirect.com/science/article/pii/0304397587900454}, + abstract={The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality "of course" which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.} +} + +@inbook{ Girard1995, + place={Cambridge}, + series={London Mathematical Society Lecture Note Series}, + title={Linear Logic: its syntax and semantics}, + booktitle={Advances in Linear Logic}, + publisher={Cambridge University Press}, + author={Girard, J.-Y.}, + editor={Girard, Jean-Yves and Lafont, Yves and Regnier, LaurentEditors}, + year={1995}, + pages={1–42}, + collection={London Mathematical Society Lecture Note Series} } -@inproceedings{Kiselyov2015, +@article{Haussler1992, + author = {Haussler, David}, + title = {Decision Theoretic Generalizations of the {PAC} Model for Neural Net and Other Learning Applications}, + journal = {Information and Computation}, + volume = {100}, + number = {1}, + pages = {78--150}, + year = {1992}, + issn = {0890-5401}, + doi = {10.1016/0890-5401(92)90010-D} +} + +@article{ Hennessy1985, + author = {Matthew Hennessy and + Robin Milner}, + title = {Algebraic Laws for Nondeterminism and Concurrency}, + journal = {J. {ACM}}, + volume = {32}, + number = {1}, + pages = {137--161}, + year = {1985}, + url = {https://doi.org/10.1145/2455.2460}, + doi = {10.1145/2455.2460}, + timestamp = {Tue, 06 Nov 2018 12:51:45 +0100}, + biburl = {https://dblp.org/rec/journals/jacm/HennessyM85.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@book{ KatzLindell2020, + author = {Jonathan Katz and + Yehuda Lindell}, + title = {Introduction to Modern Cryptography}, + edition = {3rd}, + publisher = {CRC Press}, + year = {2020}, + isbn = {9780815354369} +} + +@article{ Shamir1979, + author = {Adi Shamir}, + title = {How to Share a Secret}, + journal = {Communications of the ACM}, + volume = {22}, + number = {11}, + pages = {612--613}, + year = {1979}, + month = nov, + url = {https://doi.org/10.1145/359168.359176}, + doi = {10.1145/359168.359176} +} + +@inproceedings{ Kiselyov2015, author = {Kiselyov, Oleg and Ishii, Hiromi}, title = {Freer Monads, More Extensible Effects}, booktitle = {Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell}, @@ -251,172 +251,172 @@ @inproceedings{Kiselyov2015 isbn = {978-1-4503-3808-0} } -@book{MilewskiDao, +@book{ MilewskiDao, author = {Milewski, Bartosz}, title = {The Dao of Functional Programming}, publisher = {Self-published}, year = {2018}, - note = {Available online at \url{https://bartoszmilewski.com}} -} - -@book{Milner80, - author = {Robin Milner}, - title = {A Calculus of Communicating Systems}, - series = {Lecture Notes in Computer Science}, - volume = {92}, - publisher = {Springer}, - year = {1980}, - url = {https://doi.org/10.1007/3-540-10235-3}, - doi = {10.1007/3-540-10235-3}, - isbn = {3-540-10235-3}, - timestamp = {Tue, 14 May 2019 10:00:35 +0200}, - biburl = {https://dblp.org/rec/books/sp/Milner80.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} - -@book{Montesi2023, - title = {Introduction to {Choreographies}}, - author = {Montesi, Fabrizio}, - year = {2023}, - publisher = {Cambridge University Press}, - address = {Cambridge}, - url = {https://www.cambridge.org/core/books/introduction-to-choreographies/65D3DA3CFF11AB835452CBC97FAE4830}, - urldate = {2023-02-02}, - doi = {10.1017/9781108981491}, - abstract = {In concurrent and distributed systems, processes can - complete tasks together by playing their parts in a joint - plan. The plan, or protocol, can be written as a - choreography: a formal description of overall behaviour - that processes should collaborate to implement, like - authenticating a user or purchasing an item online. - Formality brings clarity, but not only that: choreographies - can contribute to important safety and liveness properties. - This book is an ideal introduction to theory of - choreographies for students, researchers, and professionals - in computer science and applied mathematics. It covers - languages for writing choreographies, their semantics, and - principles for implementing choreographies correctly. The - text treats the study of choreographies as a discipline in - its own right, following a systematic approach that starts - from simple foundations and proceeds to more advanced - features in incremental steps. Each chapter includes - examples and exercises aimed at helping with understanding - the theory and its relation to practice.}, - isbn = {978-1-108-83376-9}, - keywords = {choreographic-programming,choreographic-language,choreography,concurrency-theory} -} - -@article{Nipkow2001, - title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, - author = {Nipkow, Tobias}, - journal = {Journal of Automated Reasoning}, - volume = {26}, - pages = {51--66}, - year = {2001}, - publisher = {Kluwer Academic Publishers} -} - -@book{Sangiorgi2011, - location = {Cambridge}, - title = {Introduction to Bisimulation and Coinduction}, - isbn = {978-1-107-00363-7}, - url = {https://www.cambridge.org/core/books/introduction-to-bisimulation-and-coinduction/8B54001CB763BAE9C4BA602C0A341D60}, - abstract = {Induction is a pervasive tool in computer science and - mathematics for defining objects and reasoning on them. - Coinduction is the dual of induction and as such it brings - in quite different tools. Today, it is widely used in - computer science, but also in other fields, including - artificial intelligence, cognitive science, mathematics, - modal logics, philosophy and physics. The best known - instance of coinduction is bisimulation, mainly employed to - define and prove equalities among potentially infinite - objects: processes, streams, non-well-founded sets, etc. - This book presents bisimulation and coinduction: the - fundamental concepts and techniques and the duality with - induction. Each chapter contains exercises and selected - solutions, enabling students to connect theory with - practice. A special emphasis is placed on bisimulation as a - behavioural equivalence for processes. Thus the book serves - as an introduction to models for expressing processes (such - as process calculi) and to the associated techniques of - operational and algebraic analysis.}, - publisher = {Cambridge University Press}, - author = {Sangiorgi, Davide}, - urldate = {2025-06-16}, - date = {2011}, - doi = {10.1017/CBO9780511777110} -} - -@incollection{Thomas1990, - author = {Wolfgang Thomas}, - editor = {Jan van Leeuwen}, - title = {Automata on Infinite Objects}, - booktitle = {Handbook of Theoretical Computer Science, Volume {B:} Formal Models and Semantics}, - pages = {133--191}, - publisher = {Elsevier and {MIT} Press}, - year = {1990} -} - -@book{Cutland1980, - author = {Cutland, Nigel J.}, - title = {Computability: An Introduction to Recursive Function Theory}, - year = {1980}, - publisher = {Cambridge University Press}, - address = {Cambridge}, - isbn = {978-0-521-29465-2} -} - -@article{ShepherdsonSturgis1963, - author = {Shepherdson, J. C. and Sturgis, H. E.}, - title = {Computability of Recursive Functions}, - journal = {Journal of the ACM}, - volume = {10}, - number = {2}, - year = {1963}, - pages = {217--255}, - doi = {10.1145/321160.321170}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA} + note = {Available online at \url{https://bartoszmilewski.com}}, +} + +@book{ Milner80, + author = {Robin Milner}, + title = {A Calculus of Communicating Systems}, + series = {Lecture Notes in Computer Science}, + volume = {92}, + publisher = {Springer}, + year = {1980}, + url = {https://doi.org/10.1007/3-540-10235-3}, + doi = {10.1007/3-540-10235-3}, + isbn = {3-540-10235-3}, + timestamp = {Tue, 14 May 2019 10:00:35 +0200}, + biburl = {https://dblp.org/rec/books/sp/Milner80.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + +@Book{ Montesi2023, + title = {Introduction to {Choreographies}}, + author = {Montesi, Fabrizio}, + year = {2023}, + publisher = {Cambridge University Press}, + address = {Cambridge}, + url = {https://www.cambridge.org/core/books/introduction-to-choreographies/65D3DA3CFF11AB835452CBC97FAE4830}, + urldate = {2023-02-02}, + doi = {10.1017/9781108981491}, + abstract = {In concurrent and distributed systems, processes can + complete tasks together by playing their parts in a joint + plan. The plan, or protocol, can be written as a + choreography: a formal description of overall behaviour + that processes should collaborate to implement, like + authenticating a user or purchasing an item online. + Formality brings clarity, but not only that: choreographies + can contribute to important safety and liveness properties. + This book is an ideal introduction to theory of + choreographies for students, researchers, and professionals + in computer science and applied mathematics. It covers + languages for writing choreographies, their semantics, and + principles for implementing choreographies correctly. The + text treats the study of choreographies as a discipline in + its own right, following a systematic approach that starts + from simple foundations and proceeds to more advanced + features in incremental steps. Each chapter includes + examples and exercises aimed at helping with understanding + the theory and its relation to practice.}, + isbn = {978-1-108-83376-9}, + keywords = {choreographic-programming,choreographic-language,choreography,concurrency-theory} +} + +@article{ Nipkow2001, + title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})}, + author = {Nipkow, Tobias}, + journal = {Journal of Automated Reasoning}, + volume = {26}, + pages = {51--66}, + year = {2001}, + publisher = {Kluwer Academic Publishers} +} + +@Book{ Sangiorgi2011, + location = {Cambridge}, + title = {Introduction to Bisimulation and Coinduction}, + isbn = {978-1-107-00363-7}, + url = {https://www.cambridge.org/core/books/introduction-to-bisimulation-and-coinduction/8B54001CB763BAE9C4BA602C0A341D60}, + abstract = {Induction is a pervasive tool in computer science and + mathematics for defining objects and reasoning on them. + Coinduction is the dual of induction and as such it brings + in quite different tools. Today, it is widely used in + computer science, but also in other fields, including + artificial intelligence, cognitive science, mathematics, + modal logics, philosophy and physics. The best known + instance of coinduction is bisimulation, mainly employed to + define and prove equalities among potentially infinite + objects: processes, streams, non-well-founded sets, etc. + This book presents bisimulation and coinduction: the + fundamental concepts and techniques and the duality with + induction. Each chapter contains exercises and selected + solutions, enabling students to connect theory with + practice. A special emphasis is placed on bisimulation as a + behavioural equivalence for processes. Thus the book serves + as an introduction to models for expressing processes (such + as process calculi) and to the associated techniques of + operational and algebraic analysis.}, + publisher = {Cambridge University Press}, + author = {Sangiorgi, Davide}, + urldate = {2025-06-16}, + date = {2011}, + doi = {10.1017/CBO9780511777110} +} + +@incollection{ Thomas1990, + author = {Wolfgang Thomas}, + editor = {Jan van Leeuwen}, + title = {Automata on Infinite Objects}, + booktitle = {Handbook of Theoretical Computer Science, Volume {B:} Formal Models and Semantics}, + pages = {133--191}, + publisher = {Elsevier and {MIT} Press}, + year = {1990} +} + +@book{ Cutland1980, + author = {Cutland, Nigel J.}, + title = {Computability: An Introduction to Recursive Function Theory}, + year = {1980}, + publisher = {Cambridge University Press}, + address = {Cambridge}, + isbn = {978-0-521-29465-2} +} + +@article{ ShepherdsonSturgis1963, + author = {Shepherdson, J. C. and Sturgis, H. E.}, + title = {Computability of Recursive Functions}, + journal = {Journal of the ACM}, + volume = {10}, + number = {2}, + year = {1963}, + pages = {217--255}, + doi = {10.1145/321160.321170}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA} } @inproceedings{Valiant1984, - author = {Valiant, L. G.}, - title = {A Theory of the Learnable}, - year = {1984}, - isbn = {0-89791-133-4}, - publisher = {Association for Computing Machinery}, - address = {New York, NY, USA}, - url = {https://doi.org/10.1145/800057.808710}, - doi = {10.1145/800057.808710}, - booktitle = {Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing}, - pages = {436--445}, - series = {STOC '84} + author = {Valiant, L. G.}, + title = {A Theory of the Learnable}, + year = {1984}, + isbn = {0-89791-133-4}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/800057.808710}, + doi = {10.1145/800057.808710}, + booktitle = {Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing}, + pages = {436--445}, + series = {STOC '84} } @article{EHKV1989, - author = {Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie}, - title = {A General Lower Bound on the Number of Examples Needed for Learning}, - journal = {Information and Computation}, - volume = {82}, - number = {3}, - pages = {247--261}, - year = {1989}, - issn = {0890-5401}, - url = {https://doi.org/10.1016/0890-5401(89)90002-3}, - doi = {10.1016/0890-5401(89)90002-3}, - publisher = {Academic Press} + author = {Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie}, + title = {A General Lower Bound on the Number of Examples Needed for Learning}, + journal = {Information and Computation}, + volume = {82}, + number = {3}, + pages = {247--261}, + year = {1989}, + issn = {0890-5401}, + url = {https://doi.org/10.1016/0890-5401(89)90002-3}, + doi = {10.1016/0890-5401(89)90002-3}, + publisher = {Academic Press} } @book{KearnsVazirani1994, - author = {Kearns, Michael J. and Vazirani, Umesh V.}, - title = {An Introduction to Computational Learning Theory}, - year = {1994}, - isbn = {978-0-262-11193-5}, - publisher = {MIT Press}, - address = {Cambridge, MA, USA} + author = {Kearns, Michael J. and Vazirani, Umesh V.}, + title = {An Introduction to Computational Learning Theory}, + year = {1994}, + isbn = {978-0-262-11193-5}, + publisher = {MIT Press}, + address = {Cambridge, MA, USA} } -@article{Volzer2004, +@article{ Volzer2004, title = {A constructive proof for {FLP}}, author = {V{\"o}lzer, Hagen}, journal = {Information Processing Letters}, @@ -430,61 +430,61 @@ @article{Volzer2004 } @incollection{WinskelNielsen1995, - author = {Winskel, Glynn and Nielsen, Mogens}, - isbn = {9780198537809}, - title = {Models for concurrency}, - booktitle = {Handbook of Logic in Computer Science}, - publisher = {Oxford University Press}, - year = {1995}, - month = {05}, - doi = {10.1093/oso/9780198537809.003.0001}, - url = {https://doi.org/10.1093/oso/9780198537809.003.0001}, - eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf} + author = {Winskel, Glynn and Nielsen, Mogens}, + isbn = {9780198537809}, + title = {Models for concurrency}, + booktitle = {Handbook of Logic in Computer Science}, + publisher = {Oxford University Press}, + year = {1995}, + month = {05}, + doi = {10.1093/oso/9780198537809.003.0001}, + url = {https://doi.org/10.1093/oso/9780198537809.003.0001}, + eprint = {https://academic.oup.com/book/0/chapter/421962123/chapter-pdf/52352653/isbn-9780198537809-book-part-1.pdf}, } @inproceedings{Mitchell1977, - author = {Mitchell, Tom M.}, - title = {Version Spaces: A Candidate Elimination Approach to Rule Learning}, - booktitle = {Proceedings of the 5th International Joint Conference on Artificial Intelligence}, - volume = {1}, - pages = {305--310}, - year = {1977} + author = {Mitchell, Tom M.}, + title = {Version Spaces: A Candidate Elimination Approach to Rule Learning}, + booktitle = {Proceedings of the 5th International Joint Conference on Artificial Intelligence}, + volume = {1}, + pages = {305--310}, + year = {1977} } @article{Mitchell1982, - author = {Mitchell, Tom M.}, - title = {Generalization as Search}, - journal = {Artificial Intelligence}, - volume = {18}, - number = {2}, - pages = {203--226}, - year = {1982}, - doi = {10.1016/0004-3702(82)90040-6} + author = {Mitchell, Tom M.}, + title = {Generalization as Search}, + journal = {Artificial Intelligence}, + volume = {18}, + number = {2}, + pages = {203--226}, + year = {1982}, + doi = {10.1016/0004-3702(82)90040-6} } @article{Angluin1980, - author = {Angluin, Dana}, - title = {Inductive Inference of Formal Languages from Positive Data}, - journal = {Information and Control}, - volume = {45}, - number = {2}, - pages = {117--135}, - year = {1980}, - doi = {10.1016/S0019-9958(80)90285-5} + author = {Angluin, Dana}, + title = {Inductive Inference of Formal Languages from Positive Data}, + journal = {Information and Control}, + volume = {45}, + number = {2}, + pages = {117--135}, + year = {1980}, + doi = {10.1016/S0019-9958(80)90285-5} } @book{Mitchell1997, - author = {Mitchell, Tom M.}, - title = {Machine Learning}, - year = {1997}, - publisher = {McGraw-Hill}, - isbn = {0070428077} + author = {Mitchell, Tom M.}, + title = {Machine Learning}, + year = {1997}, + publisher = {McGraw-Hill}, + isbn = {0070428077} } @mastersthesis{Calisto2022, - author = {Calisto, Bruna}, - title = {Formalization in {Coq} of the {Standardization Theorem} for {$\lambda$}-calculus}, - school = {Universidade do Minho}, - year = {2022} + author = {Calisto, Bruna}, + title = {Formalization in {Coq} of the {Standardization Theorem} for {$\lambda$}-calculus}, + school = {Universidade do Minho}, + year = {2022} } @book{Sipser2013, @@ -495,19 +495,19 @@ @book{Sipser2013 year = {2013} } @book{AroraBarak09, - author = {Sanjeev Arora and - Boaz Barak}, - title = {Computational Complexity - {A} Modern Approach}, - publisher = {Cambridge University Press}, - year = {2009} + author = {Sanjeev Arora and + Boaz Barak}, + title = {Computational Complexity - {A} Modern Approach}, + publisher = {Cambridge University Press}, + year = {2009}, } @book{Papadimitriou94, - title = {Computational Complexity}, - author = {Papadimitriou, Christos H.}, - year = {1994}, - publisher = {Addison-Wesley}, - address = {Reading, Massachusetts} + title={Computational Complexity}, + author={Papadimitriou, Christos H.}, + year={1994}, + publisher={Addison-Wesley}, + address={Reading, Massachusetts} } @inproceedings{Kildall73,