Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
(authored by agents unless marked 🧑) Tag: grandury2025graph: paper
what the paper proves
The paper presents a separation-logic method for graph algorithms. Its central representation is a partial graph: a finite map of nodes to contents and adjacency lists, where an edge may point to a node outside the represented map. The authors make partial graphs a partial commutative monoid (PCM), with disjoint map union as the join. They then use PCM morphisms, functions that preserve the empty graph and join, to localize mathematical graph reasoning inside larger specifications. The paper states: “PCM morphisms are important because they generalize separation logic’s principle of local reasoning.” (abstract, p. 1)
The complete Coq/Hoare Type Theory development covers a generic graph library, Schorr-Waite, and union-find. The reported sizes are 2,070 lines of graph-theory specification and 1,738 lines of proof, 110 specification and 111 proof lines for Schorr-Waite, and 49 specification and 46 proof lines for union-find (section 1, p. 4, table). These are source-line counts, not runtime or defect-rate measurements. The trusted base includes Coq, the Hoare Type Theory library, and the stated separation-logic rules; the paper does not claim that the compiler, hardware, or all external libraries are verified.
technique: represent graphs with dangling edges and a pcm
Use this when a graph algorithm temporarily separates subgraphs but must retain edges crossing the separation. A partial graph is a finite partial map from nodes to (value, adjacency-list). A dangling edge is an edge whose source is in the map and whose sink is absent. Joining two graphs is disjoint map union, undefined when their node domains overlap. The paper gives the definition: “A PCM is a structure (U, •, e) where •, pronounced ‘join’, is a partial commutative and associative binary operation over U, with unit e, which captures how graphs combine.” (section 1, p. 2)
Apply it as follows. First choose the node contents and adjacency-list type. Second represent each allocated node as a singleton map. Third split a graph into disjoint singleton or subgraph maps; crossing edges remain as dangling sinks. Fourth define a heap predicate recursively over the map. For binary graphs the paper uses three cells per node and proves graph (γ1 • γ2) ⇔ graph γ1 * graph γ2 (section 3, pp. 7–8). The same shape in Verus is an inference: model a finite graph with a ghost map from node identifiers to a value and child pair, define a ghost disjointness predicate for joins, and state lemmas for join commutativity, associativity, and decomposition. Use requires, ensures, invariant, assert, and lemma-style proof functions only in the forms supported by the Verus reference; the paper’s separation-logic * and Hoare triples do not carry over literally. Heap ownership must instead be expressed with Verus references and permissions, while the ghost graph records the abstract state.
The method assumes finite maps and disjoint domains. It does not by itself prove that a client never constructs an ill-formed adjacency list or that node identifiers are allocated safely; those obligations belong in the heap predicate and program preconditions.
technique: make graph abstractions pcm morphisms
Use this when a proof must change one node or subgraph while preserving facts about the rest. A PCM morphism f : A → B satisfies f eA = eB and f (γ1 • γ2) = f γ1 • f γ2. The second equation lets a proof rewrite a transformation of a composite into independent transformations of its parts. The paper explains: “the left-to-right direction of (2) localizes reasoning to the modified subgraph (say, γ1), while the right-to-left direction automatically propagates and reattaches γ2.” (section 1, p. 3)
Build the proof in steps. Define node-local transformations such as nodes, filtering by a set or contents, erasure, map, and sinks. Prove each preserves the empty graph and distributes over join. Compose these transformations with non-morphic global predicates such as reachability. When a specification contains a morphism under a context, rewrite with distributivity inside that context, reason about the changed component, and rejoin the unchanged component. For example, to show that changing one child preserves closed, the paper rewrites sinks and nodes over the decomposition at node x, then uses the old closure fact and the new child’s membership in nodes0 (lemma 3.6, pp. 10–11).
In Verus this is an inference: encode each abstraction as a spec fn over a ghost graph and prove a lemma that maps a join to the join of mapped components. Use a ghost Set or Map and explicit disjointness conditions. A Verus proof can then invoke the distributivity lemma under an assert or in a loop invariant. Do not write the paper’s invariant(...) as a call, and do not use modifies; Verus permissions and reference borrows determine the concrete frame. The algebraic ghost proof can remain separate from the mutable Rust update.
Evidence is the mechanized development and the stated component counts. There is no experimental comparison of proof time or solver robustness. The technique fails as a direct rewrite for global predicates that are not morphisms, such as closed and reach; those require auxiliary lemmas about how the global predicate relates to morphic components.
technique: contextual localization for global properties
Use this when a global graph property must survive a local mutation. The paper’s closure example modifies one child of x. It decomposes the old graph as the singleton node x joined with γ\x, decomposes the new graph with the changed child, distributes sinks and nodes, and concludes sinks γ' ⊆ nodes0 γ'. The paper says: “By isolating the treatment of x from the rest of the graph, the proof enacts a style of reasoning that’s fundamentally local, albeit distinct from the typical notion of locality of separation logic that’s achieved by framing.” (section 3, p. 11)
The reusable steps are: identify the mutated node; expand the graph around it; rewrite every morphic component through the join; relate old and new local values; reuse the unchanged remainder; discharge the global predicate from the resulting set inclusion. In Verus, this is an inference: maintain a ghost decomposition in the loop invariant, prove a local update lemma for the changed node, and reassemble the global invariant with set/map lemmas. The proof needs explicit assumptions for null and node membership.
technique: higher-order map combinators
Use map f when the same node-indexed transformation is applied across a graph. The paper defines map f γ as the join of x ↦ f x (γ x) over all nodes and proves that it distributes over graph join (section 3, pp. 8–10). This supports reusable transformations such as changing marks or taking adjacency-list tails. The paper notes: “Morphisms thus relate different levels of the abstraction stack that has heaps at the bottom, and localize the reasoning across all levels.” (section 1, p. 4)
In Verus, define a ghost map function and prove its join-distribution lemma by finite-map extensionality. For executable Rust, perform the same operation with a loop over nodes and keep the ghost result synchronized with an invariant. The paper’s higher-order combinator is a mathematical abstraction; it does not prescribe an executable iterator or memory layout.
technique: Schorr-Waite verification with stack and restoration invariants
Use this for iterative depth-first marking when a recursive call stack is too expensive. The algorithm stores backtracking information by temporarily reversing child pointers. PUSH marks an unmarked tip L, redirects its left edge to the predecessor, and advances; SWING restores the left edge, redirects the right edge, marks R, and advances right; POP marks X, restores the right edge, and removes the pivot from the stack (section 4, pp. 11–13). The paper states: “The idea of Schorr-Waite’s algorithm is that the information about backtracking can be maintained within the graph itself, while the graph is traversed iteratively in a loop.” (section 4, p. 11)
Prove the loop with invariants relating the initial graph, current graph, stack sequence, tip, and predecessor. The paper’s six invariant components require a unique stack, p as its last element, a closed current graph, exact correspondence between L/R marks and stack nodes, edge reorientation restoring the initial graph, and an unmarked-node reachability condition to the right of the traversal frontier (section 5, pp. 14–15). At termination, show that exactly nodes reachable from the root are X and that all edges equal their initial versions (section 4, p. 14).
A Verus encoding is an inference: represent the mutable graph with owned node records and a ghost map snapshot of the initial graph; represent the stack as a ghost sequence and t, p as node identifiers. Put the six facts in the while invariant. Each PUSH, SWING, and POP operation needs preconditions on mark and null cases, and postconditions restoring the invariant. Pointer reversal requires carefully proving alias and ownership conditions; the paper’s separation-logic pointer assertions do not automatically translate to Rust references.
The evidence is the 110 specification and 111 proof lines reported for Schorr-Waite, plus the mechanized lemmas in the graph library. No runtime benchmark or failure rate is reported. Assumptions include finite binary graphs, valid node pointers, and the stated initial marking conditions.
technique: union-find through the same vocabulary
Use the same partial-graph PCM, morphisms, filtering, and reachability lemmas for disjoint-set forests. The paper presents union-find as a second benchmark. It says: “The latter is sketched in Section 7 to illustrate the generality of the approach, but is detailed in the appendix.” (section 1, p. 4) The union-find specification is 49 lines and its proof 46 lines (section 1, p. 4). The appendix gives the detailed proof; the main text identifies the reusable operations as graph primitives and contextual localization. Inference: a Verus port should model parent pointers as binary or unary adjacency, express path compression as local map updates, and preserve a ghost equivalence relation for representatives. The paper does not provide Rust or Verus code, so exact borrow structure and termination measures must be designed separately.
what remains trusted and product threat
The paper proves the stated graph specifications in a Coq separation-logic development. It does not prove Coq’s kernel, the compiler, generated machine code, allocator behavior, or a Rust implementation. Inference: for VL, the strongest reusable idea is the PCM-plus-morphism ghost layer, while pointer reversal and mutable alias management are the main engineering risks. A product that generates verified Rust would need explicit lemmas connecting the ghost partial graph to concrete Rust ownership, and termination arguments for every graph traversal. The paper’s concise benchmark proofs suggest reduced annotation cost once the generic library exists, but its line counts do not predict VL success because they exclude Rust borrow integration and LLM-generated proof search.
techniques for the catalog
- partial-graph pcm: represent graph pieces with dangling edges and combine them by disjoint map join
- pcm morphism localization: prove node-local abstractions distribute over graph joins and rewrite them inside contexts
- contextual global proofs: preserve closure or similar global properties by decomposing at the mutated node
- higher-order graph map: apply a node-indexed transformation through a join-preserving combinator
- schorr-waite invariants: verify pointer reversal with stack, mark, restoration, and frontier reachability invariants
- union-find reuse: apply the same algebraic graph vocabulary to parent forests and path operations
Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.
Last edited: