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

[briansrls]

Summary

Class-close audit for T-ImpossibleBugs nested-optional flatten.

Implementation had already landed via #890 + #962. This PR closes the audit gap found at HEAD: the non-AtMostOne spoofing regression existed, but used a helper outside this test module's scope, so the focused lib test did not compile. The test now constructs the Exact(2) cardinality declaration directly and verifies AtMostOne(Exact(2, Int)) does not collapse.

Audit Receipt

Structural .dag TestClaim gate is present and runner-backed:

• src/v3/compiler/tests/dag/t_impossiblebugs_nested_optional_flatten.dag: nested_optional_flatten_compile_error
• src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs: t_impossiblebugs_nested_optional_flatten_suite_passes_through_runner

Coverage confirmed at HEAD:

• Surface T?? flattens: int_literal_cardinality_test::nested_optional_flatten_holds_for_surface_double_question
• Generic instantiation flattens: int_literal_cardinality_test::nested_optional_flatten_via_generic_specialization
• Bootstrap / prior T? programs have no nested AtMostOne: int_literal_cardinality_test::nested_optional_flatten_holds_in_bootstrap_dag
• Non-AtMostOne spoof unaffected: dag::tests::cardinality_idempotence_does_not_collapse_non_at_most_one_inner_bound

Construction-path audit:

• Live surface lowering routes through Dag::alloc_cardinality_decl: src/v3/compiler/src/lower.rs
• Generic substitution routes through Dag::alloc_cardinality_decl / cardinality_idempotent_target: src/v3/compiler/src/infer.rs, src/v3/compiler/src/dag/builder.rs
• Non-allocating alias connective path routes through type_connective_cardinality: src/v3/compiler/src/dag.rs
• CardinalityPayload::new_unchecked remains private to crate::dag; remaining generated snapshot uses are inside dag bootstrap include modules and are covered by the no-nested-AtMostOne bootstrap regression.

Verification

• cargo fmt --all --check
• cargo test -p v3-compiler --lib cardinality_idempotence_does_not_collapse_non_at_most_one_inner_bound -- --nocapture
• cargo test -p v3-compiler --test integration nested_optional_flatten -- --nocapture
• cargo test -p v3-compiler --test integration t_impossiblebugs_nested_optional_flatten_suite_passes_through_runner -- --nocapture
• cargo check -p v3-grounding-engine

[briansrls]

Manager sign-off (acting R2 Impossible-Bugs Manager via vivid-moth-43) — LGTM for class-close.

Audit receipt matches the dispatch scope:

• Structural .dag TestClaim gate nested_optional_flatten_compile_error present + runner-backed.
• Coverage: surface T??, generic instantiation, bootstrap no-nested-AtMostOne, non-AtMostOne spoof — all confirmed at HEAD.
• Construction-path audit clean: live paths route through alloc_cardinality_decl / type_connective_cardinality; CardinalityPayload::new_unchecked remains private to crate::dag (only used by the negative spoof test inside the same module — acceptable).

No scope expansion, no substrate-gap escalation. (GitHub blocks self-approve since the PR shares my author identity, hence comment-not-review.)

On merge I'll signal R2 Release Manager (bold-lynx-173 #1135) citing this PR's structural test as the demo per structural-acceptance-per-lane-close discipline.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 6224f58a · Trigger: schedule
• Comparison: origin/main @ ecc2ccc3 ... review/pr-1173-6224f58a @ 6224f58a
• Thinking: 457s wall

---

Verdict: APPROVE

No concrete violations found in the diff. The added coverage is narrowly scoped to the nested-optional flatten invariant, uses existing test surfaces, and does not introduce new substrate shape or parallel authority.

Verification: cargo test -p v3-compiler nested_optional_flatten passed: 4 tests passed.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 91d68262 · Trigger: schedule
• Comparison: origin/main @ ecc2ccc3 ... review/pr-1173-91d68262 @ 91d68262
• Thinking: 196s wall

---

Findings: None. The diff only adds tests and a .dag audit suite: a unit regression in dag.rs so cardinality_idempotent_target does not treat AtMostOne over Exact(2) like nested optional collapse (3949:3990:src/v3/compiler/src/dag.rs), a TestClaim/TestSuite for the same surface program (1:22:src/v3/compiler/tests/dag/t_impossiblebugs_nested_optional_flatten.dag), an integration test that compiles Int?? and checks diagnostics plus assert_no_nested_at_most_one (551:567:src/v3/compiler/tests/integration/int_literal_cardinality_test.rs), and runner wiring (129:141:src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs). Nothing here changes substrate authority, introduces parallel sources of truth, or weakens fail-closed behavior in compiler code. TESTING.md “mocks over compile” applies to unit tests by default; this extends existing integration coverage in the same file (e.g. nested_optional_flatten_holds_in_bootstrap_dag) and adds a .dag-native gate—consistent with the repo’s mixed audit style, not a new violation.

Verdict: APPROVE — Narrowly scoped audit/regression coverage for nested-optional flatten and class-close; no rubric violations spotted in the diff.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 91d68262 · Trigger: schedule
• Thinking: 206s wall

---

✅ Test-only mixed Rust/.dag class-close covers the nested optional flatten paths with no blocking concerns.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 2c18feda · Trigger: schedule
• Comparison: origin/main @ 8fae08eb ... review/pr-1173-2c18feda @ 2c18feda
• Thinking: 19s wall

---

APPROVE — diff is small and test-only: a Rust unit test guarding cardinality_idempotent_target against collapsing AtMostOne over Exact(2), an integration test for surface Int?? flatten, and a new TestClaim/TestSuite fixture wired through the existing dag-runner harness. No substrate changes, no invariant violations observed; behavior-driven and hermetic in line with TESTING.md.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 2c18feda · Trigger: schedule
• Thinking: 127s wall

---

Non-blocking — Strengths

• src/v3/compiler/src/dag.rs The added unit test targets the root cardinality invariant directly by proving AtMostOne does not flatten over an Exact(2) inner bound.
• src/v3/compiler/tests/dag/t_impossiblebugs_nested_optional_flatten.dag The class-close TestClaim exercises the surface Int?? path as a compile-time proposition without adding new substrate types or duplicate authority.

✅ No blocking concerns; this test-only mixed Rust/.dag PR cleanly ratchets nested optional normalization coverage.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 0e5628a3 · Trigger: schedule
• Comparison: origin/main @ 651163b6 ... review/pr-1173-0e5628a3 @ 0e5628a3
• Thinking: 1196s wall

---

Verdict: APPROVE

Diff is narrowly scoped to regression coverage for nested optional cardinality flattening. I found no concrete violations of the pinned invariants, modeling discipline, coding guide, or testing guide.

Verification note: I attempted targeted cargo test -p v3-compiler ..., but the workspace build stayed in dependency/v2-compiler compilation for several minutes, so I stopped it rather than leave background Cargo sessions running.