R3 gate #7: regen_lens_dot_rs_retired (T-LensProducer-Retirement)

INVARIANTS.md

@@ -362,7 +362,6 @@ Per **Dispatch-Discipline Mechanisms (b)**, each path in `EXPECTED_HAND_AUTHORED
 | `src/v3/compiler/src/bin/gunbc_ci.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** + **T-Workflow-As-Data** — `bin/gunbc_ci` host shim for modeled CI (`dsl/gunbc/ci.dag`). **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when CI selection + receipts are emitted/invoked without a hand `main` (`SELF_HOSTING.md` §2.2). **Interim ratchet:** `gunbc_ci` integration tests + SG-0 census. |
 | `src/v3/compiler/src/bin/r1c_e_emit_gates.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** / R1C-E emit gates (`docs/r3-program-plan.md` T-Emit `.dag` `TestClaim` lane). **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when emit-gate checks are invoked only from generated/bootstrap harness without this bin. **Interim ratchet:** `r1c_e_gates.rs` shared checks + integration harness. |
 | `src/v3/compiler/src/bin/regen_bootstrap.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — regen **bootstrap** stage host entry (`dsl/gunbc/regen*.dag` family). **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when bootstrap regen is a single declared pipeline command with no parallel Rust `main`. **Interim ratchet:** `regen_bootstrap_emit.rs` + bootstrap snapshot CI. |
-| `src/v3/compiler/src/bin/regen_lens.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — regen **lens** stage host entry. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when lens regen is pipeline-only. **Interim ratchet:** `regen_lens` + lens regen integration tests. |
 | `src/v3/compiler/src/bin/regen_parse.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — regen **parse** stage host entry. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when parse regen is pipeline-only. **Interim ratchet:** `regen_parse_emit.rs` + parse regen tests. |
 | `src/v3/compiler/src/bin/regen_parse_tables.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — regen **parse tables** stage host entry. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when parse-tables regen is pipeline-only. **Interim ratchet:** `regen_parse_tables_emit.rs` + tables regen tests. |
 | `src/v3/compiler/src/bin/regen_tokenize.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — regen **tokenize** stage host entry. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when tokenize regen is pipeline-only. **Interim ratchet:** `src/v3/compiler/src/regen_tokenize.rs` + tokenizer tests. |
@@ -406,6 +405,8 @@ Per **Dispatch-Discipline Mechanisms (b)**, each path in `EXPECTED_HAND_AUTHORED
 | `src/v3/compiler/src/r3_fc_lane2_loop_witness.rs` | **ROADMAP:** `ROADMAP.md` — **R3 T-Free-Consequences** / db18 divergence (`docs/design-db18-workflow-effect-carrier.md`); directive scanner until lowering owns `lane2_workflow`. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete per ROADMAP row when lowering attaches loop workflow effects. **Interim ratchet:** auto-loop lens claims in `r3_fc_*` tests. |
 | `src/v3/compiler/src/r3_gate_87_cementing_regen_runner_suites.rs` | **ROADMAP:** same **v3 lens capability honesty pass** / gate #87 closure. **Dissolution:** PB-B-1 gate-#87 harness inventory is generated or reflected as substrate facts (no hand-maintained `R3_GATE_87_CEMENTING_REGEN_SUITES` table); `t_pb_b_1_dag_runner_test`, `cementing_dispatch`, and `r3_gate_87_lens_cementing_regen_receipts_test` consume that single authority. **Interim ratchet:** one merge-visible table shared across those consumers (INVARIANTS P2 single authority). |
 | `src/v3/compiler/src/regen_bootstrap_emit.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — bootstrap regen emit host module. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when emit output is pipeline-only. **Interim ratchet:** regen bootstrap integration tests. |
+| `src/v3/compiler/src/regen_lens_driver.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — regen **lens** stage library (`regen.dag` / `LensRegistryEntry` walk; R3 gate #7 retired `src/bin/regen_lens.rs` from SG-0). **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when lens regen is pipeline-only / emitted from `.dag`. **Interim ratchet:** `regen_lens` bin + lens regen integration tests. |
+| `src/v3/compiler/src/regen_lens_entry.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — thin Cargo `[[bin]] regen_lens` host entry (R3 gate #7 `regen_lens_dot_rs_retired`). **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when PB-1 emits bin `main` from `.dag` `BinShim` without hand Rust. **Interim ratchet:** `regen_lens` CLI smoke + integration tests. |
 | `src/v3/compiler/src/regen_parse_emit.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — parse regen emit host module. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when emit output is pipeline-only. **Interim ratchet:** parse regen tests. |
 | `src/v3/compiler/src/regen_parse_tables_emit.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — parse-tables regen emit host module. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when emit output is pipeline-only. **Interim ratchet:** parse-tables regen tests. |
 | `src/v3/compiler/src/regen_tokenize.rs` | **ROADMAP:** `ROADMAP.md` § **T-PB-A** — tokenizer regen emit host module. **PR receipt (P5 Mechanism (b)):** this row + census line same PR. **Dissolution:** delete when emit output is pipeline-only. **Interim ratchet:** tokenizer regen tests. |

scripts/ci-merge/sg0-pr-body-append.3083.txt

@@ -0,0 +1,3 @@
+SG-0 hand-path delta: +1
+
+SG-0 pairing: (a) removed src/v3/compiler/src/bin/regen_lens.rs

src/v3/compiler/Cargo.toml

@@ -61,7 +61,7 @@ required-features = ["bootstrap-regen-fresh"]
 
 [[bin]]
 name = "regen_lens"
-path = "src/bin/regen_lens.rs"
+path = "src/regen_lens_entry.rs"
 
 [[bin]]
 name = "regen_parse"

src/v3/compiler/src/lib.rs

@@ -35,6 +35,7 @@ pub mod lens_t_las_carrier;
 pub mod pb_method_template_projection;
 pub mod r3_gate_87_cementing_regen_runner_suites;
 mod regen_bootstrap_emit;
+pub mod regen_lens_driver;
 pub mod regen_tokenize;
 
 /// SG-0 producer-owned generated-file manifest.

src/v3/compiler/src/bin/regen_lens.rs → src/v3/compiler/src/regen_lens_driver.rs

@@ -1,26 +1,31 @@
-// Unified lens-regen driver. Narrow host shim for
-// `src/v3/compiler/regen.dag`: reads every
-// `data <name>_entry: LensRegistryEntry` record out of the bootstrap
-// Dag, compiles the referenced `.dag` lens, and writes the
-// `emit_rust_module` projection to the declared output path. Adding
-// a new lens is an edit to `regen.dag`, not to this driver.
-//
-// Usage:
-//   cargo run -p v3-compiler --bin regen_lens
-//     → regenerates every lens in the registry.
-//   cargo run -p v3-compiler --bin regen_lens -- --lens cost
-//     → regenerates only the entry whose `name` field is "cost".
+//! Unified lens-regen driver for `src/v3/compiler/regen.dag`.
+//!
+//! Reads every `data <name>_entry: LensRegistryEntry` record out of the
+//! bootstrap `Dag`, compiles the referenced `.dag` lens, and writes the
+//! `emit_rust_module` projection to the declared output path. Adding a new
+//! lens is an edit to `regen.dag`, not to this driver.
+//!
+//! **R3 gate #7 (`regen_lens_dot_rs_retired`):** the former program-sized
+//! `src/bin/regen_lens.rs` shim is retired from the SG-0 hand-authored census.
+//! The `regen_lens` Cargo `[[bin]]` target is the thin `main` in
+//! `src/regen_lens_entry.rs`, which constructs the bootstrap `Dag` once and
+//! delegates here.
+//!
+//! Usage (unchanged for operators):
+//!   cargo run -p v3-compiler --bin regen_lens
+//!   cargo run -p v3-compiler --bin regen_lens -- --lens cost
 
 use std::collections::HashMap;
 use std::env;
-use std::io::{self, Write};
+use std::io::Write;
 use std::path::{Path, PathBuf};
-use std::process::{Command, ExitCode, Stdio};
+use std::process::{Command, Stdio};
 
-use v3_compiler::dag::{Dag, FieldValue, LiteralBits, ValueBody};
-use v3_compiler::emit_rust::emit_rust_module;
-use v3_compiler::generated_files::GENERATED_FILES;
-use v3_compiler::{compile_to_dag, CompileError};
+use crate::dag::{Dag, FieldValue, LiteralBits, ValueBody};
+use crate::emit_rust::emit_rust_module;
+use crate::generated_files::GENERATED_FILES;
+use crate::process_exit::ProcessExit;
+use crate::{compile_to_dag, CompileError};
 
 const LENS_REGISTRY_ENTRY_TYPE: &str = "LensRegistryEntry";
 
@@ -30,20 +35,24 @@ struct Entry {
     generated_file: String,
 }
 
-fn main() -> ExitCode {
-    match run() {
-        Ok(()) => ExitCode::SUCCESS,
-        Err(message) => {
-            let _ = writeln!(io::stderr(), "{message}");
-            ExitCode::FAILURE
-        }
+/// Entry surface for PB-1 bin-shim staging (`ProcessExit` carrier).
+///
+/// `dag` must be the bootstrap `Dag` from `Dag::new()` — the same authority used for
+/// `LensRegistryEntry` enumeration. Call sites store that `Dag` in a local and pass `&dag`
+/// (`let dag = Dag::new(); regen_lens_main(&dag)` in the `regen_lens` bin), not `&Dag::new()`.
+pub fn regen_lens_main(dag: &Dag) -> ProcessExit {
+    match run(dag) {
+        Ok(()) => ProcessExit::ExitSuccess,
+        Err(message) => ProcessExit::ExitFailure {
+            code: 1,
+            reason: message,
+        },
     }
 }
 
-fn run() -> Result<(), String> {
+fn run(dag: &Dag) -> Result<(), String> {
     let requested_name = parse_args()?;
 
-    let dag = Dag::new();
     if !dag.diagnostics().is_empty() {
         return Err(format!(
             "bootstrap Dag carries {} diagnostic(s): {:#?}",
@@ -52,7 +61,7 @@ fn run() -> Result<(), String> {
         ));
     }
 
-    let entries = read_registry(&dag)?;
+    let entries = read_registry(dag)?;
     if entries.is_empty() {
         return Err("lens registry is empty; check `src/v3/compiler/regen.dag`".to_string());
     }

src/v3/compiler/src/regen_lens_entry.rs

@@ -0,0 +1,23 @@
+//! Thin Cargo `[[bin]]` entry for `regen_lens`.
+//!
+//! **R3 gate #7 (`regen_lens_dot_rs_retired`):** keeps the `regen_lens` binary
+//! name and CLI surface stable while retiring the legacy
+//! `src/bin/regen_lens.rs` path from the SG-0 hand-authored census.
+
+use std::io::Write;
+use std::process::ExitCode;
+
+use v3_compiler::dag::Dag;
+use v3_compiler::process_exit::ProcessExit;
+use v3_compiler::regen_lens_driver::regen_lens_main;
+
+fn main() -> ExitCode {
+    let dag = Dag::new();
+    match regen_lens_main(&dag) {
+        ProcessExit::ExitSuccess => ExitCode::SUCCESS,
+        ProcessExit::ExitFailure { code, reason } => {
+            let _ = writeln!(std::io::stderr(), "{reason}");
+            ExitCode::from(code.clamp(1, 255) as u8)
+        }
+    }
+}

src/v3/compiler/src/test_runner.rs

@@ -6728,10 +6728,19 @@ fn sg0_quoted_path_from_line(line: &str) -> Option<String> {
 /// `lens_apply.rs` → `lens_declaration_apply.rs` is a **path** retirement only; the bounded
 /// lens host remains a lens-producer residual until PB-Runtime owns application/reflection
 /// (Row-4 / §7.1). Omitting this path would falsely show census “progress” after a rename.
+///
+/// **R3 gate #7 (`regen_lens_dot_rs_retired`) is not lens-producer dissolution:** retiring
+/// `src/bin/regen_lens.rs` relocates the Cargo `[[bin]]` entry to `regen_lens_entry.rs` and
+/// moves producer logic to `regen_lens_driver.rs`. Both remain hand-authored regen-lens
+/// producer surfaces until PB-1 emits the bin from `.dag` / PB-Runtime owns the pipeline — so
+/// they stay in this subset; shrinking the predicate after a path move would falsely claim
+/// census progress without dissolving the producer.
 fn is_lens_producer_census_path(path: &str) -> bool {
     matches!(
         path,
-        "src/v3/compiler/src/lens_declaration_apply.rs" | "src/v3/compiler/src/bin/regen_lens.rs"
+        "src/v3/compiler/src/lens_declaration_apply.rs"
+            | "src/v3/compiler/src/regen_lens_driver.rs"
+            | "src/v3/compiler/src/regen_lens_entry.rs"
     )
 }
 

src/v3/compiler/tests/integration/r3_lens_producer_retirement_executable_witness_test.rs

@@ -6,11 +6,13 @@
 //! state-check: the `.dag` PB census claim is runnable through `TestRunner`, and
 //! it observes the live lens-producer residual set instead of deferring to a
 //! paper-only receipt. The gate turns green when every path in the
-//! `lens_producer_files_subset_predicate` subset (today: bounded-lens host +
-//! `regen_lens` bin) is retired from the non-test census and this claim returns
-//! `Pass`. **Path rename alone does not drop the residual:** `lens_apply.rs` →
-//! `lens_declaration_apply.rs` is still a lens-producer surface until PB-Runtime
-//! owns lens application end-to-end (ROADMAP / T-PB-A census narrative).
+//! `lens_producer_files_subset_predicate` subset (today: bounded-lens host
+//! `lens_declaration_apply.rs` plus the hand-authored `regen_lens` surfaces
+//! `regen_lens_driver.rs` and `regen_lens_entry.rs` — R3 gate #7 retired only
+//! `src/bin/regen_lens.rs`, not the producer) is retired from the non-test census
+//! and this claim returns `Pass`. **Path rename alone does not drop the residual:**
+//! `lens_apply.rs` → `lens_declaration_apply.rs` is still a lens-producer surface until
+//! PB-Runtime owns lens application end-to-end (ROADMAP / T-PB-A census narrative).
 
 use v3_compiler::compile_to_dag;
 use v3_compiler::test_runner::{ClaimResult, TestRunner};
@@ -20,7 +22,7 @@ const FIXTURE_SOURCE: &str = include_str!("../dag/t_r1c_d_pb_census_gates.dag");
 const FIXTURE_PATH: &str = "src/v3/compiler/tests/dag/t_r1c_d_pb_census_gates.dag";
 const SUITE_NAME: &str = "r1_pb_census_gates_suite";
 const CLAIM_NAME: &str = "lens_producer_files_remaining";
-const CURRENT_RESIDUAL_COUNT: i64 = 2;
+const CURRENT_RESIDUAL_COUNT: i64 = 3;
 
 #[test]
 fn r3_gate_66_lens_producer_retirement_claim_executes_against_live_census() {

src/v3/compiler/tests/integration/r3_substrate_gap_reflection_closure_test.rs

@@ -14,7 +14,7 @@ const FIXTURE_SOURCE: &str = include_str!("../fixtures/r3_substrate_gap_reflecti
 const FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_substrate_gap_reflection_closure.dag";
 const SUITE_NAME: &str = "r3_substrate_gap_reflection_closure_suite";
 const CLAIM_NAME: &str = "substrate_gap_reflection_residual_census_receipt";
-const CURRENT_REFLECTION_RESIDUAL_COUNT: i64 = 2;
+const CURRENT_REFLECTION_RESIDUAL_COUNT: i64 = 3;
 
 #[test]
 fn r3_gate_64_reflection_residual_census_receipt_executes() {

src/v3/compiler/tests/integration/sg0_census_test.rs

@@ -41,6 +41,7 @@ use v3_compiler::generated_files::GENERATED_FILES;
 const CENSUS_ROOT: &str = "src/v3/compiler";
 const RETIRED_LENS_TESTGEN_RS: &str = "src/v3/compiler/src/lens_testgen.rs";
 const RETIRED_LENS_APPLY_RS: &str = "src/v3/compiler/src/lens_apply.rs";
+const RETIRED_REGEN_LENS_BIN_RS: &str = "src/v3/compiler/src/bin/regen_lens.rs";
 
 #[test]
 fn r3_gate_5_lens_apply_rs_stays_retired() {
@@ -68,6 +69,19 @@ fn r3_gate_6_lens_testgen_rs_stays_retired() {
     );
 }
 
+#[test]
+fn r3_gate_7_regen_lens_bin_rs_stays_retired() {
+    let retired_path = workspace_root().join(RETIRED_REGEN_LENS_BIN_RS);
+
+    assert!(
+        !retired_path.exists(),
+        "R3 gate #7 (`regen_lens_dot_rs_retired`) requires \
+         `{RETIRED_REGEN_LENS_BIN_RS}` to stay retired. The `regen_lens` \
+         Cargo bin delegates through `src/regen_lens_entry.rs` into \
+         `regen_lens_driver.rs` until PB-1 emits the shim from `.dag`."
+    );
+}
+
 #[test]
 fn emit_production_code_has_no_declaration_by_name_calls() {
     let manifest_dir = Path::new(env!("CARGO_MANIFEST_DIR"));
@@ -114,9 +128,12 @@ fn emit_production_code_has_no_declaration_by_name_calls() {
 // (`regen_lens_cost.rs`, `regen_lens_cost_symbolic.rs`,
 // `regen_lens_structural_resolution.rs`, `regen_lens_unused_parameters.rs`)
 // and SG-4 prep's `regen_infer_helpers.rs` all folded into a single
-// `regen_lens.rs` shim driven by `src/v3/compiler/regen.dag`'s
+// unified `regen_lens` driver driven by `src/v3/compiler/regen.dag`'s
 // `LensRegistryEntry` records. Five retirements; one net-new entry
-// (`regen_lens.rs`). The new `sg6_hand_authored_census_test.rs`
+// at the time (`src/bin/regen_lens.rs`). **R3 gate #7** (`regen_lens_dot_rs_retired`,
+// 2026-05-14): that program-sized bin path retired; logic lives in
+// `regen_lens_driver.rs` with a thin `regen_lens_entry.rs` `[[bin]]` shell.
+// The new `sg6_hand_authored_census_test.rs`
 // pins the reduced bin census + full `(name, lens_file,
 // generated_file)` registry tuples + `--lens` singleton resolve +
 // end-to-end CLI smoke; it is hand-authored test infrastructure and
@@ -262,7 +279,6 @@ const EXPECTED_HAND_AUTHORED_NON_TEST: &[&str] = &[
     "src/v3/compiler/src/bin/gunbc_ci.rs",
     "src/v3/compiler/src/bin/r1c_e_emit_gates.rs",
     "src/v3/compiler/src/bin/regen_bootstrap.rs",
-    "src/v3/compiler/src/bin/regen_lens.rs",
     "src/v3/compiler/src/bin/regen_parse.rs",
     "src/v3/compiler/src/bin/regen_parse_tables.rs",
     "src/v3/compiler/src/bin/regen_tokenize.rs",
@@ -333,6 +349,8 @@ const EXPECTED_HAND_AUTHORED_NON_TEST: &[&str] = &[
     // `tests/dag/t_r3_gate_87_cementing_regen_*.dag` (INVARIANTS P2 single authority).
     "src/v3/compiler/src/r3_gate_87_cementing_regen_runner_suites.rs",
     "src/v3/compiler/src/regen_bootstrap_emit.rs",
+    "src/v3/compiler/src/regen_lens_driver.rs",
+    "src/v3/compiler/src/regen_lens_entry.rs",
     "src/v3/compiler/src/regen_parse_emit.rs",
     "src/v3/compiler/src/regen_parse_tables_emit.rs",
     "src/v3/compiler/src/regen_tokenize.rs",

src/v3/compiler/tests/integration/sg6_hand_authored_census_test.rs

@@ -167,9 +167,9 @@ fn sg6_bin_census_is_locked_to_expected_regen_shims() {
         // checks without a host child, the wrappers + bin retire together
         // (R1 Closure dispatch on issue #973). Documented in ROADMAP T-Emit
         // / R1C-E lane row.
+        "gunbc_ci.rs",
         "r1c_e_emit_gates.rs",
         "regen_bootstrap.rs",
-        "regen_lens.rs",
         "regen_parse.rs",
         // SG-2c-1 grammar-tables prototype: `regen_parse_tables` projects
         // `src/v3/compiler/parse_tables.dag` into
@@ -192,11 +192,12 @@ fn sg6_bin_census_is_locked_to_expected_regen_shims() {
     assert_eq!(
         actual, expected,
         "SG-6 hand-authored bin census changed. The census is \
-         `r1c_e_emit_gates` (R1C-E T-Emit `.dag` wrapper logical child; \
-         issue #973), `regen_lens` (reads `src/v3/compiler/regen.dag`), \
-         `regen_parse` (reads `src/v3/std/parse_surface.dag` for Surface \
+         `gunbc_ci` (modeled CI host shim), `r1c_e_emit_gates` (R1C-E T-Emit `.dag` wrapper logical child; \
+         issue #973), `regen_parse` (reads `src/v3/std/parse_surface.dag` for Surface \
          carriers), `regen_tokenize` (reads `src/v3/compiler/tokenize.dag`), \
-         `regen_v3`, and `self_host_fixed_point`. Adding a new bin re-introduces a \
+         `regen_v3`, and `self_host_fixed_point`. The `regen_lens` binary is a \
+         thin `[[bin]]` outside `src/bin/` (R3 gate #7); its driver lives in \
+         `regen_lens_driver.rs`. Adding a new bin re-introduces a \
          per-lens (or per-target) Rust driver — the SG-6 lane requires that \
          new regen / harness targets be added via a `.dag` registry instead. \
          Both `src/bin/<name>.rs` (flat-file bins; basename reported) and \

src/v3/compiler/tests/integration/test_runner_test.rs

@@ -646,7 +646,7 @@ data suite: TestSuite = {
     );
     assert_fail_contains(
         "lens_producer_files_remaining",
-        "lens-producer subset observed 2",
+        "lens-producer subset observed 3",
     );
     assert_eq!(
         result_for("pb_self_compile_fixed_point"),