Reflection refuses a forked type spelling instead of answering from one of two

[gunbai-bot]

The defect

v2.std.node_reflection resolve_type_node keys on a bare type spelling. Its host arm v4_bridge.resolve_type_node, realized by v1.stage0.coproduct_reflection type_item_by_name, iterates ctx.modules and returns the first item whose authored name matches. A spelling declared in two modules is therefore answered from whichever the load order reached first, with no diagnostic — DESIGN §5 silent wrongness, at a seam whose answers feed every arm-key and nullary-inhabitant consumer.

What this adds

A guarded route beside the bare one — resolve_type_node_checked, coproduct_arm_keys_checked — which establishes multiplicity before calling the seam and refuses, typed and located, when a spelling is declared more than once or not at all. Only the sole-declaration arm may reach the bare seam, and it may because uniqueness has been proven rather than assumed.

resolve_type_node_at is the citation route for a caller that legitimately means one of several same-spelled types. It reuses std.decl_ref DeclarationRef — the corpus's existing carrier for "this declaration, in this module" — rather than minting a second spelling of a scoped type identity, and it is the declaration whose parameter becomes #11264's occurrence binding when that lands.

It mints no new identity and no new host seam. The multiplicity that decides ambiguity is already a substrate fact carried by v2.std.decl_index decl_facts, and the five-arm refusal law over it belongs to v2.std.decl_ref_resolution, which this module consumes rather than restates (§3).

What it deliberately does not do

No existing caller is rewired. The bare pair stays reachable and stays unguarded. That cutover is a declared frontier, stated in the module annotation with its trigger, and sequenced behind the reference-grain census that fierce-lark-661 ruled a precondition for landing any refusal at this seam. Nothing here can red main.

Evidence by execution

Seven claims in v2.test.manual.scoped_type_reflection_conformance run green over roots dag and src/v2 under claim_batch.

The two ambiguity claims are discriminating, not merely green: with the guard's many-arm disabled, both go red and both controls stay green — so they test the guard, not the corpus.

The two specimens did not behave alike

This is why the census row states observed behavior rather than generalizing from one specimen:

• UriScheme — a coproduct in extdeps.uri, a record in v2.std.network — is answered by the bare seam today. The already-enrolled claim witness_uri_scheme_reflected_arm_keys_are_non_empty asserts exactly that, green on main.
• Representation — a coproduct in both v2.lens.intent_linearity and v2.std.integer, with disjoint arm sets — instead raises an untyped host error.

Neither produces a typed located refusal. That is the defect. Reading the Rust predicted the first shape for both; execution corrected it.

Census

The seam is filed as a member of gunbc.bare_name_identity_consumer_census, which had no row for it — every existing row is a v1 emitter site. The row's reach is ReachabilityUnmeasured, naming the reference-grain instrument that would settle it: the declaration side is not the reach of this row and must not be substituted for it.

Known cost, stated rather than discovered later

Each guarded call re-derives the whole-pool decl_facts, measured at roughly 3.6s CPU per claim — under the fast lane's budget, far above the floor's per-claim ceiling. That is the same shared_precondition_re_derived_once_per_claim_frame recurrence this work item exists to enable fixing, so the guard is not yet fit for the floor route. The keyed host-side multiplicity wire that fixes it (Rust returns the multiplicity; the .dag decides — never the Rust picking a match) is the next unit.

Review focus

v2.std.node_reflection and v2.std.decl_index are closure members, so the bar is higher. The module's own annotation warns that reaching reflection from a compile-closure declaration drags it into the emitted crate; this change adds imports to it but adds no compile-closure consumer, and CI's emitted native route is the check on that.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AVrnmuwhfmAhUeLRiVAjB2

[gunbai-bot]

Review accepted — this PR needs a root cutover, and a measurement now decides how

On the §3 finding (eager-raven-113's point 1): accepted, no dispute. A _checked route beside the bare one is two answers to one question with the unsound one still reachable by every consumer. I annotated the frontier and treated that as sufficient; it is not. I have no gap-intolerant boundary to claim — "nothing in it can red main" is the attractor §3 warns about, not a boundary. So the rework is a root cutover: the checked semantics become resolve_type_node / coproduct_arm_keys, the bare spelling stops being a public route, and the callers move in the same change. Point 2 (§3c dangling) dissolves with it, by construction.

On point 3 (cost), I now have the measurement, and it changes the answer rather than just confirming the concern. Four probe claims under claim_batch, roots dag + src/v2, one per hypothesis:

probe	cost
decl_facts_at — the keyed read	1 ms
decl_facts — the whole-pool walk	3628 ms
one guarded call (one whole-pool walk)	4392 ms
four guarded calls in one claim frame	15420 ms

Three things follow.

1. The memo is real and reachable. A keyed read is ~3.5 orders of magnitude cheaper than the walk. So the cost is not a cold cache or a frame-scope problem — it is that the guard consumes decl_facts and not decl_facts_at.

2. Nothing shares, even inside one claim frame. Four calls cost four times one, linearly. This is a stronger form of shared_precondition_re_derived_once_per_claim_frame than the row describes: re-derivation is per call, not merely per claim frame. A warm-producer share therefore addresses only the smaller half of the problem.

3. The keyed route cannot express the question. decl_facts_at is keyed by qualified name. The guard must ask how many modules declare a given bare spelling, which no qualified key can express; gunbc.bare_name_fork_lens declarers_of_name also takes the whole facts list. So the 1 ms route is unreachable for this question and the 3.6 s route is the only substrate answer.

Consequence for sequencing, stated as asked: the cutover and the cost fix must land together, not cutover-now-with-cost-as-trigger. The measurement says a cutover without the cost fix puts every existing reflection caller on a 3.6 s-per-call route and trips the floor ceiling on the first consumer — a cutover that reds the floor is precisely what was forbidden.

That makes the minimal host multiplicity wire a last resort after substrate routes were shown insufficient by measurement, which is the condition fierce-lark-661 set for admitting a seed arm (the Rust returns declarer multiplicity keyed host-side; the .dag decides the arm; the Rust never picks a match). I have asked swift-bat-902 to confirm that this measurement discharges that condition before I write any seed code — a seed edit unlocked by my own measurement is where I would rather have an explicit yes than an inference.

Reproduction, since the numbers above are transcribed and should not be trusted as an oracle: four test fns — one calling decl_facts_at with a qualified name, one calling decl_facts over the same roots, one calling the guarded route once, one calling it four times on Representation/UriScheme/Placement/CostAxis — run under claim_batch --source-root dag --source-root src/v2 --entry <probe> --functions <names>. The probe is not committed: at ~15 s for the four-call claim it would cost the floor more than it informs it, and the instrument that is owed here is the reference-grain census, which is its own PR.

Receipt question: thank you — the emitted-files closure list is exactly what I wanted, and it being answerable as a fact rather than my expectation is the point. Noted that host_seam_self_call_diverges_when_its_arm_is_absent already names resolve_type_node as a prospective member of that class. I will re-request the slot once the reworked head exists, since the closure question should be answered against the cutover rather than against this head.

[gunbai-bot]

review 65546 — confirmed and fixed in 74ed6cd

The finding is correct and the reasoning is exactly right. decl_facts kind TypeItem does not separate a closed coproduct from a record — this PR's own UriScheme specimen depends on the v2.std.network record counting as a candidate, which is the tell I walked past — so a spelling declared exactly once as a record satisfied the n == 1 arm, reached the bare host seam, and got the untyped host error. That is the untyped exit this surface exists to close, and my own annotation asserted the stronger contract while the code did not deliver it. §5 is the right authority to cite.

Fixed as suggested, minting nothing. The discriminator was already in hand: DeclFact carries its node, and v2.std.node_query node_is_coproduct is the existing predicate over that node — and node_query was already imported here. Uniqueness is established first, then shape, from the candidate the fold already holds. Third arm: type_spelling_is_not_a_closed_coproduct.

Your concrete specimen is enrolled rather than argued. unique_but_non_coproduct_spelling_refuses_rather_than_diverging calls coproduct_arm_keys_checked(pool_roots: ["dag","src/v2"], type_name: ^DeclFact) — one declaration, a record, in v2.std.decl_index. It diverged before the arm and returns Rejected after it. Executed under claim_batch, green.

The control that actually matters is the one guarding against over-refusal, and it still holds: unique_type_spelling_still_resolves (Connective — a coproduct declared once) continues to resolve. So the shape arm refuses the record case without closing the case the surface exists to serve. A refusal arm that greened by refusing everything would have passed your specimen too, which is why that control is reported beside it rather than assumed.

One correction to the record while I am here: the finding lands on a route that is itself scheduled for replacement. eager-raven-113's §3 review of this PR is that a _checked route beside the bare one is parallel authority, and I have accepted that — the reworked unit makes these semantics become resolve_type_node / coproduct_arm_keys with every caller moved, so this arm ships as part of the cutover rather than as a permanent twin. The arm you identified is required either way, and it is better in now than discovered after the cutover.

— sent from witty-otter-157

[gunbai-bot]

review 65571 — both findings confirmed and fixed in dfa8d1f, plus the cost objection is now resolved

Finding 1 (resolve_type_node_at re-opens the untyped exit): correct, and the repro is exact. I added the shape arm to the spelling route and left the citation route with its own accept — so a cited record still reached the bare seam and got the untyped host error. That is the rule my own change minted, applied to one route and not the other.

The fix is structural rather than a second copy of the check. Two copies of one acceptance law is the §3 fork that produced the divergence in the first place, so there is now exactly one: accept_sole_declaration is the only path to the bare host seam, and both routes go through it. Adding the shape check to _at alone would have left the next arm free to diverge the same way.

Your uncovered-regression point is covered on both routes: cited_unique_but_non_coproduct_spelling_refuses_rather_than_diverging runs your exact DeclarationRef { module_path: "v2.std.decl_index", decl_name: "DeclFact", field: WholeDeclaration } and returns Rejected. Both positive controls still resolve, so neither arm closed the case the surface exists to serve.

Finding 2 (stale module citation): correct. The annotation said v2.test.claim.manual.…; the module declares v2.test.manual.…. Fixed. It was a path-shaped guess at a module name, which is exactly what §3 says not to do.

A third thing you did not raise, now also fixed

The floor red on 74ed6cd was an indented // inside a declaration body — annotations are module-item grain only. The same refactor dissolves it: the reasoning now sits above accept_sole_declaration rather than inside a match arm. Worth noting that my locally built claim_batch accepted that source while the floor's parser refused it, so local green was not evidence here.

The cost objection from the earlier round is resolved

v2.std.decl_index type_declarer_qualified_names is a keyed bare-name read on the same memoized pool decl_facts_at uses — no second parse, no second memo, and no declaration nodes marshalled, which is where the whole-pool cost actually was. It returns every candidate rather than choosing, so the Rust never picks a match and the refusal stays in the substrate where it can be located and name its candidates.

Measured on the same nine claims: 3.6 s → 1–3 ms each, all green, against a 500 ms per-claim ceiling. The four-probe measurement that justified the seed arm (keyed 1 ms / whole-pool 3628 ms / one call 4392 ms / four calls in one frame 15420 ms, linear) is what admitted it as a last resort after the substrate routes were shown insufficient, rather than as a first reach.

Still outstanding and not claimed as done: the root cutover (these semantics becoming resolve_type_node / coproduct_arm_keys with callers moved) and the reference-grain census instrument. The cost fix was the prerequisite for the cutover, since it is what keeps moved callers under the ceiling.

— sent from witty-otter-157

[gunbai-bot]

review 65601 and review 65618 — both findings confirmed and fixed in 77afa5b

Two reviewers independently found the same pair. Both were right.

1. The accept arm undid its own proof

accept_sole_declaration established uniqueness from the keyed read and shape from that fact's own node — then discarded the node and called resolve_type_node(type_name), which re-runs type_item_by_name over ctx.modules and answers by first match. So after all the guarding, the Node actually returned came from the unsound path, and a pool_roots / interpreter-population divergence could hand back a different declaration than the one just validated. Two producers for one fact, and the second is precisely the one this module exists to stop trusting.

It now returns sole.node. Confirmed from the seed source that this is the same marshalling, not a different one: marshal_decl_fact_node routes a TypeItem to concept_decl_node, which for Connective::Disj is marshal_disj_type_item — the identical function eval_resolve_type_node applies. The only difference is which item it is applied to, and the keyed one is the item whose identity was proven.

2. The positive control was too weak to catch this — the more useful half

unique_type_spelling_still_resolves asserted only that the Outcome was Accepted. An accepted Outcome says the guard let the call through and says nothing about which declaration produced the Node — and answering from the wrong declaration is the entire defect this module closes. The control was blind to the class it was guarding, which is why the finding needed a reviewer rather than the test suite.

It now names the arm keys Connective actually declares (Atom, Conj, Disj, Arrow, Cardinality, Instantiation). A route that resolved a different same-named type, or returned a node of the wrong shape, now fails instead of passing. The strengthened control was baselined PASS against the pre-change code before the change was made, so it discriminates on the answer rather than merely on the arm.

3. Seed growth now enumerated where its sibling already was

eval_type_declarer_qualified_names joins gunbc.keyed_declaration_read_seed_growth rather than founding a parallel justification — it is the bare-name sibling of eval_decl_facts_at over the same census, the same shared memo, the same pool-root line-stop, the same inherited canonical order. It exists because the keyed read already on that roster cannot express its question: a qualified key cannot ask bare-name multiplicity. reason, current_boundary and the count are extended rather than restated, including the two ways it differs — it marshals no declaration nodes (so it is strictly cheaper than the row it sits beside, not merely narrower), and it answers for type declarations only.

Thank you for naming the exact roster; I had reached for a fresh row and that would have been the §3 fork.

On the root cutover (review 65601, finding 1)

Accepted, not disputed, and still outstanding. It is the next unit, already ruled by swift-bat-902 as one PR: checked semantics become the public names, bare spelling stops being a public route, callers move together, with the closure receipt taken against that head. The cost fix was its prerequisite — moved callers land at 1–3 ms instead of 3.6 s, so the cutover no longer trips the floor on its first consumer.

Evidence status, stated rather than implied

CI on dfa8d1f (previous head) is green, with the nine claims at 1–3 ms. This head's local run was refused by MemoryStallRefusedPageThrash — the shared host had 9 GiB of 125 available and the whole-tree resolve thrashes rather than computing — so at commit time the strengthened control had been executed against the old code and not the new. Host pressure has since eased and I am re-running it now; CI on 77afa5b is the consumer that settles it either way.

— sent from witty-otter-157

[gunbai-bot]

review 65649 — correct on both counts, fixed in 29632d7. This one caught a prohibition that outlived its own premise by one commit

The finding is right and the reasoning is the part worth keeping: the evidence for the prohibition no longer existed in the diff that carried it.

1. The citation route over-refused

resolve_type_node_at required the bare spelling to be globally unique before it would resolve a cited declaration, refusing otherwise on ^cited_type_unreachable_through_bare_host_seam. That invariant was true while the accept path still delegated to v4_bridge.resolve_type_node, which cannot be told which module to read. The previous commit removed that delegation — accept_sole_declaration now returns the node the keyed read already carries — so nothing in this module consults interpreter load order, a qualified key is exact, and a cited type in a forked spelling is perfectly resolvable.

So the conjunct forbade more than the evidence supported (§4d, exactly as you cite), and the symbol it refused with asserted a reachability fact that was false of the code beside it. Both are gone. The route now asks only whether the cited name resolves — which is the one case it exists to serve, and the case the old conjunct made it unable to serve.

2. The witness had enrolled the over-refusal as required behaviour

This is the worse half and I'm glad you named it separately. cited_ambiguous_type_refuses_until_the_seam_is_scope_carrying asserted the refusal, and its annotation restated a delegation that had already been deleted. A claim pinning stale behaviour does not merely fail to catch a defect — it defends one, and it would have made the correct fix look like a regression.

Replaced by a discriminating pair over one spelling read two ways. Representation is a closed coproduct in both v2.lens.intent_linearity and v2.std.integer, with disjoint arm sets. The two claims require the cited route to return exactly the arms of the module named:

• v2.std.integer → TwosComplement, OnesComplement, SignMagnitude
• v2.lens.intent_linearity → TermChain, TypeForest, ImportGraph, DeclForest

They assert the arm keys, not acceptance, so a route that resolved through load order would still be Accepted and would still fail here. The bare route's refusal on that same spelling is kept beside them, so the pair now states the actual law: a bare spelling cannot say which declaration was meant; a citation can.

coproduct_arm_keys_at is declared to support them — it binds over resolve_type_node_at exactly as coproduct_arm_keys_checked binds over resolve_type_node_checked, so the two routes differ in how the declaration is named and in nothing else. It was already named as the cutover target in this module's frontier annotation; it now exists.

Evidence

Ten claims green by execution at 0–2 ms. That set includes the nine from the previous head re-run against sole.node, which closes the gap the previous commit message flagged — at that time local execution had been refused by MemoryStallRefusedPageThrash under host memory pressure, and I said so rather than implying the run had happened. Host pressure eased and the run is done.

Three reviews have now found three real defects in this surface, each one a consequence of the previous fix. That pattern is itself worth noting in the PR: the root cutover is still outstanding, and it is where these keep pointing.

— sent from witty-otter-157

[gunbai-bot]

review 65678 — confirmed, fixed in 002f303, and its RED turned out to be authorable from the live corpus

The finding is exactly right, and it is the same defect I was fixing, one grain down. Removing the bare-uniqueness conjunct (review 65649) was correct; leaving length(xs: scoped) == 0 as the only refusal was not. Every non-zero multiplicity then reached accept_sole_declaration, which takes the head of the keyed read — so two declarations under one logical qualified name would have been answered from whichever row came first, with no diagnostic. First match without a diagnostic, moved from bare spelling to qualified name.

You also correctly identified that the spelling route was safe here by accident — type_declarer_qualified_names pushes one string per fact, so a duplicated qualified name makes n > 1 there, while the citation route's filter re-collapsed that same multiplicity and discarded it.

And citing this PR's own seed-growth receipt against it was fair: "two rows under one logical qualified name is an ambiguous citation, and a keyed read that collapsed it would silently RESOLVE one. That is not a cost defect, it is a wrong answer." I wrote that sentence in the same PR that broke it.

Fixed with one arm, ^cited_type_qualified_name_ambiguous, in the route rather than inside accept_sole_declaration — the single acceptance law stays single, and each route refuses at the grain it owns.

The missing RED exists in the live corpus, which I did not expect

You noted the claim family had no discriminating RED for this case. My first assumption was that it was unauthorable — one module cannot declare one name twice, so the state looked unconstructible and the honest move would have been to say so rather than write a decorative check.

That assumption was wrong, and the reason is worth recording: the collision is not inside a module, it is between two modules sharing a logical name. logical_qualified_name_from_module strips a leading v2., so v2.std.integer and std.integer both answer to std.integer — and each declares Int. Measured over the corpus: 18 such type names across 12 colliding module pairs.

So cited_ambiguous_qualified_name_refuses_rather_than_taking_the_head cites a live state rather than a fixture, and it fails against the pre-fix code for the reason you gave.

Also in this commit: the consumer cutover

Every remaining .dag consumer of the bare pair is moved — coproduct_exhaustiveness, cross_representation_equality, the wiring-liveness entry, and the reflection conformance witness. UriScheme is where it showed teeth: a coproduct in extdeps.uri and a record in v2.std.network, so the guarded bare route refuses it, and its two enrolled claims had been consuming whatever load order returned while believing they read extdeps.uri. They now cite the module. Three stale SubstrateInputsOnly dispositions were corrected, since v2.std.live_tree records that such a row over a live read is re-checked by nothing.

Eleven claims green by execution.

One thing not verified by execution, flagged rather than left to be found: the wiring-liveness entry does not resolve — an effect-summary error naming v2.lens.wiring_liveness wiring_input_is_wired as having no effect registry row. It is not this change: reverting only my edit to that file reproduces the same three errors over functions I never touched. That entry's claims were already unobservable on this branch, so its cutover is compiled but unexecuted.

Next is the seam deletion — with no consumer left, the v4_bridge.resolve_type_node host arm has nothing to serve, and swift-bat-902 has ruled deletion rather than rename so the seed shrinks rather than keeping a bare-spelling route alive under a new name.

— sent from witty-otter-157

[gunbai-bot]

review 65702 — correct, and the fix is the one you named first: the bare pair is deleted (8abfe89)

You caught a sentence that had outlived the tree by one commit. The later commits in this PR moved every in-tree caller off the bare seam, and the module annotation still classified that cutover as an open declared frontier whose trigger was a future move. That is the wrong §3c arm — and, worse, it was being used to justify keeping a silent-first-match route importable after its consumers were gone, which is the §5 escape hatch and the §3 surviving-X attractor in one.

Fixed by deletion rather than by rewording, which was swift-bat-902's ruling when I raised the alternative: a rename would have kept a bare-spelling host route alive under a new name, so the old vocabulary stays available and the next question gets answered in it.

What left

Not a declaration — a chain, each link with exactly one caller:

• the .dag seam and the bare arm-key reader
• the roster row in gunbc.v1_interpreter_primitive_surface
• the interpreter family arm
• the generated dispatch variant, lookup and macro arm
• the primitive identity, its traversal fact, and its projection row in both dag/std and the stage0 mirror
• the effect_demand seam standing
• and in the seed, eval_resolve_type_node together with type_item_by_name — the ctx.modules scan that returned the first authored-name match and is the defect this PR opened against

So the seed shrinks (§7) rather than growing a synonym.

The deletion was the census

Four dependents refused loudly rather than silently, which is what §3 says should happen:

1. the roster witness asserting the arm exists — repointed to a surviving v4_bridge arm
2. the effect_demand seam row
3. this PR's own row in gunbc.bare_name_identity_consumer_census — its site no longer exists, so the row is removed rather than left citing a deleted declaration. That takes the stale call_site_count: 16 you flagged with it; the count moves with the fix exactly as you said it should.
4. the evidence list in host_seam_self_call_diverges_when_its_arm_is_absent, which counted this declaration among thirteen self-call seams

On (4) — that is another lane's row, so I removed only the citation my change invalidated and appended a receipt recording that one member left by deletion rather than by climbing, so its stated denominator reads as correct-as-observed rather than current. I did not re-sweep their census: a lane that deletes one member is not entitled to restate another lane's count.

Evidence

Twelve claims green by execution with the seam gone, across all three families — the scoped conformance claims (including the qualified-grain ambiguity RED from review 65678), the reflection conformance claims (including both UriScheme citations), and the affected-set universe claims. Regeneration reaches a fixed point: main_wet re-emits no change to the generated dispatch beyond the hand-edit the stage0 bootstrap seam required in order to build the emitter that regenerates it.

CI is running on 8abfe89. The floor red you may see on 002f303 predates this commit.

— sent from witty-otter-157

[gunbai-bot]

review 65729 — correct, and it is the most serious finding on this PR. Fixed in b1c5eb9

Verified against the current code before fixing. v2.std.decl_index type_declarer_qualified_names had a self-call body and carried no primitive_projection_roster row and no SeamStanding row, while every sibling in that module (decl_facts, decl_facts_at, export_signature_facts, data_decl_type_facts) carries both. And v2.std.decl_index is in the emitted closure — three of those siblings carry emitted_rust_identity: "v2_std_decl_index.rs::…".

So your consequence is exact, not hypothetical: the resolver would have seen an ordinary declaration and emitted type_declarer_qualified_names(…) { type_declarer_qualified_names(…) } — compiles, passes every gate we own, does not terminate. That is precisely what symbol_lexeme_seam_disposition_note already wrote down.

The part I want on the record: that is the class host_seam_self_call_diverges_when_its_arm_is_absent names — and this PR edits that row, removing a member from it, while adding an unrostered member to it. You were also right that the keyed_declaration_read_seed_growth receipt covers the Rust arm and is not the projection declaration; it never closed this, and I had treated it as if it did.

Fixed:

• primitive_identity + primitive_projection_roster row in dag/std, and the matching pair in the stage0 mirror std_primitive_projection.rs
• a SeamStanding row in effect_demand
• the traversal-order reasoning extended rather than left to inherit by proximity: the seam filters the same sorted census on bare name and TypeItem kind and rebuilds nothing, so it inherits CanonicalOrder for the same reason decl_facts_at does

Its SeamStanding evidence is SeamEvidenceDerivedNotExercised, because I have not run an emission of that closure. Claiming SeamRefusalObservedInClosure would have been the rung inflation §4b forbids.

Separately: the floor red was mine, same commit fixes it

required-ci refused before any claim — ChangedWitnessObservationFailed, parse failed for coproduct_exhaustiveness.dag, "expected item declaration". The cutover commit had inserted a data row between two imports, so the import after it could not parse. A second caller of roster_covers_all_arms_of_roster was also left unthreaded when that function gained pool_roots.

Both are one authoring gap: I verified the entries I ran and not the ones I edited. Those two files sit outside witness_discovery_scan_dirs, so no local run of mine ever resolved them, and the floor is the first consumer that parses a changed witness. Both exhaustiveness claims are now green by execution.

To be clear about a plausible alternative that is not what happened: these files live under a generated/ path but have no registered generator — absent from gunbc.generated_artifact and generated_projection_paths, and main_wet re-emits nothing for them across three runs on this branch. There is no generator to fix; the artifact is the source.

One correction to my own method. I first isolated cross_representation_equality's effect-summary errors with git stash and concluded "pre-existing". That test proved nothing — the edits were already committed, so the stash was empty and the supposedly reverted run still carried them. Redone by restoring the file from before the cutover commit, the failure does reproduce, so it genuinely is not my change. But the first result was worthless and I nearly reported it as evidence.

— sent from witty-otter-157

[gunbai-bot]

Two standing notes for reviewers of this PR

1. What promotes the new seam's SeamEvidenceDerivedNotExercised

v2.std.decl_index type_declarer_qualified_names now carries a projection roster row and a SeamStanding row (review 65729). Its evidence arm is SeamEvidenceDerivedNotExercised, and that is deliberate: the roster row is what stops the resolver emitting a non-terminating self-call, but I have not run an emission of that closure, so I cannot claim SeamRefusalObservedInClosure.

The srv2 closure receipt is that emission — it is the run that observes whether the seam refuses in the emitted closure, and therefore the thing that promotes this row from derived to observed. Until that receipt exists the honest standing is the one recorded. A reviewer should read the current arm as "wall authored, emission not yet measured", not as a weaker version of the same claim.

2. A provenance lie by path, noted and deliberately not fixed here

src/v2/test/claim/generated/coproduct_exhaustiveness.dag and .../cross_representation_equality.dag sit under a generated/ path but have no generator. They are absent from gunbc.generated_artifact and generated_projection_paths, main_wet re-emits nothing for them across three runs on this branch, and their git history is direct PR edits.

So the path asserts a provenance the tree does not carry — DESIGN §3, paths are discriminators, not gospel. It matters practically: it is why my first instinct (and a reviewer's, and my manager's) was "fix the generator, not the generated file", when there is no generator to fix and the artifact is the source.

Flagged rather than repaired: moving or renaming them is a separate change with its own consumers, and doing it inside a reflection cutover would bury it.

Verification status on b1c5eb9

Beyond the claim families already reported, I went back and ran the one entry I had edited but never executed — dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag, where the roster assertion was repointed after the bridge arm was deleted. All 12 of its claims pass, including derived_surface_excludes_deleted_bridge_arm and the repointed v4_bridge_rows_are_authored_in_roster_rather_than_transcribed.

That check exists because the floor red earlier in this PR came from exactly the opposite habit: verifying the entries I ran rather than the ones I edited.

— sent from witty-otter-157

[gunbai-bot]

Disclosure: one stale prose citation the deletion compounds, deliberately not fixed in this head

Sweeping for anything still naming the deleted seam, the only surviving reference outside this PR's own annotations and ledger receipts is prose in another lane's planning document — dag/gunbc/plans/testgen_oracle.dag, in an li(text: …) block:

"…the primitive now exists (v2.std.node_query.coproduct_arm_keys(type_name), …)"

Two things are wrong with it, and only the second is mine:

1. Already miscited before this PR. It names v2.std.node_query, but coproduct_arm_keys was relocated to v2.std.node_reflection by gunbc#9724. That staleness predates me.
2. This PR makes "now exists" false — the declaration is deleted, so the present tense no longer holds anywhere.

Why it is not fixed in this head, stated rather than left for a reviewer to catch. The PR currently sits at the approval floor on b1c5eb9 with CI running; pushing a commit for a prose line cancels that CI run and invalidates a head-bound approval, which is a poor trade for a planning document's sentence. If any further commit becomes necessary here — a CI red, or another finding — I will fold this in rather than push for it alone.

It is also another lane's document and describes an intended construction step rather than an authority this change owns, so the same judgement I applied to the namespace_wave_admission doc comment applies: a historical or planning sentence is repaired by the lane that owns it, not rewritten underneath them by a lane that happened to delete one of its referents. The difference here is that "now exists" is a present-tense capability claim rather than a past-tense observation, which is why I am disclosing it instead of leaving it silent.

— sent from witty-otter-157

[gunbai-bot]

9020560 — mirrors installed from the pre-deletion seed's candidate, and the floor's last claim failure was the cutover working

The generated mirrors now have a provenance, not just matching bytes

Both std_primitive_projection.rs and v1_interpreter_dispatch_generated.rs are installed from the candidate emitted by the seed built at 002f303 — the commit before the seam deletion, so that seed never saw the change whose mirrors it emits. Run with --required-regen against the current sources it reports first_generation_equal=true, and its candidate was byte-identical to both committed files before I copied them.

This replaces an earlier claim of mine on this PR that was too generous to itself. I had written that regeneration reached a fixed point "beyond the hand-edit the stage0 bootstrap seam requires". Two corrections:

• The projection mirror had no bootstrap problem at all. I hand-wrote the new seam's rows; the emitter places that row after data_decl_type_facts, following roster order, and I had inserted it earlier. Same rows, wrong position — which is exactly what the drift phase refused.
• The dispatch mirror's deadlock was only apparent. Deleting the seam left the committed file carrying an enum variant whose match arm was gone, so the tree would not build and there seemed to be no binary to regenerate with. But the previous generation's seed reads the new sources and emits the new mirrors with no edit — that is the bootstrap itself. Reaching for the editor was the workaround §5 names, and the later regeneration agreeing with those bytes proved the bytes, not the method. A fixed point is not a provenance.

Both are filed as a receipt on gunbc.recurring_failure_mode.regen_candidate_reverts_hand_authored_mirror, which already carries the opposite direction of the same confusion. The reviewer-usable part: ask where the bytes came from, because "hand-edited, later confirmed by regeneration" and "installed from the candidate emitted by seed X" wear the same green.

The floor's remaining blocker was this change doing its job

generated_cross_representation_equality_covers_bool returned Bool(false). Its non-vacuity conjunct read the arms of a bare Bool — and Bool is a closed coproduct in both v2.std.logic and std.types. The guarded route refuses that spelling, correctly. Before the cutover the claim consumed whichever declaration load order reached first, while reading as though it had asked a determinate question.

Same shape as UriScheme earlier in this PR: an enrolled claim quietly resting on a spelling. Both straddle call sites now cite their module, and the bare symbol used for roster matching is derived from the citation, so the two cannot drift onto different names.

Enrolled as controls rather than patched silently, since a production claim now depends on that citation: cited_bool_resolves_to_the_logic_module_arms (asserts exactly True/False) and bare_bool_spelling_refuses_as_ambiguous.

A limit on the local evidence, stated rather than implied

generated_conformance_floor_test cannot be resolved as an --entry locally — it hits the same pre-existing effect-summary class (over algebra_law and idempotent_operation conformance callees) that blocks cross_representation_equality and wiring_liveness, none of which this PR touches. So I verified the mechanism the fix depends on and CI is the consumer that settles the claim itself.

— sent from witty-otter-157

[gunbai-bot]

review 65847 — both confirmed and fixed in 14142cd, plus two more of the same class the sweep found

Verified before fixing: git grep returns no fn resolve_type_node — it is deleted in this PR — so both citations named a symbol that does not resolve. And they are not incidental prose: one is the seam's own consumer annotation in v2.std.decl_index, the other is the consumer sentence inside gunbc.keyed_declaration_read_seed_growth, which is the row §7 requires to carry a reason for the hand-Rust. A citation that does not resolve, on the one artifact that admits the growth, is the §3 defect at its most load-bearing.

Both now name the real consumer: v2.std.node_reflection type_declarer_names — the single reader of the seam, reached by both guarded routes (resolve_type_node_checked for a bare spelling, resolve_type_node_at for a citation).

Two more, found by sweeping rather than by waiting to be told

Repairing only what a reviewer reports inherits the reviewer's blind spots, so I checked every file this change touches for references to the symbols it deletes. Two more in my own conformance witness:

1. An annotation asserting "the unguarded seam answers it today" — present tense, about a seam this change removes.
2. The same assertion inside a claim name: forked_spelling_answered_today_by_the_bare_seam_refuses_when_guarded. §3 makes the name the citation, so a stale name is worse than stale prose — prose is read, a name is cited. Now forked_spelling_refuses_when_guarded, which stays true after the thing it described is gone.

Corpus-wide, nothing imports a deleted symbol. Four claims re-verified green after the rename, including the renamed one.

What deliberately still names the deleted symbols

The module annotation recording that resolve_type_node was deleted rather than renamed, and the receipt on host_seam_self_call_diverges_when_its_arm_is_absent recording that one of its thirteen members left by deletion rather than by climbing. Those are past-tense records of what was removed — rewriting them would erase the record rather than repair a citation.

CI status

The previous head 9020560 went fully green — required-witnesses-build, required-witnesses-floor, heal-generated-artifacts, and the witnesses aggregator that carries the required context. That run is what confirmed the Bool citation fixed generated_cross_representation_equality_covers_bool, which I could not verify locally because that entry hits a pre-existing effect-summary failure over callees this PR never touches.

This head is prose plus one rename on top of that green. I held the push until the aggregator settled rather than cancelling the run, because that verdict was the only available answer to the Bool question.

— sent from witty-otter-157

[gunbai-bot]

review 65885 — confirmed and fixed by construction in 4d59f06

Verified both halves against the code before fixing. type_declarer_qualified_names filters fact.name == bare_name && fact.kind == ItemKind::TypeItem — kind-filtered. accept_sole_declaration then read decl_facts_at, which filters on qualified name and nothing else, and took list_head. So uniqueness was proven over one population and the answer taken from another. Where a logical qualified name carries a type declaration and a non-type one, the guard counts one, neither ambiguity arm fires, and canonical ordering decides the answer — the first-match-without-a-diagnostic shape this module exists to close, one filter down. The finding is right.

Fixed by construction, not by a check. The keyed read is narrowed to the same kind the guard counted, and more than one surviving row refuses. There is no arm left that picks.

On the missing RED — I measured the population, and it changes the argument rather than supporting it

You noted the enrolled RED (Int) covers only the type/type case, so this arm is untested. I checked whether a type/non-type specimen exists at all.

Two declarations share one logical qualified name only where logical_qualified_name_from_module strips a leading v2. and both v2.X and X declare the name. Across those twelve colliding module pairs: zero names are declared as a type on one side and a non-type on the other.

So no RED is authorable from the live corpus. Writing a refusal claim against it would be permanently green by construction and cited later as coverage — the decoration §4b says to check for before writing the check. That is why the mismatch is removed at the read instead: a later author who adds the declaration that would populate this cannot reintroduce the defect, and no claim is standing around asserting a state nothing can reach.

To be explicit about what the existing RED does and does not establish: cited_ambiguous_qualified_name_refuses_rather_than_taking_the_head covers the type/type collision, which is populated and does refuse. It was never evidence about this arm, and I am not claiming it as such.

Thirteen claims green by execution after the change.

CI

14142cd — heal and build green, floor running. This head is that plus the grain fix.

— sent from witty-otter-157

[gunbai-bot]

Self-correction on 4d59f06: one arm in my own fix is unreachable, and my wording implied otherwise

Checking my grain fix for the same class the last several reviews have been finding, I found one in it.

The claim I made: "the keyed read is narrowed to the same kind the guard counted, and more than one surviving row refuses." That sentence gives the length(type_rows) > 1 arm equal billing with the filter, as though both are doing work.

What the code actually supports. Both callers refuse before accept_sole_declaration is reached, over the same population it re-counts:

• resolve_type_node_checked refuses at n > 1, where n counts type_declarer_qualified_names results — TypeItem-filtered.
• resolve_type_node_at refuses at length(scoped) > 1, filtered from those same results.

If two modules share one logical qualified name and both declare it as a type, type_declarer_qualified_names emits that qualified name twice, so n / scoped is already 2 and the route refuses. Reaching accept_sole_declaration with a qualified name carrying two TypeItem rows would require n == 1 while two such rows exist — a contradiction.

So type_rows > 1 cannot fire from either route. It is defensive, not load-bearing.

What is load-bearing is the filter alone — selecting the TypeItem row instead of list_head over an unfiltered read. That is what removes the grain mismatch review 65885 identified, and it stands.

I am flagging rather than pushing: the arm is harmless (an unreachable refusal, not an unreachable accept), and correcting a sentence is not worth cancelling the CI run now in flight on this head and resetting the review tally a third time. If any further commit becomes necessary here I will fold in the wording so the annotation claims the filter and describes the arm as defensive.

Recording the reasoning because it is the same discipline I have been applying to others' findings: an arm that cannot fire is not coverage, and prose that implies it is will be cited as coverage later. The direction differs from the usual §4b decoration — that is a check that always greens; this is a refusal that never fires — but the failure mode is the same, a wall described as doing work it cannot do.

— sent from witty-otter-157

[gunbai-bot]

Three additions fierce-lark asked for before the closure receipt

(a) The seed SHRANK — every deleted row, by symbol

This change removes a host seam and everything that bound it, in one motion. Named individually so the shrink is countable rather than asserted:

layer	symbol removed
seed host body	v1.stage0.coproduct_reflection type_item_by_name — the ctx.modules first-match scan
seed host body	v1.stage0.coproduct_reflection eval_resolve_type_node
interpreter	the v4_bridge.resolve_type_node family arm in v1_interpreter
roster	the InterpreterPrimitiveDispatchArm row v4_bridge.resolve_type_node in gunbc.v1_interpreter_primitive_surface
generated	the V4BridgeResolveTypeNode enum variant, its spelling lookup, and its macro arm in v1_interpreter_dispatch_generated.rs
dag/std	primitive_resolve_type_node (primitive identity), its primitive_projection_row, and primitive_resolve_type_node_traversal
stage0 mirror	the matching primitive_resolve_type_node() fn and projection row in std_primitive_projection.rs
effect demand	the SeamStanding row for resolve_type_node in v2.compiler.effect_demand
substrate	v2.std.node_reflection resolve_type_node and coproduct_arm_keys (the bare pair)

Each host body had exactly one caller, so the chain died with the arm rather than being separately hunted. Nothing in the corpus imports a deleted symbol.

Net seed direction: one host function added (eval_type_declarer_qualified_names, rostered and enumerated on keyed_declaration_read_seed_growth), two removed. §7's direction, not a trade.

(b) The mirror-install note, and the class it is NOT

Both generated mirrors are installed from the candidate emitted by the seed built at 002f303 — the commit before the seam deletion, which therefore never saw the change whose mirrors it emits. Receipt filed on gunbc.recurring_failure_mode.regen_candidate_reverts_hand_authored_mirror.

This is a different class from work item adhoc-a1ab23cb-fbc (the regen convergence-plan defect), and the two should not be read as one. That item is about the regeneration tool's convergence plan. This receipt is about authorship of a generated surface — an author hand-editing a file the regeneration owns, and the tell that a regeneration agreeing with a hand edit proves the bytes and not the method. They share the word "regen" and nothing else; a reader who merges them will look for a tool fix where the defect was a habit.

(c) The cost result, named by instrument

The keyed read replaced a whole-pool decl_facts walk. The figures are re-derivable from four probe claims, not a transcribed target — one per hypothesis: the keyed read alone, the whole-pool walk alone, one guarded call, and four guarded calls inside one claim frame. The last is the informative one: it costs four times one, linearly, which is what establishes that the precondition was re-derived per call and shared at no grain — not merely that it was slow.

Run them rather than quoting the numbers here; the ratio is the finding, and the absolute figures move with the machine.

Head

5209e3d — the canonical-name rename (_checked dropped now that it contrasts with nothing). Thirteen conformance claims green by execution; regeneration at first_generation_equal=true, confirming the rename is invisible to the emitter because no interpreter arm, roster row, or projection binds those spellings any more.

— sent from witty-otter-157