package incremental_cycles

  1. Overview
  2. Docs

Formalisation of an Incremental Cycle Detection algorithm

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.

OCaml library

API documentation

Interactive demo!

To install the library using opam:

opam pin incremental_cycles https://gitlab.inria.fr/agueneau/incremental-cycles.git

Building the proofs

Installing the dependencies

You 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)
Troubleshooting

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).

Building

make proofs

Organisation of the development

OCaml implementation

The 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_sparse

Coq proofs

The proofs/ directory contains the Coq proofs.

  • IncrementalCycleDetection.v: Exports the toplevel theorems and specifications
Proofs directly relating OCaml functions to their specification
  • BackwardSearch_proof.v: Proof of the backward search: functions visit_backward and backward_search
  • ForwardSearch_proof.v: Proof of the forward search: functions visit_forward and forward_search
  • ComputeCycle_proof.v: Proof of the code that returns the edges of the cycle when one is detected: functions list_of_parents and compute_cycle
  • SimpleSparse_proof.v: Proof of the toplevel functions: add_edge_or_detect_cycle and add_vertex
  • IFold_proof.v: Proof of interruptible_fold
  • RawGraph.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 potential
  • Traversal.v: Generic invariants for a graph search, used by both the backward and forward search
  • Paths.v: Auxiliary definitions for the different notions of reachability in a graph (with levels and marks) used at the specification level
Generic auxiliary definitions, lemmas and tactics
  • GraphModel.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/3
  • SqrtAsymptotics.v: Asymptotic properties of square root
  • LibRelationExtra.v: Lemmas about relations
  • TLCBuffer.v: Auxiliary lemmas about lists, sets that should ultimately be integrated in TLC
  • LibTacticsExtra.v: auxiliary generic tactics
  • HeapTacticsExtra.v: auxiliary tactics to handle time credits