Skip to content

Split type_reference_decl_file's String into TypeDeclarationProvenance: the state that meant 'no identity' becomes a constructor - #10006

Merged
gunbai-bot[bot] merged 17 commits into
mainfrom
session/quick-crab-396-pr1
Sep 2, 2026
Merged

gunbai-bot[bot] merged 17 commits into
mainfrom
session/quick-crab-396-pr1

Conversation

@briansrls

@briansrls briansrls commented Sep 2, 2026 •

Copy link
Copy Markdown
Contributor

The finding: an analysis scoped to the wrong range is indistinguishable from one that does not exist

Before authoring a coproduct arm named Refused, I ran a corpus-wide collision census — over type names. It came back clean, so I authored the name. required-regen then refused:

variant 'Refused' appears in both 'TypeRealizationDecision' and 'EmitterOutcome'

Re-running the census over variant spellings found Refused live in six declaring types. RealizationRefused is in none.

The defect was not a missing analysis. The compiler already computes exactly this collision — it is what refused. But it computes it during v2 self-compile over one resolved closure, and the question being asked was about the corpus. Same subject, two ranges. From the author's seat, the narrow analysis's silence was indistinguishable from a negative result.

This is filed as a receipt on empty_observation_narrow rather than as a new class, because it is that row's own conflation with the scope quantifier moved: not an observation that could not express what changed, but one that could not reach where the answer lived. DESIGN §2 prices a fresh authority for an existing concept as a failed decomposition.

Next-rung trigger, named as the capability rather than an artifact: a corpus-wide namespace census over every type declaration and every coproduct arm, sufficient to answer "is this spelling already declared anywhere in the corpus" before a name is authored rather than after emission. One census over the one Node tree — two checks over one namespace is the range split that produced this instance. Not built here.

The generalisable half: the ordinary word is the dangerous one. A distinctive coined name is the safe case.

The change

v1.compiler.coercion keyed type realization on decl_file: String, where the empty string silently meant "no declaration identity" — indistinguishable from a real answer. That is state_space_conflation's third form, already filed. This replaces it with std.coercion TypeDeclarationProvenance = CorpusDeclared | KernelMinted | DeclarationIdentityAbsent, and the recognizer is homed beside its minter kernel_span so the kernel arm derives from the minter rather than re-spelling its "<kernel:" test a fifth time. TypeRealizationDecision gains a RealizationGround, so a bare-table answer now carries GroundedByUnidentifiedBareRow instead of passing as grounded.

The census that justified it (#10002) is upstream; this is the root cut.

A second specimen, and it is unusually good

accepted_source_emits_uncompilable_target gains its second instance. carrier_realization_census identity_query_provenance declared a return type of TypeDeclarationProvenance and answered it in five arms: three returned the bound provenance, two returned "". The front end accepted it with zero blocking diagnostics, emit produced the mirror, and rustc refused at E0308.

The empty-string arms were the exact conflation this change exists to make unwritable, surviving inside the change that makes it unwritable.

Recognition rule: a match mixing a coproduct constructor with a kernel literal is invisible to a reader checking that every arm is present, because exhaustiveness holds and only the arm types disagree.

The rung does not move. The refusal fired in the target compiler, one phase and one language too late, and the .dag front end that had every fact needed to refuse it did not. The class stays mechanically preventable; this sharpens the existing trigger rather than replacing it.

Citations: a name may be a String, an identity may not

The floor's declarations phase raised 14 CITED-DECLARATION-ABSENT findings. A census that enumerated a defect, landing in the change that deletes the defect's subjects, would have every decl_ref pointing at a declaration no module declares — which is unlanded_citation_indistinguishable_at_the_citing_end wearing the reverse costume.

A retired spelling denotes nothing in the current tree and belongs in prose; a successor resolves and belongs in a decl_ref the index walks. So the pointers are re-aimed and the dead spellings stay verbatim in the keys_on, holder_expression and why_* fields, with both carriers stating the mapping.

Cross-carrier note. gunbc.bare_name_identity_consumer_census is another lane's. It keeps the five re-aimed pointers — a citation repair that re-judged nothing. The sentence judging what this change did to those sites' rung was deliberately moved out of it and homed here, because a rung claim about another lane's subject, authored by someone else, is how two rosters end up disagreeing about one class. The judgement is the weaker of the two available readings: the stamp is a rung on visibility and not a repair of the keying, and neither roster claims the second from the first. Reading this climb as a repair would retire rows that are still live.

Evidence

  • parse OK 4511 file(s) parse-clean
  • mirrors: 12 regenerated, verified in three passes — install, then a binary rebuilt off the installed seed (first_generation_equal=true, 150/150/150, declared_divergent=1 [main.rs] pre-existing), then --required-regen-fixed-point (fixed_point_equal=true referenced_first_generation_equal=true). Three because a single pass runs a binary predating the change it emits and can self-verify at divergence 0 for the wrong reason.
  • docs/design-ledgers.md regenerated through main_wet_one, never hand-edited. Vintage control: it rewrote all bytes and only the authored lines changed.
  • the predicted RED is enrolled — reference_realization_witness_test asserts RealizationRefused { cause: DeclarationIdentityUnavailable }.

Where this regeneration can run, recorded so the next lane does not rediscover it slowly: BuildBuddy refuses it. main_wet_one peaks at 8.37 GiB and the remote runner answered MemoryStallRefusedPageThrash — 176690 major faults/minute while computing for 5% of the wall. It fits a session container's cgroup allowance and was run locally.


The range finding, one layer up: the floor runner had the same defect

Landing the split tripped the floor's changed-witness sublane, and the cause is this PR's own finding wearing a different costume.

required_floor_runner derives changed_witness_set from the run's git diff, which is root-agnostic. It emits disposition rows only while enumerating discovered files, which is scoped to --source-root dag --source-root src/v2. The selector's range is strictly wider than the enumerator's, so a witness homed under src/v1 is selectable and undeclarable by construction — and the guard that would have named it, ChangedWitnessOutsidePreparedSubject, sits inside the per-discovered-file loop those modules never enter. Any PR editing a src/v1 witness that declares test fns refused with identities no in-diff edit could satisfy.

This is a denominator mismatch, not a missing check — the same shape as the variant collision above, and the reason both are worth one entry rather than two incidents.

The undiscoverable selection is now a typed decline, DeclinedChangedWitnessOutsideDiscovery, counted in the disposition receipt and printed by identity. A decline and not a filter, deliberately: dropping the selection would have greened the floor by making the over-selection invisible, which is the absorbing arm.

Why this PR grew: the arm's authority did not exist as data

Declining is not enough — every decline blocks, so the fix converted one refusal into 17 blocking rows. The exemption had to be keyed on the identity's home being a declared non-executing root, and that roster did not exist.

The fact "the required fold does not reach src/v1" lived in three String declarations in gunbc.ci_layer_roots. That is exactly the §4c case — an invariant in prose a machine cannot join on — and one of them was load-bearing for a gate arm, which is why the arm had to be stopped rather than allowed to infer it. Discovering that is the result, not the overrun.

So the authority is now non_executing_witness_module_prefixes, with a typed DissolutionCondition naming the capability: bare cross-module references binding by containment, vehicle the namespace cut — satisfied by neither a faster floor nor adding --source-root src/v1, since both leave the twelve last-segment collisions standing.

Keyed on membership, never on absence. The arm requires the home to be in that roster; an unreadable or empty roster exempts nothing. It is deliberately not !witness_layer_roots().contains(home) — that grants the exemption by absence, so an unrostered tree or a typo'd path would go silently non-blocking, and it substitutes "not declared executing" for "declared non-executing", which are different claims: only the second carries the §4b(2) stall and its trigger.

The grain is forced, not chosen. I first modeled a filesystem root and re-grounded it: this population is undiscovered by definition, so no path exists at the arm to compare against a directory, and the authored module identity is the only available fact. Measured rather than assumed — every v1.* module lives under src/v1, zero outside. The converse is inexact (four fixture modules under src/v1 carry other names) and those stay blocking, because the narrower exemption is the fail-closed side of an inexact join.

witness_fold_src_v1_coverage_gap_note is retired, not left beside the row: two authorities for one fact is the nickname §3 forbids. Its irreducible rationale is preserved at the roster; its "116 test fn" figure was a dated observation and is not re-asserted as live. v1_claim_scoped_witness_batch_deleted_note and v1_dead_witness_tree_triage_receipt are the same §4c debt, deliberately left standing.

The exemption evaporates on its own trigger. When the namespace cut lands, v1 leaves the roster and the arm goes dead by construction. It has no independent dissolution condition because it has no independent existence.

Controls, executed on the merged head

required-floor: changed_witnesses=20 changed_witness_blocking=0
                changed_witness_declined_in_declared_nonexecuting_root=17
17x [changed-witness] standing=declined-in-declared-non-executing-root
 3x [changed-witness] standing=planned-and-passed
required-floor: verdict=FloorClean
  • the src/v1 witness declines with the typed row, named;
  • positive control: the 3 changed witnesses inside the discovery roots still disposition normally and pass — a decline that swallowed everything would show 20;
  • discovered-file population unchanged, arithmetically from this run's own line: declared=15368, and 3488 + 366 + 0 + 49 + 11293 + 5 + 167 = 15368 exactly. The 17 are outside that sum because they were never in the declared population — which is why they were unrepresentable before.

A note on regeneration cost

A generated file whose producer is itself a generated mirror needs its producer installed a pass earlier, so an emitter change costs one regen pass per level of the chain. Three passes here. The second specimen was main's #10056 touching v1_compiler_infer.rs, not this branch — which is what establishes it as a property of generated emitters rather than of this diff.

🤖 Generated with Claude Code

https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf

briansrls and others added 6 commits September 2, 2026 04:56
…occurrences, six classes, and one class already filed

Enumerated from the DECLARATION -- v1.compiler.coercion type_reference_decl_file plus its
repaired sibling v1.compiler.emit_rust type_reference_decl_file_in_env -- and every call
occurrence under src/, classified by the TERMINAL PREDICATE each String result reaches rather
than by caller or file. A module-name grep cannot see a bare call and under-reports.

39 reproduces exactly and decomposes: 37 plain call occurrences + the declaration line + one
occurrence inside an instrument that exists to MEASURE the legacy answer. Four of the 37 sit
inside the repaired sibling's own fallback body and are not independent consumers, leaving 33
independent production occurrences; five further sites already route through the sibling.

Six classes. Two decided ones (native-numeric realization, 12; checkpoint applicability, 25)
whose repair is NOT a call-site sweep: both terminal predicates substring-match rosters of FILE
PATHS, so routing occurrences to a DeclarationRef without re-keying the rosters moves the
position from the call site into the authority. The tree already contains the failed version of
that repair -- v1.compiler.infer literal_boundary_elaboration recovers a DeclarationRef by
identity and then calls declaration_file_of on it to get a FILE back, purely so
decl_file_realizes_natively can contains() it. Two classes dispositioned CORRECT AS POSITION
under DESIGN section 3's carve-out and counted only so the denominator closes: a refusal payload
that fires precisely because identity was unavailable, and the instrument. One class dissolves
with the helper.

The kernel-minted class is a RECEIPT against gunbc.recurring_failure_mode state_space_conflation's
third form, not a new filing: that row already names this symbol set, and this census reaching
the same four authorities from the opposite direction is corroboration of its recognition rule.
Recorded with it: std.repair_input_origin was read and does not model this axis -- it partitions
the same String by producer, and its own header defers the DeclarationCarrier half to XL-0B/C --
and any KernelMinted arm must derive from v1.compiler.infer_env
resolved_node_is_kernel_identity_for_name's exact equality rather than add a fifth prefix test.

Also carried, because it changes ownership rather than the finding: XL-0B's identity route is
partly landed and is already consulted AHEAD of the legacy answer inside five declarations, so
those occurrences are fallback arms behind an existing route and converting them from this lane
would be parallel authority.

The disposition vocabulary is constructed, not checked: there is no variant spelling "rewrite the
call site", so the sweep this census argues against cannot be filed. The witness guards the two
propositions the coproducts could not make unwritable -- a class with no exhibitable specimen,
and a conversion naming no authority or an irreducible class naming one -- with no count asserted
against a literal. Rung: the class sits at mitigatable and this carrier counts rather than
refuses; the carrier's own rows are hand-classified, and its dissolution names the derived lens
as the capability that retires it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
…: defer the occurrence scope rather than negotiate it

The row read as though the nine occurrences behind XL-0B's landed identity route were
someone else's work. They are not. The exact-binding route answers WHICH DECLARATION and is
XL-0B's; the rosters answer WHAT THAT DECLARATION REALIZES AS, positionally, and are this
lane's. A reference the bindings table has no row for still falls through to a contains()
roster keyed on file paths, so the fallback arms have a condition owned by one authority and
an answer owned by the other.

What follows is deliberately not a conversion plan. Once the answer side is keyed on
identity, "should this fallback arm exist at all" becomes answerable in a way it is not
today, and a fallback behind a route that now answers correctly is dead code rather than a
migration subject. So the occurrence scope is DEFERRED and will be re-measured rather than
negotiated: pricing it now would price a population that may not survive.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
…ation it had inherited

None of the three is a member of the 39 and none is fixed here. They are filed because each
sits directly under the repair the classes prescribe, so a reader planning that repair meets
them, and because the first changes what such a repair may CLAIM about its own authority.

v1.std.core kernel_span and v1.compiler.infer kernel_span are byte-identical declarations of
one minter. v1.compiler.infer declares its own while also importing the other, so its 24
in-file call sites bind the local twin by shadowing and every other consumer binds the
v1.std.core one. Nothing observable differs today, which is the point: the kernel-provenance
arm must derive from the minter by exact equality, and a derivation from either twin is
correct only BECAUSE the bodies agree -- a coincidence the tree does not enforce. Such a
repair may say it consumes the authority coercion imports; it may not say it consolidated one.

Eleven citations name module v1.compiler.core, which no file declares; the declarations they
reach for live in v1.std.core. One of the eleven is the annotation directly above
is_kernel_minted_file, the predicate that repair deletes, so a reader following it to check
the derivation is sent to a module that does not exist. This carrier had inherited a twelfth
occurrence from a prior carrier's spelling and corrects it rather than adding to the
population -- which is how the count was noticed.

v1.compiler.type_head_exposure type_declaration_identity_key builds concat(decl_file, "::",
declared_name): a sixth representation of declaration identity, and the one furthest from a
symbol, since the position and the name are fused into a value nothing can read back apart.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
…: delete the 95-site identity channel

The identity key was a decl_file String threaded to ninety-five call sites so each could ask
lookup_checkpoint to make the same decision at the periphery. Nothing had to be built to make
the mint decide -- type_realization_decision was ALREADY the single dispatcher, consulting both
rosters, handling the unknown case, and routing migrated bare rows to the exact binding. The
only defect was where it was called from. DESIGN section 3: the dispatch that selects a
realization is itself realization, so it sits peripheral and never in the interface; a
ninety-five-site-wide identity channel was that sentence inverted.

So the decision is taken at type_reference_realization / declaration_realization, from the node,
and what travels is a std.coercion TypeRealizationDecision. A NAME MAY BE A STRING; AN IDENTITY
MAY NOT -- dag_name stays a parameter, because which peel of a reference is meant is a fact the
site holds and a mint could only guess.

THE STATE SPACE SPLIT RIDES ALONG AND IS THE REASON THIS IS ONE MOTION. The String carried three
disjoint inhabitants -- a corpus path, the synthetic pseudo-file kernel_span mints, and "" for
unknown -- while consumers discriminated only empty from non-empty. std.coercion
TypeDeclarationProvenance is those three as constructors, minted by v1.std.core
declaration_provenance_of, homed beside kernel_span and deciding the kernel arm by EXACT
EQUALITY against the minter rather than by a prefix test over its output. Deleted with it:
is_kernel_minted_file, the literal "<kernel:" row inside numeric_realization_declaring_modules,
the empty-string guards, lookup_checkpoint, type_reference_decl_file, decl_identity_file,
declaration_file_of, and the peripheral form of rust_seed_host_numeric_alias.

declaration_file_of had exactly one consumer: v1.compiler.infer literal_boundary_elaboration,
which recovered a DeclarationRef by identity and then projected it back down to a path so a
contains() roster could match it. It is now declaration_provenance_of_ref, answering from the
binding's own node. std.operator_realization OperandDeclaration likewise carried a DeclarationRef
AND a decl_file -- one identity in two representations -- and carries the provenance instead.

TWO QUESTIONS THE DECISION COULD NOT ANSWER, WIDENED RATHER THAN ROUTED AROUND. A checkpoint row
and a host numeric alias both produced a Realized, so sites asking "is this the host numeric"
re-derived it by consulting the numeric roster a second time with the same name and file -- that
second consult was the identity channel for those sites. Realized now carries a
RealizationGround. Its third arm, GroundedByUnidentifiedBareRow, makes the declared decl_file==""
rung drop visible: an answer given with no declaration was previously indistinguishable from one
keyed on a real declaration, and is now countable and refusable. The drop itself is unchanged and
its restoration trigger is not discharged.

Refused's cause was a String whose inhabitant "declaration identity unknown: empty decl_file" was
the sentinel promoted one level and re-encoded as prose; it is a five-arm
RealizationRefusalCause. dag/test/claim/reference_realization_witness_test asserted that
sentence and RED as expected -- updated here to assert the typed cause, not routed around and not
kept green by preserving the prose.

Every answer is preserved bit for bit; the climb is in the state space, not in an output. The
two instruments shrank rather than converted. gunbc.recurring_failure_mode state_space_conflation
gets a climb receipt appended rather than replaced, per DESIGN section 4b(4). Superseded notes in
v1.compiler.coercion are headed by a supersession paragraph rather than silently rewritten.

HONEST RESIDUE, with a named successor: CorpusDeclared still carries a path matched by contains,
so what a declaration realizes as is still answered positionally. v1.compiler.infer_env
global_bare_fallback_invariant already states the terminal key -- filepaths are irrelevant, the
declared module path is the containment tree -- and re-keying that arm needs a declaration
reference at each gate.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
…seven far consumers

`Disposition` is declared by std.disposition and `CensusBasis` by
gunbc.bare_name_identity_consumer_census. Declaring either a second time makes the bare name
AMBIGUOUS across the whole corpus -- v1.compiler.infer_env global_bare_fallback_invariant keeps
every homonym's full candidate list and refuses far uses of a tied name -- so the floor refused
seven sites that have nothing to do with this carrier: gunbc.host.host_standup (three),
gunbc.host.host_standup_assimilation_deduction, v2.std.decl_index, v2.lens.enforcement.vocab and
a qualified-name test, all `unresolved type 'Disposition'`.

Renamed to OccurrenceDisposition and OccurrenceCensusBasis. No content changes.

The failure is instructive and is exactly what this carrier's own subject warns about, which is
why it is recorded rather than quietly fixed: I checked the names I INVENTED for this change
against the corpus and found them free, and did not check the names that felt generic enough to
be safe. Genericness is what makes a collision likely, not what makes it unlikely. The check is
mechanical -- enumerate type/fn/data/variant declarations and look for the name -- and it now runs
over every introduced name rather than over the ones that looked risky.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
@gunbai-bot gunbai-bot Bot changed the title type_reference_decl_file: 39 legacy occurrences — census and disposition at class grain, real specimens only Consult the realization roster once at the mint and thread the answer: delete the 95-site identity channel Sep 2, 2026
briansrls and others added 7 commits September 2, 2026 05:40
…sed ones from the instrument

v1.compiler.emit_rust references declaration_provenance_of, type_reference_provenance and
provenance_is_kernel_minted without importing any of them -- caught by a scan over every symbol
this change introduces rather than by reading, which is the only way a missing import in a
17,000-line module is found before the compiler finds it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
The roster measured a tree in which type_reference_decl_file still existed. Its rows stay exactly
as measured -- a census edited to match the repair it prompted stops being evidence the repair was
needed -- and a receipt beside them records what was discharged, so nobody reads the roster as a
live work list.

The receipt also records where the roster was WRONG, which is the part worth keeping. Both decided
classes prescribed re-keying the roster before moving any occurrence. That was right about what not
to do and wrong about the unit: the roster's new key could only be produced at the 19 sites already
carrying a TypeEnv, so re-keying forces the occurrence conversion into the same change or a two-key
intermediate. The channel's WIDTH was the defect, not a cost to absorb -- and a census that counts
occurrences is structurally disposed to miss that, because it prices the sites and the sites were
never the unit.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
The `type_reference_provenance` insertion landed after the trailing
comma of the previous line, leaving a line beginning with `,` inside
the import brace. The parser refused with `expected name, found Comma`,
which refused the whole module index (`1 unparseable .dag source(s)`)
and cascaded into 18 `source annotation names no subject` diagnostics
at 13118-13135 — that block is an ordinary leading annotation over
`fn ancestry_binding_is_kernel_identity` and has a subject; the
parser had already given up before reaching it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
…ound the witness omitted

The floor reported three things and all three are this branch's.

PARSE IS CLEAN: 4511 file(s) parse-clean, so the 04_infer import repair holds.

DECLARATIONS, 14 findings. This census enumerated a defect and the same change
deleted the defect's subjects, so every decl_ref in it pointed at a declaration
no module declares. The index refuses that as CITED-DECLARATION-ABSENT, and it is
right to: a census citing dead symbols is indistinguishable at the citing end
from one citing live code -- `unlanded_citation_indistinguishable_at_the_citing_end`
wearing the reverse costume.

The split follows the peeler ruling applied to citations. A NAME MAY BE A STRING,
AN IDENTITY MAY NOT: a retired spelling denotes nothing in the current tree and
belongs in prose; a successor resolves and belongs in a decl_ref the index walks.
So the pointers are re-aimed and the dead spellings stay verbatim in the `keys_on`,
`holder_expression`, `what_is_emitted` and `why_*` fields, where they are data
about history rather than claims about the tree. Nine in the occurrence census,
five in gunbc.bare_name_identity_consumer_census, and each carrier now states the
mapping and why its prose still names the dead form.

NO ROW'S FINDING CHANGED, which is the part worth being explicit about. The split
made the ABSENCE of declaration identity a constructible state, so a bare-table
answer is stamped GroundedByUnidentifiedBareRow rather than being indistinguishable
from a grounded one. It did NOT stop those sites keying on the bare name -- every
`site`, `keys_on`, `outcome` and `reach` is about a call site the split did not
touch and still holds. The stamp is a rung on visibility, not a repair of the
keying, and neither roster claims the second from the first.

FLOOR: self_host_symbol_identity_binding_witness_test built Realized without the
`ground` field this change added. Its checkpoint comes from the table, so the
honest ground is GroundedByCheckpointRow. The stale annotation in
std.reference_realization naming `Realized { checkpoint }` is corrected to match.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
dag/gunbc/recurring_failure_mode.dag gained the state_space_conflation climb
receipt and docs/design-ledgers.md is a generated projection of that roster, so
the generated-artifact phase would have refused the pair as drifted. Regenerated
through the modeled route rather than hand-edited:

  gunbc run --source-root dag --source-root src/v2 \
    --entry dag/gunbc/instruments/generated_artifact_gate.dag \
    --function main_wet_one --arg path=docs/design-ledgers.md

VINTAGE CONTROL, because a projection regenerated by the wrong compiler is drift
that looks like a repair. The session's /usr/local/bin/gunbc is too old to resolve
the current corpus (it refuses on plan_registry, the srv3 modules, NonEmptyStr and
SecretRef), so the binary was built from this tree. The evidence that it is the
right vintage is the diff: main_wet_one rewrote all 253073 bytes and exactly one
line changed -- the receipt this branch authored. Every other byte reproduced
identically, which is the control a bare "it ran" would not have.

The remote route was tried first and cannot hold this artifact: BuildBuddy refused
with MemoryStallRefusedPageThrash at 176690 major faults/minute for 5% CPU share.
main_wet_one peaks at 8.37 GiB, above that runner's allowance and inside this
container's cgroup memory.max.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
Two conflicts, resolved by construction rather than by picking a side.

dag/gunbc/type_reference_decl_file_occurrence_census.dag was an add/add: #10002
squash-merged the census onto main while this branch carried the same file plus
the citation re-aiming. Diffed both sides before resolving -- main's side adds
nothing this branch lacks, its only difference IS the nine pre-split citations,
which name declarations this branch deletes. Took this branch's side because it is
the strict superset, not because it was ours.

docs/design-ledgers.md came back from the generated-artifact merge driver UNMERGED
with no conflict markers and the ours side verbatim, which is the driver refusing
rather than answering: both sides changed a generated projection since the merge
base, so neither side's bytes are the projection of the MERGED authorities and
taking either drops the other's authority-derived content. Regenerated through
main_wet_one as the driver instructs. It is now 270827 bytes, carries main's new
rows AND this branch's climb receipt, and against origin/main differs by exactly
the one line this branch authored.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
…, and file the range finding

THE RESULT HERE IS NOT THE COLLISION, IT IS THE RANGE. required-regen refused
with `variant 'Refused' appears in both 'TypeRealizationDecision' and
'EmitterOutcome'`. Before authoring that arm I HAD run a corpus-wide collision
census -- over TYPE names. Re-running it over VARIANT spellings found `Refused`
live in six declaring types and `RealizationRefused` in none.

The compiler already computes this collision; it is what refused. But it computes
it during v2 self-compile over ONE RESOLVED CLOSURE, and the question being asked
was about the CORPUS. Same subject, two ranges, and from the author's seat the
narrow analysis's silence was indistinguishable from a negative result. An analysis
scoped to the wrong range is, from the caller's seat, indistinguishable from an
analysis that does not exist.

Filed as a receipt on `empty_observation_narrow` rather than as a new class: the
mechanism is that row's own conflation with the scope quantifier moved -- not an
observation that could not EXPRESS what changed, but one that could not REACH where
the answer lived -- and DESIGN section 2 prices a fresh authority for an existing
concept as a failed decomposition. Its next-rung trigger is named as the capability:
a corpus-wide namespace census over every type declaration AND every coproduct arm,
sufficient to answer "is this spelling already declared anywhere" before a name is
authored. ONE census over the one Node tree; two checks over one namespace is the
range split that produced this instance.

SECOND SPECIMEN for `accepted_source_emits_uncompilable_target`.
carrier_realization_census identity_query_provenance returned a
TypeDeclarationProvenance in three arms and "" in two. The front end ACCEPTED it,
emit produced the mirror, rustc refused at E0308. The empty-string arms were the
exact conflation this change exists to make unwritable, surviving inside the change
that makes it unwritable. The rung does NOT move: the refusal fired in the target
compiler, one phase and one language too late, so the class stays mechanically
preventable and this sharpens the existing trigger.

CROSS-CARRIER EDIT, narrowed. gunbc.bare_name_identity_consumer_census keeps the
five re-aimed pointers, which are a citation repair that re-judged nothing. The
sentence judging what the split did to THOSE sites' rung was moved out of it and
homed in this change's own census, because a rung claim about another lane's
subject, authored by someone else, is how two rosters end up disagreeing about one
class. The judgement itself is unchanged and deliberately the weaker reading: the
stamp is a rung on VISIBILITY and not a repair of the keying, and neither roster
claims the second from the first.

MIRRORS: 12 regenerated and verified to a fixed point.
  pass 1  installed the 12 named files
  pass 2  from a binary rebuilt off the INSTALLED seed: first_generation_equal=true,
          planned=150 executed=150 adjudicated=150, declared_divergent=1 [main.rs]
          which is pre-existing
  pass 3  --required-regen-fixed-point: fixed_point_equal=true
          referenced_first_generation_equal=true
Three passes because a single pass runs a binary that predates the change it emits
and can self-verify at divergence 0 for the wrong reason.

WHERE THIS REGENERATION CAN RUN, recorded so the next lane does not rediscover it
slowly: BuildBuddy refuses it. main_wet_one peaks at 8.37 GiB and the remote runner
answered MemoryStallRefusedPageThrash -- 176690 major faults/minute while computing
for 5% of the wall. It fits this container's cgroup allowance and was run locally.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
@gunbai-bot gunbai-bot Bot changed the title Consult the realization roster once at the mint and thread the answer: delete the 95-site identity channel Split type_reference_decl_file's String into TypeDeclarationProvenance: the state that meant 'no identity' becomes a constructor Sep 2, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review September 2, 2026 09:02
Brian Searls and others added 4 commits September 2, 2026 09:29
rust-unit-tests refused with E0061 in compiler_tests.rs: is_copy and
coerce_primitive_type now take the decision rather than (target, dag_name,
decl_file), and this file is hand-maintained seed, not a regenerated mirror, so
required-regen's fixed point says nothing about it. It compiles under
`cargo test --lib` and under `clippy --all-targets`, and under nothing else --
which is why three green regen passes sat above a red test target. Worth stating
plainly: the fixed point I reported was real and it was not evidence about this
file.

All 32 sites passed "" as decl_file, i.e. the no-declaration-identity case, so
each becomes type_realization_decision(target, name, DeclarationIdentityAbsent)
and every asserted value is unchanged. That the expectations all still hold is the
useful part: the split preserves every prior answer and only makes the ground
explicit.

Local `cargo test --release -p v1-compiler --lib`: 644 passed, 1 failed,
141 ignored. The one failure is shell_service_unmodeled_output_key_refuses, which
is main's -- no file in this diff is on the shell-service path -- and has a fix in
flight.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
…-executing witness root

THREE THINGS, and the third grew the PR for a reason worth stating.

REQUEST_CHANGES (codex review 58658) IS FIXED, NOT ARGUED. provenance_is_kernel_minted
was a Bool view that re-matched the coproduct this change introduces -- the parallel
representation the split exists to remove, and DESIGN section 5 prefers a single
authority from which the realization is derived over a check that re-states it. It had
exactly one caller, so the dissolution is total: rust_operand_realization_of_type matches
KernelMinted directly, the predicate is deleted from v1.std.core, the import is gone, and
the census row that cited it now names std.coercion TypeDeclarationProvenance -- the
constructor that actually answers the question. An earlier reviewer considered and dropped
this note; an approval is a hygiene check, not evidence, so it did not settle it.

THE CHANGED-WITNESS RANGE FIX NOW HAS A DISPOSITION. Converting the undiscoverable
selection into a typed decline moved the refusal rather than removing it: every decline
blocks, so 17 declines became 17 blocking rows. The exemption is keyed on MEMBERSHIP in a
declared roster, never on the absence of a match in witness_layer_roots -- "not declared
executing" and "declared non-executing" are different claims, and only the second carries
the 4b(2) stall and its trigger. Keying on the first would grant the exemption BY ABSENCE,
so an unrostered tree or a typo'd path would go silently non-blocking.

AND THAT ROSTER DID NOT EXIST AS DATA, WHICH IS THE RESULT RATHER THAN THE OVERRUN. The
fact "the required fold does not reach src/v1" lived in three String declarations in
gunbc.ci_layer_roots -- exactly the DESIGN section 4c case, an invariant in prose a machine
cannot join on -- and one of them was load-bearing for a gate arm that consequently had to
be told to stop rather than infer it. So the arm's authority is now
non_executing_witness_module_prefixes with a typed DissolutionCondition naming the
capability (bare references binding by containment; vehicle, the namespace cut; satisfied
by neither a faster floor nor adding --source-root src/v1).

THE GRAIN IS FORCED, NOT CHOSEN, and I re-grounded it mid-implementation after first
modeling a filesystem root. This population is undiscovered BY DEFINITION -- no file was
enumerated -- so no path exists at the arm to compare against a directory, and the authored
module identity is the only fact available there. Measured rather than assumed: every
module named v1.* lives under src/v1, zero outside. The converse is inexact -- four fixture
modules under src/v1 carry other names -- and those stay blocking, because the narrower
exemption is the fail-closed side of an inexact join.

witness_fold_src_v1_coverage_gap_note is RETIRED rather than left beside the row: two
authorities for one fact is the nickname section 3 forbids, and the String was the half no
mechanism could read. Its irreducible rationale (why the one-token --source-root fix was
refused) is preserved at the roster; its "116 test fn" figure was a dated observation and is
not re-asserted as live. v1_claim_scoped_witness_batch_deleted_note and
v1_dead_witness_tree_triage_receipt are the same 4c debt, deliberately untouched here.

EVIDENCE: regen first_generation_equal=true 150/150/150 (declared_divergent=1 [main.rs],
pre-existing); cargo test --release -p v1-compiler --lib 647 passed 0 failed 141 ignored --
shell_service_unmodeled_output_key_refuses now passes with main's #10025 merged, so the
earlier "not mine" is verified rather than asserted. Generated conflicts (design-ledgers.md,
compiler_tests.rs, v1_compiler_compiler_tests_rust.rs) came back UU with NO markers -- the
driver refusing rather than answering -- and were resolved by regeneration over the merged
.dag authorities, never by taking a side.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
…ities

Resolved BY REGENERATION, never by taking a side. Four conflicts, all generated
artifacts, all returned UU with NO conflict markers -- the generated-artifact driver
refusing rather than answering, which is what it is for: both sides changed a
projection since the merge base, so neither side's bytes are the projection of the
MERGED authorities. No .dag authority conflicted at all, which is what makes
regeneration the correct resolution here rather than merely the convenient one.

THREE REGEN PASSES, AND THE COUNT IS THE PRODUCER CHAIN'S DEPTH RATHER THAN A RITUAL.
Pass 1 refused on the emitter mirrors (v1_compiler_compiler_tests_rust.rs and, from
main's #10056, v1_compiler_infer.rs); pass 2, from a seed rebuilt off those, refused on
compiler_tests.rs -- the file the first mirror EMITS; pass 3 is clean. A generated file
whose producer is itself a generated mirror needs its producer installed a pass earlier,
so an emitter change costs one pass per level. The second specimen is main's change and
not mine, which is what establishes this as a property of generated emitters rather than
of this branch.

  pass 3   first_generation_equal=true planned=150 executed=150 adjudicated=150
           declared_divergent=1 [main.rs], pre-existing
  fixed pt fixed_point_equal=true referenced_first_generation_equal=true

LEDGER VINTAGE CONTROL: main_wet_one rewrote all 305180 bytes of docs/design-ledgers.md
and it differs from origin/main by exactly 3 lines -- one per roster row this branch
authored (state_space_conflation's climb receipt, accepted_source_emits_uncompilable_target's
second specimen, empty_observation_narrow's range receipt). Every other byte reproduced
identically, which is the control that separates a regenerated projection from drift
wearing a repair's face.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015KnTJBDVSyUkrxKNUF4NCf
@gunbai-bot

gunbai-bot Bot commented Sep 2, 2026

Copy link
Copy Markdown
Contributor

review 58658's REQUEST_CHANGES is fixed by construction, not argued.

provenance_is_kernel_minted was a Bool view that re-matched the coproduct this PR introduces — the parallel representation the split exists to remove, and DESIGN §5 prefers a single authority from which the realization is derived over a check that re-states it. The finding was right.

It had exactly one caller, so the dissolution is total rather than a relocation:

  • rust_operand_realization_of_type matches KernelMinted { minted_name: _ } directly at the site;
  • the predicate is deleted from v1.std.core and its import removed;
  • the census row that cited it now names std.coercion TypeDeclarationProvenance — the constructor that actually answers the question.

No Boolean view survives anywhere. An earlier reviewer had considered and dropped the same note; an approval is a hygiene check rather than evidence, so it did not settle it.

Two things the fix surfaced, both the substrate enforcing rules I could not have broken silently:

  • my rationale comment sat inside the match body, and §4c admits annotations only at module-item grain (source annotation sits inside a declaration body, four diagnostics from one block). Moved above the declaration.
  • the emitted seed tests are generated from v1.compiler.compiler_tests_rust, so the earlier hand-edit of compiler_tests.rs was a fix in the wrong layer. Reverted and fixed at the emitter; the assertions are now derived.

The residues the approving reviews flagged — CorpusDeclared still carrying a contains-matched decl_file, and the two byte-identical kernel_span bodies whose agreement nothing enforces — are unchanged and stay declared in the diff. They are named where a later reader meets them rather than quietly fixed or quietly dropped.

— sent from quick-crab-396

@gunbai-bot
gunbai-bot Bot merged commit 6764d17 into main Sep 2, 2026
6 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/quick-crab-396-pr1 branch September 2, 2026 14:45
gunbai-bot Bot pushed a commit that referenced this pull request Sep 2, 2026
…lision)

AUTHORITY ONLY, same disposition as the previous union. Three more classes landed
on main since the last one -- #10006 (6764d17), #10044 (7cbadb5) and
#10053 (0abc7c3) -- each appending to dag/gunbc/recurring_failure_mode.dag,
so both the declaration block and the roster list conflicted again. Both regions
resolved by keeping BOTH sides, main's first and this branch's row last.

Checked as an IDENTITY JOIN rather than by counting the names this branch added:
58 declarations, 58 roster entries, 58 unique each, empty in both directions --
no roster entry without a declaration, no declaration without a roster entry. A
count equality would have passed even if one of each had drifted apart.

NO PROJECTION WAS HAND-RESOLVED. DESIGN.md and docs/design-ledgers.md are
byte-identical to origin/main here, verified rather than assumed. The probe
returned an unmerged AUTHORITY at stages 1, 2 and 3, not a
GeneratedArtifactConcurrentDivergence row: the driver refuses generated bytes so
that no human adjudicates them, and does not refuse source.

STILL DELIBERATELY INCOMPLETE. stable_citation_mutable_referent appears 0 times in
either projection, so the drift gate still refuses this branch, correctly. The
regen runs once, on the tip that will carry it.

Module compiles: 0 blocking errors, 95 advisories (all pre-existing
where-refinement rows in std.decl_ref).

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FdxzwWekWhHR2FCTTf8a1b
gunbai-bot Bot pushed a commit that referenced this pull request Sep 2, 2026
…nd regenerate

#10045 and this branch independently declared arm_body_diverges in
04_infer.dag. Git merged both cleanly -- different regions, no textual
conflict -- leaving TWO declarations and call sites binding
inconsistently. Nothing textual catches this; the compiler does:

  call shape mismatch calling 'arm_body_diverges':
    no parameter named 'n' (declared: [body])

THE CONVERGENCE WENT AGAINST MINE, ON THE MERITS. My declaration
hand-rolled the block-tail recursion and matched ExprBlock only.
#10045's delegates to ownership.fold_terminal_expr, which folds through
ExprLet AS WELL AS ExprBlock. So an arm shaped `let x = ...; return y`
diverges and my predicate answered false -- the fabricated refusal my own
annotation warns against, in the code that annotation sat above.
Re-inventing a walk the codebase already owned is the DESIGN section 2
failure and here it also cost correctness. Theirs survives; my
declaration is deleted and my call site rewired to it. My rationale
carries a measured receipt (extdeps.uri_path path_segment_tokens) so it
moves onto the surviving declaration rather than being dropped, with a
note recording that two met and which won.

THE MIRRORS ARE REGENERATED, NOT RESOLVED. Four generated stage0 mirrors
conflicted. They are derived, so neither parent's copy is a valid
resolution and both were tried and both failed loudly at the build:
main's v1_std_core.rs has no Divergent, mine has no
declaration_provenance_of (#10006). The regenerated mirror carries BOTH
-- verified on the installed bytes, not inferred from a green build --
which is what no hand-picked side could produce. Regen ran with a
compiler built from pristine main, and the candidate bytes were
transferred by hash (sha256 72cd5275...) rather than trusted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
gunbai-bot Bot added a commit that referenced this pull request Sep 3, 2026
…9964)

* infer: a diverging match arm contributes nothing to the match's join

`v1.compiler.infer` built a match expression's type by folding EVERY arm's body
type with `prefer_specific_type`. An arm whose body is a `return` has the
FUNCTION'S RETURN TYPE as its body type, so a `let` bound from such a match was
typed as the union of the binding and the function's return coproduct -- and
passing that binding to a parameter declared with the binding's own type refused:

  fn f(xs: List<Cell>) -> Res {
    let cell = match cell_of(xs: xs) {
      Absent => return Unknown { why: 0 }
      Present { value } => value
    }
    Ok { cell: Cell { n: takes_cell(cell: cell) } }
  }
  error: value does not inhabit its declared type at the direct call argument for
  parameter 'cell': declared 'Product(Cell)', produced 'Coproduct(Res)'

That is a FABRICATED REFUSAL against correct .dag -- DESIGN §5's fabricated
plausible output with the sign flipped -- on the ordinary compiler floor DESIGN
§4b says must be held first: values inhabit their declared types.

THE FIX is one line of authority in `src/v1/04_infer.dag`: `arm_body_types`
excludes arms whose body diverges, via a new `arm_body_diverges` that sees both a
bare `return` and a block whose terminal statement is one. If every arm diverges
the list is empty and the existing `Absent => scrut_rt` arm stands, so no type is
invented. The re-inference pass below it re-runs only arms whose `body_type` is
NOT fully resolved, and a diverging arm's type is resolved, so no second edit is
needed there -- checked, not assumed.

MEASURED, on a compiler built from this change:
- The 22-line reproduction above refuses at resolve before, resolves after.
- `dag/gunbc/roadmap/roadmap_forecast.dag` AS IT STANDS ON MAIN -- not edited here
  -- goes from three inhabitance refusals to `PASS witness_empty_calibration_cell_refuses`.
  Those three are what `required-witnesses-floor` refused on run 33556389758.
- 4493 file(s) parse-clean.

THE EVIDENCE STAYS ENROLLED (§4b(4)). The reproduction is committed as
`test.claim.diverging_match_arm_join_witness`, which is its own regression control
in the strong sense: if the join ever re-admits a diverging arm, the module stops
RESOLVING, so its witnesses go red at resolve rather than at assertion. Four
witnesses: the binding is not widened; the diverging arm STILL RETURNS EARLY (so
the fix cannot be satisfied by dropping the arm from evaluation too); a block
terminating in `return` also diverges; and a positive control that a match with no
diverging arm still joins every arm.

THE MIRROR IS MY IMITATION OF THE EMITTER, NOT A MEASURED FIXED POINT. The Rust
mirror is hand-applied because the running compiler is the mirror, not the .dag.
I shaped it to the emitter's actual output for `|> filter |> map` -- nested loops,
matching the `original_list` chain twenty lines above it -- after first writing a
fused loop that was semantically identical and would have drifted. Only the regen
phase can confirm the pair; this commit does not claim it has.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* review 58314: route the predicate through the canonical terminal fold, and install the emitter's mirror bytes

TWO FINDINGS FROM codex/gpt-5.6-sol, both verified against the code before acting.

1. THE PREDICATE FORKED A TRAVERSAL THE REPO ALREADY OWNS. `v1.compiler.ownership`
   `fold_terminal_expr` is the canonical shape and it handles ExprLet by recursing
   into `let_body`, which my hand-walker never looked at. `arm_body_diverges` now
   routes through that fold instead of matching ExprReturn/ExprBlock itself.
   Checked before reaching for it: ownership does not import infer, so this adds
   no cycle.

2. THE MIRROR. Fixed by INSTALLING THE EMITTER'S OWN BYTES from
   target/stage0-regen-candidate rather than hand-shaping a third guess. The drift
   CI reported was one line: `pub use crate::v1_compiler_ownership::fold_terminal_expr;`,
   a re-export the emitter derives from the import structure. My hand-written
   `arm_body_diverges` was byte-identical to the emitted one; the line I could not
   have guessed is the one that made it drift. Two hand-shapes, two misses.

THE THREE-STEP CHAIN, run locally, not just the install:
  --required-regen              first_generation_equal=true planned=149 executed=149
                                adjudicated=149 declared_divergent=1 [main.rs]
  --required-regen-fixed-point  fixed_point_equal=true referenced_first_generation_equal=true
`main.rs` alone is the known declared row, so there is no undeclared divergence.
The fixed-point pass matters here specifically because pass 1 runs a binary built
from the seed it emits, and this change alters the inference the emitter itself
runs on -- the case where one pass can self-verify for the wrong reason.

WITNESSES: 6/6 PASS on the emitter's bytes, on a build verified by hash change
(194ec016) rather than by a `Finished` line.

AND ONE RETRACTION, BECAUSE IT WOULD OTHERWISE STAND AS FALSE COVERAGE. The two
ExprLet witnesses added here DO NOT DISCRIMINATE. I built the pre-fix predicate and
ran them against it: both PASS on the old hand-walker too. `{ let why = 2  return X }`
puts the `return` as the block's LAST CHILD with the `let` as a preceding sibling,
so `children |> last` already reached it. I have no surface shape that produces an
arm whose terminal is an ExprLet node.

So the ExprLet arm is covered because the CANONICAL FOLD owns it, not because a
live red was demonstrated. The review's objection stands on its own without that:
forking traversal is the defect, and routing through the fold is the repair. The
witnesses are kept as behaviour-preservation controls and are labelled as such
rather than as proof of a hole.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* Label the ExprLet witnesses as behaviour-preservation controls, at the witness

The commit before this retracted the discrimination claim in its message. A reader
of the witness file would still have found a comment calling it 'its discriminating
case'. The correction belongs where the evidence is read, not only where it was
made.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* review 5083893018: repair all three blockers, and label what the evidence does NOT establish

B1 -- THE ALL-DIVERGING CASE INVENTED A TYPE, and I had reported it checked. I
verified the empty-list path does not CRASH and reported that as verifying it is
CORRECT. The filter created a state the old code could not reach -- arms nonempty,
non-diverging arms EMPTY -- which fell into `Absent => scrut_rt` and typed the match
as the value it CONSUMES. `arm_body_types` now falls back to the full arm join in
that case; `scrut_rt` survives only for the genuinely zero-arm match.

B2 -- DIVERGENCE NOW GOVERNS BOTH STAGES. I had argued the re-inference pass cannot
re-admit a diverging arm because its body_type is resolved. True of my specimens,
not a structural property, and generic or alias-bearing returns are not covered.
The pass now returns `original` for a diverging arm outright, which makes the
universal claim unnecessary rather than proven.

B3 -- PAIRED ORDERINGS whose arms contribute differently: `Absent` carries no
element type, `Present { value: 5 }` carries Int.

EVIDENCE STATUS, STATED RATHER THAN IMPLIED BY NINE GREENS: 9/9 witnesses PASS,
regen first_generation_equal=true declared_divergent=1 [main.rs], mirror installed
from the regen candidate rather than hand-shaped. That establishes NOT-FAIL for all
three and CORRECT FOR NONE.

Both mutants were built and both left every witness green:
  MUTANT 1  pre-B1 unconditional filter        hash 8c7e053c1bbc  2/2 PASS
  MUTANT 2  keep first non-diverging arm only  hash cd33904dbf9a  2/2 PASS
Each rebuild is confirmed by a changed binary hash, so the controls ran.

So the new controls have the SAME DEFECT the review found in the old one: they
certify without discriminating. Both are labelled as behaviour controls AT THE
WITNESS, with the mutant hashes, so no reader can cite them as proof of a wall.
The repairs stand on the reasoning -- a match must not be typed as the value it
consumes, and a classification that governs one stage should govern both -- not on
evidence I do not have.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* B1: state the unauthorable RED as a 4b row with a capability trigger

Two failed instantiations plus a named structural reason, rather than a third guess.
PositionDeclaredReturn has NO PRODUCER: DeclaredTypePosition declares twelve
positions, DeclaredTypeObligation is constructed at two (PositionDirectCallArgument,
PositionListElement), and PositionDeclaredReturn appears only in the unwired-position
comment, the variant declaration, and a display string. So a terminal-position
match's own type is consulted by nothing, and the fixture was accepted under the
mutant because the seam is unwired -- not because the repair is wrong.

That converts B1 from a hole in the evidence into a located, triggered stall: rung,
ceiling, and a next-rung trigger naming the CAPABILITY (an obligation producer for
PositionDeclaredReturn) rather than an artifact. No fixture in this file can retire
it, and the row says so.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* B1 HAS A DISCRIMINATING RED after all: the wired direct-call argument seam observes it

Retracting the 4b row I filed one commit ago. It said the RED was unauthorable and
named a capability trigger. That was wrong -- not about PositionDeclaredReturn, which
is genuinely unwired, but about the conclusion drawn from it. You do not need the
return seam if you can reach a WIRED one.

`direct_call_argument_inhabitance_diags` builds its obligation with
`produced: resolved_type(n: arg_value(n: ta))` -- the resolved type of the ARGUMENT
EXPRESSION -- and `PositionDirectCallArgument` is one of the two wired positions. So
an all-diverging match in ARGUMENT position has its own computed type compared, where
the same match in TERMINAL position is consulted by nothing.

MEASURED IN BOTH DIRECTIONS, which is what the previous two instantiations could not
do:
  FIXED    binary 01a53030eafa   PASS an_all_diverging_match_in_argument_position_types_as_the_arms
  MUTANT-1 binary 8c7e053c1bbc   resolve REFUSED:
    value does not inhabit its declared type at the direct call argument for parameter
    'r': declared 'Coproduct(ProbeResult)', produced 'Coproduct(ProbeFlag)'
`produced 'Coproduct(ProbeFlag)'` is the review's defect in its own terms: the match
typed as the value it CONSUMES rather than the value it produces.

ONE CONSTRAINT THE FIXTURE HAD TO RESPECT, and it is the defect protecting itself: the
scrutinee must not be Optional. `declared_type_inhabitance` bails to
`InhabitanceUndecidable { UndecidableOptionalCarrier }` when either side carries
CardOptional, which swallows the comparison before it happens. A plain coproduct
scrutinee walks past that bail.

WHAT CHANGES IN THE FILE: the two terminal-position witnesses stay, still labelled as
behaviour controls that do not discriminate. The PositionDeclaredReturn finding stays
as the EXPLANATION for why they cannot -- 2 of 12 positions wired -- but is no longer
a ceiling claim about the class, because a wired position observes the same state.

10/10 witnesses PASS. 4493 file(s) parse-clean. No .dag authority changed, so the
mirror is untouched.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* review 58384: an all-diverging match takes the EXPECTED type, not the arm payloads

CONFIRMED BY EXECUTION, AND THE OBJECTION IS CORRECT. The previous fallback restored
the arms' body types when every arm diverged. Those are RETURN PAYLOAD types, and an
all-diverging match produces no value at all, so they are not the match's type either.
Measured on a scratch probe with a formal the seam actually checks:

  b3.dag:50:26: error: value does not inhabit its declared type at the direct call
  argument for parameter 'r': declared 'Coproduct(B3Res)', produced 'Coproduct(B3Other)'

A FABRICATED REFUSAL against an argument that never returns -- DESIGN 5's sign-flip,
the same defect this PR exists to remove, relocated from the scrutinee to the return
payload. My previous commit's discriminating RED enshrined it.

THE RULE IS NOW CONTEXTUAL, which is one of the two repairs 58384 allows: when every
arm diverges the match takes the EXPECTED type, because a value that is never produced
inhabits whatever the context requires. `scrut_rt` survives only for a match with no
arms at all. Verified: the probe above flips from refused to accepted.

WHY MY FIRST COUNTEREXAMPLE RUN SAID THE OBJECTION WAS FALSE, since that nearly became
a confident wrong rebuttal. I ran the reviewer's shape with an `Int` formal and it was
ACCEPTED, which reads as refuting them. The control says otherwise:
`b3_take_int(x: B3Ok { n: 1 })` -- a plainly wrong argument, no match involved -- is
ALSO accepted, and the function declared `-> Int` then RETURNED a `B3Res` at runtime.
The Int formal is not judged at that seam, so the probe was blind. Re-running with a
coproduct formal, which the earlier ProbeFlag measurement proved is checked, reproduced
the refusal immediately. That Int-formal hole is a separate live silent-wrongness
defect and is NOT this PR's subject; it is reported upward rather than fixed here.

EVIDENCE:
  11/11 witnesses PASS on binary 16a3739a7352, rebuilt and hashed in the same command
    as the run -- an earlier run of this same set reported two refusals off a stale
    mutant binary, so the rebuild is no longer trusted to memory.
  B1's discriminating RED SURVIVES the change: under mutant 8c7e053c1bbc it still
    refuses with declared 'Coproduct(ProbeResult)', produced 'Coproduct(ProbeFlag)'.
  regen first_generation_equal=true declared_divergent=1 [main.rs]
  fixed_point_equal=true
  4493 file(s) parse-clean, scratch probe removed.

THE NEW WITNESS IS THREE-WAY DISTINCT ON PURPOSE: formal ProbeResult, arms return
ProbeOther, scrutinee ProbeFlag. It reds if the match is typed as the scrutinee (the
original defect) OR as the arm payloads (this over-correction), so one witness covers
both directions rather than one.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* review 58406: divergence survives as a nameless type, and the case it names is INHERITED

TWO FACTS, BOTH MEASURED, AND THEY POINT DIFFERENT WAYS. codex 58406 identified a
REAL defect. Its attribution to this diff was WRONG. Both halves matter.

INHERITED, WITH A RECEIPT. origin/main built in its OWN worktree with its OWN target
dir -- binary 3b040239a0e2, and `grep -c arm_body_diverges` on main's mirror = 0,
proving it is a compiler without this PR's predicate. Main refuses the same shape:
  b4.dag:14:32: error: value does not inhabit its declared type at the direct call
  argument for parameter 'r': declared 'Coproduct(B4Res)', produced 'Coproduct(B4Other)'
So an all-diverging match bound by an ordinary non-tail `let`, whose unreachable
binding flows onward, is falsely refused ON MAIN. This PR neither introduces nor
worsens it -- and repairs it rather than declaring a rung drop for a defect that is
one edit away, which is the same rule that ruled out a drop earlier in this lane.

THE REPAIR IS THE FIRST ONE THAT MATCHES THIS PR'S OWN TITLE. The arm-join fallback
and the expected-type fallback were both APPROXIMATIONS of "a diverging arm
contributes nothing to the join" that leak in contexts the sentence covers: the
first fabricated the arms' return payloads, the second only worked where a
contextual type existed, and an ordinary non-tail `let` passes `expected: none`.
`divergent_type()` is a deliberately NAMELESS node: a value that is never produced
has no type to report, so consumers asking its name get "" and DECLINE. Two local
patches was DESIGN 6's forked-logic trap arriving on schedule.

THE SILENCING CONTROL, because "it declines" is one character from the absorbing
fallback DESIGN 5 hard-rejects. A genuine inhabitance violation must still refuse in
the presence of a divergent binding. Two arms, one file, measured on binary
4fcbc484bbb7:
  baseline_violation           -- same violation, NO divergence in the body
  violation_beside_divergence  -- same violation, sharing a body with an all-diverging
                                  match whose nameless-typed binding is consumed first
BOTH REFUSE, each with its own located diagnostic (b5.dag:12:28 and b5.dag:25:28,
`declared 'Coproduct(B5Res)', produced 'Coproduct(B5Other)'`). The baseline refusing
is what makes the second line evidence rather than an assumption. And the line
between them -- the divergent binding's own consumption -- produced NO diagnostic,
which is the correct discrimination: it declines where there is no value to judge and
nowhere else. The line still stops for real errors.

EVIDENCE: 12/12 witnesses PASS; B1's discriminating RED still refuses under mutant
8c7e053c1bbc; regen first_generation_equal=true declared_divergent=1 [main.rs];
fixed_point_equal=true; 4493 file(s) parse-clean; scratch probes and the main
worktree removed.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* review 5085499375 (D1): divergence is an explicit fact, not an absent name

A nameless Resolved node conflated DIVERGES with COULD NOT RESOLVE. The only
feature distinguishing it was the empty name, so every consumer that declines on
a missing name declined on both -- and the second is a state that must still be
judged. That is silencing, and it was structural rather than hypothetical.

InferredNode -- the existing authority for what inference knows about a node --
gains a fourth answer, Divergent, deliberately NOT a shape of Resolved.
TypeResolutionVerdict gains DivergentExpression and type_is_divergent(n) is the
reader consumers match on; is_fully_resolved still answers false for divergence,
but by its own arm rather than by sharing the unresolved path.

divergent_type() moves to 00_core beside InferredNode: resolution as well as
inference must now construct and recognize it, and leaving it in 04_infer would
have forced 04_resolve to mint a second nameless node for the same concept.

Making the fact structural produced a 10-site census, each answered deliberately
rather than defaulted: inferred_to_node none; is_compiler_error false (divergence
is a fact, not a failure); resolve_optional_node carries it (unit_type would
fabricate a type for unreachable code, a diagnostic would refuse a program that
is not wrong); inferred_to_outputs []; two emit_rust wire_contract sites refuse
(a diverging initializer names no alias); serialize_inferred_node_ref keeps the
fact in the serialized form; and cli_run returns a typed error.

Two of the sites rustc caught are .dag-authored and the .dag exhaustiveness
checker missed them: their matches are over Optional<InferredNode> with NESTED
patterns, so accepted source emitted Rust that does not compile. Repaired at the
authority, not in the mirror; the checker gap is filed separately.

Chain: 12/12 witnesses PASS, first_generation_equal=true declared_divergent=1
[main.rs], fixed_point_equal=true, 4493 files parse-clean, fmt clean.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* review 58547: spell combine_resolution_verdicts over all four verdicts

The acc match used a wildcard, so DivergentExpression fell through a catch-all at
the verdict layer in exactly the way it fell through an absent name at the node
layer -- the conflation this change exists to remove. The emitted mirror carried
that wildcard verbatim, which is what the reviewer saw. The next variant added
would have been absorbed silently rather than refusing.

Behaviour is preserved by construction, not by inspection: the inner match is
bound to a let and the three non-refusal arms all return it, so the arms are
identical to the wildcard they replace. The tempting rewrite -- rank the variants
and take the stronger -- reads better and CHANGES one case, acc=UnderResolved with
next=DivergentExpression, from Divergent to UnderResolved. That case is unreachable
today (divergence is a whole-type sentinel, never a container child), so taking it
would have been an unobservable semantic change smuggled in under a style fix.
Left alone deliberately; if the ordering is wrong it deserves its own subject.

Chain: 12/12 witnesses PASS, first_generation_equal=true declared_divergent=1
[main.rs], parse and fmt clean.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* converge the two arm_body_diverges declarations the merge produced, and regenerate

#10045 and this branch independently declared arm_body_diverges in
04_infer.dag. Git merged both cleanly -- different regions, no textual
conflict -- leaving TWO declarations and call sites binding
inconsistently. Nothing textual catches this; the compiler does:

  call shape mismatch calling 'arm_body_diverges':
    no parameter named 'n' (declared: [body])

THE CONVERGENCE WENT AGAINST MINE, ON THE MERITS. My declaration
hand-rolled the block-tail recursion and matched ExprBlock only.
#10045's delegates to ownership.fold_terminal_expr, which folds through
ExprLet AS WELL AS ExprBlock. So an arm shaped `let x = ...; return y`
diverges and my predicate answered false -- the fabricated refusal my own
annotation warns against, in the code that annotation sat above.
Re-inventing a walk the codebase already owned is the DESIGN section 2
failure and here it also cost correctness. Theirs survives; my
declaration is deleted and my call site rewired to it. My rationale
carries a measured receipt (extdeps.uri_path path_segment_tokens) so it
moves onto the surviving declaration rather than being dropped, with a
note recording that two met and which won.

THE MIRRORS ARE REGENERATED, NOT RESOLVED. Four generated stage0 mirrors
conflicted. They are derived, so neither parent's copy is a valid
resolution and both were tried and both failed loudly at the build:
main's v1_std_core.rs has no Divergent, mine has no
declaration_provenance_of (#10006). The regenerated mirror carries BOTH
-- verified on the installed bytes, not inferred from a green build --
which is what no hand-picked side could produce. Regen ran with a
compiler built from pristine main, and the candidate bytes were
transferred by hash (sha256 72cd5275...) rather than trusted.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* correct the arm_body_diverges attribution: the survivor is mine, not #10045's

My previous commit stated the convergence backwards. Checked against the
trees rather than assumed from position in the merged file:

  origin/main            arm_body_diverges(n: Node)      ExprBlock only
  #9964 pre-merge head   arm_body_diverges(body: Node)   folds via fold_terminal_expr

So the ExprBlock-only declaration is main's incumbent from #10045, and the
fold_terminal_expr one is this branch's. The OUTCOME is unchanged and still
correct -- the fold_terminal_expr declaration survives because it handles
ExprLet, which the other does not -- but I described it as "theirs survives,
mine is deleted" when it is the reverse.

The error was attribution by position: I read the declaration at the lower
line number in the merged file as the incumbent and never asked which tree
each came from. One `git show <ref>:<file>` on each side settles it, and I
skipped it because the merged file alone looked sufficient.

Consequence worth stating rather than burying: this branch now DELETES a
function main has carried since #10045 and re-points its call site at this
one. That is deliberate -- two spellings of one predicate is the DESIGN
section 3 violation -- but it is a substantive change to code this branch
did not author, so it belongs in the annotation and not only in a commit
message.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

* cite the blast-radius census beside the section 3 argument for the deletion

tidy-lynx-804 checked independently that the deleted arm_body_diverges had
exactly one declaration, one recursive self-call and one caller on
origin/main, plus its generated mirror. That census is what makes the
deletion landable; the section 3 "two spellings of one predicate" argument
only makes it defensible, and those are different claims.

It goes in the annotation rather than in this message because a commit
message is flattened by squash-merge and the next reader will be in the
source. Per DESIGN section 4c this is annotation-channel text: it cannot
alter any semantic occurrence, resolution result, or target-program byte,
so no mirror regeneration follows from it -- and CI's regen fixed-point
check is the thing that verifies that claim rather than my assertion of it.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant