Denominate the enrolment margin in eval steps: the plan, and Phase 1's model

[gunbai-bot]

DRAFT — Phase 1 is landed and green; Phases 2–3 are not started. This body is the durable statement of what is in and what is pending, written for someone picking the lane up cold.

Plan document: docs/plans/enrolment-margin-eval-step-denomination.md

---

Status

In	Phase 1 — the carrier. Green at 574602505fb, run 34853617920, all four jobs.
Pending	Phase 2 (the enrolment margin), Phase 3 (the CPU line), the plan-doc link, and a separate attribution lane.
Before undraft	The plan doc must be linked from the drop row it discharges. Not done — see Owed below.

---

Why this lane exists

gunbc#11195 moved the required floor's claim ceiling onto eval steps and made CPU observed-only for every claim. It did not move every per-subject budget. v2.workflow.floor_enrolment_margin still derives a 302ms budget from required_floor_per_subject_cpu_line_ms and compares an observed CPU reading against it, so a newly enrolled witness can still be refused on a figure that is a property of the machine rather than of the claim.

That is clause (iv) of the §4b(3) drop floor_cost_cpu_regression_at_constant_eval_steps, in the trigger's own words:

NO PER-SUBJECT BUDGET MAY CONSUME A RUN-LEVEL READING

and it is the only clause #11195 left standing. A drop is retired by its trigger and by nothing else, so the drop stands until Phase 3 completes.

---

Phase 1 — IN, green at 574602505fb

The step count moved inside the ClaimCostReading arms:

ObservedCpuReading          { cpu_ms, eval_steps }
RightCensoredCpuReading     { cpu_lower_bound_ms, censoring_ceiling_ms, eval_steps_before_censor }
CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms, eval_steps_before_censor }

with observed_eval_steps (Present on the observed arm only — the point question) and eval_steps_at_least (total over all three — the one question a stopped row answers soundly). FloorCostRow.eval_steps: Int is deleted, not deprecated.

This executed the next_rung_trigger of gunbc.guarantee_stall.eval_steps_outside_the_reading_coproduct_stall verbatim, so that stall is retired — roster entry and file removed, because a stall is a standing state and this class moved.

Inside the arms rather than a sibling coproduct, because a sibling satisfies the trigger's letter while leaving the incoherent row constructible: an observed CPU reading beside a before-censor step count. Whether the claim reached its end is one fact about one occurrence and it discriminates both readings. Not clock fusion — no arm compares a step count to a millisecond.

What Phase 1 surfaced

Three sites were silently treating a bound as work performed. This is the return on cutting at the root rather than adding a field:

• The equal-work inflation cohort paired rows on step equality, so a censored row whose before-censor count happened to equal a completed row's performed count joined the cohort, and the whole difference between them was then attributed to inflation. performed_steps_agree now refuses it — including two equal bounds, since "at least N" twice says nothing about whether the two claims did the same work.
• The determinism comparison gained a fourth arm, CompletedIdentityStepsNotPerformed, because verdict_reached and the cost reading are independent axes: reaching a verdict does not entitle a fold to a performed count.
• row_step_count_is_complete is deleted — a Bool beside the value, where the accessor now performs the case split. Its own annotation already said "the same arm that censors the cost censors the steps".

Evidence, executed

Read from the green run's own required_floor_claim_cost artifact (executed=3840), not inferred from a green lane — the floor log prints only non-PASS lines, so green alone does not distinguish passed from never ran:

witness	role	result
two_equal_bounds_do_not_agree_on_performed_work	RED	pass, verdict reached
the_point_question_answers_on_one_arm_and_the_bound_question_on_every_arm	control	pass
a_parsed_row_takes_eval_steps_from_the_steps_column	migrated parse	pass

The RED is red only because the count moved: a bound is not reachable through observed_eval_steps at all, so no re-spelling of the comparison recovers the old answer.

Two corrections recorded, so they are not re-derived

• No Rust changes, and none were needed. An earlier census in this lane said three seed files; it counted files mentioning eval_steps rather than files consuming the carrier. The seed does not mirror gunbc.floor_cost_distribution at all — its sites are the runner's own measurement and TSV emission — and Phase 1 changes no column. The artifact format is untouched.
• The first Phase 1 push was red on the floor lane while build was green. That is the acceptance-path disagreement floor_cost_distribution already documents: the whole-corpus strict path checks joins the entry-scoped path accepts. Both reds were mine — a non-exhaustive match on the arm Phase 1 added, and a Nat/Int branch join (eval_step_count_value returns Nat, as millisecond_count does; Nat widens to Int in argument position but not across an if-join, which is exactly where it refused). Repaired with the corpus's own extrema idiom — sort_by then first / first(reverse), as gunbc.roadmap_forecast does — rather than minting a Nat→Int conversion, which would have been the authoring-time workaround §5 names.

---

Phase 2 — PENDING: the enrolment margin consumes it

floor_enrolment_margin_budget_ms becomes an EvalStepCount derived through the same pinned calibration the claim ceiling uses (v2.workflow.floor_eval_step_calibration eval_step_budget_for), from a declared policy in milliseconds of work. Not a second calibration and not a literal: §5's oracle rule admits the budget only because it is grounded in a controlled fixture, and a second rate would fork that authority.

EnrolmentMarginStanding keeps its arms and changes their denomination — EnrolmentWithinMargin / EnrolmentOverMargin carry EvalStepCount, and the CPU reading is carried beside the verdict as an observation rather than deciding it, the shape #11195 gave the claim ceiling. EnrolmentBoundWithoutCeiling survives unchanged in meaning.

Evidence to author. RED: a claim whose eval steps exceed the enrolment budget refuses. CONTROL: a claim far over the 302ms CPU line with in-budget steps is admitted, with the CPU observation recorded. These must be re-authored here, not cited from #11195 — a different budget is a different subject.

Fixture note for whoever takes this. The enrolment-margin and debt-admission suites currently pass fixture_incidental_steps(), annotated as incidental because those fixtures exercise the CPU half and no assertion reads the count. Phase 2 gives them a real step parameter, at which point the value stops being incidental.

Phase 3 — PENDING: retire the CPU line, or say why it stays

required_floor_per_subject_cpu_line_ms exists only because two per-subject gates still read a CPU clock. After Phase 2 the enrolment margin is not one of them, and the remaining consumer is v2.workflow.floor_cost_debt_admission. Phase 3 decides that one: denominate it too and delete the symbol with its dissolution condition discharged, or keep it with a population of exactly one, stated.

Only when no per-subject budget reads a run-level figure does clause (iv) retire.

---

Owed before undraft

The plan document is not yet linked from the authority that governs it. Its home is the drop row it discharges (gunbc.rung_drop.floor_cost_cpu_regression_at_constant_eval_steps), and Phase 2 edits that row anyway. Note for whoever does it: touching a rung_drop row drifts docs/design-rung-drops.md, so run tools.docs_projection_gate regen before pushing. That regen refuses on BuildBuddy with HostBudgetUnreadable (no bound cgroup) but runs in a session container, which has memory.max set. Letting CI's heal do it instead costs a full CI cycle and the heal-pushed commit then stalls at action_required with zero check-runs until someone approves the run.

A separate lane, not part of this PR

fierce-lark ruled (2026-09-14) that a blocking floor red carries a typed attribution arm. Recorded here because it is a ruling, not a derivation, and it would otherwise be lost:

• ChangedByThisDiff — blocks, author owns.
• UnchangedIdentityRegressed — blocks, lane/roster owns; the author is told plainly it is not theirs.
• FirstMeasurementOfAnUnchangedIdentity — routes to roster/debt, blocks nobody.
• Unattributed — blocks. If any classification input is unavailable (no cut census, no selection receipt), this is the arm. Never default into the routing arm.

Attribution decides who owns a red, never whether it blocks — collapsing those two questions is what makes a two-arm shape look sufficient. A routing arm may never carry a regression. Define FirstMeasurement by fact: no prior accepted measurement of this identity exists in the floor's measured population (the frozen cut plus every later accepted measurement), and it was not selected as changed — not by roster absence, because after #11195 the roster is the cut minus declared removals, so a removed identity is absent without ever being new. Its RED: an on-roster, unselected identity over budget must classify as UnchangedIdentityRegressed, must block, and must not be classifiable as either other arm.

---

Deliberately not done

• Not re-arming a CPU ceiling anywhere. Floor cost ceiling: two tiers over eval_steps (grandfathered roster at 500ms-equiv, new witnesses at 100ms-equiv), CPU observed-only, §4b(3) drop #11195's evidence stands: three prose-only heads measured the same floor at 36.7s / 40.8s / 44.7s summed CPU, and one identity at an identical 2884 eval steps read 34ms, 455ms and 511ms. A CPU line refuses on the environment, not on the claim.
• Not normalising per runner, and not enrolling slow identities as cost-debt rows. Both are refused designs of record.

🤖 Generated with Claude Code

https://claude.ai/code/session_01D8Hk99iz2Q1H32CydKF6YS

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-09-14T16:47:51.546146Z	5746025	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 574602505f

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Keep lower-bound steps structurally distinct

When an equal-work consumer uses this new total accessor, the constructor distinction is erased: both an observed count and a before-censor lower bound become the same EvalStepCount, so eval_step_count_value(eval_steps_at_least(...)) can compare them without matching either reading. That is exactly the invalid cohort the deleted guarantee stall was meant to make unwritable; the safe implementation of performed_steps_agree only avoids the path in the current consumer. Preserve bound provenance in the return type (or keep the stall open) so future callers cannot silently reintroduce this comparison.

Useful? React with 👍 / 👎.