diff --git a/.agents/specs/doc-checkpoint-lifecycle-states.md b/.agents/specs/doc-checkpoint-lifecycle-states.md index e0b69b941..eba44371b 100644 --- a/.agents/specs/doc-checkpoint-lifecycle-states.md +++ b/.agents/specs/doc-checkpoint-lifecycle-states.md @@ -476,19 +476,282 @@ each rebinding every derived name so it cannot apply to nothing: 4. `PARTIAL` removed from `CLAIM_ON_ARRIVAL` — a new `PARTIAL` row stops being a claim. +## W3 — the repair: W2 loosened the gate on nine transitions + +W2 landed on `main` as `ba4634204` (#1609) **without an independent review**. A +post-landing review returned FAIL. This section is the repair, on `main` rather +than a revert: W2 makes 52 transitions observable and 9 of them regress, and the +9 are one line. + +### The defect + +`transitions()` keyed the move class on **both** endpoints: + +```python +kind = CLAIM if previous in STATES and state in STATES else RECORD +``` + +Before W2 a row sitting in `INVENTORIED`, `SPIKE` or `ANCHOR-BACKFILL` was +**absent from the BEFORE map**, so `previous` was `None`, the ARRIVAL rule fired +and pulled in `REQUIRED["lifecycle"] = (STATUS, BENCHMARKS)`. Resolving the +record states made `previous` resolve, which made the arrival rule unreachable +(`previous is not None`), and the both-endpoints test then sent the move down +the RECORD branch and dropped both surfaces. + +**569 of the 793 resolved rows — 72% — sit in a record state**, so this is the +exit path of nearly every row in the tree. + +W2's own justification for the polarity was that "the arrival rule below already +governs a row that appears as `DONE`". It cannot: the arrival rule is guarded by +`previous is None`, and resolving the record states is exactly what stopped that +being true. + +### Nine transitions, red before `ba4634204`, green after + +Constructed scratch commits on `503e45900`, one pair per transition, each +changing only `.agents/kernel-matrix.md` and the row's spec, with the spec's +`## Now` **paid** and `docs/STATUS.md` / `docs/BENCHMARKS.md` **withheld**. Exit +code taken from the checker directly, never through a pipe. + +| transition | `e2a9e035d` (pre-W2) | `ba4634204` == `503e45900` | W3 | +|---|---|---|---| +| `INVENTORIED -> ACTIVE` | rc 1 | **rc 0** | rc 1 | +| `INVENTORIED -> GATING` | rc 1 | **rc 0** | rc 1 | +| `INVENTORIED -> DONE` | rc 1 | **rc 0** | rc 1 | +| `SPIKE -> ACTIVE` | rc 1 | **rc 0** | rc 1 | +| `SPIKE -> GATING` | rc 1 | **rc 0** | rc 1 | +| `SPIKE -> DONE` | rc 1 | **rc 0** | rc 1 | +| `ANCHOR-BACKFILL -> ACTIVE` | rc 1 | **rc 0** | rc 1 | +| `ANCHOR-BACKFILL -> GATING` | rc 1 | **rc 0** | rc 1 | +| `ANCHOR-BACKFILL -> DONE` | rc 1 | **rc 0** | rc 1 | + +Pre-W2 reports `added as ACTIVE`; W3 reports `INVENTORIED -> ACTIVE`. The +verdict is restored and the message is better than either. + +### The three real commits, and a correction to the report + +The review named `2a976eb9f` (`ENG-CUDAGRAPH-DEDUP` `INVENTORIED -> ACTIVE`), +`678fc672c` (`ENG-RECORD-ANCHOR-RATCHET` `SPIKE -> ACTIVE`) and `7a0e6c82b` +(`MODEL-MUSIC-minimax-music3…` `SPIKE -> ACTIVE`) as "ERROR under base, OK under +W2". Re-derived: **all three are rc 0 under all three checkers**, because all +three PAID `docs/STATUS.md` and `docs/BENCHMARKS.md` — the pre-W2 gate made +them. The commits still prove the point, on the classification rather than the +exit code. Withhold those two paths from the same tree change: + +| commit | pre-W2 | W2 | W3 | +|---|---|---|---| +| `2a976eb9f` | `added as ACTIVE`, demands STATUS | **no lifecycle move at all** | `INVENTORIED -> ACTIVE`, demands STATUS | +| `678fc672c` | `READY -> ACTIVE`, demands STATUS | **no lifecycle move at all** | `SPIKE -> ACTIVE`, demands STATUS | +| `7a0e6c82b` | `added as ACTIVE`, demands STATUS | **no lifecycle move at all** | `SPIKE -> ACTIVE`, demands STATUS | + +### Why W2's safety argument could not see this + +W2 replayed 400 commits and reported **0 newly green**. That number is an +artifact, not evidence. The replay measures commits that were red under the base +gate; the base gate **enforced** the obligation W2 removed, so every commit that +would have gone green had already paid it. **A replay of already-gated history +is structurally incapable of detecting the removal of the obligation that gated +it.** The nine transitions are therefore pinned as CONSTRUCTED cases in +`tests/scripts/test_doc_checkpoint.py`, and the replay is used only for the +cost, which is what it can measure. + +### The fix, and what it costs + +```python +kind = CLAIM if state in STATES else RECORD +``` + +Key on the **destination**. It closes all nine, preserves W1's +`ANCHOR-BACKFILL` ruling (`DONE -> ANCHOR-BACKFILL` stays RECORD, and so do +`DONE -> INVENTORIED` and `DONE -> SPIKE`), and matches the polarity +`CLAIM_ON_ARRIVAL` already uses — a rule that reads where the row landed and +ignores where it came from. + +Replayed over the same 400 non-merge commits ending at `e2a9e035d`: + +| verdict | commits | +|---|---:| +| red under pre-W2 | 44 | +| red under W2 | 45 | +| red under W3 | 47 | +| **newly red, W3 against pre-W2** | **3** | +| **newly green, W3 against pre-W2** | **0** | +| newly red, W3 against W2 | 2 | +| newly green, W3 against W2 | 0 | + +Each of the three is a genuinely unpaid surface: + +| commit | move | what is missing | +|---|---|---| +| `67e53e716` | `TOOLS-PARSER-BREADTH` `INVENTORIED -> PARTIAL` | `docs/BENCHMARKS.md` (STATUS paid) | +| `33f570ea9` | `ENG-WEIGHT-OFFLOAD` `INVENTORIED -> READY` | `docs/BENCHMARKS.md` (STATUS paid) | +| `ab6e65216` | `ENG-CUDAGRAPH-BREAK` `INVENTORIED -> READY` | `docs/BENCHMARKS.md`, `docs/STATUS.md` | + +**The `ab6e65216` accounting is corrected.** W2 counted it as one newly-red true +positive. Its *lifecycle* half is a true positive under W3. Its `## Now` half — +the only error W2 itself raised on it — is a **false positive**: the row's +`Spike/spec` column links `specs/eng-cudagraph-break.md`, which that commit +CREATES, 834 lines, with a populated `## Now` at `:818`. `spec_for_row` takes +the FIRST link on the line, which is an evidence link to +`specs/decode-graph-scratch-uaf-2026-07-18.md`, so the gate demanded a file the +change had no reason to touch. The move being unobserved is true; the message is +wrong. Pinned by `SpecForRowTakesTheFirstLink` and carried in `## Owed`. + +### The public-term criterion, re-derived per state + +W2's `RECORD_STATES` comment said the three are "real lifecycle positions that +the public pages carry **NO** term for", and W2 made that criterion executable +in `test_partial_is_a_public_status_term` / +`test_anchor_backfill_is_not_a_public_status_term`. Applying W2's own criterion +to `INVENTORIED` returns the **opposite** answer to the one W2 recorded, and +neither the W2 spec nor the W2 tests contain the string `Inventoried` — it was +derived for `ANCHOR-BACKFILL` and extended to two more states without being +re-derived. The criterion is falsified in both directions: + +- **Not sufficient.** `docs/STATUS.md:42` defines + `| Inventoried | The gap has a stable record but no accepted implementation |` + and `:56` uses it in a live projection cell. +- **Not necessary.** `READY`, `TODO`, `BLOCKED`, `DROPPED` and `N/A` are all in + `STATES` and `docs/STATUS.md` names none of them (grep count 0 each). + +The criterion that survives is whether the position belongs to the CAPABILITY or +to the ROW'S RECORD. Re-derived separately for each of the three: + +**`INVENTORIED` — on the page, and still a record state.** `STATUS.md`'s own +definition describes the RECORD ("the gap has a stable record") together with +the ABSENCE of an implementation, so carrying the word does not make arriving +there a capability claim. The two obvious costs were measured rather than +argued, and neither decides it: moving `INVENTORIED` into `STATES` changes **0 +of 793** row resolutions, and the 400-commit replay is **identical** either way +(47 red, 2 newly red vs W2, 0 newly green). What decides it is that +`INVENTORIED` is where a PRE-CLAIM row and a DEMOTED row both sit. With it in +`STATES`, `SPIKE -> INVENTORIED` would demand `docs/STATUS.md` and +`docs/BENCHMARKS.md` for a row that has never claimed anything — the +public-document edit with nothing true to write that +`check-doc-checkpoint.py:4-17` records as the reason the file was rewritten. It +stays a record state. + +**`SPIKE` — pre-claim by protocol.** `.agents/feature-matrix.md` gives a `SPIKE` +row a `CLAIM-*` and not a spec, and `docs/STATUS.md` carries no term (grep 0). +Neither limb argues for admitting it. Note that unlike `INVENTORIED`, `SPIKE` +also carries a measured resolution cost: admitting it moves 2 of 793 rows to the +wrong state (`MODEL-TEXT-deepseek-v2…` `BLOCKED -> SPIKE`, +`MODEL-TEXT-kimi-linear…` `READY -> SPIKE`), because their evidence prose says +"the row stays `SPIKE`". That is the measurement W2 recorded for the +cell-anchoring asymmetry, and it belongs to `SPIKE` alone. + +**`ANCHOR-BACKFILL` — W1's ruling, re-derived independently and unchanged.** It +is a property of the record by definition, `docs/STATUS.md` carries no term +(grep 0), and a `DONE <-> ANCHOR-BACKFILL` move changes nothing a reader of that +page could be told. + +### The residual this leaves, sized + +Destination-keying does not observe a **demotion**: `DONE -> INVENTORIED` is a +retraction that `docs/STATUS.md` genuinely projects, and it stays a RECORD move +owing only the spec's `## Now`. Sized rather than asserted: over the 400 commits +ending at `e2a9e035d` the transition census is **11 claim -> claim, 6 record -> +claim, 0 claim -> record, 0 record -> record**, plus 14 arrivals. The 6 are +exactly the population W2 un-gated. The demotion has zero traffic. Carried in +`## Owed`. + +### W3 tests + +`TheDestinationDecidesTheMoveClass` in `tests/scripts/test_doc_checkpoint.py` +pins all nine transitions constructed, that paying both surfaces discharges +them, and that the arrival rule is unreachable once `previous` resolves. Its +mutation restores W2's both-endpoints line and requires all nine to go green, +then re-asserts the red after restoring, so a mutation that never applied cannot +read as a pass. `test_a_move_into_a_record_state_is_still_a_record_move` holds +the other polarity for all three record states. + +Three W2 tests are repaired rather than added: + +1. `test_a_record_move_reaching_a_claim_state_stays_a_record_move` pinned the + defect on a false premise. Renamed to + `test_a_record_move_reaching_a_claim_state_is_a_claim_move`, with the premise + corrected in the docstring. +2. `test_anchor_backfill_stays_out_of_the_tuple` asserted + `"ANCHOR-BACKFILL" in spec.split("## Owed", 1)[1]`. The first literal + `## Owed` is inline prose at `:59`, not the section at `:479`, so it scanned + 420 lines of spec body and could not fail — and it did not: W2 rewrote + `## Owed` without `ANCHOR-BACKFILL` and the test stayed green. Re-anchored to + the section body through `owed_section()`, which is itself mutation-tested by + `test_the_owed_section_reader_is_not_the_whole_file`. **Red-before evidence: + the re-anchored assertion FAILS against W2's `## Owed` at `503e45900`.** +3. `test_every_row_the_checker_could_resolve_there_is_a_phantom` catches + REPLACING a `FUSED` cell with `` `ACTIVE` `` and does not catch ADDING + `` `ACTIVE` `` as a new column beside it — 3 passed, rc 0 — because it + asserts `len(classification) == 1`. Given the file's header says the + classification stands "in place of a lifecycle state", the additive shape is + the likelier way it changes. + `test_no_resolved_row_carries_a_bare_state_cell` asks the other question: + every resolved row's only bare backticked cell is its own ID cell, so a real + State column is a second one however it arrives. + +### Two corrections to W2 record keeping + +- `spec_now_errors`'s comment said "52 of 52 `SPIKE` rows". Re-derived over the + seven `ROW_TABLES` at `503e45900`: **50 of 50**. The `ANCHOR-BACKFILL` figure + in the same sentence, 50 of 56, is correct, as is 416 of 463 for + `INVENTORIED`. +- `TheSglangMatrixIsNotALifecycleTable` reported 46 keyed rows and four + classification values summing to 43 without reconciling the two. + Reconciled: 46 = `FUSED` 24 + `SGLANG-DISTINCT` 5 + `OUT-OF-SCOPE` 8 + + unbackticked `INVENTORIED` 6 + 3 rows whose axis cell is formatted differently + again (`SGLANG-SCHED-INBATCH` "ACTIVE (order-only)", `SGLANG-CONSTRAIN-JUMP`, + `SGLANG-ORACLE-PERF`). + +### W3 counters, re-measured + +W2 measured its counters and W3 measures them again on the same tree, base +version restored from the index and the W3 version restored byte-for-byte +afterwards against a pre-taken sha256. + +| counter | at `503e45900` | with W3 | why it cannot move | +|---|---|---|---| +| `check-gate-commands.py --check` | rc 0 | rc 0 | `GATED_STATES` (`:56`) is its own tuple and does not import this one; `RUNNABLE_BASELINE` (`:424`) keys on matrix rows, and `GATE-DOC-CHECKPOINT-STATES` has no matrix row | +| `check-agent-record.py` | rc 0, `ENGINE=169 MODEL=377 QUANT=84 KERNEL=57 BACKEND=85 ANCHOR-ROT=37` | identical | no matrix row and no index row changes; #1434's index row already names this owning row, so `UNOWNED_HIGH_WATER` cannot move | +| record-anchor ratchet | unchanged | unchanged | no matrix row changes | +| `docs/STATUS.md` prose ratchet | untouched | untouched | no public document changes | + +The `## Gates` section of this spec is NOT edited by W3, which is the #1376 +shape: filling a spec's `## Gates` moves its row into the runnable population. +No row moves lifecycle state in this change either, so it owes no checkpoint +surface. + ## Owed - [#1434](https://github.com/mudler/vllm.cpp/issues/1434) is closed by W1 for - `PARTIAL` and by W2 for all four residuals it filed. What remains is narrower - than what it replaced, and each item is sized rather than asserted: + `PARTIAL`, by W2 for resolution of the record states, and by W3 for the move + classification. What remains is narrower than what it replaced, and each item + is sized rather than asserted: + - **A DEMOTION out of a claim state is still not projected.** `DONE -> + INVENTORIED` is a retraction `docs/STATUS.md` carries a term for, and + destination-keying makes it a RECORD move owing only the spec's `## Now`. + Admitting it means either putting `INVENTORIED` in `STATES`, which makes + `SPIKE -> INVENTORIED` demand both public surfaces for a row that has never + claimed anything, or splitting the class by direction — a different rule and + a different row. Measured traffic: **0 of the 17 non-arrival transitions in + 400 commits**. + - `ANCHOR-BACKFILL` and `SPIKE` moves owe their spec's `## Now` and nothing + else, by the W1 ruling re-derived per state in `## W3`. That is a decision, + not debt, and it is listed here so the state names stay in this section. - `spec_for_row` returns the FIRST `specs/*.md` link on a row line, which is not always the `Spike/spec` column. **97 of 793 rows (12%)** link more than - one spec, so on those the error can name a spec the change did not have to - touch. `ab6e65216` above is exactly this: the move is real, the spec named is - an evidence link. Pre-existing and unchanged by W2, which raises its - exposure. Fixing it means deciding which column is authoritative per matrix, - or accepting any linked spec — the second is a loosening and needs its own - argument. + one spec. `ab6e65216` is exactly this: the move is real, the spec named is + an evidence link, and the file the row actually links is created by that same + commit with a populated `## Now`. Pinned by `SpecForRowTakesTheFirstLink` + so a repair is a deliberate edit. Fixing it means deciding which column is + authoritative per matrix, or accepting any linked spec — the second is a + loosening and needs its own argument. + - `row_states` lets a cell-anchored RECORD state win OUTRIGHT and `continue` + past `STATE_CELL`, so an evidence cell that OPENS with a backticked record + state demotes a claim row wherever the real State column sits. **Zero rows + do that today.** The repair is already sized: taking whichever of the last + `RECORD_CELL` and the last `STATE_CELL` match ends LATER in the line changes + **0 of 793** resolutions. Not made here because it is a separate semantic + change to the resolver and wants its own red-before case. - A row ID that leaves a table entirely is still unobserved. Measured at **zero occurrences in 400 commits**, so this is a hole with no known traffic rather than a live gap. @@ -497,12 +760,29 @@ each rebinding every derived name so it cannot apply to nothing: and is a different row: it moves what counts as a move for rows this change does not touch. - `.agents/sglang-matrix.md` stays out of `ROW_TABLES` by decision, not by - omission. If it ever gains a real lifecycle State column, - `test_every_row_the_checker_could_resolve_there_is_a_phantom` fails and the - decision is made again. + omission. If it ever gains a real lifecycle State column, either + `test_every_row_the_checker_could_resolve_there_is_a_phantom` or + `test_no_resolved_row_carries_a_bare_state_cell` fails and the decision is + made again. ## Now -W2 landed on `row/GATE-DOC-CHECKPOINT-STATES-W2` from base `e2a9e035d`. Next: -fresh scoped review of the immutable head, re-running the four W2 mutations and -the 400-commit replay to confirm the newly-red count is still 1. +W2 landed on `main` as `ba4634204` (#1609) from base `e2a9e035d`, **without an +independent review**. The post-landing fresh review reproduced the resolution +work as sound — 52 transitions become observable — and returned **FAIL** on one +finding: keying the move class on both endpoints removed +`REQUIRED["lifecycle"]` from the nine +`{INVENTORIED, SPIKE, ANCHOR-BACKFILL} -> {ACTIVE, GATING, DONE}` transitions, +which the arrival rule had gated before resolution made `previous` non-`None`. +The review also found the `INVENTORIED` public-term criterion applied without +being re-derived, the `ab6e65216` cost accounting counting a false positive as a +true one, an additive-column blind spot in the `sglang-matrix` decline, and a +tautological `## Owed` assertion. + +W3 is the repair, on `main` rather than a revert, on branch +`row/GATE-DOC-CHECKPOINT-STATES-W3` from base `503e45900`: one line in +`transitions()`, the per-state re-derivation recorded in `## W3`, and the four +test repairs. Next: fresh scoped review of the immutable head — mutate the +destination-keyed line back to the both-endpoints form and confirm all nine go +green, re-run the 400-commit replay for 3 newly red / 0 newly green against +`e2a9e035d`, and confirm no pinned counter moved. diff --git a/scripts/check-doc-checkpoint.py b/scripts/check-doc-checkpoint.py index 27da1657f..1858fbc71 100755 --- a/scripts/check-doc-checkpoint.py +++ b/scripts/check-doc-checkpoint.py @@ -79,11 +79,49 @@ "N/A", ) -# RECORD states are real lifecycle positions that the public pages carry NO term -# for. .agents/feature-matrix.md:14-20 names all three: INVENTORIED and SPIKE are -# pre-claim, and ANCHOR-BACKFILL is a property of the RECORD -- "a legacy -# implemented row without exact code, test and real-spec anchors" -- so the -# capability is already implemented and only the row's anchors are missing. +# RECORD states are lifecycle positions of the ROW'S RECORD rather than of the +# CAPABILITY. .agents/feature-matrix.md:14-20 names all three: INVENTORIED and +# SPIKE are pre-claim, and ANCHOR-BACKFILL is a property of the RECORD -- "a +# legacy implemented row without exact code, test and real-spec anchors" -- so +# the capability is already implemented and only the row's anchors are missing. +# +# 2026-08-21, W3: the criterion W2 wrote here -- "real lifecycle positions that +# the public pages carry NO term for" -- is FALSE, and it was derived for one +# state and then applied to three. docs/STATUS.md:42 defines +# `| Inventoried | The gap has a stable record but no accepted implementation |` +# and :56 uses it in a live projection cell ("Distributed execution | Inventoried +# or partial by lane"). In the other direction READY, TODO, BLOCKED, DROPPED and +# N/A are all in STATES and docs/STATUS.md carries no term for any of them, grep +# count 0 each. Word-on-the-page is therefore neither necessary nor sufficient, +# and tests/scripts/test_doc_checkpoint.py pins both halves of that so the wrong +# criterion cannot be reintroduced by quoting this file. +# +# Re-derived per state, separately, on what REQUIRED["lifecycle"] actually +# demands -- (STATUS, BENCHMARKS), carried all or none: +# +# INVENTORIED -- ADMITTED to the page, DECLINED for the tuple. STATUS.md's own +# definition describes the RECORD ("the gap has a stable record") together +# with the ABSENCE of an implementation, so carrying the word does not make +# arriving there a capability claim. Neither obvious cost decides it, and +# both were measured rather than argued: moving it into STATES changes 0 of +# 793 row resolutions, and the 400-commit replay ending at e2a9e035d is +# identical either way. What decides it is that INVENTORIED is where a +# PRE-CLAIM row and a DEMOTED row both sit, so admitting it makes +# SPIKE -> INVENTORIED demand docs/STATUS.md and docs/BENCHMARKS.md for a row +# that has never claimed anything -- the public-document edit with nothing +# true to write that this file's header records as the reason for the +# rewrite. The half that genuinely goes unpaid is a DEMOTION out of a claim +# state into it; that is listed under `## Owed` in the row's spec, and it is +# 0 of the 17 non-arrival transitions in the same 400 commits. +# +# SPIKE -- pre-claim by protocol: .agents/feature-matrix.md gives a SPIKE row a +# `CLAIM-*` and not a spec, and docs/STATUS.md carries no term (grep 0). +# Neither limb of the criterion argues for admitting it. +# +# ANCHOR-BACKFILL -- W1's ruling, re-derived independently and unchanged. It is +# a property of the record BY DEFINITION, docs/STATUS.md carries no term +# (grep 0), and a DONE <-> ANCHOR-BACKFILL move changes nothing a reader of +# that page could be told. # # 2026-08-21, W2 of the same row: they are RESOLVED but not CLASSIFIED as claims. # The earlier reading (recorded in doc-checkpoint-lifecycle-states.md `## Owed`) @@ -118,6 +156,16 @@ # QUANT-GGUF-PRESETS READY -> INVENTORIED) still resolve correctly. Measured over # all 793 rows against a column-position proxy: 12 of 226 resolutions disagreed # with it before, 10 of 793 after, and no previously-correct row regresses. +# +# THE OUTRIGHT WIN IS A LATENT HAZARD, recorded here so the next reader does not +# have to rediscover it. row_states takes the record cell and `continue`s past +# STATE_CELL, so an EVIDENCE cell that OPENS with a backticked record state +# demotes a claim row no matter where the real State column sits. Zero rows do +# that today, and the sized repair is already measured: taking whichever of the +# last RECORD_CELL and the last STATE_CELL match ends LATER in the line changes +# 0 of the same 793 resolutions. It is not made here because it is a separate +# semantic change to the resolver and wants its own red-before case; it is +# listed under `## Owed` in .agents/specs/doc-checkpoint-lifecycle-states.md. RECORD_CELL = re.compile( r"\|\s*`(" + "|".join(re.escape(s) for s in RECORD_STATES) + r")`" ) @@ -262,11 +310,42 @@ def transitions( ) -> list[tuple[str, str, str | None, str, str]]: """Every lifecycle move, as (table, row, previous, state, kind). - `kind` is CLAIM when both endpoints are states docs/STATUS.md has a term for, - and RECORD when either endpoint is one it does not. A RECORD move is still a + `kind` is keyed on the DESTINATION alone. A move INTO a claim state is a + CLAIM. A move into a record state is a RECORD move, which is still a lifecycle move -- AGENTS.md `## Public documents` owes the moved row spec's `## Now` for ANY state change -- it simply owes nothing the public pages could truthfully say. + + 2026-08-21, W3 (#1434). W2 keyed on BOTH endpoints, and that LOOSENED the + gate on nine transitions. Before W2 a row sitting in INVENTORIED, SPIKE or + ANCHOR-BACKFILL was absent from the BEFORE map, so `previous` was None and + the ARRIVAL rule fired, pulling in REQUIRED["lifecycle"]. Resolving the + record states made `previous` resolve, which made the arrival rule + unreachable, and the both-endpoints test then sent the move down the RECORD + branch and dropped (STATUS, BENCHMARKS). So every member of + {INVENTORIED, SPIKE, ANCHOR-BACKFILL} x {ACTIVE, GATING, DONE} went RED -> + GREEN across W2, with the spec `## Now` paid and the public surfaces + withheld: 9 of 9 rc 1 at e2a9e035d, 9 of 9 rc 0 at ba4634204, measured on + scratch commits. 569 of the 793 resolved rows sit in a record state, so that + is the exit path of most of the tree. + + Destination-keying closes all nine, keeps W1's ANCHOR-BACKFILL ruling + (DONE -> ANCHOR-BACKFILL is still RECORD), and matches the polarity + CLAIM_ON_ARRIVAL already uses -- a rule that reads the destination and + ignores where the row came from. Replayed over the 400 non-merge commits + ending at e2a9e035d: 3 newly red against the pre-W2 gate and 0 newly green, + each of the three a genuinely unpaid surface (67e53e716, 33f570ea9, + ab6e65216). + + THE REPLAY CANNOT BE THE WHOLE EVIDENCE, which is the lesson W2 missed. It + measures newly-GREEN over commits that landed UNDER the obligation being + removed, so no such commit can exist and "0 newly green" is an artifact + rather than a safety result. The three real commits that exercise these + transitions -- 2a976eb9f, 678fc672c, 7a0e6c82b -- are green under every + variant BECAUSE they paid both surfaces; withhold those two paths from the + same tree change and W2 alone reports no lifecycle move at all. The nine + transitions are therefore pinned as CONSTRUCTED cases in + tests/scripts/test_doc_checkpoint.py, not by replay. """ moves: list[tuple[str, str, str | None, str, str]] = [] for path in sorted(paths & set(ROW_TABLES)): @@ -280,7 +359,9 @@ def transitions( continue if previous == state: continue - kind = CLAIM if previous in STATES and state in STATES else RECORD + # Destination-keyed. The both-endpoints form is what W2 + # loosened; see the docstring for the nine transitions. + kind = CLAIM if state in STATES else RECORD moves.append((path, row, previous, state, kind)) return moves @@ -321,7 +402,9 @@ def spec_now_errors(paths: set[str], before: str, after: str) -> list[str]: # by omission. Demanding one here would demand a document # .agents/feature-matrix.md says does not exist yet. The `## Now` # obligation still binds every record row that DOES link a spec, - # which is 50 of 56 ANCHOR-BACKFILL rows and 52 of 52 SPIKE rows. + # which is 50 of 56 ANCHOR-BACKFILL rows and 50 of 50 SPIKE rows + # (re-derived over the seven ROW_TABLES at 503e45900; W2 recorded + # 52 of 52 and the population has moved since). continue errors.append( f"{table}: {row} moved lifecycle state but its row links no spec, " diff --git a/tests/scripts/test_doc_checkpoint.py b/tests/scripts/test_doc_checkpoint.py index 65e7a8b25..6b514bccf 100755 --- a/tests/scripts/test_doc_checkpoint.py +++ b/tests/scripts/test_doc_checkpoint.py @@ -42,6 +42,24 @@ | `KERNEL-BETA` | beta | [beta](specs/beta.md) | `{beta}` | ops | """ +SECTION = re.compile(r"^##\s+(?P.+?)\s*$", re.MULTILINE) + + +def owed_section(path: Path) -> str: + """The body of the `## Owed` SECTION, not the first place that text appears. + + An inline mention of `## Owed` in prose is not the section, and splitting on + the literal makes an assertion about the section unfalsifiable -- see + test_the_owed_section_reader_is_not_the_whole_file. + """ + body = path.read_text(encoding="utf-8") + for match in SECTION.finditer(body): + if match.group("name") == "Owed": + rest = body[match.end():] + return SECTION.split(rest, maxsplit=1)[0] + raise AssertionError(f"{path} has no `## Owed` section") + + # A row spec carrying the relocated live position (ENG-NOW-DERIVED, #374). SPEC_WITH_NOW = "# Alpha\n\n## Scope\n\nthings\n\n## Now\n\nRun the focused gate.\n" SPEC_WITHOUT_NOW = "# Alpha\n\n## Scope\n\nthings\n" @@ -645,9 +663,16 @@ class AnchorBackfillIsDeliberatelyExcluded(unittest.TestCase): """The ruling #1434 asked for, kept executable rather than only argued. `.agents/feature-matrix.md` names `PARTIAL`, `BLOCKED` and `ANCHOR-BACKFILL` - together, so "the matrix calls it a state" cannot be the test. The test is - whether `docs/STATUS.md` PROJECTS it, because `REQUIRED["lifecycle"]` is - (STATUS, BENCHMARKS) and carries all of them or none. + together, so "the matrix calls it a state" cannot be the test. + + W1 and W2 wrote the test as "does docs/STATUS.md PROJECT the word". W3 + falsifies that as a CRITERION and keeps the falsification executable below: + `Inventoried` is on the page and is a record state, while READY, TODO, + BLOCKED, DROPPED and N/A are claim states the page has never named. The word + remains a useful piece of EVIDENCE about a state and it is not the rule. The + rule is whether the position belongs to the CAPABILITY or to the ROW'S + RECORD, because `REQUIRED["lifecycle"]` is (STATUS, BENCHMARKS) and carries + all of them or none. """ def test_partial_is_a_public_status_term(self): @@ -670,16 +695,83 @@ def test_anchor_backfill_stays_out_of_the_tuple(self): That is the shape check-doc-checkpoint.py:4-17 records as the reason this file was rewritten: 16 of 20 red CI runs and six hardcoded - escape-hatch path sets. Paying the `## Now` half it genuinely owes needs - REQUIRED to carry a spec-only class, which is a different change and is - listed under `## Owed` in doc-checkpoint-lifecycle-states.md. + escape-hatch path sets. The `## Now` half is paid -- spec_now_errors is + called from errors_for directly -- and the residual it leaves is the + DEMOTION out of a claim state into a record one, which is what the spec + section this test reads has to keep naming. + + Anchored to the `## Owed` SECTION, not to the first literal `## Owed` in + the file. W2 split on the string, and the first occurrence is inline + prose 420 lines above the section, so the assertion scanned most of the + spec body and could not fail. """ self.assertNotIn("ANCHOR-BACKFILL", checker.STATES) - spec = ( + owed = owed_section( ROOT / ".agents/specs/doc-checkpoint-lifecycle-states.md" - ).read_text(encoding="utf-8") - self.assertIn("## Owed", spec) - self.assertIn("ANCHOR-BACKFILL", spec.split("## Owed", 1)[1]) + ) + self.assertIn("ANCHOR-BACKFILL", owed) + + def test_the_owed_section_reader_is_not_the_whole_file(self): + """MUTATION on the reader above, because a tautology reads as a pass. + + A section reader that silently returned the file would make the test + above green no matter what `## Owed` says. Prove it is a section: the + text it returns must be a strict, much smaller suffix of the spec, and + must not contain the spec's title line. + """ + path = ROOT / ".agents/specs/doc-checkpoint-lifecycle-states.md" + body = path.read_text(encoding="utf-8") + owed = owed_section(path) + self.assertIn(owed, body) + self.assertNotIn(body.splitlines()[0], owed) + self.assertLess(len(owed), len(body) / 2) + self.assertGreater(len(owed), 0) + + def test_inventoried_is_a_public_status_term_and_still_a_record_state(self): + """The half W2 never checked, and it inverts W2's stated criterion. + + W2's `RECORD_STATES` comment said the three are "real lifecycle positions + that the public pages carry NO term for". `docs/STATUS.md` defines + `Inventoried` in the lifecycle table and uses it in a live projection + cell, so applying W2's own executable admission criterion to INVENTORIED + returns the OPPOSITE answer to the one W2 recorded. The ruling survives + re-derivation on a different argument -- INVENTORIED is where a pre-claim + row and a demoted row both sit, so admitting it makes SPIKE -> + INVENTORIED demand both public surfaces for a row that has never claimed + anything -- and this test holds the two facts together so nobody has to + take the comment's word for either. + """ + status = (ROOT / "docs/STATUS.md").read_text(encoding="utf-8") + self.assertIn( + "| Inventoried | The gap has a stable record but no accepted " + "implementation |", + status, + ) + self.assertIn("Inventoried", status.split("### User-facing surfaces", 1)[1]) + self.assertIn("INVENTORIED", checker.RECORD_STATES) + self.assertNotIn("INVENTORIED", checker.STATES) + + def test_the_public_term_test_is_neither_necessary_nor_sufficient(self): + """Both limbs, so the wrong criterion cannot come back by quotation. + + NOT SUFFICIENT: `Inventoried` is on the page and is a record state. + NOT NECESSARY: five claim states appear nowhere on it. + """ + status = (ROOT / "docs/STATUS.md").read_text(encoding="utf-8") + self.assertIn("Inventoried", status) + self.assertIn("INVENTORIED", checker.RECORD_STATES) + for state in ("READY", "TODO", "BLOCKED", "DROPPED", "N/A"): + with self.subTest(state=state): + self.assertIn(state, checker.STATES) + self.assertNotIn(state, status) + self.assertNotIn(state.capitalize(), status) + + def test_spike_is_not_a_public_status_term(self): + """Re-derived separately from ANCHOR-BACKFILL rather than bundled.""" + status = (ROOT / "docs/STATUS.md").read_text(encoding="utf-8") + self.assertNotIn("SPIKE", status) + self.assertNotIn("Spike", status) + self.assertIn("SPIKE", checker.RECORD_STATES) @@ -812,19 +904,23 @@ def test_entering_the_claim_set_from_a_record_state_is_seen(self): self.assertTrue(errors) self.assertIn(".agents/specs/alpha.md", " ".join(errors)) - def test_a_record_move_reaching_a_claim_state_stays_a_record_move(self): + def test_a_record_move_reaching_a_claim_state_is_a_claim_move(self): """INVENTORIED -> DONE crosses the boundary, so which side wins? - The record side. STATUS.md can say what a DONE row does, but the move - itself starts from a position that page never carried, and the arrival - rule below already governs a row that appears as DONE. Pinned so that - the polarity is a decision rather than an accident of the `and`. + The CLAIM side, keyed on the destination. W2 pinned the opposite on a + false premise -- "the arrival rule below already governs a row that + appears as DONE" -- and the arrival rule fires only when `previous is + None`, which is exactly what W2 stopped being true. Resolving the record + states is what removed the arrival rule's cover, so the both-endpoints + test silently dropped (STATUS, BENCHMARKS) for the very moves that had + been gated through it. See TheDestinationDecidesTheMoveClass for all + nine and for the mutation that proves this line is what fires them. """ classes, _ = self.classify( ROW_TABLE.format(alpha="INVENTORIED", beta="DONE"), ROW_TABLE.format(alpha="DONE", beta="DONE"), ) - self.assertNotIn("lifecycle", classes) + self.assertIn("lifecycle", classes) def test_a_record_move_on_a_row_linking_no_spec_is_not_an_error(self): """The one narrowing in this change, and it is stated as such. @@ -1002,6 +1098,197 @@ def all_claim(paths, before, after): self.assertEqual(self.errors(paid, *moved), []) +class TheDestinationDecidesTheMoveClass(unittest.TestCase): + """GATE-DOC-CHECKPOINT-STATES W3 (#1434): the repair of a W2 LOOSENING. + + W2 keyed the move class on both endpoints:: + + kind = CLAIM if previous in STATES and state in STATES else RECORD + + Before W2 a row sitting in INVENTORIED, SPIKE or ANCHOR-BACKFILL was absent + from the BEFORE map, so `previous` was None and the ARRIVAL rule fired, + pulling in REQUIRED["lifecycle"] = (STATUS, BENCHMARKS). Resolving the record + states made `previous` resolve, which made the arrival rule unreachable, and + the both-endpoints test then sent the move down the RECORD branch. Nine + transitions went RED -> GREEN across W2 with the spec `## Now` paid and the + public surfaces withheld, and 569 of the 793 resolved rows sit in a record + state, so that is the exit path of most of the tree. + + Measured on scratch commits with the real CLI, spec `## Now` paid and + docs/STATUS.md + docs/BENCHMARKS.md withheld: 9 of 9 rc 1 at e2a9e035d, 9 of + 9 rc 0 at ba4634204 (== 503e45900), 9 of 9 rc 1 with the destination-keyed + form. + + THESE CASES ARE CONSTRUCTED ON PURPOSE. W2's safety argument was a replay of + 400 commits reporting 0 newly green, and a replay of already-gated history + cannot detect the removal of the obligation that gated it: every commit that + would have gone green had already paid, because the pre-W2 gate made it. The + three real commits that exercise these transitions -- 2a976eb9f, 678fc672c, + 7a0e6c82b -- are green under every variant for exactly that reason. Withhold + the two public paths from the same tree change and W2 alone reports no + lifecycle move at all. + """ + + RECORD_SOURCES = ("INVENTORIED", "SPIKE", "ANCHOR-BACKFILL") + CLAIM_DESTINATIONS = ("ACTIVE", "GATING", "DONE") + + def errors(self, paths, before_text, after_text): + original = checker.blob + + def fake(rev, path): + if path.startswith(".agents/specs/"): + return SPEC_WITH_NOW + return before_text if rev == "BEFORE" else after_text + + checker.blob = fake + try: + return checker.errors_for(set(paths), "BEFORE", "AFTER") + finally: + checker.blob = original + + def classify(self, before_text, after_text): + original = checker.blob + checker.blob = lambda rev, path: ( + before_text if rev == "BEFORE" else after_text + ) + try: + return checker.classify({".agents/kernel-matrix.md"}, "BEFORE", "AFTER") + finally: + checker.blob = original + + def move(self, source, destination): + return ( + ROW_TABLE.format(alpha=source, beta="DONE"), + ROW_TABLE.format(alpha=destination, beta="DONE"), + ) + + def test_every_exit_from_a_record_state_demands_the_public_surfaces(self): + """RED-BEFORE, all nine. The spec `## Now` is PAID in every case, so the + only thing under test is whether (STATUS, BENCHMARKS) is still owed.""" + paid = [".agents/kernel-matrix.md", ".agents/specs/alpha.md"] + for source in self.RECORD_SOURCES: + for destination in self.CLAIM_DESTINATIONS: + with self.subTest(source=source, destination=destination): + errors = self.errors(paid, *self.move(source, destination)) + self.assertTrue( + errors, f"{source} -> {destination} must be a claim move" + ) + joined = " ".join(errors) + for surface in ("docs/STATUS.md", "docs/BENCHMARKS.md"): + self.assertIn(surface, joined) + self.assertIn(f"{source} -> {destination}", joined) + + def test_all_nine_are_satisfiable_by_paying_the_surfaces(self): + """The obligation has to be dischargeable, or it is a wall not a gate.""" + paid = [ + ".agents/kernel-matrix.md", + ".agents/specs/alpha.md", + "docs/STATUS.md", + "docs/BENCHMARKS.md", + ] + for source in self.RECORD_SOURCES: + for destination in self.CLAIM_DESTINATIONS: + with self.subTest(source=source, destination=destination): + self.assertEqual( + self.errors(paid, *self.move(source, destination)), [] + ) + + def test_restoring_the_both_endpoint_form_loosens_all_nine(self): + """MUTATION. Put W2's line back and every one of the nine goes green. + + Rebinding `checker.transitions` is the whole mutation: `lifecycle_moves` + and `spec_now_errors` both resolve it as a module global at call time, + so nothing else has to be rebuilt. Restored in `finally`, and the + post-restore assertion re-proves the red so a mutation that never + applied cannot read as a pass. + """ + paid = [".agents/kernel-matrix.md", ".agents/specs/alpha.md"] + original = checker.transitions + + def both_endpoints(paths, before, after): + return [ + ( + path, + row, + previous, + state, + checker.CLAIM + if previous in checker.STATES and state in checker.STATES + else checker.RECORD, + ) + for path, row, previous, state, _kind in original( + paths, before, after + ) + ] + + checker.transitions = both_endpoints + try: + for source in self.RECORD_SOURCES: + for destination in self.CLAIM_DESTINATIONS: + with self.subTest(source=source, destination=destination): + self.assertEqual( + self.errors(paid, *self.move(source, destination)), + [], + "the both-endpoints form must go blind here; it did " + "not, so these cases measure something else", + ) + finally: + checker.transitions = original + for source in self.RECORD_SOURCES: + for destination in self.CLAIM_DESTINATIONS: + self.assertTrue(self.errors(paid, *self.move(source, destination))) + + def test_a_move_into_a_record_state_is_still_a_record_move(self): + """W1's ANCHOR-BACKFILL ruling, and the two states it was extended to. + + Destination-keying preserves all three: a row LEAVING the claim set owes + its spec's `## Now` and nothing the public pages could truthfully say. + This is the half the fix must NOT widen, and the residual it leaves -- + a demotion out of a claim state going unprojected -- is `## Owed` in the + row's spec. It is 0 of the 17 non-arrival transitions in the 400 commits + ending at e2a9e035d. + """ + for destination in checker.RECORD_STATES: + with self.subTest(destination=destination): + classes, _ = self.classify(*self.move("DONE", destination)) + self.assertNotIn("lifecycle", classes) + + def test_the_record_exit_still_owes_its_spec_now(self): + """The `## Now` half is not dropped by promoting the move to a claim.""" + errors = self.errors( + [".agents/kernel-matrix.md", "docs/STATUS.md", "docs/BENCHMARKS.md"], + *self.move("SPIKE", "ACTIVE"), + ) + self.assertTrue(errors) + self.assertIn(".agents/specs/alpha.md", " ".join(errors)) + + def test_the_arrival_rule_is_unreachable_for_a_resolved_row(self): + """The mechanism behind the loosening, pinned directly. + + W2's justification for the both-endpoints polarity was that "the arrival + rule below already governs a row that appears as DONE". It cannot: the + arrival rule is guarded by `previous is None`, and resolving the record + states is precisely what stopped `previous` being None. + """ + for source in self.RECORD_SOURCES: + with self.subTest(source=source): + original = checker.blob + before, after = self.move(source, "DONE") + checker.blob = lambda rev, path: ( + before if rev == "BEFORE" else after + ) + try: + moves = checker.transitions( + {".agents/kernel-matrix.md"}, "BEFORE", "AFTER" + ) + finally: + checker.blob = original + alpha = [m for m in moves if m[1] == "KERNEL-ALPHA"] + self.assertEqual(len(alpha), 1) + self.assertEqual(alpha[0][2], source, "previous must resolve") + self.assertEqual(alpha[0][4], checker.CLAIM) + + class ANewPartialRowIsAClaim(unittest.TestCase): """GATE-DOC-CHECKPOINT-STATES W2 (#1434), residual 4. @@ -1062,6 +1349,44 @@ def test_removing_partial_from_the_arrival_set_restores_the_blind_spot(self): self.assertIn("lifecycle", self.classify("", self.ROW.format("PARTIAL"))[0]) +class SpecForRowTakesTheFirstLink(unittest.TestCase): + """W3 (#1434): a KNOWN DEFECT, pinned so the cost accounting stops lying. + + `spec_for_row` returns the FIRST `.agents/specs/...` link on a row's line, + and a matrix line reaches its `Spike/spec` column only after an evidence + column that often links a spec of its own. The gate then names a file the + change had no reason to touch. + + It is not hypothetical. `ab6e65216` moved `ENG-CUDAGRAPH-BREAK` INVENTORIED + -> READY and CREATED `.agents/specs/eng-cudagraph-break.md`, 834 lines, with + a populated `## Now` at :818 -- the exact obligation. The row's earlier + "owed" column links `specs/decode-graph-scratch-uaf-2026-07-18.md`, so that + is what the gate demanded. The MOVE being unobserved before W2 is true; the + MESSAGE is wrong, and W2's replay counted it as a true positive. + + NOT FIXED HERE. 97 of the 793 rows link more than one spec, so choosing the + Spike/spec column changes which file the gate demands for a whole population + and needs its own red-before measurement. Listed under `## Owed` in + .agents/specs/doc-checkpoint-lifecycle-states.md. This test pins the current + behaviour so that repairing it is a deliberate edit rather than a drift, and + it FAILS the day someone changes the resolution -- which is when the `## + Owed` entry gets closed. + """ + + LINE = ( + "| `ROW-X` | item | owed: the contract of " + "[uaf](specs/decode-graph-scratch-uaf.md) enforced at the seam " + "| spec [x](specs/row-x.md) | `READY` | ops |" + ) + + def test_the_evidence_link_wins_over_the_spike_spec_column(self): + self.assertEqual( + checker.spec_for_row(self.LINE, "ROW-X"), + ".agents/specs/decode-graph-scratch-uaf.md", + ) + self.assertIn("specs/row-x.md", self.LINE) + + class TheSglangMatrixIsNotALifecycleTable(unittest.TestCase): """GATE-DOC-CHECKPOINT-STATES W2 (#1434), residual 2: DECLINED, with the measurement that declines it kept executable. @@ -1078,6 +1403,13 @@ class TheSglangMatrixIsNotALifecycleTable(unittest.TestCase): implementation" column. Rewording one of those sentences would then read as an SGLANG row changing lifecycle state and would demand docs/STATUS.md, docs/BENCHMARKS.md and a spec `## Now` for a move that never happened. + + W3 reconciles the row count W2 reported without reconciling. 46 keyed rows = + 37 carrying exactly one legend cell (FUSED 24, SGLANG-DISTINCT 5, + OUT-OF-SCOPE 8) + 6 whose axis cell reads a bare unbackticked `INVENTORIED` + + 3 whose axis cell is formatted differently again (`SGLANG-SCHED-INBATCH` + "ACTIVE (order-only)", `SGLANG-CONSTRAIN-JUMP`, `SGLANG-ORACLE-PERF`). That + is 24 + 5 + 8 + 6 + 3 = 46, and the "43" W2 recorded is the first four. """ LEGEND = ("FUSED", "SGLANG-DISTINCT", "OUT-OF-SCOPE") @@ -1119,6 +1451,43 @@ def test_every_row_the_checker_could_resolve_there_is_a_phantom(self): "re-decide whether this file belongs in ROW_TABLES", ) + def test_no_resolved_row_carries_a_bare_state_cell(self): + """W3: the ADDITIVE shape the count test above cannot see. + + Replacing a `FUSED` cell with `` `ACTIVE` `` does fail the test above. + Adding `` `ACTIVE` `` as a NEW column while KEEPING `FUSED` does not -- + the classification count is still exactly 1 and the file passes. Given + the header says the classification stands "in place of a lifecycle + state", growing a real State column ALONGSIDE it is the likelier way + this file changes. + + So ask the other question directly: where did the token the checker + matched come from? Today, from prose. Every resolved row's only bare + backticked cell is its own ID cell; a real State column would be a + second one, whichever way it arrived. + """ + bare = re.compile(r"^`[A-Z0-9][A-Za-z0-9_./-]*`$") + resolved = checker.row_states(self.text) + self.assertTrue(resolved) + for line in self.text.splitlines(): + identifier = checker.ROW_ID.match(line) + if not identifier or identifier.group(1) not in resolved: + continue + cells = [cell.strip() for cell in line.strip().strip("|").split("|")] + standalone = [ + cell + for cell in cells[1:] + if bare.fullmatch(cell) + and cell.strip("`") in checker.LIFECYCLE_STATES + ] + self.assertEqual( + standalone, + [], + f"{identifier.group(1)} carries a standalone state cell " + f"{standalone}, so this file now has a real lifecycle axis; " + "re-decide whether it belongs in ROW_TABLES", + ) + if __name__ == "__main__": unittest.main()