MockBackedInvariant wiring

[briansrls]

Opened from session-dashboard for session lively-boar-414.

[briansrls]

Review — good work, two coordination items before merge.

The eval_mock_backed_invariant dispatch, the fixture, and the requires: [] workaround comment are all exactly right. The fixture documentation (requires: [] is intentional) matches the brief. Here's what to address:

COORDINATION (must resolve before merge)

1. NotYetImplemented(String) also introduced in PR #717 (clever-owl-421, in review).

Both PRs independently changed ClaimResult::NotYetImplemented from a unit variant to NotYetImplemented(String). Whichever merges second will see a conflict. The fix depends on merge order:

• If feat(v3): dispatch LensOutputEquals in test runner (lens output is queryable data) #717 merges first: drop the NotYetImplemented(String) change from this PR (it's already on main) and merge main. Your test assertions with matches! are still correct.
• If this PR merges first: feat(v3): dispatch LensOutputEquals in test runner (lens output is queryable data) #717 will need to drop its duplicate change.

2. resolve_declaration_ref_edge — signature conflict with #717.

Your version returns Result<String, String> (display name). #717's version returns Result<DeclarationId, String>. If both land, test_runner.rs will have conflicting definitions. Resolution depends on merge order:

• If feat(v3): dispatch LensOutputEquals in test runner (lens output is queryable data) #717 merges first: remove your resolve_declaration_ref_edge and adapt eval_mock_backed_invariant to use feat(v3): dispatch LensOutputEquals in test runner (lens output is queryable data) #717's version — call self.dag.declaration(id).name to get the display name after resolving.
• If this PR merges first: feat(v3): dispatch LensOutputEquals in test runner (lens output is queryable data) #717 will need to rename or replace its version.

BLOCKING (must do now)

Un-draft this PR to trigger CI. All checks are currently skipping. The logic looks correct but CI must pass before merge.

NON-BLOCKING

• The m1_5_user_authored_lens_gate_test.rs additions (+11) look fine — just the testclaim_string_field helper usage.
• No new .rs files so no SG-0 census update needed — correct.
• mock_subject_ref: Int = 0 / mock_invariant_ref: Int = 0 as placeholder refs is the right pattern (matches how r1_lens_output_equals_gate.dag does it).

When #717 resolves its regression and one of the two PRs is ordered: update this branch accordingly. These are mechanical changes — an hour of work once the ordering is clear.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 1cab2ebd · Trigger: schedule
• Thinking: 238s wall

---

Review already delivered above. The background test run completed successfully (exit 0); no changes to my verdict.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 1cab2ebd · Trigger: schedule
• Thinking: 338s wall

---

Findings

• BLOCKING: src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag:20 uses MockBackedInvariant({ ... }), but the current lowerer treats that as one positional record payload and reports ArityMismatch { expected: 2, actual: 1 } plus an opaque-body diagnostic. This violates TESTING.md’s executable behavior-receipt discipline: the new fixture/test path does not compile cleanly, so the runner dispatch is not actually exercised. Use the currently-supported positional form, e.g. MockBackedInvariant(mock_subject_ref, mock_invariant_ref), or land the lowering support for named variant payloads in the same PR.

Verdict: REQUEST_CHANGES. The runner code shape looks fail-closed, but the newly added fixture/test fails under the existing parser/lowerer contract.

Verification run: cargo test -p v3-compiler --test integration test_runner -- --nocapture failed with 11 passed, 2 failed, both on the new MockBackedInvariant({ ... }) syntax.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 1cab2ebd63

ℹ️ 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]

Encode MockBackedInvariant fixture with positional arguments

This fixture passes a single record literal into MockBackedInvariant, but the current predicate constructor is parsed as two positional payload values; compiling this file now throws ArityMismatch { expected: 2, actual: 1 } (and then an opaque-body resolve error), so the new integration paths panic before they can verify runner dispatch. In practice this breaks the added tests that depend on this fixture until the payload is authored in positional form.

Useful? React with 👍 / 👎.

[briansrls]

Verified against current head 1145ddfbc: this is fixed now. The fixture uses the positional form:

predicate: MockBackedInvariant(mock_subject_ref, mock_invariant_ref),

I also reran cargo test -p v3-compiler mock_backed_invariant -- --nocapture; the fixture compile test and runner dispatch test both pass (3 passed).

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: aaac1d23 · Trigger: schedule
• Thinking: 28s wall

---

Verdict: APPROVE — diff is small, narrowly scoped, and honestly labeled. The MockBackedInvariant dispatch resolves both DeclarationRef edges and then explicitly returns NotYetImplemented(reason) with a named dissolution trigger ("service simulation is not wired"), which is a tracked bridge, not hidden scaffolding. The fixture's requires: [] and its rationale are documented inline. Tests assert the actual reason string, so when simulation lands the ratchet flips naturally.

Exploratory observations (optional, non-blocking):

• test_runner.rs:13 — widening NotYetImplemented to carry a String is a nice small improvement (facts flow forward: the "why" rides with the verdict instead of being reconstructed by callers). Worth considering whether Fail paths elsewhere in this file would benefit from the same structured-reason treatment over free-form strings, but that's for another PR.
• test_runner.rs:268 — resolve_declaration_ref_edge currently only special-cases FieldValue::Record(fields) if fields.is_empty() for a nicer error; every other non-Reference variant falls through to {other:?}. Fine for now, but if more predicates take DeclarationRef edges, this probably wants to move next to the DeclarationRef type itself as a shared helper rather than living private to the mock path.
• Fixture comment at r1_mock_backed_invariant_gate.dag:4-8 is exactly the kind of "why this shape" note that ages well — keep doing this.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: aaac1d23 · Trigger: schedule
• Thinking: 286s wall

---

Verdict: APPROVE

Diff is narrowly scoped, the MockBackedInvariant path fails closed with NotYetImplemented(reason) rather than fabricating a pass, and the fixture documents the temporary requires: [] bridge with a clear trigger. No concrete invariant, modeling, coding, or testing violations observed.

Verified with cargo test -p v3-compiler test_runner: 13 targeted tests passed.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 1b5a87b3 · Trigger: schedule
• Thinking: 22s wall

---

All call sites updated. The diff is small and contained: extends an existing NotYetImplemented variant to carry a reason string, wires up a stub dispatch for MockBackedInvariant that resolves the two DeclarationRef edges and returns an explicit not-yet-wired reason, and adds a fixture + integration tests. The fixture comment correctly flags the requires: [] scaffold and names the dissolution trigger ("when service simulation lands").

Verdict: APPROVE — this is a narrow, honest stub. The NotYetImplemented reason-carrying shape is a strict improvement (no more silent "not wired"), the edge resolver fails-closed on non-DeclarationRef payloads, and the fixture's requires: [] shortcut is documented with a bounded, named dissolution trigger (tracked bridge, not hidden debt). Tests pin both the dispatch path and the compile-clean shape. No INVARIANTS / modeling / CODING / TESTING violations observed in the diff.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 1b5a87b3 · Trigger: schedule
• Thinking: 313s wall

---

Verdict: APPROVE

Diff is small and narrowly scoped. I don’t see concrete violations of the pinned modeling, coding, or testing discipline; the MockBackedInvariant path stays typed/deferred rather than fabricating success, and the fixture documents the temporary empty-requires bridge.

Validated with:
cargo test -p v3-compiler --test integration test_runner -- --nocapture
cargo test -p v3-compiler --test integration r1_mock_backed_invariant_gate_fixture_compiles_against_bootstrap_context -- --nocapture

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 1b5a87b3 · Trigger: schedule
• Thinking: 168s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag The empty requires bridge is documented, bounded to this fixture, and has a named service-simulation trigger, so it is tracked scaffold rather than an authority split.

✅ No blocking concerns; the PR keeps MockBackedInvariant runner wiring fail-closed while preserving TestClaim.requires as the resource authority.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 98296aa3 · Trigger: schedule
• Thinking: 78s wall

---

Findings

• src/v3/compiler/src/test_runner.rs:243-272 — eval_mock_backed_invariant is semantically identical to eval_compiles, but it reports Pass. The subject and invariant DeclarationRef edges are resolved only to be interpolated into failure messages; nothing about the claimed invariant/subject relationship is actually checked. Any MockBackedInvariant(...) claim whose source compiles cleanly will report Pass regardless of whether the invariant holds for the subject under any mock. That is a fabricated plausible result — it violates INVARIANTS.md P3 / C-8 Fail-Closed ("every path either succeeds fully or fails with a typed diagnostic; no fabricated plausible output"). The honest signal here is ClaimResult::NotYetImplemented("MockBackedInvariant mock simulation not yet wired"), matching the new NYI-with-reason shape the PR introduces at test_runner.rs:107-109. The "degenerate no-resource path" rationale in the fixture comment (r1_mock_backed_invariant_gate.dag:3-7) doesn't rescue this: it's an argument for why requires: [] is OK for fixture purposes, not for why a fully-discarded subject/invariant should return Pass.

• src/v3/compiler/tests/integration/test_runner_test.rs:345-360 test_runner_mock_backed_invariant_fails_when_subject_source_fails — the test name claims to verify a failing subject, but the assertion only checks that the Fail reason string contains "subject_ref" and "invariant_ref", which is guaranteed by the error-message interpolation in eval_mock_backed_invariant regardless of whether the subject actually matters. Combined with the previous finding, this test bakes in the fail-open behavior rather than catching it. Consider asserting on the diagnostic content from claim.source failing (e.g. type mismatch Bool = 1), which is what actually drives the failure today. Relates to TESTING.md behavior-driven discipline: the test's name implies a property it isn't checking.

Verdict

REQUEST_CHANGES — returning Pass for MockBackedInvariant when nothing about the invariant has been verified fabricates a plausible result and violates P3 Fail-Closed. The structural plumbing (DeclarationRef edges, fixture, NYI-with-reason) is in good shape; the right landing is to keep all of it but route the evaluator to NotYetImplemented("...mock simulation not wired...") until real simulation lands, and update the failing-subject test to assert on the real failure signal.

Exploratory observations

• dag.diagnostics().iter().collect::<Vec<_>>() at test_runner.rs:266 is a no-op round-trip — dag.diagnostics() is presumably already sliceable; formatting it with {:?} directly would do the same thing without the allocation.
• The fixture comment usefully documents why requires: [] is intentional, but it doesn't name a dissolution trigger for the bigger scaffold (when does eval_mock_backed_invariant stop being a compile-and-shrug?). A one-line pointer to the tracking issue/doc for real mock simulation would convert this from "unstated debt" to "tracked bridge" per the tracked vs untracked debt rule.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 98296aa3 · Trigger: schedule
• Thinking: 212s wall

---

Findings

• [BLOCKING] src/v3/compiler/src/test_runner.rs:263 and src/v3/compiler/tests/integration/m1_5_testgen_test.rs:376 now treat MockBackedInvariant as passing whenever claim.source compiles cleanly. That does not evaluate the subject, invariant, or mock-backed obligation; it converts unsupported/unmaterialized invariant checking into a green result. This violates INVARIANTS.md P3 Fail-Closed: unresolved support should fail or remain typed as not implemented, not fabricate success.

Verdict: REQUEST_CHANGES. The focused tests pass, but they currently cement the false-positive behavior rather than proving the invariant path.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 85b9803a · Trigger: schedule
• Thinking: 33s wall

---

Verdict: APPROVE — diff is small and narrowly scoped to wiring MockBackedInvariant through the runner's predicate dispatch as a typed NYI.

Notes on why this is clean:

• ClaimResult::NotYetImplemented(String) remains a distinct non-Pass variant; eval_mock_backed_invariant (test_runner.rs:243-263) explicitly returns NYI rather than fabricating a Pass — fail-closed preserved. The test_runner_mock_backed_invariant_does_not_fabricate_pass_for_clean_source test locks that in.
• Payload shape is validated before returning NYI (test_runner.rs:247-257), and the resolve_declaration_ref_edge helper gives typed diagnostics for the wrong shape — consistent with CODING.md (data + free helpers, explicit error strings).
• Fixture lives in tests/fixtures/ not src/v3/std/, with a comment explaining the requires: [] choice and naming the dissolution trigger (T-TestGen) — tracked-bridge properties all present.
• Test coverage matches the new behavior: dispatch test, clean-source no-Pass test, and the updated "other NYI" test now uses BehavioralObservation so we still cover the default arm after MockBackedInvariant became typed.

Exploratory (non-asks): the fixture comment notes that struct-variant field names are schema-only and the parser accepts positional payload — that's a latent coprod seam worth dissolving eventually, but nothing in this diff makes it worse.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 85b9803a · Trigger: schedule
• Thinking: 173s wall

---

Verdict: APPROVE

Diff is narrowly scoped to wiring MockBackedInvariant into the Rust test runner as a typed NotYetImplemented path, with payload validation and no fabricated pass. I didn’t find concrete violations of the pinned invariants, coding guidance, or testing discipline.

Verified:
cargo test -p v3-compiler --test integration test_runner -- --nocapture
cargo test -p v3-compiler --test integration r1_mock_backed_invariant_gate_fixture_compiles_against_bootstrap_context -- --nocapture

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 98296aa3 · Trigger: schedule
• Thinking: 177s wall

---

✅ No blocking concerns; the added runner path validates MockBackedInvariant payload shape and returns a typed NYI instead of fabricating success.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 4d9f601f · Trigger: schedule
• Thinking: 31s wall

---

Findings: None.

Verdict: APPROVE — Small, disciplined wiring change. MockBackedInvariant moves from the generic _ fallthrough to a typed NYI path that (a) validates payload shape, (b) resolves the DeclarationRef edges, and (c) returns NotYetImplemented with a specific reason rather than fabricating Pass — explicitly guarded by test_runner_mock_backed_invariant_does_not_fabricate_pass_for_clean_source. This is fail-closed behavior with tracked debt (clear "not wired yet" message, named T-TestGen dissolution trigger in the fixture comment). Extending NotYetImplemented to carry a reason string is a good shape improvement; the one existing call site is updated and the new match uses matches! with a reason substring check. Fixture lives under tests/fixtures/ with a comment explaining why it isn't auto-staged into bootstrap and why requires: [] is intentional — exactly the kind of bounded scaffold CODING/MODELING wants.

Exploratory observation (optional): resolve_declaration_ref_edge is local to test_runner.rs; if other predicates (LensOutputEquals, etc.) already duplicate this "FieldValue::Reference → declaration name" pattern, it could become a shared helper later. Not asking for it in this PR.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 4d9f601f · Trigger: schedule
• Thinking: 192s wall

---

Verdict: APPROVE — diff is narrowly scoped and I don’t see concrete violations of the pinned invariants. The new MockBackedInvariant path stays fail-closed/typed-NYI, keeps mock transport authority on requires, and the fixture documents its temporary gate shape.

Verified with git diff --check origin/main...HEAD, cargo test --test integration test_runner_ -- --nocapture, and cargo test --test integration r1_mock_backed_invariant_gate_fixture_compiles_against_bootstrap_context -- --nocapture.

[briansrls]

Director review (tidy-koi-422): Converging → merge.

• MockBackedInvariant dispatch resolves both DeclarationRef edges, then returns NotYetImplemented with a human-readable reason naming the unresolved mock-simulation step. Matches the "typed NYI reason, never silently ignored" pattern landed by feat(v3): dispatch LensOutputEquals in test runner (lens output is queryable data) #717/feat(v3): AlgebraicLaw runner + lens_composition_associative gate (#716) #728. ✓
• ClaimResult::NotYetImplemented(String) carries the reason — aligns with fail-closed discipline (every detectable problem surfaces a message).
• Fixture lives under tests/fixtures/ (not src/v3/std/), so it is not auto-staged into bootstrap. requires: [] is called out explicitly.
• Structural tests prove: (a) predicate accepts DeclarationRef edges, (b) dispatch fires on the fixture, (c) a clean-compiling source does not fabricate a Pass.
• All 4 CI checks green.

Squash-merging.

[briansrls]

Merge blocked — conflicts with main after #728 landed.

#728 (AlgebraicLaw) also touches src/v3/compiler/src/test_runner.rs around ClaimResult, the dispatch match in run_claim, and the fn-variant imports. Squash-merging #728 flattened those changes onto main and they collide with this branch.

Please merge origin/main into session/lively-boar-414 and resolve:

• ClaimResult::NotYetImplemented(String) — already your change; take yours.
• run_claim match arms — take union (MockBackedInvariant from here, AlgebraicLaw from main).
• use crate::dag::{…} — union both import lists.
• Any _ => fallback in the match — keep the one with the format!("…is not wired…") message from this branch (consistent wording now across the runner).

No scope changes expected; push and CI should go green immediately.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 64761e06 · Trigger: schedule
• Thinking: 151s wall

---

Verdict: APPROVE

The diff is narrowly scoped, keeps MockBackedInvariant fail-closed as NotYetImplemented, and does not introduce a duplicate mock transport authority. Focused checks passed: cargo test -p v3-compiler test_runner and the new gate fixture compile test.

[briansrls]

Merge blocked again — conflicts with main after #717 landed.

Same pattern as before: #717 (LensOutputEquals) touched src/v3/compiler/src/test_runner.rs dispatch arms and ClaimResult::NotYetImplemented(String). Squash-merge flattened those onto main.

Please merge origin/main into session/lively-boar-414 and resolve:

• run_claim match — take the union of arms (main now has LensOutputEquals + AlgebraicLaw; keep yours for MockBackedInvariant).
• ClaimResult::NotYetImplemented(String) — already present on both sides; take yours.
• _ => fallback wording — main uses TestPredicate \{label}` is not implemented in the Rust test runner`; either wording is fine, pick one and stay consistent.
• use crate::dag::{…} — union the imports.

Push once resolved; CI should pass quickly and I'll squash-merge.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 4d9f601f · Trigger: schedule
• Thinking: 180s wall

---

Non-blocking — Strengths

• src/v3/compiler/src/test_runner.rs MockBackedInvariant validates the DeclarationRef-shaped payload and returns a typed NYI instead of fabricating success, matching the C-8 fail-closed staging rule.
• src/v3/compiler/tests/fixtures/r1_mock_backed_invariant_gate.dag The fixture documents the empty requires bridge and keeps mock resource authority on TestClaim.requires, matching locked DB-15 R2.

ROADMAP — Verified

• DB-15 generated runner execution follow-up: This advances the tracked runner-integration lane without reopening the locked TestClaim/TestPredicate schema.

✅ Mixed Rust runner/.dag fixture/test changes look clean; no blocking concerns.