Repository navigation
Affected set of one edit: gunbc.regen_affected_set bounds the mirrors a .dag edit can change (reverse closure + declared v1_rt.rs bootstrap edge + generation-input roster), refusing when the edited set is unlocatable - #9744
Merged
Merged
Conversation
…irrors a .dag edit can change -- reverse closure over the regen's own edge index, a declared bootstrap edge for v1_rt.rs, a declared generation-input roster, and a refusal (never a widen) for an unlocatable edited path Realizes regen_round_cost's DerivableNow disposition as an authority a regen can consume. `claim_executor --regen-affected-set` reads the floor's diff range, names each edited .dag as a module, and prints the model's bound; the host's native reverse walk is held to the model's answer on every run. The three measured edits of 2026-08-30 are the live-tree controls. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KGCnzm2zkb37mVHgrGCt9L
… 57579 on #9738) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KGCnzm2zkb37mVHgrGCt9L
Contributor
Author
|
Live receipt of the entry point on this branch (producer Read: the three — sent from smart-boar-394 |
gunbai-bot Bot
added a commit
that referenced
this pull request
Aug 30, 2026
… only the mirrors one edit can change, and refuses when the bound cannot locate the edit (#9757) * Consume the affected-set bound in regen: a round adjudicates, writes 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 * Name the phases the scope actually touches on the round-cost instrument'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 * A selection is a filter: regen_scope_select built its answer by monoid 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 * An empty affected selection was a hard refusal, where the model calls 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 * Restore regen_emission_scope_for_diff's doc comment to the function it 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 * Name the two round residues separately: they have different triggers 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 * A source annotation inside a match arm: ten parse errors, and my whole 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 * Delete regen_round_scope_consumer_note: a String row of pure commentary, 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 * Annotations must name a subject: move the three scope blocks above the 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 --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Step 3 of the regen-round-cost lane (after #9735, #9738): the affected-set bound scoped as
DerivableNowingunbc.regen_round_costbecomes an authority a regen can consume, built as ruled (operator ruling 2026-08-30): the runtime shim is a declared bootstrap edge, never a filename exception, and an edited population the tree cannot name refuses rather than widening to the whole population.The authority —
gunbc.regen_affected_setregen_affected_set(edited, unlocatable, edges, compared, modules) -> AffectedSetBound, three arms:AffectedMirrors { edited, mirrors, bootstrap_products }— the reverse closure of the edited modules over the regen's own closure edges (cli_run both_closure_edge_index: dotted references incl. every import, plus bare references), joined to the committed mirror population, plus the products of any declared bootstrap edge whose source is in the closure. A structural over-approximation computed AS the answer (DESIGN §5), never exact.WholePopulation { edited, generation_inputs }— an edit under a declared generation-input prefix (regen_generation_input_prefixes = ["v1.compiler.", "extdeps.languages."]): the emitter itself changed, so every emitted byte's producer changed and no reverse closure sees it. A declared bootstrap source is excluded from this arm by the declaration's own content (its measured effect is closure + product).EditedSetUnlocatable { unlocatable, reason }— the refusal arm, taken before any closure: a departed.dag, an unreadable one, or one with nomoduleline. Zero members; it does not fall back toWholePopulation— "whole rebuild required" and "the selection could not answer" are different states (§5, absorbing fallback).regen_bootstrap_edgesdeclaresv1.compiler.runtime_rust -> v1_rt.rswith its measured reason (tree 0fe2c51 drift:{v1_compiler_runtime_rust.rs, v1_rt.rs}, only the first in the graph).regen_reverse_closureis a bounded fold (n steps over n modules) so termination is by construction.The host —
claim_executor --regen-affected-setrequired_regen_host::run_regen_affected_set: edited population from the floor's own diff range (floor_git_diff_range, so the selection and the gate read one edit), module names viaextract_module_path_public, edges module→module offboth_closure_edge_indexoverregen_source_roots()(an endpoint the index cannot map to a module is a refusal, not a dropped edge), compared rows = module index ⋈committed_generated_basenames. The host's native reverse walk hands the model the reached subgraph; the model re-derives the closure and answers; lockstep every run — if the model's mirrors differ from the host walk's, the run refuses rather than electing a side. Output: provenance line,edited/unlocatablerows, the bound line, onememberline per mirror. Exit 1 on the refusal arm.regen_round_cost.regen_affected_set_disposition.fromnow names this authority.Evidence (by execution)
dag/test/claim/self_host_regen_affected_set_witness_test.dag— 7 fns, alltrueon srv1 with the builttarget/release/gunbc(--source-root dag --source-root src/v2): transitive-only reverse closure; leaf edit bound; RED no-dependents bounds to itself; runtime-template edit carries the declared product; emitter edit → WholePopulation; RED unlocatable refuses with zero members; bound line byte-exact.required_regen_host::regen_affected_set_tests— 4/4 remotely (BuildBuddy,cargo test -p v1-compiler --lib regen_affected_set_tests, 218s): host walk and model fold agree on the witness's fixture graph; unlocatable refuses and selects nothing; diff reader classifies named / departed / never-written /.rs; live-tree controls on one index build — the three measured edits of 2026-08-30:std.content_hash→AffectedMirrors∋std_content_hash.rs, ∌v1_rt.rs, proper subset;v1.compiler.runtime_rust→ ∋v1_compiler_runtime_rust.rsandv1_rt.rs;v1.compiler.emit_rust→WholePopulation.cargo check -p v1-compiler --all-targets: my code compiles; the one error (declaration_index_integrityimporting privatecompile_dag_multi_module_fixture) and the clippydisallowed_macrosincssl_assemble.rsare onorigin/mainuntouched by this diff.Not in this PR
Consuming the bound to restrict the emit (a per-module emit option in
05_emit_rust—emit_rustiterates everytyped.modulesmodule today) is the D3 that the cost receipt did not justify (emit ≈ 20% of a real round; the whole-crate rebuild is the larger cost until the stage0 partition carries the mirrors).🤖 Generated with Claude Code
https://claude.ai/code/session_01KGCnzm2zkb37mVHgrGCt9L