From 54416b6a269823f31b1510191af7a1ac0475023f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 24 Sep 2026 09:04:13 +0000 Subject: [PATCH 1/2] Resolver-minted declaration references carry a marker the reader keys on, never the spine shape a literal also has Co-Authored-By: Claude Opus 5.5 (1M context) --- ...cognised_by_a_shape_a_literal_also_has.dag | 26 ++++++ src/v2/compiler/03_resolve.dag | 4 +- src/v2/std/qualified_name.dag | 90 ++++++++++++++----- .../declaration_reference_marker_test.dag | 86 ++++++++++++++++++ .../declaration_reference_form_test.dag | 4 +- 5 files changed, 185 insertions(+), 25 deletions(-) create mode 100644 dag/gunbc/recurring_failure_mode/declaration_reference_recognised_by_a_shape_a_literal_also_has.dag create mode 100644 src/v2/test/claim/qualified_name/declaration_reference_marker_test.dag diff --git a/dag/gunbc/recurring_failure_mode/declaration_reference_recognised_by_a_shape_a_literal_also_has.dag b/dag/gunbc/recurring_failure_mode/declaration_reference_recognised_by_a_shape_a_literal_also_has.dag new file mode 100644 index 00000000000..06734a1b286 --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/declaration_reference_recognised_by_a_shape_a_literal_also_has.dag @@ -0,0 +1,26 @@ +module gunbc.recurring_failure_mode.declaration_reference_recognised_by_a_shape_a_literal_also_has + +import std.types { NonEmptyStr } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data declaration_reference_recognised_by_a_shape_a_literal_also_has: RecurringFailureMode = RecurringFailureMode { + identity: "declaration_reference_recognised_by_a_shape_a_literal_also_has" as NonEmptyStr, + + receipts: [ + "**a declaration reference is recognised by a shape a literal also has** (INVALID STATE: v2.std.qualified_name declaration_reference_path_optional answered 'this node is a resolved reference to a corpus declaration' from the SHAPE of the node alone -- a TypeNode Conj in the fold_list head/tail spine -- and that shape is not owned by references. An integer literal lowers to the same cons list of digit atoms (v2.std.integer FreeMonoid, grounded by #12197), so the literal 606060 read as the declaration path integer_tag_digit_6.integer_tag_digit_0.integer_tag_digit_6... on fixtures/native_cli_door.", + + "HARM: the reader's contract -- a declaration reference reads as its path or as nothing -- was false for every value whose carrier is a cons list, and v2.compiler.resolution_provenance resolution_provenance_second_resolver_dissolve_on routes every consumer of declaring paths to this reader, so infer, eval, translate and reference_closure each inherited the ambiguity silently. Found by stern-moth-549 through #12218's emit-build, whose consumer attributed a literal to a module; that PR interim-guarded its one consumer by SymbolIndex membership (validation standing where construction was available, DESIGN section 5).", + + "DISTINGUISHING FACTS: the tell is a recogniser keyed on a generic container shape (a cons list, a record, a pair) for a fact only one producer establishes. Such a recogniser is correct only while no other producer builds that shape, which is not a time-stable fact: every new grounding of a value as a list (here the integer payload) silently widens its accepted set.", + + "RUNG FOUND AT: OUTSIDE THE LADDER -- silent wrongness; the literal was accepted as a reference and nothing refused.", + + "REPAIR AND RUNG CLAIMED: the resolver now mints the reference through v2.std.qualified_name declaration_reference_node, a one-edge Conj whose only label is the marker symbol declaration_reference_marker, over the spine; declaration_reference_path_optional reads the marker and never the shape. The marker's lexeme is not an identifier in the dag grammar, so no authored record field, binder or name can spell it: for the colliding populations the corpus can author (literals, records, dotted mentions) the confusion is unwritable, rung 4 at the surface-source subject grain. A hand-built Node in .dag code can still construct the marker by calling the constructor, so the Node-construction subject is not claimed above 3.", + + "EVIDENCE: v2.test.claim.qualified_name.declaration_reference_marker -- declaration_reference_integer_literal_reads_as_no_reference (the 606060 specimen through the dag literal producer; red on the shape-keyed reader), declaration_reference_marked_reference_reads_its_exact_path, declaration_reference_unmarked_spine_reads_as_no_reference (the drop-the-marker mutation), declaration_reference_identifier_labelled_wrapper_reads_as_no_reference. Real-route inhabitance: v2.test.claim.namespace_xl0.cross_module_reference_resolution reads the resolver's output through the same reader.", + + "CEILING: 4 at the surface-source grain (reached). NEXT-RUNG TRIGGER for the Node-construction grain: a constructor-visibility capability that confines declaration_reference_node to v2.compiler.resolve; none exists in the substrate today." + ], + + evidence: [], +} diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index cb57a0bbdd0..08f8beaa1bd 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -61,7 +61,7 @@ import v2.std.qualified_name { qualified_name_from_node, qualified_name_last_segment, qualified_name_snoc, - qualified_name_spine_node + declaration_reference_node } import v2.std.resolution_policy { ImportScoped, @@ -617,7 +617,7 @@ fn resolved_reference_identity(ctx: ResolveContext, path: QualifiedName) -> Reso fn resolved_reference_node(identity: ResolvedReferenceIdentity, occurrence_id: NodeOccurrenceIdentity) -> Node { match identity { ResolvedToKernelSymbol { symbol: symbol } => canonical_atom(identity: symbol, occurrence_id: occurrence_id) - ResolvedToDeclaration { path: path } => qualified_name_spine_node(qn: path, occurrence_id: occurrence_id) + ResolvedToDeclaration { path: path } => declaration_reference_node(qn: path, occurrence_id: occurrence_id) } } diff --git a/src/v2/std/qualified_name.dag b/src/v2/std/qualified_name.dag index 1bba94e930c..b75424880d0 100644 --- a/src/v2/std/qualified_name.dag +++ b/src/v2/std/qualified_name.dag @@ -290,12 +290,13 @@ fn qualified_name_from_node(root: Node) -> Outcome { // reads it; this is its inverse, and the two are kept in one module so that no producer can spell // the spine with labels the reader does not accept (the label set is fold_list_node's, consumed // through qn_spine_role -- never re-spelled here). Body lowering produces the spine for an authored -// dotted reference before resolution; resolution produces it AFTER, as the resolved carrier of a -// corpus declaration reference (v2.compiler.resolve resolved_reference_node): the reference to a +// dotted reference before resolution; resolution produces it AFTER, under the marker of +// declaration_reference_node below, as the resolved carrier of a corpus declaration reference +// (v2.compiler.resolve resolved_reference_node): the reference to a // declaration is the declaration's containment path, which is the one identity the index, the // candidate rows, DeclarationLocus and DeclarationRef already agree on (DESIGN section 3: name the // symbol the containment tree already names, never a second scheme beside it). A resolved body -// therefore holds a corpus declaration reference as a spine and never as a bare Atom, and a bare +// therefore holds a corpus declaration reference as a marked spine and never as a bare Atom, and a bare // Atom after resolution is a kernel canonical symbol, a literal, or a frame-local binder. fn qualified_name_spine_node(qn: QualifiedName, occurrence_id: NodeOccurrenceIdentity) -> Node { let spine = fold_list_node( @@ -307,25 +308,72 @@ fn qualified_name_spine_node(qn: QualifiedName, occurrence_id: NodeOccurrenceIde node_with_occurrence_id(kind: spine.kind, children: spine.children, occurrence_id: occurrence_id) } -// A DECLARATION REFERENCE READS AS ITS PATH OR AS NOTHING. The reader accepts only a Conj root in -// the spine shape, so a bare Atom is never a reference and a consumer asking "is this node a -// resolved reference to a corpus declaration" gets a decidable answer from the shape alone, before -// it reads the Conj as a record. A one-segment spine IS a reference -- a declaration in a root that -// names no module has a one-segment path -- so a reference is never narrowed to the multi-segment -// case. The empty spine, which is also the empty record, is refused by the shape gate itself (it -// has no children where the gate demands two) and answers Absent from the outer arm; every spine -// the gate admits reaches QnFoldDone through QnSpineHead, whose target must be an Atom, so an -// accepted fold carries at least one segment and a length guard here would be dead. A well-formed -// spine whose fold refuses is a malformed node, not a reference, and also answers Absent so that -// the consumer's own arm decides it. +// A DECLARATION REFERENCE IS MARKED, NOT RECOGNISED BY SHAPE. The spine above is a cons list, and a +// cons list is not only a path: an integer literal lowers to the same list of digit atoms +// (v2.std.integer, FreeMonoid), so a reader keyed on the spine shape read the literal +// 606060 as the "path" integer_tag_digit_6.integer_tag_digit_0... (gunbc.recurring_failure_mode +// declaration_reference_recognised_by_a_shape_a_literal_also_has). The resolver therefore mints the +// reference as a one-edge Conj whose only label is this marker, over the spine. The marker's lexeme +// is not an identifier in the dag grammar, so no authored record field, binder or name can carry it: +// a record literal lowers to a Conj whose labels are the author's field identifiers, and this label +// is none of them. Only a producer that calls declaration_reference_node writes it. +fn declaration_reference_marker() -> Symbol { + symbol_intern_lexeme(lexeme: "") +} + +// THE ONE PRODUCER OF THE MARKED CARRIER (consumed by v2.compiler.resolve resolved_reference_node). +// The occurrence stays on the marker node, which is the node that stands where the reference stood. +fn declaration_reference_node(qn: QualifiedName, occurrence_id: NodeOccurrenceIdentity) -> Node { + node_with_occurrence_id( + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: declaration_reference_marker() }, + target: qualified_name_spine_node(qn: qn, occurrence_id: occurrence_id) + }, + ], + occurrence_id: occurrence_id + ) +} + +// A DECLARATION REFERENCE READS AS ITS PATH OR AS NOTHING, keyed on the marker and never on the +// spine shape: a bare spine -- an authored dotted mention before resolution, an integer literal, +// any other cons list -- answers Absent. Under the marker, a spine whose fold refuses is a malformed +// node, not a reference, and also answers Absent so that the consumer's own arm decides it. +fn declaration_reference_spine_optional(node: Node) -> Optional { + match node.kind { + TypeNode { connective: Conj } => + if count(node.children) == 1 { + fold(node.children, init: optional_absent(), f: fn(acc, edge) { + match edge.label { + Named { name: label } => + if symbol_eq(a: label, b: declaration_reference_marker()) { + optional_present(value: edge.target) + } else { + acc + } + _ => acc + } + }) + } else { + optional_absent() + } + _ => optional_absent() + } +} + fn declaration_reference_path_optional(node: Node) -> Optional { - if qualified_name_spine_shape_present(root: node) { - match qualified_name_from_node(root: node) { - Accepted { value: qn, diagnostics: _ } => optional_present(value: qn) - Rejected { diagnostics: _ } => optional_absent() - } - } else { - optional_absent() + match declaration_reference_spine_optional(node: node) { + Present { value: spine } => + if qualified_name_spine_shape_present(root: spine) { + match qualified_name_from_node(root: spine) { + Accepted { value: qn, diagnostics: _ } => optional_present(value: qn) + Rejected { diagnostics: _ } => optional_absent() + } + } else { + optional_absent() + } + Absent => optional_absent() } } diff --git a/src/v2/test/claim/qualified_name/declaration_reference_marker_test.dag b/src/v2/test/claim/qualified_name/declaration_reference_marker_test.dag new file mode 100644 index 00000000000..2d35babae4e --- /dev/null +++ b/src/v2/test/claim/qualified_name/declaration_reference_marker_test.dag @@ -0,0 +1,86 @@ +module v2.test.claim.qualified_name.declaration_reference_marker + +import std.occurrence_identity { OccurrenceSynthetic } +import v2.extdeps.languages.dag { dag_int_literal_node_from_lexeme } +import v2.std.diagnostic { Accepted, Rejected } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.logic { Bool } +import v2.std.node { Conj, Edge, Named, Node, TypeNode, node_subtree_nodes } +import v2.std.optional { Absent, Present } +import v2.std.qualified_name { + declaration_reference_node, + declaration_reference_path_optional, + qualified_name_from_dotted_string, + qualified_name_spine_node +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A DECLARATION REFERENCE IS READ BY ITS MARKER, NEVER BY ITS SHAPE (v2.std.qualified_name +// declaration_reference_path_optional; gunbc.recurring_failure_mode +// declaration_reference_recognised_by_a_shape_a_literal_also_has). The inputs are SUPPLIED at the +// reader's boundary: the literal through the dag language's own literal producer, the reference +// through the one constructor the resolver mints with. The inhabitance claim that the real +// resolver emits the marked carrier is v2.test.claim.namespace_xl0.cross_module_reference_resolution. + +fn drm_path_reads_absent(n: Node) -> Bool { + match declaration_reference_path_optional(node: n) { + Present { value: _ } => false + Absent => true + } +} + +// THE SPECIMEN (red on main, whose reader keyed on the spine shape): the literal 606060 lowers to +// a cons list of digit atoms under its magnitude field, and that node read as the path +// integer_tag_digit_6.integer_tag_digit_0... Every node of the literal is asked, as a consumer +// walking a resolved body asks it. +test fn declaration_reference_integer_literal_reads_as_no_reference() -> Bool { + match dag_int_literal_node_from_lexeme(lexeme: "606060", occurrence_id: OccurrenceSynthetic) { + Accepted { value: literal, diagnostics: _ } => + fold(node_subtree_nodes(root: literal), init: true, f: fn(acc, n) { + acc && drm_path_reads_absent(n: n) + }) + Rejected { diagnostics: _ } => false + } +} + +test fn declaration_reference_marked_reference_reads_its_exact_path() -> Bool { + let path = qualified_name_from_dotted_string(dotted: "v2.test.drm_provider.DrmDeclared") + match declaration_reference_path_optional( + node: declaration_reference_node(qn: path, occurrence_id: OccurrenceSynthetic) + ) { + Present { value: read } => read == path + Absent => false + } +} + +// THE MUTATION: the same path with the marker dropped -- the bare spine the resolver used to mint -- +// is not a reference. +test fn declaration_reference_unmarked_spine_reads_as_no_reference() -> Bool { + drm_path_reads_absent( + n: qualified_name_spine_node( + qn: qualified_name_from_dotted_string(dotted: "v2.test.drm_provider.DrmDeclared"), + occurrence_id: OccurrenceSynthetic + ) + ) +} + +// AN AUTHORED ONE-FIELD RECORD OVER A SPINE is not a reference either: its label is an identifier, +// and the marker's lexeme is not one. +test fn declaration_reference_identifier_labelled_wrapper_reads_as_no_reference() -> Bool { + drm_path_reads_absent( + n: Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: ^declaration_reference }, + target: qualified_name_spine_node( + qn: qualified_name_from_dotted_string(dotted: "v2.test.drm_provider.DrmDeclared"), + occurrence_id: OccurrenceSynthetic + ) + }, + ], + occurrence_id: OccurrenceSynthetic + } + ) +} diff --git a/src/v2/test/claim/translate/declaration_reference_form_test.dag b/src/v2/test/claim/translate/declaration_reference_form_test.dag index 644beda0384..2661b374361 100644 --- a/src/v2/test/claim/translate/declaration_reference_form_test.dag +++ b/src/v2/test/claim/translate/declaration_reference_form_test.dag @@ -19,7 +19,7 @@ import v2.std.diagnostic { Accepted, NonEmptyDiagnostics, Outcome, Rejected } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import v2.std.logic { Bool } import v2.std.node { Atom, Node, Symbol, TypeNode } -import v2.std.qualified_name { qualified_name_from_dotted_string, qualified_name_spine_node } +import v2.std.qualified_name { declaration_reference_node, qualified_name_from_dotted_string } import v2.std.text { String } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -47,7 +47,7 @@ data drf_target: TargetModel = rust_sg2_type_expression_projection_target_model( data drf_expected_spelling: String = "crate::v2_test_drf_provider::DrfDeclared" fn drf_reference_spine() -> Node { - qualified_name_spine_node( + declaration_reference_node( qn: qualified_name_from_dotted_string(dotted: "v2.test.drf_provider.DrfDeclared"), occurrence_id: OccurrenceSynthetic ) From 4fdf1b266892401b2d6192b6939c6783a17a387f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 24 Sep 2026 10:09:10 +0000 Subject: [PATCH 2/2] declaration_reference_node: the spine under the marker is synthetic, so one occurrence is carried by one node Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/std/qualified_name.dag | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/v2/std/qualified_name.dag b/src/v2/std/qualified_name.dag index b75424880d0..002440cfd41 100644 --- a/src/v2/std/qualified_name.dag +++ b/src/v2/std/qualified_name.dag @@ -27,7 +27,7 @@ import v2.std.optional { } import v2.std.compilers.lexing { symbol_intern_lexeme, symbol_lexeme } import v2.std.logic { Bool } -import std.occurrence_identity { NodeOccurrenceIdentity } +import std.occurrence_identity { NodeOccurrenceIdentity, OccurrenceSynthetic } import v2.std.node { Atom, Conj, Edge, EdgeLabel, Named, Node, NodeFold, Positional, Symbol, TypeNode, fold_node, node_synthetic, node_with_occurrence_id, symbol_eq } import v2.std.text { String } @@ -322,14 +322,15 @@ fn declaration_reference_marker() -> Symbol { } // THE ONE PRODUCER OF THE MARKED CARRIER (consumed by v2.compiler.resolve resolved_reference_node). -// The occurrence stays on the marker node, which is the node that stands where the reference stood. +// The occurrence stays on the marker node alone, which is the node that stands where the reference +// stood; the spine under it is synthetic, so one source occurrence is carried by exactly one node. fn declaration_reference_node(qn: QualifiedName, occurrence_id: NodeOccurrenceIdentity) -> Node { node_with_occurrence_id( kind: TypeNode { connective: Conj }, children: [ Edge { label: Named { name: declaration_reference_marker() }, - target: qualified_name_spine_node(qn: qn, occurrence_id: occurrence_id) + target: qualified_name_spine_node(qn: qn, occurrence_id: OccurrenceSynthetic) }, ], occurrence_id: occurrence_id