Repository navigation
compute fabric design - #9604
Merged
briansrls merged 26 commits intoAug 28, 2026
Merged
Conversation
…ss-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 00b242b 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>
… 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 (b6003a4) 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>
…t, 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>
…eage 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>
… 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 107304a), 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 * 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>
…cause 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 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>
…ers (#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>
…ound (#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>
…tly 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>
…ector: 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>
…as 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, a real repair: it inferred absence from an EMPTY ERROR STRING on a failed read, so an artifact that exists and cannot be read reported the same absence as one the producer never wrote. Rung: structurally guaranteed on the source-to-.dag path for consumers that route through the folds, measured by execution at the fixture boundary; NOT structural on the emitted-Rust path; mitigatable nowhere else, since the raw operations stay callable. The remaining sites that conclude absence from a failure are enumerated at identity grain in filesystem_absence_establishment_adoption_standing -- monotone, no tree-measured ratchet. Six hermetic witnesses, SubstrateInputsOnly, green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * A successful read of an unlisted entry is a disagreement, not an absence review 57099 on gunbc#9564: filesystem_file_observation's absent arm returned the established absence and never consulted the read, so a file created between List and Read yielded "absent" while its bytes were in hand. A positive observation discarded is fail-open at the seam this module exists to close. THE REVIEW'S REMEDY IS DECLINED AND A DIFFERENT ONE TAKEN. Prioritizing the successful read lets the read decide the listing's question -- this module's own conflation turned around, since Read's success channel is exactly the one that cannot separate absent from unreadable -- and under the opposite race, a file deleted between the two calls, it reconstructs the original defect. Picking either observation as the winner fabricates one consistent world out of two observations of different instants, which is the plausible output section 5 forbids. So the disagreement is a fourth arm, FilesystemFileObservationsDisagree, whose cause carries both observations and whose remedy is its own: re-observe the pair atomically. It is deliberately not folded into FilesystemFileIndeterminate -- "I could not look" and "I looked twice and got two answers" have different remedies. Both converted consumers stop on it; the match is exhaustive, so a third consumer cannot silently inherit an arm. Two regression witnesses, and the discrimination is measured: with the absent arm restored to its three-state form, a_successful_read_of_an_unlisted_entry_is_not_ an_absence goes RED and the other seven stay green. Also, on a caution from eager-heron-604 against classifying from the call site: the codex_supervised_turn row in the adoption roster is re-grounded on the producer. extdeps.shell Test.IsFile is `test -f` whose own exit table reads `1 => Path is missing or not a regular file`, so one exit code carries missing, wrong-kind and could-not-look. The row stands, on the operation's declaration. 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: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
…itations resolve against nothing (#9529) * A removal's "still covered elsewhere" half is a citation, and prose citations resolve against nothing Nine-ish carriers named `gunbc_ci_floor_plan` as live justification for removing a check; the 2026-08-15 floor cut deleted it. Measured, the removal-justification population is three carriers, not nine — the rest are already-marked history or correct past-tense deletion records. The defect is a COMPOSITION, not a mistake. Each removal was sound when written: the drift gate left the push path (2026-07-22) because the floor still ran it; the hook was slimmed to fmt-only (2026-07-25) because CI still ran fmt. The floor cut then deleted the authority both cited. No diff was wrong and no review could have caught it, because each justification was falsified by a later change with no way to see it. What landed: - `gunbc.commit_workflow` gains `CheckRemoval` / `RemovalResidual`, so a removal's coverage claim is a `DeclarationRef` the declaration index resolves on every required parse run. Had the citation been typed, the floor cut would have refused instead of landing silently. - Deliberately NOT a join against `commit_gate_roster`'s GithubActionsCiJob enrollments: no .dag authority states which checks the required run performs (`compiler_frontend_program_status` answers NotDerivable for exactly this), so a green join would assert coverage nothing established. The ref proves the mechanism EXISTS — the wall against the deletion this class died of — and claims nothing more. - A finding beyond the brief: `.github/workflows/witnesses.yml` runs `cargo fmt` in NEITHER lane. The pre-push hook was slimmed on the stated ground that fmt remained a required CI step; it is now the only surface running fmt, and that same ruling argues at length that a hook enforces nothing. Recorded as a `RemovalUncovered` residual, countable at check grain rather than only narrated in DESIGN's re-add list. - The drift gate's claim is TRUE again by a route its prose never named (#9415's generated-artifact phase), so the brief's headline hole is closed; the stale citation was not. Evidence: three witnesses green by execution, all three flip to `false` under a mutation collapsing the classifier to answer from the row rather than descending into the residual — the total-at-the-level-examined failure this carrier is shaped to forbid. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Drop RemovalUncovered.since: it was a second copy of removed_on Review 57001 flagged `since`/`cause` as prose rather than typed reasons and explicitly deprioritized it. Reading the field turned up a sharper defect it did not name: in the only row inhabiting the arm, `since` and the row's own `removed_on` were the SAME LITERAL ("2026-08-15") — two representations of one fact with no authority saying which wins if they drift. That is the §2 redundancy this whole carrier exists to reduce, reintroduced one field in. Uncoverage begins when the check was removed, and `removed_on` already states that. A row that was covered and became uncovered LATER is a different shape; it gets modeled when a real specimen exists rather than minted now on speculation. `cause` stays prose deliberately. Typing it means a coproduct of removal causes, and a one-row population cannot establish those arms — minting them now is the re-invention §2 warns against, and the reviewer's own reasoning (that calling this blocking would recreate the tension the PR reduces) applies with more force to inventing a taxonomy from one specimen. Re-verified after the type change: all three witnesses return `true`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 57017: honest arm name, no Bool predicate, and the §4c parse break that failed CI THE CI FAILURE FIRST, because it was latent in the original commit rather than introduced by this one. `claim_executor --required-ci` parse phase refused with 15 errors: "source annotation sits inside a declaration body. Only module-item grain is modeled" (DESIGN §4c). The roster's per-row comment sat INSIDE `data check_removal_roster = [ ... ]` from the first commit. My local verification ran the interpreter, which tolerates it; the required parse phase does not. So the local green was real and strictly weaker than the gate — worth recording, because "witness returns true" and "the corpus parses" are different questions and I had only asked the first. All annotations are hoisted to module scope. Review 57017, finding 1 — the arm proved existence while its NAME claimed coverage. Correct, and the prescribed fix (a resolvable edge to the required execution authority) is not buildable: no .dag authority states which checks the required run performs, which `compiler_frontend_program_ status` records as `NotDerivable` for `SelfHostCargoPhaseEnrolled`. Fabricating that edge would be the authority substitution the carrier's own comment declines. What IS wrong is naming an arm for a rung its evidence does not reach — §4b(1) rung inflation — so `RemovalCoveredBy` becomes `RemovalCoverageClaimed`: the mechanism must exist, coverage is claimed, and the gap is in the name rather than only in a paragraph. Review 57017, finding 2 — the `*_is_* -> Bool` predicate. Correct on the repository's own terms (`v2.std.subject_evidence` class A; `extdeps.bazel.test_status`: a Bool classifying coproduct arms "destroys exhaustiveness at every call site — a tenth status would have been absorbed into false and no consumer would have been asked"). A third residual arm would have been silently absorbed. `removal_is_uncovered` is deleted and `uncovered_removals` matches the coproduct in place, so a new arm fails to compile at the site that must decide about it. The witness no longer tests a Bool predicate — that would entrench the parallel surface the fix removed. It asserts the selection and that the `cause` payload survives, which is the concrete thing predicate dissolution costs. The compiler then forced the descent it exists to teach: `selected[0]` is `Optional`, so the match must go through Present/Absent, with Absent fail-closed to false. All three witnesses re-verified: return `true`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Review 57058: the query was promoting a claim into a coverage conclusion Codex is right, and this is a fail-open I introduced rather than one I inherited. The previous commit renamed the arm to RemovalCoverageClaimed so the CARRIER stopped overclaiming, and left the QUERY doing exactly what the rename was supposed to stop: `uncovered_removals` excluded every claimed row and its own comment called it "the repository's answer to which checks are unguarded". So a mechanism whose declaration still exists while its required-phase enrollment was deleted read as guarded. That is ⊥-as-ignorance rendered as ⊥-as-answer — the empty-observation narrow DESIGN names as strictly worse than the widen §5 already forbids, because a widen is merely expensive and a narrow is silently uncovered. Fixing the arm's NAME and leaving the query's PARTITION is the same defect one level out, which is the part I missed the first time. The partition is now stated at the grain the evidence supports: `removals_declared_uncovered` and `removals_with_unverified_coverage_ claim`, which together exhaust the roster. There is deliberately no third query and no `verified covered` arm — no producer could inhabit one, since no .dag authority states which checks the required run performs, and an arm nothing can reach is the permanently-green decoration §4b forbids. Stated plainly at the call site: the COMPLEMENT of declared-uncovered is not the guarded set, and the honest count of what this repository can currently prove is guarded, at check grain, is zero. A fourth witness makes that structural rather than a paragraph: the two queries partition the roster with no remainder, so a future `verified covered` arm breaks the sum and must be reckoned with at that site instead of being added silently and quietly excluded from the unguarded answer — which is precisely how this defect arose. All four witnesses return `true`. 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>
… reach (#9513) The sibling fixture that landed with the split predicate was discriminating when written and stops being so the moment the declaration index projects variant-pattern names into `referenced` (#9504): `membership_bound_through` then finds `Accepted` unaided, and the arm goes green with the import-claim disjunct and without it. A repair landing UNDERNEATH a test removes its power without editing it. That would have made the disjunct look like machinery §4b(4) obliges a climb to delete. It is not. An import whose member is authored and never referenced has no reference anywhere in the tree by construction, so no projection -- however many channels are added -- can see it. Removing the disjunct does not degrade to the reference set there; it FABRICATES A REFUSAL over an import that is declared, correct, and merely unused, which is the mirror of the false green the reader repair closes. Measured on this tree, both arms: green (as committed) 21 passed, 0 failed red (disjunct deleted) 19 passed, 2 failed The new fixture asserts its plant before reading any disposition, so a verdict cannot be read off a delta that was never produced. 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>
…undle at the root (#9544) * A declared context window that configured nothing: the capacity bundle hid a dead field behind a live one `InferenceCapacityPolicy.max_model_len` declared 8192 and no renderer consumed it. The unit carried OLLAMA_HOST and OLLAMA_MODELS and said nothing about context, so the number stood beside a process it did not configure while both hosts served 131072 — a declaration and a running service that had never been the same fact. The bundle is why that read as fine. `shared_memory_budget_bytes` sits in the same record with no admission consumer anywhere, so the record's existence looked like a capacity mechanism while only one of its two fields could ever be causal, and the dead field sat behind the live one. It is deleted outright rather than carried forward as an optional or a placeholder admission, on the ruling that removed this module's endpoint credential: a required field with no consumer is not a placeholder for a future check. The context field was also named for vLLM's `--max-model-len` while the only modeled runtime is Ollama, whose grounded name is OLLAMA_CONTEXT_LENGTH — a parameter named for a runtime this deployment does not serve. `extdeps.ollama.server_env` grows the real upstream variable beside the two it already owns, and the gunbc-side value is a `TokenCount` from the std.measure family rather than a bare Nat. Replacement is at the root rather than layered on it. `OllamaServingLaunchProfile` carries the values the Ollama process actually consumes; `InferenceCapacityPolicy`, `SparkServingServingPolicy`, and `ServingConfigurationIdentity` are deleted. The identity went rather than gaining the missing field: it named "configuration" while covering a subset, repeated release facts, and keyed on a moving model ref — adding context would have completed a duplicate. The canonical identity of the realized configuration is already the content identity of the rendered bytes, shared by the desired and observed sides. `spark_serving_user_unit_spec_structural_hash` and its field helper are deleted for the same reason: a hand-enumerated second identity over a value whose bytes are already hashed. Nothing called them — `serving_membership` imported the hash and reconciled on the rendered content identity — so this is a dead scaffold, and the enumeration's failure mode was to report no change for a real change. The one-arm `SparkServingRuntimeKind` goes with the seed that was its only reader. 131072 is SELECTED here as the migration decision. The wet `/api/ps` reading of `context_length: 131072` on both hosts is its evidence, not its source: observed state does not become desired state, and the previously inert 8192 must not become authoritative merely because the renderer gained a consumer. Making the carrier causal at the stale value would have shrunk the live window 16x on first converge. The new witness states the causal link as a discrimination in both directions: two windows must not render the same bytes or the same content identity, and the desired unit is the one rendered at the declared window and not at any other. Every arm is red against the pre-change tree. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * The window datum is a TokenCount at its source, not a Nat wrapped one line later Review 57042 caught the one raw-scalar seam the rest of the diff had already closed: `spark_serving_desired_context_length` carried token-count semantics in its name while holding a bare `Nat`, and was lifted into `TokenCount` by the profile constructor immediately below it. Every other carrier and parameter on this path — `OllamaServingLaunchProfile.configured_context`, `SparkServingUserUnitSpec.configured_context`, `ollama_context_length_env_assignment` — is already `TokenCount`, so the wrap was the only place the quantity existed untyped. Typing the datum removes the wrap rather than adding a conversion, and the `std.nat` import goes with it: nothing else in the module names `Nat`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Restore SparkServingRelease, which a span-delete swallowed between the two types it was aimed at CI caught what no local check did: `unresolved type 'SparkServingRelease'` and `no field 'model' on type 'SparkServingRelease'` across serving_membership, serving_converge_plan, and four witness modules. The cut that removed the capacity bundle ran from the InferenceCapacityPolicy header through the end of SparkServingServingPolicy. `SparkServingRelease` sat BETWEEN those two declarations, so it went with them. The edit asserted that the span CONTAINED both types it meant to delete; it never asserted the span contained nothing else, and a containment check cannot see what it swallowed. The type is restored verbatim. The general repair is the census now run over every edited module: enumerate the `type`/`fn`/`data` declarations before and after and diff them, so what actually disappeared is stated rather than inferred from the intent of the edit. That census over all four files reports exactly the intended removals -- InferenceCapacityPolicy, SparkServingServingPolicy, ServingConfigurationIdentity, SparkServingRuntimeKind, OllamaRuntime, the two configuration-seed functions, the runtime-kind wire, and the two spec-hash helpers -- and the three intended additions. Both approving reviews checked that removed symbols had no remaining callers. That question was the right one and its answer was true; it just could not surface a symbol that was deleted without being intended, because nothing named it as removed. The fail-closed substrate did: every real dependent refused loudly, which is the deletion census the doctrine promises. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
…in for (#9453) * Replace the credential citation with the import edge it was standing in for gunbc.tailscale_acl_phase2_credential named gunbc.auth.credentials and gunbc.auth.optional_impersonation in four DeclarationRef rows and asserted the binding with a string-equality function, while reaching those modules by no import edge at all. A DeclarationRef is inert data -- no closure follows it -- so the module this carrier depends on for its credentials entered no compile closure and was typechecked by nothing, and its own defect (a bare shell.GCloud reference with no edge to extdeps.shell) stood on main behind that silence. The check was the matching decoration: every clause compared a row's literal field against the same literal, so its RED was authorable only by editing the row it read. Permanently green by construction and cited as evidence that the credential flow bound these authorities. Construction over validation (DESIGN section 5): the binding is now an import edge, carried by the same mechanism that typechecks the calls. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * wip: author the rest of the carrier's edges * Address review 56750: de-duplicate the witness match, make the strategy match exhaustive The witness restated the predicate's own match beside a call to it. Deleted. The wildcard arm is replaced by the named GcloudCli arm so a third strategy is a compile refusal at the operator-policy site rather than a silent false. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the strategy predicate too: it had the property I deleted the others for tailscale_acl_operator_adc_strategy is a literal data constant, so a predicate matching it is green by construction and reddenable only by editing the row it reads -- the exact property for which this change deleted five string comparisons. Keeping it was inconsistent; it is a change detector, not a check. The strategy is still carried structurally: it is passed to gcp_oauth_access_token, so a value that does not inhabit GcpOAuth2AccessTokenStrategy refuses at that call. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Attach the witness annotation to its declaration The replaced comment block left a blank line before the following declaration. Section 4c admits only ATTACHED standalone leading // blocks; an unattached one refuses, which is why the witness entry started refusing before emit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore the live-write scaffold disposition my predicate deletion swallowed The deletion sliced from the annotation to design_holds, and that span also contained data tailscale_acl_phase2_live_write_disposition, so the witness referencing it went red. Restored verbatim from main, with the stale annotation that described the deleted predicate removed rather than left over it. The blank-line change in the witness is reverted: it was a wrong diagnosis of this error, not a fix for it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rebuild DESIGN.md as main's projection plus this change's paragraph The merge left DESIGN.md carrying the ours side verbatim, which drops main's authority-derived content -- what the generated-artifact merge driver warns about. Rebuilt from main's projection with the same two substitutions applied to the merged .dag authority, so the projection and its authority agree and main's new rows survive. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The witness that EXECUTES against gunbc.auth.credentials records its edge too test.claim.gcp_oauth_access_token_witness called gcp_oauth_access_token and both leaf patterns with zero import statements, reaching them through the flat whole-tree namespace. That is depended-upon-but-unimported by a live consumer rather than by a prose row -- the same accidental pool coverage this change repairs in the carrier, in the worse place. Measured before adding the edge: each of the four names is declared in exactly one module across dag/ and src/v2, so the candidate set is a singleton and the import cannot reorder a binding. No claim is made about bare-name resolution where a name is multiply declared. Found by crisp-cat-907, verified by swift-badger-524, routed via warm-hawk-909. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The witness I said EXECUTES does not execute, and the annotation now says so first I committed this file's import edge as "the witness that EXECUTES against gunbc.auth.credentials" and opened its annotation with the same claim. I never measured it. Measured now: 0 test fn, so floor discovery folds nothing from it; no importer, so the support-module pattern that legitimises a zero-test-fn file does not apply; no live_tree_disposition, so the fail-closed default would decline it anyway. Eleven plain fn reachable by nothing. Asserting execution without measuring it is the exact failure this change is about, committed one level up: the PR's thesis is that a DeclarationRef creates no edge, so a module cited that way is inert data dressed as an authority, and I then offered inert evidence as proof of the repair. Found by smart-ram-730. The prescribed repair is NOT applied, because it would declare something false. Converting to test fn under SubstrateInputsOnly would enroll assertions whose leaves are host effects: both roll-ups call gcp_oauth_access_token_via_gcloud, whose body is shell.GCloud.AuthPrintAccessToken(), and the ADC leaves declare uses net: std.resources.Network. Run directly, the gcloud leaf answers Unimplemented { what: "unknown service operation: shell.GCloud.AuthPrintAccessToken" } -- the call exists and nothing is behind it. Enrolled that way it would be refused at the hermetic boundary, counted executed, assert nothing, and carry a _test.dag name so BarrenTestSidecar vouched for it: a silently inert witness converted into a loudly enrolled one, which is the decoration DESIGN 4b calls worse than absent. smart-ram-730 verified this and withdrew the prescription. So the annotation states the NO-ROUTE fact positively and first, rather than by omission, and names what would actually make it execute -- modeling the gcloud service operation, or restructuring onto a subject with no host effect. Neither is done here; both are a different lane from a citation repair. The import edge stays. It is a fact about REFERENCE, not execution: this module names those symbols and resolved them through the flat whole-tree namespace, so it was depended-upon-but-unimported regardless of whether its assertions ever run. The file is pre-existing (2749a44, #6165) and carries these properties on main unchanged; this commit does not fix that and does not claim to. * The Unimplemented receipt was measured before the import edge existed, so it described a module this file no longer is I put a stale measurement into the commit that was correcting a false claim. The annotation said the gcloud leaf answers Unimplemented { what: "unknown service operation: shell.GCloud.AuthPrintAccessToken" } and concluded "nothing is behind it". That reading was real, but it was taken on main at dabe4c5 -- BEFORE this file had import extdeps.shell in its closure -- where the operation could not resolve at all. Carried across that boundary it described a module this file is no longer. Executed with the edge in place, both roll-ups DISPATCH: ◐ started shell.GCloud.AuthPrintAccessToken cause: TypeError { msg: "failed to execute 'gcloud': No such file or directory (os error 2)" } and the swapped roll-up first performs two real reads of ~/.config/gcloud/application_default_credentials.json. So the service operation is modeled and live; these entries execute a process exec and a file read, and fail only because the runner lacks the binary. The conclusion the stale receipt was offered for happens to survive unchanged -- SubstrateInputsOnly is false either way, and now for a stronger reason: not "the leaf is unreachable" but "the leaf demonstrably performs host effects". That is precisely what made it invisible. A false premise under a correct conclusion produces no contradiction to trip over, so nothing forced a re-read; the argument looked sound because it was sound, on the wrong evidence. Also corrected: "what would make it execute" named modeling the gcloud service operation. It is already modeled. What is missing is a subject with no host effect, or a disposition that admits one. Found by running the two roll-ups rather than re-reading the code -- the same instrument that produced the stale number, pointed at the current tree. --------- 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>
…ted, counted refusal (#9466) * Surface #9439's two failing dispositions as typed diagnostics, and split variant delegation out of registry-absent REBUILT ON MAIN'S CONSTRUCTION. gunbc#9439 landed the per-candidate disposition twelve hours ago -- CandidateSurvived / CandidateOwnModule / CandidateRegistryAbsent / CandidateExportProofFailed, with a census and a row at (module, name, disposition) grain. My branch carried an independently written classifier with the same four arms; it is DELETED rather than merged, because two authorities for one decision is the section 3 violation and theirs is on main. WHAT #9439 DID NOT DO, by its own note: the census 'is NOT SURFACED during an ordinary build'. So the two FAILING arms still vanished from the emission -- no diagnostic, no location, nothing a build reports. That is the empty-observation narrow: the emitter answers 'this name is not part of the interface' where the truth is 'I could not prove that it was', and DESIGN rates a narrow strictly worse than the widen section 5 forbids, because a widen is merely expensive and a narrow is silently uncovered. reference_derived_row_diagnostics is a THIRD projection of rows that already exist, beside the use-lines and the census. Nothing re-derives the disposition, so the emitted crate cannot move. TWO diagnostics, not one carrying a cause (ruling: warm-hawk-909 via smart-ram-730). Registry-absent is fixed by AUTHORING AN IMPORT; export-proof-failed is fixed by making the emitter able to prove an export the provider already holds. Opposite remedies, different owners, different populations, potentially different reachability. DESIGN 4b files one row per class. THE FIFTH ARM, and it exists because it was MEASURED. A census of the failing arms over the regen seed closure returned a population dominated by bare VARIANT names -- Absent, Cons, Eq, ExprCall, Bind -- all landing in CandidateRegistryAbsent, because the registry holds declarations and a variant is not one. #9439 filters candidates by `already` and is_kernel_type only, with no variant filter ahead of the disposition, so its registry-absent column counts mostly names already correctly bound. THE ARM CARRIES ITS PARENT, and that is the design rather than a detail. The tempting shape -- one arm meaning 'variants need no import' -- is FALSE and reproduces the same conflation one level down: a variant whose parent is declared here is bound by the module's own use-glob and owes nothing, while a variant whose parent lives elsewhere needs that PARENT imported. Opposite remedies. So the arm claims the obligation is DELEGATED and names the delegate; the parent then answers for itself as its own candidate row. Objection raised by smart-ram-730, who was right that my first shape repeated the defect it was fixing. NOT ESTABLISHED, and said so on the carrier rather than assumed: delegation is sound only if every parent named by a routed row is itself a candidate. That check is mechanical and is the arm's next rung. Witness: #9439's census witness extended -- the fifth arm's discriminating RED (red against the four-arm classifier, green against five), a positive control that a non-variant still answers registry-absent, and three tests over the diagnostics (only the two failing arms produce any, both advisory, opposite remedies in the text). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix two refusals from the first gen-0 compile: ModuleEmission field and the TypeSummary import path Both caught by execution rather than review: the emitter refused with 2 hard diagnostics before writing any candidate tree. - emit_module_full built a ModuleEmission without import_refusals after the type gained the field. - the census witness imported TypeSummary/EnumRepr from v1.compiler.emit_info, which is not the module's declared name; it is v1.compiler.infer_emit_info. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Install the regenerated mirrors and the cli_run arms they make compilable The seed mirror is a TWO-FILE change for a new 00_core coproduct variant -- declaration in v1_std_core.rs, exhaustive match arms in cli_run.rs -- and the two are circularly ordered: the arms name variants the committed mirror does not carry, so generation 0 stops building the moment they land alone. rustc reports E0004 against the CONSUMING file, which points away from the missing half. Mirrors regenerated by generation 0 from the edited .dag; three files drifted, including the emitted census witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Add the two cli_run match arms the regenerated mirror makes compilable Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Surface only the export-proof arm as a diagnostic: the registry-absent population is target-language tokens THE CENSUS RAN, on the rebuilt construction, over the regen seed closure (claim_executor --required-regen --source-root dag --source-root src/v2, whose subject is regen_input_sources grown to a joint fixpoint over import, dotted-reference and bare-reference edges). Two arms instrumented, generation 1: export-proof-failed 0 registry-absent 473 rows, 63 distinct names, 110 modules AND READING THE 473 DECIDED THE DESIGN. The top of that population is Vec 88, bool 73, Option 50, i64 48, empty_map 33, then BTreeSet, Fn, fn, u8, serde_json, '_' and '-'. Those are RUST TARGET-LANGUAGE tokens, proposed by the candidate walk's emitted-source arm, which tokenizes the module's own emitted Rust and offers every identifier in it. No .dag provider can ever supply 'bool'. Registry-absent is therefore the CORRECT disposition for them and a diagnostic would be a false report in nearly every row -- printed on every build, in every module, forever. So that arm stays a census column. Its trigger is not a burndown of the 473: it is that the candidate walk stop proposing target-language vocabulary, after which the diagnostic can be wired with no other change. ReferenceDerivedImportProviderUnknown stays DECLARED and is produced by nothing. The class is real and its shape is settled; only its input is not yet clean. THE FLIP CONDITION IS NOW MET FOR ExportUnproven, both halves: population zero over a named closure, AND a discriminating RED authorable -- and authored -- at the fixture boundary, which is what separates 'observed zero' from 'cannot fire'. Whether it flips is warm-hawk-909's call. A REFUTED PREDICTION, recorded because it was decision-relevant and was asked for before either arm flips: registry-absent was expected to overlap heavily with UnlistedImportUse, both being described as 'referenced but never imported'. Measured on one run -- 63 registry-absent names, 36 UnlistedImportUse names, INTERSECTION ZERO. UnlistedImportUse names .dag types masked at resolve time; registry-absent is dominated by Rust tokens that never reached the resolver. They are not two views of one population, so ProviderUnknown's trigger does NOT point at the family-closure-SVN burndown as this carrier previously assumed. Witness gains registry_absent_produces_no_diagnostic, which fails the moment someone wires that arm -- the wall that keeps the false reports out. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Flip ExportUnproven to blocking (approved), both halves of the condition met warm-hawk-909 approved the flip: population zero over a named closure AND a discriminating RED authorable -- and authored -- at the fixture boundary. The second half is what separates a real wall that is quiet from an arm that has never fired, and only the first is a count. ReferenceDerivedImportExportUnproven leaves the advisory arms of is_error_diagnostic, is_interpreter_blocking_diagnostic and the discovery-corpus advisory set; the default blocking arm now carries it. ProviderUnknown stays advisory and stays produced by nothing. The emission still produces its files beside a blocking diagnostic rather than returning none: production precedes adjudication, so the candidate tree survives the refusal and the refusal is what stops the line. The carrier now records why ProviderUnknown must stay unwired in the strongest available form, which is not that its rows are unfixable: Vec/bool/Option/i64 are EVIDENCE THE CANDIDATE FILTER IS WRONG, and wiring a permanently-false report onto nearly every build is worse than shipping nothing because IT TRAINS READERS TO IGNORE THE CHANNEL. A diagnostic nobody reads is worth less than an absent one, because the absent one is honest about its coverage. Witness updated: the export-unproven diagnostic is asserted blocking rather than advisory. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the producer attribution, and make the diagnostic match wildcard-free TWO FIXES, both from clever-boar-140, who owns the coproduct. 1. MECHANISM ATTRIBUTION WAS WRONG IN MY CARRIER. I wrote that the candidate filter's emitted-source disjunct 'offers any identifier appearing in the emitted Rust'. It cannot: that disjunct is an admission GATE over an already proposed candidate list. The PRODUCER of Vec/bool/i64 is collect_item_realized_surface_names -- rust_identifier_tokens over render_rust_type -- which emits target-language SPELLINGS by construction, and reference_is_host_realized_builtin misses them because it is keyed on .dag vocabulary (is_container_type reads std.types container_type_arity), so Vec and BTreeSet, the Rust spellings of List and Set, pass a filter that exists precisely to remove host-realized names. Verified both halves against the code before taking the correction. It matters because it moves where a repair goes: narrowing the gate would delete genuine emitter-attested candidates and leave the real source untouched. 2. THE DIAGNOSTIC MATCH HAD A WILDCARD, which is the defect this change exists to repair, in the change itself. The coproduct now carries THREE not-applicable arms against two genuine drops, so a '_' makes the next drop arm silent by default -- total at the level examined, blind one level down. Every non-reporting disposition is now enumerated, so a sixth arm fails to compile here instead of inheriting 'produces no diagnostic'. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct the registry-absent characterisation: the 473 is MIXED, not all target vocabulary I generalised from the head of a sorted list -- the rule I had derived from the '-' rows this morning and then broke on the population I derived it from. deep-ant-102 pushed back on the census SCOPE and smart-ram-730 relayed it; both halves verified against the code before taking it. THE TRAP: the census invocation passes --source-root dag --source-root src/v2, but the SUBJECT is regen_input_sources, whose roots are SeedV1 and DagCorpus (cli_run regen_source_roots) and exclude src/v2 entirely -- stage0 IS the v1 seed and a seed reaching into src/v2 would depend on the successor it bootstraps toward. The source-root FLAGS and the regen SUBJECT are not the same thing. So registry-absent conflates two classes: (a) EXTINGUISHED Vec, bool, i64, BTreeSet -- no .dag declaration exists or can; render_rust_type minted the spelling. (b) OUT-OF-CLOSURE empty_map 33 (v2.std.collection), Optional 25 with Present 47 and Absent 13 (v2.std.optional) -- REAL .dag names whose providers exist and were not selected in. Verified by reading both declarations. Class (b) is precisely the closure-conditioned population this change exists to surface, sitting inside rows I had written off as unfixable. The proportion is UNMEASURED -- about twelve of 63 names were examined -- and the carrier says so rather than inferring it. WHAT DOES NOT CHANGE: the flip, which rests on an authored fixture RED and not on the zero; and keeping ProviderUnknown unwired, which is justified by class (a) alone -- a permanently-false report on those rows trains readers to ignore the channel whether or not part of the population is movable. WHAT CHANGES: registry-absent is ENTRY-RELATIVE, not a fixed target, and its trigger is now that class (a) leave the arm rather than that the whole population be dismissed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Row-count and distinct-name point opposite ways: state both, quote neither as a proportion Refinement from smart-ram-730 and clever-boar-140. My carrier said 'roughly twelve of the 63 names were examined' -- a figure I inherited rather than verified. What is actually established: BY ROW immovable names dominate: Vec 88 + bool 73 + Option 50 + i64 48 of 473. Verified here -- none of Vec, bool, i64, BTreeSet, Fn, u8, serde_json has any .dag declaration in the tree. BY DISTINCT NAME the examined sample is 4 of 63 and ALL FOUR ARE MOVABLE. Those point opposite ways, and the structure is why the population was misread twice: high-count immovable names at the head, movable names in the tail with small counts. empty_map's 33 rows were the THIRD-LARGEST count and were still classified as target vocabulary on the first pass. Fifty-nine names remain unexamined by anyone, and the carrier now forbids quoting either figure as a proportion. Also records the variant half, which is structural rather than incidental: Present and Absent are Optional's VARIANTS, so a consumer key reading a declaration index's field alone reports no-provider-anywhere for every variant name in the corpus. The key must read declared UNION variants. That reading is clever-boar-140's, recorded as attribution rather than as something this module verified. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the structural variant fact and how it composes with the fifth arm's ordering clever-boar-140 withdrew the corroboration I objected to and settled the question from the producer instead: build_item_info emits one ItemInfo per TOP-LEVEL ITEM, no arm descends into a coproduct's children, and the single item_registry insert is keyed on that name -- so a variant name is absent from the registry under EVERY closure, not merely this one. Verified against both sites before recording it. THE TWO FACTS COMPOSE, and the composition explains why Present and Absent sit under OUT-OF-CLOSURE rather than under EXTINGUISHED: this PR's fifth arm is tested BEFORE the registry lookup, so a variant whose parent is IN closure is delegated and never reaches the registry. The registry's structural inability to hold variants surfaces only when the parent is OUT of closure and type_summaries cannot recognise the name as a variant at all. That is precisely why my four names could not discriminate the variant-set reading from the closure reading, and why the structural argument was needed rather than the sample. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Regenerate the three drifted mirrors against the final head Generation 1 reaches first_generation_equal=true; export_unproven=0 and provider_unknown=0 (unwired) on the regen seed closure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * A variant whose parent is unresolvable gets its own arm, not registry-absent's name Found in review by clever-boar-140, who owns the coproduct: the Absent arm of the parent lookup handed back CandidateRegistryAbsent. Reaching it means THIS IS KNOWN TO BE A VARIANT and its parent is not established -- while registry-absent says the bare-name REGISTRY holds no entry, a statement about a different map, reached by a different route, with a different remedy. A reader auditing that row would go looking at the registry, where the missing fact does not live. Two states distinguishable at the point of collapse, collapsed anyway -- the same shape my wildcard removal one function down exists to prevent, left standing one function up. CHECKING ITS REACHABILITY SURFACED THE SHARPER HALF. derive_variant_to_enum inserts the EMPTY STRING as the parent when one variant name appears in two enums. So the lookup answers Present with a parent naming nothing, and the arm I wrote would have produced CandidateVariantDelegatedToParent { parent_enum: "" } -- a delegation to no one, wearing the very payload that was supposed to make the arm honest. That is the top-as-ignorance shape inside the fix for a conflation. That case is REACHABLE; variant-name collision across coproducts is real enough that the compiler carries a VariantCollision diagnostic for it. The Absent case is not, while both this predicate and the parent map derive from the same EnumRepr summaries -- and it routes to the new arm anyway, because a quiet guard should say what it means rather than borrow another arm's name. CandidateVariantParentUnresolved, with a census column, an enumerated no-diagnostic arm, and two witnesses: a fixture authoring the collision directly (RED against the arm-less form, which delegated to the empty string), and one asserting the disposition never reports as registry-absent. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Regenerate the stage0 mirrors for the sixth disposition arm The .dag gained CandidateVariantParentUnresolved and the variant_parent_unresolved census column after the previous regen, so the committed mirrors carried five arms where the authority declares six. Review 56923 reported this as two findings, and they are one: it names a behavioral defect (the Rust dispatch collapses the ambiguity-sentinel and Absent cases) whose cause is structural (the arm is not declared in that file at all). The distinction matters for the remedy -- a collapse is fixed by descending a match, an absence only by regen -- so anyone reading the first finding literally would have searched for an arm to split in a file whose type has no sixth arm to split. Emitted by generation 0 from 157cef3; the two drifted files are exactly the two the sixth arm touches. v1_std_core.rs does not drift, which is the expected result: the arm is a 05_emit_rust disposition, not a 00_core diagnostic variant. * Demote the export-proof refusal to advisory: its first execution over a second closure returned 87, not 0 The flip to blocking was approved on a measurement of the regen seed closure, where CandidateExportProofFailed's population is zero. The required build lane also runs a v2-emission phase over a different closure -- entry:src/v2/compiler/00_compile.dag, 169 modules -- and there the population is 87. Run 33111325404 at b331e24 refused that phase and reddened the required check. The flip condition was "population over a NAMED CLOSURE is zero AND a discriminating RED is authorable". Both halves held and the conclusion was still wrong: the zero was a property of the closure, not of the arm, and a per-closure zero licenses nothing about another closure. That is the denominator error this same carrier already names one clause down for the sibling arm -- registry-absent is entry-relative rather than a fixed target -- and the reasoning was available for this arm and not applied to it. The bounded sequence ruled for this work said count == 0 flips and count > 0 is the burndown roster at identity grain. The terminal event has fired with the second answer, so 87 is the roster and the arm stays advisory until it burns down. What the brief asked for is unchanged: the diagnostic is still typed, located and counted, so the silent omission is closed. Severity decides whether the line stops, not whether the omission is visible. The falsification is recorded in the carrier rather than the trigger being repointed, and the corrected condition is stated: the population must be zero over every closure a required phase compiles. * Name the three required closures in the carrier rather than describing them smart-ram-730's point: 'every closure a required phase compiles' is a set that moves. It grew when #9035 added the v2-emission phase and again when that phase's subject widened from dag/std/abi.dag to the v2 pipeline root. A described set leaves a future phase addition to whoever remembers; a named one makes it visibly re-open the flip question. Also records that only two of the three are measured for this arm (0 and 87), so even the corrected condition is not currently evaluable, and that deep-ant-102 delivered this exact objection before the flip and it was acknowledged and not carried. A dropped warning and a missing insight have different remedies. * Fix the carrier note's inner double quotes, which terminated the .dag string The previous commit's note embedded a quoted phrase inside a double-quoted string literal, so the parse ended mid-sentence and the module index refused the whole file. Caught by regen, five minutes into a remote build, at a byte offset 46420 that names the position and not the cause -- the error reads 'expected item declaration' because the parser was looking at prose it had fallen out of a string into. * Regenerate the mirrors for the advisory demotion Drift is exactly the two files the change touches: v1_std_core.rs carries the three severity classifiers gaining a ReferenceDerivedImportExportUnproven arm, and the witness mirror carries the _is_blocking -> _is_advisory rename. v1_compiler_emit_rust.rs correctly does not move -- the demotion is a 00_core severity fact, not an emitter one. Emitted by generation 0 from 13ea193; the run reports first_generation_equal=true after installing the candidate. * Re-apply the two diagnostic arms onto main's cli_run.rs instead of restoring a pre-merge copy The previous commit restored cli_run.rs wholesale from the snapshot taken before stripping the arms for gen-0. That snapshot predates main's change to record_from_module, which gained an &Rc<OccurrenceTransport> parameter, so restoring the whole file silently reverted main's edit to a file that had auto-merged cleanly. rustc caught it as E0061. The arms are a two-hunk addition, not a file. Re-applied onto main's version beside their sibling UnlistedVariantValueUse arms. * State that step 2 landed in the note that still called it future work reference_derived_use_lines_note described the PRE-CHANGE world inside the change that closes it: 'typed refusal at step-2 is future work', in a branch that lands CandidateExportProofFailed and ReferenceDerivedImportExportUnproven at seven sites each. A reader trusting the note concludes the wall does not exist in the PR that builds it. Found by smart-ram-730, who raised it from the opposite direction -- they read a note claiming the emission REFUSES and measured blocking=0 against it. That claim turned out to be on an abandoned local lineage rather than this branch, but reading my own note to answer them surfaced the inverse defect, which is mine and materially worse: a false 'it refuses' overstates a wall, a stale 'future work' denies one that is there. The clause now names the disposition and the diagnostic, and says explicitly that the emission is NOT refused -- because 'typed refusal' otherwise implies one. The diagnostic is advisory, so emission completes and produces its files beside it, measured on the required build lane at this branch: entry:src/v2/compiler/00_compile.dag emitted=175 blocking=0. What step 2 closed is the SILENCE, not the emission. Severity stays where it is owned, in v1.compiler.core reference_derived_import_refusal_severity_note. The annotation above the coproduct QUOTED the old wording. It keeps the quote, now marked as superseded, because the before-state is what motivates the arms -- but a quotation that silently tracked the edited note would cite a text that no longer exists. Its 'four things' also became six when the two variant arms landed. * Regenerate the emit_rust mirror for the note edit The note text is emitted into the mirror, so editing it necessarily drifts v1_compiler_emit_rust.rs. Two-generation regen at fdf4ccf plus the note commit: gen-0 first_generation_equal=false with drift in exactly that one file, install, REBUILD, gen-1 first_generation_equal=true. The single-file drift was the discriminator this run needed, not just its result. An EMPTY drift would not have been good news: it would have meant the uncommitted edit never reached the runner and the regen had measured a tree without it. Non-empty drift naming exactly the mirror of the edited file is what establishes the measurement was of the right tree, and it doubles as the parse check -- a .dag parse failure returns NO_CANDIDATE, which is how a stray quote in a note surfaced earlier on this branch. * Seed the merge resolution from the side that compiles, then let regen decide The merge of #9551 conflicted on v1_compiler_emit_rust.rs and the generated-artifact driver refused it correctly -- path left unmerged, no markers, regeneration recipe printed. I then seeded the resolution from MAIN's side, and the two-generation regen refused to build it: error[E0599]: no variant named CandidateVariantDelegatedToParent found for enum ReferenceDerivedCandidateDisposition --> v1_tests_claim_reference_derived_disposition_census_witness_test.rs could not compile v1-compiler (lib) due to 19 previous errors Main's mirror predates this branch's dispositions and this branch's witness mirror references them, so that side cannot be a compilable gen-0 seed. THE LESSON IS ABOUT WHAT 'DO NOT PICK A SIDE' MEANS. I took it to mean the final bytes must come from regeneration, which is right, and inferred that the starting seed was therefore arbitrary, which is wrong. Gen-0 runs the COMMITTED mirror to emit the candidate, so the seed must compile -- a side that does not is not a neutral starting point, it is a broken compiler. The choice of seed is not a choice of content and it is not free either. Seeded from this branch's side instead, which is main's #9551 bytes plus the note edit -- established rather than assumed: fdf4ccf regenerated with EMPTY drift, so its mirrors already equalled main's, and 037cda8 added only the note text on top. Regen output follows and is the authority. --------- 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: gunbc-ci-auto-heal <bts53@scarletmail.rutgers.edu>
…, zero new names (#9552) SystemdSliceDirective was a two-arm coproduct spelling MemoryMax and MemoryHigh a second time and carrying both values as NonEmptyStr. The fabric cell resource boundary declares five values, so realizing it needed MemorySwapMax=, TasksMax= and CPUWeight= -- and adding three arms would have widened the knob-name fork gunbc.systemd_property_directive_overlap counts from two to five. Instead the directive is a sole_constructor record pairing a SystemdUnitProperty with a modeled SystemdDirectiveValue, reachable only through per-knob mints. Zero knob names are minted: the wire spelling has one owner, systemd_unit_property_wire, reached through the property. MemoryCurrent= has no spelling because no mint produces it, not because a check rejects it. Claude-Session: https://claude.ai/code/session_01G2LsQXUHjevegFefaPU9BE Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t makes a charge sayable release_money got its production consumer in the previous change; settle_money still had none. This is that half, and it is the last thing standing between the broker and a reservation lifecycle that can actually end. ONE ENDING VOCABULARY, NOT TWO. A hold ends abandoned or consumed, and both leave the SAME state: the cell free and the encumbrance closed. A second outcome type for settlement would have been five refusal arms renamed -- the fork DESIGN section 3 forbids, and one that drifts the moment either side gains a cause the other lacks. So CellRelease generalises to CellHoldEnd and both endings return it. A caller never needs the outcome to say which ending happened, because it called one of them. Settlement adds exactly one arm, for the state release genuinely cannot reach: the receipt refused before any hold was touched. THE MONEY TRANSITION ARRIVES ALREADY COMPUTED, AND THAT IS NOT A CALLER DECIDING IT. Each ending owns its own transition -- release derives the amount from the ledger entry, settlement presents an actual spend -- and both are fenced on the lease generation inside product.fabric.budget. What end_cell_hold decides is the only thing both share: an advanced account frees the cell, a refusal does not. Matching on WHICH ending this is would have put a second money authority here, to be kept in step with budget.dag forever. WHY THE RECEIPT IS THE DIFFERENCE. Release needs no evidence beyond the lease: abandoning a hold spends nothing and the released quantity is whatever the ledger already says. Settlement CHARGES, so it needs something establishing what was spent and that the spender was entitled to say so -- which is exactly what product.fabric.execution's receipt admission already decides, with four separated causes. Those stay separated: a receipt from a different attempt is not stale, it is unrelated, and folding four remedies into "the budget refused" would tell an operator to look at an account when the answer is that the receipt belongs to something else. THE AMOUNT COMES FROM THE RECEIPT AND FROM NOWHERE ELSE. An amount parameter beside the receipt would let a caller charge one figure while presenting evidence for another, with nothing able to detect the disagreement. Only a SettlementReceipt carries an actual spend, so the payload is MATCHED rather than trusted -- an execution receipt records billable seconds, which product.fabric.execution says in line is an observation and not authoritative spend, because quantum, rounding, minimum charge and caps all sit between seconds and money and the rule is the supplier's. Three rows, positive control first because the other two are worthless without it, all green by execution. The payload claim carries an executed RED: admitting an ExecutionReceipt as though it carried spend returns false. Both release rows re-run green after the refactor, so the generalisation did not break the path it generalised. Compile 0 blocking across the module, witness and probe entries. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot
Bot
changed the base branch from
main
to
fabric/reservation-release
August 28, 2026 12:35
Recorded where the next lane will find it -- on admit_cell_settlement, because that function CONSUMES a grant -- rather than as three rows a reader would treat as three pieces of work. Measured on origin/main: ExecutionGrant appears at three construction sites and all three are test fixtures. Every production reference takes one as a parameter or filters a list of them. There is no producer, and the three gaps below are that one absence seen from three sides. ONE -- a ReleaseDirective cannot name a cell. product.fabric.arbitration produces the directive and nothing consumes it; it carries resource_reservations as ReservationRefs and the release actuator needs a SLOT KEY. Nothing relates them, and every fixture value is an opaque literal because no consumer has ever had to interpret one. The relation is not safely inventable: ReservationRef is a branded NonEmptyStr, so ANY string inhabits it and a parse has no shape to check against -- a wrong guess is undetectable at the type level and releases a cell someone else holds. TWO -- the acquire-side atomic join is a requirement with no implementation. product.fabric.execution states that every reservation is applied tentatively and committed only if EVERY ledger admits. With no producer that has never run. THREE -- the identity layer is unproduced. Excluding fixtures and the brand declarations, ObservationReceiptRef, ExecutionAttemptKey, LeaseKey, GrantKey and ReceiptKey have ZERO construction sites; ReservationRef has two and both are in this module. So the producer decides five identity conventions, not one. THE DECIDED DESIGN travels with the note so its author inherits a ruling rather than reopening it: when a directive can name a cell, refuse more than one resource reservation per directive and fold over the atomic one-cell release. The plural the model proves load-bearing is a list of DIRECTIVES -- a Work under re-execution holds two grants -- and that folds cleanly, leaving whole grants released and whole grants held with no grant partial. Two-phase commit, compensating release and undo logs are ruled out: they make the partial state reachable and then work to escape it. AND THE CITATION NAMES ITS TREE, because half this note does not resolve from main: fabric_reservation_payload and this module are unmerged. On main NEITHER reference is derivable; on this stack the money reference has a modeled derivation and the resource reference still does not. That is the precise gap -- the producer owns one derivation, not two. Compile 0 blocking. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… 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>
Contributor
|
Thanks — approval noted, and two of the three supporting claims check out against the reviewed head
|
Merged
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 28, 2026
…hot had re-added what #9496 deliberately removed The update-branch snapshot inside the squashed #9604 carried main as it stood at 18:18Z, which still contained the fifth-arm discriminating red that #9466 added. #9496 then retracted it on main. Merging the stale snapshot forward re-proposed that block, so this branch's delta silently reverted another lane's deliberate removal. This branch owns four files. Anything else in its diff is snapshot residue, not a change anyone authored here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This was referenced Aug 28, 2026
Closed
Closed
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…
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.
Stacked on #9598 (base
fabric/reservation-release), which is stacked on #9542. The diff here is the settlement half alone.release_moneygot its production consumer in #9598;settle_moneystill had none. This is that half — the last piece between the broker and a reservation lifecycle that can actually end.One ending vocabulary, not two
A hold ends abandoned or consumed, and both leave the same state: cell free, encumbrance closed. A second outcome type for settlement would have been five refusal arms renamed — the fork §3 forbids, and one that drifts the moment either side gains a cause the other lacks. So
CellReleasegeneralises toCellHoldEndand both endings return it. A caller never needs the outcome to say which ending happened, because it called one of them.Settlement adds exactly one arm, for the state release genuinely cannot reach: the receipt refused before any hold was touched.
The money transition arrives already computed
That is not a caller deciding it. Each ending owns its own transition — release derives the amount from the ledger entry, settlement presents an actual spend — and both are fenced on the lease generation inside
product.fabric.budget. Whatend_cell_holddecides is the only thing both share: an advanced account frees the cell, a refusal does not. Matching on which ending this is would have put a second money authority here, to be kept in step withbudget.dagforever.Why the receipt is the difference
Release needs no evidence beyond the lease: abandoning a hold spends nothing, and the released quantity is whatever the ledger already says. Settlement charges, so it needs something that establishes what was spent and that the spender was entitled to say so — which is exactly what
product.fabric.execution's receipt admission already decides, with four separated causes.Those stay separated. A receipt from a different attempt is not stale, it is unrelated, and folding four remedies into "the budget refused" would tell an operator to look at an account when the answer is that the receipt belongs to something else.
The amount comes from the receipt and nowhere else
An amount parameter beside the receipt would let a caller charge one figure while presenting evidence for another, with nothing able to detect the disagreement. Only a
SettlementReceiptcarries an actual spend, so the payload is matched rather than trusted — an execution receipt records billable seconds, whichproduct.fabric.executionsays in line is an observation and not authoritative spend, because quantum, rounding, minimum charge and caps all sit between seconds and money, and the rule is the supplier's.Evidence
Three rows, positive control first because the other two are worthless without it, all green by execution:
The payload claim carries an executed RED: admitting an
ExecutionReceiptas though it carried spend returnsfalse.Both release rows re-run green after the refactor, so the generalisation did not break the path it generalised. Compile 0 blocking across the module, witness and probe entries.
What is not claimed
The rows sit where settlement differs from release; everything downstream of an admitted receipt is the ending vocabulary #9598 already covers, and re-testing it would assert one fold twice. The successful free-write remains a host effect with live-probe evidence only, as in #9598.