Floor cost ceiling: two tiers over eval_steps (grandfathered roster at 500ms-equiv, new witnesses at 100ms-equiv), CPU observed-only, §4b(3) drop

[gunbai-bot]

What this is

The required floor's per-claim cost ceiling gates on eval_steps, not CPU. CPU is observed and published for every claim and decides nothing. The wall-safety deadline stays armed.

Why: three prose-only heads of #11173 showed all 3,775 floor claims uniformly ~10% slower twice, and one identity at a byte-identical eval_steps=2884 read 34ms / 455ms / 511ms. The 500ms CPU line sits inside an environmental band, so a CPU ceiling refuses on runner noise rather than on the claim. eval_steps is a property of the tree: the calibration specimen returned an identical count across architectures and load.

The ceiling is two-tier, and neither budget is a literal

• Grandfathered — identities enrolled at the cut commit, a closed roster at identity grain: 500ms-equivalent.
• New witnesses — anything not in that roster (a rename is a deletion plus an addition): 100ms-equivalent, and a breach refuses.

Both budgets are envelope_ms × pinned rate through v2.workflow.floor_eval_step_calibration. The rate is pinned from a controlled fixture whose recursion depth is a source literal — never a measurement of the live population (§5: "a measurement copied from the same current tree is not an oracle"). The pin takes the slowest reading in its sample, so drift tightens the ceiling rather than widening it.

Tier selection consumes roster membership from the identity alone. There is no legacy: flag, no caller-supplied label, and no way for an identity outside the roster to acquire the larger budget.

What it gives up, declared rather than carried quietly

A §4b(3) rung drop: CPU-time regressions at constant eval_steps now have no refusing wall on the acceptance path. The restoration trigger names a capability and quantifies over every per-subject budget, not just the ceiling that prompted it.

Evidence

22 witnesses in the budget module, executing: the over-budget refusal, a claim far over the CPU line with in-budget steps passing on either tier, the CPU observation still carried when another limit fires, the roster identity join in both directions, and three witnesses asserting this lane's own new claims are not grandfathered — which replaced two paragraphs that had asserted that rule while the mechanism was breaking it.

Two things a reader should know

The ceiling refused its own author. A witness added here asserted all three struck identities in one claim and performed 114,570 eval steps against the 72,300 new-witness budget. It is now three claims, one membership probe each — which is what the refusal text itself asks for. A ceiling that has refused its author once is better evidence that it bites than any fixture.

A comparison whose base is stale reports the subject as unchanged. Re-integrating the measure.dag cluster, git diff --stat showed 26 insertions and 0 deletions — clean — while a diff against origin/main showed 18 deletions: --stat compares to the index, and #11220 had landed mid-regen. Naming the ref you compare against, and making it the authority rather than the local one, is what caught it. Same class as the stale-mirror green earlier in this branch.

The #11297 collision, and why sed gets it wrong

floor_enrolment_margin landed on main (#11297) importing and calling required_floor_claim_cpu_safety_limit_ms — a symbol this branch deletes when the ceiling stops gating on CPU. Both files were taken from origin/main whole, #11297's semantics untouched, and only the references were repointed onto the survivor, required_floor_claim_work_envelope_ms, which carries the same 500ms grandfathered envelope.

It is not a textual substitution, because the two symbols have different return types — the deleted one returned Int, the survivor returns Millisecond. Three distinct treatments were needed:

site shape	treatment
millisecond(count: required_floor_claim_cpu_safety_limit_ms())	wrapper REMOVED: required_floor_claim_work_envelope_ms()
< required_floor_claim_cpu_safety_limit_ms() (bare-Int comparison)	unwrapping ADDED: < millisecond_count(m: required_floor_claim_work_envelope_ms())
the millisecond import left with no call site	trimmed from floor_enrolment_margin's std.measure import

Live-tense annotation citations of the deleted name in floor_cost_debt_admission and its test moved with the calls — a citation naming a symbol its own closure deletes is a dangling §3 reference. The single remaining mention, in required_floor itself, is past-tense and records the rename deliberately; it is not a miss.

Follow-up, named and deliberately not folded in: denominating floor_enrolment_margin itself in eval_steps rather than milliseconds, starting from #11297's shape.

🤖 Generated with Claude Code

[gunbai-bot]

Verified and fixed in 147860c8cb0.

The paragraph argued for the defect the code below it had already repaired

NotMeasured IS THE HONEST ARM AND NOT A DEGRADATION is this host's reasoning from before review 65264 — the review that found the collapse had left the model's arm with no producer on the acceptance path and put the operator-facing string the model forbids in front of an author. The fix landed. The argument for the defect did not leave with it.

What makes it worse than an ordinary stale sentence is where it sat: four lines above the expression that repaired it, arguing for the exact collapse the repair removed. A later reader reconciling code to comment would restore the defect and believe they were fixing an inconsistency. And as you note, the arm's own doc twelve hundred lines up already says the opposite in terms — collapsing into either neighbour loses the remedy — so the file carried both answers.

The paragraph now states what the code does and why neither neighbour fits: there is a reading, so NotMeasured's remedy ("produce a measurement") is the wrong instruction; and there is no CPU ceiling, so CeilingCensored has nothing to report beside the bound. I kept the superseded claim as recorded history rather than deleting it, because the next reader's question is "why not NotMeasured?" and the answer is the history.

On the pattern, since this is the eighth instance

This is round ten, and roughly the eighth instance of prose_repealed_by_the_change_that_wrote_it — the row this change files. Every detector I built was keyed on something this instance does not have:

• it cites no deleted symbol (my symbol sweep, round 5);
• it overstates no capability (round 6);
• it names nothing that fails to resolve (rounds 8 and 9).

It is simply the losing side of an argument the code already settled, left standing next to the winner. I don't have a mechanical check for that, and I don't think one exists short of the row's own trigger: an assertion about the tree needs an executing consumer in the same closure. A Rust comment has none by construction.

Annotations only; cargo clippy --all-targets -- -D warnings clean.

— sent from smart-heron-867

[gunbai-bot]

Both findings in review 65940 are real, both are confirmed, and both are fixed in 6124d37e912. rustc found the first independently at the same time; the second named a third site I had not yet reached. Thank you — the second finding is the one that mattered, because it identified the cause rather than the symptom.

The cause. #11297 landed on main calling required_floor_claim_cpu_safety_limit_ms, a symbol this branch deletes. I repaired that by taking floor_enrolment_margin.dag and its test from origin/main whole and repointing the references. That was wrong in one direction I did not check: the file is not only #11297's. EnrolmentBoundWithoutCeiling is this branch's arm, added in response to review 65264 — and taking main's copy deleted the model arm while leaving its Rust mirror standing. That is exactly the state the review describes: "the seed produces a standing the authority never declares."

Worth recording because a declaration-level diff is blind to it: #11297 only added declarations, so a symbol-level comparison of the two versions showed nothing lost. The loss was inside a coproduct. Nothing short of a compile or this review would have caught it.

What changed. The arm is restored on top of #11297's file rather than by choosing a side — the arm, its producer, its four total folds (including #11297's new enrolment_unpaired_pairing_hole), the import, and the rationale annotations that travelled with it.

The sweep was incomplete in two further places the review's second finding points at:

• EnrolmentDeclaredCostReading::Censored read r.cpu_safety_limit_ms. rustc suggested wall_safety_limit_ms. That suggestion is wrong — it prints a foreign clock's ceiling beside a CPU bound, the clock fusion std.measure measure_clock_basis_note exists to forbid. The arm is renamed BoundWithoutCeiling and carries no ceiling, because there is none.
• floor_cost_debt_row was non-exhaustive over the now-three-arm ClaimCostReading, as the review says. A bound with no ceiling can never establish the supplied ceiling, so it refuses — on its own arm. Reusing RefusedCensoredNotEstablished would mean filling censoring_ceiling_ms from the supplied ceiling: writing a figure the reading never carried into a field named for one it did.

Evidence, executing. The arm had no .dag witness at all — its only model-side evidence was a name-rendering match arm, which is what review 65264 objected to and what a naive restore would have re-created. Two witnesses now drive a CpuLowerBoundWithoutCeiling reading through the real folds: one asserts it refuses under a cause distinct from both neighbours it is tempting to collapse into, one asserts the debt admission refuses it without fabricating a ceiling.

— sent from smart-heron-867

[gunbai-bot]

Review 65986: every claim verified true, and the finding is correct. Fixed in 926b1f738ed.

I checked each one against the tree rather than taking it on the summary:

• the four identities are named as renamed/deleted in floor_grandfathered_removals — yes;
• each still appears in a chunk (exactly twice in the file: once as a disposition, once as a roster row) — yes;
• all_removals_name_roster_members required floor_grandfathered_holds to be true of each removal identity — yes.

So completing a removal would have turned the gate red. The disposition list could document a departure but never cause one, and both DESIGN citations land: §5's "a disposition list that cannot shrink the subject universe is not a removal mechanism", and §4b(1), because the header claimed the removal half "executes" while the only acceptance-path fold asserted continued membership.

I took neither of the two offered fixes, and the reason is worth stating. Deleting the four chunk rows destroys the only record that those rows were ever legitimate members — and with it the ability to check that a removal names a real member rather than a typo, which is what the old witness was reaching for. Treating the shrink as a frontier would have left the contract with no downward direction at all.

The cut stays frozen and the removals subtract. floor_grandfathered_holds is now the cut MINUS the declared removals. The universe shrinks monotonically, and every subtraction stays checkable against what was observed.

This also keeps the file's two existing mechanisms from collapsing into two names for one thing — a distinction the review could not have seen from the diff alone, since the strike predates it:

• a STRIKE edits the chunks because the cut itself was wrong — the row was never eligible, so the observation is corrected at its source. That is how three of this lane's own witnesses, wrongly captured by a mid-lane cut, were handled.
• a REMOVAL leaves the cut alone because the cut was right and the member later left.

The witness asserted the contract backwards and now asserts it forwards: every_declared_removal_names_a_cut_row_and_has_left_the_roster requires each removal to be present in the cut (the anti-fiction half) and absent from the roster after subtraction (the half that makes it a removal rather than an annotation).

One fork closed while here, which the fix would otherwise have opened: floor_grandfathered_roster() returned the un-subtracted cut, so after this change two surfaces named for the roster would have answered differently about membership — the §3 meaning fork. Renamed to floor_grandfathered_cut() / floor_grandfathered_cut_size().

On cost, since this sits on the floor's hot path and this PR's own ceiling gates on eval_steps: the cut scan short-circuits on a hit and the removal scan runs only after one, so a miss — the worst case this module measures, at 43,583 eval steps — pays nothing for the subtraction.

CI is running on 926b1f738ed; I am not claiming this green until it is.

— sent from smart-heron-867

[gunbai-bot]

Review 66007: both findings correct, both verified against the tree, both fixed in 2229cb7177c.

The fork is mine, and it came from a substitution by magnitude. When #11297 landed calling the deleted required_floor_claim_cpu_safety_limit_ms, I repaired it by repointing those call sites at required_floor_claim_work_envelope_ms — because both return 500. My own commit message said "carries the same 500ms envelope", which is the whole error in one clause: the question was meaning and I answered it with magnitude. The review is right that this is precisely the coincidence measure_clock_basis_note exists to warn about.

I confirmed the contradiction rather than taking it on the summary: floor_changed_witness states that the envelope is policy in milliseconds of work and "no clock is ever compared to it", while after my repair floor_enrolment_margin_budget_ms derived a CPU budget from it and judged observed CPU against that budget, and floor_cost_debt_admission took it as the CPU ceiling. Both statements could not be true.

I took the first of the two options offered: keep a CPU-denominated authority. required_floor_per_subject_cpu_line_ms — CPU milliseconds, compared directly against an observed CPU reading. It is not a nickname for the envelope: same magnitude, two quantities. It is not a deadline either — nothing is armed on it, since the only armed limits are the wall deadline and the eval-step ceiling.

It lands with its dissolution condition, and that condition is not new debt: it is clause (iv) of the rung_drop row this PR already declares — no per-subject budget may consume a run-level reading — made nameable rather than left implicit.

Repointed everywhere, including the live acceptance path the review specifically named: floor_enrolment_margin (both call sites), its test, floor_cost_debt_admission's prose, and required_floor_runner.rs, which read the envelope by name to bound the enrolment budget. One more site the review did not list, found by sweeping rather than by fixing what was reported: a witness comparing a 4000ms CPU figure to the envelope. The envelope's only remaining production consumer is the grandfathered tier's eval-step conversion, which is what it is for.

Second finding, also correct and also mine. The header said the floor "ALREADY refuses a newly enrolled witness that crosses the 500ms ceiling: it is interrupted". This change makes that false — nothing interrupts at 500ms of CPU any more. The remedy it describes still happens, by a different limit, so the sentence is corrected rather than deleted, with the correction recorded beside it. That is exactly the class this PR itself files, prose_repealed_by_the_change_that_wrote_it, and it is fair that the class caught its author.

CI is running on 2229cb7177c; I am not claiming green until it reports.

— sent from smart-heron-867