This is a formalisation of an incremental cycle detection algorithm, which is a minor variant of the algorithm described in Section 2 of A New Approach to Incremental Cycle Detection and Related Problems by Bender, M. A., Fineman, J. T., Gilbert, S., & Tarjan, R. E. (2015).
NB: the aforementioned paper can alternatively be found on sci-hub. Note also that this is not the version that can be found on arXiv. The arXiv version is quite older and has not been updated with the latest improvements from the authors.
The development in this repository is described in our paper Formal Proof and Analysis of an Incremental Cycle Detection Algorithm, published at ITP'19.
To install the library using opam:
opam pin incremental_cycles https://gitlab.inria.fr/agueneau/incremental-cycles.gitYou need to have opam >= 2.0 installed.
Option A: If you already have an opam switch with Coq >= 8.8 and the coq-released opam repository:
opam install -y --deps-only .Option B: create a fresh local opam switch with everything needed:
opam switch create -y --deps-only --repositories=default,coq-released=https://coq.inria.fr/opam/released .
eval $(opam env)For Option B, if the invocation fails at some point, either remove the _opam directory and re-run the command (this will redo everything), or do eval $(opam env) and then opam install -y --deps-only . (this will continue from where it failed).
make proofsThe src/ directory contains the OCaml implementations that we verify.
simple_sparse.ml implements the cycle detection algorithm for sparse graphs, without strong components (Section 2 of the paper)raw_graph.ml provides an implementation for the graph structure assumed by Simple_sparseThe proofs/ directory contains the Coq proofs.
IncrementalCycleDetection.v: Exports the toplevel theorems and specificationsBackwardSearch_proof.v: Proof of the backward search: functions visit_backward and backward_searchForwardSearch_proof.v: Proof of the forward search: functions visit_forward and forward_searchComputeCycle_proof.v: Proof of the code that returns the edges of the cycle when one is detected: functions list_of_parents and compute_cycleSimpleSparse_proof.v: Proof of the toplevel functions: add_edge_or_detect_cycle and add_vertexIFold_proof.v: Proof of interruptible_foldRawGraph.v: Gives specifications for the Raw_graph interface. Proves them and implements the IsRawGraph predicate for the implementation in raw_graph.ml.GraphFunctionalInvariants.v: Functional invariants of the algorithm (Inv)GraphCostInvariants.v: Potential function for the amortized complexity analysis (net, received, spent...)Graph.v: Separation logic predicate for the whole graph structure IsGraph, including functional invariants and potentialTraversal.v: Generic invariants for a graph search, used by both the backward and forward searchPaths.v: Auxiliary definitions for the different notions of reachability in a graph (with levels and marks) used at the specification levelGraphModel.v: Interface for a standard model of a directed graph, at the logical level. The development is parameterized by any specific logical graph satisfying this interface.GraphModelInst.v: Provides one possible instantiation for GraphModel.v, just to ensure that the interface can be implemented.PowerTwoThird.v: Lemmas about the function x -> x^2/3SqrtAsymptotics.v: Asymptotic properties of square rootLibRelationExtra.v: Lemmas about relationsTLCBuffer.v: Auxiliary lemmas about lists, sets that should ultimately be integrated in TLCLibTacticsExtra.v: auxiliary generic tacticsHeapTacticsExtra.v: auxiliary tactics to handle time credits