feat(CFG): Verified implementation of Kildall's algorithm - #782
Draft
quartztz wants to merge 6 commits into
Draft
Conversation
quartztz
marked this pull request as draft
August 7, 2026 16:07
ctchou
reviewed
Aug 7, 2026
Comment on lines
+38
to
+40
| * [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] |
Collaborator
There was a problem hiding this comment.
Please add these references to the file references.bib.
ctchou
reviewed
Aug 8, 2026
Comment on lines
+27
to
+44
| /-- 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 | ||
| /-- 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 |
Collaborator
There was a problem hiding this comment.
I have some questions about the design of CFG:
- Normally the nodes and edges of a graph are taken to be sets (which can be modeled by
SetorFinset). Why do you define them to be lists and then build types from them (NodeOfandEdgeOf)? Scanning the code inKildall.lean, I'm not sure you ever used the fact thatnodesandedgesare lists (rather than sets). - For that matter, do you really need the generality that
nodesandedgesare subsets ofNodeandEdge. Can they simply be the whole types? Then you won't need constraints likesetOf_memanddstOf_mem. - There is something called
Quiverin mathlib:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/Quiver/Basic.html
Would it usable for your purpose? - Why did you put
_at the beginning of_srcOfanddstOf?
Author
There was a problem hiding this comment.
I agree with the fact that the current presentation is very roundabout. I did not know about Quiver, but I feel like applying it would fix these comments: using a single type for Nodes and a quiver to characterize the edges would both remove unneeded fields and make the projections easier.
The _ was a crude way to mark that field as "internal", since the preferred API (that returns a NodeOf g) is defined in terms of it. However, this problem disappears when applying the other changes, so i'll draft a new structure to hopefully fix everything in one go.
Thank you for your comments and for the pointer!
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
As discussed on Zulip, here is an implementation of Kildall's worklist algorithm for solving dataflow equations. The design features a small CFG api, as well as a characterization of correctness in terms of different flavors of fixpoints. Three main theorems show that
Definitions of the structures are in
Analysis/Dataflow/CFG.lean, and the algorithm and proofs are inAnalysis/Dataflow/Kildall.lean. I didn't feel like it fit semantically in any other directory, but I'll be glad to move it if there's better.TODO: fix all lints :(