diff --git a/dag/gunbc/explicit_witness_admission.dag b/dag/gunbc/explicit_witness_admission.dag index 2926724d433..d4defd78453 100644 --- a/dag/gunbc/explicit_witness_admission.dag +++ b/dag/gunbc/explicit_witness_admission.dag @@ -158,6 +158,14 @@ data explicit_witness_admissions: List = [ 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", diff --git a/dag/test/claim/coproduct_payload_soundness_witness_test.dag b/dag/test/claim/coproduct_payload_soundness_witness_test.dag new file mode 100644 index 00000000000..546040d0eb5 --- /dev/null +++ b/dag/test/claim/coproduct_payload_soundness_witness_test.dag @@ -0,0 +1,87 @@ +module test.claim.coproduct_payload_soundness_witness_test + +// A COPRODUCT PAYLOAD CAN INHABIT ITS PARENT COPRODUCT FIELD, AND NOTHING REFUSES IT. +// +// This is the general form of the defect repaired in #8853 at one site. There, +// `dag_int_literal_node_from_magnitude` declared its parameter as +// `std.occurrence_identity.OccurrenceId` -- the PAYLOAD carried inside `MintedOccurrence` -- and +// assigned it straight into `Node.occurrence_id`, whose type is the `NodeOccurrenceId` coproduct. +// Nothing refused the assignment. The consequence surfaced 2,000 lines and one pipeline stage away +// as `non-exhaustive pattern match on: OccurrenceId { value: 79 }` in sixteen floor claims, because +// the total match over that field had no arm for a value that is not in its type. +// +// The declaration fix closed the live instance. It established nothing about the class, and the +// targeted sweep that found no second instance of that exact field/type pair is evidence about a +// spelling, not about the typing hole. So the question this file asks is the general one: can an +// ARBITRARY coproduct payload inhabit the field declared as its parent coproduct? +// +// MEASURED ANSWER, by direct execution before this witness was written -- minimal pair, no Node, no +// occurrence, no compiler internals: +// +// type CppInner { value: Int } +// type CppOuter = CppWrapped { inner: CppInner } +// type CppHolder { subject: CppOuter } +// +// POSITIVE CppHolder { subject: CppWrapped { inner: cpp_inner() } } accepted, exit 0 +// NEGATIVE CppHolder { subject: cpp_inner() } ACCEPTED BY TYPING, +// then at runtime: +// PatternMatchFailure +// { value: "CppInner { value: 7 }" } +// +// So the mechanism is not Node-specific and not occurrence-specific. It is a floor-class soundness +// hole -- values inhabit declared types -- and DESIGN section 4b puts a floor failure below the +// ladder rather than on a rung of it: this is not a class sitting at `mitigatable`, it is the +// baseline guarantee not holding. +// +// 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. +// +// 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 +// identity there still executes and its outcome is still asserted, but a failure counts as +// agreement. `gunbc.explicit_witness_admission` DOCUMENTS the red and its dissolution and, per the +// ruling recorded at floor_expected_red_chunk_13, does not itself gate the floor. Enrolling only in +// the second is what reds a build. +// +// THE POSITIVE CONTROL IS NOT OPTIONAL AND IS NOT COSMETIC. Without it, a compiler that refused +// EVERY record literal would satisfy the claim above. The control asserts that the correct spelling +// -- payload inside its arm -- still compiles, so what the red measures is the distinction and not +// the mechanism's blanket refusal. +// +// dissolve-on: none. Per DESIGN section 4b(4), a climb deletes the redundant lower-rung production +// machinery but never the evidence: when the wall lands, this probe's admission row deletes and the +// witness stays enrolled as a permanent regression control. Deleting it on the climb would recreate +// specification-without-execution one rung up. + +fn cpp_soundness_negative_fixture_source() -> String { + "module cpp.probe\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_payload_where_coproduct_required() -> CppHolder {\n CppHolder { subject: cpp_inner() }\n}\n" +} + +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. +test fn cpp_payload_where_coproduct_required_must_refuse() -> Bool { + !compile_dag_rust_emit_check( + cpp_soundness_negative_fixture_source(), + "src/cpp_probe.rs", + [], + [] + ) +} + +// THE POSITIVE CONTROL. The correct spelling must still compile, or the red above is satisfied by a +// compiler that refuses everything and measures nothing. +test fn cpp_payload_inside_its_own_arm_still_compiles() -> Bool { + compile_dag_rust_emit_check( + cpp_soundness_positive_fixture_source(), + "src/cpp_control.rs", + [], + [] + ) +} diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index 36e234d168e..1e293ac392b 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -389,8 +389,19 @@ fn floor_expected_red_chunk_13() -> List { Cons { head: "test.claim.method_arg_declared_contract_witness_test.w_method_arg_infers_against_declared_contract_not_element_type_test", tail: Empty {} } } +// The record-literal seam of the payload-as-coproduct soundness class (gunbc#8865). ELIGIBLE under +// this roster's own rule: it reaches its subject and answers -- compile_dag_rust_emit_check runs the +// fixture and returns, so the red is a real verdict, not a route gap. Its positive control +// (cpp_payload_inside_its_own_arm_still_compiles) is deliberately NOT enrolled: it must stay an +// ordinary green, or the pair stops discriminating. +// +// This row deletes in the change that lands the wall. The roster's passing-row arm is what makes +// that self-announcing rather than something anyone has to remember. fn floor_expected_red_chunk_14() -> List { - Empty {} + Cons { + head: "test.claim.coproduct_payload_soundness_witness_test.cpp_payload_where_coproduct_required_must_refuse", + tail: Empty {} + } } fn floor_expected_red_chunk_15() -> List {