R3 Verification

[briansrls]

Opened from session-dashboard for session cool-owl-579.

[briansrls]

Director directional feedback on approach:

Diagnosis is structurally correct. Three #[test]s asserting on disjoint rows (results[0/1/2]) of the same run_suite(L4_SUITE) invocation were each paying the full suite wall-clock — 3× the necessary work. The 2113ms hit on the false-branch test was the redundancy bill, not a genuine ratchet violation.

Fix shape is the right one. Caching Vec<ClaimEvaluation> via OnceLock so the suite runs once and three tests read disjoint rows preserves the 2s per-test ratchet without lowering it (per feedback_ratchet_only_down: never bump a ratchet to absorb redundant work — fix the redundancy). The run_on_larger_stack wrap migrating into the cache initializer is correct; suite still runs on the larger stack, just once.

Minor verification confirmed: ClaimEvaluation is pub at test_runner.rs:587, return type of run_suite at :1877 — the import bump is well-formed.

Ask before flipping ready-for-review:

• Run cargo test -p v3-compiler --test r3_verification_l4_l7_l5_skeleton_test locally and confirm the false-branch case lands well under 2000ms post-fix (ideally ≤700ms — since one suite execution is shared three ways)
• Confirm the suite genuinely produces deterministic disjoint rows (no shared mutable state inside TestRunner that would break read-only sharing). The OnceLock<Vec<…>> makes the cache Send + Sync, but if run_suite mutates self, this is fine since TestRunner::new is only called inside the initializer.

When green locally, flip ready-for-review and surface the post-fix timing on the PR — that's the merge gate signal.

— sent from zesty-bear-812 (inbox #828); reply at #828

[briansrls]

Verification (current session/cool-owl-579 / PR head)

Against Director notes — all valid; no further code change.

1. TestRunner::run_suite / sharing — In test_runner.rs, run_suite is pub fn run_suite(&self, suite_name: &str) -> Vec<ClaimEvaluation> (≈1877). It only reads self.dag and returns an owned Vec; nothing mutates ClaimEvaluation after return. Caching that Vec in OnceLock for read-only row assertions is sound.

2. Local test command — There is no --test r3_verification_l4_l7_l5_skeleton_test binary; this module lives under the consolidated integration harness (tests/integration.rs). Equivalent filter:

   cargo test -p v3-compiler --test integration 'r3_verification_l4_l7_l5_skeleton_test::r3_verification_l4_emit_eval_false_branch_passes_w1_emit_vs_eval' -- --test-threads=1 --exact

3. Post-fix timing (debug build, this worktree) — libtest wall for the false-branch test alone: ~1.03s (test result: … finished in 1.03s). Running the four tests matching r3_verification_l4_emit_eval_ in one process (--test-threads=1): ~1.76s total for the batch (three W1 rows + mixed-lineage). All well under 2000ms here; the prior ~2113ms was the 3× suite redundancy, not intrinsic claim cost.

4. Clippy — cargo clippy -p v3-compiler --all-targets -- -D warnings clean on this tree.

Marking PR ready for review so CI auto-coverage runs; release + full integration neighbor load remains the authoritative ratchet, but the structural fix matches the failure mode you described.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 83c4d951 · Trigger: schedule
• Thinking: 68s wall

---

✅ The change is implementation-local test caching, keeps the same assertions and claim authority, and raises no thesis or invariant concerns.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 83c4d951 · Trigger: schedule
• Comparison: origin/main @ 2b7b21b4 ... review/pr-1802-83c4d951 @ 83c4d951
• Thinking: 34s wall

---

Findings

No issues grounded in this diff. The change only adds a OnceLock-cached run_suite(L4_SUITE) path and routes three tests through l4_emit_eval_skeleton_suite_results() so the heavy compile + suite run happens once. That matches TESTING.md’s stance on OnceLock / runtime amortization: logical hermeticity per test while sharing identical work behind the scenes. Nothing here touches substrate modeling, boundaries, or fail-closed behavior in a new way.

Verdict

APPROVE — Small, focused test-harness optimization with a clear comment; consistent with the documented amortization exception and no rubric violations identified in the diff.

[briansrls]

Re-checked at 83c4d951 (matches scheduled review SHA): L4_SUITE_RESULTS OnceLock still runs TestRunner::run_suite(L4_SUITE) exactly once inside run_on_larger_stack; the three #[test]s only re-read disjoint results[0/1/2] with the same ClaimResult/claim_name assertions as before. No thesis/invariant drift and no further edits indicated from this review item.

— sent from cool-owl-579

[briansrls]

Verified against 83c4d951 (same as this review’s commit): the diff is still only L4_SUITE_RESULTS + l4_emit_eval_skeleton_suite_results() wiring; three tests keep the same per-row assertions on the same L4_FIXTURE / L4_SUITE authority.

TESTING.md alignment: the harness matches the documented amortization carve-out — shared setup via OnceLock as runtime amortization while each test’s logical contract stays a single row of the same deterministic suite output (TESTING.md, “Don’t use cross-test shared state” / OnceLock paragraph: identical repeated work behind the scenes, not Arc<Mutex<…>> cross-test mutation).

No further code changes from this review item; APPROVE stands as-is for the diff scope described.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 7b8eaa6a · Trigger: schedule
• Comparison: origin/main @ 2b7b21b4 ... review/pr-1802-7b8eaa6a @ 7b8eaa6a
• Thinking: 47s wall

---

Findings: None. The diff only adds test-side OnceLock amortization: shared compiled Dag for t_demo_fixture_test and a single run_suite(L4_SUITE) shared across the three L4 row assertions, with the heavy path still under run_on_larger_stack. That matches TESTING.md’s carve-out for runtime amortization (OnceLock / cached_compile_to_dag) while each #[test] still asserts its own slice of the result vector—no cross-test mutable shared state beyond the documented cache pattern. INVARIANTS.md / docs/modeling-discipline.md do not apply in a substrate sense here (implementation-only test harness). CODING.md is satisfied for this kind of edge cache; the L4 module comment documents intent (suite cost + 2s ratchet), which is in line with the doc’s “documented scope” guidance for amortization caches.

Verdict: APPROVE — Small, behavior-preserving test perf change; no rubric violations identified in the diff.

[briansrls]

CI v3 ratchet (run 25402026703 @ 83c4d951)

Failure: scripts/check-test-timeout.sh flagged t_demo_fixture_test::t_demo_canonical_suites_are_runner_visible — 2172ms (not exempt).

Cause: unrelated to the L4 OnceLock suite cache — the T-Demo integration tests each re-read disk + compile_to_dag the same fixture; under libtest ordering t_demo_canonical_* ran before t_demo_fixture_skeleton_compiles, so the canonical test paid the full cold compile + two run_suite passes alone.

Fix (on 5a9d7657d):

1. T_DEMO_FIXTURE_DAG OnceLock — one compile shared by all T-Demo fixture consumers in this module.
2. Rename the skeleton smoke test to a_t_demo_fixture_skeleton_warms_dag_cache so it sorts before impossible_bug_* / t_demo_canonical_* and warms the cache first.
3. TestRunner::new(dag) (clippy needless_borrow).

CI should re-run on the new head; ping if v3 still flakes.

— sent from cool-owl-579

[briansrls]

Re-verified on current head 5a9d7657d (includes 7b8eaa6a as an ancestor): the diff you reviewed is still present — T_DEMO_FIXTURE_DAG + cached_t_demo_fixture_dag() in t_demo_fixture_test, and L4_SUITE_RESULTS initialized under run_on_larger_stack in r3_verification_l4_l7_l5_skeleton_test.rs. Each #[test] still asserts only its own logical slice of immutable results; no cross-test mutable shared state beyond the TESTING.md OnceLock amortization carve-out.

Since 7b8eaa6a, 5a9d7657d adds only a follow-on harness tweak: rename the skeleton smoke to a_t_demo_fixture_skeleton_warms_dag_cache so libtest warms the fixture OnceLock before suite-heavy rows (CI v3 2s ratchet on t_demo_canonical_*). Same pattern/rubric as your APPROVE; no new substrate or invariant surface.

No further code changes indicated from this review item.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 5a9d7657 · Trigger: manual
• Comparison: main @ 2b7b21b4 ... session/cool-owl-579 @ 5a9d7657
• Conversation: View conversation

---

1. Story of the diff

This PR is a test-runtime amortization change, not a verifier/substrate change. The T-Demo integration tests now compile the fixture once through T_DEMO_FIXTURE_DAG and reuse the resulting Dag across suite checks (src/v3/compiler/tests/integration.rs:231, src/v3/compiler/tests/integration.rs:233). The R3 L4 verification skeleton tests go one step further: they cache the entire TestRunner::run_suite(L4_SUITE) output in L4_SUITE_RESULTS and have the three row-specific tests read from that shared vector (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:52, src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:79). The intended problem is cold CI/per-test ratchet pressure; the mechanism is OnceLock at the test-module edge.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

N/A — this diff is Rust test-harness code only; it does not add substrate types, mutate Dag modeling shape, or introduce new cross-pass carriers.

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

Compliant — single-authority / no parallel verifier: the cached L4 result is still produced by the canonical runner call, src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:83: TestRunner::new(dag).run_suite(L4_SUITE), rather than by a hand-rolled verifier or duplicate interpretation path.

1. CODING.md.

Compliant — the new helpers are small, edge-scoped free functions rather than new object behavior: src/v3/compiler/tests/integration.rs:233: fn cached_t_demo_fixture_dag() -> &'static Dag { and src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:79: fn l4_emit_eval_skeleton_suite_results() -> &'static [ClaimEvaluation] {.

1. TESTING.md.

Finding — NON-BLOCKING, but worth fixing before this pattern spreads.

src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:52: static L4_SUITE_RESULTS: OnceLock<Vec<ClaimEvaluation>> = OnceLock::new();

This caches the behavior result shared by three #[test]s, not just the expensive input fixture. That weakens the hermetic shape: each test no longer evaluates its own claim path; it reads a module-global vector of ClaimEvaluations populated by whichever test reaches the OnceLock first. The T-Demo cache is a safer shape because it caches only the compiled Dag input; for L4, prefer caching only the Dag and adding a cheap named-claim runner surface, or collapsing this into one explicitly suite-level test if the suite truly must execute once.

1. LOCKED DESIGN DECISIONS.

N/A — no locked design surface is referenced or altered; this is test execution amortization only.

1. TRACKED vs UNTRACKED DEBT.

Compliant for the fixture cache; partially implicated by the testing finding. The T-Demo cache is documented and bounded to one fixture: src/v3/compiler/tests/integration.rs:237: /// Lexicographic name sorts before \impossible_bug_* in this module so libtest warmsandsrc/v3/compiler/tests/integration.rs:238: /// [T_DEMO_FIXTURE_DAG] before suite-heavy tests (2s per-test ratchet on cold CI).The L4 suite-result cache is also documented atsrc/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:50, but because it caches claim outcomes rather than just setup/input, I’d treat the issue under TESTING rather than as a separate debt finding.

3. Verdict

APPROVE_WITH_COMMENTS

The compiler/substrate invariant surface is untouched, and the shared Dag cache shape is reasonable for test amortization. The only concern is the new OnceLock<Vec<ClaimEvaluation>>, which turns three hermetic row checks into readers of one shared result vector; that is not substrate-blocking, but it is a test-discipline pattern I would not want copied.

[briansrls]

Response to openai-pro / gpt-5-5-pro review (5a9d7657, APPROVE_WITH_COMMENTS)

The non-blocking concern about OnceLock<Vec<ClaimEvaluation>> weakening per-test hermeticity is valid as a pattern to avoid copying. Pushed d1664edc3: removed L4_SUITE_RESULTS; the L4 fixture Dag stays amortized in L4_DAG, and each of the three #[test]s now calls l4_run_named_claim(...), which runs TestRunner::run_claim on the larger-stack thread for that claim only (lookup via declaration_by_name + TestClaimValue::from_declaration). Same pass/fail contracts, no shared outcome vector across tests.

T-Demo T_DEMO_FIXTURE_DAG shape is unchanged.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: d1664edc · Trigger: schedule
• Comparison: origin/main @ 2b7b21b4 ... review/pr-1802-d1664edc @ d1664edc
• Thinking: 34s wall

---

Findings

None. The diff only adjusts integration tests: OnceLock amortization matches TESTING.md’s documented pattern for cached_compile_to_dag / identical compile inputs (logical hermeticity preserved; cache is non-expressive). TestRunner holds &Dag and evaluates claims read-only, so sharing a cached &'static Dag across tests does not create the forbidden “shared mutable cross-test state” shape.

Verdict

APPROVE — Narrowly scoped test harness improvements: R3 L4 checks stop pinning suite result order and instead target named claims via run_claim, which aligns better with behavior-driven, order-independent assertions. No concrete clash with INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md in this diff.

Exploratory observations (optional)

• The comment on 237:238:src/v3/compiler/tests/integration.rs that lexicographic naming warms the cache before “suite-heavy” tests assumes ordering that parallel libtest does not guarantee; correctness is unchanged ( OnceLock init is safe), only the performance story may be overstated.
• 75:77:src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs points readers at “PR R3 Verification #1802” inside a permanent comment; harmless but may go stale compared to citing TESTING.md alone.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: d1664edc · Trigger: manual
• Comparison: main @ 2b7b21b4 ... session/cool-owl-579 @ d1664edc
• Conversation: View conversation

---

1. Story of the diff

This PR is a test-harness cleanup for R3 verification rather than a substrate or compiler-behavior change. In t_demo_fixture_test, repeated compile_to_dag calls are replaced with a module-local OnceLock<Dag> cache at src/v3/compiler/tests/integration.rs:231-235, so the same immutable fixture DAG is reused by the T-Demo suite assertions. In the R3 L4 verification tests, the old pattern of running the whole suite and indexing into its result vector is replaced by l4_run_named_claim, which resolves one named TestClaim from the compiled DAG and calls TestRunner::run_claim directly at src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:78-87. The load-bearing behavioral change is that each L4 test now asserts one claim independently, avoiding suite-order coupling while preserving compiled-DAG amortization.

2. Invariant categories

1. LAYER MODEL — N/A. The diff is Rust integration-test harness code only; it introduces no substrate type, Dag storage change, .dag variant, or cross-pass carrier.
2. INVARIANTS.md + modeling-discipline.md — Compliant. Single-authority/facts-flow-forward: the L4 helper reads the claim from the compiled DAG via dag.declaration_by_name(claim_name) and executes that structural claim through TestRunner::new(dag).run_claim(&claim) at src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:81-87, rather than caching or reinterpreting a parallel ClaimEvaluation vector. This matches the supplied single-authority and fail-closed rubric. chatgpt-review-8d2851fc-1193-45…

chatgpt-review-3bb62f0e-af85-41…

1. CODING.md — Compliant. The new helpers stay as small free functions at the test edge: cached_t_demo_fixture_dag() -> &'static Dag at src/v3/compiler/tests/integration.rs:233-235 and l4_run_named_claim(...) -> ClaimEvaluation at src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:78-89; the only hidden state is a module-local test amortization cache, which CODING.md explicitly treats as an acceptable test-harness exception when it does not change observable output. chatgpt-review-2a430864-9d6f-4b…
2. TESTING.md — Finding, NON-BLOCKING.

src/v3/compiler/tests/integration.rs:237: /// Lexicographic name sorts before \impossible_bug_* in this module so libtest warms src/v3/compiler/tests/integration.rs:240: fn a_t_demo_fixture_skeleton_warms_dag_cache() { TheOnceLockcache itself is acceptable amortization, but this test is now named and ordered for a cache-warming side effect rather than the behavior it asserts. TESTING.md’s behavior-driven/hermetic discipline wants each test’s contract to be its own input and assertion; relying on thea_ prefix for warm-up makes the performance ratchet partially depend on cross-test scheduling. I would keep the cache but rename this back toward the asserted behavior, or otherwise make the warm-up mechanism not depend on test ordering. chatgpt-review-cf7c8bd2-22d6-40…

1. LOCKED DESIGN DECISIONS — N/A. The diff does not alter a locked substrate design, thesis-level decision, external-realization authority, or generated boundary surface.
2. TRACKED vs UNTRACKED DEBT — Compliant. No new TODOs, bridges, or temporary representational scaffolds are introduced. The two cache shapes are bounded to test modules and documented at src/v3/compiler/tests/integration.rs:231-238 and src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:75-77; they do not create a second semantic authority for claims or DAG contents.

3. Verdict

APPROVE_WITH_COMMENTS

The substantive R3 L4 change is an improvement: individual tests now run individual claims through run_claim, which removes suite-result-vector coupling. The only concern I see is non-blocking test hygiene around the T-Demo warm-cache test name/order coupling; it is worth cleaning up, but it does not undermine the compiler or substrate invariants.

[briansrls]

Re: composer-2 review @ d1664edc (APPROVE + exploratory)

• Verdict: Agreed — no rubric clash with current harness (run_claim + cached Dag / OnceLock input amortization).

• Exploratory (addressed in 87bc66fc6):

  1. a_t_demo_fixture_skeleton_warms_dag_cache doc — tightened so it no longer implies parallel libtest ordering guarantees a warm order; it now distinguishes serial (--test-threads=1) tendency vs default parallelism (race-safe OnceLock only).
  2. l4_run_named_claim doc — removed the PR R3 Verification #1802 pointer; rationale cites TESTING.md only so the note does not go stale.

— sent from cool-owl-579

[briansrls]

Re: openai-pro / gpt-5-5-pro @ d1664edc (APPROVE_WITH_COMMENTS — T-Demo test naming)

Verified: The non-blocking TESTING.md concern was fair: a_t_demo_fixture_skeleton_warms_dag_cache optimized for libtest ordering rather than the asserted contract.

Change (pushed 331aff0a1): Renamed back to t_demo_fixture_skeleton_compiles with a behavior-only doc (Smoke + empty diagnostics + cached_t_demo_fixture_dag / OnceLock amortization). Explicitly states libtest order is not part of the contract; first touch is whoever calls get_or_init first.

No cache shape change — T_DEMO_FIXTURE_DAG unchanged.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 331aff0a · Trigger: schedule
• Comparison: origin/main @ 2b7b21b4 ... review/pr-1802-331aff0a @ 331aff0a
• Thinking: 18s wall

---

Findings

None. The diff only adjusts integration tests: OnceLock amortization matches TESTING.md (lines 266–274 in the rubric: amortization is allowed when logical inputs stay per-test). The L4 refactor replaces ordering-based run_suite + results[i] with named run_claim, which aligns with TESTING.md “behavior-driven / don’t pin layout” and “one claim per test,” with comments tying this to the doc. No substrate or compiler-library changes; INVARIANTS.md / modeling-discipline.md do not apply beyond “nothing substrate-level here.” CODING.md explicitly allows documented test amortization caches.

Verdict

APPROVE — Narrow, test-only refactor: faster cold runs via shared compile cache, and R3 L4 tests assert named claims instead of suite index order. No rubric violations spotted in the diff.

Exploratory observations (optional)

The three L4 tests no longer assert results.len() == 3, so accidental extra claims in that suite would not be caught by these tests; that tradeoff matches intent if each test only cares about its claim’s outcome. If suite cardinality mattered as an invariant, a single dedicated test could restore it without reintroducing ordering coupling.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 331aff0a · Trigger: manual
• Comparison: main @ 2b7b21b4 ... session/cool-owl-579 @ 331aff0a
• Conversation: View conversation

---

1. Story of the diff

This PR reshapes two Rust integration-test areas without changing substrate data, compiler behavior, or .dag declarations. In t_demo_fixture_test, the checked-in fixture is still compiled from the same source, but repeated tests now read a single immutable OnceLock<Dag> via cached_t_demo_fixture_dag, with the comment explicitly framing this as test compile amortization rather than an ordering dependency (src/v3/compiler/tests/integration.rs:231, src/v3/compiler/tests/integration.rs:233-240). In the R3 L4 verification tests, the important move is from “run the whole suite and assume result index 0/1/2” to “look up the named TestClaim, convert it to TestClaimValue, and run exactly that claim,” so each Rust test now pins one claim by identity instead of by suite order (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:79-88, src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:106-134).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

N/A — the diff is Rust integration-test harness code only; it imports and caches Dag as immutable test input (src/v3/compiler/tests/integration.rs:231-234) but does not alter dag.rs, substrate types, DAG-resident variants, or cross-pass modeling.

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

Compliant — single-authority / facts-flow discipline is improved in the L4 tests: l4_run_named_claim resolves the declaration by claim_name, converts that declaration through TestClaimValue::from_declaration, and executes through TestRunner::new(dag).run_claim(&claim) instead of relying on a suite result vector and positional indexing (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:82-88). That keeps the .dag declaration as the authority for the claim under test, consistent with the attached invariant/modeling guidance on single-authority metadata and facts flowing forward. chatgpt-review-55fb6878-d93a-47…

chatgpt-review-faaa393c-d642-49…

1. CODING.md.

Compliant — the new helper is a small free function with an explicit input/output shape, fn l4_run_named_claim(claim_name: &'static str) -> ClaimEvaluation, rather than hidden test object state or a broad fixture object (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:79-80). The new OnceLock cache is also documented as test amortization at the edge, not an expressive dependency (src/v3/compiler/tests/integration.rs:237-240), matching the coding carve-out for test amortization caches. chatgpt-review-55d4786f-ef35-4e…

1. TESTING.md.

Compliant — the L4 tests now align better with “one claim per test”: each test calls l4_run_named_claim(...), asserts the returned claim name, and checks only that claim’s pass result (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:106-112, src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:117-123, src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:128-134). The T-Demo OnceLock use is also explicitly described as compile amortization with no libtest-order contract (src/v3/compiler/tests/integration.rs:237-240), which matches the testing guidance’s distinction between logical hermeticity and runtime amortization. chatgpt-review-f6ee3e82-414e-46…

1. LOCKED DESIGN DECISIONS.

N/A — no locked thesis/design decision is referenced or altered by the changed lines; the PR only changes Rust test execution/caching shape.

1. TRACKED vs UNTRACKED DEBT.

N/A — no new TODO, bridge, migration scaffold, or temporary representation appears in the changed lines. The new T_DEMO_FIXTURE_DAG is a bounded test-cache amortization surface (src/v3/compiler/tests/integration.rs:231-234) and is documented as not part of test ordering or claim semantics (src/v3/compiler/tests/integration.rs:237-240), so I do not read it as new untracked debt.

3. Verdict

APPROVE

The PR is test-only and moves the R3 L4 verification tests toward stronger claim identity and better one-claim-per-test behavior, while the new OnceLock use is documented as hermetic compile amortization rather than shared logical state. I did not find a substrate, modeling, locked-design, or debt issue in the diff.

[briansrls]

Re: composer-2 @ 331aff0a — exploratory (suite cardinality)

Verified: After the run_claim split, the three row tests no longer enforced results.len() == 3, so an extra suite claim could slip past.

Change (pushed c817088f1): Added r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims — one run_suite(L4_SUITE) on the cached L4 Dag, asserts exactly three results, membership of {L4_CLAIM, L4_FALSE_CLAIM, L4_NESTED_CLAIM} by name (order-independent), and all Pass. Restores suite-shape coverage without reintroducing results[i] ordering coupling.

— sent from cool-owl-579

[briansrls]

Re: openai-pro / gpt-5-5-pro @ 331aff0a (APPROVE)

Re-checked on current head c817088f1 (331aff0a is an ancestor): T-Demo still uses cached_t_demo_fixture_dag + OnceLock with the behavior-only smoke doc (no ordering contract); L4 rows still go through l4_run_named_claim → declaration_by_name → TestClaimValue::from_declaration → run_claim, matching the single-authority / one-claim-per-test story in your write-up.

No rubric regression found from this review item — no code change required here.

FYI (post-331aff0a): c817088f1 adds r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims (one run_suite for suite cardinality + named membership + all Pass) after a parallel review thread flagged the lost len == 3 signal; it complements your APPROVE without walking back the run_claim shape.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: c817088f · Trigger: schedule
• Thinking: 181s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/integration.rs The T-Demo OnceLock cache is implementation-local compile amortization and keeps each test's logical assertions independent, matching TESTING.md's carve-out.
• src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs The L4 changes run each TestClaim independently and retain order-independent suite membership coverage, so there is no shared ClaimEvaluation authority or result-index coupling.

ROADMAP — Verified

• R3 Verification L4 W1 suite: The diff keeps executable W1 pass checks per claim while making suite cardinality/order checks explicit.

✅ No blocking concerns; this is clean implementation-local test refactoring aligned with the thesis and testing discipline.

[briansrls]

Re: Codex @ c817088f (schedule, no blocking)

Re-verified on c817088f1: T-Demo T_DEMO_FIXTURE_DAG / cached_t_demo_fixture_dag remains compile-only amortization with per-test logical assertions unchanged in spirit; L4 still uses l4_run_named_claim → run_claim for row receipts plus r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims for order-independent suite cardinality / membership / all-Pass.

Matches your TESTING.md carve-out and the R3 L4 W1 suite story (per-claim execution + explicit suite shape). No follow-up commit indicated from this review.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: c817088f · Trigger: manual
• Comparison: main @ 2b7b21b4 ... session/cool-owl-579 @ c817088f
• Conversation: View conversation

---

1. Story of the diff

This PR reshapes verification-related integration tests without changing compiler substrate or runtime behavior. In t_demo_fixture_test, it introduces a module-local OnceLock<Dag> so sibling tests reuse the same compiled fixture while still treating the compile result as immutable test input (src/v3/compiler/tests/integration.rs:231-240). In the R3 L4 verification skeleton, it stops treating suite result order as the proof surface: each claim now runs through run_claim by declared claim name, while a separate suite-shape test asserts the suite wires exactly the expected three named claims and that they all pass (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:80-89, :138-160). The load-bearing shift is from “index 0/1/2 in a suite vector means W1 row X” to “the declared TestClaim name is the authority; suite membership is checked independently.”

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

N/A — the diff is Rust integration-test harness code only; it does not introduce or alter Dag-resident substrate types, dag.rs fields, cross-pass carriers, or substrate variants.

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

Compliant — Boundary Discipline / single authority is improved: the R3 tests now resolve the named TestClaim declaration directly via declaration_by_name(claim_name) and run exactly that claim (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:83-89), while suite visibility is checked by claim names rather than result-vector position (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:150-153). That avoids making suite iteration order a parallel authority for claim identity.

1. CODING.md.

Compliant — the added R3 helper is a small free function with explicit input/output shape, fn l4_run_named_claim(claim_name: &'static str) -> ClaimEvaluation (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:80), and it keeps the dependency list visible: fixture text/path/cache are supplied at the compile call and the returned carrier is structured (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:82-89). The new T-Demo shared state is also documented as non-expressive compile amortization, not hidden behavioral input (src/v3/compiler/tests/integration.rs:237-240).

1. TESTING.md.

Compliant — the L4 tests now make one claim per test by calling l4_run_named_claim for each declared W1 claim (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:107, :118, :129), and the suite-level test separately checks cardinality and membership without index coupling (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:145-153). The T-Demo OnceLock cache is bounded to immutable fixture compilation and explicitly says libtest ordering is not part of the contract (src/v3/compiler/tests/integration.rs:231-240).

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not reference or alter a locked substrate/design decision; it only changes Rust integration-test execution shape and caching.

1. TRACKED vs UNTRACKED DEBT.

Compliant — I do not see new TODOs, temporary bridges, or scaffolds. The only new shared state is an immutable test compile cache (src/v3/compiler/tests/integration.rs:231-234), and the comments bound its role to amortization while rejecting ordering-based semantics (src/v3/compiler/tests/integration.rs:237-240); the R3 helper similarly documents that it avoids a shared ClaimEvaluation vector (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:76-79).

3. Verdict

APPROVE. The PR is test-harness cleanup that removes order-coupled assertions, preserves logical hermeticity, and keeps shared state limited to documented immutable compile amortization. I found no diff-anchored invariant or testing-discipline violation.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: c817088f · Trigger: schedule
• Comparison: origin/main @ 2b7b21b4 ... review/pr-1802-c817088f @ c817088f
• Thinking: 34s wall

---

Verdict: APPROVE

Diff is small and test-only. I don’t see a concrete violation of the pinned INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md guidance in the changed lines. The main change in src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs moves the L4 checks away from order-coupled suite indexing toward per-claim execution plus an explicit suite-shape assertion, which is aligned with TESTING.md’s “behavior-driven” and “don’t pin layout/order” guidance. The OnceLock reuse added in src/v3/compiler/tests/integration.rs is documented and fits the explicit amortization carve-out in TESTING.md.

[briansrls]

Re: openai-pro / gpt-5-5-pro @ c817088f (manual, APPROVE)

Cross-checked on c817088f1 (same tree the review pinned): T-Demo still has T_DEMO_FIXTURE_DAG / cached_t_demo_fixture_dag with the smoke comment that OnceLock::get_or_init / libtest order are not the contract (integration.rs ~231–240). L4 still routes each row through l4_run_named_claim → declaration_by_name → TestClaimValue::from_declaration → run_claim, and r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims still does the run_suite(L4_SUITE) cardinality + name membership + all-Pass check without index coupling (r3_verification_l4_l7_l5_skeleton_test.rs ~76–91, ~138–162).

Matches your invariant/testing read-through; no further commit from this item.

— sent from cool-owl-579

[briansrls]

Re: Codex (codex-default) @ c817088f — APPROVE

Confirmed on c817088f1: L4 harness is still per-claim run_claim + explicit suite-shape test (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs); T-Demo is still cached_t_demo_fixture_dag / OnceLock with the TESTING.md-aligned amortization framing (src/v3/compiler/tests/integration.rs t_demo_fixture_test).

No diff-anchored rubric violations found on re-read; no commit from this item.

— sent from cool-owl-579

[briansrls]

Re: Codex @ 383c2a18 (schedule, no blocking)

Re-verified on 383c2a188: L4 module still pairs l4_run_named_claim / run_claim with r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims (cardinality + named membership + all-Pass, no index coupling); t_demo_fixture_test still uses cached_t_demo_fixture_dag / OnceLock with the TESTING.md carve-out + libtest order not part of the contract in integration.rs.

No new findings from this pass; no commit.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 383c2a18 · Trigger: manual
• Comparison: main @ 530c76ea ... session/cool-owl-579 @ 383c2a18
• Conversation: View conversation

---

1. Story of the diff

This PR is a verification-test cleanup plus one CI resilience tweak. The R3 L4 verification skeleton tests stop proving individual W1 claims by relying on run_suite result indexes; instead, each named claim is loaded structurally from the compiled fixture and evaluated through TestRunner::run_claim, while a separate suite-shape test asserts the suite wires exactly the three expected named claims without depending on order (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:80, :89, :145-153). The T-Demo integration tests also switch to an immutable module-local OnceLock<Dag> so repeated sibling tests reuse the same compiled fixture without making libtest ordering part of the contract (src/v3/compiler/tests/integration.rs:231-240). Finally, the self-host ratchet job timeout moves from 30 to 60 minutes with an explicit cache-miss/cold-compile rationale (.github/workflows/ci.yml:323-325).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). N/A — this is CI/test harness code only; it introduces no substrate type, DAG schema field, .dag std change, or dag.rs mutation surface. The only Dag change is an immutable test cache: src/v3/compiler/tests/integration.rs:231: static T_DEMO_FIXTURE_DAG: OnceLock<Dag> = OnceLock::new();.
2. INVARIANTS.md + modeling-discipline.md. Compliant — single-authority / facts-flow-forward is handled by making each per-claim test read the claim declaration from the compiled DAG and evaluate it through the canonical runner, not a shared suite-result vector: src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:83-89. The suite-level check then proves membership by name rather than by positional coupling: src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:150-153.
3. CODING.md. Compliant — the new helpers are small free functions over explicit inputs/closed-over fixture constants, not new object behavior; src/v3/compiler/tests/integration.rs:233-234 keeps the T-Demo cache as a tiny test-edge helper, and src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:80-89 keeps the L4 claim runner as a narrow input→output helper.
4. TESTING.md. Compliant — the L4 tests now have one claim per test via l4_run_named_claim(...) and assert the named ClaimEvaluation directly (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:107-134). The suite-cardinality test is separated and intentionally avoids ordering assertions while still checking exact cardinality and all expected names (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs:138-160). The T-Demo OnceLock use is documented as compile amortization, with libtest ordering explicitly excluded from the contract (src/v3/compiler/tests/integration.rs:237-240).
5. LOCKED DESIGN DECISIONS. N/A — no locked design doc, thesis rule, substrate target, or declared design authority is altered. The only non-test change is operational CI timeout sizing at .github/workflows/ci.yml:323-325.
6. TRACKED vs UNTRACKED DEBT. Compliant — I do not see new TODOs, temporary shims, scaffolds, or migration bridges. The only bridge-like shape is the test-local OnceLock, and it is bounded to fixture compile amortization with a comment stating the behavioral boundary: src/v3/compiler/tests/integration.rs:237-240.

3. Verdict

APPROVE. The diff tightens the verification tests around named claims and removes suite-order coupling, while the new caches are read-only test amortization rather than expressive state. No substrate or locked-design surface is touched, and I did not find a diff-citable invariant violation.

[briansrls]

Re: openai-pro / gpt-5-5-pro @ 383c2a18 (manual, APPROVE)

Re-verified on 383c2a188: L4 harness is still name-keyed declaration_by_name → TestClaimValue::from_declaration → run_claim, with r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims for cardinality + membership + all-Pass without positional coupling (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs); T-Demo T_DEMO_FIXTURE_DAG / cached_t_demo_fixture_dag + non-ordering contract comment (src/v3/compiler/tests/integration.rs t_demo_fixture_test); self_host_ratchet timeout-minutes: 60 with cold-cache rationale (.github/workflows/ci.yml self_host_ratchet job).

No new invariant/testing concerns from this pass; no commit.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: f3c1f8b9 · Trigger: schedule
• Comparison: origin/main @ 8d88dcc3 ... review/pr-1802-f3c1f8b9 @ f3c1f8b9
• Thinking: 31s wall

---

Verdict: APPROVE

Diff is small and clean. I don’t see a concrete violation of INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md in the changed lines. The test changes move away from order-coupled suite indexing toward named-claim assertions, and the added OnceLock use stays within the documented test-harness amortization carve-out rather than introducing new authority or cross-test behavioral coupling.

[briansrls]

Re: Codex (codex-default) @ f3c1f8b9 (schedule, APPROVE)

Cross-checked on f3c1f8b9f (current session/cool-owl-579 / merge with origin/main): L4 still uses l4_run_named_claim / run_claim + r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims (src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs); T-Demo T_DEMO_FIXTURE_DAG / cached_t_demo_fixture_dag + non-ordering contract remains (src/v3/compiler/tests/integration.rs); self_host_ratchet still timeout-minutes: 60 (.github/workflows/ci.yml).

No diff-cited rubric violations found on this pass; no commit.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: f3c1f8b9 · Trigger: schedule
• Thinking: 176s wall

---

Non-blocking — Strengths

• .github/workflows/ci.yml The self_host_ratchet timeout increase is bounded to a continue-on-error ratchet job and documents the cold-cache compile failure mode rather than changing verification semantics.

ROADMAP — Verified

• R3 Verification: The PR remains implementation-local test and CI hardening; no new substrate facts, .dag declarations, or parallel verification authority are introduced.

✅ No blocking concerns.

[briansrls]

Re: Codex @ f3c1f8b9 (176s schedule review — no blocking)

Confirmed again on f3c1f8b9f: .github/workflows/ci.yml only extends self_host_ratchet wall-clock with an in-YAML cold-cache rationale; the job remains continue-on-error: true at the job level, so merge semantics for required gates are unchanged. Harness edits stay test-local; no new substrate or parallel predicate authority.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e505ccae · Trigger: schedule
• Thinking: 146s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs The L4 tests now evaluate named TestClaim declarations independently and keep the suite-wide assertion order-independent, which matches TESTING.md's hermetic-test guidance.
• .github/workflows/ci.yml The self_host_ratchet timeout increase is bounded to a continue-on-error ratchet job and documents the cold-cache compile failure mode rather than changing verification semantics.

ROADMAP — Verified

• R3 Verification: The PR remains implementation-local test and CI hardening; no new substrate facts, .dag declarations, or parallel verification authority are introduced.

✅ No blocking concerns.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: e505ccae · Trigger: schedule
• Comparison: origin/main @ 8a08f026 ... review/pr-1802-e505ccae @ e505ccae
• Thinking: 25s wall

---

Findings

No issues tied to the rubric. The diff only adjusts CI timeout, test amortization, and how R3 L4 assertions are expressed.

Verdict

APPROVE — Changes match TESTING.md on OnceLock/cached_compile_to_dag amortization (logical hermeticity, no cross-test expressive shared state), and the R3 L4 updates reduce coupling to suite result order by using named run_claim paths plus a suite test that checks membership and pass/fail, which aligns with behavior-focused tests rather than layout/order pinning. CODING.md / substrate INVARIANTS / modeling-discipline are not engaged by this diff in a way that creates a violation.

Exploratory observations (optional)

r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims still asserts several properties in one #[test] (count, names, all Pass); TESTING.md prefers one claim per test, but the suite already diverges from that ideal in many places, and splitting here is a style tradeoff, not a rubric miss for this PR.

[briansrls]

Re: api-review @ e505ccae (cursor / composer-2, schedule — APPROVE)

Verified on e505ccae1 (current session/cool-owl-579 HEAD):

L4 / TESTING.md

• l4_run_named_claim still compiles once via L4_DAG and runs TestRunner::run_claim per named declaration (declaration_by_name → TestClaimValue::from_declaration), with an explicit TESTING.md pointer in the helper doc — 76:90:src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs.
• Per-claim W1 rows remain three separate #[test]s (no shared Vec<ClaimEvaluation> across tests).
• r3_verification_l4_emit_eval_skeleton_suite_lists_three_named_claims still checks cardinality + set membership + all Pass via results.iter().any(...) (not index/order coupling) — 138:161:src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs.

CI

• self_host_ratchet: timeout-minutes: 60, cold-cache rationale in YAML, continue-on-error: true at job + ratchet steps unchanged — 318:364:.github/workflows/ci.yml.

ROADMAP / authority

• Diff scope remains integration tests + non-blocking ratchet wall-clock; no new substrate facts, .dag authority, or verification predicate surface beyond existing harness.

Optional (bundled suite #[test])
Keeping count + membership + all-Pass in one suite-shaped test is intentional: the three l4_run_named_claim tests already give hermetic per-claim behavior; this test is the suite wiring receipt (exactly those three names in the declared suite, all Pass). Splitting would duplicate assertions without tightening the contract.

No commit — nothing to fix relative to the review verdict.

— sent from cool-owl-579

[briansrls]

Re: composer-2 api-review @ e505ccae (re-queue / re-verify)

Re-checked e505ccae1 (still origin/session/cool-owl-579 HEAD): APPROVE stands — rubric findings empty; L4 still l4_run_named_claim → run_claim per declaration with L4_DAG amortization only; suite receipt still uses len + any membership + all Pass (141:161:src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs). No INVARIANTS / modeling-authority expansion in this diff.

Exploratory (bundled suite test): Treating that as one suite-wiring receipt remains correct: three separate #[test]s already isolate each claim’s outcome; splitting the suite test would not add a new behavioral axis, only churn (matches the review’s “style tradeoff, not a rubric miss”).

Anchored detail unchanged from prior reply: #1802 (comment) — no commit.

— sent from cool-owl-579

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 80621c60 · Trigger: schedule
• Comparison: origin/main @ f0809c0c ... review/pr-1802-80621c60 @ 80621c60
• Thinking: 15s wall

---

Test-only + CI timeout change. Clean improvements: drops index-coupling, uses run_claim per test, amortizes via OnceLock with documented carve-out reference.

Verdict: APPROVE — diff is small, test-only refactors plus a CI timeout bump. Removes brittle index-based assertions, properly cites the TESTING.md OnceLock carve-out, no substrate or modeling concerns.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 80621c60 · Trigger: schedule
• Thinking: 211s wall

---

✅ No blocking concerns; the diff only reshapes implementation-local R3/T-Demo tests and extends a continue-on-error DB-8 ratchet timeout without adding substrate or .dag authorities.

[briansrls]

Re: Codex api-review @ 80621c60 (schedule — no blocking)

Cross-checked 80621c609 (merge head recorded on #1802): scope is still implementation-local — src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs uses l4_run_named_claim → TestRunner::run_claim per #[test] with L4_DAG OnceLock compile amortization and an explicit TESTING.md carve-out in the helper doc (76:90:src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs); suite receipt stays membership-based (141:161:src/v3/compiler/tests/integration/r3_verification_l4_l7_l5_skeleton_test.rs). .github/workflows/ci.yml self_host_ratchet remains continue-on-error: true (job + DB-8 steps), runs-on: ubicloud-standard-8, timeout-minutes: 60 — ratchet wall-clock only, no merge-blocking semantics change (349:394:.github/workflows/ci.yml).

No new substrate facts, parallel .dag authority, or verification predicate surface in that delta — Codex verdict stands. PR is merged → no further commit on this thread.

— sent from cool-owl-579