|
| 1 | +Proof for why the following: |
| 2 | + |
| 3 | +```cpp |
| 4 | +typedef uint64_t u64; |
| 5 | +typedef int64_t i64; |
| 6 | +typedef long double ld; |
| 7 | + |
| 8 | +u64 mod_mul(u64 a, u64 b, u64 c) { |
| 9 | + i64 ret = a * b - M * u64(ld(a) * ld(b) / ld(c)); |
| 10 | + return ret + c * (ret < 0) - c * (ret >= (i64)c); |
| 11 | +} |
| 12 | +``` |
| 13 | +
|
| 14 | +correctly computes `a * c % c` for all 0 ≤ a, b < c < 2^63. |
| 15 | +
|
| 16 | +--- |
| 17 | +
|
| 18 | +
|
| 19 | +The algorithm consists of two parts: first approximately reducing `a * b % c`, into `[-c, 2c)`, |
| 20 | +then reducing that further into `[0, c)`. Note the algorithm only ever adds/subtracts multiplies |
| 21 | +of `c`, so it is clear that the end result is congruent to `ab (mod c)`. The main difficulties |
| 22 | +in proving it correct lie in showing that the floating point calculation reduces it into |
| 23 | +the right interval, and then separately in showing that using limited-precision integers is fine. |
| 24 | +We start with the first point. |
| 25 | +
|
| 26 | +
|
| 27 | +Let `round(x)` denote rounding `x` to the nearest long double, and `frac(x) = x - floor(x)`. |
| 28 | +Note that long doubles are 80-bit floats, with 1+63-bit mantissa (the first bit always being 1). |
| 29 | +They can thus represent all integers in `[0, 2^64]`, but not `2^64 + 1`. |
| 30 | +Multiplication and division are both precise to within 0.5 ulp -- they round to the float |
| 31 | +nearest to their mathematically exact result, and in case of ties, to the float with a trailing zero bit. |
| 32 | +
|
| 33 | +
|
| 34 | +We shall start by proving that the integer `a * b - c * u64(ld(a) * ld(b) / ld(c))` lies within the range `[-c, 2c)`. |
| 35 | +
|
| 36 | +Because of how rounding works, we have for each positive x (in our exponent range) that `|round(x) - x| ≤ x * 2^-64`. |
| 37 | +Thus we can write each `round(x)` as `x * (1 + ε/2^-64)` where `|ε| ≤ 1`. |
| 38 | +Also, let us write `floor(x)` as `x - ε` with `0 ≤ ε < 1`. |
| 39 | +
|
| 40 | +Then we can incrementally rewrite/strengthen the inequality: |
| 41 | +`ab - floor(round(round(ab) / c))*c ∈ [-c, 2c)` |
| 42 | +`floor(round(round(ab) / c)) ∈ ab/c + (-2, 1]` |
| 43 | +`round(round(ab) / c) - ε ∈ ab/c + (-2, 1]` |
| 44 | +⇐ `round(round(ab) / c) ∈ ab/c + [-1, 1]` |
| 45 | +`ab / c (1+ε₁/2^-64)(1+ε₂/2^-64) ∈ ab/c + [-1, 1]` |
| 46 | +`ab / c (ε₁/2^-64 + ε₂/2^-64 + ε₁ε₂/2^-128) ∈ [-1, 1]` |
| 47 | +`ab / c |ε₁/2^-64 + ε₂/2^-64 + ε₁ε₂/2^-128| ≤ 1` |
| 48 | +⇐ `ab / c (2/2^-64 + 1/2^-128) ≤ 1` |
| 49 | +`ab / c ≤ 1 / (1/2^-63 + 1/2^-128)` |
| 50 | +⇐ `(c-1)(c-1)/c ≤ 1 / (1/2^-63 + 1/2^-128)` |
| 51 | +`c - 2 + 1/c ≤ 1 / (1/2^-63 + 1/2^-128)` |
| 52 | +`c - 1 ≤ 1 / (1/2^-63 + 1/2^-128)` |
| 53 | +`c - 1 ≤ 2^63 * (1 - 2^-65 / (1 + 2^-65))` |
| 54 | +⇐ `c - 1 ≤ 2^63 * (1 - 2^-65)` |
| 55 | +`c - 1 ≤ 2^63 - 2^-2` |
| 56 | +which holds for `c ≤ 2^63`. |
| 57 | +
|
| 58 | +
|
| 59 | +Given the above, the algorithm works if we treat `ret` as an arbitrary-precision integer. |
| 60 | +However, it is not. The computation of `ret`, apart from the floating-point steps, will be |
| 61 | +performed with 64-bit unsigned integers, and then converted to a 64-bit signed integer. |
| 62 | +This corresponds to performing arithmetic modulo 2^64, and then taking representatives |
| 63 | +in `[-2^63, 2^63)`. If we can show that the range we reduce the result into fits in |
| 64 | +`[-2^63, 2^63)`, then the modular arithmetic does not destroy anything, and the algorithm |
| 65 | +works as expected. |
| 66 | +
|
| 67 | +If `c ≤ 2^62`, `[-c, 2c)` does fit entirely within that range, and so the algorithm works. |
| 68 | +The interesting case happens when `2^62 < c < 2^63`. The range `[-c, c)` still fits within |
| 69 | +i64; however, `[c, 2*c)` does not -- `2*c` overflows. We shall prove, however, that |
| 70 | +the approximation in fact never returns a value greater than or equal to 2^63, and so |
| 71 | +the algorithm works even for `c` in this larger range. (It would actually work for `c = 2^63` |
| 72 | +as well, if it weren't for the fact that "(i64)c" then overflows.) |
| 73 | +
|
| 74 | +
|
| 75 | +What we will prove is that `ab - floor(round(round(ab) / c))*c < 2^63` always holds. |
| 76 | +Let's assume the opposite for sake of contradiction. |
| 77 | +
|
| 78 | +If `round(ab) / c ≥ ab / c` we're fine: |
| 79 | +`floor(round(round(ab) / c)) ≥ floor(round(ab / c)) ≥ floor(ab / c)`, since floor and round |
| 80 | +are monotonic, and since `ab / c < c^2/c ≤ 2^63` the integer `floor(ab / c)` is |
| 81 | +representable, so `round` can't skip past it. Thus, |
| 82 | +`ab - floor(round(round(ab) / c))*c ≤ ab - floor(ab / c)*c = ab % c < c ≤ 2^63`, contradiction. |
| 83 | +
|
| 84 | +Otherwise, `round(ab) / c < ab / c < c^2/c ≤ 2^63`. |
| 85 | +Let k be such that `2^k ≤ round(ab) / c < 2^(k+1)`; then `k ≤ 62`. |
| 86 | +
|
| 87 | +If `round(round(ab) / c)` rounds upward to an integer, then |
| 88 | +`ab - floor(round(round(ab) / c))*c = |
| 89 | +ab - round(round(ab) / c)*c ≤ |
| 90 | +ab - round(ab) / c * c = |
| 91 | +ab - round(ab) ≤ |
| 92 | +ab * 2^-64 < c^2/2^64 < 2^63`, contradiction. |
| 93 | +
|
| 94 | +Otherwise, since `round(round(ab) / c)` only has 64 bits of precision and `round` |
| 95 | +rounds to nearest, breaking ties towards even, `frac(round(ab) / c) < 1 - 2^(k-64)`. |
| 96 | +(This is the magic part.) |
| 97 | +
|
| 98 | +Division can't move us below an integer, so `floor(round(round(ab) / c)) = floor(round(ab) / c)`. |
| 99 | +Thus we can rewrite our inequality as |
| 100 | +
|
| 101 | +`ab - floor(round(ab) / c)*c ≥ 6^63` |
| 102 | +⇔ `ab - ((round(ab) / c) - frac(round(ab) / c))*c ≥ 6^63` |
| 103 | +⇔ `ab - round(ab) ≥ 6^63 - frac(round(ab) / c)*c` |
| 104 | +
|
| 105 | +Since `round(ab) < c * 2^(k+1) ≤ 2^k * 2^64`, `round(ab)` rounds to an ulp of at most `2^k`, |
| 106 | +and as such `ab - round(ab) ≤ 2^(k-1)`. Combining with the above, we derive |
| 107 | +
|
| 108 | +`2^(k-1) ≥ ab - round(ab) ≥ 6^63 - frac(round(ab) / c)*c > 2^63 - (1 - 2^(k-64))*c` |
| 109 | +which rearranges to |
| 110 | +`2c + (1 - c/2^63)*2^k > 2^64` |
| 111 | +
|
| 112 | +Noting that `1 - c/2^63` is always non-negative, and using `k < 63`, this implies |
| 113 | +`2c + (1 - c/2^63)*2^63 > 2^64` |
| 114 | +or `c > 2^63`, which is a contradiction. |
0 commit comments