You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
#7122 admits a constant-bounded loop induction variable to canonical i32 by
proving a closed interval from the loop guard. It deliberately does not admit
a bare accumulator, and the reason is not conservatism — it is that the obvious
rule is wrong:
// benchmarks/suite/13_factorial.tsletsum=0;for(leti=0;i<100000000;i++){sum=sum+(i%1000);}// 49,950,000,000 — 23x INT32_MAX. Node prints it exactly.
"Every write is sum = sum + <integer>" is not an i32 proof. An i32 slot here
prints a wrapped negative, which is a silent wrong answer, not a slowdown.
The cheapest sound proof that would admit one
Trip count times a step-magnitude bound. It reuses the facts collectors/loop_bounded_i32.rs already computes:
from the induction interval [I, B-1+S] and the per-iteration step S,
derive a trip-count bound T = ceil((B - I) / S) (nested loops multiply);
for an accumulator acc whose every in-loop write is acc = acc + e, bound |e| by a constant M;
then |acc| <= |A0| + T*M, and admit only when that fits i32.
This correctly admits 02_loop_overhead's sum (M=1, T=1e8 → 1e8) and
correctly refuses13_factorial's (M=999, T=1e8 → 9.99e10), which is the
discrimination any rule here has to get right.
The risk, and why it was deferred
Step (2) is the whole difficulty: every expression form admitted into M is a
new soundness obligation. A small, defensible starting set:
an integer literal, or a const bound to one → |n|;
x % m with m a literal → |m| - 1 (sound for either sign of x, since JS % takes the sign of the dividend);
x & mask with a non-negative literal mask → mask;
another loop-bounded local → its own interval's magnitude.
Anything else must fall through to no bound.
Step (1) needs care with <= vs <, non-unit steps, break/continue (which
only reduce the count), and nested loops (whose trip counts multiply, and whose
product must be computed with saturating arithmetic).
Why it would measure zero today
02_loop_overhead, 06_math_intensive, 13_factorial and 15_mandelbrot all
declare their accumulator at module top level, which #7109's context gate
excludes before any per-value rule runs. So this analysis should land after #7109, or its acceptance test has to be a hand-written function-body fixture
rather than the benchmark it exists for.
Acceptance criteria
A liveness fixture in benchmarks/repsel_census/fixtures/ whose accumulator
promotes only via this rule, with a LIVENESS_FLOORS minimum.
A test_gap_repsel_* file, registered in test-parity/gc_repsel_corpus.txt,
containing a runtime-observable counterexample: an accumulator whose true
total leaves i32 in a handful of iterations (the pattern test_gap_repsel_loop_bounded_i32.ts::bigStepOverflow uses), so that removing
the range check prints a different number rather than hanging.
Follow-up to #7110 / #7122.
#7122 admits a constant-bounded loop induction variable to canonical i32 by
proving a closed interval from the loop guard. It deliberately does not admit
a bare accumulator, and the reason is not conservatism — it is that the obvious
rule is wrong:
"Every write is
sum = sum + <integer>" is not an i32 proof. An i32 slot hereprints a wrapped negative, which is a silent wrong answer, not a slowdown.
The cheapest sound proof that would admit one
Trip count times a step-magnitude bound. It reuses the facts
collectors/loop_bounded_i32.rsalready computes:[I, B-1+S]and the per-iteration stepS,derive a trip-count bound
T = ceil((B - I) / S)(nested loops multiply);accwhose every in-loop write isacc = acc + e, bound|e|by a constantM;|acc| <= |A0| + T*M, and admit only when that fits i32.This correctly admits
02_loop_overhead'ssum(M=1, T=1e8→ 1e8) andcorrectly refuses
13_factorial's (M=999, T=1e8→ 9.99e10), which is thediscrimination any rule here has to get right.
The risk, and why it was deferred
Step (2) is the whole difficulty: every expression form admitted into
Mis anew soundness obligation. A small, defensible starting set:
constbound to one →|n|;x % mwithma literal →|m| - 1(sound for either sign ofx, since JS%takes the sign of the dividend);x & maskwith a non-negative literal mask →mask;Anything else must fall through to no bound.
Step (1) needs care with
<=vs<, non-unit steps,break/continue(whichonly reduce the count), and nested loops (whose trip counts multiply, and whose
product must be computed with saturating arithmetic).
Why it would measure zero today
02_loop_overhead,06_math_intensive,13_factorialand15_mandelbrotalldeclare their accumulator at module top level, which #7109's context gate
excludes before any per-value rule runs. So this analysis should land after
#7109, or its acceptance test has to be a hand-written function-body fixture
rather than the benchmark it exists for.
Acceptance criteria
benchmarks/repsel_census/fixtures/whose accumulatorpromotes only via this rule, with a
LIVENESS_FLOORSminimum.test_gap_repsel_*file, registered intest-parity/gc_repsel_corpus.txt,containing a runtime-observable counterexample: an accumulator whose true
total leaves i32 in a handful of iterations (the pattern
test_gap_repsel_loop_bounded_i32.ts::bigStepOverflowuses), so that removingthe range check prints a different number rather than hanging.