You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
0 commit comments