diff --git a/packages/compiler/src/backend/llvm/emit-function.ts b/packages/compiler/src/backend/llvm/emit-function.ts
index 78f208ff1..c26c93b84 100644
--- a/packages/compiler/src/backend/llvm/emit-function.ts
+++ b/packages/compiler/src/backend/llvm/emit-function.ts
@@ -27,7 +27,7 @@ import { findMapEntryFusions } from "./map-entry-fusion.js";
 import { findLocalStackUnions } from "./stack-unions.js";
 import { findLocalStackObjects, findReassignedStackObjects } from "./stack-objects.js";
 import { findLocalUnionStorage } from "./local-union-storage.js";
-import { INT32_RANGE, analyzeIntegerRanges } from "../../ir/integer-ranges.js";
+import { INT32_RANGE, analyzeIntegerRangeFacts } from "../../ir/integer-ranges.js";
 import { findBytesBounds } from "./bytes-bounds.js";
 import { findInt32Locals } from "./int32-locals.js";
 import { findIntegerViews } from "./integer-views.js";
@@ -217,7 +217,9 @@ export function emitFunction(emitter: LlEmitter, fn: IrFunction): string {
   emitter.localUnionStorage = new Map();
   emitter.walkBorrows = emitter.walkBorrowsByFunction.get(fn.name) ?? new Set();
   const slotFacts = emitter.int32Slots.facts(fn.name);
-  emitter.integerRanges = analyzeIntegerRanges(numericFn, slotFacts);
+  const rangeFacts = analyzeIntegerRangeFacts(numericFn, slotFacts);
+  emitter.integerRanges = rangeFacts.ranges;
+  emitter.integerLoopRanges = rangeFacts.loopRanges;
   emitter.int32Elements = slotFacts.elements ?? null;
   emitter.bytesBounds = findBytesBounds(numericFn, emitter.integerRanges);
   // Debug builds keep every number local a double for the debugger's
diff --git a/packages/compiler/src/backend/llvm/emit-statements.ts b/packages/compiler/src/backend/llvm/emit-statements.ts
index e641f3ecd..1a6e73c17 100644
--- a/packages/compiler/src/backend/llvm/emit-statements.ts
+++ b/packages/compiler/src/backend/llvm/emit-statements.ts
@@ -50,7 +50,9 @@ import {
   SPECULATIVE_RANGE,
   emitSafeIntegerCheck,
   emitSpeculativeInteger,
+  planProvenIntegerLoop,
   planSpeculativeLoop,
+  type ProvenLoopPlan,
   speculativeReads,
   speculativeWriteTarget,
 } from "./speculative-integers.js";
@@ -1765,7 +1767,9 @@ export function emitLoopCopies(
         )
       : null;
   if (!plan) {
-    emitCopy(exit);
+    const proven = allowed ? planProvenLoop(emitter, loop) : null;
+    if (proven) emitProvenLoop(emitter, proven, exit, emitCopy);
+    else emitCopy(exit);
     return;
   }
   const B = emitter.B;
@@ -1844,7 +1848,7 @@ export function emitLoopCopies(
       const leave = B.newLabel("spec.leave");
       emitCopy(leave);
       B.startBlock(leave);
-      emitter.writeBackSpeculativeGlobals(deferred);
+      emitter.writeBackDeferred(deferred);
       B.br(exit);
     }
   } finally {
@@ -1853,10 +1857,91 @@ export function emitLoopCopies(
   }
 }
 
+/** A proven integer loop (speculative-integers.ts) for this loop, or null.
+ * A shadowed local's double is stale until the loop is left, which only
+ * the loop's exit, a return and an exception do: the loop is planned only
+ * where an exception leaves the function (no enclosing try or finally, no
+ * coroutine frame), so no handler reads the stale double. */
+function planProvenLoop(
+  emitter: LlEmitter,
+  loop: Extract<IrStmt, { kind: "while" | "doWhile" | "for" }>,
+): ProvenLoopPlan | null {
+  if (
+    loop.kind !== "for" ||
+    !emitter.speculativeLoopsEnabled ||
+    emitter.speculation !== null ||
+    emitter.speculationResume !== null ||
+    emitter.tryStack.length > 0 ||
+    emitter.finallyStack.length > 0 ||
+    emitter.currentCoro !== null
+  )
+    return null;
+  const cursors = emitter.integerLoopRanges.get(loop);
+  if (!cursors) return null;
+  return planProvenIntegerLoop(
+    loop,
+    cursors,
+    (id) => emitter.currentLocals.has(id) && emitter.speculativeLocal(id),
+    (id) => emitter.integerLoopBindings.has(id) || emitter.int32Locals.has(id),
+    (e) => {
+      const range = emitter.integerRanges.get(e);
+      return (
+        range !== undefined &&
+        range !== null &&
+        range.min >= -Number.MAX_SAFE_INTEGER &&
+        range.max <= Number.MAX_SAFE_INTEGER
+      );
+    },
+  );
+}
+
+/** Emit a proven integer loop: its shadowed locals start from their
+ * doubles (integers in their loop ranges on entry), its planned writes
+ * compute integers into the shadows only, and leaving the loop through its
+ * exit writes each double back. */
+function emitProvenLoop(
+  emitter: LlEmitter,
+  plan: ProvenLoopPlan,
+  exit: string,
+  emitCopy: (exit: string) => void,
+): void {
+  const B = emitter.B;
+  for (const [id, range] of plan.locals) {
+    const shadow = B.slot();
+    B.entryAllocas.push(
+      `${shadow} = alloca i64 ; integer ${emitter.currentLocals.get(id)?.name ?? id}`,
+    );
+    const value = B.tmp(),
+      integer = B.tmp();
+    B.line(`${value} = load double, ptr ${emitter.binding(id).slot}`);
+    B.line(`${integer} = fptosi double ${value} to i64`);
+    B.line(`store i64 ${integer}, ptr ${shadow}`);
+    emitter.integerLoopBindings.set(id, { slot: shadow, type: "i64", signed: true, range });
+  }
+  const deferred = new Set<string>();
+  for (const id of plan.locals.keys()) deferred.add(id);
+  emitter.speculation = { writes: plan.writes, resume: new Map(), deferred };
+  try {
+    const leave = B.newLabel("integer.leave");
+    emitCopy(leave);
+    B.startBlock(leave);
+    emitter.writeBackDeferred(deferred);
+    B.br(exit);
+  } finally {
+    emitter.speculation = null;
+    for (const id of plan.locals.keys()) emitter.integerLoopBindings.delete(id);
+  }
+}
+
 /** A speculated write in the fast copy: compute the value as a safe
  * integer, store it to the shadow and its exact double to the local.
- * Any failed check re-executes the statement in the ordinary copy. */
-export function emitSpeculativeWrite(emitter: LlEmitter, s: IrStmt, resume: string): void {
+ * Any failed check re-executes the statement in the ordinary copy. A
+ * proven integer loop's write (no `resume`) has nothing to check. */
+export function emitSpeculativeWrite(
+  emitter: LlEmitter,
+  s: IrStmt,
+  resume: string | undefined,
+): void {
   const B = emitter.B;
   const target = speculativeWriteTarget(s)!;
   const binding = emitter.integerLoopBindings.get(target.localId)!;
@@ -1864,7 +1949,7 @@ export function emitSpeculativeWrite(emitter: LlEmitter, s: IrStmt, resume: stri
   let bails = false;
   emitter.declare("declare i1 @llvm.expect.i1(i1, i1)");
   const bail = (condition: string): void => {
-    if (condition === "false") return;
+    if (condition === "false" || resume === undefined) return;
     bails = true;
     const expected = B.tmp();
     B.line(`${expected} = call i1 @llvm.expect.i1(i1 ${condition}, i1 false)`);
@@ -1893,7 +1978,7 @@ export function emitSpeculativeWrite(emitter: LlEmitter, s: IrStmt, resume: stri
     B.line(`${biased} = add i64 ${result}, ${Number.MAX_SAFE_INTEGER}`);
     B.line(`${outside} = icmp ugt i64 ${biased}, ${2 * Number.MAX_SAFE_INTEGER}`);
     bail(outside);
-  } else result = emitSpeculativeInteger(emitter, target.value, bail, reads);
+  } else result = emitSpeculativeInteger(emitter, target.value, bail, reads, resume === undefined);
   // Speculable values read only numbers past this point.
   if (emitter.frames.pop()!.length > 0)
     throw new InternalCompilerError("llvm emitter bug: speculative write owns a temporary");
@@ -1908,8 +1993,8 @@ export function emitSpeculativeWrite(emitter: LlEmitter, s: IrStmt, resume: stri
   const done = B.newLabel("spec.done");
   B.br(done);
   B.startBlock(failed);
-  emitter.writeBackSpeculativeGlobals(deferred);
-  B.br(resume);
+  emitter.writeBackDeferred(deferred);
+  B.br(resume!);
   B.startBlock(done);
 }
 
diff --git a/packages/compiler/src/backend/llvm/emitter.ts b/packages/compiler/src/backend/llvm/emitter.ts
index 1d745b981..adee90840 100644
--- a/packages/compiler/src/backend/llvm/emitter.ts
+++ b/packages/compiler/src/backend/llvm/emitter.ts
@@ -1022,6 +1022,8 @@ export class LlEmitter {
    * not a constructor (where they change), not async or a generator. */
   finalFieldBorrows = false;
   integerRanges: IntegerRanges = new Map();
+  /** The current function's bounded for-loop cursors (integer-ranges.ts). */
+  integerLoopRanges: ReadonlyMap<IrStmt, ReadonlyMap<string, IntegerRange>> = new Map();
   /** Number arrays of the current function whose every present element is
    * an int32 (Int32[] contracts), or null when the module has none. */
   int32Elements: ((arr: IrExpr) => boolean) | null = null;
@@ -2653,7 +2655,8 @@ export class LlEmitter {
     return emitLoopCopies(this, loop, allowed, exit, emitCopy);
   }
 
-  writeBackSpeculativeGlobals(deferred: Set<string>): void {
+  /** Store the double of each deferred shadow back to its binding. */
+  writeBackDeferred(deferred: Set<string>): void {
     const B = this.B;
     for (const id of deferred) {
       const integer = B.tmp(),
@@ -2732,7 +2735,7 @@ export class LlEmitter {
     }
     return this.globalWriters.get(id) ?? new Set<string>();
   }
-  private emitSpeculativeWrite(s: IrStmt, resume: string): void {
+  private emitSpeculativeWrite(s: IrStmt, resume: string | undefined): void {
     return emitSpeculativeWrite(this, s, resume);
   }
 
@@ -4378,7 +4381,7 @@ export class LlEmitter {
       this.B.startBlock(resume.label);
     }
     if (this.speculation?.writes.has(s)) {
-      this.emitSpeculativeWrite(s, this.speculation.resume.get(s)!);
+      this.emitSpeculativeWrite(s, this.speculation.resume.get(s));
       return;
     }
     const previous = this.B.debugLocation;
diff --git a/packages/compiler/src/backend/llvm/speculative-integers.test.ts b/packages/compiler/src/backend/llvm/speculative-integers.test.ts
index ae9172298..3acfec0fb 100644
--- a/packages/compiler/src/backend/llvm/speculative-integers.test.ts
+++ b/packages/compiler/src/backend/llvm/speculative-integers.test.ts
@@ -2,6 +2,7 @@ import { expect, test } from "vitest";
 import { F64, type IrExpr, type IrStmt } from "../../ir/ir.js";
 import {
   isSpeculableValue,
+  planProvenIntegerLoop,
   planSpeculativeLoop,
   speculativeReads,
 } from "./speculative-integers.js";
@@ -194,3 +195,74 @@ test("loops that only count and compare keep one copy", () => {
   ]);
   expect(planSpeculativeLoop(scaled as never, all)?.locals.has("n")).toBe(true);
 });
+
+test("bounded cursors with proven writes are shadowed in a proven integer loop", () => {
+  // for (i = 0; i < n; i++) { if (a < b) run = run + 1; else run = 0;
+  //   if (run > longest) longest = run; }
+  const sum = bin("+", ref("run"), num(1));
+  const step = assign("run", sum);
+  const reset = assign("run", num(0));
+  const copy = assign("longest", ref("run"));
+  const forLoop = (body: IrStmt[]): IrStmt => ({
+    kind: "for",
+    init: null,
+    cond: bin("<", ref("i"), ref("n")),
+    update: assign("i", bin("+", ref("i"), num(1))),
+    body,
+    loc,
+  });
+  const branch = (then: IrStmt[], else_: IrStmt[] | null): IrStmt => ({
+    kind: "if",
+    cond: bin("<", ref("a"), ref("b")),
+    then,
+    else_,
+    loc,
+  });
+  const body = [branch([step], [reset]), branch([copy], null)];
+  const range = { min: 0, max: 100 };
+  const cursors = new Map([
+    ["run", range],
+    ["longest", range],
+  ]);
+  const plan = planProvenIntegerLoop(forLoop(body) as never, cursors, all, () => false, all)!;
+  expect([...plan.locals]).toEqual([
+    ["run", range],
+    ["longest", range],
+  ]);
+  expect(plan.writes).toEqual(new Set([step, reset, copy]));
+  // A binding the loop does not bound keeps its double.
+  const only = planProvenIntegerLoop(
+    forLoop(body) as never,
+    new Map([["run", range]]),
+    all,
+    () => false,
+    all,
+  )!;
+  expect([...only.locals.keys()]).toEqual(["run"]);
+  // An unproven sum leaves `run` unshadowed, and its copy reads `run`
+  // where nothing proves it integral.
+  const unproven = (e: IrExpr): boolean => e !== sum && e.kind !== "varRef";
+  expect(
+    planProvenIntegerLoop(forLoop(body) as never, cursors, all, () => false, unproven),
+  ).toBeNull();
+  // An expression-position write refuses the binding.
+  const inner: IrStmt = {
+    kind: "exprStmt",
+    expr: { kind: "incDec", op: "+", prefix: false, localId: "longest", type: F64, loc },
+    loc,
+  };
+  expect([
+    ...planProvenIntegerLoop(
+      forLoop([...body, inner]) as never,
+      cursors,
+      all,
+      () => false,
+      all,
+    )!.locals.keys(),
+  ]).toEqual(["run"]);
+  // A labeled jump may leave past the write-back.
+  const jump: IrStmt = { kind: "break", label: "outer", loc };
+  expect(
+    planProvenIntegerLoop(forLoop([...body, jump]) as never, cursors, all, () => false, all),
+  ).toBeNull();
+});
diff --git a/packages/compiler/src/backend/llvm/speculative-integers.ts b/packages/compiler/src/backend/llvm/speculative-integers.ts
index cf1295fa2..a309a9785 100644
--- a/packages/compiler/src/backend/llvm/speculative-integers.ts
+++ b/packages/compiler/src/backend/llvm/speculative-integers.ts
@@ -3,7 +3,7 @@ import { everyExprChild, everyStmtChild } from "../../ir/traverse.js";
 import { f64Lit } from "./common.js";
 import type { LlValue, LlvmEmitterContext } from "./expr-context.js";
 import { exactInteger, widenInteger } from "./integer-values.js";
-import { withinInt32 } from "../../ir/integer-ranges.js";
+import { type IntegerRange, withinInt32 } from "../../ir/integer-ranges.js";
 
 /** Speculative integer loops.
  *
@@ -410,6 +410,97 @@ export function planSpeculativeLoop(
   return { locals, writes: speculated, observerFree };
 }
 
+/** A proven integer loop. The bindings integer-ranges.ts bounds over a for
+ * loop (`loopRanges`) hold an integer on entry and at every write, so the
+ * loop keeps them in i64 shadow slots without a second copy or checks, and
+ * writes their doubles once, when it is left. */
+export interface ProvenLoopPlan {
+  /** Shadowed bindings and their loop ranges. */
+  locals: Map<string, IntegerRange>;
+  /** Statement-level writes computed as integers. */
+  writes: Set<IrStmt>;
+}
+
+/** Plan a proven integer loop. `cursors` are the loop's bounded bindings,
+ * `eligible` the locals a shadow may stand for, `integral` those the emitter
+ * already holds as integers and `proven` the expressions the range analysis
+ * proves integral. A shadowed binding's double is stale until the loop is
+ * left, so every exit has to pass the write-back: the caller plans only
+ * loops where an exception leaves the function, and a labeled jump (which
+ * may leave past the write-back) keeps the loop ordinary. */
+export function planProvenIntegerLoop(
+  loop: SpeculativeLoop,
+  cursors: ReadonlyMap<string, IntegerRange>,
+  eligible: (localId: string) => boolean,
+  integral: (localId: string) => boolean,
+  proven: (e: IrExpr) => boolean,
+): ProvenLoopPlan | null {
+  if (cursors.size === 0) return null;
+  const writes = new Map<string, IrStmt[]>();
+  const refused = new Set<string>();
+  let rejected = false;
+  const expr = (e: IrExpr): boolean => {
+    if (e.kind === "assignExpr" || e.kind === "incDec") refused.add(e.localId);
+    return everyExprChild(e, expr, nested);
+  };
+  const nested = (s: IrStmt): boolean => {
+    if (s.kind === "assign" || s.kind === "varDecl") refused.add(s.localId);
+    return everyStmtChild(s, expr, nested);
+  };
+  const stmt = (s: IrStmt): boolean => {
+    if (rejected) return false;
+    if (
+      !SIMPLE_STATEMENTS.has(s.kind) ||
+      ((s.kind === "break" || s.kind === "continue") && s.label !== undefined)
+    ) {
+      rejected = true;
+      return false;
+    }
+    const target = s.kind === "varDecl" ? null : speculativeWriteTarget(s);
+    if (target) {
+      if (target.value !== null && cursors.has(target.localId)) {
+        const list = writes.get(target.localId) ?? [];
+        list.push(s);
+        writes.set(target.localId, list);
+      } else refused.add(target.localId);
+      return target.value === null || expr(target.value);
+    }
+    if (s.kind === "varDecl") refused.add(s.localId);
+    return everyStmtChild(s, expr, stmt);
+  };
+  if (loop.cond) expr(loop.cond);
+  if (loop.kind === "for" && loop.update) nested(loop.update);
+  for (const s of loop.body) stmt(s);
+  if (rejected) return null;
+  const locals = new Map<string, IntegerRange>();
+  for (const [id, list] of writes) {
+    if (refused.has(id) || !eligible(id)) continue;
+    const exact = list.every((s) => {
+      const value = speculativeWriteTarget(s)!.value!;
+      return isSpeculableValue(value, false) && proven(value);
+    });
+    if (exact) locals.set(id, cursors.get(id)!);
+  }
+  // Every binding a shadowed write reads is shadowed, already an integer,
+  // or proven integral where it is read.
+  const grounded = (e: IrExpr): boolean =>
+    e.kind === "varRef"
+      ? locals.has(e.localId) || integral(e.localId) || proven(e)
+      : everyExprChild(e, grounded, () => false);
+  for (let changed = true; changed;) {
+    changed = false;
+    for (const id of [...locals.keys()])
+      if (!writes.get(id)!.every((s) => grounded(speculativeWriteTarget(s)!.value!))) {
+        locals.delete(id);
+        changed = true;
+      }
+  }
+  if (locals.size === 0) return null;
+  const planned = new Set<IrStmt>();
+  for (const id of locals.keys()) for (const s of writes.get(id)!) planned.add(s);
+  return { locals, writes: planned };
+}
+
 const SAFE = Number.MAX_SAFE_INTEGER;
 
 /** The range every speculative shadow holds. */
@@ -501,11 +592,14 @@ export function emitSpeculativeInteger(
   e: IrExpr,
   bail: (condition: string) => void,
   reads: ReadonlyMap<IrExpr, LlValue> = new Map(),
+  integral = false,
 ): string {
   const B = host.B;
   // A value the range analysis already proves takes the ordinary integer
-  // emission, which needs no checks.
-  const proven = e.kind === "bin" ? host.integerRanges.get(e) : undefined;
+  // emission, which needs no checks. A proven integer loop's write
+  // (`integral`) is proven throughout and computes its operands as integers
+  // instead: the ordinary emission of a sum past int32 is a double.
+  const proven = e.kind === "bin" && !integral ? host.integerRanges.get(e) : undefined;
   if (proven && proven.min >= -SAFE && proven.max <= SAFE && speculativeReads(e).length === 0)
     return speculativeLeaf(host, host.emitExpr(e), e, bail);
   switch (e.kind) {
@@ -533,8 +627,8 @@ export function emitSpeculativeInteger(
     }
     case "bin": {
       if (e.op !== "+" && e.op !== "-" && e.op !== "*" && e.op !== "%") break;
-      const a = emitSpeculativeInteger(host, e.left, bail, reads);
-      const b = emitSpeculativeInteger(host, e.right, bail, reads);
+      const a = emitSpeculativeInteger(host, e.left, bail, reads, integral);
+      const b = emitSpeculativeInteger(host, e.right, bail, reads, integral);
       const result = B.tmp();
       if (e.op === "+" || e.op === "-") {
         // With one operand's range known, the other is checked against the
@@ -590,7 +684,7 @@ export function emitSpeculativeInteger(
     }
     case "unary": {
       if (e.op !== "-") break;
-      const a = emitSpeculativeInteger(host, e.operand, bail, reads);
+      const a = emitSpeculativeInteger(host, e.operand, bail, reads, integral);
       const zero = B.tmp(),
         result = B.tmp();
       // -0 is not an integer result.
diff --git a/packages/compiler/src/ir/integer-loop-facts.ts b/packages/compiler/src/ir/integer-loop-facts.ts
index 84fabf956..d207c4c12 100644
--- a/packages/compiler/src/ir/integer-loop-facts.ts
+++ b/packages/compiler/src/ir/integer-loop-facts.ts
@@ -36,6 +36,11 @@ function variableIncrement(id: string, value: IrExpr): { localId: string; sign:
  * filtering, breaks and continues can only reduce the budget. A nested
  * loop or opaque control region invalidates the bindings it writes.
  *
+ * A cursor may also be reset to an integer literal (`run = 0`) or set to
+ * another bounded binding (`longest = run`): every value it then holds is
+ * its entry value, a reset value or a value the source held, plus at most
+ * the increments of the whole loop.
+ *
  * The counter's step is a positive integer literal or a binding the loop
  * never writes whose entry fact is a positive integer range (the sieve's
  * `j += i`): every update then adds an exact integer in that range, so the
@@ -68,6 +73,8 @@ export function boundedIntegerLoopFacts(
     refused = new Set<string>();
   const lower = new Map<string, number>(),
     upper = new Map<string, number>();
+  const resets = new Map<string, IntegerRange>(),
+    copies = new Map<string, Set<string>>();
   let opaque = 0;
   const write = (id: string, delta: number | null): void => {
     written.add(id);
@@ -81,8 +88,29 @@ export function boundedIntegerLoopFacts(
     lower.set(id, lo);
     upper.set(id, hi);
   };
+  const assignment = (id: string, value: IrExpr): void => {
+    const delta = increment(id, value);
+    if (opaque || delta !== null) write(id, delta);
+    else if (
+      value.kind === "numLit" &&
+      Number.isSafeInteger(value.value) &&
+      !Object.is(value.value, -0)
+    ) {
+      written.add(id);
+      const range = resets.get(id);
+      resets.set(id, {
+        min: Math.min(range?.min ?? value.value, value.value),
+        max: Math.max(range?.max ?? value.value, value.value),
+      });
+    } else if (value.kind === "varRef" && value.localId !== id) {
+      written.add(id);
+      const sources = copies.get(id) ?? new Set<string>();
+      sources.add(value.localId);
+      copies.set(id, sources);
+    } else write(id, null);
+  };
   const expr = (e: IrExpr): boolean => {
-    if (e.kind === "assignExpr") write(e.localId, increment(e.localId, e.value));
+    if (e.kind === "assignExpr") assignment(e.localId, e.value);
     if (e.kind === "incDec") write(e.localId, e.op === "+" ? 1 : -1);
     return everyExprChild(e, expr, stmt);
   };
@@ -95,7 +123,7 @@ export function boundedIntegerLoopFacts(
       s.kind === "tryCatch" ||
       s.kind === "switch";
     if (region) opaque++;
-    if (s.kind === "assign") write(s.localId, increment(s.localId, s.value));
+    if (s.kind === "assign") assignment(s.localId, s.value);
     if (s.kind === "varDecl" || s.kind === "forOf") write(s.localId, null);
     const completed = everyStmtChild(s, expr, stmt);
     if (region) opaque--;
@@ -147,15 +175,45 @@ export function boundedIntegerLoopFacts(
   // Header facts also cover the failing final condition and zero iterations.
   const maximum = Math.max(start.max, last + step.max);
   if (Number.isSafeInteger(maximum)) result.set(counter, { min: start.min, max: maximum });
-  for (const [id, hi] of upper) {
-    const range = initial.get(id);
-    if (!range || refused.has(id) || id === counter) continue;
-    const decrement = iterations * lower.get(id)!;
-    const increment = iterations * hi;
-    if (!Number.isSafeInteger(decrement) || !Number.isSafeInteger(increment)) continue;
-    const min = range.min + decrement;
-    const max = range.max + increment;
-    if (Number.isSafeInteger(min) && Number.isSafeInteger(max)) result.set(id, { min, max });
+  // Every value a copy reads lies in its source's range: a cursor bounded
+  // here, or a binding the loop never writes.
+  const source = (id: string): IntegerRange | undefined =>
+    result.get(id) ?? (stable(id) ? initial.get(id) : undefined);
+  // Copies wait for their sources; a cycle of copies stays unbounded.
+  for (let changed = true; changed;) {
+    changed = false;
+    for (const id of written) {
+      const range = initial.get(id);
+      if (!range || refused.has(id) || id === counter || result.has(id)) continue;
+      let min = range.min,
+        max = range.max;
+      const reset = resets.get(id);
+      if (reset) {
+        min = Math.min(min, reset.min);
+        max = Math.max(max, reset.max);
+      }
+      let bounded = true;
+      const sources = copies.get(id);
+      if (sources)
+        for (const from of sources) {
+          const copied = source(from);
+          if (!copied) bounded = false;
+          else {
+            min = Math.min(min, copied.min);
+            max = Math.max(max, copied.max);
+          }
+        }
+      if (!bounded) continue;
+      const decrement = iterations * (lower.get(id) ?? 0);
+      const increment = iterations * (upper.get(id) ?? 0);
+      if (!Number.isSafeInteger(decrement) || !Number.isSafeInteger(increment)) continue;
+      min += decrement;
+      max += increment;
+      if (Number.isSafeInteger(min) && Number.isSafeInteger(max)) {
+        result.set(id, { min, max });
+        changed = true;
+      }
+    }
   }
   return result;
 }
diff --git a/packages/compiler/src/ir/integer-ranges.test.ts b/packages/compiler/src/ir/integer-ranges.test.ts
index 8e1c97f66..6605e1d23 100644
--- a/packages/compiler/src/ir/integer-ranges.test.ts
+++ b/packages/compiler/src/ir/integer-ranges.test.ts
@@ -1,5 +1,6 @@
 import { expect, test } from "vitest";
 import {
+  analyzeIntegerRangeFacts,
   analyzeIntegerRanges,
   bitwiseIdentityOperand,
   bitwiseRange,
@@ -1041,3 +1042,119 @@ test("bitwise identity operands follow ToInt32 and the shift-count mask", () =>
   expect(identity("<<", num(0), x)).toBeNull();
   expect(identity(">>>", num(0), x)).toBeNull();
 });
+
+test("a for loop bounds cursors it resets and copies, and their writes keep the loop range", () => {
+  // for (x = 0; x < 100; x++) { if (flag === 0) run = run + 1; else run = 0;
+  //   if (run > longest) longest = run; changes = changes + 1; }
+  const sum = bin("+", ref("run"), num(1)),
+    copied = ref("run"),
+    counted = bin("+", ref("changes"), num(1));
+  const write = (localId: string, value: IrExpr): IrStmt => ({
+    loc,
+    kind: "assign",
+    localId,
+    value,
+  });
+  const loop: IrStmt & { kind: "for" } = {
+    loc,
+    kind: "for",
+    init: { loc, kind: "varDecl", localId: "x", init: num(0) },
+    cond: condition("<", ref(), num(100)),
+    update: assign(bin("+", ref(), num(1))),
+    body: [
+      {
+        loc,
+        kind: "if",
+        cond: condition("===", ref("flag"), num(0)),
+        then: [write("run", sum)],
+        else_: [write("run", num(0))],
+      },
+      {
+        loc,
+        kind: "if",
+        cond: condition(">", ref("run"), ref("longest")),
+        then: [write("longest", copied)],
+        else_: null,
+      },
+      write("changes", counted),
+    ],
+  };
+  const declare = (localId: string): IrStmt => ({ loc, kind: "varDecl", localId, init: num(0) });
+  const f = fn([declare("run"), declare("longest"), declare("changes"), loop]);
+  f.locals.push(
+    ...["run", "longest", "changes", "flag"].map((id) => ({
+      id,
+      name: id,
+      type: F64,
+      mutable: true,
+    })),
+  );
+  const ranges = analyzeIntegerRanges(f);
+  // Each of the 100 passes adds at most one, so `run + 1` and
+  // `changes + 1` stay within the loop range though their operands reach it.
+  const range = { min: 0, max: 100 };
+  expect(ranges.get(sum)).toEqual({ min: 1, max: 100 });
+  expect(ranges.get(counted)).toEqual({ min: 1, max: 100 });
+  expect(ranges.get(copied)).toEqual({ min: 1, max: 100 });
+  expect(analyzeIntegerRangeFacts(f).loopRanges.get(loop)).toEqual(
+    new Map([
+      ["run", range],
+      ["longest", range],
+      ["changes", range],
+    ]),
+  );
+  for (const mutation of ["fraction", "cycle", "nested"] as const) {
+    const changed = structuredClone(f);
+    const body = (changed.body[3] as IrStmt & { kind: "for" }).body;
+    if (mutation === "fraction") body.push(write("run", num(0.5)));
+    // `run = longest` and `longest = run` bound neither.
+    if (mutation === "cycle") body.push(write("run", ref("longest")));
+    if (mutation === "nested")
+      body.push({
+        loc,
+        kind: "while",
+        cond: condition("<", ref("unknown"), num(1)),
+        body: [write("run", num(0))],
+      });
+    const cursors = analyzeIntegerRangeFacts(changed).loopRanges.get(changed.body[3]!);
+    expect(cursors?.has("run"), mutation).toBe(false);
+    expect(cursors?.get("changes"), mutation).toEqual(range);
+  }
+});
+
+test("a cursor of a loop over a typed array keeps its writes exact up to 2^53 - 1", () => {
+  // for (x = 0; x < bytes.length; x++) changes = changes + 1;
+  const bytes: IrExpr = {
+    loc,
+    kind: "varRef",
+    localId: "bytes",
+    type: { kind: "bytes", elem: "u8" },
+  };
+  const length: IrExpr = {
+    loc,
+    kind: "bytesIntrinsic",
+    method: "length",
+    receiver: bytes,
+    args: [],
+    type: F64,
+  };
+  const counted = bin("+", ref("changes"), num(1));
+  const f = fn([
+    { loc, kind: "varDecl", localId: "changes", init: num(0) },
+    {
+      loc,
+      kind: "for",
+      init: { loc, kind: "varDecl", localId: "x", init: num(0) },
+      cond: condition("<", ref(), length),
+      update: assign(bin("+", ref(), num(1))),
+      body: [{ loc, kind: "assign", localId: "changes", value: counted }],
+    },
+  ]);
+  f.locals.push(
+    { id: "changes", name: "changes", type: F64, mutable: true },
+    { id: "bytes", name: "bytes", type: { kind: "bytes", elem: "u8" }, mutable: false },
+  );
+  // The sum of the header range passes 2^53 - 1; the write takes the loop
+  // range instead.
+  expect(analyzeIntegerRanges(f).get(counted)).toEqual({ min: 0, max: Number.MAX_SAFE_INTEGER });
+});
diff --git a/packages/compiler/src/ir/integer-ranges.ts b/packages/compiler/src/ir/integer-ranges.ts
index 5c365e2ca..8755bdac2 100644
--- a/packages/compiler/src/ir/integer-ranges.ts
+++ b/packages/compiler/src/ir/integer-ranges.ts
@@ -15,6 +15,13 @@ export interface IntegerRange {
   max: number;
 }
 export type IntegerRanges = ReadonlyMap<IrExpr, IntegerRange | null>;
+/** Facts per expression, and per for loop the bindings its body writes only
+ * as bounded cursors (boundedIntegerLoopFacts): each holds an integer in its
+ * loop range on entry and at every write in the loop. */
+export interface IntegerRangeFacts {
+  ranges: IntegerRanges;
+  loopRanges: ReadonlyMap<IrStmt, ReadonlyMap<string, IntegerRange>>;
+}
 const SIGNED: IntegerRange = { min: -2147483648, max: 2147483647 };
 const UNSIGNED: IntegerRange = { min: 0, max: 4294967295 };
 /** Int32 and uint32 at once: the bound under which `%` (modeled only for
@@ -227,8 +234,17 @@ export interface IntegerSlotFacts {
  * range those writes and its entry value span across the region.
  * Suspensions and captured bindings deliberately remain outside the proof. */
 export function analyzeIntegerRanges(fn: IrFunction, slots: IntegerSlotFacts = {}): IntegerRanges {
+  return analyzeIntegerRangeFacts(fn, slots).ranges;
+}
+
+/** analyzeIntegerRanges with the loop ranges of the function's for loops. */
+export function analyzeIntegerRangeFacts(
+  fn: IrFunction,
+  slots: IntegerSlotFacts = {},
+): IntegerRangeFacts {
   const ranges = new Map<IrExpr, IntegerRange | null>();
-  if (fn.async || fn.generator) return ranges;
+  const loopRanges = new Map<IrStmt, Map<string, IntegerRange>>();
+  if (fn.async || fn.generator) return { ranges, loopRanges };
   const captures = new Set(
     [...(fn.captures ?? []), ...(fn.classCaptures ?? [])].map((c) => c.localId),
   );
@@ -436,6 +452,26 @@ export function analyzeIntegerRanges(fn: IrFunction, slots: IntegerSlotFacts = {
     return result;
   }
 
+  // Loop ranges of the bindings the enclosing for loops bound
+  // (boundedIntegerLoopFacts) while their bodies are analyzed.
+  let counterRanges: ReadonlyMap<string, IntegerRange> = new Map();
+  /** The value a write stores in a binding a for loop bounds. Every value
+   * the binding holds in the loop lies in its loop range, so the written
+   * value takes that range even when its operands' ranges add past it
+   * (`changes = changes + 1` with `changes` at the loop's limit). */
+  function boundedWrite(id: string, value: IrExpr, facts: Facts): IntegerRange | null {
+    const bound = counterRanges.get(id);
+    const before = ranges.get(value);
+    const computed = expr(value, facts);
+    if (!bound) return computed;
+    const range = computed
+      ? { min: Math.max(computed.min, bound.min), max: Math.min(computed.max, bound.max) }
+      : bound;
+    if (range.min > range.max) return computed;
+    ranges.set(value, before === undefined ? range : before ? union(before, range) : null);
+    return range;
+  }
+
   function remember(e: IrExpr, range: IntegerRange | null): IntegerRange | null {
     // Shared IR objects have to satisfy the proof at every occurrence.
     const previous = ranges.get(e);
@@ -565,12 +601,17 @@ export function analyzeIntegerRanges(fn: IrFunction, slots: IntegerSlotFacts = {
         range = facts.get(e.localId) ?? boxedRange(e.localId);
         break;
       case "assignExpr":
-        range = expr(e.value, facts);
+        range = boundedWrite(e.localId, e.value, facts);
         set(facts, e.localId, range);
         break;
       case "incDec": {
         const before = facts.get(e.localId) ?? null;
-        const after = before ? integerArithmeticRange(e.op, before, { min: 1, max: 1 }) : null;
+        const bound = counterRanges.get(e.localId);
+        const sum = before ? integerArithmeticRange(e.op, before, { min: 1, max: 1 }) : null;
+        const after =
+          bound && sum
+            ? { min: Math.max(sum.min, bound.min), max: Math.min(sum.max, bound.max) }
+            : sum;
         set(facts, e.localId, after);
         range = e.prefix ? after : before;
         break;
@@ -756,11 +797,11 @@ export function analyzeIntegerRanges(fn: IrFunction, slots: IntegerSlotFacts = {
     for (const s of stmts) {
       switch (s.kind) {
         case "varDecl":
-        case "assign": {
-          const value = s.kind === "varDecl" ? s.init : s.value;
-          set(facts, s.localId, value ? expr(value, facts) : null);
+          set(facts, s.localId, s.init ? expr(s.init, facts) : null);
+          break;
+        case "assign":
+          set(facts, s.localId, boundedWrite(s.localId, s.value, facts));
           break;
-        }
         case "exprStmt":
           expr(s.expr, facts);
           break;
@@ -831,7 +872,31 @@ export function analyzeIntegerRanges(fn: IrFunction, slots: IntegerSlotFacts = {
           if (s.cond) expr(s.cond, loop);
           const inside = new Map(loop);
           if (s.cond) refine(s.cond, true, inside);
-          body(s.body, inside);
+          // Only the body's writes are the ones the bound counted.
+          const outer = counterRanges;
+          const headWrites = s.cond ? writes(s.cond) : new Set<string>();
+          if (s.update) for (const id of writes(s.update)) headWrites.add(id);
+          const cursors = new Map<string, IntegerRange>();
+          for (const [id, range] of bounded)
+            if (id !== counter?.id && !headWrites.has(id)) cursors.set(id, range);
+          // A loop analyzed again (inside another loop) keeps the bindings
+          // every analysis bounds, with the union of their ranges.
+          const previous = loopRanges.get(s);
+          if (!previous) loopRanges.set(s, cursors);
+          else
+            for (const [id, range] of previous) {
+              const other = cursors.get(id);
+              if (other) previous.set(id, union(range, other));
+              else previous.delete(id);
+            }
+          const active = new Map(outer);
+          for (const [id, range] of cursors) active.set(id, range);
+          counterRanges = active;
+          try {
+            body(s.body, inside);
+          } finally {
+            counterRanges = outer;
+          }
           // Continue can bypass any body assignment. The update therefore
           // starts from header invariants rather than the body's exit facts,
           // plus what the condition proved about bindings the body never
@@ -919,5 +984,5 @@ export function analyzeIntegerRanges(fn: IrFunction, slots: IntegerSlotFacts = {
   const entry: Facts = new Map();
   if (slots.params) for (const [id, range] of slots.params) set(entry, id, range);
   body(fn.body, entry);
-  return ranges;
+  return { ranges, loopRanges };
 }
diff --git a/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5686-loop-cursor-resets-and-copies.ts.json b/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5686-loop-cursor-resets-and-copies.ts.json
new file mode 100644
index 000000000..8aef0174d
--- /dev/null
+++ b/packages/compiler/test/ts7/baselines/order-parity/tests/corpus/5686-loop-cursor-resets-and-copies.ts.json
@@ -0,0 +1,6 @@
+{
+ "order": [
+  "<repo>/tests/corpus/5686-loop-cursor-resets-and-copies.ts"
+ ],
+ "diags": []
+}
diff --git a/tests/corpus/5686-loop-cursor-resets-and-copies.ts b/tests/corpus/5686-loop-cursor-resets-and-copies.ts
new file mode 100644
index 000000000..ae5ff3589
--- /dev/null
+++ b/tests/corpus/5686-loop-cursor-resets-and-copies.ts
@@ -0,0 +1,157 @@
+// Loop cursors that a for loop resets, copies and counts (`run = 0`,
+// `longest = run`, `lines++`): typed-array and array scans, exits through
+// break, return and a caught exception, a labeled continue, loops that run
+// zero times, cursors near 2^53, decrements and reads inside the loop.
+
+function longestRun(values: Int32Array): number {
+  let longest = 0;
+  let run = 0;
+  let changes = 0;
+  let previous = 0;
+  for (let i = 0; i < values.length; i++) {
+    const v = values[i]!;
+    if (v >= 0) {
+      run++;
+      if (run > longest) longest = run;
+    } else run = 0;
+    if (v < 0 !== previous < 0) changes++;
+    previous = v;
+  }
+  return longest * 1000 + changes;
+}
+
+function countBytes(bytes: Uint8Array): string {
+  let lines = 0;
+  let words = 0;
+  let digits = 0;
+  let inWord = false;
+  for (let i = 0; i < bytes.length; i++) {
+    const b = bytes[i]!;
+    if (b === 10) lines++;
+    if (b === 10 || b === 32) inWord = false;
+    else if (!inWord) {
+      inWord = true;
+      words++;
+    }
+    if (b >= 48 && b <= 57) digits++;
+  }
+  return `${lines} ${words} ${digits}`;
+}
+
+function firstLongRun(values: number[], limit: number): number {
+  let run = 0;
+  let at = -1;
+  for (let i = 0; i < values.length; i++) {
+    if (values[i]! > 0) run++;
+    else run = 0;
+    if (run === limit) {
+      at = i;
+      break;
+    }
+  }
+  return at * 100 + run;
+}
+
+function returnInside(values: number[]): number {
+  let count = 0;
+  for (let i = 0; i < values.length; i++) {
+    if (values[i] === 0) return count;
+    count++;
+  }
+  return -count;
+}
+
+function throwInside(values: number[]): number {
+  let count = 0;
+  for (let i = 0; i < values.length; i++) {
+    if (values[i]! < 0) throw new Error(`negative after ${count}`);
+    count++;
+  }
+  return count;
+}
+
+function caughtInside(values: number[]): string {
+  let count = 0;
+  try {
+    for (let i = 0; i < values.length; i++) {
+      if (values[i]! < 0) throw new Error("negative");
+      count++;
+    }
+  } catch (error) {
+    return `caught after ${count}`;
+  }
+  return `done ${count}`;
+}
+
+function labeled(rows: number[][]): number {
+  let total = 0;
+  let skipped = 0;
+  outer: for (let r = 0; r < rows.length; r++) {
+    let run = 0;
+    for (let i = 0; i < rows[r]!.length; i++) {
+      if (rows[r]![i]! < 0) {
+        skipped++;
+        continue outer;
+      }
+      run++;
+    }
+    total += run;
+  }
+  return total * 100 + skipped;
+}
+
+function nearLimit(): number[] {
+  let up = 9007199254740981;
+  let down = -9007199254740981;
+  let copy = 0;
+  for (let i = 0; i < 10; i++) {
+    up++;
+    down--;
+    copy = up;
+  }
+  let untouched = 9007199254740991;
+  for (let i = 0; i < 0; i++) untouched = untouched - 1;
+  return [up, down, copy, up - 9007199254740981, untouched];
+}
+
+function readsInside(n: number): number {
+  let count = 0;
+  let sum = 0;
+  for (let i = 0; i < n; i++) {
+    if (i % 3 === 0) count++;
+    sum += count * 2 + i;
+  }
+  return sum;
+}
+
+function countDown(values: Float64Array): number {
+  let remaining = values.length;
+  let below = 0;
+  for (let i = 0; i < values.length; i++) {
+    remaining = remaining - 1;
+    if (values[i]! < 0.5) below = below + 2;
+    else below = below - 1;
+  }
+  return remaining * 1000 + below;
+}
+
+const ints = new Int32Array(64);
+for (let i = 0; i < ints.length; i++) ints[i] = ((i * 37) % 11) - 3;
+console.log("longestRun", longestRun(ints), longestRun(new Int32Array(0)));
+const text = new TextEncoder().encode("const value = 42;\nreturn x_y 7 plus 8\n\nend");
+console.log("countBytes", countBytes(text), countBytes(new Uint8Array(0)));
+console.log("firstLongRun", firstLongRun([1, 2, 0, 3, 4, 5, 6, 0], 3), firstLongRun([1, 0, 1], 5));
+console.log("returnInside", returnInside([4, 5, 0, 6]), returnInside([1, 2, 3]));
+try {
+  throwInside([1, 2, -1, 4]);
+} catch (error) {
+  console.log("throwInside", (error as Error).message);
+}
+console.log("throwInside", throwInside([]));
+console.log("caughtInside", caughtInside([3, 2, -1]), caughtInside([1, 2]));
+console.log("labeled", labeled([[1, 2, 3], [4, -1, 5], [], [6, 7]]));
+console.log("nearLimit", nearLimit().join(","));
+console.log("readsInside", readsInside(10), readsInside(0));
+const samples = new Float64Array(20);
+for (let i = 0; i < samples.length; i++) samples[i] = (i * 0.37) % 1;
+console.log("countDown", countDown(samples), countDown(new Float64Array(0)));
diff --git a/tests/harness/corpus-costs/5686-loop-cursor-resets-and-copies.ts.json b/tests/harness/corpus-costs/5686-loop-cursor-resets-and-copies.ts.json
new file mode 100644
index 000000000..738b5b70e
--- /dev/null
+++ b/tests/harness/corpus-costs/5686-loop-cursor-resets-and-copies.ts.json
@@ -0,0 +1 @@
+{ "plain": 2650, "san": 2200 }