From aee96b32fee759b6f9f2baa84777b7341ef4970e Mon Sep 17 00:00:00 2001 From: arpan Date: Mon, 14 Sep 2026 15:48:16 +0530 Subject: [PATCH] Spec review round three: fourteen findings, and what three rounds say about the scope Round two's section 4.6, written because two sections cancelled each other, cancelled against a rule round two added in the same commit. Section 3.2 required every anchor's seq to exceed the last; section 4.6 requires anchoring a checkpoint far below the head, at the pruned-through seq. So the checkpoint anchor was refused, so every prune was refused, forever. The section that names the cross-module class reproduced it one round later. Fixed by giving anchors a kind: interval and checkpoint are ordered separately. **The "superseded" defence needed a provider call that did not exist.** Section 4.6 claims an attacker who launders an erasure must leave an anchored checkpoint an operator can see. The frozen provider had make, check and latest, and the only anchor history the kernel could read was the local table, which section 3.3 establishes is a cache the writer under suspicion can trim. The provider gains since(seq), which is enumeration answered outside, and the prune verifies the anchors it is about to supersede while the rows that would settle it still exist. **The ledger window was not computable.** A ledger row carries no window and no limit; those travel on Charge, from the authority document, because state.py must not read policy. Resolving it inside the prune would reinstate the dependency section 4.2 removes, and a row whose grant is gone has no window at all. The operator supplies it: ctrlrun prune --older-than. **anchor_unavailable leaves the break set.** A transport failure is not a finding about evidence, and a set that conflates them teaches operators to ignore the ones that matter: a briefly unreachable timestamp authority would have graded G28 fail, indistinguishable from a truncation. Refusing to act when you cannot ask is fail-closed; reporting tampering when you cannot ask is a false positive. anchor_repudiated joins it, because check() answering no had no name and it is the provider's one substantive answer. **G32 is new.** G28 graded truncation against an anchor and G29 graded a prune against the chain; the interaction section 4.6 exists to fix was graded by neither, which is how two correct sections ship cancelling each other. Also: rule 2 and section 8's G29 still stated the absolute where section 10 had moved to a delta; that delta compared kinds rather than (kind, seq), so one pre-existing break disarmed the guard for that kind everywhere; a refused prune would have left a receipt asserting an erasure that never happened; section 9 had no row for item 1, which amends a frozen protocol and adds a public type; and three line-number citations into the other repository were wrong within a day, so they are cited by their words now. Section 12.3 records the round counts, and what they diagnose. Almost every high finding after round one lives in the interaction between the anchor and retention, not in either alone. That is evidence for the scope question section 1 leaves to the maintainer, and it is sharper evidence than existed when section 1 was written. Signed-off-by: arpan --- docs/SPEC-v0.11.md | 196 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 151 insertions(+), 45 deletions(-) diff --git a/docs/SPEC-v0.11.md b/docs/SPEC-v0.11.md index f0a17f7b..839ee092 100644 --- a/docs/SPEC-v0.11.md +++ b/docs/SPEC-v0.11.md @@ -20,7 +20,7 @@ demonstration, and it is a transcript rather than an argument. |---|---|---| | 0 | this document | none | | 1 | a reader that names a bad row and blinds nothing else (§5) | none; its evidence is its tests | -| 2 | the anchor, and the two break kinds it makes detectable (§3) | `G28` | +| 2 | the anchor, and the break kinds it makes detectable (§3) | `G28` | | 3 | retention: a chain-preserving prune, its checkpoint, and a hold (§4) | `G29`, `G30` | | 4 | one chain across five receipt schema versions, walked end to end (§6) | `G31` | | 5 | enforcement coverage, from events already written (§7) | none; it reports | @@ -44,9 +44,12 @@ Every item is measured against these. revocation, no signing. `SPEC-v0.3.md` §1.1's rule, that CTRLRun consumes identity and issues none, applied to time. It is the line between this milestone and the one `ROADMAP.md` keeps off the roadmap, and an anchor that minted anything would have crossed it. -2. **A prune leaves the chain verifiable across the gap, or it is refused.** A prune that produces a - chain reporting `missing` has destroyed evidence and called it retention. There is no `--force`, - no `--allow-gap`, and no setting that admits a chain nobody can verify. +2. **A prune introduces no break the chain did not already have, or it is refused.** A prune that + produces a `missing` has destroyed evidence and called it retention. Stated as a **delta** and not + as "the chain verifies", because `unchained` is a pre-existing condition on any store migrated + from v0.1 to v0.5, survives a prefix prune and can never be inside a prefix: the absolute version + made retention permanently impossible on the oldest and largest stores, which are the ones it is + for. There is no `--force`, no `--allow-gap`, and no setting that admits a break the prune caused. 3. **A malformed row names itself and blinds nothing else.** One tampered row costs one row. 4. **A clean coverage result is not a verdict.** No score, no percentage, no badge, and no sentence a reader could quote as one. `SPEC-v0.4.md` §3.9 on a new surface: verify never grades an @@ -154,13 +157,15 @@ not reach. **An anchor freezes a prefix.** It records that at time T the chain's head was `(seq, hash)`, so anything at or below that `seq` can no longer be removed or altered without the anchored pair -failing to reproduce. +failing to reproduce, **unless an anchored checkpoint accounts for its removal** (§4.6). That clause +is not a loophole and §4.6 is where it is kept from becoming one: a checkpoint must itself be +anchored, through the provider, which is outside the store. That sentence is the whole claim, and everything else follows from it by arithmetic: | Attack | Detected? | |---|---| -| §2.1's truncation, when the anchored `seq` is above the new head | **yes**: the anchored `seq` is absent | +| §2.1's truncation, when the anchored `seq` is above the new head | **yes**: the anchored `seq` is absent, and no anchored checkpoint accounts for it (§4.6) | | any rewrite at or below an anchored `seq` | **yes**: the hash there differs | | §2.2's forged append | **no.** It lands at head + 1, above every anchored `seq`, so no anchored pair stops reproducing. A later anchor freezes the forged chain as readily as an honest one | | receipts written and erased entirely between two anchors | **no.** They were never at or below an anchored `seq` | @@ -209,9 +214,24 @@ design avoided. | Call | Answers | |---|---| -| `make(seq, hash)` | returns an opaque token, or raises | +| `make(seq, hash, kind)` | returns an opaque token, or raises. `kind` is `interval` or `checkpoint` | | `check(seq, hash, token)` | whether that pair and that token correspond | -| **`latest()`** | **the highest `seq` the provider itself holds an anchor for, and its token** | +| `latest()` | the highest `seq` the provider holds an anchor for, and its token | +| **`since(seq)`** | **every anchor the provider holds at or above `seq`.** Enumeration, not a single answer | + +**`since()` is why §4.6's argument is not circular.** §4.6 says an attacker who launders an erasure +must leave an anchored checkpoint in the provider's record, so an operator can see a prune happened. +With `latest()` alone the kernel can read only its own local table for that history, and §3.3 spends +a subsection establishing the local table is a cache the writer under suspicion can trim: delete +every local row at or below the laundering checkpoint and nothing above it is missing, so `latest()` +reveals nothing. Enumeration moves the history to the side that cannot be rewritten. + +**An anchor carries its `kind`, and `interval` and `checkpoint` are ordered separately.** An earlier +draft ordered all anchors by `seq` and required each to be above the last, which a review showed +refuses the one anchor §4.6 requires: a deployment anchoring hourly and pruning at ninety days makes +its checkpoint anchor far *below* its newest interval anchor, so the rule refused it, so the prune +was refused, **forever**. §4.6 was written because an anchoring deployment should not have to choose +between pruning and a permanent tamper signal, and as drafted it landed on the first horn. `latest()` is the one that closes the gap, because it is answered **outside**. CTRLRun's table is then a cache and not a record: if it names fewer anchors than the provider holds, the provider wins @@ -229,10 +249,11 @@ and the missing one is checked anyway. - **An anchor whose time runs backwards against the one before it is refused.** A monotonic sequence is the only property the kernel can check about a timestamp it did not issue, and an anchor sequence that goes backwards is either a misconfiguration or the attack. -- **An anchor whose `seq` is at or below the one before it is refused**, which is the same rule on - the other axis and §4.5's rule for a checkpoint. The first draft ordered only time, while - `latest()` is defined on `seq`, so nothing required the two orderings to agree and an anchor could - be made backwards in `seq` while moving forwards in time. +- **An `interval` anchor whose `seq` is at or below the previous `interval` anchor is refused**, and + a `checkpoint` anchor is ordered only against other checkpoints. The first draft ordered only time + while `latest()` is defined on `seq`, so nothing required the two orderings to agree; the fix for + that then refused every checkpoint, which is why the two kinds are ordered separately rather than + jointly. ### 3.3 Where it lives, and the question that decides it @@ -263,7 +284,7 @@ file is worth. The sentence `SPEC-v0.8.md` §6.6 and `THREAT_MODEL.md` both use unchanged: it is worth what its source is worth, and the documentation says so where the feature is described. -### 3.4 The two break kinds, and the report they are not in +### 3.4 The three break kinds, and the report they are not in **`CHAIN_BREAKS` does not change. It stays closed at six, and `verify_chain` is not touched.** @@ -286,9 +307,30 @@ So the anchor gets **its own report and its own closed set**, `ANCHOR_BREAKS`, a | Kind | When | |---|---| -| `anchor_broken` | an anchored pair does not reproduce: the anchored `seq` is **present and hashes differently**, or it is absent and **not accounted for by a checkpoint** (§4.6). §2.4's table is what this does and does not cover, and an append is not in it | -| `anchor_missing` | **a configuration that anchors holds no anchor at all**, or the provider's `latest()` names an anchor the local table does not have | -| `anchor_unavailable` | the provider cannot be reached **at verification time**. Never a pass, and named rather than silent | +| `anchor_broken` | an anchored pair does not reproduce: the anchored `seq` is **present and hashes differently**, or it is absent and **not accounted for by an anchored checkpoint** (§4.6). §2.4's table is what this does and does not cover, and an append is not in it | +| `anchor_missing` | **a configuration that anchors holds no anchor at all**, or `since()` names an anchor the local table does not have | +| `anchor_repudiated` | `check()` answered **no**: the provider does not recognise a pair the local table claims it anchored. A forged or revoked token, or a provider that disowns the pair | + +**`anchor_repudiated` exists because the outside record is allowed to say no.** The first draft's set +had no name for `check()` returning false, which is the provider's one substantive answer and the +entire reason for holding the record outside the store. A refusal with no name is the shape §3.4 +exists to fix. + +**`anchor_unavailable` is NOT in this set**, and an earlier draft put it there. It is a **transport +failure**, not a finding about the evidence, and a set that conflates the two teaches an operator to +ignore the ones that matter: a timestamp authority briefly unreachable would grade `G28` `fail`, +indistinguishable in the report from a truncation. `SPEC-v0.10.md`'s `upstream_unverified` is the +precedent and it cuts the other way: it is a **decision-time refusal**, not a break in a verification +report. **Refusing to act when you cannot ask is fail-closed; reporting tampering when you cannot ask +is a false positive**, and §3.4's own argument against the old `anchor_missing` applies one level +out. So an unreachable provider makes the report `unavailable` rather than `ok` or broken, `G28` +grades `N/A` with that reason, and §10 carries both rows. + +**Precedence, because two rows could both hold.** In the canonical attack, truncate the chain and +delete the newest local anchor, both `anchor_broken` and `anchor_missing` apply. **`anchor_broken` +wins**, and the report carries it: `anchor_missing` reads to an operator as a misconfiguration and +`anchor_broken` reads as tamper, and naming the milder one first is how a real finding gets filed as +a config ticket. **`anchor_missing` does not fire on the exposed window, and an earlier draft made it do exactly that.** That draft read *"the store's chain reaches a `seq` none of them covers"*, which is the state @@ -308,11 +350,6 @@ check that fires on the honest case is not fail-closed, it is broken**, and `SPE rule about a guarantee that could not have failed has a mirror image here: a guarantee that could not have passed. -**`anchor_unavailable` is in the set, and it was not.** §3.2 requires the provider to be consulted at -verification time and requires a raise never to be a pass, and the first draft had no name for what -the report carries when that happens: it named the reason in §10 from the `make` side only. A -refusal with no name in the closed set is the shape §3.4 exists to fix, one report out. - This is better than the amendment on three counts, and the third is the one that decides it. `G11` is genuinely untouched rather than argued to be. `SPEC-v0.6.md` §6.5's closed set stays closed, so this milestone amends one frozen surface instead of two. And §9's frozen table can name @@ -323,7 +360,7 @@ claim the frozen-name test's shape cannot express. `upstream_unverified` in a new place: an anchor that is never made would otherwise switch the check off by being absent. `SPEC-v0.4.md` §3.8's false green is the failure this refuses. -A configuration that does **not** anchor reports neither, and `G28` is `N/A` with a reason true of +A configuration that does **not** anchor reports none of them, and `G28` is `N/A` with a reason true of the operator's document. Anchoring is opt-in and then fail-closed, which is the rule `SPEC-v0.3.md` states in its preamble and every item inherits. @@ -465,6 +502,25 @@ implementer codes refusals from. `NEW` is not in the table because `effect.py` says it "is never written to a store". +**The window is supplied to the prune, not resolved by it (O7).** A review found the first draft's +version uncomputable: a ledger row carries `grant_id`, `metric`, `amount`, `effect_key`, `attempt`, +`consumed_at` and `released_at`, and **no window and no limit**. Those travel on `Charge`, from the +authority document, and `state.py` says why in as many words: *a store that resolved a grant's +budgets would be reading the policy*, which `ARCHITECTURE.md` §6 forbids. + +So resolving the window inside the prune would reinstate exactly the dependency §4.2 removes, and it +has two failure modes with no good answer: a row whose `grant_id` is no longer in the document has no +window at all, and a window an operator lengthens later retroactively un-prunes rows already pruned. + +**`ctrlrun prune --older-than` takes a duration and the prune refuses any `COMMITTED` row newer than +it.** The operator supplies the number, as they supply the range, and the kernel checks the rule +rather than deriving the input. That is `SPEC-v0.9.md` §5.4's shape once more: the provider answers, +the kernel matches. It also makes the refusal computable from the ledger alone, which is the property +§4.2 needs. + +The operator is told what number to use, and it is the only advice this section gives: **the longest +window on any budget of any grant**, which `SPEC-v0.9.md` §7.3 makes a safe over-approximation. + A prune that released a hold by deleting it would be manufacturing authority, which is the hole `SPEC-v0.9.md` §4 exists to close. A prune that refused to touch `COMMITTED` rows would be a retention feature that retains everything. @@ -513,6 +569,12 @@ Neither is refusable alone, and together they break rule 2. So: draft never said which came first, so the two rules were unsatisfiable together on the shipped store. Before, and the crash window is the safe one: a receipt for a prune that did not happen over-reports, where a prune with no receipt is indistinguishable from §2.1. +- **That receipt records an intent, and its outcome is recorded against it.** Writing it first means + it is already in the chain when the hold check and every §10 refusal run, so a **refused** prune + would otherwise leave a receipt asserting an erasure that never happened. That is not the crash + window, it is the ordinary outcome of `ctrlrun prune` against a held range. The receipt carries + what was *asked for*, and its refusal is an ordinary `DENIED` result on that same action, which is + what every other refusal in this kernel already does. ### 4.6 An anchor and a prune, which cancelled each other @@ -593,14 +655,17 @@ what lets a refused row carry a position at all and what makes the docstring tru message: `SPEC-v0.7.md` §6.11's rule, because the canonicalizer quotes what it refused and a lone surrogate in a report is a report that cannot be printed. -Every reader then chooses. Every caller of that shared read chooses: `receipts` prints the row as unreadable and prints the others, and so does the operator server's `_receipts` tool. +Every caller of that shared read chooses: `receipts` prints the row as unreadable and prints the others, and so does the operator server's `_receipts` tool. `verify_chain` reports `content_altered` at that `seq`, which is what it already does for a document it cannot hash, so one tamper reads as one break whichever half catches it. `inspect` on an unrelated action never sees it at all, which is the case §2.3 measured. ### 5.3 The negative control -**A store with no bad row reports exactly what it reports today**, byte for byte, on every reader. +**A store with no bad row keeps working for everybody whose store is intact**, and that is the +claim rather than "byte for byte on every reader": item 1 deliberately changes one thing about a +clean store's output, because §5.2's `SELECT seq` makes a receipt's position come from the column +instead of from the document. This is the half that is easy to lose: a change that made a clean chain read differently would be a change to shipped output, and item 1 is not a change to shipped output for anybody whose store is intact. @@ -613,11 +678,11 @@ intact. (0.7), `v5` (0.8), `v6` (0.9), `v7` (0.10). The count is taken from `receipt.py`'s constants, which is the only place it cannot be stale. -`ROADMAP.md`'s v0.11 prose said four and was corrected. **Its Exit line still says four**, and that -is the line `G31` is graded against, so item 4 corrects it there in the same edit. The same Exit line -also requires that *the checkpoint receipt of a prune carries the version current when it was -written*, which no guarantee in §8 covers: item 3 asserts it, because a checkpoint written today and -read in two years is the case this milestone exists for. +`ROADMAP.md`'s v0.11 prose said four, and so did its Exit line, which is what `G31` is graded +against. Both are corrected there. The Exit line also requires that *the checkpoint receipt of a +prune carries the version current when it was written*, which no guarantee in §8 covers: item 3 +asserts it, because a checkpoint written today and read in two years is the case this milestone +exists for. **No new field.** The version string already exists, and the rule since `SPEC-v0.3.md` §12.2 is that every reader upgrades before any writer switches. What is new is the proof. @@ -665,9 +730,10 @@ own output in the shape `CLAIMS.md` uses. | Id | Grades | Item | |---|---|---| | `G28` | a chain truncated at or below an anchored `seq` is refused against its anchor | 2 | -| `G29` | a prune across a checkpoint leaves a chain that verifies | 3 | +| `G29` | a prune leaves the chain with no break it did not already have | 3 | | `G30` | a held range refuses to prune | 3 | | `G31` | a chain spanning five receipt schema versions verifies end to end | 4 | +| `G32` | **an honestly pruned chain leaves a clean anchor report** | 3 | Each with a positive control, each graded or `N/A` with a reason true of the operator's document, and **each grading the same under `--only` as in a full run**. `SPEC-v0.9.md` §13.8 records G22 passing @@ -680,18 +746,25 @@ guarantee's text in `ctrlrun.guarantees/v7` and in `ctrlrun verify`'s output. Co that argues a claim and leaving the claim in the registry is worse than not correcting it: the argument is read once and the registry is read by every operator who runs `verify`. -**The same uncorrected sentence is on `ROADMAP.md` line 389**, the Exit line `G28` is graded against: -*"the truncation and append cases that `SPEC-v0.6.md` §6.4 lists as undetected now detect."* §6 of -this document quotes that very line for a different reason and did not notice. **Item 2 corrects it -there**, in the same edit that corrects line 378. +**The same claim was on `ROADMAP.md`'s Exit line for v0.11**, which is what `G28` is graded against: +*"the truncation and append cases that `SPEC-v0.6.md` §6.4 lists as undetected now detect."* It is +corrected there now, along with the anchor bullet above it. **Cited by its words and not by a line +number**: an earlier draft of this document gave three different line numbers for two sentences in +another repository, and all three were wrong within a day. **`G28`'s positive control is the attack in §2.1**, run against a real store: truncate, fix the head, require the break. A guarantee whose scenario has never seen the attack it exists for is `SPEC-v0.4.md` §2.2's guarantee that could not have failed. +**`G32` exists because §4.6's defect class would otherwise turn nothing red.** `G28` grades +truncation against an anchor and `G29` grades a prune against the chain; the *interaction*, an honest +prune leaving the anchor report clean, was graded by neither, and that interaction is the one a review +found had made items 2 and 3 mutually exclusive. A guarantee for each half and none for the pair is +how two correct sections ship cancelling each other. + ### 8.1 `G11`'s contract does not change, and §3.4 is what makes that true (O6) -O6 asked whether the two new break kinds are reported as `G11` failures or as a new guarantee. **A +O6 asked whether the new break kinds are reported as `G11` failures or as a new guarantee. **A new guarantee, and `G11` is untouched.** `G11` is *an altered receipt is detected*, shipped and graded since v0.6. Routing `anchor_broken` @@ -708,7 +781,7 @@ by an argument. `G11` grades the hash chain, which every deployment has, and can break. `G28` grades the anchor, is opt-in, and is `N/A` with a reason on a deployment that does not anchor. -**Item 2 asserts this directly**: `G11` passes on a store whose anchor report carries both kinds. A +**Item 2 asserts this directly**: `G11` passes on a store whose anchor report carries every kind in `ANCHOR_BREAKS`. A guarantee whose independence is argued rather than run is what this section already got wrong once. --- @@ -720,19 +793,21 @@ One justification per row. Anything not here is a spec amendment before it is co **`SPEC-v0.10.md` §9.4 is why this section is written differently from its predecessors.** Three of v0.10's §9 rows were frozen and never built, and nothing turned red because no test asserted that a frozen name exists. That test now exists. **Every row below names the item that builds it**, and the -release item adds each to the frozen-name list or records in §12 why it was deliberately not built. +release item adds each to the frozen-name list or records in §13 why it was deliberately not built. | Symbol | Item | Why an existing name does not serve | |---|---|---| | `ctrlrun.anchor.AnchorProvider` | 2 | the operator's own code answering from the operator's own system, in the shape `SPEC-v0.9.md` §5.4 settled for a scope provider. Three calls, not two (§3.2), and `latest()` is the one that makes §3.3 true. A default implementation that fetched anything would put a network client in the wheel every user installs | -| `ctrlrun.anchor.ANCHOR_BREAKS` | 2 | its own closed set, because putting the two kinds in `CHAIN_BREAKS` fails `G11`'s control (§3.4). A **symbol**, so the frozen-name test asserts it by import rather than by membership | +| `ctrlrun.anchor.ANCHOR_BREAKS` | 2 | its own closed set, because putting them in `CHAIN_BREAKS` fails `G11`'s control (§3.4). A **symbol**, so the frozen-name test asserts it by import rather than by membership | | `ctrlrun.anchor.verify_anchors` | 2 | the walk that produces an `AnchorReport`. Separate from `verify_chain`, which is not touched | | `ctrlrun.anchor.AnchorReport` | 2 | what `verify_anchors` returns | | `anchor=` on `Control` | 2 | a deployment anchors or it does not; it is a property of the deployment, not of an action, so it does not go on `execute` | +| `ctrlrun.receipt.UnreadableReceipt` | 1 | §5.2's refusal, carried **by type and never by message**. The first draft of §9 had no row for item 1 at all, which is `SPEC-v0.10.md` §9.4's failure in the mirror direction: a public name shipping with no frozen row | +| `ctrlrun.state.StateStore.receipts` yields `Receipt | UnreadableReceipt` | 1 | **amends `SPEC-v0.6.md` §9.2's frozen protocol**, and both backends change: the read gains `SELECT seq` (§5.2) and stops raising on one bad row. The bar is cleared because a second backend cannot implement §5 without it | | `ctrlrun.state.StateStore.put_anchor` / `.anchors` | 2 | **amends `SPEC-v0.6.md` §9.2's frozen protocol.** The bar is *a second backend could not be written without it*, and an anchor's local cache cannot be reconstructed from the tables that exist | | `ctrlrun.state.StateStore.put_checkpoint` / `.checkpoint` | 3 | the same amendment. §4.2 is why a checkpoint the walk trusts cannot live in a receipt document | | `ctrlrun.state.StateStore.put_hold` / `.holds` / `.release_hold` | 3 | **the first draft froze `ctrlrun hold` with no storage at all**, and `G30` grades a held range refusing to prune against a table that did not exist. A review found it; this is the row that was missing | -| `ctrlrun.migrations.MIGRATIONS` contains an entry whose `.id` is `0008_anchor_checkpoint_hold` | 2, 3 | the three tables above. **Written as a membership claim on a named symbol, because a migration id can never be an attribute path**: `hasattr(ctrlrun.migrations, "0008_…")` can never be true, a name starting with a digit is not an identifier, and a review showed the previous wording was still unwritable as a test row. So the frozen-name list gains a second shape, `(module, symbol, member)`, and this is its only user | +| `ctrlrun.migrations.MIGRATIONS` contains an entry whose `.id` is `0008_anchor_checkpoint_hold` | 2, 3 | the three tables above. **A membership claim on a named symbol, because a migration id can never be an attribute path**: `hasattr(ctrlrun.migrations, "0008_…")` can never be true, since a name beginning with a digit is not an identifier. The frozen-name list's rows gain an explicit **kind** (`parameter` or `member`), because the existing three-tuple shape already exists and a bare third element cannot say which check to run: a review put this row into it and got `TypeError: ... is not a callable object` from `inspect.signature` | | `ctrlrun anchor`, `ctrlrun prune`, `ctrlrun hold` | 2, 3 | CLI commands. An anchor is made on a schedule by an operator and a prune is an operator's act (§4.2), where every other surface in this kernel is a library call made by an agent. §11 keeps the management plane off the roadmap and these are not one: each writes rows and prints lines | **Every row above names something a test can assert**, and the shape it needs is stated per row. A review put @@ -762,12 +837,13 @@ that fills. The prune's own receipt is where approval belongs, and §4.2 puts it | Situation | Result | |---|---| | the anchor provider raises, times out, or answers a shape the canonicalizer refuses **when an anchor is made** | `anchor_unavailable`; the anchor is not made and nothing is recorded as anchored | -| the same, **at verification time** | `anchor_unavailable` in the report, never a pass. The first draft wrote this row from the `make` side only and had no name for the verification side | -| an anchor whose `seq` is at or below the one before it | refused (§3.2) | +| the provider cannot be reached **at verification time** | the report is `unavailable`; `G28` is `N/A` with that reason. **Not a break, and not a pass.** An earlier draft made it a break, so a briefly unreachable timestamp authority graded `G28` `fail`, indistinguishable from a truncation | +| an `interval` anchor whose `seq` is at or below the previous `interval` anchor | refused (§3.2). A `checkpoint` anchor is ordered only against other checkpoints, and an earlier draft's joint ordering refused every prune | | a configuration anchors and the store holds **no anchor at all**, or `latest()` names one the local table lacks | `anchor_missing`, a break, never a pass. **Not** the ordinary window `(last anchored seq, current head]`, which §2.4 blesses | -| an anchored pair does not reproduce | `anchor_broken` | +| an anchored pair does not reproduce, **and no anchored checkpoint accounts for it** | `anchor_broken` (§3.4, §4.6). An anchor below an anchored checkpoint is **superseded**, not broken | +| `check()` answers no for a pair the local table claims was anchored | `anchor_repudiated` | | an anchor's time runs backwards against the one before it | refused | -| a prune that would leave the chain reporting a break **the prune caused**: any of `CHAIN_BREAKS`' six that the same store did not report before it | refused, with the `seq` named. **Not "any break".** A review found that `unchained` is a pre-existing condition on any store migrated from v0.1 to v0.5, survives a prefix prune, and can never be removed by one, because the row has no `seq` to be in a prefix of. "Any break" makes retention permanently unavailable on the oldest and largest stores, which are the ones it is for | +| a prune that would leave the chain reporting a break **the prune caused**: a `(kind, seq)` pair the same store did not report before it | refused, with the `seq` named. **Per pair, not per kind**: a store already reporting `missing` at `seq 7` must not thereby admit a new `missing` at `seq 1`. `unchained` carries no `seq` and is compared as `(unchained, None)` | | a prune through the chain's head | refused. It leaves no chained receipt for the head to name | | a checkpoint naming a `seq` at or below the one already recorded | refused (§4.5): this is the second of two racing prunes | | a prune that would delete a ledger row whose effect is `AMBIGUOUS`, `RESERVED` or `EXECUTING` | refused (§4.4) | @@ -845,9 +921,9 @@ the dominant shape was *a fix applied to the argument and not to the artifact*: |---|---| | §2.4's append claim, rewritten as a table | the claim survived in **§8's `G28` row**, which is the text that becomes the graded guarantee, and on `ROADMAP.md`'s Exit line | | `anchor_missing` moved out of `CHAIN_BREAKS` so it stops failing `G11` | its **definition** was untouched, so it fired on every honest deployment and failed `G28` universally instead | -| §4.4's release rule replaced with settlement | §10 carried the **unconditional** version, and pruning a `COMMITTED` row inside §7.3's window manufactures budget authority | +| §4.4's release rule replaced with settlement | §10 carried the **unconditional** version, and pruning a `COMMITTED` row inside `SPEC-v0.9.md` §7.3's window manufactures budget authority | | §9's three unwritable rows named | the migration row **still cannot be an attribute path**; naming it did not change its shape | -| §11.1 declared the citation class closed | **three new citation defects in the new text**, one quoting a paraphrase as if it were a file's words | +| §12.1 declared the citation class closed | **three new citation defects in the new text**, one quoting a paraphrase as if it were a file's words | **And one nobody looked for in either round until it was searched for: §4.6.** Items 2 and 3 were specified in isolation, each verified alone, and cancelled each other. §3 did not contain the word @@ -859,6 +935,36 @@ did while fixing it. A milestone that stops at one round ships the second set. --- +### 12.3 Round three: fourteen findings, and what the three rounds say about the document + +The pattern did not stop. Round two's new §4.6, written to fix two sections that cancelled each +other, **cancelled against a rule round two added in the same commit**: §3.2 required every anchor's +`seq` to exceed the last, and §4.6 requires anchoring a checkpoint far below the head, so no prune +could ever run. The section that names the cross-module class reproduced it one round later. + +| Round | Findings | Of which introduced by the previous round's fixes | +|---|---|---| +| one | 12 | n/a | +| two | 15 | 10 | +| three | 14 | most of the high ones | + +**What the three rounds actually diagnose is scope.** Almost every high finding after round one lives +in the *interaction* between the anchor (item 2) and retention (item 3): an honest prune breaking +every older anchor, the checkpoint anchor refused by the anchor ordering, the laundering attack on +"superseded", the ledger window that is not computable without reinstating a dependency §4.2 removed. +The anchor alone and the reader alone generated few defects and no high ones after round one. + +**That is the evidence for the question §1 leaves open**, and it is now a much sharper question than +it was when §1 was written. It remains the maintainer's, and this section exists so it is decided +from measurements rather than from a sense of how big the milestone feels. + +**The sweep this round asked for, adopted as a rule.** After any change to a definition, re-derive +§1.1's rules, §2.4's table, §8's registry and §10's rows from it, rather than editing the row that +motivated the change. Every one of round three's `HIGH` findings and half its `MEDIUM` ones was a +definition changed in one place and left standing in another. + +--- + ## 13. What building v0.11 settled Written by item 6, in one pass, from the CHANGELOG line each item leaves.