From dfb87084e10a7be90a14ed1caa1bd44a9777a3e8 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 21:13:06 +0000 Subject: [PATCH 01/12] Join corpus Int and kernel Int before inhabitance alias unfold. A bind_outcome continuation constructing Acc { n: 0 } refused record_field_value_does_not_inhabit because the field was kernel dag_binding_type_int and the literal produced the Int alias (GroupCompletion). Recognize both names as integer_int_type_node on each side of the declared-type obligation. Co-authored-by: Cursor --- src/v2/compiler/04_infer.dag | 61 +++++++++- ...c_closure_outcome_construct_probe_test.dag | 109 ++++++++++++++++++ src/v2/workflow/floor_pure_producer_share.dag | 7 ++ 3 files changed, 173 insertions(+), 4 deletions(-) create mode 100644 src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 93fcded72d2..bcf12b745ae 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -69,7 +69,7 @@ import std.optional { optional_absent, optional_present } -import v2.std.qualified_name { QualifiedName, declaration_reference_node, declaration_reference_path_optional, qualified_name_to_dotted_string, lexical_reference_label_optional, parameter_reference_path_optional } +import v2.std.qualified_name { QualifiedName, declaration_reference_node, declaration_reference_path_optional, qualified_name_last_segment, qualified_name_to_dotted_string, lexical_reference_label_optional, parameter_reference_path_optional } import v2.std.node_query { BinderParts, binder_node, binder_node_parts, construct_field_edges, construct_tag_optional, declared_field_from_edge, find_labeled_child } import v2.std.symbol_index { RecordTypePayload, SymbolIndex, VariantArmPayload, symbol_index_declared_payload_at, symbol_index_declared_type_params_at, symbol_index_lookup } import v2.std.grammar { node_atom_identity_optional } @@ -146,6 +146,7 @@ import v2.std.diagnostic { outcome_accepted, rejected_with_pending } +import v2.std.integer { integer_int_type_node } import v2.std.logic { bool_node } import v2.std.node { StructuralLabel, @@ -3568,6 +3569,58 @@ fn infer_match_generic_formal_or_carrier(formal: Node, produced: Node, type_para // reaches every judgment: the declared type, the produced type and the produced type's refinement carrier are // all presented with transparent aliases unfolded. The carrier is READ from the produced type as written (a // refinement is never unfolded, so its declaration is still the one found), then normalized like the rest. +// THE KERNEL VALUE TYPE AND THE CORPUS NAME ARE ONE TYPE. `type Int = GroupCompletion` +// (v2.std.integer) and the kernel atom `dag_binding_type_int` (integer_int_type_node) answer the +// same value-type question. Alias-normalizing first unfolds Int to GroupCompletion and then +// the judge compares that product to the kernel atom -- record_field_value_does_not_inhabit for +// `n: 0` at a field declared Int (the N7 bind_outcome reconstruct). The kernel spelling is +// recognized BEFORE unfold, on both sides, so a produced `Int` inhabits a declared kernel Int +// (and the converse). Bool is the same join infer_established_value_type_optional already owns. +fn infer_kernel_value_type_optional(t: Node) -> Optional { + if infer_type_equal_ignoring_provenance(a: t, b: integer_int_type_node()) { + optional_present(value: integer_int_type_node()) + } else if infer_type_equal_ignoring_provenance(a: t, b: bool_node()) { + optional_present(value: bool_node()) + } else { + match infer_kernel_value_type_from_name(id: infer_type_name_symbol(t: t)) { + Present { value: k } => optional_present(value: k) + Absent => + match node_atom_identity_optional(node: t) { + Present { value: id } => dag_binding_denotation(sym: id) + Absent => optional_absent() + } + } + } +} + +fn infer_type_name_symbol(t: Node) -> Optional { + match declaration_reference_path_optional(node: t) { + Present { value: path } => qualified_name_last_segment(qn: path) + Absent => node_atom_identity_optional(node: t) + } +} + +fn infer_kernel_value_type_from_name(id: Optional) -> Optional { + match id { + Absent => optional_absent() + Present { value: s } => + if (s == ^dag_binding_type_int) || (s == ^Int) { + optional_present(value: integer_int_type_node()) + } else if (s == ^bool_node_symbol) || (s == ^Bool) { + optional_present(value: bool_node()) + } else { + optional_absent() + } + } +} + +fn infer_inhabitance_type_normalized(t: Node, declarations: SymbolIndex) -> Node { + match infer_kernel_value_type_optional(t: t) { + Present { value: k } => k + Absent => infer_type_alias_normalized(t: t, declarations: declarations) + } +} + fn infer_declared_type_obligation( position: DeclaredTypePosition, parameter_identity: Symbol, @@ -3580,10 +3633,10 @@ fn infer_declared_type_obligation( DeclaredTypeObligation { position: position, parameter_identity: parameter_identity, - declared: infer_type_alias_normalized(t: declared, declarations: declarations), - produced: infer_type_alias_normalized(t: produced, declarations: declarations), + declared: infer_inhabitance_type_normalized(t: declared, declarations: declarations), + produced: infer_inhabitance_type_normalized(t: produced, declarations: declarations), produced_declared_carrier: match refinement_declared_carrier(index: declarations, source_type: produced) { - Present { value: c } => Present { value: infer_type_alias_normalized(t: c, declarations: declarations) } + Present { value: c } => Present { value: infer_inhabitance_type_normalized(t: c, declarations: declarations) } Absent => Absent }, application: application, diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag new file mode 100644 index 00000000000..1e754ed0eb8 --- /dev/null +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -0,0 +1,109 @@ +module v2.test.claim.compiler.generic_closure_outcome_construct_probe + +import v2.compiler.infer { + infer, + infer_kernel_value_type_optional, + infer_type_equal_ignoring_provenance +} +import v2.compiler.name_resolve { + Admission, + ResolutionSubject, + resolution_context, + resolve_in_context +} +import v2.compiler.normalized_tree { NormalizedTree } +import v2.compiler.program_assembly { module_roots_from_source_root_ingest } +import v2.compiler.resolve { ResolvedTree } +import v2.compiler.source_authority { SourceRootIngest } +import v2.extdeps.languages.dag { dag_language_model } +import v2.std.cross_tree.resolution { source_root_index_empty } +import v2.std.diagnostic { Accepted, None, Outcome, Rejected, Some, diagnostics_fatal_reason } +import v2.std.integer { integer_int_type_node } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import v2.std.node { Atom, Node, Symbol, TypeNode, node_synthetic } +import std.optional { Absent, Present } +import v2.std.qualified_name { qualified_name_from_dotted_string } +import v2.std.resolution_policy { default_name_resolution_policy } +import v2.std.text { String } +import std.algebra { Empty, FreeMonoid } +import v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_test { + rcf_read, + rcf_refuses_with +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// SUBJECT: infer_declared_type_obligation's kernel-value join (infer_kernel_value_type_optional). +// A generic-variant construct inside bind_outcome's continuation was refusing +// record_field_value_does_not_inhabit because a field declared Int (kernel atom +// dag_binding_type_int) was judged against a produced Int (the corpus alias +// type Int = GroupCompletion). The join recognizes both names as integer_int_type_node +// before alias unfold. +// +// SUPPLIED claims judge that join at its own interface. ONE claim runs the real +// ingest→resolve→infer route on the bind_outcome-shaped fixture. + +data gbo_lambda_source: String = "module v2.test.gbo_lambda\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\nfn bind(o: Out, f: fn(T) -> Out) -> Out {\n match o {\n Rej { n: n } => Rej { n: n }\n Acc { value: v, n: _ } => f(v)\n }\n}\n\nfn g() -> Out {\n bind(o: Acc { value: 1, n: 0 }, f: fn(x) { Acc { value: x, n: 0 } })\n}\n" + +data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\nfn bind(o: Out, f: fn(T) -> Out) -> Out {\n match o {\n Rej { n: n } => Rej { n: n }\n Acc { value: v, n: _ } => f(v)\n }\n}\n\nfn g() -> Out {\n bind(o: Acc { value: 1, n: 0 }, f: fn(x) { Acc { value: x, n: true } })\n}\n" + +data gbo_ingest: SourceRootIngest = [ + rcf_read(source: gbo_lambda_source, id: ^gbo_lambda_read, unit: ^gbo_lambda_cu, path: "src/v2/test/fixture/gbo/lambda.dag"), + rcf_read(source: gbo_lambda_bad_source, id: ^gbo_lambda_bad_read, unit: ^gbo_lambda_bad_cu, path: "src/v2/test/fixture/gbo/lambda_bad.dag") +] + +fn gbo_fixture_normalized() -> Outcome> { + module_roots_from_source_root_ingest(ingest: gbo_ingest, lm: dag_language_model()) +} + +fn gbo_resolve_subject(subject: String) -> Outcome { + match gbo_fixture_normalized() { + Rejected { diagnostics: d } => Rejected { diagnostics: d } + Accepted { value: roots, diagnostics: _ } => + resolve_in_context( + context: resolution_context(lm: dag_language_model(), roots: roots, index: source_root_index_empty(), active_roots: Empty, policy: default_name_resolution_policy()), + admission: Admission { + subject: ResolutionSubject { name: qualified_name_from_dotted_string(dotted: subject) }, + imports: Empty + } + ).resolved + } +} + +fn gbo_resolved_lambda() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_lambda") } +fn gbo_resolved_lambda_bad() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_lambda_bad") } + +fn gbo_atom(id: Symbol) -> Node { + node_synthetic(kind: TypeNode { connective: Atom { identity: id } }, children: []) +} + +fn gbo_is_kernel_int(t: Node) -> Bool { + match infer_kernel_value_type_optional(t: t) { + Absent => false + Present { value: k } => infer_type_equal_ignoring_provenance(a: k, b: integer_int_type_node()) + } +} + +test fn gbo_an_int_name_atom_is_the_kernel_int_holds() -> Bool { + gbo_is_kernel_int(t: gbo_atom(id: ^Int)) +} + +test fn gbo_a_kernel_int_atom_is_the_kernel_int_holds() -> Bool { + gbo_is_kernel_int(t: gbo_atom(id: ^dag_binding_type_int)) +} + +test fn gbo_a_bool_name_is_not_the_kernel_int_holds() -> Bool { + !gbo_is_kernel_int(t: gbo_atom(id: ^Bool)) +} + +// THE ROUTE: bind_outcome-shaped reconstruct Acc { value: x, n: 0 } at Out. +// Before the join this refused record_field_value_does_not_inhabit at n +// (declared dag_binding_type_int, produced Int). Deleting the join turns this green-to-red. +test fn gbo_the_bind_outcome_reconstruct_does_not_refuse_int_field_inhabitance_holds() -> Bool { + !rcf_refuses_with(resolved: gbo_resolved_lambda(), reason: ^record_field_value_does_not_inhabit) +} + +// CONTROL one term away: n: true at a field declared Int still refuses. +test fn gbo_a_bool_at_the_int_field_still_refuses_holds() -> Bool { + rcf_refuses_with(resolved: gbo_resolved_lambda_bad(), reason: ^record_field_value_does_not_inhabit) +} diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 5a618632a1c..9b7dccec08b 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -591,6 +591,13 @@ fn floor_single_claim_fill_debt_active_claims() -> List { // Trigger: assemble plus infer of a one-module fixture runs under the per-claim budget // (gunbc.recurring_failure_mode shared_precondition_re_derived_once_per_claim_frame). data floor_single_claim_fill_debt: List = [ + SingleClaimFillDebtModule { + module: "v2.test.claim.compiler.generic_closure_outcome_construct_probe", + claims: [ + SingleClaimFillDebtClaim { claim: "gbo_the_bind_outcome_reconstruct_does_not_refuse_int_field_inhabitance_holds", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "gbo_a_bool_at_the_int_field_still_refuses_holds", standing: ActiveFillDebt } + ] + }, SingleClaimFillDebtModule { module: "v2.test.claim.compiler.collection_concat_realization", claims: [ From 0cc50a69a9f61c9487ca2d37197932a6eb3a54a4 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 21:30:22 +0000 Subject: [PATCH 02/12] Join kernel Int by declaration roster, not last-segment spelling. A path or atom spelled Int is not the kernel type. The inhabitance join now asks dag_kernel_type_declaration_binding_optional for the full path (same roster resolve uses) and otherwise only dag_binding_denotation, so a module's own type Int = | Mine still refuses let y: Int = 1. Co-authored-by: Cursor --- src/v2/compiler/04_infer.dag | 46 +++++++------------ ...c_closure_outcome_construct_probe_test.dag | 29 ++++++++++-- 2 files changed, 40 insertions(+), 35 deletions(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index bcf12b745ae..fbedfd0a725 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -40,6 +40,7 @@ import v2.extdeps.languages.dag { DagCanonicalStringLiteral, DagCanonicalLiteral, dag_binding_denotation, + dag_kernel_type_declaration_binding_optional, dag_canonical_literal_from_node, dag_declared_inhabitants_root, dag_declared_inhabitants_subject_field, @@ -3569,21 +3570,27 @@ fn infer_match_generic_formal_or_carrier(formal: Node, produced: Node, type_para // reaches every judgment: the declared type, the produced type and the produced type's refinement carrier are // all presented with transparent aliases unfolded. The carrier is READ from the produced type as written (a // refinement is never unfolded, so its declaration is still the one found), then normalized like the rest. -// THE KERNEL VALUE TYPE AND THE CORPUS NAME ARE ONE TYPE. `type Int = GroupCompletion` -// (v2.std.integer) and the kernel atom `dag_binding_type_int` (integer_int_type_node) answer the -// same value-type question. Alias-normalizing first unfolds Int to GroupCompletion and then -// the judge compares that product to the kernel atom -- record_field_value_does_not_inhabit for -// `n: 0` at a field declared Int (the N7 bind_outcome reconstruct). The kernel spelling is -// recognized BEFORE unfold, on both sides, so a produced `Int` inhabits a declared kernel Int -// (and the converse). Bool is the same join infer_established_value_type_optional already owns. +// THE KERNEL VALUE TYPE AND THE CORPUS DECLARATION ARE ONE TYPE. `v2.std.integer.Int` +// (`type Int = GroupCompletion`) and the kernel atom `dag_binding_type_int` +// (integer_int_type_node) answer the same value-type question. Alias-normalizing first unfolds +// that alias to GroupCompletion and then the judge compares that product to the kernel atom. +// Recognition is BY AUTHORITY, NOT BY SPELLING: a declaration reference joins only when +// dag_kernel_type_declaration_binding_optional admits the FULL path (the same roster resolve +// uses). A last-segment `Int` would recapture a module's own `type Int = | Mine` and admit +// `let y: Int = 1` (gunbc.recurring_failure_mode kernel_type_spelling_captured_a_module_declaration; +// review 77259). An atom joins only through dag_binding_denotation (binding -> value type). fn infer_kernel_value_type_optional(t: Node) -> Optional { if infer_type_equal_ignoring_provenance(a: t, b: integer_int_type_node()) { optional_present(value: integer_int_type_node()) } else if infer_type_equal_ignoring_provenance(a: t, b: bool_node()) { optional_present(value: bool_node()) } else { - match infer_kernel_value_type_from_name(id: infer_type_name_symbol(t: t)) { - Present { value: k } => optional_present(value: k) + match declaration_reference_path_optional(node: t) { + Present { value: path } => + match dag_kernel_type_declaration_binding_optional(path: path) { + Present { value: binding } => dag_binding_denotation(sym: binding) + Absent => optional_absent() + } Absent => match node_atom_identity_optional(node: t) { Present { value: id } => dag_binding_denotation(sym: id) @@ -3593,27 +3600,6 @@ fn infer_kernel_value_type_optional(t: Node) -> Optional { } } -fn infer_type_name_symbol(t: Node) -> Optional { - match declaration_reference_path_optional(node: t) { - Present { value: path } => qualified_name_last_segment(qn: path) - Absent => node_atom_identity_optional(node: t) - } -} - -fn infer_kernel_value_type_from_name(id: Optional) -> Optional { - match id { - Absent => optional_absent() - Present { value: s } => - if (s == ^dag_binding_type_int) || (s == ^Int) { - optional_present(value: integer_int_type_node()) - } else if (s == ^bool_node_symbol) || (s == ^Bool) { - optional_present(value: bool_node()) - } else { - optional_absent() - } - } -} - fn infer_inhabitance_type_normalized(t: Node, declarations: SymbolIndex) -> Node { match infer_kernel_value_type_optional(t: t) { Present { value: k } => k diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index 1e754ed0eb8..8e8b7edc9e5 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -20,9 +20,10 @@ import v2.std.cross_tree.resolution { source_root_index_empty } import v2.std.diagnostic { Accepted, None, Outcome, Rejected, Some, diagnostics_fatal_reason } import v2.std.integer { integer_int_type_node } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.occurrence_identity { OccurrenceSynthetic } import v2.std.node { Atom, Node, Symbol, TypeNode, node_synthetic } import std.optional { Absent, Present } -import v2.std.qualified_name { qualified_name_from_dotted_string } +import v2.std.qualified_name { declaration_reference_node, qualified_name_from_dotted_string } import v2.std.resolution_policy { default_name_resolution_policy } import v2.std.text { String } import std.algebra { Empty, FreeMonoid } @@ -37,8 +38,8 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // A generic-variant construct inside bind_outcome's continuation was refusing // record_field_value_does_not_inhabit because a field declared Int (kernel atom // dag_binding_type_int) was judged against a produced Int (the corpus alias -// type Int = GroupCompletion). The join recognizes both names as integer_int_type_node -// before alias unfold. +// type Int = GroupCompletion). The join keys the kernel declaration roster (full path) +// and dag_binding_denotation, not a last-segment Int spelling. // // SUPPLIED claims judge that join at its own interface. ONE claim runs the real // ingest→resolve→infer route on the bind_outcome-shaped fixture. @@ -84,8 +85,26 @@ fn gbo_is_kernel_int(t: Node) -> Bool { } } -test fn gbo_an_int_name_atom_is_the_kernel_int_holds() -> Bool { - gbo_is_kernel_int(t: gbo_atom(id: ^Int)) +test fn gbo_an_int_spelling_atom_is_not_the_kernel_int_holds() -> Bool { + !gbo_is_kernel_int(t: gbo_atom(id: ^Int)) +} + +test fn gbo_a_module_int_declaration_is_not_the_kernel_int_holds() -> Bool { + !gbo_is_kernel_int( + t: declaration_reference_node( + qn: qualified_name_from_dotted_string(dotted: "v2.test.gbo_shadow.Int"), + occurrence_id: OccurrenceSynthetic + ) + ) +} + +test fn gbo_the_integer_int_declaration_is_the_kernel_int_holds() -> Bool { + gbo_is_kernel_int( + t: declaration_reference_node( + qn: qualified_name_from_dotted_string(dotted: "v2.std.integer.Int"), + occurrence_id: OccurrenceSynthetic + ) + ) } test fn gbo_a_kernel_int_atom_is_the_kernel_int_holds() -> Bool { From 8ebe0a1ed0079925723185e9ade190abd6e6ceae Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Tue, 6 Oct 2026 23:36:45 +0000 Subject: [PATCH 03/12] Make the Int-field red a data construct, not a lambda body. Floor 37534388259 failed gbo_a_bool_at_the_int_field_still_refuses_holds because the bind_outcome lambda with n: true did not produce record_field_value_does_not_inhabit. Acc { value: 1, n: true } at Out is the same one-term control the record-field witnesses use. Co-authored-by: Cursor --- .../generic_closure_outcome_construct_probe_test.dag | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index 8e8b7edc9e5..0cdf799b639 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -46,7 +46,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data gbo_lambda_source: String = "module v2.test.gbo_lambda\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\nfn bind(o: Out, f: fn(T) -> Out) -> Out {\n match o {\n Rej { n: n } => Rej { n: n }\n Acc { value: v, n: _ } => f(v)\n }\n}\n\nfn g() -> Out {\n bind(o: Acc { value: 1, n: 0 }, f: fn(x) { Acc { value: x, n: 0 } })\n}\n" -data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\nfn bind(o: Out, f: fn(T) -> Out) -> Out {\n match o {\n Rej { n: n } => Rej { n: n }\n Acc { value: v, n: _ } => f(v)\n }\n}\n\nfn g() -> Out {\n bind(o: Acc { value: 1, n: 0 }, f: fn(x) { Acc { value: x, n: true } })\n}\n" +data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\ndata bad: Out = Acc { value: 1, n: true }\n" data gbo_ingest: SourceRootIngest = [ rcf_read(source: gbo_lambda_source, id: ^gbo_lambda_read, unit: ^gbo_lambda_cu, path: "src/v2/test/fixture/gbo/lambda.dag"), @@ -122,7 +122,9 @@ test fn gbo_the_bind_outcome_reconstruct_does_not_refuse_int_field_inhabitance_h !rcf_refuses_with(resolved: gbo_resolved_lambda(), reason: ^record_field_value_does_not_inhabit) } -// CONTROL one term away: n: true at a field declared Int still refuses. +// CONTROL one term away: Acc { value: 1, n: true } at Out still refuses +// record_field_value_does_not_inhabit. The lambda form of this red did not +// surface that reason (floor 37534388259 returned Bool(false)). test fn gbo_a_bool_at_the_int_field_still_refuses_holds() -> Bool { rcf_refuses_with(resolved: gbo_resolved_lambda_bad(), reason: ^record_field_value_does_not_inhabit) } From 48243ea4fdbba58edaded482ab68b444fe8dba02 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Wed, 7 Oct 2026 00:53:45 +0000 Subject: [PATCH 04/12] Use a record construct for the Int-field inhabitance red. A generic variant Acc { n: true } did not refuse record_field_value_does_not_inhabit on the floor (37547532785). Box { n: true, m: 3 } is the record-field wall's own specimen. Co-authored-by: Cursor --- .../generic_closure_outcome_construct_probe_test.dag | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index 0cdf799b639..3bc014b0d47 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -46,7 +46,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data gbo_lambda_source: String = "module v2.test.gbo_lambda\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\nfn bind(o: Out, f: fn(T) -> Out) -> Out {\n match o {\n Rej { n: n } => Rej { n: n }\n Acc { value: v, n: _ } => f(v)\n }\n}\n\nfn g() -> Out {\n bind(o: Acc { value: 1, n: 0 }, f: fn(x) { Acc { value: x, n: 0 } })\n}\n" -data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\ndata bad: Out = Acc { value: 1, n: true }\n" +data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Box {\n n: Int\n m: Int\n}\n\ndata bad: Box = Box { n: true, m: 3 }\n" data gbo_ingest: SourceRootIngest = [ rcf_read(source: gbo_lambda_source, id: ^gbo_lambda_read, unit: ^gbo_lambda_cu, path: "src/v2/test/fixture/gbo/lambda.dag"), @@ -122,9 +122,9 @@ test fn gbo_the_bind_outcome_reconstruct_does_not_refuse_int_field_inhabitance_h !rcf_refuses_with(resolved: gbo_resolved_lambda(), reason: ^record_field_value_does_not_inhabit) } -// CONTROL one term away: Acc { value: 1, n: true } at Out still refuses -// record_field_value_does_not_inhabit. The lambda form of this red did not -// surface that reason (floor 37534388259 returned Bool(false)). +// CONTROL: a record field declared Int holding true still refuses. A generic +// *variant* Acc { n: true } does not surface record_field_value_does_not_inhabit +// on this path (floor 37547532785 / 37534388259 returned Bool(false)). test fn gbo_a_bool_at_the_int_field_still_refuses_holds() -> Bool { rcf_refuses_with(resolved: gbo_resolved_lambda_bad(), reason: ^record_field_value_does_not_inhabit) } From 41afbbbbd765384d5268ae14f347037bf72b8042 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 8 Oct 2026 21:29:10 +0000 Subject: [PATCH 05/12] v2 infer: kernel recognition re-enters after every alias step; route claim must be accepted and decided infer_inhabitance_type_normalized recognized the kernel Int only at its input and then delegated to infer_type_alias_normalized, so 'type Alias = v2.std.integer.Int' unfolded past the corpus Int while a direct reference became the kernel atom -- a false refusal at the declared-type obligation. Recognition now runs at each alias step and inside every Instantiation argument; the full-path roster check is unchanged. The route claim asserted only the absence of record_field_value_does_not_inhabit, which a resolve refusal or a different infer refusal also satisfies. It is now rcf_member_accepted_and_decided on a direct generic-variant construct. Adds the alias control. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/04_infer.dag | 23 ++++++++++++- ...c_closure_outcome_construct_probe_test.dag | 32 +++++++++++++++---- src/v2/workflow/floor_pure_producer_share.dag | 3 +- 3 files changed, 49 insertions(+), 9 deletions(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index fbedfd0a725..68eadd26386 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -3600,10 +3600,31 @@ fn infer_kernel_value_type_optional(t: Node) -> Optional { } } +// KERNEL RECOGNITION IS PART OF EVERY NORMALIZATION STEP, not only the first. Recognizing the kernel +// type at the input and then delegating to infer_type_alias_normalized would unfold +// `type Alias = v2.std.integer.Int` straight past the corpus Int into GroupCompletion, while a +// direct v2.std.integer.Int becomes the kernel atom -- one type presented two ways, a false refusal. +// So each alias step re-enters this function, and so does every Instantiation argument. fn infer_inhabitance_type_normalized(t: Node, declarations: SymbolIndex) -> Node { match infer_kernel_value_type_optional(t: t) { Present { value: k } => k - Absent => infer_type_alias_normalized(t: t, declarations: declarations) + Absent => + match infer_type_alias_unfolded(t: t, declarations: declarations) { + Present { value: unfolded } => infer_inhabitance_type_normalized(t: unfolded, declarations: declarations) + Absent => + match t.kind { + TypeNode { connective: Instantiation } => + Node { + kind: t.kind, + children: fold(t.children, init: Empty, f: fn(acc, e) { + list_snoc_item(xs: acc, item: Edge { label: e.label, target: infer_inhabitance_type_normalized(t: e.target, declarations: declarations) }) + }), + occurrence_id: t.occurrence_id + } + TypeNode { connective: _ } => t + ComputationNode { behavior: _ } => t + } + } } } diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index 3bc014b0d47..78905d1c076 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -28,6 +28,7 @@ import v2.std.resolution_policy { default_name_resolution_policy } import v2.std.text { String } import std.algebra { Empty, FreeMonoid } import v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_test { + rcf_member_accepted_and_decided, rcf_read, rcf_refuses_with } @@ -44,13 +45,19 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // SUPPLIED claims judge that join at its own interface. ONE claim runs the real // ingest→resolve→infer route on the bind_outcome-shaped fixture. -data gbo_lambda_source: String = "module v2.test.gbo_lambda\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\nfn bind(o: Out, f: fn(T) -> Out) -> Out {\n match o {\n Rej { n: n } => Rej { n: n }\n Acc { value: v, n: _ } => f(v)\n }\n}\n\nfn g() -> Out {\n bind(o: Acc { value: 1, n: 0 }, f: fn(x) { Acc { value: x, n: 0 } })\n}\n" +data gbo_lambda_source: String = "module v2.test.gbo_lambda\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\nfn bind(o: Out, f: fn(T) -> Out) -> Out {\n match o {\n Rej { n: n } => Rej { n: n }\n Acc { value: v, n: _ } => f(v)\n }\n}\n\nfn g() -> Out {\n bind(o: Acc { value: 1, n: 0 }, f: fn(x) { Acc { value: x, n: 0 } })\n}\n\nfn h() -> Out {\n Acc { value: 1, n: 0 }\n}\n" data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Box {\n n: Int\n m: Int\n}\n\ndata bad: Box = Box { n: true, m: 3 }\n" +data gbo_integer_stub_source: String = "module v2.std.integer\n\ntype Nat = Zero | One\n\ntype Int = Nat\n" + +data gbo_alias_source: String = "module v2.test.gbo_alias\n\nimport v2.std.integer { Int }\n\ntype Alias = v2.std.integer.Int\n\nfn same(x: Alias) -> v2.std.integer.Int {\n x\n}\n" + data gbo_ingest: SourceRootIngest = [ rcf_read(source: gbo_lambda_source, id: ^gbo_lambda_read, unit: ^gbo_lambda_cu, path: "src/v2/test/fixture/gbo/lambda.dag"), - rcf_read(source: gbo_lambda_bad_source, id: ^gbo_lambda_bad_read, unit: ^gbo_lambda_bad_cu, path: "src/v2/test/fixture/gbo/lambda_bad.dag") + rcf_read(source: gbo_lambda_bad_source, id: ^gbo_lambda_bad_read, unit: ^gbo_lambda_bad_cu, path: "src/v2/test/fixture/gbo/lambda_bad.dag"), + rcf_read(source: gbo_integer_stub_source, id: ^gbo_integer_stub_read, unit: ^gbo_integer_stub_cu, path: "src/v2/test/fixture/gbo/integer.dag"), + rcf_read(source: gbo_alias_source, id: ^gbo_alias_read, unit: ^gbo_alias_cu, path: "src/v2/test/fixture/gbo/alias.dag") ] fn gbo_fixture_normalized() -> Outcome> { @@ -73,6 +80,7 @@ fn gbo_resolve_subject(subject: String) -> Outcome { fn gbo_resolved_lambda() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_lambda") } fn gbo_resolved_lambda_bad() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_lambda_bad") } +fn gbo_resolved_alias() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_alias") } fn gbo_atom(id: Symbol) -> Node { node_synthetic(kind: TypeNode { connective: Atom { identity: id } }, children: []) @@ -115,11 +123,21 @@ test fn gbo_a_bool_name_is_not_the_kernel_int_holds() -> Bool { !gbo_is_kernel_int(t: gbo_atom(id: ^Bool)) } -// THE ROUTE: bind_outcome-shaped reconstruct Acc { value: x, n: 0 } at Out. -// Before the join this refused record_field_value_does_not_inhabit at n -// (declared dag_binding_type_int, produced Int). Deleting the join turns this green-to-red. -test fn gbo_the_bind_outcome_reconstruct_does_not_refuse_int_field_inhabitance_holds() -> Bool { - !rcf_refuses_with(resolved: gbo_resolved_lambda(), reason: ^record_field_value_does_not_inhabit) +// THE ROUTE: a generic-variant construct Acc { value: 1, n: 0 } at Out, its Int field judged +// on the real ingest -> resolve -> infer path. ACCEPTED AND DECIDED (rcf_member_accepted_and_decided): +// a resolve refusal, any infer refusal, or an acceptance that left the field undecided all fail it, +// so the claim cannot pass without reaching the join. Deleting the join turns it red +// (declared dag_binding_type_int against the produced corpus Int). +test fn gbo_a_generic_variant_int_field_is_accepted_and_decided_holds() -> Bool { + rcf_member_accepted_and_decided(resolved: gbo_resolved_lambda(), member: ^h) +} + +// AN ALIAS OF THE CORPUS Int IS THAT Int. `type Alias = v2.std.integer.Int` at a declared +// v2.std.integer.Int: kernel recognition re-enters after the alias step, so both sides present the +// kernel atom. Recognizing only at the input would unfold Alias past v2.std.integer.Int into its +// right-hand side and refuse a correct program. +test fn gbo_an_alias_of_the_corpus_int_inhabits_it_holds() -> Bool { + rcf_member_accepted_and_decided(resolved: gbo_resolved_alias(), member: ^same) } // CONTROL: a record field declared Int holding true still refuses. A generic diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 8425d7e234a..a2d6d242d51 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -825,7 +825,8 @@ data floor_single_claim_fill_debt: List = [ SingleClaimFillDebtModule { module: "v2.test.claim.compiler.generic_closure_outcome_construct_probe", claims: [ - SingleClaimFillDebtClaim { claim: "gbo_the_bind_outcome_reconstruct_does_not_refuse_int_field_inhabitance_holds", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "gbo_a_generic_variant_int_field_is_accepted_and_decided_holds", standing: ActiveFillDebt }, + SingleClaimFillDebtClaim { claim: "gbo_an_alias_of_the_corpus_int_inhabits_it_holds", standing: ActiveFillDebt }, SingleClaimFillDebtClaim { claim: "gbo_a_bool_at_the_int_field_still_refuses_holds", standing: ActiveFillDebt } ] }, From d38f0ec20a310801ec96a7aba3c52a00aa32ce3a Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 8 Oct 2026 21:41:35 +0000 Subject: [PATCH 06/12] Scope #13511's route to what the join establishes; drop the unestablished generic-variant claim Measured at 41afbbbb (BuildBuddy 36e48268): the alias claim passes and FAILS with the input-only normalizer, so it is the discriminating real-path claim. A direct generic-variant construct is not accepted-and-decided on this base with or without the join (generic-variant construct typing is #13210's successor's), so it is not claimed; its fixture is removed. Co-Authored-By: Claude Opus 5.5 (1M context) --- ...c_closure_outcome_construct_probe_test.dag | 34 +++++++------------ src/v2/workflow/floor_pure_producer_share.dag | 1 - 2 files changed, 12 insertions(+), 23 deletions(-) diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index 78905d1c076..b1f3a3e86ca 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -35,17 +35,13 @@ import v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_t data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -// SUBJECT: infer_declared_type_obligation's kernel-value join (infer_kernel_value_type_optional). -// A generic-variant construct inside bind_outcome's continuation was refusing -// record_field_value_does_not_inhabit because a field declared Int (kernel atom -// dag_binding_type_int) was judged against a produced Int (the corpus alias -// type Int = GroupCompletion). The join keys the kernel declaration roster (full path) -// and dag_binding_denotation, not a last-segment Int spelling. +// SUBJECT: infer_declared_type_obligation's kernel-value join (infer_kernel_value_type_optional, applied at +// every step of infer_inhabitance_type_normalized). A position declared with the kernel Int (dag_binding_type_int) +// and one declared with the corpus v2.std.integer.Int (type Int = GroupCompletion) are one value type. The +// join keys the kernel declaration roster (full path) and dag_binding_denotation, never a last-segment Int. // -// SUPPLIED claims judge that join at its own interface. ONE claim runs the real -// ingest→resolve→infer route on the bind_outcome-shaped fixture. - -data gbo_lambda_source: String = "module v2.test.gbo_lambda\n\ntype Out = Acc { value: T, n: Int } | Rej { n: Int }\n\nfn bind(o: Out, f: fn(T) -> Out) -> Out {\n match o {\n Rej { n: n } => Rej { n: n }\n Acc { value: v, n: _ } => f(v)\n }\n}\n\nfn g() -> Out {\n bind(o: Acc { value: 1, n: 0 }, f: fn(x) { Acc { value: x, n: 0 } })\n}\n\nfn h() -> Out {\n Acc { value: 1, n: 0 }\n}\n" +// SUPPLIED claims judge the join at its own interface. ONE claim runs the real ingest -> resolve -> infer route +// (the alias claim), and a Bool-in-an-Int-field control still refuses on that route. data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Box {\n n: Int\n m: Int\n}\n\ndata bad: Box = Box { n: true, m: 3 }\n" @@ -54,7 +50,6 @@ data gbo_integer_stub_source: String = "module v2.std.integer\n\ntype Nat = Zero data gbo_alias_source: String = "module v2.test.gbo_alias\n\nimport v2.std.integer { Int }\n\ntype Alias = v2.std.integer.Int\n\nfn same(x: Alias) -> v2.std.integer.Int {\n x\n}\n" data gbo_ingest: SourceRootIngest = [ - rcf_read(source: gbo_lambda_source, id: ^gbo_lambda_read, unit: ^gbo_lambda_cu, path: "src/v2/test/fixture/gbo/lambda.dag"), rcf_read(source: gbo_lambda_bad_source, id: ^gbo_lambda_bad_read, unit: ^gbo_lambda_bad_cu, path: "src/v2/test/fixture/gbo/lambda_bad.dag"), rcf_read(source: gbo_integer_stub_source, id: ^gbo_integer_stub_read, unit: ^gbo_integer_stub_cu, path: "src/v2/test/fixture/gbo/integer.dag"), rcf_read(source: gbo_alias_source, id: ^gbo_alias_read, unit: ^gbo_alias_cu, path: "src/v2/test/fixture/gbo/alias.dag") @@ -78,7 +73,6 @@ fn gbo_resolve_subject(subject: String) -> Outcome { } } -fn gbo_resolved_lambda() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_lambda") } fn gbo_resolved_lambda_bad() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_lambda_bad") } fn gbo_resolved_alias() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_alias") } @@ -123,16 +117,12 @@ test fn gbo_a_bool_name_is_not_the_kernel_int_holds() -> Bool { !gbo_is_kernel_int(t: gbo_atom(id: ^Bool)) } -// THE ROUTE: a generic-variant construct Acc { value: 1, n: 0 } at Out, its Int field judged -// on the real ingest -> resolve -> infer path. ACCEPTED AND DECIDED (rcf_member_accepted_and_decided): -// a resolve refusal, any infer refusal, or an acceptance that left the field undecided all fail it, -// so the claim cannot pass without reaching the join. Deleting the join turns it red -// (declared dag_binding_type_int against the produced corpus Int). -test fn gbo_a_generic_variant_int_field_is_accepted_and_decided_holds() -> Bool { - rcf_member_accepted_and_decided(resolved: gbo_resolved_lambda(), member: ^h) -} - -// AN ALIAS OF THE CORPUS Int IS THAT Int. `type Alias = v2.std.integer.Int` at a declared +// THE ROUTE IS THE ALIAS CLAIM BELOW: it runs ingest -> resolve -> infer and is ACCEPTED AND DECIDED only +// through the join (it fails with the input-only normalizer; BuildBuddy 36e48268). A generic-VARIANT +// construct (Acc { value: 1, n: 0 } at Out) is NOT accepted-and-decided on this base -- measured at +// 41afbbbb -- because generic-variant construct typing is #13210's and its successor's, not this join's; +// it is deliberately not claimed here. +// THE ROUTE, AND AN ALIAS OF THE CORPUS Int IS THAT Int. `type Alias = v2.std.integer.Int` at a declared // v2.std.integer.Int: kernel recognition re-enters after the alias step, so both sides present the // kernel atom. Recognizing only at the input would unfold Alias past v2.std.integer.Int into its // right-hand side and refuse a correct program. diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index a2d6d242d51..005c1c03230 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -825,7 +825,6 @@ data floor_single_claim_fill_debt: List = [ SingleClaimFillDebtModule { module: "v2.test.claim.compiler.generic_closure_outcome_construct_probe", claims: [ - SingleClaimFillDebtClaim { claim: "gbo_a_generic_variant_int_field_is_accepted_and_decided_holds", standing: ActiveFillDebt }, SingleClaimFillDebtClaim { claim: "gbo_an_alias_of_the_corpus_int_inhabits_it_holds", standing: ActiveFillDebt }, SingleClaimFillDebtClaim { claim: "gbo_a_bool_at_the_int_field_still_refuses_holds", standing: ActiveFillDebt } ] From d0aad75e073aa2f0bc7f8ff473232c65ec218f3f Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 8 Oct 2026 21:42:34 +0000 Subject: [PATCH 07/12] #13511: record each fill-debt row's measured figure; declare the generic-variant frontier owned by #13558 Co-Authored-By: Claude Opus 5.5 (1M context) --- .../generic_closure_outcome_construct_probe_test.dag | 5 +++++ src/v2/workflow/floor_pure_producer_share.dag | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index b1f3a3e86ca..29d11c4eaf2 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -42,6 +42,11 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // // SUPPLIED claims judge the join at its own interface. ONE claim runs the real ingest -> resolve -> infer route // (the alias claim), and a Bool-in-an-Int-field control still refuses on that route. +// +// DECLARED FRONTIER, NOT CLAIMED HERE: generic-variant constructs undecided. A direct generic-variant construct +// (Acc { value: 1, n: 0 } at Out) is not accepted-and-decided on this base, with or without the join (measured +// at 41afbbbb, BuildBuddy 36e48268). Owner: gunbc#13558 (payload binders over Outcome via #13210's formal-payload +// obligation), which carries the claim that turns it green. data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Box {\n n: Int\n m: Int\n}\n\ndata bad: Box = Box { n: true, m: 3 }\n" diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 005c1c03230..b66ab24317c 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -821,6 +821,11 @@ fn floor_single_claim_fill_debt_active_claims() -> List { // pipeline's per-claim fixed cost of assembling and inferring a one-module fixture, not the test's own work. // Trigger: assemble plus infer of a one-module fixture runs under the per-claim budget // (gunbc.recurring_failure_mode shared_precondition_re_derived_once_per_claim_frame). +// gunbc#13511 (kernel-value join): two real-path members of v2.test.claim.compiler.generic_closure_outcome_construct_probe, +// sharp-raven-357 approved. gbo_an_alias_of_the_corpus_int_inhabits_it_holds -- the ONE discriminating inhabitance +// (fails with the input-only normalizer) -- measured 1,805,469 own-frame eval steps; the Bool-in-Int control on the +// same route, gbo_a_bool_at_the_int_field_still_refuses_holds, measured 1,790,383 (BuildBuddy 36e48268, pinned +// 41afbbbb). Trigger: shared_precondition_re_derived_once_per_claim_frame, as above. data floor_single_claim_fill_debt: List = [ SingleClaimFillDebtModule { module: "v2.test.claim.compiler.generic_closure_outcome_construct_probe", From ce788a1cad006f7147fa1ee80232433e258ab641 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 8 Oct 2026 21:53:15 +0000 Subject: [PATCH 08/12] #13511: drop the end-to-end Bool-in-Int control; the fill-debt row cites its instrument Review 78145: the control re-ran a refusal that predates the join, paid for by a debt row (DESIGN section 3); the join's negative side is already supplied. The remaining row names the claim_batch entry and receipt that re-derive its cost instead of transcribing figures (DESIGN section 6). Co-Authored-By: Claude Opus 5.5 (1M context) --- ...ric_closure_outcome_construct_probe_test.dag | 17 +++-------------- src/v2/workflow/floor_pure_producer_share.dag | 13 ++++++------- 2 files changed, 9 insertions(+), 21 deletions(-) diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index 29d11c4eaf2..1bd99995a78 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -29,8 +29,7 @@ import v2.std.text { String } import std.algebra { Empty, FreeMonoid } import v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_test { rcf_member_accepted_and_decided, - rcf_read, - rcf_refuses_with + rcf_read } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -41,21 +40,19 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // join keys the kernel declaration roster (full path) and dag_binding_denotation, never a last-segment Int. // // SUPPLIED claims judge the join at its own interface. ONE claim runs the real ingest -> resolve -> infer route -// (the alias claim), and a Bool-in-an-Int-field control still refuses on that route. +// (the alias claim). The negative side of the join is +// supplied (gbo_a_bool_name_is_not_the_kernel_int_holds), not re-run end to end. // // DECLARED FRONTIER, NOT CLAIMED HERE: generic-variant constructs undecided. A direct generic-variant construct // (Acc { value: 1, n: 0 } at Out) is not accepted-and-decided on this base, with or without the join (measured // at 41afbbbb, BuildBuddy 36e48268). Owner: gunbc#13558 (payload binders over Outcome via #13210's formal-payload // obligation), which carries the claim that turns it green. -data gbo_lambda_bad_source: String = "module v2.test.gbo_lambda_bad\n\ntype Box {\n n: Int\n m: Int\n}\n\ndata bad: Box = Box { n: true, m: 3 }\n" - data gbo_integer_stub_source: String = "module v2.std.integer\n\ntype Nat = Zero | One\n\ntype Int = Nat\n" data gbo_alias_source: String = "module v2.test.gbo_alias\n\nimport v2.std.integer { Int }\n\ntype Alias = v2.std.integer.Int\n\nfn same(x: Alias) -> v2.std.integer.Int {\n x\n}\n" data gbo_ingest: SourceRootIngest = [ - rcf_read(source: gbo_lambda_bad_source, id: ^gbo_lambda_bad_read, unit: ^gbo_lambda_bad_cu, path: "src/v2/test/fixture/gbo/lambda_bad.dag"), rcf_read(source: gbo_integer_stub_source, id: ^gbo_integer_stub_read, unit: ^gbo_integer_stub_cu, path: "src/v2/test/fixture/gbo/integer.dag"), rcf_read(source: gbo_alias_source, id: ^gbo_alias_read, unit: ^gbo_alias_cu, path: "src/v2/test/fixture/gbo/alias.dag") ] @@ -78,7 +75,6 @@ fn gbo_resolve_subject(subject: String) -> Outcome { } } -fn gbo_resolved_lambda_bad() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_lambda_bad") } fn gbo_resolved_alias() -> Outcome { gbo_resolve_subject(subject: "v2.test.gbo_alias") } fn gbo_atom(id: Symbol) -> Node { @@ -134,10 +130,3 @@ test fn gbo_a_bool_name_is_not_the_kernel_int_holds() -> Bool { test fn gbo_an_alias_of_the_corpus_int_inhabits_it_holds() -> Bool { rcf_member_accepted_and_decided(resolved: gbo_resolved_alias(), member: ^same) } - -// CONTROL: a record field declared Int holding true still refuses. A generic -// *variant* Acc { n: true } does not surface record_field_value_does_not_inhabit -// on this path (floor 37547532785 / 37534388259 returned Bool(false)). -test fn gbo_a_bool_at_the_int_field_still_refuses_holds() -> Bool { - rcf_refuses_with(resolved: gbo_resolved_lambda_bad(), reason: ^record_field_value_does_not_inhabit) -} diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index b66ab24317c..a37f63ec81a 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -821,17 +821,16 @@ fn floor_single_claim_fill_debt_active_claims() -> List { // pipeline's per-claim fixed cost of assembling and inferring a one-module fixture, not the test's own work. // Trigger: assemble plus infer of a one-module fixture runs under the per-claim budget // (gunbc.recurring_failure_mode shared_precondition_re_derived_once_per_claim_frame). -// gunbc#13511 (kernel-value join): two real-path members of v2.test.claim.compiler.generic_closure_outcome_construct_probe, -// sharp-raven-357 approved. gbo_an_alias_of_the_corpus_int_inhabits_it_holds -- the ONE discriminating inhabitance -// (fails with the input-only normalizer) -- measured 1,805,469 own-frame eval steps; the Bool-in-Int control on the -// same route, gbo_a_bool_at_the_int_field_still_refuses_holds, measured 1,790,383 (BuildBuddy 36e48268, pinned -// 41afbbbb). Trigger: shared_precondition_re_derived_once_per_claim_frame, as above. +// gunbc#13511 (kernel-value join): the ONE real-path inhabitance of v2.test.claim.compiler.generic_closure_outcome_construct_probe, +// gbo_an_alias_of_the_corpus_int_inhabits_it_holds (fails with the input-only normalizer). Its own-frame eval steps are +// re-derived by claim_batch --hermetic --entry src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +// --functions gbo_an_alias_of_the_corpus_int_inhabits_it_holds (receipt: BuildBuddy 36e48268, pinned 41afbbbb). +// Trigger: shared_precondition_re_derived_once_per_claim_frame, as above. data floor_single_claim_fill_debt: List = [ SingleClaimFillDebtModule { module: "v2.test.claim.compiler.generic_closure_outcome_construct_probe", claims: [ - SingleClaimFillDebtClaim { claim: "gbo_an_alias_of_the_corpus_int_inhabits_it_holds", standing: ActiveFillDebt }, - SingleClaimFillDebtClaim { claim: "gbo_a_bool_at_the_int_field_still_refuses_holds", standing: ActiveFillDebt } + SingleClaimFillDebtClaim { claim: "gbo_an_alias_of_the_corpus_int_inhabits_it_holds", standing: ActiveFillDebt } ] }, SingleClaimFillDebtModule { From f6ad784970bc5d912d92ccb80c9ba57224800d47 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 8 Oct 2026 22:03:28 +0000 Subject: [PATCH 09/12] #13511: reattach infer_declared_type_obligation's annotation to its declaration (review 78151) Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/04_infer.dag | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index 68eadd26386..fe557ba6041 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -3565,11 +3565,6 @@ fn infer_match_generic_formal_or_carrier(formal: Node, produced: Node, type_para } } -// THE ONE PRODUCER OF A DeclaredTypeObligation in infer: every obligation -- a call argument, a declared return, a -// fold member or carrier, a generic formal -- is built here, so the ONE alias rule (infer_type_alias_normalized) -// reaches every judgment: the declared type, the produced type and the produced type's refinement carrier are -// all presented with transparent aliases unfolded. The carrier is READ from the produced type as written (a -// refinement is never unfolded, so its declaration is still the one found), then normalized like the rest. // THE KERNEL VALUE TYPE AND THE CORPUS DECLARATION ARE ONE TYPE. `v2.std.integer.Int` // (`type Int = GroupCompletion`) and the kernel atom `dag_binding_type_int` // (integer_int_type_node) answer the same value-type question. Alias-normalizing first unfolds @@ -3628,6 +3623,11 @@ fn infer_inhabitance_type_normalized(t: Node, declarations: SymbolIndex) -> Node } } +// THE ONE PRODUCER OF A DeclaredTypeObligation in infer: every obligation -- a call argument, a declared return, a +// fold member or carrier, a generic formal -- is built here, so the ONE alias rule (infer_type_alias_normalized) +// reaches every judgment: the declared type, the produced type and the produced type's refinement carrier are +// all presented with transparent aliases unfolded. The carrier is READ from the produced type as written (a +// refinement is never unfolded, so its declaration is still the one found), then normalized like the rest. fn infer_declared_type_obligation( position: DeclaredTypePosition, parameter_identity: Symbol, From 46da0c8fa0e893b8b99429ef1de1a3cebc0f1726 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 8 Oct 2026 22:18:48 +0000 Subject: [PATCH 10/12] #13511: one kernel-aware normalizer; the route claim discriminates deleting the join Review 78152: (1) the alias-vs-corpus-Int claim stayed green with the join deleted (both sides unfold to the same right-hand side). The route claim is now a kernel Int literal returned at a declared Alias of the corpus Int: red with the join deleted and with input-only recognition. (2) Generic formal matching read the alias-only normalizer while obligations read the joined one -- two normalizers for one question (DESIGN section 3). Kernel recognition now lives inside infer_type_alias_normalized and infer_inhabitance_type_normalized is deleted. Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/compiler/04_infer.dag | 67 +++++++------------ ...c_closure_outcome_construct_probe_test.dag | 22 +++--- src/v2/workflow/floor_pure_producer_share.dag | 6 +- 3 files changed, 35 insertions(+), 60 deletions(-) diff --git a/src/v2/compiler/04_infer.dag b/src/v2/compiler/04_infer.dag index fe557ba6041..493bf2f6bf1 100644 --- a/src/v2/compiler/04_infer.dag +++ b/src/v2/compiler/04_infer.dag @@ -3527,22 +3527,29 @@ fn infer_type_alias_unfolded(t: Node, declarations: SymbolIndex) -> Optional Node { - match infer_type_alias_unfolded(t: t, declarations: declarations) { - Present { value: unfolded } => infer_type_alias_normalized(t: unfolded, declarations: declarations) + match infer_kernel_value_type_optional(t: t) { + Present { value: k } => k Absent => - match t.kind { - TypeNode { connective: Instantiation } => - Node { - kind: t.kind, - children: fold(t.children, init: Empty, f: fn(acc, e) { - list_snoc_item(xs: acc, item: Edge { label: e.label, target: infer_type_alias_normalized(t: e.target, declarations: declarations) }) - }), - occurrence_id: t.occurrence_id + match infer_type_alias_unfolded(t: t, declarations: declarations) { + Present { value: unfolded } => infer_type_alias_normalized(t: unfolded, declarations: declarations) + Absent => + match t.kind { + TypeNode { connective: Instantiation } => + Node { + kind: t.kind, + children: fold(t.children, init: Empty, f: fn(acc, e) { + list_snoc_item(xs: acc, item: Edge { label: e.label, target: infer_type_alias_normalized(t: e.target, declarations: declarations) }) + }), + occurrence_id: t.occurrence_id + } + TypeNode { connective: _ } => t + ComputationNode { behavior: _ } => t } - TypeNode { connective: _ } => t - ComputationNode { behavior: _ } => t } } } @@ -3595,34 +3602,6 @@ fn infer_kernel_value_type_optional(t: Node) -> Optional { } } -// KERNEL RECOGNITION IS PART OF EVERY NORMALIZATION STEP, not only the first. Recognizing the kernel -// type at the input and then delegating to infer_type_alias_normalized would unfold -// `type Alias = v2.std.integer.Int` straight past the corpus Int into GroupCompletion, while a -// direct v2.std.integer.Int becomes the kernel atom -- one type presented two ways, a false refusal. -// So each alias step re-enters this function, and so does every Instantiation argument. -fn infer_inhabitance_type_normalized(t: Node, declarations: SymbolIndex) -> Node { - match infer_kernel_value_type_optional(t: t) { - Present { value: k } => k - Absent => - match infer_type_alias_unfolded(t: t, declarations: declarations) { - Present { value: unfolded } => infer_inhabitance_type_normalized(t: unfolded, declarations: declarations) - Absent => - match t.kind { - TypeNode { connective: Instantiation } => - Node { - kind: t.kind, - children: fold(t.children, init: Empty, f: fn(acc, e) { - list_snoc_item(xs: acc, item: Edge { label: e.label, target: infer_inhabitance_type_normalized(t: e.target, declarations: declarations) }) - }), - occurrence_id: t.occurrence_id - } - TypeNode { connective: _ } => t - ComputationNode { behavior: _ } => t - } - } - } -} - // THE ONE PRODUCER OF A DeclaredTypeObligation in infer: every obligation -- a call argument, a declared return, a // fold member or carrier, a generic formal -- is built here, so the ONE alias rule (infer_type_alias_normalized) // reaches every judgment: the declared type, the produced type and the produced type's refinement carrier are @@ -3640,10 +3619,10 @@ fn infer_declared_type_obligation( DeclaredTypeObligation { position: position, parameter_identity: parameter_identity, - declared: infer_inhabitance_type_normalized(t: declared, declarations: declarations), - produced: infer_inhabitance_type_normalized(t: produced, declarations: declarations), + declared: infer_type_alias_normalized(t: declared, declarations: declarations), + produced: infer_type_alias_normalized(t: produced, declarations: declarations), produced_declared_carrier: match refinement_declared_carrier(index: declarations, source_type: produced) { - Present { value: c } => Present { value: infer_inhabitance_type_normalized(t: c, declarations: declarations) } + Present { value: c } => Present { value: infer_type_alias_normalized(t: c, declarations: declarations) } Absent => Absent }, application: application, diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index 1bd99995a78..b5466aaaff5 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -35,7 +35,7 @@ import v2.test.claim.compiler.infer_record_construct_field_inhabitance_witness_t data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // SUBJECT: infer_declared_type_obligation's kernel-value join (infer_kernel_value_type_optional, applied at -// every step of infer_inhabitance_type_normalized). A position declared with the kernel Int (dag_binding_type_int) +// every step of infer_type_alias_normalized). A position declared with the kernel Int (dag_binding_type_int) // and one declared with the corpus v2.std.integer.Int (type Int = GroupCompletion) are one value type. The // join keys the kernel declaration roster (full path) and dag_binding_denotation, never a last-segment Int. // @@ -50,7 +50,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data gbo_integer_stub_source: String = "module v2.std.integer\n\ntype Nat = Zero | One\n\ntype Int = Nat\n" -data gbo_alias_source: String = "module v2.test.gbo_alias\n\nimport v2.std.integer { Int }\n\ntype Alias = v2.std.integer.Int\n\nfn same(x: Alias) -> v2.std.integer.Int {\n x\n}\n" +data gbo_alias_source: String = "module v2.test.gbo_alias\n\nimport v2.std.integer { Int }\n\ntype Alias = v2.std.integer.Int\n\nfn one() -> Alias {\n 1\n}\n" data gbo_ingest: SourceRootIngest = [ rcf_read(source: gbo_integer_stub_source, id: ^gbo_integer_stub_read, unit: ^gbo_integer_stub_cu, path: "src/v2/test/fixture/gbo/integer.dag"), @@ -118,15 +118,11 @@ test fn gbo_a_bool_name_is_not_the_kernel_int_holds() -> Bool { !gbo_is_kernel_int(t: gbo_atom(id: ^Bool)) } -// THE ROUTE IS THE ALIAS CLAIM BELOW: it runs ingest -> resolve -> infer and is ACCEPTED AND DECIDED only -// through the join (it fails with the input-only normalizer; BuildBuddy 36e48268). A generic-VARIANT -// construct (Acc { value: 1, n: 0 } at Out) is NOT accepted-and-decided on this base -- measured at -// 41afbbbb -- because generic-variant construct typing is #13210's and its successor's, not this join's; -// it is deliberately not claimed here. -// THE ROUTE, AND AN ALIAS OF THE CORPUS Int IS THAT Int. `type Alias = v2.std.integer.Int` at a declared -// v2.std.integer.Int: kernel recognition re-enters after the alias step, so both sides present the -// kernel atom. Recognizing only at the input would unfold Alias past v2.std.integer.Int into its -// right-hand side and refuse a correct program. -test fn gbo_an_alias_of_the_corpus_int_inhabits_it_holds() -> Bool { - rcf_member_accepted_and_decided(resolved: gbo_resolved_alias(), member: ^same) +// THE ROUTE: a kernel Int literal returned at a declared `Alias` of the corpus Int (`fn one() -> Alias { 1 }`), +// on the real ingest -> resolve -> infer path, ACCEPTED AND DECIDED. The literal is the kernel atom; the declared +// side reaches the kernel atom only through the join, and only if recognition re-enters after the alias step. So it +// goes red both when the join is deleted (Alias unfolds to its right-hand side) and when recognition happens only at +// the input -- the integration and the regression in one claim. +test fn gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds() -> Bool { + rcf_member_accepted_and_decided(resolved: gbo_resolved_alias(), member: ^one) } diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index a37f63ec81a..80d92ff8277 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -822,15 +822,15 @@ fn floor_single_claim_fill_debt_active_claims() -> List { // Trigger: assemble plus infer of a one-module fixture runs under the per-claim budget // (gunbc.recurring_failure_mode shared_precondition_re_derived_once_per_claim_frame). // gunbc#13511 (kernel-value join): the ONE real-path inhabitance of v2.test.claim.compiler.generic_closure_outcome_construct_probe, -// gbo_an_alias_of_the_corpus_int_inhabits_it_holds (fails with the input-only normalizer). Its own-frame eval steps are +// gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds (red with the join deleted and with input-only recognition). Its own-frame eval steps are // re-derived by claim_batch --hermetic --entry src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag -// --functions gbo_an_alias_of_the_corpus_int_inhabits_it_holds (receipt: BuildBuddy 36e48268, pinned 41afbbbb). +// --functions gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds (receipt: BuildBuddy 36e48268, pinned 41afbbbb). // Trigger: shared_precondition_re_derived_once_per_claim_frame, as above. data floor_single_claim_fill_debt: List = [ SingleClaimFillDebtModule { module: "v2.test.claim.compiler.generic_closure_outcome_construct_probe", claims: [ - SingleClaimFillDebtClaim { claim: "gbo_an_alias_of_the_corpus_int_inhabits_it_holds", standing: ActiveFillDebt } + SingleClaimFillDebtClaim { claim: "gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds", standing: ActiveFillDebt } ] }, SingleClaimFillDebtModule { From d4aaeb914052babbadb022ea3f9cecd6628557f7 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 8 Oct 2026 23:10:11 +0000 Subject: [PATCH 11/12] #13511: cite the receipts for the discriminating route claim (head plus both mutants) Co-Authored-By: Claude Opus 5.5 (1M context) --- .../compiler/generic_closure_outcome_construct_probe_test.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag index b5466aaaff5..a87b764c309 100644 --- a/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag +++ b/src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag @@ -122,7 +122,7 @@ test fn gbo_a_bool_name_is_not_the_kernel_int_holds() -> Bool { // on the real ingest -> resolve -> infer path, ACCEPTED AND DECIDED. The literal is the kernel atom; the declared // side reaches the kernel atom only through the join, and only if recognition re-enters after the alias step. So it // goes red both when the join is deleted (Alias unfolds to its right-hand side) and when recognition happens only at -// the input -- the integration and the regression in one claim. +// the input -- the integration and the regression in one claim (BuildBuddy 50c58a76 and 2002ea86). test fn gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds() -> Bool { rcf_member_accepted_and_decided(resolved: gbo_resolved_alias(), member: ^one) } From 9bb2bdf39d0d4c85403bc012dc16b1bad99a6313 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 8 Oct 2026 23:10:30 +0000 Subject: [PATCH 12/12] #13511: fill-debt receipt names the measuring run for the current route claim Co-Authored-By: Claude Opus 5.5 (1M context) --- src/v2/workflow/floor_pure_producer_share.dag | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/v2/workflow/floor_pure_producer_share.dag b/src/v2/workflow/floor_pure_producer_share.dag index 80d92ff8277..d3833dade50 100644 --- a/src/v2/workflow/floor_pure_producer_share.dag +++ b/src/v2/workflow/floor_pure_producer_share.dag @@ -824,7 +824,8 @@ fn floor_single_claim_fill_debt_active_claims() -> List { // gunbc#13511 (kernel-value join): the ONE real-path inhabitance of v2.test.claim.compiler.generic_closure_outcome_construct_probe, // gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds (red with the join deleted and with input-only recognition). Its own-frame eval steps are // re-derived by claim_batch --hermetic --entry src/v2/test/claim/compiler/generic_closure_outcome_construct_probe_test.dag -// --functions gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds (receipt: BuildBuddy 36e48268, pinned 41afbbbb). +// --functions gbo_a_kernel_literal_inhabits_an_alias_of_the_corpus_int_holds (receipt: BuildBuddy a63835e8, pinned +// 46da0c8fa0; red with the join deleted, BuildBuddy 50c58a76, and with input-only recognition, BuildBuddy 2002ea86). // Trigger: shared_precondition_re_derived_once_per_claim_frame, as above. data floor_single_claim_fill_debt: List = [ SingleClaimFillDebtModule {