Commit 1aea373
committed
Fix
The current implementation of `rem_euclid` for floating point numbers
violates the invariant, stated in the documentation, that:
```rust
a.rem_euclid(b) ~= a - b * a.div_euclid(b)
```
In a 2001 paper[^1], Daan Leijen (who notably later created the Koka
programming language) provides the correct formulation of this (and
of `div_euclid`) in "Algorithm E":
q_E = q_T - I
r_E = r_T + I * b
where
I = if r_T >= 0 then 0 else if b > 0 then 1 else -1
q_T = trunc(a / b)
r_T = a - b * q_T
a is a dividend, a real number
b is a divisor, a real number
In section 1.5 of the paper, he gives a proof of correctness.
Since we document[^2] that `a % b` is computed as...
```rust
a - b * (a / b).trunc()
```
...we can use `a % b` to compute `r_T`.
As we know the maxim, from Knuth, to...
> Beware of bugs in the above code; I have only proved it correct, not
> tried it.
...we have additionally subjected our encoding of this formulation to
fuzzing. It seems to hold up against the desired invariants.
This is of course a breaking change. But the current implementation
is broken, and libs-api has signaled openness to fixing it.
[^1]: "Division and Modulus for Computer Scientists",
Daan Leijen, 2001,
<https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf>
[^2]: https://doc.rust-lang.org/std/ops/trait.Rem.html#impl-Rem-for-f64{f16,f32,f64,f128}::rem_euclid
1 parent bd36e69 commit 1aea373
4 files changed
+16
-4
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
310 | 310 | | |
311 | 311 | | |
312 | 312 | | |
313 | | - | |
| 313 | + | |
| 314 | + | |
| 315 | + | |
| 316 | + | |
314 | 317 | | |
315 | 318 | | |
316 | 319 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
310 | 310 | | |
311 | 311 | | |
312 | 312 | | |
313 | | - | |
| 313 | + | |
| 314 | + | |
| 315 | + | |
| 316 | + | |
314 | 317 | | |
315 | 318 | | |
316 | 319 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
286 | 286 | | |
287 | 287 | | |
288 | 288 | | |
289 | | - | |
| 289 | + | |
| 290 | + | |
| 291 | + | |
| 292 | + | |
290 | 293 | | |
291 | 294 | | |
292 | 295 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
286 | 286 | | |
287 | 287 | | |
288 | 288 | | |
289 | | - | |
| 289 | + | |
| 290 | + | |
| 291 | + | |
| 292 | + | |
290 | 293 | | |
291 | 294 | | |
292 | 295 | | |
| |||
0 commit comments