diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 539546ecabd..786b1770baa 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/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::() { @@ -2387,6 +2398,51 @@ impl<'a> TestRunner<'a> { }; } + // R3 gate #47 (`auto_loop_parallelism_unproven_falls_back_sequential`): without + // `Lens` 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::() { + 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 = `" + )); + } + }; + 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. diff --git a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag b/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag index 961096f5bf1..342a4332eb7 100644 --- a/src/v3/compiler/tests/fixtures/r3_free_consequences_second_batch.dag +++ b/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 type constant_fold_expected_report = DimensionReport type cost_structurally_derived_observed_report = DimensionReport @@ -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: [] } diff --git a/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs b/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs index 7323adeeeff..9af8b54ca64 100644 --- a/src/v3/compiler/tests/integration/r3_free_consequences_second_batch_test.rs +++ b/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}"), } } }