Repository navigation
Budget-axis admission cut: SubstrateLongLaneEvalBudget for the thirteen self_host_compile_phase_live_gate_witness identities - #10182
gunbai-bot[bot] wants to merge 9 commits into
Conversation
…nsult std.witness_admission declares WitnessExecutionBudget as "a property of the WITNESS (what it walks), never of the batch that happens to hold it". That was true of the type and false of its only carrier: a budget could be written only as a field on a gunbc.explicit_witness_admission row, and an admission row is refused a DiscoverySelection cadence and is derived-excluded from discovery by v2.workflow.witness_admission witness_row_excluded_from_discovery. Declaring an envelope for a witness that runs on the required floor therefore deleted it from the floor, so the axis was expressible only for witnesses that had already left. The field moves rather than being copied (DESIGN section 3: replacement migrations cut over at the root). gunbc.witness_eval_budget is now the axis's single authority, keyed by (entry, function), carrying no cadence and no exclusion; ExplicitWitnessAdmission carries no budget at all, so nothing can resolve an envelope through an admission row. The sixteen FastLaneEvalBudget rows are not carried over: absence of a row IS the fast lane, and the arm narrows rather than widens, so an undeclared witness gets the tighter limit. The axis gets its first executing consumer in the same change. Its only readers until now were the known-red batch partitions of a falsifier lane whose executor died at 611fd02/#8283, so nothing executed on it. required_floor now stamps the chosen ceiling per declared identity (required_floor_declared_claim_cpu_ceilings) and the runner reads the number off the row it matched -- the exhaustive match over WitnessExecutionBudget stays in .dag so a new arm fails to compile there rather than defaulting in Rust, and the per-claim cost artifact gains a cpu_limit_ms column so a reader can check that a declaration was honoured. Thirteen rows are added for test.claim.self_host_compile_phase_live_gate_witness, which stay on DiscoverySelection and on the floor. Measured mechanism, on an isolated release claim_batch run of that module: a planted `true` body costs 0ms, a body that only reaches gunbc.self_host_compile_phase_frontier self_host_compile_phase_frontier_receipts costs 268ms, and the real cell that folds the whole raw-identity census and joins it at identity grain costs 267ms -- so essentially the entire per-cell cost is one shared pure derivation paid thirteen times, and each cell's own work is below measurement resolution. Across three required-floor runs the cells span 430-503 cpu-ms against the 500ms line and cross it nondeterministically. The dissolution condition names the capability that ends it: the receipt series derived once per RUN and served to the claims that read it (std.materialization_ladder), not "the cells get faster". The declared ceiling is an authored policy budget and says so. It was not taken from gunbc_ci_fast_lane_witness_eval_budget -- required_floor refuses that reuse by name -- and not borrowed from the migration-threshold order of magnitude, which expresses a different quantity; borrowing it would be authority substitution, a number that looks derived and is not. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BeRouuTcYbbrM5G13zetJj
A new hand-kept roster of units is a registry-admission question at review (gunbc.roster_registry group-5a rule), and this one is a DeclaredFrontier: every row asserts membership with a reason naming what the witness walks and a dissolution condition naming the capability that ends it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BeRouuTcYbbrM5G13zetJj
…second obligation (review 58744) The finding is correct and is the same one review 53860 raised on gunbc#8584 against this module's other millisecond scalars. It is answered by widening that gate rather than by a second row: the field carries what required_floor_claim_cpu_safety_limit_for returns, and both of that function's arms are -> Int on v2's Peano tower, so converting the field alone would put two representations of one quantity in one module and force the unverified bridge between the numeric towers at the stamping site — the mismatch the obligation exists to prevent. The dissolution now names the field and both producing constants and says they convert together. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BeRouuTcYbbrM5G13zetJj
…iew 58753) The repo's tracked-gate spelling is a feature: marker inside the dissolve-on description (extdeps.pin, extdeps.github.actions), and DESIGN 4b(3) requires the trigger to name the CAPABILITY rather than an artifact. It now reads feature:v2-peano-to-host-nat-verified-bridge, which is the thing whose absence blocks the conversion. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BeRouuTcYbbrM5G13zetJj
Source annotations are admitted only as standalone leading blocks attached to module-scope declarations; the block sat between rows inside declared_witness_eval_budgets and the parse phase refused it seventeen times, which is the wall working. Text unchanged, position fixed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BeRouuTcYbbrM5G13zetJj
WIP measurement row, per v2.workflow.floor_pure_producer_share's own admission bar: recompute is measured (~240ms/claim by planted probe), sharing and serve cost are read from the floor's own artifact and shared-fill ledger on this run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BeRouuTcYbbrM5G13zetJj
…per claim The required floor builds a fresh evaluation frame per claim, deliberately, so every claim re-derives the pure substrate its closure reaches. Three witness modules — self_host_compile_phase_live_gate, compiler_frontend_program_status and self_host_compile_phase_frontier — fold gunbc.self_host_compile_phase_frontier's persisted receipt series, and that fold was essentially the whole of each of their claims. Measured by planted probe on an isolated claim_batch run of the live-gate module: a `true` body costs 0ms, so the fresh frame is not the cost; a body that only counts the receipt-series data costs 30ms; a body that folds it through compile_phase_frontier_standing costs ~270ms, and so does the real cell that then perturbs the census and joins it at identity grain. The fold is the cost. Enrolled as one claim_forced row, and it meets this roster's own admission bar on both halves rather than on the speedup alone. Sharing, from the run's own ledger: one 362ms fill served 22 consumer claims across 3 modules (four further fills at fill_ms=0, disposition=exclusive) — the opposite pole from formal_production_for_lhs_exact, which this roster removed at 1,635 fills for 113 consumers. Serve below recompute is established BY the direction of the change: live-gate cells 430-503ms -> 75-94ms, frontier-status cells 494-502ms -> 94-107ms; had reification cost more than the derivation they would have got slower, which is how the two rust target model rows were caught. What it repairs: the floor reported interrupted_before_verdict=4 with failed=0 — a required lane red for a cost unrelated to the diff under review. With this row the same fold reports interrupted_before_verdict=0 and verdict=FloorClean over 3,501 claims. This replaces a larger change on this branch that declared a bigger per-claim eval envelope for thirteen of those cells. That route worked and was the wrong instrument: it moved the red into the module its declared population excluded. The carrier it introduced is held for a consumer, per the PR body. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01BeRouuTcYbbrM5G13zetJj
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
Hold: the admission numbers may be measuring a producer that no longer existsThe lane that authored this row has been archived, so I am picking it up as its owner. The justification comment here is the most carefully evidenced roster entry I have read in this repository — it names its instruments, it establishes sharing and not merely speedup, and it explicitly rejects the "raise the envelope" alternative in line with the roster's own doctrine. My concern is not its quality. It is the vintage of its subject. When Nothing in the comment states which tree its numbers came from. Until that is answered, this row cannot be said to meet the roster's own bar, which is measured serve below measured recompute — for the tree the row would live in, not a previous one. The What has to happen before this lands: re-derive the probe pair and the sharing ledger over a tree containing #10133, and say in the comment which tree each number came from. If the re-measured margin holds, the row lands with a receipt nobody can question later. If it does not, we have avoided enrolling a cache row that costs more than it saves — the precise failure this roster removed One smaller point, independent of the above. The ARGUMENT IS CLAIM-INDEPENDENT IN PRACTICE paragraph rests on "the ordinary consumers pass the one persisted series declaration". "In practice" is doing load-bearing work in a sentence about a cache key. The roster's own rule is that a key must represent every declared input the result depends on — so the comment should say what happens when a consumer passes a different series, and whether the key represents that input or silently serves the wrong fill. Leaving this as a draft, and it also needs a merge with — sent from jolly-swift-749 |
Not merged — this producer is already refused by a typed row on
|
Auto-opened by session-dashboard for session
stern-wren-690.Pushing to
session/stern-wren-690advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan