From 4779ebc5cbc74104f02481b7b5e0e9fb9e076032 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Tue, 28 Apr 2026 23:21:02 -0400 Subject: [PATCH 1/2] WIP: vivid-wren-534 --- src/v3/compiler/src/dag.rs | 34 +++++++++++++++++++ ...impossiblebugs_nested_optional_flatten.dag | 22 ++++++++++++ .../int_literal_cardinality_test.rs | 15 ++++++++ .../integration/t_pb_b_1_dag_runner_test.rs | 13 +++++++ 4 files changed, 84 insertions(+) create mode 100644 src/v3/compiler/tests/dag/t_impossiblebugs_nested_optional_flatten.dag diff --git a/src/v3/compiler/src/dag.rs b/src/v3/compiler/src/dag.rs index df9361d10c6..39e7ab844ed 100644 --- a/src/v3/compiler/src/dag.rs +++ b/src/v3/compiler/src/dag.rs @@ -3945,4 +3945,38 @@ mod tests { canonical `Int?` decl (recursive alias chain, not one step)" ); } + + #[test] + fn cardinality_idempotence_does_not_collapse_non_at_most_one_inner_bound() { + let mut dag = Dag::new(); + dag.populate_primitive_cache(); + let int_decl = dag.int_shape().expect("bootstrap Int").declaration; + let exact_two = push_test_declaration( + &mut dag, + None, + TypeConnective::Cardinality(CardinalityPayload::new_unchecked( + int_decl, + CardinalityBound::Exact(2), + )), + Vec::new(), + ); + + assert_eq!( + cardinality_idempotent_target(&dag, exact_two, CardinalityBound::AtMostOne), + None, + "AtMostOne over Exact(2) is optional fixed-cardinality, not nested optional" + ); + + let optional_exact_two = dag.alloc_cardinality_decl( + exact_two, + CardinalityBound::AtMostOne, + SourceSpan::new("cardinality_exact_spoof_test", 0, 0), + ); + let TypeConnective::Cardinality(payload) = &dag.declaration(optional_exact_two).connective + else { + panic!("optional Exact(2) should remain a Cardinality declaration"); + }; + assert_eq!(payload.element(), exact_two); + assert_eq!(payload.bound(), CardinalityBound::AtMostOne); + } } diff --git a/src/v3/compiler/tests/dag/t_impossiblebugs_nested_optional_flatten.dag b/src/v3/compiler/tests/dag/t_impossiblebugs_nested_optional_flatten.dag new file mode 100644 index 00000000000..0587f9ceb38 --- /dev/null +++ b/src/v3/compiler/tests/dag/t_impossiblebugs_nested_optional_flatten.dag @@ -0,0 +1,22 @@ +// T-ImpossibleBugs nested-optional flatten class-close gate. +// +// The claim program typechecks only if the surface `Int??` parameter lowers to +// the same cardinality shape as `Int?`; without the constructor invariant, the +// return annotation would require `Int?` while the body carries `Int??`. + +module v3.compiler.tests.t_impossiblebugs.nested_optional_flatten + +import std.verification { TestClaim, TestSuite, TestPredicate } + +data nested_optional_flatten_compile_error: TestClaim = { + name: "nested_optional_flatten_compile_error", + source: "fn flatten_probe(x: Int??) -> Int? = x\n", + file_name: "nested_optional_flatten_compile_error.v3", + predicate: Compiles, + requires: [] +} + +data suite_nested_optional_flatten_class_close: TestSuite = { + name: "t-impossiblebugs/nested-optional-flatten/class-close", + claims: [nested_optional_flatten_compile_error] +} diff --git a/src/v3/compiler/tests/integration/int_literal_cardinality_test.rs b/src/v3/compiler/tests/integration/int_literal_cardinality_test.rs index 5f444fc8c4d..ad015c866e1 100644 --- a/src/v3/compiler/tests/integration/int_literal_cardinality_test.rs +++ b/src/v3/compiler/tests/integration/int_literal_cardinality_test.rs @@ -548,6 +548,21 @@ fn nested_optional_flatten_holds_in_bootstrap_dag() { assert_no_nested_at_most_one(&dag, "bootstrap"); } +#[test] +fn nested_optional_flatten_holds_for_surface_double_question() { + let src = "\ +fn flatten_probe(x: Int??) -> Int? = x +"; + let dag = compile_to_dag(src, "nested_optional_surface_double_question.v3") + .expect("surface Int?? should silently normalize to Int?"); + assert!( + dag.diagnostics().is_empty(), + "surface nested optional should be diagnostic-free, got: {:?}", + dag.diagnostics() + ); + assert_no_nested_at_most_one(&dag, "surface T??"); +} + #[test] fn nested_optional_flatten_via_generic_specialization() { // `unwrap_id` is generic over T and takes/returns `T?`. Calling it with diff --git a/src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs b/src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs index 815cdf76c59..4008ed57218 100644 --- a/src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs +++ b/src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs @@ -126,6 +126,19 @@ fn t_pb_b_1_execute_command_boundary_suite_passes_through_runner() { run_suite_all_pass(&dag, "suite_execute_command_boundary"); } +#[test] +fn t_impossiblebugs_nested_optional_flatten_suite_passes_through_runner() { + let dag = lower( + include_str!("../dag/t_impossiblebugs_nested_optional_flatten.dag"), + "src/v3/compiler/tests/dag/t_impossiblebugs_nested_optional_flatten.dag", + ); + run_suite_all_pass_with_expected_claim_names( + &dag, + "suite_nested_optional_flatten_class_close", + &["nested_optional_flatten_compile_error"], + ); +} + /// R1 gate suites from `tests/fixtures/r1_gates.dag` — same `TestClaim` authority and /// exact `claim_name` receipt as the retired /// `r1_manual_claim_gate_test` / `testgen_structural_coverage_gate_test` shims. From 6224f58adf0feb9bd97fd3b3598a2a39ceaf6e63 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 29 Apr 2026 03:23:24 +0000 Subject: [PATCH 2/2] test(v3): fix nested optional spoof regression setup --- src/v3/compiler/src/dag.rs | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/src/v3/compiler/src/dag.rs b/src/v3/compiler/src/dag.rs index 39e7ab844ed..9008248f28f 100644 --- a/src/v3/compiler/src/dag.rs +++ b/src/v3/compiler/src/dag.rs @@ -3951,15 +3951,24 @@ mod tests { let mut dag = Dag::new(); dag.populate_primitive_cache(); let int_decl = dag.int_shape().expect("bootstrap Int").declaration; - let exact_two = push_test_declaration( - &mut dag, - None, - TypeConnective::Cardinality(CardinalityPayload::new_unchecked( + let exact_two = dag.alloc_declaration_id(); + dag.push_declaration(Declaration { + id: exact_two, + name: None, + connective: TypeConnective::Cardinality(CardinalityPayload::new_unchecked( int_decl, CardinalityBound::Exact(2), )), - Vec::new(), - ); + type_params: Vec::new(), + phantom_params: Vec::new(), + meta_tag: None, + specialization_parent: None, + inhabits: None, + value_body: None, + refinement: None, + nominal_opacity: None, + span: SourceSpan::new("cardinality_exact_spoof_test", 0, 0), + }); assert_eq!( cardinality_idempotent_target(&dag, exact_two, CardinalityBound::AtMostOne),