perf(repsel): bound loop accumulators for i32

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,

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.

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.

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();