Make the proof and mutation gates say what they prove

[jserv]

Three commits, each standing on its own.

Emit verify profiles from the recipe's variables

The frama-c MCP server can run the proofs make verify runs, but only if it loads the same program. Every field that decides that had to be restated by hand, and a hand-written function set is the drift a proof gate cannot afford: it produces a confident answer about a program the build system does not prove.

print-verify-profiles emits that JSON from the variables the verify-<name> recipe consumes. Include directories and force-includes move into shared variables so neither list is spelled twice; they were duplicated at first, under a comment claiming they could not drift.

FRAMAC_ISYSTEM_DIRS is used unquoted rather than through patsubst: its value carries a shell substitution containing a space, so a patsubst over it splits mid-command. That mangling still proves green on any target whose sources need no libc, which is most of them.

Contract the two proved functions that had none

elf_place_segment and futex_uaddr_is_aligned sat in their targets' -wp-fct lists with no ACSL contract, so WP proved only that their bodies commit no runtime error. Nothing there can reject a broken source.

elf_place_segment now states the property its caller depends on: an accepted placement never overlaps the runtime infra reserve, which holds the page-table pool, the shim code and the EL1-only shim data.

Both raise the obligation count, so both floors move with them. MIN_GOALS is a tripwire against an emptied body or a dropped contract, which prove 0 of 0, and it only means that while it sits at the target's baseline. Left alone it would have tolerated verify-elf losing 15 obligations and verify-futexdeadline losing 2, silently.

Make the mutation gate say what it actually proves

A function proved by two targets could only be mutated in the one whose VERIFY_<T>_SRC named its file. hex_nibble lives in src/utils.h and is proved by both verify-elf and verify-rsp precisely because assuming it once was a past mistake, and neither could mutate it. The runner now shadows a mutant header through MUTANT_INCDIR.

The staged path mirrors the original's path under src/ and MUTANT_INCDIR is the staging root, not the copy's parent. Deriving it as the parent got src/utils.h right by luck and every nested header wrong: "proved/netlink.h" fell through -Isrc to the real header, so the run proved unmutated code while reporting a mutation nobody caught. A #error probe now confirms each shadow is reached; the unmutated baseline structurally cannot, since it stages a byte-identical copy.

Mutation runs pass -wp-cache none, because WP stores a timeout as a verdict and replays it, which would be a catch with no prover run behind it.

One thing this makes visible

The gate reported "121 caught", which read as 121 proofs demonstrably rejecting their broken sources. It does not mean that. All 121 are caught by exhausting the prover, not by refutation - [Unknown]/[Failed] never appear in this tree, and raising the budget eightfold to 240s on a quiet host changes nothing.

They still count, and the reasoning is recorded rather than assumed: what makes exhaustion evidence is the baseline proving every goal while each mutant exhausts on the one its own function owns. A merely-hard goal would exhaust in the baseline too, and a failing baseline is fatal rather than scored.

---

Summary by cubic

Makes the Frama-C proof gate and the mutation gate prove what they claim: verify profiles are emitted from the same variables the recipes consume, proved functions gain the contracts their callers rely on, included headers can finally be mutated, and mutation verdicts count only goals the mutated function owns.

Proof gate

• make print-verify-profiles emits the frama-c-mcp JSON from the same variables verify-<name> consumes, so the server can no longer prove a different program; include dirs and force-includes moved into shared FRAMAC_INCLUDE_DIRS / FRAMAC_FORCE_INCLUDES instead of being spelled twice.
• elf_place_segment now states an accepted placement never overlaps the runtime infra reserve, and futex_uaddr_is_aligned states its result in the bit domain; elf_place_segment's assigns clause was dropped after proving only against log_impl's WP-generated frame — check-wp-result.py now reports that frame, matching both wordings Frama-C uses for a missing spec — so VERIFY_ELF_MIN_GOALS went 156→172 with the new contract and back to 159 once the false frame fell, and VERIFY_FUTEXDEADLINE_MIN_GOALS went 128→130.
• check-proof-targets now runs on make check, and BUILD_FLAVOR_GOALS skips print-% goals so that scanner's sub-make cannot wipe a sanitizer build's objects.

Mutation gate

• Header mutants are staged under MUTANT_INCDIR (the staging root, not the copy's parent) so they shadow the real files, and a #error probe confirms each shadow is reached — run serially, since a concurrent sibling could spoil its exit-status answer — because the byte-identical baseline cannot detect a fall-through.
• Mutation runs pass -wp-cache none because WP otherwise replays a stored timeout as a catch; baselines that fail only while the pool is busy are retried serially, and their targets' mutations then run serially too.
• Verdicts report refutation and resource exhaustion separately — every catch here is [Timeout] — and MUTANT_ESCALATE=<n>, off by default, re-runs resource verdicts at a larger budget, reporting MISSED for a mutation that merely turned an easy goal into a slow one. Every open goal must belong to the mutated function, decided by the longest matching name in the target's own proved set and checked by a self-test, with caller obligations naming the callee qualifying for both; coverage is counted by function and by (target, function) pair.

^{Written for commit b6ff88c. Summary will update on new commits.}