Proof Marker Sets

A QEMU proof’s real content is its marker set: the lines the boot must print, the lines it must not, and the exit status QEMU must reach. That set used to be bespoke shell in one tools/qemu-*.sh script per proof. It is now data.

Three artifacts make up a converted proof:

Why data

Mutation-testing an assertion – changing what it expects and confirming the proof turns red – is the only way to know it is not a no-op, and an assertion that reads as passing while proving nothing is a defect family this project keeps hitting. Across 300 hand-written scripts that check could not be run mechanically. Over declarative marker sets it is a loop: make proof-marker-mutation-check builds a synthetic log each set accepts, then perturbs every declared assertion in turn and requires the asserter to reject the result.

Grammar

One directive per line. Blank lines and # comments are free-form. A comment may precede any directive and belongs to it: the rationale a hand-written harness carried for a particular assertion stays attached to the marker that replaced it, because the marker set is now the only record of what the proof proves.

outcome      qemu-proof-outcome.sh
exit-status  1
require      kernel-clean line  '[posix-fcntl] F_GETFL=2'
require      kernel      regex  '^\[posix-fcntl\] F_DUPFD base=[0-9]+ newfd>=10$'
forbid       kernel      text   'panic'
count-eq-2   kernel      text   '[devicemmio-smoke] DeviceMmio.info ok'
require-file terminal    exists
witness      'evidence: id=7 state=ok'

• outcome – qemu-proof-outcome.sh (the proof’s only passing QEMU status is 1) or qemu-startup-stall-guard.sh (the proof accepts 124). It runs before any marker is read, so a stalled boot still exits 3 for the retry harness instead of being reported as a missing marker.
• exit-status – one or more accepted QEMU exit statuses. A set that accepts 124 must declare the stall guard.
• Sense – require, forbid, or count-<op>-<n> where <op> is one of eq, ne, ge, gt, le, lt. A count marker counts lines, matching grep -c.
• Target – kernel (the raw UART log), kernel-clean (the same log with carriage returns stripped), terminal, or either (a match in the kernel or terminal log satisfies it, matching the two-operand grep the scripts used).
• Match kind – line (grep -Fxq, whole line), text (grep -Fq, substring), or regex (grep -Eq, POSIX ERE), each with an optional -i suffix for a case-insensitive match.
• Pattern – always wrapped in one leading and one trailing ', and decoded by stripping exactly one character from each end. Every pattern is therefore representable, including one with significant trailing whitespace, which a bare field would lose to the repository’s no-trailing-whitespace rule.
• require-file – kernel or terminal, exists or nonempty.
• witness – a synthetic log line for the mutation gate only. It asserts nothing about a real run; supply one when a regex marker’s witness cannot be synthesized, or when several markers describe one evidence line.

The asserter runs the same grep invocation each match kind names, so a converted proof keeps the exact matching semantics of the script it replaced rather than re-implementing them in another regex dialect.

Adding a proof

1. Write the manifest and the Makefile test-* target as before. The recipe’s assertion line stays tools/qemu-<name>-smoke.sh assert $$log $$term_log $$status.
2. ln -s qemu-marker-proof.sh tools/qemu-<name>-smoke.sh.
3. Write tools/proofs/qemu-<name>-smoke.markers.
4. make proof-marker-mutation-check – every assertion must be shown to be load-bearing.
5. make proof-registry-refresh – records the new proof’s manifest, ISO, device profile, timeout, and accepted statuses.

A proof with logic the grammar cannot express keeps a hand-written script; that is the supported case, not a failure. Its assertions are then outside the mutation gate, so prefer the data form when the proof is a marker list.

The registry

docs/workflow/proof-registry.toml is derived from the Makefile, never edited by hand, and refreshed with make proof-registry-refresh. Per proof it records the manifest, ISO, named device profile, timeout, harness, marker set, accepted statuses, and any target-scoped Makefile variable override. [profiles] resolves profile names to QEMU arguments, [variables] resolves the Makefile variables those arguments reference, and [host_probed] names the ones a runner must evaluate itself (KVM availability) together with their definitions.

make proof-registry-check fails when the registry and the Makefile disagree, and additionally reconstructs sampled proofs’ QEMU command lines from registry data alone and compares them against make --dry-run. That is what makes “consumable by a non-make runner” a check rather than a claim; python3 tools/qemu_proof_registry.py --verify-launch 232 sweeps every registered proof.

Targets the single-boot model does not describe – multi-boot sequences, or recipes whose assertion entry point is not <harness> assert – are listed under [skipped] with a reason rather than silently omitted.