musl-verify

Machine-checked functional correctness for part of musl libc, in QCP 2.1.3 and Coq. Annotated sources may arrive before their proofs; a case is verified only when make check re-derives its verification conditions and successfully checks every selected proof from scratch.

make gen        annotated C + strategies -> verification conditions
make            compile every .v -- this is the claim
make check      regenerate, compile, and reject unfinished proofs
make gen MODULE=musl_stdio
make gen CASE=musl_stdio/__stdio_read.c
make check MODULE=musl_stdio
make check CASE=musl_stdio/__stdio_read.c
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.1.3: the release tagged QCP-V2.1.3 (47d4a34), or the main-branch binary refresh of the same day, 2026-09-21 (bd8516c); the tree regenerates, compiles and checks from a clean checkout under either. That is 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.

Two things to know about the revision:

• Why not 2.0/2.1.2. The strtod.c and wcstod.c cases verify the long double -> double/float narrowing returns; symexec only inserts the fp128_to_fp64 / fp128_to_fp32 conversion nodes from the bd8516c binaries on. Every pre-existing case still regenerates and re-checks under bd8516c.
• Where the Rocq libraries sit. In a dune-built checkout they are at _build/default/Rocq/<lib>, while FRAMEWORK expects them at $(QCP_HOME)/Rocq/<lib>. A QCP_HOME whose Rocq/ entries are symlinks into _build/default/Rocq/ (plus one to the checkout’s linux-binary) satisfies the Makefile as-is; set it in CONFIGURE. A checkout whose libraries were built in place (make -C Rocq) is a QCP_HOME as it stands.

make gen now runs scripts/fixgen.py afterwards. It repairs, idempotently, two emission defects in the 2.1.3 generator output, present in both builds above: the goal writer prints the LONGDOUBLE store name the base library spells LongDouble, and the *_def.v embedded proofs predate the current base-library API. This is a QCP generator compatibility layer, not a verified-stdio migration step: it never reads that workspace, copies a contract, or imports a proof. Nothing under VC/ or annotated_C/gen/ needs hand-editing.

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          # regenerate goals and compile every .v
make check    # also reject Admitted outside *_proof_auto.v

The same gen and check targets accept one optional selector:

make gen MODULE=musl_stdio
make gen CASE=musl_stdio/__stdio_read.c
make check MODULE=musl_stdio
make check CASE=musl_stdio/__stdio_read.c

CASE is the path below annotated_C/src; its .c suffix is optional. MODULE and CASE are mutually exclusive. Unknown selectors are rejected instead of silently doing no work. Proofs are developed and owned here; source migration does not copy or overwrite anything below VC/code_proof.

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.

Explicit concurrent stdio cases

clearerr, feof, ferror, fileno and __do_orphaned_stdio_locks use the FILE/identity model and an explicitly selected native adapter. Their Makefile command uses STDIO_CONCURRENT_SYMEXEC (default: ../scratch/stdio-qcp-adapter-build/symexec). The actual __errno_location helper also uses that adapter with its TP-register binding. close_file and __stdio_seek_owned use STDIO_CLOSE_SYMEXEC (default ../scratch/stdio-captured-qcp-build/symexec), an isolated build adding patches 0015 and 0016 for returned callback capabilities and captured contract values; see tools/qcp-patches/captured-close-experiment.json. Other cases retain SYMEXEC. The adapter requires the independently recorded source build and patches in tools/qcp-patches/identified-release-experiment.json. Its source is not claimed to be byte-identical to the QCP 2.1.3 release. Neither the distributed binary nor CONFIGURE is replaced. A checkout with only the release binary must prepare that adapter before checking these cases. clearerr additionally selects --stdio-owned-clear=stdio_probe_clear for its original flags assignment. The orphan traversal selects the actual __pthread_self and a_store profiles; its private chain owns links rather than shared lock words.

The current six-function batch accepts explicit deferred library/platform/tool interfaces; see docs/stdio-conditional-six.md for the contracts and reproduction commands, and docs/stdio-bottom-library-progress.md for the remaining dependency closure. CSV entries retain the conditional result. Complete FILE payload acquisition and release have whole-runtime primitive-boundary preservation proofs; complete C control flow and environment scheduling composition remains deferred.

tests/qcp/ contains regression scripts, C fixtures, independent Coq certificates and counterexamples for these adapters; see tests/README.md. These sources and tools/qcp-patches/ are required to review and reproduce the native extensions. Generated goals, Coq/Python caches, local scratch files and historical run logs are excluded from commits. make clean removes generated verification artifacts and caches while preserving manual proofs and local CONFIGURE.

What make does and does not establish

It checks the generated obligations against each function’s written contract, including early return paths. Calls use the declared callee contracts; make does not by itself establish that every declaration has a matching implementation proof. That dependency closure is tracked separately. The six concurrent stdio callers use the explicit deferred-interface scope described above.

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.

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.

Proofs are developed here. Source synchronization may change annotated C, headers or lib/; regenerate the selected case immediately and update its *_proof_manual.v in this repository. No migration command imports or replaces manual proofs.