Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
32 commits
Select commit Hold shift + click to select a range
1c21c60
A coproduct payload can inhabit its parent coproduct field, and nothi…
Aug 22, 2026
0443eab
Merge remote-tracking branch 'origin/main' into session/coproduct-pay…
Aug 22, 2026
fab60fd
Enrol the probe in the roster that actually gates the floor
Aug 22, 2026
719f04a
Transparent-alias identity as a precomputed census relation, and the …
Aug 22, 2026
407a15f
wip: declared-field inhabitance wall in 04_infer.dag
Aug 22, 2026
aa3e652
wip: parse fixes
Aug 22, 2026
58b1ab8
wip: annotations at module-item grain
Aug 22, 2026
846553e
Merge #8865 (the class's executing evidence) into the wall that close…
Aug 22, 2026
e78c61c
Require an alias edge to license identity agreement, not a shared las…
Aug 22, 2026
3a681db
Regenerate the stage0 mirror for the inhabitance wall
Aug 22, 2026
90d001a
Scope the diagnostic control honestly: it is closure-scoped, not corp…
Aug 22, 2026
9bfd538
Two corpus-derived arms: an empty-record base and a variant-projectio…
Aug 22, 2026
409944b
Retire the expecting-red rows: the wall lands in this change
Aug 22, 2026
fab1745
Merge #8873 (transparent alias identity on SymbolIndex) — the identit…
Aug 22, 2026
87e6404
Consume the transparent-alias identity relation: the wall must reach …
Aug 22, 2026
2a4a12b
Corpus census repairs: six sites the wall refuses, plus the materiali…
Aug 22, 2026
a620748
Regenerate the mirror for the alias-aware wall
Aug 22, 2026
bc409b6
Enrol the alias-mediated arm as its own witness: deleting the relatio…
Aug 22, 2026
3937789
Two more sites of the same class the wall surfaced, plus the comparan…
Aug 22, 2026
8a894ea
The list-element seam: locality_affinity built consumer identities fr…
Aug 22, 2026
40b0d7c
Declare the two seams closing seam (2) enumerated: the class is one q…
Aug 22, 2026
05987d7
Owner per seam, and fix the ranking to the silent-wrongness rule rath…
Aug 22, 2026
c409532
Merge remote-tracking branch 'origin/main' into session/snappy-tern-856
Aug 22, 2026
69f62c8
A fifth seam, found by a mis-written probe: the declared return type …
Aug 22, 2026
aa34761
Record the copied-versus-emitted trap in the regen receipt, beside th…
Aug 22, 2026
c6757e8
Merge remote-tracking branch 'origin/main' into session/snappy-tern-856
Aug 22, 2026
89eabf1
Regenerate the mirror onto #8873's landed relation
Aug 22, 2026
af8ea93
Merge remote-tracking branch 'origin/main' into session/snappy-tern-856
Aug 22, 2026
30bb8d1
The merge resurrected the expecting-red rows the wall retires: delete…
Aug 22, 2026
a4a6fa9
Merge main into the wall branch: 87 files landed since the last green…
Aug 22, 2026
dd293b3
Merge main into the wall branch: five PRs landed in a two-minute burs…
Aug 22, 2026
f21d4ff
Restore the sentence break the three-way join moved: the period belon…
Aug 22, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 0 additions & 8 deletions dag/gunbc/explicit_witness_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -158,14 +158,6 @@ data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
reason: "NO LONGER THE CLOSING VALIDATION FOR roadmap node v1-test-migration as of 2026-08-11 (gunbc#8146, review 51212) — that node rebound to test_migration_debt_test.dag retained_rust_kernel_wall_holds_against_live_tree when the authority inverted from classifying departures to declaring residents, and gunbc.roadmap_authority is the single authority for that binding. RETAINED as an expecting-red probe only: it still measures a real derived quantity and greening it would still be progress. It was: the discriminating closing validation for roadmap node v1-test-migration, RED BY DESIGN while any independently discovered legacy #[test] function has no typed behavior disposition. Unlike the diff-scoped deletion guard it cannot pass on zero progress; stale, duplicate, unresolved and unclassified identities all refuse.",
dissolution: unbound_dissolution(description: "the derived unclassified legacy-behavior set reaches zero with every disposition admitted — this row deletes in the completing change, promoting the unchanged acceptance witness to ordinary DiscoverySelection as the permanent migration regression wall")
),
known_red_probe(
entry: "dag/test/claim/coproduct_payload_soundness_witness_test.dag",
f: "cpp_payload_where_coproduct_required_must_refuse",
kind: CorpusWitnessKind,
budget: FastLaneEvalBudget,
reason: "A COPRODUCT PAYLOAD CAN INHABIT ITS PARENT COPRODUCT FIELD AND NOTHING REFUSES IT -- the general form of the defect #8853 repaired at one site. There, a std.occurrence_identity.OccurrenceId (the payload carried inside MintedOccurrence) was declared as a parameter and assigned into Node.occurrence_id, whose type is the NodeOccurrenceId coproduct; nothing refused it, and the consequence surfaced one pipeline stage away as `non-exhaustive pattern match on: OccurrenceId` in sixteen floor claims. MEASURED GENERALLY, minimal pair, no Node and no compiler internals: CppHolder { subject: cpp_inner() } is ACCEPTED BY TYPING and dies at runtime with PatternMatchFailure, while the correct spelling CppHolder { subject: CppWrapped { inner: cpp_inner() } } compiles and executes -- so the mechanism is neither Node-specific nor occurrence-specific. This is BELOW FLOOR, not a rung: DESIGN section 4b places `values inhabit declared types` in the ordinary compiler floor, and a floor failure is a below-baseline safety regression rather than a class sitting at mitigatable. Red BY DESIGN and not relaxable: the only edit that may green it is making the ill-typed construction refuse. Its positive control (cpp_payload_inside_its_own_arm_still_compiles) is enrolled as an ordinary green claim so the red measures the distinction rather than a blanket refusal. Owner: the compiler type-soundness lane. THIS ROW DOCUMENTS THE RED AND ITS DISSOLUTION; the required floor is gated by the identity's row in v2.workflow.floor_expected_red, per the ruling at floor_expected_red_chunk_13. Both rows delete together when the wall lands.",
dissolution: unbound_dissolution(description: "the construction refuses with a located, blocking type diagnostic -- this row deletes in the change that lands the wall, promoting the witness to ordinary DiscoverySelection as the permanent regression control DESIGN section 4b(4) requires stay enrolled")
),
known_red_probe(
entry: "dag/test/claim/observation_raw_print_retirement_acceptance_test.dag",
f: "observation_emit_frontier_is_zero",
Expand Down
59 changes: 54 additions & 5 deletions dag/test/claim/coproduct_payload_soundness_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,27 @@ module test.claim.coproduct_payload_soundness_witness_test
//
// WHAT IS ASSERTED. compile_dag_rust_emit_check must REFUSE the fixture below: placing a variant's
// payload where the variant's own type is declared must be a located, blocking type diagnostic, not
// a program that compiles and dies at its first match. The witness returns false today, which is why
// it is enrolled as an expecting-red identity rather than asserted green here.
// a program that compiles and dies at its first match.
//
// THE WALL LANDED AND THIS PAIR IS NOW GREEN BY EXECUTION, measured on the remote runner against the
// same two fixtures, one commit apart, with nothing else changed:
//
// BEFORE negative -> `compiled: 9 files emitted, 0 diagnostics` (the hole)
// AFTER negative -> `type mismatch: expected 'Coproduct(CppOuter)', got 'Product(CppInner)'`
// `v2 self-compile produced 1 hard diagnostic(s)`
// BEFORE and AFTER, positive control -> `0 diagnostics`
//
// The refusing authority is `v1.compiler.infer` `coproduct_payload_where_parent_required`, consulted
// at the record-literal field seam. Both this file's expecting-red rows -- the
// gunbc.explicit_witness_admission admission and the v2.workflow.floor_expected_red roster entry --
// deleted in that same change, and this witness stays enrolled as the permanent regression control
// DESIGN section 4b(4) requires: deleting the evidence on the climb would recreate
// specification-without-execution one rung up.
//
// WHAT THIS PAIR DOES NOT MEASURE, stated rather than implied covered. The wall closes the
// record-literal field seam and only it: a `let` binding, a method argument, and the direct-call
// argument seam are judged by other authorities and are not exercised here. Per gunbc#8868 the seam
// enumeration for this class is unfinished, so this is one seam closed, not the class closed.
//
// ENROLLED IN TWO PLACES, AND THEY ARE NOT THE SAME FACT -- I got this wrong on the first attempt
// and the floor caught it. `v2.workflow.floor_expected_red` is what GATES the required floor: an
Expand All @@ -63,9 +82,9 @@ fn cpp_soundness_positive_fixture_source() -> String {
"module cpp.control\n\nimport std.types { Int }\n\ntype CppInner { value: Int }\n\ntype CppOuter\n = CppWrapped { inner: CppInner }\n\ntype CppHolder {\n subject: CppOuter\n}\n\nfn cpp_inner() -> CppInner {\n CppInner { value: 7 }\n}\n\nfn cpp_wrapped_holder() -> CppHolder {\n CppHolder { subject: CppWrapped { inner: cpp_inner() } }\n}\n"
}

// THE DISCRIMINATING RED. `CppInner` is the payload inside `CppWrapped`, not a member of `CppOuter`,
// so this assignment must refuse at typing. It does not: the program compiles and the failure is
// deferred to whatever later match reads the field.
// THE DISCRIMINATING RED, now the regression control. `CppInner` is the payload inside `CppWrapped`,
// not a member of `CppOuter`, so this assignment must refuse at typing. Before the wall it did not:
// the program compiled and the failure was deferred to whatever later match read the field.
test fn cpp_payload_where_coproduct_required_must_refuse() -> Bool {
!compile_dag_rust_emit_check(
cpp_soundness_negative_fixture_source(),
Expand All @@ -85,3 +104,33 @@ test fn cpp_payload_inside_its_own_arm_still_compiles() -> Bool {
[]
)
}

fn cpp_alias_mediated_negative_fixture_source() -> String {
"module cpp.alias\n\nimport std.types { Int }\n\ntype CppInner { value: Int }\n\ntype CppInnerAlias = CppInner\n\ntype CppOuter\n = CppWrapped(CppInner)\n\ntype CppHolder {\n subject: CppOuter\n}\n\nfn cpp_inner_via_alias() -> CppInnerAlias {\n CppInner { value: 7 }\n}\n\nfn cpp_alias_payload_where_coproduct_required() -> CppHolder {\n CppHolder { subject: cpp_inner_via_alias() }\n}\n"
}

// THE ALIAS-MEDIATED RED, and it is not a restatement of the one above -- it is the arm that made the
// difference between a wall that refuses a demonstration and a wall that reaches production.
//
// A first measured version of this wall refused the direct spelling and stayed SILENT on the live
// specimen it was built against: `v2.std.materialize` storing `content_hash(n)` into a field declared
// `ContentHash`. `content_hash` returns `v2.std.node` `Hash`, a TRANSPARENT ALIAS of the payload type
// `Fnv1a64Structural`, and that fact does not survive `resolve_item_types` -- so the seam could not
// recover it by peeling and the refusal never fired. This fixture is that shape reduced to nothing but
// the mechanism: the producer's declared return type is an alias of the payload rather than the payload
// itself, and the variant carries its payload positionally rather than as a named field, so neither the
// name nor the arm shape is doing the work.
//
// Measured on the pre-relation binary this fixture COMPILED (`0 diagnostics`); with
// `transparent_alias_identity_agrees` consulted it refuses
// (`expected 'Coproduct(COuter)', got 'Primitive(CAlias)'` on the equivalent probe). Deleting the
// alias arm from the wall leaves both witnesses above green and only this one red, which is exactly why
// it is enrolled separately.
test fn cpp_alias_mediated_payload_must_also_refuse() -> Bool {
!compile_dag_rust_emit_check(
cpp_alias_mediated_negative_fixture_source(),
"src/cpp_alias.rs",
[],
[]
)
}
6 changes: 3 additions & 3 deletions dag/test/claim/heal_revalidation_witness_test.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module test.claim.heal_revalidation_witness

import std.content_hash { Fnv1a64Structural, content_hash_atom }
import std.content_hash { ContentHash, Fnv1a64, content_hash_atom }
import std.types { CommitSha }
import extdeps.github.checks { Success }
import gunbc.merge_admission {
Expand All @@ -26,8 +26,8 @@ import gunbc.heal_revalidation {
data prior_head: CommitSha = "1111111111111111111111111111111111111111"
data healed_head: CommitSha = "2222222222222222222222222222222222222222"
data other_head: CommitSha = "3333333333333333333333333333333333333333"
data required_roster: Fnv1a64Structural = content_hash_atom(value: "heal-roster")
data required_gate: Fnv1a64Structural = content_hash_atom(value: "heal-gate")
data required_roster: ContentHash = Fnv1a64(content_hash_atom(value: "heal-roster"))
data required_gate: ContentHash = Fnv1a64(content_hash_atom(value: "heal-gate"))

fn produced() -> HealOutcome {
HealProduced {
Expand Down
3 changes: 2 additions & 1 deletion dag/test/claim/materialization_provider_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module test.claim.materialization_provider_witness
import std.types { Bool, Int, List, String }
import std.content_hash {
ContentHash,
Fnv1a64,
content_hash_atom,
as_content_hash_cryptographic,
sha256_hex_digest,
Expand Down Expand Up @@ -240,7 +241,7 @@ test fn red_wrong_content_refuses_never_hits() -> Bool {
req: witness_closure_request(),
probe: ProbeFound {
artifact: witness_complete_closure_artifact(),
observed_digest: content_hash_atom(value: "closure-payload-corrupt")
observed_digest: Fnv1a64(content_hash_atom(value: "closure-payload-corrupt"))
}
)
lookup_is_refused_wrong_content(l: poisoned) && (lookup_is_hit(l: poisoned) == false)
Expand Down
2 changes: 1 addition & 1 deletion docs/plans/compiler-guarantee-recovery-gap-analysis.md

Large diffs are not rendered by default.

145 changes: 145 additions & 0 deletions src/v1/04_infer.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1985,6 +1985,142 @@ fn type_name_transparently_aliases_to(
}
}

// THE DECLARED-FIELD INHABITANCE WALL (DESIGN 4b floor: "values inhabit declared types").
//
// The state this refuses: a record-literal field declared as a COPRODUCT is initialised with a
// value whose type is one of that coproduct's own VARIANT PAYLOAD types. The payload is not a
// member of the parent, so the assignment is unsound -- but until this wall the seam judged only
// kernel scalars (kernel_value_declared_type_mismatch bails unless the ACTUAL is a kernel type)
// and record literals (structured_application_site_type_mismatch bails unless the actual EXPR is
// an ExprRecordLit). An actual that is a CALL -- the overwhelmingly common spelling -- was judged
// by nothing, so the program compiled and died at the first total match over the field.
//
// The receipt is #8865's minimal pair, and the class is not synthetic: it is the mechanism that
// permitted the 2026-08-22 outage. v2.extdeps.languages.dag built `Node { occurrence_id: <raw
// OccurrenceId> }` where the field is declared `NodeOccurrenceId` and `OccurrenceId` is the
// payload of its `MintedOccurrence` arm; the value entered the bad state at that record literal,
// stayed latent two months, and surfaced 2,000 lines and one pipeline stage away as
// `non-exhaustive pattern match on: OccurrenceId { value: 79 }` in sixteen floor claims.
//
// THE SCOPE IS THE RECORD-LITERAL FIELD SEAM, AND ONLY IT. This wall does not judge `let`
// bindings, method arguments, or the direct-call argument seam (whose TYPE judgment is separately
// switched off for `v2.*` by module_skips_direct_call_arg_check). Per gunbc#8868, the seam
// enumeration for this class is UNFINISHED -- assume a further seam until someone enumerates
// them -- so this closes one seam and says so rather than closing the class.
//
// WHY THE PREDICATE IS KEYED ON PAYLOAD MEMBERSHIP RATHER THAN ON MISMATCH IN GENERAL. Once the
// two names are established incompatible and the formal is a non-generic coproduct, ANY actual is
// arguably wrong; refusing all of them would make this a general field-type wall, whose
// false-positive classes are exactly the four representation gaps the conformance wall measured
// (brand aliases, optionality's two forms, anonymous literals, expansion depth). Requiring the
// actual to be a DECLARED PAYLOAD TYPE OF ONE OF THE FORMAL'S OWN VARIANTS positively identifies
// the confusion instead of inferring it from an absence, so a refusal here always names a
// spelling the author can point at: the wrapping arm is in the same declaration.
//
// NAME IDENTITY IS BORROWED, NOT REBUILT. A first measured version of this wall refused the direct
// shape (`CppHolder { subject: cpp_inner() }`) and stayed SILENT on the production specimen this
// lane was given as its acceptance target -- `v2.std.materialize` storing `content_hash(n)` into a
// field declared `ContentHash` -- and the isolating pair says why: an otherwise identical fixture
// whose producer returns a TRANSPARENT ALIAS of the payload type was not refused, while the same
// fixture returning the payload type outright was. `content_hash` returns `v2.std.node` `Hash`,
// which is exactly such an alias of `Fnv1a64Structural`. The fact needed -- what a declaration
// aliases -- does not survive `resolve_item_types`, so no amount of peeling at this seam can
// recover it, which is gunbc#8873's finding and the reason its relation is computed ONCE during
// census construction. This wall therefore consumes `transparent_alias_identity_agrees` over the
// `SymbolIndex` the judgment already carries rather than minting a second identity relation, per
// the coordination ruling recorded on that lane.
//
// COST. Every guard ahead of the declaration walk is a string compare or a cardinality read, and
// the walk itself is bounded by the formal declaration's own variant/field count -- never by the
// corpus. Nothing is re-derived from normalized structure: the judgment reads the same resolved
// formal node the seam already holds, and the alias relation is a map lookup on a census built once.
fn coproduct_variant_payload_admits_type_name(
decl: Node,
actual_name: String,
type_env: TypeEnv,
module_name: String,
source_indices: Map<String, NewlineIndex>
) -> Bool {
decl.children |> any(variant =>
variant.children |> any(payload =>
let payload_type = match payload.inferred {
Present { value: Resolved { node: rt } } => rt
_ => field_node_type_expr(n: payload)
}
let payload_name = authored_name_at(source_indices: source_indices, node: payload_type)
let names_agree = application_type_names_compatible(
formal_name: payload_name,
lit_name: actual_name,
type_env: type_env,
module_name: module_name,
source_indices: source_indices) || transparent_alias_identity_agrees(
index: type_env.symbol_index, left: payload_name, right: actual_name)
payload_name != "" && names_agree
)
)
}

// The wall's decision procedure, over the record-literal field seam's own formal/actual pair.
//
// TWO EXCLUSIONS ARE LOAD-BEARING AND NEITHER IS INCIDENTAL. `Optional` is the language's own
// cardinality carrier rather than an ordinary coproduct -- a `T` standing in an `Optional<T>`
// position is the declared spelling, not a payload escape -- so both the CardOptional cardinality
// and a formal or actual literally named `Optional` are excluded before any declaration is walked.
// And a GENERIC coproduct is excluded because its payload positions can be type variables, which
// 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.
fn coproduct_payload_where_parent_required(
formal: Node,
actual: Node,
scope: InferScope
) -> Bool {
let source_indices = scope.type_env.source_indices
let either_optional = formal.return_cardinality == CardOptional || actual.return_cardinality == CardOptional
if either_optional || type_node_is_callable(n: formal) || type_node_is_callable(n: actual) {
false
} else {
let formal_name = authored_name_at(source_indices: source_indices, node: formal)
let actual_name = authored_name_at(source_indices: source_indices, node: actual)
let either_is_optional_carrier = qualified_last_segment(name: formal_name) == "Optional" ||
qualified_last_segment(name: actual_name) == "Optional"
if formal_name == "" || actual_name == "" || either_is_optional_carrier {
false
} else if application_type_names_compatible(
formal_name: formal_name,
lit_name: actual_name,
type_env: scope.type_env,
module_name: scope.module_name,
source_indices: source_indices) {
false
} else if transparent_alias_identity_agrees(
index: scope.type_env.symbol_index, left: formal_name, right: actual_name) {
false
} else {
let actual_rep = transparent_alias_representative(index: scope.type_env.symbol_index, name: actual_name)
match lookup_type_by_name(env: scope.type_env, name: formal_name) {
Present { value: decl } =>
let decl_is_concrete_coproduct = decl.connective == Disj && (decl.params |> count) == 0 && (decl.children |> count) > 0
let names_a_variant = has_child_named(n: decl, name: qualified_last_segment(name: actual_name), source_indices: source_indices) ||
has_child_named(n: decl, name: qualified_last_segment(name: actual_rep), source_indices: source_indices)
if decl_is_concrete_coproduct == false {
false
} else if names_a_variant {
false
} else {
coproduct_variant_payload_admits_type_name(
decl: decl,
actual_name: actual_name,
type_env: scope.type_env,
module_name: scope.module_name,
source_indices: source_indices)
}
Absent => false
}
}
}
}

// The peeling entry point, retained for the record-literal FIELD site, which has
// no prepared call plan to carry a peeled formal. It peels inside the ExprRecordLit
// arm exactly as before, so a non-record-literal actual still pays nothing.
Expand Down Expand Up @@ -5457,6 +5593,15 @@ fn infer_record_lit_structural(type_name: String?, field_inits: List<Node>, span
span: ar_typed.span,
module_name: scope.module_name
)]
} else if expected_node.return_cardinality != CardOptional
&& coproduct_payload_where_parent_required(
formal: formal_peeled, actual: actual_peeled, scope: scope) {
[type_mismatch_error(
expected: node_type_shape(n: formal_peeled, source_indices: scope.type_env.source_indices),
got: node_type_shape(n: actual_peeled, source_indices: scope.type_env.source_indices),
span: ar_typed.span,
module_name: scope.module_name
)]
} else {
[]
}
Expand Down
Loading
Loading