Repository navigation
Delete the floor's stale live-tree decline - #9106
Merged
Merged
Conversation
Contributor
Author
|
Self-hosted measurement is complete in run 32721781133: required step 60m39s; floor about 50m13s; 11,690 planned/executed/terminal; 182 route gaps; 48 semantic failures; 49 interrupted before verdict. All identity artifacts uploaded. The PR remains draft pending the cost/landing decision. |
Contributor
Author
Triage: 48 semantic failures (run 32721781133)Categories: (i) real defect/drift the wall correctly exposed; (ii) probe authored incorrectly and never executed to reveal it; (iii) probe subject/expected population moved since authorship. This is triage only—no repairs are folded into this PR.
Provisional totals: 20 category (i), 8 category (ii), 20 category (iii). The classifications are routing reads, not repair verdicts; owners should confirm them against each carrier's intended subject before changing code. |
Contributor
Author
|
Correction to the provisional category totals in the preceding 48-row table: 21 category (i), 7 category (ii), 20 category (iii) = 48. The per-row classifications are unchanged. |
Contributor
Author
Triage: 88 unenrolled route gaps (run 32721781133)Every row is an actual operation reached at the hermetic boundary. None is an ordinary committed-source checkout read. The ground is copied from the typed refusal.
Operation totals: |
Contributor
Author
Mechanism summary: interruptions and expected-red runtime errorsNo per-identity repair work was performed.
|
added 2 commits
August 24, 2026 18:16
# Conflicts: # src/v2/workflow/floor_route_gap.dag
briansrls
pushed a commit
that referenced
this pull request
Aug 24, 2026
…FreezeIntersection line-stop (#9133) * Retire merged route gaps from deferral freeze Cherry-picked from royal-cat-509's d8363d1 (branch behind draft #9106). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Shrink-log row: attribute the collision to main standalone, and DELETED not MIGRATED Two corrections raised by eager-crane-282 and verified at origin/main 8ab8a8e: the contradiction is not a merge artifact (all four are in floor_route_gap_chunk_04 on main standalone), and nothing is rehomed, so the disposition matches the 2026-08-19 sweep's DELETED. Adds the join method and the 4/614 counts the precedent entry carries. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- 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> Co-authored-by: Brian Searls <briansearls1@gmail.com>
added 7 commits
August 24, 2026 21:16
# Conflicts: # dag/gunbc/witness_deferral_freeze.dag
added 2 commits
August 25, 2026 15:10
# Conflicts: # dag/gunbc/witness_deferral_freeze.dag
# Conflicts: # src/v2/test/claim/complexity/accumulator_copy_roster_gate_test.dag # src/v2/workflow/floor_expected_red.dag
This was referenced Aug 28, 2026
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 28, 2026
…ty strings cannot distinguish
All 47 stay enrolled. What changes is what the header claims about them.
THE OVERCLAIM. The chunk said every row "EXECUTES, REACHES ITS SUBJECT AND ANSWERS
FALSE". The run establishes the first and third and not the second: Bool has no
spelling for "I could not observe my subject", so an unreached subject and a
genuine NO both render as returned Bool(false). That is this document's own
execution-provenance-loss class, and the clause is removed rather than softened
because a reader quoting it would be quoting a property nothing measured.
THE THREE GROUPS. A row here is a bare identity string with no reason field, so
enrolment says exactly one thing about 47 rows failing for at least six causes
with different remedies. Named in the header as follow-ups, verified against the
cited files rather than accepted on report:
1. The three guarantee_floor_class_probe_witness generic-instantiation rows fail
because a WALL LANDED, not because the hole is open. Discriminating evidence:
both of that hole's controls PASS and the sibling field_through_generics hole
probe also passes, so the harness reached the judgment and the other hole is
genuinely still open -- a harness seeing nothing would have taken the sibling
down too. That module's own scope note prescribes the remedy verbatim: rewrite
as ExpectBlockingRefusal rather than delete the probe, which is DESIGN 4b(4).
2. The four sole_constructor f10 rows answered an open question the first time
they ran. Their annotation states a question, not a marked red, and the answer
is yes: _ab fails while _ba passes on identical source with imports swapped,
and the two direct probes fail in opposite directions -- last-import-wins. The
distinction is decidable in the file: f13 and f19, enrolled here on the same
footing, carry an explicit "Deliberately RED" marking and the f10 four do not.
3. The three cost_coverage_witness rows are the subject-reachability candidate.
That module's 7 passing fns are the ones that survive an empty subject; the 3
failing ones demand non-zero content. Consistent with a genuine NO and equally
consistent with a subject never reached. Enrolled as failing, which is what was
observed; not asserted to be semantic.
WHY FOLLOW-UPS AND NOT A SPLIT. Enrolment is a reversible holding state with a loud
exit: the floor refuses on an enrolled row that starts passing and names it, which
is the same path by which this change removes one. So none of the three can be left
quietly at rest. Against that, holding rows back keeps the floor red, and the
compute fabric is fail-closed on the floor -- gunbc.fleet_desired_admission refuses
to advance the desired ref until the floor concludes Success on some revision.
A STALE PREMISE FOUND WHILE CHECKING THE ABOVE.
gunbc.declined_live_tree_defect_classification states it "must never become" an
expected-red enrolment "because the floor does not run it at all". Eight of the
modules it classifies contain rows enrolled here, and the floor DOES now run them --
they are in run 33145062452's FAIL lines. The clause is not wrong about authority
substitution in general; its REASON has been overtaken by #9106. Not edited here,
because it is that carrier's to correct and a second account of one fact is the
defect either way.
The triage behind groups 1-3 is crisp-newt-899's, checked here against the files.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J
This was referenced Aug 28, 2026
Merged
Merged
Merged
Merged
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
… cost axis declared rather than absorbed (#9591) * Complete #9106's enrolment on the verdict axis: 47 in, 1 out, and the cost axis declared rather than absorbed #9106 deleted the floor's stale live-tree decline -- a file-grain prediction that a live-tree reader could not join the hermetic fold, which had stopped agreeing with what the interpreter does. Deleting it was correct and it admitted a population that had never executed. Main has been red on four causes since. Measured on run 33145062452 (3a8344b): failed=47 interrupted_before_verdict=44 completed_over_cost_requirement=2 stale_quarantine=1. TWO OF THE FOUR CLOSE HERE, and both are the existing mechanism's own paths rather than new machinery. chunk_24 enrols the 47. Every one EXECUTES, REACHES ITS SUBJECT AND ANSWERS FALSE -- the run classifies each as `returned Bool(false)`, which is the semantic verdict this roster is defined over. None overlaps `floor_route_gap` (checked at identity grain: zero), none is already enrolled (zero), none is a budget outcome. THE TREE ALREADY DEMANDED THIS, which is what makes enrolment the intended completion rather than a convenient one. `quarantine_probe_disposition_witness_test` `the_former_live_tree_declined_row_is_now_expected_red` asserts that `legacy_test_behavior_unclassified_frontier_is_zero` is held by this roster. It was authored against the post-#9106 world and has failed every run since, because the row it names was never added -- and that witness is itself one of the 47. Four rows are therefore expected to leave chunk_24 on the first run after it lands, by the roster's own removal path rather than by an edit. The stale-quarantine row comes out: `duplicate_definition_in_one_module_is_refused` is enrolled and PASSING, and the run named it and asked. Repayment and deletion are one act. THE OTHER TWO ARE DECLARED, NOT ABSORBED, and the diff deliberately does not touch them. An interrupted row produced NO VERDICT; enrolling it would assert "this runs and fails and someone is fixing it" about an identity that never answered -- the exact 101-row mistake this file's header opens with, and `ExpectedRedArm` refuses budget outcomes by construction so it would not take. The 2 completed-over-cost rows answered, but what they owe is a cost and not a failure. Cost is not a verdict. The population is bounded and measured at identity grain: 44 interrupted, all CPU-clock against 5000ms, concentrated in live-tree corpus witnesses (13 grammar_coverage_witness, 6 enforcement_live_witness, 6 accumulator_copy_roster_gate, rest across 10 modules); 2 completed-over-cost, both transport_script_wall_compile_red, wall clock at 18882ms and 19024ms against 10000ms. Every interrupted figure is a LOWER BOUND, so their real cost is unmeasured. WHERE THEY GO IS NOT A NEW MECHANISM. `required_floor` names the remedies exhaustively -- reduce what the witness reaches for, or a lane declaring its own dated ceiling -- and rules relocation out. A carrier for exactly this axis is already built and open as gunbc#9517 (`v2.workflow.floor_cost_debt` + a `DeclinedCostDebt` arm), and its roster returns `Empty`: the machinery landed without its population. These 46 are that population. Authoring them into a module that is not on main would fork the authority, so they are handed to that lane at identity grain instead of duplicated here. RUNG (DESIGN 4b(3)): the cost axis stays below the floor's bar -- the run still stops, so nothing is silently admitted, but 46 identities reach no usable verdict every run and no mechanism on main holds them. RESTORATION TRIGGER: #9517's roster carries these 46 under its O=R admission -- and NOT when #9517 merely merges, because #9517 as it stands closes zero of them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Verify the empty-roster claim on witty-wren-148's branch rather than relaying it The chunk_24 declaration asserted that #9517's floor_cost_debt roster returns Empty on the authority of a relayed reading. That reading was correct, and a correct relayed claim is still a claim this file cannot check. Read directly: floor_cost_debt_chunks() on origin/session/witty-wren-148 is Empty {} and the file authors no qualified-name literal, so floor_cost_debt_holds answers false for every name and nothing is ever DeclinedCostDebt. The consequence is what the restoration trigger already turns on and is now stated where a reader meets it: #9517 merging closes none of these 46. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Correct a cross-branch claim that went false within the hour, and un-number the chunk TWO FIXES, both about the same failure mode arriving on different clocks. THE STALE ASSERTION. The previous commit recorded, as a first-hand reading, that #9517's floor_cost_debt roster returns Empty. The reading was honest and it was wrong within the hour -- that branch was moving while I read it, and its roster now carries a population including these 46. A bare present-tense claim about ANOTHER LANE'S HEAD has no producer on this side of the boundary that could re-derive it, so nothing here refuses when it goes false. The sentence is deleted rather than re-pinned to a newer number, because a second number rots the same way. What survives is only what this module can stand behind: these 46 are absent from this roster, deliberately, and why. The restoration trigger is restated to name the CAPABILITY (DESIGN 4b(3), 2026-08-26): a roster ON MAIN carrying the 46 under O=R admission. Explicitly not "#9517 merges", since a merge of an empty roster closes none of them, and explicitly not "that lane enrols them", because an enrolment on an unmerged branch changes nothing about what the required run on main observes. Both of those would fire while main stayed red on 46 rows. THE CHUNK IS NO LONGER NUMBERED. Three open branches each mint floor_expected_red_chunk_24 into this file: this one, #9587 (one add-slice row) and #9569 (six sole_constructor rows, which are also six of the 47 here). The numeric suffix is a shared mutable counter every concurrent lane computes independently from the same base, so collision is the expected outcome, not a risk. And it is worse than an ordinary conflict. Two lanes appending a same-named fn at different offsets can merge with NO conflict markers, leaving one file with two definitions of one name, and this repository has measured what happens then: test.claim.duplicate_definition_binding_probe exists because a duplicate definition is silently accepted and the later binding wins. The merge would not fail; it would quietly drop one lane's rows and stay green. A position-derived name is a second naming scheme for something the declaration already names (DESIGN section 3), and this is that rule's cost arriving in the merge graph. A meaning-carrying name cannot be independently derived by two lanes, so the collision becomes unrepresentable instead of detected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Drop an overclaim, and name the three groups the roster's bare identity strings cannot distinguish All 47 stay enrolled. What changes is what the header claims about them. THE OVERCLAIM. The chunk said every row "EXECUTES, REACHES ITS SUBJECT AND ANSWERS FALSE". The run establishes the first and third and not the second: Bool has no spelling for "I could not observe my subject", so an unreached subject and a genuine NO both render as returned Bool(false). That is this document's own execution-provenance-loss class, and the clause is removed rather than softened because a reader quoting it would be quoting a property nothing measured. THE THREE GROUPS. A row here is a bare identity string with no reason field, so enrolment says exactly one thing about 47 rows failing for at least six causes with different remedies. Named in the header as follow-ups, verified against the cited files rather than accepted on report: 1. The three guarantee_floor_class_probe_witness generic-instantiation rows fail because a WALL LANDED, not because the hole is open. Discriminating evidence: both of that hole's controls PASS and the sibling field_through_generics hole probe also passes, so the harness reached the judgment and the other hole is genuinely still open -- a harness seeing nothing would have taken the sibling down too. That module's own scope note prescribes the remedy verbatim: rewrite as ExpectBlockingRefusal rather than delete the probe, which is DESIGN 4b(4). 2. The four sole_constructor f10 rows answered an open question the first time they ran. Their annotation states a question, not a marked red, and the answer is yes: _ab fails while _ba passes on identical source with imports swapped, and the two direct probes fail in opposite directions -- last-import-wins. The distinction is decidable in the file: f13 and f19, enrolled here on the same footing, carry an explicit "Deliberately RED" marking and the f10 four do not. 3. The three cost_coverage_witness rows are the subject-reachability candidate. That module's 7 passing fns are the ones that survive an empty subject; the 3 failing ones demand non-zero content. Consistent with a genuine NO and equally consistent with a subject never reached. Enrolled as failing, which is what was observed; not asserted to be semantic. WHY FOLLOW-UPS AND NOT A SPLIT. Enrolment is a reversible holding state with a loud exit: the floor refuses on an enrolled row that starts passing and names it, which is the same path by which this change removes one. So none of the three can be left quietly at rest. Against that, holding rows back keeps the floor red, and the compute fabric is fail-closed on the floor -- gunbc.fleet_desired_admission refuses to advance the desired ref until the floor concludes Success on some revision. A STALE PREMISE FOUND WHILE CHECKING THE ABOVE. gunbc.declined_live_tree_defect_classification states it "must never become" an expected-red enrolment "because the floor does not run it at all". Eight of the modules it classifies contain rows enrolled here, and the floor DOES now run them -- they are in run 33145062452's FAIL lines. The clause is not wrong about authority substitution in general; its REASON has been overtaken by #9106. Not edited here, because it is that carrier's to correct and a second account of one fact is the defect either way. The triage behind groups 1-3 is crisp-newt-899's, checked here against the files. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * The run adjudicated the prediction: 47 becomes 44, and the count was wrong by one in an instructive way Run 33154432928 on a474f45: failed=0 stale_quarantine=3. WHAT WAS PREDICTED, registered in the PR body before the run: enrolling legacy_test_behavior_unclassified_frontier_is_zero satisfies the assertion the three quarantine_probe_disposition_witness_test claims make ABOUT this roster, so they stop failing and report STALE-QUARANTINE. The floor named exactly those three. They are removed here by the roster's own removal path. THE PREDICTION SAID FOUR. The fourth name was legacy_test_behavior_unclassified_frontier_is_zero itself, and it did not flip -- correctly. It is the row the join is ABOUT, not a row that passes as a consequence: it still fails on its own subject and this roster still holds it. I conflated "the identity a witness names" with "an identity that changes state when the witness is satisfied", and a join has both roles in it at once. That is recorded in the header rather than quietly corrected, because the error is the more instructive half of the result. WHY THE ENROLMENT WAS STILL RIGHT FOR ALL THREE, and this is what keeps the removal from reading as a mistake being fixed: they failed on main and answered false, so they met this roster's admission when they were added. What removed them is that the same change repaired their subject. A roster that could not hold a row for one run and release it on the next would force an author to predict the repair perfectly before landing it -- and the loud STALE-QUARANTINE exit is exactly the mechanism that makes holding safe. FLOOR STATE AFTER THIS: failed=0, stale_quarantine=0 expected. The verdict axis closes. The 44 interrupted and 2 completed-over-cost remain and are the declared cost axis, owned by #9517; required_floor_outcome_is_clean makes interrupted_before_verdict.is_empty() a conjunct at claim_executor.rs:1766, so main stays red until that lane lands. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 28, 2026
… keep only what it added #9591 enrolled all 47 identities from #9106's un-declined live-tree population, including this branch's single row, in `floor_expected_red_chunk_live_tree_admission`. Landing this branch's own chunk on top would put one identity in the roster twice -- two rows to remove when it starts passing, and a stale-quarantine arm that only half fires. Per the sequencing agreed with warm-tern-34, whichever lands second drops its chunk rather than landing the identity twice. So the conflict resolves to main's side EXACTLY: the roster in this branch is now byte-identical to main's, and the chunk function and its aggregator edge are gone. WHAT SURVIVES is the part the bulk enrolment does not carry: the per-row mechanism, re-homed as an annotation on the chunk that now owns the row. The bulk header establishes THAT the row fails; this establishes WHY, and for this row the why is load-bearing -- infer accepts and the composition refuses because the fixture root is a connective outside the four kinds v2 derives, and the sibling witnesses pass on the same fixture only by hand-authoring the `DerivedGrounding` that is exactly the `root == root` grounding the frontier carrier replaced. Without that written down, the cheap green looks like a fix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
…9584) * Eight extdeps modules carried no mandatory external-authority anchor `v2.lens.mandatory_tag.corpus_scan_witness_test:corpus_live_clean_tree_wall_holds` began executing on main when #9106 deleted the floor's stale live-tree decline, and it found the live extdeps corpus dirty: eight modules landed after the witness stopped running and none of them carries the mandatory `extdeps_external_authority_anchor`. Seven had no anchor declaration at all and now carry an inline `ExternalAuthority { uri: Uri { scheme: Https, locator: ... } }` literal naming the upstream document each module actually reads — git's `for-each-ref` and `worktree` documentation for the two wire decoders, phosphor-pid-control's README for the three OpenBMC fan-program modules, and RFC 8259 sections 4 and 6 for the JSON member partition and the number decode. The literal form is used rather than a reference to a same-file declaration, which the host scanner reads as ABSENT. The eighth, `extdeps.standards.rfc_8118`, already carried the literal under a second name (`rfc_8118_external_authority_anchor`). That is one fact under a name the wall cannot see, so the declaration is RENAMED rather than duplicated, and its four references — two citation witnesses and the `std.citation` scaffold binding's `decl_name` — move with it. `member_conservation`'s note claimed it carried no citation of its own; it now says which upstream fact the anchor rests on (an object is a sequence of members) and keeps the distinction the old sentence was drawing — the reading discipline is ours, the thing it partitions is RFC 8259's. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * A same-file anchor alias read as ABSENT, not as an unresolved alias The eight anchors above left `extdeps.cpu_attachment.lotes_azifa072` still violating: it DOES declare the mandatory anchor, as a reference to `azifa072_drawing_authority` declared four lines above it in the same file and imported from nowhere. The host projection behind `extdeps_external_authority_live_clean_tree_holds()` followed an alias only through the module's IMPORTS, and answered `Absent` when the symbol named none — so the wall reported `missing:extdeps.cpu_attachment.lotes_azifa072` for a module that is not missing anything. That is a state-space conflation with opposite remedies on its two sides: "this module declares no anchor" is an authoring defect, "this module declares one I did not follow" is a defect in the reader. Reshaping the corpus to satisfy the reader would have been the workaround; the alias's remaining home is the module itself, so the projection now resolves it there, with a per-(module, symbol) cycle key so a self-referential alias refuses rather than recursing. Two tests hold the change from both directions: the local-alias case projects present/Https/`www.lotes.cc/en/contact.php` (it read absent before), and the missing-anchor fixture still projects absent — local resolution widened what resolves without fabricating presence. Measured on this tree: all six projection tests pass, including `corpus_live_clean_tree_wall_holds_...`, which failed before this commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Bind the conventional anchor name instead of renaming it into an ambiguity The first commit renamed `rfc_8118_external_authority_anchor` to the conventional `extdeps_external_authority_anchor` on the reasoning that one fact must not carry two names. CI's namespace-wave-admission phase refused it with a `NewAmbiguity`: `test.claim.citation_cit1_consumer_witness` cites TWO modules' authorities, and after the rename the name `extdeps_external_authority_anchor` resolved to both `extdeps.runtime.abi.sysv_amd64` and `extdeps.standards.rfc_8118` in one module. That is the silent last-import-wins hazard, and it is exactly why the document-specific name existed. So the two names are not a nickname — they answer different questions. The conventional name is what the mandatory-tag corpus wall reads, and it is per module, so it collides the moment one reader cites two authorities; the document-specific name is what a consumer imports, and it is unique tree-wide. The corpus already settles this: `extdeps.cpu_attachment.ilm4926` and `lotes_azifa072` bind the conventional name to the specific one rather than forking the locator. The four renamed files are restored to main's bytes and `rfc_8118` gains that binding. It resolves only because of the projection fix in the previous commit — before it, a same-file alias read as ABSENT, which is what made the rename look like the only option in the first place. Measured on this tree: all six projection tests pass, including `corpus_live_clean_tree_wall_holds_...`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Consume the authorities that already existed instead of re-minting them Review 57231 (codex/gpt-5.6-sol) found five of the seven new anchors re-mint a locator this tree already declares, and it is right on both counts. extdeps.git already declares `git_for_each_ref_external_authority_anchor` and `git_worktree_external_authority_anchor` beside the operations whose wire the two decoders read, with byte-identical locators. A decoder is not a second publisher of git's documentation, so both now import the named declaration and bind the conventional name to it. Neither creates a cycle: nothing under extdeps.git imports either decoder. extdeps.bmc.pid_control_program already declares the phosphor-pid-control README authority, so decode, semantic_identity and representability now consume it. That needs an importable name — the conventional one is per module and cannot be imported into a module that must also declare it — so the program module names its literal `phosphor_pid_control_external_authority_anchor` and binds the conventional name to that, exactly the split the rfc_8118 ambiguity forced. Two defects surfaced doing this, both caught by running the wall's oracle rather than by reading the diff: - `data X: T =` followed by its value on the NEXT line is not accepted by the grammar. Five modules were unparseable and the module index refused them all — a failure that looks nothing like an anchor problem from the outside. - the module is `extdeps.git`, not `extdeps.git.git`: the module path is the folder, and the index panicked naming the path it could not find. Measured on this tree: all six projection tests pass, including `corpus_live_clean_tree_wall_holds_...`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Aug 28, 2026
* Six unresolvable names in the v2 root's emitted Rust: qualify the cross-module calls and use the declared list_length (#9547)
The v2 compiler root emits cleanly -- 0 blocking, 2083 advisory, 175 files --
and the emitted crate does not compile. Measured on 00b242b81a1 with
`gunbc compile --entry src/v2/compiler/00_compile.dag --target rust`, then
cargo over the emitted tree with its own emitted Cargo.toml: 20 rustc errors.
Six of them are source defects in this repository's own .dag, not emitter
defects and not self-host work, and this commit is those six.
THREE ARE NAMES USED WITH NEITHER AN IMPORT NOR A QUALIFICATION.
`decl_facts` is declared in v2.std.decl_index and used bare in two modules;
`PartialFunction` is declared in std.algebra and used bare in a type position.
The interpreter resolves them, so nothing refused; the emitter reports them as
`unlisted import use` advisories and emits the bare name, which is E0425. The
repair follows the idiom already on one of the two lines -- grammar_coverage.dag
declares no imports at all and qualifies every other cross-module reference
inline -- so these are qualified rather than imported. inferred_tree.dag already
carries five imports, so PartialFunction is added to that list.
THREE ARE A FREE-FUNCTION SPELLING OF A METHOD. `length(xs:)` has no declaration
anywhere in .dag; `length` is a MethodDeclaration in dag/std/methods.dag that the
interpreter intercepts. The corpus spells this `.length(` at 804 sites and
`list_length(` at 306; only reference_deps used the free form. Repointed at
std.types.list_length, whose declared parameter is `items`, not `xs`.
MEASURED, EACH ROUND A FULL RE-EMIT AND A FULL CARGO BUILD OF THE EMITTED TREE:
20 -> 17 after the three qualifications, 17 -> 14 after the three list_length
sites. Exactly the fixed errors disappeared both times and NOTHING WAS UNMASKED
behind them. That is worth stating because it is the outcome the masking
argument says not to assume: rustc stops after name resolution, so every count
here is a lower bound on a fully-resolving crate, and 20 -> 17 -> 14 establishes
only that no masking occurred AT THIS LAYER, never that none exists.
WHAT IS DELIBERATELY NOT IN THIS COMMIT, because none of it is a source defect:
five host builtins with no .dag body (layer_import_facts and the four
*_resolution_facts), four errors from Filesystem.Read emitting `.await?` against
an unbound handle in a sync fn, three emitter type-argument defects, one
unclassified E0391 variance cycle, and two deliberate compile_error!
sentinels that 05_emit_rust.dag emits instead of fabricating a default.
No Rust touched. No roster edited. No policy changed.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares (#9560)
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into `compile_dag_rust_emit_check` and not into its census
sibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a45e) the floor refuses
with `completed_over_cost_requirement=1` and `failed=0`:
`test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_
and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run
carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any
row of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both `green_named_authority_source` and
`green_own_declaration_source`, each of which a later claim then reads free.
Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and `run_claim_measured` performs the same split it already performs.
Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows
have never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Name the forcing class that decides warm-versus-net, and name the third state as the one that must not exist
The bracket in the previous commit fixes ONE instance. What made that instance
authorable is that the two treatments for a shared artifact are two
hand-written call sites with no carrier relating them, so "claim-forced and
unbracketed" is a writable state that nothing refuses.
THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED.
Preparation-forceable -- every identity it can be asked for is knowable before
the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index`
is this arm, and the run reports `provenance=built-by-preparation` for both
index identities the floor's resolves can reach. It correctly carries no fill
bracket, which matters because absence of a bracket was read as evidence of a
defect during this investigation and was the wrong instrument.
Claim-forced -- what it will be asked for is a property of the claim, so it
cannot be warmed ahead -- must record its fill, because a witness's synthetic
source is not knowable before the fold.
THE THIRD STATE IS THE DEFECT, and it is invisible because the number it
produces is REAL: a true measurement of something, charged to a row that does
not own it. Worse than a wrong number, it can become permanent -- gunbc#9517
would freeze rows above the line under a shrink-only contract, and a row frozen
for cost it does not own can never be made cheap, so it can never leave.
PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review
diligence; the third state stays writable and this paragraph will not stop the
next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing
class and the warm-or-net treatment is DERIVED from it, at which point the
third state has no spelling. That construction is not made here and is not
claimed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Two 04_infer rows carried counts that had rotted — name the instrument, and stop restating the superseded figures as history (#9462)
* 04_infer: the traversal-idiom count rotted to 16 while the tree carried 29 -- name the instrument
explicit_return_conformance_note argued that collect_explicit_return_values is not a new
shape but the seed's ordinary traversal idiom, and grounded that on a transcribed count:
"16 such sites on origin/main" across seven named modules.
Measured, both on origin/main and on this branch: 29 sites across EIGHT modules.
04_emit_info 1 · 04_sigs 1 · 04_infer 5 · 05_emit 3 · 05_emit_rust 8
compile 1 · complexity 6 · trait_derive_emit 4
trait_derive_emit was absent from the note's list entirely, so the clause was wrong about
the population's membership and not only its size.
NOTHING EDITED THE NOTE. The tree moved underneath it, which is precisely the decay mode
DESIGN §3 gives for a positional citation -- it rots without anyone touching either end --
and it is what the 2026-08-24 ruling forbids by name: cite the instrument, never transcribe
its output. The recipe is one grep and it is now stated instead of its result.
THE ARGUMENT NEVER NEEDED THE NUMBER, which is the part worth keeping. What makes this the
seed's idiom rather than a new shape is that EVERY such collector recurses itself, and that
holds at 16, at 29, and at whatever it measures next. A clause whose force depends on a
figure it cannot keep current was overstating its own evidence -- the number was doing
rhetorical work, not logical work.
Two derived ordinals went with it. "the 17th instance of a 16-instance idiom" and
"collect_explicit_return_values is the 17th ... the 18th" were positions in the disproven
count, so they were already false; they now read as further instances with no ordinal. An
ordinal is a transcribed measurement wearing the costume of a structural fact, and it is
worse than the raw count because it does not look like a measurement at all.
Prose-only, in one data row. No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Regenerate the stage0 mirrors, and delete the dead child_type_at accessor
REGEN. The prose change in 04_infer edits two `data ...: String` rows. Those are program
data, not annotations, so they emit into the stage0 Rust mirror, and CI's build lane
refused with:
required-regen: FAIL generated surface drift: v1_compiler_infer.rs
Regenerated through the sanctioned producer -- `claim_executor --required-regen
--source-root dag --source-root src/v2` -- rather than hand-edited. A hand-authored mirror
is exactly what that gate exists to refuse, and its only reachable green would have been
the forbidden action.
EVERY CHANGED LINE IS ACCOUNTED FOR, because a regen can also delete orphan content a
committed projection carries that no authority produces:
v1_compiler_infer.rs 2 lines the two data rows edited in the parent commit
v1_compiler_infer_types.rs 14 lines deleted: the child_type_at body
Nothing else moved. Re-running regen against the installed mirrors reports
first_generation_equal=true. (declared_divergent=1 [main.rs] is pre-existing; it is present
in the failing run on the parent commit too.)
DEAD ACCESSOR. v1.04_types child_type_at had ZERO callers -- measured across the whole
corpus, not just .dag: one definition in 04_types.dag, one in the generated mirror, no
consumers, no re-export, no prose reference.
It is deleted rather than left because of where it sits. It is a decoy beside
child_type_node, the live accessor that discriminates a type child from a field child by
whether `inferred` is populated -- a fabricated provenance stamp the parser writes at parse
time. Anyone repairing that discrimination reads both functions and has to work out which
one matters. Approved by compiler direction as needing no ruling.
WHY THIS WIDENS AN ALREADY-APPROVED PR, stated because the usual answer is that it should
not. #9462 was red and required a regen commit regardless, so the approval resets either
way and the deletion rides along at zero marginal cost -- and it keeps this to ONE regen
cycle rather than two. Without that, the correct call would have been a separate PR.
No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The sibling row carried the SAME disproven count -- one sentence fixed, the claim left standing
FOUND FROM OUTSIDE, NOT BY ME. The first commit repaired explicit_return_conformance_note and
left seed_node_traversal_frontier asserting the identical thing a few lines above it:
"the idiom is 16 self-recursive `children |> flat_map` sites on origin/main across
04_emit_info, 04_sigs, 04_infer, 05_emit, 05_emit_rust, compile and complexity"
Same 16, same seven-module list, same two errors -- the tree measures 29 across EIGHT, with
trait_derive_emit absent from the list entirely. I edited a SENTENCE when the defect was a
CLAIM, which is the document-wide-correction failure, committed inside the change whose whole
subject is a rotted figure.
THE SECOND COUNT IN THAT ROW GOES TOO, AND THE REASONING IS THE INTERESTING PART. It carried
"579 direct Node-storage field reads in 04_infer alone". A plausible reconstruction -- counting
`.children`, `.params`, `.inferred` and their siblings -- returns roughly TWICE that. That
establishes the number is STALE without establishing what the right one is, because I cannot
recover the recipe its author used.
So the repair is DELETION, not an update. Replacing a stale figure with one my own instrument
produced would swap an uncheckable number for a checkable-LOOKING wrong one, which is worse:
the first is visibly unverifiable, the second gets cited as verified. The site population is
named by its instrument (grep the idiom under src/v1); the field-read population has no agreed
instrument and is stated as a SHAPE rather than a count.
That asymmetry is why the earlier commit deliberately left this figure alone, and why leaving
it was still wrong -- declining to invent a recipe was right, declining to remove the number
was not.
Mirror regenerated through claim_executor --required-regen. One line in v1_compiler_infer.rs,
which is the row above. Prose only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The counts were deleted as CLAIMS and kept as HISTORY -- which is the same decay inside the sentence announcing its removal
Found in review, not by me, and it is the sharper half of this PR.
The previous commits removed the rotted figures from both 04_infer rows as ASSERTIONS and then
restated them as provenance: "it read 16 sites across seven modules while the tree measures 29
across eight". That is still a number in a live `data … : String` authority. It rots the same
way the original did, nothing re-derives it, and it gets quoted back as though this row had
measured it -- so the row announcing that it no longer transcribes an instrument's output was
transcribing one in the same breath.
BOTH ROWS NOW CARRY ZERO FIGURES, verified mechanically rather than by reading:
grep '^data explicit_return_conformance_note' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
grep '^data seed_node_traversal_frontier' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
The before-and-after lives in the PR, which is the artifact that is allowed to carry a
superseded measurement, because it is dated and nobody consumes it as current authority.
A SECOND, INDEPENDENT PREDICATE DEFECT, also named in review. Both rows pointed at a LEXICAL
instrument (grep `children |> flat_map`) while asserting SEMANTIC properties -- self-recursive,
and the seed's ONLY traversal idiom. A grep bounds the literal-occurrence population and cannot
establish recursion or exhaustiveness. Naming an instrument does not fix a claim if the
instrument answers a different question, which is the same right-number-wrong-subject failure the
counts themselves were. Both rows now say so: the grep bounds the literal population, and the
recursion property is read off the sites rather than off the count.
WHY DELETION AND NOT AN UPDATE, restated because it is the part a reader will want to argue with:
one row's field-read count has no reproducible recipe and a plausible reconstruction disagrees by
a wide margin. That establishes STALE without establishing CORRECT. Substituting a figure from my
own instrument would swap an uncheckable number for a checkable-LOOKING wrong one -- worse,
because the first is visibly unverifiable and the second gets cited as verified. That population
is stated as a shape.
Mirror regenerated through claim_executor --required-regen and applied from the candidate rather
than hand-edited; the diff is exactly the two rows, 4 lines, no other drift.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Restore the mirror the merge resolution dropped: --theirs took main's bytes, which never carried the prose fix
THE MERGE CONFLICT WAS IN A GENERATED FILE and I resolved it with --theirs to complete the merge,
intending to regenerate immediately. That resolution takes MAIN's mirror, which by construction
does not contain this branch's edits -- so for one commit the authority (04_infer.dag) carried the
repaired prose and its mirror carried main's older text. A regen fixed-point check is exactly what
catches that, and it did:
changed lines: 4, in the two rows this branch edits, nothing else
Mirror re-derived from the MERGED authority through claim_executor --required-regen and applied
from the candidate rather than hand-edited.
WHY THIS IS WORTH A COMMIT MESSAGE RATHER THAN A SILENT FIXUP: picking a side of a conflict in a
generated file is never a resolution, it is a coin flip between two stale artifacts. The authority
merged cleanly on its own -- the mirror had no business being adjudicated at all, and the only
correct answer was to recompute it. Taking --ours would have been equally wrong in the other
direction, dropping main's edits to the same file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* An escalation is not an infrastructure loss: give ExecutionAttemptLineage the arm the resident-model thesis is measured on (#9546)
A local model that reaches a terminal result it cannot carry, followed by a
more capable model taking the next try, is the single observation the
"progressively smaller models suffice" claim is denominated in. Measured on
this tree, nothing could express it: grep for Episode/continuation/retry_of/
predecessor across dag/gunbc, dag/std and src/v2 returns nothing episode-shaped,
and ExecutionAttemptLineage's three arms are InitialAttempt, InfrastructureRetry
and RequestedReexecution. So an escalation had to be recorded as either an
infrastructure retry -- which says the work told us nothing -- or as an
unrelated initial attempt, which discards the edge entirely.
CapabilityEscalation is a sibling of InfrastructureRetry rather than an arm of
one generic Retry, because the two differ in exactly what lineage exists to
record: an infrastructure loss says nothing about the work, while an escalation
says the work exceeded the capability that was tried. Like its sibling it names
the prior attempt AND the receipt that established the prior result, so merely
resolving a more expensive model after a cheaper one is a selection fact rather
than an escalation.
The two arms are deliberately the same SHAPE, which is what the third witness is
for: a control checking only the prior-attempt key would pass identically
against a lineage that had collapsed them, so the discriminating assertion
matches on the arm and fails if an escalation ever reads as a retry or the
reverse.
WHAT IS NOT VERIFIED, stated because a green I cannot stand behind is worse than
no green. `gunbc compile` takes no --entry, and the whole-corpus run over this
tree reports 31139 diagnostics ON PRISTINE MAIN, 1283 of them "expected item
declaration" on `//` annotation lines -- so that CLI path does not route source
annotations the way the required parse phase does, and cannot adjudicate this
tree. My attempted discriminating RED (deleting one arm from an exhaustive
match) returned 31139, byte-identical to the pristine baseline: it added zero
errors and therefore discriminated nothing. An earlier local run appeared clean
only because it was killed at its timeout mid-typecheck and the truncated output
rendered identically to a completed clean one. CI is the check here.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) (#9527)
* A typed wall for barren witness files exists, is wired to a hard failure, and the required floor never calls it: 62 unenrolled claims, the third scanner, and 37 promotions
The brief was 62 claims declared plain `fn` and never enrolled. Chasing why produced a
larger finding than the population: `v2.workflow.floor_naming_hygiene`
`floor_entry_is_barren_test_sidecar` has refused this exact class since it was written,
`floor_discovery_finalize` turns it into `FloorDiscoveryRefused`, and the host returns that
as `Err`. It stops the line. It has never been on the line.
MEASURED, not inferred: main run 33092582255 (headSha 107304a579), both lanes green, four
barren `*_test.dag` entries present at that sha, and zero occurrences of `barren` or
`sidecar` in the 693,975-byte run log.
WHY: `run_required_floor` builds its roster from `prepared.witness_files`, produced by
`witness_file_from_source`, which answers `None` for a file with no `test fn` — and the
caller discarded that answer. The walled `.dag` producer is reachable only through
`discover_floor_witness_roster`, which the required floor never calls. Three scanners for
one fact live in one binary and the wall guards the one production retired. The Rust test
asserting the wiring is not the missing piece: it still PASSES, because the wiring is
intact on the producer path — a green local `cargo test` says nothing about the required
path.
WHAT LANDED: preparation records the discarded fact; the floor asks
`floor_naming_hygiene`'s own `floor_test_sidecar_suffix` which recorded paths are
`*_test.dag` and refuses `cause=BarrenTestSidecar`. The rule keeps one home; only its
consumer moved. The recorded set uses the RULE's vocabulary — neither `test fn` nor
`test data` — so the 13 test-data-only files are not over-refused. The floor's summary line
is bounded above rather than left exact-and-silent. 37 leaf claims promoted, 37/37 PASS,
and the 4 sibling-conjunction aggregates deleted: each was a hand-rolled substitute for
enrolment with exactly one occurrence in the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
* Consume the modeled sidecar predicates instead of re-spelling them in Rust: delete the forked suffix test and the added test-decl scan
review 56971 requested changes on #9499 and was right on both counts; #9499 merged before
the rework landed, so main currently carries the fork and this is the repair.
FINDING 2, the reimplemented predicate. `floor_barren_test_sidecars` read
`floor_test_sidecar_suffix` from the `.dag` and then applied `strip_prefix("./")` and
`ends_with` in Rust. Reading the constant does not make the computation derived from the
authority — the two can drift independently. It now INVOKES the modeled predicates and
decides nothing itself. My own framing ("policy stays home, only the consumer moves") was
the error: I moved the CONSTANT home and left the COMPUTATION forked.
FINDING 1, the added test-declaration scan. The `!line.starts_with("test data ")` check is
DELETED. It existed to stop the wall over-refusing the 13 test-data-only files, which is
exactly what `floor_discovery_scan_test_decl_names` already does inside
`floor_entry_is_barren_test_sidecar`.
THE SHAPE, and why it costs one call rather than one per corpus file — which is what pushed
me into the fork to begin with. Preparation records a CANDIDATE SET, not a verdict: every
source `witness_file_from_source` declined, asking nothing about suffixes and nothing about
`test data`. `floor_entries_requiring_test_sidecar` (new, in `v2.workflow.floor_naming_hygiene`,
composing the existing `floor_entry_requires_test_sidecar`) is then asked ONCE for the whole
roster — a pure string question, one crossing — and `floor_entry_is_barren_test_sidecar` is
asked per survivor with that file's content, typically zero or a handful of invocations.
THE CANDIDATE SET IS DELIBERATELY OVER-INCLUSIVE AND THAT IS WHAT MAKES IT SOUND: a
test-data-only file lands in it and the `.dag` answers NOT barren, because its own scan counts
`test data` as a test decl. Rust can only widen the question, never decide it, so a
Rust/`.dag` disagreement cannot produce a wrong refusal — only a candidate the authority
discards. A missing candidate source is a typed refusal rather than a skip (§5).
RE-VERIFIED BY EXECUTION, because changing the mechanism invalidates the evidence for it.
Same binary, corpora identical except `filesystem_read_outcome_witness_test.dag`:
RED refuses `cause=BarrenTestSidecar count=1` naming it; GREEN completes site-projection
(sites=13351 files=1697 claims=11910). The first re-run attempt failed loudly with
`no declaration named 'v2.workflow.floor_naming_hygiene.floor_entries_requiring_test_sidecar'`
because the control trees came from HEAD while the new `.dag` function was still uncommitted
— a binary/corpus mismatch the control caught rather than one that shipped.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
---------
Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Delete the floor's stale live-tree decline (#9106)
* Delete the floor's stale live-tree decline
* Enroll surfaced required-floor dispositions
* Retire executing witnesses from deferral freeze
* Retire routed witnesses from deferral freeze
* Retire merged route gaps from deferral freeze
* Enroll post-merge shell route gaps
* Enroll activated semantic reds
* Place expected-red provenance at module grain
* Enroll newly exposed parser-drop route gap
* Adjudicate live-tree cut witness fallout
* Keep quarantine disposition annotation at module grain
* Fix expected-red chunk merge boundary
* Declare the live-tree census debt
* Retire five executing freeze rows
* Retire two supplied route gaps
* Bind exposed floor debt to repair lanes
* Retire stale live-tree decline prose
* Close route-gap lists after stale-row retirement
* Retire repaired expected-red rows
* Classify realization floor non-verdict
* Compose discovery census with live-tree cut
* Declare the exposed gitattributes drift
* Bind the accumulator analysis explicitly
* Preserve new diagnostic histogram arms
* Update floor projection annotation
* Close floor cut review obligations
* Remove stale retained-parameter annotation
* Correct live-tree cutover annotations
* Retire repaired live-tree census stalls
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences (#9447)
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences
The producer (#9439) correctly refused the binding envelope: its denominator is
the candidates that reached the decision, produced by the same pass that decides
them. This lands the envelope with a denominator that is not that.
The open question -- does every emit-time repair candidate correspond to a
parse-time reference occurrence -- is answered NO, in three independent
directions at once: the roster is deduplicated by SPELLING before any decision
(grain), it admits names merely for appearing as an identifier in the EMITTED
Rust (superset -- nothing authored them, so they can have no occurrence id), and
it drops occurrences the repairer correctly never touches (subset). So R_X(B) is
a PEER of O_X(B) keyed on repair sites, not an instance of it.
The completeness law is one law for any key, so it is hoisted key-generic into
std.observation_completeness and both envelopes instantiate it -- two subjects,
two denominators, one join. decl_field_label moves to std.decl_ref for the same
reason, with the third projection in std.observation named rather than tolerated.
Roster provenance is structural rather than ordered: SubjectRoster is
sole_constructor, prove_subject_roster is its only mint, and the admission takes
one -- so joining against an unproven roster has no spelling.
What this does NOT establish is stated in the carrier beside what it does: the
producer could still assemble the roster from the candidates it decided. The
tautology becomes visible and nameable rather than dissolved, which is an
improvement and not a proof; the next-rung trigger is recorded.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Restore legacy_binding_delta's own occurrences: payload, over-renamed by the hoist's blanket sed
The hoist renames the completeness arms' payload from `occurrences:` to `keys:`,
because at the repair envelope's instantiation the key is a repair site and
"occurrences" would be a lie. `{ occurrences: ... }` also spells the payload on
six unrelated ProvenanceTotality arms in legacy_binding_delta, and a blanket
rename over the witness took those with it -- 71 blocking errors, none of them in
the module the hoist was about.
Caught by compiling the blast radius rather than grepping it, which is the whole
reason it was compiled: "two witness files" is a file count, not a symbol
census, and the payload name was never the thing being renamed -- the TYPE was.
* Rename the roster carrier off a name the enforcement lens already owns, and drop the declaration move out of this change
Three CI failures, three causes.
SubjectRoster was already declared by v2.lens.enforcement.vocab for an
unrelated concept. Whole-corpus resolution handed THIS type to that lens's own
consumers and their `entries` field stopped existing -- nine diagnostics, none
of them in a module this change touches. Renamed to ProvenRepairRoster. The
shape is the finding rather than the fix: the duplicate was minted here and
every symptom surfaced elsewhere, so no compile of this closure could have
shown it, which is what makes "my closure is clean" structurally unable to
catch this class.
decl_field_label's move to std.decl_ref is reverted. It caused both the regen
drift on std_decl_ref.rs and two TargetChanged wave-admission deltas. The
declaration stays in the binding envelope and the repair envelope imports it --
one authority, no fork -- and the relocation lands as its own change where its
two rows are the whole reviewable diff.
The first cut of that annotation justified the revert by citing the wave grain
note's "two change classes in one diff" clause. That was a mis-citation: the
clause's subject is a wave that BOTH REQUALIFIES AND MOVES a symbol, and this
requalifies nothing. Corrected in place rather than dropped, because a carrier
that once stated an invented prohibition should say so.
One unused import removed (ObservationCompleteness in the observation witness).
The remaining two UnexplainedSubjectMotion deltas are a confirmed defect in the
wave-admission channel's reader, owned by another lane; its refusal is left
standing rather than cleared by an admission row, which over a channel that
cannot see the reference would be a manual override rather than an admission.
Evidence: 21/21 witness arms return true; mutating prove_repair_roster's digest
comparison to a constant turns the provenance arm false while the positive
control stays true. All three affected closures compile at 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main, and take the three obligations #9440's landing created
crisp-crab's #9440 merged first, so by the order the two lanes committed to,
this change owes the collision resolution -- and owes it HERE rather than in a
follow-up, because declaration names bind closure-globally and two declarations
of one name on main is a collision, not a shadowing. Neither author can observe
it by compiling their own branch: both were green against main independently.
The receipt is this lane's own SubjectRoster duplicate, which produced nine
diagnostics, every one in v2.lens.enforcement modules that change never touched.
Three obligations, all measured rather than assumed:
- the placeholder `type CompleteLegacyRepairObservation<R>` is deleted from
v2.workflow.legacy_baseline_capture and the real carrier imported from
v2.workflow.legacy_repair_observation. Its accepted arm LegacyBaselineCaptured
is constructible for the first time; the annotation is rewritten to record
why the deletion could not wait rather than left describing a hole that is
now filled.
- the two LegacyObservationCompleteness references the hoist renamed --
the import member and the LegacyBaselineObservationIncomplete payload --
migrated to ObservationCompleteness<Int>. crisp-crab measured their exposure
at exactly two lines and named both; both appeared where they said.
- the second type parameter survives the swap deliberately. O is what the
resolver selected per occurrence, R what the repairer decided per repair
site; one parameter would force the emitter's repair vocabulary to equal the
resolver's binding vocabulary, which is the conflation the operator ruling
forbids, committed in the parameter list instead of the fields.
NOT carried: #9440's three dead imports. The offer was withdrawn after the
coupling was priced -- they are inert, nothing waits on them, and tying someone
else's cleanup to this branch's blocker was never the cheap option.
v2.workflow.legacy_baseline_capture compiles 0 blocking after the change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main: pick up the wave-admission membership fix (#9490) and the repair-decision producer (#9439)
#9490 splits membership_declared from membership_bound_through, so an authored
import claim answers the ADD direction outright. Both UnexplainedSubjectMotion
rows this branch was refusing on carry an explicit import claim naming
std.observation_completeness, so both close without the gate having to reach a
pattern arm or an inferred-slot field type.
#9439 landed the producer this envelope was built for: reference_derived_
candidate_disposition and reference_derived_census in v1.05_emit_rust. The
correspondence finding this branch rests on was read off that pass, and it is
now on main rather than on a branch -- so the annotation citing it names a
declaration that resolves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Refuse a malformed denominator: a roster naming one site twice certified as complete (review 56949)
`std.observation_completeness` returned `ObservationComplete` for expected
`[A, A]` against observed `[A]`. Nothing missing -- A IS present, so both
expected entries filter out. Nothing foreign. Nothing repeated -- the repeat
test counts OBSERVED occurrences and there is one. So the envelope certified
exactness over a denominator that asked for one site twice.
All three refusals judged the ANSWER set. None judged the QUESTION set, and an
ill-formed question set defeats all three at once.
WHY 21 ARMS MISSED IT: every arm varied the OBSERVATION against a well-formed
roster; none varied the ROSTER. A missing AXIS, not a missing case within one --
and the module header already said completeness is a join between two sets while
every arm exercised one of them. The near miss that hid it: `[A,A]` answered
`[A,A]` DOES refuse correctly as repeated-observed, so the obvious fixture finds
nothing. Only the answered-once case slipped.
REPAIRED AT TWO LAYERS, and the receipt shows neither substitutes for the other:
- `ObservationRepeatedExpected`, checked FIRST. The other three arms are
statements ABOUT a question set and are meaningless without a well-formed one;
answering "missing" here names the OBSERVATION as the defect when the ROSTER
is, sending a consumer to fix the wrong artifact.
- `prove_repair_roster` refuses a duplicate outright, so a `ProvenRepairRoster`
cannot HOLD one -- construction at the mint rather than validation at the join.
The generic arm is NOT dead after the proof-side wall: the law is key-generic and
`legacy_binding_observation` derives its expected list with no proven roster, so
the arm is reachable from that consumer's denominator. A quiet guard, not a
decoration.
MUTATION RECEIPT, two independent mutations in sequence (not overlapped):
deleting the law's check reds 2 arms and leaves the proof arm TRUE; deleting the
proof's refusal reds only the proof arm. Unmutated, 24 arms green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Carry the repeated-expected arm into the two binding witnesses the new variant also made non-exhaustive
`ObservationRepeatedExpected` landed with arms added to the repair envelope and
its witness, and NOT to the two binding witnesses that match the same
key-generic law. Six matches, one arm each.
WHY IT REACHED CI: the local check was `v1_src_dag_parse`, which returned
`4210 file(s) parse-clean` and was read as evidence the tree was well-formed.
Exhaustiveness is a RESOLVE-time judgment, so a parse sweep can never see it --
parse-clean and resolves are different claims about different phases, and the
green one was not about the thing being changed. The verification is now a
resolve of each affected witness, which reproduces the six diagnostics when the
arms are absent and passes when they are present.
The variant refusing every exhaustive match across three files is the substrate
doing its job -- nothing could have silently kept the old vocabulary. What
failed was my check, not the wall.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
* scm: a typed read-command result that names no destination (#9443)
* scm: a typed read-command result that names no destination
Recut onto current main so the diff matches the scope this PR claims.
WHY THE RECUT. The previous composition reached main through the save
branch's ancestry, so it carried repository_save.dag and its witness --
neither of which is on main, and both of which belong to #9434, which is
draft. Merging this PR would therefore have landed the parked save half
as a consequence of branch topology rather than as a decision anyone
made. Nobody would have done anything wrong; the ancestry would simply
have outranked the park.
The park is respected rather than routed around. No convert_to_draft
event exists on #9434 and draft is not this tooling's default, so the
hold is unexplained rather than accidental -- and the correct response to
an unexplained hold is to leave it standing.
WHAT REMAINS, and why the load refinement is not scope creep: splitting
RepositoryLoadRefusal out of RepositoryLoad is what lets
ScmReadRepositoryUnavailable carry a refusal that CANNOT hold a success.
Without it this module's unavailable arm would be constructible holding
RepositoryLoaded, with nothing to refuse the pair. It is the enabling
half of this change, not a neighbour travelling with it.
The dependency runs one way, checked before cutting: the save witness
imports RepositoryLoadRefused, and nothing read-side references save. So
dropping save costs this PR nothing.
Both keystones return `true` on this tree over current main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Drop the refusal-path accessor: the third instance of a shape this PR
documents as twice-removed
`repository_load_refusal_path` had exactly one occurrence in the tree --
its own definition. No consumer, so DESIGN section 6 residue.
WHAT MAKES THIS WORSE THAN ORDINARY DEAD CODE: read_command.dag's own
header, in this same PR, cites this exact helper shape being removed
twice before -- once as `checkout_succeeded`, once from
`gunbc.scm.ancestry` under review 56207 -- and states the reason that
survives. This change re-added the third instance while documenting the
first two. Neither a lens nor a green run can see that; only reading the
two files against each other does.
The surviving rationale in the deleted comment block was about the TYPES
(why no `loaded: Bool` exists), not about the accessor, so it moves to
`type RepositoryLoad` rather than being deleted along with the function.
A prose row removed for one reason must not silently take its contents
with it.
It gains the reason the shape keeps recurring, which was written down
nowhere: with no consumer the accessor is residue, and WITH one it is
worse -- a fourth refusal arm would be absorbed by the projection instead
of failing to compile at each site that must decide about it.
Both keystones return `true` after the deletion.
Reported by review 57012.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Enroll the three read-command route gaps the floor actually reported
The floor reported route_gap_unenrolled=3 on this branch, all three in
scm_read_command_witness, all with one cause:
the hermetic route has no arm for Read (operation declares no
mock_response)
scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer
scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log
scm_read_command_keystone_holds
Same boundary already recorded for the load witness: extdeps.filesystem
declares no mock_response, so the hermetic frame has no arm for a FAILING
read. All three claims exercise the absent-repository path, and the
keystone inherits the gap by composing them. They pass under `gunbc run`,
which performs the real read; they cannot reach their subject hermetically.
MEASURED, NOT PREDICTED. These were foreseeable and were deliberately NOT
pre-enrolled: enrolling an identity that does not gap is a stale row and
reds the build, which is what stale_route_gap counts. The rows are added
now because a run reported these exact three identities.
Enrolment records the gap as known debt. It does not make the gap
acceptable and it is not a fix: the remedy is a hermetic arm for a failing
read, which belongs to the filesystem boundary and not to this PR.
Roster 112 -> 115; the module still evaluates and returns its list.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
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>
* Anchor a relative source root the same way in both module-index builders (#9548)
* Anchor a relative source root the same way in both module-index builders
The two builders disagreed on how a relative source root resolves:
try_build_module_index anchored through anchor_source_root (process
workspace), while try_index_source_root_into_module_index read the string
straight off the filesystem (process CWD). One concept, two answers,
selected by which builder a caller happened to reach.
The fork survived because the one place it is observable is the one place
nothing was asserting: every CI invocation runs with its CWD at the
workspace root, where both spellings denote the same directory.
A root that cannot be anchored still falls through to the existence
refusal with its ORIGINAL spelling, so the diagnostic names what the
caller asked for rather than a rewritten form they never wrote.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Trigger a fresh merge ref against main after #9551
The merge ref is computed when the head is pushed, against main as it was
at that moment; main moving afterwards recomputes nothing, and a RERUN
replays the original pinned ref. #9551 landed the four emit mirrors after
this branch's last push, so its base predates the regen fix.
Empty rather than a local merge of main deliberately: main's change here IS
the generated mirrors, and merging it locally would mean hand-resolving
emitted files -- the one state the regen gate forbids. Pushing recomputes
the base without touching them.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
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>
* Measure the fan decoder's execution identity, and refuse to call it bound (#9536)
* Instrument the decoder's execution identity by composing two things that already existed
gunbc.bmc_fan_program_interpretation modelled a decoder identity and refused to author
one, because both digests are properties of an execution and a hand-written pair would
be two literals typed by whoever typed the decoder -- agreeing because one person wrote
both, and continuing to agree after the thing they describe changed. This produces them
from an execution instead, which is what an operator adoption needs: a corrected decoder
that assigns different meaning to the same bytes must be distinguishable from a refactor
that assigns the same meaning.
NOTHING IS MINTED. Both halves were found by searching before building, which is why
this module is short:
v2.lens.module_graph import_closure_live enumerates the entry's closure
tools.multi_module_compile_fixture compile_fixture returns a structural digest over
the (path, content) vector AND the
running compiler binary's own hash,
both host-computed from what ran
ONE NEAR-MISS IS DELIBERATELY NOT REUSED, and it is recorded so nobody "fixes" this by
adopting it. std.interface_summary typed_module_key is exactly the right shape -- a
source key combined with compiler identity -- at the wrong grain: its module_key folds a
module's source hash with its DIRECT IMPORT INTERFACE hashes. A body-only change in a
transitively imported module leaves it unchanged while changing what this decoder
produces; std.decimal canonical_exact_decimal could be rewritten and the key would not
move. It answers "may I reuse a cached typecheck"; this answers "is this the same
reader". Borrowing the first to answer the second invents the entailment rather than
misstating any fact.
THE DISCRIMINATING PAIR IS MEASURED, both halves, because an identity that moves on
everything and one that moves on nothing both look fine from a single run. Baseline
3282f082abc9d722 over 40 modules; one comment line added to std/decimal.dag, inside the
closure, moved it to 9bcfbd782022b120; one comment line added to gunbc/fleet_fan_wiring.dag,
outside it, left it byte-identical to baseline. Both restored byte-exactly. The compiler
digest held across all three.
The second half is the one worth having: a digest over the whole tree passes the first
test and is useless, since every unrelated edit would invalidate an adoption.
WHAT IS NOT CLAIMED. There is no enrolled witness, and the reason is structural rather
than neglect: the instrument reads the live tree and takes about four and a half minutes,
so the floor planner declines it, and the mutation half would have to edit tracked
source, which no hermetic witness may do. The evidence is a recorded measurement with its
controls -- weaker than an executing one, and said so rather than dressed up. The
next-rung trigger is a fixture-grain closure the instrument owns, at which point the pair
becomes an ordinary witness.
Cost is recorded too, because it decides where this may run: the closure walk alone is
about 4m28s. On demand only; nothing here is enrolled in a required lane, and a
four-minute live-tree walk on every push would be the corpus-denominated cost that gets
paid by every consumer wanting something else.
* Report the identity as measured-but-unbound, because nothing here proves the decoder ran on this vector
The side-chat raised the objection that matters and it is right. This instrument
enumerates a closure, hashes that exact vector, and compiles it. It does NOT execute the
decoder against that vector -- a semantic program digest is produced by some other run,
through the interpreter's own resolution of the same entry. Pairing this identity with
that digest would be two individually correct observations with an invented arrow
between them: the same fake join removed from the capture observer on #9299, one level
up.
The two subjects are very probably identical, since the walk follows the same import
edges the interpreter resolves. "Very probably" is what the objection is about. Nothing
here proves the interpreter received this vector and no wider one.
So the standing is not handed out from here. DecoderIdentityEstablished is what lets a
consumer treat two readings as same-reader, and granting it from a run that did not
perform the reading would restore the unbound claim under a name that reads as bound.
The binding is now its own three-state carrier, the measured-but-unbound arm names its
own gap, and the standing derived from it is still the absent one.
That is the instrument reporting what it has rather than failing. The obligation is
NARROWED rather than discharged: what was missing was any producer at all; what is
missing now is one execution that both hashes its source vector and runs the decoder
against that exact vector, returning the identity and the semantic result together.
That trigger is recorded on the arm.
* Sharpen the binding trigger to name the missing host capability
Looked rather than assumed, and the gap is larger than 'finish the instrument'. Two
routes could bind the identity to a decode and neither is reachable today.
EXECUTE-THE-VECTOR: the seed registers exactly one fixture builtin,
compile_dag_multi_module_fixture, which COMPILES a supplied (path, content) vector. No
builtin evaluates one. So running the decoder against that exact vector needs a new host
surface -- v1 seed growth, which the freeze admits only in service of the v2 self-host
program, and this is not that.
PROVE-THE-SUBJECTS-EQUAL: nothing exposes the RUNNING program's resolved module set.
module_declaration_facts reads the source tree, which is the same authority the closure
walk already consumed, so comparing the two would compare a reading against itself rather
than against what the interpreter received.
Recorded at this grain because a trigger that reads as small invites someone to just
finish it, find the capability absent, and close the gap with an argument instead -- which
is the invented arrow this carrier exists to refuse.
* Consume the decoder declaration instead of re-minting it (review 57069)
A byte-identical DeclarationRef for the decoder stood in this instrument
beside gunbc.bmc_fan_program_interpretation fan_program_decoder, which is
the module declaring the standing the instrument exists to discharge --
and which this module already imported from, so consuming it costs one
import member. Two authorities for one fact can drift independently
(DESIGN section 3); worse here than in general, because a drift would
identify a reader other than the one whose standing is at stake.
The entry PATH stays authored and is not the same fork: a module path
does not carry which source root stores the module, and deriving one
needs an observed ModuleStorageIndex rather than a pure transform. The
annotation now says so, so the next reader does not read the surviving
path as a missed half of this repair.
Measured after: identity unchanged -- 40 modules,
source_closure=3282f082abc9d722, compiler_runtime=f2c179fb7e10d373,
the same values the pre-fix baseline reported.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Say that the typed_module_key grain claim is an argument, not a measurement
The note asserted as fact that a body-only change in a transitively
imported module leaves typed_module_key unchanged while changing what the
decoder produces. The reasoning is sound and has now been endorsed by two
reviews and one external adjudication -- which is exactly why it needed
correcting rather than leaving: convergent readings of one argument are
not independent evidence about that argument, and an approved PR carrying
an unmeasured claim stated as fact is the rung inflation DESIGN 4b(1)
names as worse than sitting low.
I tried to measure it and found the route blocked, so the note now carries
that instead of the assertion. The only live producer of import interface
hashes is v2.lens.interface_summary module_key_for_rel_path. It has zero
consumers in the corpus; the first attempt to run it refused with
export_signature_facts `empty authored type name` on
extdeps.shell.credentials env_credential -- a pattern returning an
anonymous record, one of three such declarations. So that lens's live path
is inert in the DESIGN section 6 sense: the machinery exists and the first
exercise of it does not work.
Authoring the two export lists by hand was rejected rather than
overlooked: the claim IS that a body edit leaves the exports equal, so
asserting that equality assumes what the control exists to establish.
Next-rung trigger recorded on the note. Identity re-measured unchanged
(40 modules, source_closure=3282f082abc9d722).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Delete three commentary String rows and the digests they transcribed (review 57083)
The review flagged typed_module_key_grain_note, decoder_identity_
discrimination_note and decoder_identity_cost_note as the section 4c
pattern DESIGN discourages -- pure prose duplicating the // blocks above
them -- and noted broad corpus precedent for it. Precedent is the reason
to fix it in new code rather than the reason to keep it: adding fresh
instances of a discouraged pattern because the corpus is full of them is
how a discouraged pattern becomes the convention.
DESIGN is stricter here than the remark was. Two of the three rows
transcribed digests and a wall time into prose, inside the very module
whose entry point re-derives them, which is the standing "name the
instrument, never transcribe its output" ruling and not merely commentary
debt. So the numbers are gone from the // blocks too. What survives is
the SHAPE of the controls, which does not rot: an edit INSIDE the closure
moves source_closure, an edit OUTSIDE it leaves it byte-identical, both
restore. Anyone wanting the figures runs report_decoder_identity, which
prints them with the module count.
The // blocks are kept where they carry irreducible rationale -- why
typed_module_key is the wrong grain, why no hermetic witness can hold this
pair -- which section 4c permits and which the String rows were only
restating.
Re-measured after: unchanged, 40 modules, same digests the instrument
prints.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
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>
* Witness evidence integrity: an undeclared live_tree_disposition silently declines the module — make silence REFUSE, burn down the 338, then the staged DeclinedLiveTree root deletion is safe (#9471)
* The live-read derivation detects a quarter of the readers it would have to replace
`v2.std.live_tree`'s note named the nightly affected-set falsifier as the thing
that catches a row declaring `SubstrateInputsOnly` while reading live state.
That cadence was deleted by the floor cut (#8283) and the repository carries
three workflows, none of which runs a predict-only cold comparison. The same
note stated the undeclared fail-closed default as THE fact, while the required
floor's own scan defaults the identical silence the opposite way -- so a reader
asking what happens to a witness that declares nothing was told the half that
withholds it, and the consumer that actually executes admits it.
What survives as the backstop is `effect_reach_derived_reads_live_tree_for_entry`,
and it does not derive this fact. It answers host-reading only when two
INDEPENDENT existentials both hold somewhere in the import closure -- some file
carries a repository path literal, some file carries a host-sink call shape --
so a closure that performs a real `Filesystem.Read` and names no path answers
false, and two modules that never call each other supply the two halves between
them. The ceiling is filed as a §4b row on the derivation's own authority, with
its next-rung trigger naming the capability (call-reachability-grade per-witness
classification) rather than an artifact that would contribute to one.
The evidence is a planted pair rather than a corpus count: two fixture entries
differing by exactly one import edge whose only content is a path-literal row,
performing a byte-identical read. The positive control derives host-reading; the
sink-only entry does not. Authored both sides, so the red is a property of the
derivation and cannot be dissolved by corpus drift.
The consequence runs opposite to the standing objection that an authored
disposition duplicates a derivable fact. `reads_live_tree_effective` consults the
declaration FIRST and reaches the derivation only for a row already claiming
SubstrateInputsOnly, so the derivation is the sole thing between a lying row and
a predict-skip. Replacing the declaration with it would be a scope narrowing
wearing a construction argument.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* The derivation's third bound: an unreadable closure file is skipped toward ADMIT
Confirmed by reading effect_reach_derived_reads_live_tree_for_closure_paths: a
closure file that cannot be read hits a bare `continue`, leaving both flags as
they were. Every unreadable file therefore biases the accumulation toward false,
which biases toward admitting a row that claims SubstrateInputsOnly -- the one
arm that could notice its own blindness discards it, in the direction that
weakens the only thing standing behind a lying declaration.
It compounds the empty-adjacency bound rather than sitting beside it: where the
closure is the entry alone, one failed read leaves the loop having seen nothing.
And unlike the conjunction and the adjacency, which are properties of the corpus
and measurable today, this one is a property of the run, so its magnitude is
whatever the filesystem did that time and nothing records it.
Found by swift-badger-524.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Route the ceiling row onto the ladder vocabulary instead of a prose blob
Review 56493 observed that the §4b class row was a large `String`, which §4c
names as misplaced data, and reported that no typed §4b carrier existed to route
into. One does: `gunbc.guarantee_rung_drop` declares the closed `GuaranteeRung`
vocabulary, and `gunbc.hermetic_mock_fidelity` already files a discovered class
in exactly this shape -- typed rung and ceiling, closed-coproduct reasons, and
rationale left in annotations beside the row.
So the row follows that pattern rather than minting a class of its own. The three
bounds become a closed coproduct, because naming them is what lets the class be
recognised a second time; enforcement becomes two reachable arms rather than a
sentence; and the next-rung trigger is DERIVED by a total function over the
coproduct rather than stored, which makes a trigger-less row unwritable instead
of merely checked. That all three bounds derive the same trigger is the finding,
not a redundancy: the capability replaces the approach rather than patching a
term.
The record is named for its subject. No corpus-wide §4b carrier exists, and
minting one from a single instance would put a second authority beside
hermetic_mock_fidelity -- the ladder VOCABULARY is the part that must not fork,
and that is what is reused.
Verified by execution: `gunbc compile --entry src/v2/std/effect_reach.dag`
returns 0 blocking errors, 21 files emitted.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Record that stamping the silent population was built and dropped
A future reader who finds the fail-closed default and the 24.7% backstop
measurement will reach for the obvious move -- stamp every silent witness file
-- and there is nothing in the tree telling them it was already tried. It was:
520 files stamped, silence made a typed located refusal on both consumers, then
discarded because the floor's decline arm was already being deleted at its root,
which is what made a truthful ReadsLiveTree stamp cost coverage in the first
place.
The note records the reason rather than the fact, because the reason is what
transfers: the arm's deletion is the enabling event for a truthful stamp, not
its reward, and the question revives when the selection consumer acquires an
enforcement it currently lacks -- not when the silent population grows.
Suggested by swift-badger-524, who observed the work would otherwise be visible
only in a reflog and one message.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Sweep the dead-cadence enforcement claim from all three of its homes
One claim lived in three places: v2.std.live_tree's disposition note, the same
module's stamp_provenance row, and a mirrored comment above
parse_entry_live_tree_disposition in cli_run.rs. Each said the nightly
affected-set falsifier catches a row declaring SubstrateInputsOnly while reading
live state. falsifier.yml was deleted by the 2026-08-15 floor cut. Correcting one
home leaves the other two as authorities for a false claim, so all three move
together.
The stamp_provenance row gets more than a past tense, because its consequence is
specific: the 2026-07-11 batch is machine-vouched rather than author-vouched and
inherits the deleted classifier's blind spot -- a live read hidden behind an
import was invisible to entry-text scanning. Those stamps were admitted on the
promise that a cadence would catch them if wrong. That promise is now UNMET, not
merely unfulfilled: nothing verifies a stamp, and one that was wrong the day it
was written is still wrong and still unobserved.
Three other authorities carry the same claim and belong to other owners; they are
deliberately not in this diff.
Verified: gunbc compile --entry src/v2/std/live_tree.dag -> 6 files emitted,
0 diagnostics.
Sites located by swift-badger-524.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Turn the supply fold from an honest screen into a real cross-mode selector: the six inputs supply.dag names as missing (#9472)
* wip: cross-mode supply selector
* wip2
* wip3
* wip4: duration state, commitment horizon
* review: fail-closed unbounded-duration availability, quote billing basis projection, Second-typed axis params
* witness: choose the window that the previous fold actually admitted
* Answer the new affordability arm in the sibling fabric witness suite
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids (#9564)
* Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids
Review 46148 ruled that absence is established by a successful listing and never
by a failed read. The ruling was written as a `data ... : String` note, which
DESIGN section 4c calls commentary no `Accepted` program can read -- and it was
then violated in gunbc.deploy_transition, authored beside the note, where a
present-and-unreadable marker rendered as absent and so as PERMITTED at the belt
seam (#9561). A note is not a mechanism.
extdeps.filesystem.filesystem_io gains a carrier with one mint.
FilesystemEstablishedAbsence is sole_constructor; its only mint takes a
FilesystemDirectoryListing, itself sole_constructor and minted only from a
listing whose success channel was true. A module deciding absence from a read
alone has no value to return and no way to build one. filesystem_entry_presence
and filesystem_file_observation are the folds: presence is decided by the
listing, the read is consulted only for an entry the listing named, and every
way of not establishing absence lands in one indeterminate arm.
Consumers, so this is not a carrier with no consumer:
- gunbc.roadmap_verification_receipt, both walks. Already correct by hand; they
now consume the carrier instead of restating the rule, and their private
second spelling of List's wire encoding is deleted for
filesystem_listing_names_entry.
- gunbc.devboot.build read_text_file,…
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
…d at the accounting root, not by declining rows (#9609) * The wall ceiling still charged the shared fill: complete the 2026-08-27 attribution ruling on the clock it is enforced against The floor's cost axis blocks merges, and on main it refuses over two rows whose own cost is 0ms and 1ms. test.claim.transport_script_wall_compile_red's two RED controls refused main run 33145062452 at ~18100ms against a 10000ms WALL requirement. The floor's own instrument says what that figure is, on those exact rows: wall_red_string_join_into_retained_record_refuses marginal_cpu_ms=0 fill_cpu_ms=18966 wall_red_deleted_free_minter_refuses marginal_cpu_ms=1 fill_cpu_ms=18823 Both provenance=filled-shared-artifact, both triggered_by themselves. They are first payers for a shared memo every later claim naming the same source then reads free -- not expensive witnesses. Across all 12949 rows of that run the MAXIMUM marginal_cpu_ms is 72 and only three rows have fill>5000ms, so there is no expensive witness on the floor at all; there are first payers. WHY THIS WAS ALREADY DECIDED AND STILL HAPPENED. The 2026-08-27 operator-line ruling -- a shared-artifact fill is not this claim's marginal cost, and charging it makes a merge-blocking ceiling a function of EXECUTION ORDER rather than of the tree -- is implemented in run_claim_measured. On the CPU clock. The comment directly above the wall figure said in its own words that wall_nanos stayed the measurement basis unchanged, and wall_budget_completion_outcome enforced on that unadjusted number. One accounting rule with two homes, one of which does not apply it: the DESIGN section 3 failure the CPU comment sitting six lines above it already names. WHAT LANDS. Fill wall time is recorded at both memo-miss sites, beside the CPU recording and never without it, so a fill cannot be counted on one clock and not the other -- which is the state that produced this. The claim loop splits the wall clock through a named marginal_wall_nanos, and the receipt records the quantity actually enforced, per the rule the CPU side's own comment states. SPLIT, NEVER DROPPED. Both halves are reported as new marginal_wall_ms / fill_wall_ms / measured_wall_ms columns on the [floor-shared-fill] line and they sum to what the claim spent. The report guard now fires on EITHER clock's fill: a fill that blocks on I/O can spend wall time while charging almost no CPU, and under the previous CPU-keyed guard that fill would have been subtracted from the enforced figure and reported nowhere -- a cost dropped rather than split, which is the one thing the ruling forbids. WHY THE ROOT AND NOT THE ROWS. The defect is not a property of these two rows. It belongs to whichever row reaches a shared memo first, which is a function of discovery order, so withholding this pair leaves the mechanism live and the same refusal reappears on a different pair when the corpus reorders -- with a withhold established as the remedy. That is the absorbing fallback: the deficit's frequency driven to zero by construction while the cause stands. EVIDENCE, AND WHAT IT DOES NOT COVER. The three added controls establish the arithmetic and that the ceiling still refuses an unsplit figure -- the second arm is what makes the first a control rather than a restatement, so the pair fails if the split is removed AND if the ceiling stops firing. They drive marginal_wall_nanos directly, so they do NOT establish that production still calls it and would pass if that wiring were deleted. The executing consumer for the wiring is the floor run itself: these two rows refuse on main and must reach a verdict here, which is a discriminating input rather than a fresh green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Complete #9106's enrolment on the verdict axis: 47 in, 1 out, and the cost axis declared rather than absorbed #9106 deleted the floor's stale live-tree decline -- a file-grain prediction that a live-tree reader could not join the hermetic fold, which had stopped agreeing with what the interpreter does. Deleting it was correct and it admitted a population that had never executed. Main has been red on four causes since. Measured on run 33145062452 (3a8344b): failed=47 interrupted_before_verdict=44 completed_over_cost_requirement=2 stale_quarantine=1. TWO OF THE FOUR CLOSE HERE, and both are the existing mechanism's own paths rather than new machinery. chunk_24 enrols the 47. Every one EXECUTES, REACHES ITS SUBJECT AND ANSWERS FALSE -- the run classifies each as `returned Bool(false)`, which is the semantic verdict this roster is defined over. None overlaps `floor_route_gap` (checked at identity grain: zero), none is already enrolled (zero), none is a budget outcome. THE TREE ALREADY DEMANDED THIS, which is what makes enrolment the intended completion rather than a convenient one. `quarantine_probe_disposition_witness_test` `the_former_live_tree_declined_row_is_now_expected_red` asserts that `legacy_test_behavior_unclassified_frontier_is_zero` is held by this roster. It was authored against the post-#9106 world and has failed every run since, because the row it names was never added -- and that witness is itself one of the 47. Four rows are therefore expected to leave chunk_24 on the first run after it lands, by the roster's own removal path rather than by an edit. The stale-quarantine row comes out: `duplicate_definition_in_one_module_is_refused` is enrolled and PASSING, and the run named it and asked. Repayment and deletion are one act. THE OTHER TWO ARE DECLARED, NOT ABSORBED, and the diff deliberately does not touch them. An interrupted row produced NO VERDICT; enrolling it would assert "this runs and fails and someone is fixing it" about an identity that never answered -- the exact 101-row mistake this file's header opens with, and `ExpectedRedArm` refuses budget outcomes by construction so it would not take. The 2 completed-over-cost rows answered, but what they owe is a cost and not a failure. Cost is not a verdict. The population is bounded and measured at identity grain: 44 interrupted, all CPU-clock against 5000ms, concentrated in live-tree corpus witnesses (13 grammar_coverage_witness, 6 enforcement_live_witness, 6 accumulator_copy_roster_gate, rest across 10 modules); 2 completed-over-cost, both transport_script_wall_compile_red, wall clock at 18882ms and 19024ms against 10000ms. Every interrupted figure is a LOWER BOUND, so their real cost is unmeasured. WHERE THEY GO IS NOT A NEW MECHANISM. `required_floor` names the remedies exhaustively -- reduce what the witness reaches for, or a lane declaring its own dated ceiling -- and rules relocation out. A carrier for exactly this axis is already built and open as gunbc#9517 (`v2.workflow.floor_cost_debt` + a `DeclinedCostDebt` arm), and its roster returns `Empty`: the machinery landed without its population. These 46 are that population. Authoring them into a module that is not on main would fork the authority, so they are handed to that lane at identity grain instead of duplicated here. RUNG (DESIGN 4b(3)): the cost axis stays below the floor's bar -- the run still stops, so nothing is silently admitted, but 46 identities reach no usable verdict every run and no mechanism on main holds them. RESTORATION TRIGGER: #9517's roster carries these 46 under its O=R admission -- and NOT when #9517 merely merges, because #9517 as it stands closes zero of them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Verify the empty-roster claim on witty-wren-148's branch rather than relaying it The chunk_24 declaration asserted that #9517's floor_cost_debt roster returns Empty on the authority of a relayed reading. That reading was correct, and a correct relayed claim is still a claim this file cannot check. Read directly: floor_cost_debt_chunks() on origin/session/witty-wren-148 is Empty {} and the file authors no qualified-name literal, so floor_cost_debt_holds answers false for every name and nothing is ever DeclinedCostDebt. The consequence is what the restoration trigger already turns on and is now stated where a reader meets it: #9517 merging closes none of these 46. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Correct a cross-branch claim that went false within the hour, and un-number the chunk TWO FIXES, both about the same failure mode arriving on different clocks. THE STALE ASSERTION. The previous commit recorded, as a first-hand reading, that #9517's floor_cost_debt roster returns Empty. The reading was honest and it was wrong within the hour -- that branch was moving while I read it, and its roster now carries a population including these 46. A bare present-tense claim about ANOTHER LANE'S HEAD has no producer on this side of the boundary that could re-derive it, so nothing here refuses when it goes false. The sentence is deleted rather than re-pinned to a newer number, because a second number rots the same way. What survives is only what this module can stand behind: these 46 are absent from this roster, deliberately, and why. The restoration trigger is restated to name the CAPABILITY (DESIGN 4b(3), 2026-08-26): a roster ON MAIN carrying the 46 under O=R admission. Explicitly not "#9517 merges", since a merge of an empty roster closes none of them, and explicitly not "that lane enrols them", because an enrolment on an unmerged branch changes nothing about what the required run on main observes. Both of those would fire while main stayed red on 46 rows. THE CHUNK IS NO LONGER NUMBERED. Three open branches each mint floor_expected_red_chunk_24 into this file: this one, #9587 (one add-slice row) and #9569 (six sole_constructor rows, which are also six of the 47 here). The numeric suffix is a shared mutable counter every concurrent lane computes independently from the same base, so collision is the expected outcome, not a risk. And it is worse than an ordinary conflict. Two lanes appending a same-named fn at different offsets can merge with NO conflict markers, leaving one file with two definitions of one name, and this repository has measured what happens then: test.claim.duplicate_definition_binding_probe exists because a duplicate definition is silently accepted and the later binding wins. The merge would not fail; it would quietly drop one lane's rows and stay green. A position-derived name is a second naming scheme for something the declaration already names (DESIGN section 3), and this is that rule's cost arriving in the merge graph. A meaning-carrying name cannot be independently derived by two lanes, so the collision becomes unrepresentable instead of detected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Drop an overclaim, and name the three groups the roster's bare identity strings cannot distinguish All 47 stay enrolled. What changes is what the header claims about them. THE OVERCLAIM. The chunk said every row "EXECUTES, REACHES ITS SUBJECT AND ANSWERS FALSE". The run establishes the first and third and not the second: Bool has no spelling for "I could not observe my subject", so an unreached subject and a genuine NO both render as returned Bool(false). That is this document's own execution-provenance-loss class, and the clause is removed rather than softened because a reader quoting it would be quoting a property nothing measured. THE THREE GROUPS. A row here is a bare identity string with no reason field, so enrolment says exactly one thing about 47 rows failing for at least six causes with different remedies. Named in the header as follow-ups, verified against the cited files rather than accepted on report: 1. The three guarantee_floor_class_probe_witness generic-instantiation rows fail because a WALL LANDED, not because the hole is open. Discriminating evidence: both of that hole's controls PASS and the sibling field_through_generics hole probe also passes, so the harness reached the judgment and the other hole is genuinely still open -- a harness seeing nothing would have taken the sibling down too. That module's own scope note prescribes the remedy verbatim: rewrite as ExpectBlockingRefusal rather than delete the probe, which is DESIGN 4b(4). 2. The four sole_constructor f10 rows answered an open question the first time they ran. Their annotation states a question, not a marked red, and the answer is yes: _ab fails while _ba passes on identical source with imports swapped, and the two direct probes fail in opposite directions -- last-import-wins. The distinction is decidable in the file: f13 and f19, enrolled here on the same footing, carry an explicit "Deliberately RED" marking and the f10 four do not. 3. The three cost_coverage_witness rows are the subject-reachability candidate. That module's 7 passing fns are the ones that survive an empty subject; the 3 failing ones demand non-zero content. Consistent with a genuine NO and equally consistent with a subject never reached. Enrolled as failing, which is what was observed; not asserted to be semantic. WHY FOLLOW-UPS AND NOT A SPLIT. Enrolment is a reversible holding state with a loud exit: the floor refuses on an enrolled row that starts passing and names it, which is the same path by which this change removes one. So none of the three can be left quietly at rest. Against that, holding rows back keeps the floor red, and the compute fabric is fail-closed on the floor -- gunbc.fleet_desired_admission refuses to advance the desired ref until the floor concludes Success on some revision. A STALE PREMISE FOUND WHILE CHECKING THE ABOVE. gunbc.declined_live_tree_defect_classification states it "must never become" an expected-red enrolment "because the floor does not run it at all". Eight of the modules it classifies contain rows enrolled here, and the floor DOES now run them -- they are in run 33145062452's FAIL lines. The clause is not wrong about authority substitution in general; its REASON has been overtaken by #9106. Not edited here, because it is that carrier's to correct and a second account of one fact is the defect either way. The triage behind groups 1-3 is crisp-newt-899's, checked here against the files. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * The run adjudicated the prediction: 47 becomes 44, and the count was wrong by one in an instructive way Run 33154432928 on a474f45: failed=0 stale_quarantine=3. WHAT WAS PREDICTED, registered in the PR body before the run: enrolling legacy_test_behavior_unclassified_frontier_is_zero satisfies the assertion the three quarantine_probe_disposition_witness_test claims make ABOUT this roster, so they stop failing and report STALE-QUARANTINE. The floor named exactly those three. They are removed here by the roster's own removal path. THE PREDICTION SAID FOUR. The fourth name was legacy_test_behavior_unclassified_frontier_is_zero itself, and it did not flip -- correctly. It is the row the join is ABOUT, not a row that passes as a consequence: it still fails on its own subject and this roster still holds it. I conflated "the identity a witness names" with "an identity that changes state when the witness is satisfied", and a join has both roles in it at once. That is recorded in the header rather than quietly corrected, because the error is the more instructive half of the result. WHY THE ENROLMENT WAS STILL RIGHT FOR ALL THREE, and this is what keeps the removal from reading as a mistake being fixed: they failed on main and answered false, so they met this roster's admission when they were added. What removed them is that the same change repaired their subject. A roster that could not hold a row for one run and release it on the next would force an author to predict the repair perfectly before landing it -- and the loud STALE-QUARANTINE exit is exactly the mechanism that makes holding safe. FLOOR STATE AFTER THIS: failed=0, stale_quarantine=0 expected. The verdict axis closes. The 44 interrupted and 2 completed-over-cost remain and are the declared cost axis, owned by #9517; required_floor_outcome_is_clean makes interrupted_before_verdict.is_empty() a conjunct at claim_executor.rs:1766, so main stays red until that lane lands. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Exercise the cost-debt contract's exit path: the two wall rows become cheap, so they leave the roster v2.workflow.floor_cost_debt withholds 276 identities from the floor's plan -- suppress_withheld removes them before the fold, so a withheld row does not execute at all. Both transport_script_wall_compile_red rows were in it. WHY THAT HAD TO CHANGE IN THIS PR RATHER THAN LATER. While those rows sat in the roster the floor reported completed_over_cost_requirement=0 BECAUSE THEY DID NOT RUN, which is indistinguishable in that counter from this branch's wall netting having repaired them. The fix's discriminating evidence is precisely those two rows reaching a verdict where they previously refused, and a withheld row produces no verdict to transition. Landing the netting while they stayed withheld would have shipped a repair with no observable consumer. THE DELETION IS THE CONTRACT'S OWN PRESCRIBED EXIT, not a judgement call made here. floor_cost_debt's header names this lane and states the condition: 'cool-koi-235 is repairing it at the root by netting fill out of the wall clock as it already is for CPU; when that lands these two become cheap rather than invisible and their rows should be DELETED, which is the ordinary shrink this contract is built for.' That condition is now met. The same header explains why it declined to drop them pre-emptively -- 'dropping a row whose cost is an artifact is right only once the artifact is gone' -- and that reasoning is kept in the past tense rather than deleted, because it is what lets a later reader tell this shrink from a premature one. CHECKED BEFORE EDITING, because suppress_withheld applies to THREE rosters and a deletion here makes any dormant enrolment elsewhere observable again: neither identity appears in floor_expected_red, floor_route_gap or floor_non_verdict, so nothing wakes. They return to ordinary execution with no disposition attached. Also checked: no witness asserts either identity's membership in this roster -- the discovery census witness pins a different member on purpose, the seed-growth carrier enumerates no identities, and required_floor's mention is historical calibration prose. Their own marginal work is 0ms and 1ms. What withholding hid was an accounting artifact, not a cost. The two current-population counts in the header move 276 -> 274. The two historical figures in the same file do not: they describe a superseded roster and a measurement taken on a different tree, and rewriting them would destroy the provenance the file keeps deliberately. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Aug 28, 2026
…th home of one accounting rule (#9612) * The wall ceiling still charged the shared fill: complete the 2026-08-27 attribution ruling on the clock it is enforced against The floor's cost axis blocks merges, and on main it refuses over two rows whose own cost is 0ms and 1ms. test.claim.transport_script_wall_compile_red's two RED controls refused main run 33145062452 at ~18100ms against a 10000ms WALL requirement. The floor's own instrument says what that figure is, on those exact rows: wall_red_string_join_into_retained_record_refuses marginal_cpu_ms=0 fill_cpu_ms=18966 wall_red_deleted_free_minter_refuses marginal_cpu_ms=1 fill_cpu_ms=18823 Both provenance=filled-shared-artifact, both triggered_by themselves. They are first payers for a shared memo every later claim naming the same source then reads free -- not expensive witnesses. Across all 12949 rows of that run the MAXIMUM marginal_cpu_ms is 72 and only three rows have fill>5000ms, so there is no expensive witness on the floor at all; there are first payers. WHY THIS WAS ALREADY DECIDED AND STILL HAPPENED. The 2026-08-27 operator-line ruling -- a shared-artifact fill is not this claim's marginal cost, and charging it makes a merge-blocking ceiling a function of EXECUTION ORDER rather than of the tree -- is implemented in run_claim_measured. On the CPU clock. The comment directly above the wall figure said in its own words that wall_nanos stayed the measurement basis unchanged, and wall_budget_completion_outcome enforced on that unadjusted number. One accounting rule with two homes, one of which does not apply it: the DESIGN section 3 failure the CPU comment sitting six lines above it already names. WHAT LANDS. Fill wall time is recorded at both memo-miss sites, beside the CPU recording and never without it, so a fill cannot be counted on one clock and not the other -- which is the state that produced this. The claim loop splits the wall clock through a named marginal_wall_nanos, and the receipt records the quantity actually enforced, per the rule the CPU side's own comment states. SPLIT, NEVER DROPPED. Both halves are reported as new marginal_wall_ms / fill_wall_ms / measured_wall_ms columns on the [floor-shared-fill] line and they sum to what the claim spent. The report guard now fires on EITHER clock's fill: a fill that blocks on I/O can spend wall time while charging almost no CPU, and under the previous CPU-keyed guard that fill would have been subtracted from the enforced figure and reported nowhere -- a cost dropped rather than split, which is the one thing the ruling forbids. WHY THE ROOT AND NOT THE ROWS. The defect is not a property of these two rows. It belongs to whichever row reaches a shared memo first, which is a function of discovery order, so withholding this pair leaves the mechanism live and the same refusal reappears on a different pair when the corpus reorders -- with a withhold established as the remedy. That is the absorbing fallback: the deficit's frequency driven to zero by construction while the cause stands. EVIDENCE, AND WHAT IT DOES NOT COVER. The three added controls establish the arithmetic and that the ceiling still refuses an unsplit figure -- the second arm is what makes the first a control rather than a restatement, so the pair fails if the split is removed AND if the ceiling stops firing. They drive marginal_wall_nanos directly, so they do NOT establish that production still calls it and would pass if that wiring were deleted. The executing consumer for the wiring is the floor run itself: these two rows refuse on main and must reach a verdict here, which is a discriminating input rather than a fresh green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Complete #9106's enrolment on the verdict axis: 47 in, 1 out, and the cost axis declared rather than absorbed #9106 deleted the floor's stale live-tree decline -- a file-grain prediction that a live-tree reader could not join the hermetic fold, which had stopped agreeing with what the interpreter does. Deleting it was correct and it admitted a population that had never executed. Main has been red on four causes since. Measured on run 33145062452 (3a8344b): failed=47 interrupted_before_verdict=44 completed_over_cost_requirement=2 stale_quarantine=1. TWO OF THE FOUR CLOSE HERE, and both are the existing mechanism's own paths rather than new machinery. chunk_24 enrols the 47. Every one EXECUTES, REACHES ITS SUBJECT AND ANSWERS FALSE -- the run classifies each as `returned Bool(false)`, which is the semantic verdict this roster is defined over. None overlaps `floor_route_gap` (checked at identity grain: zero), none is already enrolled (zero), none is a budget outcome. THE TREE ALREADY DEMANDED THIS, which is what makes enrolment the intended completion rather than a convenient one. `quarantine_probe_disposition_witness_test` `the_former_live_tree_declined_row_is_now_expected_red` asserts that `legacy_test_behavior_unclassified_frontier_is_zero` is held by this roster. It was authored against the post-#9106 world and has failed every run since, because the row it names was never added -- and that witness is itself one of the 47. Four rows are therefore expected to leave chunk_24 on the first run after it lands, by the roster's own removal path rather than by an edit. The stale-quarantine row comes out: `duplicate_definition_in_one_module_is_refused` is enrolled and PASSING, and the run named it and asked. Repayment and deletion are one act. THE OTHER TWO ARE DECLARED, NOT ABSORBED, and the diff deliberately does not touch them. An interrupted row produced NO VERDICT; enrolling it would assert "this runs and fails and someone is fixing it" about an identity that never answered -- the exact 101-row mistake this file's header opens with, and `ExpectedRedArm` refuses budget outcomes by construction so it would not take. The 2 completed-over-cost rows answered, but what they owe is a cost and not a failure. Cost is not a verdict. The population is bounded and measured at identity grain: 44 interrupted, all CPU-clock against 5000ms, concentrated in live-tree corpus witnesses (13 grammar_coverage_witness, 6 enforcement_live_witness, 6 accumulator_copy_roster_gate, rest across 10 modules); 2 completed-over-cost, both transport_script_wall_compile_red, wall clock at 18882ms and 19024ms against 10000ms. Every interrupted figure is a LOWER BOUND, so their real cost is unmeasured. WHERE THEY GO IS NOT A NEW MECHANISM. `required_floor` names the remedies exhaustively -- reduce what the witness reaches for, or a lane declaring its own dated ceiling -- and rules relocation out. A carrier for exactly this axis is already built and open as gunbc#9517 (`v2.workflow.floor_cost_debt` + a `DeclinedCostDebt` arm), and its roster returns `Empty`: the machinery landed without its population. These 46 are that population. Authoring them into a module that is not on main would fork the authority, so they are handed to that lane at identity grain instead of duplicated here. RUNG (DESIGN 4b(3)): the cost axis stays below the floor's bar -- the run still stops, so nothing is silently admitted, but 46 identities reach no usable verdict every run and no mechanism on main holds them. RESTORATION TRIGGER: #9517's roster carries these 46 under its O=R admission -- and NOT when #9517 merely merges, because #9517 as it stands closes zero of them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Verify the empty-roster claim on witty-wren-148's branch rather than relaying it The chunk_24 declaration asserted that #9517's floor_cost_debt roster returns Empty on the authority of a relayed reading. That reading was correct, and a correct relayed claim is still a claim this file cannot check. Read directly: floor_cost_debt_chunks() on origin/session/witty-wren-148 is Empty {} and the file authors no qualified-name literal, so floor_cost_debt_holds answers false for every name and nothing is ever DeclinedCostDebt. The consequence is what the restoration trigger already turns on and is now stated where a reader meets it: #9517 merging closes none of these 46. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Correct a cross-branch claim that went false within the hour, and un-number the chunk TWO FIXES, both about the same failure mode arriving on different clocks. THE STALE ASSERTION. The previous commit recorded, as a first-hand reading, that #9517's floor_cost_debt roster returns Empty. The reading was honest and it was wrong within the hour -- that branch was moving while I read it, and its roster now carries a population including these 46. A bare present-tense claim about ANOTHER LANE'S HEAD has no producer on this side of the boundary that could re-derive it, so nothing here refuses when it goes false. The sentence is deleted rather than re-pinned to a newer number, because a second number rots the same way. What survives is only what this module can stand behind: these 46 are absent from this roster, deliberately, and why. The restoration trigger is restated to name the CAPABILITY (DESIGN 4b(3), 2026-08-26): a roster ON MAIN carrying the 46 under O=R admission. Explicitly not "#9517 merges", since a merge of an empty roster closes none of them, and explicitly not "that lane enrols them", because an enrolment on an unmerged branch changes nothing about what the required run on main observes. Both of those would fire while main stayed red on 46 rows. THE CHUNK IS NO LONGER NUMBERED. Three open branches each mint floor_expected_red_chunk_24 into this file: this one, #9587 (one add-slice row) and #9569 (six sole_constructor rows, which are also six of the 47 here). The numeric suffix is a shared mutable counter every concurrent lane computes independently from the same base, so collision is the expected outcome, not a risk. And it is worse than an ordinary conflict. Two lanes appending a same-named fn at different offsets can merge with NO conflict markers, leaving one file with two definitions of one name, and this repository has measured what happens then: test.claim.duplicate_definition_binding_probe exists because a duplicate definition is silently accepted and the later binding wins. The merge would not fail; it would quietly drop one lane's rows and stay green. A position-derived name is a second naming scheme for something the declaration already names (DESIGN section 3), and this is that rule's cost arriving in the merge graph. A meaning-carrying name cannot be independently derived by two lanes, so the collision becomes unrepresentable instead of detected. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Drop an overclaim, and name the three groups the roster's bare identity strings cannot distinguish All 47 stay enrolled. What changes is what the header claims about them. THE OVERCLAIM. The chunk said every row "EXECUTES, REACHES ITS SUBJECT AND ANSWERS FALSE". The run establishes the first and third and not the second: Bool has no spelling for "I could not observe my subject", so an unreached subject and a genuine NO both render as returned Bool(false). That is this document's own execution-provenance-loss class, and the clause is removed rather than softened because a reader quoting it would be quoting a property nothing measured. THE THREE GROUPS. A row here is a bare identity string with no reason field, so enrolment says exactly one thing about 47 rows failing for at least six causes with different remedies. Named in the header as follow-ups, verified against the cited files rather than accepted on report: 1. The three guarantee_floor_class_probe_witness generic-instantiation rows fail because a WALL LANDED, not because the hole is open. Discriminating evidence: both of that hole's controls PASS and the sibling field_through_generics hole probe also passes, so the harness reached the judgment and the other hole is genuinely still open -- a harness seeing nothing would have taken the sibling down too. That module's own scope note prescribes the remedy verbatim: rewrite as ExpectBlockingRefusal rather than delete the probe, which is DESIGN 4b(4). 2. The four sole_constructor f10 rows answered an open question the first time they ran. Their annotation states a question, not a marked red, and the answer is yes: _ab fails while _ba passes on identical source with imports swapped, and the two direct probes fail in opposite directions -- last-import-wins. The distinction is decidable in the file: f13 and f19, enrolled here on the same footing, carry an explicit "Deliberately RED" marking and the f10 four do not. 3. The three cost_coverage_witness rows are the subject-reachability candidate. That module's 7 passing fns are the ones that survive an empty subject; the 3 failing ones demand non-zero content. Consistent with a genuine NO and equally consistent with a subject never reached. Enrolled as failing, which is what was observed; not asserted to be semantic. WHY FOLLOW-UPS AND NOT A SPLIT. Enrolment is a reversible holding state with a loud exit: the floor refuses on an enrolled row that starts passing and names it, which is the same path by which this change removes one. So none of the three can be left quietly at rest. Against that, holding rows back keeps the floor red, and the compute fabric is fail-closed on the floor -- gunbc.fleet_desired_admission refuses to advance the desired ref until the floor concludes Success on some revision. A STALE PREMISE FOUND WHILE CHECKING THE ABOVE. gunbc.declined_live_tree_defect_classification states it "must never become" an expected-red enrolment "because the floor does not run it at all". Eight of the modules it classifies contain rows enrolled here, and the floor DOES now run them -- they are in run 33145062452's FAIL lines. The clause is not wrong about authority substitution in general; its REASON has been overtaken by #9106. Not edited here, because it is that carrier's to correct and a second account of one fact is the defect either way. The triage behind groups 1-3 is crisp-newt-899's, checked here against the files. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * The run adjudicated the prediction: 47 becomes 44, and the count was wrong by one in an instructive way Run 33154432928 on a474f45: failed=0 stale_quarantine=3. WHAT WAS PREDICTED, registered in the PR body before the run: enrolling legacy_test_behavior_unclassified_frontier_is_zero satisfies the assertion the three quarantine_probe_disposition_witness_test claims make ABOUT this roster, so they stop failing and report STALE-QUARANTINE. The floor named exactly those three. They are removed here by the roster's own removal path. THE PREDICTION SAID FOUR. The fourth name was legacy_test_behavior_unclassified_frontier_is_zero itself, and it did not flip -- correctly. It is the row the join is ABOUT, not a row that passes as a consequence: it still fails on its own subject and this roster still holds it. I conflated "the identity a witness names" with "an identity that changes state when the witness is satisfied", and a join has both roles in it at once. That is recorded in the header rather than quietly corrected, because the error is the more instructive half of the result. WHY THE ENROLMENT WAS STILL RIGHT FOR ALL THREE, and this is what keeps the removal from reading as a mistake being fixed: they failed on main and answered false, so they met this roster's admission when they were added. What removed them is that the same change repaired their subject. A roster that could not hold a row for one run and release it on the next would force an author to predict the repair perfectly before landing it -- and the loud STALE-QUARANTINE exit is exactly the mechanism that makes holding safe. FLOOR STATE AFTER THIS: failed=0, stale_quarantine=0 expected. The verdict axis closes. The 44 interrupted and 2 completed-over-cost remain and are the declared cost axis, owned by #9517; required_floor_outcome_is_clean makes interrupted_before_verdict.is_empty() a conjunct at claim_executor.rs:1766, so main stays red until that lane lands. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NHhQMNap6UfsQbkmVEQm7J * Net shared-artifact fill out of the CPU evaluation deadline: the fourth home of one accounting rule The required floor refuses on interrupted_before_verdict, 44 rows on run 33185280160, every one of them on the Cpu clock. Those interruptions are produced by a deadline that charges a claim for work every later claim reads free. THE RULE IS NOT NEW AND THIS IS ITS FOURTH HOME. The 2026-08-27 operator-line ruling -- a shared-artifact fill is not this claim's marginal cost, and charging it makes a merge-blocking ceiling a function of EXECUTION ORDER rather than of the tree -- has now been applied one site at a time: the completion-side CPU split, then the completion-side WALL split, and now the CPU deadline. Each application happened only after that site's omission had cost something. WHY POST-HOC NETTING COULD NOT REACH THIS. run_claim_measured nets at COMPLETION; the deadline fires DURING execution on a baseline taken from raw thread_cpu_nanos(). A row killed mid-fill never reaches the netting at all. Worse for exactly the population at issue: per std.evaluation_budget's PREEMPTION-1 note the poll is only read between eval_expr calls and compile_dag_rust_emit_check never calls back into eval_expr, so the deadline fires at the first poll AFTER a compile fill returns, having been charged the whole thing. The row completes the fill, every later claim reads the memo free, and the row that paid for it dies. THE CONSTRUCTION IS A CLOCK, NOT A BASELINE PAIR. budgeted_cpu_nanos() is thread CPU less this thread's accumulated fill, and every CPU budget site reads it -- arm_eval_deadline, eval_deadline_remaining_ms, the stride poll, and the enter_evaluation_budget scoped guard. Because both the arming instant and the polling instant come from that one function, the fill accrued between them cancels inside a subtraction that already exists. The alternative -- storing a (cpu, fill) baseline tuple and subtracting at each poll -- requires every present and future site to REMEMBER to net, and a site that forgets is a silent defect. Here there is nothing to forget (DESIGN 5, construction over validation). It is monotone, which a deadline requires: fill is measured on the same thread clock inside the miss path, so raw CPU rises by at least as much as fill over any interval and the difference never decreases. THE COUNTER MOVED, AND HAD TO. It now lives in v1_interpreter with cli_run delegating, because the deadline must net the same quantity WHILE a claim runs and the interpreter cannot read a cell cli_run owns. One counter with two readers rather than two counters that drift -- which is the same one-rule-many-homes defect this commit repairs, avoided rather than repeated. EVIDENCE. Three controls, and the discriminating pair is established by execution: with budgeted_cpu_nanos reverted to raw thread_cpu_nanos, the fill assertion and the monotonicity assertion both FAIL while the ordinary-work control still passes -- a control insensitive to the fix, which is what makes the other two informative. Three earlier formulations of that test were wrong and are recorded in the test's own annotations, because each failed while the production code was correct: one compared against a spin loop's measured cost and the runner reported zero, conflating a dead clock with broken netting; one asserted an identity between deltas spanning different overlapping intervals; one injected a fill larger than the thread's own CPU, a state production cannot reach because a fill is bounded by the raw clock by construction. WHAT IS NOT CLAIMED. No floor run has adjudicated this, so nothing is asserted about how many of the 44 clear. Two opposite predictions were registered before the fact and only a run decides. If NEITHER group moves, the netting did not reach the deadline path and the result says nothing about cost. THE WALL DEADLINE IS UNREPAIRED AND DECLARED. It still arms on a raw Instant and still charges a fill to whoever paid it. All 44 interruptions are Cpu, so the arm is currently unexercised -- a fact about today's population, not the mechanism -- so it is a countable obligation in gunbc.guarantee_rung_drop whose trigger is an OBSERVATION that fires from the ledger without anyone remembering the row exists: the first INTERRUPTED-BEFORE-VERDICT row whose clock is Wall. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Exercise the cost-debt contract's exit path: the two wall rows become cheap, so they leave the roster v2.workflow.floor_cost_debt withholds 276 identities from the floor's plan -- suppress_withheld removes them before the fold, so a withheld row does not execute at all. Both transport_script_wall_compile_red rows were in it. WHY THAT HAD TO CHANGE IN THIS PR RATHER THAN LATER. While those rows sat in the roster the floor reported completed_over_cost_requirement=0 BECAUSE THEY DID NOT RUN, which is indistinguishable in that counter from this branch's wall netting having repaired them. The fix's discriminating evidence is precisely those two rows reaching a verdict where they previously refused, and a withheld row produces no verdict to transition. Landing the netting while they stayed withheld would have shipped a repair with no observable consumer. THE DELETION IS THE CONTRACT'S OWN PRESCRIBED EXIT, not a judgement call made here. floor_cost_debt's header names this lane and states the condition: 'cool-koi-235 is repairing it at the root by netting fill out of the wall clock as it already is for CPU; when that lands these two become cheap rather than invisible and their rows should be DELETED, which is the ordinary shrink this contract is built for.' That condition is now met. The same header explains why it declined to drop them pre-emptively -- 'dropping a row whose cost is an artifact is right only once the artifact is gone' -- and that reasoning is kept in the past tense rather than deleted, because it is what lets a later reader tell this shrink from a premature one. CHECKED BEFORE EDITING, because suppress_withheld applies to THREE rosters and a deletion here makes any dormant enrolment elsewhere observable again: neither identity appears in floor_expected_red, floor_route_gap or floor_non_verdict, so nothing wakes. They return to ordinary execution with no disposition attached. Also checked: no witness asserts either identity's membership in this roster -- the discovery census witness pins a different member on purpose, the seed-growth carrier enumerates no identities, and required_floor's mention is historical calibration prose. Their own marginal work is 0ms and 1ms. What withholding hid was an accounting artifact, not a cost. The two current-population counts in the header move 276 -> 274. The two historical figures in the same file do not: they describe a superseded roster and a measurement taken on a different tree, and rewriting them would destroy the provenance the file keeps deliberately. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
…rol the row, keep the probe (#9589) `test.claim.duplicate_definition_binding_probe.duplicate_definition_in_one_module_is_refused` is enrolled in `v2.workflow.floor_expected_red` and now PASSES. The floor has been printing its own remedy on every run -- "is enrolled as expected-red and PASSED - remove it from v2.workflow.floor_expected_red" -- so the mechanism had already decided; nobody had done it. WHY IT IS NOT INERT. A repaired row left enrolled is a LIVE EXEMPTION: the witness is fixed today, and should it regress it is already rostered, so `stale_quarantine` admits it silently. Leaving it is not tolerating one small red, it is holding a wall disarmed for that identity. THE ROW'S OWN DISSOLUTION CONDITION FIRED. Its annotation (authored in #9093) declared it "dissolves from this roster when same-name declarations in one module refuse at ingestion, then remains as an ordinary permanent regression control". That is what happened, by the route the same annotation predicted: the module is `ReadsLiveTree`, so before the root cut every such site routed to `DeclinedLiveTree` -- discovered, counted, never run. #9106 deleted that decline, the row executed for the first time, and it passed. This is one of that PR's GOOD outcomes, not one of the 47 failures it also surfaced. UN-ENROL, NOT DELETE (DESIGN 4b(4)). The probe stays as a permanent regression control: removing the witness with its roster row would close the conjunct by destroying the executing evidence that the wall holds, which is the 4b(4) failure one level in. THE GREEN IS DISCRIMINATING, checked rather than assumed. On main run 33141550579 the row is reported under the PLAIN stale-quarantine arm (not `PassedOverBudget`, whose text carries a budget clause), and its positive control `single_definition_module_is_clean` is absent from the FAILED set in the same run -- so the assertion is not green by the probe source having broken some other way. What is NOT claimed is the mechanism: the row asserts a blocking-diagnostic count and that count is now met; which predicate produces the diagnostic has not been read, and naming one from the row's passing alone would be a situation mistaken for a cause. SCOPE: THIS CLOSES ONE OF FOUR CONJUNCTS AND DOES NOT UNBLOCK MAIN. The floor refuses on the nine-conjunct `required_floor_outcome_is_clean`; four are non-empty on main and on every branch containing #9106 -- failures=47, stale_quarantine=1, interrupted_before_verdict=44, completed_over_cost_requirement=2. This removes the second. The other three stand, and `completed_over_cost_requirement=2` is two independent cost rows rather than this row double-counted (the arm that pushes to both carries a budget clause; this row does not). The chunk stays non-empty and linked, so `floor_expected_red_chunk_coherence_check` is unaffected. Verified with the parse sweep: `v1_src_dag_parse` reports 4241 files parse-clean, exit 0, citation debt unchanged at 42. Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Aug 28, 2026
* The floor's demand and its supply selection are one join, and select_supply gets its first caller
select_supply has been complete and unconsumed since it landed. This module
is the join: the required floor's own Work becomes a Demand, and the candidate
roster is ranked by the authority that already knew how, rather than by a
second ranking written beside it.
What this does NOT do is stated in the module header rather than left to be
inferred: selecting an offer is a DECISION, not an execution. No Grant is
committed, no process starts, no host effect is reached. The invariant
fabric_witness_run builds toward -- no committed Grant, no process -- is not
established here.
Four rows, green by execution in one run: a host larger than the floor is
selected for it (positive control), a host smaller than the floor is
CONSIDERED and REFUSED rather than silently dropped (the discriminating red),
an empty roster selects nothing and considers nothing, and the floor demand
carries the authority's own satisfaction requirement rather than a copy.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* A compare-and-set whose target came from the expectation could commit against a slot that was never there
std.durable_compare_and_set has had no production realization since it landed.
This is the first, and it is the shape that module's own header asks for: the
store owns the read and the conditional write in one operation, so no caller
ever supplies a free-standing observation and the declared key-relation
boundary is closed by construction rather than observed and refused.
The mechanism is generation-suffixed slots. A slot at generation N is the file
<root>/<key>.<N>, written once and never rewritten, so both expectations reduce
to one primitive -- create-if-absent is create-new key.1, update-from-N is
create-new key.N+1 -- and create-new is O_EXCL. Exclusion is therefore performed
by the operating system on the write itself rather than by a lock the caller
holds, which is the gap the interface names: the existing exclusion is flock,
single-host by construction, and cannot serialize two writers on different
hosts. Verified on both the interpreter and the emitter paths rather than taken
from the prose note, because a rung is per-path.
THE DEFECT THIS COMMIT ALSO REPAIRS WAS MINE, FOUND BEFORE IT LANDED. The first
cut derived the target generation from the EXPECTATION and let O_EXCL decide.
That is sound for ExpectSlotAbsent and wrong for ExpectSlotGeneration, because
O_EXCL excludes competing writers for the TARGET PATH and establishes nothing
about which generation is currently the head. An attempt expecting generation 7
against an EMPTY store computed target 8, found key.8 free, won the create, and
reported a commit on a precondition that was never true.
The target is now derived from the OBSERVATION. An expectation is a claim about
the store, and deriving the write target from the claim rather than from the
store is the whole of the bug. The invariant is that the read establishes
eligibility and the exclusive write decides the winner -- reading first does not
reopen a time-of-check-to-time-of-use race, because two writers that both
observe head N both derive N+1 and exactly one create succeeds.
THE EVIDENCE IS THE FILESYSTEM, NOT A BOOLEAN. The live probe drives five
attempts and the store is left holding exactly slot-a.1 and slot-a.2. There is
no slot-a.8 and no slot-b.8, and under the old derivation both would exist --
an expectation of generation 7 is refused against a slot at generation 2 and
against a slot that does not exist at all, with no write attempted in either
case.
That probe is an entry point rather than a shell script because an ad-hoc .sh
here is unmodeled realization: if a measurement is worth re-deriving it is worth
an entry point.
TWO FURTHER DEFECTS FOUND BY BUILDING RATHER THAN BY READING. CasOutcome has
three arms and none can say the attempt's digest does not match its payload;
reporting that as a store refusal blames the store for the caller lying, so the
input is narrowed instead of the shared type widened -- a sole_constructor
verified-attempt whose only mint verifies the digest, which the interface says
is exactly the realizing store's duty and which is available here because this
realization is concrete at the type the hash function accepts. And the key is
interpolated into a path, so a key carrying a separator escaped the store root;
refused at the mint, and refusing the separator alone is sufficient because the
generation suffix is always appended so a bare dot-dot can never be a final
component.
A WITNESS WAS DELETED RATHER THAN REPAIRED. the_target_generation_is_derived_-
from_the_expectation_and_never_supplied was green, and it was green because it
pinned the defective invariant. Keeping it beside the fix would leave the corpus
asserting both the defect and its repair. Its replacement cannot be hermetic:
the corrected derivation reads the store, so every discriminating row for it
performs a host effect and belongs to the live probe.
Scope declared rather than overclaimed. sole_constructor confines construction
on the source-to-.dag path; DESIGN records by execution that an emitted mirror
is forgeable, so the mint is sufficient for the path this carrier travels and
nothing more is claimed. O_EXCL serializes writers only against the SAME store
instance -- two local roots on two hosts are two stores. And the probe treats an
unreadable generation as the end of the chain because the transport cannot
distinguish absent from unreadable; that conflation is declared with a rung and
a trigger rather than resolved by parsing an error string.
Not opened for merge: no production consumer exists yet. The broker cut is what
consumes it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Selection decides which cell, the store decides whether we get it -- and the offer names the cell
The first production consumer of three authorities that were each complete and
unconsumed: product.fabric.selection ranked nothing for anyone, the floor's
demand-side dispatch had only witness rows behind it, and the file-backed
compare-and-set had no caller at all. The value is not new vocabulary -- this
invents none -- it is that those three stop being furniture.
THE INVARIANT, and the reason the two steps are in this order: SELECTION IS A
DECISION, NOT A CLAIM. Two brokers ranking one roster reach the SAME answer, so
selection alone hands one cell to both. The compare-and-set is what makes the
reservation exclusive, and the store rather than a lock decides, so it holds
across hosts. No committed compare-and-set, no reservation.
THE ARROW, which is the part that changed after review. The first cut took the
slot as a parameter BESIDE the selection, so a caller could reserve srv3-06
against a decision that chose a different supplier: two true facts with the
relation between them asserted by neither, and every arm still reading as
plausible. Five hermetic rows and two live receipts were green over it, because
each tests a projection and none tests the join.
The repair is construction. FabricCellCandidate is sole_constructor and its mint
refuses unless the offer's executor is exactly the slot's canonical instance
name, so the broker now takes a roster and no slot at all, and recovers the key
from the WINNING offer. That is the same renderer's output carried through
selection rather than a second identity authority -- the property the store's
key must have. A reservation for a cell the market did not choose has no
spelling.
THE RUNG IS PATH-SCOPED AND THE MODULE SAYS SO. Structurally impossible on the
source-to-.dag acceptance path: the validator is fixed and module-owned with
zero caller freedom, so it cannot be defeated the way a caller-supplied
predicate can. UNESTABLISHED across emission -- DESIGN carries an executed
receipt that a fixed-law mint of this shape emits as a pub struct with a pub
field deriving Deserialize. A class's rung is the minimum across its paths, so
both are stated and the next-rung trigger is named.
EVIDENCE, by execution and by the filesystem rather than by return values.
Seven hermetic rows green, including the arrow's positive control and its
discriminating red (an offer executed by anyone else refuses at the mint), and
a fail-open guard asserting all four non-commit arms report the cell unheld.
Three live rows: the broker reserves the cell whose offer won, leaving exactly
srv3-06.1; a second writer expecting the same absent slot LOSES, leaving exactly
srv3-06.1 and srv3-06.2 with no third file and nothing overwritten; and an
empty roster reserves nothing, leaving the store EMPTY -- the only observation
that catches a broker fabricating a decision the market refused to make.
The probe's own refusal codes split NoCellAdmissible into nothing-offered and
everything-rejected, because one code for both hid a fixture declaring 1 thread
against the floor's required 8, which read exactly like a correct refusal.
WHAT THIS DOES NOT DO. It issues no ExecutionGrant, starts no process and
reaches no host. A reservation is the precondition for a Grant and is not one:
ExecutionGrant carries reservations that must commit atomically across ledgers,
and manufacturing one from a slot generation would fabricate the very atomicity
that record exists to guarantee.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* A capacity class the supplier cannot author: control-plane work refuses customer capacity at admission
gunbc.fabric_capacity_class_gap has recorded, unconsumed, that nothing
structurally prevents CONTROL-PLANE capacity -- the cells running our own
scheduler, reconciliation, admission and receipt work -- from being offered as
customer-executable supply. That class sat BELOW mitigatable: not a failure
being contained, an invalid state simply representable and unremarked. This is
its named next-rung trigger, and the gap carrier's own words for what it was
waiting on.
WHERE THE CLASS DOES NOT GO, AND WHY THE CARRIER'S TRIGGER TEXT IS WRONG.
That trigger reads "a capacity class on product.fabric.work Shape". Taken
literally it names the Shape RECORD -- and Shape is one type carried by BOTH
ExecutionRequirements and SupplierOffer, so a required field there is stated by
the SUPPLIER. That is ClassOnSupplierOffer, the arm the same carrier refuses two
declarations earlier, arriving through the type system with its refutation
intact: it asks the party with the least knowledge and the most incentive to say
yes to make the safety assertion. Nobody would choose it; the shared type hands
it over. The ruled rationale governs over the ruled name -- "we originate the
demand, so we hold the fact" is true of the work side and false of a type the
supply side also carries.
A SECOND, INDEPENDENT REASON Shape WAS THE WRONG CARRIER, and it is why this
was worth stopping for rather than arguing about: shape_material HAND-ENUMERATES
its inputs. A class added there would have been SILENTLY ABSENT from the material
identity, so two shapes differing only in class would share one identity -- and
the guard against exactly that, unstated_and_stated_do_not_collapse_in_the_material,
varies the ENVELOPE and would have stayed green over it.
THAT TRAP FOLLOWED THE FIELD TO ITS NEW HOME. work_identity_material
hand-enumerates too, and reads all four requirements fields by hand today. Its
own annotation records isolation having been omitted and repaired "ONE FIELD
LATER". This is the third field. capacity_class is added to that material, and
the row proving it -- two demands alike but for their class must not share an
identity -- is authored to vary THE CLASS, because the existing collapse guard
varies the envelope and cannot fail on this. Verified by execution in both
directions: removing the field from the material turns that row FALSE while the
identical-demands control stays TRUE.
The hand-enumeration itself is NOT repaired here. Deriving materials from the
record is the right fix and changes every material identity in the fabric -- a
content-hash event, not a field addition -- and bundling it inside a safety cut
would have a reviewer approve one change while receiving two.
WHAT AN EXECUTOR IS SANCTIONED FOR IS OUR FACT. ExecutionRequirements says what
work REQUIRES; gunbc.fabric_executor_class says what an executor may serve, and
it is a fleet-side roster we author about machines we own or rent. The supplier
is never asked. That follows the precedent already in product.supplier.ubicloud,
which refuses to name an isolation profile from a published price list -- and a
class invented from a catalog would be worse than an invented profile, because a
broker reading it would ROUTE ACROSS A SAFETY BOUNDARY rather than mis-rank.
Our own cells are control-plane BY CONSTRUCTION rather than by a roster row
someone must remember to add: a RunnerSlotIdentity cannot name anything but a
cell in our build fleet, so fleet_cell_sanction derives the sanction from the
identity. An UNCLASSIFIED executor REFUSES rather than defaulting -- "we have
not classified this" and "this serves customers" are different states with
different remedies, and a default would let the roster grow a sanction nobody
authored.
ADMISSION RUNS BEFORE FUNGIBILITY, and the order is the safety property. Once
two offers are fungible they are interchangeable by definition, so a class
boundary checked after ranking is a boundary already crossed. The broker filters
the roster first, so an unsanctioned cell is never a candidate and cannot be
reached by a tie-break, a price, or a later change to the ranking.
EVIDENCE: eight hermetic rows green, both walls asserted in both directions
(control-plane work refused on customer capacity AND customer work refused on
our cells), each with the positive control that stops it being satisfied by an
admission that refuses everything. The e2e broker probe still reserves the cell
whose offer won, leaving exactly srv3-06.1. Re-verified on a compiler rebuilt
from this HEAD after finding the previous binary was 87 commits stale.
CapacityAdmission and CapacityAdmitted collided with gunbc.fleet_capacity_control,
which answers a different question -- whether a HOST is active by provider. Names
are corpus-global and a duplicate refuses whole-corpus while every entry-scoped
witness passes, so the collision was found by sweep rather than by the eight
green rows. Renamed to CapacityClassAdmission / CapacityClassAdmitted.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The partial commit has no constructor: an atomic two-ledger reservation, because purity makes the join free
ExecutionGrant carries resource_reservations and money_reservation, and its own
annotation states the invariant: "resource admitted with money refused must
commit no resource reservation, and money admitted with resource refused must
commit no money reservation; both are one canonical state transition. A partial
commit is the state that leaks capacity or budget with no grant to account for
it, and it is unreachable only if the join is atomic rather than sequential."
That join did not exist. This is it.
ATOMICITY IS NOT A PROTOCOL HERE, AND THAT IS THE WHOLE DESIGN. Two-phase
commit, compensating release, an undo log -- every one of those makes the
partial state REACHABLE and then works to escape it, which is validation
standing where construction was available. These ledgers are PURE: reserving
returns a new ledger rather than mutating one. So the join simply declines to
produce a pair unless both sides advanced, and the partial commit has no
constructor. Nothing unwinds because nothing was ever applied. On a money
refusal the advanced resource ledger is computed and goes out of scope -- in a
mutating design that branch is the leak.
GENERIC OVER BOTH QUANTITIES, WHICH IS WHY THIS CUT IS SMALL. EncumbranceLedger
<Q, S> in extdeps.accounting.encumbrance is already the cited authority for
holding a commitment against an appropriation, and product.fabric.budget is one
instantiation of it for money -- complete, with lease generation fencing, and
consumed by nothing but its own witness. A resource ledger is a SECOND
INSTANTIATION, not a second authority, so this join names no quantity at all.
Inventing a resource-specific ledger beside the generic would be the
re-invention DESIGN calls a failed decomposition.
An earlier note of mine said this was blocked on "two ledgers that do not
exist". That was wrong and is corrected here: the generic authority and the
money instantiation both exist. `ReservationRef` being a branded string is true;
"therefore nothing holds anything" was an inference past a verified fact, and
budget.dag holds and fences things today.
ONE REFERENCE KEYS BOTH SIDES, and that is load-bearing rather than tidy. The
encumbrance authority refuses a duplicate reference, and its own note explains
why: first-match resolution and rewrite-all-matches are the same operation only
while a reference is unique.
THE REFUSAL ARMS CARRY NO LEDGER AT ALL, so a caller cannot mistake a refusal
for a no-op advance and persist it. That is the reachable form of the leak in a
pure design: a caller writes back whatever joint_reservation_ledgers returns, so
an arm that carried the advanced pair would be committed to storage by a caller
doing exactly the right thing.
EVIDENCE, INCLUDING A RED THAT ACTUALLY FIRES. Six rows green, both refusal
directions asserted separately because the arms are separate code. Verified by
execution in both directions: with the money-refusal branch changed to commit
the resource side -- the partial commit itself -- the guard returns FALSE while
the positive control stays TRUE.
A FIRST DRAFT OF THAT GUARD WAS A DECORATION AND IS RECORDED HERE BECAUSE IT
ALMOST SHIPPED. It asserted that the caller's own ledger was unchanged after a
refusal. The ledgers are pure values, so that assertion CANNOT FAIL whatever the
join does -- permanently green by construction, and worse than absent because it
would have been cited as the guard against precisely the leak it could not
detect. The replacement asserts what is authorable: a refusal yields nothing to
persist.
WHAT THIS DOES NOT DO. It mints no ReservationRef and issues no ExecutionGrant.
Binding the held pair to a minted reference, and requiring ExecutionGrant to
carry held reservations rather than branded strings, is the following cut -- and
it is now executable rather than blocked, which the previous frontier was not.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The intermediate reservation had no reason to exist: the broker holds both ledgers itself
HEAD landed product.fabric.joint_reservation as a standalone module that took two
pure ledgers and returned a joined outcome. Nothing else was ever going to call
it. The only caller it could have -- the broker in gunbc.fabric_control_plane --
already holds the demand, the offer, the selection cost and the store slot, so
routing them out to a module that knows none of those and back again is a second
representation of one decision (§2). It is deleted at the root rather than
refined from the leaves (§3, delete-first), and what replaces it is the broker
making the reservation directly.
WHAT SURVIVES IS THE GUARANTEE, NOT THE MODULE. CellReservation gains a
BudgetRefused arm and CellReserved gains the advanced account, and that pairing
is the whole safety argument: no arm carries an account without a cell, and no
arm carries a cell without an account. The partial commit -- an encumbrance with
nothing running, or a running cell nobody is paying for -- has no constructor, so
it is unwritable rather than checked (§4b, structurally impossible).
THE ORDERING CLAIM WAS WITHDRAWN, AND THE RECEIPT IS WHY. A witness asserting
"the budget refuses before the store is touched" was authored, went green, and
STAYED GREEN under a mutation moving the compare-and-set ahead of the
encumbrance. The substrate is lazy: the branch that is not returned is never
forced, so both spellings are equally effect-free and the row discriminated
nothing -- a decoration cited as coverage. It is replaced by rows that assert
what the carrier actually guarantees.
THREE ROWS, EACH EXCLUDING WHAT THE OTHERS ADMIT. A ceiling below the liability
refuses with a ledger cause. An offer quoted in a currency the account does not
hold refuses on the OTHER axis, which is what excludes a broker that returns
BudgetRefused unconditionally -- and it is only authorable because the currency
presented to the budget comes from the offer rather than from the account, which
would have made the check green by construction. A ceiling of 999 against a
liability of 1000 refuses only if the FULL selection cost was presented, so a
broker encumbering the marginal charge alone goes red where the other two stay
green.
Compile: 0 blocking over both entries. All five rows verified returning true by
execution, not by typecheck.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The annotation said the refusals were counted and nothing counted them
Review 57180 (codex/gpt-5.6-sol, REQUEST_CHANGES) flagged two Boolean predicates
over substrate coproducts and cited a predicate-dissolution rule in DESIGN.md.
THAT RULE IS NOT IN DESIGN.md. It lives in docs/plans/nat-grounding-unification-
design.md and it is narrower than cited: a manual match is forbidden WHERE A
CANONICAL FOLD ALREADY EXISTS, which is why is_zero must become nat_cata.
Neither CapacityClassAdmission nor CellReservation has a catamorphism, so the
rule as stated does not reach either site.
Following it to the code found two real defects underneath it, and both are
worse than the thing that was reported.
THE ROSTER WAS SILENTLY NARROWED WHILE THE ANNOTATION CLAIMED OTHERWISE.
admitted_cell_roster kept the admitted through the Bool; refused_cell_admissions
collected the refused and HAD NO CALLER. So a demand refused entirely on the
capacity-class safety line and a demand nobody offered anything for arrived as
one symbol, and their remedies are opposite: offer more capacity, versus stop
asking for capacity you are not sanctioned to use. The prose above them read
"the refusals are COUNTED rather than silently filtered". Nothing counted them.
That is the empty-observation narrow with a sentence standing where the
mechanism was supposed to be.
Two folds re-running one judgement could also only agree by convention -- an
edit to either could put a candidate in neither half or in both, undetected. One
partition_cell_roster now makes the decision once and returns both halves, so
they cannot disagree, and NoCellAdmissible carries the refused population so the
two states are distinguishable by the caller. The Bool dies with its only
production caller.
THE OTHER PREDICATE HAD NO PRODUCTION CONSUMER AT ALL. cell_reservation_is_held
was called only by the two witness rows that existed to cover it -- an artifact
whose only consumer is its own test. Deleted. What replaces it exercises the
partition through the real broker: a refused executor is reported, an empty
roster reports none, and the pair excludes a broker that always reports a
refusal.
AND THE FOUR CAPACITY ROWS WERE ASSERTING THROUGH A COLLAPSE THEY THEMSELVES
DECLARED ILLEGAL. The Bool answered false for both a refused class and an
unclassified executor, while the unclassified row's own annotation said those
two states have different remedies and must not be collapsed. The row could not
see the distinction it was about. Each now names its arm, and the substitution
is executed rather than asserted: swapping the unclassified row's selector to
the other refusal arm returns false, which is the red the old Bool could not
produce.
Compile: 0 blocking. Eight rows verified returning true by execution, plus the
one mutation returning false.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The reservation had no way to end: the release half, and the slot finally says who holds it
The broker minted reservations and nothing ever ended them. product.fabric.budget
has had settle_money and release_money since it landed, fenced on the lease
generation; product.fabric.arbitration models the DECISION as ReleaseDirective
and says in its own header that the fabric releases nothing there. What was
missing was the actuator. Measured before starting: release_money and
settle_money had witness callers and ZERO production consumers.
THE SLOT PAYLOAD WAS WRITE-ONLY AND RELEASE IS ITS FIRST READER. That is the
part of this change that is not plumbing. The broker wrote the reservation into
the slot and nothing ever read it back, so the question release has to ask -- IS
THIS CELL HELD, AND BY WHICH RESERVATION -- had no answer. Without one, release
is a blind write: it frees whatever is in the slot on the strength of a
generation the CALLER supplied, which is a second account of who holds the cell
and free to disagree with the store.
The generation fence does not close that. It establishes the slot has not MOVED
since it was observed, which is a different question from whether it is held and
by whom. A slot already free at generation N admits a release presenting N, and
that is not a harmless no-op: it writes free over free, so a re-reservation
racing the second release finds its precondition broken by the release of a hold
that never existed.
So CellSlotState is typed, CellHeld carries the reservation reference itself
rather than re-rendering the demand and offer into a second spelling of an
identity that already exists, and the decode REFUSES an unrecognised payload
rather than answering either state.
THE PARTIAL RELEASE HAS NO CONSTRUCTOR, and it leaks the opposite way to the
reservation's: freeing the cell while the encumbrance stands bills a customer
for an idle machine, and releasing the money while the cell stays held strands
capacity under work nothing requires. Same construction argument as the reserve
half -- the money transition is pure, the slot write is the only effect, and no
arm of CellRelease carries one without the other.
AND THE FUNCTION WAS UNREACHABLE UNTIL THE LAST COMMIT OF THIS CHANGE, WHICH THE
WITNESSES COULD NOT HAVE TOLD ME. release_reserved_cell takes a
CasSlotObservation, and that type had no production producer anywhere: the file
store answers CasSlotProbe and file_compare_and_set converts internally without
ever building an observation. So the release path was callable only from
hand-built values, and my own witnesses were authoring the exact input the store
is supposed to supply -- an artifact with no final consumer, hidden by its own
tests. Found by writing the live probe row, not by the witnesses.
The repair is one observation surface in the store, observe_cas_slot_state, plus
release_reserved_cell_at beside the pure decision. It deliberately does not
delegate the bound arm to cas_probe_as_readable: that projection answers
CasReadableAbsent for a slot past the probe bound, which is right for reporting
a lost race and wrong for a decision caller, who would read "the cell is empty"
from a store that could not tell it anything and pick the remedy for an empty
cell instead of repairing the slot. file_compare_and_set is left alone -- it
produces outcomes rather than observations, so there is no second producer, and
restructuring it would rewrite a load-bearing function whose header narrates a
previously-fixed write-decides bug for no gain to it.
Seven witness rows, every one green by execution, and the holder wall carries an
executed RED: disabling the comparison returns false. Compile 0 blocking across
the witness and probe entries.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The two tags were the same length and the decode was quietly relying on it
Review 57256 (APPROVE, non-blocking) noticed that decode_cell_slot_payload
computed the body ONCE against the length of the held tag and reused it for the
free arm, which is correct only because both tags happen to be five characters.
The note is right and the coupling bought nothing, so it is removed rather than
documented.
WHY IT WAS WORTH A COMMIT RATHER THAN A REPLY. The failure it sets up is silent
and delayed: a third tag of any other length decodes to a body sliced at the
wrong offset, and every existing row stays green because the two tags that
already exist still agree. So the check that would catch it is exactly the check
nobody writes -- the round trip over a tag that does not exist yet.
The same defect had a second face the note did not name: each tag was spelled
TWICE, once rendering and once decoding, so the two spellings could drift
independently of the lengths. Both are one rule. The tags are named once and the
body is derived from the tag that MATCHED, so there is no offset to get wrong
and no second spelling to disagree.
PROVEN BY EXECUTION RATHER THAN BY INSPECTION, because "now it is decoupled" is
the kind of claim that reads as obviously true and is worth one run: with
cell_free_tag temporarily changed from "free|" to "released|" -- five characters
to nine -- both_slot_states_survive_the_round_trip still returns true. Under the
previous form that substitution sliced the free body at offset 5 and would have
failed. Tag restored, compile 0 blocking.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* compute fabric design (#9604)
* Six unresolvable names in the v2 root's emitted Rust: qualify the cross-module calls and use the declared list_length (#9547)
The v2 compiler root emits cleanly -- 0 blocking, 2083 advisory, 175 files --
and the emitted crate does not compile. Measured on 00b242b81a1 with
`gunbc compile --entry src/v2/compiler/00_compile.dag --target rust`, then
cargo over the emitted tree with its own emitted Cargo.toml: 20 rustc errors.
Six of them are source defects in this repository's own .dag, not emitter
defects and not self-host work, and this commit is those six.
THREE ARE NAMES USED WITH NEITHER AN IMPORT NOR A QUALIFICATION.
`decl_facts` is declared in v2.std.decl_index and used bare in two modules;
`PartialFunction` is declared in std.algebra and used bare in a type position.
The interpreter resolves them, so nothing refused; the emitter reports them as
`unlisted import use` advisories and emits the bare name, which is E0425. The
repair follows the idiom already on one of the two lines -- grammar_coverage.dag
declares no imports at all and qualifies every other cross-module reference
inline -- so these are qualified rather than imported. inferred_tree.dag already
carries five imports, so PartialFunction is added to that list.
THREE ARE A FREE-FUNCTION SPELLING OF A METHOD. `length(xs:)` has no declaration
anywhere in .dag; `length` is a MethodDeclaration in dag/std/methods.dag that the
interpreter intercepts. The corpus spells this `.length(` at 804 sites and
`list_length(` at 306; only reference_deps used the free form. Repointed at
std.types.list_length, whose declared parameter is `items`, not `xs`.
MEASURED, EACH ROUND A FULL RE-EMIT AND A FULL CARGO BUILD OF THE EMITTED TREE:
20 -> 17 after the three qualifications, 17 -> 14 after the three list_length
sites. Exactly the fixed errors disappeared both times and NOTHING WAS UNMASKED
behind them. That is worth stating because it is the outcome the masking
argument says not to assume: rustc stops after name resolution, so every count
here is a lower bound on a fully-resolving crate, and 20 -> 17 -> 14 establishes
only that no masking occurred AT THIS LAYER, never that none exists.
WHAT IS DELIBERATELY NOT IN THIS COMMIT, because none of it is a source defect:
five host builtins with no .dag body (layer_import_facts and the four
*_resolution_facts), four errors from Filesystem.Read emitting `.await?` against
an unbound handle in a sync fn, three emitter type-argument defects, one
unclassified E0391 variance cycle, and two deliberate compile_error!
sentinels that 05_emit_rust.dag emits instead of fabricating a default.
No Rust touched. No roster edited. No policy changed.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares (#9560)
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into `compile_dag_rust_emit_check` and not into its census
sibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a45e) the floor refuses
with `completed_over_cost_requirement=1` and `failed=0`:
`test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_
and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run
carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any
row of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both `green_named_authority_source` and
`green_own_declaration_source`, each of which a later claim then reads free.
Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and `run_claim_measured` performs the same split it already performs.
Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows
have never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Name the forcing class that decides warm-versus-net, and name the third state as the one that must not exist
The bracket in the previous commit fixes ONE instance. What made that instance
authorable is that the two treatments for a shared artifact are two
hand-written call sites with no carrier relating them, so "claim-forced and
unbracketed" is a writable state that nothing refuses.
THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED.
Preparation-forceable -- every identity it can be asked for is knowable before
the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index`
is this arm, and the run reports `provenance=built-by-preparation` for both
index identities the floor's resolves can reach. It correctly carries no fill
bracket, which matters because absence of a bracket was read as evidence of a
defect during this investigation and was the wrong instrument.
Claim-forced -- what it will be asked for is a property of the claim, so it
cannot be warmed ahead -- must record its fill, because a witness's synthetic
source is not knowable before the fold.
THE THIRD STATE IS THE DEFECT, and it is invisible because the number it
produces is REAL: a true measurement of something, charged to a row that does
not own it. Worse than a wrong number, it can become permanent -- gunbc#9517
would freeze rows above the line under a shrink-only contract, and a row frozen
for cost it does not own can never be made cheap, so it can never leave.
PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review
diligence; the third state stays writable and this paragraph will not stop the
next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing
class and the warm-or-net treatment is DERIVED from it, at which point the
third state has no spelling. That construction is not made here and is not
claimed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Two 04_infer rows carried counts that had rotted — name the instrument, and stop restating the superseded figures as history (#9462)
* 04_infer: the traversal-idiom count rotted to 16 while the tree carried 29 -- name the instrument
explicit_return_conformance_note argued that collect_explicit_return_values is not a new
shape but the seed's ordinary traversal idiom, and grounded that on a transcribed count:
"16 such sites on origin/main" across seven named modules.
Measured, both on origin/main and on this branch: 29 sites across EIGHT modules.
04_emit_info 1 · 04_sigs 1 · 04_infer 5 · 05_emit 3 · 05_emit_rust 8
compile 1 · complexity 6 · trait_derive_emit 4
trait_derive_emit was absent from the note's list entirely, so the clause was wrong about
the population's membership and not only its size.
NOTHING EDITED THE NOTE. The tree moved underneath it, which is precisely the decay mode
DESIGN §3 gives for a positional citation -- it rots without anyone touching either end --
and it is what the 2026-08-24 ruling forbids by name: cite the instrument, never transcribe
its output. The recipe is one grep and it is now stated instead of its result.
THE ARGUMENT NEVER NEEDED THE NUMBER, which is the part worth keeping. What makes this the
seed's idiom rather than a new shape is that EVERY such collector recurses itself, and that
holds at 16, at 29, and at whatever it measures next. A clause whose force depends on a
figure it cannot keep current was overstating its own evidence -- the number was doing
rhetorical work, not logical work.
Two derived ordinals went with it. "the 17th instance of a 16-instance idiom" and
"collect_explicit_return_values is the 17th ... the 18th" were positions in the disproven
count, so they were already false; they now read as further instances with no ordinal. An
ordinal is a transcribed measurement wearing the costume of a structural fact, and it is
worse than the raw count because it does not look like a measurement at all.
Prose-only, in one data row. No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Regenerate the stage0 mirrors, and delete the dead child_type_at accessor
REGEN. The prose change in 04_infer edits two `data ...: String` rows. Those are program
data, not annotations, so they emit into the stage0 Rust mirror, and CI's build lane
refused with:
required-regen: FAIL generated surface drift: v1_compiler_infer.rs
Regenerated through the sanctioned producer -- `claim_executor --required-regen
--source-root dag --source-root src/v2` -- rather than hand-edited. A hand-authored mirror
is exactly what that gate exists to refuse, and its only reachable green would have been
the forbidden action.
EVERY CHANGED LINE IS ACCOUNTED FOR, because a regen can also delete orphan content a
committed projection carries that no authority produces:
v1_compiler_infer.rs 2 lines the two data rows edited in the parent commit
v1_compiler_infer_types.rs 14 lines deleted: the child_type_at body
Nothing else moved. Re-running regen against the installed mirrors reports
first_generation_equal=true. (declared_divergent=1 [main.rs] is pre-existing; it is present
in the failing run on the parent commit too.)
DEAD ACCESSOR. v1.04_types child_type_at had ZERO callers -- measured across the whole
corpus, not just .dag: one definition in 04_types.dag, one in the generated mirror, no
consumers, no re-export, no prose reference.
It is deleted rather than left because of where it sits. It is a decoy beside
child_type_node, the live accessor that discriminates a type child from a field child by
whether `inferred` is populated -- a fabricated provenance stamp the parser writes at parse
time. Anyone repairing that discrimination reads both functions and has to work out which
one matters. Approved by compiler direction as needing no ruling.
WHY THIS WIDENS AN ALREADY-APPROVED PR, stated because the usual answer is that it should
not. #9462 was red and required a regen commit regardless, so the approval resets either
way and the deletion rides along at zero marginal cost -- and it keeps this to ONE regen
cycle rather than two. Without that, the correct call would have been a separate PR.
No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The sibling row carried the SAME disproven count -- one sentence fixed, the claim left standing
FOUND FROM OUTSIDE, NOT BY ME. The first commit repaired explicit_return_conformance_note and
left seed_node_traversal_frontier asserting the identical thing a few lines above it:
"the idiom is 16 self-recursive `children |> flat_map` sites on origin/main across
04_emit_info, 04_sigs, 04_infer, 05_emit, 05_emit_rust, compile and complexity"
Same 16, same seven-module list, same two errors -- the tree measures 29 across EIGHT, with
trait_derive_emit absent from the list entirely. I edited a SENTENCE when the defect was a
CLAIM, which is the document-wide-correction failure, committed inside the change whose whole
subject is a rotted figure.
THE SECOND COUNT IN THAT ROW GOES TOO, AND THE REASONING IS THE INTERESTING PART. It carried
"579 direct Node-storage field reads in 04_infer alone". A plausible reconstruction -- counting
`.children`, `.params`, `.inferred` and their siblings -- returns roughly TWICE that. That
establishes the number is STALE without establishing what the right one is, because I cannot
recover the recipe its author used.
So the repair is DELETION, not an update. Replacing a stale figure with one my own instrument
produced would swap an uncheckable number for a checkable-LOOKING wrong one, which is worse:
the first is visibly unverifiable, the second gets cited as verified. The site population is
named by its instrument (grep the idiom under src/v1); the field-read population has no agreed
instrument and is stated as a SHAPE rather than a count.
That asymmetry is why the earlier commit deliberately left this figure alone, and why leaving
it was still wrong -- declining to invent a recipe was right, declining to remove the number
was not.
Mirror regenerated through claim_executor --required-regen. One line in v1_compiler_infer.rs,
which is the row above. Prose only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The counts were deleted as CLAIMS and kept as HISTORY -- which is the same decay inside the sentence announcing its removal
Found in review, not by me, and it is the sharper half of this PR.
The previous commits removed the rotted figures from both 04_infer rows as ASSERTIONS and then
restated them as provenance: "it read 16 sites across seven modules while the tree measures 29
across eight". That is still a number in a live `data … : String` authority. It rots the same
way the original did, nothing re-derives it, and it gets quoted back as though this row had
measured it -- so the row announcing that it no longer transcribes an instrument's output was
transcribing one in the same breath.
BOTH ROWS NOW CARRY ZERO FIGURES, verified mechanically rather than by reading:
grep '^data explicit_return_conformance_note' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
grep '^data seed_node_traversal_frontier' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
The before-and-after lives in the PR, which is the artifact that is allowed to carry a
superseded measurement, because it is dated and nobody consumes it as current authority.
A SECOND, INDEPENDENT PREDICATE DEFECT, also named in review. Both rows pointed at a LEXICAL
instrument (grep `children |> flat_map`) while asserting SEMANTIC properties -- self-recursive,
and the seed's ONLY traversal idiom. A grep bounds the literal-occurrence population and cannot
establish recursion or exhaustiveness. Naming an instrument does not fix a claim if the
instrument answers a different question, which is the same right-number-wrong-subject failure the
counts themselves were. Both rows now say so: the grep bounds the literal population, and the
recursion property is read off the sites rather than off the count.
WHY DELETION AND NOT AN UPDATE, restated because it is the part a reader will want to argue with:
one row's field-read count has no reproducible recipe and a plausible reconstruction disagrees by
a wide margin. That establishes STALE without establishing CORRECT. Substituting a figure from my
own instrument would swap an uncheckable number for a checkable-LOOKING wrong one -- worse,
because the first is visibly unverifiable and the second gets cited as verified. That population
is stated as a shape.
Mirror regenerated through claim_executor --required-regen and applied from the candidate rather
than hand-edited; the diff is exactly the two rows, 4 lines, no other drift.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Restore the mirror the merge resolution dropped: --theirs took main's bytes, which never carried the prose fix
THE MERGE CONFLICT WAS IN A GENERATED FILE and I resolved it with --theirs to complete the merge,
intending to regenerate immediately. That resolution takes MAIN's mirror, which by construction
does not contain this branch's edits -- so for one commit the authority (04_infer.dag) carried the
repaired prose and its mirror carried main's older text. A regen fixed-point check is exactly what
catches that, and it did:
changed lines: 4, in the two rows this branch edits, nothing else
Mirror re-derived from the MERGED authority through claim_executor --required-regen and applied
from the candidate rather than hand-edited.
WHY THIS IS WORTH A COMMIT MESSAGE RATHER THAN A SILENT FIXUP: picking a side of a conflict in a
generated file is never a resolution, it is a coin flip between two stale artifacts. The authority
merged cleanly on its own -- the mirror had no business being adjudicated at all, and the only
correct answer was to recompute it. Taking --ours would have been equally wrong in the other
direction, dropping main's edits to the same file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* An escalation is not an infrastructure loss: give ExecutionAttemptLineage the arm the resident-model thesis is measured on (#9546)
A local model that reaches a terminal result it cannot carry, followed by a
more capable model taking the next try, is the single observation the
"progressively smaller models suffice" claim is denominated in. Measured on
this tree, nothing could express it: grep for Episode/continuation/retry_of/
predecessor across dag/gunbc, dag/std and src/v2 returns nothing episode-shaped,
and ExecutionAttemptLineage's three arms are InitialAttempt, InfrastructureRetry
and RequestedReexecution. So an escalation had to be recorded as either an
infrastructure retry -- which says the work told us nothing -- or as an
unrelated initial attempt, which discards the edge entirely.
CapabilityEscalation is a sibling of InfrastructureRetry rather than an arm of
one generic Retry, because the two differ in exactly what lineage exists to
record: an infrastructure loss says nothing about the work, while an escalation
says the work exceeded the capability that was tried. Like its sibling it names
the prior attempt AND the receipt that established the prior result, so merely
resolving a more expensive model after a cheaper one is a selection fact rather
than an escalation.
The two arms are deliberately the same SHAPE, which is what the third witness is
for: a control checking only the prior-attempt key would pass identically
against a lineage that had collapsed them, so the discriminating assertion
matches on the arm and fails if an escalation ever reads as a retry or the
reverse.
WHAT IS NOT VERIFIED, stated because a green I cannot stand behind is worse than
no green. `gunbc compile` takes no --entry, and the whole-corpus run over this
tree reports 31139 diagnostics ON PRISTINE MAIN, 1283 of them "expected item
declaration" on `//` annotation lines -- so that CLI path does not route source
annotations the way the required parse phase does, and cannot adjudicate this
tree. My attempted discriminating RED (deleting one arm from an exhaustive
match) returned 31139, byte-identical to the pristine baseline: it added zero
errors and therefore discriminated nothing. An earlier local run appeared clean
only because it was killed at its timeout mid-typecheck and the truncated output
rendered identically to a completed clean one. CI is the check here.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) (#9527)
* A typed wall for barren witness files exists, is wired to a hard failure, and the required floor never calls it: 62 unenrolled claims, the third scanner, and 37 promotions
The brief was 62 claims declared plain `fn` and never enrolled. Chasing why produced a
larger finding than the population: `v2.workflow.floor_naming_hygiene`
`floor_entry_is_barren_test_sidecar` has refused this exact class since it was written,
`floor_discovery_finalize` turns it into `FloorDiscoveryRefused`, and the host returns that
as `Err`. It stops the line. It has never been on the line.
MEASURED, not inferred: main run 33092582255 (headSha 107304a579), both lanes green, four
barren `*_test.dag` entries present at that sha, and zero occurrences of `barren` or
`sidecar` in the 693,975-byte run log.
WHY: `run_required_floor` builds its roster from `prepared.witness_files`, produced by
`witness_file_from_source`, which answers `None` for a file with no `test fn` — and the
caller discarded that answer. The walled `.dag` producer is reachable only through
`discover_floor_witness_roster`, which the required floor never calls. Three scanners for
one fact live in one binary and the wall guards the one production retired. The Rust test
asserting the wiring is not the missing piece: it still PASSES, because the wiring is
intact on the producer path — a green local `cargo test` says nothing about the required
path.
WHAT LANDED: preparation records the discarded fact; the floor asks
`floor_naming_hygiene`'s own `floor_test_sidecar_suffix` which recorded paths are
`*_test.dag` and refuses `cause=BarrenTestSidecar`. The rule keeps one home; only its
consumer moved. The recorded set uses the RULE's vocabulary — neither `test fn` nor
`test data` — so the 13 test-data-only files are not over-refused. The floor's summary line
is bounded above rather than left exact-and-silent. 37 leaf claims promoted, 37/37 PASS,
and the 4 sibling-conjunction aggregates deleted: each was a hand-rolled substitute for
enrolment with exactly one occurrence in the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
* Consume the modeled sidecar predicates instead of re-spelling them in Rust: delete the forked suffix test and the added test-decl scan
review 56971 requested changes on #9499 and was right on both counts; #9499 merged before
the rework landed, so main currently carries the fork and this is the repair.
FINDING 2, the reimplemented predicate. `floor_barren_test_sidecars` read
`floor_test_sidecar_suffix` from the `.dag` and then applied `strip_prefix("./")` and
`ends_with` in Rust. Reading the constant does not make the computation derived from the
authority — the two can drift independently. It now INVOKES the modeled predicates and
decides nothing itself. My own framing ("policy stays home, only the consumer moves") was
the error: I moved the CONSTANT home and left the COMPUTATION forked.
FINDING 1, the added test-declaration scan. The `!line.starts_with("test data ")` check is
DELETED. It existed to stop the wall over-refusing the 13 test-data-only files, which is
exactly what `floor_discovery_scan_test_decl_names` already does inside
`floor_entry_is_barren_test_sidecar`.
THE SHAPE, and why it costs one call rather than one per corpus file — which is what pushed
me into the fork to begin with. Preparation records a CANDIDATE SET, not a verdict: every
source `witness_file_from_source` declined, asking nothing about suffixes and nothing about
`test data`. `floor_entries_requiring_test_sidecar` (new, in `v2.workflow.floor_naming_hygiene`,
composing the existing `floor_entry_requires_test_sidecar`) is then asked ONCE for the whole
roster — a pure string question, one crossing — and `floor_entry_is_barren_test_sidecar` is
asked per survivor with that file's content, typically zero or a handful of invocations.
THE CANDIDATE SET IS DELIBERATELY OVER-INCLUSIVE AND THAT IS WHAT MAKES IT SOUND: a
test-data-only file lands in it and the `.dag` answers NOT barren, because its own scan counts
`test data` as a test decl. Rust can only widen the question, never decide it, so a
Rust/`.dag` disagreement cannot produce a wrong refusal — only a candidate the authority
discards. A missing candidate source is a typed refusal rather than a skip (§5).
RE-VERIFIED BY EXECUTION, because changing the mechanism invalidates the evidence for it.
Same binary, corpora identical except `filesystem_read_outcome_witness_test.dag`:
RED refuses `cause=BarrenTestSidecar count=1` naming it; GREEN completes site-projection
(sites=13351 files=1697 claims=11910). The first re-run attempt failed loudly with
`no declaration named 'v2.workflow.floor_naming_hygiene.floor_entries_requiring_test_sidecar'`
because the control trees came from HEAD while the new `.dag` function was still uncommitted
— a binary/corpus mismatch the control caught rather than one that shipped.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
---------
Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Delete the floor's stale live-tree decline (#9106)
* Delete the floor's stale live-tree decline
* Enroll surfaced required-floor dispositions
* Retire executing witnesses from deferral freeze
* Retire routed witnesses from deferral freeze
* Retire merged route gaps from deferral freeze
* Enroll post-merge shell route gaps
* Enroll activated semantic reds
* Place expected-red provenance at module grain
* Enroll newly exposed parser-drop route gap
* Adjudicate live-tree cut witness fallout
* Keep quarantine disposition annotation at module grain
* Fix expected-red chunk merge boundary
* Declare the live-tree census debt
* Retire five executing freeze rows
* Retire two supplied route gaps
* Bind exposed floor debt to repair lanes
* Retire stale live-tree decline prose
* Close route-gap lists after stale-row retirement
* Retire repaired expected-red rows
* Classify realization floor non-verdict
* Compose discovery census with live-tree cut
* Declare the exposed gitattributes drift
* Bind the accumulator analysis explicitly
* Preserve new diagnostic histogram arms
* Update floor projection annotation
* Close floor cut review obligations
* Remove stale retained-parameter annotation
* Correct live-tree cutover annotations
* Retire repaired live-tree census stalls
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences (#9447)
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences
The producer (#9439) correctly refused the binding envelope: its denominator is
the candidates that reached the decision, produced by the same pass that decides
them. This lands the envelope with a denominator that is not that.
The open question -- does every emit-time repair candidate correspond to a
parse-time reference occurrence -- is answered NO, in three independent
directions at once: the roster is deduplicated by SPELLING before any decision
(grain), it admits names merely for appearing as an identifier in the EMITTED
Rust (superset -- nothing authored them, so they can have no occurrence id), and
it drops occurrences the repairer correctly never touches (subset). So R_X(B) is
a PEER of O_X(B) keyed on repair sites, not an instance of it.
The completeness law is one law for any key, so it is hoisted key-generic into
std.observation_completeness and both envelopes instantiate it -- two subjects,
two denominators, one join. decl_field_label moves to std.decl_ref for the same
reason, with the third projection in std.observation named rather than tolerated.
Roster provenance is structural rather than ordered: SubjectRoster is
sole_constructor, prove_subject_roster is its only mint, and the admission takes
one -- so joining against an unproven roster has no spelling.
What this does NOT establish is stated in the carrier beside what it does: the
producer could still assemble the roster from the candidates it decided. The
tautology becomes visible and nameable rather than dissolved, which is an
improvement and not a proof; the next-rung trigger is recorded.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Restore legacy_binding_delta's own occurrences: payload, over-renamed by the hoist's blanket sed
The hoist renames the completeness arms' payload from `occurrences:` to `keys:`,
because at the repair envelope's instantiation the key is a repair site and
"occurrences" would be a lie. `{ occurrences: ... }` also spells the payload on
six unrelated ProvenanceTotality arms in legacy_binding_delta, and a blanket
rename over the witness took those with it -- 71 blocking errors, none of them in
the module the hoist was about.
Caught by compiling the blast radius rather than grepping it, which is the whole
reason it was compiled: "two witness files" is a file count, not a symbol
census, and the payload name was never the thing being renamed -- the TYPE was.
* Rename the roster carrier off a name the enforcement lens already owns, and drop the declaration move out of this change
Three CI failures, three causes.
SubjectRoster was already declared by v2.lens.enforcement.vocab for an
unrelated concept. Whole-corpus resolution handed THIS type to that lens's own
consumers and their `entries` field stopped existing -- nine diagnostics, none
of them in a module this change touches. Renamed to ProvenRepairRoster. The
shape is the finding rather than the fix: the duplicate was minted here and
every symptom surfaced elsewhere, so no compile of this closure could have
shown it, which is what makes "my closure is clean" structurally unable to
catch this class.
decl_field_label's move to std.decl_ref is reverted. It caused both the regen
drift on std_decl_ref.rs and two TargetChanged wave-admission deltas. The
declaration stays in the binding envelope and the repair envelope imports it --
one authority, no fork -- and the relocation lands as its own change where its
two rows are the whole reviewable diff.
The first cut of that annotation justified the revert by citing the wave grain
note's "two change classes in one diff" clause. That was a mis-citation: the
clause's subject is a wave that BOTH REQUALIFIES AND MOVES a symbol, and this
requalifies nothing. Corrected in place rather than dropped, because a carrier
that once stated an invented prohibition should say so.
One unused import removed (ObservationCompleteness in the observation witness).
The remaining two UnexplainedSubjectMotion deltas are a confirmed defect in the
wave-admission channel's reader, owned by another lane; its refusal is left
standing rather than cleared by an admission row, which over a channel that
cannot see the reference would be a manual override rather than an admission.
Evidence: 21/21 witness arms return true; mutating prove_repair_roster's digest
comparison to a constant turns the provenance arm false while the positive
control stays true. All three affected closures compile at 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main, and take the three obligations #9440's landing created
crisp-crab's #9440 merged first, so by the order the two lanes committed to,
this change owes the collision resolution -- and owes it HERE rather than in a
follow-up, because declaration names bind closure-globally and two declarations
of one name on main is a collision, not a shadowing. Neither author can observe
it by compiling their own branch: both were green against main independently.
The receipt is this lane's own SubjectRoster duplicate, which produced nine
diagnostics, every one in v2.lens.enforcement modules that change never touched.
Three obligations, all measured rather than assumed:
- the placeholder `type CompleteLegacyRepairObservation<R>` is deleted from
v2.workflow.legacy_baseline_capture and the real carrier imported from
v2.workflow.legacy_repair_observation. Its accepted arm LegacyBaselineCaptured
is constructible for the first time; the annotation is rewritten to record
why the deletion could not wait rather than left describing a hole that is
now filled.
- the two LegacyObservationCompleteness references the hoist renamed --
the import member and the LegacyBaselineObservationIncomplete payload --
migrated to ObservationCompleteness<Int>. crisp-crab measured their exposure
at exactly two lines and named both; both appeared where they said.
- the second type parameter survives the swap deliberately. O is what the
resolver selected per occurrence, R what the repairer decided per repair
site; one parameter would force the emitter's repair vocabulary to equal the
resolver's binding vocabulary, which is the conflation the operator ruling
forbids, committed in the parameter list instead of the fields.
NOT carried: #9440's three dead imports. The offer was withdrawn after the
coupling was priced -- they are inert, nothing waits on them, and tying someone
else's cleanup to this branch's blocker was never the cheap option.
v2.workflow.legacy_baseline_capture compiles 0 blocking after the change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main: pick up the wave-admission membership fix (#9490) and the repair-decision producer (#9439)
#9490 splits membership_declared from membership_bound_through, so an authored
import claim answers the ADD direction outright. Both UnexplainedSubjectMotion
rows this branch was refusing on carry an explicit import claim naming
std.observation_completeness, so both close without the gate having to reach a
pattern arm or an inferred-slot field type.
#9439 landed the producer this envelope was built for: reference_derived_
candidate_disposition and reference_derived_census in v1.05_emit_rust. The
correspondence finding this branch rests on was read off that pass, and it is
now on main rather than on a branch -- so the annotation citing it names a
declaration that resolves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Refuse a malformed denominator: a roster naming one site twice certified as complete (review 56949)
`std.observation_completeness` returned `ObservationComplete` for expected
`[A, A]` against observed `[A]`. Nothing missing -- A IS present, so both
expected entries filter out. Nothing foreign. Nothing repeated -- the repeat
test counts OBSERVED occurrences and there is one. So the envelope certified
exactness over a denominator that asked for one site twice.
All three refusals judged the ANSWER set. None judged the QUESTION set, and an
ill-formed question set defeats all three at once.
WHY 21 ARMS MISSED IT: every arm varied the OBSERVATION against a well-formed
roster; none varied the ROSTER. A missing AXIS, not a missing case within one --
and the module header already said completeness is a join between two sets while
every arm ex…
briansrls
added a commit
that referenced
this pull request
Aug 28, 2026
* The floor's demand and its supply selection are one join, and select_supply gets its first caller
select_supply has been complete and unconsumed since it landed. This module
is the join: the required floor's own Work becomes a Demand, and the candidate
roster is ranked by the authority that already knew how, rather than by a
second ranking written beside it.
What this does NOT do is stated in the module header rather than left to be
inferred: selecting an offer is a DECISION, not an execution. No Grant is
committed, no process starts, no host effect is reached. The invariant
fabric_witness_run builds toward -- no committed Grant, no process -- is not
established here.
Four rows, green by execution in one run: a host larger than the floor is
selected for it (positive control), a host smaller than the floor is
CONSIDERED and REFUSED rather than silently dropped (the discriminating red),
an empty roster selects nothing and considers nothing, and the floor demand
carries the authority's own satisfaction requirement rather than a copy.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* A compare-and-set whose target came from the expectation could commit against a slot that was never there
std.durable_compare_and_set has had no production realization since it landed.
This is the first, and it is the shape that module's own header asks for: the
store owns the read and the conditional write in one operation, so no caller
ever supplies a free-standing observation and the declared key-relation
boundary is closed by construction rather than observed and refused.
The mechanism is generation-suffixed slots. A slot at generation N is the file
<root>/<key>.<N>, written once and never rewritten, so both expectations reduce
to one primitive -- create-if-absent is create-new key.1, update-from-N is
create-new key.N+1 -- and create-new is O_EXCL. Exclusion is therefore performed
by the operating system on the write itself rather than by a lock the caller
holds, which is the gap the interface names: the existing exclusion is flock,
single-host by construction, and cannot serialize two writers on different
hosts. Verified on both the interpreter and the emitter paths rather than taken
from the prose note, because a rung is per-path.
THE DEFECT THIS COMMIT ALSO REPAIRS WAS MINE, FOUND BEFORE IT LANDED. The first
cut derived the target generation from the EXPECTATION and let O_EXCL decide.
That is sound for ExpectSlotAbsent and wrong for ExpectSlotGeneration, because
O_EXCL excludes competing writers for the TARGET PATH and establishes nothing
about which generation is currently the head. An attempt expecting generation 7
against an EMPTY store computed target 8, found key.8 free, won the create, and
reported a commit on a precondition that was never true.
The target is now derived from the OBSERVATION. An expectation is a claim about
the store, and deriving the write target from the claim rather than from the
store is the whole of the bug. The invariant is that the read establishes
eligibility and the exclusive write decides the winner -- reading first does not
reopen a time-of-check-to-time-of-use race, because two writers that both
observe head N both derive N+1 and exactly one create succeeds.
THE EVIDENCE IS THE FILESYSTEM, NOT A BOOLEAN. The live probe drives five
attempts and the store is left holding exactly slot-a.1 and slot-a.2. There is
no slot-a.8 and no slot-b.8, and under the old derivation both would exist --
an expectation of generation 7 is refused against a slot at generation 2 and
against a slot that does not exist at all, with no write attempted in either
case.
That probe is an entry point rather than a shell script because an ad-hoc .sh
here is unmodeled realization: if a measurement is worth re-deriving it is worth
an entry point.
TWO FURTHER DEFECTS FOUND BY BUILDING RATHER THAN BY READING. CasOutcome has
three arms and none can say the attempt's digest does not match its payload;
reporting that as a store refusal blames the store for the caller lying, so the
input is narrowed instead of the shared type widened -- a sole_constructor
verified-attempt whose only mint verifies the digest, which the interface says
is exactly the realizing store's duty and which is available here because this
realization is concrete at the type the hash function accepts. And the key is
interpolated into a path, so a key carrying a separator escaped the store root;
refused at the mint, and refusing the separator alone is sufficient because the
generation suffix is always appended so a bare dot-dot can never be a final
component.
A WITNESS WAS DELETED RATHER THAN REPAIRED. the_target_generation_is_derived_-
from_the_expectation_and_never_supplied was green, and it was green because it
pinned the defective invariant. Keeping it beside the fix would leave the corpus
asserting both the defect and its repair. Its replacement cannot be hermetic:
the corrected derivation reads the store, so every discriminating row for it
performs a host effect and belongs to the live probe.
Scope declared rather than overclaimed. sole_constructor confines construction
on the source-to-.dag path; DESIGN records by execution that an emitted mirror
is forgeable, so the mint is sufficient for the path this carrier travels and
nothing more is claimed. O_EXCL serializes writers only against the SAME store
instance -- two local roots on two hosts are two stores. And the probe treats an
unreadable generation as the end of the chain because the transport cannot
distinguish absent from unreadable; that conflation is declared with a rung and
a trigger rather than resolved by parsing an error string.
Not opened for merge: no production consumer exists yet. The broker cut is what
consumes it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Selection decides which cell, the store decides whether we get it -- and the offer names the cell
The first production consumer of three authorities that were each complete and
unconsumed: product.fabric.selection ranked nothing for anyone, the floor's
demand-side dispatch had only witness rows behind it, and the file-backed
compare-and-set had no caller at all. The value is not new vocabulary -- this
invents none -- it is that those three stop being furniture.
THE INVARIANT, and the reason the two steps are in this order: SELECTION IS A
DECISION, NOT A CLAIM. Two brokers ranking one roster reach the SAME answer, so
selection alone hands one cell to both. The compare-and-set is what makes the
reservation exclusive, and the store rather than a lock decides, so it holds
across hosts. No committed compare-and-set, no reservation.
THE ARROW, which is the part that changed after review. The first cut took the
slot as a parameter BESIDE the selection, so a caller could reserve srv3-06
against a decision that chose a different supplier: two true facts with the
relation between them asserted by neither, and every arm still reading as
plausible. Five hermetic rows and two live receipts were green over it, because
each tests a projection and none tests the join.
The repair is construction. FabricCellCandidate is sole_constructor and its mint
refuses unless the offer's executor is exactly the slot's canonical instance
name, so the broker now takes a roster and no slot at all, and recovers the key
from the WINNING offer. That is the same renderer's output carried through
selection rather than a second identity authority -- the property the store's
key must have. A reservation for a cell the market did not choose has no
spelling.
THE RUNG IS PATH-SCOPED AND THE MODULE SAYS SO. Structurally impossible on the
source-to-.dag acceptance path: the validator is fixed and module-owned with
zero caller freedom, so it cannot be defeated the way a caller-supplied
predicate can. UNESTABLISHED across emission -- DESIGN carries an executed
receipt that a fixed-law mint of this shape emits as a pub struct with a pub
field deriving Deserialize. A class's rung is the minimum across its paths, so
both are stated and the next-rung trigger is named.
EVIDENCE, by execution and by the filesystem rather than by return values.
Seven hermetic rows green, including the arrow's positive control and its
discriminating red (an offer executed by anyone else refuses at the mint), and
a fail-open guard asserting all four non-commit arms report the cell unheld.
Three live rows: the broker reserves the cell whose offer won, leaving exactly
srv3-06.1; a second writer expecting the same absent slot LOSES, leaving exactly
srv3-06.1 and srv3-06.2 with no third file and nothing overwritten; and an
empty roster reserves nothing, leaving the store EMPTY -- the only observation
that catches a broker fabricating a decision the market refused to make.
The probe's own refusal codes split NoCellAdmissible into nothing-offered and
everything-rejected, because one code for both hid a fixture declaring 1 thread
against the floor's required 8, which read exactly like a correct refusal.
WHAT THIS DOES NOT DO. It issues no ExecutionGrant, starts no process and
reaches no host. A reservation is the precondition for a Grant and is not one:
ExecutionGrant carries reservations that must commit atomically across ledgers,
and manufacturing one from a slot generation would fabricate the very atomicity
that record exists to guarantee.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* A capacity class the supplier cannot author: control-plane work refuses customer capacity at admission
gunbc.fabric_capacity_class_gap has recorded, unconsumed, that nothing
structurally prevents CONTROL-PLANE capacity -- the cells running our own
scheduler, reconciliation, admission and receipt work -- from being offered as
customer-executable supply. That class sat BELOW mitigatable: not a failure
being contained, an invalid state simply representable and unremarked. This is
its named next-rung trigger, and the gap carrier's own words for what it was
waiting on.
WHERE THE CLASS DOES NOT GO, AND WHY THE CARRIER'S TRIGGER TEXT IS WRONG.
That trigger reads "a capacity class on product.fabric.work Shape". Taken
literally it names the Shape RECORD -- and Shape is one type carried by BOTH
ExecutionRequirements and SupplierOffer, so a required field there is stated by
the SUPPLIER. That is ClassOnSupplierOffer, the arm the same carrier refuses two
declarations earlier, arriving through the type system with its refutation
intact: it asks the party with the least knowledge and the most incentive to say
yes to make the safety assertion. Nobody would choose it; the shared type hands
it over. The ruled rationale governs over the ruled name -- "we originate the
demand, so we hold the fact" is true of the work side and false of a type the
supply side also carries.
A SECOND, INDEPENDENT REASON Shape WAS THE WRONG CARRIER, and it is why this
was worth stopping for rather than arguing about: shape_material HAND-ENUMERATES
its inputs. A class added there would have been SILENTLY ABSENT from the material
identity, so two shapes differing only in class would share one identity -- and
the guard against exactly that, unstated_and_stated_do_not_collapse_in_the_material,
varies the ENVELOPE and would have stayed green over it.
THAT TRAP FOLLOWED THE FIELD TO ITS NEW HOME. work_identity_material
hand-enumerates too, and reads all four requirements fields by hand today. Its
own annotation records isolation having been omitted and repaired "ONE FIELD
LATER". This is the third field. capacity_class is added to that material, and
the row proving it -- two demands alike but for their class must not share an
identity -- is authored to vary THE CLASS, because the existing collapse guard
varies the envelope and cannot fail on this. Verified by execution in both
directions: removing the field from the material turns that row FALSE while the
identical-demands control stays TRUE.
The hand-enumeration itself is NOT repaired here. Deriving materials from the
record is the right fix and changes every material identity in the fabric -- a
content-hash event, not a field addition -- and bundling it inside a safety cut
would have a reviewer approve one change while receiving two.
WHAT AN EXECUTOR IS SANCTIONED FOR IS OUR FACT. ExecutionRequirements says what
work REQUIRES; gunbc.fabric_executor_class says what an executor may serve, and
it is a fleet-side roster we author about machines we own or rent. The supplier
is never asked. That follows the precedent already in product.supplier.ubicloud,
which refuses to name an isolation profile from a published price list -- and a
class invented from a catalog would be worse than an invented profile, because a
broker reading it would ROUTE ACROSS A SAFETY BOUNDARY rather than mis-rank.
Our own cells are control-plane BY CONSTRUCTION rather than by a roster row
someone must remember to add: a RunnerSlotIdentity cannot name anything but a
cell in our build fleet, so fleet_cell_sanction derives the sanction from the
identity. An UNCLASSIFIED executor REFUSES rather than defaulting -- "we have
not classified this" and "this serves customers" are different states with
different remedies, and a default would let the roster grow a sanction nobody
authored.
ADMISSION RUNS BEFORE FUNGIBILITY, and the order is the safety property. Once
two offers are fungible they are interchangeable by definition, so a class
boundary checked after ranking is a boundary already crossed. The broker filters
the roster first, so an unsanctioned cell is never a candidate and cannot be
reached by a tie-break, a price, or a later change to the ranking.
EVIDENCE: eight hermetic rows green, both walls asserted in both directions
(control-plane work refused on customer capacity AND customer work refused on
our cells), each with the positive control that stops it being satisfied by an
admission that refuses everything. The e2e broker probe still reserves the cell
whose offer won, leaving exactly srv3-06.1. Re-verified on a compiler rebuilt
from this HEAD after finding the previous binary was 87 commits stale.
CapacityAdmission and CapacityAdmitted collided with gunbc.fleet_capacity_control,
which answers a different question -- whether a HOST is active by provider. Names
are corpus-global and a duplicate refuses whole-corpus while every entry-scoped
witness passes, so the collision was found by sweep rather than by the eight
green rows. Renamed to CapacityClassAdmission / CapacityClassAdmitted.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The partial commit has no constructor: an atomic two-ledger reservation, because purity makes the join free
ExecutionGrant carries resource_reservations and money_reservation, and its own
annotation states the invariant: "resource admitted with money refused must
commit no resource reservation, and money admitted with resource refused must
commit no money reservation; both are one canonical state transition. A partial
commit is the state that leaks capacity or budget with no grant to account for
it, and it is unreachable only if the join is atomic rather than sequential."
That join did not exist. This is it.
ATOMICITY IS NOT A PROTOCOL HERE, AND THAT IS THE WHOLE DESIGN. Two-phase
commit, compensating release, an undo log -- every one of those makes the
partial state REACHABLE and then works to escape it, which is validation
standing where construction was available. These ledgers are PURE: reserving
returns a new ledger rather than mutating one. So the join simply declines to
produce a pair unless both sides advanced, and the partial commit has no
constructor. Nothing unwinds because nothing was ever applied. On a money
refusal the advanced resource ledger is computed and goes out of scope -- in a
mutating design that branch is the leak.
GENERIC OVER BOTH QUANTITIES, WHICH IS WHY THIS CUT IS SMALL. EncumbranceLedger
<Q, S> in extdeps.accounting.encumbrance is already the cited authority for
holding a commitment against an appropriation, and product.fabric.budget is one
instantiation of it for money -- complete, with lease generation fencing, and
consumed by nothing but its own witness. A resource ledger is a SECOND
INSTANTIATION, not a second authority, so this join names no quantity at all.
Inventing a resource-specific ledger beside the generic would be the
re-invention DESIGN calls a failed decomposition.
An earlier note of mine said this was blocked on "two ledgers that do not
exist". That was wrong and is corrected here: the generic authority and the
money instantiation both exist. `ReservationRef` being a branded string is true;
"therefore nothing holds anything" was an inference past a verified fact, and
budget.dag holds and fences things today.
ONE REFERENCE KEYS BOTH SIDES, and that is load-bearing rather than tidy. The
encumbrance authority refuses a duplicate reference, and its own note explains
why: first-match resolution and rewrite-all-matches are the same operation only
while a reference is unique.
THE REFUSAL ARMS CARRY NO LEDGER AT ALL, so a caller cannot mistake a refusal
for a no-op advance and persist it. That is the reachable form of the leak in a
pure design: a caller writes back whatever joint_reservation_ledgers returns, so
an arm that carried the advanced pair would be committed to storage by a caller
doing exactly the right thing.
EVIDENCE, INCLUDING A RED THAT ACTUALLY FIRES. Six rows green, both refusal
directions asserted separately because the arms are separate code. Verified by
execution in both directions: with the money-refusal branch changed to commit
the resource side -- the partial commit itself -- the guard returns FALSE while
the positive control stays TRUE.
A FIRST DRAFT OF THAT GUARD WAS A DECORATION AND IS RECORDED HERE BECAUSE IT
ALMOST SHIPPED. It asserted that the caller's own ledger was unchanged after a
refusal. The ledgers are pure values, so that assertion CANNOT FAIL whatever the
join does -- permanently green by construction, and worse than absent because it
would have been cited as the guard against precisely the leak it could not
detect. The replacement asserts what is authorable: a refusal yields nothing to
persist.
WHAT THIS DOES NOT DO. It mints no ReservationRef and issues no ExecutionGrant.
Binding the held pair to a minted reference, and requiring ExecutionGrant to
carry held reservations rather than branded strings, is the following cut -- and
it is now executable rather than blocked, which the previous frontier was not.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The intermediate reservation had no reason to exist: the broker holds both ledgers itself
HEAD landed product.fabric.joint_reservation as a standalone module that took two
pure ledgers and returned a joined outcome. Nothing else was ever going to call
it. The only caller it could have -- the broker in gunbc.fabric_control_plane --
already holds the demand, the offer, the selection cost and the store slot, so
routing them out to a module that knows none of those and back again is a second
representation of one decision (§2). It is deleted at the root rather than
refined from the leaves (§3, delete-first), and what replaces it is the broker
making the reservation directly.
WHAT SURVIVES IS THE GUARANTEE, NOT THE MODULE. CellReservation gains a
BudgetRefused arm and CellReserved gains the advanced account, and that pairing
is the whole safety argument: no arm carries an account without a cell, and no
arm carries a cell without an account. The partial commit -- an encumbrance with
nothing running, or a running cell nobody is paying for -- has no constructor, so
it is unwritable rather than checked (§4b, structurally impossible).
THE ORDERING CLAIM WAS WITHDRAWN, AND THE RECEIPT IS WHY. A witness asserting
"the budget refuses before the store is touched" was authored, went green, and
STAYED GREEN under a mutation moving the compare-and-set ahead of the
encumbrance. The substrate is lazy: the branch that is not returned is never
forced, so both spellings are equally effect-free and the row discriminated
nothing -- a decoration cited as coverage. It is replaced by rows that assert
what the carrier actually guarantees.
THREE ROWS, EACH EXCLUDING WHAT THE OTHERS ADMIT. A ceiling below the liability
refuses with a ledger cause. An offer quoted in a currency the account does not
hold refuses on the OTHER axis, which is what excludes a broker that returns
BudgetRefused unconditionally -- and it is only authorable because the currency
presented to the budget comes from the offer rather than from the account, which
would have made the check green by construction. A ceiling of 999 against a
liability of 1000 refuses only if the FULL selection cost was presented, so a
broker encumbering the marginal charge alone goes red where the other two stay
green.
Compile: 0 blocking over both entries. All five rows verified returning true by
execution, not by typecheck.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The annotation said the refusals were counted and nothing counted them
Review 57180 (codex/gpt-5.6-sol, REQUEST_CHANGES) flagged two Boolean predicates
over substrate coproducts and cited a predicate-dissolution rule in DESIGN.md.
THAT RULE IS NOT IN DESIGN.md. It lives in docs/plans/nat-grounding-unification-
design.md and it is narrower than cited: a manual match is forbidden WHERE A
CANONICAL FOLD ALREADY EXISTS, which is why is_zero must become nat_cata.
Neither CapacityClassAdmission nor CellReservation has a catamorphism, so the
rule as stated does not reach either site.
Following it to the code found two real defects underneath it, and both are
worse than the thing that was reported.
THE ROSTER WAS SILENTLY NARROWED WHILE THE ANNOTATION CLAIMED OTHERWISE.
admitted_cell_roster kept the admitted through the Bool; refused_cell_admissions
collected the refused and HAD NO CALLER. So a demand refused entirely on the
capacity-class safety line and a demand nobody offered anything for arrived as
one symbol, and their remedies are opposite: offer more capacity, versus stop
asking for capacity you are not sanctioned to use. The prose above them read
"the refusals are COUNTED rather than silently filtered". Nothing counted them.
That is the empty-observation narrow with a sentence standing where the
mechanism was supposed to be.
Two folds re-running one judgement could also only agree by convention -- an
edit to either could put a candidate in neither half or in both, undetected. One
partition_cell_roster now makes the decision once and returns both halves, so
they cannot disagree, and NoCellAdmissible carries the refused population so the
two states are distinguishable by the caller. The Bool dies with its only
production caller.
THE OTHER PREDICATE HAD NO PRODUCTION CONSUMER AT ALL. cell_reservation_is_held
was called only by the two witness rows that existed to cover it -- an artifact
whose only consumer is its own test. Deleted. What replaces it exercises the
partition through the real broker: a refused executor is reported, an empty
roster reports none, and the pair excludes a broker that always reports a
refusal.
AND THE FOUR CAPACITY ROWS WERE ASSERTING THROUGH A COLLAPSE THEY THEMSELVES
DECLARED ILLEGAL. The Bool answered false for both a refused class and an
unclassified executor, while the unclassified row's own annotation said those
two states have different remedies and must not be collapsed. The row could not
see the distinction it was about. Each now names its arm, and the substitution
is executed rather than asserted: swapping the unclassified row's selector to
the other refusal arm returns false, which is the red the old Bool could not
produce.
Compile: 0 blocking. Eight rows verified returning true by execution, plus the
one mutation returning false.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The reservation had no way to end: the release half, and the slot finally says who holds it
The broker minted reservations and nothing ever ended them. product.fabric.budget
has had settle_money and release_money since it landed, fenced on the lease
generation; product.fabric.arbitration models the DECISION as ReleaseDirective
and says in its own header that the fabric releases nothing there. What was
missing was the actuator. Measured before starting: release_money and
settle_money had witness callers and ZERO production consumers.
THE SLOT PAYLOAD WAS WRITE-ONLY AND RELEASE IS ITS FIRST READER. That is the
part of this change that is not plumbing. The broker wrote the reservation into
the slot and nothing ever read it back, so the question release has to ask -- IS
THIS CELL HELD, AND BY WHICH RESERVATION -- had no answer. Without one, release
is a blind write: it frees whatever is in the slot on the strength of a
generation the CALLER supplied, which is a second account of who holds the cell
and free to disagree with the store.
The generation fence does not close that. It establishes the slot has not MOVED
since it was observed, which is a different question from whether it is held and
by whom. A slot already free at generation N admits a release presenting N, and
that is not a harmless no-op: it writes free over free, so a re-reservation
racing the second release finds its precondition broken by the release of a hold
that never existed.
So CellSlotState is typed, CellHeld carries the reservation reference itself
rather than re-rendering the demand and offer into a second spelling of an
identity that already exists, and the decode REFUSES an unrecognised payload
rather than answering either state.
THE PARTIAL RELEASE HAS NO CONSTRUCTOR, and it leaks the opposite way to the
reservation's: freeing the cell while the encumbrance stands bills a customer
for an idle machine, and releasing the money while the cell stays held strands
capacity under work nothing requires. Same construction argument as the reserve
half -- the money transition is pure, the slot write is the only effect, and no
arm of CellRelease carries one without the other.
AND THE FUNCTION WAS UNREACHABLE UNTIL THE LAST COMMIT OF THIS CHANGE, WHICH THE
WITNESSES COULD NOT HAVE TOLD ME. release_reserved_cell takes a
CasSlotObservation, and that type had no production producer anywhere: the file
store answers CasSlotProbe and file_compare_and_set converts internally without
ever building an observation. So the release path was callable only from
hand-built values, and my own witnesses were authoring the exact input the store
is supposed to supply -- an artifact with no final consumer, hidden by its own
tests. Found by writing the live probe row, not by the witnesses.
The repair is one observation surface in the store, observe_cas_slot_state, plus
release_reserved_cell_at beside the pure decision. It deliberately does not
delegate the bound arm to cas_probe_as_readable: that projection answers
CasReadableAbsent for a slot past the probe bound, which is right for reporting
a lost race and wrong for a decision caller, who would read "the cell is empty"
from a store that could not tell it anything and pick the remedy for an empty
cell instead of repairing the slot. file_compare_and_set is left alone -- it
produces outcomes rather than observations, so there is no second producer, and
restructuring it would rewrite a load-bearing function whose header narrates a
previously-fixed write-decides bug for no gain to it.
Seven witness rows, every one green by execution, and the holder wall carries an
executed RED: disabling the comparison returns false. Compile 0 blocking across
the witness and probe entries.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* The two tags were the same length and the decode was quietly relying on it
Review 57256 (APPROVE, non-blocking) noticed that decode_cell_slot_payload
computed the body ONCE against the length of the held tag and reused it for the
free arm, which is correct only because both tags happen to be five characters.
The note is right and the coupling bought nothing, so it is removed rather than
documented.
WHY IT WAS WORTH A COMMIT RATHER THAN A REPLY. The failure it sets up is silent
and delayed: a third tag of any other length decodes to a body sliced at the
wrong offset, and every existing row stays green because the two tags that
already exist still agree. So the check that would catch it is exactly the check
nobody writes -- the round trip over a tag that does not exist yet.
The same defect had a second face the note did not name: each tag was spelled
TWICE, once rendering and once decoding, so the two spellings could drift
independently of the lengths. Both are one rule. The tags are named once and the
body is derived from the tag that MATCHED, so there is no offset to get wrong
and no second spelling to disagree.
PROVEN BY EXECUTION RATHER THAN BY INSPECTION, because "now it is decoupled" is
the kind of claim that reads as obviously true and is worth one run: with
cell_free_tag temporarily changed from "free|" to "released|" -- five characters
to nine -- both_slot_states_survive_the_round_trip still returns true. Under the
previous form that substitution sliced the free body at offset 5 and would have
failed. Tag restored, compile 0 blocking.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* compute fabric design (#9604)
* Six unresolvable names in the v2 root's emitted Rust: qualify the cross-module calls and use the declared list_length (#9547)
The v2 compiler root emits cleanly -- 0 blocking, 2083 advisory, 175 files --
and the emitted crate does not compile. Measured on 00b242b81a1 with
`gunbc compile --entry src/v2/compiler/00_compile.dag --target rust`, then
cargo over the emitted tree with its own emitted Cargo.toml: 20 rustc errors.
Six of them are source defects in this repository's own .dag, not emitter
defects and not self-host work, and this commit is those six.
THREE ARE NAMES USED WITH NEITHER AN IMPORT NOR A QUALIFICATION.
`decl_facts` is declared in v2.std.decl_index and used bare in two modules;
`PartialFunction` is declared in std.algebra and used bare in a type position.
The interpreter resolves them, so nothing refused; the emitter reports them as
`unlisted import use` advisories and emits the bare name, which is E0425. The
repair follows the idiom already on one of the two lines -- grammar_coverage.dag
declares no imports at all and qualifies every other cross-module reference
inline -- so these are qualified rather than imported. inferred_tree.dag already
carries five imports, so PartialFunction is added to that list.
THREE ARE A FREE-FUNCTION SPELLING OF A METHOD. `length(xs:)` has no declaration
anywhere in .dag; `length` is a MethodDeclaration in dag/std/methods.dag that the
interpreter intercepts. The corpus spells this `.length(` at 804 sites and
`list_length(` at 306; only reference_deps used the free form. Repointed at
std.types.list_length, whose declared parameter is `items`, not `xs`.
MEASURED, EACH ROUND A FULL RE-EMIT AND A FULL CARGO BUILD OF THE EMITTED TREE:
20 -> 17 after the three qualifications, 17 -> 14 after the three list_length
sites. Exactly the fixed errors disappeared both times and NOTHING WAS UNMASKED
behind them. That is worth stating because it is the outcome the masking
argument says not to assume: rustc stops after name resolution, so every count
here is a lower bound on a fully-resolving crate, and 20 -> 17 -> 14 establishes
only that no masking occurred AT THIS LAYER, never that none exists.
WHAT IS DELIBERATELY NOT IN THIS COMMIT, because none of it is a source defect:
five host builtins with no .dag body (layer_import_facts and the four
*_resolution_facts), four errors from Filesystem.Read emitting `.await?` against
an unbound handle in a sync fn, three emitter type-argument defects, one
unclassified E0391 variance cycle, and two deliberate compile_error!
sentinels that 05_emit_rust.dag emits instead of fabricating a default.
No Rust touched. No roster edited. No policy changed.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares (#9560)
* The census memo's fill was never attributed, so one claim was charged for two compiles the roster shares
gunbc#9477 made a shared memoized compile's fill a preparation cost rather than
the first payer's, because a merge-blocking per-claim ceiling charged with an
order-dependent number is a fact about discovery order and not about the tree.
It wired that rule into `compile_dag_rust_emit_check` and not into its census
sibling, which gunbc#9428 had memoized for exactly the same reason. One
accounting rule, two homes, applied in one of them.
MEASURED, not inferred. On main run 33131296988 (b6003a45e) the floor refuses
with `completed_over_cost_requirement=1` and `failed=0`:
`test.claim.callable_candidate_ambiguity_witness.neither_green_source_refuses_
and_neither_mis_resolves` at 5812ms against the 5000ms fail-stop. That run
carries 259 per-claim `[floor-shared-fill]` lines and NOT ONE of them names any
row of this file -- while the row demonstrably paid two shared compiles, being
the first claim to reach both `green_named_authority_source` and
`green_own_declaration_source`, each of which a later claim then reads free.
Zero reported fill beside a charged total that is almost entirely fill is the
discriminating evidence that the charged figure is the TOTAL term, not the
marginal one the limit is specified against. Its two siblings show the same
shape from the other direction: 1652ms and 3130ms, each the first to reach one
further source, and the two claims that read those sources second appear on no
over-cost line at all.
THE FIX IS THE ONE THE RECEIPTS ALREADY RULED FOR. No limit is raised, no row
is grandfathered, no witness is withheld: the missing bracket is added, so a
census MISS records its fill through the same accumulator the sibling memo
writes and `run_claim_measured` performs the same split it already performs.
Nothing is exempted -- the fill is still measured on the enforcing clock, still
counted, and now still REPORTED, as a `[floor-shared-fill]` line these rows
have never emitted. Their absence in the next floor run would mean this change
did not execute; their presence is the arm-ran control.
The two forward-freeze receipts are corrected in the same change. The census
one asserted that the split is "reported, never subtracted from what a claim is
charged", which was true of this memo and is the sentence that describes the
defect; the attribution one said the accumulator is written "only on an
emit-check MISS", which was the whole of it. No declaration is added, so
neither receipt's hand-item delta moves.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* Name the forcing class that decides warm-versus-net, and name the third state as the one that must not exist
The bracket in the previous commit fixes ONE instance. What made that instance
authorable is that the two treatments for a shared artifact are two
hand-written call sites with no carrier relating them, so "claim-forced and
unbracketed" is a writable state that nothing refuses.
THE DISCRIMINATOR IS WHEN THE ARTIFACT CAN BE FORCED.
Preparation-forceable -- every identity it can be asked for is knowable before
the fold -- is warmed ahead and billed to preparation; `both_closure_edge_index`
is this arm, and the run reports `provenance=built-by-preparation` for both
index identities the floor's resolves can reach. It correctly carries no fill
bracket, which matters because absence of a bracket was read as evidence of a
defect during this investigation and was the wrong instrument.
Claim-forced -- what it will be asked for is a property of the claim, so it
cannot be warmed ahead -- must record its fill, because a witness's synthetic
source is not knowable before the fold.
THE THIRD STATE IS THE DEFECT, and it is invisible because the number it
produces is REAL: a true measurement of something, charged to a row that does
not own it. Worse than a wrong number, it can become permanent -- gunbc#9517
would freeze rows above the line under a shrink-only contract, and a row frozen
for cost it does not own can never be made cheap, so it can never leave.
PROSE IS NOT A WALL AND THE ROW SAYS SO. Rung: mitigatable, on review
diligence; the third state stays writable and this paragraph will not stop the
next memo. Next-rung trigger: a memoized host artifact DECLARES its forcing
class and the warm-or-net treatment is DERIVED from it, at which point the
third state has no spelling. That construction is not made here and is not
claimed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Two 04_infer rows carried counts that had rotted — name the instrument, and stop restating the superseded figures as history (#9462)
* 04_infer: the traversal-idiom count rotted to 16 while the tree carried 29 -- name the instrument
explicit_return_conformance_note argued that collect_explicit_return_values is not a new
shape but the seed's ordinary traversal idiom, and grounded that on a transcribed count:
"16 such sites on origin/main" across seven named modules.
Measured, both on origin/main and on this branch: 29 sites across EIGHT modules.
04_emit_info 1 · 04_sigs 1 · 04_infer 5 · 05_emit 3 · 05_emit_rust 8
compile 1 · complexity 6 · trait_derive_emit 4
trait_derive_emit was absent from the note's list entirely, so the clause was wrong about
the population's membership and not only its size.
NOTHING EDITED THE NOTE. The tree moved underneath it, which is precisely the decay mode
DESIGN §3 gives for a positional citation -- it rots without anyone touching either end --
and it is what the 2026-08-24 ruling forbids by name: cite the instrument, never transcribe
its output. The recipe is one grep and it is now stated instead of its result.
THE ARGUMENT NEVER NEEDED THE NUMBER, which is the part worth keeping. What makes this the
seed's idiom rather than a new shape is that EVERY such collector recurses itself, and that
holds at 16, at 29, and at whatever it measures next. A clause whose force depends on a
figure it cannot keep current was overstating its own evidence -- the number was doing
rhetorical work, not logical work.
Two derived ordinals went with it. "the 17th instance of a 16-instance idiom" and
"collect_explicit_return_values is the 17th ... the 18th" were positions in the disproven
count, so they were already false; they now read as further instances with no ordinal. An
ordinal is a transcribed measurement wearing the costume of a structural fact, and it is
worse than the raw count because it does not look like a measurement at all.
Prose-only, in one data row. No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Regenerate the stage0 mirrors, and delete the dead child_type_at accessor
REGEN. The prose change in 04_infer edits two `data ...: String` rows. Those are program
data, not annotations, so they emit into the stage0 Rust mirror, and CI's build lane
refused with:
required-regen: FAIL generated surface drift: v1_compiler_infer.rs
Regenerated through the sanctioned producer -- `claim_executor --required-regen
--source-root dag --source-root src/v2` -- rather than hand-edited. A hand-authored mirror
is exactly what that gate exists to refuse, and its only reachable green would have been
the forbidden action.
EVERY CHANGED LINE IS ACCOUNTED FOR, because a regen can also delete orphan content a
committed projection carries that no authority produces:
v1_compiler_infer.rs 2 lines the two data rows edited in the parent commit
v1_compiler_infer_types.rs 14 lines deleted: the child_type_at body
Nothing else moved. Re-running regen against the installed mirrors reports
first_generation_equal=true. (declared_divergent=1 [main.rs] is pre-existing; it is present
in the failing run on the parent commit too.)
DEAD ACCESSOR. v1.04_types child_type_at had ZERO callers -- measured across the whole
corpus, not just .dag: one definition in 04_types.dag, one in the generated mirror, no
consumers, no re-export, no prose reference.
It is deleted rather than left because of where it sits. It is a decoy beside
child_type_node, the live accessor that discriminates a type child from a field child by
whether `inferred` is populated -- a fabricated provenance stamp the parser writes at parse
time. Anyone repairing that discrimination reads both functions and has to work out which
one matters. Approved by compiler direction as needing no ruling.
WHY THIS WIDENS AN ALREADY-APPROVED PR, stated because the usual answer is that it should
not. #9462 was red and required a regen commit regardless, so the approval resets either
way and the deletion rides along at zero marginal cost -- and it keeps this to ONE regen
cycle rather than two. Without that, the correct call would have been a separate PR.
No semantics, no behaviour, no gate.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The sibling row carried the SAME disproven count -- one sentence fixed, the claim left standing
FOUND FROM OUTSIDE, NOT BY ME. The first commit repaired explicit_return_conformance_note and
left seed_node_traversal_frontier asserting the identical thing a few lines above it:
"the idiom is 16 self-recursive `children |> flat_map` sites on origin/main across
04_emit_info, 04_sigs, 04_infer, 05_emit, 05_emit_rust, compile and complexity"
Same 16, same seven-module list, same two errors -- the tree measures 29 across EIGHT, with
trait_derive_emit absent from the list entirely. I edited a SENTENCE when the defect was a
CLAIM, which is the document-wide-correction failure, committed inside the change whose whole
subject is a rotted figure.
THE SECOND COUNT IN THAT ROW GOES TOO, AND THE REASONING IS THE INTERESTING PART. It carried
"579 direct Node-storage field reads in 04_infer alone". A plausible reconstruction -- counting
`.children`, `.params`, `.inferred` and their siblings -- returns roughly TWICE that. That
establishes the number is STALE without establishing what the right one is, because I cannot
recover the recipe its author used.
So the repair is DELETION, not an update. Replacing a stale figure with one my own instrument
produced would swap an uncheckable number for a checkable-LOOKING wrong one, which is worse:
the first is visibly unverifiable, the second gets cited as verified. The site population is
named by its instrument (grep the idiom under src/v1); the field-read population has no agreed
instrument and is stated as a SHAPE rather than a count.
That asymmetry is why the earlier commit deliberately left this figure alone, and why leaving
it was still wrong -- declining to invent a recipe was right, declining to remove the number
was not.
Mirror regenerated through claim_executor --required-regen. One line in v1_compiler_infer.rs,
which is the row above. Prose only.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* The counts were deleted as CLAIMS and kept as HISTORY -- which is the same decay inside the sentence announcing its removal
Found in review, not by me, and it is the sharper half of this PR.
The previous commits removed the rotted figures from both 04_infer rows as ASSERTIONS and then
restated them as provenance: "it read 16 sites across seven modules while the tree measures 29
across eight". That is still a number in a live `data … : String` authority. It rots the same
way the original did, nothing re-derives it, and it gets quoted back as though this row had
measured it -- so the row announcing that it no longer transcribes an instrument's output was
transcribing one in the same breath.
BOTH ROWS NOW CARRY ZERO FIGURES, verified mechanically rather than by reading:
grep '^data explicit_return_conformance_note' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
grep '^data seed_node_traversal_frontier' | grep -oE '(16|29|579|18|17th|18th|seven|eight)' -> empty
The before-and-after lives in the PR, which is the artifact that is allowed to carry a
superseded measurement, because it is dated and nobody consumes it as current authority.
A SECOND, INDEPENDENT PREDICATE DEFECT, also named in review. Both rows pointed at a LEXICAL
instrument (grep `children |> flat_map`) while asserting SEMANTIC properties -- self-recursive,
and the seed's ONLY traversal idiom. A grep bounds the literal-occurrence population and cannot
establish recursion or exhaustiveness. Naming an instrument does not fix a claim if the
instrument answers a different question, which is the same right-number-wrong-subject failure the
counts themselves were. Both rows now say so: the grep bounds the literal population, and the
recursion property is read off the sites rather than off the count.
WHY DELETION AND NOT AN UPDATE, restated because it is the part a reader will want to argue with:
one row's field-read count has no reproducible recipe and a plausible reconstruction disagrees by
a wide margin. That establishes STALE without establishing CORRECT. Substituting a figure from my
own instrument would swap an uncheckable number for a checkable-LOOKING wrong one -- worse,
because the first is visibly unverifiable and the second gets cited as verified. That population
is stated as a shape.
Mirror regenerated through claim_executor --required-regen and applied from the candidate rather
than hand-edited; the diff is exactly the two rows, 4 lines, no other drift.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
* Restore the mirror the merge resolution dropped: --theirs took main's bytes, which never carried the prose fix
THE MERGE CONFLICT WAS IN A GENERATED FILE and I resolved it with --theirs to complete the merge,
intending to regenerate immediately. That resolution takes MAIN's mirror, which by construction
does not contain this branch's edits -- so for one commit the authority (04_infer.dag) carried the
repaired prose and its mirror carried main's older text. A regen fixed-point check is exactly what
catches that, and it did:
changed lines: 4, in the two rows this branch edits, nothing else
Mirror re-derived from the MERGED authority through claim_executor --required-regen and applied
from the candidate rather than hand-edited.
WHY THIS IS WORTH A COMMIT MESSAGE RATHER THAN A SILENT FIXUP: picking a side of a conflict in a
generated file is never a resolution, it is a coin flip between two stale artifacts. The authority
merged cleanly on its own -- the mirror had no business being adjudicated at all, and the only
correct answer was to recompute it. Taking --ours would have been equally wrong in the other
direction, dropping main's edits to the same file.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* An escalation is not an infrastructure loss: give ExecutionAttemptLineage the arm the resident-model thesis is measured on (#9546)
A local model that reaches a terminal result it cannot carry, followed by a
more capable model taking the next try, is the single observation the
"progressively smaller models suffice" claim is denominated in. Measured on
this tree, nothing could express it: grep for Episode/continuation/retry_of/
predecessor across dag/gunbc, dag/std and src/v2 returns nothing episode-shaped,
and ExecutionAttemptLineage's three arms are InitialAttempt, InfrastructureRetry
and RequestedReexecution. So an escalation had to be recorded as either an
infrastructure retry -- which says the work told us nothing -- or as an
unrelated initial attempt, which discards the edge entirely.
CapabilityEscalation is a sibling of InfrastructureRetry rather than an arm of
one generic Retry, because the two differ in exactly what lineage exists to
record: an infrastructure loss says nothing about the work, while an escalation
says the work exceeded the capability that was tried. Like its sibling it names
the prior attempt AND the receipt that established the prior result, so merely
resolving a more expensive model after a cheaper one is a selection fact rather
than an escalation.
The two arms are deliberately the same SHAPE, which is what the third witness is
for: a control checking only the prior-attempt key would pass identically
against a lineage that had collapsed them, so the discriminating assertion
matches on the arm and fails if an escalation ever reads as a retry or the
reverse.
WHAT IS NOT VERIFIED, stated because a green I cannot stand behind is worse than
no green. `gunbc compile` takes no --entry, and the whole-corpus run over this
tree reports 31139 diagnostics ON PRISTINE MAIN, 1283 of them "expected item
declaration" on `//` annotation lines -- so that CLI path does not route source
annotations the way the required parse phase does, and cannot adjudicate this
tree. My attempted discriminating RED (deleting one arm from an exhaustive
match) returned 31139, byte-identical to the pristine baseline: it added zero
errors and therefore discriminated nothing. An earlier local run appeared clean
only because it was killed at its timeout mid-typecheck and the truncated output
rendered identically to a completed clean one. CI is the check here.
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) (#9527)
* A typed wall for barren witness files exists, is wired to a hard failure, and the required floor never calls it: 62 unenrolled claims, the third scanner, and 37 promotions
The brief was 62 claims declared plain `fn` and never enrolled. Chasing why produced a
larger finding than the population: `v2.workflow.floor_naming_hygiene`
`floor_entry_is_barren_test_sidecar` has refused this exact class since it was written,
`floor_discovery_finalize` turns it into `FloorDiscoveryRefused`, and the host returns that
as `Err`. It stops the line. It has never been on the line.
MEASURED, not inferred: main run 33092582255 (headSha 107304a579), both lanes green, four
barren `*_test.dag` entries present at that sha, and zero occurrences of `barren` or
`sidecar` in the 693,975-byte run log.
WHY: `run_required_floor` builds its roster from `prepared.witness_files`, produced by
`witness_file_from_source`, which answers `None` for a file with no `test fn` — and the
caller discarded that answer. The walled `.dag` producer is reachable only through
`discover_floor_witness_roster`, which the required floor never calls. Three scanners for
one fact live in one binary and the wall guards the one production retired. The Rust test
asserting the wiring is not the missing piece: it still PASSES, because the wiring is
intact on the producer path — a green local `cargo test` says nothing about the required
path.
WHAT LANDED: preparation records the discarded fact; the floor asks
`floor_naming_hygiene`'s own `floor_test_sidecar_suffix` which recorded paths are
`*_test.dag` and refuses `cause=BarrenTestSidecar`. The rule keeps one home; only its
consumer moved. The recorded set uses the RULE's vocabulary — neither `test fn` nor
`test data` — so the 13 test-data-only files are not over-refused. The floor's summary line
is bounded above rather than left exact-and-silent. 37 leaf claims promoted, 37/37 PASS,
and the 4 sibling-conjunction aggregates deleted: each was a hand-rolled substitute for
enrolment with exactly one occurrence in the corpus.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
* Consume the modeled sidecar predicates instead of re-spelling them in Rust: delete the forked suffix test and the added test-decl scan
review 56971 requested changes on #9499 and was right on both counts; #9499 merged before
the rework landed, so main currently carries the fork and this is the repair.
FINDING 2, the reimplemented predicate. `floor_barren_test_sidecars` read
`floor_test_sidecar_suffix` from the `.dag` and then applied `strip_prefix("./")` and
`ends_with` in Rust. Reading the constant does not make the computation derived from the
authority — the two can drift independently. It now INVOKES the modeled predicates and
decides nothing itself. My own framing ("policy stays home, only the consumer moves") was
the error: I moved the CONSTANT home and left the COMPUTATION forked.
FINDING 1, the added test-declaration scan. The `!line.starts_with("test data ")` check is
DELETED. It existed to stop the wall over-refusing the 13 test-data-only files, which is
exactly what `floor_discovery_scan_test_decl_names` already does inside
`floor_entry_is_barren_test_sidecar`.
THE SHAPE, and why it costs one call rather than one per corpus file — which is what pushed
me into the fork to begin with. Preparation records a CANDIDATE SET, not a verdict: every
source `witness_file_from_source` declined, asking nothing about suffixes and nothing about
`test data`. `floor_entries_requiring_test_sidecar` (new, in `v2.workflow.floor_naming_hygiene`,
composing the existing `floor_entry_requires_test_sidecar`) is then asked ONCE for the whole
roster — a pure string question, one crossing — and `floor_entry_is_barren_test_sidecar` is
asked per survivor with that file's content, typically zero or a handful of invocations.
THE CANDIDATE SET IS DELIBERATELY OVER-INCLUSIVE AND THAT IS WHAT MAKES IT SOUND: a
test-data-only file lands in it and the `.dag` answers NOT barren, because its own scan counts
`test data` as a test decl. Rust can only widen the question, never decide it, so a
Rust/`.dag` disagreement cannot produce a wrong refusal — only a candidate the authority
discards. A missing candidate source is a typed refusal rather than a skip (§5).
RE-VERIFIED BY EXECUTION, because changing the mechanism invalidates the evidence for it.
Same binary, corpora identical except `filesystem_read_outcome_witness_test.dag`:
RED refuses `cause=BarrenTestSidecar count=1` naming it; GREEN completes site-projection
(sites=13351 files=1697 claims=11910). The first re-run attempt failed loudly with
`no declaration named 'v2.workflow.floor_naming_hygiene.floor_entries_requiring_test_sidecar'`
because the control trees came from HEAD while the new `.dag` function was still uncommitted
— a binary/corpus mismatch the control caught rather than one that shipped.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012aG5paMUmwmfRSp7czE5dY
---------
Co-authored-by: Brian Searls <bts53@scarletmail.rutgers.edu>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Delete the floor's stale live-tree decline (#9106)
* Delete the floor's stale live-tree decline
* Enroll surfaced required-floor dispositions
* Retire executing witnesses from deferral freeze
* Retire routed witnesses from deferral freeze
* Retire merged route gaps from deferral freeze
* Enroll post-merge shell route gaps
* Enroll activated semantic reds
* Place expected-red provenance at module grain
* Enroll newly exposed parser-drop route gap
* Adjudicate live-tree cut witness fallout
* Keep quarantine disposition annotation at module grain
* Fix expected-red chunk merge boundary
* Declare the live-tree census debt
* Retire five executing freeze rows
* Retire two supplied route gaps
* Bind exposed floor debt to repair lanes
* Retire stale live-tree decline prose
* Close route-gap lists after stale-row retirement
* Retire repaired expected-red rows
* Classify realization floor non-verdict
* Compose discovery census with live-tree cut
* Declare the exposed gitattributes drift
* Bind the accumulator analysis explicitly
* Preserve new diagnostic histogram arms
* Update floor projection annotation
* Close floor cut review obligations
* Remove stale retained-parameter annotation
* Correct live-tree cutover annotations
* Retire repaired live-tree census stalls
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences (#9447)
* R_X(B): the legacy use-line repair envelope, keyed on repair sites because emit-time candidates do not correspond to reference occurrences
The producer (#9439) correctly refused the binding envelope: its denominator is
the candidates that reached the decision, produced by the same pass that decides
them. This lands the envelope with a denominator that is not that.
The open question -- does every emit-time repair candidate correspond to a
parse-time reference occurrence -- is answered NO, in three independent
directions at once: the roster is deduplicated by SPELLING before any decision
(grain), it admits names merely for appearing as an identifier in the EMITTED
Rust (superset -- nothing authored them, so they can have no occurrence id), and
it drops occurrences the repairer correctly never touches (subset). So R_X(B) is
a PEER of O_X(B) keyed on repair sites, not an instance of it.
The completeness law is one law for any key, so it is hoisted key-generic into
std.observation_completeness and both envelopes instantiate it -- two subjects,
two denominators, one join. decl_field_label moves to std.decl_ref for the same
reason, with the third projection in std.observation named rather than tolerated.
Roster provenance is structural rather than ordered: SubjectRoster is
sole_constructor, prove_subject_roster is its only mint, and the admission takes
one -- so joining against an unproven roster has no spelling.
What this does NOT establish is stated in the carrier beside what it does: the
producer could still assemble the roster from the candidates it decided. The
tautology becomes visible and nameable rather than dissolved, which is an
improvement and not a proof; the next-rung trigger is recorded.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Restore legacy_binding_delta's own occurrences: payload, over-renamed by the hoist's blanket sed
The hoist renames the completeness arms' payload from `occurrences:` to `keys:`,
because at the repair envelope's instantiation the key is a repair site and
"occurrences" would be a lie. `{ occurrences: ... }` also spells the payload on
six unrelated ProvenanceTotality arms in legacy_binding_delta, and a blanket
rename over the witness took those with it -- 71 blocking errors, none of them in
the module the hoist was about.
Caught by compiling the blast radius rather than grepping it, which is the whole
reason it was compiled: "two witness files" is a file count, not a symbol
census, and the payload name was never the thing being renamed -- the TYPE was.
* Rename the roster carrier off a name the enforcement lens already owns, and drop the declaration move out of this change
Three CI failures, three causes.
SubjectRoster was already declared by v2.lens.enforcement.vocab for an
unrelated concept. Whole-corpus resolution handed THIS type to that lens's own
consumers and their `entries` field stopped existing -- nine diagnostics, none
of them in a module this change touches. Renamed to ProvenRepairRoster. The
shape is the finding rather than the fix: the duplicate was minted here and
every symptom surfaced elsewhere, so no compile of this closure could have
shown it, which is what makes "my closure is clean" structurally unable to
catch this class.
decl_field_label's move to std.decl_ref is reverted. It caused both the regen
drift on std_decl_ref.rs and two TargetChanged wave-admission deltas. The
declaration stays in the binding envelope and the repair envelope imports it --
one authority, no fork -- and the relocation lands as its own change where its
two rows are the whole reviewable diff.
The first cut of that annotation justified the revert by citing the wave grain
note's "two change classes in one diff" clause. That was a mis-citation: the
clause's subject is a wave that BOTH REQUALIFIES AND MOVES a symbol, and this
requalifies nothing. Corrected in place rather than dropped, because a carrier
that once stated an invented prohibition should say so.
One unused import removed (ObservationCompleteness in the observation witness).
The remaining two UnexplainedSubjectMotion deltas are a confirmed defect in the
wave-admission channel's reader, owned by another lane; its refusal is left
standing rather than cleared by an admission row, which over a channel that
cannot see the reference would be a manual override rather than an admission.
Evidence: 21/21 witness arms return true; mutating prove_repair_roster's digest
comparison to a constant turns the provenance arm false while the positive
control stays true. All three affected closures compile at 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main, and take the three obligations #9440's landing created
crisp-crab's #9440 merged first, so by the order the two lanes committed to,
this change owes the collision resolution -- and owes it HERE rather than in a
follow-up, because declaration names bind closure-globally and two declarations
of one name on main is a collision, not a shadowing. Neither author can observe
it by compiling their own branch: both were green against main independently.
The receipt is this lane's own SubjectRoster duplicate, which produced nine
diagnostics, every one in v2.lens.enforcement modules that change never touched.
Three obligations, all measured rather than assumed:
- the placeholder `type CompleteLegacyRepairObservation<R>` is deleted from
v2.workflow.legacy_baseline_capture and the real carrier imported from
v2.workflow.legacy_repair_observation. Its accepted arm LegacyBaselineCaptured
is constructible for the first time; the annotation is rewritten to record
why the deletion could not wait rather than left describing a hole that is
now filled.
- the two LegacyObservationCompleteness references the hoist renamed --
the import member and the LegacyBaselineObservationIncomplete payload --
migrated to ObservationCompleteness<Int>. crisp-crab measured their exposure
at exactly two lines and named both; both appeared where they said.
- the second type parameter survives the swap deliberately. O is what the
resolver selected per occurrence, R what the repairer decided per repair
site; one parameter would force the emitter's repair vocabulary to equal the
resolver's binding vocabulary, which is the conflation the operator ruling
forbids, committed in the parameter list instead of the fields.
NOT carried: #9440's three dead imports. The offer was withdrawn after the
coupling was priced -- they are inert, nothing waits on them, and tying someone
else's cleanup to this branch's blocker was never the cheap option.
v2.workflow.legacy_baseline_capture compiles 0 blocking after the change.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Merge main: pick up the wave-admission membership fix (#9490) and the repair-decision producer (#9439)
#9490 splits membership_declared from membership_bound_through, so an authored
import claim answers the ADD direction outright. Both UnexplainedSubjectMotion
rows this branch was refusing on carry an explicit import claim naming
std.observation_completeness, so both close without the gate having to reach a
pattern arm or an inferred-slot field type.
#9439 landed the producer this envelope was built for: reference_derived_
candidate_disposition and reference_derived_census in v1.05_emit_rust. The
correspondence finding this branch rests on was read off that pass, and it is
now on main rather than on a branch -- so the annotation citing it names a
declaration that resolves.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Refuse a malformed denominator: a roster naming one site twice certified as complete (review 56949)
`std.observation_completeness` returned `ObservationComplete` for expected
`[A, A]` against observed `[A]`. Nothing missing -- A IS present, so both
expected entries filter out. Nothing foreign. Nothing repeated -- the repeat
test counts OBSERVED occurrences and there is one. So the envelope certified
exactness over a denominator that asked for one site twice.
All three refusals judged the ANSWER set. None judged the QUESTION set, and an
ill-formed question set defeats all three at once.
WHY 21 ARMS MISSED IT: every arm varied the OBSERVATION against a well-formed
roster; none varied the ROSTER. A missing AXIS, not a missing case within one --
and the module header already said completeness is a join between two sets while
every arm ex…
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 30, 2026
…tural discriminators; union the parser's type-reference channel at every wall consumer; sixth admission shrink The wave wall's reference collector still reported four declaring/labelling roles as references — a record TYPE declaration's field labels, a named call argument's label, a parameter binder, and a coproduct declaration's variant names — each able to fabricate the same false refusal the record-literal case did (#9106), and each now excluded by its own structural discriminator rather than a guessed parent rule: - a declared field label is the field_to_child_node shape (declared type in `inferred`, no children/params, no expr data, no connective, an authored ident) — a refinement base type has `inferred: None` and stays collected; - ExprCall joins ExprRecordLit in the parent-kind rule: argument labels are suppressed, argument values still walked, the callee spelling untouched; - everything directly on the params edge declares a name, so the edge passes the binder flag, consumed at one level — the param's declared type in children[0] is still collected; - Connective::Disj is set only by the coproduct item builders, so a Disj parent's direct children are variant declarations (already exported via `variants`); their payload fields are still walked. The complementary defect is closed in the same change: `direct_membership` and `binding_rows` now union `authored_type_references` exactly as `membership_bound_through` already did — a declared type is parked in `inferred`, which the walk never visits, so a module whose only reach into another was a declared field or payload type produced no membership edge and no binding row, and a cut repointing a declared type moved nothing on either side of the wall. The exclusions above make this union more load-bearing, not less: the genuine reference beside each suppressed label lives in the parser-stamped channel. Eight test pairs, every one verified BOTH directions by execution on BuildBuddy: green with the fix, red against the unfixed collector — including two measured decorations discarded on the way (a same-module variant supplier only ever produced the self-candidate; an unimported cross-module supplier never entered the candidate set), before the blanket-import fixture made the variant arm's RED reachable. Also the sixth admission shrink: #9698 merged, so its two RequiredCiLane rows report stale on every run from here and are removed by the trigger they were authored with. The roster is empty again. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GpYEk9gSYmMkwL1489D79U
gunbai-bot Bot
added a commit
that referenced
this pull request
Aug 30, 2026
…tural discriminators; union the parser's type-reference channel at every wall consumer; sixth admission shrink (#9714) The wave wall's reference collector still reported four declaring/labelling roles as references — a record TYPE declaration's field labels, a named call argument's label, a parameter binder, and a coproduct declaration's variant names — each able to fabricate the same false refusal the record-literal case did (#9106), and each now excluded by its own structural discriminator rather than a guessed parent rule: - a declared field label is the field_to_child_node shape (declared type in `inferred`, no children/params, no expr data, no connective, an authored ident) — a refinement base type has `inferred: None` and stays collected; - ExprCall joins ExprRecordLit in the parent-kind rule: argument labels are suppressed, argument values still walked, the callee spelling untouched; - everything directly on the params edge declares a name, so the edge passes the binder flag, consumed at one level — the param's declared type in children[0] is still collected; - Connective::Disj is set only by the coproduct item builders, so a Disj parent's direct children are variant declarations (already exported via `variants`); their payload fields are still walked. The complementary defect is closed in the same change: `direct_membership` and `binding_rows` now union `authored_type_references` exactly as `membership_bound_through` already did — a declared type is parked in `inferred`, which the walk never visits, so a module whose only reach into another was a declared field or payload type produced no membership edge and no binding row, and a cut repointing a declared type moved nothing on either side of the wall. The exclusions above make this union more load-bearing, not less: the genuine reference beside each suppressed label lives in the parser-stamped channel. Eight test pairs, every one verified BOTH directions by execution on BuildBuddy: green with the fix, red against the unfixed collector — including two measured decorations discarded on the way (a same-module variant supplier only ever produced the self-candidate; an unimported cross-module supplier never entered the candidate set), before the blanket-import fixture made the variant arm's RED reachable. Also the sixth admission shrink: #9698 merged, so its two RequiredCiLane rows report stale on every run from here and are removed by the trigger they were authored with. The roster is empty again. Claude-Session: https://claude.ai/code/session_01GpYEk9gSYmMkwL1489D79U Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Fable 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
1 participant
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.
Uncapped verdict receipt for the interrupted cohort
The floor headline cannot distinguish DID NOT ANSWER from ANSWERED YES, and when the interrupted cohort was finally allowed to finish, 9 of 44 answered NO. Production runs sequentially and
claims_executedcounts entering the fold; the 5,000ms CPU fail-stop returnsBudgetInterruptedbefore a semantic verdict. Run 32407436149 is the same-file precedent for putting terminal evidence on the surface readers consume.This was an out-of-band MEASUREMENT CAPABILITY; production admission and safety limits are unchanged. Complete observation 1: source
0f5b0c079e7; executable SHA-256aa024abc8b189dfa705a7039063a817add85654caae75f03ca950ecf79607d53; built 2026-08-27T01:07:51Z from that checkout; content probe confirmed this candidate'sFloorRouteGapExpectationdecoder. All 44 reached terminal outcomes sequentially: 35 PASS, 9 FAIL, 19,396,175ms witness wall and 151,880ms resolve wall. CPU tracked wall closely.The refreshed observation used source
7172d0d773aand executable SHA-256d21f68373eb8d75df63f2b8e8b267e532e23590de9693305a93008f1a0095fbb; it completed the same 44 in 18,896,576ms witness wall and 138,184ms resolve wall. Its terminal transport truncated the middle, so it is not used to fabricate a complete current per-row table. This table is explicitly observation 1.dag.test.claim.lifecycle_survivor_corpus_census.no_raw_lifecycle_string_survivors_remaingunbc.test.claim.realization_attempt_keystone_test.witness_real_corpus_entry_produces_typed_standinggunbc.test.claim.witness_execution_class_live_census_test.witness_live_roster_census_holdsv2.lens.no_dual_representation_test.no_dual_representation_test_clean_holdsv2.lens.no_dual_representation_test.no_dual_representation_test_coverage_honesty_holdsv2.test.lens_wiring_liveness.wiring_liveness_corpus_test.wiring_liveness_corpus_witnessesv2.test.claim.complexity.accumulator_copy_roster_gate_lean_bash.roster_bash_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate_lean_bash.roster_lean_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate.roster_compile_stage_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate.roster_glob_discovery_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate.roster_lens_cost_model_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate.roster_lens_traversal_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate.roster_machine_code_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate.roster_std_algebra_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate_std.roster_std_change_dag_zero_suspects_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate_swift.roster_swift_zero_suspects_within_ratchetv2.test.claim.enforcement.cost_coverage_witness.cost_coverage_corpus_roster_nonemptyv2.test.claim.enforcement.cost_coverage_witness.cost_coverage_dag_tree_receipt_by_executionv2.test.claim.enforcement.cost_coverage_witness.cost_coverage_decl_facts_roster_smoke_totality_holdsv2.test.claim.enforcement.cost_coverage_witness.cost_coverage_v2_tree_receipt_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_corpus_roster_dedupes_decl_factsv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_dag_tree_receipt_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_dag_tree_totality_holdsv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_decl_facts_roster_smoke_totality_holdsv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_parse_fraction_is_derivedv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_take_n_fixed_roster_saturates_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_take_n_live_dag_subset10_work_units_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_take_n_live_dag_subset5_work_units_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_v1_core_file_reject_locus_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_v1_rejected_rows_identity_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_v1_tokenize_file_reject_locus_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_v1_tree_receipt_by_executionv2.test.claim.enforcement.grammar_coverage_witness.grammar_coverage_v2_tree_receipt_by_executionv2.test.claim.enforcement_inventory_witness.enforcement_inventory_global_receipt_holdsv2.test.claim.enforcement_live_witness.bound_contracts_derive_live_receiptsv2.test.claim.enforcement_live_witness.complexity_repo_wide_verdict_matches_roadmapv2.test.claim.enforcement_live_witness.enforcement_consistency_gate_holdsv2.test.claim.enforcement_live_witness.live_corpus_is_currently_all_body_unavailablev2.test.claim.enforcement_live_witness.per_root_sentinels_hold_in_one_walkv2.test.claim.enforcement_live_witness.unbound_contracts_omit_semantic_receiptsv2.test.realization_vocabulary_containment.cli_vocabulary.rest_path_reaches_no_cli.compiler_substrate_reaches_no_cli_construction_vocabularyv2.test.realization_vocabulary_containment.cli_vocabulary.rest_path_reaches_no_cli.extdeps_reaches_no_cli_construction_vocabularyv2.test.realization_vocabulary_containment.cli_vocabulary.rest_path_reaches_no_cli.gunbc_consumers_reach_transport_vocabulary_only_by_named_admissionv2.test.realization_vocabulary_containment.cli_vocabulary.rest_path_reaches_no_cli.test_corpus_reaches_cli_vocabulary_only_as_declared_exercisebudget_refused=0after a cut is not evidence that the population is clean. It may mean the floor stopped executing that population. None of the nine identities appears in the accessible logs for runs 32186963581 or 32193032348, butfloor_expected_red.dagsays the prior 313-member passing population was never emitted at identity grain. Intersection with that historical population is therefore unestablished, not zero.Current-main sequencing refresh
Merged current main at
e1f65b36505. #9274 had already landed and discharged the observation-emitter migration census: its three surviving identities pass and its two obsolete identities were deleted by that repair, so #9106 removes the now-stale five-identityGuaranteeStall. #9276 remains open, so the external-model live-cover stall remains truthful on this candidate.The merge also exposed two new live imports of the deleted
DeclinedLiveTreearm in main’s discovery census. The census and all 16 of its witnesses are migrated to the surviving three-arm disposition: ordinary live-tree readers are planned, while long-home and fixture-home exclusions remain declined. The 4,057-file parse/index check reports no absent imports; the full targeted suite passed after correcting the derived aggregate’s dependency population from two to three.Latest floor adjudication (run 32926887613)
The floor completed its full routed population exactly:
planned = executed = terminal = 12,110. Two expected-red controls now pass and their stale roster rows are removed while both witnesses remain executing permanent regression controls:witness_overcommit_fails_conservationanddoc_graph_registered_plan_roots_all_admitted. The satisfied registered/admitted-rootGuaranteeStallretires with its row.The realization keystone’s branch-only
RuntimeErrorwas repaired by #9259 before landing. Required-floor run32936021845on composed head1fa238ddf09measuredgunbc.test.claim.realization_attempt_keystone_test.witness_planted_minimal_module_emitspassing in 2,779ms. Its provisional expected-red, non-verdict, andGuaranteeStallrows are therefore absent; the witness remains executing as a permanent regression control.The composed run completed
planned = executed = terminal = 12,295with six ordinary failures, 44 CPU interruptions, and two completed-over-cost outcomes. The realization identity passed; the six failures are the remaining attributed external-model, observation-lockstep, operation-argv, and accumulator-control findings, not regressions in the realization repair.Landing state — current main composition
Main has been carrying fifteen failing facts that nothing runs, and
DeclinedLiveTreeis why nobody knew. This cut exposes them by moving 782 identities from discovered-and-declined to executing. Those fifteen executing identities are temporarily pre-forgiven throughv2.workflow.floor_expected_red; they are not skipped and are notknown_red_proberows. Each continues to execute,Bool(false)holds its declared debt, and a repair producesNowPassingand forces roster removal.Run 32882641450 first measured the residual as 17 failures. Two accumulator controls are separately owned analyzer/floor-envelope findings and are excluded from this cut's debt population. The remaining split, independently verified against the changed-file set, is:
Main is green only because those carriers remain in
DeclinedLiveTree. None of their carriers is modified by this PR: the deletion changes reachability, not subjects or assertions. This is the delete-first census working as designed—not fifteen regressions caused by the cut.Ten owned obligations behind the fifteen identities
test.claim.doc_reachability_witness.doc_graph_has_no_orphan_docs;v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_orphan_docs; composite projectionv2.test.lens_doc_reachability.doc_reachability_test.doc_graph_is_cleanNowPassingtest.claim.doc_reachability_witness.doc_graph_has_no_dangling_links;v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_dangling_links; the same composite clean projectionNowPassingtest.claim.doc_reachability_witness.doc_graph_registered_plan_roots_all_admittedv2.test.claim.enforcement.lens_module_gate_witness.lens_closure_question_zero_holds_live;.lens_module_gate_holds_live;.question_zero_verdict_live_holdsv2.lens.mandatory_tag.corpus_scan_witness_test.corpus_live_clean_tree_wall_holdsv2.test.execution.emit_ingest_grammar_relation_round_trip.same_grammar_parse_ingest_bridge_holdsv2.test.execution.self_host_candidate_generation.candidate_generation_translate_self_emit_dag_add_slice_holdsv2.test.lens_non_fold_residue.non_fold_residue_test.non_fold_residue_no_unrostered_or_stalev2.test.lens_test_migration_debt.test_migration_debt_test.retained_rust_kernel_wall_holds_against_live_treeThe composite doc-graph identity projects two facts and is enrolled once; it does not create an eleventh obligation. Repairs are deliberately outside this PR so the root deletion remains reviewable and each finding keeps its own owner and remedy.
Landing qualification
The evidence base guards again because the 782 identities execute and every terminal outcome remains typed. Fifteen of those identities are pre-forgiven while their ten underlying obligations are repaired; this is visible debt, not green evidence and not a second decline. A fresh run on the current-main composition is required before readiness.
Residual result
Current-main refresh: after merging main at
2372178f20e, run 32761519653 demonstrated the newly landedRouteGapFreezeIntersectionwall on four identities added by main's 16-rowshell.Execroute-gap chunk. Those four stale freeze rows are retired atd8363d1aea8, with all siblings preserved.The next execution, 32768782787, closed planned = executed = terminal = 11,747 and measured 11,280 passed, 25 semantic failures, 5 unenrolled route gaps, 198 held route gaps, and 0 stale route gaps. It is also the first execution-grade evidence on a tree containing the four-row freeze retirement: other contemporary runs stopped in preparation, while this one projected and terminally folded all 11,747 identities.
The five new gaps—three effect-plan Bash rows and two stdin-fidelity rows—each formerly appeared as semantic false but reached
Run / NoMockResponseafter main deleted the shell mock. That transition is from a verdict to no verdict: the hermetic strategy is not applicable at the effect boundary, rather than the assertion being malformed or false. Typed route-gap enrollment records that different state and its different remedy; it does not paper over five semantic defects. At branch head86417a743f6, the full named denominator is 203 derived route-gap identities (main at the compared point carried 110), with route gaps ∩ freeze = 0, route gaps ∩ live expected-red = 0, and live expected-red ∩ freeze = 0.The residual is population churn, not a simple shrink from 28 to 25: 23 failure identities are shared; the five Bash/stdin identities left the failure set for typed route-gap; and current main added two failures (
duplicate_definition_in_one_module_is_refusedandretained_rust_kernel_wall_holds_against_live_tree). Thus28 - 5 + 2 = 25, with every movement named.This cut converts 782 live-tree identities from discovered-and-declined into executing ones, and doing so surfaces 28 pre-existing failures, itemised in the identity-grain triage below: 18 category-(i) live findings, 7 category-(ii) wet/wrongly-authored probe rows, and 3 moved-subject rows that produced no verdict and were deliberately not enrolled as expected-red. None is repaired here; making these previously unwatched facts visible is the change's result.
Run 32734768389 closed the ledger exactly: planned = executed = terminal = 11,690; passed 11,232; known-red held 55; failed 28; interrupted 49; completed-over-cost 2; known-red runtime-errored 142. Route gaps are fully accounted: unenrolled 0, held 182, stale 0.
Against the preceding execution run, planned/executed/terminal and passed are identical. The only failure movement is exactly the intended disposition change: failures 48 → 28 and known-red-held 35 → 55, accounting independently for the 17 moved-subject enrollments plus 3 primitive controls made live. This is a same-population determinism receipt, not merely two nearby totals.
Summary
RequiredFloorDisposition.DeclinedLiveTreefrom the.dagauthority and Rust realizationlive_tree_disposition,reads_live_tree_effective, andwitness_file_from_source; they still own affected-set eligibility and discoveryWhy
Hermetic checkout reads are deterministic input access. The old site-projection arm predicted hermetic eligibility from a file declaration even though the interpreter already classifies actual host effects per identity. Nothing replaces the deleted planner-time classification: genuine gaps remain typed
HermeticHostEffectRefusedroute gaps.Measurement status
Draft while the pull-request witnesses workflow measures this behavior change on the actual self-hosted CI runner class. The prior execution measurement is run 32345970386: 626 of approximately 783 newly admitted identities passed; the remainder reached genuine effects without hermetic routes. This PR's CI result will supply current wall-clock, executed identity, route-gap, and phase-limit evidence before readiness.
Checks
cargo fmt --all --checkgit diff --checkIndependent decline evidence
PR #9098 independently establishes that the separate long-home decline currently hides a live semantic red. It is evidence about that lane, not this population, but it shows that declining before execution can conceal defects rather than merely defer coverage. The newly admitted live-tree population may likewise expose semantic reds; such a red is an expected and welcome finding by this cut, not evidence that routing the witness broke it.
Self-hosted CI measurement
Draft run 32721781133 on
srv4-03measured the required CI step at 60m39s (11:28:02–12:28:41 UTC); the floor itself ran for approximately 50m13s. The 180-minute job limit was not approached, but this exceeds the cited 30–50 minute historical range at its upper edge. There is no back-to-back same-runner baseline, so sccache warmth and runner contention confound attribution.The identity ledger closed exactly: offered 12,245; routed/planned/executed/terminal 11,690; declined long 546; declined fixture 9. Outcomes were 11,232 passed, 35 expected-red held, 48 semantic failures, 49 interrupted before verdict, 2 completed over the cost requirement, 182 route gaps (88 unenrolled and 94 held), and 142 enrolled expected-red identities that runtime-errored. The floor failed truthfully rather than timing out, and all three receipt artifacts uploaded.
This PR remains draft pending triage routing and landing sequencing; it is not proposed as merge-ready from this measurement alone.
Cost disposition
Wall-clock is not a blocker: 60m39s is the measured required-step total against the workflow’s 180-minute hard limit. It is not a measured delta. No back-to-back same-runner baseline exists, so the comparison with historical 30–50 minute totals is confounded by sccache warmth and fleet contention and must not be quoted as attribution to this deletion. The actual blocker is the truthful terminal ledger: 48 semantic failures, 88 unenrolled route gaps, 49 interrupted identities, and 142 expected-red runtime errors, all triaged in PR comments.
Below-baseline compiler-floor regressions exposed
Three newly executing controls show primitive calls with an extra argument, a missing argument, and a wrong-typed argument all being accepted at compile time. DESIGN §4b states: “gunbc must first hold the ordinary compiler floor — names resolve, applications bind in exact bijection, values inhabit declared types, fields exist, closed variants eliminate exhaustively — and a failure there is a below-baseline safety regression, never compensated by higher-order capability.” These three application-bijection failures are the headline finding from the cut and are routed to the existing compiler-floor application/type-wall lanes; they are not repaired here.
Their identities were already enrolled in expected-red chunk 21; this change only removes the liveness exclusions whose written restoration trigger is deletion of
DeclinedLiveTree. They now execute as live expected reds and are held. When the assigned primitive-contract wall lands, the same probes will flip toNowPassingwithout a new probe being authored—the §4b(4) evidence already exists and guards the transition.Existing
sole_constructoraudit becomes executing evidenceThe six failing audit rows cover f10 order-sensitive ambiguous selection, f13 unwired variant construction, and f19 the unrefused default-value position. DESIGN §4b already records those three structural holes from targeted grep with zero live exposure. This run does not invent a new class; it converts the authored/grep-established claim into executing measurement, which is the evidence climb §4b(1) requires. The gap analysis’s “0 live exposure” wording now needs review by its owner; this PR flags that stale statement and does not edit their authority.
Wrong-symbol binding finding
Two independent tests (
lever_a_local_receipts_holdandlens_closure_question_zero_holds_live) use a bare-name call intended for an imported function, but resolution silently binds the enclosing test itself and recurses to the depth limit. Probe authorship made the collision possible, but silent wrong-symbol binding with no diagnostic is a compiler name-resolution finding in its own right, not merely authoring debt. It is separated for routing and not repaired here.Cross-run identity confirmation
The older duplicate draft #8977 independently reproduced the same fixed populations across two bases: 48 semantic failures, 49 interruptions, 88 unenrolled route gaps, and 2 completed-over-cost rows. Its declaration-grain join resolved all 24 modules carrying the 48 failures and found
ReadsLiveTreeon 24/24, with zero counterexamples and zero unresolved modules. Thus the failures are measured members of the population whose decline this PR deletes, not unrelated failures that merely appeared in the same run. #8977 is being closed in favor of this fresher measurement branch.Triage dispositions added here
The landing precondition was revised from seven expected-red enrollments to two on execution evidence. Run 32768782787 observed
Bool(false)forlegacy_test_behavior_unclassified_frontier_is_zeroandduplicate_definition_in_one_module_is_refused; those two are enrolled in this change. The five self-host behavioral identities from the same admission join instead producedNO-ROUTEand were already enrolled in the route-gap roster, where they remain untouched. Enrolling them expected-red was refused because it would fabricate semantic verdicts that never occurred and manufacture a route-gap ∩ expected-red contradiction.The 88 newly observed route gaps are enrolled by identity together with the interpreter-observed operation and typed ground; a later operation or remedy-ground change blocks rather than being absorbed by an identity-only row. Their distribution matches the prior wet-effect measurement and contains no ordinary committed-checkout read.
Of the 20 moved-subject rows, 17 reached their subjects and returned
Bool(false); they are enrolled expected-red so they continue executing while their owners re-establish the assertions, and the stale-row wall will demand removal after repair. Three produced no verdict—two accumulator-copy rows could not resolve their scanner andcost_coverage_unknown_fractiondivided by zero—so they are deliberately not called expected-red and remain expectation/probe repairs.The 17 held rows have a dissolution mechanism but currently no assigned repair owner; absent explicit routing, they are held indefinitely rather than scheduled work.
Construction wall demonstrated on the real cut
Run 32730435751 stopped before identity execution because
expected_red_freeze_intersectionfound six identities simultaneously asserting live expected-red execution andLegacyFrozenPathDeferralnon-execution. The wall refused at the first point the contradiction was decidable, with an authorable, located, counted diagnostic naming the six identities and head. This is an executed construction-wall red on the real change, not a fixture.The run also settled which fact was stale: these identities had already executed and answered false, so their freeze rows no longer protected any deferral. The exact six rows were retired while all non-colliding siblings at the three partial entries remain frozen. This follows the freeze authority's established 2026-08-19 remedy for the same contradiction (38 identities across 24 entries), rather than introducing a new disposition.
The other 11 newly enrolled expected-red identities have an empty join against the freeze roster. A second identity join found 19 typed route-gap enrollments still frozen. This is the more serious finding precisely because no wall reported it: absent the manual join, 19 identities would have silently retained incompatible declarations with no mechanism that noticed. The loud six-row contradiction demonstrated a working wall; the silent 19-row contradiction demonstrated a missing one.
A route-gap identity did not produce a semantic verdict, but that is not what the freeze row asserts.
LegacyFrozenPathDeferralsays path policy leaves the identity never routed. An interpreter-observed typed refusal proves the identity was routed, planned, and executed to its effect boundary; reaching that boundary is execution even though refusal there yields no verdict. The run therefore falsified the freeze fact, and the exact 19 rows were retired while non-colliding siblings remained frozen.At head
625e0c15fe8, the achieved invariant is: the freeze, live expected-red, and typed route-gap witness rosters are pairwise disjoint. Its hand-verified evidence is17 expected-red additions ∩ freeze = 0,88 typed route gaps ∩ freeze = 0, and88 typed route gaps ∩ live expected-red = 0. Only the expected-red/freeze pair currently has a construction wall, so this state is established but not fully guarded. Follow-up rownode://adhoc-185e69b4-818specifies the bounded repair: enforce pairwise disjointness of all three rosters; it is not implemented in this PR.\n\n### Inherited preparation refusal after main advanced\n\nRun 32782015417 (head
bec89a2) cleared parse, regeneration, and v2 emission, then refused during floor preparation on four unresolved references ingunbc.systemctl_show_read:systemctl_show_property_path,systemctl_show_property_service,systemctl_show_property_read_ssh_argv, andsystemd_property_capture_from_outcome. This is inherited semantic merge skew between #9057 (21f48af, which totalized the transport interface and removed the old helpers) and #9062 (bc992db, authored against the earlier carrier and adding call sites that depended on those helpers). Both changes were individually coherent; their squash-merged file retained the new call sites without the declarations, with no textual conflict. Main remains green only becauseDeclinedLiveTreedeclines this carrier. This cut makes the pre-existing does-not-resolve-or-prepare defect visible; it is not a semantic red, cannot honestly be roster-enrolled, and is being repaired separately underadhoc-644c300a-f07rather than absorbed here.\n\n\n### Current-main execution receipt\n\nRun 32794539384 atc191626cleared parse, regeneration, v2 emission, and preparation, then executed the full identity population:planned=executed=terminal=11828. Outcomes werepassed=11483,known_red_held=48,failed=27,interrupted_before_verdict=49,completed_over_cost_requirement=2,route_gap_held=203,route_gap_unenrolled=1, andknown_red_runtime_errored=15. The sole unenrolled route gap wastest.claim.claude_sdk_parser_drop_live_witness.witness_wet_receipt_control_response_parser_drop_holds, observed atRead / NoMockResponse; headfb6785benrolls that typed no-verdict fact. The 27 semantic failures and 15 runtime errors remain separately reported evidence populations rather than being absorbed into route-gap or expected-red dispositions.\nCurrent 27-failure identity adjudication (run 32794539384)
No row below is absorbed merely because it is red. Real-defect rows remain blocking findings pending named owners/follow-ups; wrong-witness rows require repair or deletion, not expected-red enrollment.
test.claim.doc_reachability_witness.doc_graph_has_no_orphan_docstest.claim.doc_reachability_witness.doc_graph_registered_plan_roots_all_admittedtest.claim.doc_reachability_witness.doc_graph_has_no_dangling_linkstest.claim.lever_a_local_receipt_witness.lever_a_local_receipts_holdtest.claim.quarantine_probe_disposition_witness_test.every_quarantine_probe_derives_exactly_one_dispositionDeclinedLiveTreedisposition.test.claim.quarantine_probe_disposition_witness_test.every_supplied_population_is_load_bearing_on_the_live_claimtest.claim.quarantine_probe_disposition_witness_test.the_live_tree_declined_row_is_the_one_the_floor_declinestest.claim.sole_constructor_completeness_audit_probe.f10_direct_selected_sealed_type_refusestest.claim.sole_constructor_completeness_audit_probe.f10_direct_selected_open_type_is_cleantest.claim.sole_constructor_completeness_audit_probe.f10_neither_direct_ab_at_least_one_violationtest.claim.sole_constructor_completeness_audit_probe.f10_neither_direct_order_independenttest.claim.sole_constructor_completeness_audit_probe.f13_variant_construction_refusestest.claim.sole_constructor_completeness_audit_probe.f19_record_lit_default_value_position_refusesv2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_orphan_docsv2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_dangling_linksv2.test.lens_doc_reachability.doc_reachability_test.doc_graph_is_cleanv2.lens.mandatory_tag.corpus_scan_witness_test.corpus_live_clean_tree_wall_holdsv2.test.lens_non_fold_residue.non_fold_residue_test.non_fold_residue_no_unrostered_or_stalev2.test.claim.complexity.accumulator_copy_roster_gate_std.roster_std_render_repeat_string_bootstrap_within_ratchetv2.test.claim.complexity.accumulator_copy_roster_gate.red_control_planted_copy_still_alarmsv2.test.claim.enforcement.cost_coverage_witness.cost_coverage_unknown_fraction_is_derivedv2.test.claim.enforcement.lens_module_gate_witness.lens_closure_question_zero_holds_livev2.test.claim.enforcement.lens_module_gate_witness.lens_module_gate_holds_livev2.test.claim.enforcement.lens_module_gate_witness.question_zero_verdict_live_holdsv2.test.execution.emit_ingest_grammar_relation_round_trip.same_grammar_parse_ingest_bridge_holdsv2.test.execution.self_host_candidate_generation.candidate_generation_translate_self_emit_dag_add_slice_holdsv2.test.lens_test_migration_debt.test_migration_debt_test.retained_rust_kernel_wall_holds_against_live_treePartition: 21 real defects, 6 wrong witnesses, 0 newly enrolled expected reds. Owners and dissolution triggers are intentionally not invented; product direction is routing the real findings before any enrollment.
The 49 interruptions are non-verdict cost facts
All 49 are
Cpubudget refusals against the 5-second per-identity ceiling; none is classified or enrolled as an expected red. The identity families are accumulator-copy (10), grammar-coverage (13), cost-coverage (4), enforcement-inventory (7), enforcement-live (6), realization-vocabulary containment (4), and five other corpus lenses. Reported costs range from the 5-second interrupt boundary to at least 38.714 seconds; the ledger correctly calls the true terminal cost unmeasured because execution was preempted. Their remedy is cost reduction or a separately admitted lane with an explicit ceiling, not semantic-red enrollment.The parser-drop
Read / NoMockResponseroute gap is likewise a non-verdict. Its dissolution trigger is a published hermetic Read mock/fixture for the committed receipt or a separately admitted wet lane. Its owning repair lane is not yet assigned and must be named before this draft is proposed for landing.Adjudication applied at head
562ed3dThe 27-row census is not being converted into 21 new expected-red enrollments. The landing treatment is narrower:
sole_constructor_completeness_audit_proberows are enrolled against the authority and next-rung triggers already written in DESIGN §4b and compiler-guarantee gap-analysis item 28. This PR is the single deletion item 28 names as restoring their execution; when each compiler wall lands, the probe passes and the stale-row wall demands removal from the roster.DeclinedLiveTreeare repaired in this change: the live holder population is now empty, the mutation control covers the three populations that remain live, and the former declined specimen is asserted as the observed expected-red identity it now is. The survivingLiveTreeDispositionscan is explicitly retained only as an affected-set-selection control.roster_std_render_repeat_string_bootstrap_within_ratchetandred_control_planted_copy_still_alarmscalled a scanner absent from their loaded execution index;cost_coverage_unknown_fraction_is_deriveddivided by zero. Their stale freeze rows and the obsolete offline recipe reference delete in the same change; every sibling remains frozen.loyal-lynx-169as compiler-floor name-resolution defects.git diff origin/main...HEADcontains no doc-reachability or doc-graph carrier. They are routed main-side rather than attributed to this cut.interrupted_before_verdictis gating, not diagnostic-only:required_floor_outcome_is_cleanrequires that collection to be empty. Therefore the 49 CPU budget refusals remain a separate blocking budget decision—reduce their cost or admit an explicitly costed lane—not correctness failures and never expected-red rows.The parser-drop route gap is owned by this lane. Its trigger remains a published hermetic Read mock/fixture for the committed receipt or a separately admitted wet lane.
Budget producer classification
The 49 CPU refusals are genuine pre-verdict safety interruptions, not completed witnesses crossing the diagnostic cost line. The typed producer chain is
InterpError::EvalBudgetExceeded→ClaimOutcome::BudgetInterrupted { elapsed_at_least_ms, ... }→ClaimTerminality::SafetyInterrupted. The evaluator returns at the cooperative deadline; the measured CPU is therefore a lower bound on cost-to-verdict and no semantic verdict exists.This is distinct from both completed-cost states. A witness that finishes past a safety requirement retains its verdict as
CompletedOverBudgetand gates throughcompleted_over_cost_requirementwith an exact duration. Independently,over_cost_line_diagnosticapplies only toVerdictReachedexact measurements against the retired 1552ms calibration line and never gates;SafetyInterruptedis explicitly false for that predicate. The three states and remedies are therefore preserved rather than conflated. The interrupt gate is correct, and acquisition reshaping/shared computation remains the only honest road; this PR does not alter classification or budget.Red that arose while declined
test.claim.doc_reachability_witness_test.doc_graph_registered_plan_roots_all_admittedis red on current main while still invisible to the required fold because its carrier declaresReadsLiveTree. This is not an assertion that was already red when declined: it went red during the decline after the 2026-08-24 docs/probes bankruptcy deleted the documents named byhand_authored_doc_bind_incomings. ThoseProbeDocbinds are now orphaned;admitted_extra_rootscounts only roots present in the document universe, so the witness’sadmitted == passedequality fails. The deletion in this PR will surface that pre-existing main defect; it does not cause it. Repair owner:clever-bear-323, classifying each remaining bind as rehome or delete. This PR neither repairs nor enrolls the row.Landing guarantee and bounded predecessor bar
This cut guarantees:
planned == executed == terminal;It does not guarantee that every semantic witness returns true before the cut may land. A malformed observation subject blocks; a coherent subject producing a valid negative observation receives an exact executing disposition.
The bounded predecessor bar is A + B: (A) accumulator finding-vs-analysis standing (#9179 plus this PR’s census retirements/rung-drop declaration), and (B) the 19 stale
ProbeDocbinds removed by #9181/#9183, verified on the composed candidate by both identity differences being empty: registered roots − admitted roots, and admitted roots − registered roots. Scalar equality is insufficient.doc_graph_has_no_orphan_docsanddoc_graph_has_no_dangling_linksare measured on the composed candidate. A still-failing row is enrolled as an executing expected-red with its exact then-live cause population, owner, and dissolution trigger; a passing row is discharged with no enrollment.Accumulator census disposition measured before deletion
Direct wet execution at accumulator-standing head
8ee84122used a fixed five-minute per-identity measurement window. Five rows returnedBool(true): machine-code (~62s), compile-stage (~84s), glob-discovery (~11s), lens-cost-model (~21s), and std-change (~275s). Two returnedBool(false)and were classified through the typedRosterStandingproduct rather than treated as undifferentiated reds: lens-traversal and Lean are bothFindingNotEstablishedplusAnalysisNotEstablished, now located asSourceParseRejected. They were not delivering coverage, but the causes differ in standing. Both live subjects are inside the required production parse sweep and parse clean on green main, while the accumulator lens returnsSourceParseRejected. Lean (991 lines) and the accumulator analyzer (865 lines) therefore remain as two typed coverage-debt rows owned by the accumulator-lens grammar. Their shared next-rung trigger is ‘the lens parses what the production parser accepts.’ The broad 28,391-diagnostic run used/usr/local/bin/gunbcbuilt 2026-08-18, predating current resolver behavior, and is not evidence about either subject. Rebuilding from this exact head collapses that output to a pre-executionWholeCorpusCompileBudgetBelowMeasuredDemandrefusal (7,053,705,216 B readable versus 7,516,192,768 B measured demand): zero diagnostics were emitted because no compile started, not because the corpus was measured clean. Three entered evaluation but returned no verdict within the fixed window: std-algebra, Bash, and Swift. They remain cost/non-verdict facts; no semantic disposition is inferred.The declared rung drop therefore distinguishes an exact measured population: five proven live guards, two retained typed lens-coverage gaps, and three bounded non-completions. Removing ten corpus-reading identities does not imply ten guards were lost, and it does not imply the post-cut corpus is clean. The unguarded exposure after removal is every module until ingestion-time per-module standing exists.
Orphan-doc expected-red and adjacent count evidence
doc_graph_has_no_orphan_docsremains an executing expected semantic red.Bool(false)holds it;Bool(true)is NowPassing and demands removal; runtime error, route gap, or interruption is no semantic verdict and cannot hold it. The count does not decide this disposition.The completed floor ledger separately carries a typed, located, non-blocking orphan-count observation attached to the exact candidate tree. Its identity standing is explicitly unobservable at this boundary: it reports magnitude and does not establish which documents are orphans. An unchanged count is not evidence of an unchanged population. Identity substitution remains unobservable. No numeric literal is authored as a gate or ratchet.
No subject-bound accepted-main orphan-count receipt store exists. Consequently movement is
NoPriorCountReceiptin this PR; building such a store is out of scope. A future store may distinguish unchanged, changed-with-delta, and no-prior-receipt using a subject-bound accepted-main receipt, never a source literal. The independent replicated observation at #9186 head7136eb4fa8was 33 (8 briefs, 24 plans, 1 extdeps document; sorted-list digest2144f187b0f5), but that session-local list is not transcribed into gating authority. Next rungs are an observer surface carrying exact orphan identities and a subject-bound accepted-main receipt store.Declared versus defaulted live-tree population
parse_entry_live_tree_dispositiondefaults an absent declaration toReadsLiveTree. That default is fail-closed for affected-set prediction (never prediction-skip) but the floor reused it with inverse effect (decline before execution). This PR deletes only the floor consumer;live_tree_dispositionandreads_live_tree_effectiveremain the affected-set authority. Before readiness, the 782 newly executing identities are split by carrier into explicitReadsLiveTreedeclarations versus absent/defaulted declarations, so deliberate and omission-derived declines are not reported as one population.Refreshed composed-candidate census
Run 32864137626 at head
1e7aaf3085ereached identity execution withplanned=executed=terminal=11907,passed=11573,known_red_held=55,failed=15,interrupted_before_verdict=43,route_gap_held=204,route_gap_unenrolled=0,stale_route_gap=0, andknown_red_runtime_errored=15. The interrupt movement from 49 to 43 is exactly the six redundant whole-corpus acquisitions removed by #9158. The equalfailed=15andknown_red_runtime_errored=15scalars are coincidental: an exact identity join finds intersection = 0; these are two disjoint outcome populations.Three of the fifteen failures —
doc_graph_has_no_orphan_docs,doc_graph_registered_plan_roots_all_admitted, anddoc_graph_has_no_dangling_links— are the exact measured red arm of clever-bear-323’s #9181 → #9183 → #9186 chain. A throwaway composition of current main with that chain measured the post-repair controls passing, includingdoc_graph_registered_plan_roots_all_admitted. This PR neither repairs nor enrolls those rows: duplicating the repair would collide with the existing chain, while enrolling reds already measured to turn green would create stale expectations on arrival. Condition B is re-measured only after the chain lands.Post-merge execution receipt at
63ad957Run 32882641450 cleared the merge-induced parse defect and completed the floor with
planned=executed=terminal=11926,passed=11589,known_red_held=56,failed=17,interrupted_before_verdict=43,route_gap_held=204,route_gap_unenrolled=0,stale_route_gap=0, andknown_red_runtime_errored=15. The previous fifteen semantic failures are identity-stable. Two current-mainReadsLiveTreecontrols newly enter the executing population:v2.test.claim.complexity.accumulator_copy_roster_gate.red_control_planted_copy_still_alarmsandv2.test.claim.complexity.accumulator_copy_roster_gate.a_readable_clean_subject_is_established_clean; both returnBool(false), while their sibling malformed-source typed-cause control passes. They are recorded as unadjudicated surfaced findings, not enrolled or repaired here: disposition requires reading the typedFindingStandingarm and exact cause rather than collapsing either result into a generic red.Newly observed, not newly broken
The two accumulator-control failures are first executions, not regressions introduced by this deletion.
a_readable_clean_subject_is_established_cleanwas added by #9188 (46b7a05eb9e) on 2026-08-25 and merged without ever executing because its carrier declaresReadsLiveTree; within hours, this branch provided its first floor execution and found the new control false on arrival. WhileDeclinedLiveTreestood, a control could be authored, reviewed, merged, discovered on every run, and still never guard.red_control_planted_copy_still_alarmspredates #9188 (the carrier history reaches #8050 and earlier). Its first execution here shows the accumulator lens does not detect its own planted defect. Both findings are attributed to the lens owners and remain executing observations; #9106 neither enrolls nor repairs them. The movement is 15 previously observed failures plus 2 first-ever-executed controls, not 17 failures caused by the deletion.Typed classification correction
The earlier claim that the accumulator lens failed to classify these fixtures is withdrawn. Direct exhaustive probes at
63ad957measured the clean literal asNoSuspectand the planted literal asSuspectObserved; all fiveFindingNotEstablishedcauses were false for both (BuildBuddyc22f0180-656a-4918-8828-3005366bb949). Neither control reads the filesystem. They become false only in required-floor union execution, locating the defect in closure-dependent binding/resolution or equivalent union wiring, not source classification.Pre-registered bare-name ambiguity trigger fired
The required-floor implementation names this question beside its diagnostic as “THE SILENT PICK, COUNTED”: transitively reached modules spell one bare name, the flat registry retains a precedence winner no author selected, and the code says zero would show the registry adequate while any nonzero population sizes the per-module-environment correction. Run 32882641450 measured
scopes_affected=1144 of 1523,names_total=101987, andworst_scope=129. This is exposure, not 1,144 wrong programs; compatible declarations may produce the same answer.One wrong selection is confirmed by execution: an accumulator-lens internal call supplying one argument to
arg_value_symbolselected the identity-twin declaration requiring three, producingCallContractMismatch. Five of six measured cross-twin colliding names have equal arity, so contract checking cannot detect those selections. The two controls classify correctly in their isolated entry closure and become false only under the floor union. #9106 records the fired trigger and specimen but leaves the dedicated per-module-environment correction outside this PR.Current-main run 32918791246 and owned raw-red dispositions
At the pre-merge head, the full floor closed
planned = executed = terminal = 12,052, with 11,705 passed, 72 expected-red held, 202 route gaps held, 44 interrupted, 16 expected-red runtime errors, and 11 reported failures. Two of those failure states were stale route-gap rows whose outcomes changed:frontier_cover_of_live_extdeps_tree_holdsnow returnsBool(false), whilewitness_live_roster_census_holdsisBudgetInterrupted. Their exact route-gap rows are deleted; neither outcome is relabelled.The remaining nine raw semantic failures are pre-existing, newly visible facts. None of their carriers is changed here, and they remain ordinary executing failures rather than expected-red enrolments. Four bounded
gunbc.guarantee_rung_drop.GuaranteeStallrows preserve their cause grain and exact identity populations. The carrier has no separate owner field, so each durablenext_rung_triggernames both its semantic completion condition and its reachable work-item node:node://adhoc-89fcf94a-bdd;node://adhoc-d6c03c1c-951;node://adhoc-3cb769e0-0a6;node://adhoc-a3b0e05f-374.This is a declared, bounded rung drop—not a second decline and not expected-red pre-forgiveness. Each repair lane has an exact semantic trigger; #9106 does not absorb their repairs. The current-main merge at
da11de63399preserves main’s new identity-navigation expected-red as independent chunk 27 and retains main’s removal of cited-symbol mode.Post-merge deleted-symbol-family audit
After merging
origin/mainatda11de63399, the deletion family was grepped across both current main and this candidate: removed declaration names,DeclinedLiveTree,declined_live_tree, anddeclined_live. There are zero live imports, calls, type positions, or Rust field/arm references outside files already changed by this cut. Remaining main-side hits divide into prose and dated receipts. Three present-tense annotations were rewritten to describe the fired root deletion; historical measurements, commit receipts, and frozen shrink history remain unchanged. This audit asks the resolve-level symbol question directly and does not cite the parse-clean population as evidence of absence.