Make the corpus replay's own rules fail, and prove each one bites

[iderex]

The issue this belongs to

#86, and it is not closed by this change. The reason is already written on the issue rather
than restated here: the first item of its produce list names the response
decoding as a target, there is no entry point for one in this tree, and a corpus
directory for it would be the empty-corpus state the same issue asks the build to
redden on.

What changed

The corpus replay landed as four assertions over one fixed directory. Each of
them read tests/fixtures/corpus/, that corpus is healthy, and a rule that has
only ever run against a healthy subject cannot be told apart from a rule that
refuses nothing. Two of #86's four conditions are statements about a run going
RED - that an empty corpus reddens the build, and that a deliberately unhandled
input in a seed reddens it - and neither had ever been watched happening.

The rules now answer instead of asserting. rules(root, named) takes the corpus
root and the target names as arguments and returns the refusals it found, each as
a rule identifier and the subject it names. The gate hands it this tree's corpus
and the names in TARGETS and requires the answer to be empty. Each proof hands
it a root built for exactly one defect and requires the answer to name exactly
that rule and no other.

replay_every_seed(root, call) takes the target function the same way, so a proof
can hand it a target that does not name what it did with a seed and watch the
failure come out of the loop rather than be counted as an answer.

The rules the gate runs and the rules the proofs trip are one function rather than
two. A proof that ran against a second copy of the logic would prove the copy.

Three of the four rule assertions are now one test whose message names which
rules broke and on which subjects, so nothing that was asserted before is
asserted less: what moved is where the rule lives, not what it refuses.

What failure it prevents

A replay that reports a pass for a surface nobody reached. Four states do that
and all four exit zero: a root holding no directory, a directory holding no seed,
a directory with no entry point behind it, and a target with no directory. A
fifth is the loop itself - catching a panic and counting it turns an input the
code cannot name into a line in a report.

This is a guard hardened rather than a defect repaired. No such state has been
observed in this tree; the corpus was healthy before this change and is healthy
after it. What was missing was any run in which a rule here has ever refused
anything.

Evidence

The suite, at the commit being pushed:

cargo test --locked 2>&1 | grep -E '^test result:' | awk '{s+=$4} END {print s" tests passed in "NR" binaries"}'
650 tests passed in 9 binaries

cargo test --locked --test replay_the_seed_corpus
test result: ok. 11 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.02s

Five of those eleven are the rules and the replay over this tree's corpus; six
are the proofs. The count in that binary before and after:

git show origin/main:tests/replay_the_seed_corpus.rs | grep -c '^#\[test\]'
5
git show HEAD:tests/replay_the_seed_corpus.rs | grep -c '^#\[test\]'
11

The other legs of the gate that read this file, run here:

cargo build --locked --all-targets
    Finished `dev` profile [unoptimized + debuginfo] target(s)

cargo clippy --all-targets -- -D warnings -D clippy::all -D clippy::pedantic -D clippy::cargo
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 13.02s

bash .github/format/format.sh check | tail -1
Every tracked source file above is written the way the formatter would write it.

bash .github/invariants/invariants.sh check | tail -1
Every rule above was applied to its subject and refused nothing.

bash .github/doc-paths/doc-paths.sh check | tail -1
Every path these documents name resolves against the tracked set.

One path this change touches:

git diff --name-only origin/main...HEAD
tests/replay_the_seed_corpus.rs

What a guard here refuses, and the proof it bites

Six deliberate removals, one at a time, each reverted before the next. Every run
is cargo test --locked --test replay_the_seed_corpus against the working tree
carrying that one edit. These are runs made by hand rather than something a
reader re-derives from the tree: repeating one means making the same edit.

What was removed	What went red	The rest
the two lines pushing a-directory-holds-no-seed	a_directory_with_no_seed_is_refused	10 passed; 1 failed
the block pushing the-root-holds-no-directory	a_root_with_no_directory_is_refused	10 passed; 1 failed
the loop pushing a-directory-names-no-target	a_directory_naming_no_target_is_refused	10 passed; 1 failed
the loop pushing a-target-has-no-directory	a_target_with_no_directory_is_refused	10 passed; 1 failed
let answer = call(...) replaced by the same call under catch_unwind, falling back to a string	a_seed_the_target_does_not_handle_reddens_the_replay	10 passed; 1 failed
the !answer.is_empty() assertion inside replay_every_seed	a_target_that_answers_nothing_reddens_the_replay	10 passed; 1 failed

Each removal reddened exactly one proof and left the other ten green, which is
what says a proof is about its own rule rather than about the file.

Two of them were also run against the real corpus rather than against a root
built for the purpose, because #86's conditions are about this tree's corpus.
Both edits were reverted and git status is clean at the commit pushed.

Emptying one real corpus directory, which is #86's an empty corpus reddens the build:

mv tests/fixtures/corpus/server-address/* <elsewhere>
cargo test --locked --test replay_the_seed_corpus
test the_corpus_this_tree_carries_breaks_no_rule ... FAILED
test the_named_refusals_are_each_reached_by_a_seed ... FAILED
test result: FAILED. 9 passed; 2 failed; 0 ignored; 0 measured; 0 filtered out

Adding a corpus directory with no entry point behind it, which is the state a
replay walks past while exiting zero:

mkdir tests/fixtures/corpus/a-surface-with-no-entry-point
printf 'anything' > tests/fixtures/corpus/a-surface-with-no-entry-point/a-seed
cargo test --locked --test replay_the_seed_corpus
test every_seed_is_replayed_and_every_target_answers ... FAILED
test the_corpus_this_tree_carries_breaks_no_rule ... FAILED
the corpus directory a-surface-with-no-entry-point names no target this file
can replay. [...] Replaying it as nothing would be a run that reports a pass
for a surface nobody reached.
test result: FAILED. 9 passed; 2 failed; 0 ignored; 0 measured; 0 filtered out

The near-miss beside the panic proof is a test rather than a note.
the_same_root_without_that_seed_replays_green hands the same target the same
root with the one unhandled seed removed and requires a green replay of one seed,
so the red run beside it is about the seed rather than about a target that fails
at everything. the_healthy_root_breaks_no_rule is the same idea for the four
rules: the root each of them is a one-change neighbour of is asserted to break no
rule first, so nothing those proofs report can be attributed to their own base.

What this does not cover

#86 stays open after this. Its first produce item names the response decoding as
one of three fuzz targets and there is no entry point for one in this tree.

No fuzz target and no coverage-guided run. #86 asks for both, and neither is
in this change or in this tree. What is here is the replay half, which is the
part that gates, and it is now proven rather than only asserted.

The unhandled input is proven against a target built for the proof, not against
a parser in this crate. No parser here can be made to panic without changing
it, so the proof supplies a target that fails on one literal byte string. What
that proves is that the replay does not swallow such a failure. It says nothing
about whether any parser in src/ can be driven to one.

A target nobody thought of is still not caught, and cannot be. A surface that
was never named has no corpus directory, so the empty-directory rule has nothing
to fail on. Two such surfaces are named on #86 already and the module
documentation names them where a reader of the file meets them.

Nothing measured performance. The replay binary reports 0.02 seconds and that
is what the harness printed, not a measurement anybody made a claim from.

Who has read it

Nobody but the author. There is no second reader on this board tonight, and the
runs above stand in place of one: six removals each reddening exactly one proof,
two demonstrations against the real corpus, and every gate leg that reads this
file run locally with its verdict pasted.

---

A correction to this body, made after the merge. The sentence that stood at
the second heading above read It does not close #86. The linked-issue parser
matches the verb and the number and does not read the negation in front of them,
so merging this closed #86 as completed with two of its produce items unbuilt.
The issue is reopened and carries the reading. Both sentences here are rewritten
so the number never follows a closing verb, which is what the two landings before
this one did by writing Refs and by leaving the number off the sentence.