Bind floor witnesses to owner-qualified declarations by gunbai-bot[bot] · Pull Request #9436 · gunb-ai/gunbc

gunbai-bot · 2026-08-27T12:00:23Z

Summary

Repair the 15 branch-only floor failures exposed by #9400 once emission consumes the resolver's exact owner_module_path. Generic RFC/bob declarations are given intrinsic names, the srv3 NBD witness imports the declarations and variants it uses, and the callable-ambiguity controls are expressed against the new selective-import boundary without changing their floor identities.

This PR includes #9400 because it is the implementation branch being repaired.

Test plan

git diff --check
pre-push cargo fmt --all --check
GitHub required build/floor checks on the combined branch

Repairs #9400.

gunbai-bot · 2026-08-27T17:03:49Z

Addressed review 56812 in 3f95218. The existing .dag seed-growth authority now carries a PR-local, reproducible receipt: the namespace admission Rust file remains flat at 33 declarations, the sole declaration-level change is a one-for-one const→static storage repair, and the 54 additions are exact authored transition data whose stale-row check is their deletion trigger. Rebase regeneration and fixed-point checks pass.

A call's target was decided twice. Inference resolved the callee with the module's imports in hand; 05_emit_rust then re-decided it from the authored LEAF SPELLING -- map_contains_key(rt_functions(), func) -- at a grain where those imports no longer exist. An explicitly imported v2 declaration whose name collides with a v1_rt bridge name was emitted as the unrelated primitive. That is DESIGN's authority-substitution class: resolution held the answer and a second mechanism answered for it. FuncSigResolved now binds the signature AND the declaration it came from, and v1.std.core CallTargetIdentity records what was chosen on the call node. Emission reads it. The three re-lookup seams are gone -- plain calls, the generic-method bridge, and callable-field selection. Two supporting facts fall out of touching this territory and are stated rather than bundled silently. CallableCandidate's is_builtin Bool is deleted: the identity variant already carries it and nothing consulted the Bool once the decision read the variant. ExprCall is cross-referencing data, so call-initialized product data routes to the typed-expression emitter instead of the literal/mock path. Parent function environments become import-aware. This is here because the change does not build without it, not as a bundled cleanup: once a call's target is the exact declaration resolution chose, a WRONGLY chosen declaration reaches rustc rather than being accidentally corrected by a leaf-spelling re-lookup. Three such bindings existed on main, each a name its own module never imports -- dag_collect_support's to_string, and infer's map_has twice. With the emit repair alone the seed fails to compile with exactly those three errors; with the narrowing it builds, and all three resolve to the generically-typed builtin, which is the correct callee. Those three are the measured population of the narrowing's EXERCISED consumers; they are not a corpus census, which regen coverage cannot establish. Evidence: claim_executor --required-regen first_generation_equal=true, planned/executed 136/136, one pre-existing declared divergence (main.rs). All final mirrors produced by the fixed .dag pipeline. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… removed the leaf-spelling re-lookup that was supplying them by parent-pool coincidence Six files call or reference names they never import. Until this branch, a leaf-spelling re-lookup at emission found them anyway in a parent pool they had no declared claim on. Owner-qualified emission does not create these defects; it removes the mask, and the resolver then reports each one. Every site reaches terminal green on the acceptance ladder. None is left at state 3 -- a change that merely converted the type disagreements into unresolved names would have removed masking without completing the migration. Three seed sites reached terminal green automatically: the Unresolved arm routes to the generic builtin and had been unreachable, because the coincidence-admitted declaration short-circuited ahead of it. The four wider-corpus sites repaired here needed authored imports. All six edits are additive import lines. No semantic edits. Verified: whole-corpus compile (3026 sources, 1057 indexed modules), which reproduces the floor's subject -- per-entry compile is a different subject with a greener answer, and an earlier pass was misled by it. required-regen first_generation_equal=true, 136/136, declared_divergent=1 [main.rs]. toolchain_home_interference_probe_wet exits 0 under a bound RUNNER_TEMP and 1 without it, on identical code, so its local red is environmental. Not closed here: five pre-existing 'file' transport emission diagnostics in extdeps/filesystem/filesystem_io.dag, visible only because the compile reached emit for the first time. That file is untouched and the message lives in src/v1/05_emit.dag, not in this diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…aking it computable THE DEFECT, STATED AT THE GRAIN THE MEASUREMENT SUPPORTS. `TransitionAdmission.subject` was `DeltaSubject`, whose fields are `String` because it is built at runtime from discovered module names. The roster is a `const`. Measured against those exact types, both arms: module: String::from("probe.consumer") -> error[E0015]: cannot call non-const associated function <String as From<&str>>::from in constants -- three times, one per field module: String::new() -> compiles clean, emits metadata So the roster was NOT uninhabitable, and an earlier statement of this defect (mine) said it was. It held exactly one shape -- every field the empty string -- and that shape matches no delta. What no const row could do was NAME A REAL MODULE: a hatch with no working position. WHAT IT WAS NOT. A row authored anyway does not silently pass. It matches nothing, lands in `stale_admissions`, prints with its own cause, and the ADMITTED arm is conjoined on that list being empty -- so it REFUSES. An earlier report of this as an escape hatch that accepts rows and silently matches nothing was withdrawn at source. Both failure paths were always loud; only the admission arm was fiction (§4b -- decoration cited as coverage, inside an otherwise real wall). THE FIX KEEPS CONST-NESS, WHICH IS DOING UNNAMED SAFETY WORK. A const roster cannot be COMPUTED, so no code path can synthesise an admission: the admission set is exactly what a human authored and a reviewer read. Reaching for a function or a `LazyLock<Vec<_>>` restores authorability by making admissions computable, which is the absorbing fallback arriving through a type signature -- the module's own header already forbids its behavioural twin, an admission "by a predicate ... which admits everything and zeroes the wall's deficit frequency by construction". So admission rows get their own `AdmissionSubject` with `&'static str` fields, matched against the runtime `DeltaSubject`. That is also the better §3 statement: an admission row's subject is a PATTERN naming one subject, not a subject. WHY THE EXISTING COVERAGE COULD NOT SEE THIS, and it is the part worth keeping. Two thorough tests already exercised the admission path -- exact-match admits, wrong-subject refuses and reports stale -- and both build their rows in a `let` with `.to_string()`. Neither ever touched the `const` constraint that actually bound production. So an auditor reading the admission path found green, careful evidence about a mechanism no authorable production row could reach: the coverage made the defect MORE hidden, not less. a_row_authored_in_a_const_admits_its_delta_exactly_as_a_runtime_row_would a_row_naming_the_empty_module_refuses_rather_than_admitting_silently The first one's discriminating property is COMPILATION at a real module name, which is what the old type refused. The second asserts the stale report BY LABEL, because an unattributable refusal is close to the defect being fixed. Both stay enrolled after the climb rather than dissolving with it (§4b -- a climb deletes the redundant production machinery, never the evidence). 22/22 green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

… floor (#9535) `resolved_call_emission_identity_witness_test.dag` landed in #9436 with seven claims all declared plain `fn`. The floor's discovery scan matches on the `test fn ` line prefix, so it enrolls nothing from the file, and a `*_test.dag` that enrolls nothing is refused: REQUIRED-FLOOR REFUSAL cause=BarrenTestSidecar count=1 That refusal fires for every PR based on main, so main is red for the whole fleet. The file declares `live_tree_disposition = SubstrateInputsOnly`, so it is meant to run. WHAT THIS CHANGE IS NOT. It does not quarantine the file, exclude it from discovery, or add it to an admission roster. Those would be the escape-hatch shape -- proceeding as if the refusal had not fired -- against a wall that landed hours ago to catch exactly this. The wall is correct; the enrollment was missing. Nor is it a known-red admission. `gunbc.explicit_witness_admission` exists for a claim that is correct but red against a stale mirror, and that is not the situation: #9436 regenerated the stage0 mirror in its own commit, so the resolver repair these claims assert is present in both the authored `.dag` and the emitted mirror on main. There is no drift to declare. ON EVIDENCE, STATED PLAINLY: a local measurement of these claims was attempted and WITHDRAWN as invalid, not reported. They call `compile_dag_rust_emit_check`, which is a host builtin with no `.dag` definition, so they exercise the binary rather than the repaired sources; the binary available locally predates #9436 by three hours, which is exactly the condition under which claims asserting post-repair behaviour report false. The instrument that decides this is CI, which builds from the tree under test and is current by construction. If any claim is red here, that is the real verdict and the file goes back to its author with it. Only the seven declarations change. No claim body is touched. 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>

…shrinks The namespace-wave-admission phase fails on every PR with a current merge base, reporting 53 stale admissions. None of them names anything those PRs touch. It is blocking at least #9447, #9512 and #9531, and it will block every PR from here. THE MECHANISM, and the roster's own contract already prescribed the fix. The 53 rows admit exact binding deltas from #9400's owner-qualified call-target cut. Once #9436 merged, any branch with a current merge base carries that cut on BOTH sides, so the admitted deltas no longer occur, so every row matches nothing and reports stale. The comment above the const already said what to do: "this temporary transition roster must shrink with its subject." This is that shrink. MEASURED BEFORE PRUNING, because a partial roster would have made a blanket delete wrong: 53 rows authored, 53 reported stale, 0 unadjudicated deltas. Not a subset -- no row was still carrying a live admission. (My first count said 54 and was wrong: the looser pattern also matched the struct definition line. The numbering runs 01-54 with 19 already pruned earlier by this same rule.) cargo test -p v1-compiler --test namespace_wave_admission -> 32 passed, 0 failed WHAT THIS DOES NOT FIX, AND IT IS THE MORE IMPORTANT HALF. Staleness is computed only inside WaveAdmissionOutcome::Adjudicated. On main the baseline resolves to the head, the outcome is NoSubject, and no WaveAdmissionReport is built at all -- so a spent roster is structurally invisible on the one branch everyone reads as the health signal, and its cost lands on whoever opens the next unrelated PR instead of on the wave's own author. That is exactly how these 53 came to block other lanes. Nothing will surface the NEXT post-wave roster either. I am not repairing that here. Where the staleness check belongs is a design question -- making a wall fire on main is not a change to smuggle in beside an unblocking prune -- and it is recorded at the carrier and reported as a gap in the instrument. Found by sharp-ram-84, who declined to prune it themselves because namespace_wave_admission.rs is the instrument deciding their own PR's admissibility. That was the right call: a PR that edits its own gate to go green is the shape we spent today refusing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013crMNyLvjKC2Q5UF851PKy

…s are refusing every PR (#9541) The wave-admission phase is red on every open pull request in the repository, and the cause is the roster doing exactly what its own rule says it should. WHAT IS HAPPENING. NAMESPACE_TRANSITION_ADMISSIONS carried 53 exact admissions for the owner-qualified call-target cut. That subject has landed (#9436, #9504); #9400 itself closed unmerged and no successor is open. So every row matches no delta, and `stale_admissions` reports all 53. WHY IT REACHES UNRELATED WORK, which is the part that makes this a fix rather than housekeeping. Staleness is computed PER RUN: a row is stale unless some delta in THAT RUN matches it. A pull_request build adjudicates the MERGE commit, so once the rows were on main every open PR inherited all 53 -- and a PR touching no namespace at all is precisely the case that can never match them. Measured: three of my own branches, none of which touches srv3, admissions, waves or namespaces, each report the identical 53. THIS IS THE ROSTER'S OWN DECLARED LIFECYCLE, not a reinterpretation of it. The const's doc comment: "A row that no longer matches is itself a finding (`stale_admissions`), so this temporary transition roster must shrink with its subject." And gunbc.namespace_wave_admission's seed-growth justification: "stale rows refuse, so the roster has its own deletion trigger: any absorbed or vanished delta makes required CI red until that row is removed ... it dissolves row-by-row with the transition it names." EMPTY IS THE RESTING STATE AND IS NOT PERMISSIVE, which is why shrinking is safe. With no rows, a run carrying no delta reports nothing and passes; a run carrying a real delta reports it as UNADJUDICATED and refuses. So the failure mode of having shrunk too early is a LOUD refusal naming the delta, closed by authoring a row -- never a silent admission. The next transition adds its rows here and removes them when its subject lands. The const declaration itself is retained, not deleted: gunbc.seed_growth enumerates it by name at declaration grain. 32 tests in tests/namespace_wave_admission.rs pass; none asserts on the roster's contents (both arms build their admissions in a `let`). 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>

Recomputed at 5a62da7 (RUNNER_HEAD confirmed on the runner), replacing the be89e23-based bytes: a mirror computed at a stale base is stale whatever CI later reports, so the base window was closed rather than waited out. Two-generation procedure, pristine tree at that head: gen-0 first_generation_equal=false, drift in exactly these four files install candidate, REBUILD claim_executor gen-1 first_generation_equal=true The rebuild between passes is the point: a single pass verifies an emission against a binary that predates it. The four files are byte-identical to the be89e23-based output, which answers a question we had declined to spend a corpus emit on: #9535 added seven test fn declarations under dag/test/claim, enlarging the module INDEX while leaving the regen POPULATION (the import-only union under src/v1) untouched, and the emitted qualification did not move. #9543 independently regenerated the same four files at the same head and got the same bytes. Two independent negatives on index-sensitivity at this grain. Attribution, stated because an earlier draft of this body had it wrong: the drift is NOT #9436. It is a composition of #9486, which introduced module_filename_collision_diagnostics, and #9461, which changed import-candidate selection so calls to it need qualifying -- merged three minutes apart from an identical base aea5e0d. Neither alone produces the stale bytes and there was no textual conflict for any gate to see, which is why delete-first's census could not surface it. Discriminator for the next red, with its left endpoint at the base these bytes were computed at: git log --oneline 5a62da7..origin/main -- 'src/v1/**/*.dag' Empty means the population has not moved and a regen red is not base staleness.

…n census, tapping nothing The exact consumer relation is what makes a replacement cut's population exact and what decides whether residue goes loud or silent when X is deleted. The ruled construction is to observe decisions the compiler ALREADY makes, keyed by the parser-minted occurrence identity -- reconstructing resolution from outside would answer with what a reimplementation believes rather than what the compiler selected. But a tap cannot be placed where the information is already gone, and which sites have lost it is not knowable from a type name. So the first output is not the relation: it is where exact occurrence identity and exact target identity COEXIST. THE PRICING RESULT: zero of five callable-resolution sites are tappable, because not one receives the occurrence identity -- every one is keyed by a bare name: String. Threading that seam is not a repair for stragglers, it is the whole precondition, and 0B.1b cannot begin on this family until it lands. The target axis discriminates, which is what makes this a measurement rather than a decoration: four sites carry the exact selected declaration in the outcome, one (borrowed_census_decl) carries the owning module while the declaration NAME does not survive. Two remedies, not one -- an erased target is repaired by widening an outcome, an absent occurrence by threading an input. THE ROSTER WAS RE-DERIVED AGAINST CURRENT MAIN BEFORE LANDING, and that is the more useful half. First read four days of main movement ago, it recorded all three FuncSigLookup sites as computed-then-erased. Between the readings #8952 and #9436 landed and FuncSigResolved gained its `declared` field. Publishing the first reading would have named a defect that no longer existed and priced work already done, in the file it was measuring. The revision field is not bookkeeping: these two files moved 440 lines while the claim was being written. Counts are DERIVED from the two axes, never stored, so a transcribed verdict cannot disagree with the facts beside it. Four unsurveyed decision surfaces are counted refusals rather than absent rows. No tap is placed, no relation produced. 13/13 green, including the four-corner control -- tappable is a conjunction at one site, and a conjunction written as a disjunction passes every single-axis test. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…n census, tapping nothing (#9600) * Price the resolver tap before building it: the decision-site retention census, tapping nothing The exact consumer relation is what makes a replacement cut's population exact and what decides whether residue goes loud or silent when X is deleted. The ruled construction is to observe decisions the compiler ALREADY makes, keyed by the parser-minted occurrence identity -- reconstructing resolution from outside would answer with what a reimplementation believes rather than what the compiler selected. But a tap cannot be placed where the information is already gone, and which sites have lost it is not knowable from a type name. So the first output is not the relation: it is where exact occurrence identity and exact target identity COEXIST. THE PRICING RESULT: zero of five callable-resolution sites are tappable, because not one receives the occurrence identity -- every one is keyed by a bare name: String. Threading that seam is not a repair for stragglers, it is the whole precondition, and 0B.1b cannot begin on this family until it lands. The target axis discriminates, which is what makes this a measurement rather than a decoration: four sites carry the exact selected declaration in the outcome, one (borrowed_census_decl) carries the owning module while the declaration NAME does not survive. Two remedies, not one -- an erased target is repaired by widening an outcome, an absent occurrence by threading an input. THE ROSTER WAS RE-DERIVED AGAINST CURRENT MAIN BEFORE LANDING, and that is the more useful half. First read four days of main movement ago, it recorded all three FuncSigLookup sites as computed-then-erased. Between the readings #8952 and #9436 landed and FuncSigResolved gained its `declared` field. Publishing the first reading would have named a defect that no longer existed and priced work already done, in the file it was measuring. The revision field is not bookkeeping: these two files moved 440 lines while the claim was being written. Counts are DERIVED from the two axes, never stored, so a transcribed verdict cannot disagree with the facts beside it. Four unsurveyed decision surfaces are counted refusals rather than absent rows. No tap is placed, no relation produced. 13/13 green, including the four-corner control -- tappable is a conjunction at one site, and a conjunction written as a disjunction passes every single-axis test. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * Split the remedy count in two: the census was collapsing the distinction it exists to make The standing derived ONE not-tappable count, defined as answers-a-reference AND NOT tappable. Because tappable is a conjunction over two independent axes, that reported the same number for a site missing its occurrence identity and a site whose target was erased -- and those need OPPOSITE repairs: one threads an INPUT into the decision site, the other widens an OUTCOME to retain what the site already selected. This module's own note says exactly that, in as many words, and then the derived count collapsed it. The census contradicted itself in the one place a reader takes the number from rather than the prose, which is worse than a note that had never made the distinction. The witness had permanently RATIFIED the collapse: the four-corner control asserted a single threading count of three, so the occurrence-exact/target-erased corner was encoded as owing occurrence threading, a repair it does not need. Now two overlapping derived counts. The axes are independent, so they do NOT partition the population: a site deficient on both inhabits both, because it owes both repairs, and forcing a partition would be the same collapse in a tidier shape. The four corners read 1 tappable / 2 occurrence-threading / 2 target-retention, and the production roster reads 5 surveyed / 0 tappable / 5 occurrence-threading / 1 target-retention -- which is what the measurement always found: threading is the family-wide prerequisite and borrowed_census_decl additionally needs its outcome widened. Found in side-chat review, not by the blocking review on the PR. 13/13 green by execution. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

The objection is that five admission rows expand hand-written compiler Rust with none of the required receipts, and that a dissolution condition does not by itself authorize the growth. Both halves are right as stated, so the row now carries the measurement in the shape #9436 filed for the 53-row cut. The load-bearing number: the declaration count is UNCHANGED, 38 on origin/main and 38 here. No function, type, const, capability or mechanism is added -- the rows are data consumed by the already-rostered declaration, from an authored literal with no scan, file read, environment read or computed predicate. 65 added lines, of which 16 are the justification and 49 are row literals; the one removed line is the const's own empty initializer. And the rows are not scaffold beside the wall, they are the wall's required input: the roster refuses a real delta as UNADJUDICATED until its author adds a row, so a relocation that acyclicity FORCED has exactly one sanctioned way to land. Declining to author them would not reduce hand Rust; it would leave the relocation unmergeable. The move that would actually reduce it -- migrating the roster's pure fold to .dag -- is blocked on ModuleDeclarationRecord having no .dag carrier, which this module's own CLASS A justification already names and which authoring one here would fork.

…t claimed; the receipt's architecture is checked (#9784) * The nonce's one-time-ness and the receipt's architecture are now checked, not carried INTAKE-AGENT-0A (ruling 3 "artifact and callback contract") exit point 3 and the wrong-architecture half of exit point 4. Both states were authorable and silently attested. attest_diagnostic_boot took ONE optional receipt. IntakeAttemptNonce is documented as a one-time callback token, but an optional cannot express the state that makes it one-time — a second callback bearing the same nonce — so the one-time-ness was prose. It now takes the LIST of callbacks delivered to one issuance: zero is AgentReceiptAbsent as before, more than one is DuplicateAgentCallback. A duplicate is refused even when the two callbacks are byte-identical, because the endpoint's one-time-ness is the property under test and choosing one of two to honour is an absorbing fallback (DESIGN §5): it widens on ambiguity instead of stopping the line. IntakeAgentBootReceipt.architecture was carried into the attestation and never compared with anything, so an x86-64 agent callback attested an AArch64 unit's issuance. The architecture is a fact ABOUT the issued artifact, so it lands on IssuedAttemptNonce beside the digest that names that artifact rather than being re-derived from the receipt it checks. Both new controls discriminate on the real acceptance path, proven by mutation, not by green: replacing the architecture comparison with `(true)` turns an_agent_on_the_wrong_architecture_does_not_attest_the_boot false, and disabling the duplicate refusal turns a_second_callback_on_one_nonce_is_a_replay_not_a_boot false. The five attestation witnesses in machine_intake_disposition_witness_test all return true unmutated. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019fKvi5dnJ8TcE514qbmWTk * Issuance carries the artifact; the callback population is sealed at acquisition The reviewing authority's two construction gaps on INTAKE-AGENT-0A. Both were fields that were CHECKED without their relationship being CONSTRUCTED, which is validation standing where construction was available (DESIGN §5). THE ARTIFACT BINDING. IssuedAttemptNonce carried artifact_digest and artifact_architecture as sibling fields, so the pair was independently authorable: an issuance could name an AArch64 artifact's digest beside X86_64, and an x86 agent repeating that digest passed BOTH checks while the artifact the digest names is AArch64. It now carries the exact BootArtifact, so digest and architecture are two projections of one authority and the mismatched pair has nowhere to be written. That required gunbc.boot_artifact, an ordinary single-authority relocation: boot_artifact_delivery already imports machine_intake_receipt, so issuance could not reach BootArtifact from there without a cycle, and the import graph's one structural law is acyclicity (§4). Copying the two fields into issuance was the alternative, and it is the fork §3 forbids -- two places answering "which artifact is this", free to disagree. The artifact is not a fact about delivery; delivery is one consumer and issuance is another. THE SEALED BATCH. Taking List<IntakeAgentBootReceipt> made a duplicate representable, which is what allowed the replay refusal at all, but left completeness asserted by the CALLER: a caller handed two callbacks by the endpoint could pass one, and the attestation would attest a boot whose nonce had in fact been replayed. The cardinality check was real; the population it counted was not. The attester now consumes AgentCallbackDeliveryBatch, sole_constructor and minted in this module, naming the issuance it is the population of and carrying the digest of the acquiring party's own record. Cardinality is checked BEFORE any callback is inspected, because a replayed nonce is a fact about the population and reading a receipt first would let a well-formed one speak for a batch that should have been refused outright. RUNG, DECLARED HONESTLY: the seal does not yet establish that the mint's caller supplied every callback the endpoint received -- no endpoint producer exists here, so completeness is a claim the acquisition layer makes and this layer records. That class is MITIGATABLE, strictly better than a caller-shaped list and strictly weaker than a proof. Next-rung trigger: the callback endpoint producer, at which point the mint is reachable only from it and completeness becomes structural. The duplicate refusal carries acquisition_evidence rather than per-callback transport identities, which the review suggested: IntakeAgentBootReceipt has no transport identity, and the fields it does carry are identical across legitimate duplicates -- the artifact digest especially -- so listing them would be a nickname for a fact this model does not hold. The evidence ref locates the record that does hold it. The nonce is never carried; it is a secret. A batch sealed for one issuance cannot speak for another, with its own control. All seven attestation witnesses execute and return true. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019fKvi5dnJ8TcE514qbmWTk * Completeness is not observable from a population nobody closed: three outcomes, not two Review 57762 and the reviewing authority found the same thing independently. observed_agent_callback_population is publicly callable and takes the callbacks and the acquisition evidence as INDEPENDENT arguments, so a caller handed [r1, r2] can pass [r1] with the evidence for both. sole_constructor stops the record literal being written elsewhere; it does not constrain who calls the mint or where they got the list. The name said "sealed delivery batch" and the construction did not seal anything, which is a hollow alias: every downstream reader inherits an assertion the type never held. The knife is monotonicity under hidden callbacks - whether a reading survives every completion of the population. received > 1 survives: a hidden sibling only makes a duplicate more true. A field mismatch survives: any hidden sibling would itself be a duplicate and also refuse, so every completion refuses. But one MATCHING callback does not survive - a sibling turns it into a replay - and neither does zero, because a caller can prefilter a real callback to zero exactly as easily as a duplicate to one. So the two indefinite readings no longer produce a verdict. DiagnosticBootAttestation is three-valued, and DiagnosticBootCompletenessUnestablished reports what was observed, the acquisition record it was observed in, and the supporting activity. Collapsing it into either neighbour is state_space_conflation: into refusal it reports a boot as failed on a caller's filtering decision; into attestation it reports one as proven on the same. AgentReceiptAbsent is deleted. Reading "the agent did not call back" off a list's length is a claim about the world drawn from a caller's filtering decision; it returns with the producer that can close a population. DiagnosticBootAttested is now constructed by nothing. That is a declared terminal, not dead code: it is what the intake transaction requires, held at its honest arity so the future producer has one authority to satisfy rather than a shape invented later. Its trigger names the CAPABILITY, not an artifact - an acquisition producer that CLOSES a population, with a declared closure boundary or one-shot nonce consumption. Producer identity alone is insufficient: without closure a producer can mint a singleton after the first callback and accept a second afterwards. Two witnesses changed meaning rather than shape. The empty-population case asserted AgentReceiptAbsent and now asserts Unestablished naming the supporting activity; the matching-callback case asserted attestation and now reads the asymmetry directly - same call, differing only in the callback, a match yields Unestablished and a wrong nonce a definite refusal. The provenance control uses two populations identical except for their acquisition record, so it reads the field rather than checking a constant. 31 witnesses, all green by execution. Also: five namespace transition admissions for the BootArtifact relocation into gunbc.boot_artifact. The required run reported FloorClean with the failing phase namespace-wave-admission at 5 unadjudicated TargetChanged deltas; the roster is empty after the sixth dissolution and empty is not permissive. Each row names one exact (module, declaration, spelling) triple, blast radius 0, dissolving when this PR merges. * Review 57801: the hand-Rust receipt, measured rather than argued The objection is that five admission rows expand hand-written compiler Rust with none of the required receipts, and that a dissolution condition does not by itself authorize the growth. Both halves are right as stated, so the row now carries the measurement in the shape #9436 filed for the 53-row cut. The load-bearing number: the declaration count is UNCHANGED, 38 on origin/main and 38 here. No function, type, const, capability or mechanism is added -- the rows are data consumed by the already-rostered declaration, from an authored literal with no scan, file read, environment read or computed predicate. 65 added lines, of which 16 are the justification and 49 are row literals; the one removed line is the const's own empty initializer. And the rows are not scaffold beside the wall, they are the wall's required input: the roster refuses a real delta as UNADJUDICATED until its author adds a row, so a relocation that acyclicity FORCED has exactly one sanctioned way to land. Declining to author them would not reduce hand Rust; it would leave the relocation unmergeable. The move that would actually reduce it -- migrating the roster's pure fold to .dag -- is blocked on ModuleDeclarationRecord having no .dag carrier, which this module's own CLASS A justification already names and which authoring one here would fork. * The provenance goes on the wrapper, and one nonce constructor was answering for two failures Two findings from the reviewing authority against the exact pushed head, both mine. FIRST, THE ANNOTATION WAS LYING AND THE CONTROL COULD NOT SEE IT. The source said "every outcome names the population it was read from". It was true of DiagnosticBootAttested, of DiagnosticBootCompletenessUnestablished, and of DuplicateAgentCallback -- and FALSE of ArtifactDigestMismatch, ArchitectureMismatch, BoardSerialMismatch and the nonce refusal, which returned a cause and dropped the record entirely. The control named an_outcome_carries_the_acquiring_record_it_was_read_from exercised only the unestablished path, so it greened while every ordinary singleton refusal discarded the record. That is this repository's own §5 trap authored by me: a claim about paths with an oracle blind to those paths. Fixed structurally rather than by narrowing the comment. population_evidence now sits on the DiagnosticBootNotAttested wrapper, so no adjudication path can return without it, and DuplicateAgentCallback drops its own copy -- the cause carries only what distinguishes it. The new control uses two DEFINITE mismatch refusals identical in every respect except the acquisition record they were observed in, which is the arm that was actually lying; a second control checks the duplicate refusal still locates its record now that the field moved up. SECOND, NonceMismatch WAS TWO FAILURES UNDER ONE NAME. It was constructed both when the supplied population was bound to another issuance -- an acquisition splice, produced by whoever assembled the input -- and when a callback inside a correctly bound population returned the wrong nonce, which is agent content. Different producers, different evidence locations, different remedies, and one constructor loses exactly the information a refusal exists to preserve. Now CallbackPopulationForOtherIssuance and AgentCallbackNonceMismatch. Neither carries the nonce: it is a secret with no place in durable output, so the cause names which comparison failed and the wrapper's evidence says where to look. The foreign-population control and the wrong-callback-nonce control now discriminate the two; under the old single constructor both greened on either bug. 33 witnesses, all green by execution (PASS=33 FAIL=0). * The fixture stopped claiming to be an endpoint The helper was named delivered and described as the batch an ENDPOINT would mint -- the population it actually received, sealed with the digest of its own record. That is exactly the completeness claim the production type and the PR body now withdraw, left standing in the test where it would teach the next reader the withdrawn model. It is observed_population now, and its annotation says what is true: the callbacks and the record reference are handed over independently, as they are at every real call site, and nothing here closes an acquisition or seals anything. 33 witnesses green (PASS=33 FAIL=0). --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>

…moves The namespace-wave-admission phase refused this PR with 4 unadjudicated deltas, 0 stale, 47 consumed. The four are the call sites of match_pattern_is_irrefutable, whose target moved when review 59122's §3 fix dissolved the duplicate predicate into v1.std.core: v1.compiler.emit_rust::collect_pattern_rc_variant_guards v1.compiler.emit_rust::emit_typed_match_arm_strs v1.compiler.emit_rust::rc_arm_has_refutable_plain_field v1.compiler.emit_rust::rc_pattern_preludes `match_pattern_is_irrefutable` base {v1.compiler.emit_rust} -> head {v1.std.core} TargetChanged does not auto-admit -- gunbc.compiler_frontend_program_interlock records that it refuses unless an exact authored transition admission names it -- so this adds one exact row per binding, following the #10011 and #9436 re-home precedent. These are DATA rows in the already-rostered NAMESPACE_TRANSITION_ADMISSIONS declaration: no new declaration, type, function or admission mechanism, so the existing seed-growth justification covers them. They carry their own deletion trigger, as that roster's rule requires -- once this PR merges the rows match no delta and go stale, which reds required CI until they are removed. WHY THE FILE IS EDITED DIRECTLY rather than through a .dag. The rows exist only in src/v1/stage0/src/namespace_wave_admission.rs; no .dag carries them, so there is nothing to project from. Confirmed two ways rather than assumed: the --required-regen pass never names this file (0 mentions in its log), and `git check-attr merge` reports `unspecified` for it while reporting `generated-artifact` for v1_compiler_emit_rust.rs and docs/design-failure-modes.md as a control. It is hand Rust that the candidate tree copies through. NOT FIXED HERE, because it is not this lane's: the floor still refuses on one site, src/v2/compiler/self_host/native_agreement_support.dag:21, missing `SemanticMismatch { actual: Rejected, falsification: Present }`. That is #10109's and its diff adds exactly that arm. This PR cannot go green until #10109 lands. A NOTE ON THE DIAGNOSIS, because the first one was wrong and its wrongness was invisible. The propagate arms in the previous commit introduce exactly four new pattern bindings (ds, cd, ds, ds), and I initially attributed deltas=4 to those and confirmed it by counting them in the diff. Two independent explanations each predicted four, so the matching count ratified the wrong one. The itemisation sits ~50 lines above the failure line in the job log and names the real subject. The failing set is not enumerated AT the failure line while all 47 passing admissions are, which is the wrong way round. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf

…tes surfaced, all closed) (#10028) * See through nested patterns in the .dag exhaustiveness checker `check_match_exhaustiveness` folded arm coverage as `VariantPattern { name: n, parent_enum: _, field_bindings: _ }` and keyed a covered-set on the head name alone, so an arm restricting a field to ONE inner constructor marked its whole variant covered. The parser does not lose the nesting -- `parse_field_bindings` recurses into `parse_pattern` -- so the fact was DISCARDED, not missing. MEASURED, both halves, on `type Inner = P { v: Bool } | Q` / `type Outer = A { i: Inner } | B` with `match o { A { i: P { v: v } } => v B => false }`: before: gunbc compile --target rust -> exit 0, `compiled: 6 files emitted, 0 diagnostics` cargo check on the emission -> error[E0004]: non-exhaustive patterns: `&Inner::Q` not covered, exit 101 after: gunbc compile -> refused at emit, error[m.dag:5:3]: non-exhaustive match: missing variant(s) A { i: Q } The emission was a FAITHFUL lowering of the accepted graph, so the target compiler was performing the analysis the front end declined. That backstop is expiring: rustc catches these only while the seed still emits Rust, and section 7 shrinks the seed toward zero. THE CONSTRUCTION. Coverage is now a pattern MATRIX -- rows of patterns over a vector of column types -- specialised one constructor at a time. Per-field coverage would fail open in the original direction (`A { x: P, y: Q }` beside `A { x: R, y: S }` reports both columns covered while `A { x: P, y: S }` matches nothing), so the columns are carried jointly and never separately. Field types come from `lookup_variant_in_type`, the same authority that types the binding a nested pattern introduces. The branch gate is signature COMPLETENESS, not "some row is irrefutable" -- the latter drops the constructor rows that also cover a wildcard's values and refuses `A { x: P, y: _ }` beside `A { x: _, y: P }` and `A { x: Q, y: Q }`, which is exhaustive. That near-miss is pinned by its own control. RETAINED BLINDNESS, DECLARED RATHER THAN WIDENED: a column whose type carries no closed constructor roster -- Int, String, Bool -- is not refused when covered only by literals. That is the pre-existing top-level behaviour carried to depth, and closing Bool would refuse live code (`v2.compiler.infer` `infer_bool_literal_pattern_classify` is exhaustive THROUGH its nesting). NEXT-RUNG TRIGGER: a closed constructor roster for the kernel scalar types. Rung claimed for nested COPRODUCT columns only: below-the-ladder -> 3. EVIDENCE. 13 single-module fixtures executed against a seed rebuilt from this change, 13/13 at their asserted counts. Eight are new, and two cannot pass under a weaker implementation: `w_two_nested_columns_are_judged_jointly_not_per_field` is red under per-field coverage, `w_overlapping_wildcard_columns_are_not_over_refused` is red under the completeness-gate near-miss above. `w_optional_nested_*` carries the shape that actually occurred -- nesting inside `Present` over `Optional<T>`, where the roster is SYNTHESISED rather than read off declared children. The population specimen is gunbc#9964 (still-swift-363): adding a fourth `InferredNode` variant refused SEVEN flat matches and stayed silent on TWO nested ones in the same run. Those two sites were repaired there; this is the checker. Ledger: a second instance on the existing `accepted_source_emits_uncompilable_target` row -- same invalid state, different mechanism -- converted to one-line form per gunbc#9898. Regen: `v1_compiler_infer_patterns.rs` only. Baseline regen on an unmodified tree drifts `compiler_tests.rs` and `std_realization_schedule.rs`; those are not this change and are not committed here. The candidate is byte-identical from linux/amd64 and arm64 (sha256 00b0f2f949de75a6, 1414 lines). `docs/design-ledgers.md` regenerated via `tools.generated_artifact_gate` `main_wet_one`: one line changed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Hold the variant-in-type-position narrowing, and correct the Bool scope claim Two corrections against my own previous commit, both found by measurement rather than review. 1. THE VARIANT-IN-TYPE-POSITION NARROWING IS REVERTED, NOT REFINED. I had read the two `gunbc.package_delivery` refusals as false positives: the producer returns `HostCliDependencyAbsent?`, Optional of a single VARIANT, so by inhabitance only that variant can occur and the parent's other arm is unreachable. That reading is not wrong about inhabitance, and it is still not what should govern. The .dag type system already answers what that column is, and answers it out loud: on `Present { value: a } => a.tool` it refuses `no field 'tool' on type 'VObs'` (still-swift-363, executed). The corpus sites survive only because they destructure IN THE PATTERN, which works against a variant even when the column is the parent -- one column, two spellings, and only one makes the type system speak. A roster answering `singleton` while resolution answers `parent` is one concept with two answers inside one compiler (section 3). The decisive ground is section 5 and it does not require the merits to be settled: the narrowing is the arm that makes the checker STOP REPORTING a class. If it is wrong it suppresses a real floor class permanently; if the other reading is wrong, two sites carry an unreachable arm -- wasteful, loud, safe. Under genuine uncertainty the refusing arm wins. What is actually undecided -- whether a variant should be a FIRST-CLASS TYPE, making `HostCliDependencyAbsent?` genuinely a singleton Optional -- is recorded at the declaration as a section 4b(2) no-untracked-stall. It is a substrate question (Rust cannot express it, hence the emitter's variant_to_enum) and is deliberately not settled here. The two witnesses are inverted to PIN the parent-roster behaviour, with the negative left loud on purpose: if the substrate later makes variants first-class, that witness fails, and the failure is the signal. 2. THE BOOL SCOPE CLAIM IN THE PREVIOUS COMMIT WAS FALSE. It said Bool columns stay open. `std.types` declares `type Bool = True | False`, an ordinary Disj, so a Bool column resolves to a two-arm roster and IS closed -- correctly, since the emitted match faces the same two arms. `gunbc.host_standup GreenPlaceFromGunbcGate` matching `{ gate_verdict: false }` without covering `true` is a genuine nested defect, not a phantom. So the checker is right and the prose was wrong. It UNDERSTATED what the change does, which is still a rung-honesty defect: a scope sentence nobody can check against the code fails the same way an inflated one does, pointing the other way. Genuinely open, refused nowhere: Int and String. That half of the claim survives. CENSUS, corrected for a double-count. An earlier figure of 190 counted BOTH renderings the compiler emits per diagnostic -- a byte-range summary line and an `error[file:line:col]` line -- so it read instrument output as subject content. Split: 95 and 95. Comparable figures, both grepped on the error form over a whole-corpus compile of dag + src/v2: main's checker ... 11 sites this change ...... 95 sites, 47 files delta ............ 84 newly exposed Main is green with those 11 already standing because the required floor runs a gate closure and does not compile the whole corpus -- "main is green" and "the corpus eliminates closed variants exhaustively" were never the same claim. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Record the two census rulings at the carriers that will be read next Annotation-only: the emitted seed is byte-identical, which is section 4c's erased projection doing what it promises -- prose that changes no semantic bytes. 1. THE package_delivery PAIR IS A MODELING DEFECT, NOT A MISSING ARM (tidy-lynx-804, after reading the producer). My previous note framed those two sites as an open question with two defensible repairs. That was too weak. Adding a `HostCliDependencyPresent` arm would answer for a state that cannot occur by inhabitance -- a fabricated plausible output at a site whose whole purpose is refusal, silencing the checker without making anything exhaustive. The real repair is ordinary section 2 modeling and is cheaper than the substrate question I had named: the concept `an absence carrying tool and hint` already exists but is fused into a variant, so it cannot be named in a type position. Give it its own type, let the observation be `Present | Absent(that type)`, and both matches become exhaustive with one arm -- legitimately. That is its own PR and explicitly NOT a row in this census. So my 4b(2) row was pointing at the wrong blocker. Whether a variant should be FIRST-CLASS is still undecided and still recorded, but it is not what these two sites are waiting on. 2. A MECHANICAL `=> false` IS A TEST-ONLY REPAIR. I had called the 8 production sites carrying the same Scaffold shape `probably A-like`. They are not, and the reasoning generalises to every future census of this class: in a `test fn -> Bool` the arm is a claim ABOUT THE FIXTURE and naming each shape BUYS fail-closure, because a variant added later turns the site red again. In a production `fn` the identical arm is a semantic answer returned to a real caller and SPENDS that property, converting a site that fails loudly on an unhandled variant into one that silently answers false. Same shape, opposite effect -- and the diagnostic cannot tell them apart, because it reports the missing witness and not what the enclosing declaration returns. Recorded in the witness carrier rather than a handoff message, because the census will keep producing this shape after the handoff is forgotten. 3. THE POLARITY READ IS BLOCKING, NOT ADVISORY. I had filed it as a caveat. A site whose match INVERTS its assertion needs `true`, and writing `false` flips what the test means while leaving it green -- and NEITHER instrument in this program can catch that: the suite is green by construction either way, and the site leaves the refusal census either way. Nothing downstream contradicts a wrong polarity, so it has to be read at the site before the arm is written. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Strike the withdrawn polarity obligation from the witness carrier A blocking per-site POLARITY read was recorded here two commits ago. It had already been retracted when I wrote it -- the retraction went to another lane and not to me -- so I cemented an obligation nobody was holding. It is struck rather than quietly deleted, because the reason it was put in a witness carrier is the reason leaving it would be worse than never recording it: a carrier outlives the thread that wrote it, so a retracted requirement standing here reads as live to everyone who touches this census afterwards. WHAT CLOSED IT was a structural argument, not a larger sample. Every group A enclosing declaration is NULLARY -- `test fn name() -> Bool`, no parameters -- so nothing threads in from outside and the scrutinee is a closed term. Exactly one arm is ever taken, and an arm added for a shape the closed scrutinee does not have is UNREACHABLE: never evaluated, producing no value. Polarity is a property of how a value reaches an assertion; a dead arm has none to get wrong. Verified here before amending: 63 of 63 nullary, zero exceptions, zero unresolved. What replaces it is the useful half, and it BOUNDS this PR's own claims rather than adding an obligation to someone else's: the green at a repaired A site is green BY CONSTRUCTION, so there is no discriminating red to construct per site and this suite must not be cited as validating a repair batch. A batch is reviewable by reading the arms against the declaration, and by the witnesses here covering the CHECKER. The test-vs-production buys/spends distinction is untouched and still stands. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Restate the polarity obligation as a distinction, not a withdrawal This annotation has now been wrong in both directions -- first recording a blocking per-site polarity read, then withdrawing it wholesale -- and the operator's ruling separates them. The added arms are unreachable, so the suite passes identically before and after and cannot discriminate a wrong arm. That retires the EXECUTING witness, not the SOURCE read: an arm whose value is never computed is still an authored claim about what the value would be, and only a reading of the source can judge it. Unreachability removes runtime execution as an oracle; it does not make the authored value self-justifying. The sharpest part, and the part this carrier had wrong: the checker's shrinking refusal set is the discriminating evidence for EXHAUSTIVENESS, not for POLARITY. The two had been conflated here, which is what produced both the over-demand and the over-withdrawal. Restated rather than deleted, for the same reason it was struck rather than deleted before: a witness carrier outlives the thread that wrote it, so an obligation left in either wrong state reads as settled to whoever next touches the census. Annotation-only -- every changed line begins with //, verified mechanically rather than by eye, so under DESIGN section 4c this is erased before any semantic pass and cannot move a diagnostic. The live checker is unchanged at 788ee9c, so no downstream receipt is invalidated by this commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Re-trigger CI: the run on f7d13bd registered as a corpse Run 33683206017 was created 21:06:04Z for this head and never acquired a runner: status=pending, jobs=0, updatedAt frozen at 21:06:05Z -- one second after creation and untouched 22 minutes later. `gh run rerun` refuses it with "this workflow is already running", so the dead registration holds the slot and cannot be revived in place. Classified before acting rather than assumed: the repository's CI is healthy. Runs created AFTER this one, on file-instrument-class and four other session branches, are in_progress. So this is an isolated never-acquired registration, not queue contention and not a provider outage, and re-triggering is the right response rather than waiting longer. An empty commit is the mechanism because a workflow_dispatch run would not attach to the pull request as a check, and the corpse blocks rerun. No source change: the tree is identical to f7d13bd. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * File the go and python instances of the class, with the python arm's discriminating detail still-swift-363 produced a three-line probe accepted with zero blocking diagnostics on all three reachable targets; rust emits a compiling module and python and go do not. They stated honestly that they had NOT run either toolchain, so the go and python halves arrived as source readings. I ran python, and the executed result is materially worse than the reading: py_compile PASSES import SUCCEEDS typing.get_type_hints NameError: name 'Optional' is not defined calling the function NameError: name 'Present' is not defined `from __future__ import annotations` defers annotations to strings, so the undefined `Optional` never evaluates at import and the module loads clean. The defect surfaces only when the function is CALLED. That is the sentence worth carrying: AN EMISSION DEFECT THAT SURVIVES IMPORT IS FAR MORE DANGEROUS THAN ONE THAT DIES AT IMPORT, because every cheap verification anyone would reach for reports success. "python emission is uncompilable" understates it into something a reader would expect a smoke test to catch. The GO arm is recorded as a SOURCE READING and not a toolchain receipt, because no go toolchain exists in this container. It is kept lexically separate from the python result rather than sitting beside it as though both were executed: two values returned from single-return signatures, `[]*int64` declared against `[]interface{}` returned, and an undefined `Present`. Filed as a further instance on the existing row rather than as a new class -- these are the same invalid state reached on two more targets, and minting a second name for it is the nicknaming DESIGN section 3 forbids. Row compiles 0-blocking at 10 files and 95 advisories; the projection was regenerated rather than hand-edited, and the checker restored by sha afterward. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Dissolve the duplicate irrefutability predicate into v1.std.core (review 59122) review 59122 (codex/gpt-5.6-sol, REQUEST_CHANGES) found that this PR added `pattern_is_irrefutable` to 04_patterns while `match_pattern_is_irrefutable` already existed in 05_emit_rust -- two hand-written discriminators over one type, free to drift as MatchPattern grows. Verified before acting: the predicate is mine, added by bc31751, absent from main, and the two bodies agree on every constructor that exists today. The finding is correct. Irrefutability is a fact ABOUT `MatchPattern`, so it now lives with the type in v1.std.core (00_core.dag), which already declares MatchPattern and hosts 202 functions. Both consumers import it; neither re-derives it. Definition count is now 1 in v1.std.core and 0 in each consumer. Two judgement calls. The surviving NAME is main's `match_pattern_is_irrefutable` rather than mine -- renaming an established symbol to this branch's spelling would be nickname churn on top of a section 3 fix. The surviving BODY is the exhaustive one rather than emit's `_ => false`: a catch-all answers `false` for any constructor added to MatchPattern later, silently classifying a new irrefutable form as refutable, while the exhaustive match refuses and makes the author decide. Behaviour-preserving today, fail-closed tomorrow. VERIFIED BY REGEN FIXED POINT, not by reading the two bodies. Pass 1 declared drift in exactly the three expected mirrors and nothing else: v1_std_core.rs gains the function, v1_compiler_infer_patterns.rs loses its local copy, and v1_compiler_emit_rust.rs loses its local copy while its five call sites become `crate::v1_std_core::`-qualified -- the mechanical consequence of the definition changing modules, not of the predicate changing meaning. Pass 2, run from a binary built from the installed seed, reports first_generation_equal=true at 153/153. That second pass is the receipt: the recipe warns a single pass can self-verify at divergence 0 for the wrong reason. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Repair the eleven nested-pattern exhaustiveness sites the new checker surfaces The checker in this PR reports 13 sites that main's checker cannot see. Two are owned elsewhere (#10137, #10109); these are the eleven unowned. They follow ONE rule, not three shapes: an added arm must preserve the producer's declared state AS FAR AS THE CONSUMER'S CARRIER CAN REPRESENT IT. PROPAGATE (4) -- refinement_preservation:42, :44, :60, idempotent_operation_conformance:200. These RECONSTRUCT an Outcome. Widening alone would match `diagnostics: _` while still EMITTING `diagnostics: None`, which does not discard a present fact -- it FABRICATES the absence of one, downstream, where nothing can recover it (DESIGN.md section 5, fabricated-plausible-output). They now bind `diagnostics: ds` and re-emit it. This is not a new rule: the Rejected arm directly beneath each already reads `Rejected { diagnostics: d } => Rejected { diagnostics: d }`, so the change removes a section 3 fork between two arms of a single match. refinement_preservation:42 FORWARDS into an inner match rather than reconstructing, so plain propagation had nowhere to put the outer advisory. It uses the existing `v2.std.diagnostic.bind_outcome_accepted`, which is exactly that composition -- merge into an accepted inner, prepend via rejected_with_pending on a rejected one. No new combinator was minted. WIDEN (6) -- refinement_preservation:54, :70, :79, idempotent_operation_conformance:238, language_behavior_equivalence_test:255, :268. The four witnesses assert propositions that name no diagnostics; the two bridges FORWARD a claim into a runner and return Verdict / TestClaimRun, which carry no position for an emit-time advisory, so widening asserts nothing false. idempotent:238 was checked against its own authored rationale rather than its name: that annotation states a non-pass claim is established only by a comparison that RAN AND DIVERGED, and an `Accepted { diagnostics: Some }` run did run -- so `Some => false` would contradict the sentence the site exists to enforce. REFUSE (1) -- compile_eval_thesis_proof_test:86, a VALUE-CONSTRUCTOR omission. `diagnostics: _` is already a wildcard there, so `Some => false` is not merely wrong but unwritable; the missing variant is the other value constructor, which the witness cannot destructure and so cannot evaluate its proposition over. Arm is false, with TranslateResult added to the import block. CARRIER GAP, recorded not fixed: widening the two language_behavior_equivalence bridges DROPS the emit-time advisory, because Verdict and TestClaimRun have nowhere to put it. That is section 4b's outside-the-modeled-guarantee column -- honest loss at a boundary -- whereas every alternative fabricates an event: mapping Accepted{diagnostics: Some} onto SemanticMismatch{actual: Rejected} asserts a mismatch observed against a rejection that never happened, and TestClaimRun is a product with no refusal variant, so there is no arm to add. NOT TAKEN, deliberately: the whole of refinement_preservation_generated_nonempty_list_claim is literally bind_outcome(o, f), and the section 2 fold would dissolve sites :42 and :44 by removing both matches. That reshapes the function well beyond the ruled repair; "the checker forced me to touch this line" is not authority to restructure the code around it. Recorded in the PR as an observation. VERIFIED BY EXECUTION, binary built 12:53:33 from the merged tree: of the twelve sites this checker reported under the src/v2 root arm, one remains -- native_agreement_support:21, which is #10109's. No new error kind appeared; the 20 other blocking errors in that arm are in ownership_movable_test.dag (imports v1.compiler.ownership, unreachable because v1 is not a source root in this arm) and a deliberate leak fixture, neither of which this diff touches. Ruling and per-site verification with tidy-lynx-804 (BT-N). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Admit the four TargetChanged bindings the irrefutability dissolution moves The namespace-wave-admission phase refused this PR with 4 unadjudicated deltas, 0 stale, 47 consumed. The four are the call sites of match_pattern_is_irrefutable, whose target moved when review 59122's §3 fix dissolved the duplicate predicate into v1.std.core: v1.compiler.emit_rust::collect_pattern_rc_variant_guards v1.compiler.emit_rust::emit_typed_match_arm_strs v1.compiler.emit_rust::rc_arm_has_refutable_plain_field v1.compiler.emit_rust::rc_pattern_preludes `match_pattern_is_irrefutable` base {v1.compiler.emit_rust} -> head {v1.std.core} TargetChanged does not auto-admit -- gunbc.compiler_frontend_program_interlock records that it refuses unless an exact authored transition admission names it -- so this adds one exact row per binding, following the #10011 and #9436 re-home precedent. These are DATA rows in the already-rostered NAMESPACE_TRANSITION_ADMISSIONS declaration: no new declaration, type, function or admission mechanism, so the existing seed-growth justification covers them. They carry their own deletion trigger, as that roster's rule requires -- once this PR merges the rows match no delta and go stale, which reds required CI until they are removed. WHY THE FILE IS EDITED DIRECTLY rather than through a .dag. The rows exist only in src/v1/stage0/src/namespace_wave_admission.rs; no .dag carries them, so there is nothing to project from. Confirmed two ways rather than assumed: the --required-regen pass never names this file (0 mentions in its log), and `git check-attr merge` reports `unspecified` for it while reporting `generated-artifact` for v1_compiler_emit_rust.rs and docs/design-failure-modes.md as a control. It is hand Rust that the candidate tree copies through. NOT FIXED HERE, because it is not this lane's: the floor still refuses on one site, src/v2/compiler/self_host/native_agreement_support.dag:21, missing `SemanticMismatch { actual: Rejected, falsification: Present }`. That is #10109's and its diff adds exactly that arm. This PR cannot go green until #10109 lands. A NOTE ON THE DIAGNOSIS, because the first one was wrong and its wrongness was invisible. The propagate arms in the previous commit introduce exactly four new pattern bindings (ds, cd, ds, ds), and I initially attributed deltas=4 to those and confirmed it by counting them in the diff. Two independent explanations each predicted four, so the matching count ratified the wrong one. The itemisation sits ~50 lines above the failure line in the job log and names the real subject. The failing set is not enumerated AT the failure line while all 47 passing admissions are, which is the wrong way round. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * File the ConstructorsOpen conflation, and discharge the 17 now-consumed rows TWO UNRELATED THINGS THE REQUIRED RUN AT 543c83d ASKED FOR. 1. THE ADMISSION ROSTER. Main's 17 `call-reachability grounding gunbc#10156` rows became CONSUMED when that transition landed, and this branch touches the roster, so they are due. A previous commit deliberately preserved them on the grounds that nothing observed said they were consumed; that was correct on the evidence then and is superseded by an observation that says they are. Deleted, with the identity join run FIRST: the phase's own CONSUMED ADMISSION enumeration joined against the labelled rows on (module::in_declaration, spelling, target), both set differences EMPTY under LC_ALL=C, 17 for 17. The dead const is removed too -- this time exactly its two declaration lines, NOT the surrounding prose, which is the over-deletion the previous merge had to repair from main's side. Roster is now 4 rows: this PR's own, which inherit the same obligation. 2. A THIRD INSTANCE OF THE PR'S OWN FAILURE CLASS, FOUND BY REVIEW 59399 AND FILED RATHER THAN FIXED. `constructor_roster_for` answers `ConstructorsOpen` from an ELSE branch, conflating three states with three different correct answers: a genuine open scalar (a witness is owed), a single-constructor product -- a record, no `|`, hence no Disj connective -- which is CLOSED with one constructor and whose total destructure is total, and a type whose lookup FAILED, which is ignorance and not an answer. The arm answers `[]`, i.e. exhaustive, when no row head is irrefutable. That is a widening failure arm and it is AUTHORED BY THIS PR, not inherited: origin/main carries zero occurrences of ConstructorsOpen and never examines these positions at all. WHY IT IS FILED AND NOT FIXED, MEASURED RATHER THAN ARGUED. The one-line remedy -- delete the guard so the arm refuses -- was implemented, built, and reverted. Positive control fires; a `_`-arm match stays green; and the corpus reports NINETEEN sites, sampled rather than counted, which are FALSE POSITIVES of the second kind: v2.std.grammar derive_grammar_relation_token_edges_recursive_step matches a Witness with both arms present and is reported for its nested DeriveGrammarRelationTokensProgress column, a three-field record. Flipping the arm trades a fail-open for a fail-closed-on-valid-input without touching the modelling deficit underneath, and for the third state it would blame the author for the checker's ignorance -- DESIGN section 5's top-as-answer versus top-as-ignorance, the same clause the review cites, pointing the other way. Rung found at 1 (the emitted target refuses at its own compiler, so the harm is a failed downstream build, not a silent wrong answer). Ceiling STRUCTURAL, because membership is decidable from the type environment. Next-rung trigger: split the roster three ways, sufficient for a closed single-constructor product to be adjudicated as closed and an unresolved type to refuse as unresolved; the nineteen sites are that trigger's acceptance corpus, not its debt. NOT IN THIS COMMIT, AND NOT A DEFECT: the required run also refused on COMPLETED-OVER-COST-REQUIREMENT for v2.test.emit.rust_produced_decl_emit.rust_produced_decl_name_discriminates at cost=507ms against a 500ms CPU budget, in a file this PR does not touch, with claims_failed=0, unexpected_failures=0 and 13/13 changed witnesses passed. That is the known near-the-line variance class; the remedy is a rerun, not a diff. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf * Correct this change's own scope sentence about what ConstructorsOpen covers The note above `ConstructorRoster` read "GENUINELY OPEN, and refused nowhere: Int and String columns", enumerating two states. That is false, and it is false in the way the paragraph DIRECTLY ABOVE IT warns against: that paragraph corrects an earlier draft for understating scope and calls it a rung-honesty defect, because "a scope sentence nobody can check against the code is the same failure as an inflated one, pointing the other way". This sentence committed the same error one paragraph below its own warning. `ConstructorsOpen` is an ELSE branch. It is not the set {Int, String}; it is everything that is not optional, not a witness, and carries no Disj connective -- three states with three different correct answers: - a genuine open scalar, where a finite literal set cannot cover the value space and a witness is owed; - a SINGLE-CONSTRUCTOR PRODUCT (a record, no `|`, hence no Disj), which is CLOSED with exactly one constructor and whose total destructure is total; - a type whose lookup FAILED, where resolve_scrutinee_type returns the node unchanged -- IGNORANCE, NOT AN ANSWER. The note now names all three, carries the live specimen (v2.std.grammar derive_grammar_relation_token_edges_recursive_step, whose nested DeriveGrammarRelationTokensProgress column is a three-field record), records the measured nineteen-site false-positive population that reverted the obvious fix, and names the three-way roster split as the next-rung trigger with those sites as its acceptance corpus. FOUND BY READING THE APPROVAL RATHER THAN BANKING IT. review 59419 credited this block for "honestly naming what stays open (Int/String columns) as a next-rung trigger". The block does exist and does say that, so the credit was accurate -- but checking it is what surfaced that the sentence itself was incomplete. An approval resting on a claim the code only partly supports is harder to catch than one resting on an absent artifact. ANNOTATION ONLY, so §4c's annotation-erased projection means no semantic change: the stage0 mirror is byte-unchanged (verified, zero diff) and no regen is owed. Full-root compile is clean at 0 blocking errors. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01XMY7pX8yLX44MtbRPpFeuf --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

gunbai-bot Bot changed the title ~~Repair #9400's 15 floor failures: owner_module_path threading cascades type errors through srv3_host_effect_apply_witness_test.dag; main is green both sides so these are the diff's own~~ Bind floor witnesses to owner-qualified declarations Aug 27, 2026

gunbai-bot Bot marked this pull request as ready for review August 27, 2026 12:02

gunbai-bot Bot force-pushed the session/calm-lark-589-fix branch 2 times, most recently from 734e6ff to 3f95218 Compare August 27, 2026 17:03

gunbai-bot Bot force-pushed the session/calm-lark-589-fix branch 2 times, most recently from c9f627d to bd5e3aa Compare August 27, 2026 18:41

gunbai-bot Bot mentioned this pull request Aug 27, 2026

compiler direction #9502

Closed

6 tasks

gunbai-bot Bot force-pushed the session/calm-lark-589-fix branch 2 times, most recently from d774351 to 28d53f2 Compare August 27, 2026 20:16

Brian Searls and others added 14 commits August 27, 2026 21:54

Bind floor witnesses to their intended declaration owners

2086793

Complete the RFC 8118 anchor rename

69f383a

Use the RFC-qualified anchor in the selector witness

c81062b

Admit owner-qualified namespace transition

0f0c028

Receipt the transition admission roster

8f8d86a

Prune the stale citation transition admission

b9c388e

Refresh the admission receipt after membership split

03e625a

Keep transition admissions const-authored

50dfd7c

Receipt the const admission subject split

cd96642

Type CWC fold algebras at their declaration

c6043b1

Restore the transitive callable ambiguity probe

19b30b4

gunbai-bot Bot force-pushed the session/calm-lark-589-fix branch from 28d53f2 to 19b30b4 Compare August 27, 2026 21:54

briansrls merged commit 7c079cd into main Aug 27, 2026
1 of 2 checks passed

briansrls deleted the session/calm-lark-589-fix branch August 27, 2026 22:43

gunbai-bot Bot mentioned this pull request Aug 28, 2026

Consume the modeled sidecar predicates instead of re-spelling them in Rust (review 56971 follow-up to #9499) #9527

Merged

gunbai-bot Bot mentioned this pull request Aug 28, 2026

The annotation-carrier witness re-pointed its planted citations and the exemption roster did not follow: 5 declarations findings on main #9645

Merged

gunbai-bot Bot mentioned this pull request Aug 31, 2026

INTAKE-AGENT-0A: an observed duplicate is refused; completeness is not claimed; the receipt's architecture is checked #9784

Merged

Navigation Menu

Repository navigation

Bind floor witnesses to owner-qualified declarations - #9436

Bind floor witnesses to owner-qualified declarations#9436
briansrls merged 14 commits into
mainfrom
session/calm-lark-589-fix

gunbai-bot Bot commented Aug 27, 2026 •

edited

Loading

Uh oh!

gunbai-bot Bot commented Aug 27, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gunbai-bot Bot commented Aug 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Test plan

Uh oh!

gunbai-bot Bot commented Aug 27, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

gunbai-bot Bot commented Aug 27, 2026 •

edited

Loading