musl-verify

Machine-checked functional correctness for part of musl libc, in QCP 2.0 and Coq. Every function here has a separation-logic contract and a proof that its C satisfies it, and make re-derives the verification conditions from the annotated source and re-checks every proof from scratch.

make gen        annotated C + strategies -> verification conditions
make            compile every .v -- this is the claim
make check      refuse an Admitted outside a *_proof_auto.v
make summary    what is in here
make clean      drop everything generated

See ORGANIZATION for the directory layout.

Requirements

Coq 8.20.1. Not Rocq 9.x – QCP does not support it. The build needs coqc, coqdep and coq_makefile, either on PATH or named by COQBIN. The reference toolchain is the one in the coqorg/coq:8.20.1-ocaml-4.13.1-flambda image, so OCaml 4.13.1+flambda.

QCP 2.0, the distribution that ships linux-binary/symexec and linux-binary/StrategyCheck and, under Rocq/, the separation-logic libraries the contracts are written against. Those libraries have to be built: the seventeen -R paths in this project’s Makefile (FRAMEWORK) point into them, and a proof here cannot compile until they have .vo files. Getting the distribution is between you and the QCP authors; its own docs/linux-setup.md, docs/macos-setup.md and docs/windows-setup.md cover installing it.

GNU make, and room to work: the built container image is around 5 GB, and each coqc is memory hungry, which is why JOBS defaults to 4 rather than your core count.

Setup

With the container image

QCP’s distribution root contains a Dockerfile that starts from the coqorg image above, copies QCP to /home/coq/qcp and builds its Rocq libraries. Build it once:

cd /path/to/qcp && docker build -t qcp .

/home/coq/qcp is this project’s default QCP_HOME, so inside that image no configuration is needed. Mount this repository and build:

docker run --rm -it -v "$PWD:/work" -w /work \
  --user "$(id -u):$(id -g)" -e HOME=/home/coq qcp make

Both of those flags earn their place. --user is what makes the output yours: make writes generated goals and .vo files into the working tree, and the image’s own user is coq with uid 1000, so without it everything make produces belongs to somebody else. And once the uid is not the image’s, HOME no longer points at the opam switch the toolchain lives in, so the build stops on [ERROR] Opam has not been initialised before it compiles anything – -e HOME=/home/coq is what avoids that. If your own uid happens to be 1000, neither flag is needed.

Natively

Follow QCP’s setup guide for your platform, then build its Rocq libraries – this is the step that is easy to skip and the one this project depends on. That build reads a CONFIGURE of its own in each of the two directories below; in the reference image both hold just COQBIN= and SUF=, meaning take coqc from PATH. Then, in order:

cd /path/to/qcp/Rocq/unifysl && make depend && make -j5
cd /path/to/qcp/Rocq        && make depend && make -j5

Then tell this project where things are, by copying CONFIGURE.example to CONFIGURE and filling in what differs from the defaults:

QCP_HOME=/path/to/qcp
COQBIN=/path/to/coq/bin/
JOBS=8

CONFIGURE is local and untracked; every line in it is optional.

Checking that it worked

make          # regenerates the goals, then compiles every .v
make check    # no Admitted outside a *_proof_auto.v

A clean make is the whole claim of this repository. If it fails, nothing here is established, so treat a red build as a result and not as an environment problem to route around.

_CoqProject is generated by make from what is on disk; do not edit it.

What make does and does not establish

It establishes that each function satisfies the contract written above it, for every input the precondition admits, on every path including the ones that return early – and that the contract a caller assumes about a callee is the one the callee’s own file proves.

Two things ride along and are worth stating plainly.

QCP’s solver is trusted. Obligations discharged automatically during symbolic execution land in *_proof_auto.v, which stays Admitted by design: a receipt for work the tool did, not a debt. make check exempts those files and nothing else. The upstream human verification project ships its own the same way.

Specification strength is not measured here. make proves the code meets the spec. It cannot prove the spec says anything interesting; a contract that promises almost nothing is easy to satisfy and would pass. Judging that means reading the contracts, or breaking the code on purpose and checking that the proofs stop going through.

Regenerating before checking, and why it matters

make gen runs symbolic execution over the stored annotated C and overwrites the goals; only *_proof_manual.v survives, because symexec will not overwrite a manual proof that exists. So a proof in this project is checked against obligations derived from the C that is in this project, not against obligations recorded alongside it.

That is stricter than it sounds. A checker that compiles .v files as it finds them and never re-derives will accept a tree carrying a _goal.v that its own annotated C no longer produces – edit the annotations after the last symexec run and nothing complains. Here that cannot happen, and it has already cost one case its most recent proof: regenerating its goal from its own stored C gave a different obligation than the proof closed, so an earlier version that did reproduce went in instead.

Contributing a verified case

A case is one C file and may define several functions; all of them are verified, and the file’s header comment names them. ORGANIZATION says which files are sources and which make gen regenerates – add only sources.

Three things a contribution has to satisfy.

A clean make and a clean make check, from make clean. Not a build that works incrementally on your machine.

No assumed contract left unproved. If a case assumes a contract for a callee and no file in this repository proves the callee against that same contract, the case proves an implication rather than the function. Such a case is held back rather than shipped with a caveat, and lands once its callee does. Two callers assuming mutually incompatible contracts for the same unproved callee is the same problem twice: at most one can survive that callee’s proof.

Manual proofs may need renumbering here. Goal files are regenerated rather than carried in, and this repository loads every module’s strategies where a tree holding one case loads only that case’s. A wider strategy set can split one obligation into more goals than you saw, and *_proof_manual.v is keyed by split-goal number – so a proof that closed goals 1..10 where you wrote it can need a proof for an inserted goal and the rest shifted. That repair belongs here, in this repository’s copy, and is not a defect in the proof you developed.