Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 35 additions & 0 deletions src/v3/compiler/src/emit/rust_target.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
52 changes: 52 additions & 0 deletions src/v3/compiler/src/test_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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::<i64>() {
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 = <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_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.
Expand Down
Original file line number Diff line number Diff line change
@@ -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<Int> = 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)
Original file line number Diff line number Diff line change
Expand Up @@ -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<CrossTargetOptimizationEvidence>
type constant_fold_expected_report = DimensionReport<CrossTargetOptimizationEvidence>
type cost_structurally_derived_observed_report = DimensionReport<CrossTargetOptimizationEvidence>
Expand Down Expand Up @@ -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<Int> = 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: []
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,22 +2,30 @@
//!
//! 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;

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.
Expand Down Expand Up @@ -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 {
Expand All @@ -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 {:?}",
Expand Down
Loading