Tests as Theorems

How it works

You have a library under test. QuickProof sits next to it and lets you write tests that state properties of the code. We call such a test a spec: it still runs on any input, and it can also be proved in Rocq, for every input.

The report as text

$ tools/qp examples rle
[0:00] qp verify: a fresh clone of the proof repository
[0:01] Clight generated again: identical to the committed files
[0:21] build: 10/10 files, 20 s
[0:43] statements compared with the contract: identical

- files changed since the contract: 2; frozen files changed: none
- regenerated code.v: identical to the committed files
- elaborated statement and whole_prog of `rle_decode_safe`: identical to the contract
- `Admitted`/`admit`/`Axiom`/`Parameter`/`Conjecture` in the proof: none

| theorem           | result | axioms                    |
| `rle_decode_safe` | PROVED | 13: standard + VST malloc |

Verdict: PASS (exit 0).

From a spec to a theorem

The diagram above shows the whole flow. It starts with an executable spec, which looks like a test with arbitrary input. The calls nondet_u8(), nondet_u32(), nondet_size() and nondet_bytes() give arbitrary values, integers, bytes and so on, and qp_assume() restricts them to the valid ones. The spec then runs the function under test in its most general case. Do not worry about how fast the spec runs: the goal is not execution but the most general theorem, such as decode(encode(x)) == x for every x, or target(x) == reference(x). qp_assert checks the result.

An example spec, the one that docker run … verify rle in the quick start checks:

/* Law rle_decode_safe: for every input of up to 4 KiB, rle_decode never
   reports more output than the buffer it was given, and never reads or
   writes out of bounds. */
#include <stdlib.h>
#include "quickproof.h"
#include "rle.h"

int main(void) {
    size_t n = nondet_size();          /* any length ...    */
    qp_assume(n <= 4096);              /* ... up to 4 KiB   */
    uint8_t *in = malloc(n);
    if (in == NULL)
        return 0;
    nondet_bytes(in, n);               /* any bytes         */

    uint8_t out[256];
    size_t m = rle_decode(in, n, out, sizeof out);
    qp_assert(m <= sizeof out);

    free(in);
    return 0;
}

QuickProof generates the theorem

Theorem rle_decode_safe : harness_safe whole_prog.

The theorem cannot be proved while some input makes a qp_assert fail: a failing check counts like any other error, such as an access out of bounds. So the theorem relies on the assertions implicitly: it states that the spec is memory safe, and that includes every assertion. qp check first runs the spec on the code, under CompCert’s interpreter and against mutants of the code, so most false or vacuous specs show up before any proof work. qp assemble then translates the code and the spec with clightgen into Rocq, where they can be reasoned about, and pairs them with the standard theorem that the spec is memory safe, admitted at first. What is left is to point an agent system of your choice at that theorem.

None of the code the AI writes needs to be trusted: the check rests on VST and Rocq, and on the trusted parts listed below. Rocq’s kernel checks the proof, VST is proved sound with respect to CompCert’s semantics of Clight, and qp verify checks that the agent changed neither the statement, the spec, the code nor the framework, and added no axioms of its own.

Existing harnesses

QuickProof can also translate existing harnesses into executable specs: libFuzzer targets, AFL++ and honggfuzz harnesses, CBMC proof harnesses and SV-COMP tasks (libFuzzer is stable, the rest is a preview). We recommend not relying on them alone: as properties they tend to be weak, and most of them only check that the code does not crash. What sets QuickProof apart is that a spec is written to be proved, not run, so it can state more general and more interesting properties.

When a property is false

A spec written with QuickProof can turn out to be false, that is, unprovable. There are two reasons: a mistake in the spec, or a bug in the code. Either one is best caught before the proof starts. So run the spec first, natively in C and in the semantics of Clight, with qp check; it also runs the spec against mutants of the code, to make sure the spec checks something at all. If a mismatch turns up, either the spec or the code has to change. There is no way around it, since the proof covers every input; that is how even the least likely bugs get rooted out.

A false spec can still slip past the checks: a finite number of runs may simply miss the input that breaks it. Then the proof does not go through, and the agents come back with that input instead of a proof. When the code is at fault, we patch it, prove the same property on the fixed version and list the patch in the repository.

For the rle example, against a release of the decoder with a bug, the runs find an input of odd length within seconds that makes it write past its buffer. Some zlib specs were false on zlib 1.3.2 as released, and six of those nine bugs are now fixed upstream (the list). The WireGuard specs found that the Linux kernel’s lib/crypto handled lengths of 4 GiB and more wrongly. No caller in the kernel passes such lengths, and the proof is about the code with our two patches.

What you review, and what you trust

Two things deserve your attention: the specs written with QuickProof, and the changes made to the code for the proof. Everything else is checked by tools that time and many experts have tested: Rocq’s kernel checks the proof, VST is proved sound with respect to CompCert’s semantics of Clight, and qp verify compares QuickProof’s environment (the specifications of nondet_*, malloc and qp_assert) with the framework release. The translation of C into Clight by clightgen is one of the steps not proved here; we trust it as everyone who uses CompCert does.

What a proof means

The theorem says that a QuickProof spec is correct for any values of the framework’s generator functions: run under CompCert’s semantics, it never reaches undefined behaviour (an access out of bounds, a use after free, a read of uninitialised memory, a signed overflow) and fails no qp_assert. What it does not state is, for example, anything about parallel runs. The final theorem says that every run is correct, with no undefined behaviour and no failed qp_assert, but not that a run terminates.

The theorem is about C as CompCert defines it for 64-bit x86 Linux (LP64), not about the binary that gcc or clang build. Compiler bugs and other platforms (on ARM, for instance, char is unsigned) are outside it. malloc and free are described abstractly, by VST’s library: the proof holds for any allocator that meets that specification. malloc may return NULL on any call, so the spec and the library must both handle it.

Quick start

The quickest way to see how it works is to check a proof that is already done. The Docker image contains the whole toolchain, QuickProof itself and its examples:

# check the proof of an example, in Docker (a minute or two)
docker run --rm ghcr.io/genproof/quickproof verify rle

In a minute or two you get the verdict PASS. Next, write your first property, or, without Docker, install everything with opam (Install) and follow the recipe. To prove your own code in Docker, see the Docker walkthrough.