Proofs: Ryu

Ryu returns the shortest, closest decimal in the rounding interval full

This proof shows: correctness.

Setting. $x = v \cdot 2^{e_2}$ is a positive binary64 number with $v = 4m_2$, and its rounding interval $I_x$ has ends $L = u \cdot 2^{e_2}$ and $H = w \cdot 2^{e_2}$ with $u = v - 1 - \sigma$, $w = v + 2$, $\sigma \in \{0, 1\}$. Both ends belong to $I_x$ when $m_2$ is even and neither does when $m_2$ is odd. So $H - x = 2 \cdot 2^{e_2}$ and $x - L = (1 + \sigma) 2^{e_2} \le H - x$.

What is assumed. (A1) Line L3 computes the exact floors $vm = \lfloor L/10^E \rfloor$, $vr = \lfloor x/10^E \rfloor$, $vp = \lfloor H/10^E \rfloor$ at the starting exponent $E = e_{10}$. This is Adams's table-precision result. (A2) The flags of lines L4, L5 and L7 tell exactly whether $L/10^E$ and $x/10^E$ are integers, in every case where that changes the output. For $e_2 < 0$ this is exact: $x/10^{e_{10}} = v \cdot 5^{-e_2 - q}/2^q$ is an integer iff $2^q \mid v$, and $u$, $w$ are not multiples of 4, so for $q \ge 2$ the ends are never integers at that scale. For $e_2 \ge 0$ the cutoff $q \le 21$ is taken from the reference implementation. The tests check (A1) and the final output in exact rationals.

For a scale $10^k$, call an integer $n$ admissible at $k$ if $n \cdot 10^k \in I_x$.

Lemma 1 (shortest decimals). Let $k^\ast$ be the largest $k$ such that some integer is admissible at $k$. Then the decimals in $I_x$ with the fewest significant digits are exactly the $n \cdot 10^{k^\ast}$ with $n$ admissible at $k^\ast$.

Proof. $I_x$ is narrower than $x$ itself, so $H < 2L$, and the leading decimal positions of numbers in $I_x$ differ by at most one. Write $\lambda(y)$ for the position of the leading digit of $y$ and $\tau(y)$ for the position of its last nonzero digit, so $y$ has $\lambda(y) - \tau(y) + 1$ significant digits. Every $y \in I_x$ has $\tau(y) \le k^\ast$ by maximality. If $I_x$ contains a power of ten $10^t$, then $t \le k^\ast$ and also $10^t \le H < 10^{t+1}$, so $k^\ast = t$, the multiples of $10^t$ in $I_x$ are among $10^t, \ldots, 9 \cdot 10^t$ and all have one digit; one digit is the minimum. Otherwise every $y \in I_x$ has the same $\lambda(y) = \lambda$, and the length $\lambda - \tau(y) + 1$ is minimal exactly when $\tau(y) = k^\ast$, that is, when $y$ is a multiple of $10^{k^\ast}$ (a multiple of $10^{k^\ast}$ in $I_x$ is not a multiple of $10^{k^\ast + 1}$). $\square$

Lemma 2 (the start is fine enough). At the start, $E = e_{10} \le k^\ast$, and either $x/10^{E}$ is an integer or $E < k^\ast$.

Proof. For $e_2 \ge 0$, $q = \lfloor e_2 \log_{10} 2 \rfloor - [e_2 > 3]$ and $10^{e_{10}} = 10^q$. For $e_2 < 0$, $q = \lfloor -e_2 \log_{10} 5 \rfloor - [-e_2 > 1]$, $e_{10} = e_2 + q$, and $10^{e_{10}}/2^{e_2} = 10^q/5^{-e_2}$. In both cases $10^{e_{10}} \le 2^{e_2}$, and when the subtracted indicator is 1, $10^{e_{10}} \le 2^{e_2}/10$. The interval $[L, H]$ has length $(3 + \sigma) 2^{e_2} \ge 3 \cdot 2^{e_2}$, so its interior contains a multiple of $10^{e_{10}}$, which gives $k^\ast \ge e_{10}$; when the indicator is 1 the interior has length at least $30 \cdot 10^{e_{10}}$ and contains a multiple of $10^{e_{10}+1}$, so $k^\ast > e_{10}$. When the indicator is 0, either $0 \le e_2 \le 3$, so $q = 0$, $E = 0$ and $x = v \cdot 2^{e_2}$ is an integer, or $e_2 = -1$, so $q = 0$, $E = -1$ and $x/10^{-1} = 5v$ is an integer. $\square$

Lemma 3 (the loops stop at $k^\ast$). Keep the invariant that at exponent $E$, $vm = \lfloor L/10^E \rfloor$, $vr = \lfloor x/10^E \rfloor$, and $vp$ is the largest integer $n \le H/10^E$ with $n \cdot 10^E \le H$ allowed (that is, $vp = \lfloor H/10^E \rfloor$, minus 1 if $H/10^E$ is an integer and $H$ is excluded). Line L5 establishes it, and dividing by 10 preserves it because $\lfloor \lfloor y \rfloor / 10 \rfloor = \lfloor y/10 \rfloor$, while for an excluded integer end $\lfloor (n - 1)/10 \rfloor$ is again the largest allowed integer below $n/10$.

The integers in $(vm, vp]$ are exactly the integers admissible at $E$ that are strictly above $L/10^E$. So $\lfloor vp/10 \rfloor > \lfloor vm/10 \rfloor$ holds iff some multiple of 10 lies in $(vm, vp]$, that is, iff some integer strictly above $L/10^{E+1}$ is admissible at $E + 1$. The only admissible integer it misses is $L/10^{E+1}$ itself, when $L$ is included and is a multiple of $10^{E+1}$. Line L6 runs while the first kind exists; when it stops, no admissible integer at any coarser scale lies strictly above $L$ (each would give one at $E+1$). Line L7 then continues exactly while the included end $L$ is a multiple of $10^{E+1}$; the flag tracks that $L/10^E$ is an integer, and $vm \bmod 10 = 0$ tests the next digit. When both loops stop, no integer is admissible at $E + 1$ and some is admissible at $E$ (by Lemma 2 at the start, and by the loop condition after each step). Hence $E = k^\ast$. $\square$

Lemma 4 (rounding). At $E = k^\ast$ let $r = x/10^{E} \in [vr, vr + 1)$. Line L6 records $\ell$, the first digit of $r - vr$, and whether all later digits are zero. Then $r - vr > 1/2$ iff $\ell \ge 6$ or ($\ell = 5$ and some later digit is nonzero), and $r - vr = 1/2$ iff $\ell = 5$ and all later digits are zero. Lines L8 and L9 therefore choose $vr + 1$ exactly when $r - vr > 1/2$, or $r - vr = 1/2$ and $vr$ is odd, or $vr$ is not admissible; this needs at least one digit to have been dropped, or $r$ to be an integer, which Lemma 2 guarantees.

The candidate chosen is admissible. If $vr$ is not admissible, then $vr \cdot 10^E < L$ (it is at most $x$), and since some integer is admissible and all admissible integers exceed $vr$, the least of them is $vr + 1$. If $vr + 1$ is chosen by rounding but were not admissible, then $H \le (vr + 1)10^E$, so $H - x < 10^E/2$, hence $x - L \le H - x < 10^E/2$ and $L > vr \cdot 10^E$; then neither $vr$ nor $vr + 1$ is admissible, and no other integer is (they lie outside $[L, H]$), contradicting $E = k^\ast$. $\square$

Theorem. Under (A1) and (A2), RYU returns $d \cdot 10^E$ with $E = k^\ast$ and $d$ the admissible integer at $k^\ast$ nearest to $x/10^{k^\ast}$, ties to even. By Lemma 1 this is the shortest decimal in $I_x$ and the closest to $x$ among the shortest. $d$ is not divisible by 10, since otherwise $d/10$ would be admissible at $k^\ast + 1$.

Proof. Lemmas 2 and 3 give $E = k^\ast$; Lemma 4 gives the choice of $d$. The nearest admissible integer to $r$ is $vr$ or $vr + 1$, because these are the integers on either side of $r$ and whichever is nearer and admissible is chosen. $\square$