Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
dab1d5f
XL-3: declaring-identity spelling carrier and verdict fold, file fixt…
Sep 12, 2026
417672f
XL-3: record measured collector coverage, not a silent empty ingest.
Sep 12, 2026
184225f
XL-3: wire the spelling census producer on the production ingest route.
Sep 12, 2026
ab415d9
XL-3: type-position kernel loss is not the call-lowering trigger.
Sep 12, 2026
1c98869
XL-3: the spelling census producer is wired, not held.
Sep 12, 2026
e14a7f9
XL-3: the usable class is a qualified cross-module mention, and it is…
Sep 12, 2026
dde7b6d
XL-3: drop dead fixture-path strings and the tautological coverage ch…
Sep 12, 2026
fc61bf6
XL-3: type-position fixtures observe; they are not held on a retracte…
Sep 12, 2026
2ce8184
XL-3: the miss is qualification, not type-position.
Sep 12, 2026
aaaada3
XL-3: name qualification, not lowering, on the producer comment.
Sep 12, 2026
b6a6c18
XL-3: IdentityUnbound is an index-path miss; frontiers are three capa…
Sep 12, 2026
f3ee6c8
XL-3: record the index-path Unbound cause on the producer.
Sep 12, 2026
b40d4e1
XL-3: measure a dotted field type as its own row, not merged with the…
Sep 12, 2026
45c5e32
XL-3: drop the Bool requalification helper and Symbol == alias.
Sep 12, 2026
8112d7c
XL-3: refuse a fabricated empty census on ingest Rejected.
Sep 13, 2026
46a93b1
XL-3: ingest committed fixture files; consume carrier_provenance.
Sep 13, 2026
0639108
XL-3: import filesystem_io so production-ingest witnesses can read fi…
Sep 13, 2026
fe4a4db
Merge origin/session/sharp-owl-21: inherit #11201 binding-frontier row.
Sep 13, 2026
463200b
XL-3: inherit #11201's spelling-derived DeclarationRef frontier.
Sep 13, 2026
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
2 changes: 1 addition & 1 deletion dag/gunbc/compiler_frontend_program_status.dag
Original file line number Diff line number Diff line change
Expand Up @@ -928,7 +928,7 @@ fn stage_status(s: NamespaceCutStage) -> MilestoneStanding {
)
StageXL3DeclaringIdentitySpelling =>
NotDerivable {
why: "no carrier censuses occurrences not yet spelled at their declaring identity. The wave wall's binding channel keys on leaf segments, deliberately invariant under requalification, so it cannot answer this either. Derivable once the spelling census exists." as NonEmptyStr,
why: "the spelling census producer exists (v2.compiler.declaring_identity_spelling_census spelling_census_from_ingest) over the production ingest route. Frontiers are separate capabilities: BARE value outside a call, parameter reference, and BARE type name in PARAMETER position reach; BARE type name in FIELD position does not (not a qualification fact -- measured by v2.test.claim.declaring_identity_spelling.production_ingest field_vs_parameter); names inside calls are missing (body-lowering, eager-raven / #11207); QUALIFIED/dotted references are missing in every position (dotted-reference gap, not lowering). A qualified field type is absent for both independent reasons and cannot discriminate. kernel Int has no corpus declaration. IdentityUnbound on a same-module ingest census row is an index-path probe, not a compiler fact -- enrolled control v2.test.claim.provenance.cross_file_provenance cfp_own_module_site binds on resolve_reference_provenance. Derivable once the producer answers over qualified mentions; restoring dotted will not restore bare field types. Stacks on #11201; waits on #11201 landing, not the merge freeze." as NonEmptyStr,
cause: needs(i: DeclaringIdentitySpellingCensus)
}
StageXL4ReferenceDerivedGraph =>
Expand Down
109 changes: 109 additions & 0 deletions dag/std/declaring_identity_spelling.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,109 @@
module std.declaring_identity_spelling

import std.types { Bool }
import std.decl_ref { DeclarationRef, decl_ref }
import std.dissolution { DissolutionCondition, retires_dissolution }
import v2.std.algebra { is_prefix_of, list_reverse }
import v2.std.qualified_name { QualifiedName }

// XL-3: whether one mention is spelled as the identity that declared its target.
// Canonical spelling is the SymbolIndex path (v2.std.symbol_index), the same qualified
// projection 03_resolve already uses. This module does not walk trees and does not collect
// sites. Producer consumes v2.compiler.reference_site_collector's
// ReferenceSiteCollection (.sites plus .unreadable_roots) and refuse to treat the
// census as complete unless reference_site_collection_is_total. Do not add a second
// collector or a parse-tree walker.
//
// WHAT PRODUCTION INGEST ACTUALLY SEES is measured by
// v2.test.claim.declaring_identity_spelling.production_ingest and
// v2.test.claim.namespace_xl0.call_argument_mention_survival:
// SURVIVES as sites (unusable for requalification): a BARE value not inside a
// call; a parameter reference; a BARE type name in PARAMETER position.
// DOES NOT: a BARE type name in FIELD position (separate from qualification);
// names inside calls (body-lowering, eager-raven / #11207);
// QUALIFIED/dotted references in any position (dotted-reference gap, not lowering);
// kernel types, which have no corpus declaration.
// A qualified field type is absent for two independent reasons and cannot
// discriminate either class.
// A bare same-module name resolves inside its own module, so it is not the XL-3
// population. The usable class is the qualified cross-module mention, absent with
// no call anywhere; a trigger naming only body-lowering (#11207) does not cover it.

// ResolvedSpelling.declaring is consumed TODAY from
// v2.compiler.repair_input_origin_roster carrier_provenance (RepairInputDeclared).
// That DeclarationRef is spelling-derived (owner-prefix drop + dotted render) and is a
// DECLARED FRONTIER on that producer -- repair_input_declared_binding_frontier_dissolve_on.
// This census inherits that frontier: when that row retires, this field is DERIVED from
// std.occurrence_binding OccurrenceBindingResult over ScopedOccurrenceRef (gunbc#11264's
// surviving authority) and must never be a third minted identity here. canonical is
// ProvenanceResolved.target and is unaffected.
data declaring_identity_spelling_declared_binding_frontier_dissolve_on: DissolutionCondition =
retires_dissolution(
ref: decl_ref(
module_path: "v2.compiler.repair_input_origin_roster",
decl_name: "repair_input_declared_binding_frontier_dissolve_on"
)
)

type UnresolvableCause
= IdentityAmbiguous
| IdentityUnbound
| IdentityOwnerless

type ResolvedPathVerdict
= SpelledCanonically
| SpelledShorter
| ResolvedAuthoredNotOnCanonicalPath

type DeclaringIdentitySpelling
= ResolvedSpelling {
authored: QualifiedName
declaring: DeclarationRef
canonical: QualifiedName
path_verdict: ResolvedPathVerdict
}
| UnresolvableSpelling {
authored: QualifiedName
cause: UnresolvableCause
}

fn authored_is_suffix_of_canonical(authored: QualifiedName, canonical: QualifiedName) -> Bool {
is_prefix_of(
prefix: list_reverse(xs: authored),
xs: list_reverse(xs: canonical),
eq: fn(a, b) { a == b }
)
}

fn resolved_path_verdict(authored: QualifiedName, canonical: QualifiedName) -> ResolvedPathVerdict {
if authored == canonical {
SpelledCanonically
} else if authored_is_suffix_of_canonical(authored: authored, canonical: canonical) {
SpelledShorter
} else {
ResolvedAuthoredNotOnCanonicalPath
}
}

fn declaring_identity_spelling_resolved(
authored: QualifiedName,
declaring: DeclarationRef,
canonical: QualifiedName
) -> DeclaringIdentitySpelling {
ResolvedSpelling {
authored: authored,
declaring: declaring,
canonical: canonical,
path_verdict: resolved_path_verdict(authored: authored, canonical: canonical)
}
}

fn declaring_identity_spelling_unresolvable(
authored: QualifiedName,
cause: UnresolvableCause
) -> DeclaringIdentitySpelling {
UnresolvableSpelling {
authored: authored,
cause: cause
}
}
11 changes: 11 additions & 0 deletions dag/test/claim/compiler_frontend_program_status_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ import gunbc.namespace_cut_stage {
StageXL0Denominator,
StageXL1BaselineCapture,
StageXL2RootDeletionRehearsal,
StageXL3DeclaringIdentitySpelling,
StageXL4ReferenceDerivedGraph,
StageAct0ActivationGate,
stage_prerequisites,
Expand Down Expand Up @@ -588,6 +589,16 @@ test fn xl0_is_not_derivable_and_awaits_the_repair_input_origin_producer() -> Bo
&& count(milestones_awaiting(i: RepairInputOriginRosterProducer)) == 0
}

// XL-3 stays NotDerivable while the usable class -- qualified cross-module
// mentions -- is invisible on the production ingest route. Bare PARAMETER
// type names are not that class: they reach. Bare FIELD type names are a
// fourth missing class, not a dotted case, and are also not the usable class.
test fn xl3_is_not_derivable_while_qualified_cross_module_mentions_are_invisible() -> Bool {
standing_is(want: ClassNotDerivable, s: stage_status(s: StageXL3DeclaringIdentitySpelling))
&& any(stages_awaiting(i: DeclaringIdentitySpellingCensus),
l => l == namespace_cut_stage_label(s: StageXL3DeclaringIdentitySpelling))
}

// F2 -- XL-1 IS THE CAPABILITY, THE BASELINE MILESTONE IS THE BASE-SPECIFIC FACT, AND THEY ARE NOT
// THE SAME QUESTION. XL-1 used to delegate to NamespaceBaselineObservationComplete outright, which
// made "the capture transaction can succeed" and "a capture has been taken against THIS base" one
Expand Down
145 changes: 145 additions & 0 deletions src/v2/compiler/declaring_identity_spelling_census.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,145 @@
module v2.compiler.declaring_identity_spelling_census

import std.algebra { Empty, FreeMonoid }
import std.declaring_identity_spelling {
DeclaringIdentitySpelling,
IdentityAmbiguous,
IdentityOwnerless,
IdentityUnbound,
declaring_identity_spelling_resolved,
declaring_identity_spelling_unresolvable
}
import std.repair_input_origin {
RepairInputDeclared,
RepairInputIdentityAbsent,
RepairInputIdentityAmbiguous,
RepairInputTargetWithoutDeclarationIdentity
}
import v2.std.algebra { fold_list, list_snoc_item }
import v2.std.diagnostic { Outcome, bind_outcome, outcome_accepted }
import v2.std.language_model { LanguageModel }
import v2.std.node { Node }
import v2.std.symbol_index { empty_symbol_index }
import v2.compiler.normalized_tree { normalized_tree_roots_to_nodes }
import v2.compiler.program_assembly { module_roots_from_source_root_ingest }
import v2.compiler.reference_site_collector {
UnreadableModuleRoot,
collect_reference_sites
}
import v2.compiler.repair_input_origin_roster { carrier_provenance }
import v2.compiler.resolution_provenance {
ProvenanceAmbiguous,
ProvenanceOwnerless,
ProvenanceResolved,
ProvenanceUnbound,
ResolutionProvenance,
answer_site,
module_roster_from_roots,
resolve_reference_sites
}
import v2.compiler.source_authority { SourceRootIngest }
import v2.compiler.symbol_index_fill { symbol_index_fill_module_roots }

// XL-3 PRODUCER: one mention, one spelling row, over the production ingest route.
//
// Route: v2.compiler.program_assembly module_roots_from_source_root_ingest
// -> v2.compiler.normalized_tree normalized_tree_roots_to_nodes
// -> v2.compiler.reference_site_collector collect_reference_sites
// -> v2.compiler.resolution_provenance resolve_reference_sites
// -> std.declaring_identity_spelling
//
// Consume ReferenceSiteCollection as a whole: .sites for the fold, .unreadable_roots
// carried through. Completeness is emptiness of that carried list (the same fact
// reference_site_collection_is_total names on the collection), never a second Bool
// helper and never inferred from a short row list.
//
// WHAT THIS ROUTE CANNOT SEE is measured, not speculated.
// IdentityUnbound on a same-module ingest census row is an INDEX-PATH probe:
// enrolled control cfp_own_module_site binds; ingest fill does not insert the
// data name at the collector site's parser-keyed path (same class as
// v2.test.claim.provenance.loaded_carrier_receipts receipt 2). Not a fact
// that v2 cannot compile a local name.

type DeclaringIdentitySpellingCensus {
rows: FreeMonoid<DeclaringIdentitySpelling>
unreadable_roots: FreeMonoid<UnreadableModuleRoot>
}

fn spelling_from_answer(answer: ResolutionProvenance) -> DeclaringIdentitySpelling {
let site = answer_site(answer: answer)
match carrier_provenance(answer: answer) {
RepairInputDeclared { declaring: declaring } =>
match answer {
ProvenanceResolved { site: _, target: target, owner: _ } =>
declaring_identity_spelling_resolved(
authored: site.spelling,
declaring: declaring,
canonical: target
)
ProvenanceOwnerless { site: _, target: _ } =>
declaring_identity_spelling_unresolvable(
authored: site.spelling,
cause: IdentityOwnerless
)
ProvenanceAmbiguous { site: _ } =>
declaring_identity_spelling_unresolvable(
authored: site.spelling,
cause: IdentityAmbiguous
)
ProvenanceUnbound { site: _ } =>
declaring_identity_spelling_unresolvable(
authored: site.spelling,
cause: IdentityUnbound
)
}
RepairInputTargetWithoutDeclarationIdentity { target_spelling: _ } =>
declaring_identity_spelling_unresolvable(
authored: site.spelling,
cause: IdentityOwnerless
)
RepairInputIdentityAmbiguous =>
declaring_identity_spelling_unresolvable(
authored: site.spelling,
cause: IdentityAmbiguous
)
RepairInputIdentityAbsent =>
declaring_identity_spelling_unresolvable(
authored: site.spelling,
cause: IdentityUnbound
)
}
}

fn spelling_census_over_roots(roots: FreeMonoid<Node>) -> DeclaringIdentitySpellingCensus {
let collected = collect_reference_sites(roots: roots)
DeclaringIdentitySpellingCensus {
rows: fold_list(
xs: resolve_reference_sites(
index: symbol_index_fill_module_roots(index: empty_symbol_index(), roots: roots),
roster: module_roster_from_roots(roots: roots),
sites: collected.sites
),
empty: Empty,
cons: fn(acc, answer) {
list_snoc_item(xs: acc, item: spelling_from_answer(answer: answer))
}
),
unreadable_roots: collected.unreadable_roots
}
}

fn spelling_census_from_ingest(
ingest: SourceRootIngest,
lm: LanguageModel
) -> Outcome<DeclaringIdentitySpellingCensus> {
bind_outcome(
o: module_roots_from_source_root_ingest(ingest: ingest, lm: lm),
f: fn(normalized) {
outcome_accepted(
value: spelling_census_over_roots(
roots: normalized_tree_roots_to_nodes(roots: normalized)
)
)
}
)
}
Loading