From 3c509b67899a6ad42aad17431a1691b1d376fb95 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 01:56:06 +0000 Subject: [PATCH 1/8] WIP: declared-type inhabitance obligation carrier (UNVERIFIED, not for push) Carrier types, the single declared_type_inhabitance relation consuming #8876's coproduct_payload_where_parent_required, the DeclaredTypeNotInhabited diagnostic, and the list-element position wired. Mirrors NOT regenerated; the wall does not execute in any built artifact yet. Verification dispatch in flight. --- src/v1/00_core.dag | 4 ++ src/v1/04_infer.dag | 129 ++++++++++++++++++++++++++++++++++- src/v1/stage0/src/cli_run.rs | 2 + 3 files changed, 134 insertions(+), 1 deletion(-) diff --git a/src/v1/00_core.dag b/src/v1/00_core.dag index a1f7a76efd7..e09970b3713 100644 --- a/src/v1/00_core.dag +++ b/src/v1/00_core.dag @@ -187,6 +187,7 @@ type CompilerDiagnostic permitted_callers: List, span: SourceSpan } + | DeclaredTypeNotInhabited { position: String, expected: String, got: String, span: SourceSpan } | UnlistedImportUse { name: String, span: SourceSpan } | AmbiguousReference { name: String, candidates: List, span: SourceSpan } | CallArgumentNameUnknown { callee: String, argument: String, declared: List, span: SourceSpan } @@ -325,6 +326,7 @@ fn diagnostic_to_span(d: CompilerDiagnostic) -> SourceSpan { permitted_callers: _, span: s } => s + DeclaredTypeNotInhabited { position: _, expected: _, got: _, span: s } => s UnlistedImportUse { name: _, span: s } => s AmbiguousReference { name: _, candidates: _, span: s } => s CallArgumentNameUnknown { callee: _, argument: _, declared: _, span: s } => s @@ -396,6 +398,8 @@ fn diagnostic_to_message(d: CompilerDiagnostic) -> String { join(permitted, separator: ", "), "]" ) + DeclaredTypeNotInhabited { position: pos, expected: e, got: g, span: _ } => + concat("value does not inhabit its declared type at the ", pos, ": declared '", e, "', produced '", g, "'") UnlistedImportUse { name: n, span: _ } => concat("unlisted import use '", n, "' (referenced but not in any import's name list)") AmbiguousReference { name: n, candidates: cs, span: _ } => concat("ambiguous reference '", n, "': ", to_string(value: cs |> count), " candidates: ", join(cs, separator: ", "), " — qualify by containment path, alias, or rename") CallArgumentNameUnknown { callee: c, argument: a, declared: ds, span: _ } => diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index b70b0458aba..bf861404809 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2070,6 +2070,118 @@ fn coproduct_variant_payload_admits_type_name( // makes "the actual is one of this coproduct's payload types" undecidable from the declaration // alone; refusing there would be a fabricated refusal, which DESIGN section 5 forbids exactly as it // forbids a fabricated success. +// ONE OBLIGATION, ONE AUTHORITY. The grammar has fourteen type positions and twelve of them +// can receive a source value. Before this carrier each position that judged anything judged it +// with its own local chain of else-if predicates, which is one rule in N representations: a +// position added later inherits nothing, and a rule fixed at one position stays broken at the +// rest. A DeclaredTypeObligation names WHERE the obligation arose, WHAT was declared and WHAT +// was produced; declared_type_inhabitance is the single relation that decides; the position +// travels with the obligation so the diagnostic can locate the refusal without the decision +// procedure forking per position. +type DeclaredTypePosition + = PositionRecordLiteralField + | PositionListElement + | PositionMapValue + | PositionDataInitializer + | PositionDeclaredReturn + | PositionLetAnnotation + | PositionVariantPayload + | PositionGenericTypeArgument + | PositionCastTarget + | PositionParameterDefault + | PositionCallableReturn + | PositionDirectCallArgument + +type DeclaredTypeObligation { + position: DeclaredTypePosition + declared: Node + produced: Node + span: SourceSpan +} + +// UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. Each reason names something the +// modeled facts genuinely cannot settle at this seam. A position that has not been wired yet is +// NOT undecidable -- it is a missing obligation producer, and it is absent from the census +// rather than present with a verdict. Reading "we did not look" as "it cannot be decided" is +// the rung inflation DESIGN 4b names, applied to this relation's own self-description. +type InhabitanceUndecidableReason + = UndecidableGenericFormal + | UndecidableOptionalCarrier + | UndecidableFormalUnresolved + | UndecidableProducedIdentityErased + +type InhabitanceRefusalReason + = RefusedPayloadAtParent + | RefusedKernelAtStructured + +type InhabitanceVerdict + = Inhabits + | InhabitanceRefused { reason: InhabitanceRefusalReason } + | InhabitanceUndecidable { reason: InhabitanceUndecidableReason } + +fn declared_type_position_label(position: DeclaredTypePosition) -> String { + match position { + PositionRecordLiteralField => "record literal field" + PositionListElement => "list element" + PositionMapValue => "map value" + PositionDataInitializer => "data initializer" + PositionDeclaredReturn => "declared return" + PositionLetAnnotation => "let annotation" + PositionVariantPayload => "variant payload" + PositionGenericTypeArgument => "generic type argument" + PositionCastTarget => "cast target" + PositionParameterDefault => "parameter default" + PositionCallableReturn => "callable return" + PositionDirectCallArgument => "direct call argument" + } +} + +// THE SINGLE DECISION PROCEDURE. It CONSUMES the established predicates rather than restating +// them: coproduct_payload_where_parent_required already peels transparent aliases through +// transparent_alias_identity_agrees, so alias identity is decided in exactly one place in the +// tree and this relation inherits it instead of re-deriving a second answer. +fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferScope) -> InhabitanceVerdict { + let declared = obligation.declared + let produced = obligation.produced + let source_indices = scope.type_env.source_indices + let declared_name = authored_name_at(source_indices: source_indices, node: declared) + let produced_name = authored_name_at(source_indices: source_indices, node: produced) + let either_optional = declared.return_cardinality == CardOptional || produced.return_cardinality == CardOptional + let declared_is_generic = (declared.params |> count) > 0 + if either_optional { + InhabitanceUndecidable { reason: UndecidableOptionalCarrier } + } else if declared_is_generic { + InhabitanceUndecidable { reason: UndecidableGenericFormal } + } else if declared_name == "" { + InhabitanceUndecidable { reason: UndecidableFormalUnresolved } + } else if produced_name == "" { + InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } + } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { + InhabitanceRefused { reason: RefusedPayloadAtParent } + } else { + Inhabits + } +} + +// The obligation carries its own position, so ONE emitter locates every refusal. A per-position +// diagnostic function would be the N-representation problem moved one layer down. +fn declared_type_obligation_diags(obligation: DeclaredTypeObligation, scope: InferScope) -> List { + match declared_type_inhabitance(obligation: obligation, scope: scope) { + Inhabits => [] + InhabitanceUndecidable { reason: _ } => [] + InhabitanceRefused { reason: _ } => + [make_error_node( + diagnostic: DeclaredTypeNotInhabited { + position: declared_type_position_label(position: obligation.position), + expected: node_type_shape(n: obligation.declared, source_indices: scope.type_env.source_indices), + got: node_type_shape(n: obligation.produced, source_indices: scope.type_env.source_indices), + span: obligation.span + }, + module_name: scope.module_name + )] + } +} + fn coproduct_payload_where_parent_required( formal: Node, actual: Node, @@ -4602,7 +4714,22 @@ fn infer_expr_body(texpr: Node, scope: InferScope, expected: Node?) -> InferResu } let elem_results = elements |> map(e => infer_expr(texpr: e, scope: scope, expected: elem_expected)) let typed_elements = elem_results |> map(r => r.typed) - let elem_diags = flat_map(elem_results, r => r.diagnostics) + let elem_inhabitance_diags = match elem_expected { + Present { value: declared_elem } => + flat_map(typed_elements, te => + declared_type_obligation_diags( + obligation: DeclaredTypeObligation { + position: PositionListElement, + declared: declared_elem, + produced: resolved_type(n: te), + span: te.span + }, + scope: scope + ) + ) + Absent => [] + } + let elem_diags = concat(flat_map(elem_results, r => r.diagnostics), elem_inhabitance_diags) let elem_type_node = if count(elem_results) > 0 { match first(elem_results) { Present { value: r } => resolved_type(n: r.typed) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 351dc600c6f..d12db20b7b1 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -4738,6 +4738,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (String, Str CompilerDiagnostic::ConstructorCallAdmissionRefused { .. } => { "ConstructorCallAdmissionRefused" } + CompilerDiagnostic::DeclaredTypeNotInhabited { .. } => "DeclaredTypeNotInhabited", CompilerDiagnostic::UnlistedImportUse { .. } => "UnlistedImportUse", CompilerDiagnostic::AmbiguousReference { .. } => "AmbiguousReference", CompilerDiagnostic::CallArgumentNameUnknown { .. } => "CallArgumentNameUnknown", @@ -4783,6 +4784,7 @@ pub fn compile_clean_diagnostic_histogram_key(d: &Rc) -> (String, Str constructor_decl_name, .. } => constructor_decl_name.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { position, .. } => position.clone(), CompilerDiagnostic::UnlistedImportUse { name, .. } => name.clone(), CompilerDiagnostic::AmbiguousReference { name, .. } => name.clone(), CompilerDiagnostic::CallArgumentNameUnknown { argument, .. } => argument.clone(), From fdde6fb435280e72652d6d77bdb351e38849d19b Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 02:55:38 +0000 Subject: [PATCH 2/8] Wire the kernel-at-structured route and its witness (still unverified) --- ..._inhabitance_list_element_witness_test.dag | 101 ++++++++++++++++++ src/v1/04_infer.dag | 4 + 2 files changed, 105 insertions(+) create mode 100644 dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag diff --git a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag new file mode 100644 index 00000000000..1ed96abeae2 --- /dev/null +++ b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag @@ -0,0 +1,101 @@ +module test.claim.declared_type_inhabitance_list_element_witness + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CensusObserved, + CensusNotRunnable, + census_rows_of_class, + census_total_count +} +import std.types { String, Bool, Int } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THE FLOOR CLAUSE THIS GUARDS: a value accepted at a declared-type position inhabits that +// declared type. DESIGN names it as floor, so a breach is a below-baseline safety regression +// rather than a missing nicety, and it is not softened to mitigatable anywhere in this file. +// +// WHY ONE CARRIER AND NOT ONE CHECK PER POSITION. The grammar has fourteen type positions; +// twelve can receive a source value. Before the obligation carrier, each position that judged +// anything judged it with its own local chain of predicates -- one rule in N representations, +// where a position added later inherits nothing and a rule repaired at one position stays +// broken at the rest. A DeclaredTypeObligation names WHERE the obligation arose, WHAT was +// declared and WHAT was produced; declared_type_inhabitance is the single relation that +// decides; the position rides along so the diagnostic can locate the refusal without the +// decision procedure forking. This file is the executing evidence for the FIRST position wired +// through that carrier, and its arms are the shape every later position reuses. +// +// THE RELATION CONSUMES, IT DOES NOT RE-DERIVE. Alias identity is decided once in the tree: +// coproduct_payload_where_parent_required peels transparent aliases through +// transparent_alias_identity_agrees, and the kernel arm defers to +// kernel_value_declared_type_mismatch. A second answer to either question authored here would +// be the nicknaming failure at the level of judgments. +// +// PATH SCOPE, per DESIGN 4b's rung-per-path rule: this asserts source -> .dag acceptance only. +// The refusal sits in inference, so nothing reaches emission with a non-inhabiting list +// element -- but that is a consequence of where the wall sits, not a second measurement, and +// it is not claimed as one. + +fn violation_count(source: String, wanted: String) -> Int { + match compile_dag_diagnostic_census(source) { + CensusObserved { rows: rows } => census_total_count(rows: census_rows_of_class(rows: rows, wanted: wanted)) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +// RED ARM ONE -- the plain kernel at a structured declared type. This is the floor case, and it +// is in this file because the FIRST wiring of the carrier ACCEPTED it: the relation consulted +// only the payload-at-parent predicate, so RefusedKernelAtStructured was a declared verdict +// variant that no code path could produce. A variant nothing constructs is a decoration that +// reads as coverage, which is the rung inflation DESIGN 4b names. This arm exists so that +// deleting the kernel route from the relation goes red rather than quiet. +data kernel_at_structured_source: String = "module probe_inhabit_nega\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [7] }\n" + +test fn w_plain_kernel_at_declared_list_element_is_refused() -> Bool { + violation_count(source: kernel_at_structured_source, wanted: "DeclaredTypeNotInhabited") >= 1 +} + +// RED ARM TWO -- an arm's PAYLOAD type standing where the PARENT coproduct is declared. The +// shape gunbc#8865 recorded, measured here at the list-element position rather than inferred +// from the record-field one: two positions are two paths, and a wall proven at one says +// nothing about the other. +data payload_at_parent_source: String = "module probe_inhabit_negb\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn mk_inner() -> Inner { Inner { v: 1 } }\nfn probe() -> List { [mk_inner()] }\n" + +test fn w_arm_payload_where_parent_declared_is_refused() -> Bool { + violation_count(source: payload_at_parent_source, wanted: "DeclaredTypeNotInhabited") >= 1 +} + +// GREEN ARM -- the control that stops the wall being a wrecking ball. A genuine member of the +// declared coproduct must still compile and must raise NO inhabitance diagnostic. Without it, +// a relation that refused every list element would score identically on both red arms above, +// and the reds would establish nothing. +data inhabiting_member_source: String = "module probe_inhabit_pos\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [SameRev] }\n" + +test fn w_declared_coproduct_member_is_accepted() -> Bool { + violation_count(source: inhabiting_member_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// REACHABILITY -- an undefined name at the same position must refuse whether or not the +// inhabitance wall exists. This separates "the position is judged and the value was refused" +// from "the position is never reached at all", which the accepting arms above cannot +// distinguish on their own. It is asserted on a DIFFERENT class than the wall's, deliberately: +// keying it on DeclaredTypeNotInhabited would make it a second copy of arm one. +data undefined_name_source: String = "module probe_inhabit_reach\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [nosuchname_zzz_probe] }\n" + +test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { + violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +// UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. An optional carrier at the +// declared position is genuinely undecidable at this seam -- optionality lives in +// return_cardinality while the produced value carries the nominal coproduct, so the two are +// not comparable here without peeling a representation this relation does not own. It must +// therefore NOT refuse. This arm is what keeps Undecidable honest: if the relation ever starts +// refusing optionals it goes red, and if a future author repurposes an Undecidable reason to +// mean "unimplemented" this is the arm that notices. +data optional_carrier_source: String = "module probe_inhabit_opt\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn maybe() -> Rel? { none }\nfn probe() -> List { [maybe()] }\n" + +test fn w_optional_carrier_is_undecidable_not_refused() -> Bool { + violation_count(source: optional_carrier_source, wanted: "DeclaredTypeNotInhabited") == 0 +} diff --git a/src/v1/04_infer.dag b/src/v1/04_infer.dag index bf861404809..c18d70c2223 100644 --- a/src/v1/04_infer.dag +++ b/src/v1/04_infer.dag @@ -2156,6 +2156,10 @@ fn declared_type_inhabitance(obligation: DeclaredTypeObligation, scope: InferSco InhabitanceUndecidable { reason: UndecidableFormalUnresolved } } else if produced_name == "" { InhabitanceUndecidable { reason: UndecidableProducedIdentityErased } + } else if kernel_value_declared_type_mismatch( + formal: declared, actual: produced, + type_env: scope.type_env, source_indices: source_indices) { + InhabitanceRefused { reason: RefusedKernelAtStructured } } else if coproduct_payload_where_parent_required(formal: declared, actual: produced, scope: scope) { InhabitanceRefused { reason: RefusedPayloadAtParent } } else { From 8a3571570768fa29a9610b2399de22d226644f63 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 03:09:53 +0000 Subject: [PATCH 3/8] Install the emitted mirrors for the inhabitance carrier --- src/v1/stage0/src/v1_compiler_infer.rs | 243 ++++++++++++++++++++++++- src/v1/stage0/src/v1_std_core.rs | 8 + 2 files changed, 244 insertions(+), 7 deletions(-) diff --git a/src/v1/stage0/src/v1_compiler_infer.rs b/src/v1/stage0/src/v1_compiler_infer.rs index 250b7fafdc1..9d8e8d20fe5 100644 --- a/src/v1/stage0/src/v1_compiler_infer.rs +++ b/src/v1/stage0/src/v1_compiler_infer.rs @@ -1,7 +1,11 @@ // Generated by v1 compiler -- do not edit. // Source module: v1.compiler.infer +use self::DeclaredTypePosition::*; use self::DescentSizeExpr::*; +use self::InhabitanceRefusalReason::*; +use self::InhabitanceUndecidableReason::*; +use self::InhabitanceVerdict::*; pub use crate::extdeps_container_oci_digest::{ oci_other_digest_algorithm, oci_other_digest_encoded, }; @@ -3032,6 +3036,169 @@ pub fn coproduct_variant_payload_admits_type_name( } } +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum DeclaredTypePosition { + PositionRecordLiteralField, + PositionListElement, + PositionMapValue, + PositionDataInitializer, + PositionDeclaredReturn, + PositionLetAnnotation, + PositionVariantPayload, + PositionGenericTypeArgument, + PositionCastTarget, + PositionParameterDefault, + PositionCallableReturn, + PositionDirectCallArgument, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct DeclaredTypeObligation { + pub position: DeclaredTypePosition, + pub declared: Rc, + pub produced: Rc, + pub span: Rc, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum InhabitanceUndecidableReason { + UndecidableGenericFormal, + UndecidableOptionalCarrier, + UndecidableFormalUnresolved, + UndecidableProducedIdentityErased, +} + +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, serde::Serialize, serde::Deserialize, +)] +#[serde(tag = "_variant")] +pub enum InhabitanceRefusalReason { + RefusedPayloadAtParent, + RefusedKernelAtStructured, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +#[serde(tag = "_variant")] +pub enum InhabitanceVerdict { + Inhabits, + InhabitanceRefused { + reason: InhabitanceRefusalReason, + }, + InhabitanceUndecidable { + reason: InhabitanceUndecidableReason, + }, +} + +pub fn declared_type_position_label(position: DeclaredTypePosition) -> String { + match position.clone() { + DeclaredTypePosition::PositionRecordLiteralField => "record literal field".to_string(), + DeclaredTypePosition::PositionListElement => "list element".to_string(), + DeclaredTypePosition::PositionMapValue => "map value".to_string(), + DeclaredTypePosition::PositionDataInitializer => "data initializer".to_string(), + DeclaredTypePosition::PositionDeclaredReturn => "declared return".to_string(), + DeclaredTypePosition::PositionLetAnnotation => "let annotation".to_string(), + DeclaredTypePosition::PositionVariantPayload => "variant payload".to_string(), + DeclaredTypePosition::PositionGenericTypeArgument => "generic type argument".to_string(), + DeclaredTypePosition::PositionCastTarget => "cast target".to_string(), + DeclaredTypePosition::PositionParameterDefault => "parameter default".to_string(), + DeclaredTypePosition::PositionCallableReturn => "callable return".to_string(), + DeclaredTypePosition::PositionDirectCallArgument => "direct call argument".to_string(), + } +} + +pub fn declared_type_inhabitance( + obligation: Rc, + scope: Rc, +) -> Rc { + { + let declared = obligation.declared.clone(); + let produced = obligation.produced.clone(); + let source_indices = scope.type_env.clone().source_indices.clone(); + let declared_name = authored_name_at(source_indices.clone(), declared.clone()); + let produced_name = authored_name_at(source_indices.clone(), produced.clone()); + let either_optional = ((declared.return_cardinality.clone() == Cardinality::CardOptional) + || (produced.return_cardinality.clone() == Cardinality::CardOptional)); + let declared_is_generic = ((declared.params.clone().len() as i64) > 0); + if either_optional.clone() { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableOptionalCarrier, + }) + } else { + if declared_is_generic.clone() { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableGenericFormal, + }) + } else { + if (declared_name.clone() == "".to_string()) { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableFormalUnresolved, + }) + } else { + if (produced_name.clone() == "".to_string()) { + Rc::new(InhabitanceVerdict::InhabitanceUndecidable { + reason: InhabitanceUndecidableReason::UndecidableProducedIdentityErased, + }) + } else { + if kernel_value_declared_type_mismatch( + declared.clone(), + produced.clone(), + scope.type_env.clone(), + source_indices.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedKernelAtStructured, + }) + } else { + if coproduct_payload_where_parent_required( + declared.clone(), + produced.clone(), + scope.clone(), + ) { + Rc::new(InhabitanceVerdict::InhabitanceRefused { + reason: InhabitanceRefusalReason::RefusedPayloadAtParent, + }) + } else { + Rc::new(InhabitanceVerdict::Inhabits) + } + } + } + } + } + } + } +} + +pub fn declared_type_obligation_diags( + obligation: Rc, + scope: Rc, +) -> Rc>> { + match (*declared_type_inhabitance(obligation.clone(), scope.clone())).clone() { + InhabitanceVerdict::Inhabits => Rc::new(vec![]), + InhabitanceVerdict::InhabitanceUndecidable { reason: _, .. } => Rc::new(vec![]), + InhabitanceVerdict::InhabitanceRefused { reason: _, .. } => Rc::new(vec![make_error_node( + Rc::new(CompilerDiagnostic::DeclaredTypeNotInhabited { + position: declared_type_position_label(obligation.position.clone()), + expected: node_type_shape( + obligation.declared.clone(), + scope.type_env.clone().source_indices.clone(), + ), + got: node_type_shape( + obligation.produced.clone(), + scope.type_env.clone().source_indices.clone(), + ), + span: obligation.span.clone(), + }), + scope.module_name.clone(), + )]), + } +} + pub fn coproduct_payload_where_parent_required( formal: Rc, actual: Rc, @@ -8135,13 +8302,38 @@ if ((call_ambiguity_cands.clone().len() as i64) > 0) { } __result }); - let elem_diags = Rc::new({ - let mut __result = Vec::new(); - for r in elem_results.iter().cloned() { - __result.extend((*r.diagnostics.clone()).iter().cloned()); - } - __result - }); + let elem_inhabitance_diags = match elem_expected.clone() { + Some(declared_elem) => Rc::new({ + let mut __result = Vec::new(); + for te in typed_elements.iter().cloned() { + __result.extend( + (*declared_type_obligation_diags( + Rc::new(DeclaredTypeObligation { + position: DeclaredTypePosition::PositionListElement, + declared: declared_elem.clone(), + produced: resolved_type(te.clone()), + span: te.span.clone(), + }), + scope.clone(), + )) + .iter() + .cloned(), + ); + } + __result + }), + None => Rc::new(vec![]), + }; + let elem_diags = v1_rt::concat( + Rc::new({ + let mut __result = Vec::new(); + for r in elem_results.iter().cloned() { + __result.extend((*r.diagnostics.clone()).iter().cloned()); + } + __result + }), + elem_inhabitance_diags.clone(), + ); let elem_type_node = if ((elem_results.clone().len() as i64) > 0) { match elem_results.clone().first().cloned() { Some(r) => resolved_type(r.typed.clone()), @@ -21847,3 +22039,40 @@ pub fn reconcile_with_census_extra( }) } } + +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionRecordLiteralField; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionListElement; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionMapValue; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDataInitializer; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDeclaredReturn; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionLetAnnotation; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionVariantPayload; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionGenericTypeArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionCastTarget; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionParameterDefault; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionCallableReturn; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct PositionDirectCallArgument; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableGenericFormal; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableOptionalCarrier; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableFormalUnresolved; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct UndecidableProducedIdentityErased; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedPayloadAtParent; +#[derive(Debug, Clone, Copy, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct RefusedKernelAtStructured; diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index b6accf4e9d1..ed59d3d9e43 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -510,6 +510,12 @@ pub enum CompilerDiagnostic { permitted_callers: Rc>, span: Rc, }, + DeclaredTypeNotInhabited { + position: String, + expected: String, + got: String, + span: Rc, + }, UnlistedImportUse { name: String, span: Rc, @@ -660,6 +666,7 @@ pub fn diagnostic_to_span(d: Rc) -> Rc { annotation_attachment_refusal_origin(r.clone()) } CompilerDiagnostic::ConstructorCallAdmissionRefused { span: s, .. } => s.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { span: s, .. } => s.clone(), CompilerDiagnostic::UnlistedImportUse { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousReference { span: s, .. } => s.clone(), CompilerDiagnostic::CallArgumentNameUnknown { span: s, .. } => s.clone(), @@ -708,6 +715,7 @@ pub fn diagnostic_to_message(d: Rc) -> String { CompilerDiagnostic::BareNoneNotAdmittedByFieldType { field: f, type_name: t, declared_type: dt, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("bare 'None' cannot inhabit field '".to_string(), f.clone()), "' of '".to_string()), t.clone()), "': declared type '".to_string()), dt.clone()), "' carries no absence — it is not optional and declares no 'None' variant".to_string()), CompilerDiagnostic::SourceAnnotationRefused { refusal: r, .. } => annotation_attachment_refusal_message(r.clone()), CompilerDiagnostic::ConstructorCallAdmissionRefused { constructor_module_path: cm, constructor_decl_name: cn, caller_module_path: caller_m, caller_decl_name: caller_n, permitted_callers: permitted, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("constructor call admission refused: '".to_string(), cm.clone()), ".".to_string()), cn.clone()), "' refuses call from '".to_string()), caller_m.clone()), ".".to_string()), caller_n.clone()), "' — permitted callers: [".to_string()), permitted.clone().join(&", ".to_string())), "]".to_string()), + CompilerDiagnostic::DeclaredTypeNotInhabited { position: pos, expected: e, got: g, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("value does not inhabit its declared type at the ".to_string(), pos.clone()), ": declared '".to_string()), e.clone()), "', produced '".to_string()), g.clone()), "'".to_string()), CompilerDiagnostic::UnlistedImportUse { name: n, .. } => v1_rt::concat(v1_rt::concat("unlisted import use '".to_string(), n.clone()), "' (referenced but not in any import's name list)".to_string()), CompilerDiagnostic::AmbiguousReference { name: n, candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous reference '".to_string(), n.clone()), "': ".to_string()), ((cs.clone().len() as i64)).to_string()), " candidates: ".to_string()), cs.clone().join(&", ".to_string())), " — qualify by containment path, alias, or rename".to_string()), CompilerDiagnostic::CallArgumentNameUnknown { callee: c, argument: a, declared: ds, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("call shape mismatch calling '".to_string(), c.clone()), "': no parameter named '".to_string()), a.clone()), "' (declared: [".to_string()), ds.clone().join(&", ".to_string())), "])".to_string()), From 1509c316ce2552bb452b2414a9bc254d9a3a9dfc Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 03:55:43 +0000 Subject: [PATCH 4/8] Regenerate both mirrors from the merged authorities, not from a textual merge Git conflicted on v1_std_core.rs and AUTO-MERGED v1_compiler_infer.rs. Resolving only the file git complained about left the pair internally inconsistent: one mirror declared the roster variant and not the inhabitance one, while its sibling used both. That state is not something any emitter produces, and it does not compile. Generated files are projections of one authority and are only consistent as a SET, so both are replaced wholesale by a fresh emit from the merged .dag rather than merged file-by-file. Measured on that emit: both variants present in all three seed files, and all four inhabitance arms hold -- nega and negb refused at the list element, pos accepted, reach refused. Neither wall was eaten by the merge. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- src/v1/stage0/src/v1_std_core.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/v1/stage0/src/v1_std_core.rs b/src/v1/stage0/src/v1_std_core.rs index ef800cf006c..cf0d36f6381 100644 --- a/src/v1/stage0/src/v1_std_core.rs +++ b/src/v1/stage0/src/v1_std_core.rs @@ -527,6 +527,12 @@ pub enum CompilerDiagnostic { constructor_decl_name: String, span: Rc, }, + DeclaredTypeNotInhabited { + position: String, + expected: String, + got: String, + span: Rc, + }, UnlistedImportUse { name: String, span: Rc, @@ -678,6 +684,7 @@ pub fn diagnostic_to_span(d: Rc) -> Rc { } CompilerDiagnostic::ConstructorCallAdmissionRefused { span: s, .. } => s.clone(), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { span: s, .. } => s.clone(), + CompilerDiagnostic::DeclaredTypeNotInhabited { span: s, .. } => s.clone(), CompilerDiagnostic::UnlistedImportUse { span: s, .. } => s.clone(), CompilerDiagnostic::AmbiguousReference { span: s, .. } => s.clone(), CompilerDiagnostic::CallArgumentNameUnknown { span: s, .. } => s.clone(), @@ -727,6 +734,7 @@ pub fn diagnostic_to_message(d: Rc) -> String { CompilerDiagnostic::SourceAnnotationRefused { refusal: r, .. } => annotation_attachment_refusal_message(r.clone()), CompilerDiagnostic::ConstructorCallAdmissionRefused { constructor_module_path: cm, constructor_decl_name: cn, caller_module_path: caller_m, caller_decl_name: caller_n, permitted_callers: permitted, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("constructor call admission refused: '".to_string(), cm.clone()), ".".to_string()), cn.clone()), "' refuses call from '".to_string()), caller_m.clone()), ".".to_string()), caller_n.clone()), "' — permitted callers: [".to_string()), permitted.clone().join(&", ".to_string())), "]".to_string()), CompilerDiagnostic::AdmitCallersEntryNotDeclRef { constructor_decl_name: cn, .. } => v1_rt::concat(v1_rt::concat("admit_callers entry on '".to_string(), cn.clone()), "' is not a decl_ref(module_path: \"...\", decl_name: \"...\") call: an entry that cannot be interpreted would otherwise be dropped, silently shrinking the permitted-caller roster below what was authored".to_string()), + CompilerDiagnostic::DeclaredTypeNotInhabited { position: pos, expected: e, got: g, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("value does not inhabit its declared type at the ".to_string(), pos.clone()), ": declared '".to_string()), e.clone()), "', produced '".to_string()), g.clone()), "'".to_string()), CompilerDiagnostic::UnlistedImportUse { name: n, .. } => v1_rt::concat(v1_rt::concat("unlisted import use '".to_string(), n.clone()), "' (referenced but not in any import's name list)".to_string()), CompilerDiagnostic::AmbiguousReference { name: n, candidates: cs, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("ambiguous reference '".to_string(), n.clone()), "': ".to_string()), ((cs.clone().len() as i64)).to_string()), " candidates: ".to_string()), cs.clone().join(&", ".to_string())), " — qualify by containment path, alias, or rename".to_string()), CompilerDiagnostic::CallArgumentNameUnknown { callee: c, argument: a, declared: ds, .. } => v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat(v1_rt::concat("call shape mismatch calling '".to_string(), c.clone()), "': no parameter named '".to_string()), a.clone()), "' (declared: [".to_string()), ds.clone().join(&", ".to_string())), "])".to_string()), From ba6ce3e1e211769b041a468c2481499b64508462 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 05:08:23 +0000 Subject: [PATCH 5/8] The wall's first landing found a real one: octet rows declared as bit-records The list-element inhabitance obligation refused six data rows in emit_on_demand_match_loop_fold_family_witness, 30 elements in all. It was right, and the annotation was wrong. data match_expected_octets: List = [0, 1, 0, 0, 0] Byte here resolves through v2.std.machine to std.bit's `type Byte { bits: List }` -- a product. A plain Int does not inhabit it. The values were never bit-records: their only consumer is `emit_host_octets_byte_string(octets: List)`, which takes the octets as numbers. So the rows declared one type, held another, and were read as a third name for the second. Nothing in the corpus noticed, because the direct-call argument position is exactly the one still exempted pending gunbc#8925 -- the value flowed into a List parameter unchecked. Corrected to List, which is what the consumer's signature already said, and dropped the now-unused Byte import rather than leave a name in scope that no longer means anything here. Verified on the committed tree, both directions, one remote dispatch: fixed exit=0 inhabit_errors=0 compiled: 149 files emitted control exit=1 inhabit_errors=30 30 hard diagnostic(s) The control restores the List annotation and nothing else, so the discriminator is the annotation itself and not the harness. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...mand_match_loop_fold_family_witness_test.dag | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag index b2e166c3811..964ee6bdf2a 100644 --- a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag +++ b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag @@ -1,7 +1,7 @@ module v2.test.execution.emit_on_demand_match_loop_fold_family_witness import std.logic { Bool } -import std.types { String } +import std.types { Int, String } import std.content_hash { ContentHash, Fnv1a64Structural } import std.measure { ByteSize, byte_size } import std.cache_interface { @@ -73,7 +73,6 @@ import v2.test.emit.fold_call_closure_fixture { fold_fixture_param_canonical_arrow, fold_fixture_param_wrong_arrow, } -import v2.std.machine { Byte } import v2.std.collection { List } @@ -122,12 +121,12 @@ fn family_cache_root_for(test_id: String) -> String { concat(family_cache_root, "/", test_id) } -data match_expected_octets: List = [0, 1, 0, 0, 0] -data match_alt_expected_octets: List = [0, 2, 0, 0, 0] -data loop_expected_octets: List = [0, 1, 0, 0, 0] -data loop_alt_expected_octets: List = [0, 2, 0, 0, 0] -data fold_expected_octets: List = [0, 7, 0, 0, 0] -data fold_alt_expected_octets: List = [0, 255, 255, 255, 255] +data match_expected_octets: List = [0, 1, 0, 0, 0] +data match_alt_expected_octets: List = [0, 2, 0, 0, 0] +data loop_expected_octets: List = [0, 1, 0, 0, 0] +data loop_alt_expected_octets: List = [0, 2, 0, 0, 0] +data fold_expected_octets: List = [0, 7, 0, 0, 0] +data fold_alt_expected_octets: List = [0, 255, 255, 255, 255] fn match_fixture_inputs() -> Inputs { inputs_for_emit_host( @@ -212,7 +211,7 @@ fn mlf_family_member_run( source: Medium, member_id: String, expect_compile_skipped: Bool, - expected_octets: List + expected_octets: List ) -> Bool { match run_emit_host_cached_with_run_args( workspace_dir: workspace, From f88b81701c218f4f2a67b7740c85bf67c237b37d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 06:06:34 +0000 Subject: [PATCH 6/8] A reachability control that asserted our own class at zero was measuring nothing Review 54993 caught a contradiction between this arm's prose and its assertion, and the prose was the honest half. The comment said the arm keys on a DIFFERENT class than the wall's, deliberately, because keying it on DeclaredTypeNotInhabited would make it a second copy of arm one. The assertion was: violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 That is the wall's own class at zero, and it is satisfied identically by "the position is judged and our wall correctly stayed silent" and by "the position is never reached by anything" -- precisely the distinction the arm exists to draw. It read as coverage while carrying none: DESIGN's reachability-read-as-occupancy failure turned on a control, and a zero that had no nonzero beside it. The class was measured rather than guessed. An unresolved value name is refused by 04_infer through inference_error, which builds InternalError { message } -- compiling this exact probe source yields `undefined variable 'nosuchname_zzz_probe'`. The arm now demands that refusal. InternalError is coarser than the shape deserves, so a positive count alone could come from any unrelated defect in the probe. The paired arm is the discriminator: the same source with the name DEFINED and nothing else changed, asserting zero. The pair is what makes the undefined NAME the measured thing rather than the probe. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ..._inhabitance_list_element_witness_test.dag | 29 ++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag index 1ed96abeae2..9204c53e7ae 100644 --- a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag @@ -81,10 +81,37 @@ test fn w_declared_coproduct_member_is_accepted() -> Bool { // from "the position is never reached at all", which the accepting arms above cannot // distinguish on their own. It is asserted on a DIFFERENT class than the wall's, deliberately: // keying it on DeclaredTypeNotInhabited would make it a second copy of arm one. +// +// THE ASSERTION MUST BE POSITIVE, AND AN EARLIER REVISION OF IT WAS NOT. This arm shipped +// asserting DeclaredTypeNotInhabited == 0 -- the wall's OWN class, at zero -- while the prose +// above claimed it keyed on a different one. That assertion is satisfied identically by "the +// position is judged and our wall correctly stayed silent" and by "the position is never +// reached by anything", which is precisely the distinction the arm exists to make, so it read +// as coverage while carrying none. It is DESIGN's reachability-read-as-occupancy failure +// turned on a control: a zero is only readable beside a nonzero. Corrected to demand the +// refusal it was named for (review 54993). +// +// WHY InternalError IS THE CLASS: an unresolved value name is refused by v1.compiler.04_infer +// through inference_error, which constructs InternalError { message } -- measured, not assumed +// ("undefined variable 'nosuchname_zzz_probe'" against this exact source). It is coarser than +// the shape deserves, and that coarseness is why the paired green arm below is not optional: +// alone, a positive InternalError count could be produced by any unrelated defect in the +// probe. The pair is what makes the undefined NAME the thing being measured. data undefined_name_source: String = "module probe_inhabit_reach\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn probe() -> List { [nosuchname_zzz_probe] }\n" +// The same source with the name DEFINED and nothing else changed. It is the discriminator for +// the arm above: if this also reported InternalError, the positive count there would be an +// artifact of the probe rather than evidence about the name. +data defined_name_source: String = "module probe_inhabit_reach_ok\nimport std.types { Int }\ntype Inner { v: Int }\ntype Rel = | Wrapped(Inner) | SameRev\nfn mk() -> Rel { SameRev }\nfn probe() -> List { [mk()] }\n" + test fn w_undefined_name_at_the_same_position_still_refuses() -> Bool { - violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 + violation_count(source: undefined_name_source, wanted: "InternalError") > 0 + && violation_count(source: undefined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 +} + +test fn w_reachability_control_discriminates_on_the_name() -> Bool { + violation_count(source: defined_name_source, wanted: "InternalError") == 0 + && violation_count(source: defined_name_source, wanted: "DeclaredTypeNotInhabited") == 0 } // UNDECIDABLE IS A PROPERTY OF THE FACTS, NEVER OF THE WIRING. An optional carrier at the From 30ce9d2c07b4fd0601337ffedbd5cebc3d661669 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 10:38:17 +0000 Subject: [PATCH 7/8] The octet rows say why they are Int, and name the carrier that would replace them Review 55052 approved and asked, non-blocking, for a tracked pointer toward a proper octet carrier, on the ground that no Octet alias exists today. One does, and it changes the shape of the answer: extdeps.network.ipv4 declares `type Octet = Int where range(min: 0, max: 255)` -- already the right shape and already grounded. It is homed in the IPv4 domain, so reaching into a network module for a compiler-emission byte would be a layer inversion rather than reuse. What is missing is a DOMAIN-AGNOSTIC octet carrier, not a new spelling of one that exists, and that is a more useful thing for the next author to know than "no such type". The annotation records three facts a reader of these rows would otherwise have to re-derive: that Byte is a bit-record so the Int literals never inhabited it; that List is the consumer's own declared type rather than a weakened carrier; and that Int is nonetheless weaker than an octet deserves, with the replacement named and the order stated -- the parameter moves first, since the declaration follows its consumer. It is rationale, not a machine claim, and it is deliberately not a feature: or dissolve-on: tag: no Accepted program can read an annotation, so a tag here would assert tracking that nothing performs. When the carrier lands, the obligation belongs on it. Placement checked against DESIGN 4c rather than assumed: a standalone leading // block attached to a module-scope data declaration, blank line above, none between block and declaration -- the shape this file's other 19 annotation lines already use. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...nd_match_loop_fold_family_witness_test.dag | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag index 964ee6bdf2a..8c93523b661 100644 --- a/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag +++ b/src/v2/test/claim/execution/emit_on_demand_match_loop_fold_family_witness_test.dag @@ -121,6 +121,25 @@ fn family_cache_root_for(test_id: String) -> String { concat(family_cache_root, "/", test_id) } +// WHY List AND NOT List, AND WHAT WOULD REPLACE IT. These rows are octet +// values compared against emitted bytes. They were declared List while holding +// integers, which the list-element inhabitance obligation refused: std.bit's Byte is +// `type Byte { bits: List }`, a bit-record, so an Int literal never inhabited it. +// The consumer's signature already carried the right type -- v2.compiler.emit_host +// `emit_host_octets_byte_string(octets: List)` -- so this is the declaration +// agreeing with its single authority, not a carrier weakened to satisfy a wall. +// +// Int is nonetheless weaker than the values deserve: an octet is 0..255 and nothing +// here says so. The correctly shaped type already exists and is grounded -- +// extdeps.network.ipv4 `Octet`, declared as Int refined by range(min: 0, max: 255) -- +// but it is homed in the IPv4 domain, and reaching into a network module for a +// compiler-emission byte would be the layer inversion DESIGN 3 warns about rather +// than a reuse. What is missing is a domain-agnostic octet carrier, not a new +// spelling of one that exists. +// +// So the pointer, deliberately stated as rationale rather than a machine claim: when +// such a carrier lands, these rows and emit_host_octets_byte_string's parameter move +// to it together -- the parameter first, since the declaration follows its consumer. data match_expected_octets: List = [0, 1, 0, 0, 0] data match_alt_expected_octets: List = [0, 2, 0, 0, 0] data loop_expected_octets: List = [0, 1, 0, 0, 0] From 9cccff4b34da0d3414a4bf97b2a52f2f598afa61 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 11:03:14 +0000 Subject: [PATCH 8/8] =?UTF-8?q?Every=20arm=20in=20this=20witness=20was=20e?= =?UTF-8?q?nrolled,=20reviewed,=20cited=20=E2=80=94=20and=20executed=20by?= =?UTF-8?q?=20nothing?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The file declared ReadsLiveTree. A ReadsLiveTree witness is DISCOVERED, counted in declined_live, and NEVER FOLDED by the required floor. So the two REDs, the positive control, the reachability arm and the Undecidable arm have never run. That is worse than having written no test. Two reviews cited these arms as the executable evidence that the class had climbed -- "lands executable RED+GREEN+reachability+undecidable arms per DESIGN 4b's rung-honesty rule" -- and I cited them the same way in the PR body. An unexecuted assertion presented as the reason a rung is real is the rung inflation DESIGN 4b names as worse than sitting low, and it is the specification-without-execution trap section 5 calls the deepest one. I did not find this by reading my own file. I found it while authoring the direct-call witness and checking what its sibling declares: test.claim.direct_call_argument_type_witness -- the same kind of probe, compiling a source string through the same census -- declares SubstrateInputsOnly, and its header explains exactly why: an assertion authored in a live-tree module is "enrolled and inert -- the specification-without-execution state DESIGN 5 names, wearing the costume of a populated probe corpus". Nothing here needs a live read. Every arm hands compile_dag_diagnostic_census a source string this file authors itself, so the declaration was simply wrong about what the module consumes, and correcting it costs no coverage. WHAT I AM NOT CLAIMING. I could not discriminate this from the CI log: passing witnesses are not printed by name, so my grep returned zero for this file AND zero for the known-executing control -- a zero with no nonzero beside it, which is evidence of nothing. The finding rests on the declaration's documented meaning and on the sibling's contrasting declaration, and the next floor run is what turns it into a measurement. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_014QRQgQyZvAgydCNpFGLR2b --- ...ype_inhabitance_list_element_witness_test.dag | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag index 9204c53e7ae..25b0a6312d1 100644 --- a/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag +++ b/dag/test/claim/declared_type_inhabitance_list_element_witness_test.dag @@ -8,9 +8,19 @@ import gunbc.compile_diagnostic_census { census_total_count } import std.types { String, Bool, Int } -import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } - -data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +// SUBSTRATE-ONLY, AND THE EARLIER ReadsLiveTree DECLARATION MADE EVERY ARM BELOW INERT. A +// ReadsLiveTree witness is DISCOVERED, counted in declined_live, and NEVER FOLDED -- so these +// arms were enrolled, reviewed, cited as this PR's executable evidence, and executed by nothing. +// That is the specification-without-execution trap DESIGN 5 calls the deepest one, and it is +// worse here than a missing test would have been, because the arms were named as the reason the +// class had climbed. The sibling test.claim.direct_call_argument_type_witness had already made +// this exact move and said why: an assertion in a live-tree module is "enrolled and inert ... +// wearing the costume of a populated probe corpus". This file needs no live read -- every arm +// hands compile_dag_diagnostic_census a source STRING it authors itself -- so nothing is lost by +// declaring what it actually consumes. +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // THE FLOOR CLAUSE THIS GUARDS: a value accepted at a declared-type position inhabits that // declared type. DESIGN names it as floor, so a breach is a below-baseline safety regression