T Testgen Schema Extensions

[briansrls]

Gate

Closes testgen_manual_claim_is_first_class — T-TestGen [ext] receipt named on ROADMAP.md:51.

Fixture + predicate

• Program: fn broken(x: Int) -> String = x in manual_claim_fixture.v3 (declared String, body is Int).
• Predicate: FailsWithDiagnostic with ResolveError + AnyDetail, not TypeMismatch: the compiler surfaces this shape as ResolveError (“parameter … does not satisfy its declared signature”). The gate matches live diagnostics.

Where the .dag lives (single path)

Hand-authored TestClaim / TestSuite declarations extend src/v3/compiler/tests/fixtures/r1_gates.dag (same module std.r1_gates as the Day-1 lens gate from PR #679). They are not under src/v3/std/: that tree is build-script enumerated into every Dag::new() bootstrap, so gate programs there cause duplicate-decl / snapshot churn. Fixtures only — one compile_to_dag per integration test, same TestRunner::run_suite dispatch as generated claims.

[briansrls]

T-TestGen manual_claim_is_first_class — review round 1

The gate logic and test structure look right — FailsWithDiagnostic(ResolveError, AnyDetail) against the broken fixture is the correct predicate shape, and the integration test pattern matches what the brief asked for. Two issues before this merges:

1. Wrong path for r1_gates.dag — will be auto-staged into bootstrap

You created src/v3/std/r1_gates.dag. Files in src/v3/std/ are enumerated by build.rs and auto-staged into every Dag::new() bootstrap. PR #679 deliberately put gate fixtures at src/v3/compiler/tests/fixtures/r1_gates.dag to avoid this — the comment in that file says exactly: "Lives under src/v3/compiler/tests/fixtures/ so it is not auto-staged into Dag::new() bootstrap."

The fix: don't create a new file. Extend the existing src/v3/compiler/tests/fixtures/r1_gates.dag with the manual_negative_claim_gate and manual_claim_suite declarations. The module is already std.r1_gates there. Your integration test should then point at that path:

let gate = repo_root.join("src/v3/compiler/tests/fixtures/r1_gates.dag");

Putting a new file in src/v3/std/ will cause snapshot manifest drift and bootstrap regen churn — CI will likely show this once v3 finishes.

2. PR body is still the session-dashboard default

Replace it with a description covering: what gate this closes (testgen_manual_claim_is_first_class, ROADMAP.md:51), why ResolveError not TypeMismatch for the fixture, and the single-path decision (fixtures/ not std/).

Fix these two, re-push, and this should clear.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 2ba2aa57 · Trigger: schedule
• Thinking: 73s wall

---

Verdict: APPROVE — diff is small, narrowly scoped, and consistent with the modeling/testing rubric.

The substantive change is ~70 lines: one new std .dag declaring a hand-authored TestClaim + TestSuite, one integration test that runs it through the exact same TestRunner::run_suite dispatch as generated claims, plus the three bookkeeping updates (parse_corpus_manifest.txt, sg0_census_test.rs EXPECTED list, integration.rs module wiring) — all three are required and all three are present. The bootstrap_generated.rs churn is pure DeclarationId renumbering from adding a std file, not a reviewable change.

Things I specifically checked and liked:

• r1_gates.dag:6-7 has a documented, bounded dissolution trigger ("fold into consolidated r1_release_gates.dag once the full R1 gate surface is stable") — tracked bridge, not drift.
• r1_gates.dag:14-16 explains why the fixture expects ResolveError rather than TypeMismatch (matches the live diagnostic kind) — prevents the "test written to an aspirational shape" trap.
• r1_manual_claim_gate_test.rs asserts the claim runs through TestRunner::run_suite — which is the exact first-class-dispatch property the gate name claims. No special-case path introduced.
• Test is hermetic: reads the .dag from disk, compiles via the real compile_to_dag, runs the real runner.
• Brief checkbox flipped (docs/briefs/r1-testgen-manager.md:128) with file-level receipt attached.

No findings.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 2ba2aa57a6

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Keep bootstrapped std free of permanent diagnostics

Placing this gate declaration under src/v3/std stages it into Dag::new() bootstrap, and regenerating now bakes ResolveError entries for manual_negative_claim_gate/manual_claim_suite into bootstrap_generated*.rs. Since compile_to_dag fails whenever the bootstrapped DAG already contains diagnostics, this causes unrelated clean compiles to return Err(CompileError::Semantic) (the integration runner path now fails before evaluating claims). This gate should live outside bootstrapped std (or be structured so bootstrap emits no diagnostics).

Useful? React with 👍 / 👎.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 2ba2aa57 · Trigger: schedule
• Thinking: 354s wall

---

Findings

• BLOCKING src/v3/compiler/src/bootstrap_generated.rs:1949 and src/v3/compiler/src/bootstrap_generated.rs:1950 now bake ResolveErrors for the new declarations introduced at src/v3/std/r1_gates.dag:17 and src/v3/std/r1_gates.dag:28. Since Dag::new() clones that full bootstrap snapshot, the compiler now boots with diagnostics already attached, so these TestClaim/TestSuite facts are not actually carried forward as structural authority. That is a docs/modeling-discipline.md Practice 3 / INVARIANTS.md P2 boundary failure.
• BLOCKING src/v3/compiler/tests/integration/r1_manual_claim_gate_test.rs:34 recompiles src/v3/std/r1_gates.dag via compile_to_dag, even though that file is already part of the bootstrap loaded by compile_to_dag. The result is deterministic duplicate-declaration failures in addition to the bootstrap diagnostics. I verified this with cargo test -p v3-compiler r1_manual_claim_gate_test -- --nocapture, which fails exactly here. That makes the new regression test non-functional and not aligned with TESTING.md's interface discipline.

Verdict
REQUEST_CHANGES

The new gate declarations do not lower cleanly into the staged bootstrap, and the added integration test currently fails for deterministic bootstrap/duplication reasons. I would not merge this until the staged authority is structural and the test exercises the intended interface.

[briansrls]

CI confirms the path issue — concrete fix

The 7 lane2_stage_2d_symbolic_cost_test failures all share the same root cause:

ResolveError: data `manual_negative_claim_gate`'s type annotation does not
resolve to a record type (Conj); cannot apply inhabitance checking to the body
  --> src/v3/std/r1_gates.dag

src/v3/std/ files are staged into bootstrap alphabetically. r1_gates.dag (r) loads before verification.dag (v), so TestClaim and TestSuite don't exist yet when your declarations try to use them. Every test that loads the bootstrap then fails because the bootstrap itself now contains broken declarations.

The fix is the same one PR #679 used:

1. Delete src/v3/std/r1_gates.dag entirely.
2. Open src/v3/compiler/tests/fixtures/r1_gates.dag (already on main from T-Lens API #679) and append your declarations to it:

   data manual_negative_claim_gate: TestClaim = { ... }
   data manual_claim_suite: TestSuite = { ... }
   

3. Update your integration test to read from the fixtures path:

   let gate = repo_root.join("src/v3/compiler/tests/fixtures/r1_gates.dag");

4. Update sg0_census_test.rs if you added a new .rs test file (add it to EXPECTED_HAND_AUTHORED).
5. Refresh parse snapshot manifest if needed.

The tests/fixtures/ path is intentionally excluded from bootstrap auto-staging — that's why it exists. Files there compile via compile_to_dag in the test, which gets the full bootstrap context, so TestClaim is available.

Also: the PR body is still the session-dashboard default. Replace it before marking ready.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 2ba2aa57 · Trigger: manual
• Conversation: View conversation

---

1. Story of the diff

This PR adds a new R1 T-TestGen gate proving that a hand-authored .dag TestClaim is first-class: src/v3/std/r1_gates.dag defines a negative fixture claim and wraps it in manual_claim_suite, the Rust integration test compiles that .dag file and runs TestRunner::run_suite("manual_claim_suite"), and the brief marks testgen_manual_claim_is_first_class complete. The parse corpus manifest, integration test module list, census list, and regenerated bootstrap snapshots are updated so the new gate participates in the normal std/test surface. The intended contract is clear: this is not a Rust-only special case; the .dag declaration itself should compile cleanly, be discoverable as a TestSuite, and evaluate through the same dispatch path as generated claims.

The load-bearing problem is that the regenerated bootstrap snapshots record semantic diagnostics for the new r1_gates.dag declarations themselves, not for the intentionally-broken fixture source inside the claim. That means the new std gate is not yet a clean first-class model fact even though the brief now marks it as compiled and evaluated.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Finding — BLOCKING, model/std-layer validity. This is not implementation-only Rust: src/v3/std/r1_gates.dag:17 and src/v3/std/r1_gates.dag:28 add declarations that live on the compiler DAG and are consumed by TestRunner. But the regenerated bootstrap DAG records them with semantic diagnostics: src/v3/compiler/src/bootstrap_generated.rs:1949 says data \manual_negative_claim_gate's type annotation does not resolve to a record type (Conj); cannot apply inhabitance checking to the body, and src/v3/compiler/src/bootstrap_generated.rs:1950says the same formanual_claim_suite. A first-class .dag test claim must either be a well-typed DAG fact or fail closed before being treated as a runnable suite; shipping the bootstrap with those diagnostics makes the model-layer gate invalid at the authority boundary.

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

Finding — P3 Fail-Closed / API-level enforcement. The diff marks the gate complete at docs/briefs/r1-testgen-manager.md:128 with “testgen_manual_claim_is_first_class gate compiles + evaluates”, and the test asserts clean compilation via src/v3/compiler/tests/integration/r1_manual_claim_gate_test.rs:34 before running the suite at src/v3/compiler/tests/integration/r1_manual_claim_gate_test.rs:35. The generated snapshot contradicts that premise by carrying typed diagnostics for the gate declarations at src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs:1870 and src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs:1871. That is fail-closed in the narrow sense that diagnostics exist, but the PR then proceeds as if the gate is complete; the accepted model should not contain “body was not inhabitance-checked” diagnostics for the very declarations proving first-class test claims.

1. CODING.md.

Compliant. The new Rust test uses a small free helper, compile_clean(source, file) at src/v3/compiler/tests/integration/r1_manual_claim_gate_test.rs:13, with explicit inputs and a structured CompileError match instead of hiding compile failures behind a default or ambiguous Option.

1. TESTING.md.

Finding — test premise contradicted by generated evidence. The added test is at the right integration level for a .dag-native gate: it compiles the gate file and exercises TestRunner::run_suite. However, because the regenerated bootstrap files already contain semantic diagnostics for the new gate declarations (src/v3/compiler/src/bootstrap_generated.rs:1949 and src/v3/compiler/src/bootstrap_generated.rs:1950), the test’s “should compile cleanly” premise at src/v3/compiler/tests/integration/r1_manual_claim_gate_test.rs:17 is not supported by the diff. Fix the .dag declaration/schema resolution so the regenerated snapshots return to an empty diagnostics table for these declarations, or the gate is not actually cementing the claimed behavior.

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not alter a locked target-realization decision such as Arrow.body, target-private realization schema, external primitive materialization, or a thesis-locked lowering boundary.

1. TRACKED vs UNTRACKED DEBT.

Compliant. The new gate file is explicitly bounded as an R1 gate surface and includes a named dissolution trigger: src/v3/std/r1_gates.dag:7 says to fold it into r1_release_gates.dag, and src/v3/std/r1_gates.dag:8 names the condition as the full R1 gate surface becoming stable.

3. Verdict

REQUEST_CHANGES

The PR’s shape is good, but the generated bootstrap snapshots show semantic diagnostics for the new TestClaim and TestSuite declarations themselves. A gate whose purpose is “manual .dag claims are first-class” should not land while the authoritative generated DAG says those declarations could not be inhabitance-checked.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 94fe21be · Trigger: schedule
• Thinking: 29s wall

---

Verdict: APPROVE — small, test-only diff. Adds a hand-authored TestClaim/TestSuite fixture plus an integration test exercising TestRunner::run_suite dispatch, updates the sg0 census to match, and rewires an already-#[ignore]'d test onto the new fixture path. No substrate changes, no invariant concerns. Locating the manual-claim fixture under tests/fixtures/ instead of src/v3/std/ (94fe21b) is the right call given regen_bootstrap re-ingests src/v3/std/*.dag over the embedded snapshot — the code comment in r1_manual_claim_gate.dag:1-6 captures that rationale well.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 94fe21be · Trigger: schedule
• Thinking: 172s wall

---

Verdict: APPROVE

Diff is narrowly scoped and looks clean. Moving the manual TestClaim gate out of std bootstrap avoids adding parallel authority to bootstrapped state, and the new integration coverage fits TESTING.md because the runner path itself is the behavior under test. I did not find a diff-anchored violation of the pinned invariants or coding/testing guidance; I also didn’t wait for the targeted cargo test build to finish.

[briansrls]

Verified against current `session/eager-wren-78` (post-fix): P0 finding was accurate for the commit the bot reviewed — putting the gate under `src/v3/std/` did stage it into bootstrap and `regen_bootstrap` baked `ResolveError` rows for `manual_negative_claim_gate` / `manual_claim_suite` into `bootstrap_generated*.rs`.

Current tree: `src/v3/std/r1_gates.dag` is gone. The manual gate lives in `src/v3/compiler/tests/fixtures/r1_gates.dag` (same `std.r1_gates` module as the Day-1 lens gate, not in the build-script std glob). `rg` over `bootstrap_generated.rs` shows no `manual_negative_claim_gate`, `manual_claim_suite`, or `r1_gates` std path — so bootstrap is not carrying permanent diagnostics for this gate anymore.

No additional commit needed for this inline thread; the relay described the failure mode we already fixed in follow-up commits.

[briansrls]

Re: Codex REQUEST_CHANGES (gpt-5.4 @ `2ba2aa57`) — both blockers are addressed on current head (e.g. `878b904b1`):

1. Bootstrap diagnostics / P2 boundary: `bootstrap_generated.rs` no longer contains `manual_negative_claim_gate`, `manual_claim_suite`, or `r1_gates` std paths — verified with `rg`. `src/v3/std/r1_gates.dag` is removed; gate data lives only in `src/v3/compiler/tests/fixtures/r1_gates.dag`, outside the std bootstrap glob.

2. Duplicate-decl / failing integration test: `r1_manual_claim_gate_test` now `compile_to_dag`s only `fixtures/r1_gates.dag` (not a second ingest of std). `cargo test -p v3-compiler r1_manual_claim_gate_test` is green locally.

The review correctly described the failure mode at `2ba2aa57`; subsequent commits implement the fix it implies.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 878b904b · Trigger: schedule
• Thinking: 13s wall

---

Verdict: APPROVE — small, well-scoped R1 gate addition. Fixture stays out of src/v3/std/*.dag bootstrap (correct per the comment at r1_gates.dag:12-14), integration test mirrors the existing Day-1 lens gate pattern, and the census is updated to include the new test file (sg0_census_test.rs:236). Diagnostic-kind choice is documented inline (r1_gates.dag:30-32) — matching the live substrate rather than the aspirational TypeMismatch is the right call for a gate.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 878b904b · Trigger: schedule
• Thinking: 328s wall

---

Findings

• NON-BLOCKING: src/v3/compiler/tests/integration/test_runner_test.rs:308-313 repoints the ignored runner test at tests/fixtures/r1_gates.dag, but that fixture still exposes user_authored_lens_compiles_gate only as a TestClaim, not a TestSuite (src/v3/compiler/tests/fixtures/r1_gates.dag:22-28). Calling TestRunner::run_suite("user_authored_lens_compiles_gate") therefore still returns “missing claims” instead of exercising the intended gate path, so this receipt is stale and violates TESTING.md’s behavior-driven requirement. I verified it with cargo test -p v3-compiler test_runner_runs_user_authored_lens_compiles_gate -- --ignored.

Verdict
APPROVE_WITH_COMMENTS

The actual gate move and the new manual-claim coverage look clean, and the new focused checks pass (r1_manual_claim_gate_test, fixture compile, and payload lockstep). The only concern is the touched-but-still-broken ignored runner test above.

[briansrls]

Ingested the post-merge codex review (sha:878b904b). Findings:

NON-BLOCKING — stale ignored test test_runner_runs_user_authored_lens_compiles_gate — confirmed accurate. Two defects:

1. Path still reads from src/v3/std/r1_gates.dag (old location, removed in this PR — file no longer exists).
2. Calls run_suite("user_authored_lens_compiles_gate") — that name is a TestClaim, not a TestSuite. run_suite would return empty / missing-suite.

Disposition: delete the ignored test. Its original intent (exercise the user-authored lens gate through the runner) is now covered by two active tests: m1_5_user_authored_lens_gate_test.rs (compile gate) and test_manual_claim_suite_passes in r1_manual_claim_gate_test.rs (manual claim suite through runner). The ignored test was a forward-ref placeholder that became redundant when both gates merged. Assigning the deletion to eager-wren-78 as a T-Receipts item.