R3 gate #47: auto loop parallelism unproven falls back sequential

src/v3/compiler/src/test_runner.rs

@@ -44,8 +44,18 @@ const TC1_SUBSTRATE_LENS_ETA_DEFERRED_FIXTURE: &str =
 /// `canonical_lens_name_dispatch_arms_pinned` does not treat this as a new string-literal name
 /// dispatch arm on the canonical lens bridge (see disposition:
 /// `docs/briefs/r2-pb-canonical-lens-bridge-disposition.md`).
+///
+/// **Deferral receipt:** structural proxy dissolves when ordinary lens output consumes DB-20
+/// workflow parallelism data (`ROADMAP.md` § Active deferrals → `DB-20`; `docs/db-history/db-20.md`).
 const R3_PARALLEL_EMIT_WITNESS_LENS_NAME: &str = "r3_auto_parallelism_parallel_emit_witness";
 
+/// R3 gate #47 (`LensOutputEquals` witness in `r3_free_consequences_second_batch.dag`).
+///
+/// Compared by declaration-name matching like `R3_PARALLEL_EMIT_WITNESS_LENS_NAME`.
+/// **Deferral receipt:** `ROADMAP.md` § Active deferrals → `DB-20`; see repository `docs/db-history/db-20.md`.
+const R3_AUTO_LOOP_SEQUENTIAL_EMIT_WITNESS_LENS_NAME: &str =
+    "r3_auto_loop_parallelism_sequential_emit_witness";
+
 /// R3 gate #45 (`LensOutputEquals` witness in `r3_free_consequences_first_batch.dag`).
 ///
 /// Compared as `Some(R3_BRANCH_ARMS_SERIALIZE_WITNESS_LENS_NAME)` — **not** `Some("…")` inline —
@@ -2349,7 +2359,8 @@ impl<'a> TestRunner<'a> {
 
         // R3 gate #43 (`auto_parallelism_independent_binds_emit_parallel`): independent top-level
         // binds must emit a parallel Rust schedule (`std::thread::scope`). Structural witness via
-        // program text — dissolution when ordinary DB-20 parallelism lens output reaches `.dag`.
+        // program text — dissolution when ordinary DB-20 parallelism lens output reaches `.dag`
+        // (ROADMAP.md § Active deferrals → DB-20; docs/db-history/db-20.md).
         if lens_decl.name.as_deref() == Some(R3_PARALLEL_EMIT_WITNESS_LENS_NAME) {
             let expected_int = match expected_decl.value_body.as_ref() {
                 Some(ValueBody::Scalar(LiteralBits::Int(s))) => match s.parse::<i64>() {
@@ -2387,6 +2398,51 @@ impl<'a> TestRunner<'a> {
             };
         }
 
+        // R3 gate #47 (`auto_loop_parallelism_unproven_falls_back_sequential`): without
+        // `Lens<Iteration-Independence>` opt-in, lowering must not apply heuristic parallel loop
+        // scheduling. Structural proxy until DB-20 carries loop scheduling in the ordinary lens
+        // surface (ROADMAP.md § Active deferrals → DB-20; docs/db-history/db-20.md;
+        // docs/design-db20-lane2-stage2e-parallelism-lens.md): emitted Rust must not use the same
+        // `std::thread::scope` batch path as pairwise-independent top-level binds.
+        // TODO(DB-20): replace whole-program `thread::scope` substring checks with a marker scoped to
+        // the emitted loop/bind scheduling site once the producer lands.
+        if lens_decl.name.as_deref() == Some(R3_AUTO_LOOP_SEQUENTIAL_EMIT_WITNESS_LENS_NAME) {
+            let expected_int = match expected_decl.value_body.as_ref() {
+                Some(ValueBody::Scalar(LiteralBits::Int(s))) => match s.parse::<i64>() {
+                    Ok(v) => v,
+                    Err(_) => {
+                        return ClaimResult::Fail(format!(
+                            "LensOutputEquals(r3_auto_loop_parallelism_sequential_emit_witness): expected Int literal is not a valid i64 decimal for `{expected_name}`"
+                        ));
+                    }
+                },
+                _ => {
+                    return ClaimResult::Fail(format!(
+                        "LensOutputEquals(r3_auto_loop_parallelism_sequential_emit_witness): expected_ref `{expected_name}` must be `data …: Int = <literal>`"
+                    ));
+                }
+            };
+            let emitted = match crate::emit_rust::emit_rust(&program_dag) {
+                Ok(s) => s,
+                Err(err) => {
+                    return ClaimResult::Fail(format!(
+                        "LensOutputEquals(r3_auto_loop_parallelism_sequential_emit_witness): emit_rust failed for `{}`: {err:?}",
+                        claim.file_name
+                    ));
+                }
+            };
+            let parallel_scope_batch = emitted.contains("thread::scope");
+            let computed_int = i64::from(!parallel_scope_batch);
+            return if computed_int == expected_int {
+                ClaimResult::Pass
+            } else {
+                ClaimResult::Fail(format!(
+                    "LensOutputEquals(r3_auto_loop_parallelism_sequential_emit_witness): expected `{expected_int}` (1 = no `thread::scope` / sequential fallback), computed `{computed_int}` for `{}`",
+                    claim.file_name
+                ))
+            };
+        }
+
         // T-LaneE cost receipt: `ProgramOutputBind` is the structural contract for a claim
         // source output-bind cost check. Dispatch on that input role, not on lens declaration
         // spelling; otherwise the canonical lens-name bridge would survive under a helper.

src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag

@@ -37,6 +37,13 @@ fn auto_loop_parallelism_pending_lens(_d: Dag) -> Int = 0
 
 data auto_loop_parallelism_pending_expected: Int = 1
 
+// R3 #47 witness: without Iteration-Independence opt-in, emit_rust must not use the parallel
+// `std::thread::scope` batch path (proxy for sequential iteration / no heuristic auto-parallelism)
+// until the ordinary loop-parallelism lens producer lands.
+fn r3_auto_loop_parallelism_sequential_emit_witness(_d: Dag) -> Int = 0
+
+data r3_auto_loop_parallelism_sequential_emit_expected: Int = 1
+
 type constant_fold_observed_report = DimensionReport<CrossTargetOptimizationEvidence>
 type constant_fold_expected_report = DimensionReport<CrossTargetOptimizationEvidence>
 type cost_structurally_derived_observed_report = DimensionReport<CrossTargetOptimizationEvidence>
@@ -56,12 +63,12 @@ data auto_loop_parallelism_provable_independence_emits_parallel: TestClaim = {
 
 data auto_loop_parallelism_unproven_falls_back_sequential: TestClaim = {
   name: "auto_loop_parallelism_unproven_falls_back_sequential",
-  source: "// free-consequences fixture: unproven iteration independence falls back to sequential loop emission.\nlet _: Int = 0\n",
+  source: "// free-consequences fixture: multi-element map without Iteration-Independence opt-in — emit_rust must not use parallel thread::scope scheduling (sequential fallback).\nlet ys = map(cons(1, singleton(2)), |x| x + 1)\n",
   file_name: "r3_free_consequences_auto_loop_parallelism_unproven.v3",
   predicate: LensOutputEquals(
-    auto_loop_parallelism_pending_lens,
+    r3_auto_loop_parallelism_sequential_emit_witness,
     auto_loop_parallelism_program_input,
-    auto_loop_parallelism_pending_expected
+    r3_auto_loop_parallelism_sequential_emit_expected
   ),
   requires: []
 }

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

@@ -1,9 +1,10 @@
 //! **Layer:** integration
 //!
-//! R3 T-Free-Consequences second-batch author-now/fire-later claims. The
-//! auto-loop-parallelism claims exercise the ordinary lens-data path; the
-//! cross-target-optimization claims lock the cost-related
-//! `BinaryDimensionReportEquals` shape.
+//! R3 T-Free-Consequences second-batch author-now/fire-later claims. Gate `#47`
+//! asserts sequential fallback via `LensOutputEquals` + `emit_rust` witness
+//! (`r3_auto_loop_parallelism_sequential_emit_witness`); the other auto-loop
+//! claims stay fail-closed on the scalar placeholder lens; the cross-target
+//! optimization claims lock the cost-related `BinaryDimensionReportEquals` shape.
 
 use std::sync::OnceLock;
 
@@ -17,6 +18,9 @@ use crate::common::run_on_larger_stack;
 const FIXTURE_SOURCE: &str = include_str!("../fixtures/r3_free_consequences_second_batch.dag");
 const FIXTURE_PATH: &str = "src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag";
 const SUITE_NAME: &str = "r3_free_consequences_second_batch_suite";
+/// Suite order is still checked against `TestRunner` output; expected Pass/Fail/NYI is keyed by
+/// name so reordering `claims` in the `.dag` cannot accidentally swap pass vs fail without a
+/// compile-time name mismatch on the `assert_eq!(result.claim_name, expected_name)` line.
 const EXPECTED_CLAIMS: [&str; 5] = [
     "auto_loop_parallelism_provable_independence_emits_parallel",
     "auto_loop_parallelism_unproven_falls_back_sequential",
@@ -56,20 +60,33 @@ fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes_inner() {
     let results = TestRunner::new(second_batch_dag()).run_suite(SUITE_NAME);
     assert_eq!(results.len(), EXPECTED_CLAIMS.len());
 
-    for (idx, (result, expected_name)) in results.iter().zip(EXPECTED_CLAIMS).enumerate() {
+    for (result, expected_name) in results.iter().zip(EXPECTED_CLAIMS) {
         assert_eq!(result.claim_name, expected_name);
-        if idx < 3 {
-            assert!(
-                matches!(&result.result, ClaimResult::Fail(_)),
-                "expected {expected_name} to fail closed on the pending ordinary loop-parallelism lens, got {:?}",
-                result.result
-            );
-        } else {
-            assert!(
-                matches!(&result.result, ClaimResult::NotYetImplemented(_)),
-                "expected {expected_name} to stay author-now/fire-later on BinaryDimensionReportEquals, got {:?}",
-                result.result
-            );
+        match expected_name {
+            "auto_loop_parallelism_unproven_falls_back_sequential" => {
+                assert!(
+                    matches!(&result.result, ClaimResult::Pass),
+                    "expected {expected_name} to Pass (sequential emit witness — no thread::scope), got {:?}",
+                    result.result
+                );
+            }
+            "auto_loop_parallelism_provable_independence_emits_parallel"
+            | "auto_loop_parallelism_dependence_emits_sequential" => {
+                assert!(
+                    matches!(&result.result, ClaimResult::Fail(_)),
+                    "expected {expected_name} to fail closed on the pending ordinary loop-parallelism lens, got {:?}",
+                    result.result
+                );
+            }
+            "cross_target_optimization_constant_fold_consistent"
+            | "cross_target_optimization_cost_structurally_derived" => {
+                assert!(
+                    matches!(&result.result, ClaimResult::NotYetImplemented(_)),
+                    "expected {expected_name} to stay author-now/fire-later on BinaryDimensionReportEquals, got {:?}",
+                    result.result
+                );
+            }
+            _ => panic!("unexpected claim in second-batch suite: {expected_name}"),
         }
     }
 }