Gagallium

In a recent paper, Arthur Charguéraud and François Pottier present a formal proof of an OCaml implementation of Tarjan’s union-find algorithm. The proof covers two aspects: first, functional correctness (“the algorithm is correct”), but also asymptotic complexity. For example, one of the results of the paper is that the link function runs in \(O(α(n))\) elementary steps, \(α\) being the inverse of the Ackermann function.

Actually, the complexity results of the paper are not presented using the “big-O” notation, commonly used in asymptotic complexity proofs: the various constants are explicit and manipulated through the proof.

In these blog posts (current, interlude and final), I’ll describe a tentative extension of CFML, the Coq library François and Arthur used for their proof. Its goal is to enable asymptotic reasoning, big-O notations and such to be used to prove complexity of programs.

CFML: verify OCaml programs in Coq

CFML is a Coq library useful to prove properties about OCaml programs. Its typical usage is as follows: (1) write some OCaml code; (2) use CFML’s generator to parse the OCaml code and produce a “characteristic formula”; expressed as a Coq axiom, that describes the semantics of the program; (3) import this formula and write a specification in Coq for the program; (4) prove the specification using CFML tactics. The specifications are expressed using separation logic, a logical framework convenient when talking about mutable data.

Let’s illustrate this by proving correctness of the incr function (a function that increments a reference).

OCaml code:

let incr r =
  r := !r + 1

After calling CFML’s generator, step (2) produces a Coq source file containing the characteristic formula for incr. This formula has the same shape and structure as the OCaml program, which will be useful to read the goals produced by the CFML tactics.

Parameter incr_cf :
  tag tag_top_fun Label_default
    Body incr r =>
    (LetApp _x4 := ml_get r in
               App ml_set r (_x4 + 1);)

The user doesn’t need to read the produced file nor the characteristic formula, though. We’ll just need to Require it at the beginning of our proof.

Step (3) is writing a specification: a pair of a precondition, that must hold for the function to run, and a postcondition, describing the returned value and the state of the memory after executing the function. In our case, before running incr, r must be a reference containing some integer value i; after running incr, r must contain i+1.

Lemma incr_spec :
  Spec incr r |R>> forall (i: int),
    R (r ~~> i) (# r ~~> (i+1)).

Some hairy notations are involved, but basically, (r ~~> i) is the precondition, and (# r ~~> (i+1)) the postcondition. The ~~> notation denotes a “points-to” relation: here, r is a pointer to a memory cell containing the value i. The # means that incr returns unit. Let us prove interactively this specification. To prove a goal of the form Spec foo ..., we first use the xcf tactic to introduce the characteristic formula of foo.

Lemma incr_spec :
  Spec incr r |R>> forall (i: int),
    R (r ~~> i) (# r ~~> (i+1)).
Proof.
  xcf. intros.

The resulting goal is of the form formula pre post, formula being a part of the characteristic formula, pre and post the precondition and postcondition for the corresponding piece of code.

r : loc
i : int
============================
 (LetApp _x4 := ml_get r in
   App ml_set r (_x4 + 1);) (r ~~> i \* \[]) (# r ~~> (i + 1))

We make the proof progress step by step, traversing the program shape, by applying tactics that match the head constructor of formula: here, it’s a LetApp; we use the xapps tactic. If the goal started with a If, we would have used xif, etc. We need another xapp after that, for the App constructor. Finally, what remains to be proven is a “heap implication”, stating that the final memory matches the post-condition.

============================
 # r ~~> (i + 1) \* \[] ===> # r ~~> (i + 1) \* Hexists H', H'

The hsimpl tactic does the job.

Lemma incr_spec :
  Spec incr r |R>> forall (i: int),
    R (r ~~> i) (# r ~~> (i+1)).
Proof.
  xcf. intros.
  xapps. xapp. hsimpl.
Qed.

CFML + time credits: prove algorithmic complexity

We rely on (and admit) the following property of the OCaml compiler: if one ignores the cost of garbage collection, counting the number of function calls and for/while loop iterations performed by the source program is an accurate measure, up to a constant factor, of the number of machine instructions executed by the compiled program.

We thus consider a new kind of heap resource (something that can be put in pre/postconditions): time credits. The program is now required to consume a time credit at each step of computation.

If we produce the characteristic formula for incr with the “-credits” option, its specification and proof becomes:

Lemma incr_spec :
  Spec incr r |R>> forall (i: int),
    R (\$ 1 \* r ~~> i) (# r ~~> (i+1)).
Proof.
  xcf. intros.
  xpay.
  xapps. xapp. hsimpl.
Qed.

What changed? We now have to give one credit (\$ 1) in the precondition of incr, as it performs one step of computation. The credit does not appear in the postcondition: it is consumed by the function. In the proof, we use the xpay tactic to justify that we are indeed able to pay for the computation step.

The complexity of a function is then represented as the number of credits contained in the precondition: that is, how much you have to pay for it to run. Interestingly, credits can also be stored in the heap for later consumption: this enables amortization (a standard reasoning in the literature - e.g. in Introduction to Algorithms by Cormen et al.).

Asymptotic reasoning on time credits

The proof of Union-Find states and tracks explicitly how many credits are needed at every step of the proof. For example, the precondition of find requires “\(α(N) + 2\) credits”. We would like to be able to write instead “\(O(α(N))\) credits”; first to match usual informal algorithmic reasoning, but also to enable asymptotic reasoning, that is, proofs of properties true “for a big enough \(N\)”.

Reasoning with big-Os is also more modular: the exact number of credits an auxiliary function needs may change without impacting proofs using it, as long as the asymptotic bound stays the same.

The prototype extension of CFML I developed tries to address this. Its features are as follows:

• Given an explicit cost function (a “number of credits”), allow to prove an asymptotic “big-O” bound for it. The cost function may be defined after other functions asymptotically bounded by big-Os.
• Allow various manipulations on big-O bounds: composition, parameter transformation, etc.

This does not include for the moment the proof of Swiss-army-knife theorems like the master theorem; but they can now be stated, using the new asymptotic notions.

This seems to be only a matter of writing down the right definitions and lemmas. This is partly true, but it also appears that the “big-O” notation is often used in a quite informal way, so formalizing it requires extra attention on some aspects.

For example, the “\(O\)” notation requires implicitly some notion of “going towards infinity”. When manipulating cost functions with multiple parameters (e.g., “\(f(m,n)\) is \(O(g(m,n))\)”), which notion of “going to infinity” we should choose is not obvious, and all are not equivalent: it’ll depend on later use.

In our example, we could say both \(m\) and \(n\) have to go to infinity. But maybe we will want to fix \(m\) afterwards, and still have \(f(m,n)\) be a \(O(g(m, n))\); in this case we need an other notion of “going to infinity”: \(m \times n + n\) is indeed a \(O(m \times n)\) for both \(m\) and \(n\) growing to infinity, but it is clearly not the case when fixing \(m = 0\)…

New notions introduced in CFML + asymptotic credits

To formalize these notions, and be able to talk more clearly about this little dilemma, we reuse the notion of filter from the literature.

The generic notion of filter describes a way of “going to infinity” in a set (\(\mathbb{Z}, \mathbb{Z}^2, \ldots\)). On \(\mathbb{Z}\), we will have one obvious filter, that will work in any situation, so the benefits of the method are not clear. However, as illustrated above, on \(\mathbb{Z}^2\) (i.e. for functions with two parameters), which notion of “going to infinity” should be used is not clear, and moreover depends on later usage of the specification. Filters allow to formally describe this situation: one can define various filters for \(\mathbb{Z}^2\), and clearly state which is used in a \(O()\).

Following are the new predicates introduced in CFML: filter, and more. They are all needed to understand what’s going on during the proofs, however in simple scripts most of them needn’t be manipulated directly by the user.

Definition filter A := (A -> Prop) -> Prop.
Class Filter {A} (ultimately: filter A).

A filter is a set of sets (a set of elements of type A being of type A -> Prop), that represents a “set of neighborhoods”; in our case, neighborhoods of infinity. The Filter class bundles additional properties that must be satisfied, like e.g. stability by intersection. This definition allows us to write ultimately P, when ultimately is a filter, meaning that P is true at some point “when going towards infinity”.

Definition dominated (ultimately: filter A) (f g: A -> B).

The textbook definition of “\(f\) is \(O(g)\)”, using filters: more or less, exists k, ultimately (fun x => |f x| ≤ k |g x|).

Definition monotonic (leA: A -> A -> Prop) (leB: B -> B -> Prop) (f: A -> B).
Definition monotonic_after leA leB (f: A -> B) (a0: A).

Monotonicity of f wrt. the relations leA on the domain and leB on the codomain. monotonic_after means “monotonic after a0”; usually combined with a filter to have a notion of asymptotic monotonicity.

Definition idominated (ultimately: filter A) leA (f g: A -> B).

A variant of dominated, that we’ll use in practice: it allows more lemmas to be automatic (without side-conditions to prove). idominated _ _ f g basically means that either f and g are \(O(1)\), either dominated _ f g (\(f\) is \(O(g)\)); and g is asymptotically monotonic.

Definition SpecO (ultimately: filter A) leA (g: A -> Z)
                   (spec: (A -> Z) -> Prop) :=
  exists (f: A -> Z),
    (forall x, 0 <= f x) /\
    monotonic _ _ f      /\
    idominated _ _ f g   /\
    spec f.

A wrapper useful to state specifications using big-Os: it basically means “there exists some f function, which is a \(O(g)\), and spec f is true” (plus some necessary additional facts). Usually, spec is of the form Spec .. |R>> ..., i.e. a standard CFML specification.

As an appetizer for the second part, I’ll leave you with two specifications that use big-Os. The first is for our incr function, the second is for a mktree recursive function, that builds a complete tree of depth \(n\) is \(O(2^n)\) time.

Lemma incr_spec :
  SpecO1 (fun F =>
    Spec incr r |R>> forall (i: int),
      R (\$ F tt \* r ~~> i) (# r ~~> (i+1))).

Lemma mktree_spec :
  SpecO (fun n => 2 ^ n) (fun F =>
    Spec mktree (depth: int) (x: a) |R>>
    0 <= depth ->
    R (\$ F depth) (fun (t: tree a) => \[])).