Lane 1 Stage 1a: L1.5 tail + CostLens L-8 + banked-dissolutions ratchet

.github/workflows/ci.yml

@@ -103,3 +103,34 @@ jobs:
 
       - name: v3 Compiler Clippy
         run: cargo clippy -p v3-compiler --all-targets -- -D warnings
+
+      - name: L-8 Lens surface gate
+        run: |
+          # L-8 (INVARIANTS.md): migrated .dag lenses must not collapse
+          # their typed failure carriers into primitives at the public
+          # Rust surface. The forbidden shape is any `pub fn ... -> T`
+          # for T in {usize, bool, i64} inside a hand-written wrapper
+          # alongside a generated lens module — e.g., the deleted
+          # `pub fn cost_of(&self, port: PortId) -> usize` wrapper that
+          # shadowed the generated `CostLookup` carrier.
+          #
+          # Scope: every `src/v3/compiler/src/lens_*.rs` wrapper except
+          # `lens_depth.rs` (hand-written legacy lens, not migrated
+          # from .dag, so out of L-8 scope). `*_generated.rs` files are
+          # also scanned — they should never contain a collapsing
+          # wrapper, and catching one there would mean the emitter
+          # regressed.
+          wrappers=$(ls src/v3/compiler/src/lens_*.rs 2>/dev/null | grep -v "/lens_depth.rs$" || true)
+          if [ -z "$wrappers" ]; then
+            echo "L-8: no lens wrapper files to scan"
+            exit 0
+          fi
+          matches=$(grep -nE "pub fn .*-> (usize|bool|i64)" $wrappers 2>/dev/null || true)
+          if [ -n "$matches" ]; then
+            echo "::error::L-8 violation: lens wrapper collapses typed carrier to a primitive"
+            echo "$matches"
+            exit 1
+          fi
+
+      - name: Banked-dissolutions ratchet
+        run: scripts/check-banked-dissolutions.sh

INVARIANTS.md

@@ -2266,6 +2266,72 @@ loop-body collapse."* This is the right shape for E-8 debt: the
 ignore ledger names the blocking substrate capability, so the
 test's re-enable condition is unambiguous.
 
+### L-8: Lens Rust surfaces preserve typed failure carriers (2026-04-17)
+
+Public Rust surfaces of migrated `.dag` lenses MUST preserve the
+lens's typed failure carrier. When a `.dag` lens computes a typed
+result carrier (e.g., `CostLookup`, `Origin`), the public Rust API
+that exposes the lens MUST NOT erase that carrier into a panicking
+shim or an opaque primitive (`usize`, `bool`, etc.). Callers of the
+lens must be able to distinguish `Found(T)` from `Missing(reason)`
+at the type level.
+
+**Accepted patterns:**
+
+1. Re-export the generated carrier and query function directly
+   (Provenance / CostLens pattern):
+   ```rust
+   pub use generated::{Carrier, query_fn};
+   ```
+2. Typed wrapper whose public API uses the same carrier:
+   ```rust
+   impl CostLens<'a> {
+       pub fn cost_of(&self, port: PortId) -> CostLookup { ... }
+   }
+   ```
+
+**Forbidden patterns:**
+
+1. Collapsing typed miss states to a primitive via panic:
+   ```rust
+   pub fn cost_of(&self, port: PortId) -> usize { ... panic!(...) }
+   ```
+2. Silent collapse to a sentinel (`_ => 0`, `_ => false`) — erases
+   the distinction without even signaling.
+
+**Why:** the `.dag` lens authored a typed failure carrier because
+the miss state is a real outcome the lens computes. Erasing it at
+the wrapper loses information callers legitimately need. Panic is
+fail-closed but not composable — the caller has no recourse besides
+aborting.
+
+Earlier drafts allowed explicitly-named convenience helpers (e.g.
+`cost_of_or_zero`) that collapse a carrier to a primitive at a
+named boundary. **That exception is removed** (review round 1a.3):
+the grep gate forbids every primitive-returning `pub fn` in
+`lens_*.rs`, and the prose matches. If a specific caller needs a
+collapse, it writes the `match` at its own call-site — three lines
+that make the collapse visible in the call graph rather than hiding
+behind a wrapper name. Alignment between prose and ratchet is
+itself a single-authority concern.
+
+**Mechanical gate:** CI grep check blocks every primitive-returning
+public fn in a lens wrapper file:
+
+```
+grep -nE "pub fn .*-> (usize|bool|i64)" src/v3/compiler/src/lens_*.rs
+```
+
+Scope excludes `lens_depth.rs` (hand-written legacy lens, not
+migrated from `.dag`; out of L-8 scope). Zero matches required.
+Lens wrappers return typed carriers.
+
+**Origin:** Half A review feedback (2026-04-17) + round 1a.3
+prose/ratchet alignment. Full design:
+[docs/design-lens-rust-boundary.md](docs/design-lens-rust-boundary.md).
+Lane 1 Stage 1a migrated the one offender (`CostLens`); the gate
+prevents regressions.
+
 ### Single-authority metadata
 
 The compiler should provide all metadata (tool definitions, output

docs/lane1-stage-b-substrate-keyed-lookup.md

@@ -145,7 +145,7 @@ Add the grep check above to `.github/workflows/ci.yml` as part of the v3 job. Ze
 
 Stop work and surface if:
 
-1. **Substrate type emission missing a primitive** — e.g., `Map<K, V>` isn't emitted to Rust HashMap cleanly. If the .dag Map → Rust HashMap mapping has gaps, surface before hand-writing a workaround.
+1. **Substrate type emission missing a primitive** — e.g., the reflected map type isn't emitted to Rust HashMap cleanly. If that map-to-HashMap mapping has gaps, surface before hand-writing a workaround. The specific forbidden form (new map declaration in v3 std parallel to `dsl/std/types.dag`) is banked in `docs/post-l15-phase-plan.md § Banked dissolutions`; check DB-5 for the intended binding.
 
 2. **A lens genuinely needs a lookup primitive not in substrate.dag** — beyond `port(d, id)`, `node(d, id)`, `resolve_producer(d, id)` (the three query functions locked in [DB-5](./design-substrate-keyed-lookup-api.md)). Don't invent locally; add to substrate with justification.
 

docs/post-l15-phase-plan.md

@@ -170,18 +170,38 @@ When a reviewer points at a rejected shape in a lane/master doc, the fix is to d
 
 **Mechanical gate (runs in Lane 1 Stage 1a):** a CI grep check that fails the build if any lane doc (`docs/lane*.md`, `docs/phase*.md`) contains a forbidden string. Two files are exempt from the scan because they legitimately enumerate rejected names: the DB docs themselves (`docs/design-*.md`) — where rejection is recorded — and this master plan (`docs/post-l15-phase-plan.md`) — where the ratchet itself lives.
 
+The `FORBIDDEN=(...)` block below is the **single authority** for the ratchet. `scripts/check-banked-dissolutions.sh` parses this block directly — adding a rejected shape means extending this list in the master plan, not mirroring it in the script. The human-readable table above must stay in sync (enforced at review).
+
 ```bash
-# Sketch: scan only lane/stage docs; DB docs and master plan are exempt
 FORBIDDEN=(
+  # Row 1 — DB-5: substrate fields
   "port_by_id" "node_by_id"
+  # Row 2 — DB-6: closed transport coproduct
   "RestTransport" "ShellTransport" "GrpcTransport" "TransportKind"
+  # Row 3 — DB-1: target_language on Correction
   "target_language: TargetLanguageId"
+  # Row 4 — DB-4: clean-emission contract fields
+  "struct_fields: StructFieldRule"
   "StructFieldRule" "AllowAttributeOnStructDecl"
+  # Row 5 — DB-9: 6th Behavior variant
   "MutualLoop"
+  # Row 6 — DB-2: emitter shim deprecations
+  "#[deprecated]"
+  # Row 7 — DB-5: new Map declaration in v3 std (parallel to dsl/std/types.dag)
+  "Map<K, V>"
 )
 # Scan: docs/lane*.md and docs/phase*.md, fail on any match.
 ```
 
+**Coverage invariant.** The array above carries at least one forbidden
+substring for every row in the rejected-shape table. When a new row is
+added to the table, the corresponding strings land in the array in the
+same edit. Conversely, the array must not carry entries whose
+rejections aren't documented in a table row — every entry is
+answerable with a DB doc reference. Reviewers enforce both directions
+by hand when the table/array change; the per-row comments above
+cross-reference DB docs to make the mapping explicit.
+
 When a future DB doc rejects a shape, add the rejected name to this list as part of the DB's acceptance. The list only grows; a banked dissolution is permanent.
 
 ## Half B → lane dissolution map

scripts/check-banked-dissolutions.sh

@@ -0,0 +1,94 @@
+#!/usr/bin/env bash
+# Banked-dissolutions ratchet (Lane 1 Stage 1a).
+#
+# Scans lane and phase docs for shapes that the design-blocker set
+# (DB-1…DB-10) has formally rejected. The single authority is the
+# `FORBIDDEN=(...)` array in docs/post-l15-phase-plan.md § "Banked
+# dissolutions — rejected shapes" — this script PARSES that block
+# directly instead of hardcoding a second list.
+#
+# Exempt from the scan:
+#   docs/design-*.md         — DB docs record the rejections
+#   docs/post-l15-phase-plan.md — master plan carries the ratchet itself
+#
+# Usage: scripts/check-banked-dissolutions.sh
+#   Exits 0 when clean; exits 1 with a report on any match.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "$0")/.." && pwd)"
+cd "$REPO_ROOT"
+
+MASTER_PLAN="docs/post-l15-phase-plan.md"
+
+if [ ! -f "$MASTER_PLAN" ]; then
+  echo "banked-dissolutions: missing master plan $MASTER_PLAN" >&2
+  exit 1
+fi
+
+# Parse the authoritative FORBIDDEN array from the master plan. awk
+# isolates the lines between `FORBIDDEN=(` and `)`; grep extracts each
+# quoted string, sed strips the surrounding quotes. The master plan's
+# block is the single source of truth — see the plan's § Banked
+# dissolutions for rationale.
+#
+# Implementation note: using grep -oE + sed instead of a pure-bash
+# regex loop because entries like `"#[deprecated]"` contain characters
+# (`#`, `[`, `]`) that bash's `${var/pattern/}` treats as glob
+# metacharacters, leading to infinite loops in the naive version.
+FORBIDDEN=()
+while IFS= read -r entry; do
+  [ -n "$entry" ] && FORBIDDEN+=("$entry")
+done < <(
+  awk '/^FORBIDDEN=\($/,/^\)$/' "$MASTER_PLAN" \
+    | grep -oE '"[^"]+"' \
+    | sed 's/^"//; s/"$//'
+)
+
+if [ "${#FORBIDDEN[@]}" -eq 0 ]; then
+  echo "banked-dissolutions: could not extract FORBIDDEN array from $MASTER_PLAN" >&2
+  echo "The master plan's § Banked dissolutions block must contain a bash-style \`FORBIDDEN=(...)\` array." >&2
+  exit 1
+fi
+
+shopt -s nullglob
+FILES=()
+for pattern in docs/lane*.md docs/phase*.md; do
+  for file in $pattern; do
+    case "$file" in
+      docs/post-l15-phase-plan.md) ;;
+      docs/design-*.md) ;;
+      *) FILES+=("$file") ;;
+    esac
+  done
+done
+shopt -u nullglob
+
+if [ ${#FILES[@]} -eq 0 ]; then
+  echo "banked-dissolutions: no lane/phase docs to scan"
+  exit 0
+fi
+
+violations=0
+for pat in "${FORBIDDEN[@]}"; do
+  hits=$(grep -nHF -- "$pat" "${FILES[@]}" 2>/dev/null || true)
+  if [ -n "$hits" ]; then
+    if [ "$violations" -eq 0 ]; then
+      echo "banked-dissolutions ratchet: forbidden shapes found in lane/phase docs."
+      echo "Authority: $MASTER_PLAN § Banked dissolutions."
+      echo
+    fi
+    echo "--- forbidden: $pat ---"
+    echo "$hits"
+    echo
+    violations=$((violations + 1))
+  fi
+done
+
+if [ "$violations" -gt 0 ]; then
+  echo "banked-dissolutions ratchet: $violations forbidden shape(s) found."
+  echo "Fix: delete the restatement and reference the DB doc instead."
+  exit 1
+fi
+
+echo "banked-dissolutions ratchet: clean (${#FILES[@]} docs scanned, ${#FORBIDDEN[@]} forbidden shapes from $MASTER_PLAN)"

src/v3/compiler/src/lens_testgen.rs

@@ -1,7 +1,7 @@
 use crate::dag::{
     AtomPayload, Dag, Declaration, DeclarationId, Field, FieldValue, LiteralBits, TypeConnective,
 };
-use crate::lens_cost::CostLens;
+use crate::lens_cost::{cost_of, CostLookup};
 use crate::{compile_to_dag, CompileError};
 use std::collections::HashMap;
 
@@ -428,13 +428,50 @@ impl<'a> TestgenLens<'a> {
         )
     }
 
+    /// Return the complexity-lens cost for `bind_name` in a freshly
+    /// compiled fixture. `None` means the bind is not in the fixture
+    /// (legitimate skip — some testgen paths construct probes that
+    /// don't include a named bind). The two other failure modes
+    /// panic, because they indicate a structural invariant violation
+    /// the test harness must surface, not a silent "skip this claim":
+    ///
+    ///   - `CostLookup::MissingCost` — the lens computed no cost for
+    ///     a bind that testgen explicitly constructed. A well-formed
+    ///     fixture always has a cost for the named bind; MissingCost
+    ///     here means the fixture is malformed or the lens regressed.
+    ///
+    ///   - `i64 → usize` conversion failure — the lens emitted a
+    ///     negative cost. The complexity algebra is non-negative by
+    ///     construction, so a negative is a compiler invariant
+    ///     violation, not a caller concern.
+    ///
+    /// Keeping the two failure modes distinct prevents silently
+    /// dropping generated cost claims (Half A review blocker).
     fn bind_cost_of(&self, source: &str, file_name: &str, bind_name: &str) -> Option<usize> {
         let dag = compile_any(source, file_name);
         let bind = dag.nodes().iter().find_map(|node| match node {
             crate::dag::Behavior::Bind(bind) if bind.name == bind_name => Some(bind),
             _ => None,
         })?;
-        Some(CostLens::new(&dag).cost_of(bind.value))
+        let cost = match cost_of(&dag, &bind.value) {
+            CostLookup::FoundCost { _0: cost } => cost,
+            CostLookup::MissingCost => {
+                panic!(
+                    "testgen: cost lens returned MissingCost for bind `{bind_name}` \
+                     in fixture `{file_name}` — the named bind was found in the \
+                     Dag but has no cost entry. Indicates a malformed fixture or \
+                     a regression in the complexity lens."
+                );
+            }
+        };
+        Some(usize::try_from(cost).unwrap_or_else(|_| {
+            panic!(
+                "testgen: complexity lens emitted negative cost `{cost}` for bind \
+                 `{bind_name}` in fixture `{file_name}` — the cost algebra is \
+                 non-negative by construction; a negative value is a compiler \
+                 invariant violation."
+            )
+        }))
     }
 
     fn named_std_type_ids(&self) -> Vec<DeclarationId> {

src/v3/compiler/src/lib.rs

@@ -20,14 +20,42 @@ pub mod diagnostics;
 pub mod emit_go;
 pub mod emit_python;
 pub mod emit_rust;
-pub mod lens_cost;
 pub mod lens_depth;
 pub mod lens_testgen;
 pub mod lens_unused_parameters;
 pub mod operators;
 pub mod serialize;
 pub mod types;
 
+/// Cost lens. The authority lives in `src/v3/lenses/complexity.dag`;
+/// the Rust projection is auto-emitted into
+/// `src/v3/compiler/src/lens_cost_generated.rs` and re-exported here
+/// so callers use `v3_compiler::lens_cost::{cost_of, CostLookup}`.
+/// Editing the lens means editing the `.dag` — there is no
+/// hand-written implementation on this crate side.
+///
+/// L-8 compliance: `cost_of` returns the typed `CostLookup` carrier
+/// (`MissingCost | FoundCost(Int)`). Callers pattern-match on the
+/// variant rather than receiving a panicked-collapsed `usize`.
+pub mod lens_cost {
+    #[allow(
+        dead_code,
+        unused_imports,
+        unused_parens,
+        unused_variables,
+        clippy::clone_on_copy,
+        clippy::collapsible_else_if
+    )]
+    mod generated {
+        use crate::dag::*;
+        use crate::diagnostics::*;
+
+        include!("lens_cost_generated.rs");
+    }
+
+    pub use generated::{cost_of, CostLookup};
+}
+
 /// Provenance lens. The authority lives in
 /// `src/v3/lenses/provenance.dag`; the Rust projection is auto-emitted
 /// into `src/v3/compiler/src/lens_provenance_generated.rs` and wrapped