Skip to content
Closed
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
4 changes: 2 additions & 2 deletions dag/extdeps/docker/container_inspect.dag
Original file line number Diff line number Diff line change
Expand Up @@ -953,15 +953,15 @@ fn docker_inspect_nested_network_settings(obj: JsonValue) -> NestedObjectRead<Ne
// ONE FOLD, NOT THREE INSTANTIATIONS OF IT. A first cut carried a byte-identical copy per nested
// type because the field access at ONE call site could not infer `T` -- and the answer to that is
// to name the type at that site, not to mint three declarations of one concept in a shared decoder.
fn nested_value(r: NestedObjectRead<T>) -> T? {
fn nested_value<T>(r: NestedObjectRead<T>) -> T? {
match r {
NestedAbsent => none
NestedMalformed { causes: _ } => none
NestedRead { value: v } => Present { value: v }
}
}

fn nested_causes(r: NestedObjectRead<T>) -> List<String> {
fn nested_causes<T>(r: NestedObjectRead<T>) -> List<String> {
match r {
NestedAbsent => []
NestedMalformed { causes: cs } => cs
Expand Down
4 changes: 2 additions & 2 deletions dag/extdeps/languages/json/parse.dag
Original file line number Diff line number Diff line change
Expand Up @@ -635,7 +635,7 @@ fn json_field_string_list(obj: JsonValue, key: String) -> JsonFieldRead<List<Str
// matches would report the first and hide the rest, which turns one decode into four round trips
// against a live daemon -- and against a CAPTURE, which cannot be re-run at all, it would hide
// findings permanently.
fn json_field_value(r: JsonFieldRead<T>) -> T? {
fn json_field_value<T>(r: JsonFieldRead<T>) -> T? {
match r {
FieldAbsent => none
FieldMalformed { cause: _ } => none
Expand All @@ -644,7 +644,7 @@ fn json_field_value(r: JsonFieldRead<T>) -> T? {
}


fn json_field_cause(r: JsonFieldRead<T>) -> String? {
fn json_field_cause<T>(r: JsonFieldRead<T>) -> String? {
match r {
FieldAbsent => none
FieldMalformed { cause: c } => Present { value: c }
Expand Down
49 changes: 47 additions & 2 deletions dag/gunbc/instruments/native_emission_controls.dag
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,47 @@ fn effectful_fold_step_cases() -> List<NativeEmissionCase> {
]
}

// RULE: a type parameter carries its own cardinality (v1.compiler.emit_rust rust_carrier_optional_wrap,
// gunbc.recurring_failure_mode optional_type_parameter_emitted_without_its_cardinality). `get: K?` on a
// generic record emitted `pub get: K`, so an Absent had no representation and this carrier's
// construction with Absent did not compile -- the red is the label's. The cases read the field back
// both ways, and each has a red asking for an answer it does not give.
type ControlOptionalParam<K> {
get: K?
pair: K
}

fn control_optional_param_absent() -> ControlOptionalParam<Int> {
ControlOptionalParam { get: Absent, pair: 1 }
}

fn control_optional_param_present() -> ControlOptionalParam<Int> {
ControlOptionalParam { get: Present { value: 7 }, pair: 2 }
}

fn optional_param_is_absent(c: ControlOptionalParam<Int>) -> Bool {
match c.get {
Present { value: _ } => false
Absent => true
}
}

fn optional_param_value_or_zero(c: ControlOptionalParam<Int>) -> Int {
match c.get {
Present { value: v } => v
Absent => 0
}
}

fn optional_type_parameter_cases() -> List<NativeEmissionCase> {
[
NativeEmissionCase { identity: "optional_type_param_holds_absent", held: optional_param_is_absent(c: control_optional_param_absent()) },
NativeEmissionCase { identity: "optional_type_param_red_present_is_not_absent", held: !optional_param_is_absent(c: control_optional_param_present()) },
NativeEmissionCase { identity: "optional_type_param_holds_present_value", held: optional_param_value_or_zero(c: control_optional_param_present()) == 7 },
NativeEmissionCase { identity: "optional_type_param_red_absent_reads_no_value", held: optional_param_value_or_zero(c: control_optional_param_absent()) == 0 }
]
}

data native_emission_expected_identities: List<String> = [
"set_struct_eq_same_members_in_another_order",
"set_struct_eq_red_bare_field_differs",
Expand All @@ -197,11 +238,15 @@ data native_emission_expected_identities: List<String> = [
"claim_driver_filesystem_absent_path_read_is_refused",
"effectful_fold_step_counts_every_refused_read",
"effectful_fold_step_red_seen_counts_elements",
"effectful_fold_step_red_empty_keeps_init"
"effectful_fold_step_red_empty_keeps_init",
"optional_type_param_holds_absent",
"optional_type_param_red_present_is_not_absent",
"optional_type_param_holds_present_value",
"optional_type_param_red_absent_reads_no_value"
]

fn native_emission_cases() -> List<NativeEmissionCase> {
concat(concat(concat(header_bound_cases(), filter_in_branch_condition_cases()), claim_driver_filesystem_cases()), effectful_fold_step_cases())
concat(concat(concat(concat(header_bound_cases(), filter_in_branch_condition_cases()), claim_driver_filesystem_cases()), effectful_fold_step_cases()), optional_type_parameter_cases())
}

fn case_row(c: NativeEmissionCase) -> String {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1311,7 +1311,7 @@ fn sel_channel(channel: NonEmptyStr, s: SelSnapshotReading) -> BmcChannelRead {
} }
}

fn members_channel(channel: NonEmptyStr, m: MembersReading<T>) -> BmcChannelRead {
fn members_channel<T>(channel: NonEmptyStr, m: MembersReading<T>) -> BmcChannelRead {
BmcChannelRead { channel: channel, standing: match m {
MembersRead { members: _ } => BmcChannelAnswered
MembersUnread { cause: c } => BmcChannelFailed { cause: c }
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/machine_intake/mtjade1_access_observation.dag
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ fn field_unread(field: NonEmptyStr, cause: String) -> RecordedManagerDecode {
RecordedManagerRefused { gap: CaptureFieldUnread { field: field, cause: cause } }
}

fn read_cause(r: JsonFieldRead<T>) -> String {
fn read_cause<T>(r: JsonFieldRead<T>) -> String {
match r {
FieldAbsent => "absent"
FieldMalformed { cause: c } => c
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
module gunbc.recurring_failure_mode.optional_type_parameter_emitted_without_its_cardinality

import std.types { NonEmptyStr }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data optional_type_parameter_emitted_without_its_cardinality: RecurringFailureMode = RecurringFailureMode {
identity: "optional_type_parameter_emitted_without_its_cardinality" as NonEmptyStr,

receipts: [
"**an optional type parameter is emitted without its cardinality** (INVALID STATE: a generic declaration writes `K?` on one of its own type parameters -- `type Plain<K, V> { get: K? }`, `type PartialFunction<K, V> { lookup: fn(K) -> V? }` -- and the Rust emitter spells the parameter by its bare name, dropping the Optional: `pub get: K`. The four arms of v1.compiler.emit_rust that spell a type parameter (the declared-generic leaf in render_rust_decl_type and in the signature renderer, the TypeVariable arms of render_rust_type and render_rust_applied_type_arg) returned to_pascal(name) and never consulted return_cardinality, which every other leaf routes through rust_carrier_optional_wrap.",

"HARM: silent wrongness. An absent value has no representation in the emitted type, so a program that stores Absent in such a field either fails to compile at the construction site or, through a generic instantiation that happens to be optional, carries the wrong shape. Measured on main (2026-10-04): `get: K?` in a generic record emitted `pub get: K`. A `fn(K) -> V?` field kept its Option only by accident: the parameter resolved through a module-scope binding (v1.compiler.infer build_type_env param_bindings) instead of as a type parameter, so it reached a different, cardinality-aware arm. Scoping type parameters to their declaration (native broker 1C, rule 2) removed that accident and made the defect visible on std.algebra PartialFunction and FinitelySupportedFunction.",

"DISTINGUISHING FACTS: the same `?` on a non-parameter leaf (`get: Int?`) emits Option<i64>. Only a leaf the emitter recognises as one of the declaration's generic parameters drops it, and only on the arms that spell the parameter by name.",

"RUNG FOUND AT: outside the ladder (silent). CLIMBED TO: mechanically preventable. Every type-parameter spelling arm wraps through rust_carrier_optional_wrap, and gunbc.instruments.native_emission_controls carries an optional-parameter carrier that is constructed with Absent and with Present and read back natively: drop the wrap and its emission refuses at rustc (no Absent for a bare K), which is the label's red. CEILING: 3 (structurally guaranteed), once cardinality is part of the type-reference node the emitter is handed rather than a field each arm must remember to read.",

"NEXT-RUNG TRIGGER, as the capability: type references reach emission as one carrier that renders cardinality and spelling together, SUFFICIENT THAT no renderer arm can return a type spelling without its Optional wrap.",
],

evidence: [
DeclarationRef { module_path: "v1.compiler.emit_rust", decl_name: "rust_carrier_optional_wrap", field: WholeDeclaration },
],
}
93 changes: 93 additions & 0 deletions dag/test/claim/type_parameter_declaration_scope_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,93 @@
module test.claim.type_parameter_declaration_scope_witness

import std.types { String, Bool, Int, List }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import tools.multi_module_compile_fixture {
MultiModuleCompileFixture,
MultiModuleCompileFixtureOutcome,
FixtureInstrumentRefused,
FixtureCompileRefused,
FixtureCompileCompleted,
FixtureSource,
fixture_source,
compile_fixture,
fixture_has_class
}

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// THE CLASS: A TYPE PARAMETER THAT BINDS OUTSIDE ITS OWN DECLARATION.
//
// v1.compiler.infer build_type_env used to insert every generic TYPE declaration's parameters into
// the module's bindings, so `type Box<Q>` made a bare `Q` resolvable anywhere in that module -- and,
// through an import's exported surface, in its importers, which is why the implicit-name filters
// (is_type_variable_name over T/K/V/...) existed to strip them again. A function could then write
// `-> Q` with no `<Q>` of its own and be accepted, and the Rust emitter, which renders only DECLARED
// parameters, produced a generic function without its type parameters. A parameter now binds only
// while its own declaration is resolved (v1.compiler.infer_resolve declaration_type_param_names).
//
// THE SUBJECT IS AUTHORED MANIFESTS, compiled by tools.multi_module_compile_fixture with no corpus
// roots, so the claims are about the scoping rule and nothing else in the tree. NO std.types import
// in any fixture: the manifest has no corpus, and Int is a kernel type every module sees.

data tps_same_module_leak_source: String = "module tps.same\n\ntype TpsBox<Q> {\n v: Q\n}\n\nfn tps_leak(x: Int) -> Q {\n x\n}\n"

data tps_definer_source: String = "module tps.definer\n\ntype TpsBox<Q> {\n v: Q\n}\n"

data tps_cross_import_leak_source: String = "module tps.user\n\nimport tps.definer { TpsBox }\n\nfn tps_unwrap(b: TpsBox<Int>) -> Q {\n b.v\n}\n"

data tps_declared_source: String = "module tps.user\n\nimport tps.definer { TpsBox }\n\nfn tps_unwrap<Q>(b: TpsBox<Q>) -> Q {\n b.v\n}\n"

fn tps_run_one(path: String, source: String) -> MultiModuleCompileFixtureOutcome {
compile_fixture(MultiModuleCompileFixture { sources: [fixture_source(path, source)], entry: path })
}

fn tps_run_with_definer(user_source: String) -> MultiModuleCompileFixtureOutcome {
compile_fixture(MultiModuleCompileFixture {
sources: [
fixture_source("tps/definer.dag", tps_definer_source),
fixture_source("tps/user.dag", user_source)
],
entry: "tps/user.dag"
})
}

// Read by matching, so FixtureInstrumentRefused -- the harness breaking -- satisfies neither a red
// nor the control.
fn tps_diagnosed_as(o: MultiModuleCompileFixtureOutcome, wanted: String) -> Bool {
match o {
FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } =>
fixture_has_class(rows: rows, wanted: wanted),
FixtureCompileCompleted { module_count: n, emitted_files: files, resolved_rust_functions: _, diagnostics: rows, source_digest: sd, compiler_digest: cd } =>
fixture_has_class(rows: rows, wanted: wanted),
FixtureInstrumentRefused { cause: c } => false
}
}

fn tps_completed_clean(o: MultiModuleCompileFixtureOutcome) -> Bool {
match o {
FixtureCompileCompleted { module_count: n, emitted_files: files, resolved_rust_functions: _, diagnostics: rows, source_digest: sd, compiler_digest: cd } =>
count(rows) == 0 && count(files) > 0 && n > 0,
FixtureCompileRefused { module_count: n, diagnostics: rows, source_digest: sd, compiler_digest: cd } => false,
FixtureInstrumentRefused { cause: c } => false
}
}

// THE RED, SAME MODULE. `Q` is declared only by TpsBox; tps_leak declares no parameters and names `Q`
// as its return. Under module-scope binding this was accepted (and returned an Int as a Q).
test fn a_sibling_type_parameter_does_not_bind_in_another_declaration() -> Bool {
tps_diagnosed_as(tps_run_one("tps/same.dag", tps_same_module_leak_source), "UnresolvedType")
}

// THE RED, ACROSS AN IMPORT. tps.user imports TpsBox and names its parameter `Q` bare. The import
// carries the type, never the parameter.
test fn an_imported_type_parameter_does_not_bind_in_the_importer() -> Bool {
tps_diagnosed_as(tps_run_with_definer(tps_cross_import_leak_source), "UnresolvedType")
}

// THE POSITIVE CONTROL, read first in a red: the same importer declaring its own `<Q>` compiles clean,
// so the reds are refusals of the leak and not a harness that refuses every manifest.
test fn a_declared_type_parameter_binds_in_its_own_declaration() -> Bool {
tps_completed_clean(tps_run_with_definer(tps_declared_source))
&& !tps_diagnosed_as(tps_run_with_definer(tps_declared_source), "UnresolvedType")
}
24 changes: 17 additions & 7 deletions src/v1/04_env.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1387,13 +1387,13 @@ fn inductive_fields_list_to_map(fields: List<InductiveField>) -> Map<String, Lis
)
}

fn env_with_type_variable_bindings(env: TypeEnv, tp_names: List<String>) -> TypeEnv {
fold(tp_names, init: env, f: (e, tp_name) =>
let tp_binding = TypeBinding {
name: tp_name,
resolved: Node { occurrence_identity: OccurrenceSynthetic, name: tp_name, span: kernel_span(name: tp_name), ident_span: Present { value: kernel_span(name: tp_name) }, children: [], connective: NoConnective, params: [], inferred: Present { value: TypeVariable { id: tp_name } }, return_cardinality: Required, uses: [], body: none, transport: none, properties: [], type_annotation: none, is_self_recursive: false, has_non_tail_self_call: false, match_pattern: none, module_item_kind: NotAModuleItem, declaration_marker: Unmarked, declaration: none, expr_data: NoExprData },
provenance: SubValueUnknown, alias_rhs: none
}
// ONE INSERT FOR EVERY SCOPED TYPE-PARAMETER BINDING. A declaration's type parameters are bound
// only around that declaration (v1.compiler.infer_resolve declaration_type_param_names); the two
// callers differ only in the binding's shape -- a TypeVariable for item resolution, a nominal leaf for
// the module's topological resolution of declaration bodies -- so the scoping is written once.
fn env_with_type_parameter_bindings(env: TypeEnv, tp_bindings: List<TypeBinding>) -> TypeEnv {
fold(tp_bindings, init: env, f: (e, tp_binding) =>
let tp_name = tp_binding.name
let shadowed = effective_visible_binding(str_bindings: e.str_bindings, parents: e.parents, name: tp_name)
let updated_index = unit_variant_index_shadow_insert(unit_variant_index: e.unit_variant_index, shadowed: shadowed, binding: tp_binding, source_indices: e.source_indices)
TypeEnv { module_path: e.module_path,
Expand All @@ -1415,6 +1415,16 @@ fn env_with_type_variable_bindings(env: TypeEnv, tp_names: List<String>) -> Type
)
}

fn env_with_type_variable_bindings(env: TypeEnv, tp_names: List<String>) -> TypeEnv {
env_with_type_parameter_bindings(env: env, tp_bindings: tp_names |> map(tp_name =>
TypeBinding {
name: tp_name,
resolved: Node { occurrence_identity: OccurrenceSynthetic, name: tp_name, span: kernel_span(name: tp_name), ident_span: Present { value: kernel_span(name: tp_name) }, children: [], connective: NoConnective, params: [], inferred: Present { value: TypeVariable { id: tp_name } }, return_cardinality: Required, uses: [], body: none, transport: none, properties: [], type_annotation: none, is_self_recursive: false, has_non_tail_self_call: false, match_pattern: none, module_item_kind: NotAModuleItem, declaration_marker: Unmarked, declaration: none, expr_data: NoExprData },
provenance: SubValueUnknown, alias_rhs: none
}
))
}

// A census-backed declaration has no materialized module TypeEnv, but its exact owner and the
// completed symbol census are declaration authority. Build the same owner-position environment
// for every signature fact recovered from that declaration; a caller environment is not a
Expand Down
Loading
Loading