From 2c5750a5d6baea2813a14ce89b9c04eefcfae145 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 21:25:56 +0000 Subject: [PATCH 1/3] WIP: Section 5 de-fork manager toward one dsl std authority: STEP 1 FIRST and --- src/v2/compiler/03_name_resolve.dag | 94 +++++------ src/v2/std/cross_tree/resolution.dag | 227 +++++++++++++++++++-------- 2 files changed, 209 insertions(+), 112 deletions(-) diff --git a/src/v2/compiler/03_name_resolve.dag b/src/v2/compiler/03_name_resolve.dag index c01a70c9503..c72c0a91a5f 100644 --- a/src/v2/compiler/03_name_resolve.dag +++ b/src/v2/compiler/03_name_resolve.dag @@ -55,16 +55,16 @@ import v2.std.passing_candidate_fold { PassingCandidateFold } import v2.std.cross_tree.import_model { - CrossTreeAdmitted, - CrossTreeDenied, - FundamentalityUnknown, - SourceRootRef, - TreeFundamentalityOrder + SourceRootRef } import v2.std.cross_tree.resolution { - cross_tree_import_admitted_qualified, - cross_tree_import_is_same_tree, - source_root_set_from_module_roots + EdgeCrossAdmitted, + EdgeCrossAmbiguous, + EdgeCrossDenied, + EdgeNormalResolution, + SourceRootIndex, + cross_tree_edge_decision, + source_root_index_empty } import v2.std.qualified_name { QualifiedName, @@ -424,12 +424,28 @@ fn admit_import_root_find( } +fn admit_import_visible_entry( + roots: FreeMonoid, + import_edge: Import, + state: AdmissionState +) -> AdmissionState { + admit_import_root_find( + found: module_root_find( + roots: roots, + name: import_edge.target + ), + origin: import_edge.target, + state: state + ) +} + + fn admit_import_entry( roots: FreeMonoid, import_edge: Import, state: AdmissionState, subject_qn: QualifiedName, - order: TreeFundamentalityOrder, + index: SourceRootIndex, active_roots: FreeMonoid ) -> AdmissionState { match state { @@ -442,36 +458,24 @@ fn admit_import_entry( diagnostics: resolve_diagnostics(reason: ^resolve_import_not_visible) } ImportVisible => - if cross_tree_import_is_same_tree(from_qn: subject_qn, to_qn: import_edge.target) { - admit_import_root_find( - found: module_root_find( - roots: roots, - name: import_edge.target - ), - origin: import_edge.target, - state: state - ) - } else { - match cross_tree_import_admitted_qualified( - from_qn: subject_qn, - to_qn: import_edge.target, - roots: active_roots, - order: order - ) { - CrossTreeAdmitted => - admit_import_root_find( - found: module_root_find( - roots: roots, - name: import_edge.target - ), - origin: import_edge.target, - state: state - ) - CrossTreeDenied { reason: _ } => - AdmissionRejected { - diagnostics: resolve_diagnostics(reason: ^resolve_cross_tree_import_denied) - } - } + match cross_tree_edge_decision( + index: index, + from_qn: subject_qn, + to_qn: import_edge.target, + active_roots: active_roots + ) { + EdgeNormalResolution => + admit_import_visible_entry(roots: roots, import_edge: import_edge, state: state) + EdgeCrossAdmitted => + admit_import_visible_entry(roots: roots, import_edge: import_edge, state: state) + EdgeCrossDenied => + AdmissionRejected { + diagnostics: resolve_diagnostics(reason: ^resolve_cross_tree_import_denied) + } + EdgeCrossAmbiguous => + AdmissionRejected { + diagnostics: resolve_diagnostics(reason: ^resolve_cross_tree_import_ambiguous) + } } } } @@ -483,7 +487,7 @@ fn admit_imports( imports: FreeMonoid, state: AdmissionState, subject_qn: QualifiedName, - order: TreeFundamentalityOrder, + index: SourceRootIndex, active_roots: FreeMonoid ) -> AdmissionState { fold_list( @@ -495,7 +499,7 @@ fn admit_imports( import_edge: import_edge, state: acc, subject_qn: subject_qn, - order: order, + index: index, active_roots: active_roots ) } @@ -523,7 +527,7 @@ fn namespace_for_subject( lm: LanguageModel, roots: FreeMonoid, admission: Admission, - order: TreeFundamentalityOrder, + index: SourceRootIndex, active_roots: FreeMonoid ) -> Outcome { match validate_module_roots(roots: roots) { @@ -549,7 +553,7 @@ fn namespace_for_subject( state: admission_initial(base: base) ), subject_qn: admission.subject.name, - order: order, + index: index, active_roots: active_roots ) { AdmissionAccepted { bindings: b, origins: _ } => @@ -585,14 +589,14 @@ fn resolve_with_admission_policy( lm: LanguageModel, roots: FreeMonoid, admission: Admission, - order: TreeFundamentalityOrder, + index: SourceRootIndex, active_roots: FreeMonoid ) -> Outcome { match namespace_for_subject( lm: lm, roots: roots, admission: admission, - order: order, + index: index, active_roots: active_roots ) { Accepted { value: admitted, diagnostics: namespace_diag } => diff --git a/src/v2/std/cross_tree/resolution.dag b/src/v2/std/cross_tree/resolution.dag index 1a2a2a33203..85cd9f20f90 100644 --- a/src/v2/std/cross_tree/resolution.dag +++ b/src/v2/std/cross_tree/resolution.dag @@ -1,29 +1,40 @@ // src/v2/std/cross_tree/resolution.dag // -// Route C Phase B — QualifiedName-grounded cross-tree resolution helpers. -// Bridges name_resolve admission to import_model without String module-path interim. -// Consumers: v2.compiler.name_resolve (namespace_for_subject cross-tree gate). +// Route C Phase C — grounded cross-tree resolution helpers. +// Bridges name_resolve admission to import_model using a QualifiedName -> SourceRootRef +// index built from the host-tagged ingest (DagSourceReadWitness.source_root, PR-A). +// Consumers: v2.compiler.name_resolve (admit_import_entry cross-tree gate), +// v2.compiler.program_assembly (index construction during the assembly fold). // -// SCAFFOLD — feature:route-c-cross-tree-resolution-qn-fallback -// dissolve-on (grounded source_root at ingest): add source_root: SourceRootRef to -// DagSourceReadWitness (src/v2/compiler/source_authority.dag); host tags by which -// --source-root the file came from; delete source_root_ref_from_qualified_name and -// source_root_set_from_module_roots QN-prefix fallback. -// ACTIVATION GATE (hard): supplying a non-Unknown TreeFundamentalityOrder for real -// compilation (cross-tree direction-flip) MUST NOT land until grounded source_root -// tagging replaces this fallback. INERT Unknown-default is allowed; relying on QN-prefix -// for admitted cross-tree edges is forbidden (DESIGN §4). +// GROUNDED (§4): per-edge source-tree identity comes from filesystem-truth provenance +// (which --source-root each file was read from), NOT a QualifiedName-prefix guess. The +// prior QN-prefix fallback (source_root_ref_from_qualified_name / +// source_root_set_from_module_roots) is DELETED — it mis-tagged the 9 src/v2 files that +// declare non-`v2.`-prefixed modules (extdeps.shell, bisect.add, extdeps.fixture.*, +// test.claim.fold_list_generic_instantiation) as DslTree, which is unsound, not merely +// impure. ACTIVATION (the prior header's hard gate): cross-tree imports are now admitted +// on grounded provenance, so the direction is live for real compilation. +// +// Fundamentality is grounded as a tree-pair relation (tree_fundamentality_order), NOT a +// caller-supplied global scalar: dsl is the single authority v2 builds on, so a v2->dsl +// import targets the strictly-more-fundamental tree (admit, layer permitting) and a dsl->v2 +// import inverts fundamentality (deny). A global `MoreFundamental` would fail OPEN on a +// dsl->v2.std peer edge (layer-direction holds at equal ordinals); deriving the order per +// pair closes that inversion (§5 fail-closed). module v2.std.cross_tree.resolution import v2.std.algebra { Cons, Empty, FreeMonoid, fold_list } import v2.std.cross_tree.import_model { + CoFundamental, CrossTreeAdmitted, - CrossTreeAdmissionVerdict, CrossTreeDenied, CrossTreeImport, DslTree, + LessFundamental, + MoreFundamental, SourceRootRef, + SourceRootSet, TreeFundamentalityOrder, V2Tree, cross_tree_import_admitted, @@ -38,33 +49,103 @@ import v2.std.layer { LayerPrefixWorkflow } import v2.std.logic { Bool } -import v2.std.qualified_name { QualifiedName, QnCons, QnEmpty } +import v2.std.qualified_name { QualifiedName, QnCons, QnEmpty, qualified_name_eq } import v2.std.text { String } -// ── Source-tree tagging (QN-prefix fallback — see module header dissolve-on) ─── +// ── Grounded source-root index (QualifiedName -> SourceRootRef) ───────────────── +// +// Built during program assembly: each parsed module root's QualifiedName is paired with +// the source_root its DagSourceReadWitness carried (the host filesystem truth). This is the +// §4-grounded replacement for the deleted QN-prefix guess. -// 🟡 SCAFFOLD — feature:route-c-cross-tree-resolution-qn-fallback — bind dissolve-on above. -// KNOWN LIMITATION: cross-tree-overlaid module paths (e.g. extdeps.shell in BOTH -// dsl/extdeps/shell/shell.dag and src/v2/extdeps/shell.dag) mis-tag as DslTree even when -// witness_layer_roots overlay makes the v2 copy authoritative. QN materialization does NOT -// fix this — the path stays extdeps.shell in both trees. Harmless while FundamentalityUnknown -// denies all cross-tree edges (floor-verified inert); forbidden: admitting cross-tree edges -// through this fallback after direction-flip activation. -fn source_root_ref_from_qualified_name(qn: QualifiedName) -> SourceRootRef { - match qn { - QnEmpty => DslTree - QnCons { head: h, tail: _ } => - if h == ^v2 { - V2Tree +type SourceRootBinding { + module: QualifiedName + root: SourceRootRef +} + +type SourceRootIndex = FreeMonoid + + +fn source_root_index_empty() -> SourceRootIndex { + Empty +} + +fn source_root_index_insert( + index: SourceRootIndex, + module: QualifiedName, + root: SourceRootRef +) -> SourceRootIndex { + Cons { head: SourceRootBinding { module: module, root: root }, tail: index } +} + + +// SourceRootLookup — fail-closed 3-state result. Absent (module not in the ingest) is NOT +// an error here: the edge falls through to ordinary module_root_find, which produces the +// accurate unresolved-import diagnostic. Ambiguous (one QualifiedName bound to conflicting +// trees — the cross-tree-overlay hazard the QN-prefix guess silently mis-tagged) is a §5 +// fail-closed denial. +type SourceRootLookup + = SourceRootResolved { root: SourceRootRef } + | SourceRootAbsent + | SourceRootAmbiguous + + +fn source_root_index_lookup( + index: SourceRootIndex, + module: QualifiedName +) -> SourceRootLookup { + fold_list( + xs: index, + empty: SourceRootAbsent, + cons: fn(acc, binding) { + if qualified_name_eq(a: binding.module, b: module) { + match acc { + SourceRootAbsent => SourceRootResolved { root: binding.root } + SourceRootResolved { root: prev } => + if source_root_ref_eq(a: prev, b: binding.root) { + SourceRootResolved { root: prev } + } else { + SourceRootAmbiguous + } + SourceRootAmbiguous => SourceRootAmbiguous + } } else { - DslTree + acc + } + } + ) +} + + +// ── Tree-pair fundamentality (the operator's grounded de-fork decision) ───────── +// +// dsl ⊐ v2: dsl is the single std/extdeps/ci-spec authority v2 builds on. Same-tree pairs +// are CoFundamental but are never reached via cross_tree_edge_decision (it short-circuits +// same-tree to EdgeNormalResolution before consulting fundamentality). +fn tree_fundamentality_order( + from_tree: SourceRootRef, + to_tree: SourceRootRef +) -> TreeFundamentalityOrder { + match from_tree { + V2Tree => + match to_tree { + V2Tree => CoFundamental + DslTree => MoreFundamental + } + DslTree => + match to_tree { + V2Tree => LessFundamental + DslTree => CoFundamental } } } -// Layer tier from module QualifiedName — mirrors DESIGN.md §3 four-tier DAG. +// ── Layer tier from module QualifiedName ─────────────────────────────────────── +// Mirrors DESIGN.md §3 four-tier DAG. Unlike the deleted tree guess, layer tier IS encoded +// in the module path by construction (std/extdeps/compiler/workflow), so reading it from the +// QualifiedName is grounded, not a nickname. fn layer_prefix_from_qualified_name(qn: QualifiedName) -> LayerPrefix { match qn { QnEmpty => LayerPrefixStd @@ -114,47 +195,59 @@ fn source_root_set_insert( } -// Derive the active source-root set from a pool of qualified names. -fn source_root_set_from_module_roots(qns: FreeMonoid) -> FreeMonoid { - fold_list( - xs: qns, - empty: Empty, - cons: fn(acc, qn) { - source_root_set_insert(roots: acc, r: source_root_ref_from_qualified_name(qn: qn)) - } - ) -} - - // Interim empty module-path strings — CrossTreeImport admission ignores them; // dissolve-on: bold-bee 3a.2 QualifiedName materialization replaces with QN render. data cross_tree_module_path_interim: String = "" -// QualifiedName-grounded cross-tree admission (Phase B wiring surface). -fn cross_tree_import_admitted_qualified( + +// ── Grounded per-edge admission decision ──────────────────────────────────────── +// +// CrossTreeEdgeDecision — what admit_import_entry should do with one import edge, decided +// from the grounded index. EdgeNormalResolution = resolve via module_root_find (same tree, +// or target absent from the ingest so module_root_find owns the unresolved diagnostic); +// EdgeCrossAdmitted = grounded cross-tree edge that passes fundamentality + layer direction; +// EdgeCrossDenied = grounded cross-tree edge that fails them; EdgeCrossAmbiguous = a +// module bound to conflicting trees (fail-closed). +type CrossTreeEdgeDecision + = EdgeNormalResolution + | EdgeCrossAdmitted + | EdgeCrossDenied + | EdgeCrossAmbiguous + + +fn cross_tree_edge_decision( + index: SourceRootIndex, from_qn: QualifiedName, to_qn: QualifiedName, - roots: FreeMonoid, - order: TreeFundamentalityOrder -) -> CrossTreeAdmissionVerdict { - cross_tree_import_admitted( - edge: CrossTreeImport { - from_tree: source_root_ref_from_qualified_name(qn: from_qn), - from_layer: layer_prefix_from_qualified_name(qn: from_qn), - from_module: cross_tree_module_path_interim, - to_tree: source_root_ref_from_qualified_name(qn: to_qn), - to_layer: layer_prefix_from_qualified_name(qn: to_qn), - to_module: cross_tree_module_path_interim - }, - roots: roots, - order: order - ) -} - - -fn cross_tree_import_is_same_tree(from_qn: QualifiedName, to_qn: QualifiedName) -> Bool { - source_root_ref_eq( - a: source_root_ref_from_qualified_name(qn: from_qn), - b: source_root_ref_from_qualified_name(qn: to_qn) - ) + active_roots: SourceRootSet +) -> CrossTreeEdgeDecision { + match source_root_index_lookup(index: index, module: from_qn) { + SourceRootAbsent => EdgeNormalResolution + SourceRootAmbiguous => EdgeCrossAmbiguous + SourceRootResolved { root: from_tree } => + match source_root_index_lookup(index: index, module: to_qn) { + SourceRootAbsent => EdgeNormalResolution + SourceRootAmbiguous => EdgeCrossAmbiguous + SourceRootResolved { root: to_tree } => + if source_root_ref_eq(a: from_tree, b: to_tree) { + EdgeNormalResolution + } else { + match cross_tree_import_admitted( + edge: CrossTreeImport { + from_tree: from_tree, + from_layer: layer_prefix_from_qualified_name(qn: from_qn), + from_module: cross_tree_module_path_interim, + to_tree: to_tree, + to_layer: layer_prefix_from_qualified_name(qn: to_qn), + to_module: cross_tree_module_path_interim + }, + roots: active_roots, + order: tree_fundamentality_order(from_tree: from_tree, to_tree: to_tree) + ) { + CrossTreeAdmitted => EdgeCrossAdmitted + CrossTreeDenied { reason: _ } => EdgeCrossDenied + } + } + } + } } From c86459ae92ddbc82eba457bebaed783083973fc5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 21:36:31 +0000 Subject: [PATCH 2/3] WIP: Section 5 de-fork manager toward one dsl std authority: STEP 1 FIRST and --- src/v2/compiler/03_name_resolve.dag | 41 +++-- .../name_resolve/admission_fail_closed.dag | 8 +- .../name_resolve/malformed_imported_root.dag | 10 +- src/v2/compiler/program_assembly.dag | 86 ++++++++--- src/v2/compiler/source_authority.dag | 15 +- ...ame_resolve_cross_tree_resolution_test.dag | 141 ++++++++++++++---- 6 files changed, 218 insertions(+), 83 deletions(-) diff --git a/src/v2/compiler/03_name_resolve.dag b/src/v2/compiler/03_name_resolve.dag index c72c0a91a5f..35854cddfad 100644 --- a/src/v2/compiler/03_name_resolve.dag +++ b/src/v2/compiler/03_name_resolve.dag @@ -620,32 +620,41 @@ fn resolve_with_admission_policy( } -// Extract QualifiedNames from raw module root Nodes (SCAFFOLD — dissolves with grounded source_root). -fn module_root_nodes_to_qns(roots: FreeMonoid) -> FreeMonoid { - fold_list( - xs: roots, - empty: Empty, - cons: fn(acc, root) { - match qualified_name_from_module_node(root: root) { - Accepted { value: qn, diagnostics: _ } => Cons { head: qn, tail: acc } - Rejected { diagnostics: _ } => acc - } - } +// Index-less single-tree resolution: no source-root provenance is supplied, so every import +// is resolved by module_root_find within the given roots. Cross-tree admission requires the +// grounded index (resolve_with_admission_grounded), so this path is correct for single-tree +// compiles; a genuinely cross-tree import to a module absent from `roots` fails closed as an +// unresolved import. +fn resolve_with_admission( + lm: LanguageModel, + roots: FreeMonoid, + admission: Admission +) -> Outcome { + resolve_with_admission_policy( + lm: lm, + roots: roots, + admission: admission, + index: source_root_index_empty(), + active_roots: Empty ) } -// Fail-closed default: FundamentalityUnknown denies all cross-tree imports. -fn resolve_with_admission( +// Grounded cross-tree resolution: the QualifiedName -> SourceRootRef index and active +// source-root set are derived from the host-tagged ingest (program_assembly). Cross-tree +// import edges are admitted on grounded provenance + tree-pair fundamentality (§4/§5). +fn resolve_with_admission_grounded( lm: LanguageModel, roots: FreeMonoid, - admission: Admission + admission: Admission, + index: SourceRootIndex, + active_roots: FreeMonoid ) -> Outcome { resolve_with_admission_policy( lm: lm, roots: roots, admission: admission, - order: FundamentalityUnknown, - active_roots: source_root_set_from_module_roots(qns: module_root_nodes_to_qns(roots: roots)) + index: index, + active_roots: active_roots ) } diff --git a/src/v2/compiler/name_resolve/admission_fail_closed.dag b/src/v2/compiler/name_resolve/admission_fail_closed.dag index 18b70ad2176..54a80912ff4 100644 --- a/src/v2/compiler/name_resolve/admission_fail_closed.dag +++ b/src/v2/compiler/name_resolve/admission_fail_closed.dag @@ -13,12 +13,10 @@ import v2.compiler.name_resolve { ImportVisible, ResolutionSubject, admit_import_entry, - module_root_nodes_to_qns, resolve_with_admission, validate_module_roots } -import v2.std.cross_tree.import_model { FundamentalityUnknown } -import v2.std.cross_tree.resolution { source_root_set_from_module_roots } +import v2.std.cross_tree.resolution { source_root_index_empty } import v2.extdeps.languages.dag { dag_grammar_atom, dag_language_model_surface_empty_prelude, @@ -154,8 +152,8 @@ fn admit_import_missing_module_is_rejected() -> Bool { import_edge: fc_import_missing_target(), state: fc_initial_admission_state(), subject_qn: fc_qn(seg: ^fc_subject_seg), - order: FundamentalityUnknown, - active_roots: source_root_set_from_module_roots(qns: module_root_nodes_to_qns(roots: roots)) + index: source_root_index_empty(), + active_roots: Empty ) { AdmissionAccepted { bindings: _, origins: _ } => false AdmissionRejected { diagnostics: _ } => true diff --git a/src/v2/compiler/name_resolve/malformed_imported_root.dag b/src/v2/compiler/name_resolve/malformed_imported_root.dag index ec00bcbf987..c6c1256a853 100644 --- a/src/v2/compiler/name_resolve/malformed_imported_root.dag +++ b/src/v2/compiler/name_resolve/malformed_imported_root.dag @@ -10,11 +10,9 @@ import v2.compiler.name_resolve { AdmissionState, Import, ImportVisible, - admit_import_entry, - module_root_nodes_to_qns + admit_import_entry } -import v2.std.cross_tree.import_model { FundamentalityUnknown } -import v2.std.cross_tree.resolution { source_root_set_from_module_roots } +import v2.std.cross_tree.resolution { source_root_index_empty } import v2.extdeps.languages.dag { dag_grammar_atom, dag_named_edge @@ -117,8 +115,8 @@ fn witness_malformed_root_is_rejected_holds() -> Bool { import_edge: import_edge_for_malformed(), state: initial_admission_state(), subject_qn: malformed_entry_name(), - order: FundamentalityUnknown, - active_roots: source_root_set_from_module_roots(qns: module_root_nodes_to_qns(roots: roots)) + index: source_root_index_empty(), + active_roots: Empty ) ) } diff --git a/src/v2/compiler/program_assembly.dag b/src/v2/compiler/program_assembly.dag index cfcc1b3308b..31c2a2a08da 100644 --- a/src/v2/compiler/program_assembly.dag +++ b/src/v2/compiler/program_assembly.dag @@ -14,6 +14,7 @@ module v2.compiler.program_assembly import v2.compiler.name_resolve { Admission, resolve_with_admission, + resolve_with_admission_grounded, validate_module_roots } import v2.compiler.normalize { normalize } @@ -22,8 +23,15 @@ import v2.compiler.source_authority { DagSourceReadWitness, SourceRootIngest, source_authority_diagnostic, + source_root_set_from_ingest, } import v2.compiler.tokenize { tokenize } +import v2.extdeps.languages.dag { qualified_name_from_module_node } +import v2.std.cross_tree.resolution { + SourceRootIndex, + source_root_index_empty, + source_root_index_insert +} import v2.std.language_model { LanguageModel } import v2.std.algebra { Empty, FreeMonoid, fold_list, list_snoc_item } import v2.std.artifact { SourceFile } @@ -41,7 +49,8 @@ import v2.std.node { Node } type ProgramAssemblyFoldState = ProgramAssemblyFoldOk { - roots: FreeMonoid + roots: FreeMonoid, + index: SourceRootIndex } | ProgramAssemblyFoldFailed { diagnostics: NonEmptyDiagnostics @@ -82,6 +91,10 @@ fn program_assembly_read_to_normalized_root( } +// Per-read step: tokenize → parse_module → normalize the module root, AND pair its +// QualifiedName with the host source_root tag into the grounded index. A root whose module +// QualifiedName cannot be projected is left out of the index (validate_module_roots rejects +// it downstream); a Rejected parse short-circuits the whole fold. fn program_assembly_fold_step( state: ProgramAssemblyFoldState, read: DagSourceReadWitness, @@ -90,11 +103,20 @@ fn program_assembly_fold_step( match state { ProgramAssemblyFoldFailed { diagnostics: d } => ProgramAssemblyFoldFailed { diagnostics: d } - ProgramAssemblyFoldOk { roots: acc } => + ProgramAssemblyFoldOk { roots: acc, index: idx } => match program_assembly_read_to_normalized_root(read: read, lm: lm) { Accepted { value: root, diagnostics: _ } => - ProgramAssemblyFoldOk { - roots: list_snoc_item(xs: acc, item: root) + match qualified_name_from_module_node(root: root) { + Accepted { value: qn, diagnostics: _ } => + ProgramAssemblyFoldOk { + roots: list_snoc_item(xs: acc, item: root), + index: source_root_index_insert(index: idx, module: qn, root: read.source_root) + } + Rejected { diagnostics: _ } => + ProgramAssemblyFoldOk { + roots: list_snoc_item(xs: acc, item: root), + index: idx + } } Rejected { diagnostics: d } => ProgramAssemblyFoldFailed { diagnostics: d } @@ -103,19 +125,31 @@ fn program_assembly_fold_step( } -// Whole-ingest fold: per-read tokenize → parse_module → normalize; first Rejected short-circuits. -fn module_roots_from_source_root_ingest( +// Whole-ingest fold: per-read parse + grounded source-root index accumulation. +fn program_assembly_fold_ingest( ingest: SourceRootIngest, lm: LanguageModel -) -> Outcome> { - match fold_list( +) -> ProgramAssemblyFoldState { + fold_list( xs: ingest, - empty: ProgramAssemblyFoldOk { roots: program_assembly_empty_roots() }, + empty: ProgramAssemblyFoldOk { + roots: program_assembly_empty_roots(), + index: source_root_index_empty() + }, cons: fn(state, read) { program_assembly_fold_step(state: state, read: read, lm: lm) } - ) { - ProgramAssemblyFoldOk { roots: roots } => + ) +} + + +// Module roots from the ingest (parse leg only; index discarded). First Rejected short-circuits. +fn module_roots_from_source_root_ingest( + ingest: SourceRootIngest, + lm: LanguageModel +) -> Outcome> { + match program_assembly_fold_ingest(ingest: ingest, lm: lm) { + ProgramAssemblyFoldOk { roots: roots, index: _ } => outcome_accepted(value: roots) ProgramAssemblyFoldFailed { diagnostics: d } => Rejected { diagnostics: d } @@ -142,20 +176,30 @@ fn assemble_program_from_module_roots( } -// Program assembly: whole ingest monoid → validated roots → admitted resolved program. +// Program assembly: whole ingest → validated roots → GROUNDED admitted resolved program. +// The grounded source-root index and active source-root set are derived from the same +// host-tagged ingest (§4 provenance), so cross-tree import edges are admitted on filesystem +// truth + tree-pair fundamentality rather than a QualifiedName-prefix guess. fn assemble_program_from_ingest( ingest: SourceRootIngest, admission: Admission, lm: LanguageModel ) -> Outcome { - bind_outcome( - o: module_roots_from_source_root_ingest(ingest: ingest, lm: lm), - f: fn(roots) { - assemble_program_from_module_roots( - roots: roots, - admission: admission, - lm: lm + match program_assembly_fold_ingest(ingest: ingest, lm: lm) { + ProgramAssemblyFoldFailed { diagnostics: d } => + Rejected { diagnostics: d } + ProgramAssemblyFoldOk { roots: roots, index: idx } => + bind_outcome( + o: validate_module_roots(roots: roots), + f: fn(validated_roots) { + resolve_with_admission_grounded( + lm: lm, + roots: validated_roots, + admission: admission, + index: idx, + active_roots: source_root_set_from_ingest(ingest: ingest) + ) + } ) - } - ) + } } diff --git a/src/v2/compiler/source_authority.dag b/src/v2/compiler/source_authority.dag index d13041a0277..cc89e678404 100644 --- a/src/v2/compiler/source_authority.dag +++ b/src/v2/compiler/source_authority.dag @@ -74,8 +74,9 @@ type DagSourceReadWitness { compilation_unit: Symbol // Grounded source-tree provenance: which `--source-root` the host read this file from // (filesystem truth at ingest), NOT a guess from the module's self-declared QN prefix. - // Replaces the resolution.dag QN-prefix fallback — see source_root_set_from_ingest below. - // dissolve-on: PR-B wires this into resolve_with_admission + deletes the QN fallback. + // Folded into the active source-root set (source_root_set_from_ingest below) and the + // QualifiedName -> SourceRootRef index (program_assembly), which together replaced the + // deleted resolution.dag QN-prefix fallback — cross-tree admission is grounded on this. source_root: SourceRootRef } @@ -442,11 +443,11 @@ fn source_root_provenance_coverage_receipt( // Grounded active source-root set, folded from the host-tagged ingest witnesses. -// This is the §4-grounded replacement for resolution.dag's QN-prefix -// `source_root_set_from_module_roots` — each witness carries the filesystem truth of -// which `--source-root` it was read from, so the set is derived from provenance, not a -// guess. INERT in PR-A (defined, not yet wired); PR-B threads it into resolve_with_admission -// and deletes the QN-prefix fallback (the activation gate in resolution.dag's header). +// This is the §4-grounded replacement for resolution.dag's deleted QN-prefix +// source-root guess — each witness carries the filesystem truth of which `--source-root` +// it was read from, so the set is derived from provenance, not a guess. Wired into +// assemble_program_from_ingest (program_assembly) as the active_roots of grounded +// cross-tree admission. fn source_root_set_from_ingest(ingest: SourceRootIngest) -> SourceRootSet { fold_list( xs: ingest, diff --git a/src/v2/test/claim/name_resolve_cross_tree_resolution_test.dag b/src/v2/test/claim/name_resolve_cross_tree_resolution_test.dag index 28d4bcd2a60..9d8c3319f6d 100644 --- a/src/v2/test/claim/name_resolve_cross_tree_resolution_test.dag +++ b/src/v2/test/claim/name_resolve_cross_tree_resolution_test.dag @@ -1,8 +1,14 @@ -// Scope: Route C Phase B witnesses — cross-tree resolution wiring in name_resolve. +// Scope: Route C Phase C witnesses — GROUNDED cross-tree resolution in name_resolve. // -// GREEN: dual-root pool, same-tree imports resolve (dsl→dsl, v2→v2). -// GREEN: cross-tree import resolves when TreeFundamentalityOrder is MoreFundamental. -// RED: cross-tree import denied fail-closed when TreeFundamentalityOrder is Unknown. +// GREEN: dual-root pool, same-tree imports resolve (dsl→dsl, v2→v2) via the index-less path. +// GREEN: v2→dsl cross-tree import resolves — grounded index tags subject V2Tree / target +// DslTree, and tree_fundamentality_order(V2,Dsl)=MoreFundamental admits it (layer +// direction holds). This edge was DENIED before grounding landed (Unknown default). +// RED: dsl→v2 cross-tree import is denied fail-closed — grounded index tags subject DslTree +// / target V2Tree, and tree_fundamentality_order(Dsl,V2)=LessFundamental denies it. +// Subject and target are BOTH std-layer (equal ordinals) so layer direction holds: +// the denial is isolated to fundamentality, not the layer check. Flip either tag (or +// the fundamentality relation) and this witness goes the wrong way. // // Enrolled in CI via _test.dag naming convention (floor discovery auto-enroll). @@ -13,9 +19,7 @@ import v2.compiler.name_resolve { Import, ImportVisible, ResolutionSubject, - module_root_nodes_to_qns, - resolve_with_admission, - resolve_with_admission_policy + resolve_with_admission_grounded } import v2.compiler.program_assembly { assemble_program_from_module_roots } import v2.extdeps.languages.dag { @@ -24,8 +28,12 @@ import v2.extdeps.languages.dag { dag_named_edge } import v2.std.algebra { Cons, Empty, FreeMonoid, fold_list_node } -import v2.std.cross_tree.import_model { FundamentalityUnknown, MoreFundamental } -import v2.std.cross_tree.resolution { source_root_set_from_module_roots } +import v2.std.cross_tree.import_model { DslTree, SourceRootSet, V2Tree } +import v2.std.cross_tree.resolution { + SourceRootIndex, + source_root_index_empty, + source_root_index_insert +} import v2.std.diagnostic { Accepted, Rejected, locus_eq, port_locus } import v2.std.logic { Bool } import v2.std.node { @@ -132,6 +140,19 @@ fn ct_qn_v2(seg_b: Symbol) -> QualifiedName { } } +// [v2, std] — a v2-tree std-layer module QualifiedName (layer ordinal 0). +fn ct_qn_v2_std() -> QualifiedName { + QnCons { + head: ^v2, + tail: QnCons { head: ^std, tail: QnEmpty } + } +} + +// Both source trees present in the compilation closure (active source-root set). +fn ct_both_trees() -> SourceRootSet { + Cons { head: V2Tree, tail: Cons { head: DslTree, tail: Empty } } +} + // ── dsl same-tree (program_assembly_multi_file posture) ─────────────────────── @@ -205,7 +226,7 @@ fn ct_v2_same_tree_admission() -> Admission { } -// ── cross-tree (v2 subject → dsl target) ───────────────────────────────────── +// ── cross-tree v2 subject → dsl target (admitted: MoreFundamental) ──────────── fn ct_cross_tree_roots() -> FreeMonoid { Cons { @@ -242,6 +263,72 @@ fn ct_cross_tree_admission() -> Admission { } } +// Grounded index: v2 subject is V2Tree, dsl target is DslTree (host filesystem truth). +fn ct_v2_to_dsl_index() -> SourceRootIndex { + source_root_index_insert( + index: source_root_index_insert( + index: source_root_index_empty(), + module: ct_qn_v2(seg_b: ^ct_cross_v2_subject_seg), + root: V2Tree + ), + module: ct_qn_one(seg: ^ct_cross_dsl_target_seg), + root: DslTree + ) +} + + +// ── cross-tree dsl subject → v2 target (denied: LessFundamental) ────────────── +// Both modules std-layer (subject single-seg → std; target [v2, std] → std), so the layer +// direction check passes at equal ordinals and the denial isolates to fundamentality. + +fn ct_dsl_to_v2_roots() -> FreeMonoid { + Cons { + head: ct_subject_with_import_use( + qn_spine: ct_qn_node(seg: ^ct_inv_dsl_subject_seg), + import_use_sym: ^ct_inv_import_use_sym, + imported_decl: ^ct_inv_v2_export_sym + ), + tail: Cons { + head: ct_module_root( + qn_spine: ct_qn_spine( + segments: Cons { head: ^v2, tail: Cons { head: ^std, tail: Empty } } + ), + export_sym: ^ct_inv_v2_export_sym, + export_atom: ^dag_c3_surface_sugar_service + ), + tail: Empty + } + } +} + +fn ct_dsl_to_v2_admission() -> Admission { + Admission { + subject: ResolutionSubject { + name: ct_qn_one(seg: ^ct_inv_dsl_subject_seg) + }, + imports: Cons { + head: Import { + target: ct_qn_v2_std(), + visibility: ImportVisible + }, + tail: Empty + } + } +} + +// Grounded index: dsl subject is DslTree, v2 target is V2Tree (host filesystem truth). +fn ct_dsl_to_v2_index() -> SourceRootIndex { + source_root_index_insert( + index: source_root_index_insert( + index: source_root_index_empty(), + module: ct_qn_one(seg: ^ct_inv_dsl_subject_seg), + root: DslTree + ), + module: ct_qn_v2_std(), + root: V2Tree + ) +} + // ── GREEN witnesses ───────────────────────────────────────────────────────── @@ -267,15 +354,13 @@ fn witness_v2_same_tree_import_resolves_holds() -> Bool { } } -fn witness_cross_tree_more_fundamental_resolves_holds() -> Bool { - let roots = ct_cross_tree_roots() - let lm = dag_language_model_surface_empty_prelude() - match resolve_with_admission_policy( - lm: lm, - roots: roots, +fn witness_cross_tree_v2_to_dsl_grounded_resolves_holds() -> Bool { + match resolve_with_admission_grounded( + lm: dag_language_model_surface_empty_prelude(), + roots: ct_cross_tree_roots(), admission: ct_cross_tree_admission(), - order: MoreFundamental, - active_roots: source_root_set_from_module_roots(qns: module_root_nodes_to_qns(roots: roots)) + index: ct_v2_to_dsl_index(), + active_roots: ct_both_trees() ) { Accepted { value: _, diagnostics: _ } => true Rejected { diagnostics: _ } => false @@ -283,15 +368,15 @@ fn witness_cross_tree_more_fundamental_resolves_holds() -> Bool { } -// ── RED witnesses ───────────────────────────────────────────────────────────── +// ── RED witness ───────────────────────────────────────────────────────────── -fn witness_cross_tree_unknown_order_denied_holds() -> Bool { - let roots = ct_cross_tree_roots() - let lm = dag_language_model_surface_empty_prelude() - match resolve_with_admission( - lm: lm, - roots: roots, - admission: ct_cross_tree_admission() +fn witness_cross_tree_dsl_to_v2_grounded_denied_holds() -> Bool { + match resolve_with_admission_grounded( + lm: dag_language_model_surface_empty_prelude(), + roots: ct_dsl_to_v2_roots(), + admission: ct_dsl_to_v2_admission(), + index: ct_dsl_to_v2_index(), + active_roots: ct_both_trees() ) { Accepted { value: _, diagnostics: _ } => false Rejected { diagnostics: r } => @@ -307,6 +392,6 @@ fn witness_cross_tree_unknown_order_denied_holds() -> Bool { test fn name_resolve_cross_tree_resolution_witnesses() -> Bool { witness_dsl_same_tree_import_resolves_holds() && witness_v2_same_tree_import_resolves_holds() - && witness_cross_tree_more_fundamental_resolves_holds() - && witness_cross_tree_unknown_order_denied_holds() + && witness_cross_tree_v2_to_dsl_grounded_resolves_holds() + && witness_cross_tree_dsl_to_v2_grounded_denied_holds() } From 4d2bdd3ab71b07e47f802c3713a3ba365a1006c3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 21 Jun 2026 22:09:35 +0000 Subject: [PATCH 3/3] ci: force clean checkout (prior run resolved stale WIP-draft tree) No tree change vs c86459a. The reused self-hosted runner resolved the inconsistent intermediate commit 2c5750a (resolution.dag had the symbol deleted while 03_name_resolve.dag still called it); HEAD c86459a is clean. A fresh sha forces actions/checkout to reset the poisoned workspace. Co-Authored-By: Claude Opus 4.8