Browse documentation

Your first property

On this page

You will write a property of a run-length decoder as a C program, find a bug with qp check, fix it, make the property stronger and generate the theorems that a proof has to establish. That part takes about ten minutes, most of it spent waiting for the checks.

The proof itself is written by AI agents, or by a person who knows VST (the Verified Software Toolchain, a program logic for C in Rocq (formerly Coq)), and takes longer. The last two steps show how to hand the theorems over and how to check the proof that comes back.

Every output below is from a real run of qp on this example. Hashes, paths and timings will differ on your machine.

Before you start

You need Coq 8.20.1, CompCert 3.15 and VST 2.15, gcc with AddressSanitizer and UndefinedBehaviorSanitizer, git and Python 3. Install describes the Docker image and the opam setup. Then get QuickProof and put qp on your PATH:

shell
mkdir ~/qp-tutorial && cd ~/qp-tutorial
git clone https://github.com/genproof/quickproof-public.git quickproof
export PATH="$PWD/quickproof/tools:$PATH"

If the toolchain lives in an opam switch, set QP_OPAM_SWITCH to its name instead of changing your PATH.

1. The library

QuickProof works on a library pinned at a commit of a git repository. Make a tiny one: a decoder for run-length encoded data, where the input is a sequence of (count, byte) pairs.

shell
mkdir rle && cd rle

rle.h:

C
#ifndef RLE_H
#define RLE_H
#include <stddef.h>
#include <stdint.h>

/* Decode run-length encoded data. The input is a sequence of (count, byte) pairs.
   Writes at most cap bytes to out and returns the number of bytes written. */
size_t rle_decode(const uint8_t *in, size_t n, uint8_t *out, size_t cap);

#endif

rle.c:

C
#include "rle.h"

size_t rle_decode(const uint8_t *in, size_t n, uint8_t *out, size_t cap)
{
    size_t m = 0;
    for (size_t i = 0; i < n; i += 2) {
        size_t count = in[i];
        uint8_t byte = in[i + 1];
        if (count > cap - m)
            count = cap - m;
        for (size_t k = 0; k < count; k++)
            out[m + k] = byte;
        m += count;
    }
    return m;
}

Commit it and tag the release:

shell
git init -q && git add . && git commit -qm "rle 1.0" && git tag v1.0
cd ..

2. A project

A QuickProof project lives in a workspace, a directory with a projects/ subdirectory. qp new creates one project, pinned to the library's latest release tag:

shell
mkdir ws
qp --workspace ws new rle "$PWD/rle"
created ~/qp-tutorial/ws/projects/rle: upstream ~/qp-tutorial/rle at v1.0 (8badf2581278), framework 6a23ce1
next: CODE/PATCH in project.conf, UNITS in quickproof.conf, laws in harness/, then `qp check rle`

project.conf now records the library's repository and commit. quickproof.conf lists the units: the C files that are translated to Clight, the C dialect that CompCert and VST work with. The library's own files are commented out. In ws/projects/rle/quickproof.conf, remove the # in front of rle.c, so that the list reads:

shell
UNITS=(
  "rle.c=src/rle"
  "$GP/libc/libc.c=src/libc"
  "$GP/libc/malloc_unit.c=src/malloc"
)

3. The property

A property is a C program, a harness, that draws its input from QuickProof's environment and checks the result with assertions. qp and its files call such a harness a law, which is why its first comment starts with "Law". Save this as ws/projects/rle/harness/decode_bounded.c:

C
/* Law decode_bounded: for any input of up to 4096 bytes, rle_decode stays inside its buffers
   and never reports more output than the capacity it was given. */
#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);           /* exactly n bytes */
    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;
}

In the theorem, nondet_size() and nondet_bytes() stand for any value, so the theorem covers every byte string of up to 4096 bytes. qp_assume restricts the inputs and qp_assert states the property. The first comment states it in words; people read it as the claim, so keep it accurate.

4. Check it

Before anyone spends time on a proof, qp check tries to show that the property is false or too weak. It runs the harness natively on random inputs under the sanitizers, under CompCert's reference interpreter (the semantics the theorem is about), and against mutated copies of the library:

shell
cd ws/projects/rle
qp check rle
== VST lint
clean
== native runs
decode_bounded       upstream  FAILED 756/3000, first: seed 3 (signal 6)
== interpreter
decode_bounded       interp    STOP at seed 3: Stuck state / error (ccomp -interp exit 126) -- counterexample to harness_safe
== mutants
failing on the unmutated code (seeds ignored): decode_bounded (76)
...

The property is false. The first failing input, seed 3, is 11 bytes long. Built by hand with QuickProof's native driver (runtime/fuzz_driver.c) under AddressSanitizer, it stops with:

ERROR: AddressSanitizer: heap-buffer-overflow
READ of size 1 at 0x50200000001b thread T0
    #0 in rle_decode rle.c:8
    #1 in harness_main harness/decode_bounded.c:17
0x50200000001b is located 0 bytes after 11-byte region

On an input of odd length, line 8 reads in[i + 1], one byte past the end.

5. Fix the library

Decide what the decoder should do with a trailing odd byte. Here it ignores it:

shell
cd ~/qp-tutorial/rle
sed -i 's/i < n; i += 2/i + 1 < n; i += 2/' rle.c
git commit -qam "rle_decode: ignore a trailing odd byte" && git tag v1.1

Point the project at the new commit and check again:

shell
cd ~/qp-tutorial/ws/projects/rle
sed -i "s|^COMMIT=.*|COMMIT=$(git -C ~/qp-tutorial/rle rev-parse HEAD)   # v1.1|" project.conf
qp check rle
== VST lint
clean
== native runs
decode_bounded       upstream  ok (3000 runs)
== interpreter
decode_bounded       interp    ok (20 runs, no stop; 10 timed out)
== mutants
...
Killed by some harness: **5/14**; 0 of the others only hang (the laws do not claim termination).

The 10 time-outs come from the interpreter's time limit on long inputs.

6. A stronger property

qp check made 14 mutants of rle.c, small changes such as replacing a constant or flipping a comparison, and ran the harness against each. Only 5 of the 14 broken decoders failed it. Among the survivors:

- `rle.c:8` in `rle_decode`: `uint8_t byte = in[i + 1];` with `0`
- `rle.c:5` in `rle_decode`: `size_t m = 0;` with `1`
- `rle.c:11` in `rle_decode`: `for (size_t k = 0; k < count; k++)` with `1`

A decoder that writes zeros instead of the input's bytes satisfies this property. So does one that leaves the first byte of every run unwritten. The property only says that the decoder stays in bounds, and nothing about what it decodes. A proof of it would be true and would miss all of these bugs.

Add a second property that says what the output must be. Save it as harness/decode_exact.c:

C
/* Law decode_exact: for any input of up to 4096 bytes, rle_decode writes exactly what the input
   describes: each pair (count, byte) adds count copies of byte, cut off at the capacity, and the
   return value is the number of bytes written. */
#include <stdlib.h>
#include "quickproof.h"
#include "rle.h"

int main(void)
{
    size_t n = nondet_size();
    qp_assume(n <= 4096);
    uint8_t *in = malloc(n);
    if (in == NULL)
        return 0;
    nondet_bytes(in, n);

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

    size_t want = 0;
    for (size_t i = 0; i + 1 < n; i += 2) {
        for (size_t k = 0; k < in[i] && want < sizeof out; k++) {
            qp_assert(out[want] == in[i + 1]);
            want++;
        }
    }
    qp_assert(m == want);

    free(in);
    return 0;
}

The loop at the end restates the format in the simplest way possible, independently of the decoder, and checks every output byte against it.

shell
qp check rle
Killed by some harness: **13/14**; 0 of the others only hang (the laws do not claim termination).

| harness | killed |
|---|---|
| `decode_bounded` | 5/14 |
| `decode_exact` | 13/14 |

Survivors (an equivalent mutant, or behaviour no harness checks):

- `rle.c:9` in `rle_decode`: `if (count > cap - m)` with `>=`

The one survivor changes nothing: when count equals cap - m, both versions leave it at cap - m. Such a mutant is called equivalent, and no harness can catch it. The properties are ready to be proved. The whole report is in CHECK.md, next to project.conf.

7. Generate the theorems

qp assemble builds the repository in which the proof will be written: the library at the pinned commit, the harnesses, QuickProof as a submodule, the Clight translation of every C file, and one theorem per harness.

shell
qp assemble rle ~/qp-tutorial/rle-proof
git -C ~/qp-tutorial/rle-proof log --oneline
680c253 (HEAD -> master, tag: contract) Contract: rle, 2 theorems (decode_bounded, decode_exact Admitted), upstream a1d2caa78491, quickproof 6a23ce1f4761

The theorem for the second property, at the end of src/contracts/decode_exact.v:

Rocq
Theorem decode_exact : harness_safe whole_prog.
Proof.
Admitted.

whole_prog is decode_exact.c linked with rle.c, and Admitted means there is no proof yet. The commit is tagged contract. From now on the harnesses, the library and the statements are frozen, and the proof may only add Rocq files under src/. The theorem suite in src/contracts/suite.v states both properties together.

8. Check before the proof

qp verify is the check that decides whether a proof counts. Run it now, while there is no proof:

shell
qp verify ~/qp-tutorial/rle-proof
- files changed since the contract: 0; frozen files changed: none
- regenerated code.v: identical to the committed files
- elaborated statement and whole_prog of `decode_bounded`: identical to the contract
- elaborated statement and whole_prog of `decode_exact`: identical to the contract
- elaborated statement and whole_prog of `suite`: identical to the contract
- `Admitted`/`admit`/`Axiom`/`Parameter`/`Conjecture` in the Coq sources of the proof (...): **3** (a proof is delivered without them): src/contracts/decode_bounded.v:55 (Admitted), src/contracts/decode_exact.v:55 (Admitted), src/contracts/suite.v:19 (Admitted)

| theorem | result | axioms |
|---|---|---|
| `decode_bounded` | not proved (Admitted) | 1 (listed in VERIFY.md) |
| `decode_exact` | not proved (Admitted) | 1 (listed in VERIFY.md) |
| `suite` | not proved (Admitted) | 1 (listed in VERIFY.md) |

Verdict: FAIL (exit 1).

It clones the repository again, rebuilds everything and runs the checks listed in the report. All three theorems are still Admitted, so the verdict is FAIL. This run took 28 seconds.

9. The proof

AI agents write the proof: a specification and loop invariants for rle_decode, and proofs of the function and of each main. QuickProof does not include our agents. Give yours the repository and the brief for agents, or instructions like these:

Prove the theorems in src/contracts/ of this repository (Coq 8.20.1, VST 2.15).
Add Rocq files under src/. Do not change the harnesses, the C code, quickproof/, _CoqProject,
the generated code.v files, or any theorem statement.
Done means: `suite` is proved, nothing is Admitted, no axiom is added, and
`quickproof/tools/qp verify .` prints PASS.
A property may be false. If it is, find an input that breaks it and report it; do not weaken anything.

You need not read the proof or trust the agent. Run the check again:

shell
qp verify ~/qp-tutorial/rle-proof

For a complete proof, every theorem shows PROVED with 13 axioms, "standard + VST malloc", and the report ends with:

Verdict: PASS (exit 0).

Check a proof shows a full passing report, from the example in examples/rle, and explains each line. Once proved, decode_exact covers every input of up to 4096 bytes, not only the 3000 that were tested.

Next