feat(v3): T-Substrate-Lens-Primitive — Lens<C> carrier + Q6.5 widening

[briansrls]

Summary

First substrate slice for the lens framework (docs/design-lens-framework.md, docs/briefs/r2-substrate-manager.md). Director-locked option (c) on parent inbox #1130 (2026-04-29) after a stop-and-ping flagging the LensInstanceKindWitness.payload dependent-typing grammar gap.

P1 / P2 receipt

• P1 Step 1 — DAG ancestor: Lens<C> is a sibling concept to existing AnalysisDimension<Carrier> (dimensions.dag:72); both publish a generic compositional analysis surface. Lens<C> adds the 5-L1-behavior contract (read/sequential/branch/iterate/validate) the framework folds over; AnalysisDimension<Carrier> stays at the legacy three-field surface (witness_of/compose+identity/break_diagnostic) until consumers cut over. Reuses Witness<C> / OptionalDiagnostic / DimensionReport<C> from dimensions.dag and Monoid<C> from dsl/std/algebra.dag verbatim — no parallel reps introduced.
• P1 Step 2 — single fact per row: Lens<C> carries the irreducible 6-field contract; sequential: Monoid<C> replaces the prior parallel compose + unit field pair via structural inhabitance (Director directive 2026-04-28 + gpt-5-5-pro Finding Consolidate binaries into gunbc-dag package #4) so the monoid law is structurally enforceable, not merely documented.
• P2 — single authority: Q6.5 two-layer split. Layer-1 CompilerDiagnosticKind closed sum stays Substrate-Manager-owned and unchanged; Layer-2 lens-instance kinds enter via LensInstanceKind(LensInstanceKindWitness) exclusively. Diagnostic.kind widens to AnyDiagnosticKind so a single Diagnostic value can carry either layer without re-introducing a cross-manager handoff.

Substrate change

• New: src/v3/std/lens.dag declares Lens<C> with the locked 6-field shape: name, read: fn(Dag, Behavior) -> Witness<C>, sequential: Monoid<C>, branch: fn(C, C) -> C, iterate: fn(C, LoopBound) -> C, validate: fn(Dag, C) -> OptionalDiagnostic.
• Edit: src/v3/std/diagnostics.dag adds DiagnosticKindDecl, LensInstanceKindWitness (decl-only — see gap receipt), AnyDiagnosticKind = CompilerKind(CompilerDiagnosticKind) | LensInstanceKind(LensInstanceKindWitness). Widens Diagnostic.kind from CompilerDiagnosticKind to AnyDiagnosticKind. CompilerDiagnosticKind closed sum is unchanged.

Substrate gap receipt — LensInstanceKindWitness.payload intentionally absent

Per stop-and-ping at parent inbox #1130: today's .dag grammar cannot express the design-doc shape payload: <inhabits kind_decl.payload> (refinement-type-on-sibling-field). The flat alternative { kind_decl, payload_kind_shape } ratifies the very illegal state Q6.5 §State-space discipline rejects (three independent coordinates admitting (Lens<TenantFlow>, "WrongName", payload-of-different-shape)).

Director-approved option (c): LensInstanceKindWitness { kind_decl: DeclarationRef } — decl-only. Layer-2 kind identity and namespace authority land now via the decl-ref; the structured payload value is intentionally NOT carried through the substrate until dependent-field typing or substrate inhabitance witnesses lower without hand-Rust scaffolding. The dissolution trigger is named in the type's 🟡 SCAFFOLD comment, and the acceptance test lens_instance_kind_witness_payload_intentionally_absent fails loudly the moment a payload field is added — forcing the trigger comment to retire in lock-step.

Acceptance

src/v3/compiler/tests/integration/lens_substrate_carrier_test.rs — five structural claims over the regenerated bootstrap Dag:

• lens_carrier_has_locked_six_field_shape
• diagnostic_kind_widened_to_any_diagnostic_kind
• compiler_diagnostic_kind_closed_sum_unchanged (anti-bridge enforcement: Layer-1 closed sum cannot drift)
• any_diagnostic_kind_has_two_layer_constructors
• lens_instance_kind_witness_payload_intentionally_absent (gap-closure fail-loud trigger)

SG-0 ratchet receipt added with Director acceptance citation. parse_corpus_manifest.txt refreshed via the standard helper.

Commands run

cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap
cargo test -p v3-compiler --test integration refresh_handwritten_parse_snapshot_manifest -- --ignored
cargo test -p v3-compiler --test integration lens_substrate_carrier   # 5/5 pass
cargo test -p v3-compiler --test integration sg0_v3                   # 5/5 pass
cargo test -p v3-compiler --test integration handwritten_parse_snapshot_matches  # 1/1 pass
cargo test -p v3-compiler --test integration method_template_contract # 3/3 pass (regression check post-merge)

Notes for reviewers

iterate argument order: iterate: fn(C, LoopBound) -> C matches docs/design-lens-framework.md (the design-doc shape, also cited in the STOP+PING). docs/briefs/r2-substrate-manager.md writes iterate: (LoopBound, C) -> C; this PR follows the design doc per Director-locked option (c). Brief should be updated as a follow-up bookkeeping pass; carrier shape is intentional, not accidental.

Out of scope (subsequent lanes)

• Migration of cost.dag / complexity.dag / idempotency.dag / parallelism.dag PROXY lenses to consume Lens<C> (R3-T-CostLens-Composition + R2-Evaluator PR-A..E).
• fold_lens<C>: Lens<C> → Dag → DimensionReport<C> generic fold machinery (I2 in design doc).
• User-authored lens TestClaim wiring (I7 in design doc).
• Three worked-example fixture lens instances (I4 in design doc).
• Cross-domain product fixture (I5).
• Closing the dependent-payload grammar gap (LensInstanceKindWitness payload field).

Test plan

• cargo test -p v3-compiler --test integration lens_substrate_carrier passes.
• cargo test -p v3-compiler --test integration sg0_v3 passes (ratchet receipt valid).
• cargo fmt --all --check clean.
• CI rerun.
• Manager review.

🤖 Generated with Claude Code

[briansrls]

Early manager feedback on draft #1186:

The implementation direction matches the option (c) shape call: Lens<C> in src/v3/std/lens.dag, Q6.5 widening through AnyDiagnosticKind, closed CompilerDiagnosticKind preserved, and decl-only LensInstanceKindWitness with the dependent-payload gap made explicit. That is the right first-slice surface.

Before moving this out of draft, please tighten the operational surface:

1. Update the PR title/body. Current title/body are dashboard placeholders. The body should state the P1/P2 receipt, the option (c) payload deferral, exact regen/test commands, and that this PR does not migrate the four existing lenses.
2. Run/trigger CI. Because the PR is draft, all checks are skipped right now. Either run the focused local checks and list them, then mark ready, or use a manual dashboard trigger if you need a pre-ready CI read.
3. Resolve the iterate argument-order discrepancy explicitly. docs/design-lens-framework.md says iterate: (C, LoopBound) -> C; docs/briefs/r2-substrate-manager.md says iterate: (LoopBound, C) -> C. Your implementation uses (C, LoopBound), matching the design doc and your STOP+PING note. Keep that if intentional, but call out the brief mismatch in the PR body so reviewers do not treat it as accidental.
4. Confirm parse/bootstrap inclusion. Since src/v3/std/lens.dag is a new std file, make sure the generated full bootstrap sees Lens and that any parse manifest / SG-0 ratchet updates required by the new file are committed.

No request to broaden scope. Keep this PR as the carrier slice only.

— sent from jolly-ram-908 (inbox #1130); reply at #1130

[briansrls]

Manager feedback addressed:

1. Title/body: already refreshed via gh pr edit before manager pass — title is feat(v3): T-Substrate-Lens-Primitive — Lens<C> carrier + Q6.5 widening; body has full P1/P2 receipt, option (c) payload deferral, exact regen/test commands, explicit out-of-scope list (no PROXY-lens migration).
2. CI: flipped to ready via gh pr ready 1186. Local check results before flip: lens_substrate_carrier 5/5 pass, sg0_v3 5/5 pass, handwritten_parse_snapshot_matches 1/1 pass, method_template_contract 3/3 pass (regression check post-feat(v3): add MethodTemplateContract substrate carrier #1175 merge). cargo fmt --all --check clean.
3. iterate argument-order discrepancy: noted in PR body under "Notes for reviewers". Implementation follows docs/design-lens-framework.md (fn(C, LoopBound) -> C); the brief at docs/briefs/r2-substrate-manager.md writes (LoopBound, C) -> C — design doc is the locked authority per option (c). Brief bookkeeping update is a follow-up.
4. Parse/bootstrap inclusion verified at head: bootstrap_generated.rs line 885 declares Lens with the 6-field shape and span pointing at src/v3/std/lens.dag; parse_corpus_manifest.txt contains src/v3/std/lens.dag\t6\t9852\t28d5539a5b28716e; SG-0 EXPECTED_HAND_AUTHORED_TEST updated with the new test path + Director-acceptance receipt.

Carrier-slice scope unchanged. — sent from tidy-wolf-507

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: fa5bba2c · Trigger: schedule
• Thinking: 223s wall

---

BLOCKING (1)

Root Cause

• src/v3/spec/v3_l1.dag DeclarationRef is still an unrefined universal declaration pointer → add a typed declaration-reference/invariant path for DiagnosticKindDecl, or make this specific broad reference an explicitly bounded scaffold with its own dissolution trigger.

⚠️ The lens carrier slice is otherwise clean, but the new Layer-2 diagnostic-kind witness leaves its core authority unconstrained.

[briansrls]

BLOCKING: kind_decl: DeclarationRef accepts any declaration, so LensInstanceKindWitness does not structurally guarantee the declared DiagnosticKindDecl authority it claims (illegal states unrepresentable / API-level enforcement).

[briansrls]

Same residual class as the existing PatternRealization pattern at src/v3/std/emit_model.dag lines 140–152 and (recently merged) MethodTemplateContract.dag_method: DeclarationRef at emit_model.dag:371 — bare DeclarationRef admits any declaration; the structural constraint ("must be a DiagnosticKindDecl whose parent is the owning Lens<C> inhabitance") is enforced fail-closed at the boundary because the substrate grammar can't yet express DeclarationRef<DiagnosticKindDecl> (refinement-type-on-DeclarationRef).

Per parent-inbox #1130 dispatch (verbatim) on the option (c) lock: "For Q6.5, do not encode a fake dependent payload. Add DiagnosticKindDecl and AnyDiagnosticKind ... or equivalently a small LensInstanceKindWitness { kind_decl: DeclarationRef } without payload. The DeclarationRef must resolve to DiagnosticKindDecl; payload checking is explicitly deferred."

The dispatch explicitly accepted bare DeclarationRef for kind_decl and named the resolution check as deferred — same residual class the broader Q6.5 §State-space discipline acknowledges (option (a) was rejected for fabricating dependent state; option (c) is decl-only with the resolution check at the same boundary as PatternRealization's variant-of-target check). The 🟡 SCAFFOLD comment at diagnostics.dag lines ~75–95 names the dissolution trigger: "refinement/dependent field typing or substrate inhabitance witnesses lower without hand-Rust scaffolding." Tightening here without that trigger landing would either ratify option (a)'s rejected illegal state (free payload_kind_shape coordinate) or require hand-Rust dependent-typing scaffolding the dispatch explicitly forbade. — sent from tidy-wolf-507

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: fa5bba2c · Trigger: schedule
• Comparison: origin/main @ fbc55ad6 ... review/pr-1186-fa5bba2c @ fa5bba2c
• Thinking: 163s wall

---

Findings: None that rise to a documented invariant violation on the diff. Lens<C> uses Monoid<C> for sequential composition (aligned with INVARIANTS.md P1 substrate-fact procedure / DAG-ancestor example). Q6.5 is implemented as a two-layer kind model with an explicit anti-bridge rule on CompilerDiagnosticKind, owner-by-containment called out for DiagnosticKindDecl, and LensInstanceKindWitness documented as 🟡 SCAFFOLD with a concrete dissolution trigger (diagnostics.dag around the new types). New integration tests assert bootstrap shape (not full-pipeline “compile to test one lens”), and sg0_census_test.rs records the per-PR hand-Rust receipt and a forward dissolution note, which matches the spirit of the paired-dispatch / census discipline in the rubric you were given.

Verdict: APPROVE — The change set is narrowly scoped (new lens.dag, diagnostics.dag widening + regenerated bootstrap, focused tests and manifest/census wiring). I did not see a concrete breach of fail-closed, single-authority, or the documented scaffold rules on the touched lines; the intentional decl-only Layer-2 witness is called out as a substrate gap with a named trigger rather than smuggling a free TypeShape payload coordinate.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: c515b7e6 · Trigger: schedule
• Comparison: origin/main @ 46aa8a6c ... review/pr-1186-c515b7e6 @ c515b7e6
• Thinking: 63s wall

---

Read the rubric from the pinned context paths and reviewed git diff origin/main...HEAD (hand-authored slice: lens.dag, diagnostics.dag, integration test wiring, sg0_census_test.rs, manifest; plus regenerated bootstrap_generated*.rs).

Findings: None. Nothing in the diff clearly contradicts INVARIANTS.md, docs/modeling-discipline.md, CODING.md, or TESTING.md: the Lens<C> carrier uses structural Monoid<C> for sequential composition (avoids parallel compose/unit vs monoid authority), Q6.5 widens Diagnostic.kind via AnyDiagnosticKind instead of extending CompilerDiagnosticKind, and the LensInstanceKindWitness gap is explicitly documented with a named dissolution trigger and a ratchet test (lens_substrate_carrier_test.rs). The new integration tests document the Director exception and include an SG-0 census note with a forward dissolution path, which matches the scaffold / paired-dispatch spirit in INVARIANTS.md P5.

Verdict: APPROVE — Narrow substrate slice, boundaries and transitional debt are spelled out in the diff; no rubric violations identified with diff-grounded evidence.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 5bb049cd · Trigger: schedule
• Comparison: origin/main @ 46aa8a6c ... review/pr-1186-5bb049cd @ 5bb049cd
• Thinking: 32s wall

---

Imports check out. The diff is well-scoped: a new Lens<C> substrate carrier, widening Diagnostic.kind to a two-layer sum, and acceptance tests pinning the locked shapes plus a documented gap receipt for LensInstanceKindWitness.payload.

The scaffolds are properly tracked: each TRANSITIONAL/SCAFFOLD note documents the bound and the dissolution trigger (refinement/dependent-field typing). The anti-bridge invariant on CompilerDiagnosticKind is structurally enforced via the pinned closed-sum test. Lens<C> reuses existing Monoid<C>, Witness<C>, OptionalDiagnostic rather than introducing parallel representations. The kind_decl: DeclarationRef residual is explicitly tied to the same dissolution trigger as the payload gap — consistent with the existing PatternRealization precedent the comment cites.

Verdict: APPROVE — substrate addition is small, locked-shape-pinned by tests, and every scaffold has a named dissolution trigger. The Q6.5 two-layer split is the right way to admit lens-instance kinds without bridging through the Layer-1 closed sum.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: d1d25997 · Trigger: schedule
• Comparison: origin/main @ 192ea485 ... review/pr-1186-d1d25997 @ d1d25997
• Thinking: 228s wall

---

Verdict: APPROVE

Diff is narrowly scoped and the new substrate carriers are documented with clear authority boundaries and dissolution triggers. I did not find concrete violations of the pinned invariants, coding, or testing discipline.

Verification run: cargo test -p v3-compiler lens_substrate_carrier_test --test integration passed, 5/5 tests.