From 6301150b736f2313f3f5e2b03572152dc0093d0a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 17:31:13 +0000 Subject: [PATCH 01/16] Reflection refuses a forked type spelling instead of answering from one of two 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, so a spelling declared in two modules is answered from whichever the load order reached first, with no diagnostic. That is DESIGN section 5 silent wrongness at a seam whose answers feed every arm-key and nullary-inhabitant consumer. WHAT THIS CHANGE ADDS, and what it deliberately does not. It adds a guarded route beside the bare one -- resolve_type_node_checked and 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 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. It does NOT rewire any existing caller. The bare pair stays reachable and stays unguarded; that cutover is a declared frontier, stated in the module annotation with its trigger, and it is sequenced behind the reference-grain census that fierce-lark-661 ruled a precondition for landing any refusal at this seam. EVIDENCE BY EXECUTION, not by reading the body. Seven claims in v2.test.manual.scoped_type_reflection_conformance run green over the roots dag and src/v2. The two ambiguity claims are discriminating: with the guard's many-arm disabled, both go red and both controls stay green, so they test the guard and not the corpus. The two specimens did NOT behave alike, and the census row says so rather than generalizing from one. UriScheme -- a coproduct in extdeps.uri and a record in v2.std.network -- is ANSWERED by the bare seam today, which the already-enrolled claim witness_uri_scheme_reflected_arm_keys_are_non_empty asserts 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, which is the defect. It also files the seam 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, because the declaration side is not the reach 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 by claim_batch -- under the fast lane's budget but 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 is the next unit. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01AVrnmuwhfmAhUeLRiVAjB2 --- .../bare_name_identity_consumer_census.dag | 10 ++ src/v2/std/node_reflection.dag | 129 ++++++++++++++++- ...coped_type_reflection_conformance_test.dag | 130 ++++++++++++++++++ 3 files changed, 268 insertions(+), 1 deletion(-) create mode 100644 src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag diff --git a/dag/gunbc/bare_name_identity_consumer_census.dag b/dag/gunbc/bare_name_identity_consumer_census.dag index 5ed3583330e..64ac49f51aa 100644 --- a/dag/gunbc/bare_name_identity_consumer_census.dag +++ b/dag/gunbc/bare_name_identity_consumer_census.dag @@ -226,6 +226,16 @@ data bare_name_identity_consumers: List = [ sibling: SiblingPresentButOrdered { sibling: decl_ref(module_path: "v1.compiler.infer_items", decl_name: "leaf_owner_modules_from_registry"), precedence: "the ambiguity arm runs INSTEAD of last-write-wins, which is the shape every row above is missing" }, call_site_count: 2, }, + { + site: decl_ref(module_path: "v2.std.node_reflection", decl_name: "resolve_type_node"), + fact_sought: "the declaration Node of the closed coproduct a type name denotes, which is what every arm-key and nullary-inhabitant answer is then read off", + keys_on: "a bare Symbol spelling and nothing else -- the seam's whole signature is the spelling, so the resolving scope is not an input the key can cover", + identity: AvailableUpstreamNotThreaded { nearest_holder: decl_ref(module_path: "v2.std.decl_ref_resolution", decl_name: "resolve_declaration_ref_live") }, + outcome: SilentWrongProviderAnswer { what_is_emitted: "the arm-key list of whichever declaration the interpreter's loaded-module order reached first, with nothing said about which. The mechanism is read from the host arm v4_bridge.resolve_type_node, realized by v1.stage0.coproduct_reflection type_item_by_name, which iterates ctx.modules and returns the FIRST item whose authored name matches and whose registry kind is TypeItem. WHAT WAS ACTUALLY EXECUTED, because reading that body is not evidence about the running compiler and the two specimens did NOT behave alike: for UriScheme -- a coproduct in extdeps.uri and a record in v2.std.network -- the seam ANSWERS, and the already-enrolled claim v2.test.manual.coproduct_reflection_conformance witness_uri_scheme_reflected_arm_keys_are_non_empty is green on main asserting exactly that non-empty answer; for Representation -- a coproduct in both v2.lens.intent_linearity and v2.std.integer, with disjoint arm sets -- the seam instead raises an untyped host error, unknown closed type, rather than picking. So this row claims a silent answer for the first shape and NOT for the second, and neither shape produces a typed located refusal, which is the defect the row is filed for. Both observations are from claim_batch runs over the roots dag and src/v2 against the claims in v2.test.manual.scoped_type_reflection_conformance" }, + reach: ReachabilityUnmeasured { what_would_settle_it: "a REFERENCE-grain census -- referencing module, bare spelling, candidate declaring modules -- over every call site of the three reflection seams, joined against the homonym declaration set from gunbc.bare_name_fork_lens bare_name_declarations_of. The declaration side is NOT the reach of this row and must not be substituted for it: a spelling declared twice but never referenced bare across scope reaches nothing here. That instrument does not exist yet and this row deliberately does not guess its result; fierce-lark-661 has ruled it a precondition for any refusal at this seam, and gunbc.bare_name_identity_consumer_census's own sweep-before-refusal law says the same thing. The call_site_count on this row is at a stated grain that is NOT the reach: it counts call sites of all THREE reflection seams -- resolve_type_node, coproduct_arm_keys and coproduct_nullary_inhabitants -- because the latter two reach this decision through the first, so the decision is made once per such site. It counts SITES, not ambiguous sites; how many of them name a spelling that is actually forked is exactly the unmeasured reach above" }, + sibling: SiblingPresentButUnreachable { sibling: decl_ref(module_path: "v2.std.decl_ref_resolution", decl_name: "resolve_declaration_ref_live"), why_unreachable: "the identity-keyed authority exists, is live-tree keyed, and already derives an explicit ambiguity arm from exactly the multiplicity this seam ignores -- but nothing routes to it, because resolve_type_node's parameter is a Symbol and a Symbol cannot name a module. The sibling is not consulted second, as at the ordered rows above; it is unreachable through this signature at all, so the repair is a signature change and not a reordering" }, + call_site_count: 16, + }, ] // THE HISTOGRAM IS DERIVED, NEVER STORED. A stored count is a second representation of the roster diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index 82a42119a85..de89dca2373 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -1,7 +1,19 @@ module v2.std.node_reflection +import std.decl_ref { DeclarationRef } import v2.std.collection { List } -import v2.std.diagnostic { Outcome } +import v2.std.diagnostic { + AmbiguousIntent, + Diagnostic, + Outcome, + Unavailable, + bind_outcome, + invariant_port_locus, + outcome_accepted, + outcome_rejected +} +import v2.std.compilers.lexing { symbol_intern_lexeme, symbol_lexeme } +import v2.std.decl_index { DeclFact, TypeItem, decl_facts, logical_qualified_name_from_module } import v2.std.node { Node, Symbol } import v2.std.node_query { coproduct_arm_key_list_from_node } @@ -45,3 +57,118 @@ fn coproduct_nullary_inhabitants( discriminant_of: discriminant_of ) } + +// THE SCOPE-CARRYING ROUTE, AND WHY THE BARE ONE ABOVE CANNOT STAY THE ONLY ONE. +// +// `resolve_type_node` keys on a BARE spelling. Its host arm (v4_bridge.resolve_type_node, +// realized by v1.stage0.coproduct_reflection type_item_by_name) answers it by scanning the +// interpreter's loaded modules in order and returning the FIRST item whose authored name +// matches. When one spelling is declared as a closed coproduct in two modules, that scan +// returns whichever module the load order reached first -- a different arm set, with no +// diagnostic. It is DESIGN section 5 silent wrongness: not a refusal, a wrong answer that +// typechecks. The corpus inhabits the invalid state today, so this is a live class and not a +// hypothetical one; the discriminating pair enrolled against it is in +// `v2.test.claim.manual.scoped_type_reflection_conformance`. +// +// The fix mints NO new identity and NO new host seam, which is the whole point (DESIGN +// section 3). The multiplicity that decides ambiguity is already a substrate fact: +// `v2.std.decl_index` decl_facts carries one row per declaration with its bare `name`, its +// `kind`, and its `qualified_name`. So the guard is derivable here, in `.dag`, from the index +// that `v2.std.decl_ref_resolution` already treats as the authority for exactly this question +// -- "how many declarations answer to this name" -- and whose five-arm refusal law this module +// deliberately does not restate. +// +// Consumers (DESIGN section 3c). Consumed by execution in this change: the conformance witness +// named above. Declared frontier, with its trigger stated: the floor's cross-claim memo and +// `coproduct_arm_keys`'s callers (`v2.lens.affected_set`, the generated coproduct witnesses) +// cut over to `coproduct_arm_keys_at` once a key shape is agreed with the floor-cost lane -- +// that cutover is the trigger, and until it lands the bare pair above stays reachable and +// stays unguarded, which this annotation states rather than hides. +fn type_decl_facts_named(pool_roots: List, type_name: Symbol) -> List { + filter( + xs: decl_facts(pool_roots: pool_roots), + predicate: fn(fact) { + fact.name == symbol_lexeme(sym: type_name) && fact.kind == TypeItem + } + ) +} + +fn scoped_type_reflection_diagnostic(type_name: Symbol, invariant: Symbol) -> Diagnostic { + Diagnostic { + reason: invariant, + at: invariant_port_locus(port: type_name, invariant: invariant), + correction: Unavailable { reason: AmbiguousIntent } + } +} + +// A bare spelling resolves ONLY where the index proves exactly one type declaration answers to +// it; zero and many each refuse, typed and located, rather than widening to a first match +// (DESIGN section 5 -- a failure arm refuses, never widens). The single-row arm is the only one +// that may reach the bare host seam, and it may do so precisely because uniqueness has been +// established BEFORE the call rather than assumed by it. +fn resolve_type_node_checked(pool_roots: List, type_name: Symbol) -> Outcome { + let candidates = type_decl_facts_named(pool_roots: pool_roots, type_name: type_name) + let n = length(xs: candidates) + if n == 0 { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^type_declaration_absent + ) + ) + } else if n > 1 { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^type_spelling_ambiguous_across_modules + ) + ) + } else { + outcome_accepted(value: resolve_type_node(type_name: type_name)) + } +} + +fn coproduct_arm_keys_checked( + pool_roots: List, + type_name: Symbol +) -> Outcome> { + bind_outcome( + o: resolve_type_node_checked(pool_roots: pool_roots, type_name: type_name), + f: fn(node) { + outcome_accepted(value: coproduct_arm_key_list_from_node(node: node)) + } + ) +} + +// THE ROUTE THAT MAKES A CALLER SAY WHICH MODULE IT MEANT. `resolve_type_node_checked` refuses an +// ambiguous spelling but cannot resolve one; a caller that legitimately means one of several +// same-spelled types names it by citation instead, reusing `std.decl_ref` DeclarationRef -- the +// corpus's existing carrier for "this declaration, in this module" -- so no second spelling of a +// scoped type identity is minted here. When PR #11264 lands its occurrence bindings, this is the +// declaration whose parameter becomes that binding: the citation is refined in place, not forked. +fn resolve_type_node_at(pool_roots: List, ref: DeclarationRef) -> Outcome { + let wanted = logical_qualified_name_from_module( + module_name: ref.module_path as String, + name: ref.decl_name as String + ) + let type_name = symbol_intern_lexeme(lexeme: ref.decl_name as String) + let candidates = type_decl_facts_named(pool_roots: pool_roots, type_name: type_name) + let scoped = filter(xs: candidates, predicate: fn(fact) { fact.qualified_name == wanted }) + if length(xs: scoped) == 1 && length(xs: candidates) == 1 { + outcome_accepted(value: resolve_type_node(type_name: type_name)) + } else if length(xs: scoped) == 0 { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^cited_type_declaration_absent + ) + ) + } else { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^cited_type_unreachable_through_bare_host_seam + ) + ) + } +} diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag new file mode 100644 index 00000000000..73259e20e5e --- /dev/null +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -0,0 +1,130 @@ +module v2.test.manual.scoped_type_reflection_conformance + +import std.decl_ref { DeclarationRef, WholeDeclaration } +import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } +import v2.std.node_reflection { + coproduct_arm_keys_checked, + resolve_type_node_at, + resolve_type_node_checked +} + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THE POOL ROOTS THIS CLAIM READS. Named, not discovered: the claim is about what the live +// declaration index says under a stated population, and a population the claim does not state +// is one a reader cannot re-derive (DESIGN section 6 -- name the instrument). +data scoped_reflection_pool_roots: List = ["dag", "src/v2"] + +fn outcome_is_rejected(o: Outcome) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + +fn outcome_is_accepted(o: Outcome) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => true + Rejected { diagnostics: _ } => false + } +} + +// THE DISCRIMINATING RED. `Representation` is declared as a closed coproduct in two modules of +// this very pool -- `v2.lens.intent_linearity` and `v2.std.integer` -- with DISJOINT arm sets. +// The bare host seam answers it by first match over the interpreter's loaded modules, so before +// this change `coproduct_arm_keys` returned one of two different answers with no diagnostic and +// no way for a caller to know which. The claim is not that two declarations exist -- that is a +// fact about the corpus and would be a change detector. The claim is that the GUARDED route +// REFUSES rather than answering, which is a fact about this module's behaviour and goes red the +// moment the guard is removed or widened to a first match. +test fn ambiguous_type_spelling_refuses_rather_than_first_matching() -> Bool { + outcome_is_rejected( + o: coproduct_arm_keys_checked( + pool_roots: scoped_reflection_pool_roots, + type_name: ^Representation + ) + ) +} + +test fn ambiguous_type_spelling_refuses_at_the_node_route_too() -> Bool { + outcome_is_rejected( + o: resolve_type_node_checked( + pool_roots: scoped_reflection_pool_roots, + type_name: ^Representation + ) + ) +} + +// THE POSITIVE CONTROL, and it is the one that keeps the wall from being satisfied by refusing +// everything. `Connective` is declared once in this pool, so the guard must let it through and +// the arm keys must still come back. A guard that refused here would pass the two claims above +// while destroying the surface, which is why this claim is enrolled beside them and not after. +test fn unique_type_spelling_still_resolves() -> Bool { + outcome_is_accepted( + o: coproduct_arm_keys_checked( + pool_roots: scoped_reflection_pool_roots, + type_name: ^Connective + ) + ) +} + +// AN ABSENT SPELLING REFUSES ON ITS OWN ARM rather than falling through to the seam, which is +// what makes the zero case a refusal and not a divergent host call. +test fn absent_type_spelling_refuses() -> Bool { + outcome_is_rejected( + o: resolve_type_node_checked( + pool_roots: scoped_reflection_pool_roots, + type_name: ^NoSuchTypeIsDeclaredAnywhereInThisPool + ) + ) +} + +// THE CITATION ROUTE. Naming the module resolves a unique spelling; it does NOT yet rescue an +// ambiguous one, because the bare host seam it delegates to cannot be told which module to read +// -- so that case refuses too, and says so on its own arm rather than guessing. Shrinking that +// refusal is what consuming #11264's occurrence binding buys, and this claim is where the change +// will show. +test fn cited_unique_type_resolves_through_its_module() -> Bool { + outcome_is_accepted( + o: resolve_type_node_at( + pool_roots: scoped_reflection_pool_roots, + ref: DeclarationRef { + module_path: "v2.std.node", + decl_name: "Connective", + field: WholeDeclaration + } + ) + ) +} + +test fn cited_ambiguous_type_refuses_until_the_seam_is_scope_carrying() -> Bool { + outcome_is_rejected( + o: resolve_type_node_at( + pool_roots: scoped_reflection_pool_roots, + ref: DeclarationRef { + module_path: "v2.std.integer", + decl_name: "Representation", + field: WholeDeclaration + } + ) + ) +} + +// THE SECOND SPECIMEN, AND THE ONE WHOSE CONTRAST IS ALREADY ENROLLED. UriScheme is declared in +// two modules of this pool -- a closed coproduct in extdeps.uri and a RECORD in v2.std.network -- +// and the unguarded seam answers it today rather than refusing: the enrolled claim +// v2.test.manual.coproduct_reflection_conformance witness_uri_scheme_reflected_arm_keys_are_non_empty asserts that +// coproduct_arm_keys(^UriScheme) returns a non-empty list, and it is green on main. So this pair +// is the case where the bare seam picks one of two declarations and says nothing, while the pair +// in the claims above is the case where it raises an untyped host error instead. Both are the same +// missing scope; only the guarded route below tells them apart from a caller's position, and the +// contrast claim is CITED rather than restated here so this module does not fork it. +test fn forked_spelling_answered_today_by_the_bare_seam_refuses_when_guarded() -> Bool { + outcome_is_rejected( + o: coproduct_arm_keys_checked( + pool_roots: scoped_reflection_pool_roots, + type_name: ^UriScheme + ) + ) +} From 74ed6cddbd2706b7c6eeec73b7dab083040a2b17 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 18:04:33 +0000 Subject: [PATCH 02/16] Refuse a unique but non-coproduct spelling instead of diverging into the host review 65546: the guard established uniqueness of the SPELLING and stopped there. decl_facts kind TypeItem does not separate a closed coproduct from a record -- this module's own UriScheme specimen depends on the v2.std.network RECORD counting as a candidate -- so a spelling declared exactly once as a record satisfied the n == 1 arm, reached the bare host seam, and was answered with the untyped host error "type is not a closed coproduct", which is precisely the untyped exit this surface exists to close and the contract the module's own annotation already asserted. The discriminator was already in hand and no new authority is minted: DeclFact carries its node, and v2.std.node_query node_is_coproduct is the existing predicate over that node. Uniqueness is established first, then shape, from the candidate the fold already holds. The reviewer's specimen is enrolled rather than argued: coproduct_arm_keys_checked on DeclFact -- one declaration, a record, in v2.std.decl_index -- diverged before this arm and refuses on its own arm after it. The positive control is the load-bearing half of the evidence and it still holds: Connective, a coproduct declared once, still RESOLVES, so the shape arm refuses the record case without over-refusing the case the surface exists to serve. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01AVrnmuwhfmAhUeLRiVAjB2 --- src/v2/std/node_reflection.dag | 31 +++++++++++++++++-- ...coped_type_reflection_conformance_test.dag | 16 ++++++++++ 2 files changed, 45 insertions(+), 2 deletions(-) diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index de89dca2373..8a6f3a67fb2 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -15,7 +15,7 @@ import v2.std.diagnostic { import v2.std.compilers.lexing { symbol_intern_lexeme, symbol_lexeme } import v2.std.decl_index { DeclFact, TypeItem, decl_facts, logical_qualified_name_from_module } import v2.std.node { Node, Symbol } -import v2.std.node_query { coproduct_arm_key_list_from_node } +import v2.std.node_query { coproduct_arm_key_list_from_node, node_is_coproduct } // THE HOST TYPE-REFLECTION SURFACE, AND WHY IT IS ITS OWN MODULE. // @@ -124,7 +124,34 @@ fn resolve_type_node_checked(pool_roots: List, type_name: Symbol) -> Out ) ) } else { - outcome_accepted(value: resolve_type_node(type_name: type_name)) + match list_head(xs: candidates) { + HeadAbsent => + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^type_declaration_absent + ) + ) + HeadFound { value: sole } => + // THE THIRD ARM, AND WHY UNIQUENESS ALONE WAS NOT THE CONTRACT. decl_facts kind TypeItem + // does not distinguish a closed coproduct from a record -- this module's own UriScheme + // specimen depends on the v2.std.network RECORD counting as a candidate -- so a spelling + // declared exactly once as a record satisfied the uniqueness arm and reached the bare host + // seam, which answers it with an untyped host error rather than a typed located refusal. + // That is the same untyped exit this surface exists to close, so uniqueness is checked and + // then SHAPE is checked, from the node the candidate already carries. No new authority: + // node_is_coproduct is v2.std.node_query's existing predicate over the same Node. + if node_is_coproduct(node: sole.node) { + outcome_accepted(value: resolve_type_node(type_name: type_name)) + } else { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^type_spelling_is_not_a_closed_coproduct + ) + ) + } + } } } diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag index 73259e20e5e..4a7660a13e7 100644 --- a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -128,3 +128,19 @@ test fn forked_spelling_answered_today_by_the_bare_seam_refuses_when_guarded() - ) ) } + +// THE REVIEWER'S SPECIMEN, ENROLLED RATHER THAN ARGUED. review 65546 found that the guard +// established uniqueness of the SPELLING without establishing that the sole declaration is a +// closed coproduct: decl_facts kind TypeItem covers records too, so a spelling declared exactly +// once as a record passed the uniqueness arm and reached the bare host seam, which answers with an +// untyped host error rather than a typed located refusal. DeclFact is such a spelling -- one +// declaration, a record, in v2.std.decl_index. Before the shape arm this claim diverged; it now +// refuses on its own arm, which is the contract this module's annotation already asserted. +test fn unique_but_non_coproduct_spelling_refuses_rather_than_diverging() -> Bool { + outcome_is_rejected( + o: coproduct_arm_keys_checked( + pool_roots: scoped_reflection_pool_roots, + type_name: ^DeclFact + ) + ) +} From dfa8d1fd8d11921f41f2499e401bb6229a44d0a8 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 18:48:06 +0000 Subject: [PATCH 03/16] Key the reflection guard host-side: 3.6s per call becomes 1-3ms THE COST DEFECT THIS REMOVES, measured rather than argued. The guard established bare-name multiplicity by folding the whole declaration corpus, because decl_facts_at is keyed by QUALIFIED name and a bare spelling has no module. Four probe claims under claim_batch over roots dag and src/v2: the keyed read 1ms, the whole-pool walk 3628ms, one guarded call 4392ms, and FOUR guarded calls in ONE claim frame 15420ms -- linear, so the precondition was re-derived per CALL and shared at no grain. That is gunbc.recurring_failure_mode shared_precondition_re_derived_once_per_claim_frame sitting inside the very route meant to make the reflection memo key sound, and it put the guard roughly seven times above the floor's per-claim ceiling. THE WIRE, and the boundary that admits it. v2.std.decl_index type_declarer_qualified_names is a keyed bare-name read: the host filters the SAME memoized pool decl_facts_at reads -- no second parse, no second memo -- and marshals no declaration nodes, which is where the whole-pool cost lived. It returns EVERY qualified name declaring the spelling as a type, so multiplicity and candidate identity are both decided in the substrate and the Rust never picks a match. The moment it chose among candidates it would be the bare-name identity defect it exists to remove, one layer down. Admitted as a seed arm only after the substrate routes were shown insufficient BY MEASUREMENT, per the standing condition; it grows the seed and the measurement above is its reason. The same nine claims are now 1-3ms each, all green, under the floor ceiling with three orders of magnitude of headroom. ONE ACCEPT PATH, WHICH IS THE REAL FIX FOR review 65571. The shape arm had been added to the spelling route and not to the citation route, so resolve_type_node_at still reached the bare seam for a record and answered with an untyped host error -- the exact exit its sibling had just closed. Two copies of one acceptance law is the DESIGN section 3 fork that produced the divergence, so accept_sole_declaration is now the only path to the seam and neither route may call it otherwise. The finding is covered on both routes rather than only where it was reported. Also from review 65571: the module annotation cited v2.test.claim.manual.scoped_type_reflection_conformance, but the module declares v2.test.manual.scoped_type_reflection_conformance. The citation did not resolve; corrected. The indented annotation block inside the guard body was a parse error at module-item grain (required-witnesses-floor on 74ed6cd) and is dissolved by the same refactor: the reasoning now sits above accept_sole_declaration, where a reader and the parser both expect it. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01AVrnmuwhfmAhUeLRiVAjB2 --- .../v1/v1_interpreter_primitive_surface.dag | 9 ++ src/v1/stage0/src/coproduct_reflection.rs | 45 ++++++++ src/v1/stage0/src/v1_interpreter.rs | 14 +++ .../src/v1_interpreter_dispatch_generated.rs | 3 + src/v2/std/decl_index.dag | 21 ++++ src/v2/std/node_reflection.dag | 104 ++++++++++++------ ...coped_type_reflection_conformance_test.dag | 19 ++++ 7 files changed, 184 insertions(+), 31 deletions(-) diff --git a/dag/gunbc/v1/v1_interpreter_primitive_surface.dag b/dag/gunbc/v1/v1_interpreter_primitive_surface.dag index 3d252c3ec0f..e498a1bf889 100644 --- a/dag/gunbc/v1/v1_interpreter_primitive_surface.dag +++ b/dag/gunbc/v1/v1_interpreter_primitive_surface.dag @@ -979,6 +979,15 @@ fn v1_interpreter_authored_roster_arms() -> List InterpResult { + // Same line-stop as `eval_decl_facts_at`, and for the same reason: a root that contributes + // nothing is invisible in a keyed answer, because an empty result is what a genuine miss looks + // like — so the refusal fires against the DECLARED roots, before the read. + let pool_root_defects_found = pool_root_defects(pool_roots); + if !pool_root_defects_found.is_empty() { + return Err( + crate::v1_interpreter::InterpError::PoolRootContributesNothing { + caller: "type_declarer_qualified_names", + declared: pool_roots.len(), + defects: pool_root_defects_found, + }, + ); + } + let facts = decl_facts_for_roots_shared(pool_roots); + let mut names: Vec = Vec::new(); + for fact in facts.iter() { + if fact.name == bare_name && fact.kind == ItemKind::TypeItem { + names.push(str_value(fact.qualified_name.clone())); + } + } + Ok(crate::v1_interpreter::list_value(names)) +} + fn eval_decl_facts_rows(ctx: &InterpContext, facts: &[DeclFactRaw]) -> InterpResult { let mut rows = Vec::with_capacity(facts.len()); for fact in facts { diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index a3ffc7242d7..d20be4585fe 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -18292,6 +18292,20 @@ macro_rules! v1_builtin_arms { )?)) }, + arm "free_call.type_declarer_qualified_names" { "type_declarer_qualified_names" } => { + let pool_roots = + expect_str_list($positional.first().copied(), "type_declarer_qualified_names")?; + let bare_name = + expect_value_str($positional.get(1).copied(), "type_declarer_qualified_names")?; + Ok(Some( + crate::coproduct_reflection::eval_type_declarer_qualified_names( + $ctx, + &pool_roots, + bare_name.as_str(), + )?, + )) + }, + arm "free_call.module_declaration_facts_at" { "module_declaration_facts_at" } => { let pool_roots = expect_str_list($positional.first().copied(), "module_declaration_facts_at")?; diff --git a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs index 6b99ee5437a..ff43e92a08d 100644 --- a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs +++ b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs @@ -73,6 +73,7 @@ pub enum EvalBuiltinArm { FreeCallExportSignatureFacts, FreeCallDeclFacts, FreeCallDeclFactsAt, + FreeCallTypeDeclarerQualifiedNames, FreeCallModuleDeclarationFacts, FreeCallModuleDeclarationFactsAt, FreeCallFactCardinalityDeclFacts, @@ -212,6 +213,7 @@ pub fn lookup_eval_builtin_inner(spelling: &str) -> Option { "export_signature_facts" => Some(EvalBuiltinArm::FreeCallExportSignatureFacts), "decl_facts" => Some(EvalBuiltinArm::FreeCallDeclFacts), "decl_facts_at" => Some(EvalBuiltinArm::FreeCallDeclFactsAt), + "type_declarer_qualified_names" => Some(EvalBuiltinArm::FreeCallTypeDeclarerQualifiedNames), "module_declaration_facts" => Some(EvalBuiltinArm::FreeCallModuleDeclarationFacts), "module_declaration_facts_at" => Some(EvalBuiltinArm::FreeCallModuleDeclarationFactsAt), "fact_cardinality_decl_facts" => Some(EvalBuiltinArm::FreeCallFactCardinalityDeclFacts), @@ -349,6 +351,7 @@ macro_rules! eval_builtin_inner_arm { ("free_call.export_signature_facts") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallExportSignatureFacts }; ("free_call.decl_facts") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallDeclFacts }; ("free_call.decl_facts_at") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallDeclFactsAt }; + ("free_call.type_declarer_qualified_names") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallTypeDeclarerQualifiedNames }; ("free_call.module_declaration_facts") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallModuleDeclarationFacts }; ("free_call.module_declaration_facts_at") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallModuleDeclarationFactsAt }; ("free_call.fact_cardinality_decl_facts") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallFactCardinalityDeclFacts }; diff --git a/src/v2/std/decl_index.dag b/src/v2/std/decl_index.dag index 802d07b62b3..cf228f2b670 100644 --- a/src/v2/std/decl_index.dag +++ b/src/v2/std/decl_index.dag @@ -29,6 +29,27 @@ fn decl_facts_at(pool_roots: List, qualified_name: String) -> List, bare_name: String) -> List { + type_declarer_qualified_names(pool_roots: pool_roots, bare_name: bare_name) +} + fn export_signature_facts(pool_roots: List) -> List { export_signature_facts(pool_roots: pool_roots) } diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index 8a6f3a67fb2..964fcbcd7df 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -13,7 +13,12 @@ import v2.std.diagnostic { outcome_rejected } import v2.std.compilers.lexing { symbol_intern_lexeme, symbol_lexeme } -import v2.std.decl_index { DeclFact, TypeItem, decl_facts, logical_qualified_name_from_module } +import v2.std.decl_index { + DeclFact, + decl_facts_at, + logical_qualified_name_from_module, + type_declarer_qualified_names +} import v2.std.node { Node, Symbol } import v2.std.node_query { coproduct_arm_key_list_from_node, node_is_coproduct } @@ -68,7 +73,7 @@ fn coproduct_nullary_inhabitants( // diagnostic. It is DESIGN section 5 silent wrongness: not a refusal, a wrong answer that // typechecks. The corpus inhabits the invalid state today, so this is a live class and not a // hypothetical one; the discriminating pair enrolled against it is in -// `v2.test.claim.manual.scoped_type_reflection_conformance`. +// `v2.test.manual.scoped_type_reflection_conformance`. // // The fix mints NO new identity and NO new host seam, which is the whole point (DESIGN // section 3). The multiplicity that decides ambiguity is already a substrate fact: @@ -84,12 +89,19 @@ fn coproduct_nullary_inhabitants( // cut over to `coproduct_arm_keys_at` once a key shape is agreed with the floor-cost lane -- // that cutover is the trigger, and until it lands the bare pair above stays reachable and // stays unguarded, which this annotation states rather than hides. -fn type_decl_facts_named(pool_roots: List, type_name: Symbol) -> List { - filter( - xs: decl_facts(pool_roots: pool_roots), - predicate: fn(fact) { - fact.name == symbol_lexeme(sym: type_name) && fact.kind == TypeItem - } +// WHY THIS IS A KEYED READ AND NOT A FOLD OVER decl_facts. The first version of this guard filtered +// the whole declaration corpus, which was correct and cost roughly 3.6s per call against 1ms for a +// keyed read, sharing at no grain -- four calls inside ONE claim frame cost four times one. That put +// the guard that makes reflection sound far above the floor's per-claim ceiling, and it was itself +// gunbc.recurring_failure_mode shared_precondition_re_derived_once_per_claim_frame in the very route +// meant to make the reflection memo key sound. v2.std.decl_index type_declarer_qualified_names is +// the keyed answer: the host filters the same memoized pool decl_facts_at reads and marshals no +// declaration nodes, and it returns EVERY candidate rather than choosing among them, so the +// multiplicity and the candidate identities are both decided here. +fn type_declarer_names(pool_roots: List, type_name: Symbol) -> List { + type_declarer_qualified_names( + pool_roots: pool_roots, + bare_name: symbol_lexeme(sym: type_name) ) } @@ -101,13 +113,52 @@ fn scoped_type_reflection_diagnostic(type_name: Symbol, invariant: Symbol) -> Di } } +// THE ONLY PATH TO THE BARE HOST SEAM, SHARED BY BOTH ROUTES ON PURPOSE. review 65571 found that +// the shape check had been added to the spelling route and not to the citation route, so the +// citation route still reached the seam for a record and got an untyped host error -- the exact +// exit the sibling had just closed. Two copies of one acceptance law is the section 3 fork that +// produced that divergence, so there is now ONE copy and neither route may call the seam except +// through it. +// +// It establishes SHAPE after its caller has established uniqueness. decl_facts kind TypeItem does +// not separate a closed coproduct from a record -- this module's own UriScheme specimen depends on +// the v2.std.network RECORD counting as a candidate -- so uniqueness alone was never the contract +// the annotations claimed. No new authority: node_is_coproduct is v2.std.node_query's existing +// predicate, read from the node the keyed fact already carries. +fn accept_sole_declaration( + pool_roots: List, + type_name: Symbol, + sole_qualified_name: String +) -> Outcome { + match list_head(xs: decl_facts_at(pool_roots: pool_roots, qualified_name: sole_qualified_name)) { + HeadAbsent => + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^type_declaration_absent + ) + ) + HeadFound { value: sole } => + if node_is_coproduct(node: sole.node) { + outcome_accepted(value: resolve_type_node(type_name: type_name)) + } else { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^type_spelling_is_not_a_closed_coproduct + ) + ) + } + } +} + // A bare spelling resolves ONLY where the index proves exactly one type declaration answers to // it; zero and many each refuse, typed and located, rather than widening to a first match // (DESIGN section 5 -- a failure arm refuses, never widens). The single-row arm is the only one // that may reach the bare host seam, and it may do so precisely because uniqueness has been // established BEFORE the call rather than assumed by it. fn resolve_type_node_checked(pool_roots: List, type_name: Symbol) -> Outcome { - let candidates = type_decl_facts_named(pool_roots: pool_roots, type_name: type_name) + let candidates = type_declarer_names(pool_roots: pool_roots, type_name: type_name) let n = length(xs: candidates) if n == 0 { outcome_rejected( @@ -132,25 +183,12 @@ fn resolve_type_node_checked(pool_roots: List, type_name: Symbol) -> Out invariant: ^type_declaration_absent ) ) - HeadFound { value: sole } => - // THE THIRD ARM, AND WHY UNIQUENESS ALONE WAS NOT THE CONTRACT. decl_facts kind TypeItem - // does not distinguish a closed coproduct from a record -- this module's own UriScheme - // specimen depends on the v2.std.network RECORD counting as a candidate -- so a spelling - // declared exactly once as a record satisfied the uniqueness arm and reached the bare host - // seam, which answers it with an untyped host error rather than a typed located refusal. - // That is the same untyped exit this surface exists to close, so uniqueness is checked and - // then SHAPE is checked, from the node the candidate already carries. No new authority: - // node_is_coproduct is v2.std.node_query's existing predicate over the same Node. - if node_is_coproduct(node: sole.node) { - outcome_accepted(value: resolve_type_node(type_name: type_name)) - } else { - outcome_rejected( - d: scoped_type_reflection_diagnostic( - type_name: type_name, - invariant: ^type_spelling_is_not_a_closed_coproduct - ) - ) - } + HeadFound { value: sole_qualified_name } => + accept_sole_declaration( + pool_roots: pool_roots, + type_name: type_name, + sole_qualified_name: sole_qualified_name + ) } } } @@ -179,10 +217,14 @@ fn resolve_type_node_at(pool_roots: List, ref: DeclarationRef) -> Outcom name: ref.decl_name as String ) let type_name = symbol_intern_lexeme(lexeme: ref.decl_name as String) - let candidates = type_decl_facts_named(pool_roots: pool_roots, type_name: type_name) - let scoped = filter(xs: candidates, predicate: fn(fact) { fact.qualified_name == wanted }) + let candidates = type_declarer_names(pool_roots: pool_roots, type_name: type_name) + let scoped = filter(xs: candidates, predicate: fn(qn) { qn == wanted }) if length(xs: scoped) == 1 && length(xs: candidates) == 1 { - outcome_accepted(value: resolve_type_node(type_name: type_name)) + accept_sole_declaration( + pool_roots: pool_roots, + type_name: type_name, + sole_qualified_name: wanted + ) } else if length(xs: scoped) == 0 { outcome_rejected( d: scoped_type_reflection_diagnostic( diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag index 4a7660a13e7..89602a8d774 100644 --- a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -144,3 +144,22 @@ test fn unique_but_non_coproduct_spelling_refuses_rather_than_diverging() -> Boo ) ) } + +// THE SAME SPECIMEN ON THE CITATION ROUTE, which review 65571 found uncovered. The shape arm was +// added to the spelling route and the citation route kept its own accept, so a cited RECORD still +// reached the bare seam and answered with an untyped host error. Both routes now accept only +// through v2.std.node_reflection accept_sole_declaration, and this claim is what would go red if +// either grew a second accept again -- which is the divergence that produced the finding, not just +// the missing check. +test fn cited_unique_but_non_coproduct_spelling_refuses_rather_than_diverging() -> Bool { + outcome_is_rejected( + o: resolve_type_node_at( + pool_roots: scoped_reflection_pool_roots, + ref: DeclarationRef { + module_path: "v2.std.decl_index", + decl_name: "DeclFact", + field: WholeDeclaration + } + ) + ) +} From b387233bf7d38771f3ea0c38af98124480cd7598 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 19:13:06 +0000 Subject: [PATCH 04/16] File two receipts: the repair reproduced its own class, and a route that greens what the floor refuses Neither row is new. Both were found while repairing the reflection seam, and both belong on classes the ledger already carries, so they are filed as receipts rather than as neighbours. shared_precondition_re_derived_once_per_claim_frame gains a third specimen, and it is recorded for WHERE it happened: inside the repair for the defect this class's own consumers are blocked on. Establishing bare-name multiplicity had no keyed route -- decl_facts_at is keyed by qualified name, which a bare spelling has none of -- so the guard folded the whole declaration corpus once per call, and the lane meant to make the floor's cross-claim memo keyable reproduced the recurrence it was meant to unlock. Its measurement sharpens the row's grain rather than restating it. Four probe claims: keyed read 1ms, whole-pool walk 3628ms, one guarded call 4392ms, four guarded calls inside ONE claim frame 15420ms. The last is the informative one -- four times one, linearly -- so the precondition was re-derived once per CALL and shared at no grain, not even within the single frame the evaluator does memoize across. The second specimen reported that narrowing per parse call; this one measures it additively, and it says a producer share keyed per claim frame would have addressed only the smaller half. interpreted_run_accepts_what_the_floors_resolve_refuses gains a second specimen that carries a MEASURED mechanism for its own instance, which that row explicitly lacks and asks for. claim_batch ran a claim green over an indented body annotation while required-witnesses-floor refused the identical bytes. The isolating experiment that row prescribes was run, and the answer is that its open hypothesis does not apply here: a six-line single module, one local binary, compiled two ways -- gunbc compile REFUSES it typed and located, claim_batch ACCEPTS it and greens the claim. Same bytes, same binary, no population difference available to explain it. For this instance the difference is WHICH ROUTE RUNS THE CHECK: the BodyGrainNotModeled arm is reached on the compile and emit path and the claim route never reaches it. The receipt states what that does NOT settle, because the two specimens share a symptom and that is not evidence of a shared cause: the first refused with VariantNotFound under the floor's resolve, a diagnostic the claim route DOES compute, so its disagreement cannot be this mechanism and its population experiment remains unrun. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- ...preted_run_accepts_what_the_floors_resolve_refuses.dag | 8 ++++++++ ...hared_precondition_re_derived_once_per_claim_frame.dag | 7 +++++++ 2 files changed, 15 insertions(+) diff --git a/dag/gunbc/recurring_failure_mode/interpreted_run_accepts_what_the_floors_resolve_refuses.dag b/dag/gunbc/recurring_failure_mode/interpreted_run_accepts_what_the_floors_resolve_refuses.dag index 1d854b11e59..8306dc6b5fb 100644 --- a/dag/gunbc/recurring_failure_mode/interpreted_run_accepts_what_the_floors_resolve_refuses.dag +++ b/dag/gunbc/recurring_failure_mode/interpreted_run_accepts_what_the_floors_resolve_refuses.dag @@ -17,6 +17,14 @@ data interpreted_run_accepts_what_the_floors_resolve_refuses: RecurringFailureMo "SPECIMEN, gunbc#11026, 2026-09-11, both observations first-hand. `dag/std` distinguishes `List` from `FreeMonoid`: `[]` with `concat([x], acc)` builds the first, `Empty` with `Cons` the second, and a new module mixed them. `claim_batch --entry` over that tree resolved the entry -- reported 168 modules, 6554 resolved items -- and ran eight witnesses to PASS, including the discriminating ones. The required floor refused the SAME tree at `modules_resolved=110` with `dag/std/algebra.dag:367: variant 'Empty' not found in type 'List'`. Both readings are receipts; what is missing is the fact that explains the difference.", + "SECOND SPECIMEN, gunbc#11291, 2026-09-13, both observations first-hand -- and it carries a MEASURED mechanism for ITS OWN instance, which the first specimen still lacks. An indented `//` inside a declaration body: `claim_batch --entry` ran the claim and reported PASS, while required-witnesses-floor refused the identical bytes with `required-ci: parse FAIL ... source annotation sits inside a declaration body. Only module-item grain is modeled`. The author had a green execution receipt from a real consumer for source the merge path refuses, which is this row's shape exactly.", + + "ITS MECHANISM IS NOT POPULATION, AND THAT IS THE POINT OF RECORDING IT. The first specimen's open question is whether the disagreement comes from the runner or from resolving under a larger module set, and the isolating experiment this row prescribes is to compare the same entry under both. Run for this instance, the answer is NEITHER: a six-line single module, one indented annotation, ONE locally built binary, compiled two ways. `gunbc compile --source-root ` REFUSES it typed and located at `5:3`; `claim_batch --source-root dag --source-root src/v2 --entry ` ACCEPTS it and greens the claim. Same bytes, same binary, same declaration, no population difference available to explain it -- so for this instance the difference is in WHICH ROUTE RUNS THE CHECK, not in what the checks would say. The `AnnotationAttachmentRefusal` `BodyGrainNotModeled` arm is reached on the compile and emit path (`v1_compiler.cli_run.compile_clean`); the claim route resolves and evaluates without reaching it.", + + "WHAT THIS DOES AND DOES NOT SETTLE, because the two specimens share a shape and that is not evidence they share a cause. It settles that AT LEAST ONE member of this class is a route that does not run a check rather than two checks disagreeing -- which is a strictly worse failure than a gate mismatch, since no amount of strictness on the claim route's own gate would have caught it. It does NOT explain the first specimen: that one refused with `VariantNotFound` under the floor's resolve, a diagnostic the claim route DOES compute, so its disagreement cannot be this mechanism and the population experiment remains unrun for it. Identical symptom, two candidate causes, one now measured.", + + "THE PRACTICAL RULE THIS SPECIMEN ADDS: a local `claim_batch` green is not evidence about ANY refusal that lives on the compile or emit path, including the DESIGN section 4c annotation-grain refusals. For those classes the cheap local route is structurally silent rather than merely differently gated, so the check before pushing is a compile of the touched root, not a claim run over it.", + "WHAT WOULD ISOLATE IT, stated so the next occurrence produces the answer instead of another anecdote: the two runs differ in the POPULATION they resolve (an entry closure versus the floor's module set) and in nothing else that has been checked, so the discriminating experiment is to resolve the same entry under both populations and compare the diagnostic sets. If the entry closure alone refuses, the difference is in the runner; if it accepts while the larger set refuses, the difference is in how a declaration is typed when more modules are present, which is a different and more interesting class. Until that is run, no mechanism belongs in this row.", "DISTINGUISHING FACTS, available before any push and independent of the cause: a change lands in a layer whose idioms the author inferred from a NEIGHBOURING layer, the local run is green first try, and no floor result exists yet. The boundary against neighbours: this is NOT [[accepted_source_emits_uncompilable_target]], where the refusing party is a TARGET compiler outside this repository and the emission is the subject; both answers here are our own, about the same source, at the same stage. It is NOT [[realization_arms_diverge_on_whether_the_program_refuses]] either -- that class is two realizations of an ALREADY ACCEPTED program disagreeing at evaluation time, where here the disagreement is about acceptance itself and never reaches evaluation on the refusing side.", diff --git a/dag/gunbc/recurring_failure_mode/shared_precondition_re_derived_once_per_claim_frame.dag b/dag/gunbc/recurring_failure_mode/shared_precondition_re_derived_once_per_claim_frame.dag index ca8784e773f..b70a1f47ecf 100644 --- a/dag/gunbc/recurring_failure_mode/shared_precondition_re_derived_once_per_claim_frame.dag +++ b/dag/gunbc/recurring_failure_mode/shared_precondition_re_derived_once_per_claim_frame.dag @@ -22,6 +22,12 @@ data shared_precondition_re_derived_once_per_claim_frame: RecurringFailureMode = "SECOND SPECIMEN, gunbc#11032, arriving by the same recognition rule a day later and diagnosed by a lane that had not read this row. A newly landed family -- the where-refinement parse witnesses from gunbc#10946 -- refused the 500ms line on main with interrupted_before_verdict and nothing failing. Partitioned, the shared precondition dominated: v2.compiler.parse parse_grammar_digest and the production index were re-derived on EVERY PARSE CALL although prepare_grammar had fixed both before the first token, and the shared fixture sources were re-parsed per claim. The producer that named it is the floor's cross-claim demand census (main run 34556223550, required_floor_cross_claim_demand.tsv, row parse_grammar_digest). The repair was the one this row prescribes: carry both facts on the prepared grammar, the seam where the grammar is already resolved, and share the fixture trees warm (v2.workflow.floor_pure_producer_share floor_cross_claim_pure_producers_warm). Its frame is narrower than a claim -- per parse call -- which widens this row's reach rather than founding a neighbour: the question that finds it is still the one above. It also shows the census already locating the class and nothing refusing on it, which is this row's next-rung trigger unmet.", + "THIRD SPECIMEN, gunbc#11291, and it is recorded because of WHERE it occurred rather than because the shape is new: inside the repair for the defect this row's own consumers are blocked on. The reflection guard that makes a bare type spelling refuse rather than resolve to one of several same-spelled declarations had to establish bare-name multiplicity, and v2.std.decl_index decl_facts_at is keyed by QUALIFIED name, which a bare spelling has none of -- so the only substrate answer was to fold the whole declaration corpus, once per call. The lane that was meant to make the floor's cross-claim memo keyable therefore reproduced the recurrence it was meant to unlock, which is the hazard worth naming: a repair for this class is exactly where an author is least likely to look for it.", + + "ITS MEASUREMENT SHARPENS THE ROW'S GRAIN, and is the reason it is filed here rather than left in a PR. Four probe claims under claim_batch over roots dag and src/v2, one per hypothesis: the keyed read at 1ms, the whole-pool walk at 3628ms, one guarded call at 4392ms, and FOUR guarded calls inside ONE claim frame at 15420ms. The last figure is the informative one -- four times one, linearly -- so the precondition was re-derived once per CALL and shared at no grain, not even within the single frame the evaluator does memoize across. That is the same narrowing the second specimen reported per parse call, now measured additively rather than inferred, and it says a producer share keyed per claim frame would have addressed only the smaller half of this instance.", + + "ITS REPAIR IS THE ONE THIS ROW PRESCRIBES, taken at the seam where the fact is already resolved: v2.std.decl_index type_declarer_qualified_names answers the bare-name question against the SAME memoized declaration pool decl_facts_at already reads, marshalling no declaration nodes -- which is where the whole-pool cost actually lived. The nine claims that cost 3.6s each then cost 1-3ms each. Recorded with the boundary that admitted it, because the boundary is what keeps the repair from founding a new defect: the host returns EVERY candidate and never chooses among them, so the multiplicity and the candidate identities are decided in the substrate and a bare-name identity defect is not reintroduced one layer below the one being removed.", + "WHAT THE DIAGNOSTIC OFFERED AND WHY BOTH ARMS WERE WRONG, recorded because two readers took them in turn and neither questioned the frame. The refusal named exactly two remedies -- reduce the cost, or move the row to a lane declaring its own ceiling -- and a cost ladder showed the first unreachable, since the cheapest possible precondition was already 1.45x the line. That made the second arm look forced, and it is worse than it looks: the only off-floor home in the tree is a namespace the floor's own authority describes as NOT COVERED by anything, so routing there would have executed the rows nowhere and greened the gate over four unobserved claims. A diagnostic that enumerates its remedies teaches its reader that the enumeration is exhaustive; here the repair was in neither arm, and the reason is that both arms are about what the cost is ALLOWED to be while the defect was how many times it was paid.", "RUNG FOUND AT: mitigatable. The gate refuses, typed and located, and contains the harm -- it did not ship a wrong verdict. What it does not do is name the duplication, so the refusal is discovered per family and diagnosed by hand, and on this specimen two readers in sequence reasoned about cost allowance before anyone asked about cost multiplicity.", @@ -33,5 +39,6 @@ data shared_precondition_re_derived_once_per_claim_frame: RecurringFailureMode = evidence: [ DeclarationRef { module_path: "v2.compiler.parse", decl_name: "parse_grammar_digest", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.std.decl_index", decl_name: "type_declarer_qualified_names", field: WholeDeclaration }, ], } From 77afa5bd70faf165ff9651a53c128f77effcb332 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 19:52:41 +0000 Subject: [PATCH 05/16] Return the node the guard proved, and enumerate the seed arm on the roster that owns it review 65601 and review 65618, same two findings, both correct. THE ACCEPT ARM UNDID ITS OWN PROOF. accept_sole_declaration established uniqueness from the keyed read and shape from that fact's own node, and then threw the node away 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 versus interpreter-population divergence could still hand back a different declaration than the one just validated. Two producers for one fact, and the second is the one this module exists to stop trusting. It now returns sole.node. That is the same marshalling, not a different one: marshal_decl_fact_node sends a TypeItem to concept_decl_node, which for Connective::Disj is marshal_disj_type_item -- the identical function eval_resolve_type_node applies. The difference is only which item it is applied to, and the keyed one is the item whose identity was proven. THE POSITIVE CONTROL WAS TOO WEAK TO CATCH THIS, which is 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, so the control was blind to the class it was guarding. It now names the arm keys Connective actually declares, so a route that resolved a different same-named type, or returned a node of the wrong shape, fails instead of passing. The strengthened control was baselined PASS against the pre-change code before the change was made, so it is discriminating on the answer and not merely on the arm. THE SEED ARM IS 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, because 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 and the same inherited canonical order. It is there because the keyed read already on that roster cannot express its question: a qualified key cannot ask bare-name multiplicity. The reason, boundary and count fields 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, and it answers for type declarations only. EXECUTING EVIDENCE FOR THIS HEAD IS CI, STATED RATHER THAN IMPLIED. The nine claims were green at 1-3ms on the previous head. This head's run was refused locally by MemoryStallRefusedPageThrash -- the shared host had 9 GiB of 125 available and the whole-tree resolve thrashes rather than computing -- so the strengthened control has been executed against the OLD code and not yet against the new. CI is the consumer that settles it. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- .../keyed_declaration_read_seed_growth.dag | 29 ++++++++++++++++--- src/v2/std/node_reflection.dag | 2 +- ...coped_type_reflection_conformance_test.dag | 26 +++++++++++++++-- 3 files changed, 50 insertions(+), 7 deletions(-) diff --git a/dag/gunbc/keyed_declaration_read_seed_growth.dag b/dag/gunbc/keyed_declaration_read_seed_growth.dag index 82f1ceec9dc..b71dbf771d5 100644 --- a/dag/gunbc/keyed_declaration_read_seed_growth.dag +++ b/dag/gunbc/keyed_declaration_read_seed_growth.dag @@ -53,13 +53,34 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } // projects std.primitive_projection. Each was edited by hand in the same change as its authority // because the seed cannot build the emitter that regenerates it without them -- the ordinary // stage0 bootstrap seam, not new hand growth. +// A THIRD ITEM JOINED THIS RECEIPT LATER (gunbc#11291), and it is enumerated here rather than in a +// parallel justification because it is the same seam narrowed along a different key. +// eval_type_declarer_qualified_names is the BARE-NAME sibling of eval_decl_facts_at: same census, +// same decl_facts_for_roots_shared memo, same pool-root line-stop, same canonical order inherited +// rather than chosen. It exists because the keyed read already here CANNOT express its question -- +// decl_facts_at keys on a QUALIFIED name and a bare spelling has no module -- so the only substrate +// answer was to fold the whole declaration corpus once per call, measured at ~3.6s against ~1ms for +// the keyed read and sharing at no grain, four calls in one claim frame costing four times one. +// That is recorded as a third specimen on +// gunbc.recurring_failure_mode.shared_precondition_re_derived_once_per_claim_frame. +// +// ITS CORRECTNESS CONTENT IS THE SAME ONE THE ROW ABOVE NAMES, which is why it belongs beside it: +// it returns the MATCHING SET -- every qualified name declaring that bare spelling as a type -- and +// never a first hit, because multiplicity is the whole answer. A host that chose among candidates +// would be the bare-name identity defect its consumer exists to remove, one layer below the one +// being removed. Its consumer, v2.std.node_reflection resolve_type_node, refuses typed and located +// on multiplicity and names its candidates from what this returns. +// +// It marshals no declaration nodes, which is where the population read's cost actually lived; it is +// therefore cheaper than eval_decl_facts_at rather than merely narrower. data keyed_declaration_read_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification { hand_authored_declarations: [ DeclarationRef { module_path: "v1_compiler.coproduct_reflection", decl_name: "eval_decl_facts_at", field: WholeDeclaration }, - DeclarationRef { module_path: "v1_compiler.cli_run.entry_resolve", decl_name: "module_declaration_fact_at", field: WholeDeclaration } + DeclarationRef { module_path: "v1_compiler.cli_run.entry_resolve", decl_name: "module_declaration_fact_at", field: WholeDeclaration }, + DeclarationRef { module_path: "v1_compiler.coproduct_reflection", decl_name: "eval_type_declarer_qualified_names", field: WholeDeclaration } ], - reason: "A keyed read of a host census is a property of the host that holds it. Both items are the keyed projection of a population read that already exists beside them, and each is its own item because each answers for a different census: eval_decl_facts_at over the declaration facts, module_declaration_fact_at over the module-path index.\n\nTHE RETURN SHAPE IS THE CORRECTNESS CONTENT. eval_decl_facts_at returns the MATCHING SET rather than a bool or a first hit, because multiplicity is what DeclarationRefAmbiguous is derived from -- 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, and it is the reason this item is enumerated rather than treated as an inlined filter. module_declaration_fact_at returns an Option because the two questions a keyed caller asks -- is this module declared, and at which path -- are one lookup, and answering only the first would send the second back through the population read.\n\nEXECUTING EVIDENCE, not a shape argument: test.claim.decl_ref_keyed_read_agreement_witness_test asks one reference BOTH ways over one pool and requires the two feeds to land on the same arm AND names which arm, across all five, with the ambiguous arm reached at multiplicity two from a real duplicate-qualified-name fixture pool rather than a synthesized fact list.\n\nENUMERATED RATHER THAN COUNTED. Both are free functions, so the citable count and the real count are both two; nothing lands in seed_growth_uncitable_item_keys. The interpreter arms and the modified existing items are disclosed in this file's header instead.", + reason: "A keyed read of a host census is a property of the host that holds it. Both items are the keyed projection of a population read that already exists beside them, and each is its own item because each answers for a different census: eval_decl_facts_at over the declaration facts, module_declaration_fact_at over the module-path index.\n\nTHE RETURN SHAPE IS THE CORRECTNESS CONTENT. eval_decl_facts_at returns the MATCHING SET rather than a bool or a first hit, because multiplicity is what DeclarationRefAmbiguous is derived from -- 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, and it is the reason this item is enumerated rather than treated as an inlined filter. module_declaration_fact_at returns an Option because the two questions a keyed caller asks -- is this module declared, and at which path -- are one lookup, and answering only the first would send the second back through the population read.\n\nEXECUTING EVIDENCE, not a shape argument: test.claim.decl_ref_keyed_read_agreement_witness_test asks one reference BOTH ways over one pool and requires the two feeds to land on the same arm AND names which arm, across all five, with the ambiguous arm reached at multiplicity two from a real duplicate-qualified-name fixture pool rather than a synthesized fact list.\n\nENUMERATED RATHER THAN COUNTED. All three are free functions, so the citable count and the real count are both three; nothing lands in seed_growth_uncitable_item_keys. The interpreter arms and the modified existing items are disclosed in this file's header instead.\n\nTHE THIRD ITEM, eval_type_declarer_qualified_names, is the bare-name sibling of eval_decl_facts_at over the SAME census and the same memo, added because a qualified key cannot express bare-name multiplicity. It carries the same return-shape law for the same reason: it answers with every qualified name declaring the spelling as a type, so its consumer can refuse on multiplicity and name its candidates, and the host never picks among them. The header records the measurement that admitted it.", owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId, - trigger: "Delete both when the declaration census is a MODELED operation over a modeled prepared inventory rather than a host walk -- at which point a keyed read of it is an ordinary modeled query over a modeled collection and needs no host producer at all. This receipt dissolves with gunbc.decl_facts_shared_memo_seed_growth and gunbc.census_memo_seed_growth and not before: they are one seam, and retiring the memo while its keyed reader stayed hand-written would leave the reader keyed on a population nothing models.", - current_boundary: "Two pure functions of their declared arguments, each reading one already-built artifact and holding nothing. eval_decl_facts_at consults decl_facts_for_roots_shared -- the same census, the same canonical key over the pool-root multiset, the same shared-artifact fill accounting -- and filters DeclFactRaw rows on exact qualified_name equality, which is the law v2.std.decl_facts_skeleton decl_facts_matching_qualified_name already carries on the interpreted side; it therefore inherits the population read's CanonicalOrder rather than choosing one, because a filter cannot reorder what it does not rebuild. module_declaration_fact_at reads build_module_path_index, which was already process-cached before this change. Neither adds state, and neither can answer where the population read refuses: the pool-root defect line-stop fires first in both, against the DECLARED roots, because an empty keyed answer is exactly what a genuine miss looks like and the two must stay distinguishable. What they do NOT bound is the demand: a fold over N citations makes N keyed calls, so the census provider must retain across them, which is why claim_batch registers the census for its invocation and why gunbc run -- whose dispatch diverges and so cannot clear -- is deliberately left unregistered with no keyed consumer reached through it." + trigger: "Delete all three when the declaration census is a MODELED operation over a modeled prepared inventory rather than a host walk -- at which point a keyed read of it is an ordinary modeled query over a modeled collection and needs no host producer at all. This receipt dissolves with gunbc.decl_facts_shared_memo_seed_growth and gunbc.census_memo_seed_growth and not before: they are one seam, and retiring the memo while its keyed reader stayed hand-written would leave the reader keyed on a population nothing models.", + current_boundary: "Three pure functions of their declared arguments, each reading one already-built artifact and holding nothing. eval_decl_facts_at consults decl_facts_for_roots_shared -- the same census, the same canonical key over the pool-root multiset, the same shared-artifact fill accounting -- and filters DeclFactRaw rows on exact qualified_name equality, which is the law v2.std.decl_facts_skeleton decl_facts_matching_qualified_name already carries on the interpreted side; it therefore inherits the population read's CanonicalOrder rather than choosing one, because a filter cannot reorder what it does not rebuild. module_declaration_fact_at reads build_module_path_index, which was already process-cached before this change. Neither adds state, and neither can answer where the population read refuses: the pool-root defect line-stop fires first in both, against the DECLARED roots, because an empty keyed answer is exactly what a genuine miss looks like and the two must stay distinguishable. What they do NOT bound is the demand: a fold over N citations makes N keyed calls, so the census provider must retain across them, which is why claim_batch registers the census for its invocation and why gunbc run -- whose dispatch diverges and so cannot clear -- is deliberately left unregistered with no keyed consumer reached through it.\n\neval_type_declarer_qualified_names sits inside every sentence above with one narrowing and one widening. It consults the same decl_facts_for_roots_shared census under the same canonical key and the same pool-root line-stop, and it filters DeclFactRaw on exact bare-name equality AND TypeItem kind rather than on qualified_name -- a different key over the same rows, not a different census. The widening is that it does NOT reach eval_decl_facts_rows at all: it marshals no declaration nodes and returns only qualified-name strings, so it is strictly cheaper than the row it is keyed beside and cannot inherit a marshalling defect from it. The narrowing is that it answers for TYPE declarations only, because that is the question its consumer asks; a caller wanting another kind would need its own key rather than a widened arm here." } diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index 964fcbcd7df..169b5c7dd32 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -140,7 +140,7 @@ fn accept_sole_declaration( ) HeadFound { value: sole } => if node_is_coproduct(node: sole.node) { - outcome_accepted(value: resolve_type_node(type_name: type_name)) + outcome_accepted(value: sole.node) } else { outcome_rejected( d: scoped_type_reflection_diagnostic( diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag index 89602a8d774..0b92a02c9ff 100644 --- a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -1,7 +1,9 @@ module v2.test.manual.scoped_type_reflection_conformance import std.decl_ref { DeclarationRef, WholeDeclaration } +import v2.std.algebra { any, for_all, length } import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.node { Symbol } import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } import v2.std.node_reflection { coproduct_arm_keys_checked, @@ -60,12 +62,32 @@ test fn ambiguous_type_spelling_refuses_at_the_node_route_too() -> Bool { // everything. `Connective` is declared once in this pool, so the guard must let it through and // the arm keys must still come back. A guard that refused here would pass the two claims above // while destroying the surface, which is why this claim is enrolled beside them and not after. +// +// IT ASSERTS THE ANSWER AND NOT MERELY THE ARM, because review 65601 showed why that distinction +// is load-bearing here. An accepted Outcome says the guard let the call through; it says nothing +// about WHICH declaration produced the Node, and the whole defect this module exists to close is a +// seam that answers from the wrong declaration. So the control names the arm keys `Connective` +// actually declares. A route that resolved some other same-named type, or handed back a node of +// the wrong shape, would still be Accepted and would fail here. +fn outcome_arm_keys_are(o: Outcome>, expected: List) -> Bool { + match o { + Accepted { value: keys, diagnostics: _ } => + length(xs: keys) == length(xs: expected) + && for_all( + xs: expected, + predicate: fn(k) { any(xs: keys, predicate: fn(got) { got == k }) } + ) + Rejected { diagnostics: _ } => false + } +} + test fn unique_type_spelling_still_resolves() -> Bool { - outcome_is_accepted( + outcome_arm_keys_are( o: coproduct_arm_keys_checked( pool_roots: scoped_reflection_pool_roots, type_name: ^Connective - ) + ), + expected: [^Atom, ^Conj, ^Disj, ^Arrow, ^Cardinality, ^Instantiation] ) } From 29632d7fc7c24c751dacd4297aaee33e21957fce Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 20:29:32 +0000 Subject: [PATCH 06/16] Let a citation resolve a forked spelling, and stop enrolling the over-refusal review 65649, and it caught a prohibition that outlived its own premise by one commit -- mine. WHAT WAS WRONG. resolve_type_node_at required the BARE spelling to be globally unique before it would resolve a CITED declaration, and refused otherwise on an invariant naming the bare host seam. That 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 any more, a qualified key is exact, and a cited type whose spelling is forked is perfectly resolvable. The conjunct forbade more than the evidence supported (DESIGN section 4d), and the invariant symbol it refused with asserted a reachability fact that was false of the code beside it. The citation route now asks only whether the cited name resolves. It is the route that can ANSWER what the spelling route can only refuse, which is the single reason it exists; the old conjunct made it unable to serve that case at all. THE WITNESS HAD ENROLLED THE OVER-REFUSAL AS REQUIRED BEHAVIOUR, which is the worse half: cited_ambiguous_type_refuses_until_the_seam_is_scope_carrying asserted the refusal, and its annotation restated a delegation the previous commit had already deleted. A claim that pins stale behaviour does not merely fail to catch a defect, it defends one. It is 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, so the two new claims require the cited route to return exactly the arms of the module NAMED -- TermChain/TypeForest/ ImportGraph/DeclForest for one, TwosComplement/OnesComplement/SignMagnitude for the other. They assert the arm keys and not mere acceptance, so a route that resolved through load order would still be Accepted and would still fail here. The bare route's refusal on the same spelling is retained beside them, so the pair states the actual law: a bare spelling cannot say which declaration was meant, and 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 -- no second arm-key law. 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-2ms, including the nine from the previous head re-run against sole.node -- which closes the gap that head's commit message flagged, where local execution had been refused by host memory pressure. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- src/v2/std/node_reflection.dag | 54 +++++++++++++------ ...coped_type_reflection_conformance_test.dag | 41 ++++++++++---- 2 files changed, 70 insertions(+), 25 deletions(-) diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index 169b5c7dd32..b495a73543b 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -205,12 +205,41 @@ fn coproduct_arm_keys_checked( ) } -// THE ROUTE THAT MAKES A CALLER SAY WHICH MODULE IT MEANT. `resolve_type_node_checked` refuses an -// ambiguous spelling but cannot resolve one; a caller that legitimately means one of several -// same-spelled types names it by citation instead, reusing `std.decl_ref` DeclarationRef -- the -// corpus's existing carrier for "this declaration, in this module" -- so no second spelling of a +// THE ARM-KEY READING OF THE CITATION ROUTE, declared because the spelling route has one and a +// caller that cites its module needs the same answer shape. 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 -- no second arm-key law. +// Consumer: the conformance claims in v2.test.manual.scoped_type_reflection_conformance that read +// a forked spelling through each of its declaring modules. +fn coproduct_arm_keys_at( + pool_roots: List, + ref: DeclarationRef +) -> Outcome> { + bind_outcome( + o: resolve_type_node_at(pool_roots: pool_roots, ref: ref), + f: fn(node) { + outcome_accepted(value: coproduct_arm_key_list_from_node(node: node)) + } + ) +} + +// THE ROUTE THAT MAKES A CALLER SAY WHICH MODULE IT MEANT, and the one that can RESOLVE what the +// spelling route can only refuse. `resolve_type_node_checked` refuses an ambiguous spelling because +// a bare name does not say which declaration was meant; a caller that legitimately means one of +// several same-spelled types names it by citation instead, reusing `std.decl_ref` DeclarationRef -- +// the corpus's existing carrier for "this declaration, in this module" -- so no second spelling of a // scoped type identity is minted here. When PR #11264 lands its occurrence bindings, this is the // declaration whose parameter becomes that binding: the citation is refined in place, not forked. +// +// IT ASKS ONLY WHETHER THE CITED NAME RESOLVES, and review 65649 is why that is worth stating. An +// earlier revision also required the BARE spelling to be globally unique, and refused otherwise on +// an invariant naming the bare host seam. That prohibition was true when the accept path still +// delegated to the seam, which could not be told which module to read -- and it outlived its own +// premise by one commit: once `accept_sole_declaration` began returning the node the KEYED read +// already carries, nothing in this module consults load order, so a qualified key is exact and a +// cited type in a forked spelling is perfectly resolvable. Keeping the conjunct would have forbidden +// more than the evidence supports (DESIGN section 4d) and would have made the citation route unable +// to serve the only case it exists for. fn resolve_type_node_at(pool_roots: List, ref: DeclarationRef) -> Outcome { let wanted = logical_qualified_name_from_module( module_name: ref.module_path as String, @@ -219,13 +248,7 @@ fn resolve_type_node_at(pool_roots: List, ref: DeclarationRef) -> Outcom let type_name = symbol_intern_lexeme(lexeme: ref.decl_name as String) let candidates = type_declarer_names(pool_roots: pool_roots, type_name: type_name) let scoped = filter(xs: candidates, predicate: fn(qn) { qn == wanted }) - if length(xs: scoped) == 1 && length(xs: candidates) == 1 { - accept_sole_declaration( - pool_roots: pool_roots, - type_name: type_name, - sole_qualified_name: wanted - ) - } else if length(xs: scoped) == 0 { + if length(xs: scoped) == 0 { outcome_rejected( d: scoped_type_reflection_diagnostic( type_name: type_name, @@ -233,11 +256,10 @@ fn resolve_type_node_at(pool_roots: List, ref: DeclarationRef) -> Outcom ) ) } else { - outcome_rejected( - d: scoped_type_reflection_diagnostic( - type_name: type_name, - invariant: ^cited_type_unreachable_through_bare_host_seam - ) + accept_sole_declaration( + pool_roots: pool_roots, + type_name: type_name, + sole_qualified_name: wanted ) } } diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag index 0b92a02c9ff..12a9fb6608b 100644 --- a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -6,6 +6,7 @@ import v2.std.diagnostic { Accepted, Outcome, Rejected } import v2.std.node { Symbol } import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } import v2.std.node_reflection { + coproduct_arm_keys_at, coproduct_arm_keys_checked, resolve_type_node_at, resolve_type_node_checked @@ -102,11 +103,8 @@ test fn absent_type_spelling_refuses() -> Bool { ) } -// THE CITATION ROUTE. Naming the module resolves a unique spelling; it does NOT yet rescue an -// ambiguous one, because the bare host seam it delegates to cannot be told which module to read -// -- so that case refuses too, and says so on its own arm rather than guessing. Shrinking that -// refusal is what consuming #11264's occurrence binding buys, and this claim is where the change -// will show. +// THE CITATION ROUTE, AND THE CLAIM THAT SAYS WHAT IT IS FOR. Naming the module resolves the cited +// declaration whether or not the bare spelling is forked -- that is the whole point of citing one. test fn cited_unique_type_resolves_through_its_module() -> Bool { outcome_is_accepted( o: resolve_type_node_at( @@ -120,16 +118,41 @@ test fn cited_unique_type_resolves_through_its_module() -> Bool { ) } -test fn cited_ambiguous_type_refuses_until_the_seam_is_scope_carrying() -> Bool { - outcome_is_rejected( - o: resolve_type_node_at( +// THE DISCRIMINATING PAIR, AND IT IS 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 bare +// route must refuse it -- no bare spelling can say which was meant -- and the cited route must +// resolve it to exactly the arms of the module named, not to the other module's. Asserting the ARM +// KEYS rather than mere acceptance is what makes this a test of the answer: a citation route that +// resolved through load order would still be Accepted here and would return the wrong arm set. +// +// This claim previously asserted the opposite -- that the cited route REFUSES -- which enrolled an +// over-refusal as required behaviour (review 65649). It was true of an earlier revision whose accept +// path still delegated to the bare host seam, and it outlived that premise by one commit. +test fn cited_forked_spelling_resolves_to_the_module_named() -> Bool { + outcome_arm_keys_are( + o: coproduct_arm_keys_at( pool_roots: scoped_reflection_pool_roots, ref: DeclarationRef { module_path: "v2.std.integer", decl_name: "Representation", field: WholeDeclaration } - ) + ), + expected: [^TwosComplement, ^OnesComplement, ^SignMagnitude] + ) +} + +test fn cited_forked_spelling_resolves_to_the_other_module_named() -> Bool { + outcome_arm_keys_are( + o: coproduct_arm_keys_at( + pool_roots: scoped_reflection_pool_roots, + ref: DeclarationRef { + module_path: "v2.lens.intent_linearity", + decl_name: "Representation", + field: WholeDeclaration + } + ), + expected: [^TermChain, ^TypeForest, ^ImportGraph, ^DeclForest] ) } From 77391a574ad92f07e414a289f42c005eee46a66d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 20:52:03 +0000 Subject: [PATCH 07/16] Cut the affected-set lens onto the guarded reflection route The first consumer moves off the bare seam. v2.lens.affected_set read three type declarations by BARE SPELLING -- Gate, MetaProcessKind, RepoProcessKind -- through a seam that answers a forked spelling from whichever module the interpreter's load order reached first, silently. This lens then consumed that answer AS THE PROCESS UNIVERSE, which is the worst possible consumer for a silently wrong arm set. THE REFUSAL LANDS IN VOCABULARY THE LENS ALREADY OWNS. RepoProcessUniverse has UniverseIncomplete carrying a FailClosedReason, and FailClosedReason has ReasonDiagnostics over NonEmptyDiagnostics -- so a guard refusal maps onto an arm designed for exactly "the universe could not be established", with no Outcome plumbing at that seam and no new vocabulary. Each refusal arm names which reflection read refused in uncovered_kind, so the diagnostic locates the unanswerable spelling rather than reporting the universe merely unavailable. A REFUSED READ IS NOT AN EMPTY ONE, and that distinction is why the fold threads Outcomes rather than lists. An empty process list is a legitimate answer meaning the corpus declares no such process; a refusal means the question was never settled. Collapsing the second into the first would build a confidently empty universe on an unanswered question -- the widening DESIGN section 5 forbids, and invisible, because UniverseComplete with no processes typechecks. THE WITNESS NEEDED A CLAIM IT DID NOT HAVE. Its helper degrades a refusal to an empty list so the existing assertions keep their shape, and that is exactly what makes a corpus of total refusal look healthy: !identity_in over an empty list is true, so the negative half of affected_set_universe_includes_meta_self would pass with every read refusing. affected_set_universe_reflection_reads_resolve asserts the reads actually resolve, which is what makes the others mean what they say. ITS LIVE-TREE DISPOSITION CHANGED WITH THE CUTOVER and is corrected rather than left stale: the claims used to reach reflection through a seam taking only a bare spelling, so SubstrateInputsOnly was true; they now name pool roots and consult the live declaration index, so they read the live tree and say so. Five claims green by execution. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- src/v2/lens/affected_set.dag | 103 +++++++++++++++--- .../test/claim/affected_set_universe_test.dag | 64 +++++++++-- 2 files changed, 145 insertions(+), 22 deletions(-) diff --git a/src/v2/lens/affected_set.dag b/src/v2/lens/affected_set.dag index 5971963b20d..37b1064f74a 100644 --- a/src/v2/lens/affected_set.dag +++ b/src/v2/lens/affected_set.dag @@ -31,8 +31,10 @@ import v2.std.diagnostic { Accepted, None, Rejected, + bind_outcome, diagnostics_merge, - diagnostics_singleton + diagnostics_singleton, + outcome_accepted } import v2.std.node { Arrow, @@ -59,7 +61,7 @@ import v2.std.node { content_hash, } import v2.std.witness { Holds, Witness } -import v2.std.node_reflection { coproduct_arm_keys } +import v2.std.node_reflection { coproduct_arm_keys_checked } import v2.lens.application { AncestorFrame, AncestorWalk, collect_ancestor_frames, find_child_by_name, subterm_at, substitute_at } type Dag = Node @@ -1296,15 +1298,41 @@ data affected_set_reflect_gate_type: Symbol = ^Gate data affected_set_reflect_meta_process_kind_type: Symbol = ^MetaProcessKind data affected_set_reflect_repo_process_kind_type: Symbol = ^RepoProcessKind -fn ci_gate_processes() -> List { - coproduct_arm_keys(type_name: affected_set_reflect_gate_type) |> map(key => - RepoProcess { kind: CiGateProcess, identity: key } +// THE REFLECTION READS ARE NOW SCOPE-CARRYING AND CAN REFUSE, which is why each returns an Outcome +// rather than a bare list. They read type declarations by BARE SPELLING, and a bare spelling that +// two modules declare cannot say which was meant -- the seam used to answer such a spelling from +// whichever module the interpreter's load order reached first, silently, and this lens consumed +// that answer as the process universe. v2.std.node_reflection coproduct_arm_keys_checked refuses +// typed and located instead, so the refusal has to arrive somewhere, and RepoProcessUniverse +// already owns the vocabulary for it: UniverseIncomplete carrying a FailClosedReason. +fn reflected_processes( + pool_roots: List, + type_name: Symbol, + kind: RepoProcessKind +) -> Outcome> { + bind_outcome( + o: coproduct_arm_keys_checked(pool_roots: pool_roots, type_name: type_name), + f: fn(keys) { + outcome_accepted( + value: keys |> map(key => RepoProcess { kind: kind, identity: key }) + ) + } ) } -fn meta_processes() -> List { - coproduct_arm_keys(type_name: affected_set_reflect_meta_process_kind_type) |> map(key => - RepoProcess { kind: MetaProcessRole, identity: key } +fn ci_gate_processes(pool_roots: List) -> Outcome> { + reflected_processes( + pool_roots: pool_roots, + type_name: affected_set_reflect_gate_type, + kind: CiGateProcess + ) +} + +fn meta_processes(pool_roots: List) -> Outcome> { + reflected_processes( + pool_roots: pool_roots, + type_name: affected_set_reflect_meta_process_kind_type, + kind: MetaProcessRole ) } @@ -1314,9 +1342,12 @@ fn universe_has_process_of_kind(processes: List, kind_key: Symbol) }) } -fn repo_process_universe_from(processes: List) -> RepoProcessUniverse { +fn repo_process_universe_from_kinds( + processes: List, + kind_keys: List +) -> RepoProcessUniverse { fold( - coproduct_arm_keys(type_name: affected_set_reflect_repo_process_kind_type), + kind_keys, init: UniverseComplete { processes: processes }, f: fn(acc, kind_key) { match acc { @@ -1336,10 +1367,54 @@ fn repo_process_universe_from(processes: List) -> RepoProcessUniver ) } -fn repo_process_universe() -> RepoProcessUniverse { - repo_process_universe_from( - processes: list_append(left: ci_gate_processes(), right: meta_processes()) - ) +// A REFUSED REFLECTION READ IS AN INCOMPLETE UNIVERSE, not an empty one, and the distinction is the +// whole reason this fold threads Outcomes rather than lists. An empty process list is a legitimate +// answer meaning the corpus declares no such process; a refusal means the question could not be +// answered at all. Collapsing the second into the first would hand this lens a confidently empty +// universe built on a question that was never settled -- which is the widening DESIGN section 5 +// forbids, and it would be invisible because UniverseComplete with no processes typechecks. +// +// The uncovered_kind on each refusal arm names WHICH reflection read refused, so the diagnostic +// locates the unanswerable spelling rather than reporting that the universe is merely unavailable. +fn repo_process_universe_from( + pool_roots: List, + processes: List +) -> RepoProcessUniverse { + match coproduct_arm_keys_checked( + pool_roots: pool_roots, + type_name: affected_set_reflect_repo_process_kind_type + ) { + Rejected { diagnostics: d } => + UniverseIncomplete { + uncovered_kind: affected_set_reflect_repo_process_kind_type, + reason: ReasonDiagnostics { diagnostics: d } + } + Accepted { value: kind_keys, diagnostics: _ } => + repo_process_universe_from_kinds(processes: processes, kind_keys: kind_keys) + } +} + +fn repo_process_universe(pool_roots: List) -> RepoProcessUniverse { + match ci_gate_processes(pool_roots: pool_roots) { + Rejected { diagnostics: d } => + UniverseIncomplete { + uncovered_kind: affected_set_reflect_gate_type, + reason: ReasonDiagnostics { diagnostics: d } + } + Accepted { value: gates, diagnostics: _ } => + match meta_processes(pool_roots: pool_roots) { + Rejected { diagnostics: d } => + UniverseIncomplete { + uncovered_kind: affected_set_reflect_meta_process_kind_type, + reason: ReasonDiagnostics { diagnostics: d } + } + Accepted { value: metas, diagnostics: _ } => + repo_process_universe_from( + pool_roots: pool_roots, + processes: list_append(left: gates, right: metas) + ) + } + } } data construction_justification: ConstructionJustification = ConstructionJustification { diff --git a/src/v2/test/claim/affected_set_universe_test.dag b/src/v2/test/claim/affected_set_universe_test.dag index 1485c20aa86..7e2de20668b 100644 --- a/src/v2/test/claim/affected_set_universe_test.dag +++ b/src/v2/test/claim/affected_set_universe_test.dag @@ -4,6 +4,7 @@ import v2.std.logic { Bool } import v2.std.collection { List } import v2.std.node { Symbol } import v2.std.algebra { bag_eq } +import v2.std.diagnostic { Accepted, Outcome, Rejected } import v2.lens.affected_set { RepoProcess, RepoProcessUniverse, @@ -19,9 +20,14 @@ import gunbc.ci_spec { gunbc_ci_gates, gunbc_ci_falsifier_gates } -import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly +// THE DISPOSITION CHANGED WITH THE CUTOVER, and it is a fact about this module rather than a +// formality. These claims used to reach reflection through a seam that took only a bare spelling, +// so nothing they called named a source population and SubstrateInputsOnly was true. The reads are +// now scope-carrying: they name pool roots and consult the live declaration index through +// v2.std.decl_index, so the claims read the live tree and say so. +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree fn symbol_eq(a: Symbol, b: Symbol) -> Bool { a == b @@ -39,9 +45,33 @@ fn identity_in(ps: List, sym: Symbol) -> Bool { fold(ps, init: false, f: fn(acc, p) { acc || (p.identity == sym) }) } +// THE ROOTS THIS LENS READS, named because the reflection reads are now scope-carrying and a +// population the claim does not state is one a reader cannot re-derive. +data affected_set_universe_pool_roots: List = ["dag", "src/v2"] + + +// A REFUSED READ IS NOT AN EMPTY ONE. These claims previously consumed bare lists; the reads can now +// refuse, so each unwraps explicitly and a refusal fails the claim rather than degrading to an empty +// process set that would satisfy several of the assertions below by vacuity. +fn processes_or_empty(o: Outcome>) -> List { + match o { + Accepted { value: ps, diagnostics: _ } => ps + Rejected { diagnostics: _ } => [] + } +} + +fn read_refused(o: Outcome>) -> Bool { + match o { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } +} + test fn affected_set_universe_gate_processes_match_declared_gates() -> Bool { bag_eq( - xs: process_identities(ps: ci_gate_processes()), + xs: process_identities( + ps: processes_or_empty(o: ci_gate_processes(pool_roots: affected_set_universe_pool_roots)) + ), ys: gate_discriminants( gates: concat(gunbc_ci_gates, gunbc_ci_falsifier_gates) ), @@ -50,20 +80,38 @@ test fn affected_set_universe_gate_processes_match_declared_gates() -> Bool { } test fn affected_set_universe_includes_meta_self() -> Bool { - identity_in(ps: meta_processes(), sym: ^AffectedSetLens) - && identity_in(ps: meta_processes(), sym: ^TestgenLens) - && !identity_in(ps: meta_processes(), sym: ^NotARealMetaProcess) + let metas = processes_or_empty( + o: meta_processes(pool_roots: affected_set_universe_pool_roots) + ) + identity_in(ps: metas, sym: ^AffectedSetLens) + && identity_in(ps: metas, sym: ^TestgenLens) + && !identity_in(ps: metas, sym: ^NotARealMetaProcess) +} + +// THE READS MUST ACTUALLY RESOLVE, asserted separately because processes_or_empty deliberately +// degrades a refusal to an empty list for the assertions above. Without this claim a corpus in +// which every reflection read refused would still satisfy the negative half of the claim above -- +// !identity_in over an empty list is true -- so the refusal would be invisible exactly where it +// matters most. This is the claim that makes the others mean what they say. +test fn affected_set_universe_reflection_reads_resolve() -> Bool { + !read_refused(o: ci_gate_processes(pool_roots: affected_set_universe_pool_roots)) + && !read_refused(o: meta_processes(pool_roots: affected_set_universe_pool_roots)) } test fn affected_set_universe_is_complete() -> Bool { - match repo_process_universe() { + match repo_process_universe(pool_roots: affected_set_universe_pool_roots) { UniverseComplete { processes: _ } => true UniverseIncomplete { uncovered_kind: _, reason: _ } => false } } test fn affected_set_universe_incomplete_fails_closed() -> Bool { - match repo_process_universe_from(processes: ci_gate_processes()) { + match repo_process_universe_from( + pool_roots: affected_set_universe_pool_roots, + processes: processes_or_empty( + o: ci_gate_processes(pool_roots: affected_set_universe_pool_roots) + ) + ) { UniverseComplete { processes: _ } => false UniverseIncomplete { uncovered_kind: k, reason: _ } => k == ^MetaProcessRole } From 002f3030b3920d8d5dae50994711b282759bff43 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 21:34:22 +0000 Subject: [PATCH 08/16] Move the last consumers off the bare seam, and refuse ambiguity at the qualified grain too TWO THINGS, and the second is a defect the first would have hidden. THE REMAINING CONSUMERS ARE CUT OVER. coproduct_exhaustiveness, cross_representation_equality, the wiring-liveness entry and the reflection conformance witness all read type declarations by bare spelling through the unguarded seam; all four now name pool roots and go through the guarded route, and each handles refusal explicitly rather than flattening it. No .dag consumer of the bare pair remains. Each refusal is handled where the two states actually differ. A refused read is not an empty arm set and not an unreachable field: in the exhaustiveness roster a refusal fails coverage rather than reading as zero arms; in the wiring entry it fails the claim rather than presenting an empty tree that would make every input read as unwired. UriScheme IS WHERE THE CUTOVER SHOWS ITS TEETH. It is a coproduct in extdeps.uri and a RECORD in v2.std.network, so the guarded bare route refuses it -- correctly. Its two enrolled claims had been consuming whatever load order returned while believing they were reading extdeps.uri, which is the defect, not a casualty of the fix. They now CITE the module, which is the only way to ask what they were always asking. THE LIVE-TREE DISPOSITIONS ARE CORRECTED, not left stale. Three entries declared SubstrateInputsOnly and now consult the live declaration index. v2.std.live_tree states that a row declaring SubstrateInputsOnly while reading live state is re-checked by NOTHING, so a stale row is a lie no consumer would catch -- which makes correcting it part of the change rather than tidying after it. review 65678: THE CITATION ROUTE STILL TOOK A FIRST MATCH, one grain down. Removing the bare-uniqueness conjunct was right; leaving ZERO as its only refusal was not, because every non-zero multiplicity then reached an accept path that takes the HEAD of the keyed read. Two declarations under one LOGICAL qualified name would have been answered from whichever row came first, with no diagnostic -- the same shape this module exists to close, moved from bare spelling to qualified name. This PR's own seed-growth receipt states the law it broke: two rows under one logical qualified name is an ambiguous citation, and collapsing it silently RESOLVES one, which is a wrong answer and not a cost defect. It now refuses. ITS RED IS AUTHORABLE FROM THE REAL CORPUS, which is the part worth recording, because the obvious reading is that one module cannot declare one name twice and the state is therefore unconstructible. 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. Eighteen such names across twelve colliding module pairs, so the enrolled claim cites a live state rather than a fixture. Eleven claims green by execution. NOT VERIFIED BY EXECUTION, stated rather than left for a reviewer: the wiring-liveness entry does not resolve, with 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 -- so the cutover there is compiled but unexecuted, and that entry's claims were already unobservable on this branch. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- src/v2/std/node_reflection.dag | 16 +++++ .../generated/coproduct_exhaustiveness.dag | 21 +++++-- .../cross_representation_equality.dag | 13 ++++- .../coproduct_reflection_conformance_test.dag | 58 ++++++++++++++++--- ...coped_type_reflection_conformance_test.dag | 25 ++++++++ .../wiring_liveness_test.dag | 36 ++++++++++-- 6 files changed, 149 insertions(+), 20 deletions(-) diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index b495a73543b..7ba41a99ce5 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -231,6 +231,15 @@ fn coproduct_arm_keys_at( // scoped type identity is minted here. When PR #11264 lands its occurrence bindings, this is the // declaration whose parameter becomes that binding: the citation is refined in place, not forked. // +// IT REFUSES MULTIPLICITY AT ITS OWN GRAIN TOO, which review 65678 caught me missing. Removing the +// bare-uniqueness conjunct was right; leaving the ZERO case as the only refusal was not, because it +// sent every non-zero multiplicity into the accept path, and that path takes the head of the keyed +// read. Two declarations under ONE logical qualified name would then have been answered from +// whichever row came first -- the same first-match-without-a-diagnostic shape this module exists to +// close, moved one grain down from bare spelling to qualified name. This module's own seed-growth +// receipt states the law that forbids it: two rows under one logical qualified name is an ambiguous +// citation, and collapsing it silently RESOLVES one, which is a wrong answer and not a cost defect. +// // IT ASKS ONLY WHETHER THE CITED NAME RESOLVES, and review 65649 is why that is worth stating. An // earlier revision also required the BARE spelling to be globally unique, and refused otherwise on // an invariant naming the bare host seam. That prohibition was true when the accept path still @@ -255,6 +264,13 @@ fn resolve_type_node_at(pool_roots: List, ref: DeclarationRef) -> Outcom invariant: ^cited_type_declaration_absent ) ) + } else if length(xs: scoped) > 1 { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^cited_type_qualified_name_ambiguous + ) + ) } else { accept_sole_declaration( pool_roots: pool_roots, diff --git a/src/v2/test/claim/generated/coproduct_exhaustiveness.dag b/src/v2/test/claim/generated/coproduct_exhaustiveness.dag index fed1a18f749..6200d0d8239 100644 --- a/src/v2/test/claim/generated/coproduct_exhaustiveness.dag +++ b/src/v2/test/claim/generated/coproduct_exhaustiveness.dag @@ -13,7 +13,10 @@ import v2.std.collection { List } import v2.std.diagnostic { Accepted, None, Outcome, Rejected } import v2.std.logic { Bool } import v2.std.node { Node, Symbol } -import v2.std.node_reflection { coproduct_arm_keys } +import v2.std.node_reflection { coproduct_arm_keys_checked } + +// THE ROOTS THE REFLECTION READS CONSULT, named so the population is re-derivable. +data coproduct_exhaustiveness_pool_roots: List = ["dag", "src/v2"] import v2.std.verification { ClaimAnchorKey, DiagnosticClaim, @@ -100,17 +103,27 @@ fn roster_covers_arms( } } +// THE READ IS NOW SCOPE-CARRYING AND CAN REFUSE. A refusal fails this claim rather than reading as +// zero arms, which it would have done if the Outcome were flattened to an empty list -- and the +// `length(arms) > 0` conjunct below would then have caught it only by accident. The refusal arm is +// explicit so the two states stay distinguishable: a spelling no module declares, and a spelling +// two modules declare, are both unanswerable here and neither is "covered". fn roster_covers_all_arms_of_roster( + pool_roots: List, gens: List>, coproduct_type: Symbol ) -> Bool { - let arms = coproduct_arm_keys(type_name: coproduct_type) - (length(xs: arms) > 0) - && roster_covers_arms(gens: gens, coproduct_type: coproduct_type, arms: arms) + match coproduct_arm_keys_checked(pool_roots: pool_roots, type_name: coproduct_type) { + Rejected { diagnostics: _ } => false + Accepted { value: arms, diagnostics: _ } => + (length(xs: arms) > 0) + && roster_covers_arms(gens: gens, coproduct_type: coproduct_type, arms: arms) + } } fn roster_covers_all_arms_of(coproduct_type: Symbol) -> Bool { roster_covers_all_arms_of_roster( + pool_roots: coproduct_exhaustiveness_pool_roots, gens: testgen_scheduled_coproduct_exhaustiveness_generators(), coproduct_type: coproduct_type ) diff --git a/src/v2/test/claim/generated/cross_representation_equality.dag b/src/v2/test/claim/generated/cross_representation_equality.dag index e82308e8865..8660d2d20d2 100644 --- a/src/v2/test/claim/generated/cross_representation_equality.dag +++ b/src/v2/test/claim/generated/cross_representation_equality.dag @@ -1,6 +1,9 @@ module v2.test.generated.cross_representation_equality -import v2.std.node_reflection { coproduct_arm_keys } +import v2.std.node_reflection { coproduct_arm_keys_checked } + +// THE ROOTS THE REFLECTION READ CONSULTS, named so the population is re-derivable. +data cross_representation_pool_roots: List = ["dag", "src/v2"] fn reference_cross_representation_equality_anchor() -> GeneratedAnchorKey { @@ -50,7 +53,13 @@ fn roster_covers_straddle(modeled: Symbol, native: Symbol) -> Bool { } fn roster_covers_genuine_straddle(modeled: Symbol, native: Symbol) -> Bool { - (length(xs: coproduct_arm_keys(type_name: modeled)) > 0) + (match coproduct_arm_keys_checked( + pool_roots: cross_representation_pool_roots, + type_name: modeled + ) { + Rejected { diagnostics: _ } => false + Accepted { value: arms, diagnostics: _ } => length(xs: arms) > 0 + }) && roster_covers_straddle(modeled: modeled, native: native) } diff --git a/src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag b/src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag index 62a5879790c..9bc55f8b7da 100644 --- a/src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag @@ -1,18 +1,48 @@ module v2.test.manual.coproduct_reflection_conformance +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + import extdeps.languages.rust.capabilities { RustCapability } import extdeps.uri { UriScheme, uri_scheme_inhabitants } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import v2.std.diagnostic { Accepted, Outcome, Rejected } import v2.std.node_reflection { - coproduct_arm_keys, + coproduct_arm_keys_at, + coproduct_arm_keys_checked, coproduct_nullary_inhabitants } import v2.test.fixture.coproduct_reflection_generic_wrapper { nullary_reflection_through_generic_wrapper } -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly +// READS THE LIVE TREE AS OF THE REFLECTION CUTOVER -- the reads name pool roots and consult the +// live declaration index. v2.std.live_tree records that a SubstrateInputsOnly row over a live read +// is re-checked by nothing, so a stale row here would be a lie no consumer would catch. +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THE ROOTS THE REFLECTION READS CONSULT, named so the population is re-derivable. +data reflection_conformance_pool_roots: List = ["dag", "src/v2"] + +// UriScheme IS A FORKED SPELLING AND THIS IS WHERE THE CUTOVER SHOWS. It is a closed coproduct in +// extdeps.uri and a RECORD in v2.std.network, so the guarded bare route REFUSES it -- correctly, +// because a bare spelling cannot say which of the two was meant. Before the cutover the seam +// answered it from whichever module load order reached first, and the two claims below consumed +// that answer while believing they were reading extdeps.uri. They now CITE the module, which is +// the only way to ask the question they were always asking. +data reflect_uri_scheme_ref: DeclarationRef = DeclarationRef { + module_path: "extdeps.uri", + decl_name: "UriScheme", + field: WholeDeclaration +} + +fn conformance_arm_keys_or_empty(o: Outcome>) -> List { + match o { + Accepted { value: keys, diagnostics: _ } => keys + Rejected { diagnostics: _ } => std.algebra.Empty + } +} data reflect_connective_type: Symbol = ^Connective data reflect_behavior_type: Symbol = ^Behavior @@ -69,7 +99,7 @@ test fn witness_nullary_reflection_accepts_imported_named_coproduct_through_gene Accepted { value: inhabitants, diagnostics: _ } => bag_eq( xs: imported_derive_trait_discriminants(inhabitants: inhabitants), - ys: coproduct_arm_keys(type_name: reflect_imported_derive_trait_type), + ys: conformance_arm_keys_or_empty(o: coproduct_arm_keys_checked(pool_roots: reflection_conformance_pool_roots, type_name: reflect_imported_derive_trait_type)), eq: symbol_eq ) Rejected { diagnostics: _ } => false @@ -102,8 +132,8 @@ test fn witness_nullary_reflection_rejects_requested_a_with_context_b() -> Bool test fn witness_connective_behavior_arm_sets_are_distinct() -> Bool { !bag_eq( - xs: coproduct_arm_keys(type_name: reflect_connective_type), - ys: coproduct_arm_keys(type_name: reflect_behavior_type), + xs: conformance_arm_keys_or_empty(o: coproduct_arm_keys_checked(pool_roots: reflection_conformance_pool_roots, type_name: reflect_connective_type)), + ys: conformance_arm_keys_or_empty(o: coproduct_arm_keys_checked(pool_roots: reflection_conformance_pool_roots, type_name: reflect_behavior_type)), eq: symbol_eq ) } @@ -135,7 +165,7 @@ test fn witness_behavior_nullary_inhabitant_set_matches_arm_keys() -> Bool { discriminant_of: behavior_discriminant ) { Accepted { value: inhabitants, diagnostics: _ } => - let keys = coproduct_arm_keys(type_name: reflect_behavior_type) + let keys = conformance_arm_keys_or_empty(o: coproduct_arm_keys_checked(pool_roots: reflection_conformance_pool_roots, type_name: reflect_behavior_type)) bag_eq( xs: nullary_inhabitant_discriminants(inhabitants: inhabitants), ys: keys, @@ -190,7 +220,12 @@ fn uri_scheme_roster_discriminants(inhabitants: List) -> List test fn witness_uri_scheme_declared_roster_matches_reflected_arm_keys() -> Bool { bag_eq( xs: uri_scheme_roster_discriminants(inhabitants: uri_scheme_inhabitants()), - ys: coproduct_arm_keys(type_name: reflect_uri_scheme_type), + ys: conformance_arm_keys_or_empty( + o: coproduct_arm_keys_at( + pool_roots: reflection_conformance_pool_roots, + ref: reflect_uri_scheme_ref + ) + ), eq: symbol_eq ) } @@ -199,5 +234,12 @@ test fn witness_uri_scheme_declared_roster_matches_reflected_arm_keys() -> Bool // reflection call that silently returned nothing -- the empty-observation narrow -- would // green the wall while checking nothing at all. test fn witness_uri_scheme_reflected_arm_keys_are_non_empty() -> Bool { - length(xs: coproduct_arm_keys(type_name: reflect_uri_scheme_type)) > 0 + length( + xs: conformance_arm_keys_or_empty( + o: coproduct_arm_keys_at( + pool_roots: reflection_conformance_pool_roots, + ref: reflect_uri_scheme_ref + ) + ) + ) > 0 } diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag index 12a9fb6608b..2a39c6e3b8c 100644 --- a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -208,3 +208,28 @@ test fn cited_unique_but_non_coproduct_spelling_refuses_rather_than_diverging() ) ) } + +// THE AMBIGUITY RED AT THE QUALIFIED GRAIN, which review 65678 found the claim family missing. +// Removing the bare-uniqueness conjunct from the citation route was right; leaving ZERO as its only +// refusal was not, because every non-zero multiplicity then reached an accept path that takes the +// HEAD of the keyed read -- first match without a diagnostic, one grain down from the bare spelling +// this module exists to fix. +// +// IT IS AUTHORABLE FROM THE REAL CORPUS, which is the part worth recording, because the obvious +// reading is that one module cannot declare one name twice and therefore the state is +// unconstructible. The collision is not within a module, it is BETWEEN two modules that share a +// LOGICAL qualified 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. Eighteen such +// names exist across twelve colliding module pairs, so this is a live state and not a fixture. +test fn cited_ambiguous_qualified_name_refuses_rather_than_taking_the_head() -> Bool { + outcome_is_rejected( + o: resolve_type_node_at( + pool_roots: scoped_reflection_pool_roots, + ref: DeclarationRef { + module_path: "v2.std.integer", + decl_name: "Int", + field: WholeDeclaration + } + ) + ) +} diff --git a/src/v2/test/lens_wiring_liveness/wiring_liveness_test.dag b/src/v2/test/lens_wiring_liveness/wiring_liveness_test.dag index 90d7ab358a2..c904eddf28f 100644 --- a/src/v2/test/lens_wiring_liveness/wiring_liveness_test.dag +++ b/src/v2/test/lens_wiring_liveness/wiring_liveness_test.dag @@ -1,9 +1,17 @@ module v2.test.lens_wiring_liveness.wiring_liveness_test -import v2.std.node_reflection { resolve_type_node } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } +import v2.std.diagnostic { Accepted, Outcome, Rejected } +import v2.std.node_reflection { resolve_type_node_checked } -data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// READS THE LIVE TREE AS OF THE REFLECTION CUTOVER. The reflection read now names pool roots and +// consults the live declaration index through v2.std.decl_index, so SubstrateInputsOnly became +// false for this entry. Correcting it is not a formality: v2.std.live_tree records that a row +// declaring SubstrateInputsOnly while actually reading live state is re-checked by NOTHING, so a +// stale row here would be a lie no consumer would catch. +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree fn wl_atom(identity: Symbol) -> Node { Node { @@ -55,8 +63,18 @@ test fn wiring_liveness_dead_input_is_unwired() -> Bool { ) == false } -fn wl_reflected_dependency_kind() -> Node { - resolve_type_node(type_name: ^DependencyKind) +// THE ROOTS THE REFLECTION READ CONSULTS, named so the population is re-derivable. +data wl_reflection_pool_roots: List = ["dag", "src/v2"] + +// THE READ CAN NOW REFUSE, and a refusal must not be silently substituted by an empty tree here: +// this function feeds a wiring walk, and an empty root would make every input read as unwired -- +// a confident false answer built on a question that was never settled. The refusal is surfaced as +// an Outcome and the caller decides, rather than being flattened at the read. +fn wl_reflected_dependency_kind() -> Outcome { + resolve_type_node_checked( + pool_roots: wl_reflection_pool_roots, + type_name: ^DependencyKind + ) } fn wl_edge_target(e: Edge) -> Node { @@ -70,7 +88,13 @@ fn wl_first_field_reachable(root: Node, edges: List) -> Bool { } } +// A REFUSED READ FAILS THIS CLAIM RATHER THAN READING AS AN UNREACHABLE FIELD. The two states are +// different facts -- the type could not be resolved, versus the type resolved and its first field +// is not reachable -- and only the second is what this claim is about. test fn wiring_liveness_real_reflected_type_field_reachable() -> Bool { - let root = wl_reflected_dependency_kind() - return wl_first_field_reachable(root: root, edges: node_labeled_child_edges(node: root)) + match wl_reflected_dependency_kind() { + Rejected { diagnostics: _ } => false + Accepted { value: root, diagnostics: _ } => + wl_first_field_reachable(root: root, edges: node_labeled_child_edges(node: root)) + } } From 8abfe895f5b81a62acaafa5e24e1f7c8494856c4 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 22:12:33 +0000 Subject: [PATCH 09/16] Delete the bare reflection seam: the first-match scan leaves the seed entirely THE ROOT CUTOVER COMPLETES BY DELETION RATHER THAN RENAME. With every consumer moved, v2.std.node_reflection resolve_type_node and coproduct_arm_keys had no caller left, so the whole first-match route is removed rather than kept alive under another name. A rename would have preserved a bare-spelling host route the next question could be answered in -- the surviving-X attractor DESIGN section 3 warns about -- and left an importable escape hatch after its consumers were gone, which is what review 65702 identified and DESIGN section 5 forbids outright. WHAT LEAVES, and it is a chain rather than a declaration. 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. Each had exactly one caller, so the whole chain died with the arm and the seed SHRINKS (DESIGN section 7) rather than growing a synonym. THE DELETION WAS THE CENSUS, exactly as DESIGN section 3 says it should be. Four dependents refused loudly rather than silently: the roster witness asserting the arm exists, which now names a surviving v4_bridge arm; the effect_demand seam row; this PR's own row in gunbc.bare_name_identity_consumer_census, whose site no longer exists, so the row is removed rather than left as a citation to a deleted declaration -- taking the stale call_site_count review 65702 also flagged; and the evidence list in gunbc.recurring_failure_mode host_seam_self_call_diverges_when_its_arm_is_absent, which counted this declaration among thirteen self-call seams. THAT LAST ONE IS ANOTHER LANE'S ROW AND IS TREATED AS SUCH. Its dangling citation is removed because my change invalidated it, and a receipt records that one member left by DELETION rather than by climbing -- so its stated denominator reads as correct-as-observed rather than current. Its census is not re-swept here: a lane that deletes one member is not entitled to restate another lane's count. THE MODULE ANNOTATION IS REWRITTEN TO MATCH THE TREE. It had classified the cutover as an open declared frontier whose trigger was a future move, and that sentence outlived the tree by one commit -- the cutover landed in this same change. Classifying a completed cutover as an open frontier is the wrong DESIGN section 3c arm, and it was being used to justify keeping the unguarded route importable. EVIDENCE: twelve claims green by execution with the seam gone, across all three families -- the scoped conformance claims including the qualified-grain ambiguity RED, the reflection conformance claims including both UriScheme citations, and the affected-set universe claims. The regeneration reaches a fixed point: main_wet re-emits no change to the generated dispatch beyond the hand-edit the stage0 bootstrap seam required to build the emitter that regenerates it. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- .../bare_name_identity_consumer_census.dag | 10 ---- ...f_call_diverges_when_its_arm_is_absent.dag | 3 +- .../v1/v1_interpreter_primitive_surface.dag | 9 --- dag/std/primitive_identity.dag | 13 ++--- dag/std/primitive_projection.dag | 2 - ...rpreter_primitive_surface_witness_test.dag | 2 +- src/v1/stage0/src/coproduct_reflection.rs | 40 -------------- src/v1/stage0/src/std_primitive_projection.rs | 15 ----- src/v1/stage0/src/v1_interpreter.rs | 2 - .../src/v1_interpreter_dispatch_generated.rs | 39 ++++++------- src/v2/compiler/effect_demand.dag | 7 --- src/v2/std/node_reflection.dag | 55 ++++++++++++------- 12 files changed, 59 insertions(+), 138 deletions(-) diff --git a/dag/gunbc/bare_name_identity_consumer_census.dag b/dag/gunbc/bare_name_identity_consumer_census.dag index 64ac49f51aa..5ed3583330e 100644 --- a/dag/gunbc/bare_name_identity_consumer_census.dag +++ b/dag/gunbc/bare_name_identity_consumer_census.dag @@ -226,16 +226,6 @@ data bare_name_identity_consumers: List = [ sibling: SiblingPresentButOrdered { sibling: decl_ref(module_path: "v1.compiler.infer_items", decl_name: "leaf_owner_modules_from_registry"), precedence: "the ambiguity arm runs INSTEAD of last-write-wins, which is the shape every row above is missing" }, call_site_count: 2, }, - { - site: decl_ref(module_path: "v2.std.node_reflection", decl_name: "resolve_type_node"), - fact_sought: "the declaration Node of the closed coproduct a type name denotes, which is what every arm-key and nullary-inhabitant answer is then read off", - keys_on: "a bare Symbol spelling and nothing else -- the seam's whole signature is the spelling, so the resolving scope is not an input the key can cover", - identity: AvailableUpstreamNotThreaded { nearest_holder: decl_ref(module_path: "v2.std.decl_ref_resolution", decl_name: "resolve_declaration_ref_live") }, - outcome: SilentWrongProviderAnswer { what_is_emitted: "the arm-key list of whichever declaration the interpreter's loaded-module order reached first, with nothing said about which. The mechanism is read from the host arm v4_bridge.resolve_type_node, realized by v1.stage0.coproduct_reflection type_item_by_name, which iterates ctx.modules and returns the FIRST item whose authored name matches and whose registry kind is TypeItem. WHAT WAS ACTUALLY EXECUTED, because reading that body is not evidence about the running compiler and the two specimens did NOT behave alike: for UriScheme -- a coproduct in extdeps.uri and a record in v2.std.network -- the seam ANSWERS, and the already-enrolled claim v2.test.manual.coproduct_reflection_conformance witness_uri_scheme_reflected_arm_keys_are_non_empty is green on main asserting exactly that non-empty answer; for Representation -- a coproduct in both v2.lens.intent_linearity and v2.std.integer, with disjoint arm sets -- the seam instead raises an untyped host error, unknown closed type, rather than picking. So this row claims a silent answer for the first shape and NOT for the second, and neither shape produces a typed located refusal, which is the defect the row is filed for. Both observations are from claim_batch runs over the roots dag and src/v2 against the claims in v2.test.manual.scoped_type_reflection_conformance" }, - reach: ReachabilityUnmeasured { what_would_settle_it: "a REFERENCE-grain census -- referencing module, bare spelling, candidate declaring modules -- over every call site of the three reflection seams, joined against the homonym declaration set from gunbc.bare_name_fork_lens bare_name_declarations_of. The declaration side is NOT the reach of this row and must not be substituted for it: a spelling declared twice but never referenced bare across scope reaches nothing here. That instrument does not exist yet and this row deliberately does not guess its result; fierce-lark-661 has ruled it a precondition for any refusal at this seam, and gunbc.bare_name_identity_consumer_census's own sweep-before-refusal law says the same thing. The call_site_count on this row is at a stated grain that is NOT the reach: it counts call sites of all THREE reflection seams -- resolve_type_node, coproduct_arm_keys and coproduct_nullary_inhabitants -- because the latter two reach this decision through the first, so the decision is made once per such site. It counts SITES, not ambiguous sites; how many of them name a spelling that is actually forked is exactly the unmeasured reach above" }, - sibling: SiblingPresentButUnreachable { sibling: decl_ref(module_path: "v2.std.decl_ref_resolution", decl_name: "resolve_declaration_ref_live"), why_unreachable: "the identity-keyed authority exists, is live-tree keyed, and already derives an explicit ambiguity arm from exactly the multiplicity this seam ignores -- but nothing routes to it, because resolve_type_node's parameter is a Symbol and a Symbol cannot name a module. The sibling is not consulted second, as at the ordered rows above; it is unreachable through this signature at all, so the repair is a signature change and not a reordering" }, - call_site_count: 16, - }, ] // THE HISTOGRAM IS DERIVED, NEVER STORED. A stored count is a second representation of the roster diff --git a/dag/gunbc/recurring_failure_mode/host_seam_self_call_diverges_when_its_arm_is_absent.dag b/dag/gunbc/recurring_failure_mode/host_seam_self_call_diverges_when_its_arm_is_absent.dag index be525621b50..c3f9a8d2d23 100644 --- a/dag/gunbc/recurring_failure_mode/host_seam_self_call_diverges_when_its_arm_is_absent.dag +++ b/dag/gunbc/recurring_failure_mode/host_seam_self_call_diverges_when_its_arm_is_absent.dag @@ -37,6 +37,8 @@ data host_seam_self_call_diverges_when_its_arm_is_absent: RecurringFailureMode = "WHY THE COMPARISON COULD NOT SEE IT, recorded because the next investigator will reach for the same instrument: two heads with one binary separates 'this head regressed' from 'nothing' only if the binary is sound. Where the binary carries the defect, the honest control needs a second ARTIFACT, not a second head. Three lanes matching one signature in two days was already the stronger inference and was available before the false report. ", "UNCERTAINTIES CARRIED, ONE OF THEM NOW DISCHARGED AND SAID SO HERE RATHER THAN LEFT STANDING BESIDE ITS ANSWER. This row used to carry, as its first uncertainty, that the specimen execution was a lane report and that no pre-#11121 binary had been run against it: the two-binary discrimination above did exactly that run, on a corpus head held fixed, so that uncertainty is closed and the mechanism no longer rests on a source reading alone. What remains uncertain is unchanged. The emitted-path claims are taken from `symbol_lexeme_seam_disposition_note`, the identity-form realization now in `v1_compiler.v1_rt`, and the resolver's stated suppression behaviour, not from an emission run performed for this row; that the two UNROSTERED self-call sites are absent from the emitted seed is a read of `src/v1` at f9d37e43a1, and whether an emission run that reached them would confirm a compiled self-call was not established by execution here. The denominator is a regex over first-expression self-application; a self-call reached through a `let` or a nested expression would be missed by the search and is not claimed absent.", + "ONE OF THE THIRTEEN IS GONE RATHER THAN CLIMBED, recorded by another lane (gunbc#11291) so the denominator above is not read as still current. `v2.std.node_reflection` resolve_type_node was one of the two self-call declarations this row names as having an interpreter arm and NO projection row -- the state it calls PROSPECTIVE exposure. It was not given a projection row and it did not climb: it was DELETED, together with its roster arm, its interpreter family arm, and the host functions beneath it (eval_resolve_type_node and the type_item_by_name scan), because a scope-carrying replacement left it with no consumer. So the count this row states is correct as OBSERVED on 2026-09-12 at f9d37e43a1 and is one lower afterwards, and the remaining member of that pair is `v2.std.data_index` data_init_decl_facts_live alone. The row is not re-swept here, because a lane that deletes one member is not thereby entitled to restate another lane's census.", + ], evidence: [ @@ -45,7 +47,6 @@ data host_seam_self_call_diverges_when_its_arm_is_absent: RecurringFailureMode = DeclarationRef { module_path: "std.primitive_projection", decl_name: "primitive_projection_roster", field: WholeDeclaration }, DeclarationRef { module_path: "std.primitive_projection", decl_name: "symbol_lexeme_seam_disposition_note", field: WholeDeclaration }, DeclarationRef { module_path: "gunbc.v1_interpreter_primitive_surface", decl_name: "v1_interpreter_primitive_arms", field: WholeDeclaration }, - DeclarationRef { module_path: "v2.std.node_reflection", decl_name: "resolve_type_node", field: WholeDeclaration }, DeclarationRef { module_path: "v2.std.data_index", decl_name: "data_init_decl_facts_live", field: WholeDeclaration }, DeclarationRef { module_path: "gunbc.recurring_failure_mode.dispatch_correctness_resting_on_arm_order", decl_name: "dispatch_correctness_resting_on_arm_order", field: WholeDeclaration }, DeclarationRef { module_path: "gunbc.recurring_failure_mode.unresolved_callee_conflated_with_dispatched_elsewhere", decl_name: "unresolved_callee_conflated_with_dispatched_elsewhere", field: WholeDeclaration }, diff --git a/dag/gunbc/v1/v1_interpreter_primitive_surface.dag b/dag/gunbc/v1/v1_interpreter_primitive_surface.dag index e498a1bf889..227693ea006 100644 --- a/dag/gunbc/v1/v1_interpreter_primitive_surface.dag +++ b/dag/gunbc/v1/v1_interpreter_primitive_surface.dag @@ -1942,15 +1942,6 @@ fn v1_interpreter_authored_roster_arms() -> List = [ "concept_decl_facts_live", "symbol_lexeme", "symbol_intern_lexeme", - "resolve_type_node", "data_init_decl_facts_live", ] @@ -1588,12 +1587,9 @@ data primitive_symbol_lexeme_traversal: PrimitiveTraversalOrderFact = PrimitiveT data primitive_symbol_intern_lexeme_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_symbol_intern_lexeme, order: OrderFreeResult } -// resolve_type_node is a name lookup of one type's Node: the result is a function of the -// argument, not of a walk whose order could leak. data_init_decl_facts_live is the sibling of -// concept_decl_facts_live: eval_data_init_decl_facts_live walks for_each_live_registry_item over -// ctx modules and items, so SourcePreservingOrder is the executed reading, not CanonicalOrder. -data primitive_resolve_type_node_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_resolve_type_node, order: OrderFreeResult } - +// data_init_decl_facts_live is the sibling of concept_decl_facts_live: +// eval_data_init_decl_facts_live walks for_each_live_registry_item over ctx modules and items, so +// SourcePreservingOrder is the executed reading, not CanonicalOrder. data primitive_data_init_decl_facts_live_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_data_init_decl_facts_live, order: SourcePreservingOrder } data primitive_projection_traversal_facts: List = [ @@ -1610,7 +1606,6 @@ data primitive_projection_traversal_facts: List = [ primitive_concept_decl_facts_live_traversal, primitive_symbol_lexeme_traversal, primitive_symbol_intern_lexeme_traversal, - primitive_resolve_type_node_traversal, primitive_data_init_decl_facts_live_traversal, ] diff --git a/dag/std/primitive_projection.dag b/dag/std/primitive_projection.dag index 5d594614464..dfba21b3fa9 100644 --- a/dag/std/primitive_projection.dag +++ b/dag/std/primitive_projection.dag @@ -82,7 +82,6 @@ data primitive_concept_decl_facts: PrimitiveIdentity = primitive_identity_slug(n data primitive_concept_decl_facts_live: PrimitiveIdentity = primitive_identity_slug(name: "concept_decl_facts_live") data primitive_symbol_lexeme: PrimitiveIdentity = primitive_identity_slug(name: "symbol_lexeme") data primitive_symbol_intern_lexeme: PrimitiveIdentity = primitive_identity_slug(name: "symbol_intern_lexeme") -data primitive_resolve_type_node: PrimitiveIdentity = primitive_identity_slug(name: "resolve_type_node") data primitive_data_init_decl_facts_live: PrimitiveIdentity = primitive_identity_slug(name: "data_init_decl_facts_live") data symbol_lexeme_seam_disposition_note: String = "THE TWO SYMBOL BRIDGES WERE HOST SEAMS THAT NOTHING SAID WERE HOST SEAMS, and the cost of that silence is why they are rostered here rather than left alone. v2.std.compilers.lexing symbol_lexeme and symbol_intern_lexeme have self-call bodies -- the HostRealizedSeam shape exactly, correct by construction because reaching one recurses to the evaluation-budget refusal -- and the interpreter has carried real arms for both since they were written (gunbc.v1_interpreter_primitive_surface v4_bridge.symbol_lexeme, v4_bridge.symbol_intern_lexeme). But with no roster row the RESOLVER saw an ordinary declaration, so Rust emission emitted the declaration, and `pub fn symbol_lexeme(sym: String) -> String { symbol_lexeme(sym) }` COMPILES. The emitted v2 compiler closure therefore carried two functions that type-check, pass every gate we own, and diverge from the interpreter by not terminating -- the DESIGN section 5 fabricated-plausible-output failure in its quietest form, since unlike the sibling seams (decl_facts and friends, which at least refuse loudly as unresolved v1_rt symbols) nothing anywhere reports this one. @@ -118,7 +117,6 @@ fn primitive_projection_roster() -> List { primitive_projection_row(primitive: primitive_lookup, module_path: "v2.std.collection", decl_name: "map_lookup_primitive_delegate", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_symbol_lexeme, module_path: "v2.std.compilers.lexing", decl_name: "symbol_lexeme", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_symbol_intern_lexeme, module_path: "v2.std.compilers.lexing", decl_name: "symbol_intern_lexeme", fidelity: HostRealizedSeam), - primitive_projection_row(primitive: primitive_resolve_type_node, module_path: "v2.std.node_reflection", decl_name: "resolve_type_node", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_data_init_decl_facts_live, module_path: "v2.std.data_index", decl_name: "data_init_decl_facts_live", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_length, module_path: "v2.std.algebra", decl_name: "length", fidelity: ModeledProjection), primitive_projection_row(primitive: primitive_map_insert, module_path: "v2.std.collection", decl_name: "map_insert", fidelity: ModeledProjection), diff --git a/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag b/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag index fae76ffa970..ae1269880af 100644 --- a/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag +++ b/dag/test/claim/v1_interpreter_primitive_surface_witness_test.dag @@ -73,7 +73,7 @@ test fn method_rows_are_authored_in_roster_rather_than_transcribed() -> Bool { test fn v4_bridge_rows_are_authored_in_roster_rather_than_transcribed() -> Bool { let rows = v1_interpreter_authored_roster_arms() |> filter(r => r.dispatch_symbol == "eval_call" && r.form == FreeCall) - rows |> any(r => r.authored_spelling == "resolve_type_node") + rows |> any(r => r.authored_spelling == "coproduct_nullary_inhabitants") && rows |> all(r => r.enumeration == AuthoredInRoster) } diff --git a/src/v1/stage0/src/coproduct_reflection.rs b/src/v1/stage0/src/coproduct_reflection.rs index 753eef4fb2f..5af8667c1d6 100644 --- a/src/v1/stage0/src/coproduct_reflection.rs +++ b/src/v1/stage0/src/coproduct_reflection.rs @@ -134,37 +134,6 @@ pub fn eval_symbol_lexeme( Ok(str_value(sym)) } -pub(crate) fn type_item_by_name<'a>( - ctx: &'a InterpContext, - type_name: &str, -) -> InterpResult<(&'a Rc, String)> { - let si = ctx.source_indices(); - for module in ctx.modules.iter() { - for item in module.items.iter() { - let name = authored_name_at(si.clone(), item.clone()); - if name != type_name { - continue; - } - let is_type = ctx - .item_registry - .get(&name) - .map(|info| info.kind == ItemKind::TypeItem) - .unwrap_or(false) - || ctx - .item_registry - .get(&item.name) - .map(|info| info.kind == ItemKind::TypeItem) - .unwrap_or(false); - if is_type { - return Ok((item, item.span.file.clone())); - } - } - } - Err(InterpError::TypeError { - msg: format!("resolve_type_node: unknown closed type `{type_name}`"), - }) -} - fn nullary_connective_variant(ctx: &InterpContext, name: &str) -> Value { Value::Variant { type_name: ctx.sym("Connective"), @@ -336,15 +305,6 @@ pub fn marshal_disj_type_item( )) } -pub fn eval_resolve_type_node( - ctx: &InterpContext, - args: &[(Option, Value)], -) -> InterpResult { - let type_name = expect_symbol(args.first().map(|(_, v)| v), "resolve_type_node")?; - let (item, _) = type_item_by_name(ctx, type_name)?; - marshal_disj_type_item(ctx, &ctx.source_indices(), item) -} - fn logical_qualified_name(module_name: &str, name: &str) -> String { // Concept-index reflection keeps the authored module path (including `v2.`). // Decl-index uses `decl_logical_qualified_name` instead (strips `v2.`). diff --git a/src/v1/stage0/src/std_primitive_projection.rs b/src/v1/stage0/src/std_primitive_projection.rs index 657d0622e4d..80aef078a2a 100644 --- a/src/v1/stage0/src/std_primitive_projection.rs +++ b/src/v1/stage0/src/std_primitive_projection.rs @@ -200,15 +200,6 @@ pub fn primitive_symbol_intern_lexeme() -> Rc { CACHED.with(|c: &Rc| c.clone()) } -pub fn primitive_resolve_type_node() -> Rc { - thread_local! { - static CACHED: Rc = { - primitive_identity_slug("resolve_type_node".to_string()) - }; - } - CACHED.with(|c: &Rc| c.clone()) -} - pub fn primitive_data_init_decl_facts_live() -> Rc { thread_local! { static CACHED: Rc = { @@ -308,12 +299,6 @@ pub fn primitive_projection_roster() -> Rc>> { "symbol_intern_lexeme".to_string(), Rc::new(ProjectionFidelity::HostRealizedSeam), ), - primitive_projection_row( - primitive_resolve_type_node(), - "v2.std.node_reflection".to_string(), - "resolve_type_node".to_string(), - Rc::new(ProjectionFidelity::HostRealizedSeam), - ), primitive_projection_row( primitive_data_init_decl_facts_live(), "v2.std.data_index".to_string(), diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index d20be4585fe..d5336699152 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -7405,8 +7405,6 @@ macro_rules! v1_bridge_family_arms { // name disagreeing with the roster fails to compile. family STD_NODE_REFLECTION_BRIDGE_FNS "v2.std.node_reflection" lookup_eval_call_bridge_std_node_reflection eval_call_bridge__v2_std_node_reflection_arm { - arm "v4_bridge.resolve_type_node" { "resolve_type_node" } => - crate::coproduct_reflection::eval_resolve_type_node($ctx, &$args), arm "v4_bridge.coproduct_nullary_inhabitants" { "coproduct_nullary_inhabitants" } => crate::coproduct_reflection::eval_coproduct_nullary_inhabitants($ctx, $node, &$args), } diff --git a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs index ff43e92a08d..742c410c942 100644 --- a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs +++ b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs @@ -552,27 +552,6 @@ macro_rules! eval_algebra_method_inner_arm { } #[rustfmt::skip] #[derive(Copy, Clone, Debug, PartialEq, Eq)] -pub enum EvalCallBridgeStdNodeReflectionArm { - V4BridgeResolveTypeNode, - V4BridgeCoproductNullaryInhabitants, -} - -#[rustfmt::skip] -pub fn lookup_eval_call_bridge_std_node_reflection(spelling: &str) -> Option { - match spelling { - "resolve_type_node" => Some(EvalCallBridgeStdNodeReflectionArm::V4BridgeResolveTypeNode), - "coproduct_nullary_inhabitants" => Some(EvalCallBridgeStdNodeReflectionArm::V4BridgeCoproductNullaryInhabitants), - _ => None, - } -} - -#[rustfmt::skip] -macro_rules! eval_call_bridge__v2_std_node_reflection_arm { - ("v4_bridge.resolve_type_node") => { $crate::v1_interpreter_dispatch_generated::EvalCallBridgeStdNodeReflectionArm::V4BridgeResolveTypeNode }; - ("v4_bridge.coproduct_nullary_inhabitants") => { $crate::v1_interpreter_dispatch_generated::EvalCallBridgeStdNodeReflectionArm::V4BridgeCoproductNullaryInhabitants }; -} -#[rustfmt::skip] -#[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum EvalCallBridgeStdCompilersLexingArm { V4BridgeSymbolInternLexeme, V4BridgeSymbolLexeme, @@ -612,6 +591,24 @@ macro_rules! eval_call_bridge__v2_std_qualified_name_arm { } #[rustfmt::skip] #[derive(Copy, Clone, Debug, PartialEq, Eq)] +pub enum EvalCallBridgeStdNodeReflectionArm { + V4BridgeCoproductNullaryInhabitants, +} + +#[rustfmt::skip] +pub fn lookup_eval_call_bridge_std_node_reflection(spelling: &str) -> Option { + match spelling { + "coproduct_nullary_inhabitants" => Some(EvalCallBridgeStdNodeReflectionArm::V4BridgeCoproductNullaryInhabitants), + _ => None, + } +} + +#[rustfmt::skip] +macro_rules! eval_call_bridge__v2_std_node_reflection_arm { + ("v4_bridge.coproduct_nullary_inhabitants") => { $crate::v1_interpreter_dispatch_generated::EvalCallBridgeStdNodeReflectionArm::V4BridgeCoproductNullaryInhabitants }; +} +#[rustfmt::skip] +#[derive(Copy, Clone, Debug, PartialEq, Eq)] pub enum EvalCallBridgeStdConceptIndexArm { V4BridgeConceptDeclFactsLive, } diff --git a/src/v2/compiler/effect_demand.dag b/src/v2/compiler/effect_demand.dag index 2b9514684e8..0840580f2d4 100644 --- a/src/v2/compiler/effect_demand.dag +++ b/src/v2/compiler/effect_demand.dag @@ -1275,13 +1275,6 @@ data effect_demand_seam_roster: List = [ emitted_rust_identity: "v2_std_decl_index.rs::data_decl_type_facts", evidence: SeamRefusalObservedInClosure { closure_entry: "v2.compiler.compile" } }, - SeamStanding { - declaration: "resolve_type_node", - seam_module: "v2.std.node_reflection", - projection: ProjectedPrimitive { primitive: primitive_identity_slug(name: "resolve_type_node") }, - emitted_rust_identity: "v2_std_node_reflection.rs::resolve_type_node", - evidence: SeamEvidenceDerivedNotExercised { reason: ^declaration_not_emitted_in_the_measured_closure } - }, SeamStanding { declaration: "coproduct_nullary_inhabitants", seam_module: "v2.std.node_query", diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index 7ba41a99ce5..c7602072b43 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -22,14 +22,28 @@ import v2.std.decl_index { import v2.std.node { Node, Symbol } import v2.std.node_query { coproduct_arm_key_list_from_node, node_is_coproduct } -// THE HOST TYPE-REFLECTION SURFACE, AND WHY IT IS ITS OWN MODULE. +// THE HOST TYPE-REFLECTION SURFACE, AND WHY ONE OF ITS TWO SEAMS IS GONE. // -// Both declarations below are host seams: their whole body is a self-call, answered by -// the v1 interpreter's live declaration index (roster arms v4_bridge.resolve_type_node -// and v4_bridge.coproduct_nullary_inhabitants). Nothing in the substrate can give them a -// body, because neither the resolved Node for a type NAME nor an inhabitant of an -// arbitrary T is derivable from anything the caller hands them -- the answer is a fact -// about the running compiler's own source index, not about the arguments. +// coproduct_nullary_inhabitants below is a host seam: its whole body is a self-call, +// answered by the v1 interpreter's live declaration index (roster arm +// v4_bridge.coproduct_nullary_inhabitants). Nothing in the substrate can give it a body, +// because an inhabitant of an arbitrary T is not derivable from anything the caller hands +// it -- the answer is a fact about the running compiler's own source index. +// +// resolve_type_node USED TO BE THE OTHER ONE, AND IS DELETED RATHER THAN RENAMED. It took a +// BARE type spelling, and its host arm answered by scanning the interpreter's loaded modules +// and returning the FIRST item whose authored name matched -- so a spelling two modules +// declare was answered from whichever load order reached first, with no diagnostic. That is +// the DESIGN section 5 silent wrongness this module now exists to refuse. +// +// It is deleted because after the cutover nothing consumed it: the guarded route establishes +// multiplicity and shape from the KEYED declaration read and returns the node that read +// already carries, so it never needs the bare scan, and every other consumer was moved. A +// rename would have kept a bare-spelling host route alive under a new name, which is exactly +// the surviving-X attractor DESIGN section 3 warns about -- the old vocabulary stays +// available and the next question gets answered in it. The host functions it reached, +// eval_resolve_type_node and the type_item_by_name scan beneath it, had no other caller and +// are deleted with it, so the seed shrinks (DESIGN section 7) rather than growing a synonym. // // They used to sit in v2.std.node and v2.std.node_query, which the v2 compiler's import // closure carries. Emission is decided at MODULE grain, so both were emitted into the @@ -45,14 +59,6 @@ import v2.std.node_query { coproduct_arm_key_list_from_node, node_is_coproduct } // emitted crate -- loudly, at the same grep the census reads. The rule the split states // is that reflection is an INTERPRETER-time capability: available to a lens or a witness // reading the live tree, never to a declaration the compiler must emit. -fn resolve_type_node(type_name: Symbol) -> Node { - resolve_type_node(type_name: type_name) -} - -fn coproduct_arm_keys(type_name: Symbol) -> List { - coproduct_arm_key_list_from_node(node: resolve_type_node(type_name: type_name)) -} - fn coproduct_nullary_inhabitants( type_name: Symbol, discriminant_of: fn(T) -> Symbol @@ -83,12 +89,19 @@ fn coproduct_nullary_inhabitants( // -- "how many declarations answer to this name" -- and whose five-arm refusal law this module // deliberately does not restate. // -// Consumers (DESIGN section 3c). Consumed by execution in this change: the conformance witness -// named above. Declared frontier, with its trigger stated: the floor's cross-claim memo and -// `coproduct_arm_keys`'s callers (`v2.lens.affected_set`, the generated coproduct witnesses) -// cut over to `coproduct_arm_keys_at` once a key shape is agreed with the floor-cost lane -- -// that cutover is the trigger, and until it lands the bare pair above stays reachable and -// stays unguarded, which this annotation states rather than hides. +// Consumers (DESIGN section 3c), and there is NO open frontier here any more. Consumed by execution +// in this change: v2.lens.affected_set (through the guarded route, with a refusal landing in +// UniverseIncomplete), the generated coproduct witnesses, the reflection conformance witness, the +// wiring-liveness entry, and the conformance claims in +// v2.test.manual.scoped_type_reflection_conformance. +// +// An earlier revision of this annotation classified that cutover as a DECLARED FRONTIER and said the +// bare pair stayed reachable and unguarded until it landed. review 65702 caught that the sentence +// had outlived the tree: the cutover HAD landed in this same change, so the classification was the +// wrong section 3c arm and, worse, it justified leaving a silent-first-match route importable after +// its consumers were gone -- the escape hatch DESIGN section 5 forbids and the surviving-X attractor +// section 3 warns about. The bare pair is now deleted rather than described, so there is nothing +// left for a frontier sentence to be about. // WHY THIS IS A KEYED READ AND NOT A FOLD OVER decl_facts. The first version of this guard filtered // the whole declaration corpus, which was correct and cost roughly 3.6s per call against 1ms for a // keyed read, sharing at no grain -- four calls inside ONE claim frame cost four times one. That put From e5214f0bdce0ad40f11a4af827fd0c0f6e72a7e9 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 22:13:51 +0000 Subject: [PATCH 10/16] Repoint a diagnostic that named the function this PR deleted marshal_disj_type_item refused a non-Disj item under the message "resolve_type_node: type is not a closed coproduct". That function no longer exists, so the message named a caller a reader could not find -- the stale citation class, in the one place a reader meets it at the worst moment, while diagnosing a refusal. It now names the function that actually refuses. The surviving caller is concept_decl_node, reached when a TypeItem declaration node is marshalled for decl_facts, which is the route the guarded reflection read now returns its node from. NOT CHANGED, deliberately: the doc comment in namespace_wave_admission that still names resolve_type_node and coproduct_arm_keys. It is another lane's historical record of what gunbc#9724 moved, written in the past tense of its own measurement, and the corpus convention -- stated in gunbc.bare_name_identity_consumer_census for exactly this case -- is that retired spellings survive verbatim in prose describing source as it stood, because rewriting them falsifies the observation rather than repairing it. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- src/v1/stage0/src/coproduct_reflection.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v1/stage0/src/coproduct_reflection.rs b/src/v1/stage0/src/coproduct_reflection.rs index 5af8667c1d6..a5df9b32fd6 100644 --- a/src/v1/stage0/src/coproduct_reflection.rs +++ b/src/v1/stage0/src/coproduct_reflection.rs @@ -289,7 +289,7 @@ pub fn marshal_disj_type_item( ) -> InterpResult { if item.connective != Connective::Disj { return Err(InterpError::TypeError { - msg: "resolve_type_node: type is not a closed coproduct (Disj)".to_string(), + msg: "marshal_disj_type_item: type is not a closed coproduct (Disj)".to_string(), }); } let mut edges = Vec::with_capacity(item.children.len()); From af80d3d55c081c1f6b59d46a62a9693796a27205 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 22:24:38 +0000 Subject: [PATCH 11/16] File the class: two modules can answer to one logical qualified name The declaration index's logical qualified name strips a leading `v2.`, so under the v2-mirror layout v2.std.integer and std.integer both answer to `std.integer`. A caller that cites module plus declaration name -- believing it has said exactly which declaration it means -- has said something two declarations satisfy, and a route keyed on that name binds to whichever row the keyed read ordered first. IT IS NOT THE BARE-SPELLING CLASS WEARING A NEW NAME, and the row says why, because the resemblance is close enough to merge them by mistake. A bare spelling is ambiguous BY CONSTRUCTION -- it carries no scope and every consumer knows it must be disambiguated. This is ambiguity SURVIVING disambiguation: the caller supplied the scope the bare form lacked and the index collapsed it anyway. So the repair is not "make callers cite their module", which they already did. WHAT MAKES IT AUTHORABLE, which is the part an author gets wrong: the collision is not inside a module, where a duplicate declaration is refused at resolve, but BETWEEN two modules whose logical names coincide after the strip. An author asking "can one module declare this name twice" concludes the state is unconstructible and writes no test. Twelve module pairs collide and eighteen type names are declared under both halves of a pair. The rule that derives those figures is stated on the row so a reader recomputes rather than trusts them, and the row says plainly that no reference-grain instrument over the relation exists yet. Its specimen is gunbc#11291's own citation route, which refused the ZERO case and sent every non-zero multiplicity into an accept path that takes a head -- the review tell the row records, because refusing absent-and-present reads as complete and the third state is the one nobody names. That route now refuses typed and located, and the RED enrolled against it cites a LIVE pair rather than a fixture, which is why this is filed as a class rather than as that PR's bug. RUNG AND CEILING ARE KEPT APART. Found at mitigatable, and only at the one route repaired -- nothing stops the next keyed-on-qualified-name consumer from omitting the arm and nothing enumerates the consumers that exist. The ceiling is structural impossibility through a scope-carrying occurrence identity (ScopedOccurrenceRef with ContainmentPath), where the module path is part of the identity rather than a normalised string beside it. The trigger names that capability ANSWERING BY EXECUTION over the colliding pair, and explicitly does not count the identity type being declared, nor the one multiplicity arm this PR already added. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- ...s_answer_to_one_logical_qualified_name.dag | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 dag/gunbc/recurring_failure_mode/two_modules_answer_to_one_logical_qualified_name.dag diff --git a/dag/gunbc/recurring_failure_mode/two_modules_answer_to_one_logical_qualified_name.dag b/dag/gunbc/recurring_failure_mode/two_modules_answer_to_one_logical_qualified_name.dag new file mode 100644 index 00000000000..f31354aed54 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/two_modules_answer_to_one_logical_qualified_name.dag @@ -0,0 +1,32 @@ +module gunbc.recurring_failure_mode.two_modules_answer_to_one_logical_qualified_name + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data two_modules_answer_to_one_logical_qualified_name: RecurringFailureMode = RecurringFailureMode { + identity: "two_modules_answer_to_one_logical_qualified_name" as NonEmptyStr, + + receipts: [ + "**two modules answer to ONE logical qualified name, so a citation that names its module is still not an identity** (INVALID STATE: the declaration index's logical qualified name strips a leading `v2.` -- v2.std.decl_index logical_qualified_name_from_module -- so under the v2-mirror layout `v2.std.integer` and `std.integer` both answer to `std.integer`. A caller that cites module plus declaration name, believing it has said exactly which declaration it means, has said something two declarations satisfy. HARM: a route keyed on the qualified name binds ONE GRAIN DOWN to whichever row the keyed read ordered first -- the same first-match-without-a-diagnostic shape a bare spelling has, arrived at by a caller who did the right thing and named the module.", + + "WHY IT IS NOT THE BARE-SPELLING CLASS WEARING A NEW NAME, because the resemblance is close enough to merge them by mistake. A bare spelling is ambiguous BY CONSTRUCTION: it carries no scope, so every consumer knows it must be disambiguated. This state is ambiguity SURVIVING disambiguation -- the caller supplied the scope the bare form lacked, and the index collapsed it anyway. The repair is therefore not `make callers cite their module`, which they already did; it is that the identity a citation resolves to must carry scope the strip cannot erase.", + + "DISTINGUISHING FACT, AND IT IS WHAT MAKES THE STATE AUTHORABLE RATHER THAN HYPOTHETICAL: the collision is not inside a module, where a duplicate declaration is refused at resolve, but BETWEEN two modules whose logical names coincide after the strip. That is why an author checking `can one module declare this name twice` concludes the state is unconstructible and writes no test for it. Derived over dag and src/v2 by intersecting the type names declared by each `v2.X` module with those declared by `X`: TWELVE module pairs collide and EIGHTEEN type names are declared under both halves of a pair, among them std.integer.Int and std.float.Float. The figures are a re-derivable reading rather than an oracle -- the rule that produces them is stated here so a reader recomputes rather than trusts, and a reference-grain instrument over this relation does not exist yet.", + + "RECOGNITION RULE: when a lookup is keyed on a qualified name, ask whether the key is the AUTHORED module path or a NORMALISED one, and if it is normalised, whether the normalisation can map two authored modules onto one key. If it can, a multiplicity arm is required at that key's grain even though the citation looks exact. The reviewer tell: a route that refuses the ZERO case of a keyed read and sends every non-zero multiplicity into an accept path that takes a head -- the refusal reads as complete because absent and present are both handled, and the third state is the one nobody named.", + + "SPECIMEN, gunbc#11291. The citation route added for scope-carrying type reflection refused a cited name that resolved to nothing and accepted everything else, so two declarations under one logical qualified name would have been answered from whichever came first. Found by review rather than by the claim family, which had no discriminating RED for it. The route now refuses that multiplicity typed and located on its own arm, and the RED enrolled against it -- v2.test.manual.scoped_type_reflection_conformance cited_ambiguous_qualified_name_refuses_rather_than_taking_the_head -- cites a LIVE pair (v2.std.integer and std.integer, both declaring Int) rather than a fixture, which is the whole reason this row is filed as a class and not as that PR's bug.", + + "RUNG FOUND AT: mitigatable, and only at the one route that has been repaired. The citation route refuses, typed and located, so the harm is contained where it was found. Nothing prevents the next keyed-on-qualified-name consumer from being written without the multiplicity arm, and nothing enumerates the consumers that already exist -- so the class is contained at one site rather than closed.", + + "ATTAINABLE CEILING: STRUCTURALLY IMPOSSIBLE, and the authority that would reach it is already being built rather than merely imagined. The invalid state is that an identity is representable which does not determine a declaration; a scope-carrying occurrence identity -- crisp-carp-634's ScopedOccurrenceRef, with ContainmentPath -- makes the module path part of the identity rather than a normalised string beside it, so two declarations cannot share one. Until such an identity is what citations resolve THROUGH, this stays a multiplicity arm each consumer must remember, which is mechanically preventable at best.", + + "NEXT-RUNG TRIGGER, a capability and not an artifact: a citation resolves through a scope-carrying occurrence identity whose equality distinguishes v2.std.integer.Int from std.integer.Int, ANSWERING BY EXECUTION over that pair -- sufficient that no keyed-on-qualified-name consumer can reach two declarations under one key. It is NOT satisfied by the identity type being declared, nor by one route growing a multiplicity arm, which is what this row records as already done and explicitly does not count as the climb.", + ], + + evidence: [ + DeclarationRef { module_path: "v2.std.decl_index", decl_name: "logical_qualified_name_from_module", field: WholeDeclaration }, + DeclarationRef { module_path: "v2.std.node_reflection", decl_name: "resolve_type_node_at", field: WholeDeclaration }, + ], +} From b1c5eb98c60d52ab9b9e3d1bf4997a8a7b135152 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 13 Sep 2026 23:46:28 +0000 Subject: [PATCH 12/16] Roster the new seam, and fix the parse break that refused the floor THE FLOOR RED WAS MINE AND IS FIXED. required-ci refused before any claim with ChangedWitnessObservationFailed: parse failed for coproduct_exhaustiveness.dag, "expected item declaration". The cutover commit had inserted the pool-roots data row BETWEEN two imports, so the import that followed 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 the same authoring gap rather than two accidents: I verified the entries I ran and not the ones I edited. These two live outside witness_discovery_scan_dirs, so no run of mine resolved them, and the floor is the first consumer that parses a changed witness. They are now executed: both exhaustiveness claims green. review 65729 -- THE NEW SEAM WAS UNROSTERED, and this is the more serious half. v2.std.decl_index type_declarer_qualified_names has a self-call body and carried NO primitive_projection_roster row and NO SeamStanding row, while every sibling in that module carries both. v2.std.decl_index IS in the emitted closure, so the resolver would have seen an ordinary declaration and emitted `type_declarer_qualified_names(...) { type_declarer_qualified_names(...) }` -- a function that compiles, passes every gate, and does not terminate. That is exactly the state symbol_lexeme_seam_disposition_note already records, and exactly the class host_seam_self_call_diverges_when_its_arm_is_absent names -- the row I edited in this same PR while adding an unrostered member to it. The keyed_declaration_read_seed_growth receipt covers the RUST arm and is not the projection declaration, so it never closed this. Both rows are added, in dag/std and in the stage0 mirror, and the traversal-order reasoning is 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 the observed arm would have been the rung inflation the ladder forbids. NOT MINE, established rather than assumed: cross_representation_equality fails --entry resolve with effect-summary incompleteness over v2.lens.testgen callees. Restoring the pre-change file from before the cutover commit reproduces the same failure, so the change is not the cause. An earlier attempt to isolate it via git stash proved nothing -- the edits were already committed, so the stash was empty and the "reverted" run still carried them. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- dag/std/primitive_identity.dag | 12 ++++++++++-- dag/std/primitive_projection.dag | 2 ++ src/v1/stage0/src/std_primitive_projection.rs | 15 +++++++++++++++ src/v2/compiler/effect_demand.dag | 7 +++++++ .../claim/generated/coproduct_exhaustiveness.dag | 12 ++++++++---- 5 files changed, 42 insertions(+), 6 deletions(-) diff --git a/dag/std/primitive_identity.dag b/dag/std/primitive_identity.dag index 119197f9ae5..4b6eb181c76 100644 --- a/dag/std/primitive_identity.dag +++ b/dag/std/primitive_identity.dag @@ -34,6 +34,7 @@ import std.primitive_projection { primitive_projection_roster, primitive_projection_row_for_declaration, primitive_length, primitive_map_insert, primitive_map_get, primitive_lookup, primitive_empty_map, primitive_decl_facts, primitive_decl_facts_at, primitive_export_signature_facts, primitive_data_decl_type_facts, + primitive_type_declarer_qualified_names, primitive_concept_decl_facts, primitive_concept_decl_facts_live, primitive_symbol_lexeme, primitive_symbol_intern_lexeme, primitive_data_init_decl_facts_live, @@ -1230,6 +1231,7 @@ data primitive_projection_target_canonical_names: List = [ "empty_map", "decl_facts", "decl_facts_at", + "type_declarer_qualified_names", "export_signature_facts", "data_decl_type_facts", "concept_decl_facts", @@ -1551,8 +1553,11 @@ data primitive_empty_map_traversal: PrimitiveTraversalOrderFact = PrimitiveTrave // decl_facts_corpus_walk, whose final step sorts every fact by (rel_path, name, kind_ord) before // returning. decl_facts_at is that same census filtered on qualified_name with the surviving rows // left in place, so it inherits the order rather than choosing one -- a filter cannot reorder what -// it does not rebuild. export_signature_facts derives from decl_facts_for_roots and preserves that -// order. +// it does not rebuild. type_declarer_qualified_names is the same reading one key over: it filters +// that identical census on bare name and TypeItem kind and projects each surviving row's qualified +// name, so it inherits the order for the same reason and for no separate one -- it rebuilds +// nothing, and it marshals no declaration nodes at all. export_signature_facts derives from +// decl_facts_for_roots and preserves that order. // concept_decl_facts and data_decl_type_facts route through decls_parse_only_fail_closed, which // sorts its module list (decls_parse_only_from_disk) or its inventory entries by source path // (decls_parse_only_from_inventory) before walking items in source order. concept_decl_facts_live @@ -1564,6 +1569,8 @@ data primitive_decl_facts_traversal: PrimitiveTraversalOrderFact = PrimitiveTrav data primitive_decl_facts_at_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_decl_facts_at, order: CanonicalOrder } +data primitive_type_declarer_qualified_names_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_type_declarer_qualified_names, order: CanonicalOrder } + data primitive_export_signature_facts_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_export_signature_facts, order: CanonicalOrder } data primitive_data_decl_type_facts_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_data_decl_type_facts, order: CanonicalOrder } @@ -1600,6 +1607,7 @@ data primitive_projection_traversal_facts: List = [ primitive_empty_map_traversal, primitive_decl_facts_traversal, primitive_decl_facts_at_traversal, + primitive_type_declarer_qualified_names_traversal, primitive_export_signature_facts_traversal, primitive_data_decl_type_facts_traversal, primitive_concept_decl_facts_traversal, diff --git a/dag/std/primitive_projection.dag b/dag/std/primitive_projection.dag index dfba21b3fa9..3421296e7dc 100644 --- a/dag/std/primitive_projection.dag +++ b/dag/std/primitive_projection.dag @@ -78,6 +78,7 @@ data primitive_decl_facts: PrimitiveIdentity = primitive_identity_slug(name: "de data primitive_decl_facts_at: PrimitiveIdentity = primitive_identity_slug(name: "decl_facts_at") data primitive_export_signature_facts: PrimitiveIdentity = primitive_identity_slug(name: "export_signature_facts") data primitive_data_decl_type_facts: PrimitiveIdentity = primitive_identity_slug(name: "data_decl_type_facts") +data primitive_type_declarer_qualified_names: PrimitiveIdentity = primitive_identity_slug(name: "type_declarer_qualified_names") data primitive_concept_decl_facts: PrimitiveIdentity = primitive_identity_slug(name: "concept_decl_facts") data primitive_concept_decl_facts_live: PrimitiveIdentity = primitive_identity_slug(name: "concept_decl_facts_live") data primitive_symbol_lexeme: PrimitiveIdentity = primitive_identity_slug(name: "symbol_lexeme") @@ -110,6 +111,7 @@ fn primitive_projection_roster() -> List { primitive_projection_row(primitive: primitive_decl_facts_at, module_path: "v2.std.decl_index", decl_name: "decl_facts_at", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_export_signature_facts, module_path: "v2.std.decl_index", decl_name: "export_signature_facts", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_data_decl_type_facts, module_path: "v2.std.decl_index", decl_name: "data_decl_type_facts", fidelity: HostRealizedSeam), + primitive_projection_row(primitive: primitive_type_declarer_qualified_names, module_path: "v2.std.decl_index", decl_name: "type_declarer_qualified_names", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_concept_decl_facts, module_path: "v2.std.concept_index", decl_name: "concept_decl_facts", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_concept_decl_facts_live, module_path: "v2.std.concept_index", decl_name: "concept_decl_facts_live", fidelity: HostRealizedSeam), primitive_projection_row(primitive: primitive_empty_map, module_path: "v2.std.collection", decl_name: "empty_map_primitive_delegate", fidelity: HostRealizedSeam), diff --git a/src/v1/stage0/src/std_primitive_projection.rs b/src/v1/stage0/src/std_primitive_projection.rs index 80aef078a2a..add7cbba212 100644 --- a/src/v1/stage0/src/std_primitive_projection.rs +++ b/src/v1/stage0/src/std_primitive_projection.rs @@ -137,6 +137,15 @@ pub fn primitive_decl_facts() -> Rc { CACHED.with(|c: &Rc| c.clone()) } +pub fn primitive_type_declarer_qualified_names() -> Rc { + thread_local! { + static CACHED: Rc = { + primitive_identity_slug("type_declarer_qualified_names".to_string()) + }; + } + CACHED.with(|c: &Rc| c.clone()) +} + pub fn primitive_decl_facts_at() -> Rc { thread_local! { static CACHED: Rc = { @@ -245,6 +254,12 @@ pub fn primitive_projection_roster() -> Rc>> { "decl_facts_at".to_string(), Rc::new(ProjectionFidelity::HostRealizedSeam), ), + primitive_projection_row( + primitive_type_declarer_qualified_names(), + "v2.std.decl_index".to_string(), + "type_declarer_qualified_names".to_string(), + Rc::new(ProjectionFidelity::HostRealizedSeam), + ), primitive_projection_row( primitive_export_signature_facts(), "v2.std.decl_index".to_string(), diff --git a/src/v2/compiler/effect_demand.dag b/src/v2/compiler/effect_demand.dag index 0840580f2d4..d6b8bd4d72f 100644 --- a/src/v2/compiler/effect_demand.dag +++ b/src/v2/compiler/effect_demand.dag @@ -1254,6 +1254,13 @@ data effect_demand_seam_roster: List = [ emitted_rust_identity: "v2_std_compilers_lexing.rs::symbol_intern_lexeme", evidence: SeamEvidenceDerivedNotExercised { reason: ^declaration_not_emitted_in_the_measured_closure } }, + SeamStanding { + declaration: "type_declarer_qualified_names", + seam_module: "v2.std.decl_index", + projection: ProjectedPrimitive { primitive: primitive_identity_slug(name: "type_declarer_qualified_names") }, + emitted_rust_identity: "v2_std_decl_index.rs::type_declarer_qualified_names", + evidence: SeamEvidenceDerivedNotExercised { reason: ^projection_row_authored_emission_not_re_measured } + }, SeamStanding { declaration: "decl_facts", seam_module: "v2.std.decl_index", diff --git a/src/v2/test/claim/generated/coproduct_exhaustiveness.dag b/src/v2/test/claim/generated/coproduct_exhaustiveness.dag index 6200d0d8239..588fad9404c 100644 --- a/src/v2/test/claim/generated/coproduct_exhaustiveness.dag +++ b/src/v2/test/claim/generated/coproduct_exhaustiveness.dag @@ -14,9 +14,6 @@ import v2.std.diagnostic { Accepted, None, Outcome, Rejected } import v2.std.logic { Bool } import v2.std.node { Node, Symbol } import v2.std.node_reflection { coproduct_arm_keys_checked } - -// THE ROOTS THE REFLECTION READS CONSULT, named so the population is re-derivable. -data coproduct_exhaustiveness_pool_roots: List = ["dag", "src/v2"] import v2.std.verification { ClaimAnchorKey, DiagnosticClaim, @@ -28,6 +25,9 @@ import v2.std.verification { test_claim_input } +// THE ROOTS THE REFLECTION READS CONSULT, named so the population is re-derivable. +data coproduct_exhaustiveness_pool_roots: List = ["dag", "src/v2"] + fn reference_coproduct_exhaustiveness_anchor() -> GeneratedAnchorKey { coproduct_exhaustiveness_anchor(coproduct_type: ^TestClaim, omitted_variant: ^DiagnosticClaim) } @@ -132,7 +132,11 @@ fn roster_covers_all_arms_of(coproduct_type: Symbol) -> Bool { fn witness_coproduct_exhaustiveness_roster_covers_testclaim() -> Bool { let gens = testgen_scheduled_coproduct_exhaustiveness_generators() (length(xs: gens) > 0) - && roster_covers_all_arms_of_roster(gens: gens, coproduct_type: ^TestClaim) + && roster_covers_all_arms_of_roster( + pool_roots: coproduct_exhaustiveness_pool_roots, + gens: gens, + coproduct_type: ^TestClaim + ) } fn witness_coproduct_exhaustiveness_covers_second_coproduct() -> Bool { From 9020560b132f6831dd840ede64120dd6e71af1fb Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 14 Sep 2026 01:50:44 +0000 Subject: [PATCH 13/16] Install both mirrors from the pre-deletion seed's candidate, and cite Bool THE MIRRORS ARE NOW INSTALLED, NOT AUTHORED, and the provenance is literal rather than inferred. Both src/v1/stage0/src/std_primitive_projection.rs and v1_interpreter_dispatch_generated.rs are copied 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. That seed, run with --required-regen against the current sources, reports first_generation_equal=true and its candidate is byte-identical to both committed files. WHY THAT ROUTE RATHER THAN THE FIXED POINT I ALREADY HAD. The drift phase refused std_primitive_projection.rs because I had hand-written the new seam's projection rows into it; the emitter places the row after data_decl_type_facts, following the roster order, and I had inserted it earlier. So there was never a bootstrap problem on that file -- only a generated artifact authored by hand. The dispatch file is different and is the one worth stating precisely: deleting the seam left the committed generated file carrying an enum variant whose match arm was gone, so the tree would not build and there was seemingly no binary to regenerate with. That appearance of deadlock was false. The PREVIOUS generation's seed reads the NEW sources and emits the new mirrors with no edit at all, which is the bootstrap itself. Reaching for the editor was the workaround DESIGN section 5 names, and the regeneration later AGREEING with those bytes proved the bytes and not the method -- a fixed point is not a provenance. Both halves 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 -- a regeneration reverting a hand edit. The receipt records the tell that generalises: noticing you are routing around the build IS the line-stop signal, and the discriminator a reviewer can apply without reading the diff is to 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 ONE REMAINING CLAIM FAILURE IS FIXED, and it is the cutover working rather than breaking something. generated_cross_representation_equality_covers_bool returned false because 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. 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 regression controls rather than left as a one-off repair, because a production claim now depends on that citation being the right one: cited_bool_resolves_to_the_logic_module_arms asserts v2.std.logic Bool resolves to exactly True and False, and bare_bool_spelling_refuses_as_ambiguous asserts the bare form still refuses. If either flips, the cross-representation witness is resting on a spelling again. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- ...candidate_reverts_hand_authored_mirror.dag | 8 +++++ src/v1/stage0/src/std_primitive_projection.rs | 28 +++++++-------- .../cross_representation_equality.dag | 36 +++++++++++++++---- ...coped_type_reflection_conformance_test.dag | 30 ++++++++++++++++ 4 files changed, 82 insertions(+), 20 deletions(-) diff --git a/dag/gunbc/recurring_failure_mode/regen_candidate_reverts_hand_authored_mirror.dag b/dag/gunbc/recurring_failure_mode/regen_candidate_reverts_hand_authored_mirror.dag index ed68d7d70ac..40d158bb092 100644 --- a/dag/gunbc/recurring_failure_mode/regen_candidate_reverts_hand_authored_mirror.dag +++ b/dag/gunbc/recurring_failure_mode/regen_candidate_reverts_hand_authored_mirror.dag @@ -11,6 +11,14 @@ data regen_candidate_reverts_hand_authored_mirror: RecurringFailureMode = Recurr "Invalid state: an install step whose population is `every file in the candidate` over a directory that holds BOTH generated and hand-authored files. Harm: hand-authored rows silently disappear -- not only the author's own, but rows other lanes landed earlier, because the candidate's copy is as old as the last build that produced it. The run then reports first_generation_equal and the author reports the verification they genuinely performed BEFORE the install.", + "THE OTHER DIRECTION OF THE SAME CONFUSION, gunbc#11291: not a regeneration reverting a hand edit, but an AUTHOR hand-editing a file the regeneration owns, which the drift phase then refuses. Recorded here rather than as a neighbour because both arise from one unresolved question -- WHICH SIDE AUTHORS THIS FILE -- and a reader who has internalised only the revert direction still reaches for the editor when the build breaks.", + + "THE MECHANISM, AND WHY IT LOOKED NECESSARY AT THE TIME. Deleting a host seam removed its .dag roster row and its interpreter family arm, while the COMMITTED generated dispatch file still carried the arm's enum variant. The match went non-exhaustive, so the tree would not build -- and with no binary from that tree, there was apparently nothing to regenerate with. The editor looked like the only move. It was not: the PREVIOUS generation's binary, built before the deletion, reads the NEW .dag sources and emits the new mirrors without any edit. A previous-generation seed regenerating the next generation is the bootstrap itself, and the appearance of deadlock came from looking only at the tree that would not build.", + + "THE TELL IS THE AUTHOR'S OWN STATE, NOT THE DIFF, which is what makes this worth a receipt: noticing that you are routing around the build IS the line-stop signal, and the author did not stop. DESIGN section 5 names the workaround as an absorbing fallback executed by the author, and its concealed deficit is usually in the layer the author is least equipped to inspect -- here the bootstrap order. The second instance in the same change had no deadlock at all: a projection mirror was hand-written for a NEW primitive, and the only difference from the emitted candidate turned out to be ROW ORDER, the emitter following the roster order the author had not matched. Same reach for the editor, no obstacle to justify it.", + + "THE DISCRIMINATOR A REVIEWER CAN APPLY WITHOUT READING THE DIFF, offered because a fixed point is what made this one hard to see: a regeneration that AGREES with a hand edit proves the bytes are right and proves nothing about the method, so `first_generation_equal=true` is not evidence the file was authored correctly. Ask instead where the bytes came from. The receipt a generated surface owes is `installed from the candidate emitted by seed X`, and `hand-edited, later confirmed by regeneration` is a different claim wearing the same green.", + "RUNG FOUND AT: 1, mitigatable.", "RECEIPT, gunbc#10688. Two `NAMESPACE_TRANSITION_ADMISSIONS` rows were authored in `src/v1/stage0/src/namespace_wave_admission.rs`, the phase was run, and it reported both ADMITTED-BY. The regen loop then installed the candidate, which reverted that file to a state predating gunbc#10676 -- deleting the two new rows AND the nine gunbc#10676 rows that had been on main for a day. The commit landed with a message asserting the phase green over bytes that no longer carried the admissions, and `git show --stat` on that commit read 23 insertions / 118 DELETIONS in a file the change was supposed to grow.", diff --git a/src/v1/stage0/src/std_primitive_projection.rs b/src/v1/stage0/src/std_primitive_projection.rs index add7cbba212..f41c2c1b21f 100644 --- a/src/v1/stage0/src/std_primitive_projection.rs +++ b/src/v1/stage0/src/std_primitive_projection.rs @@ -137,37 +137,37 @@ pub fn primitive_decl_facts() -> Rc { CACHED.with(|c: &Rc| c.clone()) } -pub fn primitive_type_declarer_qualified_names() -> Rc { +pub fn primitive_decl_facts_at() -> Rc { thread_local! { static CACHED: Rc = { - primitive_identity_slug("type_declarer_qualified_names".to_string()) + primitive_identity_slug("decl_facts_at".to_string()) }; } CACHED.with(|c: &Rc| c.clone()) } -pub fn primitive_decl_facts_at() -> Rc { +pub fn primitive_export_signature_facts() -> Rc { thread_local! { static CACHED: Rc = { - primitive_identity_slug("decl_facts_at".to_string()) + primitive_identity_slug("export_signature_facts".to_string()) }; } CACHED.with(|c: &Rc| c.clone()) } -pub fn primitive_export_signature_facts() -> Rc { +pub fn primitive_data_decl_type_facts() -> Rc { thread_local! { static CACHED: Rc = { - primitive_identity_slug("export_signature_facts".to_string()) + primitive_identity_slug("data_decl_type_facts".to_string()) }; } CACHED.with(|c: &Rc| c.clone()) } -pub fn primitive_data_decl_type_facts() -> Rc { +pub fn primitive_type_declarer_qualified_names() -> Rc { thread_local! { static CACHED: Rc = { - primitive_identity_slug("data_decl_type_facts".to_string()) + primitive_identity_slug("type_declarer_qualified_names".to_string()) }; } CACHED.with(|c: &Rc| c.clone()) @@ -254,12 +254,6 @@ pub fn primitive_projection_roster() -> Rc>> { "decl_facts_at".to_string(), Rc::new(ProjectionFidelity::HostRealizedSeam), ), - primitive_projection_row( - primitive_type_declarer_qualified_names(), - "v2.std.decl_index".to_string(), - "type_declarer_qualified_names".to_string(), - Rc::new(ProjectionFidelity::HostRealizedSeam), - ), primitive_projection_row( primitive_export_signature_facts(), "v2.std.decl_index".to_string(), @@ -272,6 +266,12 @@ pub fn primitive_projection_roster() -> Rc>> { "data_decl_type_facts".to_string(), Rc::new(ProjectionFidelity::HostRealizedSeam), ), + primitive_projection_row( + primitive_type_declarer_qualified_names(), + "v2.std.decl_index".to_string(), + "type_declarer_qualified_names".to_string(), + Rc::new(ProjectionFidelity::HostRealizedSeam), + ), primitive_projection_row( primitive_concept_decl_facts(), "v2.std.concept_index".to_string(), diff --git a/src/v2/test/claim/generated/cross_representation_equality.dag b/src/v2/test/claim/generated/cross_representation_equality.dag index 8660d2d20d2..24576f08b0b 100644 --- a/src/v2/test/claim/generated/cross_representation_equality.dag +++ b/src/v2/test/claim/generated/cross_representation_equality.dag @@ -1,6 +1,8 @@ module v2.test.generated.cross_representation_equality -import v2.std.node_reflection { coproduct_arm_keys_checked } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import v2.std.compilers.lexing { symbol_intern_lexeme } +import v2.std.node_reflection { coproduct_arm_keys_at } // THE ROOTS THE REFLECTION READ CONSULTS, named so the population is re-derivable. data cross_representation_pool_roots: List = ["dag", "src/v2"] @@ -52,10 +54,18 @@ fn roster_covers_straddle(modeled: Symbol, native: Symbol) -> Bool { ) } -fn roster_covers_genuine_straddle(modeled: Symbol, native: Symbol) -> Bool { - (match coproduct_arm_keys_checked( +// THE MODELED TYPE IS CITED, NOT SPELLED, and Bool is why. `Bool` is declared as a closed coproduct +// in BOTH v2.std.logic and std.types, so a bare spelling cannot say which one this claim means -- +// and before the reflection cutover this check consumed whichever the interpreter's load order +// reached first while reading as though it had asked a determinate question. The guarded route +// refuses that spelling, correctly, so each call site now names its module. The bare symbol is +// derived from the citation rather than passed beside it, so the roster match and the arm-key read +// cannot drift onto two different names. +fn roster_covers_genuine_straddle(modeled_ref: DeclarationRef, native: Symbol) -> Bool { + let modeled = symbol_intern_lexeme(lexeme: modeled_ref.decl_name as String) + (match coproduct_arm_keys_at( pool_roots: cross_representation_pool_roots, - type_name: modeled + ref: modeled_ref ) { Rejected { diagnostics: _ } => false Accepted { value: arms, diagnostics: _ } => length(xs: arms) > 0 @@ -65,11 +75,25 @@ fn roster_covers_genuine_straddle(modeled: Symbol, native: Symbol) -> Bool { fn witness_cross_representation_roster_covers_bool() -> Bool { (length(xs: testgen_scheduled_cross_representation_equality_generators()) > 0) - && roster_covers_genuine_straddle(modeled: ^Bool, native: cross_repr_native_value_bool) + && roster_covers_genuine_straddle( + modeled_ref: DeclarationRef { + module_path: "v2.std.logic", + decl_name: "Bool", + field: WholeDeclaration + }, + native: cross_repr_native_value_bool + ) } fn witness_cross_representation_roster_covers_optional_null() -> Bool { - roster_covers_genuine_straddle(modeled: ^Optional, native: cross_repr_native_value_null) + roster_covers_genuine_straddle( + modeled_ref: DeclarationRef { + module_path: "v2.std.optional", + decl_name: "Optional", + field: WholeDeclaration + }, + native: cross_repr_native_value_null + ) } data witness_cross_representation_equality_is_equals: Bool = witness_cross_representation_claim_is_equals() diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag index 2a39c6e3b8c..ed0833b0a06 100644 --- a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -233,3 +233,33 @@ test fn cited_ambiguous_qualified_name_refuses_rather_than_taking_the_head() -> ) ) } + +// THE SPECIMEN A PRODUCTION CLAIM NOW DEPENDS ON, which is what makes this pair a regression control +// rather than a second copy of the Representation pair above. Bool is declared as a closed coproduct +// in BOTH v2.std.logic and std.types, and the cross-representation equality witness reads its arms +// to prove its own non-vacuity. Before the cutover that read consumed whichever declaration load +// order reached first; the guarded bare route refuses it, and the witness now cites v2.std.logic. +// These two claims are what say that citation is the right one and that the bare form is genuinely +// ambiguous -- if either flips, the production witness is resting on a spelling again. +test fn cited_bool_resolves_to_the_logic_module_arms() -> Bool { + outcome_arm_keys_are( + o: coproduct_arm_keys_at( + pool_roots: scoped_reflection_pool_roots, + ref: DeclarationRef { + module_path: "v2.std.logic", + decl_name: "Bool", + field: WholeDeclaration + } + ), + expected: [^True, ^False] + ) +} + +test fn bare_bool_spelling_refuses_as_ambiguous() -> Bool { + outcome_is_rejected( + o: coproduct_arm_keys_checked( + pool_roots: scoped_reflection_pool_roots, + type_name: ^Bool + ) + ) +} From 14142cdbae97743b314ef46b4351342e907933e4 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 14 Sep 2026 02:46:39 +0000 Subject: [PATCH 14/16] Repoint the consumer citations the seam deletion made stale review 65847 found two citations naming resolve_type_node -- the symbol THIS PR deletes -- and both sit on the artifacts that justify the new host seam rather than on incidental prose. The seam's own consumer annotation in v2.std.decl_index, and the consumer sentence inside gunbc.keyed_declaration_read_seed_growth, which is the row section 7 requires to carry a reason for the hand-Rust. A citation that does not resolve on the one artifact admitting the growth is the section 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 and resolve_type_node_at for a citation. TWO MORE OF THE SAME CLASS, FOUND BY SWEEPING RATHER THAN BY WAITING TO BE TOLD. Repairing only what a reviewer reports inherits the reviewer's blind spots, so every file this change touches was checked for references to the symbols it deletes. The conformance witness carried an annotation asserting that "the unguarded seam answers it today", present tense, about a seam this change removes. And it carried the sharper version of the same thing in a NAME: forked_spelling_answered_today_by_the_bare_seam_refuses_when_guarded asserted the existence of the bare seam in the identity of the claim itself. Section 3 makes the name the citation, so a stale name is worse than stale prose -- prose is read, a name is cited. It is now forked_spelling_refuses_when_guarded, which stays true after the thing it used to describe is gone. The surviving references to the deleted symbols are deliberate and past-tense: 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. Those describe what was removed and are the record; rewriting them would erase it. Corpus-wide, nothing imports a deleted symbol. Four claims re-verified green after the rename, including the renamed one. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- .../keyed_declaration_read_seed_growth.dag | 5 ++-- src/v2/std/decl_index.dag | 6 ++-- ...coped_type_reflection_conformance_test.dag | 30 +++++++++++-------- 3 files changed, 24 insertions(+), 17 deletions(-) diff --git a/dag/gunbc/keyed_declaration_read_seed_growth.dag b/dag/gunbc/keyed_declaration_read_seed_growth.dag index b71dbf771d5..a09cc17638a 100644 --- a/dag/gunbc/keyed_declaration_read_seed_growth.dag +++ b/dag/gunbc/keyed_declaration_read_seed_growth.dag @@ -68,8 +68,9 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } // it returns the MATCHING SET -- every qualified name declaring that bare spelling as a type -- and // never a first hit, because multiplicity is the whole answer. A host that chose among candidates // would be the bare-name identity defect its consumer exists to remove, one layer below the one -// being removed. Its consumer, v2.std.node_reflection resolve_type_node, refuses typed and located -// on multiplicity and names its candidates from what this returns. +// being removed. Its consumer is v2.std.node_reflection type_declarer_names, reached by both guarded +// routes -- resolve_type_node_checked and resolve_type_node_at -- each of which refuses typed and +// located on multiplicity and names its candidates from what this returns. // // It marshals no declaration nodes, which is where the population read's cost actually lived; it is // therefore cheaper than eval_decl_facts_at rather than merely narrower. diff --git a/src/v2/std/decl_index.dag b/src/v2/std/decl_index.dag index cf228f2b670..0d0f4f09610 100644 --- a/src/v2/std/decl_index.dag +++ b/src/v2/std/decl_index.dag @@ -44,8 +44,10 @@ fn decl_facts_at(pool_roots: List, qualified_name: String) -> List, bare_name: String) -> List { type_declarer_qualified_names(pool_roots: pool_roots, bare_name: bare_name) } diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag index ed0833b0a06..c95c2dd978b 100644 --- a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -35,9 +35,9 @@ fn outcome_is_accepted(o: Outcome) -> Bool { // THE DISCRIMINATING RED. `Representation` is declared as a closed coproduct in two modules of // this very pool -- `v2.lens.intent_linearity` and `v2.std.integer` -- with DISJOINT arm sets. -// The bare host seam answers it by first match over the interpreter's loaded modules, so before -// this change `coproduct_arm_keys` returned one of two different answers with no diagnostic and -// no way for a caller to know which. The claim is not that two declarations exist -- that is a +// The bare host seam THAT THIS CHANGE DELETES answered it by first match over the interpreter's +// loaded modules, so before this change the bare arm-key read returned one of two different answers +// with no diagnostic and no way for a caller to know which. The claim is not that two declarations exist -- that is a // fact about the corpus and would be a change detector. The claim is that the GUARDED route // REFUSES rather than answering, which is a fact about this module's behaviour and goes red the // moment the guard is removed or widened to a first match. @@ -156,16 +156,20 @@ test fn cited_forked_spelling_resolves_to_the_other_module_named() -> Bool { ) } -// THE SECOND SPECIMEN, AND THE ONE WHOSE CONTRAST IS ALREADY ENROLLED. UriScheme is declared in -// two modules of this pool -- a closed coproduct in extdeps.uri and a RECORD in v2.std.network -- -// and the unguarded seam answers it today rather than refusing: the enrolled claim -// v2.test.manual.coproduct_reflection_conformance witness_uri_scheme_reflected_arm_keys_are_non_empty asserts that -// coproduct_arm_keys(^UriScheme) returns a non-empty list, and it is green on main. So this pair -// is the case where the bare seam picks one of two declarations and says nothing, while the pair -// in the claims above is the case where it raises an untyped host error instead. Both are the same -// missing scope; only the guarded route below tells them apart from a caller's position, and the -// contrast claim is CITED rather than restated here so this module does not fork it. -test fn forked_spelling_answered_today_by_the_bare_seam_refuses_when_guarded() -> Bool { +// THE SECOND SPECIMEN, AND THE ONE THAT SHOWS THE TWO FAILURE SHAPES ARE ONE DEFECT. UriScheme is +// declared in two modules of this pool -- a closed coproduct in extdeps.uri and a RECORD in +// v2.std.network. Before this change the unguarded seam ANSWERED it rather than refusing, picking +// one of the two and saying nothing; the pair in the claims above is the case where the same seam +// raised an untyped host error instead. Both are the same missing scope, and only the guarded route +// tells them apart from a caller's position. +// +// The contrast is stated in the past tense deliberately. It used to be carried by an enrolled claim, +// v2.test.manual.coproduct_reflection_conformance +// witness_uri_scheme_reflected_arm_keys_are_non_empty, which asserted a non-empty arm list for a +// BARE UriScheme -- and this change rewrites that claim to cite extdeps.uri, because the bare +// spelling it rested on is exactly what is being removed. Citing it here as present evidence would +// name a claim whose subject this same PR changed. +test fn forked_spelling_refuses_when_guarded() -> Bool { outcome_is_rejected( o: coproduct_arm_keys_checked( pool_roots: scoped_reflection_pool_roots, From 4d59f06a02282864197d65a5db0da0a9c0ddafdf Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 14 Sep 2026 03:24:33 +0000 Subject: [PATCH 15/16] Read the keyed fact at the grain the guard measured review 65885: accept_sole_declaration proved uniqueness over one population and took its answer from another. Both callers establish multiplicity through type_declarer_qualified_names, whose host filters on name AND kind == TypeItem. accept_sole_declaration then read decl_facts_at, which filters on qualified name and nothing else, and took the head. Where a logical qualified name carries a type declaration AND a non-type one, the guard counts one, no ambiguity arm fires, and the answer is decided by whichever row canonical order put first -- the first-match-without-a-diagnostic shape this module exists to close, one filter down. FIXED BY CONSTRUCTION RATHER THAN 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, so there is no picking behaviour to test into existence. THE STATE IS UNPOPULATED TODAY AND THAT IS NOT THE REASON IT IS FIXED, which is worth separating because the two arguments point opposite ways. 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, and a refusal claim written against it would green by construction and be cited later as coverage -- the decoration DESIGN section 4b says to check for before writing the check. The mismatch is therefore removed at the read, where a later author adding the declaration that would populate it cannot reintroduce the defect. The existing qualified-grain RED stays what it always was: it covers the type/type collision, which is populated and refuses, and it was never evidence about this arm. Thirteen claims green by execution. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- src/v2/std/node_reflection.dag | 58 ++++++++++++++++++++++++++-------- 1 file changed, 45 insertions(+), 13 deletions(-) diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index c7602072b43..16258a10e0e 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -15,6 +15,7 @@ import v2.std.diagnostic { import v2.std.compilers.lexing { symbol_intern_lexeme, symbol_lexeme } import v2.std.decl_index { DeclFact, + TypeItem, decl_facts_at, logical_qualified_name_from_module, type_declarer_qualified_names @@ -138,30 +139,61 @@ fn scoped_type_reflection_diagnostic(type_name: Symbol, invariant: Symbol) -> Di // the v2.std.network RECORD counting as a candidate -- so uniqueness alone was never the contract // the annotations claimed. No new authority: node_is_coproduct is v2.std.node_query's existing // predicate, read from the node the keyed fact already carries. +// +// IT READS AT THE GRAIN ITS CALLER MEASURED, which review 65885 caught it not doing. Both callers +// establish multiplicity over a KIND-FILTERED census: type_declarer_qualified_names counts only +// declarations whose kind is TypeItem. decl_facts_at filters on qualified name and NOTHING ELSE, so +// taking its head would answer from whichever row the canonical order happened to put first +// whenever a logical qualified name carries a type declaration AND a non-type one -- the uniqueness +// would have been proven over one population and the answer taken from another, which is the +// first-match-without-a-diagnostic shape this module exists to close, one filter down. +// +// The repair is construction rather than a check: narrow the keyed read to the same kind the guard +// counted, and refuse unless exactly one row survives. There is no arm to test into existence +// because there is no arm that picks. +// +// THE STATE IS CURRENTLY UNPOPULATED AND THAT IS NOT WHY IT IS FIXED. Two declarations share one +// logical qualified name only when logical_qualified_name_from_module strips a leading `v2.` and +// both `v2.X` and `X` declare the name; searched across those twelve colliding module pairs, ZERO +// names are declared as a type on one side and a non-type on the other today. So no RED is +// authorable from the live corpus, and writing a refusal claim against it would be a decoration +// that greens by construction (DESIGN section 4b). The mismatch is removed at the read instead, +// where it cannot be reintroduced by someone later adding the declaration that would populate it. fn accept_sole_declaration( pool_roots: List, type_name: Symbol, sole_qualified_name: String ) -> Outcome { - match list_head(xs: decl_facts_at(pool_roots: pool_roots, qualified_name: sole_qualified_name)) { - HeadAbsent => - outcome_rejected( - d: scoped_type_reflection_diagnostic( - type_name: type_name, - invariant: ^type_declaration_absent - ) + let at_name = decl_facts_at(pool_roots: pool_roots, qualified_name: sole_qualified_name) + let type_rows = filter(xs: at_name, predicate: fn(fact) { fact.kind == TypeItem }) + if length(xs: type_rows) > 1 { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^cited_type_qualified_name_ambiguous ) - HeadFound { value: sole } => - if node_is_coproduct(node: sole.node) { - outcome_accepted(value: sole.node) - } else { + ) + } else { + match list_head(xs: type_rows) { + HeadAbsent => outcome_rejected( d: scoped_type_reflection_diagnostic( type_name: type_name, - invariant: ^type_spelling_is_not_a_closed_coproduct + invariant: ^type_declaration_absent ) ) - } + HeadFound { value: sole } => + if node_is_coproduct(node: sole.node) { + outcome_accepted(value: sole.node) + } else { + outcome_rejected( + d: scoped_type_reflection_diagnostic( + type_name: type_name, + invariant: ^type_spelling_is_not_a_closed_coproduct + ) + ) + } + } } } From 5209e3dc4f7f57bcb1dd0dde75fdb0333f24df03 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Mon, 14 Sep 2026 05:49:52 +0000 Subject: [PATCH 16/16] The surviving route takes the canonical names With the bare pair deleted, `_checked` had become a nickname for THE reflection route rather than a contrast with anything -- a second name for one concept (DESIGN section 3), and one that advertises an unchecked sibling a reader will go looking for and not find. The canonical spellings were freed by the deletion, so the route takes them: resolve_type_node_checked -> resolve_type_node, coproduct_arm_keys_checked -> coproduct_arm_keys, every caller updated in this commit. The _at citation routes keep their suffix, which still contrasts with something that exists. CONFIRMED BEFORE RENAMING, not assumed: the names are free at every layer that could bind them. No interpreter family arm, no roster row in gunbc.v1_interpreter_primitive_surface, no primitive identity or projection row matches either spelling -- all were deleted with the seam. So these are ordinary .dag declarations and nothing intercepts them by name, which is why the regeneration stays at first_generation_equal=true: the rename is invisible to the emitter. THE NAME IS REUSED ACROSS A DELETION, AND THE ANNOTATIONS NOW SAY SO. The module carries prose about the seam that was removed, written when that seam owned the spelling. After the rename those sentences read as though they described the function that now carries it -- one name, two meanings, which is the fork DESIGN section 3 forbids even when the reuse itself is legitimate. The annotations now name the removed thing as THE DELETED SEAM and state explicitly that every sentence about it is about what was removed and never about its replacement, and the prose describing the old behaviour moves to past tense. Mechanical otherwise: no semantic change, no signature change, no caller behaviour change. Thirteen conformance claims green by execution after the rename; regeneration at fixed point. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_015i8EEPjwJBh7CPJQr85Ldz --- .../keyed_declaration_read_seed_growth.dag | 2 +- src/v2/lens/affected_set.dag | 8 ++--- src/v2/std/decl_index.dag | 2 +- src/v2/std/node_reflection.dag | 29 ++++++++++--------- .../generated/coproduct_exhaustiveness.dag | 4 +-- .../coproduct_reflection_conformance_test.dag | 10 +++---- ...coped_type_reflection_conformance_test.dag | 18 ++++++------ .../wiring_liveness_test.dag | 4 +-- 8 files changed, 40 insertions(+), 37 deletions(-) diff --git a/dag/gunbc/keyed_declaration_read_seed_growth.dag b/dag/gunbc/keyed_declaration_read_seed_growth.dag index a09cc17638a..2f29e932d96 100644 --- a/dag/gunbc/keyed_declaration_read_seed_growth.dag +++ b/dag/gunbc/keyed_declaration_read_seed_growth.dag @@ -69,7 +69,7 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } // never a first hit, because multiplicity is the whole answer. A host that chose among candidates // would be the bare-name identity defect its consumer exists to remove, one layer below the one // being removed. Its consumer is v2.std.node_reflection type_declarer_names, reached by both guarded -// routes -- resolve_type_node_checked and resolve_type_node_at -- each of which refuses typed and +// routes -- resolve_type_node and resolve_type_node_at -- each of which refuses typed and // located on multiplicity and names its candidates from what this returns. // // It marshals no declaration nodes, which is where the population read's cost actually lived; it is diff --git a/src/v2/lens/affected_set.dag b/src/v2/lens/affected_set.dag index 37b1064f74a..722e81421f7 100644 --- a/src/v2/lens/affected_set.dag +++ b/src/v2/lens/affected_set.dag @@ -61,7 +61,7 @@ import v2.std.node { content_hash, } import v2.std.witness { Holds, Witness } -import v2.std.node_reflection { coproduct_arm_keys_checked } +import v2.std.node_reflection { coproduct_arm_keys } import v2.lens.application { AncestorFrame, AncestorWalk, collect_ancestor_frames, find_child_by_name, subterm_at, substitute_at } type Dag = Node @@ -1302,7 +1302,7 @@ data affected_set_reflect_repo_process_kind_type: Symbol = ^RepoProcessKind // rather than a bare list. They read type declarations by BARE SPELLING, and a bare spelling that // two modules declare cannot say which was meant -- the seam used to answer such a spelling from // whichever module the interpreter's load order reached first, silently, and this lens consumed -// that answer as the process universe. v2.std.node_reflection coproduct_arm_keys_checked refuses +// that answer as the process universe. v2.std.node_reflection coproduct_arm_keys refuses // typed and located instead, so the refusal has to arrive somewhere, and RepoProcessUniverse // already owns the vocabulary for it: UniverseIncomplete carrying a FailClosedReason. fn reflected_processes( @@ -1311,7 +1311,7 @@ fn reflected_processes( kind: RepoProcessKind ) -> Outcome> { bind_outcome( - o: coproduct_arm_keys_checked(pool_roots: pool_roots, type_name: type_name), + o: coproduct_arm_keys(pool_roots: pool_roots, type_name: type_name), f: fn(keys) { outcome_accepted( value: keys |> map(key => RepoProcess { kind: kind, identity: key }) @@ -1380,7 +1380,7 @@ fn repo_process_universe_from( pool_roots: List, processes: List ) -> RepoProcessUniverse { - match coproduct_arm_keys_checked( + match coproduct_arm_keys( pool_roots: pool_roots, type_name: affected_set_reflect_repo_process_kind_type ) { diff --git a/src/v2/std/decl_index.dag b/src/v2/std/decl_index.dag index 74b53fc2186..29577565345 100644 --- a/src/v2/std/decl_index.dag +++ b/src/v2/std/decl_index.dag @@ -44,7 +44,7 @@ fn decl_facts_at(pool_roots: List, qualified_name: String) -> List, bare_name: String) -> List { diff --git a/src/v2/std/node_reflection.dag b/src/v2/std/node_reflection.dag index 16258a10e0e..f0f9a2bc1c6 100644 --- a/src/v2/std/node_reflection.dag +++ b/src/v2/std/node_reflection.dag @@ -31,13 +31,16 @@ import v2.std.node_query { coproduct_arm_key_list_from_node, node_is_coproduct } // because an inhabitant of an arbitrary T is not derivable from anything the caller hands // it -- the answer is a fact about the running compiler's own source index. // -// resolve_type_node USED TO BE THE OTHER ONE, AND IS DELETED RATHER THAN RENAMED. It took a +// A SECOND HOST SEAM USED TO SIT BESIDE IT AND IS DELETED RATHER THAN RENAMED. It carried the +// spelling `resolve_type_node`, WHICH THE SCOPE-CARRYING FUNCTION BELOW NOW CARRIES -- the name +// is reused across that deletion, so every sentence here about the SEAM is about the thing that +// was removed and never about the function of the same name that replaced it. The seam took a // BARE type spelling, and its host arm answered by scanning the interpreter's loaded modules // and returning the FIRST item whose authored name matched -- so a spelling two modules // declare was answered from whichever load order reached first, with no diagnostic. That is // the DESIGN section 5 silent wrongness this module now exists to refuse. // -// It is deleted because after the cutover nothing consumed it: the guarded route establishes +// The seam is deleted because after the cutover nothing consumed it: the guarded route establishes // multiplicity and shape from the KEYED declaration read and returns the node that read // already carries, so it never needs the bare scan, and every other consumer was moved. A // rename would have kept a bare-spelling host route alive under a new name, which is exactly @@ -70,14 +73,14 @@ fn coproduct_nullary_inhabitants( ) } -// THE SCOPE-CARRYING ROUTE, AND WHY THE BARE ONE ABOVE CANNOT STAY THE ONLY ONE. +// THE SCOPE-CARRYING ROUTE, AND THE DEFECT IT REPLACED. // -// `resolve_type_node` keys on a BARE spelling. Its host arm (v4_bridge.resolve_type_node, -// realized by v1.stage0.coproduct_reflection type_item_by_name) answers it by scanning the +// THE DELETED SEAM of this name keyed on a BARE spelling. Its host arm (v4_bridge.resolve_type_node, +// realized by v1.stage0.coproduct_reflection type_item_by_name) answered it by scanning the // interpreter's loaded modules in order and returning the FIRST item whose authored name -// matches. When one spelling is declared as a closed coproduct in two modules, that scan -// returns whichever module the load order reached first -- a different arm set, with no -// diagnostic. It is DESIGN section 5 silent wrongness: not a refusal, a wrong answer that +// matched. When one spelling is declared as a closed coproduct in two modules, that scan +// returned whichever module the load order reached first -- a different arm set, with no +// diagnostic. It was DESIGN section 5 silent wrongness: not a refusal, a wrong answer that // typechecks. The corpus inhabits the invalid state today, so this is a live class and not a // hypothetical one; the discriminating pair enrolled against it is in // `v2.test.manual.scoped_type_reflection_conformance`. @@ -202,7 +205,7 @@ fn accept_sole_declaration( // (DESIGN section 5 -- a failure arm refuses, never widens). The single-row arm is the only one // that may reach the bare host seam, and it may do so precisely because uniqueness has been // established BEFORE the call rather than assumed by it. -fn resolve_type_node_checked(pool_roots: List, type_name: Symbol) -> Outcome { +fn resolve_type_node(pool_roots: List, type_name: Symbol) -> Outcome { let candidates = type_declarer_names(pool_roots: pool_roots, type_name: type_name) let n = length(xs: candidates) if n == 0 { @@ -238,12 +241,12 @@ fn resolve_type_node_checked(pool_roots: List, type_name: Symbol) -> Out } } -fn coproduct_arm_keys_checked( +fn coproduct_arm_keys( pool_roots: List, type_name: Symbol ) -> Outcome> { bind_outcome( - o: resolve_type_node_checked(pool_roots: pool_roots, type_name: type_name), + o: resolve_type_node(pool_roots: pool_roots, type_name: type_name), f: fn(node) { outcome_accepted(value: coproduct_arm_key_list_from_node(node: node)) } @@ -252,7 +255,7 @@ fn coproduct_arm_keys_checked( // THE ARM-KEY READING OF THE CITATION ROUTE, declared because the spelling route has one and a // caller that cites its module needs the same answer shape. It binds over resolve_type_node_at -// exactly as coproduct_arm_keys_checked binds over resolve_type_node_checked, so the two routes +// exactly as coproduct_arm_keys binds over resolve_type_node, so the two routes // differ in how the declaration is NAMED and in nothing else -- no second arm-key law. // Consumer: the conformance claims in v2.test.manual.scoped_type_reflection_conformance that read // a forked spelling through each of its declaring modules. @@ -269,7 +272,7 @@ fn coproduct_arm_keys_at( } // THE ROUTE THAT MAKES A CALLER SAY WHICH MODULE IT MEANT, and the one that can RESOLVE what the -// spelling route can only refuse. `resolve_type_node_checked` refuses an ambiguous spelling because +// spelling route can only refuse. `resolve_type_node` refuses an ambiguous spelling because // a bare name does not say which declaration was meant; a caller that legitimately means one of // several same-spelled types names it by citation instead, reusing `std.decl_ref` DeclarationRef -- // the corpus's existing carrier for "this declaration, in this module" -- so no second spelling of a diff --git a/src/v2/test/claim/generated/coproduct_exhaustiveness.dag b/src/v2/test/claim/generated/coproduct_exhaustiveness.dag index 588fad9404c..2307ad8b443 100644 --- a/src/v2/test/claim/generated/coproduct_exhaustiveness.dag +++ b/src/v2/test/claim/generated/coproduct_exhaustiveness.dag @@ -13,7 +13,7 @@ import v2.std.collection { List } import v2.std.diagnostic { Accepted, None, Outcome, Rejected } import v2.std.logic { Bool } import v2.std.node { Node, Symbol } -import v2.std.node_reflection { coproduct_arm_keys_checked } +import v2.std.node_reflection { coproduct_arm_keys } import v2.std.verification { ClaimAnchorKey, DiagnosticClaim, @@ -113,7 +113,7 @@ fn roster_covers_all_arms_of_roster( gens: List>, coproduct_type: Symbol ) -> Bool { - match coproduct_arm_keys_checked(pool_roots: pool_roots, type_name: coproduct_type) { + match coproduct_arm_keys(pool_roots: pool_roots, type_name: coproduct_type) { Rejected { diagnostics: _ } => false Accepted { value: arms, diagnostics: _ } => (length(xs: arms) > 0) diff --git a/src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag b/src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag index 9bc55f8b7da..a09289a1624 100644 --- a/src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/coproduct_reflection_conformance_test.dag @@ -10,7 +10,7 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } import v2.std.diagnostic { Accepted, Outcome, Rejected } import v2.std.node_reflection { coproduct_arm_keys_at, - coproduct_arm_keys_checked, + coproduct_arm_keys, coproduct_nullary_inhabitants } import v2.test.fixture.coproduct_reflection_generic_wrapper { @@ -99,7 +99,7 @@ test fn witness_nullary_reflection_accepts_imported_named_coproduct_through_gene Accepted { value: inhabitants, diagnostics: _ } => bag_eq( xs: imported_derive_trait_discriminants(inhabitants: inhabitants), - ys: conformance_arm_keys_or_empty(o: coproduct_arm_keys_checked(pool_roots: reflection_conformance_pool_roots, type_name: reflect_imported_derive_trait_type)), + ys: conformance_arm_keys_or_empty(o: coproduct_arm_keys(pool_roots: reflection_conformance_pool_roots, type_name: reflect_imported_derive_trait_type)), eq: symbol_eq ) Rejected { diagnostics: _ } => false @@ -132,8 +132,8 @@ test fn witness_nullary_reflection_rejects_requested_a_with_context_b() -> Bool test fn witness_connective_behavior_arm_sets_are_distinct() -> Bool { !bag_eq( - xs: conformance_arm_keys_or_empty(o: coproduct_arm_keys_checked(pool_roots: reflection_conformance_pool_roots, type_name: reflect_connective_type)), - ys: conformance_arm_keys_or_empty(o: coproduct_arm_keys_checked(pool_roots: reflection_conformance_pool_roots, type_name: reflect_behavior_type)), + xs: conformance_arm_keys_or_empty(o: coproduct_arm_keys(pool_roots: reflection_conformance_pool_roots, type_name: reflect_connective_type)), + ys: conformance_arm_keys_or_empty(o: coproduct_arm_keys(pool_roots: reflection_conformance_pool_roots, type_name: reflect_behavior_type)), eq: symbol_eq ) } @@ -165,7 +165,7 @@ test fn witness_behavior_nullary_inhabitant_set_matches_arm_keys() -> Bool { discriminant_of: behavior_discriminant ) { Accepted { value: inhabitants, diagnostics: _ } => - let keys = conformance_arm_keys_or_empty(o: coproduct_arm_keys_checked(pool_roots: reflection_conformance_pool_roots, type_name: reflect_behavior_type)) + let keys = conformance_arm_keys_or_empty(o: coproduct_arm_keys(pool_roots: reflection_conformance_pool_roots, type_name: reflect_behavior_type)) bag_eq( xs: nullary_inhabitant_discriminants(inhabitants: inhabitants), ys: keys, diff --git a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag index c95c2dd978b..b17e1e2ad40 100644 --- a/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag +++ b/src/v2/test/claim/manual/scoped_type_reflection_conformance_test.dag @@ -7,9 +7,9 @@ import v2.std.node { Symbol } import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } import v2.std.node_reflection { coproduct_arm_keys_at, - coproduct_arm_keys_checked, + coproduct_arm_keys, resolve_type_node_at, - resolve_type_node_checked + resolve_type_node } data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree @@ -43,7 +43,7 @@ fn outcome_is_accepted(o: Outcome) -> Bool { // moment the guard is removed or widened to a first match. test fn ambiguous_type_spelling_refuses_rather_than_first_matching() -> Bool { outcome_is_rejected( - o: coproduct_arm_keys_checked( + o: coproduct_arm_keys( pool_roots: scoped_reflection_pool_roots, type_name: ^Representation ) @@ -52,7 +52,7 @@ test fn ambiguous_type_spelling_refuses_rather_than_first_matching() -> Bool { test fn ambiguous_type_spelling_refuses_at_the_node_route_too() -> Bool { outcome_is_rejected( - o: resolve_type_node_checked( + o: resolve_type_node( pool_roots: scoped_reflection_pool_roots, type_name: ^Representation ) @@ -84,7 +84,7 @@ fn outcome_arm_keys_are(o: Outcome>, expected: List) -> Boo test fn unique_type_spelling_still_resolves() -> Bool { outcome_arm_keys_are( - o: coproduct_arm_keys_checked( + o: coproduct_arm_keys( pool_roots: scoped_reflection_pool_roots, type_name: ^Connective ), @@ -96,7 +96,7 @@ test fn unique_type_spelling_still_resolves() -> Bool { // what makes the zero case a refusal and not a divergent host call. test fn absent_type_spelling_refuses() -> Bool { outcome_is_rejected( - o: resolve_type_node_checked( + o: resolve_type_node( pool_roots: scoped_reflection_pool_roots, type_name: ^NoSuchTypeIsDeclaredAnywhereInThisPool ) @@ -171,7 +171,7 @@ test fn cited_forked_spelling_resolves_to_the_other_module_named() -> Bool { // name a claim whose subject this same PR changed. test fn forked_spelling_refuses_when_guarded() -> Bool { outcome_is_rejected( - o: coproduct_arm_keys_checked( + o: coproduct_arm_keys( pool_roots: scoped_reflection_pool_roots, type_name: ^UriScheme ) @@ -187,7 +187,7 @@ test fn forked_spelling_refuses_when_guarded() -> Bool { // refuses on its own arm, which is the contract this module's annotation already asserted. test fn unique_but_non_coproduct_spelling_refuses_rather_than_diverging() -> Bool { outcome_is_rejected( - o: coproduct_arm_keys_checked( + o: coproduct_arm_keys( pool_roots: scoped_reflection_pool_roots, type_name: ^DeclFact ) @@ -261,7 +261,7 @@ test fn cited_bool_resolves_to_the_logic_module_arms() -> Bool { test fn bare_bool_spelling_refuses_as_ambiguous() -> Bool { outcome_is_rejected( - o: coproduct_arm_keys_checked( + o: coproduct_arm_keys( pool_roots: scoped_reflection_pool_roots, type_name: ^Bool ) diff --git a/src/v2/test/lens_wiring_liveness/wiring_liveness_test.dag b/src/v2/test/lens_wiring_liveness/wiring_liveness_test.dag index c904eddf28f..abec649f9f7 100644 --- a/src/v2/test/lens_wiring_liveness/wiring_liveness_test.dag +++ b/src/v2/test/lens_wiring_liveness/wiring_liveness_test.dag @@ -3,7 +3,7 @@ module v2.test.lens_wiring_liveness.wiring_liveness_test import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } import v2.std.diagnostic { Accepted, Outcome, Rejected } -import v2.std.node_reflection { resolve_type_node_checked } +import v2.std.node_reflection { resolve_type_node } // READS THE LIVE TREE AS OF THE REFLECTION CUTOVER. The reflection read now names pool roots and @@ -71,7 +71,7 @@ data wl_reflection_pool_roots: List = ["dag", "src/v2"] // a confident false answer built on a question that was never settled. The refusal is surfaced as // an Outcome and the caller decides, rather than being flattened at the read. fn wl_reflected_dependency_kind() -> Outcome { - resolve_type_node_checked( + resolve_type_node( pool_roots: wl_reflection_pool_roots, type_name: ^DependencyKind )