diff --git a/ROADMAP.md b/ROADMAP.md index 176b055c291..b2e07cc449e 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -5,6 +5,7 @@ Single source of truth for project status, active work, and deferred items. Long > Design spec: [docs/v3-spec.md](docs/v3-spec.md) > Validation: [docs/v3-validation-experiments.md](docs/v3-validation-experiments.md) > Lineage: [docs/design-lineage.md](docs/design-lineage.md) +> **Lens capability register: [docs/v3-lens-capability-register.md](docs/v3-lens-capability-register.md) — read before dispatching any brief that assumes "v3 subsumes v2 X".** ## How this doc is organized @@ -180,7 +181,7 @@ Tracked debt not dispatched with the 2026-04-21 lane wave currently in flight (L - **Stale §-style and line-number cross-references to pre-rewrite `INVARIANTS.md`**: Pro's post-#620 observation. Line-number refs in `docs/design-db16-refined-generic-substitution.md:297,298,413`, `docs/perf/clone-elimination.md:101`, `docs/lane2-compile-time-proofs.md:182`; §-style heading-name refs in `src/v3/M1_DESIGN.md` (§"No short-term solutions" / §"No bridges"), `src/v3/SELF_HOSTING.md` (§"Recursive syntax is sugar"), `docs/briefs/sg-4b-1-fix-declaration-lookup-cleanup.md` (§C-8 / §Track 9), `docs/briefs/p0-bug-no-profile-sentinel.md` (§"No fabrication sentinels"). Grep navigation still works because the strings survive as bullets in the new INVARIANTS.md, but line numbers have shifted and §-as-section framing is now approximate. Dissolution: sweep replacing line refs with `INVARIANTS.md#` anchors (post-#620) or name-based refs. Cosmetic, low urgency. Owner: unassigned. - **`Strict Forward Progress` subdoc ↔ heading drift**: pre-existing inconsistency between `docs/invariants/strict-forward-progress.md` (bounded-execution content) and the reviewer-usage meaning of the SFP rule name (dissolution-progress). Flagged explicitly in both P4 and P5 of INVARIANTS.md post-#620 as future cleanup. Dissolution: either rename the subdoc to reflect its bounded-execution content (and author a new dissolution-progress subdoc), or split the subdoc into two. Small scope once the design call is made on naming. Owner: unassigned. - **"Return first match" cascade cleanup** (dispatched in the 2026-04-21 wave currently in flight; listed here only to cross-reference): `src/v3/compiler/src/dag.rs:1999` and `:2023`, and ROADMAP:169 row, all inherit the "return the first match or fail-closed on multiple" phrasing from #625. Correct dissolution target is fail-closed-only. Owner: 2026-04-21 wave (cascade cleanup micro-lane). -- **Complexity lens v2/v3 comparison + cementing test**: v3's `src/v3/lenses/complexity.dag` (162 lines, 🟢 TERMINAL) is wired into the registry as the "cost" entry but has no receipt against v2's 5488-line heuristic `src/v2/complexity.dag`, and no test cements v3's current output so regressions would pass silently. Thesis-receipt lane: ~13× LOC reduction with structurally stronger fail-closed guarantees, awaiting demonstration. Also rolls in the `lens_cost_entry` → `lens_complexity_entry` registry-name cleanup (Phase 1 cosmetic). Dispatch brief: `docs/briefs/complexity-v2-v3-comparison-receipt.md`. Owner: unassigned; queue for after the 2026-04-21 wave's 5 lanes land. +- **v3 lens capability honesty pass (supersedes the complexity-receipt lane as originally scoped)**: the 2026-04-21 audit (see [docs/v3-lens-capability-register.md](docs/v3-lens-capability-register.md)) found that `src/v3/lenses/complexity.dag` does not subsume v2's `complexity.dag` — v2 produces symbolic `CostExpr` / `SizeExpr` with work/span/certainty/asymptotic-class, v3 produces a single integer depth per port. The same pattern holds for `cost.dag` (PROXY — no named size variables, Dimension wiring deferred), `idempotency.dag` (STUB — Rust oracle), and `parallelism.dag` (STUB — fail-closed placeholder). The originally-claimed "~13× LOC reduction with structurally stronger fail-closed guarantees" was comparing different functions of the program; retracted. **Follow-up work:** (1) the cementing-test discipline generalizes from one lens to every `regen.dag` entry (semantic-equality goldens per lens); (2) `docs/briefs/complexity-v2-v3-comparison-receipt.md` to be rewritten against the register — scope widens from "complexity receipt + registry rename" to "Band C honesty pass" once the register is merged. Substrate dissolution path: port `DescentEvidence` / `CallPattern` / `SubValueRelation` / `MethodSemantics` into the v3 substrate (currently blocks genuine equivalence for complexity + cost). Emit dissolution path: `match` lowering over user-defined sums (currently blocks `.dag` authority for idempotency + parallelism). Both are programs of work, not single lanes. Owner: unassigned; brief rewrite queues for after the 2026-04-21 wave's 5 lanes land and this register is in tree. - **CI ratchet architecture — exemption widening erodes the per-test timeout ratchet**: surfaced during the 2026-04-21 reflective analysis (`53b3110..ae8825a` range). Commits `37cd6128`, `4898983e`, `f84ed355` hardened the ratchet against CI-log instability, but `2d8396df` widened the exemption list. `scripts/slow-test-exemptions.txt` is 83 lines with no monotonic-shrink rule — `feedback_ratchet_only_down` violated at the meta level (the primary ratchet can drift upward through exemption growth). Dissolution: audit the exemption list, categorize each (stale / paydown / structural), delete stale entries, add a meta-ratchet that fails CI on exemption-count growth or per-exempt budget drift. Dispatch brief: `docs/briefs/ci-ratchet-architecture-audit.md`. Owner: unassigned; queue as infrastructure-principal lane, soon. - **Stale-receipt sweep in `docs/briefs/`**: surfaced during the 2026-04-21 reflective analysis. Briefs under `docs/briefs/` and prose references in adjacent docs still point at debt that the final code has partially or fully dissolved — the `DeclarationLookup` cleanup is the cited example where brief prose names debt the code has largely resolved. Integration drag, not code regression. Dissolution: sweep `docs/briefs/` for superseded claims post-wave, convert closed briefs to historical receipts under `docs/history/` or add a "Closed by #NNN" line, update inline prose in sibling docs that cite the resolved debt. Small scope, cosmetic. Owner: unassigned; do soon after the 2026-04-21 wave lands (most of its outputs will trigger more brief-staleness). diff --git a/docs/v3-lens-capability-register.md b/docs/v3-lens-capability-register.md new file mode 100644 index 00000000000..647af16e539 --- /dev/null +++ b/docs/v3-lens-capability-register.md @@ -0,0 +1,86 @@ +# v3 Lens Capability Register + +Canonical view of what every `.dag` lens under `src/v3/lenses/` actually computes, relative to its v2 counterpart (where one exists) and relative to the analysis its name implies. Load-bearing for direction review: any claim of the form "v3 replaces v2 X" must be checkable against a row in this table. + +## Why this document exists + +During the 2026-04-21 audit of the complexity lens we found that `src/v3/lenses/complexity.dag` (162 lines, marked 🟢 TERMINAL) does not subsume v2's complexity analysis. v2's `ComplexitySummary { work, span, output_size, certainty }` carries symbolic cost expressions, size variables, work/span separation, and asymptotic classification. v3's `cost_of(dag, port) -> CostLookup = FoundCost(Int) | MissingCost` carries a single integer depth per port and drops every other dimension. The 13× LOC reduction claim was comparing different functions of the program, not equivalent ones. + +Extending the audit to the other nine lenses under `src/v3/lenses/` surfaced the same pattern in three more files (`cost.dag`, `idempotency.dag`, `parallelism.dag`). The common root cause is substrate and emit gaps — the v3 substrate does not yet carry `DescentEvidence`, `CallPattern`, `SubValueRelation`, or `MethodSemantics`, and the v3 emitter cannot yet lower `match` on user-defined sums. So lenses that depend on those facts either compute a structural proxy or forward to a Rust oracle. + +The pattern was invisible at the file level because "🟢 TERMINAL" reads as both structural ("this file is a pure catamorphism, fail-closed, bounded") and behavioral ("this lens does the job its name implies") — but only the first claim was ever load-bearing for the marker. This register separates the two. + +## Status markers — two axes + +Every `.dag` lens declares both axes in its file header. + +**Structural status** — is the `.dag` file well-formed under the compiler's rules? + +| Marker | Meaning | +|---|---| +| `STRUCTURALLY TERMINAL` | Pure fold / catamorphism, fail-closed on malformed refs, no fuel, no mutual recursion, no heuristics | +| `STRUCTURALLY PARTIAL` | Intentional prototype or stub; scope explicitly bounded in the file header | +| `STRUCTURALLY UNSOUND` | Known-broken; exists as a placeholder or for regression observation only | + +**Behavioral status** — does the lens subsume the analysis its name implies? + +| Marker | Meaning | +|---|---| +| `BEHAVIORALLY COMPLETE` | Subsumes its v2 counterpart (or, if none, genuinely computes the named analysis). Has a behavioral cementing test. | +| `BEHAVIORALLY PROXY` | Computes a weaker function of the named analysis. The name overclaims relative to what the file produces. | +| `BEHAVIORALLY STUB` | The `.dag` file dispatches to a Rust oracle; the real analysis lives elsewhere. | +| `BEHAVIORALLY N/A` | v3-native analysis with no v2 counterpart; not scoped to subsume anything. | + +A lens is only "done" when **both** axes are at their strongest grade for the scope the lens claims. `STRUCTURALLY TERMINAL` alone is not done. + +## Capability table + +| Lens | Structural | Behavioral | v2 counterpart | v3 output | What v2 has that v3 drops | +|---|---|---|---|---|---| +| `complexity.dag` | TERMINAL | **PROXY** | `src/v2/complexity.dag` (5488L) | `CostLookup = FoundCost(Int) \| MissingCost` per port | `CostExpr` (Sum/Mul/Log/Const), `SizeExpr`, work/span split, `Certainty`, asymptotic classification, recurrence bounds | +| `cost.dag` | TERMINAL | **PROXY** | v2 `CostExpr` (embedded in `complexity.dag`) | `SymbolicCostLookup = FoundCost(SymbolicCost) \| MissingCost` per port | Named `SizeVar` with value semantics (v3's `SizeVariable` carries only `source_port: PortId`). `Dimension` wiring deferred on grammar gaps. No cementing test. | +| `idempotency.dag` | PARTIAL | **STUB** | None (v3-native) | `WorkflowIdempotencyReport` via dispatch | — (analysis lives in `src/v3/compiler/src/workflow_idempotency.rs`; the `.dag` is a registration shim) | +| `parallelism.dag` | PARTIAL | **STUB** | None (v3-native) | Unconditional `report_parallelism_unsupported(LensSurfacePending, …)` | — (real analysis in `src/v3/compiler/src/workflow_parallelism.rs`; the `.dag` is a fail-closed placeholder) | +| `provenance.dag` | TERMINAL | COMPLETE | None (v3-native) | `Origin = NoProducer \| MissingPort \| MissingBehavior \| Source(NodeId) \| Computed(NodeId) \| Selected(NodeId) \| Accumulated(NodeId)` | N/A | +| `unused_parameters.dag` | TERMINAL | COMPLETE | None (v3-native) | `List` | N/A | +| `variant_payload.dag` | TERMINAL | COMPLETE | None (v3-native) | `VariantPayloadShapeLookup` | N/A (see `DeclarationLookup` parallel-authority debt — ROADMAP 2026-04-21 wave, line 170 — which is an internal cleanup, not a behavioral gap) | +| `structural_resolution.dag` | TERMINAL | COMPLETE | None (v3-native) | `List` (regression pin) | N/A | +| `infer_helpers.dag` | PARTIAL | N/A | None | Bounded Cat-1/Cat-2 infer helpers only | N/A (see file header for scope — `predicate_info`, `walk_to_optional_cardinality_decl`, `callable_template_arguments`, `is_retryable_generic_decl_walk`, `declaration_is_callable`, `template_arguments_match` stay in Rust pending substrate work) | +| `lower_helpers.dag` | PARTIAL | N/A | None | `expr_span(expr) -> SourceSpan` only | N/A (see file header — `SurfaceLiteral -> LiteralBits` and tuple-variant helper rejected on emit gaps; wire-in parked on parse/parse_surface convergence) | + +## Common root causes + +The four "not done" rows (complexity, cost, idempotency, parallelism) share two blockers. Fixing these unblocks multiple lenses at once; the register exists in part so that is visible. + +### Missing substrate carriers (blocks genuine equivalence for complexity, cost) + +v2's complexity analysis imports, from `dsl/std/`: + +- `std.termination::DescentEvidence` (+ `RankingDimension`, `TerminationProof`, `ProofEdge`) +- `std.computation::CallPattern` (+ `IterationDimension`, `LoweringTarget`) +- `std.induction::SubValueRelation` (+ `CostBound`, `ShrinkFactor`, `PolynomialExponent`) +- `MethodSemantics` / `AlgebraMethodSemantics` (on `ExprMethodCall`) + +The v3 substrate (`src/v3/std/`) does not carry these. Until it does, v3 lenses over cost or complexity cannot derive symbolic bounds from termination + induction proofs the way v2 does; they can only walk bare DAG topology. This is recorded in `ROADMAP.md` P2 as "four hand-rolled `BoundedLattice` instances" but that entry flags the algebra-declaration gap, not the lens-consumer gap. Both are real; both are on the path to `BEHAVIORALLY COMPLETE` for complexity and cost. + +### Missing emit capability (blocks `.dag` authority for idempotency, parallelism) + +The v3 `emit_rust_module` cannot yet lower `match` on user-defined sums. That means a lens body that pattern-matches `WorkflowEffect` / `OperationEffect` variants cannot be the authoritative implementation — the emit would fail. So `idempotency.dag` is a thin dispatch-over-`lane2_workflow_at` shim and `parallelism.dag` is a hard `LensSurfacePending` stub. Both file headers name the specific blocker. + +This is the same class of gap recorded in `ROADMAP.md` under the 2026-04-21 receipt-closure wave ("emit_rust_module gap: SurfaceLiteral → LiteralBits rename", "emit_rust_module gap: render_variant_constructor fails on external tuple variants"). Those are different emit gaps; the user-sum-match gap belongs alongside them. + +## Discipline + +The register is a tool, not a document. If it is stale, it is worse than not existing — it licenses the exact "weeks of execution without a clear goal" failure mode that motivated it. + +1. **Every registry entry in `src/v3/compiler/regen.dag` requires a row here.** A `.dag` lens that is generated-and-shipped but absent from this table is unreviewable. +2. **Every claim of "v3 replaces v2 X" requires a behavioral cementing test.** A claim without a test is a hypothesis. The table column "What v2 has that v3 drops" must be empty (or filled with "N/A") before the behavioral status can read `COMPLETE`. +3. **Review at every ROADMAP dispatch.** Before queueing a brief that depends on a lens being equivalent to its v2 counterpart (e.g., "compare v3 complexity output against v2 complexity output"), check the row. If the row says `PROXY` or `STUB`, the brief is premature and must either wait for substrate/emit work or narrow its scope to what the lens actually computes. +4. **Downgrades are first-class.** A lens that regresses from `COMPLETE` to `PROXY` (e.g., because a cementing test failed and was weakened rather than fixed) belongs in this register immediately. Silent downgrade is the failure mode this document exists to catch. +5. **The two axes do not trade off.** `STRUCTURALLY TERMINAL` + `BEHAVIORALLY PROXY` is a valid, honest state — a well-formed file computing a weaker function than its name implies. It is not a contradiction. Claiming `COMPLETE` because the file is structurally clean is the mistake this register is named against. + +## Related docs + +- `ROADMAP.md` — the scattered debt rows that share this root cause (2026-04-21 receipt-closure wave, P2 tracked debts on lattice instances, DB-20 workflow parallelism, complexity-receipt brief entry) +- `docs/briefs/complexity-v2-v3-comparison-receipt.md` — the in-flight brief that prompted this audit; to be rewritten against this register (scope widens from "complexity + cementing" to "Band C honesty pass") +- `INVARIANTS.md` — particularly P1 Modeling Faithfulness; a `PROXY` lens whose name implies `COMPLETE` is an authored faithfulness failure even if the file is structurally clean diff --git a/src/v3/lenses/complexity.dag b/src/v3/lenses/complexity.dag index 56b77e20500..9501d49e92a 100644 --- a/src/v3/lenses/complexity.dag +++ b/src/v3/lenses/complexity.dag @@ -1,16 +1,31 @@ -// lenses.complexity — structural cost lens for the v3 DAG. +// lenses.complexity — structural depth lens for the v3 DAG. // -// 🟢 TERMINAL. Forward fold over `d.nodes` builds a per-port cost +// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY PROXY. +// See docs/v3-lens-capability-register.md. +// +// Forward fold over `d.nodes` builds a per-port integer depth // map. The substrate invariant that producers precede consumers in // `d.nodes` makes this a pure catamorphism — no fuel, no mutual // recursion, no manual termination measure. Structural termination: // `fold` drives the walk on the finite list `d.nodes`. // -// **Equivalent to the original Rust lens** at +// **This lens does not subsume v2's complexity analysis.** v2's +// `src/v2/complexity.dag` produces `ComplexitySummary { work, span, +// output_size, certainty }` with symbolic `CostExpr` / `SizeExpr` +// and asymptotic classification. This lens produces a single integer +// per port — the structural depth of the producing behavior in the +// DAG. The reduction in LOC versus v2 is achieved by computing a +// weaker function of the program, not by dissolving v2's algebra. +// Genuine equivalence blocks on porting `DescentEvidence`, +// `CallPattern`, `SubValueRelation`, and `MethodSemantics` carriers +// into the v3 substrate. See the register for the full delta. +// +// **Equivalent to the prior Rust lens** at // `src/v3/compiler/src/lens_cost.rs` on commit 1247f4b1d, which -// walked `produced_by` recursively. That oracle encodes the same -// algebra; this forward-fold is the substrate-native rewriting -// that exchanges recursive graph descent for sequential map build. +// walked `produced_by` recursively. That oracle encoded the same +// structural-depth algebra; this forward-fold is the substrate-native +// rewriting that exchanges recursive graph descent for sequential +// map build. // // **Fail-closed on malformed references.** `CostLookup` keeps // `MissingCost` distinct from `FoundCost(0)` so a port referenced by diff --git a/src/v3/lenses/cost.dag b/src/v3/lenses/cost.dag index d71a5560c85..d97fc24f910 100644 --- a/src/v3/lenses/cost.dag +++ b/src/v3/lenses/cost.dag @@ -1,3 +1,19 @@ +// lenses.cost — symbolic-cost lens over the v3 DAG. +// +// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY PROXY. +// See docs/v3-lens-capability-register.md. +// +// Produces `SymbolicCostLookup` per port using `SymbolicCost` +// combinators (`sequential`, `iterate`, `max_path`) from +// `std.algebra`. Richer than the integer-depth `complexity.dag` +// output, but `SizeVariable` here carries only `source_port: PortId` +// — there is no named size variable with value semantics the way v2's +// `SizeVar { name: String }` has. Output dimensions, certainty, and +// asymptotic classification from v2 are also not carried. Dimension +// wiring is deferred on grammar gaps (see the `Dimension` +// discussion lower in this file). No behavioral cementing test +// exercises this lens yet. + module lenses.cost import std.list { List, empty, fold, cons } diff --git a/src/v3/lenses/idempotency.dag b/src/v3/lenses/idempotency.dag index 8a21c81d05d..a5bf986df83 100644 --- a/src/v3/lenses/idempotency.dag +++ b/src/v3/lenses/idempotency.dag @@ -1,11 +1,19 @@ -// lenses.idempotency — Lane 2 Stage 2b workflow idempotency lens. +// lenses.idempotency — Lane 2 Stage 2b workflow idempotency dispatch shim. +// +// Status: STRUCTURALLY PARTIAL; BEHAVIORALLY STUB. +// See docs/v3-lens-capability-register.md. // // Reads `lane2_workflow` through the substrate accessor `lane2_workflow_at` -// (reflected on `ValueNode` / `BindNode` in `v3.std.substrate`) and projects -// through `std.effects::lane2_workflow_idempotency_report`. The Rust entry -// `v3_compiler::analyze_workflow` re-exports the Rust oracle; CI exercises lens -// emission in `m2_lens_idempotency_emit_test` (Rust/Go/Python emit smoke) and -// rustc round-trip in `m2_lens_idempotency_migration_test`. +// (reflected on `ValueNode` / `BindNode` in `v3.std.substrate`) and dispatches +// to `std.effects::lane2_workflow_idempotency_report`. The authoritative +// analysis body lives in `src/v3/compiler/src/workflow_idempotency.rs`; the +// Rust entry `v3_compiler::analyze_workflow` re-exports that oracle. This +// `.dag` file is a registration/dispatch shim, not the analysis — the +// `.dag`-as-authority posture blocks on the v3 emitter gaining `match` +// lowering over user-defined sums (`WorkflowEffect`). +// +// CI exercises lens emission in `m2_lens_idempotency_emit_test` (Rust/Go/Python +// emit smoke) and rustc round-trip in `m2_lens_idempotency_migration_test`. module lenses.idempotency diff --git a/src/v3/lenses/infer_helpers.dag b/src/v3/lenses/infer_helpers.dag index 34de679837b..4c8b99fcb6d 100644 --- a/src/v3/lenses/infer_helpers.dag +++ b/src/v3/lenses/infer_helpers.dag @@ -1,5 +1,8 @@ // SG-4b-1 prototype tranche — bounded Cat-1/Cat-2 infer helpers. // +// Status: STRUCTURALLY PARTIAL; BEHAVIORALLY N/A (intentionally bounded prototype). +// See docs/v3-lens-capability-register.md. +// // This prototype deliberately stops short of the refinement/discharge // readers. The existing reflected `BindNode` carrier does not expose // the predicate body port that `predicate_info` needs, so the helper diff --git a/src/v3/lenses/lower_helpers.dag b/src/v3/lenses/lower_helpers.dag index 956540eb0f5..175f75775fe 100644 --- a/src/v3/lenses/lower_helpers.dag +++ b/src/v3/lenses/lower_helpers.dag @@ -1,5 +1,8 @@ // SG-3g prototype — first `.dag`-authority lowering helper. // +// Status: STRUCTURALLY PARTIAL; BEHAVIORALLY N/A (intentionally bounded prototype). +// See docs/v3-lens-capability-register.md. +// // `expr_span` is the smallest real lowering primitive that survives // the current emit constraints: a pure match over `SurfaceExpr`'s // eleven named-field variants returning each variant's `span` diff --git a/src/v3/lenses/parallelism.dag b/src/v3/lenses/parallelism.dag index 566c63a22a0..ff64599e997 100644 --- a/src/v3/lenses/parallelism.dag +++ b/src/v3/lenses/parallelism.dag @@ -1,9 +1,15 @@ -// lenses.parallelism — Lane 2 Stage 2e parallel composition safety (staging stub). +// lenses.parallelism — Lane 2 Stage 2e parallel composition safety (hard stub). // -// Algebraic walk: `v3_compiler::analyze_parallelism` (Rust), kept in sync with -// `std.effects` carriers. Workflow facts on `Dag` (`lane2_workflow` on native -// Value/Bind) are not part of the reflected substrate vocabulary here — this stub -// fails closed until emit-table `match` + reflection land (same boundary as +// Status: STRUCTURALLY PARTIAL; BEHAVIORALLY STUB. +// See docs/v3-lens-capability-register.md. +// +// This file is not an analysis — `analyze_parallelism` unconditionally returns +// `report_parallelism_unsupported(LensSurfacePending, …)`. The authoritative +// analysis lives in `src/v3/compiler/src/workflow_parallelism.rs` (`v3_compiler:: +// analyze_parallelism`); workflow facts on `Dag` (`lane2_workflow` on native +// Value/Bind) are not part of the reflected substrate vocabulary here. The +// `.dag`-as-authority posture blocks on the v3 emitter gaining `match` lowering +// over user-defined sums + reflection of workflow facts (same boundary as // `lenses/idempotency.dag`). See ROADMAP Lane 2 Stage 2b “Reflection boundary.” module lenses.parallelism diff --git a/src/v3/lenses/provenance.dag b/src/v3/lenses/provenance.dag index c3dd8e16cbe..7237e3d97a0 100644 --- a/src/v3/lenses/provenance.dag +++ b/src/v3/lenses/provenance.dag @@ -1,5 +1,8 @@ // lenses.provenance — observational lens over `Port.produced_by`. // +// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY COMPLETE (v3-native, no v2 counterpart). +// See docs/v3-lens-capability-register.md. +// // One-hop backward walk from a port to the producing Behavior, returning // an `Origin` classification tagged by the producer's behavior kind. // Zero reconstruction: the lens only follows the edge that `infer` diff --git a/src/v3/lenses/structural_resolution.dag b/src/v3/lenses/structural_resolution.dag index 14b80708d78..b203cd53ffe 100644 --- a/src/v3/lenses/structural_resolution.dag +++ b/src/v3/lenses/structural_resolution.dag @@ -1,6 +1,9 @@ // lenses.structural_resolution — detect leaked `ArrowBody::Pending` // in the final Dag. // +// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY COMPLETE (v3-native regression pin). +// See docs/v3-lens-capability-register.md. +// // Defense-in-depth regression pin for the R13 fix (lower.rs). // User `fn` declarations are seeded by `seed_function_signature` // with `ArrowBody::Pending`, then `lower_fn_item` patches the diff --git a/src/v3/lenses/unused_parameters.dag b/src/v3/lenses/unused_parameters.dag index 278740a742a..109623a9d6b 100644 --- a/src/v3/lenses/unused_parameters.dag +++ b/src/v3/lenses/unused_parameters.dag @@ -1,3 +1,8 @@ +// lenses.unused_parameters — detect bind parameters never referenced in the body. +// +// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY COMPLETE (v3-native, no v2 counterpart). +// See docs/v3-lens-capability-register.md. + module lenses.unused_parameters import std.list { diff --git a/src/v3/lenses/variant_payload.dag b/src/v3/lenses/variant_payload.dag index a3dde9191bf..9b11f685643 100644 --- a/src/v3/lenses/variant_payload.dag +++ b/src/v3/lenses/variant_payload.dag @@ -1,6 +1,12 @@ // lenses.variant_payload — emitter-side classification for resolved variant // payload shapes (empty / positional single / named fields). // +// Status: STRUCTURALLY TERMINAL; BEHAVIORALLY COMPLETE (v3-native, no v2 counterpart). +// See docs/v3-lens-capability-register.md. +// (The `DeclarationLookup` parallel-authority cleanup tracked in +// ROADMAP 2026-04-21 wave is an internal C-8 tightening, not a +// behavioral gap in what this lens computes.) +// // Authority lives here; Rust projection is regenerated via `emit_rust_module` // into `src/v3/compiler/src/variant_payload_generated.rs`. Bootstrap // placement mirrors other lenses under `src/v3/lenses/` (not `src/v3/std/`)