feat(v3): R1 Lane A — LaneE gates, mock-backed runner, T-Demo lens + impossible-bug suites

ROADMAP.md

@@ -61,15 +61,15 @@ This section lists gate names + schema-compilability tags; full `TestClaim` decl
 - **T-P0.** `p0_repeat_string_correct` [Day 1] · `p0_no_fabrication_sentinel` [ext] · `p0_rest_ops_aligned` [ext]
 - **T-Sub.** `sub_match_over_user_sum` [Day 1, landed PR #702] · `sub_type_alias_where_lowers` [ext, landed PR #703] · ~~`sub_charclass_in_std_unicode`~~ — phase-1 landed PR #693; **phase-2 reclassified to R2 substrate-capability** (top-level `ValueBody` list/sum + `std.unicode` bootstrap/load-set per Class 5 Gap 3 row below) — no longer an R1 T-Sub gate; tracked in `docs/r2-structure.md` Goal 3 / T-Substrate as a 4th scoped sub-lane (consumer: tokenizer)
 - **T-Emit.** `emit_rust_fixtures_rustc_green` [ext: `ExecuteCommand`] · `emit_generic_bounds_survive` [ext] · `emit_omni_demo_fixtures_green` [ext: `ForAllTargets` + `ExecuteCommand`]
-- **T-LaneE.** `complexity_merge_sort_is_nlogn` [ext: `LensOutputEquals`] · `complexity_v3_matches_v2_oracle` [ext: `DifferentialEquals`]
-- **T-TestGen.** `testgen_structural_coverage` [ext] · `testgen_mock_backed_integration_safe` [ext: `MockBackedInvariant` wiring] · `testgen_manual_claim_is_first_class` [ext] — T-TestGen also owns scoping the predicate shape for `[ext]` gates that other lanes consume; currently includes `lens_producer_files_remaining` for T-PB-A (enumeration declared in `sg0_census_test.rs` at scoping time).
+- **T-LaneE.** `complexity_merge_sort_is_nlogn` [ext: `LensOutputEquals`] · `complexity_merge_sort_v3_matches_v2_oracle` [ext: `DifferentialEquals`] · `lane_e_bundled_witness_host_emit_parity` [ext: `DifferentialEquals`]
+- **T-TestGen.** `testgen_structural_coverage` [ext] · `testgen_mock_backed_integration_safe` [ext: `MockBackedInvariant` — runner `NotYetImplemented` until `TestClaim.requires` carries at least one `ResourceReference`; M1(2.8) fixture list bodies) · `testgen_manual_claim_is_first_class` [ext] — T-TestGen also owns scoping the predicate shape for `[ext]` gates that other lanes consume; currently includes `lens_producer_files_remaining` for T-PB-A (enumeration declared in `sg0_census_test.rs` at scoping time).
 - **T-LensAPI.** `user_authored_lens_compiles` [Day 1] · `lens_composition_associative` [ext: `AlgebraicLaw`] · `lens_output_is_queryable_data` [ext]
 - **T-PB-A.** `pb_hand_rust_at_shim_floor` [ext] · `lens_producer_files_remaining` [ext — priority slice of the non-test census: hand-Rust files implementing lens producers, drops as each migrates to `.dag`; enumeration declared in `sg0_census_test.rs` when T-TestGen scopes the predicate] · `pb_self_compile_fixed_point` [ext] · `pb_compiler_std_ratchet_zero` [ext] — live baselines read from authorities; not frozen in this doc. Hand-Rust (**non-test subset**): SG-0 census (file-level + fragments ratchet) minus the test subset owned by T-PB-B → ≤5 irreducible-shim per `docs/design-pure-bootstrap.md`. Consolidation ratchet: compiler-local types not in positive-def set → 0.
 - **T-PB-B.** `pb_test_file_generated_from_dag` [ext] · `pb_rust_tests_outside_residual_zero` [ext] — the first gates the pipeline-equivalent suite; the second gates the outcome: zero Rust-authored tests exist outside the `TESTING.md §"Post-R2 shape"` residual (compiler-internal unit tests + external-toolchain boundary tests). Single-file generation is insufficient proof of the lane's end-state.
 - **T-Demo.**
   - `fixture_compiler_nerd_canonical` [Day 1 (Compiles) / ext (lens-output demos)] — demonstrates: complexity, ownership, parallelism
   - `fixture_integration_canonical` [Day 1 (Compiles) / ext (lens-output demos)] — demonstrates: effects, idempotency, testgen
-  - `impossible_bug_class_suite_r1` [ext] — three classes demoed: idempotency-violation, suboptimal-complexity, transport/type-drift. Remaining three (nested-optional flatten, unhandled diagnostic paths, unenumerated effects) are tagged **[R2+]** in THESIS — thesis-committed but not scheduled to a specific release. THESIS §"Enumerable impossible-bug classes" is the authority on scheduling tags.
+  - `impossible_bug_class_suite_r1` [ext] — idempotency-violation (`compose_effects` + breaking `AppendEffect` under `IsIdempotent` → `ResolveError`), transport/type-drift (`TypeMismatch`) — all `Pass` claims (`FailsWithDiagnostic` only). Suboptimal-complexity vs structural `cost_of` lives in `t_demo_structural_cost_obligation_suite` (`CostBounded` receipt is runner `Fail`, asserted in integration). Remaining three (nested-optional flatten, unhandled diagnostic paths, unenumerated effects) are tagged **[R2+]** in THESIS — thesis-committed but not scheduled to a specific release. THESIS §"Enumerable impossible-bug classes" is the authority on scheduling tags.
   - `demo_user_authored_lens_rejects_violating_program` [ext] — operationalizes THESIS §"User-defined dimensions". Demo shows a user-written lens (~20 lines of `.dag`; e.g., "max external HTTP calls per workflow") rejecting a program that violates it, alongside the built-in complexity lens. Proves the ceiling of what gunbc can prove is user-extensible, not compiler-baked. Consumes `user_authored_lens_compiles` from T-LensAPI.
 
 **T-Demo scoping note.** All lanes ship features whole (no compromise per §Goals). T-Demo curates the R1 *narrative* — fixtures and impossible-bug demos selected for visceral audience impact, not exhaustive feature coverage. Audience curation is demo-scoping; feature shipment is lane-scoping.
@@ -84,6 +84,8 @@ Day-1 PR #717 landed explicit `LensOutputEquals` dispatch and fixtures with **no
 
 3. **P2 parallel lens text** — **Done (D4):** `v3-compiler/build.rs` splices `src/v3/lenses/named_function_count.dag` into generated `r1_gates.dag` from hand-edited `r1_gates.template.dag`; `m1_5_user_authored_lens_gate_test` still ratchets lowered `source` against `include_str!(.../named_function_count.dag)`. **Follow-on:** dissolve fixture-local `fn count_named_bind` / `fn named_function_count` stubs when `DeclarationRef` can resolve the lens from `program_dag` alone; optional same treatment for `lens_composition_associative_gate.source` vs `lens_composition_associative_witness.dag`.
 
+4. **PR #764 T-LaneE / test-runner scaffolds (meta-review `efbb9787`, SHIP_WITH_DEBT)** — Ingested 2026-04-25: do **not** re-litigate these as ad-hoc PR nits; track dissolution here. Checklist: structural `TestClaim` bind / input carriers (retire `cost_bind_for_claim_file` + `r1_lens_output_input_from_program` string keying, M1(2.8)); D1 `apply_lens_declaration(cost_of)` then delete `lane_e_host_*`; `Lookup<Int>` literals in `data` bodies; DB-15 `requires` with real `ResourceReference` rows for mock-backed `Pass` (until then NYI on empty `requires` is intentional); optional `.dag`-native failed-obligation predicate for T-Demo structural cost. **Receipt shape today:** `complexity_merge_sort_v3_matches_v2_oracle` is `DifferentialEquals` on `merge_sort_out` (`r1_merge_sort_pair.v3`); `lane_e_bundled_witness_host_emit_parity` is the bundled `lane_e_diff_out` witness (`r1_lane_e_differential_witness.v3` — `match` / list / `fold`, not the early `1+2` smoke).
+
 ### Dependency DAG
 
 ```

docs/briefs/r1-release-manager.md

@@ -168,8 +168,9 @@ Lane-owner dispatch status (update as sub-deliverables close):
     Trigger remains
     **half-met** until the runner actually evaluates a mock-backed
     invariant claim, not just routes it.
-  - Substrate T-LaneE (`complexity_merge_sort_is_nlogn` /
-    `complexity_v3_matches_v2_oracle`) — pending.
+  - Substrate T-LaneE (`complexity_merge_sort_is_nlogn`,
+    `complexity_merge_sort_v3_matches_v2_oracle`,
+    `lane_e_bundled_witness_host_emit_parity` — `r1_lane_e_suite`) — landed PR #764; dissolution checklist ROADMAP `Scheduled cleanups` item 4.
   - Surface T-Emit (`emit_omni_demo_fixtures_green`) — pending.
   - PR #689 closed as premature (docs/thesis/ is director-owned per
     `doc-authority.md`). Narrative holds until at least one upstream

docs/briefs/r1-testgen-manager.md

@@ -227,9 +227,9 @@ Lane-owner dispatch status (update as sub-deliverables close):
 - [x] `ExecuteCommand` predicate (Surface T-Emit consumer) — landed PR #678
 - [x] `ForAllTargets` predicate (Surface T-Emit consumer) — landed PR #678
 - [x] `LensOutputEquals` predicate (Substrate T-LaneE consumer
-      — `complexity_merge_sort_is_nlogn`) — landed PR #678
+      — `complexity_merge_sort_is_nlogn`) — landed PR #764 (suite: `r1_lane_e_suite`)
 - [x] `DifferentialEquals` predicate (Substrate T-LaneE consumer
-      — `complexity_v3_matches_v2_oracle`) — landed PR #678
+      — `complexity_merge_sort_v3_matches_v2_oracle`, `lane_e_bundled_witness_host_emit_parity`) — landed PR #764
 
 Decisions log (append as they happen):
 

docs/r2-structure.md

@@ -25,7 +25,7 @@ Post-R2 is external work (adoption, documentation, community, ecosystem modeling
 
 ## Goals
 
-**Gate-ownership discipline.** Every R1 gate listed in `ROADMAP.md §"Lane acceptance — .dag gates"` closes in R1 under the locked all-R1-gates-green criterion (see R1 closure criteria below). That means concerns gated there — **lens purity** (`lens_producer_files_remaining` on T-PB-A via PR #752), **self-hosting shim-floor close** (T-PB-A `pb_hand_rust_at_shim_floor` + `pb_compiler_std_ratchet_zero` + T-PB-B `pb_rust_tests_outside_residual_zero`), and **E-family carrier port closure** (the T-LaneE critical path enabling `complexity_merge_sort_is_nlogn` + `complexity_v3_matches_v2_oracle`) — are **R1 scope, not R2**. R2 does not duplicate release authority over gates ROADMAP already assigns to R1 lanes.
+**Gate-ownership discipline.** Every R1 gate listed in `ROADMAP.md §"Lane acceptance — .dag gates"` closes in R1 under the locked all-R1-gates-green criterion (see R1 closure criteria below). That means concerns gated there — **lens purity** (`lens_producer_files_remaining` on T-PB-A via PR #752), **self-hosting shim-floor close** (T-PB-A `pb_hand_rust_at_shim_floor` + `pb_compiler_std_ratchet_zero` + T-PB-B `pb_rust_tests_outside_residual_zero`), and **E-family carrier port closure** (the T-LaneE critical path enabling `complexity_merge_sort_is_nlogn` + `complexity_merge_sort_v3_matches_v2_oracle` + `lane_e_bundled_witness_host_emit_parity`) — are **R1 scope, not R2**. R2 does not duplicate release authority over gates ROADMAP already assigns to R1 lanes.
 
 Under that discipline, R2's goals are the Tier-1 thesis claims that are *not* gated in R1 today:
 
@@ -87,7 +87,7 @@ Continues `docs/briefs/grounding-manager.md` (refreshed for R2 scope on promotio
 **Lanes deliberately absent (R1 gates, closed by R1 lane acceptance):**
 - T-LensMigration / `lens_producer_files_remaining` — R1 T-PB-A gate per PR #752.
 - T-ShimFloor / `pb_hand_rust_at_shim_floor` / `pb_compiler_std_ratchet_zero` / `pb_rust_tests_outside_residual_zero` — R1 T-PB-A + T-PB-B gates.
-- T-EFamilyClose — R1 T-LaneE's critical-path carrier work (E-T, E-C, E-I, E-P, E-M sub-lanes), enabling the R1 `complexity_merge_sort_is_nlogn` + `complexity_v3_matches_v2_oracle` gates. All E-family carrier-port work closes in R1; only the §6a metadata-pick residual inherits to R2 (Goal 5).
+- T-EFamilyClose — R1 T-LaneE's critical-path carrier work (E-T, E-C, E-I, E-P, E-M sub-lanes), enabling the R1 `complexity_merge_sort_is_nlogn` + `complexity_merge_sort_v3_matches_v2_oracle` + `lane_e_bundled_witness_host_emit_parity` gates. All E-family carrier-port work closes in R1; only the §6a metadata-pick residual inherits to R2 (Goal 5).
 - T-TestGen-tail (`testgen_mock_backed_integration_safe` / `MockBackedInvariant` wiring) — R1 T-TestGen gate per `ROADMAP.md §"Lane acceptance — .dag gates"`. Closes in R1.
 
 R2 does not re-own any of the above; under all-R1-gates-green R1 closure, those gates ARE the close conditions and R2 inherits nothing there — with two named exceptions:

src/v3/compiler/build.rs

@@ -123,8 +123,8 @@ fn collect_dag_entries_impl(dir: &Path, prioritized: &[&str], recursive: bool) -
     entries
 }
 
-/// Escape `body` so it can replace the `R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1` placeholder
-/// inside a `.dag` double-quoted `TestClaim.source` literal (T-LensAPI D4 fixture splice).
+/// Escape `body` so it can replace a `*_SPLICE_V1` placeholder inside a `.dag` double-quoted
+/// `TestClaim.source` literal (R1 gate fixture hygiene; see `emit_r1_gates_fixture`).
 fn escape_dag_double_quoted_body(body: &str) -> String {
     let mut out = String::with_capacity(body.len() + 8);
     for ch in body.chars() {
@@ -140,21 +140,36 @@ fn escape_dag_double_quoted_body(body: &str) -> String {
     out
 }
 
-/// Emit `tests/fixtures/r1_gates.dag` from `r1_gates.template.dag` + canonical lens text.
+/// Emit `tests/fixtures/r1_gates.dag` from `r1_gates.template.dag` + canonical lens and `.v3`
+/// program text.
 ///
 /// **Hygiene:** `r1_gates.dag` is tracked in git but produced here so the spliced lens stays
-/// byte-identical to `src/v3/lenses/named_function_count.dag`. Hand-edit **`r1_gates.template.dag`**
-/// only — direct edits to `r1_gates.dag` are overwritten on the next `cargo build`. We skip
-/// `fs::write` when the generated bytes are unchanged to avoid spurious working-tree noise.
+/// byte-identical to `src/v3/lenses/named_function_count.dag`, and Lane E `TestClaim.source`
+/// strings are spliced from canonical `.v3` fixtures (single authority; INVARIANTS P2).
+/// Hand-edit **`r1_gates.template.dag`** only — direct edits to `r1_gates.dag` are overwritten
+/// on the next `cargo build`. We skip `fs::write` when the generated bytes are unchanged to
+/// avoid spurious working-tree noise.
 fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) {
-    /// Must appear exactly once in `r1_gates.template.dag` (the `TestClaim.source` line only).
-    const SPLICE_SENTINEL: &str = "R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1";
-    let template_path = manifest_path.join("tests/fixtures/r1_gates.template.dag");
+    /// Must appear exactly once in `r1_gates.template.dag` (inside the `user_authored_lens_compiles` `source:` line).
+    const LENS_SPLICE_SENTINEL: &str = "R1_NAMED_FUNCTION_COUNT_LENS_SPLICE_V1";
+    /// May appear multiple times (each `TestClaim.source` that embeds merge-sort gets the same bytes).
+    const MERGE_SORT_PAIR_V3_SPLICE: &str = "R1_MERGE_SORT_PAIR_V3_SPLICE_V1";
+    const LANE_E_DIFF_WITNESS_V3_SPLICE: &str = "R1_LANE_E_DIFFERENTIAL_WITNESS_V3_SPLICE_V1";
+
+    let fixtures_dir = manifest_path.join("tests/fixtures");
+    let template_path = fixtures_dir.join("r1_gates.template.dag");
     let lens_path = v3_dir.join("lenses/named_function_count.dag");
-    let out_path = manifest_path.join("tests/fixtures/r1_gates.dag");
+    let merge_sort_pair_v3 = fixtures_dir.join("r1_merge_sort_pair.v3");
+    let lane_e_diff_witness_v3 = fixtures_dir.join("r1_lane_e_differential_witness.v3");
+    let out_path = fixtures_dir.join("r1_gates.dag");
 
     println!("cargo:rerun-if-changed={}", template_path.display());
     println!("cargo:rerun-if-changed={}", lens_path.display());
+    println!("cargo:rerun-if-changed={}", merge_sort_pair_v3.display());
+    println!(
+        "cargo:rerun-if-changed={}",
+        lane_e_diff_witness_v3.display()
+    );
 
     let template = fs::read_to_string(&template_path).unwrap_or_else(|e| {
         panic!(
@@ -170,15 +185,53 @@ fn emit_r1_gates_fixture(manifest_path: &Path, v3_dir: &Path) {
             e
         )
     });
-    let splice_count = template.matches(SPLICE_SENTINEL).count();
-    if splice_count != 1 {
+    let merge_sort_pair_src = fs::read_to_string(&merge_sort_pair_v3).unwrap_or_else(|e| {
+        panic!(
+            "failed to read R1 merge-sort pair fixture {}: {}",
+            merge_sort_pair_v3.display(),
+            e
+        )
+    });
+    let lane_e_diff_src = fs::read_to_string(&lane_e_diff_witness_v3).unwrap_or_else(|e| {
+        panic!(
+            "failed to read R1 Lane E differential witness fixture {}: {}",
+            lane_e_diff_witness_v3.display(),
+            e
+        )
+    });
+
+    let lens_count = template.matches(LENS_SPLICE_SENTINEL).count();
+    if lens_count != 1 {
         panic!(
-            "{} must contain exactly one `{SPLICE_SENTINEL}` (found {splice_count})",
+            "{} must contain exactly one `{LENS_SPLICE_SENTINEL}` for named_function_count lens (found {lens_count})",
             template_path.display()
         );
     }
-    let escaped = escape_dag_double_quoted_body(&lens);
-    let generated = template.replace(SPLICE_SENTINEL, &escaped);
+    let merge_count = template.matches(MERGE_SORT_PAIR_V3_SPLICE).count();
+    if merge_count < 1 {
+        panic!(
+            "{} must contain at least one `{MERGE_SORT_PAIR_V3_SPLICE}` (spliced into every Lane E claim that embeds merge-sort; found {merge_count})",
+            template_path.display()
+        );
+    }
+    let diff_count = template.matches(LANE_E_DIFF_WITNESS_V3_SPLICE).count();
+    if diff_count != 1 {
+        panic!(
+            "{} must contain exactly one `{LANE_E_DIFF_WITNESS_V3_SPLICE}` for r1_lane_e_differential_witness.v3 (found {diff_count})",
+            template_path.display()
+        );
+    }
+
+    let mut generated =
+        template.replace(LENS_SPLICE_SENTINEL, &escape_dag_double_quoted_body(&lens));
+    generated = generated.replace(
+        MERGE_SORT_PAIR_V3_SPLICE,
+        &escape_dag_double_quoted_body(&merge_sort_pair_src),
+    );
+    generated = generated.replace(
+        LANE_E_DIFF_WITNESS_V3_SPLICE,
+        &escape_dag_double_quoted_body(&lane_e_diff_src),
+    );
     let needs_write = match fs::read_to_string(&out_path) {
         Ok(existing) => existing != generated,
         Err(_) => true,

src/v3/compiler/src/lower.rs

@@ -4989,10 +4989,17 @@ fn lower_expr(
                     })
                     .into_iter()
                     .collect();
+                let diagnostic_name = match expected_decl {
+                    Some(exp) if walk_to_disj_decl(dag, exp).is_some() => format!(
+                        "named constructor `{target}` is not a variant of the expected sum type `{}`",
+                        declaration_display_name(dag, exp)
+                    ),
+                    _ => target.clone(),
+                };
                 dag.mark_unresolved(
                     port,
                     Diagnostic::ResolveError {
-                        name: target.clone(),
+                        name: diagnostic_name,
                         span: span.clone(),
                         fixes,
                     },