SPEC-v0.11 review round three: fourteen findings, and the scope question they answer

[arpanghoshal]

Stacked on #196. Third round, on the rule that gave v0.9 and v0.10 three each.

§4.6 cancelled against a rule added in the same commit

Round two wrote §4.6 because two sections cancelled each other. It then cancelled against §3.2's
new monotonicity rule, added in that same commit:

• §3.2: "An anchor whose seq is at or below the one before it is refused."
• §4.6: "anchor the checkpoint, then delete", the checkpoint being at the pruned-through seq.

Anchoring hourly and pruning at ninety days, the checkpoint sits far below the newest anchor. So
the checkpoint anchor is refused, so every prune is refused, forever. §4.6 exists because a
deployment should not have to choose between pruning and a permanent tamper signal; as drafted it
landed on the first horn.

Fixed by giving anchors a kind: interval and checkpoint are ordered separately.

The "superseded" defence needed a call that did not exist

§4.6 claims an attacker who launders an erasure must leave an anchored checkpoint an operator can
see. The frozen provider had make, check, latest and no enumeration, so the only anchor
history the kernel could read was the local table, which §3.3 spends a subsection establishing is a
cache the writer under suspicion can trim. Delete every local row at or below the laundering
checkpoint and latest() shows nothing.

Two fixes, both needed: the provider gains since(seq), 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 grant_id, metric, amount, effect_key, attempt, consumed_at,
released_at. No window, no limit. Those travel on Charge, and state.py says why: a store
that resolved a grant's budgets would be reading the policy.

So resolving it inside the prune reinstates exactly the dependency §4.2 removes, and a row whose
grant is no longer in the document has no window at all. The operator supplies it:
ctrlrun prune --older-than. The kernel checks the rule rather than deriving the input, which is
SPEC-v0.9.md §5.4's shape again.

anchor_unavailable leaves the break set

A transport failure is not a finding about evidence. In the set, a briefly unreachable timestamp
authority grades G28 fail, indistinguishable in the report from a truncation. SPEC-v0.10.md's
upstream_unverified is the precedent and 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 it is §3.4's own argument one level out.

anchor_repudiated joins the set, because check() answering no had no name and it is the
provider's one substantive answer.

G32

G28 graded truncation against an anchor, G29 graded a prune against the chain, and the
interaction §4.6 exists to fix was graded by neither. A guarantee for each half and none for the
pair is how two correct sections ship cancelling each other.

Also

Rule 2 and §8's G29 still stated the absolute where §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;
§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.

What three rounds actually diagnose

Round	Findings	Introduced by the previous round's fixes
one	12	n/a
two	15	10
three	14	most of the high ones

Almost every high finding after round one lives in the interaction between the anchor (item 2) and
retention (item 3), not in either alone: the honest prune breaking every older anchor, the
checkpoint anchor refused by the anchor ordering, the laundering attack, the uncomputable window. The
anchor alone and the reader alone generated few defects and no high ones after round one.

§1 leaves open whether this is one milestone or two. That question is now answerable from
measurements, and §12.3 records them. It remains the maintainer's.

Every cross-reference resolves. No em dashes.

Not merging.

[coderabbitai]

Warning

Review limit reached

Next included review available in 36 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Advanced

Run ID: 435023ae-6ab0-4038-aaad-56acd4c34984

📥 Commits

Reviewing files that changed from the base of the PR and between ac1d5d8 and b3bcd35.

📒 Files selected for processing (1)

• docs/SPEC-v0.11.md

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}