feat(v3): T-LensAPI D1+D2+D3+D4 — lens apply, LensOutputEquals/AlgebraicLaw, R1 fixture splice

[briansrls]

Summary

Implements the T-LensAPI D1 lens-application primitive (apply_lens_declaration + frame-based EvalCtx, authoritative std.list.fold via dag.std_list_fold_decl()), and consumes it to dissolve runner NYI paths: D2 real LensOutputEquals apply/compare (compile-fail-closed on claim.source, sentinel r1_lens_output_input_from_program for Dag input, P2-aligned id_space for reflection vs lens Dag); D3 real AlgebraicLaw(Associativity, …) via int_associativity_holds_all_triples / ASSOCIATIVITY_WITNESS_TRIPLES (operator-shape recognizer removed, not renamed). D4 folds the split r1_lens_output_equals_gate.dag into r1_gates.dag using r1_gates.template.dag + v3-compiler/build.rs splice-at-build-time (sentinel count = 1, skip fs::write on no-op). L-8: removed redundant pub fn field_value_equal -> bool from lens_apply.rs (use FieldValue PartialEq / ==).

Superseded PRs

• test_runner(v3): tighten AlgebraicLaw associativity recognizer to require surfaced-algebra operator resolution (pre-D1; dissolution still owed via T-LensAPI D1) #740 (wise-koi-316, AlgebraicLaw / associativity direction) — archived without merging. This PR delivers that intent the right way: structural operator witness deleted from test_runner; associativity is checked by bounded operational lens application over fixed triples, with an explicit “not a substrate law proof” posture in docs and NotYetImplemented for other AlgebraicLawKind variants.

Scheduled cleanups (ROADMAP — LensOutputEquals / R1 fixtures)

From “Scheduled cleanups: LensOutputEquals runner and R1 gate fixtures” (§77+):

1. eval_lens_output_equals witness compile — Done (PR feat(v3): T-LensAPI D1+D2+D3+D4 — lens apply, LensOutputEquals/AlgebraicLaw, R1 fixture splice #741): real evaluation + compile_to_dag(&claim.source, …) on the apply path; failures surface as Fail (P3), not silent fixture fallback.
2. Split fixture — Done: r1_lens_output_equals_gate.dag removed; gate lives in r1_gates.dag.
3. P2 parallel lens text — Done (D4): canonical named_function_count text spliced from src/v3/lenses/named_function_count.dag into generated r1_gates.dag; integration tests ratchet bytes vs include_str! / build.rs. Follow-on (stubs / DeclarationRef / sentinel) unchanged in ROADMAP.

Recognizer dissolution (#728-class): declaration_is_binary_int_add_associativity_witness / ordered-ring add shape path removed in favor of D3 witness application (see test_runner.rs / lens_apply.rs).

New surface: template vs generated r1_gates

• Edit src/v3/compiler/tests/fixtures/r1_gates.template.dag (must contain exactly one R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1 token).
• Do not hand-edit generated src/v3/compiler/tests/fixtures/r1_gates.dag — cargo build -p v3-compiler overwrites it from the template + canonical lens file.

Non-goals (this PR)

• Full substrate Behavior reflection: reflect_behavior / reflect_program_dag_nodes_in_file remain lossy (e.g. Transform/Branch/Loop carry only result_port in the mirror); dissolution triggers stay in code comments.
• General AlgebraicLaw: only Associativity is evaluated; other kinds stay NotYetImplemented.
• Monomorphized fold beyond R1 fragment: algebra-module fold sites still skip the D1 fast path (fold_site_skips_d1_monomorph_list_fold_path); eval_callable fail-closed for unsupported Instantiation {{ template: fold }} shapes outside the certified path.
• Eliminating all name/string bridges: PROGRAM_INPUT_SENTINEL, named_function_count canonical arm, fixture stubs — documented with named dissolution triggers until DeclarationRef / structured claim metadata land.

Test plan

• Unit (v3-compiler lib): lens_apply — named_function_count_on_trivial_program, empty_fold_returns_init, monomorphized_fold_step_bind_recovered_via_instantiation_arguments, int_add_lens_associativity_sample, int_add_overflow_returns_lens_apply_error_not_wrapped_value, branch_miss_when_scrutinee_matches_no_arm, mutual_recursion_lens_hits_unimplemented_loop_for_descent_cluster, apply_lens_declaration_arity_mismatch, …
• Integration: lens_output_equals_* (including test_runner_dispatches_r1_gates_lens_output_equals_claim, lens_output_equals_canonical_lens_bytes_match_build_splice_authority, lens_output_equals_malformed_claim_source_fails_closed_with_literal_input), m1_5_user_authored_lens_gate_test::* / R1 gates fixture locksteps, test_runner_* smoke for predicates.
• CI: fmt, ci (v2 pipeline), v3 (full v3-compiler tests, clippy, L-7/L-8 gates, compiler-std + banked-dissolution scripts).

[briansrls]

Director review (tidy-koi-422) — good D1 scaffold; mark ready after addressing blockers below.

This lands the T-LensAPI D1 lens-application primitive (apply_lens_declaration) plus an int_associativity_holds D3-consumer. Substrate-shaped interpretation, frame-based scoping, LensApplyError enum, std::list::fold dispatched through dag.std_list_fold_decl() (authoritative lookup, not name-matching) — all reads cleanly and matches the brief's "bounded interpreter over substrate primitives, not general .dag interpreter" scope constraint.

Blockers

1. lens_apply is not registered in src/v3/compiler/src/lib.rs. The diff adds src/v3/compiler/src/lens_apply.rs but changedFiles: 1 confirms lib.rs is untouched. CI will fail to build the crate — the #[cfg(test)] mod tests block references crate::compile_to_dag, and the crate can't see lens_apply as a public module. Add pub mod lens_apply; near the existing pub mod lens_depth; / pub mod lens_testgen; block (lib.rs:37-39).

2. PR body is empty (Opened from session-dashboard for session tidy-badger-434). Needs a Summary / Scope / Non-goals / Test-plan section so reviewers can judge against the T-LensAPI brief. Call out explicitly: "D1 primitive + D3-consumer helper; D2 (eval_lens_output_equals swap) and D4 (single-authority lens text) are not in this PR."

3. reflect_behavior / reflect_program_dag_nodes need a scaffold tag + dissolution trigger. These helpers reflect dag.nodes() into a substrate-shaped List<Behavior> FieldValue, but the reflection is lossy — TransformNode becomes {result_port} with no target / inputs; BranchNode / LoopNode similar. The named_function_count lens only reads bind.name, so the test passes, but any lens that reads transform.target or branch.paths will see empty records. This is parallel-representation debt (hand-rolled Behavior mirror). Either:

   • (a) make reflection complete w.r.t. std.substrate.Behavior now (preferred, and the debt is structural from the jump), or
   • (b) ship lossy reflection with an explicit 🟡 Scaffold doc-comment naming which fields are currently populated and a Dissolution trigger: line — e.g. "dissolve once .dag values on disk are consumed directly by the interpreter without a Rust-side reflection pass."

   Do not land without a dissolution receipt — otherwise this accumulates into the category memory warns about (parallel-representation debt; consume the canonical source, don't scaffold a mirror).

Non-blocking — please address before mark-ready

4. Test coverage is thin for a 651-line bounded interpreter. Two golden-path tests. At minimum add receipts for:

   • Empty list through fold (init returned verbatim)
   • LoopBound::Descent → UnimplementedLoopBound (fail-closed documented)
   • ArityMismatch from wrong-arity apply_lens_declaration call
   • Branch pattern with no matching variant → BranchMiss
   • Associativity with multiple triples including zero/negative — the current test is (2, 3, 5) only

   These receipt which bounded parts fail closed, which is the acceptance criterion for a scaffold interpreter.

5. variant_label / v3_list_empty_cons_ids are O(n) scans over all declarations per call. Fine for gate fixtures; not fine once T-LaneE complexity_merge_sort_is_nlogn applies this to a realistic program DAG. Flag with a // perf: linear scan; bounded OK, revisit if lenses iterate over DAG comment, or use declaration_by_name + shape-check for List (same pattern used for Bool at bool_value) to stay consistent.

6. Allocator hotspot. Every port lookup does .cloned() on the FieldValue; list_elements clones every element. Probably fine for R1 gates, but a comment at the EvalCtx struct saying "bounded-complexity interpreter; clones are intentional for R1 scope" prevents the next reader from thinking it's oversight.

7. Behavior::Bind with non-empty params as producer raises UnsupportedConstruct("non-root function bind as producer"). Good fail-closed. Worth a one-line doc: "Only top-level lens Binds (via apply_lens_declaration) and fold-step Binds (via eval_std_fold) accept parameters; inner let-bindings that parameterize a Bind are not yet handled."

Coordination

• test_runner(v3): tighten AlgebraicLaw associativity recognizer to require surfaced-algebra operator resolution (pre-D1; dissolution still owed via T-LensAPI D1) #740 (wise-koi-316, AlgebraicLaw) should consume your int_associativity_holds once this lands. That PR is currently still a structural recognizer — your D1 primitive is what dissolves it. I'll cross-reference when you mark ready.
• feat(v3): dispatch LensOutputEquals in test runner (lens output is queryable data) #717 follow-on (clever-owl-421, "fold r1_lens into r1_gates") is D4 cleanup; doesn't depend on D1 but may conflict on r1_gates.dag depending on order of landing.

No CI signal yet (draft). Once (1)-(3) are addressed, mark ready and I'll re-review for merge.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 09546a41 · Trigger: schedule
• Thinking: 338s wall

---

BLOCKING (2)

Root Cause

• src/v3/compiler/src/test_runner.rs AlgebraicLaw has no quantified substrate law evidence/evaluator → consume declared algebraic law facts or leave the predicate NotYetImplemented instead of replacing proof with samples.
• src/v3/compiler/src/lens_apply.rs Fold lowering/instantiation drops the closure dependency as a first-class edge → preserve the step closure in the lowered transform or add a substrate realization edge that lens_apply consumes directly.

ROADMAP — Verified

• LensOutputEquals cleanup item 2: The split fixture is deleted and the claim is folded into r1_gates.dag with an integration assertion for r1_lens_output_equals_suite.

⚠️ The new gate can accept evidence that is weaker than the substrate claim.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 0e87c668 · Trigger: schedule
• Thinking: 95s wall

---

Findings

• Non-blocking — fold_noise file-sniff (src/v3/compiler/src/lens_apply.rs:295). let fold_noise = t.span.file.contains("algebra.dag"); if is_fold_instantiation(...) && !fold_noise { ... } uses span-file substring matching to decide whether to fire the substrate fold interpreter. The module docs elsewhere bracket every scaffold with "Dissolution trigger"; this one has none and no explanation of what shape in std/algebra.dag is being dodged. A future caller re-homing the same pattern into a different file will silently flip behavior. Either replace with a structural predicate or annotate with a bounded trigger like every other scaffold in this file.

• Non-blocking — executed bodies for lens_output_equals_gate are the fixture-local stubs, not the canonical lens (src/v3/compiler/tests/fixtures/r1_gates.template.dag:59-70, src/v3/compiler/src/test_runner.rs:359). apply_lens_declaration(self.dag, lens_id, …) runs against self.dag (the fixture DAG), so the gate actually evaluates the stub fn count_named_bind / fn named_function_count bodies the template hand-copies from src/v3/lenses/named_function_count.dag. Comment says "keep in sync when editing the lens file" — that's the exact INVARIANTS.md P2 / modeling-discipline "parallel representation" failure mode the rest of this PR (build.rs splice of source) explicitly solves for TestClaim.source. The cleanup is listed as a ROADMAP follow-on with a named dissolution trigger, so this is tracked debt — but there is no ratchet test catching silent drift in the meantime. Worth an assert_eq!(stub_body_span_text, ON_DISK_LENS_BODY_SUBSTRING) style guard until the DeclarationRef-from-program_dag route lands.

• Non-blocking — span_same_file fuzzy suffix match (src/v3/compiler/src/lens_apply.rs:21-23). a.file == b.file || a.file.ends_with(&b.file) || b.file.ends_with(&a.file) false-positives on any two files with a shared tail (a/x.dag vs b/x.dag). Only used to gate find_fold_step_bind, so blast radius is bounded, but worth canonicalizing to one form or dropping the ends_with fallback.

Exploratory

• PROGRAM_INPUT_SENTINEL = "r1_lens_output_input_from_program" is a substrate-visible name that steers runner behavior by literal match. It's flagged in the comment, but long-term the sentinel is the kind of coprod ("is-reflection-input vs is-data-body") that wants to dissolve into an actual predicate variant in std.verification rather than string-compare on declaration names.
• The FieldValue interpreter currently takes .clone() on every port lookup and list head. The perf comment calls this out; once T-LaneE lights up, a Cow/Rc<FieldValue> pass is likely cheaper than rewriting the interpreter.

Verdict

APPROVE_WITH_COMMENTS. Substantial, well-scoped substitution of a real lens interpreter for the previous operator-recognizer; scaffolds are documented with dissolution triggers and the build.rs splice restores single-authority for the lens source string. Main residual drift risk is the parallel stub bodies in r1_gates.template.dag, which deserve a byte-ratchet until the DeclarationRef cleanup lands.

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 0e87c66849

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

Validate associativity on more than one input triple

This path now treats AlgebraicLaw(Associativity, ...) as true after checking only (2, 3, 5), which allows false positives: a non-associative lens can be written to agree on the four sampled calls (f(2,3), f(5,5), f(3,5), f(2,8)) but fail for other inputs, so the runner returns Pass for an invalid law claim. Because this gate is used as a correctness signal, the single-sample check can silently accept incorrect witnesses; please either keep a fail-closed recognizer or evaluate a stronger set of cases before returning Pass.

Useful? React with 👍 / 👎.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 655198c8 · Trigger: schedule
• Thinking: 178s wall

---

Findings

• BLOCKING: src/v3/compiler/tests/fixtures/r1_gates.template.dag:60 and :69 add executable fixture-local mirrors of src/v3/lenses/named_function_count.dag, while src/v3/compiler/src/test_runner.rs:368 applies the lens_id from the fixture DAG. That means LensOutputEquals evaluates the copied stub, not the canonical spliced lens text. This violates INVARIANTS.md P2 / modeling-discipline single-authority metadata: the “keep in sync” comment is convention-level, and there is no generated splice or ratchet for these function bodies. The gate can now pass against stale fixture logic after the canonical lens changes.

Verdict: REQUEST_CHANGES. The main issue is narrow: make the evaluated lens come from the canonical source, or generate/ratchet the fixture stubs until the declared dissolution trigger lands.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 8cb17bdf · Trigger: schedule
• Thinking: 76s wall

---

Findings

Non-blocking:

• src/v3/compiler/src/lens_apply.rs:22 — span_same_file uses a.file.ends_with(&b.file) || b.file.ends_with(&a.file) without a path-separator anchor, so "foo.dag" matches "barfoo.dag". This is only reached in the find_fold_step_bind_by_span_overlap fallback (the instantiation primary path is now correct after commit 8cb17bd), but given the fallback's dissolution trigger is named (attach step as explicit Transform input), worth tightening or dropping once the primary path is proven universal.

• src/v3/compiler/tests/fixtures/r1_gates.dag is both git ls-files-tracked and regenerated on every cargo build by build.rs:emit_r1_gates_fixture. This creates a committed-vs-generated duplication: a developer who edits r1_gates.dag directly will have their edit silently overwritten on next build, and CI can land a committed fixture that disagrees with its regenerated form if the splice is changed without rebuilding. The m1_5_user_authored_lens_gate_test ratchet catches drift in the spliced lens bytes, but not drift in the non-spliced template body. Consider either .gitignore-ing the generated file or adding a build-script check that fs::write only runs when content differs and a CI step that fails if the tree is dirty post-build. Not substrate — implementation hygiene.

Observations (not asks):

• The r1_lens_output_input_from_program magic-string sentinel in test_runner.rs:eval_lens_output_equals is a reasonable named bridge (documented, bounded, dissolution trigger = "Dag literals in fixture DSL"). Three properties present → tracked, accept.
• ASSOCIATIVITY_WITNESS_TRIPLES is honestly labeled ("A single triple can pass for operations that are not associative (coincidence)") and the diff explicitly does not claim this is a substrate law proof — failure text, predicate-module doc, and lens witness .dag all say so consistently. That is the right posture for a D3 sample witness.
• The old structural declaration_shape_matches_ordered_ring_add_associativity_recognizer (~100 lines of "resolves through surfaced algebra" shape matching) is deleted outright — net reduction of an illegal-states-representable scaffold replaced by a narrower sample-apply that rides the same interpreter used elsewhere. Good direction.
• operator_resolves_via_surfaced_algebra is kept as #[allow(dead_code)] for the "upcoming substrate law-read path on AlgebraicLaw" (infer.rs:3693). Acceptable as a named future hook, but if that path doesn't land soon the dead helper should go — dead code with a forward promise is a weak form of tracked debt.

Verdict

APPROVE_WITH_COMMENTS — the diff replaces a structural operator-shape recognizer with a genuine bounded interpreter, deletes the old scaffold rather than layering over it, and the documentation discipline (scaffold tags, dissolution triggers, lossy-reflection warnings, witness-not-law language) is consistent across Rust, fixtures, and lens .dag files. The only real concern is the committed-vs-generated r1_gates.dag duplication from build.rs — fix or gitignore, but not blocking.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 12ac0e94 · Trigger: schedule
• Thinking: 99s wall

---

Findings

All substantive bridges in this diff carry documented + bounded + named dissolution triggers, so the following are non-blocking notes rather than violations:

• lens_apply.rs:37-41 — file-suffix string match (span.file.as_str().ends_with("std/algebra.dag")) dispatches interpreter behavior. This is a canonical heuristic signal per P1 ("heuristics indicate lost structure") and has the shape of P3's "case enumeration for open sets." The function header names the dissolution (structural predicate on lowering facts / explicit Transform edge). Acceptable as a tracked bridge, but note it's the most fragile piece in the interpreter — any .dag file renamed or re-anchored through another path will silently skip the fast path. A span-carried "is-algebra-lowering" fact would be the right target.

• lens_apply.rs:127-146 — find_fold_step_bind_via_instantiation ambiguous_fallback returns a single bind when no formals.contains(&arg.parameter) match is found but exactly one callable bind exists. This is a small heuristic escape: if formal matching breaks due to lowering change, the fallback silently picks a plausible bind. Consider making this path error (fail-closed) rather than fall back, since the dissolution trigger ("attach the step as explicit Transform input") is the intended end state anyway.

• test_runner.rs:352-372 — name-keyed dispatch (lens_decl.name.as_deref() == Some("named_function_count")) selects the canonical-compile Dag vs. program_dag vs. self.dag. Documented bridge; dissolution trigger ("DeclarationRef resolves executable lens identity") is named. The three-way id-space selection logic (lines 393-404 / 461-477) is genuinely subtle — consider extracting it to a small helper that returns (lens_program, lens_apply_id, id_space) in one place so the input-reflection and lens-apply paths can't drift on their id-space choice.

• test_runner.rs:96 — ratchet ASSOCIATIVITY_WITNESS_TRIPLES.len() > 1` is a weak guard for "material breadth." Easy to quietly shrink to 2 while nominally passing. Not a blocker, just observably weaker than the comment's intent.

• Duplicate authority observation (P2/P5): r1_gates.dag is both checked in and build-generated. The skip-if-unchanged write avoids tree churn, but a stale checked-in copy + build.rs that isn't re-run (e.g. non-cargo consumers, doc/reviewer reading the fixture directly) will read a copy that differs from the template+lens. Not a teeth violation — m1_5_user_authored_lens_gate_test and the build itself enforce parity — but the template pattern would feel safer as a .dag.in that only exists generated under OUT_DIR, with the on-disk r1_gates.dag deleted. Existing footnote in the fixture header acknowledges this; recording the thought.

Verdict

APPROVE_WITH_COMMENTS. The diff meaningfully moves T-LensAPI forward: replaces the structural associativity recognizer (P1 heuristic) with a bounded operational lens-apply primitive, dissolves the pre-D1 surfaced-algebra crate-seam, uses checked Int arithmetic, single-authorities the lens bytes via build-time splice, and every remaining bridge carries a named dissolution trigger. Tests cover overflow, arity mismatch, branch miss, Bool-literal scrutinee, empty-fold, and the mutual-recursion fail-closed surface. The file-suffix heuristic and the ambiguous-fallback step-bind resolver are the two spots most likely to bite a future lowering change; tighten when the structural edges they proxy for land.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 12ac0e94 · Trigger: schedule
• Thinking: 333s wall

---

Findings

• src/v3/compiler/src/lens_apply.rs:937 — BLOCKING, violates INVARIANTS P3 / modeling-discipline fail-closed + API-level enforcement. int_associativity_holds feeds left_ab back into the next lens application without checking that the first application returned an Int, and src/v3/compiler/src/lens_apply.rs:940 accepts equality over any FieldValue. A constant fn op(a: Int, b: Int) -> Bool = true can therefore satisfy AlgebraicLaw(Associativity, op) even though it is not a binary Int -> Int operation. The runner should reject non-Int intermediate/final outputs, or validate the arrow shape before running the witness.

Verdict: REQUEST_CHANGES. The LensOutputEquals path looks fail-closed in the cases I checked, but the AlgebraicLaw witness can certify the wrong class of lens. Targeted tests run: int_add_lens_associativity_sample and test_runner_dispatches_r1_gates_lens_output_equals_claim passed.