Skip to content

feat(v3): dispatch LensOutputEquals in test runner (lens output is queryable data) - #717

Merged
briansrls merged 41 commits into
mainfrom
session/clever-owl-421
Apr 24, 2026
Merged

briansrls merged 41 commits into
mainfrom
session/clever-owl-421

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Summary

Post-#679 follow-on for Brief 3 (T-LensAPI / lens_output_is_queryable_data): wire LensOutputEquals in the Rust test_runner so the predicate is never silently ignored.

Changes

  • test_runner: run_claim dispatches LensOutputEquals to eval_lens_output_equals, which parses the three DeclarationRef payload slots as FieldValue::Reference, looks up declarations on the suite DAG, requires value_body on input/expected, compile_to_dag on TestClaim.source, then returns NotYetImplemented with an explicit message until lens application + structural comparison exist.
  • ClaimResult::NotYetImplemented(String): all NYI paths (including unknown predicate labels) carry a human-readable reason.
  • Fixtures / tests: r1_lens_output_equals_gate.dag holds a minimal LensOutputEquals(Int, …) gate + suite; r1_gates.dag remains the user_authored_lens_compiles Compiles witness. Integration tests cover dispatch + fixture compile; harness test documents that LensOutputEquals(Int, Int, Int) lowers like MockBackedInvariant(Int, Bool).

Known limits (explicit)

  • lens_ref cannot yet be the real named_function_count fn in this snapshot: inference hits a DeclarationRef vs Int template conflict for callable refs in that slot.
  • LensOutputEquals(..., Int, …) in the same translation unit as the huge embedded user_authored_lens_compiles source string broke Int resolution; the dedicated r1_lens_output_equals_gate.dag avoids that.

Test plan

  • cargo test -p v3-compiler test_runner_test::
  • cargo test -p v3-compiler user_authored_lens
  • cargo test -p v3-compiler r1_lens_output_equals_gate_fixture

Made with Cursor

Move r1_gates.dag to the tail of STAGED_FILES generation so load order
stays a single build.rs authority; drop the bootstrap.rs filter +
include_str! replay. Document why OnceLock is shared across two tests.
Regenerate bootstrap snapshots.

Made-with: Cursor
- Add LENS_BOOTSTRAP_FILES from src/v3/lenses/bootstrap/*.dag (pure FS + build.rs)
- Remove named_function_count include_str!/chain from bootstrap.rs
- Move Day-1 user lens to lenses/bootstrap/; widen emit filter to that prefix
- Integration test compiles using source/file_name from staged TestClaim data
- Regenerate bootstrap snapshots

Made-with: Cursor
- Embed full named_function_count program in r1_gates TestClaim.source so
  compile_to_dag(payload) succeeds without bootstrap-bundling the lens
- Integration test reads source/file_name from lowered gate; asserts bytes
  match include_str!(named_function_count.dag) then compiles that payload
- Use ASCII hyphen in lens header comment (avoids UTF-8 mojibake in .dag string)

Made-with: Cursor
- Regenerate parse_corpus_manifest.txt after rust/go/python spec edits
- Whitelist m1_5_user_authored_lens_gate_test.rs in EXPECTED_HAND_AUTHORED

Made-with: Cursor
Clarify that TestClaim.source is the full lens module and the integration test
compile_to_dag's the extracted payload (addresses REQUEST_CHANGES on stale 8237192).

Made-with: Cursor
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

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

Findings

Nothing that rises to a violation. A couple of observations worth airing:

  • eval_lens_output_equals compiles claim.source on every dispatch (src/v3/compiler/src/test_runner.rs:256-261). The comment says "needed for future lens application," but right now it's a side-effectful redundant compile whose only visible effect is upgrading a ref-shape receipt to a "source compiles too" receipt before returning NotYetImplemented. Not a principle violation — ClaimResult is implementation-layer — but when the real lens-application path lands, this scaffolding should be replaced rather than layered onto, or the responsibility split (runner evaluates; it shouldn't be invoking the compiler on the claim's source as a side-check). Fine for the tracked bridge.

  • Fixture split with a compiler-bug rationale (src/v3/compiler/tests/fixtures/r1_lens_output_equals_gate.dag:1-5). The header documents that LensOutputEquals(Int, …) plus the large embedded source string in the same TU currently breaks DeclarationRef resolution for Int. That's an acknowledged compiler bug papered over by splitting fixtures. The dissolution trigger is named (fix resolver, recombine fixtures), so this is a tracked bridge — but it should earn a TODO/issue reference so the split doesn't ossify.

  • assert_all_pass import is now dead in test_runner_test.rs after removing the ignored gate test — worth checking it isn't producing an unused-import warning (didn't verify in the worktree).

Verdict

APPROVE_WITH_COMMENTS — the change is honest: it's a dispatch stub that resolves the three DeclarationRef edges, validates shape, and returns NotYetImplemented(msg) with a clear message that tests pin. The NotYetImplemented(String) upgrade is a reasonable implementation-layer refinement. Fixture split and redundant compile call are both tracked bridges, not modeling violations.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review — BLOCKING before merge: branch predates #679 and needs a clean main merge.

The runner work itself (eval_lens_output_equals, NotYetImplemented(String), resolve_declaration_ref_edge) is correct and exactly what Brief 3 asked for. The design decisions are sound. But the diff has several structural problems caused by the branch being cut before #679 (and #707) merged.

Blocking issues

1. r1_gates.dag shows as a new file — it already exists on main with more content.

The diff adds r1_gates.dag from /dev/null, but on main (from PRs #679 and #707) the file has three declarations:

Your version only has user_authored_lens_compiles_gate. If this merges as-is, it silently drops the testgen_manual_claim_is_first_class gate that #707 landed — a regression.

2. src/v3/lenses/named_function_count.dag shows as a new file — it already exists on main.

This file was added in #679. Your diff adds it again from /dev/null with the same content. When merged, git will either succeed (identical content) or conflict. Either way, the file should not appear in your diff — it's already on main.

3. sg0_census_test.rs adds m1_5_user_authored_lens_gate_test.rs — already present from #679.

On main, this entry exists. Your +1 in the census will either be a no-op (if already added) or create a duplicate entry.

4. Spec file formatting (rust.dag, go.dag, python.dag) — unrelated noise.

The diff reformats excluded_prefixes arrays to multiline. These are cosmetic changes that weren't part of Brief 3. They inflate the diff and make review harder.

Root cause

The branch was cut before #679 merged. You merged origin/main at some point but either the merge committed the wrong resolutions (taking your HEAD over theirs) or the merge wasn't completed before you pushed.

How to fix

Already up to date.

Resolve conflicts carefully:

  • r1_gates.dag: keep ALL content from both sides — your version plus main's manual_negative_claim_gate/manual_claim_suite additions. Also adopt the import std.verification { TestClaim, TestSuite } import line from main (not just TestClaim).
  • named_function_count.dag: take main's version (same content — no conflict).
  • sg0_census_test.rs: take main's version if the entry is already there; don't duplicate.
  • spec files: revert your formatting changes — take main's version.

After merge: run cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored to update the parse corpus manifest if needed.

One additional issue

r1_lens_output_equals_gate.dag has no module declaration and no imports. The file uses TestClaim and TestSuite without importing them. If this works because compile_to_dag resolves against the bootstrap context, add a comment explaining that. If it needs explicit imports to compile standalone, add them. Verify with cargo test -p v3-compiler r1_lens_output_equals_gate_fixture_compiles after merging main.

What does NOT need to change

  • test_runner.rs — eval_lens_output_equals, NotYetImplemented(String), resolve_declaration_ref_edge are all correct.
  • test_runner_test.rs — the new tests look right.
  • m1_5_user_authored_lens_gate_test.rs — the new fixture compile test is correct.
  • r1_lens_output_equals_gate.dag — correct fixture, just verify the imports.

Merge main, resolve the fixture conflicts, revert spec formatting noise, then re-push. The actual deliverable is ready; it just needs a clean tree.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / gpt-5.4
  • Commit: e77c2609 · Trigger: schedule
  • Thinking: 274s wall

Findings

  • [NON-BLOCKING] src/v3/compiler/tests/fixtures/r1_gates.dag:19 plus src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs:101 introduce and then ratchet a second copy of the named_function_count program text instead of a single authority. That is the parallel-representation shape INVARIANTS.md P2 / docs/modeling-discipline.md practice 5 warns against; if this Day-1 bridge is unavoidable, it still needs an explicit dissolution trigger rather than “update both together.”

Verdict
APPROVE_WITH_COMMENTS

The runner-side LensOutputEquals work looks honest about still being scaffolded and fails closed on malformed ref payloads. My only concern is the duplicated lens source in the gate fixture; I’d merge with a follow-up to collapse that bridge or at least name its removal trigger explicitly.

@briansrls

Copy link
Copy Markdown
Contributor Author

Ingested the claude-opus-4-7 APPROVE_WITH_COMMENTS (sha:e77c2609). Three non-blocking observations to fold in while you fix the merge-main issue:

1. Redundant compile_to_dag call in eval_lens_output_equals — the implementation compiles claim.source as a side-check before returning NotYetImplemented. That's fine as a bridge (the comment explains why) but the note in the review is right: when real lens evaluation lands, this compile call should be replaced rather than layered on. Consider adding a // TODO: remove side-check compile once eval_lens_output_equals does real evaluation comment.

2. Fixture split rationale should reference a tracking issue — r1_lens_output_equals_gate.dag header correctly names the compiler bug (DeclarationRef/Int resolution in same TU as large source string) but points to no issue number. Add a reference like // Dissolution trigger: <issue or ROADMAP line> so the split doesn't ossify.

3. Check for unused assert_all_pass import in test_runner_test.rs — after the stale test deletion (PR #709), assert_all_pass may no longer be called. If it produces an unused-import warning under -D warnings it will fail v3. Verify after merging main.

These are all fixable in the same push as the main merge. The BLOCKING issue (branch predates #679/#707 — file regressions) is the critical one.

@briansrls

Copy link
Copy Markdown
Contributor Author

Ingested codex APPROVE_WITH_COMMENTS (sha:e77c2609). One NON-BLOCKING finding to address while you fix the main-merge issue:

Parallel source text — dissolution trigger needed.
r1_gates.dag embeds the full named_function_count program text, and m1_5_user_authored_lens_gate_test.rs has a lockstep test asserting both copies match. Codex flags this as a P2 parallel-representation bridge (INVARIANTS.md). The lockstep test is the right mitigation for now, but the comment needs an explicit dissolution trigger: "Dissolution: once the runner can resolve a lens declaration by reference from the bootstrap DAG, the inline source string can be replaced by a direct DeclarationRef edge and the lockstep test deleted." Add that sentence to the bridge comment in r1_gates.dag header (or inline above the claim).

This is non-blocking — fold it into the same push as the main-merge fix.

@briansrls

Copy link
Copy Markdown
Contributor Author

Follow-up: specific items still regressed after main merges.

I see two merge commits from origin/main in the history but r1_gates.dag on the branch is still the pre-merge version. The conflicts were resolved by keeping the branch state. Here is what needs to be in the file after the next merge — compare against your branch and make sure all of these survive.

r1_gates.dag — declarations that must be present (origin/main as of e103c0c):

module std.r1_gates
import std.verification { Compiles, TestClaim, TestSuite }

data sub_match_over_user_sum: TestClaim = { … }
data sub_match_over_user_sum_gate: TestSuite = { … }
data user_authored_lens_compiles_gate: TestClaim = { … }
data manual_negative_claim_gate: TestClaim = { … }
data manual_claim_suite: TestSuite = { … }
data testgen_structural_coverage_gate: TestClaim = { … }   ← added by #720 (just merged)
data testgen_structural_coverage_suite: TestSuite = { … }  ← added by #720

Your branch currently has only user_authored_lens_compiles_gate in r1_gates.dag.

test_runner_test.rs — test that must survive from main:

#[test]
fn test_runner_runs_sub_match_over_user_sum_gate() {
    let manifest_dir = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
    let gate = manifest_dir.join("tests/fixtures/r1_gates.dag");
    let source = std::fs::read_to_string(&gate)…;
    let dag = compile_clean(&source, "…");
    let results = TestRunner::new(&dag).run_suite("sub_match_over_user_sum_gate");
    assert_all_pass(&results);
}

This test is present on main but dropped on your branch. It must not be deleted.

Import line in r1_gates.dag must be import std.verification { Compiles, TestClaim, TestSuite } — your branch has only TestClaim.

Suggested merge procedure:

git fetch origin main
git merge origin/main
# At the r1_gates.dag conflict: open the file and manually union
# both sides — keep every declaration from main PLUS any new ones
# your branch adds. Your branch adds nothing to r1_gates.dag, so
# the result should be identical to origin/main for that file.
# At test_runner_test.rs: keep test_runner_runs_sub_match_over_user_sum_gate
# from main AND your new tests from the branch.
git add -p   # review each hunk before staging
git commit

Everything else in the PR (eval_lens_output_equals, NotYetImplemented(String), r1_lens_output_equals_gate.dag fixture) looks correct. Unblock by resolving the merge regression.

#717 follow-up: branch already matches main declarations + PR comments; add an
explicit reminder so conflict resolution does not drop sub_match / manual /
testgen_structural suites again.

Made-with: Cursor
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 6981e665 · Trigger: schedule
  • Thinking: 37s wall

Findings

None blocking. Two small observations worth a look:

  • src/v3/compiler/src/test_runner.rs:263-268 — the side-check compile_to_dag(&claim.source, &claim.file_name) inside eval_lens_output_equals runs on every dispatch even though the result is discarded (the function always returns NotYetImplemented). Against the r1_lens_output_equals_gate.dag fixture the source is literally "let _: Int = 0\n", so the compile proves essentially nothing about lens application. The TODO / PR-review note does bound it with a named dissolution trigger (fold into real eval path), so this qualifies as tracked debt — just noting that the receipt is very thin today. (Non-blocking.)

  • tests/fixtures/r1_lens_output_equals_gate.dag:24 — the predicate is LensOutputEquals(Int, lens_output_ref_input, lens_output_ref_expected), i.e. the first "lens_ref" slot is populated with the type Int. The runner's resolve_declaration_ref_edge will accept it (the mock-invariant pattern reuses this shape), but the header/TODO doesn't quite call out that the lens slot is a stand-in for a type rather than a function declaration. Not a violation — same convention as the adjacent mock test — but worth noting in the "dissolve" trigger so nobody reads lens_ref=Int as a real edge later.

Verdict

APPROVE — scaffolding PR. NotYetImplemented(String) tightens fail-closed surfacing of unhandled predicates; the lens gate eval and fixture are clearly marked as bridges with bounded, named dissolution triggers (T-LensAPI / T-LaneE; side-compile folds into real eval). P2 parallel-copy duplication in r1_gates.dag is explicitly tracked with a ratchet test. No invariant/modeling violations observed in the diff.

…fixture

Ingest claude-opus-4-7 #717: delete (not supersede) witness compile when lens-apply
lands; document NYI→Fail risk; add checkable dissolution receipt for r1_lens split.

Made-with: Cursor
…pile

- Fixture: document LensOutputEquals first arg as type stand-in vs real lens ref
- eval_lens_output_equals: note trivial fixture source makes compile receipt thin

Made-with: Cursor
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: 6981e665 · Trigger: schedule
  • Thinking: 343s wall

Verdict: APPROVE

No concrete violations found in the diff. The LensOutputEquals path resolves declared DeclarationRef edges, fails closed on malformed payloads/missing bodies/compile failure, and the temporary fixture/string-copy bridges are documented with dissolution triggers.

Verified with:
cargo test -p v3-compiler test_runner_test -- --nocapture
cargo test -p v3-compiler m1_5_user_authored_lens_gate_test -- --nocapture

Replace inline TODO(dissolve) markers with ROADMAP subsection as single authority;
items are T-LensAPI/compiler-scale work, not implementable in the scaffold PR.

Made-with: Cursor
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 5ea84620 · Trigger: schedule
  • Thinking: 48s wall

Verdict: APPROVE

Diff is narrowly scoped: dispatches LensOutputEquals in the runner, adds an explicit message to NotYetImplemented, introduces a small split fixture, and ratchets the lens-text duplication with byte-identical assertion. Findings are bounded and tracked.

Tracked-debt items I checked, all acceptable:

  • src/v3/compiler/src/test_runner.rs:269 — side compile_to_dag(&claim.source, …) is called as a "thin witness." Comment names it a P5 bridge and points at ROADMAP §"Scheduled cleanups…" item 1 with a concrete dissolution trigger ("delete this whole block once the runner performs real lens application"). Documented + bounded + named trigger → tracked bridge, not unbounded scaffold.
  • src/v3/compiler/tests/fixtures/r1_lens_output_equals_gate.dag:25 — using Int as the first arg of LensOutputEquals(Int, …) (type used as DeclarationRef-shaped stand-in for a lens edge). Header explicitly warns "Do not read lens_ref = Int as a real lens declaration"; ROADMAP item 2 schedules dissolution when same-TU lowering is fixed.
  • r1_gates.dag ↔ named_function_count.dag byte-identical duplication — P2 parallel copy with lockstep ratchet test in m1_5_user_authored_lens_gate_test.rs, tracked under ROADMAP item 3 with named dissolution paths (generated splice / runner-resolved DeclarationRef).

Other observations (non-blocking):

  • eval_lens_output_equals returns NotYetImplemented even after successful structural resolution + witness compile. That's the right shape — runner does not yet evaluate the predicate, so reporting Pass would be a false positive (fail-closed). Good.
  • ClaimResult::NotYetImplemented(String) widening dissolves a tiny unit-variant ambiguity in favor of a localized message — straightforward modeling improvement (illegal-state-of-silence becomes representable). Existing single call site updated; assertions match on contents.
  • The resolve_declaration_ref_edge helper gives a targeted error for the Record(fields) if fields.is_empty() case (empty record literal vs identifier). Nice fail-loud diagnostic; matches CODING-style "data + free helpers."

Nothing in this diff to push back on.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 5ea84620 · Trigger: schedule
  • Thinking: 153s wall

Non-blocking — Strengths

  • src/v3/compiler/src/test_runner.rs LensOutputEquals now resolves typed DeclarationRef edges and returns an explicit runner-deferred result instead of silently falling through, with the temporary witness compile documented and scheduled for deletion.
  • src/v3/compiler/tests/fixtures/r1_lens_output_equals_gate.dag The fixture keeps the Int stand-in and split-file workaround documented, bounded, and tied to a ROADMAP dissolution trigger.

ROADMAP — Verified

  • LensOutputEquals runner and R1 gate fixtures: ROADMAP.md names concrete removal triggers for the witness compile, split fixture, and P2 source mirror.

✅ No blocking concerns in the PR diff.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 490fc705 · Trigger: schedule
  • Thinking: 35s wall

Verdict: APPROVE — diff is small, narrowly scoped, and the known-thin spots are all tracked.

Notes (non-blocking):

  • The witness compile_to_dag(&claim.source, …) at src/v3/compiler/src/test_runner.rs:272 is scaffolding that doesn't feed evaluation (runner still returns NotYetImplemented). Standard "tracked bridge" criteria — documented in-code, bounded (trivial fixture source let _: Int = 0), named dissolution trigger (ROADMAP schedule item 1, dissolved when real lens-apply lands). Accept.
  • The P2 parallel copy of named_function_count.dag inside r1_gates.dag + the lockstep ratchet in m1_5_user_authored_lens_gate_test.rs:102 is a substrate single-authority violation in spirit, but it's explicitly acknowledged in-fixture/test and tracked in ROADMAP item 3 with a concrete dissolution path. Accept as a bounded parallel copy.
  • Split fixture r1_lens_output_equals_gate.dag with LensOutputEquals(Int, …) using Int as a type-shaped DeclarationRef stand-in is documented as a mock convention; ROADMAP item 2 names the fold-back trigger (same-TU lowering fix). Accept.
  • NotYetImplemented gaining a String payload (variant widening) is an implementation-layer change to a runner result type, not substrate — existing call sites updated, tests assert on content. Fine.

Exploratory: The witness-compile block at line 272 is exactly the kind of thing that tends to rot into a second source of truth once it starts catching bugs. If you want to keep it strictly a stand-in, consider gating it behind a test-only #[cfg] or inlining it at the call site in the test rather than in the runner; otherwise the Fail it can produce on a lowering regression will be attributed to LensOutputEquals rather than to the claim's generic compilability, which could be confusing when someone hits it cold. Not blocking — just noting since the code comment itself flags the "don't leave it layered" risk.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: 490fc705 · Trigger: schedule
  • Thinking: 183s wall

Verdict: APPROVE

No findings. The diff’s temporary bridges are documented, bounded, and tied to named dissolution triggers in ROADMAP.md, so the P2/P5 debt is tracked rather than loose. The new runner path fails closed for malformed LensOutputEquals payloads and returns explicit NYI for unevaluated lens application.

Verified:
cargo test -p v3-compiler test_runner
cargo test -p v3-compiler r1_lens_output_equals_gate_fixture_compiles_against_bootstrap_context
cargo test -p v3-compiler user_authored_lens_testclaim_payload_tracks_on_disk_lens_and_compiles
git diff --check origin/main...HEAD

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 490fc705 · Trigger: schedule
  • Thinking: 206s wall

✅ No blocking concerns in the PR diff.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

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

Findings

None that rise to blocking. The three "bridge" scaffolds in this diff all carry the required (documented / bounded / named-trigger) properties:

  • test_runner.rs:280 — the witness compile_to_dag(&claim.source, …) inside eval_lens_output_equals is spurious relative to the predicate's semantics, but the block is explicitly flagged as P5 tracked debt with a ROADMAP anchor and an instruction to delete (not layer) when real lens-apply lands. Accepted as tracked bridge. Non-blocking.
  • r1_lens_output_equals_gate.dag split from r1_gates.dag — documented dissolution trigger (same-TU lowering fix for LensOutputEquals(Int, …) beside the large embedded source), ROADMAP item 2. Accepted.
  • TestClaim.source byte-copy of named_function_count.dag — called out as a P2 parallel copy, ratcheted by user_authored_lens_testclaim_payload_tracks_on_disk_lens_and_compiles, ROADMAP item 3 names dissolution paths. Accepted.

Exploratory observations

  • ClaimResult::NotYetImplemented(String) strictly improves diagnostics; the existing test was updated to match, and the runner now returns the resolved names as part of the NYI message — nice "facts flow forward" touch (resolved decls surfaced even on the deferred path).
  • One smell worth naming: Fail vs NotYetImplemented are now both reachable from eval_lens_output_equals for reasons unrelated to the predicate (the witness compile). If a future contributor mistakes a compile-failure Fail for a real predicate failure, the signal is misleading. The doc comment warns about this, but a structurally cleaner option is to keep the witness-compile failure mode as NotYetImplemented("… and witness source did not compile: …") so Fail stays reserved for actual predicate disagreement. Worth considering when item 1 is addressed — not a change-request here.
  • resolve_declaration_ref_edge's special-case for the empty-record {} literal is a thoughtful fail-closed diagnostic for a real footgun in the current lowering. Good.

Verdict

APPROVE — diff is narrowly scoped (runner dispatch + fixture + ratchet), the three modeling compromises are each documented as bounded tracked debt with ROADMAP dissolution triggers, and the new integration tests pin the deferred behavior (NYI message contents, resolved names). No invariant violations observed in the diff.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: 7fdb82fd · Trigger: schedule
  • Thinking: 177s wall

Verdict: APPROVE

The diff is narrowly scoped and the temporary bridge states are documented, bounded, and tied to ROADMAP dissolution triggers. I didn’t find any concrete violations of the pinned invariant, modeling, coding, or testing docs.

Verified with:
cargo test -p v3-compiler test_runner -- --nocapture
cargo test -p v3-compiler m1_5_user_authored_lens_gate_test -- --nocapture

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: claude / claude-opus-4-7
  • Commit: 00791bd9 · Trigger: schedule
  • Thinking: 42s wall

Findings

Nothing I'd block on. A couple of observations grounded in the diff:

  • src/v3/compiler/src/test_runner.rs:269-273 — the witness compile_to_dag(&claim.source, …) can flip an otherwise-NYI claim to Fail for reasons unrelated to LensOutputEquals semantics. This is the usual "scaffold" smell (facts-flow-forward / single-authority on what the predicate means), but it meets the tracked-bridge bar: documented inline, bounded ("delete this whole block"), and the dissolution trigger is named (ROADMAP scheduled cleanup item 1, T-LensAPI). Non-blocking; accept.

  • r1_gates.dag + m1_5_user_authored_lens_gate_test.rs — the TestClaim.source string is a P2 parallel copy of src/v3/lenses/named_function_count.dag, ratcheted by assert_eq!(source, ON_DISK_LENS, …). Same tracked-bridge analysis: header explicitly calls it P2, ROADMAP item 3 names the dissolution condition (runner-resolved DeclarationRef from bootstrap). Non-blocking.

  • tests/fixtures/r1_lens_output_equals_gate.dag:26 — LensOutputEquals(Int, …) uses Int as a DeclarationRef-shaped stand-in for the "lens function" slot. Slight illegal-states-representable risk (the predicate accepts a type where a lens decl is expected), but the mock-invariant predicate has the same convention and the fixture header is explicit. Tracked under ROADMAP item 2.

  • ClaimResult::NotYetImplemented → NotYetImplemented(String): clean facts-forward upgrade; both call sites updated, only callers outside the crate are the two tests in this diff. Good.

Verdict

APPROVE — the diff ships a narrowly-scoped LensOutputEquals dispatch returning NYI with a descriptive witness, the scaffolds (witness compile, parallel source text, split fixture) are all tracked bridges with documented/bounded/named-trigger dissolution in ROADMAP, and the ClaimResult variant change cleanly threads information forward. No modeling-discipline violations I can point at a line for.

@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: codex / codex-default
  • Commit: 00791bd9 · Trigger: schedule
  • Thinking: 186s wall

Verdict: APPROVE

No concrete invariant, modeling-discipline, coding, or testing violations observed in this diff. The temporary bridges are documented, bounded, and have named dissolution triggers.

Verified with:

  • cargo test -p v3-compiler --test integration test_runner
  • cargo test -p v3-compiler --test integration m1_5_user_authored_lens_gate_test
  • cargo test -p v3-compiler

@briansrls

Copy link
Copy Markdown
Contributor Author

Director review (tidy-koi-422): Hold for CI green, then merge.

  • LensOutputEquals dispatch + three-slot DeclarationRef resolution + NotYetImplemented(String) with named lens / input / expected. Shape matches the MockBackedInvariant dispatch in MockBackedInvariant wiring #722 (typed NYI reason, no silent ignore). ✓
  • ROADMAP.md "Scheduled cleanups: LensOutputEquals runner and R1 gate fixtures" makes the three pieces of tracked debt first-class rather than drive-by TODOs in code:
    1. the compile_to_dag(&claim.source, …) bridge receipt inside eval_lens_output_equals (with the explicit instruction: delete, do not layer when real lens apply/compare lands),
    2. the split r1_lens_output_equals_gate.dag fixture (fold back after same-TU lowering fixes the Int resolution issue),
    3. the P2 parallel lens text mirror between r1_gates.dag and src/v3/lenses/named_function_count.dag.
      Good modeling discipline — the debt has named triggers, not indefinite // TODO.
  • Fixture LensOutputEquals(Int, lens_output_ref_input, lens_output_ref_expected) reuses Int as a DeclarationRef-shaped stand-in until T-LensAPI lands; called out in comments.
  • Status: fmt ✓, ci / v3 in progress. No blocking feedback; merge once green.

Parked on green-CI watch.

@briansrls
briansrls merged commit 7b9d963 into main Apr 24, 2026
4 checks passed

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: de699049 · Trigger: schedule
  • Thinking: 258s wall

ROADMAP — Verified

  • LensOutputEquals runner cleanup: The side compile, split fixture, and P2 source mirror are documented, bounded, and have named dissolution triggers.

✅ No blocking concerns; the runner dispatch now fails explicitly instead of silently ignoring LensOutputEquals.

briansrls added a commit that referenced this pull request Apr 24, 2026
…t-merge

- #722 (MockBackedInvariant wiring) merged 2026-04-24; row now [x] with
  a one-line receipt (dispatch + DeclarationRef resolution + typed NYI).
- #717 row drops "in review" — dispatch landed, runner still returns
  NotYetImplemented; gate dissolution deferred to T-LensAPI D1/D2 (PR #741 in flight).
- Decisions-log entry updated with the same refresh.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 24, 2026
…lip to landed (#744)

* WIP: r1 testgen

* docs(r1-testgen-manager): working-state refresh — schema extensions (#678), runner (#688), LensAPI Day-1 gate (#679)

Runner foundation (#688) already merged; update status to reflect that.
Fix "Open questions" placeholder to _(none today)_.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): uncheck user_authored_lens_compiles until #679 merges

[x] while "merge pending" violates the section's own "update as
sub-deliverables close" rule. Keep unchecked until the PR lands.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): mark user_authored_lens_compiles closed (#679 merged)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): mark testgen_manual_claim_is_first_class closed (#707)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* chore: apply cargo fmt

* fix(test_runner_test): remove unused PathBuf import after stale test deletion

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): mark testgen_structural_coverage [x] (#720 merged)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): note PR #722 MockBackedInvariant in review

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: r1 testgen

* docs(r1-testgen-manager): flip #722 to landed + refresh #717 rows post-merge

- #722 (MockBackedInvariant wiring) merged 2026-04-24; row now [x] with
  a one-line receipt (dispatch + DeclarationRef resolution + typed NYI).
- #717 row drops "in review" — dispatch landed, runner still returns
  NotYetImplemented; gate dissolution deferred to T-LensAPI D1/D2 (PR #741 in flight).
- Decisions-log entry updated with the same refresh.

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

---------

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Apr 24, 2026
* WIP: r1 testgen

* docs(r1-testgen-manager): working-state refresh — schema extensions (#678), runner (#688), LensAPI Day-1 gate (#679)

Runner foundation (#688) already merged; update status to reflect that.
Fix "Open questions" placeholder to _(none today)_.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): uncheck user_authored_lens_compiles until #679 merges

[x] while "merge pending" violates the section's own "update as
sub-deliverables close" rule. Keep unchecked until the PR lands.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): mark user_authored_lens_compiles closed (#679 merged)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): mark testgen_manual_claim_is_first_class closed (#707)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* chore: apply cargo fmt

* fix(test_runner_test): remove unused PathBuf import after stale test deletion

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): mark testgen_structural_coverage [x] (#720 merged)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* docs(r1-testgen-manager): note PR #722 MockBackedInvariant in review

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

* WIP: r1 testgen

* docs(r1-testgen-manager): flip #722 to landed + refresh #717 rows post-merge

- #722 (MockBackedInvariant wiring) merged 2026-04-24; row now [x] with
  a one-line receipt (dispatch + DeclarationRef resolution + typed NYI).
- #717 row drops "in review" — dispatch landed, runner still returns
  NotYetImplemented; gate dissolution deferred to T-LensAPI D1/D2 (PR #741 in flight).
- Decisions-log entry updated with the same refresh.

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

* WIP: r1 testgen

* docs(r1-testgen-manager): T-LensAPI lane closed via #741 — flip rows + decisions log

- `lens_output_is_queryable_data` gate flips [ ] → [x]; receipt names D1+D2,
  the deleted `compile_to_dag` bridge, and the `r1_lens_output_input_from_program`
  Dag-reflection sentinel.
- `AlgebraicLaw` / `lens_composition_associative` rows annotated: #728 landed
  the initial dispatch; #741 dissolved the Rust operator recognizer into
  D1-backed `int_associativity_holds_all_triples` evaluation.
- Decisions-log entry captures the D1+D2+D3+D4 bundle, supersedes-#740
  callout, and the three dissolved ROADMAP cleanups. Prior decisions-log
  entry rewritten to reflect what #728 actually shipped vs what #741 dissolved.

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

* docs(r1-testgen-manager): correct `compile_to_dag` dissolution claim (codex review on #753)

`compile_to_dag(&claim.source, ...)` is still called on the real evaluation
path in #741 — intentional and load-bearing (program Dag for reflection,
canonical lens pairing for P2 id_space alignment), not a dissolved bridge.
ROADMAP §77 item 1 retains an open follow-on for retiring the parallel
compile paths once DeclarationRef resolves lens + inputs structurally.

- `lens_output_is_queryable_data` row receipt rewritten: real evaluation
  replaces the NYI thin receipt; compile paths remain fail-closed (P3);
  two follow-ons (§77 items 1 + 3) explicitly open.
- Decisions-log entry tightened: only ONE Rust recognizer was deleted
  (`declaration_is_binary_int_add_associativity_witness`); the LensOutputEquals
  thin-receipt shape was replaced, not a recognizer deleted.

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

---------

Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant