fix(849): the verdict gate replaces every unknown state, and proves the clauses that claim to #890
No Assignees
Notifications
Due Date
No due date set.
Dependencies
No dependencies set.
Reference: timothy/ersatztv#890
Reference in New Issue
Block a user
fixes #849
The H10 gate's post-write verification had five routes that all ended the same way: an exemption
success— or a genericpendinga later run re-derives into one — standing over a humanfailure.Two were attempted inside #742 and withdrawn, and that withdrawal shaped this change. The attempt
withheld the exemption by writing a GENERIC
pending, which is exactly what a later run re-derives,so it moved which run posted the forged green rather than stopping it; and it had no retry path,
because this workflow triggers only on
pull_request_targettypes. The fix needs two properties atonce — sticky, so a later run cannot re-derive it, and reconcilable, so a blip does not cost a
head its exemption permanently. Neither the repair sentinel nor a generic
pendinghas both, which iswhy there is now a second sentinel.
Behaviour
success.descriptionstartswithhard-errors, the whole count is lostsuccessstayed currentReconciliation bounds the stall: a later run pages
/statuses/{sha}in full and — only if thathistory contains the sentinel's own row, matched by the
idthe combined read reported — either findsa
Review-verdict:row underneath it (upgrading to the human-only repair sentinel) or finds none andclears it. Sound because the two endpoints disagree: a masked verdict is invisible on the combined
endpoint and still present in the per-POST history.
Review
Six rounds, each finding less than the last. Cross-family (Codex/GPT-5.6) for rounds 1–2, cold
same-family reviewers throughout, plus the author's own passes.
Stated plainly: Codex hit its usage quota, so rounds 3+ had no cross-family reviewer. In its place
a same-family agent ran a MUTATION SWEEP — enumerate every security-bearing clause the diff adds,
disarm each, run the whole suite per mutant. That is a same-family substitute, not an equivalent one.
The sweep is why several rounds exist: 60 mutants, 40 red, 20 survivors on a tree that had already
passed three per-finding review rounds by two model families. It found, among others, that the
head-push fence arm never marked a declined row (its retarget twin was proved; two callers, one
fixture) and that
state=pendingafter a repair is load-bearing — without it a repaired headre-enters the post-POST check and replaces the human-only marker with the weaker one.
Round 4 also caught a regression I introduced in round 3: type-testing the consumed fields and
resolving a failure to
""made a corrupt.creatorread as unattributable, which greened a humanfailurethatorigin/mainhad fail-closed on.Verification
scripts/tests/green (1309); the suite EXECUTES the shippedrun:body, not a paraphrase.test_MUTATION_…bound by a count assertion, so a reworded clausefails loudly rather than measuring the unmutated body. Every clause with a predecessor is mutated
back to it.
unreachability arguments — each is defence in depth behind a filter that makes its input well-formed
for every case a fixture can pose. The sweep independently confirmed that set is exactly right.
/commits/{sha}/statusrows carryid, which therow-identity comparison depends on — the job had only ever read ids from
/statuses/{sha}.Docs
New record
ci.verdict-unverified-write-sentinel. The fence/pending guarantee prose was swept byCONCEPT rather than phrase, per the scope boundary on the issue:
ci.verdict-write-retarget-fence,ci.exemption-provenance,docs/ci-cd.md,docs/remote-state-inventory.md,docs/guard-inventory.mdandCLAUDE.md.Rounds 7-8 (after the body above was drafted)
The first cross-family pass in five rounds found a Blocker and reversed two round-7 fixes:
select(type == "object"), added so a malformed NEIGHBOUR could not kill the step, made anall-unreadable
.statusesarray read as "no verdict exists" — so a docs-only PR walked to theexemption where
origin/mainhad aborted before any write. A green this branch posted andmaindid not.
opening snapshot able only to STRENGTHEN the write.
writer with
code: writecould wear that text and buy an abstention.Rebased onto #889, which landed mid-session and added
scripts/lib/h10-reviewers.sh— a parser thatreads
H10_REVIEWERSout of this very workflow. Verified by hand that it still parses the modifiedfile, resolves an allow-listed account, rejects a non-member, and that #889's own 75 tests pass
against it.
Two independent cold reviews (Codex/GPT-5.6 cross-family, and a cold Claude reviewer in its own worktree) converged on the same class: paths where "this job cannot establish what is on the head" still resolved by leaving the head alone, which protects a real verdict and leaves a forged one. Behaviour: 1. The four page-2 completeness refusals now replace the unknown state too. They were excluded on the reasoning that the probe fires when NO row for this context was on page 1, so there is no green of any provenance to leave standing — self-contradictory, since the only reason page 2 is read is that the row may be beyond page 1, which the probe's own message says. Accepted cost, stated in the record: a head with more CONTEXTS than the 50-row cap stalls every run; measured 2026-08-29, this repo puts 8 on a `main` head, and that case already stalled with an ABSENT check. 2. The no-mark downgrade covers every re-derivable write, not only `success`. Restricting it analysed the wrong PR: the damaging case is one that IS exemptible and got the generic `pending` only from a transient enumeration failure. That description carries no marker, nothing verifies it without a mark, and the next run re-derives it into the exemption with the human row below its own mark — route 2's damage through route 1's condition. `$REPAIR_DESC` stays exempt, being stronger and not re-derivable. 3. The fence branch that cannot trust its retarget count while holding a derived `success` writes the sentinel instead of abstaining. It is reached only after the classification DECLINED to inherit the row the head carries, so posting nothing left that row current; the message said the context "stays absent", true only of a head that had none. 4. Reconciliation needs a WITNESS: it may clear only over a complete history containing the sentinel's own row. `ex_unverified` means the combined endpoint just returned that row and `/statuses/{sha}` keeps one per POST, so a complete-but-empty history contradicts a write that demonstrably happened — and `page_statuses` accepts an empty page 1 as complete, which is what made it reachable. Both reviewers reproduced the clear-then-exempt outcome. The shipped positive test used exactly that impossible fixture, so it was pinning the defect; it now seeds the sentinel row, and an impossible-empty negative plus a witness mutation proof were added. 5. The mid-run "did this row change" comparison now includes the row ID. The two sentinels are byte-identical by design, so a mid-run replacement of one by another was invisible to a state/creator/description triple. Measured 2026-08-29 (Gitea 1.27.1, head736649b3): the COMBINED endpoint carries `id` on every row, ids 14..30 ascending — the job had only ever read ids from `/statuses/{sha}`. Where a server omits it both sides are empty and the comparison degrades to the pre-existing text test. 6. The repair has a FLOOR — it may never write a description weaker than the one this run decided — and is skipped when it would rewrite what is already there. Widening the gate to every write meant a transient post-write read could rewrite a correct `$REPAIR_DESC` carry-forward with the machine-clearable sentinel, reversing the ordering rule the classification chain states. Writing the sentinel and failing the job are separate decisions, which is why `replace_unknown_state` and `replace_unknown_and_die` are two functions: the read refusals were already non-zero exits on `main` and stay red; the fence branch exited 0 there and still does, because an unreadable timeline is an ordinary hiccup and reddening every one is noise this file elsewhere refuses to add. Prose corrected where it now overclaimed: "the green never stands" after the post-POST re-check is wrong — it is live between the POST and the repair, so the check makes a permanent green TRANSIENT; "a later run reconciles this automatically" is wrong in the one case where the replacement costs anything, since finding a masked verdict UPGRADES to the human-only sentinel; and the mutation-proof framing claimed every mutant restores the exact predecessor, when two do, one restores the shape #742 withdrew, and the rest disarm clauses that have no predecessor. The quiet-timeline positive control now counts timeline walks, because a single POST is also what a skipped re-check produces. refs #849 Decisions-Edit: yes Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019T79beF1Ufid3dXju4yqkFTwo more cold reviews — cross-family (Codex/GPT-5.6) and a cold Claude reviewer that ran the mutants itself — converged on two separate things: a remaining class of paths that still left an unknown state standing, and, more importantly, that several clauses this branch claimed as fixes SURVIVED mutation of the exact text they name. ## Behaviour 1. The reconciliation witness matches the CURRENT row's `id`, not merely a row with the sentinel's description. Description alone is satisfied by an OLDER identical sentinel — which is what a fixed point produces — so a read carrying only the earlier row cleared the sentinel while the verdict buried under the current one ended up below the fresh mark. Falls back to the description where the server omits `id`. 2. The two OBSERVED-mutation arms mark a head that carries a row this run declined, instead of only abstaining. They are still right not to post their CLASSIFICATION — computed against a base or head the PR may no longer have — but a declined row must not stay authoritative for the whole window until a successor finishes, and for a PR's FIRST push no successor is queued at all. Scoped to `pre_state` being non-empty, so the common path stays quiet. 3. `replace_unknown_state` RETURNS a status. Its first version ended the failure arm with a successful `echo`, so it reported 0 after both POSTs failed and the fence caller's `exit 0` reported an abstention that had not happened. 4. An `id` difference counts only when BOTH reads supplied one. A response that omits `id` beside one that includes it otherwise reads as a replacement, and this guard's reaction is to abstain — over a row the classification had already declined. 5. Every element and every consumed field of the combined response is type-checked before extraction, and a schema failure routes to the replacement. `.statuses` being an array was checked; its ELEMENTS were not, so one scalar made `select(.context == $c)` hard-error and `set -e` took the step down before any path could mark the head. 6. The path-predicate failure replaces rather than merely exiting, for the same reason. 7. `$UNVERIFIED_DESC` says "Status write", not "Exemption write". It is now written on paths that grant no exemption at all, and it is the operator-facing text of a required check. 8. The no-op-repair skip keeps the human `::error::`. Skipping the WRITE is right — the head already carries the strongest marker — but that message is the only place a reviewer is told their verdict was buried. `raced_why` is a sentence now, not the token `human`. ## Proof The cold reviewer measured three of the six round-2 claims surviving mutation of their own clause, one against the verbatim predecessor from the previous commit. Nine proofs added: the no-mark downgrade's SCOPE (not just the description it writes), the page-2 refusals, the untrusted-fence write, the row-`id` comparison, the repair floor, the no-op skip, both `$own` exclusions, the write-result return, and the both-ids-present rule. Two of those needed the test double to grow: the combined-status stub emitted no `id` at all, so the `ex_id` clause had never once run with a non-empty value; and POSTs always succeeded, so both write helpers' failure arms were unreachable. The `$own` exclusions and the no-op skip are OUTCOME-redundant — mutating either alone leaves the post sequence unchanged, which is how duplicate guards hide each other. Their proofs assert the LOG, because what the exclusions alone decide is whether the job reports a race against its own row. One clause is left deliberately unproven and named as such in the record and the guard inventory rather than counted: the path-predicate failure branch has no fixture that can reach it. ## Also Round 2 left two comment paragraphs duplicated verbatim and a block header narrower than its block; both fixed. Stale prose corrected in the workflow ("dies WITHOUT posting", "post-write verification never runs for it", "this block only runs after a `success`"), `docs/ci-cd.md` ("the fence never re-counts", "the history is read twice" — it is three now), `ci.exemption-provenance` and `docs/guard-inventory.md`. refs #849 Decisions-Edit: yes Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019T79beF1Ufid3dXju4yqkFA fourth cold review of the tip. No Blockers, no High: it enumerated every POST site and every exit and could not construct an input where this branch writes a `success` that `origin/main` would not. ## The arms judged the wrong snapshot `mark_declined_row_if_any`'s three refusals all read `$pre_*` — the FIRST read — while the POST replaces whatever row is CURRENT. So a reviewer's verdict arriving between the two reads slipped past every refusal written to protect it: the base mismatch clears `ex_attributable` so the mid-run abstain declines, `pre_creator` is empty so the allow-list loop declines, and the arm marks a row nobody evaluated. Executed trace, control and case. Both snapshots are consulted now, and either one vetoes. Recovery was not free, which is why it mattered: the next run's reconciliation counts that `Review-verdict:` row as buried and upgrades to the human-only sentinel — exactly the cost the refusal exists to avoid. The arm also marked this job's OWN ordinary machine `pending`. Every PR past its first run carries one, so "kept off the commonest path in this job" was true only of a head with no status at all. Scoped on the DESCRIPTION rather than on `creator: null`, which would also exclude a machine `success` from another workflow — the row this marking exists for. ## Two comments that invited a bug - One still described the round-4 REGRESSION as the intended behaviour ("a malformed row reads as no creator, hence re-derived"), two lines below the block recording that it was fixed. Adjacent comments giving contradictory accounts of one line, and the stale one licenses reinstating it. - The fault token's justification said "no Gitea status field contains a NUL". The token is SOH (0x01). That is not pedantry: `$'\000…'` is the EMPTY STRING in bash, so an editor correcting the code to match the comment would make every legitimately-absent field compare equal to the token and send every clean head down the fail-closed route — the gate would stall every PR. ## Docs The record quoted a predicate that no longer exists (`[ "$ex_desc" != "$pre_desc" ]`, now `$row_replaced`); `docs/ci-cd.md` stated the reconciliation witness unconditionally when the code degrades to a description match where the server omits `id`; one of the six unproven clauses carried a wrong `because` (the conclusion holds via `(.id | numbers) // -1` over a validated array, not via the schema-fault route, which governs a different endpoint's row); and the record's own counts read as a contradiction cold — 20 surviving MUTANTS collapse onto 6 distinct CLAUSES, several clauses admitting more than one disarming edit. The run-by-run provenance moved to the issue, where `docs.no-session-narrative` says it belongs. Two existing mutation proofs lost their binding to the reworded clauses and failed loudly rather than measuring the unmutated body, which is what that count assertion is for. Rebound. refs #849 Decisions-Edit: yes Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019T79beF1Ufid3dXju4yqkFmaindoes not post, and two round-7 fixes that overshot 691a14d039The first cross-family review in five rounds (Codex/GPT-5.6, once its quota reset). It found a Blocker four same-family rounds had missed, and REVERSED two of round 7's fixes — which is the more useful result, because both were made in response to a review and both overshot in the direction the finding pointed. ## The Blocker: dropping unreadable elements became "no verdict exists" Round 3 added `select(type == "object")` so a malformed NEIGHBOUR could not kill the step. When it drops EVERY element, `first // {}` yields `{}`, all `ex_*` read empty, and the job concludes no verdict exists — so a docs-only PR walks straight to the exemption. Measured: `{"total_count":1,"statuses":[7]}` posts `Exempt: docs-only change` here and posted NOTHING on `origin/main`, which raised jq error 5 and aborted under `set -e` before any write. An input on which this branch greens a head that `main` fails closed on, and if that scalar is a mangled rendering of the head's human `failure`, the rejection is what gets greened. The asymmetry is now the rule: a malformed row BESIDE one we did read is noise; a malformed row where we found NOTHING is the only evidence there was. The absence conclusion has to be earned over a list with no unreadable elements in it. ## Two round-7 fixes that overshot - **The arms judged both snapshots.** Round 6's review said they judged `$pre_*` while the POST replaces `$ex_*`; I made both veto, which is the mirror defect — an opening row since REPLACED by a machine `success` still vetoed, so the arm left that success gating the head. They judge the current row alone now. The opening snapshot keeps exactly one job: it can make the write STRONGER, never suppress it. - **The "this job's own output" exclusion keyed on the DESCRIPTION.** A description is not provenance. Any workflow with `code: write` can POST a `creator: null` row and any repository writer can POST one with a creator, either wearing this job's text — so masking a human `failure` with a lookalike `pending` bought an abstention, and the successor re-derived it as ordinary machine output with the rejection below its own mark. Removed; the attempt is recorded because it is the tempting one, and there is no issuer field that could make it safe. ## A guard that could not be reached, folded into the one that can The repair veto turned out unreachable: an `$ex_desc` of `$REPAIR_DESC` with a different `$desc` is caught by the mid-run sentinel guard long before an arm runs, and when `$desc` IS `$REPAIR_DESC` the promotion writes the same string. Rather than keep a guard no fixture can reach — or delete it on the strength of a check three hundred lines away — the invariant is enforced where it is local and provable: the mark carries the strongest description any snapshot shows, then declines to write what is already there. `ci.exemption-provenance` still called the post-final-count window a PERMANENT forged green in its `rule:` frontmatter and body; the post-POST re-count made it transient two rounds ago. refs #849 Decisions-Edit: yes Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019T79beF1Ufid3dXju4yqkF0f1cc2f733to879208d554Review-verdict: MERGEABLE @
d4b36acNine review rounds: cross-family (Codex/GPT-5.6) rounds 1-2 and 8-9, cold same-family throughout, plus a mutation SWEEP over every clause the diff adds (60 mutants, 40 red, 20 survivors) that found what per-finding review did not. Every reachable clause carries a mutation proof bound by a count assertion; six unreachable clauses are enumerated by name in the record rather than counted. CI green on this head; the earlier preflight red was a registry eviction of the pinned CI toolchain image, recovered per the documented runbook and unrelated to this diff.