Repository navigation
XL-R-2: Consume the affected-set bound in regen — a round adjudicates only the mirrors one edit can change, and refuses when the bound cannot locate the edit - #9757
Conversation
…and digests only the mirrors one edit can change, and refuses when the bound cannot locate the edit gunbc.regen_affected_set has answered "which committed mirrors can this edit change" since #9744, and nothing consumed it. This makes it a selection the regen round acts on. THE SPLIT THAT MAKES A SELECTION SAFE, and it is the whole design: a round asks two different questions of the compared population and only ONE may be scoped. * POPULATION IDENTITY -- which mirrors exist on each side. EmittedNotCommitted, CommittedNotEmitted and the hand-maintained shadow are identity joins over rosters. They read no bytes, so there is nothing for a selection to save and everything for one to hide. They stay WHOLE POPULATION under every scope. * BYTE ADJUDICATION -- whether each committed mirror equals what emit produced. A read, a rustfmt normalization and a comparison per member, plus both tree digests and the candidate write. This is what the bound is a bound ON, and this is what the scope selects. So the scope bounds which mirrors' BYTES are compared. It never bounds which mirrors exist. THREE ARMS, AND THE THIRD IS THE POINT. AffectedMirrors selects its members intersected with the committed roster; WholePopulation is the existing path, byte for byte; EditedSetUnlocatable becomes a REFUSAL of the round, not a fallback to the whole population. "Regenerate everything" and "the selection could not answer" are different states, and a widening arm here would be denominated in the corpus rather than in the change -- the absorbing fallback DESIGN section 5 forbids, in the one place where its cost is unbounded. THE DRIFT GATE IS NEVER SCOPED. measure_generated_surface -- the required CI phase and the behavioural receipt -- passes WholePopulation explicitly. The selection is for the AUTHOR'S round, over a tree that gate has already verified, and the gate is what establishes the fixed-point precondition the scoped round relies on. That precondition is stated in the model rather than assumed: a scoped round cannot discover a mirror outside its selection that was committed stale, and the unscoped gate on every push and pull request is what closes it. EVIDENCE. `regen_emission_scope_tests`: the whole-population arm selects the whole population; an affected arm selects the intersection and not the bound's list verbatim (the red a member outside the tree discriminates); an edit touching no mirror selects nothing; and the refusal arm returns Err whose message is asserted NOT to be the population -- the discriminating red for a regression to widening, which every other check in the file would stay green through. Host and model are held to one answer by `render_scope_selection`, which runs v2.workflow.required_regen regen_scope_select through the interpreter, in the unit test and again on every scoped round. Instrument: `claim_executor --regen-round-cost --regen-affected-scope`, receipt at target/stage0-regen-round-cost.txt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
…nt's own carrier A reader pricing the affected-set scope needs to know which rows of this receipt it can move. mirror_write, candidate_verify, adjudicate, hand_verify and digest are the byte-denominated phases the selection bounds; install was already change-denominated (the regen's own drift answer is its install set); and compile.emit is NOT moved, because v1.compiler.emit_rust emit_rust renders every module before any selection is consulted and four aggregates in that same fold are denominated in the whole module population. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
…d construction, and the model could not be read
Two spellings of one mistake, both caught by execution and neither by any static check alone.
`Cons { head: name, tail: acc }` inside an `if` did not resolve at all: the taken branch is a
coproduct and the untaken one is the `List<String>` the accumulator was seeded with, so the
whole module failed to resolve and the host's lockstep call refused with "if branches resolve to
incompatible types: Coproduct(FreeMonoid) vs Container(List, Primitive(String))" (CI
rust-unit-tests at 7531b27).
`list_append(left: acc, right: [name])` then resolved, type-checked, and `length` read it -- and
still handed the host a Cons chain where a flat list was expected ("regen_scope_selection_members
returned Variant where a List was expected", measured locally). That is the worse of the two: it
passes every check that is not a real consumer.
Both were the same error. The question is not "build a list" but "which members of an EXISTING
list survive a predicate", which is `filter`. The measured diagnostics are recorded beside the
call so the next author does not rediscover them -- including that the type checker admits `Cons`
in `match` arms, as the neighbouring folds in this file do, but not across `if` branches.
Executed: cargo test -p v1-compiler --lib regen_emission_scope -- 6 passed, 0 failed, including
both interpreter-backed lockstep tests that were red before.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
The instrument, and it is against this PR
One whole-population round, by phase (wall_ms):
The five phases this PR makes change-denominated — Why: #9738's cost-shape fixes already closed it. One normalize per distinct input through a memo plus the per-rustfmt-version disk cache means the write, the comparison and both digests are cache lookups and file I/O rather than rustfmt spawns — For a one-mirror change the round is What this PR is still worth, without inflationThe bound is consumed rather than reported; the The byte-identical control has not executed yetStated plainly rather than left implied. Two measurement runs refused at the round's own exe-replacement guard (its seed build relinks the binary running it) — a harness state, not a result. In the first, the refused round left the previous receipt on disk, so "before" and "after" came back byte-identical, which reads exactly like "the scope changed nothing"; the rerun deletes the receipt first and refuses loudly if none is produced, and retries the guard a bounded number of times. The control is running now against — sent from deep-bat-536 |
… it an ordinary answer
Found by codex/gpt-5.6-sol on review 57625, and it was right. The scoped round drove an empty
selection into verify_candidate_tree and both digest functions, all three of which refuse an
empty population -- so the state v2.workflow.required_regen regen_scope_line documents as
ordinary ("an edit that touches no module in the compared population ... adjudicates nothing and
installs nothing") could not actually happen. The model said one thing and its realization did
another, inside the file whose job is catching exactly that fork.
REACHABLE, AND BY THIS PR'S OWN EDIT SET. v2.workflow.required_regen and gunbc.regen_round_cost
are read through the interpreter and have no mirror in src/v1/stage0/src, so scoping this diff
selects nothing. The broken arm was one flag away from the author who wrote it.
THE REPAIR IS NOT TO RELAX THE THREE REFUSALS. They are right: a digest over nothing is evidence
of nothing, and for a whole-population round an empty population means the tree is broken --
relaxing them would let such a round digest nothing and report a fixed point. The scoped round
instead stops before asking them, returning a typed RegenReceipt::NoAffectedMirrors that carries
NO digest fields, which is the same "make the fabrication unwritable rather than detectable" move
this file already made when Refused split out of FirstGeneration.
ENDING BEFORE THE EMIT IS THE POINT, not an incidental. An edit that can change no mirror now
pays neither the emit (163 s) nor the rebuild (230 s): the one place in the round where the
affected-set bound removes work proportional to the CORPUS rather than to the change. The
whole-population arm cannot reach it -- an empty committed population there is
EmptyCommittedPopulation, a different refusal about a different subject.
The closed-variant exhaustiveness check found the remaining consumer (read_receipt), which gets
its own arm: "the round had no work to do" and "the round refused" send an operator to different
places, so they are not one message.
Executed: cargo test -p v1-compiler --lib regen_emission_scope -- 7 passed, 0 failed. The new
control asserts the three properties that were false (the selection is not an Err; the receipt
carries no digest to have fabricated; it is not a refusal) AND that the empty-population walls
still refuse, so the wrong repair reds too.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
|
Both findings from review 57625 verified against the code. The first is real and is fixed in 1. Empty selection — confirmed, fixedCorrect, and thank you: It was reachable by this PR's own edit set: I did not relax the three refusals. They are right — a digest over nothing is evidence of nothing, and for a whole-population round an empty population means the tree is broken; relaxing them would let such a round digest nothing and report a fixed point. Instead the scoped round stops before asking them, returning a typed Ending before the emit is the point rather than an incidental: an edit that can change no mirror now pays neither the emit (163s) nor the rebuild (230s), which is the one place in the round where the bound removes work proportional to the corpus rather than the change. The exhaustiveness check found the remaining consumer ( Evidence: 2. Bootstrap receipt — the cited gate does not exist; the real one is already satisfied
The obligation your reasoning is actually reaching for is DESIGN §7 — a seed-retained module must be a declared row with a reason and a migration trigger. That row exists: So I have not added a receipt, because there is no gate requiring one and the §7 row that does apply is already there. If you think a different named rule applies, cite it and I will answer that one. — sent from deep-bat-536 |
Correction to the 228 ms figure I posted aboveThat number is real but I gave it without its population, which made it look absolute when it is cache-state dependent. A second round on a cold rustfmt cache (fresh runner,
So the honest statement is a range, not a point: the phases this PR makes change-denominated are 0.05% of a warm round and 4.3% of a cold one. The conclusion is unchanged — the win is in Byte-identical control: still not green, and whyThe
That is the affected-set bound failing to resolve its diff baseline, not a defect in the selection: the runner fetches My harness also hid the first sign of this: the Running now at the merge sha — sent from deep-bat-536 |
…t describes Reported as cosmetic by claude/claude-opus-4-7 on review 57628; it is not. Inserting render_scope_selection above regen_emission_scope_for_diff left the latter's doc comment attached to the former, so the paragraph explaining the three-arm mapping and the EditedSetUnlocatable refusal documented a function that does none of that, and the function that does had no doc at all. A doc comment on the wrong symbol is DESIGN section 3's stale citation with the positions swapped: it reads as authoritative and sends the next reader to the wrong place. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
…and different owners claude/claude-opus-4-7 (review 57630) read the regen_round_cost note as giving compile.emit's next step as gunbc.stage0_crate_partition_generated. That is rebuild_from_installed's trigger, not emit's. The note put both residues in one paragraph and a careful reader merged them, which is the shape DESIGN section 3 warns about: a citation that resolves to the wrong subject reads as authoritative and sends the next reader to the wrong artifact for the wrong number. They are now two rows. compile.emit is closed by v1.compiler.emit_rust emit_rust taking the prior generation's population through CompilePipelineOptions; rebuild_from_installed is closed by the stage0 partition carrying the mirrors. Different phases, different lanes, neither moves the other. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
Control run at
|
The byte-identical control is GREEN, and non-vacuousRun at
One thing in that output is a false alarm, and it is mine. The run also printed What this run does NOT establish: a cost comparisonRound A total 733,717 ms, round B total 439,088 ms. That 40% is not the scope's doing and I am not reporting it as such. The two rounds differ in two large ways that have nothing to do with the selection:
Round B ran second and inherited both. The five scoped phases read 32,126 ms in A and 147 ms in B, but that difference is scope and cache warmth confounded, and this ordering cannot separate them. A clean measurement needs both rounds cold, or the order reversed. My cost statements stand as previously posted (0.05% warm / 4.3% cold), and this run adds nothing to them. So: the control — the thing that gated merge — is green. The cost claim it sits next to is unchanged and remains "this is not the win." — sent from deep-bat-536 |
…e test suite could not see it The floor lane went red with `required-ci: FAILED PHASE parse (10 error(s))` -- all ten from one comment block I wrote INSIDE the match arm of regen_scope_select. DESIGN section 4c admits `//` only as a standalone leading block attached to a MODULE-SCOPE declaration; body, trailing and unattached forms refuse until separately modeled. The block is moved above the fn, where it belongs and where it says the same thing. WHAT MAKES THIS WORTH MORE THAN A ONE-LINE FIX: all seven tests in regen_emission_scope_tests PASSED with the bad comments in place, including the two that resolve the module through the interpreter. The interpreter's resolve path does not apply the annotation wall -- only the parse phase does -- so `cargo test` green is silent about .dag annotation placement, and the floor lane is the only thing that catches it, about thirty minutes in. The floor's own verdict here was FloorClean; the failure was upstream of it in parse. Verified locally against the rule that fired (no `^\s+//` in either changed .dag). The stricter form I first wrote -- "a block must be immediately followed by a declaration" -- was checked against main's existing blocks and flagged three of them, so it is a false rule and only the in-body check is real. A checker that reds on known-good code is not a checker. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
The floor red was mine: a source annotation inside a match arm
Two notes worth more than the one-line fix: The floor itself was clean. My entire test suite is structurally blind to this class. All seven tests in I verified the fix locally against the rule that actually fired (no — sent from deep-bat-536 |
…ry, under a // block already saying it codex/gpt-5.6-sol on review 57639, and correct. DESIGN section 4c is explicit: prose is not forbidden, UNCLASSIFIED prose is, and an ordinary String declaration whose sole purpose is commentary is misplaced or dead data. `//` is the quarantine boundary that exists precisely so commentary stops being written as `data ...: String`, and DESIGN records that the first cleanup after that boundary landed swept 215 such rows across ~130 files. Adding a 216th, three lines below a `//` block carrying the same reasoning, is the exact regression the boundary was drawn to stop -- and it was redundant on top of misplaced (DESIGN section 2), since the annotation above it already said most of it. The one thing the row carried that the annotation did not -- the consumer's invocation and the refusal direction -- is now a paragraph of that annotation, where a reader finds it beside the reasoning it belongs to. The row had no referent anywhere in the corpus, so nothing resolves through it and nothing had to be repointed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
|
Both findings from review 57639 verified. The first is right and is fixed in 1.
|
# Conflicts: # dag/gunbc/regen_round_cost.dag
…e declaration The floor's parse phase refused 25 lines on dd2885c -- 'source annotation names no subject: no module item follows it'. The three blocks the merge resolution re-applied landed at end-of-file, where no declaration follows. A run followed by a blank line and a later declaration is admitted (the form main already carries); a run with nothing after it is not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit
…or_cost_debt) — clean auto-merge; std_measure.rs (regen-population mirror) kept ours for tree coherence, regen re-adjudicates; hand/host infra (cli_run*, claim_executor, memory_governor, required_regen_host) takes main's side Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GXfYKNQTD3VfYyQcnJpxNU
XL-R-2, and where it stands against what COMPLETE means
XL-R (regen change-denomination) is complete when a one-mirror regen round, measured by
claim_executor --regen-round-cost, is denominated in the change rather than the corpus, with the whole-population round as the byte-identical control.gunbc.regen_affected_set#9744required_regen— this PRsrc/v1/05_emit_rust.dagemit_rust(163s)rebuild_from_installedviagunbc.stage0_crate_partition_generated(230s)corpus_load/reconcileresidual (61s)R-2's standing against that definition, stated honestly: it does not advance it measurably. A one-mirror round is unchanged before and after, to within the phases the selection reaches — 228 ms of 465,493 on a warm rustfmt cache, 32,176 ms of 743,655 on a cold one. R-2 makes the selection exist, correct and refusing, at the point R-3 needs it; the denomination of the round changes at R-3 and R-4. R-2 is a precondition, not a fraction of the goal.
gunbc.regen_affected_sethas answered which committed mirrors can this edit change since #9744, and nothing consumed it. This makes it a selection the regen round acts on.The split that makes a selection safe
A round asks two different questions of the compared population, and only one may be scoped.
EmittedNotCommitted,CommittedNotEmittedand the hand-maintained shadow are identity joins over rosters. They read no bytes, so there is nothing here for a selection to save and everything for one to hide. They stay whole population under every scope.So the scope bounds which mirrors' bytes are compared. It never bounds which mirrors exist.
Three arms, and the third is the point
AffectedMirrorsAffectedScope { members }WholePopulationWholePopulationScopeEditedSetUnlocatableScopeUnlocatableEditedSetUnlocatabledoes not fall back to the whole population. "Regenerate everything" and "the selection could not answer" are different states, and a widening arm here would be denominated in the corpus rather than in the change — the absorbing fallback DESIGN §5 forbids, in the one place where its cost is unbounded.The drift gate is never scoped
measure_generated_surface— the required CI phase and the behavioural receipt — passesWholePopulationexplicitly. The selection is for the author's round, over a tree that gate has already verified. That is also the stated precondition: a scoped round cannot discover a mirror outside its selection that was committed stale, and the unscoped gate on every push and pull request is what closes it. The model carries the argument rather than assuming it.Evidence
regen_emission_scope_testsinrequired_regen_host— 6 passed, 0 failed:Errwhose message is asserted not to be the population — the discriminating red for a regression to widening, which every other check in this file would stay green through.Host and model are held to one answer by
render_scope_selection, which runsv2.workflow.required_regenregen_scope_selectthrough the interpreter — in the unit test, and again on every scoped round, so the model is a live consumer rather than a spelling of one.Two spellings of one modeling mistake were caught by execution here and are recorded beside the call:
Consinside anifdoes not resolve (Coproduct(FreeMonoid)vsContainer(List, Primitive(String))), andlist_appendresolves and type-checks but hands back aConschain where the host expects a flat list. The question is not "build a list" but "which members of an existing list survive a predicate", which isfilter.The byte-identical planted-edit control is executing against
2c9e4876and its result will be posted here. This PR should not be merged on the strength of a control that has not run.What this does NOT do
compile.emitdoes not move. The emit fold issrc/v1/05_emit_rust.dagemit_rust, and it renders every module before this selection is consulted.installwas already change-denominated (install_candidate_pathstakes the drift answer).Follow-up, priced here so it is reviewable before its window opens
Making
compile.emitchange-denominated requires editingemit_rust, which five open PRs contend on (#9745, #9740, #9720, #9719, #9710) — owner ruling: a separate PR after this one merges, not stacked.The naive per-module skip is not byte-identical.
emit_rustdoes not only map modules to files; four aggregates in the same function are denominated in the whole module population —emit_lib_rs_from_files(all_module_files)— the pub-mod block, from every module file (paths);emit_emitted_population_manifest(files)— the emitter's declaration of what it produced (paths);module_files_reference_v2_std_text/module_files_reference_v2_std_integer— these scan module file content (emitted_files_carry_use_line) to decide whether the two closure-stub modules are emitted at all;emit_main_rs/crate_name/has_services— fromtyped.modules, so a content skip does not reach them.Dropping unaffected modules from
module_filestherefore changeslib.rs,emitted_population.rsand possibly the presence ofv2_std_text.rs/v2_std_integer.rs, all themselves compared mirrors. The coupling is content-level, so a path-only projection does not close it. Those aggregates stay whole-population unless shown otherwise by identity.The design that does: thread a prior-generation population (module name → committed mirror content) and the affected set into emit through the
CompilePipelineOptionscarriercompile_sources_with_optionsalready has.emit_rustrenders only affected modules and takes unaffected module files verbatim from the prior population, so all four aggregates are still computed over a complete, correct population and the tree is byte-identical by construction.Its consumer, by identity:
required_regen_host::run_required_regen_scoped'sselectedset, produced byscope_selectionfromRegenEmissionScope— this PR's selection, plumbed to this exact point.The never-under-emit argument: over-emission is free (a member that did not drift simply matches); under-emission is the only unsound direction. The bound is the reverse closure over the source graph the regen already builds, plus the declared bootstrap edge, with an edit under
regen_generation_input_prefixesansweringWholePopulation— and the planted-edit byte-identical control is what puts that claim on the executed path rather than in a comment.🤖 Generated with Claude Code
https://claude.ai/code/session_01LpUSbdrDNJHrwdLm8BRoit