R1 Census Close

.github/workflows/ci.yml

@@ -236,13 +236,10 @@ jobs:
           # `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)
+          # Scope: every `src/v3/compiler/src/lens_*.rs` file (hand-written
+          # and `*_generated.rs` — catching a collapsed wrapper in generated
+          # code would mean the emitter regressed).
+          wrappers=$(ls src/v3/compiler/src/lens_*.rs 2>/dev/null || true)
           if [ -z "$wrappers" ]; then
             echo "L-8: no lens wrapper files to scan"
             exit 0

docs/briefs/r1-selfhosting-manager.md

@@ -117,8 +117,10 @@ Lane-owner dispatch status (update as sub-deliverables close):
       T-TestGen extensions land
 
 **T-PB-B:**
-- [x] T-PB-B-1 — Landed `src/v3/compiler/tests/dag/*.dag` + compile-only smoke
-      (`t_pb_b_1_tests_dag_smoke_test`); brief `docs/briefs/t-pb-b-1.md`.
+- [x] T-PB-B-1 — Landed `src/v3/compiler/tests/dag/*.dag` + brief
+      `docs/briefs/t-pb-b-1.md` (former compile-only smoke
+      `t_pb_b_1_tests_dag_smoke_test` retired as redundant with
+      `t_pb_b_1_dag_runner_test` — 2026-04-24).
       **Not** Rust test deletion and **not** `pb_*` — those stay unchecked below
       until Testgen signs off.
 - [x] T-PB-B-1 — Runner-backed integration test landed (PR #736,
@@ -136,10 +138,10 @@ Lane-owner dispatch status (update as sub-deliverables close):
       previous row; `contract_diagnostic_smoke.v3` + `contract_port_cost_smoke.v3`)
 - [x] Identify and scope the two TESTING.md residual categories
       per-test (extended D/G/A/B matrix in Brief D)
-- [ ] Land **Rust deletions** for the three T-PB-B-1 claim shapes once Testgen
-      signals on checklist item (4) first-deletion batch (declarative data +
-      compile smoke + runner-backed evaluation for these three suites already
-      landed via PR #736 — see `docs/briefs/t-pb-b-1.md`)
+- [ ] Land **Rust deletions** for the remaining T-PB-B-1 / thesis inventory
+      (checklist item (4) follow-on) once Testgen records sign-off in
+      `docs/briefs/r1-testgen-manager.md` (first slice: redundant compile-smoke
+      file **landed** 2026-04-24; see *Decisions log*).
 - [ ] `pb_test_file_generated_from_dag` + `pb_rust_tests_outside_residual_zero`
       predicates evaluate true
 
@@ -161,8 +163,8 @@ Decisions log (append as they happen):
   floor read from `src/v3/compiler/tests/integration/sg0_census_test.rs`;
   the ≤5 irreducible-shim target not yet reached.
 - 2026-04-24: **T-PB-B-1** — landed `src/v3/compiler/tests/dag/*.dag` (`data` `TestClaim` /
-  `TestSuite` per `std.verification`) + `t_pb_b_1_tests_dag_smoke_test`; Rust tests not
-  deleted; Testgen runner / `pb_*` coordination still open (`docs/briefs/t-pb-b-1.md`).
+  `TestSuite` per `std.verification`); redundant compile-smoke file later
+  retired. Further Rust deletions / `pb_*` coordination: `docs/briefs/t-pb-b-1.md`.
 - 2026-04-23: **Brief D** (`docs/briefs/t-pb-b-brief-d.md`) — extended T-PB-B inventory +
   D/G/A/B matrix + draft `TestClaim` fixtures (`tests/fixtures/t_pb_b_brief_d/*.v3`);
   compile smoke via `t_pb_b_brief_d_fixture_smoke_test` (no `pb_*`, Rust tests unchanged).

docs/briefs/r1-testgen-manager.md

@@ -93,8 +93,9 @@ compose. When this closes, the R1 release gates themselves
   signal, then converts pipeline / contract tests. Notify
   Self-hosting when the runner lands. **Landed batch (runner-backed):**
   `docs/briefs/t-pb-b-1.md` + `src/v3/compiler/tests/dag/` —
-  `t_pb_b_1_dag_runner_test` evaluates the landed suites (PR #736);
-  compile-smoke counterpart is `t_pb_b_1_tests_dag_smoke_test`.
+  `t_pb_b_1_dag_runner_test` evaluates the landed suites (PR #736); the
+  former compile-smoke-only `t_pb_b_1_tests_dag_smoke_test` is **retired**
+  (redundant with the runner test — *Decisions log* 2026-04-24).
   **Pre–Rust-deletion checklist (single source — edit here only; do
   not fork a competing numbered list in other briefs):** (1) **[done,
   PR #736]** Runner accepts v3 `.dag` modules under
@@ -111,9 +112,15 @@ compose. When this closes, the R1 release gates themselves
   `t_pb_b_1_contract_port_cost.dag`; standalone
   `data _: TestPredicate = …` bodies remain NYI under the same
   class-5 restriction. Receipt paragraph in `docs/briefs/t-pb-b-1.md`.
-  (4) **First Rust deletion batch — prep, not yet signed off.** Target
-  shape: one thin `Compiles`-only duplicate whose claim is already
-  covered by a landed `.dag` suite evaluated under
+  (4) **First Rust deletion batch — partial sign-off (2026-04-24).** The
+  three `#[test]` functions in the former `t_pb_b_1_tests_dag_smoke_test.rs`
+  (redundant compile-only coverage for the landed `tests/dag/*.dag` modules)
+  are **deleted**; replacement coverage and the `#[test]` → `TestClaim`
+  mapping are recorded in the *Decisions log* below. **Still open** for the
+  remainder of the inventory until a follow-on sign-off entry lands
+  (same four-point guard). Target shape for the **next** slice: one thin
+  `Compiles`-only duplicate (or `thesis_validation_test.rs` subset) whose
+  claim is already covered by a landed `.dag` suite evaluated under
   `t_pb_b_1_dag_runner_test`. Candidate inventory (under
   `src/v3/compiler/tests/integration/`, registered in `integration.rs`
   and enumerated in `sg0_census_test.rs`):
@@ -233,7 +240,37 @@ Lane-owner dispatch status (update as sub-deliverables close):
 
 Decisions log (append as they happen):
 
-- 2026-04-24: **Pre–Rust-deletion checklist item (4) prepped, not signed
+- 2026-04-24 (Lane B / #763): **Pre–Rust-deletion checklist item (4) — first slice signed
+  off (redundant T-PB-B-1 compile-smoke).** Receipts (1)–(3) re-verified
+  green (`cargo test -p v3-compiler t_pb_b_1_dag_runner_test`,
+  `test_runner_data_bodies_reject_requires_empty_call_today`); PR #735
+  merged on main (`cf59f2288` — `CostBounded` witness for the candidate
+  claims is stable). **Deleted Rust tests** (file
+  `t_pb_b_1_tests_dag_smoke_test.rs` removed) and **replacement**:
+  `t_pb_b_1_dag_runner_test::lower` keeps the **empty module diagnostics**
+  compile-smoke receipt for each declaring `tests/dag/*.dag` harness, then
+  `TestRunner::run_suite` proves embedded `TestClaim` predicates (`ClaimResult::Pass`
+  for every claim — orthogonal to the outer harness diagnostic check). **Implementation
+  (current `lower` in `t_pb_b_1_dag_runner_test.rs`):** only `Ok(dag)` returns, with an
+  explicit `assert!(dag.diagnostics().is_empty())` on that arm; `Err(Semantic(_))` **panics**
+  (not a success path) — the declaring harness must compile with an empty module
+  diagnostic table before `run_suite` runs.
+  - `t_pb_b_1_pipeline_smoke_dag_lowers_cleanly` →
+    `t_pb_b_1_dag_runner_test::t_pb_b_1_pipeline_smoke_suite_passes_through_runner`
+    / suite `suite_pipeline_pipe_unary` / claim `claim_pipe_unary_compiles`
+    ("pipe unary call program compiles").
+  - `t_pb_b_1_contract_diagnostic_smoke_dag_lowers_cleanly` →
+    `t_pb_b_1_dag_runner_test::t_pb_b_1_contract_diagnostic_smoke_suite_passes_through_runner`
+    / suite `suite_contract_diagnostic_negatives` / claim `claim_bool_int_rejected`
+    ("Bool annotation rejects Int literal").
+  - `t_pb_b_1_contract_port_cost_dag_lowers_cleanly` →
+    `t_pb_b_1_dag_runner_test::t_pb_b_1_contract_port_cost_suite_passes_through_runner`
+    / suite `suite_contract_port_and_cost` / claims `claim_answer_resolved`,
+    `claim_answer_cost_bounded`. **Follow-on** first-batch work
+    (`thesis_validation_test.rs` subset; `pipe_desugar.rs` still excluded)
+  remains under the 2026-04-24 inventory + four-point guard until a
+  separate log entry names each `#[test]` → `TestClaim` pair.
+- 2026-04-24 (PR #751): **Pre–Rust-deletion checklist item (4) prepped, not signed
   off.** Candidate inventory narrowed — `pipe_desugar.rs` **excluded**
   from first batch (asserts `Transform` target / input arity / literal
   order / return shape; `t_pb_b_1_pipeline_smoke.dag` only witnesses

docs/briefs/t-pb-b-1.md

@@ -5,10 +5,9 @@
 ## Landed in repo (this PR path)
 
 - **`src/v3/compiler/tests/dag/*.dag`** — `TestClaim` / `TestSuite` as `data` declarations (`module v3.compiler.tests.t_pb_b_1.*`), schema from `src/v3/std/verification.dag`.
-- **`t_pb_b_1_tests_dag_smoke_test`** — `compile_to_dag` smoke only (no predicate evaluation, no `pb_*`).
-- **`t_pb_b_1_dag_runner_test`** (PR #736) — runner evaluates each landed `TestSuite`'s claims via `TestRunner::run_suite`; covers `Compiles`, `FailsWithDiagnostic{TypeMismatch}`, `PortHasState`, `CostBounded`. See *Receipts for pre–Rust-deletion checklist* below for the per-item coverage.
+- **`t_pb_b_1_dag_runner_test`** (PR #736) — `lower` asserts each declaring `tests/dag/*.dag` module compiles with **empty module diagnostics** (retired compile-smoke receipt), then `TestRunner::run_suite` evaluates each landed `TestSuite` (`Compiles`, `FailsWithDiagnostic{TypeMismatch}`, `PortHasState`, `CostBounded`). See *Receipts for pre–Rust-deletion checklist* below. (The former standalone `t_pb_b_1_tests_dag_smoke_test` file is **retired** as duplicate — see `docs/briefs/r1-testgen-manager.md` *Decisions log*.)
 
-**Compile-smoke caveat (smoke tests only):** `t_pb_b_1_tests_dag_smoke_test` does **not** call `TestRunner`; it only asserts the declaring module lowers with empty diagnostics. Its helpers accept both `Ok(dag)` and `Err(CompileError::Semantic(dag))` and then check empty **module** diagnostics — that proves the declaring `.dag` / `.v3` file lowers as a harness artifact, it does **not** evaluate `TestPredicate` (`Compiles`, `FailsWithDiagnostic`, …). Predicate evaluation for the `.dag` suites lives in `t_pb_b_1_dag_runner_test` instead: `FailsWithDiagnostic` is proven there by the runner on the embedded program, **not** by empty diagnostics on the outer file (which would invert the predicate). **`t_pb_b_1_contract_diagnostic_smoke.dag`** is the sharp example: it names `FailsWithDiagnostic` for embedded `source: "let x: Bool = 1"`, the smoke still requires the **wrapper** module to lower without diagnostics, and the runner test is what actually witnesses the embedded negative. Do not treat the smoke pass as semantic proof of the negative, and do not promote diagnostic-negative fixtures to CI-backed assertions from the smoke path alone (see also Brief D duplicate-authority / dissolution; the Brief D `.v3` `let`-binding path is still smoke-only).
+**Compile-smoke caveat (Brief D `.v3` only):** `t_pb_b_brief_d_fixture_smoke_test` does **not** call `TestRunner`; it only asserts the declaring module lowers with empty diagnostics. That proves the draft `.v3` harness artifact lowers, it does **not** evaluate `TestPredicate` on embedded sources. Predicate evaluation for the **landed** `.dag` suites lives in `t_pb_b_1_dag_runner_test` instead: `FailsWithDiagnostic` is proven there by the runner on the embedded program, **not** by empty diagnostics on the outer file (which would invert the predicate). **`t_pb_b_1_contract_diagnostic_smoke.dag`** is the sharp example: it names `FailsWithDiagnostic` for embedded `source: "let x: Bool = 1"`; the wrapper module still lowers without diagnostics, and the runner test witnesses the embedded negative. Do not treat compile-smoke as semantic proof of the negative, and do not promote diagnostic-negative fixtures to CI-backed assertions from the smoke path alone (see also Brief D duplicate-authority / dissolution; the Brief D `.v3` `let`-binding path is still smoke-only).
 
 **Compiler constraint (today):** M1(2.8) rejects standalone `data …: TestPredicate = PortHasState(…)` / `CostBounded(…)` bodies as opaque. Inline those predicates **inside** each `TestClaim` `data` record (see `t_pb_b_1_contract_port_cost.dag`) until class-5 data bodies lift the restriction — call this out when Testgen chooses how to factor shared predicates.
 
@@ -24,7 +23,7 @@ Runner wiring for `src/v3/compiler/tests/dag/*.dag` **is** landed (PR #736 — s
 - **(1) Runner accepts the landed layout** — `src/v3/compiler/tests/integration/t_pb_b_1_dag_runner_test.rs` loads each landed `.dag` via `compile_to_dag` and evaluates its `TestSuite` through `TestRunner::run_suite`, asserting every claim reaches `ClaimResult::Pass`. Covers `Compiles`, `FailsWithDiagnostic{TypeMismatch}`, `PortHasState`, and `CostBounded`.
 - **(2) `requires: []` vs `empty()`** — **not equivalent in `data` bodies today.** `data …: TestClaim = { … requires: empty() }` is rejected by M1(2.8) class-5 ("data `…` field `requires` must be a list literal matching the declared `List<_>` type"). Receipt: `test_runner_data_bodies_reject_requires_empty_call_today` in `tests/integration/test_runner_test.rs` pins the diagnostic. The runner path (`src/v3/compiler/tests/dag/*.dag`) must therefore stay on the `[]` literal. `empty()` remains valid in `let` bindings (Brief D `.v3` fixtures), but those bindings are not `Declaration`s and so are not currently `run_suite`-consumable. When M1(2.8) class-5 lifts, the pinned test flips to a positive equivalence proof.
 - **(3) M1(2.8) inline `PortHasState` / `CostBounded`** — proven for the Day-1 predicate shapes on `t_pb_b_1_contract_port_cost.dag`, which inlines both variant literals on each `data …: TestClaim = { … }` record. `t_pb_b_1_pipeline_smoke.dag` / `t_pb_b_1_contract_diagnostic_smoke.dag` likewise inline `Compiles` / `FailsWithDiagnostic`. **Still NYI:** standalone `data _: TestPredicate = PortHasState(…)` / `CostBounded(…)` bodies — same class-5 restriction. Shared-predicate factoring (`let pred_*: TestPredicate = …` in `m1_5_verification_test` style) does not flow through the runner today for the same `Declaration`-vs-`Bind` reason as (2).
-- **(4) First Rust deletion batch** — **still open; prepped, not signed off** (2026-04-24). Candidate inventory (`thesis_validation_test.rs` `Compiles`/`PortHasState`/`CostBounded` subset; `pipe_desugar.rs` excluded — its asserts cover `Transform` target / arity / literal order / return shape, which the `.dag` pipeline smoke does not witness) and the four-point Testgen sign-off guard live in `docs/briefs/r1-testgen-manager.md` → *Hand-off points → Sideways to Self-hosting Manager* (single source). Deletion PRs must not open until a sign-off entry appears in that brief's *Decisions log* naming the specific `#[test]` → `.dag` `TestClaim` mapping.
+- **(4) First Rust deletion batch** — **partial (2026-04-24):** redundant `t_pb_b_1_tests_dag_smoke_test.rs` removed; Testgen sign-off + `#[test]` → `.dag` claim mapping in `docs/briefs/r1-testgen-manager.md` *Decisions log*. **Still open** for the `thesis_validation_test.rs` / `pipe_desugar` inventory (same sign-off guard) until a follow-on log entry names each `#[test]` → `TestClaim` pair.
 
 **Cross-PR coordination — #735 (symbolic cost / `Lookup`).** The landed `CostBounded("answer", Eq, 3)` witness in `t_pb_b_1_contract_port_cost.dag` is the current `cost_of(&dag, &bind.value)` result for `let answer: Int = 1 + 1 + 1 + 1` (three `+` additions). If #735 changes cost-witness semantics (symbolic-cost `Lookup` reshape, operator costing, or the `CostLookup::Hit` path), the `Eq 3` bound must be re-derived against the post-#735 runner output. Same check applies to the Brief D `.v3` sibling (`tests/fixtures/t_pb_b_brief_d/contract_port_cost_smoke.v3`). The runner-backed `t_pb_b_1_dag_runner_test` will fail loudly at `cost N did not satisfy bound 3` if the witness drifts; treat that failure as the #735 re-derivation signal, not a bug in this test.
 

docs/briefs/t-pb-b-brief-d.md

@@ -10,7 +10,7 @@
 
 **Duplicate authority (bounded, P2/P5):** The same three claims exist here (`.v3`, suite names `t-pb-b/…`) and under T-PB-B-1 (`.dag`, suite names `t-pb-b-1/…`). **`.dag` modules are runner-backed** via `t_pb_b_1_dag_runner_test` (PR #736); **Brief D `.v3` fixtures remain compile-smoke only** (`t_pb_b_brief_d_fixture_smoke_test`) until someone intentionally adds runner coverage for the `let`-binding path. **Dissolution trigger (named):** remove or shrink the `.v3` copies once Testgen accepts `src/v3/compiler/tests/dag/t_pb_b_1_*.dag` as the single maintained source for those claims—until then, any edit to claim text must keep both paths aligned (each `.v3` file header points at its `.dag` sibling, including the runner-evaluated `CostBounded` witness value).
 
-**T-PB-B-1 (landed `.dag` home):** `src/v3/compiler/tests/dag/*.dag` + `docs/briefs/t-pb-b-1.md` + `t_pb_b_1_tests_dag_smoke_test` (compile smoke) + `t_pb_b_1_dag_runner_test` (runner-backed predicate evaluation; PR #736) — first batch as **`data` declarations** in real `.dag` modules. Rust-integration-test deletion is still gated on Testgen.
+**T-PB-B-1 (landed `.dag` home):** `src/v3/compiler/tests/dag/*.dag` + `docs/briefs/t-pb-b-1.md` + `t_pb_b_1_dag_runner_test` (runner-backed predicate evaluation; PR #736) — first batch as **`data` declarations** in real `.dag` modules. The former `t_pb_b_1_tests_dag_smoke_test` compile-only harness is retired (redundant). Further Rust-integration-test deletion per inventory remains gated on Testgen (see *Decisions log* in `docs/briefs/r1-testgen-manager.md`).
 
 ---
 
@@ -100,7 +100,7 @@ Paths are modules under `src/v3/compiler/tests/` unless noted. Primary classific
 | `sg6_hand_authored_census_test` | Meta | A | |
 | `sg7_prep_variant_payload_freshness_test` | Pipeline / prep | D + G | |
 | `t_pb_b_brief_d_fixture_smoke_test` | Fixture host | A | Intentionally thin: only verifies Brief D `.v3` fixtures compile. |
-| `t_pb_b_1_tests_dag_smoke_test` | T-PB-B-1 `tests/dag/` host | A | Compile smoke for landed `.dag` `TestClaim` modules (`src/v3/compiler/tests/dag/`). |
+| `t_pb_b_1_dag_runner_test` | T-PB-B-1 `tests/dag/` host | A + D | Runner-backed; former `t_pb_b_1_tests_dag_smoke_test` **retired** (redundant). |
 | `thesis_parallelism_test` | Contract (thesis) | D + G | |
 | `thesis_validation_test` | Contract (thesis) | D + G | |
 

docs/invariants/l-8-lens-rust-surfaces-preserve-typed-failure-carriers.md

@@ -54,9 +54,9 @@ 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.
+Zero matches required. Lens wrappers return typed carriers. (The
+retired `lens_depth.rs` observational helper is deleted — no
+remaining `.dag` migration carve-out.)
 
 **Origin:** Half A review feedback (2026-04-17) + round 1a.3
 prose/ratchet alignment. Full design:

docs/invariants/layer-opacity.md

@@ -201,7 +201,7 @@ proposed:**
   flat list.
 - **Thesis-native.** The lens uses existing v3 infrastructure
   (reader lens over Dag, same shape as `lens_provenance`,
-  `lens_depth`, `lens_cost`). No new machinery.
+  `lens_cost`; `lens_depth` was a retired M0 experiment). No new machinery.
 - **Generalizes to other invariants.** The lens framework
   extends to every testable invariant over a DAG — scaffold
   boundaries, fail-closed discipline, structural duplication,