Commit 1921207
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.
To encode this in Rust, we might think to use `a % b` for
`r_T` (remainder of truncated division). After all, we document[^2]
that `a % b` is computed as...
```rust
a - b * (a / b).trunc()
```
However, as it turns out, we do not currently compute `Rem` in this
way, as can be seen trivially with:
```rust
let (x, y) = (11f64, 1.1f64);
assert_eq!(x - (x / y).trunc() * y, x % y); //~ PANIC
```
For the moment, therefore, we've encoded `r_T` in the literal way.
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 1921207
4 files changed
+44
-8
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
309 | 309 | | |
310 | 310 | | |
311 | 311 | | |
312 | | - | |
313 | | - | |
| 312 | + | |
| 313 | + | |
| 314 | + | |
| 315 | + | |
| 316 | + | |
| 317 | + | |
| 318 | + | |
| 319 | + | |
| 320 | + | |
| 321 | + | |
| 322 | + | |
314 | 323 | | |
315 | 324 | | |
316 | 325 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
309 | 309 | | |
310 | 310 | | |
311 | 311 | | |
312 | | - | |
313 | | - | |
| 312 | + | |
| 313 | + | |
| 314 | + | |
| 315 | + | |
| 316 | + | |
| 317 | + | |
| 318 | + | |
| 319 | + | |
| 320 | + | |
| 321 | + | |
| 322 | + | |
314 | 323 | | |
315 | 324 | | |
316 | 325 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
285 | 285 | | |
286 | 286 | | |
287 | 287 | | |
288 | | - | |
289 | | - | |
| 288 | + | |
| 289 | + | |
| 290 | + | |
| 291 | + | |
| 292 | + | |
| 293 | + | |
| 294 | + | |
| 295 | + | |
| 296 | + | |
| 297 | + | |
| 298 | + | |
290 | 299 | | |
291 | 300 | | |
292 | 301 | | |
| |||
| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
285 | 285 | | |
286 | 286 | | |
287 | 287 | | |
288 | | - | |
289 | | - | |
| 288 | + | |
| 289 | + | |
| 290 | + | |
| 291 | + | |
| 292 | + | |
| 293 | + | |
| 294 | + | |
| 295 | + | |
| 296 | + | |
| 297 | + | |
| 298 | + | |
290 | 299 | | |
291 | 300 | | |
292 | 301 | | |
| |||
0 commit comments