Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
9be25c1
XL-2 LoweringOccurrenceProjection PR1: constructor tag atoms are lowe…
Sep 25, 2026
68339b9
XL-2 LoweringOccurrenceProjection PR2: dotted-spine segments keep the…
Sep 25, 2026
e456207
XL-2 LoweringOccurrenceProjection PR3a: v2 occurrence-role producer (…
Sep 25, 2026
f7b5c23
occurrence_role: a reader refusal is a typed, counted outcome, never …
Sep 25, 2026
6b411d9
occurrence_role: declare the frontier on the carrier; cite the modele…
Sep 25, 2026
f8ebce0
Merge remote-tracking branch 'origin/main' into session/tidy-otter-11…
Sep 26, 2026
068d98e
occurrence_role: a row whose production has no atom identity refuses …
Sep 26, 2026
df0fea1
Merge remote-tracking branch 'origin/session/tidy-otter-111-tag-sourc…
Sep 26, 2026
92c6807
Merge branch 'session/tidy-otter-111-spine-segments' into session/tid…
Sep 26, 2026
efc9743
occurrence_role: list input_block and output_block (main replaced io_…
Sep 26, 2026
4610c18
XL-2 LoweringOccurrenceProjection PR3b: census consumes occurrence ro…
Sep 26, 2026
4b6ace9
Merge origin/main into session/tidy-otter-111-occurrence-roles (after…
Sep 27, 2026
bbf5f49
Merge session/tidy-otter-111-occurrence-roles (now on main) into cens…
Sep 27, 2026
a5a3a4d
census: absence from a listing, not a failed read; an unreadable path…
Sep 27, 2026
e3b89a9
Merge origin/main into census-roles (after #12317 landed)
Sep 27, 2026
2ed6b27
occurrence_role: admit the .dag table once, warm; the census claim pa…
Sep 27, 2026
b4fceb9
census: list the path's own parent; observe roles whatever normalizat…
Sep 27, 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
30 changes: 27 additions & 3 deletions dag/gunbc/namespace/namespace_xl2_rehearsal_census.dag
Original file line number Diff line number Diff line change
Expand Up @@ -140,9 +140,33 @@ data xl2_native_requalification_walls: List<Xl2NativeRequalificationWall> = [
// because the census's resolved arm (v2.compiler.compile NativeCensusModuleResolved) keeps no
// resolved tree to count from; counting it needs the census to carry ResolvedToKernelSymbol
// occurrences, which is the trigger for adding a count here.
type Xl2ExcludedPopulation = | Xl2KernelCanonicalReferencesUncounted

data xl2_excluded_populations: List<Xl2ExcludedPopulation> = [Xl2KernelCanonicalReferencesUncounted]
//
// HEADER SEGMENTS ARE NOT REFUSAL SITES. A module header's segments name the module itself; the
// graft consumes them and resolve never looks one up, so stripping imports cannot make resolve
// refuse at one. Measured on this composition (xl2_rehearse_stripped over supplied sources): a
// module whose header names a path that no module declares yields residual rows only at its body
// references, none at a header segment. Counted where the census has the atoms:
// v2.compiler.reference_conservation header_channel.
//
// NESTING-SCOPED REFERENCES SURVIVE THE STRIP, UNCOUNTED. Measured on the same composition: a
// module declared as v2.xl2_control_provider.shadow resolves the provider's function with its
// import stripped, because nesting under a namespace grants that namespace's scope. Such a
// reference is invisible to this census exactly as a kernel canonical one is -- no residual row
// is not evidence the cut covers it. It is carried UNCOUNTED for the same reason: the resolved arm
// keeps no resolved tree to count from, so counting it needs the census to carry which scope
// resolved each reference, which is the trigger for adding a count here. OPEN QUESTION, not
// answered by this row: whether the root-authority cut (XL-6) is meant to keep nesting-granted
// scope; if it is not, these references become residual and this arm dissolves.
type Xl2ExcludedPopulation
= Xl2KernelCanonicalReferencesUncounted
| HeaderSegmentsNotRefusalSites
| NestingScopedReferencesUncounted

data xl2_excluded_populations: List<Xl2ExcludedPopulation> = [
Xl2KernelCanonicalReferencesUncounted,
HeaderSegmentsNotRefusalSites,
NestingScopedReferencesUncounted
]

type Xl2RehearsalRun
= Xl2RehearsalBaseUnobserved { cause: Step0SubjectPinRefusal }
Expand Down
32 changes: 30 additions & 2 deletions dag/test/claim/namespace_xl2_rehearsal_census_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,9 @@ import gunbc.namespace_xl2_rehearsal_census {
Xl2ResidualChain,
Xl2ScopeUnobserved,
Xl2Strip,
Xl2KernelCanonicalReferencesUncounted,
HeaderSegmentsNotRefusalSites,
NestingScopedReferencesUncounted,
Xl2StrippedMember,
xl2_rehearse_stripped,
xl2_strip_members
Expand Down Expand Up @@ -56,6 +59,12 @@ data xl2_residual_control_source: String = "module v2.xl2_control_residual\n\nim

data xl2_two_failure_control_source: String = "module v2.xl2_control_two\n\nimport v2.std.logic { Bool }\nimport v2.xl2_control_provider { xl2_control_provider_flag, xl2_control_provider_other }\n\nfn xl2_control_two_first(p: Bool) -> Bool { xl2_control_provider_flag }\n\nfn xl2_control_two_second(p: Bool) -> Bool { xl2_control_provider_other }\n"

// THE NESTED CONTROL: a module declared UNDER the provider's namespace, naming the provider's
// function through an import the strip removes. It is the specimen behind
// NestingScopedReferencesUncounted: stripped, it still resolves, because nesting grants the
// namespace's scope, so the cut leaves no residual row for its reference.
data xl2_nested_control_source: String = "module v2.xl2_control_provider.nested\n\nimport v2.std.logic { Bool }\nimport v2.xl2_control_provider { xl2_control_provider_flag }\n\nfn xl2_control_nested_value(p: Bool) -> Bool { xl2_control_provider_flag }\n"

data xl2_clean_control_source: String = "module v2.xl2_control_clean\n\nimport v2.std.logic { Bool }\n\nfn xl2_control_clean_value(p: Bool) -> Bool { p }\n"

fn xl2_control_source(path: String, content: String) -> FixtureSource {
Expand Down Expand Up @@ -87,9 +96,10 @@ type Xl2ControlRuns {
two: Xl2RehearsalRun
pre_cut: Xl2RehearsalRun
duplicated: Xl2RehearsalRun
nesting: Xl2RehearsalRun
}

// ONE NULLARY PRODUCER, WARM, FOR ALL FOUR RUNS (v2.workflow.floor_pure_producer_share carries its
// ONE NULLARY PRODUCER, WARM, FOR ALL FIVE RUNS (v2.workflow.floor_pure_producer_share carries its
// row): each run is a front end plus its resolves, more than one claim's budget, and the first cut
// of this file paid two of them inside claims and was refused over budget on the floor.
fn xl2_control_runs() -> Xl2ControlRuns {
Expand All @@ -107,6 +117,10 @@ fn xl2_control_runs() -> Xl2ControlRuns {
xl2_control_source(path: "dag/xl2_control_shared.dag", content: xl2_residual_control_source),
xl2_control_source(path: "dag/xl2_control_shared.dag", content: xl2_clean_control_source),
clean
])),
nesting: xl2_control_rehearse(strip: xl2_strip_members(sources: [
provider,
xl2_control_source(path: "dag/xl2_control_nested.dag", content: xl2_nested_control_source)
]))
}
}
Expand Down Expand Up @@ -189,7 +203,11 @@ test fn xl2_two_failures_in_one_module_are_two_rows_holds() -> Bool {
// completeness refusals (the refusal type cannot carry them).
test fn xl2_control_names_the_native_requalification_walls_holds() -> Bool {
match xl2_control_runs().cut {
Xl2RehearsalObserved { native_requalification: walls, excluded: excluded } => count(walls) == 2 && count(excluded) == 1
Xl2RehearsalObserved { native_requalification: walls, excluded: excluded } =>
count(walls) == 2 && count(excluded) == 3
&& any(excluded, e => e == Xl2KernelCanonicalReferencesUncounted)
&& any(excluded, e => e == HeaderSegmentsNotRefusalSites)
&& any(excluded, e => e == NestingScopedReferencesUncounted)
_ => false
}
}
Expand All @@ -208,3 +226,13 @@ test fn xl2_duplicated_path_is_withheld_not_chosen_holds() -> Bool {
_ => false
}
}

// A NESTED MODULE'S REFERENCE SURVIVES THE STRIP: the provider and the module nested under its
// namespace both resolve after the import is removed, and no residual row is emitted. This is why
// NestingScopedReferencesUncounted is carried: the cut's residual cannot see this reference.
test fn xl2_nested_reference_survives_the_strip_holds() -> Bool {
match xl2_control_runs().nesting {
Xl2RehearsalObserved { residual: residual, resolved_module_count: n } => count(residual) == 0 && n == 2
_ => false
}
}
34 changes: 32 additions & 2 deletions src/v2/compiler/occurrence_role.dag
Original file line number Diff line number Diff line change
Expand Up @@ -359,7 +359,12 @@ fn roles_walk(acc: OccurrenceRoles, node: Node, by_emitted: Map<Symbol, NameProd
}

fn occurrence_roles_of_tree(tree: Node, root: GrammarRoot, rows: List<NameProductionRow>) -> OccurrenceRoleOutcome {
match name_production_table_admission(root: root, rows: rows) {
occurrence_roles_of_admitted(tree: tree, admission: name_production_table_admission(root: root, rows: rows))
}

// The walk against a table already admitted, so a caller that walks many trees admits once.
fn occurrence_roles_of_admitted(tree: Node, admission: NameProductionTableAdmission) -> OccurrenceRoleOutcome {
match admission {
NameProductionTableRefused { unlisted: u, unknown: k, unkeyed: x } => OccurrenceRoleTableRefused { unlisted: u, unknown: k, unkeyed: x }
NameProductionTableAdmitted { by_emitted: by_emitted } =>
OccurrenceRolesRead { roles: roles_walk(acc: occurrence_roles_empty(), node: tree, by_emitted: by_emitted) }
Expand All @@ -370,7 +375,32 @@ fn occurrence_role_index(roles: OccurrenceRoles) -> Map<OccurrenceId, AtomOccurr
fold_list(xs: roles.roles, empty: empty_map(), cons: fn(acc, r) { map_insert(m: acc, key: r.occurrence, value: r) })
}

// The emitted identities of the `.dag` table's productions: the keys its per-production counters
// (not_yet_read, reader_refused) can carry, derived from the grammar, so a consumer can total them.
fn dag_name_production_emitted_symbols() -> List<Symbol> {
let listed = fold(dag_name_production_rows(), init: empty_map(), f: fn(acc, row) { map_insert(m: acc, key: row.production, value: true) })
fold(dag_grammar_root().productions, init: Empty, f: fn(acc, p) {
match map_lookup(m: listed, key: p.name) {
Absent => acc
Present { value: _ } =>
match node_atom_identity_optional(node: p.emitted) {
Present { value: e } => list_snoc_item(xs: acc, item: e)
Absent => acc
}
}
})
}

// THE `.dag` TABLE, ADMITTED ONCE, AS ONE NULLARY VALUE. Admission re-derives the whole grammar
// root and folds every production's expression, which costs more than one module's walk; the result
// depends on nothing but the language, so it is enrolled WARM in v2.workflow.floor_pure_producer_share
// (beside v2.compiler.reference_conservation dag_declared_token_classes) and paid once per floor, not
// once per census claim. dag_name_production_emitted_symbols below is enrolled the same way.
fn dag_name_table_admission() -> NameProductionTableAdmission {
name_production_table_admission(root: dag_grammar_root(), rows: dag_name_production_rows())
}

// The `.dag` language's roles for one parsed module.
fn dag_occurrence_roles(artifact: ParseArtifact) -> OccurrenceRoleOutcome {
occurrence_roles_of_tree(tree: artifact.tree, root: dag_grammar_root(), rows: dag_name_production_rows())
occurrence_roles_of_admitted(tree: artifact.tree, admission: dag_name_table_admission())
}
Loading