Files
scriptc/tests
Malte Ubl 796fcbb9ce Start whole-program int32 slot facts at non-negative int32
The optimistic int32-slots fixpoint assumed exactly int32 for parameter,
result and captured-box candidates. That is too weak for remainders:
with x and n only known to be int32, `(x * 31 + n) % m` may have a
negative dividend (and a -0 result), so a kernel called as
`v = step(v, n)` could not prove step's result, v stayed a double, and
the parameters fell back to doubles too.

Unpinned candidates now start one level lower, at non-negative int32. A
write that is an int32 but may be negative demotes the slot to int32 and
reanalyzes its readers (a parameter that seeds a box demotes the box as
well); any other write drops it as before. Slots only ever widen, so the
fixpoint still ends with every remaining assumption proven at every
write. Int32 contract pins keep their int32 facts. The call-site range
retry is unchanged for slots that fail both levels.

The direct-call kernel now passes i32 to step.i32 and keeps v an i32
slot (sandbox: 2563 ms -> 964 ms, node 1256 ms). Corpus 5323 pins the
non-negative facts and every widening path (negative arguments, results
and box writes, -0 remainders, count-down recursion) against Node.
2026-10-15 04:46:13 -07:00
..
2026-07-22 18:08:04 -05:00