# 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:

| Artifact | Role |
| --- | --- |
| `tools/proofs/<harness>.markers` | the assertions, as data |
| `tools/qemu-<name>-smoke.sh` | a symlink to the shared asserter |
| `docs/workflow/proof-registry.toml` | how to start the proof, derived from the Makefile |

## 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.