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
1 change: 1 addition & 0 deletions dag/extdeps/languages/rust/emit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -225,6 +225,7 @@ data rt_function_registry: List<RuntimeFunction> = [
{ name: "record_source_chars_index_lookup", bridge_name: "record_source_chars_index_lookup", passes_by_ref: false, wraps_result: false },
{ name: "resolution_silent_pick_is_enabled", bridge_name: "resolution_silent_pick_is_enabled", passes_by_ref: false, wraps_result: false },
{ name: "name_resolution_policy_is_namespace_only", bridge_name: "name_resolution_policy_is_namespace_only", passes_by_ref: false, wraps_result: false },
{ name: "type_ref_hit_ne_bind_measure_active", bridge_name: "type_ref_hit_ne_bind_measure_active", passes_by_ref: false, wraps_result: false },
{ name: "resolution_silent_pick_record_global_bare_lcp_pick", bridge_name: "resolution_silent_pick_record_global_bare_lcp_pick", passes_by_ref: false, wraps_result: false },
{ name: "resolution_silent_pick_record_global_bare_lcp_tie", bridge_name: "resolution_silent_pick_record_global_bare_lcp_tie", passes_by_ref: false, wraps_result: false },
{ name: "resolution_silent_pick_record_fn_parent_first_hit", bridge_name: "resolution_silent_pick_record_fn_parent_first_hit", passes_by_ref: false, wraps_result: false },
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/compile_diagnostic_census.dag
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ data compile_diagnostic_census_charter_note: String = "THE PROBE OBSERVATION SUR

data compile_diagnostic_census_grounding_note: String = "SECTION 3 - this is a PROJECTION, not a second diagnostic vocabulary. diagnostic_class is exactly the class half of the host's compile_clean_diagnostic_histogram_key, whose total match over v1.std.core CompilerDiagnostic is the single authority for naming a variant; subject_name is that key's name half. Declaring the variants again here as a coproduct would fork the authority and drift the moment a variant lands, so the class arrives as a projected string and the compiler's own exhaustiveness is what keeps it total. blocking is likewise projected, not restated: the host reads it through the existing compile_clean_diagnostic_is_hard delegation to is_interpreter_blocking_diagnostic, so the severity POLICY has one home and this surface reports its verdict rather than re-deciding it."

data compile_diagnostic_census_path_scope_note: String = "THE ONE PATH THIS SURFACE MEASURES, stated so a receipt cannot claim coverage it does not have (DESIGN 4b: a class's rung is the MINIMUM across its in-scope paths, and citing the strongest path while another stays silent is inflation). The census compiles a synthetic single-module source through the v1 pipeline to the Rust render target - the same compile path compile_dag_rust_emit_check takes - and reports the diagnostics that compile produced. In GuaranteePath axes that is subject_grain SyntheticProgram and acceptance_boundary CompileAccept. The pipeline is v1, and that is stated here as a fact about this surface rather than as a path axis: compile_mode was deleted from the path row (gunbc#7572, review 46308) because every landed control derives its pipeline from its boundary, so storing it was dual representation. If a path is ever measured under two pipelines at ONE boundary, that is the trigger returning the axis as a stored fact - not a reason to keep a copy of it here meanwhile. It observes NOTHING about the interpreter's disposition of the same program, nothing about other emission targets, and nothing about corpus-grain prevalence. A probe row keyed to a path this surface does not measure must not carry a receipt derived from it."
data compile_diagnostic_census_path_scope_note: String = "THE ONE PATH THIS SURFACE MEASURES, stated so a receipt cannot claim coverage it does not have (DESIGN 4b: a class's rung is the MINIMUM across its in-scope paths, and citing the strongest path while another stays silent is inflation). The census compiles a synthetic single-module source through the v1 pipeline to the Rust render target - the same pipeline family compile_dag_rust_emit_check uses - WITH type_ref_hit_ne_bind_measure_active armed for that nested compile only (N1a; host bracket v1_rt::with_type_ref_hit_ne_bind_measure). That is a real path split on masked type-reference sites: census can emit blocking UnresolvedType for pool-present non-authority refs while compile_dag_rust_emit_check (measure off) stays on the production fail-open / UnlistedImportUse advisory path. Census-derived receipts must not be read as production compile-clean behavior for those positions (review 47457). In GuaranteePath axes that is subject_grain SyntheticProgram and acceptance_boundary CompileAccept. The pipeline is v1, and that is stated here as a fact about this surface rather than as a path axis: compile_mode was deleted from the path row (gunbc#7572, review 46308) because every landed control derives its pipeline from its boundary, so storing it was dual representation. If a path is ever measured under two pipelines at ONE boundary, that is the trigger returning the axis as a stored fact - not a reason to keep a copy of it here meanwhile. It observes NOTHING about the interpreter's disposition of the same program, nothing about other emission targets, and nothing about corpus-grain prevalence. A probe row keyed to a path this surface does not measure must not carry a receipt derived from it."

data compile_diagnostic_census_not_runnable_note: String = "CensusNotRunnable is a separate arm and NOT an empty row list, because an empty census is byte-identical to a clean compile (DESIGN 5: top-as-answer conflated with top-as-ignorance is the absorbing fallback). Could-not-measure must never be readable as the subject passing: the probe layer maps this arm to guarantee_measurement ProbeObservation ProbeNotRunnable, whose observed_is_verdict is false, and it can do so without guessing precisely because the separation is preserved here at the host seam rather than reconstructed downstream. An infrastructural failure of the compile itself - a harness error, an unreadable module index, a panic caught at the boundary - lands here with its cause, never as a green census."

Expand Down
22 changes: 22 additions & 0 deletions dag/gunbc/type_ref_hit_ne_bind_measure/authority.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
module gunbc.type_ref_hit_ne_bind_measure

import std.types { String, NonEmptyStr }
import std.disposition { Disposition, Scaffold, SingleAuthority }
import std.decl_ref { DeclarationRef, WholeDeclaration }

data type_ref_hit_ne_bind_measure_charter_note: String = "N1a (swift-fox-347 extraction; quiet-hawk-219 / operator 2026-08-02): EXECUTING DISCRIMINATOR for the type-ref fail-open class — pool-present lookup hit is not binding authority. Under measurement mode only, a masked leaf use-site without measure-authority emits typed UnresolvedType (same construction as absent-from-pool) instead of fabricating Product(<anon>). This is NOT a corpus refusal wall, NOT construction, and NOT an admission/compatibility layer. Default compile-clean / resolve / run / emit stay on main's fail-open path (measure off). Arming surface: compile_dag_diagnostic_census sets v1_rt::type_ref_hit_ne_bind_measure (host bracket, same shape as name_resolution_policy) for the nested synthetic compile only."

data type_ref_measure_binding_authority_note: String = "MEASUREMENT-ONLY predicate type_ref_measure_binding_authority. Zero production consumers: no compile-clean gate, no resolve/run/serve/emit softening, nothing consults it unless type_ref_hit_ne_bind_measure_active. Body (two arms only): (1) bare — exact key in str_bindings ∪ ancestry_str_bindings; (2) qualified — qualified prefix is a containment ancestor of env.module_path (leading-segment prefix) AND symbol_index_lookup(full name) hits. Same-authored-leaf × (same-file OR same-span) OR-arm is dead (operator: false positives not tolerated). Dissolve-on: N2 routes TypeReference through namespace-reference-derived-closure → occurrence_binding_from_candidates → OccurrenceBindingResult; this predicate and the measure arm delete."

data type_ref_hit_ne_bind_measure_dissolve_trigger: String = "DISSOLVE when N2 lands TypeReference on namespace-reference-derived-closure → occurrence_binding_from_candidates → OccurrenceBindingResult (docs/plans/containment-binding-cross-module-type-references-design.md). Then delete: type_ref_hit_ne_bind_measure_active arming, type_ref_measure_binding_authority, the masked measure UnresolvedType branch in v1.compiler.infer_resolve, this carrier, and dag/test/claim/type_ref_hit_ne_bind_measure_witness_test.dag (or flip its REDs to permanent regression controls under the canonical fold)."

data type_ref_hit_ne_bind_measure_scaffold: Disposition = Scaffold {
dissolves_to: SingleAuthority,
bind: DeclarationRef {
module_path: "gunbc.type_ref_hit_ne_bind_measure" as NonEmptyStr,
decl_name: "type_ref_hit_ne_bind_measure_dissolve_trigger" as NonEmptyStr,
field: WholeDeclaration
}
}

data type_ref_hit_ne_bind_measure_rung_note: String = "§4b honesty: N1a establishes an executing discriminator (fixture GREEN/RED via compile_dag_diagnostic_census), not a guarantee ladder climb for the open corpus. Grandfathered corpus sites remain on the fail-open production path while measure is off. Do not report N1a as refusal or construction for that population."
88 changes: 88 additions & 0 deletions dag/test/claim/type_ref_hit_ne_bind_measure_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@
module test.claim.type_ref_hit_ne_bind_measure_witness

import gunbc.compile_diagnostic_census {
CompileDiagnosticCensus,
CensusObserved,
CensusNotRunnable,
census_blocking_rows,
census_rows_of_class,
census_total_count
}
import gunbc.type_ref_hit_ne_bind_measure {
type_ref_hit_ne_bind_measure_charter_note,
type_ref_measure_binding_authority_note,
type_ref_hit_ne_bind_measure_dissolve_trigger,
type_ref_hit_ne_bind_measure_rung_note
}
import std.types { String, Bool }
import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

data type_ref_hit_ne_bind_measure_witness_note: String = "N1a discriminator probes (import-strip §14.1 matrix, measurement mode). compile_dag_diagnostic_census arms type_ref_hit_ne_bind_measure_active for the nested compile. Row1 GREEN: bare import. Row3 RED: absent-from-pool UnresolvedType. Row4 RED: pool-present bare unreachable. Row5 RED: pool-present qualified unreachable. Row7 GREEN: same-module qualified local type (self/ancestor containment arm — NOT the deleted same-leaf×span cross-tree authorizer)."

fn census_of(source: String) -> CompileDiagnosticCensus {
compile_dag_diagnostic_census(source)
}

fn unresolved_blocking_count(source: String) -> Int {
match census_of(source: source) {
CensusObserved { rows: rows } =>
census_total_count(
rows: census_rows_of_class(
rows: census_blocking_rows(rows: rows),
wanted: "UnresolvedType"
)
)
CensusNotRunnable { cause: _ } => 0 - 1
}
}

data row1_own_import_source: String = "module type_ref_row1\nimport std.content_hash { ContentHash }\nfn f(x: ContentHash) -> ContentHash { x }\n"

data row3_absent_source: String = "module type_ref_row3\nfn f(x: NoSuchTypeNameAnywhereZzz) -> NoSuchTypeNameAnywhereZzz { x }\n"

data row4_bare_pool_present_source: String = "module type_ref_row4\nfn f(x: ContentHash) -> ContentHash { x }\n"

data row5_qualified_pool_present_source: String = "module type_ref_row5\nfn f(x: std.content_hash.ContentHash) -> std.content_hash.ContentHash { x }\n"

data row7_self_module_qualified_source: String = "module type_ref_row7\ntype LocalT = Int\nfn f(x: type_ref_row7.LocalT) -> type_ref_row7.LocalT { x }\n"

test fn row1_own_import_stays_green() -> Bool {
unresolved_blocking_count(source: row1_own_import_source) == 0
}

test fn row3_absent_is_blocking_unresolved_type() -> Bool {
unresolved_blocking_count(source: row3_absent_source) >= 1
}

test fn row4_bare_pool_present_unreachable_matches_row3_shape() -> Bool {
unresolved_blocking_count(source: row4_bare_pool_present_source) >= 1
}

test fn row5_qualified_pool_present_unreachable_matches_row3_shape() -> Bool {
unresolved_blocking_count(source: row5_qualified_pool_present_source) >= 1
}

test fn row7_self_module_qualified_stays_green() -> Bool {
unresolved_blocking_count(source: row7_self_module_qualified_source) == 0
}

test fn charter_is_measurement_not_corpus_refusal() -> Bool {
string_contains(s: type_ref_hit_ne_bind_measure_charter_note, pattern: "EXECUTING DISCRIMINATOR")
&& string_contains(s: type_ref_hit_ne_bind_measure_charter_note, pattern: "NOT a corpus refusal wall")
&& string_contains(s: type_ref_hit_ne_bind_measure_rung_note, pattern: "not a guarantee ladder climb")
}

test fn measure_predicate_two_arms_only() -> Bool {
string_contains(s: type_ref_measure_binding_authority_note, pattern: "MEASUREMENT-ONLY")
&& string_contains(s: type_ref_measure_binding_authority_note, pattern: "Zero production consumers")
&& string_contains(s: type_ref_measure_binding_authority_note, pattern: "Same-authored-leaf")
&& string_contains(s: type_ref_measure_binding_authority_note, pattern: "OR-arm is dead")
}

test fn dissolve_trigger_names_n2_canonical_fold() -> Bool {
string_contains(s: type_ref_hit_ne_bind_measure_dissolve_trigger, pattern: "occurrence_binding_from_candidates")
&& string_contains(s: type_ref_hit_ne_bind_measure_dissolve_trigger, pattern: "OccurrenceBindingResult")
&& string_contains(s: type_ref_hit_ne_bind_measure_dissolve_trigger, pattern: "containment-binding-cross-module-type-references-design.md")
}
Loading
Loading