R3 gate #85: SuiteClaim wrapper migration — Enumerated/Quantified coproduct

[briansrls]

Summary

Closes the CONSUMER_LANDED step for §1.8 gate #85 forall_exists_quantifier_substrate_landed (T-Tests-As-Data-Completeness, R3 Cluster M Phase 1).

• Flips TestSuite.claims: List<TestClaim> → List<SuiteClaim> in src/v3/std/verification.dag, dissolving the staged-coproduct comment block that previously deferred the wrapper migration.
• Mechanically wraps every existing fixture suite entry as Enumerated(<TestClaim>) across all .dag fixtures + templates under src/v3/compiler/tests/ (48 sites).
• Extends TestRunner::run_suite_entry to dispatch on the SuiteClaim variant: Enumerated runs the underlying TestClaim; Quantified returns ClaimResult::NotYetImplemented with a concrete-row citation to docs/r3-structure.md §T-Tests-As-Data-Completeness + docs/r3-program-plan.md §1.8 row #85 per INVARIANTS P5(b). Unknown variants / non-reference payloads fail closed.
• Regenerates bootstrap_generated.rs + bootstrap_generated_without_parse_surface.rs snapshots via regen_bootstrap.

Substrate carriers (Quantifier, QuantifiedTestClaim, SuiteClaim) already landed via PR #2647 (DECLARED → CONSUMER_LANDED is what this PR delivers). Quantifier evaluation (PASSING) is bounded-deferred to Cluster M Phase 2 (gate #87 cementing-test discipline) + Phase 3 (gate #84 bulk-port) per the sequencing plan at docs/audit/r3-cluster-m-sequencing-plan-2026-05-09.md.

Test plan

• cargo test -p v3-compiler — 376 unit-test passes on the pre-merge head (eacd186); 10 pre-existing failures in execute_command_timebound_tests (unshare / namespace / sandbox-dependent — unrelated to this change, fail on main in the BB-remote container).
• cargo run -p v3-compiler --bin regen_bootstrap --features bootstrap-regen-fresh — clean regeneration; bootstrap snapshots match the post-merge src/v3/std/verification.dag.
• Compile check: cargo test -p v3-compiler --lib --no-run → success.

Receipt (INVARIANTS P5(b))

Single checkable receipt: TestSuite.claims field type at src/v3/std/verification.dag:406 is now List<SuiteClaim> (was List<TestClaim>), and every claims: [...] site under src/v3/compiler/tests/ wraps entries as Enumerated(...). The runner's Quantified arm cites a concrete ROADMAP row for its deferral.

Co-Authored-By: Claude Opus 4.7 (1M context) noreply@anthropic.com

[briansrls]

Disposition for the prior REQUEST_CHANGES review at head eacd186 (claude/claude-opus-4-7, 2026-05-12T05:53:37Z):

• Finding 1 — PR body is the unfilled TODO template, missing Summary + P5(b) receipt. Addressed at current head: PR body now carries a concrete Summary, Test plan, and a single-checkable Receipt section explicitly citing the TestSuite.claims type flip and the Enumerated(...) wrap.
• Finding 2 — Quantified NotYetImplemented string is a bounded deferral without a concrete ROADMAP row citation as P5(b) requires. Addressed in commit eca9d4646: the message now cites docs/r3-structure.md §"T-Tests-As-Data-Completeness" (gate RT1-RT4: model correctness — credential wiring, fail-closed auth, fil… #87 + gate Implement SDLC pipeline: worker dispatch, stage handlers, and integration tests #84 lanes) and docs/r3-program-plan.md §1.8 row #85 as the concrete tracking rows for quantifier evaluation.

Non-concerns from the prior review (clean coproduct dissolution, mechanical fixture wrap, fail-closed runner on unknown variants) are unchanged at current head.

— sent from sleek-ibex-221

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: de6148da · Trigger: schedule
• Thinking: 769s wall

---

BLOCKING (1)

Root Cause

• src/v3/std/verification.dag SuiteClaim wrapper migration flipped the suite carrier before generalizing obligation materialization over Enumerated and Quantified entries → add a SuiteClaim-level obligation projection that reads each variant's single requires authority.

ROADMAP — Verified

• T-Tests-As-Data-Completeness gate #85: docs/r3-program-plan.md §1.8 row #85 exists and tracks forall_exists_quantifier_substrate_landed under the cited lane.

⚠️ One substrate facts-flow gap needs closing before the wrapper migration lands.

[briansrls]

Addressed at commit 5f6af161e:

The SuiteClaim-level obligation projection now lives at src/v3/std/verification.dag:428-444:

• obligation_for_quantified_claim(q: QuantifiedTestClaim) -> TestObligation — same requires projection rule as obligation_for_claim.
• obligation_for_suite_claim(entry: SuiteClaim) -> TestObligation — match-dispatches Enumerated(c) | Quantified(q) onto the shared TestObligation surface.
• materialize_test_obligations(claims: List<SuiteClaim>) -> List<TestObligation> — now takes the post-migration carrier; QuantifiedTestClaim.requires flows forward through the dependency-walk on equal footing with enumerated claims.

requires remains the sole authority for ResourceReference edges on both variants per design §2.2 / P2. lane2_stage_2c_db15_test passes against the regenerated bootstrap.

— sent from sleek-ibex-221

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 5f6af161 · Trigger: manual
• Comparison: main @ e9760a32 ... session/sleek-ibex-221 @ 5f6af161
• Conversation: View conversation

---

1. Story of the diff

This PR finishes the SuiteClaim wrapper migration for tests-as-data: TestSuite.claims moves from a flat List<TestClaim> to an ordered List<SuiteClaim>, where each suite entry is explicitly either Enumerated(TestClaim) or Quantified(QuantifiedTestClaim) at src/v3/std/verification.dag:404. The existing .dag suites and Rust string-fixture tests are mechanically migrated by wrapping every previous direct claim reference in Enumerated(...), for example src/v3/compiler/tests/dag/t_pb_b_1_execute_command_boundary.dag:52-55 and src/v3/compiler/tests/integration/test_runner_test.rs:80.

The substrate side also generalizes obligation projection: enumerated claims still use obligation_for_claim, quantified claims project through obligation_for_quantified_claim, and the suite-level mapper now dispatches over SuiteClaim at src/v3/std/verification.dag:431-446. The Rust runner gains the corresponding wrapper dispatch in run_suite_entry, running enumerated claims normally and returning a tracked NotYetImplemented result for quantified evaluation at src/v3/compiler/src/test_runner.rs:2454-2503; the generated bootstrap snapshots are regenerated around the new substrate declarations.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation)

Compliant — this does touch substrate: TestSuite.claims becomes List<SuiteClaim> at src/v3/std/verification.dag:404, and the single ordered list avoids the bad alternative of parallel enumerated_claims / quantified_claims fields. That matches the coproduct-vs-coordinate test: a suite entry is one-at-a-time Enumerated or Quantified, not both simultaneously, so the sum is modeling alternatives rather than compressing coordinates. chatgpt-review-ee775cdb-6c1a-49…

2. INVARIANTS.md + modeling-discipline.md

Finding — non-blocking, single-authority metadata. The new quantified obligation projection uses the modeled quantified claim name as the claim identity: TestObligation { claim_name: q.name, resources: q.requires } at src/v3/std/verification.dag:431-432. But the new runner branch for Quantified reports claim_name: decl_label at src/v3/compiler/src/test_runner.rs:2484-2486, where decl_label was derived from the declaration symbol at src/v3/compiler/src/test_runner.rs:2471-2475. That creates two possible identities for the same quantified suite entry: dependency/obligation reporting uses q.name, while runner reporting uses the declaration name. P2 says every fact should live in exactly one authoritative place, and modeling-discipline’s single-authority metadata rule is the same shape. chatgpt-review-ee775cdb-6c1a-49…

chatgpt-review-2bfd2a62-e8ac-4c…

The low-cost fix is to parse or project the QuantifiedTestClaim enough to use its name field even while evaluation remains NotYetImplemented; malformed quantified declarations can still fail closed.

3. CODING.md

Compliant — the Rust change keeps the old pipeline readable by extracting the new suite-entry dispatch into run_suite_entry at src/v3/compiler/src/test_runner.rs:2454 rather than embedding a larger nested closure in run_suite, and every branch returns a structured ClaimEvaluation / ClaimResult rather than a primitive status. That matches CODING’s “data + functions” and structured-carrier conventions. chatgpt-review-0e895021-a534-41…

chatgpt-review-0e895021-a534-41…

4. TESTING.md

Compliant, with one caveat tied to the finding above — the diff updates the existing suite fixtures and runner string fixtures to the new .dag surface, preserving the tests-as-data direction rather than adding new Rust-only coverage. TESTING.md’s long-term shape is .dag declarations evaluated structurally by the runner, and this PR moves existing suites toward that surface by making suite entries explicit wrappers. chatgpt-review-0e895021-a534-41…

The caveat: I did not see a new test in this diff that exercises a Quantified(...) suite entry through run_suite_entry; since the branch is explicitly NYI, I would not block on full quantifier behavior, but the name-authority fix above should be easy to cement with one minimal quantified-suite fixture.

5. LOCKED DESIGN DECISIONS

Compliant — no locked design target appears to be contradicted. The change is aligned with the thesis/testing direction that tests live as .dag TestClaim data and the runner consumes declarations, rather than hand-authored behavior assertions. chatgpt-review-c506810a-0b02-47…

6. TRACKED vs UNTRACKED DEBT

Compliant — the only obvious temporary behavior is quantified runner evaluation returning ClaimResult::NotYetImplemented at src/v3/compiler/src/test_runner.rs:2484-2494. The message names the bound and intended dissolution path: “gate #85 substrate-only landing,” Cluster M Phase 2/3, gate #87 / #84 lanes, and the tracking row at docs/r3-program-plan.md §1.8 row #85. That satisfies the tracked-bridge shape in this diff: documentation, bounded scope, and a named follow-up trigger. chatgpt-review-ee775cdb-6c1a-49…

2.5. Top-down PM intent review

Compliant, subject to the non-blocking identity comment above. At the PM level, this PR preserves the intended direction: tests remain .dag data, suite ordering stays in one ordered claims list, and the quantifier surface is introduced without splitting enumerated and quantified claims into parallel authorities. The thesis says tests are structural data and that the .dag predicate vocabulary is the test-writing language; changing existing suites to Enumerated(...) entries while adding Quantified(...) as the next suite-entry shape is consistent with that direction. chatgpt-review-c506810a-0b02-47…

I do not see a concrete diff-cited semantic dilution of the zero-floor / tests-as-data plan. The added hand-Rust dispatch in test_runner.rs is an implementation consumer inside an already-hand-authored runner, and the quantified branch’s deferral is explicitly tracked rather than presented as permanent behavior.

3. Verdict

APPROVE_WITH_COMMENTS

The substrate migration is coherent: one ordered SuiteClaim list, existing suites wrapped as Enumerated, quantified obligations flowing through the same projection surface, and generated bootstrap refreshed. I would fix the quantified NYI reporting to use the modeled QuantifiedTestClaim.name rather than the declaration label, but because quantified evaluation is explicitly deferred, I would treat that as a non-blocking single-authority cleanup rather than a merge blocker.

[briansrls]

Addressed openai-pro APPROVE_WITH_COMMENTS non-blocking finding at commit 0093ae98d:

test_runner.rs:2484-2496 now reads the modeled name field off the QuantifiedTestClaim declaration via structural_fields(decl) + string_field(fields, "name"), so ClaimEvaluation.claim_name matches obligation_for_quantified_claim's q.name projection. Single identity across obligation-walk and runner reporting (INVARIANTS P2). Fail-closed fallback to the declaration label when the structural read fails.

— sent from sleek-ibex-221

[briansrls]

Addressed codex REQUEST_CHANGES at commit 708491212:

test_runner.rs Quantified branch now validates QuantifiedTestClaim shape via validate_quantified_claim_shape(decl) before returning NotYetImplemented. The validator requires the declaration be structural and carry name + generator + quantifier + predicate + requires (the substrate shape from src/v3/std/verification.dag:386-392). Malformed declarations — e.g. Quantified(some_int_decl) — now return ClaimResult::Fail with a structured reason, matching the discipline TestClaimValue::from_declaration already enforces on the Enumerated path (INVARIANTS P3 / fail-closed at the boundary).

On success the validator returns the modeled name so claim_name remains the single-authority identity matching obligation_for_quantified_claim.

— sent from sleek-ibex-221

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 5f6af161 · Trigger: schedule
• Thinking: 622s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/test_runner.rs Quantified evaluation was deferred after adding the SuiteClaim runner boundary → validate the deferred carrier's generator, quantifier, predicate, and payload arity against the substrate shape before returning NotYetImplemented.

ROADMAP — Verified

• T-Tests-As-Data-Completeness gate #85: docs/r3-program-plan.md §1.8 row #85 still tracks forall_exists_quantifier_substrate_landed and names the wrapper migration/generated-runner consumer path.

⚠️ One fail-closed boundary gap remains in the quantified suite-entry validator.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: c3c2edd1 · Trigger: schedule
• Thinking: 578s wall

---

BLOCKING (1)

Root Cause

• src/v3/std/verification.dag SuiteClaim wrapper migration updated the tests/dag copy but missed the live tests/fixtures/r1_pb_census_gates.dag consumer included by integration tests → wrap that fixture's six entries as Enumerated(...) in the same migration.

ROADMAP — Verified

• T-Tests-As-Data-Completeness gate #85: docs/r3-program-plan.md §1.8 row #85 tracks forall_exists_quantifier_substrate_landed and the SuiteClaim consumer/wrapper prerequisite.

⚠️ The prior facts-flow issue is fixed, but one live TestSuite fixture remains outside the new SuiteClaim carrier.

[briansrls]

Verified against current HEAD (84048095f):

The codex review at 5f6af161 predates 708491212 (fail-closed structural validator) and now 84048095f (payload-arity check). Current state of the quantified suite-entry boundary at src/v3/compiler/src/test_runner.rs:2454-2515:

• Variant label — variant_value(entry) must succeed; otherwise ClaimResult::Fail (TestSuite … claim entry is not a SuiteClaim variant).
• Payload arity — must be exactly 1 argument (added at 84048095f); reject otherwise with structured Fail. Both Enumerated(TestClaim) and Quantified(QuantifiedTestClaim) are single-arg coproduct arms per verification.dag:400-405.
• Reference payload — the single payload must be FieldValue::Reference; otherwise Fail.
• Quantified declaration shape — validate_quantified_claim_shape(decl) requires structural body + name + generator + quantifier + predicate + requires (list); otherwise Fail with field-specific reason.
• Unknown variant label — anything other than Enumerated/Quantified → Fail.

All four reviewer-named shape facets (generator, quantifier, predicate, payload arity) are now validated before NotYetImplemented returns. The Enumerated path continues to delegate to TestClaimValue::from_declaration for analogous structural validation.

— sent from sleek-ibex-221

[briansrls]

Addressed inline BLOCKING at verification.dag:404 at commit de39c8467:

The cited fixture path src/v3/compiler/tests/fixtures/r1_pb_census_gates.dag does not exist in the tree — but the underlying complaint (bare-TestClaim suite entries leaking past the new boundary) was real for one site I missed: the inline Rust string fixture at src/v3/compiler/tests/integration/m1_5_verification_test.rs:340. Wrapped each entry as Enumerated(...).

Sweep verification: grep -rn "claims:\s*\[" --include="*.dag" --include="*.rs" src/v3/ shows every remaining claims: [...] site (123 wrapped entries across .dag files + this Rust fixture) wraps in Enumerated(...) / Quantified(...). No bare-TestClaim carriers remain.

— sent from sleek-ibex-221

[briansrls]

Verified against current HEAD (de39c8467):

The cited path src/v3/compiler/tests/fixtures/r1_pb_census_gates.dag does not exist in the tree:

```
$ find src -iname "r1_pb_census" -o -iname "pb_census_gates"
src/v3/compiler/tests/dag/t_r1c_d_pb_census_gates.dag
```

The actually-existing PB-census-gates fixture src/v3/compiler/tests/dag/t_r1c_d_pb_census_gates.dag:147-154 already wraps all six entries as Enumerated(...) (migrated in the original WIP cherry-pick eacd186).

The one inline Rust fixture I had missed (m1_5_verification_test.rs:340) was wrapped at de39c8467. Full sweep — grep -rn "claims:\s*\[" --include="*.dag" --include="*.rs" src/v3/ — shows zero bare-TestClaim suite entries remaining.

— sent from sleek-ibex-221

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: de39c846 · Trigger: schedule
• Thinking: 605s wall

---

Non-blocking — Strengths

• src/v3/std/verification.dag SuiteClaim preserves suite ordering while projecting both Enumerated and Quantified entries through one TestObligation surface.
• src/v3/compiler/src/test_runner.rs The runner fails malformed SuiteClaim entries closed before claim execution and uses the modeled QuantifiedTestClaim.name for deferred reporting.

ROADMAP — Verified

• forall_exists_quantifier_substrate_landed: docs/r3-program-plan.md §1.8 row #85 tracks the SuiteClaim wrapper migration and deferred quantified-claim consumer work.

✅ No blocking concerns; targeted cargo verification could not complete because restricted network/offline cache resolution blocked dependency lookup.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-thinking
• Commit: 8b2473a5 · Trigger: manual
• Comparison: main @ 74ce2874 ... session/sleek-ibex-221 @ 8b2473a5
• Conversation: View conversation

---

1. Story of the diff

This PR finishes the SuiteClaim wrapper migration that was previously staged: TestSuite.claims is no longer a direct List<TestClaim>, but a List<SuiteClaim> where existing claims are wrapped as Enumerated(...) and the new quantified substrate can enter as Quantified(QuantifiedTestClaim) (src/v3/std/verification.dag:395-404). The .dag substrate also moves obligation projection up to the wrapper level, so enumerated and quantified claims both project onto the same TestObligation surface instead of requiring parallel lists or separate dependency-walk paths (src/v3/std/verification.dag:428-446). On the Rust side, TestRunner now routes each suite entry through run_suite_entry, validates the SuiteClaim variant/payload shape fail-closed, runs enumerated claims as before, and reports quantified claims as explicitly NYI after validating their structural declaration shape (src/v3/compiler/src/test_runner.rs:2454-2524, src/v3/compiler/src/test_runner.rs:5288-5307). The rest of the diff is mostly mechanical fallout: generated bootstrap snapshots and existing test fixtures are regenerated/wrapped as Enumerated(...).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — this does touch substrate: TestSuite.claims changes to List<SuiteClaim> at src/v3/std/verification.dag:404, and the implementation consumes that substrate shape through run_suite_entry rather than maintaining separate enumerated/quantified suite lists (src/v3/compiler/src/test_runner.rs:2450-2454). That matches Boundary Discipline / single-authority: one ordered carrier, two variant readers. The governing principles require boundaries to carry enough declared information and facts to live in one authoritative place. chatgpt-review-90d5320d-3cbf-40…

1. INVARIANTS.md + modeling-discipline.md.

Compliant — P2/facts-flow-forward is handled by obligation_for_suite_claim, which dispatches both Enumerated(c) and Quantified(q) onto the same TestObligation surface (src/v3/std/verification.dag:439-446). P3/fail-closed is also explicit: non-variant entries fail (src/v3/compiler/src/test_runner.rs:2455-2461), payload arity must be exactly one (src/v3/compiler/src/test_runner.rs:2467-2475), payloads must be references (src/v3/compiler/src/test_runner.rs:2477-2484), and quantified declarations must carry name/generator/quantifier/predicate/requires with requires as a list (src/v3/compiler/src/test_runner.rs:5288-5307). Modeling-discipline’s concrete practices call out fail-closed, facts-flow-forward, coproduct dissolution, and single-authority metadata as the relevant checks here. chatgpt-review-1392c254-5a7d-4e…

1. CODING.md.

Compliant — the Rust change keeps the runner logic decomposed into a small helper (run_suite_entry) and a free structural validator (validate_quantified_claim_shape) rather than burying the new branch inline in run_suite; the boundary failures return structured ClaimEvaluation / ClaimResult rather than panicking (src/v3/compiler/src/test_runner.rs:2454-2524, src/v3/compiler/src/test_runner.rs:5288-5307). That is consistent with the project’s data + functions / clear-interface style.

1. TESTING.md.

Finding — missing direct Quantified regression for the new runner branch. The diff adds a new Quantified execution path at src/v3/compiler/src/test_runner.rs:2497 and a structural validator at src/v3/compiler/src/test_runner.rs:5288, but the changed runner tests I found only migrate existing suites to Enumerated(...), e.g. src/v3/compiler/tests/integration/test_runner_test.rs:80 and src/v3/compiler/tests/integration/m1_5_verification_test.rs:340. Because the PR’s core behavior is “Quantified claims can now sit in SuiteClaim and fail/report through the runner boundary,” it should add at least one focused Quantified(...) suite entry asserting the NYI result uses the modeled quantified name, plus one malformed quantified entry/shape asserting fail-closed behavior. TESTING.md expects behavior-driven tests for the interface being promised, and .dag TestClaim/TestSuite harnesses are the preferred surface when possible. chatgpt-review-e218ceca-7ed3-4e…

1. LOCKED DESIGN DECISIONS.

N/A — I do not see this diff altering a locked design decision. It appears to implement the already-staged wrapper migration by making SuiteClaim live and regenerating consumers, not changing the higher-level design meaning.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the remaining deferred piece is explicitly scoped: the runner returns ClaimResult::NotYetImplemented for quantified evaluation and names gate #85 plus Cluster M Phase 2/3 / docs row tracking in the message (src/v3/compiler/src/test_runner.rs:2505-2513). The previous staging comment in verification.dag is also replaced with live “CONSUMER_LANDED wrapper migration” wording (src/v3/std/verification.dag:391-399), so this PR is not leaving the old wrapper migration as an unbounded bridge.

2.5. Top-down PM intent review

Compliant, with the testing caveat above. The PM-level intent is preserved: tests remain structural data, the suite surface becomes a single ordered wrapper carrier, and quantified claims are introduced without creating a parallel dependency surface. That aligns with the thesis/testing direction that the proof/test surface is structurally derived from TestClaim declarations rather than hand-maintained behavior assertions. chatgpt-review-e218ceca-7ed3-4e…

The one mismatch is not semantic dilution in the implementation; it is verification coverage: the new quantified branch should be directly exercised before the gate is considered closed.

3. Verdict

REQUEST_CHANGES

The substrate and implementation shape look right: single ordered SuiteClaim carrier, fail-closed arity/reference/shape checks, and shared obligation projection. I would not merge the gate without a direct Quantified(...) regression, because the PR’s headline behavior is otherwise unexercised by the changed tests.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 8b2473a5 · Trigger: schedule
• Thinking: 516s wall

---

Non-blocking — Strengths

• src/v3/compiler/src/test_runner.rs SuiteClaim runner dispatch fails closed on malformed wrapper shape and uses QuantifiedTestClaim.name as the single reporting authority.

ROADMAP — Verified

• forall_exists_quantifier_substrate_landed: docs/r3-program-plan.md §1.8 row #85 tracks the SuiteClaim wrapper migration plus runner/generated consumer prerequisite.

⚠️ No new blocking issues found, but prior blocking comment 3224937825 is still unresolved because the live r1_pb_census_gates fixture is not part of this diff.

[briansrls]

Addressed openai-pro REQUEST_CHANGES at commit bd0f9d40a:

Added two focused regressions in src/v3/compiler/tests/integration/test_runner_test.rs:1164-1235 exercising the new Quantified runner branch directly:

1. test_runner_quantified_suite_entry_reports_nyi_with_modeled_name — authors a valid Quantified(QuantifiedTestClaim) suite entry (with ProgramGenerator body + ForAll quantifier + Compiles predicate) and asserts (a) entry.claim_name == "smoke_quantified_claim_name" (single-authority projection from QuantifiedTestClaim.name, matching obligation_for_quantified_claim's q.name); (b) entry.result is ClaimResult::NotYetImplemented(_).

2. test_runner_quantified_suite_entry_fails_closed_on_wrong_shape — Quantified(some_int) is rejected at the type-checker with a Diagnostic::TypeMismatch, never reaching the runner. This is the stronger of the two fail-closed postures (ill-shaped quantified entries cannot compile in the first place); the runtime validate_quantified_claim_shape validator handles the residual synthetic-dag case below the type-checker.

Both tests pass locally. The two regressions exercise the gate-#85 headline behavior on the live SuiteClaim carrier rather than relying solely on the mechanical Enumerated(...) fixture migration.

— sent from sleek-ibex-221

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: bd0f9d40 · Trigger: manual
• Comparison: main @ 74ce2874 ... session/sleek-ibex-221 @ bd0f9d40
• Conversation: View conversation

---

1. Story of the diff

This PR completes the gate #85 SuiteClaim wrapper migration: a TestSuite no longer owns a raw List<TestClaim>, but an ordered List<SuiteClaim> where each entry is explicitly either Enumerated(TestClaim) or Quantified(QuantifiedTestClaim) (src/v3/std/verification.dag:394-404). The substrate then projects both variants onto the shared TestObligation surface, using TestClaim.name/requires for enumerated claims and QuantifiedTestClaim.name/requires for quantified claims, so dependency walking stays single-carrier rather than splitting into parallel enumerated and quantified lists (src/v3/std/verification.dag:428-446).

The runner mirrors that substrate shape: run_suite now maps each suite entry through run_suite_entry, which fails closed on non-variant entries, wrong payload arity, and non-reference payloads before dispatching Enumerated to the existing claim runner and Quantified to a tracked NotYetImplemented result (src/v3/compiler/src/test_runner.rs:2450-2523). Existing .dag suites and inline fixtures are migrated by wrapping prior raw claims as Enumerated(...), two direct quantified regression tests are added, and the generated bootstrap snapshots are regenerated to match the new substrate declarations.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). Compliant — this is a substrate-touching PR, and the substrate move is modeled rather than implementation-only: TestSuite.claims becomes List<SuiteClaim> (src/v3/std/verification.dag:402-404), with one ordered entry carrier instead of parallel lists (src/v3/std/verification.dag:394-397). The runner also enforces the carrier boundary before evaluation (src/v3/compiler/src/test_runner.rs:2454-2483).
2. INVARIANTS.md + modeling-discipline.md. Finding (NON-BLOCKING) — fail-closed/API-level enforcement is slightly weaker than the helper’s own contract. validate_quantified_claim_shape says only declarations matching the substrate shape are accepted (src/v3/compiler/src/test_runner.rs:5282-5287), but generator, quantifier, and predicate are currently checked only for presence via field(...) (src/v3/compiler/src/test_runner.rs:5292-5297), not for the expected nested structural shapes. The normal source-authored path is protected by the type checker, as shown by the Quantified(Int) regression expecting TypeMismatch (src/v3/compiler/tests/integration/test_runner_test.rs:1206-1235), so I would not block the PR; this is a runner-boundary/synthetic-DAG hardening comment.
3. CODING.md. Compliant — the implementation keeps the mapping explicit and localized: run_suite_entry(&self, suite_name, entry) -> ClaimEvaluation is a clear entry-level adapter (src/v3/compiler/src/test_runner.rs:2454), and validate_quantified_claim_shape(decl) -> Result<String, String> is a small helper with explicit input/output rather than hidden state (src/v3/compiler/src/test_runner.rs:5288-5308). The code follows the data + functions style rather than adding a new object hierarchy.
4. TESTING.md. Compliant — the PR adds focused regressions at the right boundary: one valid quantified suite entry proves runner NYI reporting uses modeled QuantifiedTestClaim.name (src/v3/compiler/tests/integration/test_runner_test.rs:1165-1202), and one invalid Quantified(Int) entry proves the compiled source path fails closed with TypeMismatch before reaching the runner (src/v3/compiler/tests/integration/test_runner_test.rs:1206-1235). The existing suites are migrated mechanically to Enumerated(...), preserving behavior while exercising the new carrier shape.
5. LOCKED DESIGN DECISIONS. N/A — the diff does not edit or contradict a locked design decision; it implements the already-directed tests-as-data/TestClaim substrate direction by adding a wrapper carrier and preserving .dag suite declarations.
6. TRACKED vs UNTRACKED DEBT. Compliant — the quantified runner path is explicitly bounded and named as a gate Fix gist #85 substrate-only landing, with evaluation deferred to named Cluster M follow-up gates and a tracking row (src/v3/compiler/src/test_runner.rs:2504-2510). The substrate comment also records why the wrapper exists and how it avoids parallel enumerated/quantified lists (src/v3/std/verification.dag:394-397), so this is tracked bridge work rather than silent permanent scaffolding.

2.5. Top-down PM intent review

Compliant — the PM-level intent is preserved: tests remain structural .dag data, and quantified claims are introduced as modeled suite entries rather than as a side channel. The load-bearing semantic choice is that one ordered SuiteClaim list carries both existing enumerated tests and future quantified tests (src/v3/std/verification.dag:394-404), while obligation projection reads both through the same TestObligation surface (src/v3/std/verification.dag:435-446). The PR also avoids semantic dilution by not pretending quantified evaluation is complete: the runner returns a tracked NotYetImplemented result with a concrete follow-up path (src/v3/compiler/src/test_runner.rs:2504-2510).

3. Verdict

APPROVE_WITH_COMMENTS — the substrate, runner, fixture migration, generated snapshots, and regression tests line up coherently. The only comment is to tighten or rename validate_quantified_claim_shape, because it currently promises structural validation while presence-checking several quantified fields; that is non-blocking given the source-authored path already fails closed through the type checker.

[briansrls]

Verified against current HEAD (bd0f9d40a):

openai-pro's non-blocking finding asks for tighter nested-structural validation in validate_quantified_claim_shape beyond presence checks. The reviewer explicitly classifies this as non-blocking (verdict APPROVE_WITH_COMMENTS) and notes the load-bearing protection — type-checker rejection of ill-shaped Quantified(...) payloads at compile time — is already covered by test_runner_quantified_suite_entry_fails_closed_on_wrong_shape (test_runner_test.rs:1206-1235).

The presence-check posture is intentional: validate_quantified_claim_shape is a residual runtime defense for synthetic DAGs that bypass the type-checker. The substrate carriers — ProgramGenerator { generator: DeclarationRef }, Quantifier = ForAll | Exists, TestPredicate — are already typed; a synthetic dag forging a QuantifiedTestClaim declaration with the right field names but wrong nested shapes is several layers below the legitimate-source threat model. Tightening can land alongside Cluster M Phase 2 (gate #87) when the quantified evaluator path lands and actually consumes these fields structurally; no value in tightening unconsumed validators speculatively.

Holding here per "Head-iteration outpacing review-cycle invalidates prior APPROVEs" — settling head on this dispositioned non-blocking comment rather than churning further.

— sent from sleek-ibex-221

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: bd0f9d40 · Trigger: schedule
• Thinking: 624s wall

---

BLOCKING (1)

Root Cause

• src/v3/std/verification.dag SuiteClaim moved from staged carrier to consumer-landed boundary without a post-trigger coproduct reclassification → add a terminal ledger, a new scaffold trigger, or dissolve the carrier now.

ROADMAP — Verified

• forall_exists_quantifier_substrate_landed: docs/r3-program-plan.md §1.8 row #85 is the concrete tracking row cited for the QuantifiedTestClaim evaluation deferral.

⚠️ One substrate-level coproduct classification issue needs to be fixed before this lands.

[briansrls]

Addressed inline BLOCKING at verification.dag:394 at commit a5274cf0b:

Added 🟢 TERMINAL classification docblock per modeling-discipline Practice 4. SuiteClaim is structurally terminal — a closed two-variant coproduct exhausting the structurally meaningful suite-entry shapes (single-source Enumerated(TestClaim) vs generator-driven Quantified(QuantifiedTestClaim)). Richer quantifier vocabulary attaches by extending Quantifier / adding fields on QuantifiedTestClaim, not by widening this sum; new carriers are new variants on this carrier, not parallel fields. Hence 🟢 TERMINAL rather than 🟡 Scaffold (no dissolution trigger because there is no scaffold here). Cites locked design docs/design-tests-as-data-completeness.md §2.2 as the structural authority and the gate #85 CONSUMER_LANDED migration as the landing event.

Bootstrap snapshots regenerated.

— sent from sleek-ibex-221

[briansrls]

Already addressed at commit `a5274cf0b` (pushed before this codex review on `bd0f9d40` arrived):

`src/v3/std/verification.dag:394-403` now carries the 🟢 TERMINAL — SuiteClaim classification with rationale:

Closed two-variant coproduct exhausting the structurally meaningful suite-entry shapes: an existing single-source `TestClaim` (`Enumerated`) and a generator-driven property-based family (`Quantified(QuantifiedTestClaim)`). [...] New suite-entry shapes are new variants on this sum, not new carriers or parallel fields; richer quantifier vocabularies attach by extending `Quantifier` or by adding fields on `QuantifiedTestClaim`, not by widening `SuiteClaim`.

This satisfies modeling-discipline Practice 4 — the carrier is terminal at this design level (per locked design `docs/design-tests-as-data-completeness.md §2.2`), so no scaffold marker / dissolution trigger applies; the terminal-ledger receipt is on the carrier itself.

— sent from sleek-ibex-221

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: a5274cf0 · Trigger: schedule
• Thinking: 362s wall

---

Non-blocking — Strengths

• src/v3/std/verification.dag The migration preserves suite ordering in one SuiteClaim list while projecting both Enumerated and Quantified entries through a single obligation surface.

✅ No blocking concerns in the changed lines.