Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -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<DecimalDigit>, 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 <declaration-reference> 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: [],
}
4 changes: 2 additions & 2 deletions src/v2/compiler/03_resolve.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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)
}
}

Expand Down
93 changes: 71 additions & 22 deletions src/v2/std/qualified_name.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 }

Expand Down Expand Up @@ -290,12 +290,13 @@ fn qualified_name_from_node(root: Node) -> Outcome<QualifiedName> {
// 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(
Expand All @@ -307,25 +308,73 @@ 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<DecimalDigit>), 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: "<declaration-reference>")
}

// THE ONE PRODUCER OF THE MARKED CARRIER (consumed by v2.compiler.resolve resolved_reference_node).
// 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: OccurrenceSynthetic)
},
],
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<Node> {
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<QualifiedName> {
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()
}
}

Expand Down
Original file line number Diff line number Diff line change
@@ -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
}
)
}
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
)
Expand Down