Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 27 additions & 3 deletions benchmarks/repsel_census/baseline.json
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@
"ptr-shape": 0,
"ptr-shape-consumed": 0,
"ptr-numarray": 0,
"canonical-i32": 2,
"canonical-i32": 3,
"canonical-u32": 1,
"canonical-str": 1,
"int-valued-ta": 0,
Expand Down Expand Up @@ -161,6 +161,30 @@
"unconsumed_mechanisms": {},
"consumption_sites": {}
},
{
"name": "fixture_loop_bounded_i32",
"role": "liveness",
"source": "benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts",
"floors": {
"ptr-shape": 0,
"ptr-shape-consumed": 0,
"ptr-numarray": 0,
"canonical-i32": 3,
"canonical-u32": 0,
"canonical-str": 0,
"int-valued-ta": 0,
"spec-abi-entry": 1,
"spec-abi-taptr-slot": 0
},
"candidates": {
"ptr-shape": 0,
"ptr-numarray": 0,
"canonical-slot": 5,
"int-valued-ta": 0,
"spec-abi": 4
},
"unconsumed_mechanisms": {}
},
{
"name": "batch",
"role": "corpus",
Expand Down Expand Up @@ -620,13 +644,13 @@
"candidates": {
"ptr-shape": 0,
"ptr-numarray": 1,
"canonical-slot": 5,
"canonical-slot": 4,
"int-valued-ta": 0,
"spec-abi": 0
},
"unconsumed_mechanisms": {},
"consumption_sites": {}
}
],
"generated_at": "2026-07-31T05:15:37.361861Z"
"generated_at": "2026-07-31T05:53:44.935156Z"
}
79 changes: 79 additions & 0 deletions benchmarks/repsel_census/fixtures/fixture_loop_bounded_i32.ts
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
// Liveness fixture for the monotone loop-induction i32 range proof (#7110).
//
// `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
// `| 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 two locals it must NOT promote are here on purpose: an unadmitted
// counter and an unbounded accumulator keep the fixture from being satisfied by
// any rule that simply says yes to proven-integer locals.
//
// Requirements shared with the other canonical-slot fixtures: plain synchronous
// function bodies (async/generator bodies are context-excluded), and no closure
// capture of the candidate locals.

const ROUNDS = 4096;

// PROMOTES. A bare `for` counter with a module-level `const` bound: not
// index-used, and `i++` keeps it out of `strictly_i32_bounded_locals`.
// Interval [0, 4095].
function countUp(): number {
let last = 0.5;
for (let i = 0; i < ROUNDS; i++) {
last = last + 0.25;
}
return last;
}

// PROMOTES. A `while` whose guard is a CONJUNCTION and whose step is a
// `LocalSet` Add rather than `++` — the 15_mandelbrot `iter` shape.
// Interval [0, 100].
function iterate(seed: number): number {
let iter = 0;
let x = seed;
while (x < 1000.0 && iter < 100) {
x = x * 1.5;
iter = iter + 1;
}
return iter;
}

// DOES NOT PROMOTE. `i <= 2147483647` lets the counter reach 2147483648, one
// past INT32_MAX. Node prints 2147483648 here; an i32 slot would print
// -2147483648. `break` keeps the fixture fast without weakening the proof
// obligation, which is a property of the loop text, not of the trip count.
function overshoot(): number {
let i = 2147483640;
for (; i <= 2147483647; i++) {
if (i > 2147483642) {
break;
}
}
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 {
let sum = 0;
for (let i = 0; i < ROUNDS; i++) {
sum = sum + 1000000;
}
return sum;
}

console.log(
"loopBounded:" +
countUp() +
":" +
iterate(1.0) +
":" +
overshoot() +
":" +
accumulate(),
);
112 changes: 112 additions & 0 deletions changelog.d/7122-canonical-i32-loop-induction.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,112 @@
A bare loop counter never took canonical unboxed storage. Not in a function
body, not anywhere: `canonical_safe_local` in `stmt/let_stmt.rs` required the
local to be used as an **array index** or to sit in
`strictly_i32_bounded_locals`, and a counter is neither — `i++` disqualifies a
local from the latter outright (#6072), and nothing about `i` in

```ts
for (let i = 0; i < 1000000; i++) { sum = sum + 1; }
```

involves an array. Add one `a[i]` read and it promoted immediately. The
promotion turned on the presence of an array, not on any property of `i`.

## The proof that admits it

`collectors/loop_bounded_i32.rs` proves a **closed interval** the local can
never leave, from the guard that dominates every write to it:

* one declaration, initialiser an i32-range integer literal `I`;
* every write anywhere in the function is a step (`v++`, `v = v + k`, and the
decrement mirror) with `k` a non-negative integer constant;
* every step sits directly in the body or update of a loop whose condition has
a top-level `&&`-spine conjunct `v < B` / `v <= B` / `v > B` / `v >= B`, `B` an
i32-range constant — a literal, a `const` local, or a module-level `const`
from `compile_time_constants`;
* no intervening loop and no intervening closure between the step and that
guard, so each step site runs at most once per iteration;
* the step direction agrees with the guard.

With `S` the sum of the steps at that level, an increment counter is confined to
`[I, B - 1 + S]` (`[I, B + S]` for `<=`), a decrement counter to the mirror, and
the local is admitted only when **both endpoints fit i32**.

This is a range argument, not a compatibility bound. The existing
`integer_locals ∩ index_used_locals` term is sound only because the pre-phase
shadow model already read the i32 slot for that exact set (the range-soundness
audit in `expr/slot_rep.rs` says so); this one adds no overflow surface, because
there is no reachable state in which the value leaves i32. The same argument is
already trusted one layer down — `stmt/loops.rs` allocates a *parallel* i32
shadow for a constant-bounded counter on exactly this reasoning. What is new is
lifting it to a Let-site fact, so the counter's i32 slot becomes its **only**
storage instead of a shadow kept in sync with a boxed double.

Consumed only by the canonical-i32 gate, never by the parallel-shadow
`needs_i32_slot` gate, so `PERRY_CANONICAL_I32_LOCALS=0` still reproduces the
pre-phase model bit-for-bit — the containment `int_valued_ta_locals` already
uses. No new env knob.

## The half that stays denied, and why

A bare **accumulator** is not admitted and must not be.
`benchmarks/suite/13_factorial.ts` — one of the three workloads #7110 names —
computes `sum = sum + (i % 1000)` over 1e8 iterations. That reaches
**49,950,000,000**, twenty-three times `INT32_MAX`. Node prints it exactly; an
i32 slot would print a wrapped negative. "Every write is `sum = sum + <integer>`"
is not an i32 proof, and a rule that treated it as one would be a silent wrong
answer rather than a missed optimization. Bounding an accumulator needs the
loop's trip count multiplied by a magnitude bound on the step expression —
strictly more analysis, and filed as #7123.

The `not_index_used_or_bounded` denial reason now says this, so the report
distinguishes "not implemented yet" from "must not be promoted".

## Evidence

`--opt-report=json --no-link`, macOS arm64, oracle Node 26.5.1.

```ts
function run(): number { let sum = 0; for (let i = 0; i < 1000000; i++) { sum = sum + 1; } return sum; }
```

| | `i` | `sum` |
|---|---|---|
| before | denied `not_index_used_or_bounded` | denied `not_index_used_or_bounded` |
| after | **selected `I32`** | denied `not_index_used_or_bounded` |

Emitted IR for that function, before → after: the counter's `alloca double`
becomes `alloca i32`, the condition's `load double` becomes `load i32`, and the
update's `fadd double %r11, 1.0` becomes `add i32 %r12, 1`. Selecting
canonical-i32 *moves the storage*, so unlike `Ptr<Shape>` there is no slot left
for an unconsumed selection to fall back to: every read and write of the local
is forced through the i32 slot or it does not compile.

**Census** (`compiler_output_regression.py census`): corpus-wide `canonical-i32`
**13 → 17**. No floor dropped; `fixture_canonical_slots` rises 2 → 3 (its
`u32Mixer` counter now promotes). The new liveness fixture
`fixture_loop_bounded_i32` has no bitwise mixing, no `| 0` and no array
indexing, so its three `canonical-i32` promotions can only come from this rule;
its `LIVENESS_FLOORS` minimum is pinned at 3 in code, where `--update` cannot
reach it.

**Wider sweep** (201 parsed files: 200 `test_gap_*.ts` + the app-pattern
kernels), canonical-slot verdicts before → after:

| | before | after |
|---|---|---|
| selected `I32` | 24 | **28** |
| denied `not_index_used_or_bounded` | 77 | **51** |
| denied `module_init_context` | 127 | **145** |
| denied `closure_referenced` / `declared_bigint` | 7 / 5 | 7 / 5 |

The 26 locals that leave `not_index_used_or_bounded` split 4 promoted / 18 now
blocked *only* by the module-init context gate (#7109) / 4 that were being
reported twice and are now one selection. So the rule proves **22** more locals
than it promotes today; the other 18 land the moment #7109 is fixed.

**gc-ratchet** (`--repeats 7`, `shared_ci`): OK. The gated retention and
evacuation counters are **bit-identical** between `PERRY_CANONICAL_I32_LOCALS`
on and off — the representation change moves nothing the collector counts. The
ungated `wall_ms` column moves on 7 of 8 probes (+1.2% to +8.2% slower with the
canonical model off), which is what proves the two arms were different binaries
rather than one stale archive measured twice.
21 changes: 21 additions & 0 deletions crates/perry-codegen/src/collectors/hir_facts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,14 @@ pub(crate) struct RepresentationFacts {
/// strictly-i32-bounded — the box `slot.ts` mix shape (`let l = P[0]` from
/// an Int32Array PARAM, bitwise-only updates and observations).
pub int_valued_ta_locals: HashSet<u32>,
/// Locals proven to stay inside i32 range by the monotone loop-induction
/// argument (#7110): single literal initialiser, every write a step whose
/// direction agrees with a constant-bounded guard on the immediately
/// enclosing loop, both interval endpoints inside i32. Like
/// `int_valued_ta_locals` this is a canonical-storage-only admission term
/// — it never widens the parallel-shadow `needs_i32_slot` gate. See
/// `collectors/loop_bounded_i32.rs`.
pub loop_bounded_i32_locals: HashSet<u32>,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
Expand Down Expand Up @@ -155,6 +163,10 @@ impl TypeFacts {
&self.representation.int_valued_ta_locals
}

pub(crate) fn loop_bounded_i32_locals(&self) -> &HashSet<u32> {
&self.representation.loop_bounded_i32_locals
}

pub(crate) fn not_bigint_locals(&self) -> &HashSet<u32> {
&self.representation.not_bigint_locals
}
Expand Down Expand Up @@ -414,6 +426,14 @@ pub(crate) fn collect_type_facts(
}
}
let unsigned_i32_locals = super::i32_locals::collect_unsigned_i32_locals(stmts);
// #7110: the monotone loop-induction i32 range proof. Skipped entirely when
// canonical selection is off, so the `PERRY_CANONICAL_I32_LOCALS=0`
// bisection arm reproduces the pre-phase model with no analysis run at all.
let loop_bounded_i32_locals = if crate::expr::canonical_i32_locals_enabled() {
super::loop_bounded_i32::collect_loop_bounded_i32_locals(stmts, compile_time_constants)
} else {
HashSet::new()
};
let not_bigint_locals =
super::not_bigint_locals::collect_not_bigint_locals(stmts, params, binding_types);
let (array_facts, effect_facts, materialization_hazards) =
Expand Down Expand Up @@ -504,6 +524,7 @@ pub(crate) fn collect_type_facts(
unsigned_i32_locals,
not_bigint_locals,
int_valued_ta_locals,
loop_bounded_i32_locals,
},
arrays: array_facts,
effect: effect_facts,
Expand Down
Loading
Loading