diff --git a/src/v3/compiler/src/emit/rust_target.rs b/src/v3/compiler/src/emit/rust_target.rs index d1075b42772..fd427198fc6 100644 --- a/src/v3/compiler/src/emit/rust_target.rs +++ b/src/v3/compiler/src/emit/rust_target.rs @@ -2938,6 +2938,41 @@ fn port_reaches_upstream(dag: &Dag, from_port: PortId, to_port: PortId) -> bool false } +/// R3 gate #48 (`auto_loop_parallelism_dependence_emits_sequential`): structural witness that +/// loop-carried work stays on a sequential Rust emission path (no `std::thread::scope` batch) and +/// the program carries iteration dependence evidence. +/// +/// **Loop-shaped dependence:** any lowered `Behavior::Loop` whose body result port reaches the +/// carried `init` port upstream in the scheduling graph. +/// +/// **List catamorphism path:** when lowering does not surface a `Loop` node but the emitter still +/// spells the sequential iterator fold (`.iter().fold(`), treat that as the same sequential +/// iteration receipt for this gate's fixture discipline. +/// +/// **OR semantics (intentional):** `loop_carried` and the `.iter().fold(` substring are +/// **disjunctive** so the witness stays true on either lowering shape. The substring branch alone +/// does not prove arbitrary DAG-side iteration independence; it is a **fixture-scoped** receipt for +/// the authority program in `r3_free_consequences_auto_loop_parallelism_dependence.v3` (left fold +/// with carried `acc`). Broader reuse of this helper for other programs would need stronger +/// predicates, not a silent widening here. +/// +/// **Formatting coupling:** like gate #43's `thread::scope` substring receipt, both substring tests +/// key off today's Rust templates; if `rust.dag` emission spelling drifts, update this witness in +/// the same change (dissolution: structural `WorkflowParallelismReport` / iteration-independence +/// lens output per `docs/design-free-consequences.md` once `parallelism.dag` is no longer a stub). +pub(crate) fn r3_loop_dependence_sequential_emit_witness(dag: &Dag, emitted_rust: &str) -> bool { + if emitted_rust.contains("thread::scope") { + return false; + } + let loop_carried = dag.nodes().iter().any(|behavior| { + let Behavior::Loop(l) = behavior else { + return false; + }; + port_reaches_upstream(dag, loop_body_result_port(dag, l), l.init) + }); + loop_carried || emitted_rust.contains(".iter().fold(") +} + /// True when every pair of top-level binds has no value→value dependency in either direction. /// /// Used for R3 free-consequence auto-parallelism: only **pairwise** independent clusters emit a diff --git a/src/v3/compiler/src/test_runner.rs b/src/v3/compiler/src/test_runner.rs index 786b1770baa..ecf494b59ba 100644 --- a/src/v3/compiler/src/test_runner.rs +++ b/src/v3/compiler/src/test_runner.rs @@ -64,6 +64,15 @@ const R3_AUTO_LOOP_SEQUENTIAL_EMIT_WITNESS_LENS_NAME: &str = const R3_BRANCH_ARMS_SERIALIZE_WITNESS_LENS_NAME: &str = "r3_auto_parallelism_branch_arms_serialize_witness"; +/// R3 gate #48 (`LensOutputEquals` witness in `r3_free_consequences_second_batch.dag`). +/// +/// Compared as `Some(R3_LOOP_DEPENDENCE_SEQUENTIAL_EMIT_WITNESS_LENS_NAME)` — **not** `Some("…")` +/// inline — so `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`). +const R3_LOOP_DEPENDENCE_SEQUENTIAL_EMIT_WITNESS_LENS_NAME: &str = + "r3_auto_loop_parallelism_dependence_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 @@ -2443,6 +2452,49 @@ impl<'a> TestRunner<'a> { }; } + // R3 gate #48 (`auto_loop_parallelism_dependence_emits_sequential`): loop-carried + // dependence must stay on sequential Rust emission (no `std::thread::scope`); structural + // witness via `emit::rust_target::r3_loop_dependence_sequential_emit_witness`. + if lens_decl.name.as_deref() == Some(R3_LOOP_DEPENDENCE_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_dependence_sequential_emit_witness): expected Int literal is not a valid i64 decimal for `{expected_name}`" + )); + } + }, + _ => { + return ClaimResult::Fail(format!( + "LensOutputEquals(r3_auto_loop_parallelism_dependence_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_dependence_sequential_emit_witness): emit_rust failed for `{}`: {err:?}", + claim.file_name + )); + } + }; + let witness_ok = crate::emit::rust_target::r3_loop_dependence_sequential_emit_witness( + &program_dag, + &emitted, + ); + let computed_int = i64::from(witness_ok); + return if computed_int == expected_int { + ClaimResult::Pass + } else { + ClaimResult::Fail(format!( + "LensOutputEquals(r3_auto_loop_parallelism_dependence_sequential_emit_witness): expected `{expected_int}` (1 = sequential emission + loop-carried dependence), 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_auto_loop_parallelism_dependence.v3 b/src/v3/compiler/tests/fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3 new file mode 100644 index 00000000000..cdf022c0ef4 --- /dev/null +++ b/src/v3/compiler/tests/fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3 @@ -0,0 +1,8 @@ +// Program authority for R3 gate #48 (`auto_loop_parallelism_dependence_emits_sequential`). +module user.r3_free_consequences_auto_loop_parallelism_dependence + +import std.list { List, cons, empty, fold } + +let r3_fc_loop_dep_vals: List = cons(1, cons(2, cons(3, empty()))) +let r3_fc_loop_dep_out: Int = + fold(r3_fc_loop_dep_vals, 0, |acc, x| acc + x) 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 342a4332eb7..50222e63e04 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 @@ -44,6 +44,12 @@ fn r3_auto_loop_parallelism_sequential_emit_witness(_d: Dag) -> Int = 0 data r3_auto_loop_parallelism_sequential_emit_expected: Int = 1 +// R3 gate #48 witness: runner checks sequential emission for loop-carried dependence +// (`emit::rust_target::r3_loop_dependence_sequential_emit_witness`; see `test_runner`). +fn r3_auto_loop_parallelism_dependence_sequential_emit_witness(_d: Dag) -> Int = 0 + +data r3_auto_loop_parallelism_dependence_sequential_emit_expected: Int = 1 + type constant_fold_observed_report = DimensionReport type constant_fold_expected_report = DimensionReport type cost_structurally_derived_observed_report = DimensionReport @@ -75,12 +81,12 @@ data auto_loop_parallelism_unproven_falls_back_sequential: TestClaim = { data auto_loop_parallelism_dependence_emits_sequential: TestClaim = { name: "auto_loop_parallelism_dependence_emits_sequential", - source: "// free-consequences fixture: detected loop-carried dependence emits sequential loop code.\nlet _: Int = 0\n", + source: "// Program authority for R3 gate #48 (`auto_loop_parallelism_dependence_emits_sequential`).\nmodule user.r3_free_consequences_auto_loop_parallelism_dependence\n\nimport std.list { List, cons, empty, fold }\n\nlet r3_fc_loop_dep_vals: List = cons(1, cons(2, cons(3, empty())))\nlet r3_fc_loop_dep_out: Int =\n fold(r3_fc_loop_dep_vals, 0, |acc, x| acc + x)\n", file_name: "r3_free_consequences_auto_loop_parallelism_dependence.v3", predicate: LensOutputEquals( - auto_loop_parallelism_pending_lens, + r3_auto_loop_parallelism_dependence_sequential_emit_witness, auto_loop_parallelism_program_input, - auto_loop_parallelism_pending_expected + r3_auto_loop_parallelism_dependence_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 9af8b54ca64..ef928a2db45 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 @@ -2,15 +2,18 @@ //! //! 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. +//! (`r3_auto_loop_parallelism_sequential_emit_witness`). Gate `#48` asserts +//! loop-carried dependence stays on sequential emission +//! (`r3_auto_loop_parallelism_dependence_sequential_emit_witness`). The +//! provable-independence claim stays fail-closed on the scalar placeholder lens; +//! cross-target optimization claims lock the cost-related +//! `BinaryDimensionReportEquals` shape. use std::sync::OnceLock; use v3_compiler::compile_to_dag; use v3_compiler::dag::Dag; -use v3_compiler::test_runner::{ClaimResult, TestRunner}; +use v3_compiler::test_runner::{ClaimResult, TestClaimValue, TestRunner}; use v3_compiler::CompileError; use crate::common::run_on_larger_stack; @@ -18,6 +21,11 @@ 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"; + +/// Program authority for gate #48: pinned to `r3_free_consequences_auto_loop_parallelism_dependence.v3`. +const GATE_48_PROGRAM_AUTHORITY: &str = + include_str!("../fixtures/r3_free_consequences_auto_loop_parallelism_dependence.v3"); + /// 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. @@ -57,9 +65,20 @@ fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes() { } fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes_inner() { - let results = TestRunner::new(second_batch_dag()).run_suite(SUITE_NAME); + let dag = second_batch_dag(); + let results = TestRunner::new(dag).run_suite(SUITE_NAME); assert_eq!(results.len(), EXPECTED_CLAIMS.len()); + let gate_48_decl = dag + .declaration_by_name("auto_loop_parallelism_dependence_emits_sequential") + .expect("gate #48 claim present"); + let gate_48 = TestClaimValue::from_declaration(gate_48_decl) + .unwrap_or_else(|e| panic!("gate #48 should lower to TestClaimValue: {e}")); + assert_eq!( + gate_48.source, GATE_48_PROGRAM_AUTHORITY, + "gate #48 `claim.source` must match `r3_free_consequences_auto_loop_parallelism_dependence.v3` (single program authority)", + ); + for (result, expected_name) in results.iter().zip(EXPECTED_CLAIMS) { assert_eq!(result.claim_name, expected_name); match expected_name { @@ -70,8 +89,14 @@ fn r3_free_consequences_second_batch_reaches_expected_consumer_shapes_inner() { result.result ); } - "auto_loop_parallelism_provable_independence_emits_parallel" - | "auto_loop_parallelism_dependence_emits_sequential" => { + "auto_loop_parallelism_dependence_emits_sequential" => { + assert!( + matches!(&result.result, ClaimResult::Pass), + "expected {expected_name} to Pass (dependence sequential emit witness), got {:?}", + result.result + ); + } + "auto_loop_parallelism_provable_independence_emits_parallel" => { assert!( matches!(&result.result, ClaimResult::Fail(_)), "expected {expected_name} to fail closed on the pending ordinary loop-parallelism lens, got {:?}",