From b82c70d5de2853a368f13edb96ced5f14061fe2e Mon Sep 17 00:00:00 2001
From: Chris Tate <chris@ctate.dev>
Date: Thu, 22 Oct 2026 09:56:19 -0500
Subject: [PATCH] Bound a follower's trip count only by a safe-integer span

The trip count that bounds a follower's range was the driver's span over
its step, computed in doubles. A span above 2^53 - 1 can round down: from
-(2^53 - 1) to below 2^52 - 1 the span 3 * 2^52 - 3 becomes 3 * 2^52 - 4,
so a follower that reaches 2^53 got the range limit 2^53 - 1 and ran as an
unchecked integer. Such a span now bounds no trip count, and the follower
is tested at run time (or the loop is refused when every value is known).
Below it the quotient rounds to at least its floor, and the follower's
products and sums are exact within the safe range.
---
 packages/compiler/src/ir/integer-loops.test.ts | 16 ++++++++++++++++
 packages/compiler/src/ir/integer-loops.ts      | 10 ++++++----
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/packages/compiler/src/ir/integer-loops.test.ts b/packages/compiler/src/ir/integer-loops.test.ts
index e1453abad..b6ac27e3a 100644
--- a/packages/compiler/src/ir/integer-loops.test.ts
+++ b/packages/compiler/src/ir/integer-loops.test.ts
@@ -525,4 +525,20 @@ test("counters stepped beside the tested one run as integers", () => {
   boxed.set("j", { ...vars.get("j")!, boxed: true });
   expect(matchIntegerCountedForLoop(comoving(number(10)), boxed)).toBeNull();
   expect(matchIntegerCountedForLoop(comoving(number(10), ref("i")), vars)).toBeNull();
+  // A driver span above 2^53 - 1 bounds no trip count. From -(2^53 - 1) to
+  // below 2^52 - 1 the span 3 * 2^52 - 3 rounds down to 3 * 2^52 - 4, which
+  // would put this follower's last value at 2^53 - 1 instead of 2^53.
+  const wide = comoving(number(2 ** 52 - 1), number(-(2 ** 52) + 3), {
+    kind: "block",
+    body: [step("i", "+"), step("j", "+")],
+    loc,
+  });
+  if (wide.init?.kind === "block" && wide.init.body[0]?.kind === "varDecl")
+    wide.init.body[0].init = number(-Number.MAX_SAFE_INTEGER);
+  expect(matchIntegerCountedForLoop(wide, vars)).toBeNull();
+  if (wide.init?.kind === "block" && wide.init.body[1]?.kind === "varDecl")
+    wide.init.body[1].init = ref("from");
+  expect(matchIntegerCountedForLoop(wide, vars)?.followers).toMatchObject([
+    { startGuarded: true, tripGuarded: true },
+  ]);
 });
diff --git a/packages/compiler/src/ir/integer-loops.ts b/packages/compiler/src/ir/integer-loops.ts
index c4cdc327c..c451c0852 100644
--- a/packages/compiler/src/ir/integer-loops.ts
+++ b/packages/compiler/src/ir/integer-loops.ts
@@ -269,10 +269,12 @@ export function matchIntegerCountedForLoop(
         };
   // On body entry k the driver holds `start + step * k`, so k is at most the
   // driver's span over |step|, and a follower holds its start plus its own
-  // step times k.
-  const trips = Math.floor(
-    (step > 0 ? range.max - startRange.min : startRange.max - range.min) / Math.abs(step),
-  );
+  // step times k. A span above 2^53 - 1 can round down, so it bounds no
+  // trip count. Below it the quotient rounds to at least its floor, and the
+  // follower's products and sums below are exact while they stay within
+  // ±(2^53 - 1) and round outside it otherwise.
+  const span = step > 0 ? range.max - startRange.min : startRange.max - range.min;
+  const trips = span <= Number.MAX_SAFE_INTEGER ? Math.floor(span / Math.abs(step)) : Infinity;
   const followers: IntegerLoopFollower[] = [];
   for (const id of counterIds) {
     if (id === local.id) continue;