Repository navigation
FLOOR-ROUTE-GAP-SELF-HOST: publish the executing route family that discharges the self-host behavioral witnesses from route_gap_held (49 required / 112 full) - #10077
Merged
gunbai-bot[bot] merged 5 commits intoSep 2, 2026
Conversation
…d by identity
The wave-admission phase refused both attempts with 57 unadjudicated deltas -- every one
a TargetChanged binding reading base {v2.workflow.required_floor} -> head
{v2.workflow.floor_terminal_ledger}, verified as the only shape in the report. That is
this PR's own move, and the roster's documented closure is to author a row per delta.
Enumerated, not patterned: 57 deltas, 57 rows, each naming its module, declaration and
spelling. The rows go stale the moment this merges and MUST be deleted in the first PR
after it lands -- a stale row refuses every unrelated PR in the repository.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…9-safety-vocabulary-move # Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
Main's seventeenth dissolution swept this roster to empty. My conflict resolution kept main's receipt prose but re-opened the const with the whole of my side's row list, which still carried the four dissolved rows -- so it reinstated a permission nobody re-authored and the wave phase reported them CONSUMED and refused. That is precisely the failure a conflict invites: a resolution in my favour restoring what the other side deliberately removed. The 57 rows themselves adjudicated correctly in that same run: 0 unadjudicated deltas. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
gunbai-bot
Bot
deleted the
session/snappy-koi-879-safety-vocabulary-move
branch
September 2, 2026 18:55
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 2, 2026
The trigger read '#10077 MERGING ... once that PR is in main'. That was accurate when authored and became ambiguous the moment #10077 landed (a4a6db1, 18:55:08Z): a future-tense trigger gives a later reader no way to tell whether it has fired, and the next toucher pays for the ambiguity rather than its author. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 3, 2026
…red and this change is the roster-touch that owes it #10077 merged as a4a6db1, so main carries the relocation and no run after it can produce those deltas. Run 33694346070 (on the merge commit 2b3b841) reported all 57 CONSUMED while still ADMITTING, because that commit does not touch this roster; the SJT-1 cohort's refusal states the charging rule exactly -- consumed rows are "due for deletion on this roster-touching change". Re-tensing the trigger touched the roster, so the obligation landed on the change that went looking for it. The roster returns to empty, which is not permissive: a real delta still refuses as UNADJUDICATED. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
briansrls
pushed a commit
that referenced
this pull request
Sep 3, 2026
…corpus cadence
Clause 2 of the conjunctive trigger, under the wording the issuing authority
amended it to: "the determinism invariant consumes the canonical
call-reachability authority transitively, under a consumer whose declared
substrate and cadence truthfully match the inputs it reads, whose failure
reaches the required PR floor, and which cannot predict-skip that
enforcement." The artifact reading -- a consumer inside 00_compile.dag -- was
REJECTED, and this change deliberately does not touch that file.
WHY THE PRODUCER IS PURE AND THE LIVE READ IS ELSEWHERE. determinism_compile_gate
folds only the InferredTree it is handed, so a call to a declared function whose
body reaches an order-leaking primitive is invisible to it. Closing that needs
the call graph, which is a fact about the CORPUS. But v2.compiler.compile imports
v2.lens.determinism, so a live producer reachable from there would put a
live-read carrier in every compile-importing closure -- the measured harm that
de-enrolled lens_module_gate (31 SubstrateInputsOnly stamps in the lying-stamp
census). Calling a corpus read "determinism" would not have made it tree-grain.
So the facts arrive as parameters, and the live read plus the ReadsLiveTree stamp
live in the enforcement witness.
The venue was verified by receipt, not by the precedent's claim:
v2.test.claim.enforcement.lens_module_gate_witness appears in the judged-module
identities of required run 33700978133.
EVIDENCE (claim_batch, unpiped, exit 0, 4/4 PASS):
determinism_transitive_live_closure_holds 369ms live, whole corpus
transitive_leak_in_reached_declaration_is_found 39ms leak 2 hops out -> FOUND
identical_leak_outside_the_call_graph_is_not_found 3ms same leak, unreachable -> not found
deterministic_callee_in_the_same_shape_is_clean 3ms sorted_map_keys twin -> clean
The second and third rows are the pair that proves the reachability authority
does work here: a consumer that folded every declaration instead of the reachable
ones would pass the first and FAIL the second.
A NEAR-MISS RECORDED IN THE FIXTURE RATHER THAN SILENTLY FIXED. The first version
buried the callee atom inside the call node. call_reachable_decls reads callees at
DEPTH ONE -- the marshal hoists callee atoms onto the body root -- so nothing was
reachable and both discrimination rows agreed for that single wrong cause:
leak-is-found went red, leak-outside went green over an empty walk. Written the
other way round it would have shipped two green rows proving nothing.
TWO COST FINDINGS, ONE FIXED AND ONE REFUSED, both measured by isolating probe
rather than read off the source:
module_names_live built a ~4500-name list with list_snoc_item, which is
list_append(xs, Cons{item, Empty}) and so walks the accumulator every element.
33,443ms -> 32ms by prepend-then-reverse. That one helper was 97% of the
witness; acquiring the entire declaration population is 203ms and the walk
itself roughly 120ms.
The precise dependency-closure scope was built and measured at 193,269ms
against the whole-corpus 358ms, versus a 500ms budget. Refused on cost: a
permanently budget-refused witness enforces nothing while redding the floor.
The whole-corpus scope is a structural over-approximation computed AS the
answer, which DESIGN section 5 explicitly distinguishes from the absorbing
fallback; its residue is a loud false positive, never a false negative.
ALSO IN THIS COMMIT, the namespace-wave adjudication clause 1 and 3 required.
17 exact TransitionAdmission rows, one per TargetChanged delta from run
33700978133, enumerated by identity with no predicate. And the 57 consumed
#10077 rows are DELETED: wave_admission_refusal computes consumed_due =
roster_touched && !consumed_admissions.is_empty(), so authoring an admission
touches the roster and cannot land while they stand. Their own entry assigned
that sweep to "whoever next touches this roster".
RESIDUAL RISK, STATED RATHER THAN DISCOVERED LATER: 369ms against a 500ms
per-claim CPU limit is 1.4x headroom, and the floor's own 2026-09-01 rung drop
rules that attempt CPU carries an execution-position-sensitive component with no
established bound. Two witnesses in this same run died at 502ms and 515ms.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 3, 2026
… local route migrated onto it (7 refusals in, 7 typed causes out) (#9975) * Wet-evidence convergence: count the union of both refusal vocabularies before extracting The anti-collapse count the convergence receipt requires, taken BEFORE any extraction so the post-extraction cause count has something to be measured against. 18 distinct causes deduplicated by remedy, with the three binding mismatches kept apart as 7a/7b/7c. It found the collapse in the opposite place from the one assumed: seven of the eighteen remedies are typed causes in local_repo_wet_terminal and detail-string payloads in floor_wet_route, and five more exist only in the Rust reader with no .dag spelling. The extraction therefore widens the transported route to main's grain and must not narrow main's seven causes to meet it. It also records that the terminal vocabulary is neither module's to mint: floor_terminal_ledger already owns the terminal, observation, expectation and thirteen dispositions, is imported by the conflicted consumer, and already derives PassedOverBudget/KnownRedNowPassing by expectation -- the same rule both wet modules re-derived independently. Three arrivals at one distinction is the proven coincidence DESIGN asks for before unifying vocabulary. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * One wet-admission interface over the ledger's terminal vocabulary, with a typed binding The shared interface both wet routes will consume, and the reason it mints no terminal type of its own. WHAT IT IS NOT. It does not introduce a third terminal vocabulary. Two parallel ones is the fork being closed, so a third would be the same failure wearing a new name. v2.workflow.floor_terminal_ledger already owns the raw attempt terminal, the observed-verdict versus unreadable-observation split, the expectation, and thirteen derived dispositions -- and floor_changed_witness, the fold both routes feed, already imports it. This module imports that vocabulary and asks claim_disposition whether a terminal meets its expectation rather than deriving it again. That reuse is grounded in a PROVEN COINCIDENCE, not in taste: four independent arrivals at one distinction. The ledger derives PassedOverBudget and KnownRedNowPassing from a completed-past-limit terminal by expectation; the floor's seed keeps completed_over_cost_requirement apart from interrupted_before_verdict; local_repo_wet_terminal un-collapsed LocalRepoWetCompletedOverBudget out of its nonterminal arm; and floor_wet_route separated cost debt from no-verdict the same week. None of the three read the others, and none imported the fourth. THE LOAD-BEARING PIECE IS THE BINDING. local_repo_wet_terminal compared a candidate: String with ==, which DID decide admission -- so it was a validity key, not provenance -- but a bare String cannot say WHICH relation produced it. The binding is now two arms, deliberately asymmetric: a co-resident execution binds to the prepared subject and nothing else (executor identity and freshness are meaningless for a run inside the floor), while a transported receipt binds to the semantic subject AND the executor contract, because a receipt produced by a different executor over the same tree is a different evidential fact. The executor contract is a required field, not an optional one: an absent one has no constructor and cannot be defaulted permissively. Twelve typed causes, none collapsed. The three binding mismatches stay three, and evidence of the WRONG KIND is its own cause rather than a digest that happens to differ -- the case a String comparison could only ever report as "not equal". EVIDENCE. Eight witnesses green by execution, each RED paired with a control differing by exactly the fact under test. Then a mutation to prove they discriminate rather than merely pass: short-circuiting wet_binding_causes to return no causes turns exactly the three binding witnesses RED and leaves the other three GREEN. Predicted before the run, three red three green observed. A suite that went fully red would be entangled; one that stayed green would be inert. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Fuse route and dry source: the invalid pairings lose their constructor A live defect in 3270fea, found in review and confirmed by count: `dry_source` occurred EXACTLY ONCE in wet_evidence.dag -- its own field declaration. Nothing read it, and wet_evidence_validate did not consume it. Two consequences, both of which DESIGN names: `route` and `dry_source` varied independently, so the type admitted two states with no referent -- a co-resident execution after a deliberate wet decline, and a transported receipt after an observed hermetic route gap. The dry-source distinction was therefore COMMENTARY the realization could contradict, which is validation standing where construction was available (section 5). And a data row whose only function is to say something is the misplaced prose section 4c forbids. The field asserted an antecedent no executing consumer read. THE REPAIR IS STRUCTURAL, NOT A CHECK. `WetRouteAntecedent` fuses the two facts into one coproduct -- LocalRepoAfterHermeticRouteGap | SelfHostAfterDirectWetDecline -- and the route becomes a total PROJECTION of it rather than a field beside it. The invalid combinations now have no constructor, so there is nothing left to validate: rung 4 rather than the rung 2 an exhaustive WetRouteDrySourceMismatch refusal would have bought, and it costs no witness because no invalid state survives to witness. ONE WITNESS IS ADDED, for the residue the type cannot close. A TERMINAL's route is an execution fact, not a schedule fact, so a terminal claiming a different route than its schedule derives must still refuse -- a cause that had no witness before this commit. Nine witnesses green by execution. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Close the second structural defect: the required binding was a parameter independent of the antecedent The first repair fused `route` and `dry_source` because they were adjacent IN THE TYPE. The third fact entered through a different door -- as an ARGUMENT -- and fusing a coproduct does not close a parameter. `wet_evidence_validate` took `required: WetEvidenceBinding` with nothing joining it to the schedule's antecedent, so this batch was constructible and ADMITTED: a schedule whose antecedent is `LocalRepoAfterHermeticRouteGap`, a required binding of `TransportedReceiptSubject`, and terminals carrying that same transported binding. Every pairwise check passed -- the terminal's route matched the schedule's antecedent, and the observed binding matched the required binding -- so a co-resident schedule was satisfied by transported evidence. The inverse was equally writable. `WetBindingRelationMismatch` never fired because it compares OBSERVED against REQUIRED, and those two agreed; what disagreed was ROUTE against REQUIRED RELATION, and they never met. The repair is structural rather than a fourth validator: `WetEvidenceRequirement` is one authority per batch, and route, antecedent and required binding are ALL derived from it totally. There is no longer a way to say "local schedule, transported requirement" because the requirement IS the route. `WetScheduledClaim` loses its `antecedent` field; the batch supplies it. `WetTerminalRow` KEEPS `route` as an independent execution observation. Deriving that one away would make the foreign-route refusal unauthorable -- a check whose RED cannot be written, which DESIGN section 4b calls a decoration rather than a weak wall. The schedule's route is derived; the observation's route is carried; the join between them stays load-bearing. Two consumer rules land in the module rather than only in review prose: validate one batch PER REQUIREMENT and never concatenate the routes, because the two require different binding relations and a merged call would have to weaken the requirement to admit both -- widening instead of refusing. And `WetEvidenceRefused` is not read wholesale as "receipt invalid": the verdict-not-expected arm means the evidence is VALID and the outcome is known, so a valid FAILING attempt stays publishable, or latest-attempt degrades into latest-SUCCESS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * WIP: migrate the local wet route onto the shared wet-evidence join and the ledger vocabulary Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * merge main + relocate the safety vocabulary onto the widened ledger * re-anchor two annotations the move falsifies, including the widening's own cycle argument * Migrate the local wet route's consumers onto the shared join, and tighten two witnesses that claimed more than they asserted Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Replace a vacuous roster witness with the one duplication that is actually authorable Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Record the migration step's boundary beside the extraction's, which no longer describes the head Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Hoist two annotation blocks to module-item grain and fix a fold_list call shape Both defects were authored today and both were found by execution rather than review: the DESIGN 4c annotation-placement rule refuses a // block inside a declaration body, and fold_list is declared (xs, empty, cons) rather than the (xs, init, step) I invented. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Arm A: port the seed's roster decoder to the migrated vocabulary, preserving every wall The seed's local_repo_wet_schedule reads the .dag roster through the interpreter and decodes it by type and field NAME, so the migration broke it in four places. CI caught this on both heads; no .dag witness could, because they construct fixtures directly. Walls preserved rather than ported: the identity/function agreement check is now a direct comparison of the two spellings the row carries rather than a suffix-strip, and the expectation arm still refuses everything but the one arm this lane realizes -- ClaimExpectation has two arms where its predecessor had one, and a wider type is not a wider capability. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Adjudicate the 57 namespace deltas this relocation creates, enumerated by identity The wave-admission phase refused both attempts with 57 unadjudicated deltas -- every one a TargetChanged binding reading base {v2.workflow.required_floor} -> head {v2.workflow.floor_terminal_ledger}, verified as the only shape in the report. That is this PR's own move, and the roster's documented closure is to author a row per delta. Enumerated, not patterned: 57 deltas, 57 rows, each naming its module, declaration and spelling. The rows go stale the moment this merges and MUST be deleted in the first PR after it lands -- a stale row refuses every unrelated PR in the repository. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Drop the four SJT-1 rows my merge resolution silently restored Main's seventeenth dissolution swept this roster to empty. My conflict resolution kept main's receipt prose but re-opened the const with the whole of my side's row list, which still carried the four dissolved rows -- so it reinstated a permission nobody re-authored and the wave phase reported them CONSUMED and refused. That is precisely the failure a conflict invites: a resolution in my favour restoring what the other side deliberately removed. The 57 rows themselves adjudicated correctly in that same run: 0 unadjudicated deltas. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Re-tense the admission trigger now that its condition has fired The trigger read '#10077 MERGING ... once that PR is in main'. That was accurate when authored and became ambiguous the moment #10077 landed (a4a6db1, 18:55:08Z): a future-tense trigger gives a later reader no way to tell whether it has fired, and the next toucher pays for the ambiguity rather than its author. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 * Delete the 57 consumed safety-vocabulary admissions: their trigger fired and this change is the roster-touch that owes it #10077 merged as a4a6db1, so main carries the relocation and no run after it can produce those deltas. Run 33694346070 (on the merge commit 2b3b841) reported all 57 CONSUMED while still ADMITTING, because that commit does not touch this roster; the SJT-1 cohort's refusal states the charging rule exactly -- consumed rows are "due for deletion on this roster-touching change". Re-tensing the trigger touched the roster, so the obligation landed on the change that went looking for it. The roster returns to empty, which is not permissive: a real delta still refuses as UNADJUDICATED. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4 --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 3, 2026
One file changed on both sides: src/v1/stage0/src/namespace_wave_admission.rs. That collision is guaranteed rather than unlucky -- every relocation PR touches the admission roster by construction, so two relocation lanes in flight always meet here. RESOLVED ONTO MAIN'S VERSION, KEEPING ONLY MY OWN CONTRIBUTION. Main's #9975 had already deleted the 57 consumed `ledger safety vocabulary relocation gunbc#10077` rows and recorded the EIGHTEENTH DISSOLUTION, on better reasoning than the version this branch carried: it re-tensed the rows' own trigger, which touched the roster, so the obligation landed on the change that went looking for it. My branch's prose claimed that deletion as its own. Keeping it would have been a false statement about another lane's work, so it is dropped entirely and main's account stands. What re-applies here is only the 17 TransitionAdmission rows for this PR's relocation, plus their entry. THE ORDINAL WAS CHECKED, NOT INCREMENTED. This branch had written FIFTH TRANSITION; main already has a FIFTH (gunbc#9675, 2026-08-29). The ledger's transition ordinals already collide -- FOURTH and FIFTH each name two transitions, the second FOURTH being #10077 reusing it deliberately as a back-reference. FIFTEENTH is the highest in use, so this entry is SIXTEENTH, and says why it took the next UNUSED ordinal rather than the next in sequence: a third duplicate would make the entry uncitable by its own name. Verified: no conflict markers, 17 rows, cargo check -p v1-compiler --lib clean, and none of this branch's ten .dag files were touched by the merge. witness_layer_roots is unchanged at ["dag", "src/v2"], so the new enforcement witness's import still resolves. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 3, 2026
… duplicate walks deleted (#10156) * Ground call reachability once in v2.std.fn_index, deleting both walks Two lenses each carried their own copy of the call-reachability walk over fn-arrow declarations. Diffed rather than eyeballed: the walk bodies in v2.lens.effect_reach and v2.lens.live_read_classification were IDENTICAL text. The fork was one parameter deferred, and it sat in the callee reader, not the walk -- effect_reach terminated on effect_reach_host_sink_callee_symbols_v0, live_read on live_read_carrier_callee_symbols_v0. That parameter is now explicit. call_reachable_decls takes terminal_callee_symbols: List<String>, and both lenses pass their own roster UNCHANGED. One shape, two bound rosters: the rosters are data about their own subjects and stay with the lenses that own them. The cut goes to the root of the duplication rather than to the two named symbols. Also grounded and deleted from the copies: decls_in_module, decls_in_modules, decl_module_prefix, decl_belongs_to_module, decls_matching_callee, decl_in_list, fn_arrow_decl_eq, tail_decls, is_path_like_lexeme and atom_identities_in_node -- the last of which had a THIRD copy in v2.lens.production_qualification_origin_probe, and decl_belongs_to_module a FOURTH in v2.lens.affected_set.entry_selection. A surviving copy is the SS3 attractor: it keeps answering nearby questions in its own vocabulary. call_reachable_decls_from_root moves beside the file-grain entry point with its root-grain reasoning. A second grain is a second question, not a duplicate. Two homonyms renamed rather than left to collide corpus-wide, since one name now has one meaning: v2.lens.no_dual_representation_test.scan decl_belongs_to_module (a different predicate over DualRepModuleRef) and v2.lens.production_qualification_origin_probe callees_from_node (a deeper whole-subtree walk with no terminal roster). SS3 citations that named the old home updated in v2.compiler.effect_demand and the effect_reach claim fixture. EVIDENCE, by execution rather than by typecheck: v1_src_dag_parse 4563 file(s) parse-clean claim_batch over both lens witnesses 26/26 PASS, claim_batch exit 0 (unpiped -- a piped run reports tail's status, not the batch's) DISCRIMINATING REDS, planted in the one authority and reverted: decls_matching_callee never matches -> 1 FAIL (callee-expansion arm) decl_belongs_to_module never prefixes -> 3 FAIL (seed/membership arm) COVERAGE FINDING, reported rather than repaired: every discriminating witness is in live_read_classification. None of effect_reach's 8 witnesses redden under either plant, which is consistent with that fixture's own stated design -- fixture_empty_decls is empty, so its specimens exercise the walk over nothing. The walk's enrolled evidence is therefore narrower than the witness count suggests. Not repaired here: this cut preserves behaviour exactly, and new evidence machinery is out of scope. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE * Determinism consumes the reachability authority transitively, on the corpus cadence Clause 2 of the conjunctive trigger, under the wording the issuing authority amended it to: "the determinism invariant consumes the canonical call-reachability authority transitively, under a consumer whose declared substrate and cadence truthfully match the inputs it reads, whose failure reaches the required PR floor, and which cannot predict-skip that enforcement." The artifact reading -- a consumer inside 00_compile.dag -- was REJECTED, and this change deliberately does not touch that file. WHY THE PRODUCER IS PURE AND THE LIVE READ IS ELSEWHERE. determinism_compile_gate folds only the InferredTree it is handed, so a call to a declared function whose body reaches an order-leaking primitive is invisible to it. Closing that needs the call graph, which is a fact about the CORPUS. But v2.compiler.compile imports v2.lens.determinism, so a live producer reachable from there would put a live-read carrier in every compile-importing closure -- the measured harm that de-enrolled lens_module_gate (31 SubstrateInputsOnly stamps in the lying-stamp census). Calling a corpus read "determinism" would not have made it tree-grain. So the facts arrive as parameters, and the live read plus the ReadsLiveTree stamp live in the enforcement witness. The venue was verified by receipt, not by the precedent's claim: v2.test.claim.enforcement.lens_module_gate_witness appears in the judged-module identities of required run 33700978133. EVIDENCE (claim_batch, unpiped, exit 0, 4/4 PASS): determinism_transitive_live_closure_holds 369ms live, whole corpus transitive_leak_in_reached_declaration_is_found 39ms leak 2 hops out -> FOUND identical_leak_outside_the_call_graph_is_not_found 3ms same leak, unreachable -> not found deterministic_callee_in_the_same_shape_is_clean 3ms sorted_map_keys twin -> clean The second and third rows are the pair that proves the reachability authority does work here: a consumer that folded every declaration instead of the reachable ones would pass the first and FAIL the second. A NEAR-MISS RECORDED IN THE FIXTURE RATHER THAN SILENTLY FIXED. The first version buried the callee atom inside the call node. call_reachable_decls reads callees at DEPTH ONE -- the marshal hoists callee atoms onto the body root -- so nothing was reachable and both discrimination rows agreed for that single wrong cause: leak-is-found went red, leak-outside went green over an empty walk. Written the other way round it would have shipped two green rows proving nothing. TWO COST FINDINGS, ONE FIXED AND ONE REFUSED, both measured by isolating probe rather than read off the source: module_names_live built a ~4500-name list with list_snoc_item, which is list_append(xs, Cons{item, Empty}) and so walks the accumulator every element. 33,443ms -> 32ms by prepend-then-reverse. That one helper was 97% of the witness; acquiring the entire declaration population is 203ms and the walk itself roughly 120ms. The precise dependency-closure scope was built and measured at 193,269ms against the whole-corpus 358ms, versus a 500ms budget. Refused on cost: a permanently budget-refused witness enforces nothing while redding the floor. The whole-corpus scope is a structural over-approximation computed AS the answer, which DESIGN section 5 explicitly distinguishes from the absorbing fallback; its residue is a loud false positive, never a false negative. ALSO IN THIS COMMIT, the namespace-wave adjudication clause 1 and 3 required. 17 exact TransitionAdmission rows, one per TargetChanged delta from run 33700978133, enumerated by identity with no predicate. And the 57 consumed #10077 rows are DELETED: wave_admission_refusal computes consumed_due = roster_touched && !consumed_admissions.is_empty(), so authoring an admission touches the roster and cannot land while they stand. Their own entry assigned that sweep to "whoever next touches this roster". RESIDUAL RISK, STATED RATHER THAN DISCOVERED LATER: 369ms against a 500ms per-claim CPU limit is 1.4x headroom, and the floor's own 2026-09-01 rung drop rules that attempt CPU carries an execution-position-sensitive component with no established bound. Two witnesses in this same run died at 502ms and 515ms. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE * Delete the three consumed gunbc#10011 admissions; renumber this transition The required run refused the namespace-wave-admission phase on 6df76f5: FAILED PHASE namespace-wave-admission (0 unadjudicated delta(s), 0 stale admission(s), 3 consumed admission(s) due for deletion on this roster-touching change) The floor in that same run was FloorClean with the live consumer withdrawn, so the phase failure was this and nothing else -- the withdrawal did what it was meant to do. The three rows are main's gunbc#10011 supersession-standing re-home admissions. When main authored them their transition had not merged and the block said so, verified; gunbc#10011 has since merged, so all three now report CONSUMED and the roster rule makes their deletion owed by the first roster-touching change to observe it -- this one. The resting state returns to empty. ORDINAL: this transition was authored as SIXTEENTH before the merge, and main's gunbc#10010 took SIXTEENTH in the meantime. Renumbered to SEVENTEENTH TRANSITION; the deletion above is the NINETEENTH DISSOLUTION. Also records that the deleted block's "five gunbc#10011 rows" was never a miscount -- five were authored, two were deleted as stale when review 59072 dissolved the predicate they adjudicated, and the block's own middle paragraph explains it. I reported that as a prose/roster mismatch after reading its first sentence and not the paragraph; the note is there so the next reader does not repeat it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE * Yield the dissolution record to #10106; renumber to EIGHTEENTH TRANSITION #10106 (head 29db34e, pushed before this branch's 889a5f5) already carries NINETEENTH DISSOLUTION for the SAME three gunbc#10011 rows, with the same trigger and the same quoted refusal, and SEVENTEENTH TRANSITION for its own change. Both of my ordinals collided with it. Both branches discovered the same three consumed admissions independently and both correctly concluded the deletion was owed by the first roster-touching change to observe it. The trigger obliges EVERY concurrent roster-touching branch, so concurrent discovery is the mechanism working. Two records of one event is not: it is a single-authority violation whichever ordinals they wear, and it would survive the git conflict rather than be caught by it. So this branch keeps the deletion its gate requires and authors NO dissolution record. #10106 pushed first and is mid-CI, so it carries the record. Its own SEVENTEENTH TRANSITION documents this same double-discharge one round earlier at 57 rows -- twice now, at 57 and at 3, which makes it a property of the carrier rather than an accident. This transition renumbered SEVENTEENTH -> EIGHTEENTH, free on both main and #10106 as of bfcfe04 / 29db34e. Third ordinal collision on this one file from this branch alone. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE * review 59343: remove a stale live-consumer claim and a prose String TWO OF THREE FINDINGS WERE CORRECT AND ARE FIXED HERE. 1. v2.lens.determinism claimed a required-floor live consumer supplies its facts -- "stamped ReadsLiveTree, whose failure reaches the required PR floor" -- and said that satisfied the amended clause 2. This same change WITHDREW that consumer, so the module described a guarantee its own sibling file says was removed. That is rung inflation in the §4b(1) sense and the reviewer was right that the two files contradicted each other. The annotation now states that no live consumer exists, that the trigger has therefore not fired, and where the obligation is carried. The retraction is recorded rather than silently swapped. 2. fn_index_root_grain_law was a module-scope `data ...: String` whose sole purpose was commentary, read by nothing -- what DESIGN §4c forbids outright. It reached this file by migration from v2.lens.live_read_classification g2_root_grain_law during this cut, so moving it made it mine to classify. It is now a `//` annotation on call_reachable_decls_from_root, the declaration it governs, and the earlier comment that named the symbol no longer names a deleted one. THE THIRD FINDING'S PREMISE IS WRONG and is answered on the PR rather than by a change: namespace_wave_admission.rs:1338 is a TransitionAdmission DATA ROW, not the start of hand-written compiler logic, and the hand-Rust receipt it says is missing already exists and is enrolled -- gunbc.namespace_wave_admission namespace_wave_admission_seed_growth_ justification, imported by gunbc.seed_growth_admission, enumerating TransitionAdmission and AdmissionSubject as admitted declarations. Fixture rows re-run and still discriminate: 3 PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE * Delete #10106's 47 consumed admissions (TWENTIETH DISSOLUTION) Required run 33772725454 on 646058e: floor CLEAN, phase refused. FAILED PHASE namespace-wave-admission (0 unadjudicated delta(s), 0 stale admission(s), 47 consumed admission(s) due for deletion on this roster-touching change) #10106 merged as 78e022c, so its 47 rung-drop-authority rows are consumed and the roster rule assigns their deletion to the first roster-touching change to observe it. Deleted, along with the now-unused RUNG_DROP_AUTHORITY_LABEL const. Resting state returns to this branch's own 17 rows. RECORDED THIS TIME, NOT YIELDED, and the asymmetry is deliberate. The gunbc#10011 deletion was yielded to #10106 because that branch was live and had authored the same NINETEENTH DISSOLUTION concurrently -- two records of one event merge silently and violate §3. #10106 has now merged, so nothing else will delete its consumed rows and no competing record exists; deleting without recording would leave 47 admissions vanishing from main unexplained. THIRD OCCURRENCE OF THE SAME EVENT, SECOND ON THIS BRANCH: 57 rows (main and a branch), 3 rows (this branch and #10106, both authoring the same ordinal), now 47. The trigger works correctly every time. What recurs is its cost: a branch touching this roster for its own reasons inherits the deletion of someone else's consumed rows and must author or yield a record for an event it did not cause. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CksG1GV7gm1uQh62UeV1jE --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <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.
What this is
ClaimSafetyOutcomeandClaimPreemptionReachabilitymove fromv2.workflow.required_floortov2.workflow.floor_terminal_ledger, beside theClaimAttemptTerminalarm that carries them.required_floorimports them back and remains a consumer.This is a pure relocation. No arm is added, renamed, reordered, or re-payloaded.
Why it is forced, not preferred
These are TERMINAL VOCABULARY — what a claim attempt reached — declared inside a CONSUMER. The
census says so without appeal to principle: outside
required_floorthe family is referenced 12times in the ledger, 12 in the wire, and 12 more across the two ledger test modules. The declaring
module was not where it was used.
That survived while only the floor and the ledger were involved. It became impossible the moment
a third module needed both. Migrating the local wet route onto the shared terminal vocabulary closes:
claim_batchrefuses at discovery with exactly that cycle. DESIGN §4 makes acyclicity the importgraph's only structural law, so the direction is decided for us.
The scope is seven symbols, and the closure is why
An earlier enumeration read the ledger's import block — which names four symbols — and concluded
those four were the dependency. An import list names what is referenced BY NAME; it cannot name
what is reached THROUGH an arm's payload.
CompletedPastSafetyLimitcarriespreemption: ClaimPreemptionReachability, declared in the same module. Moving only the four wouldhave left the relocated type referencing one that stayed behind, so the ledger would still import
required_floorand the edge would have changed which symbol it carried rather than disappearing.So the set was taken as a transitive closure — every named import, every payload type of every
arm, recursively — rather than as a patched list:
ClaimSafetyOutcome,ClaimPreemptionReachabilityCompletedWithinSafetyLimits,SafetyInterrupted,CompletedPastSafetyLimit,CooperativelyPollable,OpaqueHostCallUnboundedIntorString. No further hop.What stays behind, and why that is the same split the repo already made
The eight-member roster of opaque host operations that the preemption-1 rung drop is declared over
stays in
required_floor. That is policy declared OVER this vocabulary, not the vocabulary. It isthe same line
floor_route_gapalready draws between its ground type and its expectation roster —the repo has decided this shape once already.
Dragging the roster along would move a policy population into a vocabulary module and recreate the
wrong-direction dependency this change removes.
A §4b trigger was re-anchored and NOT retired
The ledger carried a next-rung trigger reading:
Every locating word in that sentence is deictic. Moving the declaration silently re-points all
three while the prose stays grammatical and readable. It does not become false — it becomes
ambiguous, which is why nothing would ever flag it. This is the positional-citation failure one
level up: not a line number that decays, but a relative reference that decays.
The trigger is restated with its location EXPLICIT, and carries a new sentence stating plainly that
this relocation does not satisfy it: the capability is the sub-family derivation, and this
change performed a move. The drop stays open at MITIGATABLE.
A relocation that appeared to retire a trigger it merely re-anchored would be a worse outcome than
the cycle this fixes — §4b(3) says a drop is retired by its trigger and by nothing else.
The stale ownership sentence is corrected rather than deleted, because it is load-bearing: it is
the reason a narrowed two-arm twin is refused, and a reader finding it naming the wrong authority
would conclude the refusal had lapsed.
Decision-equivalence
Named, not asserted: the check is
dag/test/claim/preemption_reachability_witness_test.dag, theheaviest external consumer of the moved vocabulary at 23 references, run alongside
floor_terminal_ledger_testandfloor_terminal_ledger_wire_test. Results are reported in thethread.
The fact this whole change turns on
After the move,
floor_terminal_ledgerimports exactly two workflow modules --floor2_prepared_subjectandfloor_route_gap(the latter arriving with #10057's widening) -- andboth of those import only
v2.std.*. That is the cycle OPENING rather than relocating.This is the check to apply if you review nothing else here. A relocation that merely moved which
symbol the edge carried would leave
floor_terminal_ledger -> required_floorintact under adifferent name, and the migration that surfaced the cycle would fail again for the same reason one
step later. It does not: the edge is gone, not renamed. The check was run to the
leaves rather than one hop: neither of the two surviving imports names any workflow module, so
nothing reintroduces
required_floortransitively.That distinction — edge disappears vs. edge changes symbol — is also why the scope had to be taken as
a transitive closure rather than as the four symbols the import block names. Moving only those four
would have produced exactly the relocation-not-opening outcome.
Decision-equivalence, discharged by an executing gate rather than by reading the diff
The required floor executed this tree. The
namespace-wave-admissionphase comparedbinding_rows_compared=684472and ruled on this relocation directly. Quoted verbatim from therequired-witnesses-floorjob of Actions run 33647114048:Both admitted. That is a machine stating, in its own vocabulary and at corpus scale, the two claims
this PR rests on: the edge is removed rather than re-pointed, and every relocated name still
denotes the same declaration. The hand check described above agrees with it — that check is how
I knew where to look, not what the claim rests on.
The witnesses themselves passed. The floor's partition closes exactly:
3487 = 3400 + 26 + 12, and both non-passing sets are enumerable by name: the twelve are allself_host_compile_phase_frontier_witness/self_host_compile_phase_live_gate_witness, and thetwenty-six known-red are
declared_type_expected_type_path_witness,namespace_reference_derived_closure_acceptance,dag_add_emit_round_tripandemit_ingest_python_same_language_round_trip. None is this PR's subject, sofloor_terminal_ledger_test,floor_terminal_ledger_wire_testand thepreemption_reachabilitywitnesses executed and passed. Elimination is sound here only because the residual is fully
enumerated, which is why it is enumerated rather than resting on
failed=0.The red on this PR, disclosed rather than buried
failed=0. The floor refused because twelve witnesses were undecided at the 500ms cpu deadline,which is correct fail-closed behaviour -- a run that did not finish looking has established nothing.
This is a declared standing rung drop, landed in #9932. It is cited here by PR number and by what it
CLAIMS rather than by its symbol name, because #10030 is renaming that row and striking its
cause-asserting sentences; the surviving proposition under either name is that an attempt's cpu
deadline does not qualify the claim as an intrinsic cost verdict -- it remains a required
attempt-safety and verdict-availability criterion. This PR neither discharges nor touches it. No
cause is asserted for the twelve here, because none has been established.
The margin is the argument, and it is stronger than "the class is pre-existing". The twelve
measured 501-506ms against a 500ms limit, with
completed_over_cost_requirement=0. A witness failingat 900ms would be consistent with the witness genuinely being expensive; a failure at 501 is not.
The same hairline was hit independently the same night by lanes that were not in contact -- rows at
exactly 500, at 502, and a separate PR refusing at 501 then 505 -- so this is a boundary shape
witnessed across lanes, not a property of this branch.
The reroll performed here is the bounded mitigation that row already admits -- at most one reroll per
head per signature, only where
failed=0and the refusal is carried entirely by its non-verdict andcost arms, both of which hold. It is not retry-until-green, and a green reroll is not evidence the
refused rows were wrong: it is an availability outcome on a population the row establishes is redrawn
per attempt.
On the count, stated so a reviewer cannot read the citation as explaining it: twelve is higher
than the single instance on the main-only run 33644089601 at 6764d17, which carries the same
signature with no branch of mine involved. That row's enumerated instances range over 0, 1, 2, 4, 5
and 15, so twelve sits inside the documented range. What is NOT claimed is that anything here
explains why this head drew twelve -- on a redrawn population there is no per-head explanation to
give, and this should not be read as though there were.
Both attempts refused — the complete pair, disclosed
The reroll has been used and it refused again. Actions run 33647114048, both attempts on head
74719e46ddb, re-derived per attempt withgh api repos/gunb-ai/gunbc/actions/jobs/<job>/logs --allow-escape-sequences:subject=dde5f846302033c6on both attempts, so the bytes are held fixed by construction rather thanby an argument that the diff could not matter. Attempt 2's partition closes the same way, and this
PR's witnesses are inside its 3409.
Attempt 2's single interrupted row is
self_host_compile_phase_frontier_witness.the_published_frontier_standing_does_not_claim_typeck_or_borrowck_passedat 503ms, and that identity was also among attempt 1's twelve — so this pair is a subset, not a
disjoint redraw, and it is not offered as evidence that membership changes between attempts. The two
completed_over_cost_requirementrows arecompiler_frontend_program_status_witnessidentities atcpu_ms 501 and exactly 500 with
outcome=pass, whose neighbours in the same module measured 481, 490and 499. That module sits on the line: which members cross is decided by a margin smaller than
the run-to-run variation.
The bounded reroll is one per head, and it has been spent. There is therefore no legitimate path to a
green required context on this head — no further reroll, and no bypass, since a required gate
bypassed because it is inconvenient to a bystander is an escape hatch whoever opens it.
failed=0onboth attempts and nothing in either non-passing set is this PR's subject. Whether to hold or to fund
the cost work is an operator decision, not this PR's to take.