Skip to content
Merged
27 changes: 27 additions & 0 deletions dag/gunbc/v1/v1_interpreter_primitive_surface.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2023,6 +2023,33 @@ fn v1_interpreter_authored_roster_arms() -> List<InterpreterPrimitiveDispatchArm
dispatch_emit_site: TryV2StdCollectionMapPrimitiveGroundingSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "map_grounding.map_insert" },
form: NativeSpecial,
authored_spelling: "map_insert_primitive_delegate",
realization_module: "v1_interpreter",
dispatch_symbol: "try_v2_std_collection_map_primitive_grounding",
dispatch_emit_site: TryV2StdCollectionMapPrimitiveGroundingSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "map_grounding.lookup" },
form: NativeSpecial,
authored_spelling: "map_lookup_primitive_delegate",
realization_module: "v1_interpreter",
dispatch_symbol: "try_v2_std_collection_map_primitive_grounding",
dispatch_emit_site: TryV2StdCollectionMapPrimitiveGroundingSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "map_grounding.lookup" },
form: NativeSpecial,
authored_spelling: "map_lookup",
realization_module: "v1_interpreter",
dispatch_symbol: "try_v2_std_collection_map_primitive_grounding",
dispatch_emit_site: TryV2StdCollectionMapPrimitiveGroundingSite,
enumeration: AuthoredInRoster,
},
InterpreterPrimitiveDispatchArm {
arm: InterpreterPrimitiveArmId { identity: "native_intercept.fold_list" },
form: NativeSpecial,
Expand Down
6 changes: 5 additions & 1 deletion dag/std/primitive_identity.dag
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ import std.primitive_projection {
PrimitiveProjection, PrimitiveProjectionAnswer,
DeclarationProjectsPrimitive, DeclarationProjectsNoPrimitive, DeclarationPrimitiveUndisposed,
primitive_projection_roster, primitive_projection_row_for_declaration,
primitive_length, primitive_map_insert, primitive_map_get, primitive_empty_map,
primitive_length, primitive_map_insert, primitive_map_get, primitive_lookup, primitive_empty_map,
primitive_decl_facts, primitive_decl_facts_at, primitive_export_signature_facts, primitive_data_decl_type_facts,
primitive_concept_decl_facts, primitive_concept_decl_facts_live,
primitive_symbol_lexeme, primitive_symbol_intern_lexeme,
Expand Down Expand Up @@ -1225,6 +1225,7 @@ data primitive_projection_target_canonical_names: List<String> = [
"length",
"map_insert",
"map_get",
"lookup",
"empty_map",
"decl_facts",
"decl_facts_at",
Expand Down Expand Up @@ -1539,6 +1540,8 @@ data primitive_map_insert_traversal: PrimitiveTraversalOrderFact = PrimitiveTrav

data primitive_map_get_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_map_get, order: OrderFreeResult }

data primitive_lookup_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_lookup, order: OrderFreeResult }

data primitive_empty_map_traversal: PrimitiveTraversalOrderFact = PrimitiveTraversalOrderFact { primitive: primitive_empty_map, order: OrderFreeResult }

// The parse-only reflection primitives are CanonicalOrder by EXECUTED READING of their
Expand Down Expand Up @@ -1586,6 +1589,7 @@ data primitive_projection_traversal_facts: List<PrimitiveTraversalOrderFact> = [
primitive_length_traversal,
primitive_map_insert_traversal,
primitive_map_get_traversal,
primitive_lookup_traversal,
primitive_empty_map_traversal,
primitive_decl_facts_traversal,
primitive_decl_facts_at_traversal,
Expand Down
4 changes: 4 additions & 0 deletions dag/std/primitive_projection.dag
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,7 @@ type PrimitiveProjectionAnswer
data primitive_length: PrimitiveIdentity = primitive_identity_slug(name: "length")
data primitive_map_insert: PrimitiveIdentity = primitive_identity_slug(name: "map_insert")
data primitive_map_get: PrimitiveIdentity = primitive_identity_slug(name: "map_get")
data primitive_lookup: PrimitiveIdentity = primitive_identity_slug(name: "lookup")
data primitive_empty_map: PrimitiveIdentity = primitive_identity_slug(name: "empty_map")
data primitive_decl_facts: PrimitiveIdentity = primitive_identity_slug(name: "decl_facts")
data primitive_decl_facts_at: PrimitiveIdentity = primitive_identity_slug(name: "decl_facts_at")
Expand Down Expand Up @@ -111,10 +112,13 @@ fn primitive_projection_roster() -> List<PrimitiveProjection> {
primitive_projection_row(primitive: primitive_concept_decl_facts, module_path: "v2.std.concept_index", decl_name: "concept_decl_facts", fidelity: HostRealizedSeam),
primitive_projection_row(primitive: primitive_concept_decl_facts_live, module_path: "v2.std.concept_index", decl_name: "concept_decl_facts_live", fidelity: HostRealizedSeam),
primitive_projection_row(primitive: primitive_empty_map, module_path: "v2.std.collection", decl_name: "empty_map_primitive_delegate", fidelity: HostRealizedSeam),
primitive_projection_row(primitive: primitive_map_insert, module_path: "v2.std.collection", decl_name: "map_insert_primitive_delegate", fidelity: HostRealizedSeam),
primitive_projection_row(primitive: primitive_lookup, module_path: "v2.std.collection", decl_name: "map_lookup_primitive_delegate", fidelity: HostRealizedSeam),
primitive_projection_row(primitive: primitive_symbol_lexeme, module_path: "v2.std.compilers.lexing", decl_name: "symbol_lexeme", fidelity: HostRealizedSeam),
primitive_projection_row(primitive: primitive_symbol_intern_lexeme, module_path: "v2.std.compilers.lexing", decl_name: "symbol_intern_lexeme", fidelity: HostRealizedSeam),
primitive_projection_row(primitive: primitive_length, module_path: "v2.std.algebra", decl_name: "length", fidelity: ModeledProjection),
primitive_projection_row(primitive: primitive_map_insert, module_path: "v2.std.collection", decl_name: "map_insert", fidelity: ModeledProjection),
primitive_projection_row(primitive: primitive_lookup, module_path: "v2.std.collection", decl_name: "map_lookup", fidelity: ModeledProjection),
primitive_projection_row(primitive: primitive_empty_map, module_path: "v2.std.collection", decl_name: "empty_map", fidelity: ModeledProjection),
primitive_projection_row(primitive: primitive_map_get, module_path: "v2.std.collection", decl_name: "map_get", fidelity: DivergentProjection { divergence: "declared return Outcome<Optional<V>> against the primitive's Optional<V>" as NonEmptyStr }),
]
Expand Down
13 changes: 13 additions & 0 deletions dag/test/claim/primitive_projection_authority_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ import std.primitive_projection {
primitive_length,
primitive_map_get,
primitive_map_insert,
primitive_lookup,
primitive_projection_row,
}
import std.primitive_identity {
Expand Down Expand Up @@ -163,6 +164,18 @@ test fn w_seam_and_modeled_projections_are_one_authority() -> Bool {
declaration: projection_declaration(module_path: "v2.std.collection", decl_name: "empty_map"),
primitive: primitive_empty_map,
)
&& declaration_and_primitive_are_one_authority(
declaration: projection_declaration(module_path: "v2.std.collection", decl_name: "map_insert_primitive_delegate"),
primitive: primitive_map_insert,
)
&& declaration_and_primitive_are_one_authority(
declaration: projection_declaration(module_path: "v2.std.collection", decl_name: "map_lookup_primitive_delegate"),
primitive: primitive_lookup,
)
&& declaration_and_primitive_are_one_authority(
declaration: projection_declaration(module_path: "v2.std.collection", decl_name: "map_lookup"),
primitive: primitive_lookup,
)
}

test fn w_projection_of_a_different_primitive_is_not_one_authority() -> Bool {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -284,8 +284,8 @@ test fn w_unbridged_modeled_primitive_emits_its_declaration() -> Bool {
// THE BOUNDARY CONTROL FOR THE LENGTH REPAIR, AND THE ONE THAT PROVES THE GATE IS REGISTRY
// MEMBERSHIP RATHER THAN "ROSTER ROW MEANS DECLARATION". empty_map has a roster row AND a
// registry row, so it must still lower to the bridge. A repair that had simply routed every
// ModeledProjection to its declaration would go red here -- and would also emit
// v2.std.collection map_insert's `Map { lookup: fn .. }` body against an Rc<BTreeMap> carrier.
// ModeledProjection to its declaration would go red here -- and would also have emitted
// v2.std.collection map_insert's former `Map { lookup: fn .. }` body against an Rc map carrier.
test fn w_bridged_modeled_primitive_still_lowers_to_the_bridge() -> Bool {
compile_dag_rust_emit_check(
"module test.claim.bridged_empty_map_probe\nimport std.types { Int, String, Map }\nimport std.occurrence_identity { OccurrenceId }\nimport v2.std.collection { empty_map }\nfn probe() -> Map<String, Int> { empty_map() }\n",
Expand Down
47 changes: 3 additions & 44 deletions src/v1/stage0/src/namespace_wave_admission.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1712,51 +1712,10 @@ pub struct TransitionAdmission {
/// is that touch, so the debt is paid here rather than inherited by an unrelated lane. Their
/// TRIGGER, recorded at the time as "these rows go when #11071 merges", is what fired.
///
/// gunbc#11137 sha256sum names Filesystem instead of reaching it (2026-09-12). The row below is a
/// DIFFERENT delta that this change produces, not that one restored: empty is the resting state
/// and one change authoring a row back into it is the ordinary motion.
///
/// WHAT THE CHANGE DID. `extdeps.tools.sha256sum` called `Filesystem.Write` while importing
/// `extdeps.filesystem.filesystem_io` with NO name list. A bare module import drags the whole
/// module into the candidate set for every name it declares, so filesystem_io's copy of
/// `extdeps_external_authority_anchor` -- the per-module convention row some 315 modules each
/// author -- was a candidate at this site. The import now names `{ Filesystem }`.
///
/// WHY `TargetChanged` IS THE CORRECT CLASSIFICATION. The spelling is authored on both sides and
/// what moved is which declarations it admits: base `{extdeps.filesystem.filesystem_io,
/// extdeps.shell, extdeps.tools.sha256sum}`, head `{extdeps.shell, extdeps.tools.sha256sum}`.
///
/// WHAT MAKES IT SAFE TO ADMIT, adjudicated rather than asserted. NO RESOLUTION CHANGES.
/// `extdeps.tools.sha256sum` authors its own `extdeps_external_authority_anchor`, and a module's
/// own declaration wins inside the authored region, so the site resolved to sha256sum's row at the
/// base and resolves to sha256sum's row at the head -- the removed candidate could not have won
/// either way. What narrowed is the SET, from three modules to two, which is the qualification's
/// whole purpose: the resolution stopped depending on a module the author never named. That no
/// consumer changed behaviour is the required floor's verdict on this head, re-derived by
/// `claim_executor --required-ci --source-root dag --source-root src/v2 --required-lane witnesses`
/// and read off its own `required-floor:` verdict line -- named rather than transcribed, because a
/// copied count rots without anyone touching either end (DESIGN §6).
///
/// WHY THE `String` REQUALIFICATION IN THE SAME CHANGE NEEDS NO ROW, which is a fair question to
/// ask of a diff that moves ten import lines onto `std.string_type`. It is not this adjudication's
/// assertion; it is the wave phase's own measurement. That phase compares the binding table on both
/// sides, and on this head it reported exactly ONE `TargetChanged binding` delta -- the row below --
/// and none for `String`. The ten `String` sites appear instead as
/// `ExplicitlyEvaluatedZeroDelta membership <module> -> std.string_type ... reached by a name this
/// module authors`: explicitly evaluated, zero delta. The reason is that `std.types` declares no
/// `String` at all, so `import std.types { String }` bound nothing and the read fell through to the
/// shared slot, where scope precedence already answered `std.string_type`. Naming that module
/// changes the read's AUTHORIZATION -- from an accident of precedence to something the author
/// wrote -- without changing which declaration answers it. A delta row adjudicates a changed
/// binding; there is no changed binding here to adjudicate.
///
/// Lifecycle is derived by the evaluator from the candidate set; no predicted STALE or
/// CONSUMED outcome is authored here. The old sentence predicted CONSUMED for a two-member
/// result that the singleton proof could never accept.
/// THIRTY-SIXTH DISSOLUTION (2026-09-12). #11137 merged. The required floor on gunbc#11121
/// (run 34681339370) reported that row as `STALE ADMISSION ... matches no delta in this run`.
/// RETIRED (2026-09-12): #11137 merged as 34d2a8db32d; its transition is present at the base.
/// The EMPTY DOES NOT MEAN PERMISSIVE rule above makes this shrink fail-closed. This is the
/// same instance deletion carried by the other cleanup PRs; the landing-incidence repair
/// must itself discharge the roster debt it now enforces.
/// Empty is the resting state; this touch deletes the row rather than inheriting it.
pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[];

/// The denominators a green must name (DESIGN §5): a run that cannot say what it covered is an
Expand Down
27 changes: 27 additions & 0 deletions src/v1/stage0/src/std_primitive_projection.rs
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,15 @@ pub fn primitive_map_get() -> Rc<PrimitiveIdentity> {
CACHED.with(|c: &Rc<PrimitiveIdentity>| c.clone())
}

pub fn primitive_lookup() -> Rc<PrimitiveIdentity> {
thread_local! {
static CACHED: Rc<PrimitiveIdentity> = {
primitive_identity_slug("lookup".to_string())
};
}
CACHED.with(|c: &Rc<PrimitiveIdentity>| c.clone())
}

pub fn primitive_empty_map() -> Rc<PrimitiveIdentity> {
thread_local! {
static CACHED: Rc<PrimitiveIdentity> = {
Expand Down Expand Up @@ -257,6 +266,18 @@ pub fn primitive_projection_roster() -> Rc<Vec<Rc<PrimitiveProjection>>> {
"empty_map_primitive_delegate".to_string(),
Rc::new(ProjectionFidelity::HostRealizedSeam),
),
primitive_projection_row(
primitive_map_insert(),
"v2.std.collection".to_string(),
"map_insert_primitive_delegate".to_string(),
Rc::new(ProjectionFidelity::HostRealizedSeam),
),
primitive_projection_row(
primitive_lookup(),
"v2.std.collection".to_string(),
"map_lookup_primitive_delegate".to_string(),
Rc::new(ProjectionFidelity::HostRealizedSeam),
),
primitive_projection_row(
primitive_symbol_lexeme(),
"v2.std.compilers.lexing".to_string(),
Expand All @@ -281,6 +302,12 @@ pub fn primitive_projection_roster() -> Rc<Vec<Rc<PrimitiveProjection>>> {
"map_insert".to_string(),
Rc::new(ProjectionFidelity::ModeledProjection),
),
primitive_projection_row(
primitive_lookup(),
"v2.std.collection".to_string(),
"map_lookup".to_string(),
Rc::new(ProjectionFidelity::ModeledProjection),
),
primitive_projection_row(
primitive_empty_map(),
"v2.std.collection".to_string(),
Expand Down
8 changes: 4 additions & 4 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7490,7 +7490,8 @@ macro_rules! v1_map_grounding_arms {
$cb! {
$fname;
arm "map_grounding.empty_map" { "empty_map_primitive_delegate" | "empty_map" } => "empty_map",
arm "map_grounding.map_insert" { "map_insert" } => "map_insert",
arm "map_grounding.map_insert" { "map_insert_primitive_delegate" | "map_insert" } => "map_insert",
arm "map_grounding.lookup" { "map_lookup_primitive_delegate" | "map_lookup" } => "lookup",
}
};
}
Expand Down Expand Up @@ -7559,13 +7560,12 @@ fn try_v2_std_collection_map_primitive_grounding(
let builtin_name = v1_map_grounding_arms!(v1_map_grounding_dispatch, grounded_name);
match eval_builtin(builtin_name, args, ctx) {
Ok(Some(v)) => Some(Ok(v)),
Ok(None) if builtin_name == "empty_map" => Some(Err(InterpError::TypeError {
Ok(None) => Some(Err(InterpError::TypeError {
msg: format!(
"{V2_STD_COLLECTION_MODULE}.{}: native HAMT primitive missing from eval_builtin (host misconfiguration)",
"{V2_STD_COLLECTION_MODULE}.{}: native map primitive refused this argument shape (host misconfiguration, or a non-native map carrier reached a HostRealizedSeam)",
fn_node.name
),
})),
Ok(None) => None,
Err(e) => Some(Err(e)),
}
}
Expand Down
5 changes: 5 additions & 0 deletions src/v1/stage0/src/v1_interpreter_dispatch_generated.rs
Original file line number Diff line number Diff line change
Expand Up @@ -663,6 +663,7 @@ macro_rules! eval_call_bridge__v2_std_data_index_arm {
pub enum TryV2StdCollectionMapPrimitiveGroundingArm {
MapGroundingEmptyMap,
MapGroundingMapInsert,
MapGroundingLookup,
}

#[rustfmt::skip]
Expand All @@ -671,6 +672,9 @@ pub fn lookup_try_v2_std_collection_map_primitive_grounding(spelling: &str) -> O
"empty_map_primitive_delegate" => Some(TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingEmptyMap),
"empty_map" => Some(TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingEmptyMap),
"map_insert" => Some(TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingMapInsert),
"map_insert_primitive_delegate" => Some(TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingMapInsert),
"map_lookup_primitive_delegate" => Some(TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingLookup),
"map_lookup" => Some(TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingLookup),
_ => None,
}
}
Expand All @@ -679,6 +683,7 @@ pub fn lookup_try_v2_std_collection_map_primitive_grounding(spelling: &str) -> O
macro_rules! try_v2_std_collection_map_primitive_grounding_arm {
("map_grounding.empty_map") => { $crate::v1_interpreter_dispatch_generated::TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingEmptyMap };
("map_grounding.map_insert") => { $crate::v1_interpreter_dispatch_generated::TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingMapInsert };
("map_grounding.lookup") => { $crate::v1_interpreter_dispatch_generated::TryV2StdCollectionMapPrimitiveGroundingArm::MapGroundingLookup };
}
#[rustfmt::skip]
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
Expand Down
9 changes: 9 additions & 0 deletions src/v1/stage0/tests/interpreter_dispatch_authority.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,15 @@ fn generated_lookup_covers_representative_spellings_per_site() {
all_eval_algebra_variants_reachable();
all_bridge_variants_reachable();
assert!(lookup_try_v2_std_collection_map_primitive_grounding("map_insert").is_some());
assert!(
lookup_try_v2_std_collection_map_primitive_grounding("map_insert_primitive_delegate")
.is_some()
);
assert!(lookup_try_v2_std_collection_map_primitive_grounding("map_lookup").is_some());
assert!(
lookup_try_v2_std_collection_map_primitive_grounding("map_lookup_primitive_delegate")
.is_some()
);
assert!(lookup_eval_call_native_intercept("fold_list").is_some());
assert!(lookup_try_parse_table_memo_dispatch("parse_table_lookup").is_some());
}
Expand Down
3 changes: 3 additions & 0 deletions src/v1/tests/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,9 @@ pub mod helpers;
#[cfg(test)]
mod grounded_shared_carrier_wrap_test;

#[cfg(test)]
mod map_insert_record_shaped_refusal_test;

#[cfg(test)]
mod unknown_pipeline_driver_refusal_test;

Expand Down
Loading
Loading