4 ms·
I imagine a basic proof amounts to: the result (base) is monotonically increasing (even in intermediate calculations) and the length of the slice fits in a usiz
by Gankro 10y ago
I imagine a basic proof amounts to: the result (base) is monotonically increasing (even in intermediate calculations) and the length of the slice fits in a usize, so if the correct result is always produced with infinite precision there's no concern for overflow (correct results are bounded by the len).
Similarly `s.len() >> 1` is a strictly decreasing value by division, so no concern for underflow.
- millstone 10y agoI like that. That's a powerful argument! For it to work, it requires that every number be returned as part of the result, and that all calculations are monotonically increasing, as you said. Most algorithms won't have those invariants, but perhaps you can tweak them until they do. Once you have, you can extend an infinite-width proof to a finite-width proof.