From 1c059116b4431fe8fabb2a9de65d471fb77c74b5 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 01:52:18 +0000 Subject: [PATCH 1/5] feat(v3): wire R3 gate #47 sequential fallback emit witness Gate auto_loop_parallelism_unproven_falls_back_sequential now uses LensOutputEquals + emit_rust structural witness (no std::thread::scope), matching the gate #43 bind-parallelism pattern. Fixture claim exercises a single-bind map program; other loop claims stay fail-closed on the placeholder lens. Co-authored-by: Cursor --- src/v3/compiler/src/test_runner.rs | 47 +++++++++++++++++++ .../r3_free_consequences_second_batch.dag | 13 +++-- .../r3_free_consequences_second_batch_test.rs | 27 +++++++---- 3 files changed, 75 insertions(+), 12 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index b6ef1914454..58ab7513c16 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -46,6 +46,12 @@ const TC1_SUBSTRATE_LENS_ETA_DEFERRED_FIXTURE: &str = /// `docs/briefs/r2-pb-canonical-lens-bridge-disposition.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`. +const R3_AUTO_LOOP_SEQUENTIAL_EMIT_WITNESS_LENS_NAME: &str = + "r3_auto_loop_parallelism_sequential_emit_witness"; + /// Host-written forward fold for structural depth costs (see `src/v3/lenses/complexity.dag`). /// /// T-LaneE `DifferentialEquals` compares this receipt to [`crate::lens_cost::cost_of`] (emit output @@ -2379,6 +2385,47 @@ 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 exposes loop scheduling data: emitted Rust must + // not use the same `std::thread::scope` batch path as pairwise-independent top-level binds. + 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..35c39547df1 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: map iteration without Iteration-Independence opt-in — emit_rust must not use parallel thread::scope scheduling (sequential fallback).\nlet ys = map(singleton(1), |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..11996b9baf2 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; @@ -59,11 +60,19 @@ fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes_inner() { for (idx, (result, expected_name)) in results.iter().zip(EXPECTED_CLAIMS).enumerate() { 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 - ); + if idx == 1 { + assert!( + matches!(&result.result, ClaimResult::Pass), + "expected {expected_name} to Pass (sequential emit witness — no thread::scope), got {:?}", + result.result + ); + } else { + 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(_)), From 2778c9a48c2d22cd239e7413132e70173983acc1 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 02:08:40 +0000 Subject: [PATCH 2/5] docs(v3): cite ROADMAP DB-20 deferral for R3 #43/#47 emit witnesses Address review: name the dissolution receipt (ROADMAP Active deferrals, docs/db-history/db-20.md, design-db20 stage-2e lens) in rustdoc and inline comments; add TODO(DB-20) for replacing whole-program thread::scope greps. Co-authored-by: Cursor --- src/v3/compiler/src/test_runner.rs | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 58ab7513c16..1e7b7e49327 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -44,11 +44,15 @@ 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"; @@ -2347,7 +2351,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,8 +2392,12 @@ 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 exposes loop scheduling data: emitted Rust must - // not use the same `std::thread::scope` batch path as pairwise-independent top-level binds. + // 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::() { From c80e0d734258ba130b64e1472893e29d75a59686 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 02:28:20 +0000 Subject: [PATCH 3/5] test(v3): two-element map corpus for gate #47 sequential witness Addresses exploratory review note: singleton map was a trivial one-step iteration; cons(1, singleton(2)) keeps the structural proxy meaningful if parallel scheduling ever gates on iteration count. Co-authored-by: Cursor --- .../tests/fixtures/r3_free_consequences_second_batch.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 35c39547df1..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 @@ -63,7 +63,7 @@ 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: map iteration without Iteration-Independence opt-in — emit_rust must not use parallel thread::scope scheduling (sequential fallback).\nlet ys = map(singleton(1), |x| x + 1)\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( r3_auto_loop_parallelism_sequential_emit_witness, From ec43fb37a8cce2d597b981c6286617fc2716ab69 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 9 May 2026 22:30:12 -0400 Subject: [PATCH 4/5] WIP: R3 gate #47: auto loop parallelism unproven falls back sequential --- Cargo.lock | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Cargo.lock b/Cargo.lock index 12e15eeb80a..93f914712c6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1032,6 +1032,8 @@ dependencies = [ "criterion", "libc", "num-bigint", + "serde", + "serde_json", ] [[package]] From 6a5173e85a5a33f9e6918b6a51bcd3b093dfeba4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 10 May 2026 02:45:27 +0000 Subject: [PATCH 5/5] test(v3): key second-batch expectations by claim name, not index Addresses review: idx==1 broke if suite claim order changed; match on gate #47 name keeps semantics stable while zip still locks runner order. Co-authored-by: Cursor --- .../r3_free_consequences_second_batch_test.rs | 28 ++++++++++++------- 1 file changed, 18 insertions(+), 10 deletions(-) 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 11996b9baf2..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 @@ -18,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", @@ -57,28 +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 { - if idx == 1 { + 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 ); - } else { + } + "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 ); } - } else { - assert!( - matches!(&result.result, ClaimResult::NotYetImplemented(_)), - "expected {expected_name} to stay author-now/fire-later on BinaryDimensionReportEquals, 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}"), } } }