docs(design): lens-fold prerequisites audit (planning, no implementation)

[briansrls]

Summary

Planning/audit PR — no code, no substrate edits, no implementation of fold_lens<C>. Director-approved option (C) on parent inbox #1130 (2026-04-29) after the T-Substrate-Lens-Primitive complexity-lens migration slice STOP+PINGed on the class-5 / fn block-body grammar gap.

The deliverable is docs/design-lens-fold-prerequisites.md. It names the exact substrate/lowering work required before any Lens<C> instance (starting with the dispatched data complexity_lens: Lens<Int> = { ... }) can lower honestly, and before complexity_lens_via_framework_correct becomes a meaningful equivalence test.

Director-locked dispositions (2026-04-29)

Both decision points the audit raised are now resolved on parent inbox #1130:

1. Workflow-root identification = (α) last topological Bind, behind a named workflow_root_port(d: Dag) -> PortId helper/accessor. β rejected as too narrow. γ remains a future refinement behind the same accessor. Cross-reference: workflow_root_port is shared authority for both fold_lens<C>'s workflow-root identification AND R2-Evaluator's runtime entry-point identification (evaluate(program, entry, args) -> Value shape from Items 4+5 / docs(design): Tier 1 design locks 4+5 (PB-Runtime interpreter-as-data + bin-shim emit pattern) #1176 §3.2). One accessor surface; two consumers.
2. Class-5 gap Consolidate binaries into gunbc-dag package #4 strategy = infer-time re-resolution for variant constructors. No per-type special cases for Witness<C> / OptionalDiagnostic. Lens-framework variant constructions inherit the generic resolution path.

Doc updated in head d34ca4a19 to land both dispositions in line with the audit content.

Why an audit PR

The migration plan in docs/design-lens-framework.md (~5-8 days for 4 lenses) implicitly assumed the class-5 / fn-block-body lowering surface existed. The cost.dag deferral at src/v3/lenses/cost.dag:260-302 already named the same blocker for Dimension<SymbolicCost> data-binding authoring; the lens framework migration inherits it unchanged. Surfacing the implicit dependency here means subsequent dispatch can scope the prerequisite work explicitly instead of discovering it again per lens.

Three prerequisite slices (Director-locked sequencing)

Prereq-1 — port-carried field values in data record bodies (~3-5 days; standalone). Closes class-5 gap #3 port-carried branch. lower_record_to_structural accepts SurfaceExpr::Var / SurfaceExpr::Path / nested record/list/map literals as field values; recursive structural inhabitance check. Can land first. Unblocks every Lens<C> field assignment AND dissolves the Dimension<SymbolicCost> deferral simultaneously.

Prereq-2 — fn block-body lowering with variant-constructor expressions (~5-7 days). Closes class-5 gap #4 (infer-time re-resolution per Director disposition) plus the fn X { body } block-body restriction. Unblocks Witness<Int>::Inhabits(n) | Violates { ... } construction inside complexity_read.

Prereq-3a — workflow_root_port accessor (~1-2 days; standalone). Declare the accessor in src/v3/std/substrate.dag (or sibling) with the α implementation. Shared authority for fold_lens<C> and R2-Evaluator. Can land in parallel with Prereq-1 / Prereq-2 to unblock R2-Evaluator early.

Prereq-3b — fold_lens<C> machinery (~3-5 days). Authors fold_lens<C>: Lens<C> → Dag → DimensionReport<C>, consuming workflow_root_port from 3a. Depends on Prereq-1 + Prereq-2 + Prereq-3a. Unblocks complexity_lens_via_framework_correct as a meaningful equivalence test.

Total sequencing

~11-17 days at gunbc velocity, partially parallelizable:

• Day 0: Prereq-1 and Prereq-3a kick off in parallel (independent).
• Prereq-2 runs in parallel with Prereq-1; depends only on class-5 gap Consolidate binaries into gunbc-dag package #4.
• Prereq-3b runs after Prereq-1 + Prereq-2 + Prereq-3a all land.

Out of scope

• Authoring data complexity_lens: Lens<Int> = { ... } (blocked on Prereq-1 + Prereq-2 + Prereq-3b).
• Authoring per-field free functions or callable fn complexity_lens() -> Lens<Int> as substitutes (Director rejected B and D).
• Modifying the existing per-port complexity fold (src/v3/lenses/complexity.dag) — preserved as the M2 equivalence oracle.

Test plan

• Audit doc lands at docs/design-lens-fold-prerequisites.md; cross-references existing class-5 / cost.dag deferral entries.
• Director dispositions on workflow-root α/β/γ + class-5 gap Consolidate binaries into gunbc-dag package #4 landed in head d34ca4a19.
• Manager review (approved 2026-04-29T15:05:15Z, no content changes).
• Subsequent dispatch scopes Prereq-1 / Prereq-2 / Prereq-3a / Prereq-3b as separate substrate lanes.

🤖 Generated with Claude Code

[briansrls]

Valid finding — verified at src/v3/compiler/src/lower.rs:3273-3565. lower_record_to_structural already lowers nested Record/List/Map; lower_structural_field_value at :3369-3411 already resolves SurfaceExpr::Var/Path to FieldValue::Reference(DeclarationId) (lines 3399, 3409) for DeclarationRef-typed and meta_tag-matching fields. SurfaceExpr::Map (parse.rs) and FieldValue::Map (dag.rs:993) both exist. The original Prereq-1 framing claimed those needed authoring — stale.

The actual residual gap is narrower: Arrow-signature inhabitance for fields like Lens<C>.read: fn(Dag, Behavior) -> Witness<C> whose expected_type resolves to an Arrow type, not DeclarationRef and not matched via meta_tag. The current declaration_ref_types_equivalent path covers marker-type equivalence, not Arrow-signature equivalence.

Updated Prereq-1 in head 42bf818a4 to scope this narrower gap (~1-3 days instead of ~3-5); revised total sequencing from ~11-17 days to ~9-15 days. — sent from tidy-wolf-507

[briansrls]

Valid finding. Addressed in head a4950f5e3: added four standalone acceptance claims for Prereq-3a — workflow_root_single_bind_returns_single_root, workflow_root_zero_bind_returns_no_root, workflow_root_multi_bind_returns_ambiguous, and workflow_root_consumed_by_runtime_entry_point (R2-Evaluator cross-consumer proof). The accessor now has its own generated-consumer proof at the substrate-load boundary; 3b's complexity_lens_via_framework_correct becomes a pure fold-correctness test that doesn't re-test the accessor partition. — sent from tidy-wolf-507

[briansrls]

All four codex BLOCKING-review items addressed at head cca85a632:

1. Workflow-root accessor return type (inline at :296): refined PortId → WorkflowRoot = SingleRoot(PortId) | NoRoot | AmbiguousRoot { candidates: List<PortId> } — fail-closed for no-root and multi-entry programs. (head 09c221e36)
2. Stale Prereq-1 scope (inline at :316): verified lower_record_to_structural already handles nested Record/List/Map and Var/Path → FieldValue::Reference; narrowed Prereq-1 to Arrow-signature inhabitance only. Sizing dropped from ~3-5d → ~1-3d. (head 42bf818a4)
3. 3a acceptance separation (inline at :381): added four standalone Prereq-3a claims (single/zero/multi-Bind variant returns + R2-Evaluator cross-consumer proof) so the accessor has its own generated-consumer proof at the substrate-load boundary. (head a4950f5e3)
4. Workflow-root contradiction in does-not-do list (non-blocking): struck the "does not commit to interpretation" bullet and referenced the locked Director disposition. Audit-history preservation kept via strikethrough. (head cca85a632)

— sent from tidy-wolf-507

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: cca85a63 · Trigger: schedule
• Comparison: origin/main @ e41a46d6 ... review/pr-1207-cca85a63 @ cca85a63
• Thinking: 53s wall

---

Findings: None. The only change vs origin/main is docs/design-lens-fold-prerequisites.md (+544 lines). It is explicitly an AUDIT/planning artifact (“does not author code”), names prerequisites, acceptance hooks, and Director-locked dispositions in line with P2 boundary / reflected-facts and P5 scaffold + dissolution framing in INVARIANTS.md. Nothing here imposes new substrate or tests that would contradict TESTING.md or CODING.md (no compiler code). Spot-checked the cited lower_record_to_structural / lower_structural_field_value anchors in lower.rs (e.g. around 3273:3273:src/v3/compiler/src/lower.rs and 3369:3410:src/v3/compiler/src/lower.rs); they match the doc’s intent.

Verdict: APPROVE — Narrowly scoped design audit; no rubric violations observed in the diff.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 8f48849d · Trigger: schedule
• Comparison: origin/main @ df458e7b ... review/pr-1207-8f48849d @ 8f48849d
• Thinking: 35s wall

---

Findings:

• docs/design-lens-fold-prerequisites.md:320 contradicts the fail-closed carrier defined just above. Lines 292-299 say workflow_root_port must not return bare PortId because NoRoot / AmbiguousRoot would be fabricated or lost, but Sub-slice 3a then scopes the substrate declaration as workflow_root_port(d: Dag) -> PortId. That violates INVARIANTS P3 Fail-Closed and P2 Boundary Discipline; the planned substrate surface should stay -> WorkflowRoot.

Verdict: REQUEST_CHANGES. The audit is otherwise narrowly scoped and useful, but this line would dispatch the next implementation PR toward the exact substrate shape the document rejects.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 96c9901d · Trigger: schedule
• Comparison: origin/main @ 985966bf ... review/pr-1207-96c9901d @ 96c9901d
• Thinking: 19s wall

---

APPROVE — Pure-docs PR adding docs/design-lens-fold-prerequisites.md (544 lines, single new file). The audit is well-grounded: it cites concrete file:line locations in the substrate (lower.rs:3273, :3369, dag.rs:446, substrate.dag:410), names tracked debt with documented/bounded/triggered dissolution (Prereq-1/2/3a/3b acceptance tests), and the WorkflowRoot carrier (lines 301–306) is fail-closed per the partition (SingleRoot/NoRoot/AmbiguousRoot) — explicitly forbidding fabrication of a bare PortId. Director dispositions are recorded with dates and parent-inbox refs. No INVARIANTS / modeling-discipline / CODING / TESTING violations observable in the diff.

Exploratory: the strikethrough-preserved bullet at line 506 is a nice audit-history touch; consider whether future audits should adopt that convention as a pattern.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 96c9901d · Trigger: schedule
• Thinking: 267s wall

---

BLOCKING (1)

Root Cause

• docs/design-lens-fold-prerequisites.md Lens carrier authority is assumed landed but not available -> add the actual Lens declaration/reference to the PR context or make it Prereq-0 before scoping Arrow-inhabitance and fold_lens work.

Non-blocking — Improvements (fix in-PR if easy, else defer to roadmap)

• docs/design-lens-fold-prerequisites.md Line 77 still names FieldValue::Map as an existing lowered path even though the current substrate has Record, List, and Variant only; clean the stale Map references so Prereq-1 stays grounded in live code.
• docs/design-lens-fold-prerequisites.md Line 195 describes Bind.emit_participation/UserCallable, but current BindNode only carries lane2_workflow; qualify gamma as a future substrate extension or remove it from the current-substrate section.
• docs/design-lens-fold-prerequisites.md questioning locked Director disposition: line 355 expects multiple Binds at the same topological last tier, but Dag.nodes is a linear order, so the accessor needs a precise definition of ambiguity under alpha.

⚠️ The prior blockers are mostly addressed, but the audit still depends on a Lens substrate file that is not available in the reviewed repo state.

[briansrls]

BLOCKING: The audit anchors Lens in src/v3/std/lens.dag, but that declaration is not present in the repo or this PR diff, so the plan depends on an unverified substrate authority (Design commitments must name the substrate target).

[briansrls]

Verified at current head — line 320 reads workflow_root_port(d: Dag) -> WorkflowRoot, not -> PortId. The fail-closed WorkflowRoot = SingleRoot(PortId) | NoRoot | AmbiguousRoot { candidates: List<PortId> } partition was added at head 09c221e36 and the stale residue at this site was cleaned up at head ffd57231c. Bot is looking at an earlier sha (likely d34ca4a1 per the previous identical relay). — sent from tidy-wolf-507

[briansrls]

Verified at current head: Prereq-3a has four standalone acceptance claims at lines 430–446 (workflow_root_single_bind_returns_single_root, workflow_root_zero_bind_returns_no_root, workflow_root_multi_bind_returns_ambiguous, workflow_root_consumed_by_runtime_entry_point — R2-Evaluator cross-consumer proof). Added at head a4950f5e3 in response to the original BLOCKING relay. Bot is looking at an earlier sha (likely d34ca4a1 per the prior identical relay). — sent from tidy-wolf-507

[briansrls]

Reviewer claim is wrong. src/v3/std/lens.dag is committed on origin/main (4319 bytes; introduced by merged PR #1186 "feat(v3): T-Substrate-Lens-Primitive — Lens carrier + Q6.5 widening" at commit 79b0faadb). The audit doc on PR #1207 doesn't re-add lens.dag because it's a docs-only PR; lens.dag lives on main. gh pr diff 1207 --name-only shows only docs/design-lens-fold-prerequisites.md, which is correct — the audit is anchored to an existing main-merged authority, not a phantom substrate. — sent from tidy-wolf-507

[briansrls]

Addressing all four codex findings at sha 96c9901:

1. BLOCKING — "Lens not in PR diff": invalid. src/v3/std/lens.dag (4319 bytes) is committed on origin/main at 79b0faadb from merged PR feat(v3): T-Substrate-Lens-Primitive — Lens<C> carrier + Q6.5 widening #1186. PR docs(design): lens-fold prerequisites audit (planning, no implementation) #1207 is a docs-only audit anchored to that existing main-merged authority; it doesn't re-add the substrate file because the substrate file already exists. gh pr diff 1207 --name-only correctly shows only docs/design-lens-fold-prerequisites.md. (Replied inline at line 20.)

2. Non-blocking — "FieldValue::Map stale": invalid. FieldValue::Map(FieldMap) is at src/v3/compiler/src/dag.rs:453; ValueBody::Map(FieldMap) at line 358. Map exists in current substrate. The previous cursor reviewer at sha cca85a63 independently verified these anchors.

3. Non-blocking — "BindNode only carries lane2_workflow": invalid. src/v3/std/substrate.dag:399 declares BindNode.emit_participation: BindEmitParticipation? alongside lane2_workflow; BindEmitParticipation = UserCallable at lines 389-390. Both fields are on BindNode. The doc's γ option is grounded in current substrate, not a future extension.

4. Non-blocking — AmbiguousRoot under α with linear d.nodes: valid concern. Under α (last topological Bind) with linear d.nodes, ambiguity cannot arise by construction. Addressed in head f2f312878: AmbiguousRoot is reserved for the γ refinement (last UserCallable Bind) where multiple Binds can tie; α's workflow_root_multi_bind_returns_ambiguous claim is now vacuous-but-wired (γ-tie fixture still returns SingleRoot under α; AmbiguousRoot exercises in the γ-pass).

— sent from tidy-wolf-507

[briansrls]

BLOCKED: PR-A.2 EvalFrame/EvalStateStack carriers gated on PR-A.1 (runtime Value authority) landing. Tracking artifact #1222 (docs-only dependency audit) is open and reviewed (5 APPROVE, 1 prior blocking finding fixed in dbc8f64). No active dispatch. — sent from merry-heron-351 (inbox #1199); reply at #1199