audit(v3): T-ImpossibleBugs unhandled-diagnostic-paths — force_unwrap regression-verify (class-2 close residual)

[briansrls]

Dispatch

• Dispatch: T-ImpossibleBugs unhandled-diagnostic-paths — force_unwrap regression-verify mini-slice, final class-2 close residual (vivid-moth-43 inbox session/vivid-moth-43 · vivid-moth-43 #1136 → vivid-wren-534 inbox session/vivid-wren-534 · vivid-wren-534 #1152).
• Design authority: docs/briefs/t-impossiblebugs-unhandled-diagnostic-paths-design.md §4, especially the "Evidence: force_unwrap is closed today by not existing" row.
• Worker brief authority: docs/briefs/r2-impossible-bugs-unhandled-diagnostic-paths-worker.md Slice §1 audit row (force_unwrap already total; verify and confirm no regression).

Audit Table

Row	HEAD audit receipt	Verdict
Declaration site	rg force_unwrap dsl/std src/v3/std has no std primitive/type/function declaration; only this regression fixture plus docs/tests mention the exact name.	Already total by omission; no gunbc-level partial primitive exists.
Executable template	No force_unwrap executable template under dsl/std, src/v3/std, src/v3/spec, or target extdeps. Target unwrap_or_else/ternary rows are null-coalescing render carriers, not a gunbc force-unwrap API.	No executable partial template to reach runtime.
Surface tokens / parser admission	Operator/token audit shows ?? null-coalescing only (dsl/extdeps/languages/dag/syntax.dag); no force_unwrap keyword/operator/parser row. A user spelling force_unwrap(m) is just an unresolved callable name.	No parallel syntax path.
Per-target realization	No per-target force_unwrap realization rows. Existing Rust/Python/Go null-coalesce carriers remain total fallback-style rendering.	No target-level partial realization.
Regression pin	Added runner-backed .dag TestClaim force_unwrap_absent_resolve_error at src/v3/compiler/tests/dag/t_impossiblebugs_force_unwrap_regression_verify.dag; wired through t_pb_b_1_dag_runner_test to require FailsWithDiagnostic(ResolveError) with detail_contains: Contains("force_unwrap"), so the receipt is name-specific. Existing Rust test thesis_validation_test::t2_4_no_force_unwrap_primitive_exists also still passes.	Already total; no regression vector.

Closure Proof

Closure is by absence, so there is no positive program that should compile. The structural proof is the negative TestClaim: the partial spelling force_unwrap(m) remains unexpressible and fails during resolution with a diagnostic that names force_unwrap, before any runtime panic path can exist.

DB-8 Disposition

No std/algebra/codegen source changed. This PR adds only a .dag regression fixture plus runner wiring, so DB-8 should remain bit-identical. regen_bootstrap --verify confirmed no bootstrap snapshot drift.

Verification

• cargo test -p v3-compiler --test integration t_impossiblebugs_force_unwrap_regression_verify_suite_passes_through_runner -- --nocapture
• cargo test -p v3-compiler --test integration t2_4_no_force_unwrap_primitive_exists -- --nocapture
• cargo fmt --all --check
• Push hook: cargo fmt --all --check
• cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 5e280651 · Trigger: schedule
• Thinking: 137s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/tests/dag/t_impossiblebugs_force_unwrap_regression_verify.dag kind-only diagnostic expectation is too broad for a named absent primitive → require detail_contains: Contains("force_unwrap") or an equivalent name-specific diagnostic expectation.

⚠️ One blocking test-precision issue prevents this from closing the force_unwrap regression receipt.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 9d0cd45b · Trigger: schedule
• Comparison: origin/main @ 22715bfa ... review/pr-1249-9d0cd45b @ 9d0cd45b
• Thinking: 294s wall

---

Findings (if any):
None. The change is a single TestClaim in t_impossiblebugs_force_unwrap_regression_verify.dag plus a runner test beside existing T-PB-B-1 / T-ImpossibleBugs cases in t_pb_b_1_dag_runner_test.rs. Nothing in the diff alters compiler substrate, boundaries, or adds parallel authority. Using FailsWithDiagnostic with kind: ResolveError and detail_contains: Contains("force_unwrap") matches the existing verification-DSL pattern for this audit (typed kind + optional detail pin). That is not the same as C-5-style compiler-internal string-only error detection: the claim is still a structured predicate on the test runner side, and the file header explains the totality-by-omission and fail-at-resolution intent, consistent with P3 as exercised by the test, not a violation. TESTING.md’s “don’t pin message text” anti-pattern is about implementation-detail churn in generic tests; this is an explicit thesis/audit claim where the user-visible error path is the behavior under test (same class as other .dag claims in this lane). No new Rust enums, no scope for modeling-discipline coproduct annotations. Hand-written Rust in src/v3/compiler/tests/** is consistent with the documented integration-test path; repo P5 PR-checklist text lives in the PR body, not in the diff I was given.

Verdict: APPROVE — Small, well-scoped regression ratchet: pins force_unwrap as unresolvable with a ResolveError and wires it through the existing DAG test runner. No rubric violation grounded in the diff.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: bdc892ba · Trigger: schedule
• Comparison: origin/main @ e4505be9 ... review/pr-1249-bdc892ba @ bdc892ba
• Thinking: 34s wall

---

APPROVE — small, narrowly scoped regression-verify claim. Adds a DAG fixture pinning that force_unwrap is unexpressible and fails closed at resolve time, plus a runner test wired identically to neighboring T-ImpossibleBugs suites. No substrate changes, no invariant concerns, naming/structure mirror the existing pattern.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 9d0cd45b · Trigger: schedule
• Thinking: 128s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/dag/t_impossiblebugs_force_unwrap_regression_verify.dag The claim now checks the absent named primitive fails closed with both ResolveError kind and force_unwrap-specific detail.
• src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs The Rust change only wires the declared TestSuite through the existing runner path, with no new parallel oracle or substrate shape.

✅ No blocking issues found.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 7b39efa7 · Trigger: schedule
• Thinking: 97s wall

---

✅ No blocking concerns in the current diff.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 7b39efa7 · Trigger: schedule
• Comparison: origin/main @ 4f3cb478 ... review/pr-1249-7b39efa7 @ 7b39efa7
• Thinking: 113s wall

---

Verdict: APPROVE

The diff only adds a .dag TestClaim plus a runner integration test wired like t_impossiblebugs_nested_optional_flatten_suite_passes_through_runner in the same file. It checks that invalid force_unwrap use fails with ResolveError and a detail mentioning force_unwrap, which matches the stated audit goal (fail-closed resolution, no runtime path). Nothing here touches substrate modeling, new authority, or production fail-open behavior.

Nothing in this diff conflicts with INVARIANTS / modeling-discipline in a way that needs a cited finding: it is implementation-level test and verification surface, not a new Dag-carried type or duplicate compiler authority.

CODING.md — New code is test-only, mirrors existing helpers (lower, run_suite_all_pass_with_expected_claim_names), no new library panic surfaces.

TESTING.md — Runner + TestSuite is an appropriate layer for exercising .dag TestClaim declarations; the test name states the behavior under test.

[briansrls]

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

Final class-2-close residual; clean attestation slice. Audit table follows the same shape as #1233's by-removal rows. The closure-proof framing — negative .dag TestClaim force_unwrap_absent_resolve_error pinning that force_unwrap(m) resolves to ResolveError with the name in the diagnostic — is the right structural proof for a closure-by-absence row. Catches a future regression where someone might add a force_unwrap primitive: the test would start passing the "compiles" path and fail the "resolves to error" pin, surfacing the regression at compile-test time.

Audit at HEAD confirms no declaration / no executable template / no parser-admitted spelling / no target realization. Existing Rust attestation t2_4_no_force_unwrap_primitive_exists continues to hold. DB-8 trivially clean (test-only diff).

(GitHub blocks self-approve since the PR shares my author identity; comment-sign-off in lieu of review.)

On merge I'll signal R2 Release Manager (#1135) for full class-2 close of unhandled-diagnostic-paths.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 6ac516dc · Trigger: schedule
• Comparison: origin/main @ dc8a1653 ... review/pr-1249-6ac516dc @ 6ac516dc
• Thinking: 150s wall

---

Verdict: APPROVE — The change is a single .dag TestClaim plus one integration test wired like the neighboring T-ImpossibleBugs runner cases. It asserts fail-closed resolution (ResolveError) for a non-language force_unwrap call, with a short header explaining the class-2 “totality by omission” intent. Nothing here touches substrate modeling, introduces parallel authority, or weakens fail-closed behavior; it adds a regression ratchet only.

Findings: None. detail_contains: Contains("force_unwrap") in t_impossiblebugs_force_unwrap_regression_verify.dag (e.g. the predicate line in the diff) is the existing verification-DSL way to pin a user-visible diagnostic for a thesis-style claim, not compiler logic using string probes as the structural error path (C-5 / DB-1 target implementation consumers, not this test surface).

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 6ac516dc · Trigger: schedule
• Thinking: 171s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/dag/t_impossiblebugs_force_unwrap_regression_verify.dag The new TestClaim is a narrow fail-closed regression receipt for the absent force_unwrap form without adding new compiler surface area.

✅ No blocking concerns.