i * i > n, xi * y[j], (n + 4) / 5)Open and answer this issue on GitHub.
compiler, decision · opened 2026-10-03 · updated 2026-10-24 · 1 comment
This is about 12 of the overflow sites in ADR-276 §3, plus bignum’s inner product in benches/solver-kernels.nika. The walk reads linear terms only, and Fourier-Motzkin decides only linear arithmetic.
Example: in bignum, xi * (y[j] as u64) + (out[i + j] as u64) + carry cannot overflow a u64, because every factor is below 2^32. That is interval arithmetic over the operands’ types, not linear facts.
bounds.rs already has Range::mul for interval evaluation. It would need to be confirmed by a certificate, or be accepted as its own proof rule./ and % by a positive constant are linear bounds that can be expressed with a fresh variable (q*k <= x < (q+1)*k).just do it, we need it.