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
{{ message }}
Repository navigation
repsel: bound a loop accumulator by trip count x step magnitude, so a bare accumulator can take canonical i32 #7123
#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.
Activity
docs: point the accumulator deferral at #7123
perf(repsel): admit constant-bounded loop induction variables to cano…
perf(codegen): vectorize bounded byte-sum reductions (bench_buffer_re…
fix(runtime): module-global Uint8Array receivers, with the view-cache…