fix(849): restore 13 proofs round 9 deleted by accident, and one comment that argued both sides

The round-9 cross-family review found no Blockers and no Highs, and independently confirmed the clause deletion it was asked to check. What it did find is that round 9 removed FIFTEEN test definitions and added four — a net loss of eleven — where the commit message claimed two. Verified against the parent: 227 definitions before, 216 after. The cause is mechanical and worth naming, because it produces a green suite: the round-9 edits replaced whole source RANGES (`s[:start] + new + s[end:]`) whose end anchor was the next test rather than the end of the one being rewritten, so everything in between went with it. The suite then passed because the tests were GONE, not because the code was right — the exact shape this issue exists to prevent, reproduced in its own test file. Among the casualties were round 4's proofs for two earlier BLOCKERS: - `test_a_generic_PENDING_with_no_mark_also_becomes_the_sentinel` and its mutation, which pin the no-mark downgrade covering every re-derivable write rather than only `success`; - `test_a_MALFORMED_creator_FIELD_...` and its mutation, which pin a wrong-typed field taking the fault route rather than reading as absent and licensing a re-derive. Also lost: both `$own`-exclusion proofs, the no-op-repair skip proof, the id-asymmetry pair (the reviewer's named example), and two write-failure propagation proofs. All 13 unintended deletions are restored verbatim from the parent commit and ALL PASS against round 9's code, so nothing had regressed — the harm was the missing evidence, not the behaviour. The two deletions that WERE intended stay deleted: a test superseded by `..._still_refuses`, and the positive control round 9 inverted. Prose: the comment above the unreadable-element guard still argued a malformed neighbour is safe noise once the target row was found, eleven lines above code that now refuses unconditionally — two adjacent blocks giving opposite accounts of one rule, and the stale one licenses reinstating the Blocker. Refs: #849 Decisions-Edit: yes Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019T79beF1Ufid3dXju4yqkF
2026-08-30 07:10:21 +02:00
parent c2c70e50ad
commit d4b36ac232
2 changed files with 330 additions and 14 deletions
@@ -648,18 +648,24 @@ jobs:
            if [ -z "${row//[[:space:]]/}" ]; then
              replace_unknown_and_die "The commit statuses for ${SHA:0:7} parsed as an array but could not be read row by row, so any ${CONTEXT} on this head can neither be read nor re-derived."
            fi
-            # DROPPING AN UNREADABLE ELEMENT IS SAFE ONLY ONCE THE TARGET ROW HAS BEEN FOUND.
-            # `select(type == "object")` was added so a malformed NEIGHBOUR could not kill the step —
-            # but when it drops every element, `first // {}` yields `{}`, every `ex_*` reads empty,
-            # and the job concludes NO VERDICT EXISTS. A docs-only PR then walks straight to the
-            # exemption. `origin/main` raised jq error 5 on the scalar and `set -e` aborted before any
-            # POST, so this is an input on which this branch posts a green that `main` does not — and
-            # if that scalar is a mangled rendering of the head's human `failure`, the green stands
-            # over a rejection.
+            # NO UNREADABLE ELEMENT MAY BE DROPPED SILENTLY, whether or not a target row was found.
+            # `select(type == "object")` above exists so a malformed element cannot CRASH the read —
+            # that part is right, and it is all it does. What it must not become is a licence to
+            # judge the head over the rows that happened to survive it.
            #
-            # The asymmetry is the rule: a malformed row beside a row we DID read is noise, and a
-            # malformed row where we found nothing is the only evidence there was. So the absence
-            # conclusion has to be earned over a list with no unreadable elements in it.
+            # Two ways that went wrong, both measured. When the filter drops EVERY element,
+            # `first // {}` yields `{}`, every `ex_*` reads empty, and the job concludes NO VERDICT
+            # EXISTS, so a docs-only PR walks to the exemption. And when it drops one element beside
+            # a row it DID read, that element still cannot be shown to be a different context — so it
+            # may be a mangled rendering of this head's own rejection, and the one-row-per-context
+            # invariant that would rule that out is exactly what a schema-corrupt response has
+            # already broken. `origin/main` raised jq error 5 on such a body and `set -e` aborted
+            # before any POST; both shapes were inputs on which this job posted a green that `main`
+            # did not.
+            #
+            # So the rule is unconditional: any unreadable element, or a failure to count them,
+            # refuses. The cost is a stall on a head the registry serves badly — the correct
+            # direction for a required check, which must withhold a green rather than grant one.
            unreadable=$(printf '%s' "$json" | jq -r '[(.statuses // [])[] | select(type != "object" or ((.context | type) != "string"))] | length' 2>/dev/null) || unreadable=""
            case "$unreadable" in ''|*[!0-9]*) unreadable=1 ;; esac
            # ANY UNREADABLE ELEMENT, whether or not a target row was also found. Round 8 scoped this
@@ -5888,9 +5888,9 @@ def test_a_MALFORMED_element_BESIDE_a_readable_row_still_refuses(tmp_path):
    """An element whose `.context` cannot be read cannot be shown to be a DIFFERENT context.

    Round 8 dropped malformed neighbours once a target row was found, reasoning that a bad row beside
-    a good one is noise. It is not: the unreadable element may be a mangled rendering of this head's
-    own rejection, and the one-row-per-context invariant that would rule that out is exactly what a
-    schema-corrupt response has already broken.
+    a good one is noise. It is not, and the rule is now unconditional: the unreadable element may be a
+    mangled rendering of this head's own rejection, and the one-row-per-context invariant that would
+    rule that out is exactly what a schema-corrupt response has already broken.

    This fixture is the one round 8 shipped as a POSITIVE control — a scalar beside an off-list
    `success` — and it was the failing case: the branch re-derived the off-list row and POSTed an
@@ -6588,6 +6588,316 @@ def test_MUTATION_concluding_absence_over_unreadable_elements_greens_the_head(tm
    )


+def test_a_FAILED_sentinel_write_on_the_fence_path_FAILS_the_job(tmp_path):
+    """The write helper reports whether it wrote, and the fence caller acts on it.
+
+    Its first version ended the failure arm with a successful `echo`, so it returned 0 after BOTH
+    POST attempts failed and the caller's `exit 0` beside it reported an abstention that had not
+    happened — while whatever the head carried stayed authoritative.
+    """
+    posted, r = _run_classify(tmp_path / "fixed", _emitting("docs/a.md"), timeline_mode="unreadable", post_fails=True)
+    assert posted is None, "the stub was supposed to reject every POST"
+    assert r.returncode != 0, (
+        "the job reported a clean abstention while the head was left unmarked and its POSTs had all "
+        f"failed:\n{r.stdout[-900:]}"
+    )
+    assert "COULD NOT WRITE THE UNVERIFIED SENTINEL" in (r.stdout + r.stderr), (
+        f"the job went red, but not because the sentinel write failed:\n{r.stdout[-900:]}"
+    )
+
+
+def test_a_generic_PENDING_with_no_mark_also_becomes_the_sentinel(tmp_path):
+    """The no-mark downgrade covers every re-derivable write, not only the exemption.
+
+    The damaging PR is one that IS exemptible and got the generic `pending` only from a transient
+    enumeration failure. Its description carries no marker, the post-write check does not run without
+    a mark, so a verdict landing in the write window is buried and the NEXT run re-derives that
+    `pending` into the exemption with the human row below its own mark.
+
+    The fixture is that PR: the enumerator exits 1 (generic `pending`) AND the status history cannot
+    be read (no mark).
+    """
+    posted, r = _run_classify(
+        tmp_path,
+        "#!/usr/bin/env bash\n" + DOCS_ONLY + "exit 1\n",
+        history_mode="premark-page1-error",
+    )
+    assert posted is not None and posted["description"] == UNVERIFIED_DESC, (
+        "a generic `pending` nothing could verify was posted with its re-derivable description "
+        f"intact: {posted}\n{r.stdout[-900:]}"
+    )
+
+
+def test_a_MALFORMED_creator_FIELD_on_the_existing_row_is_unknown_state_not_an_absent_one(tmp_path):
+    """A wrong TYPE is not an absent value, and reading it as one is a licence to re-derive.
+
+    Round 3 type-tested the four consumed fields and resolved a failure to `""`. For `.creator` that
+    means "no creator", i.e. unattributable, i.e. re-derive — so a head carrying a human `failure`
+    with a corrupt creator was greened. `origin/main` died on `.creator.login` BEFORE writing
+    anything, which is fail-closed, so this was a direction regression rather than a residual.
+
+    The rationale that produced it came from #763, whose site is the POST-WRITE filter: there, dying
+    leaves a green already published, so dropping the row is the safe direction. Here the alternative
+    is dying before any write. The deferral rationale did not transfer.
+    """
+    posted, r = _run_classify(tmp_path / "fixed", _emitting("docs/a.md"), status_mode="malformed-creator-field")
+    assert posted is not None and posted["description"] == UNVERIFIED_DESC, (
+        f"a corrupt creator on a human rejection produced {posted}, not the sentinel\n{r.stdout[-900:]}"
+    )
+    assert r.returncode != 0, "an unreadable row must still fail the job"
+
+
+def test_an_ID_that_appears_on_only_ONE_read_is_not_a_replacement(tmp_path):
+    """One response omitting `id` beside one that includes it is not evidence of a mid-run write.
+
+    The row, its state, its creator and its description are all unchanged; only the SERVER's
+    reporting differs. Treating that as a replacement makes the run abstain — leaving current a row
+    the classification had already declined to inherit, which is the direction that costs something.
+    """
+    posted, r = _run_classify(tmp_path / "fixed", _emitting("docs/a.md"), status_mode="id-appears-on-second-read")
+    assert posted is not None, f"an asymmetric id report was read as a mid-run replacement:\n{r.stdout[-900:]}"
+    assert posted["state"] == "success" and posted["description"].startswith("Exempt:"), (
+        f"expected the off-list row to be re-derived into the docs-only exemption; got {posted}"
+    )
+
+
+def test_an_observed_retarget_does_NOT_bury_an_ALLOWLISTED_reviewers_verdict(tmp_path):
+    """ "Declined" is decided against THIS event's base, so it is not a judgement about the row.
+
+    A genuine verdict recorded for another base is declined here and is still the right answer for
+    the base it names — the successor run for that base short-circuits on it. Burying it costs a
+    manual re-post on an ordinary retarget-onto-the-reviewed-base flow. An OFF-list row is what the
+    marking exists for and is still marked, which the sibling test above asserts.
+    """
+    posted, r = _run_classify(
+        tmp_path,
+        _emitting("docs/a.md"),
+        status_mode="existing:success",
+        status_creator="timothy",
+        status_desc="Review-verdict: MERGEABLE @ a9e3e23 (base: probe/scratch)",
+        timeline_mode="moves:0,1",
+    )
+    assert posted is None, (
+        f"a reviewer's verdict for another base was buried by an abstaining run: {posted}\n{r.stdout[-900:]}"
+    )
+
+
+def test_an_observed_retarget_does_NOT_bury_the_repair_sentinel(tmp_path):
+    """The arms may mark, but never with a weaker description than the head already carries.
+
+    `$REPAIR_DESC` is human-clearable only; `replace_unknown_state` writes the machine-clearable one.
+    A head carrying the repair sentinel has a non-empty `pre_state`, so the bare scope test fired on
+    it and inverted the ordering the repair site's own floor exists to protect — one mechanism, three
+    writers, and only two had the rule.
+    """
+    posted, r = _run_classify(
+        tmp_path,
+        _emitting("docs/a.md"),
+        status_mode="existing:pending",
+        status_creator=None,
+        status_desc=REPAIR_DESC,
+        timeline_mode="moves:0,1",
+    )
+    assert posted is None, f"the repair sentinel was overwritten by an abstaining run: {posted}"
+
+
+def test_MUTATION_comparing_ids_WITHOUT_requiring_both_makes_the_run_abstain(tmp_path):
+    """Disarming the presence guards alone, leaving the inequality."""
+    mutant, rm = _run_classify(
+        tmp_path / "mutant",
+        _emitting("docs/a.md"),
+        status_mode="id-appears-on-second-read",
+        mutate=(
+            'if [ -n "$ex_id" ] && [ -n "$pre_id" ] && [ "$ex_id" != "$pre_id" ]; then',
+            'if [ "$ex_id" != "$pre_id" ]; then',
+        ),
+    )
+    assert mutant is None, (
+        "the mutant did not abstain, so the both-present requirement is not what keeps an asymmetric "
+        f"id report from reading as a replacement: {mutant}\n{rm.stdout[-900:]}"
+    )
+
+
+def test_MUTATION_dropping_the_no_op_repair_SKIP_re_posts_what_is_already_there(tmp_path):
+    """The skip, isolated: a repair that would write what this run already wrote is not a repair.
+
+    The fixture reaches it the ordinary way — a carry-forward `$REPAIR_DESC` write whose post-write
+    walk then fails, so the floor pins `repair_desc` to the description just POSTed.
+    """
+    _run_classify(
+        tmp_path / "fixed",
+        _emitting("docs/a.md"),
+        status_mode="existing:pending",
+        status_creator=None,
+        status_desc=REPAIR_DESC,
+        history_mode="postwrite-page1-error",
+    )
+    assert len(_posted_sequence(tmp_path / "fixed")) == 1, (
+        f"the shipped code re-posted: {_posted_sequence(tmp_path / 'fixed')}"
+    )
+
+    _run_classify(
+        tmp_path / "mutant",
+        _emitting("docs/a.md"),
+        status_mode="existing:pending",
+        status_creator=None,
+        status_desc=REPAIR_DESC,
+        history_mode="postwrite-page1-error",
+        mutate=('if [ "$raced" -gt 0 ] && [ "$repair_desc" = "$desc" ]; then', "if false; then"),
+    )
+    mseq = _posted_sequence(tmp_path / "mutant")
+    assert len(mseq) == 2 and mseq[0] == mseq[1], (
+        "the mutant did not duplicate the row, so the skip is not what suppresses it and the "
+        f"assertion above proves nothing about it: {mseq}"
+    )
+
+
+def test_MUTATION_dropping_the_OWN_exclusion_on_the_UNVERIFIED_arm_reports_a_phantom_other_run(tmp_path):
+    """The twin, on the arm that counts the reconcilable sentinel.
+
+    A run carrying the unverified sentinel forward POSTs it, then its own row sits above the mark. If
+    the arm does not exclude it, the job reports that ANOTHER run recorded an unverified write on this
+    head — a second run that does not exist.
+    """
+    _, r = _run_classify(
+        tmp_path / "fixed",
+        _emitting("docs/a.md"),
+        status_mode="existing:pending",
+        status_creator=None,
+        status_desc=UNVERIFIED_DESC,
+    )
+    assert "another run recorded an unverified write" not in (r.stdout + r.stderr), (
+        f"the shipped code reported a phantom second run:\n{r.stdout[-900:]}"
+    )
+
+    _, rm = _run_classify(
+        tmp_path / "mutant",
+        _emitting("docs/a.md"),
+        status_mode="existing:pending",
+        status_creator=None,
+        status_desc=UNVERIFIED_DESC,
+        mutate=(
+            'select((.creator == null) and ((.description // "") == $ud)\n'
+            '                     and ((.description // "") != $own))] | length\')',
+            'select((.creator == null) and ((.description // "") == $ud))] | length\')',
+        ),
+    )
+    assert "another run recorded an unverified write" in (rm.stdout + rm.stderr), (
+        "the mutant did not report a phantom run, so the `$own` exclusion on the unverified arm is "
+        f"not what prevents it:\n{rm.stdout[-900:]}"
+    )
+
+
+def test_MUTATION_dropping_the_OWN_row_exclusion_reports_a_race_that_did_not_happen(tmp_path):
+    """`--arg own "$desc"` keeps this job from counting the row it has just written.
+
+    The two exclusions are OUTCOME-redundant with the no-op skip above — drop one and the other
+    still suppresses the duplicate POST — which is exactly the shape where two guards hide each
+    other. What the exclusion alone decides is the REPORT, and after the skip learned to keep the
+    human `::error::` that report is a false alarm: a run whose own carry-forward row is counted
+    tells a reviewer their verdict was overwritten when nothing raced it.
+
+    So this asserts the log, not the post sequence, and that is the honest discriminator rather than
+    a weaker one. The head carries `$REPAIR_DESC`, the history is otherwise empty (mark 0), and this
+    run's own POST lands above the mark.
+    """
+    _, r = _run_classify(
+        tmp_path / "fixed",
+        _emitting("docs/a.md"),
+        status_mode="existing:pending",
+        status_creator=None,
+        status_desc=REPAIR_DESC,
+    )
+    # `::error::A human` and not the bare phrase "was overwritten": the classification's own REASON
+    # string for a carry-forward run also contains that phrase, so matching it would report the
+    # shipped code as failing on text it is supposed to print.
+    assert "::error::A human" not in (r.stdout + r.stderr), (
+        f"the shipped code reported a race against its own row:\n{r.stdout[-900:]}"
+    )
+
+    _, rm = _run_classify(
+        tmp_path / "mutant",
+        _emitting("docs/a.md"),
+        status_mode="existing:pending",
+        status_creator=None,
+        status_desc=REPAIR_DESC,
+        mutate=(
+            'or ((.creator == null) and ((.description // "") == $rd)\n'
+            '                    and ((.description // "") != $own))',
+            'or ((.creator == null) and ((.description // "") == $rd))',
+        ),
+    )
+    assert "::error::A human" in (rm.stdout + rm.stderr), (
+        "the mutant did not report a false race, so the `$own` exclusion on the repair-sentinel arm "
+        f"is not what prevents it:\n{rm.stdout[-900:]}"
+    )
+
+
+def test_MUTATION_ignoring_the_write_result_reports_a_clean_abstention(tmp_path):
+    """The predecessor: `replace_unknown_state` followed by an unconditional `exit 0`."""
+    _, rm = _run_classify(
+        tmp_path / "mutant",
+        _emitting("docs/a.md"),
+        timeline_mode="unreadable",
+        post_fails=True,
+        # MUTATES THE CALLER'S REACTION, not the `if` itself: dropping the `if` keyword leaves a
+        # dangling `then`/`fi` and the step dies on a syntax error, which is a red for the wrong
+        # reason. Turning the failure exit into a clean one is exactly the predecessor's OUTCOME and
+        # isolates the decision.
+        mutate=(
+            "  # THE SENTINEL WRITE FAILED, so nothing marked this head and whatever it carries is still\n"
+            "  # authoritative. Exiting 0 here would report an abstention that did not happen.\n"
+            "  exit 1",
+            "  exit 0",
+        ),
+    )
+    assert rm.returncode == 0, (
+        "the mutant still failed the job, so the caller is not what turns a failed write into a red "
+        f"run and the test above proves nothing about it: rc={rm.returncode}\n{rm.stdout[-900:]}"
+    )
+
+
+def test_MUTATION_reading_a_malformed_FIELD_as_absent_greens_a_rejection(tmp_path):
+    """The round-3 form restored: type-test, then fall back to the empty string."""
+    posted, rm = _run_classify(
+        tmp_path / "mutant",
+        _emitting("docs/a.md"),
+        status_mode="malformed-creator-field",
+        mutate=(
+            'elif (.creator | type) == "null" then "" else $f end\')',
+            'else "" end\')',
+        ),
+    )
+    assert posted is not None and posted["state"] == "success", (
+        "the mutant did not green the rejection, so the schema-fault route is not what prevents it "
+        f"and the test above proves nothing about it: {posted}\n{rm.stdout[-900:]}"
+    )
+
+
+def test_MUTATION_restoring_the_SUCCESS_only_no_mark_downgrade_leaves_a_re_derivable_pending(tmp_path):
+    """The exact predecessor from this branch's own previous commit, restored.
+
+    This is the mutation the round-2 suite did not have: the nearest proof mutated the DESCRIPTION
+    the downgrade writes, not its SCOPE, and its fixture ran a succeeding enumeration — so
+    `state=success` there and the `success`-only predicate fired identically. Nothing reached the
+    downgrade with `state=pending`, and the predecessor survived the whole suite.
+    """
+    posted, r = _run_classify(
+        tmp_path / "mutant",
+        "#!/usr/bin/env bash\n" + DOCS_ONLY + "exit 1\n",
+        history_mode="premark-page1-error",
+        mutate=(
+            '[ "$max_id_before" -lt 0 ] && [ "$desc" != "$REPAIR_DESC" ]; then',
+            '[ "$state" = "success" ] && [ "$max_id_before" -lt 0 ]; then',
+        ),
+    )
+    assert posted is not None and posted["description"] != UNVERIFIED_DESC, (
+        "the `success`-only predecessor still wrote the sentinel, so this fixture does not reach the "
+        f"downgrade with state=pending and the test above proves nothing about its scope: {posted}"
+        f"\n{r.stdout[-900:]}"
+    )
+
+
 # --- Workflow token scope (ersatztv#748) -------------------------------------------------------
 #
 # Both assertions guard a property whose violation is SILENT and, for the first, unrecoverable.