audit(v3): T-ImpossibleBugs nested-optional flatten class-close

src/v3/compiler/src/dag.rs

@@ -3945,4 +3945,47 @@ 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 = dag.alloc_declaration_id();
+        dag.push_declaration(Declaration {
+            id: exact_two,
+            name: None,
+            connective: TypeConnective::Cardinality(CardinalityPayload::new_unchecked(
+                int_decl,
+                CardinalityBound::Exact(2),
+            )),
+            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),
+            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);
+    }
 }

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]
+}

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

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.