From 2c4f2db9c5bd1ac5a27786674aacd8f7071dc523 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Tue, 22 Sep 2026 16:47:25 +0200 Subject: [PATCH 1/2] probe: pin overflow law for SUM-over-add scheduler rewrite --- .../tests/scheduler_sum_rewrite.rs | 117 ++++++++++++++++++ 1 file changed, 117 insertions(+) create mode 100644 crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs diff --git a/crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs b/crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs new file mode 100644 index 000000000..cf898988a --- /dev/null +++ b/crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs @@ -0,0 +1,117 @@ +//! Scheduler rewrite falsifier: a fold may distribute over lane arithmetic only +//! when that arithmetic's row semantics survive the rewrite. +//! +//! The tempting rewrite +//! +//! `SUM(wrapping_i32(a + b)) -> SUM(a) + SUM(b)` +//! +//! is NOT generally semantics-preserving. The lane expression is 32-bit +//! wrapping arithmetic, while `Terminal::MaskedSumI32` widens each selected +//! row to `i64` before accumulating. If any selected row overflows its `i32` +//! add, distributing the fold silently changes the program. +//! +//! This is the first scheduler law: expression folding needs a proof that the +//! row operator is exact on every selected row (or a separately defined +//! widened operator). A Rayon-shaped "associative reduce" argument is not +//! enough, because it ignores the semantic boundary between row arithmetic +//! and the widened terminal fold. + +use lance_graph_mask_risc::{ + execute, LaneRef, Operand, Planes, Program, Scratch, Terminal, Value, +}; + +/// Execute the shipped widened `MaskedSumI32` over an all-selected lane. +/// +/// The mask is resident input, not an intermediate population: this helper +/// introduces no mask operation and therefore isolates only the reduction law +/// the scheduler wants to rewrite. +fn sum_all(lane: &[i32]) -> i64 { + let words = lane.len().div_ceil(64); + let mut mask = vec![u64::MAX; words]; + if let Some(last) = mask.last_mut() { + let rem = lane.len() % 64; + if rem != 0 { + *last = (1u64 << rem) - 1; + } + } + + let masks: [&[u64]; 1] = [&mask]; + let lanes = [LaneRef::I32(lane)]; + let planes = Planes { + n_rows: lane.len(), + masks: &masks, + lanes: &lanes, + }; + let program = Program::new( + vec![], + Terminal::MaskedSumI32 { + mask: Operand::Plane(0), + lane: 0, + }, + ); + let mut scratch = Scratch::for_program(&program, lane.len()).expect("addressable"); + match execute(&program, &planes, &mut scratch, None).expect("sum executes") { + Value::SumI64(v) => v, + other => panic!("MaskedSumI32 has a fixed result shape, got {other:?}"), + } +} + +/// FAILS IF a scheduler treats `SUM(a+b)` as distributive without preserving +/// the row-level `i32` wrapping semantics. +/// +/// Row 0 is the entire counterexample: `i32::MAX + 1` wraps to `i32::MIN`. +/// The literal program therefore contributes `-2^31`; distributing the +/// widened fold contributes `2^31`. Both are individually valid i64 sums, +/// so no terminal overflow guard can rescue the rewrite. +#[test] +fn wrapping_row_overflow_forbids_distributing_sum_over_add() { + let a = [i32::MAX, 0]; + let b = [1, 0]; + let derived: Vec = a + .iter() + .zip(b.iter()) + .map(|(&x, &y)| x.wrapping_add(y)) + .collect(); + + let literal = sum_all(&derived); + let distributed = sum_all(&a) + sum_all(&b); + + assert_eq!(literal, i64::from(i32::MIN), "literal wrapping lane"); + assert_eq!( + distributed, + i64::from(i32::MAX) + 1, + "widened independent folds" + ); + assert_ne!( + literal, distributed, + "the rewrite must remain illegal without a per-row no-overflow proof" + ); +} + +/// Positive control: when every selected row's add is exact in `i32`, the +/// same distribution is valid. This keeps the negative result narrow: SUM is +/// not intrinsically non-distributive; the missing scheduler fact is the row +/// arithmetic's overflow domain. +#[test] +fn distributing_sum_over_add_is_valid_when_every_row_add_is_exact() { + let a: [i32; 4] = [10, -7, 2, 100]; + let b: [i32; 4] = [3, 11, -5, -40]; + let derived: Vec = a + .iter() + .zip(b.iter()) + .map(|(&x, &y)| x.wrapping_add(y)) + .collect(); + + for (&x, &y) in a.iter().zip(b.iter()) { + assert!( + x.checked_add(y).is_some(), + "fixture must stay inside the exact i32 domain" + ); + } + + let literal = sum_all(&derived); + let distributed = sum_all(&a) + sum_all(&b); + + assert_eq!(literal, distributed); + assert_eq!(literal, 74); +} From 5bab3b06c934d5ded64cfcc4663310bc7c439460 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 22 Sep 2026 17:49:35 +0000 Subject: [PATCH 2/2] probe: rustfmt scheduler_sum_rewrite imports Cosmetic only: collapse the lance_graph_mask_risc import onto one line as rustfmt requires. No semantic change. (The probe crate is outside the CI fmt gate, so this was not caught there.) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GXUahz73MZxtxWcfpHp9dG --- crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs b/crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs index cf898988a..8b3710684 100644 --- a/crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs +++ b/crates/r2il-mask-abi-probe/tests/scheduler_sum_rewrite.rs @@ -16,9 +16,7 @@ //! enough, because it ignores the semantic boundary between row arithmetic //! and the widened terminal fold. -use lance_graph_mask_risc::{ - execute, LaneRef, Operand, Planes, Program, Scratch, Terminal, Value, -}; +use lance_graph_mask_risc::{execute, LaneRef, Operand, Planes, Program, Scratch, Terminal, Value}; /// Execute the shipped widened `MaskedSumI32` over an all-selected lane. ///