T-Lens API

[briansrls]

Summary

Day-1 T-LensAPI wiring for user_authored_lens_compiles: a minimal user-authored .dag lens plus a structural TestClaim gate, proven with compile_to_dag on top of the normal Dag::new() bootstrap — without folding the demo lens into the frozen bootstrap DAG (so symbolic cost / full-Dag emit paths stay unchanged).

What this PR does

• Adds src/v3/lenses/named_function_count.dag: demo lens lenses.named_function_count (structural terminal / behaviorally N/A per docs/v3-lens-capability-register.md). Not in regen.dag and not enumerated into Dag::new().
• Adds src/v3/compiler/tests/fixtures/r1_gates.dag: std.r1_gates module declaring user_authored_lens_compiles_gate: TestClaim with predicate: Compiles. The claim’s source is the full lens module text (byte-identical to the on-disk lens file); file_name is src/v3/lenses/named_function_count.dag.
• Adds src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs:
  • Compiles the gate fixture.
  • Reads source / file_name from the lowered TestClaim (runner-shaped path).
  • Asserts source matches include_str!(…/named_function_count.dag) (single-authority ratchet).
  • compile_to_dag(&source, &file_name) — executable Compiles receipt, not only “the record literal typechecks.”
• docs/v3-lens-capability-register.md: capability row for named_function_count.dag.
• Mechanical / CI: SG-0 hand-authored census entry for the new integration test; refreshed parse_corpus_manifest.txt when spec files touched; spec excluded_prefixes formatting churn as needed.

Why not bootstrap-bundle the lens

Earlier iterations showed that adding a user/demo lens to Dag::new() widens the DAG the Lane 2 Stage 2d symbolic cost emitter walks and can trip emit_rust_module (“port with no producer”) on CI. The landed design keeps the demo external: user lenses compile with compile_to_dag against the standard bootstrap context, but are not shipped inside the bootstrap snapshot.

Target specs (rust.dag / go.dag / python.dag) already scope SourceFiltering.excluded_prefixes to bootstrap authority trees (dsl/std/, src/v3/std/, src/v3/spec/, plus src/v3/compiler/ where applicable). This PR does not rely on a per-lens exclusion string for named_function_count; the lens simply never enters the bootstrap bundle.

Gate / roadmap

Satisfies the Day-1 user_authored_lens_compiles item under T-LensAPI in ROADMAP.md (user-authored lens compiles in the compiler’s standard context).

Reviewer note: bind.name == ""

In named_function_count.dag, count_named_bind uses bind.name == "" to detect an anonymous Bind (count only binds with a non-empty name).

In std.substrate, BindNode.name is typed as String (not Option<String>), so the empty string is the correct anonymous-bind sentinel today. If substrate ever moves to Option<String> for names, this demo would need to follow that model — not a violation on current types.

[briansrls]

Clean work — the lens loads, the fixture compiles, the gate declaration is present in bootstrap, register row is correct. Ready to merge with two small things to clean up first.

1. Inline user_authored_lens_compiles_predicate — it's an unnecessary bootstrap declaration.

r1_gates.dag declares let user_authored_lens_compiles_predicate: TestPredicate = Compiles only to use it once as the predicate field of the gate. This adds a named declaration to the bootstrap namespace that isn't a gate and will confuse the runner (it'll see a TestPredicate declaration that isn't a TestClaim). Inline it:

let user_authored_lens_compiles_gate: TestClaim = {
  name: "user_authored_lens_compiles",
  source: "...",
  file_name: "user_lens_fixture.v3",
  predicate: Compiles,
  requires: empty()
}

2. let vs data at module scope.

The test passes so let at module scope creates a declaration_by_name-reachable entry — functionally equivalent here. But data is the canonical form for named constant declarations that external tooling (the runner) looks up. All generated TestClaim values in lens_testgen.rs are rendered as data name: TestClaim = { ... }. Use data here to stay consistent with that convention and make runner dispatch unambiguous.

Everything else is correct: Behavior match is exhaustive (Value is a valid variant per substrate.dag), bootstrap loading approach is right and well-commented, register row format matches the table, the test structure is clean. Two edits and this ships.

[briansrls]

Review metadata

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

---

Findings

• src/v3/compiler/src/bootstrap.rs:148-165 — load-order workaround creates a second authority for staging order. build.rs already has a documented priority-list mechanism (staged_entries = collect_dag_entries(&std_dir, &["list.dag", "substrate_minimal.dag", "effects.dag", "substrate.dag"])) for exactly this problem (a staged file that must load after another). This PR adds a parallel mechanism: filter r1_gates.dag out of STAGED_FILES, then re-append at the end of the chain. Same load-order constraint, two places it can be expressed. Non-blocking, but adding verification.dag to the build.rs priority list (or extending it to also support a "load last" tail) keeps the ordering authority in one place. CODING.md "single authority" / cost-of-change lens.

• src/v3/compiler/src/bootstrap.rs:81-88 — NAMED_FUNCTION_COUNT_USER_LENS_DAG is a one-off include_str! for a single file under src/v3/lenses/, while the other 10 files in that directory are not bundled into Dag::new(). The header comment names this as a Day-1 fixture (bounded, named dissolution: "not wired into regen.dag"), so this counts as a tracked bridge — accept it. But note the precedent: the second user-authored lens that wants the same treatment will either copy this pattern or force a real lenses/ collector. Worth a follow-up before the third one shows up.

• src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs:13-16 — the OnceLock<Dag> cache is unused (only user_authored_lens_compiles_fixture reads it, exactly once). Not wrong, just dead generality. Trivial / non-blocking.

Verdict

APPROVE_WITH_COMMENTS — the change is small, scoped, and self-documents its bridge status. The substrate cost (one fixture lens + one staged gate file bundled into the bootstrap Dag) is real but acknowledged. Main thing worth thinking about before the next similar PR: pull staging order back into build.rs's priority list so bootstrap.rs doesn't grow a parallel ordering authority.

[briansrls]

Review metadata

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

---

Findings

• [BLOCKING] src/v3/compiler/src/bootstrap.rs:83, src/v3/compiler/src/bootstrap.rs:148, and src/v3/compiler/src/bootstrap.rs:161 reintroduce a hand-maintained bootstrap manifest outside the generated staged-file authority. The repo’s bootstrap discipline is explicitly “filesystem/build.rs owns the set; bootstrap.rs just consumes it,” and this change makes named_function_count.dag/r1_gates.dag a one-off Rust special case again. That violates INVARIANTS.md P2 / modeling-discipline.md single-authority practice at the bootstrap boundary, and it means the next “user-authored lens” example will need another bootstrap.rs edit instead of being a pure file addition.
• [NON-BLOCKING] src/v3/std/r1_gates.dag:10 and src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs:18 duplicate the exact gate fixture in two places. That weakens the claimed “declarative gate” receipt under INVARIANTS.md P2: the test asserts the TestClaim exists, but it does not execute that claim, so the staged gate can drift while the copied integration fixture still passes.

Verdict
REQUEST_CHANGES. The targeted test passes, but the bootstrap special-casing crosses the repo’s single-authority bar at a load-bearing boundary; I would want that modeled through the existing staged-file authority instead of baking another exception into bootstrap.rs.

[briansrls]

Root cause of the failing check: cost_generated_module_matches_checked_in_snapshot panics with UnsupportedBehavior("render reached a port with no producer (parameter?)"). Adding named_function_count.dag to the main bootstrap expanded the DAG that the symbolic cost lens emitter walks — it hits a behavior in the new declarations it can't handle. This is pre-existing fragility in the snapshot test, but the bootstrap expansion triggered it.

The fix is to not add either file to the main bootstrap. This is actually the cleaner design: "user-authored lens compiles" means a user writes a .dag file and compiles it against the standard bootstrap context — it doesn't need to be in the bootstrap. The current approach accidentally makes named_function_count part of the shipped compiler rather than demonstrating it as external.

Concretely:

1. Revert the bootstrap.rs changes entirely — remove both chain additions and the R1_GATES_STAGED_PATH filter. The bootstrap should be unchanged from before this PR.

2. Move r1_gates.dag out of src/v3/std/ — anything in src/v3/std/ is auto-staged by the build script, and r_ sorts before v_ so it would load before verification.dag and fail. Move it to src/v3/compiler/tests/fixtures/r1_gates.dag (a non-staged location). It's a test artifact for now; when the runner exists, its discovery path is a separate question.

3. Change the test to compile both files via compile_to_dag — this is the correct demonstration. The lens file compiles against the bootstrap context (it imports std.substrate) without being in the bootstrap:

   // Lens compiles against the bootstrap context — not inside it.
   const USER_LENS_SOURCE: &str = include_str!("../../../lenses/named_function_count.dag");
   match compile_to_dag(USER_LENS_SOURCE, "src/v3/lenses/named_function_count.dag") {
       Ok(dag) => assert!(dag.diagnostics().is_empty(), ...),
       ...
   }
   
   // Gate declaration compiles against the bootstrap context.
   const R1_GATES_SOURCE: &str = include_str!("../fixtures/r1_gates.dag");
   match compile_to_dag(R1_GATES_SOURCE, "src/v3/std/r1_gates.dag") {
       Ok(dag) => assert!(dag.diagnostics().is_empty(), ...),
       ...
   }

   Remove the bootstrapped_dag().declaration_by_name("user_authored_lens_compiles_gate") assertion — the gate declaration now lives in the test-compiled DAG, not in the main bootstrap DAG.

4. The USER_LENS_FIXTURE_V3 fixture test needs adjustment. The fixture imports lenses.named_function_count — that module won't be in the standard compile_to_dag context anymore. Either drop the import test (the lens-compiles test above already proves the key property) or use a multi-source compile if that API exists. The simplest path: drop the fixture entirely and let the lens-compiles test stand alone. The gate claim is "user-authored lens compiles" — the lens file compiling IS the proof.

This unblocks CI and better captures the thesis: user lenses are compiled externally, not embedded in the bootstrap.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 372b8266 · Trigger: schedule
• Thinking: 68s wall

---

Findings

• Parallel authority on the gate fixture source (non-blocking). The .v3 fixture text is declared in two independent places: src/v3/std/r1_gates.dag:12 as source: "..." on the TestClaim, and src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs:17-22 as USER_LENS_FIXTURE_V3. The doc comment on r1_gates.dag:3 says these are "consumed by future runners" — until that runner exists, the test is a second reader that hand-copies the same string. The whole point of staging the TestClaim is that it's the authority; the test should read gate.source rather than keep a parallel copy. Cheap drift waiting to happen (INVARIANTS.md §"parallel authority", line 106-108).

• Tail-append ordering workaround on r1_gates.dag (non-blocking, but worth a second look). src/v3/compiler/src/bootstrap.rs:151-167 filters src/v3/std/r1_gates.dag out of STAGED_FILES and re-chains it at the end because lexicographic order would load it before verification.dag. This is documented, and the const is included twice in the binary (once in STAGED_FILES via build.rs, once as R1_GATES_DAG). Fine as a one-off; if a second staged file needs the same trick, promote the ordering policy into build.rs rather than letting per-file filters accrete here.

• Cost-of-Change on per-target exclusion (non-blocking). Adding one demo lens required edits to src/v3/spec/go.dag:45, src/v3/spec/python.dag:148, and src/v3/spec/rust.dag:94-103 — three files to opt one lens out of emit. CLAUDE.md says "when the language grows by one … the answer should be 1." The property being expressed ("this lens is not emit-complete") belongs on the lens, not replicated across every target's SourceFiltering. Acceptable for a Day-1 fixture; flag for dissolution when a second emit-incomplete lens shows up.

• Minor: excluded_prefixes entry is a full path, not a prefix, e.g. src/v3/spec/rust.dag:100 "src/v3/lenses/named_function_count.dag". Works by prefix-matching semantics, but contrast with sibling entries like "dsl/std/" that clearly express directory intent. Low-stakes naming mismatch.

Verdict

APPROVE_WITH_COMMENTS. The change is narrowly scoped — a user-authored lens, a structural Day-1 gate, bootstrap plumbing, and emit-filter carve-outs — and the comments/doc updates are honest about what's scaffolding. Parallel-authority on the fixture source is the only finding I'd want addressed before this stops being a demo; everything else is tracked-bridge territory.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 372b8266 · Trigger: schedule
• Thinking: 278s wall

---

Findings

• BLOCKING: src/v3/spec/rust.dag:98, src/v3/spec/go.dag:45, and src/v3/spec/python.dag:148 add src/v3/lenses/named_function_count.dag to excluded_prefixes, while this same PR makes named_function_count a normal bootstrap-loaded callable (src/v3/compiler/src/bootstrap.rs:164, src/v3/lenses/named_function_count.dag:24). Existing emit code uses excluded_prefixes only to drop declarations from the emitted module, not to reject call sites, so a user module that imports this lens will compile but emit target code with an unresolved named_function_count reference. That violates INVARIANTS P3 / modeling-discipline fail-closed: unsupported emission needs a typed rejection, not a silently incomplete module.
• BLOCKING: src/v3/compiler/src/bootstrap.rs:89 and src/v3/compiler/src/bootstrap.rs:151 reintroduce a hand-maintained second authority for src/v3/std/r1_gates.dag: the file is still discovered through STAGED_FILES, but bootstrap now hardcodes both its contents and its path and appends it manually. That is a direct INVARIANTS P2 / modeling-discipline single-authority regression, and it also breaks the helper contract because excluded_staged_paths can no longer exclude r1_gates.dag once line 168 appends it unconditionally.

Verdict
REQUEST_CHANGES. The compile gate itself is small, but the PR currently makes the new lens compile-only by silently dropping it from emitted modules, and it reintroduces duplicate bootstrap authority for r1_gates.dag. I did not complete a targeted cargo test run because another cargo process was holding the workspace artifact lock.

[briansrls]

T-LensAPI Day-1 gate — review round 3

The lenses/bootstrap/ subdirectory approach is architecturally correct and cleaner than my earlier inline suggestion. Having a dedicated enumeration path (LENS_BOOTSTRAP_FILES) that is explicitly excluded from all three target specs (excluded_prefixes) is the right seam — it keeps user lenses out of the emission pipeline without any per-declaration annotations.

CI is still running on this revision, so I can't confirm the snapshot regression is resolved yet. The key question is whether LENS_BOOTSTRAP_FILES declarations are processed by the symbolic cost lens emitter (the thing that generated the failing snapshot). If the excluded_prefixes guard is applied before the cost lens emitter walks bootstrap declarations, we're clear. If the emitter walks all bootstrap declarations first and the filter only applies at the code-gen output stage, the regression will persist. Watch that specifically when CI results land.

Two small things to verify once CI is green:

1. r1_gates.dag tail-partitioning in build.rs: confirm the load order is [...other staged files..., r1_gates.dag] so verification.dag is fully parsed before the gate declarations that reference TestClaim and Compiles.

2. named_function_count.dag uses bind.name == "": Confirm that Bind.name is typed as String in std.substrate (not Option<String> or similar) so the empty-string sentinel is the correct expression for "anonymous bind" rather than an accidental non-exhaustive check.

Hold for CI. If green, I'll approve.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 8237192f · Trigger: schedule
• Thinking: 224s wall

---

Verdict: APPROVE — diff is small, narrowly scoped, and tests pass locally.

Findings: none blocking.

The substantive additions are:

• src/v3/lenses/named_function_count.dag — minimal user-authored lens, explicitly documented as demo/Day-1 gate, not staged into Dag::new() bootstrap, and scoped via the register entry in docs/v3-lens-capability-register.md:50.
• src/v3/compiler/tests/fixtures/r1_gates.dag + m1_5_user_authored_lens_gate_test.rs — the gate compiles the user lens externally via compile_to_dag, matching the documented shape.
• Spec-file array reformats (go.dag, python.dag, rust.dag) are pure multiline-list cosmetics; content of excluded_prefixes is unchanged.
• bootstrap_generated.rs churn is the expected span-shift regeneration from those reformats.
• build.rs change is comment/whitespace only.

Tracked-bridge check: the lens is labeled TERMINAL/N/A with the dissolution trigger documented (not in regen.dag; not bootstrap-bundled). That satisfies the tracked-debt bar.

Exploratory observations (optional):

• count_named_bind in named_function_count.dag:17-23 uses if bind.name == "" then 0 else 1. If Bind.name is ever tightened to Option<String> (a natural "illegal states unrepresentable" move — anonymous binds not representable as empty-string), this demo will need to switch to pattern-matching on the option. Not a current violation — just a foreseeable follow-up if/when that substrate change happens.
• Commit history carries several WIP: T-Lens API messages; worth squashing before merge so the lens + gate land as one logical commit. Non-blocking.

[briansrls]

Review metadata

• Provider / model: codex / gpt-5.4
• Commit: 8237192f · Trigger: schedule
• Thinking: 316s wall

---

Findings

• BLOCKING — src/v3/compiler/tests/fixtures/r1_gates.dag:14, src/v3/lenses/named_function_count.dag:6, src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs:41: the new Day-1 gate claims a program can import lenses.named_function_count, but the lens is explicitly not bootstrapped and the added test only compiles the enclosing TestClaim fixture, not the program in its source field. That misses TESTING.md’s behavior-driven bar: the diff proves “this record literal typechecks,” not “a user-authored lens can actually be imported and used.” Given current import handling, this gate also overstates live behavior.

Verdict
REQUEST_CHANGES

The direct named_function_count.dag compile looks fine, but the PR’s main receipt is inert: it never executes the new Compiles claim it adds. I’d want this wired through an executable claim path, or the claim narrowed to what the compiler actually supports today.

[briansrls]

T-LensAPI Day-1 gate — two test failures to fix

CI run 24869542541 reports two failing tests:

---

1. sg0 census drift — new hand-authored file not registered

+ src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs

You added this test file but didn't add its path to EXPECTED_HAND_AUTHORED in sg0_census_test.rs. Add the entry:

"src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs",

---

2. Parse snapshot manifest drift — spec files changed byte size

The three spec files (rust.dag, python.dag, go.dag) changed byte size when you added "src/v3/lenses/bootstrap/" to their excluded_prefixes. The checked-in snapshot manifest still records the old byte counts and hashes. Run the refresh command to regenerate it:

cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored

Then commit the updated handwritten_parse_snapshot_manifest file alongside the rest of your changes.

---

Both are mechanical fixes. Push them and CI should clear on the next run.

[briansrls]

Manager sign-off — v3, ci, fmt all green; self_host_ratchet pending but non-blocking. lenses/bootstrap/ separation, sg0 census, and parse manifest are all in sync. This is clear to merge when self_host_ratchet completes.

[briansrls]

All 4 checks green (v3 ✓, ci ✓, fmt ✓, self_host_ratchet ✓). Manager sign-off confirmed — ready to merge. There's a merge conflict with main that needs resolving before the squash can land; rebase or merge main in and push.

[briansrls]

All 4 checks green on the new run. Resolve the merge conflict with main and this lands.

[briansrls]

All 4 checks green. Merge-ready — land it.

[briansrls]

Hold on merge. Before landing: the PR body is still the session-dashboard default. Please replace it with a description covering:

1. What this PR does (lenses/bootstrap/ subdirectory, named_function_count.dag demo lens, r1_gates.dag Day-1 gate declaration, build.rs load ordering)
2. Why the bootstrap/ separation (keeps user lenses out of the cost-lens emission pipeline; excluded_prefixes in the target specs)
3. The gate this satisfies: user_authored_lens_compiles Day-1 (T-LensAPI, ROADMAP.md:52)

Also confirm: named_function_count.dag uses bind.name == "" as the anonymous-bind sentinel — Bind.name is String in std.substrate so this is correct, but call it out explicitly in the body so reviewers don't need to chase it.

All 4 checks are green. This lands once the body is real.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 7feac823 · Trigger: schedule
• Thinking: 354s wall

---

Non-blocking — Strengths

• src/v3/compiler/tests/integration/m1_5_user_authored_lens_gate_test.rs The gate reads TestClaim.source from the lowered fixture and passes that exact payload through fail-closed compile_to_dag, so the receipt exercises the lens body.
• src/v3/lenses/named_function_count.dag The demo lens is bounded, uses existing std.list and reflected substrate primitives, and adds no new substrate coproducts.

✅ No blocking concerns found in the mixed docs, .dag, and Rust test changes.

[briansrls]

Merged. Dispatching clever-owl-421 to lens_output_is_queryable_data next.