diff --git a/benchmarks/repsel_census/baseline.json b/benchmarks/repsel_census/baseline.json index 6f1457028c..3a60cc4f1a 100644 --- a/benchmarks/repsel_census/baseline.json +++ b/benchmarks/repsel_census/baseline.json @@ -285,7 +285,7 @@ "ptr-shape": 0, "ptr-shape-consumed": 0, "ptr-numarray": 0, - "canonical-i32": 3, + "canonical-i32": 4, "canonical-u32": 0, "canonical-str": 0, "int-valued-ta": 0, diff --git a/benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts b/benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts index b3ffd613dc..9b4e3c57b0 100644 --- a/benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts +++ b/benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts @@ -1,16 +1,16 @@ -// Liveness fixture for the monotone loop-induction i32 range proof (#7110). +// Liveness fixture for the loop-bound i32 range proofs (#7110/#7123). // // `fixture_canonical_slots.ts` proves canonical-i32 on STRAIGHT-LINE bitwise // locals and says so in its own comment — it deliberately avoids loops, because // before #7110 a loop counter could not select the canonical rep at all. This -// fixture is the complement: every canonical-i32 promotion in it comes from the -// loop-induction rule and from nothing else. There is no bitwise mixing, no +// fixture is the complement: every canonical-i32 promotion in it comes from a +// loop induction or bounded-accumulator rule and from nothing else. There is no bitwise mixing, no // `| 0`, no `>>> 0`, and no array indexing anywhere, so if // `collect_loop_bounded_i32_locals` returns the empty set this file's // canonical-i32 count is zero and the census goes red. // -// The three locals it must NOT promote are here on purpose: an unadmitted -// counter, an unbounded accumulator, and (since #7128) a counter that is +// The two locals it must NOT promote are here on purpose: an overflowing +// accumulator and (since #7128) a counter that is // perfectly provable and not worth promoting. Together they keep the fixture // from being satisfied by any rule that simply says yes to proven-integer // locals. @@ -62,14 +62,17 @@ function overshoot(): number { return i; } -// DOES NOT PROMOTE. A bare accumulator: `sum` has no guard bounding it, and -// 13_factorial's version of this really does reach 4.995e10. -function accumulate(): number { +// PROMOTES via #7123, and not via #7110's induction-variable rule. The counter +// gives an execution bound of 4096 and the step magnitude is 1, so the full +// accumulator interval is inside i32. +function accumulate(): string { let sum = 0; + let overflow = 0; for (let i = 0; i < ROUNDS; i++) { - sum = sum + 1000000; + sum = sum + 1; + overflow = overflow + 1000000; } - return sum; + return sum + "/" + overflow; } // DOES NOT PROMOTE — and this is the only entry here whose PROOF succeeds. diff --git a/changelog.d/7973-repsel-loop-accumulator.md b/changelog.d/7973-repsel-loop-accumulator.md new file mode 100644 index 0000000000..71184d6a19 --- /dev/null +++ b/changelog.d/7973-repsel-loop-accumulator.md @@ -0,0 +1,15 @@ +Canonical i32 representation selection can now admit a loop accumulator when +the compiler can prove that its initial magnitude plus every loop trip-count +bound times every step-magnitude bound stays within signed 32-bit range. + +The proof derives saturating trip counts from constant-bounded `for` induction +variables, multiplies them through nested loops, and starts with a deliberately +small step-expression set: integer literals and constants, remainder by a +literal, bitwise-and with a non-negative literal mask, and another loop-bounded +local. Unknown loop counts, writes, and expression forms remain boxed. In +particular, the factorial-style `sum += i % 1000` counterexample is still +refused because its bound exceeds i32. + +The change includes a representation-census liveness promotion and a registered +runtime parity probe whose three one-billion additions make an unsound widening +print a wrapped value instead of Node's 3,000,000,000. diff --git a/crates/perry-codegen/src/collectors/hir_facts.rs b/crates/perry-codegen/src/collectors/hir_facts.rs index 83ba7acfb3..bdf02e6613 100644 --- a/crates/perry-codegen/src/collectors/hir_facts.rs +++ b/crates/perry-codegen/src/collectors/hir_facts.rs @@ -484,6 +484,12 @@ pub(crate) fn collect_type_facts( } else { HashSet::new() }; + // #7123: this set now includes accumulators whose integer-ness and full + // range were proved together (for example `sum += i % 1000`). The older + // integer provenance collector deliberately does not accept bare `%`, so + // feed the stronger fact into its downstream consumers explicitly. This + // is a consequence of the range proof, not an additional assumption. + integer_locals.extend(loop_bounded_i32_locals.iter().copied()); let not_bigint_locals = super::not_bigint_locals::collect_not_bigint_locals(stmts, params, binding_types); let (mut array_facts, effect_facts, materialization_hazards) = @@ -1996,6 +2002,45 @@ mod tests { assert!(!facts.unsigned_i32_locals().contains(&2)); } + #[test] + fn bounded_modulo_accumulator_seeds_integer_provenance() { + // The pre-#7123 integer collector deliberately rejects bare `%`. + // Once trip-count x magnitude proves the whole accumulator range, that + // stronger fact must reach the ordinary integer-storage gate too. + let stmts = vec![ + mutable_number_let(1, Expr::Integer(0)), + Stmt::For { + init: Some(Box::new(mutable_number_let(2, Expr::Integer(0)))), + condition: Some(Expr::Compare { + op: perry_hir::CompareOp::Lt, + left: Box::new(Expr::LocalGet(2)), + right: Box::new(Expr::Integer(1000)), + }), + update: Some(Expr::Update { + id: 2, + op: perry_hir::UpdateOp::Increment, + prefix: false, + }), + body: vec![Stmt::Expr(Expr::LocalSet( + 1, + Box::new(Expr::Binary { + op: BinaryOp::Add, + left: Box::new(Expr::LocalGet(1)), + right: Box::new(Expr::Binary { + op: BinaryOp::Mod, + left: Box::new(Expr::LocalGet(2)), + right: Box::new(Expr::Integer(10)), + }), + }), + ))], + }, + ]; + let facts = collect_hir_facts(&stmts, &HashSet::new(), &HashSet::new()); + + assert!(facts.loop_bounded_i32_locals().contains(&1)); + assert!(facts.integer_locals().contains(&1)); + } + #[test] fn native_fact_graph_collects_platform_purity_and_noalias_subgraphs() { let mut constants = HashMap::new(); diff --git a/crates/perry-codegen/src/collectors/loop_bounded_i32.rs b/crates/perry-codegen/src/collectors/loop_bounded_i32.rs index d3afed3b83..fa5024e228 100644 --- a/crates/perry-codegen/src/collectors/loop_bounded_i32.rs +++ b/crates/perry-codegen/src/collectors/loop_bounded_i32.rs @@ -60,17 +60,25 @@ //! canonical storage (i32 slot only, no double slot, no dual writes) instead of //! a shadow that has to be kept in sync with a boxed double. //! -//! ## What it deliberately does NOT prove +//! ## Bounded accumulators (#7123) //! -//! A bare **accumulator** — `let sum = 0; for (…) sum = sum + x;` — is not -//! admitted, and must not be. `benchmarks/suite/13_factorial.ts` is the live -//! counterexample: `sum = sum + (i % 1000)` over 1e8 iterations reaches -//! 49,950,000,000, twenty-three times `INT32_MAX`. Node prints it exactly; an -//! i32 slot would print a wrapped negative. Admitting "every write is -//! `sum = sum + `" as an i32 proof is a silent wrong answer, not a -//! missed optimization. Bounding an accumulator needs the loop's *trip count* -//! multiplied by a magnitude bound on the step expression — strictly more -//! analysis than this module does; #7123 specifies it. +//! A bare **accumulator** — `let sum = 0; for (…) sum = sum + x;` — still is +//! not enough. `benchmarks/suite/13_factorial.ts` is the live counterexample: +//! `sum = sum + (i % 1000)` over 1e8 iterations reaches 49,950,000,000, +//! twenty-three times `INT32_MAX`. Node prints it exactly; an i32 slot would +//! print a wrapped negative. +//! +//! The second half of this collector therefore proves a separate inequality. +//! A `for` loop whose update is a positive constant step on one of the +//! induction variables above has a compile-time trip-count upper bound `T`. +//! Bounds multiply through nested loops (with saturating arithmetic). For an +//! accumulator with literal entry value `A0`, every write must be +//! `acc = acc + e`, and `e` must have a small syntactic magnitude bound `M`: +//! an integer literal/constant, `x % literal`, `x & non_negative_literal`, or +//! another loop-bounded induction local. The accumulated proof is then +//! `|acc| <= |A0| + sum(T * M)`. Only a result at most `INT32_MAX` is admitted. +//! Unknown loop bounds and unknown expression shapes fall through to boxed +//! storage; under-approximation is free here. //! //! Consumed only by the canonical-i32 gate (`canonical_safe_local` in //! `stmt/let_stmt.rs`), never by the parallel-shadow `needs_i32_slot` gate, so @@ -97,6 +105,12 @@ struct GuardedLevel { extreme: i64, } +#[derive(Clone, Copy, Debug)] +struct IntInterval { + lo: i64, + hi: i64, +} + /// Analysis state, accumulated over one whole function body. #[derive(Default)] struct State { @@ -163,6 +177,29 @@ pub fn collect_loop_bounded_i32_locals( out.insert(id); } } + let induction_intervals = out + .iter() + .filter_map(|id| { + let init = *st.declared_init.get(id)?; + let bound = *st.bounds.get(id)?; + let interval = match bound.dir { + Dir::Inc => IntInterval { + lo: init, + hi: bound.extreme, + }, + Dir::Dec => IntInterval { + lo: bound.extreme, + hi: init, + }, + }; + Some((*id, interval)) + }) + .collect(); + out.extend(collect_bounded_accumulator_locals( + stmts, + &st, + &induction_intervals, + )); out } @@ -868,6 +905,498 @@ fn record_write( } } +// --------------------------------------------------------------------------- +// Pass 3: trip-count x step-magnitude bounds for accumulators (#7123) +// --------------------------------------------------------------------------- + +#[derive(Clone, Copy)] +struct ExecutionBound { + loop_depth: u32, + executions: Option, +} + +impl ExecutionBound { + fn function_body() -> Self { + Self { + loop_depth: 0, + executions: Some(1), + } + } + + fn nested_loop(self, trips: Option) -> Self { + Self { + loop_depth: self.loop_depth.saturating_add(1), + executions: self + .executions + .zip(trips) + .map(|(outer, inner)| outer.saturating_mul(inner)), + } + } +} + +#[derive(Default)] +struct AccumulatorState { + /// Sum of the worst-case magnitude contribution from every syntactic write + /// site. Mutually-exclusive sites are deliberately summed: overestimating + /// only declines an optimization, while underestimating would wrap values. + contribution: HashMap, + saw_accumulation: HashSet, + disqualified: HashSet, +} + +fn collect_bounded_accumulator_locals( + stmts: &[Stmt], + induction: &State, + induction_intervals: &HashMap, +) -> HashSet { + let mut accumulators = AccumulatorState::default(); + walk_accumulator_stmts( + stmts, + ExecutionBound::function_body(), + induction, + induction_intervals, + &mut accumulators, + ); + + accumulators + .saw_accumulation + .iter() + .filter_map(|&id| { + if accumulators.disqualified.contains(&id) || induction.bad_decl.contains(&id) { + return None; + } + let init = *induction.declared_init.get(&id)?; + let contribution = *accumulators.contribution.get(&id)?; + let worst_magnitude = u128::from(init.unsigned_abs()).saturating_add(contribution); + (worst_magnitude <= i32::MAX as u128).then_some(id) + }) + .collect() +} + +/// A direct, guaranteed `for` update. Restricting the trip-count premise to a +/// single update expression avoids treating a short-circuited or conditional +/// body step as minimum progress. Extra same-direction body steps can only +/// reduce the number of iterations; the induction pass has already rejected +/// any reversing or otherwise-unrecognised write to this counter. +fn direct_for_update(update: &Expr, st: &State) -> Option<(u32, Dir, u64)> { + let (id, dir, magnitude) = match update { + Expr::Update { id, op, .. } => (*id, update_dir(*op), 1), + Expr::LocalSet(id, value) => { + let (dir, magnitude) = classify_step(*id, value, st)?; + (*id, dir, magnitude) + } + _ => return None, + }; + let magnitude = u64::try_from(magnitude).ok()?; + (magnitude > 0).then_some((id, dir, magnitude)) +} + +fn for_loop_trip_bound( + condition: Option<&Expr>, + update: Option<&Expr>, + st: &State, + induction_intervals: &HashMap, +) -> Option { + let condition = condition?; + let (id, dir, step) = direct_for_update(update?, st)?; + if !induction_intervals.contains_key(&id) { + return None; + } + let init = *st.declared_init.get(&id)?; + conjunct_guards(condition, st) + .into_iter() + .filter(|(guarded, _, _)| *guarded == id) + .filter_map(|(_, op, bound)| trip_count_for_guard(init, dir, step, op, bound)) + .min() +} + +fn trip_count_for_guard(init: i64, dir: Dir, step: u64, op: CompareOp, bound: i64) -> Option { + let (distance, agrees) = match (dir, op) { + (Dir::Inc, CompareOp::Lt) => ((i128::from(bound) - i128::from(init)).max(0), true), + (Dir::Inc, CompareOp::Le) => ((i128::from(bound) - i128::from(init) + 1).max(0), true), + (Dir::Dec, CompareOp::Gt) => ((i128::from(init) - i128::from(bound)).max(0), true), + (Dir::Dec, CompareOp::Ge) => ((i128::from(init) - i128::from(bound) + 1).max(0), true), + _ => (0, false), + }; + if !agrees { + return None; + } + let distance = u128::try_from(distance).ok()?; + let step = u128::from(step); + Some(distance.saturating_add(step - 1) / step) +} + +fn accumulator_step_magnitude( + id: u32, + value: &Expr, + st: &State, + induction_intervals: &HashMap, +) -> Option { + let Expr::Binary { + op: BinaryOp::Add, + left, + right, + } = value + else { + return None; + }; + let is_self = |e: &Expr| matches!(e, Expr::LocalGet(other) if *other == id); + let step = if is_self(left) { + right.as_ref() + } else if is_self(right) { + left.as_ref() + } else { + return None; + }; + step_magnitude_bound(step, st, induction_intervals) +} + +fn step_magnitude_bound( + e: &Expr, + st: &State, + induction_intervals: &HashMap, +) -> Option { + if let Some(value) = integer_literal(e) { + return Some(u128::from(value.unsigned_abs())); + } + if let Expr::LocalGet(id) = e { + if let Some(value) = st.const_ints.get(id).or_else(|| st.module_consts.get(id)) { + return Some(u128::from(value.unsigned_abs())); + } + let interval = induction_intervals.get(id)?; + return Some( + u128::from(interval.lo.unsigned_abs()).max(u128::from(interval.hi.unsigned_abs())), + ); + } + let Expr::Binary { op, left, right } = e else { + return None; + }; + match op { + // JS remainder has the sign of its dividend and magnitude strictly + // below the divisor's magnitude. The dividend must itself be an + // integer-proven value; otherwise `1.5 % 1` is fractional and a range + // bound alone would not justify integer storage. Zero is excluded + // because `% 0` is NaN, not an integer step. + BinaryOp::Mod => { + let dividend_is_integer = integer_literal(left).is_some() + || matches!(left.as_ref(), Expr::LocalGet(id) + if st.const_ints.contains_key(id) + || st.module_consts.contains_key(id) + || induction_intervals.contains_key(id)); + if !dividend_is_integer { + return None; + } + let divisor = integer_literal(right)?; + let magnitude = u128::from(divisor.unsigned_abs()); + (magnitude > 0).then_some(magnitude - 1) + } + // Bitwise operands are ToInt32-coerced. For a non-negative literal + // mask, the source literal itself is a conservative magnitude bound + // even when it exceeds the signed-i32 range. + BinaryOp::BitAnd => { + let mask = integer_literal(right) + .or_else(|| integer_literal(left)) + .filter(|mask| *mask >= 0)?; + Some(mask as u128) + } + _ => None, + } +} + +fn record_accumulator_write( + id: u32, + value: Option<&Expr>, + execution: ExecutionBound, + induction: &State, + induction_intervals: &HashMap, + accumulators: &mut AccumulatorState, +) { + let magnitude = value + .and_then(|value| accumulator_step_magnitude(id, value, induction, induction_intervals)); + let Some((executions, magnitude)) = execution.executions.zip(magnitude) else { + accumulators.disqualified.insert(id); + return; + }; + if execution.loop_depth == 0 { + accumulators.disqualified.insert(id); + return; + } + accumulators.saw_accumulation.insert(id); + let contribution = executions.saturating_mul(magnitude); + accumulators + .contribution + .entry(id) + .and_modify(|total| *total = total.saturating_add(contribution)) + .or_insert(contribution); +} + +fn walk_accumulator_stmts( + stmts: &[Stmt], + execution: ExecutionBound, + induction: &State, + induction_intervals: &HashMap, + accumulators: &mut AccumulatorState, +) { + for stmt in stmts { + match stmt { + Stmt::Let { init, .. } => { + if let Some(init) = init { + walk_accumulator_expr( + init, + execution, + induction, + induction_intervals, + accumulators, + ); + } + } + Stmt::Expr(expr) | Stmt::Throw(expr) => walk_accumulator_expr( + expr, + execution, + induction, + induction_intervals, + accumulators, + ), + Stmt::Return(value) => { + if let Some(value) = value { + walk_accumulator_expr( + value, + execution, + induction, + induction_intervals, + accumulators, + ); + } + } + Stmt::If { + condition, + then_branch, + else_branch, + } => { + walk_accumulator_expr( + condition, + execution, + induction, + induction_intervals, + accumulators, + ); + walk_accumulator_stmts( + then_branch, + execution, + induction, + induction_intervals, + accumulators, + ); + if let Some(else_branch) = else_branch { + walk_accumulator_stmts( + else_branch, + execution, + induction, + induction_intervals, + accumulators, + ); + } + } + Stmt::While { condition, body } | Stmt::DoWhile { condition, body } => { + // This first implementation intentionally derives execution + // counts only from a `for` loop's guaranteed update. A while + // body step may be skipped by control flow; treating it as + // minimum progress would make the trip bound unsound. + let unknown = execution.nested_loop(None); + walk_accumulator_expr( + condition, + unknown, + induction, + induction_intervals, + accumulators, + ); + walk_accumulator_stmts(body, unknown, induction, induction_intervals, accumulators); + } + Stmt::For { + init, + condition, + update, + body, + } => { + if let Some(init) = init { + walk_accumulator_stmts( + std::slice::from_ref(init.as_ref()), + execution, + induction, + induction_intervals, + accumulators, + ); + } + let trips = for_loop_trip_bound( + condition.as_ref(), + update.as_ref(), + induction, + induction_intervals, + ); + let loop_execution = execution.nested_loop(trips); + if let Some(condition) = condition { + // The condition executes once more than the body and may + // short-circuit. Writes there are outside this proof. + walk_accumulator_expr( + condition, + execution.nested_loop(None), + induction, + induction_intervals, + accumulators, + ); + } + if let Some(update) = update { + walk_accumulator_expr( + update, + loop_execution, + induction, + induction_intervals, + accumulators, + ); + } + walk_accumulator_stmts( + body, + loop_execution, + induction, + induction_intervals, + accumulators, + ); + } + Stmt::Try { + body, + catch, + finally, + } => { + walk_accumulator_stmts( + body, + execution, + induction, + induction_intervals, + accumulators, + ); + if let Some(catch) = catch { + walk_accumulator_stmts( + &catch.body, + execution, + induction, + induction_intervals, + accumulators, + ); + } + if let Some(finally) = finally { + walk_accumulator_stmts( + finally, + execution, + induction, + induction_intervals, + accumulators, + ); + } + } + Stmt::Switch { + discriminant, + cases, + } => { + walk_accumulator_expr( + discriminant, + execution, + induction, + induction_intervals, + accumulators, + ); + for case in cases { + if let Some(test) = &case.test { + walk_accumulator_expr( + test, + execution, + induction, + induction_intervals, + accumulators, + ); + } + walk_accumulator_stmts( + &case.body, + execution, + induction, + induction_intervals, + accumulators, + ); + } + } + Stmt::Labeled { body, .. } => walk_accumulator_stmts( + std::slice::from_ref(body.as_ref()), + execution, + induction, + induction_intervals, + accumulators, + ), + _ => {} + } + } +} + +fn walk_accumulator_expr( + expr: &Expr, + execution: ExecutionBound, + induction: &State, + induction_intervals: &HashMap, + accumulators: &mut AccumulatorState, +) { + match expr { + Expr::LocalSet(id, value) => { + record_accumulator_write( + *id, + Some(value), + execution, + induction, + induction_intervals, + accumulators, + ); + walk_accumulator_expr( + value, + execution, + induction, + induction_intervals, + accumulators, + ); + } + Expr::Update { id, .. } => record_accumulator_write( + *id, + None, + execution, + induction, + induction_intervals, + accumulators, + ), + Expr::Closure { body, .. } => { + // A closure can be called any number of times. Disqualify every + // local it writes in this enclosing analysis; its own codegen pass + // will independently analyse locals owned by the closure. + let mut written = HashSet::new(); + collect_written_locals(body, &mut written); + accumulators.disqualified.extend(written); + let unknown = execution.nested_loop(None); + perry_hir::walker::walk_expr_children(expr, &mut |child| { + walk_accumulator_expr(child, unknown, induction, induction_intervals, accumulators) + }); + } + _ => { + if let Some(id) = with_set_fallback_local(expr) { + accumulators.disqualified.insert(id); + } + perry_hir::walker::walk_expr_children(expr, &mut |child| { + walk_accumulator_expr( + child, + execution, + induction, + induction_intervals, + accumulators, + ) + }); + } + } +} + #[cfg(test)] #[path = "loop_bounded_i32/tests.rs"] mod tests; diff --git a/crates/perry-codegen/src/collectors/loop_bounded_i32/tests.rs b/crates/perry-codegen/src/collectors/loop_bounded_i32/tests.rs index 63297d4b84..f5857c39ab 100644 --- a/crates/perry-codegen/src/collectors/loop_bounded_i32/tests.rs +++ b/crates/perry-codegen/src/collectors/loop_bounded_i32/tests.rs @@ -129,10 +129,8 @@ fn bare_loop_counter_with_literal_bound_is_admitted() { } #[test] -fn bare_accumulator_is_not_admitted() { - // The other half of #7110, and the half that must STAY denied: - // `sum = sum + 1` is a step, but no loop guard constrains `sum`, so - // nothing bounds it. 13_factorial's `sum` really does reach 4.995e10. +fn accumulator_bounded_by_trip_count_times_step_is_admitted() { + // #7123: 1,000,000 trips * magnitude 1, from entry value zero, fits i32. let stmts = vec![ let_mut(1, Some(Expr::Integer(0))), counting_for( @@ -146,12 +144,212 @@ fn bare_accumulator_is_not_admitted() { ), ]; let got = run(&stmts); + assert!( + got.contains(&1), + "bounded accumulator must promote: {got:?}" + ); +} + +#[test] +fn accumulator_whose_true_total_leaves_i32_is_rejected() { + // Three iterations are enough to reach 3,000,000,000. This is the + // runtime-observable sabotage shape: deleting the final range check wraps. + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + counting_for( + 2, + 0, + Expr::Integer(3), + vec![set( + 1, + bin( + BinaryOp::Add, + Expr::LocalGet(1), + Expr::Integer(1_000_000_000), + ), + )], + ), + ]; + let got = run(&stmts); assert!( !got.contains(&1), - "bare accumulator must stay denied: {got:?}" + "overflowing accumulator was admitted: {got:?}" + ); +} + +#[test] +fn inclusive_non_unit_trip_count_uses_the_final_iteration() { + // `i = 0; i <= 8; i += 4` executes at 0, 4, and 8. Omitting the inclusive + // endpoint would under-count this as two iterations and unsafely admit the + // 800M accumulator; the 700M control still fits after all three writes. + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + let_mut(2, Some(Expr::Integer(0))), + Stmt::For { + init: Some(Box::new(let_mut(3, Some(Expr::Integer(0))))), + condition: Some(cmp(CompareOp::Le, Expr::LocalGet(3), Expr::Integer(8))), + update: Some(Expr::LocalSet( + 3, + Box::new(bin(BinaryOp::Add, Expr::LocalGet(3), Expr::Integer(4))), + )), + body: vec![ + set( + 1, + bin(BinaryOp::Add, Expr::LocalGet(1), Expr::Integer(700_000_000)), + ), + set( + 2, + bin(BinaryOp::Add, Expr::LocalGet(2), Expr::Integer(800_000_000)), + ), + ], + }, + ]; + let got = run(&stmts); + assert!(got.contains(&1), "three 700M steps still fit: {got:?}"); + assert!( + !got.contains(&2), + "inclusive endpoint was omitted from the trip count: {got:?}" ); } +#[test] +fn factorial_modulo_counterexample_is_rejected_by_its_magnitude() { + // 1e8 * (|1000| - 1) is above i32. The real program reaches 4.995e10; + // using the conservative 9.99e10 bound must still refuse it. + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + counting_for( + 2, + 0, + Expr::Integer(100_000_000), + vec![set( + 1, + bin( + BinaryOp::Add, + Expr::LocalGet(1), + bin(BinaryOp::Mod, Expr::LocalGet(2), Expr::Integer(1000)), + ), + )], + ), + ]; + assert!(!run(&stmts).contains(&1)); +} + +#[test] +fn bit_mask_step_uses_the_literal_mask_as_its_magnitude() { + // 1000 * 255 fits, so `acc += x & 255` is bounded even though the value of + // x itself is not known to this range analysis. + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + counting_for( + 2, + 0, + Expr::Integer(1000), + vec![set( + 1, + bin( + BinaryOp::Add, + Expr::LocalGet(1), + bin(BinaryOp::BitAnd, Expr::LocalGet(9), Expr::Integer(255)), + ), + )], + ), + ]; + assert!(run(&stmts).contains(&1)); +} + +#[test] +fn nested_loop_trip_counts_multiply() { + // 40,000 * 40,000 additions fit, but 50,000 * 50,000 do not. This catches + // an implementation that takes the inner bound without the outer count. + let nested = |bound| { + vec![ + let_mut(1, Some(Expr::Integer(0))), + counting_for( + 2, + 0, + Expr::Integer(bound), + vec![counting_for( + 3, + 0, + Expr::Integer(bound), + vec![set( + 1, + bin(BinaryOp::Add, Expr::LocalGet(1), Expr::Integer(1)), + )], + )], + ), + ] + }; + assert!(run(&nested(40_000)).contains(&1)); + assert!(!run(&nested(50_000)).contains(&1)); +} + +#[test] +fn another_loop_bounded_local_can_bound_the_step() { + // `iter` has interval [0, 100]. The accumulator write executes at most + // 800 * 800 times, so its worst-case magnitude is 64,000,000. + let iter_loop = Stmt::While { + condition: cmp(CompareOp::Lt, Expr::LocalGet(4), Expr::Integer(100)), + body: vec![set( + 4, + bin(BinaryOp::Add, Expr::LocalGet(4), Expr::Integer(1)), + )], + }; + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + counting_for( + 2, + 0, + Expr::Integer(800), + vec![counting_for( + 3, + 0, + Expr::Integer(800), + vec![ + let_mut(4, Some(Expr::Integer(0))), + iter_loop, + set(1, bin(BinaryOp::Add, Expr::LocalGet(1), Expr::LocalGet(4))), + ], + )], + ), + ]; + assert!(run(&stmts).contains(&1)); +} + +#[test] +fn an_unknown_enclosing_loop_rejects_the_accumulator() { + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + Stmt::While { + condition: Expr::Bool(true), + body: vec![set( + 1, + bin(BinaryOp::Add, Expr::LocalGet(1), Expr::Integer(1)), + )], + }, + ]; + assert!(!run(&stmts).contains(&1)); +} + +#[test] +fn any_write_outside_a_bounded_loop_rejects_the_accumulator() { + let stmts = vec![ + let_mut(1, Some(Expr::Integer(0))), + counting_for( + 2, + 0, + Expr::Integer(10), + vec![set( + 1, + bin(BinaryOp::Add, Expr::LocalGet(1), Expr::Integer(1)), + )], + ), + set(1, bin(BinaryOp::Add, Expr::LocalGet(1), Expr::Integer(1))), + ]; + assert!(!run(&stmts).contains(&1)); +} + #[test] fn const_local_bound_resolves() { // const LIMIT = 100; for (let i = 0; i < LIMIT; i++) {} diff --git a/crates/perry-codegen/src/expr/slot_rep.rs b/crates/perry-codegen/src/expr/slot_rep.rs index bc49c70fc4..0f5262a977 100644 --- a/crates/perry-codegen/src/expr/slot_rep.rs +++ b/crates/perry-codegen/src/expr/slot_rep.rs @@ -53,14 +53,13 @@ //! - `int_valued_ta_locals` (merged into `integer_locals`): every write i32 or //! a possibly-OOB int-TA read whose every observation is ToInt32-coercing; //! NaN-safe entry conversion (`toint32_wrap`) keeps OOB `undefined` → 0. -//! - `loop_bounded_i32_locals` (#7110): a monotone induction variable whose -//! reachable interval is a pair of compile-time i32 constants — single -//! literal init, every write a `+k`/`-k` step dominated by a -//! constant-bounded guard on the immediately enclosing loop, direction -//! agreeing with the guard. A real range argument, not a compatibility -//! bound: there is no reachable state in which the value leaves i32. A bare -//! accumulator is deliberately NOT admitted — see -//! `collectors/loop_bounded_i32.rs`. +//! - `loop_bounded_i32_locals` (#7110/#7123): either a monotone induction +//! variable whose reachable interval is a pair of compile-time i32 constants, +//! or an accumulator whose literal entry magnitude plus every enclosing +//! loop's trip-count bound times every write's step-magnitude bound fits i32. +//! Both are real range arguments, not compatibility bounds: there is no +//! reachable state in which the value leaves i32. Unknown loop counts and +//! step expressions remain boxed; see `collectors/loop_bounded_i32.rs`. //! - `integer_locals ∩ index_used_locals`: admission accepts `Add/Sub/Mul` //! chains that can in principle exceed i32 — but under the pre-phase shadow //! model every `LocalGet` of such a local ALREADY reads the i32 slot @@ -382,11 +381,11 @@ impl CanonicalI32Denial { if self.not_index_used_or_bounded { return Some(( "not_index_used_or_bounded", - "proven integer-valued, but never used as an array index, not \ - provably i32-bounded, and not a constant-bounded loop \ - induction variable (#7110), so nothing pins its range to 32 \ - bits. A bare accumulator lands here and must: \ - `sum = sum + (i % 1000)` over 1e8 iterations really does reach \ + "proven integer-valued, but never used as an array index and \ + not provably i32-bounded by either a constant-bounded loop \ + induction interval (#7110) or a trip-count times \ + step-magnitude accumulator bound (#7123). The factorial \ + counterexample (`sum += i % 1000` over 1e8 iterations) reaches \ 4.995e10, so an i32 slot would print a wrapped negative", Tier::CompilerLimitation, Some(NOT_BOUNDED_ISSUE), @@ -441,7 +440,7 @@ pub(crate) fn deny_canonical_i32(ctx: &FnCtx<'_>, id: u32, name: &str, denial: C /// Tracking issue for "a module-level binding can never take a canonical slot". const MODULE_GLOBAL_ISSUE: &str = "#7109"; /// Tracking issue for the index-use / i32-bound precondition. -const NOT_BOUNDED_ISSUE: &str = "#7110"; +const NOT_BOUNDED_ISSUE: &str = "#7123"; /// Tracking issue for the profitability refusal — the one denial in this list /// that is not a failed proof. const NO_BENEFIT_ISSUE: &str = "#7128"; @@ -961,9 +960,9 @@ mod repsel_denial_tests { assert_eq!(d.verdict().map(|v| v.0), Some(MODULE_INIT_CONTEXT)); } - /// A bare accumulator at module top level fails BOTH rules. The - /// value-level one is the more actionable, so it wins. This is - /// `02_loop_overhead`'s `i`. + /// An accumulator with no provable trip-count/magnitude product at module + /// top level fails BOTH rules. The value-level one is more actionable, so + /// it wins. #[test] fn a_value_rule_outranks_the_context_rule() { let d = CanonicalI32Denial { @@ -974,7 +973,7 @@ mod repsel_denial_tests { let (rule, _, tier, issue) = d.verdict().expect("a value-level denial"); assert_eq!(rule, "not_index_used_or_bounded"); assert_eq!(tier, crate::opt_report::Tier::CompilerLimitation); - assert_eq!(issue, Some("#7110")); + assert_eq!(issue, Some("#7123")); } /// Precedence is total and ordered: with every rule failing at once, the diff --git a/crates/perry-codegen/src/stmt/let_stmt.rs b/crates/perry-codegen/src/stmt/let_stmt.rs index 7fcf315cce..fe00082881 100644 --- a/crates/perry-codegen/src/stmt/let_stmt.rs +++ b/crates/perry-codegen/src/stmt/let_stmt.rs @@ -1312,15 +1312,14 @@ pub(crate) fn lower_let( // * `int_valued_ta_locals` (#6898): every write i32-producing or an int-kind // TA read, every observation ToInt32-coercing — which makes canonical-i32 // storage output-invariant with the NaN-safe entry conversion. - // * `loop_bounded_i32_locals` (#7110): a monotone induction variable whose - // whole reachable interval is a pair of compile-time i32 constants — - // single literal init, every write a step dominated by a constant-bounded - // guard on the immediately enclosing loop. This is the term that admits a - // plain `for (let i = 0; i < 1000000; i++)` counter, which satisfies - // neither `index_used_locals` (nothing is indexed) nor - // `strictly_i32_bounded_locals` (`i++` disqualifies there, #6072). - // See `collectors/loop_bounded_i32.rs` for the interval argument — and - // for why a bare accumulator is NOT admitted by it. + // * `loop_bounded_i32_locals` (#7110/#7123): either a monotone induction + // variable whose whole reachable interval is a pair of compile-time i32 + // constants, or an accumulator whose entry magnitude plus every bounded + // loop trip count times every bounded step magnitude fits i32. This term + // admits both a plain `for (let i = 0; i < 1000000; i++)` counter and a + // soundly bounded `sum = sum + 1`; neither satisfies `index_used_locals` + // or `strictly_i32_bounded_locals`. See the collector for the proof and + // the deliberately small accepted step-expression set. let canonical_safe_local = i32_safe_local || ctx.native_facts.int_valued_ta_locals().contains(&id) || ctx.native_facts.loop_bounded_i32_locals().contains(&id); diff --git a/scripts/compiler_output_harness/repsel_census.py b/scripts/compiler_output_harness/repsel_census.py index 1ecfca3a24..86b0e639ec 100644 --- a/scripts/compiler_output_harness/repsel_census.py +++ b/scripts/compiler_output_harness/repsel_census.py @@ -220,12 +220,12 @@ "canonical-u32": 1, "canonical-str": 1, }, - # #7110: every canonical-i32 promotion in this fixture comes from the - # loop-induction range proof and from nothing else -- no bitwise mixing, no + # #7110/#7123: every canonical-i32 promotion in this fixture comes from the + # loop-bound range proofs and from nothing else -- no bitwise mixing, no # `| 0`, no array indexing. Pinned at the exact count it is written to - # promote (2 counters + 1 in the accumulator loop), so losing any one of the - # three goes red rather than silently degrading to "still nonzero". - "fixture_loop_bounded_i32": {"canonical-i32": 3}, + # promote (3 counters + 1 bounded accumulator), so losing the accumulator + # rule goes red rather than silently degrading to "still nonzero". + "fixture_loop_bounded_i32": {"canonical-i32": 4}, "fixture_int_valued_ta": {"int-valued-ta": 1}, "fixture_spec_abi_taptr": {"spec-abi-entry": 1, "spec-abi-taptr-slot": 1}, # #7109. The same three reps as `fixture_canonical_slots`, but this fixture diff --git a/test-files/test_gap_repsel_loop_bounded_i32.ts b/test-files/test_gap_repsel_loop_bounded_i32.ts index 98d472fd26..68ed7dc494 100644 --- a/test-files/test_gap_repsel_loop_bounded_i32.ts +++ b/test-files/test_gap_repsel_loop_bounded_i32.ts @@ -1,14 +1,16 @@ -// Repsel Phase 1, #7110: canonical unboxed i32 storage for a monotone loop -// induction variable — a counter that is NOT used as an array index and is NOT -// in `strictly_i32_bounded_locals` (`i++` disqualifies a local there, #6072). +// Repsel Phase 1, #7110/#7123: canonical unboxed i32 storage for monotone loop +// induction variables and accumulators bounded by trip count times step +// magnitude. These locals are NOT used as array indices and are NOT in +// `strictly_i32_bounded_locals` (`i++`/self-addition disqualify them there). // // Byte-compared against `node --experimental-strip-types`. Every number below // is chosen so that a WRONG answer is loud rather than plausible: the values // sit on the i32 boundary, where an unsound admission wraps to a large negative // instead of drifting by one. // -// The three functions the analysis must REFUSE (`overshoot`, `runtimeBound`, -// `accumulate`) are the point of this file as much as the ones it admits. An +// The functions the analysis must REFUSE (`overshoot`, `runtimeBound`, and the +// overflowing accumulator) are the point of this file as much as the ones it +// admits. An // i32 slot for any of them prints a wrapped negative here, and Node prints the // true value. Keep them. @@ -111,12 +113,21 @@ function runtimeBound(limit: number): number { return i; } -// A bare accumulator has no guard bounding it. `benchmarks/suite/13_factorial.ts` -// is the same shape at 1e8 iterations, where the true total is 49,950,000,000. -function accumulate(): number { +// #7123 admits the bounded counterpart: 4096 * 1 fits in i32. +function boundedAccumulator(): number { let sum = 0; for (let i = 0; i < ROUNDS; i++) { - sum = sum + 1000000; + sum = sum + 1; + } + return sum; +} + +// Three writes of one billion leave i32 immediately. If the range check is +// removed, canonical storage wraps and this prints a different number. +function overflowingAccumulator(): number { + let sum = 0; + for (let i = 0; i < 3; i++) { + sum = sum + 1000000000; } return sum; } @@ -162,6 +173,7 @@ console.log("twoSteps:" + twoSteps()); console.log("observed:" + observed()); console.log("overshoot:" + overshoot()); console.log("runtimeBound:" + runtimeBound(2147483653)); -console.log("accumulate:" + accumulate()); +console.log("boundedAccumulator:" + boundedAccumulator()); +console.log("overflowingAccumulator:" + overflowingAccumulator()); console.log("bigStepOverflow:" + bigStepOverflow()); console.log("bigStepUnderflow:" + bigStepUnderflow()); diff --git a/test-parity/gc_repsel_corpus.txt b/test-parity/gc_repsel_corpus.txt index 92b91fc148..e6dafc8811 100644 --- a/test-parity/gc_repsel_corpus.txt +++ b/test-parity/gc_repsel_corpus.txt @@ -32,10 +32,10 @@ test_gap_int_valued_ta_locals # --- Phase 1 widening: constant-bounded loop induction variables (#7110) ---- # A counter that is neither index-used nor `strictly_i32_bounded` now takes # canonical i32 storage when the loop guard pins its whole interval inside i32. -# Three functions in the file are there to be REFUSED (`overshoot`, -# `runtimeBound`, `accumulate`); an i32 slot for any of them prints a wrapped -# negative where Node prints the true value, so this file fails loudly under an -# unsound widening rather than drifting by one. +# #7123 also admits a loop accumulator when trip count times step magnitude +# fits i32. The file's refusal probes (`overshoot`, `runtimeBound`, and +# `overflowingAccumulator`) print wrapped values under an unsound widening, so +# this fails loudly rather than merely changing an optimization report. test_gap_repsel_loop_bounded_i32 # --- Phase 2: specialized calling convention / spec-ABI raw params (#6905) --