Proofs: Dragon4 (Steele-White)

Dragon4 prints the shortest, nearest decimal in the rounding interval full

This proof shows: correctness.

Setting. Binary64, $x > 0$ finite, $x = m \cdot 2^{q}$ as returned by L1 ($m < 2^{53}$, $q \ge -1074$, and $m \ge 2^{52}$ unless $q = -1074$). Let $x^{-}$ and $x^{+}$ be the neighbors of $x$ (with $x^{+} = 2^{1024}$ for the largest finite number), $g^{-} = (x - x^{-})/2$ and $g^{+} = (x^{+} - x)/2$, and let $R$ be the rounding interval $[x - g^{-}, x + g^{+}]$ when $m$ is even and $(x - g^{-}, x + g^{+})$ when $m$ is odd. $R$ is the set of reals that a reader with round to nearest, ties to even, maps to $x$ (IEEE 754-2019, Clause 4.3.1; for the largest finite number the upper end is the overflow threshold of Clause 7.4). "Inside $R$" means in this interval, closed or open according to the parity of $m$; this is the variable inclusive. A decimal $y > 0$ has $n$ significant digits if $y = N \cdot 10^{t}$ with integers $N, t$ and $10^{n - 1} \le N < 10^{n}$.

Lemma 1 (setup, L2). After L2, $r/s = x$, $m^{+}/s = g^{+}$ and $m^{-}/s = g^{-}$.

Proof. If $m \ne 2^{52}$ or $q = -1074$, both neighbors are at distance $2^{q}$: in a binade the floats are the multiples of $2^{q}$, and at $q = -1074$ the subnormals and the smallest binade share that spacing. Then $g^{\pm} = 2^{q - 1}$, and the two branches give $r/s = 2m2^{q}/2$ or $2m/2^{1 - q}$, equal to $x$, and $m^{\pm}/s = 2^{q}/2$ or $1/2^{1 - q}$, equal to $2^{q-1}$. If $m = 2^{52}$ and $q > -1074$, then $x$ is a power of two, $x^{+} - x = 2^{q}$ and $x - x^{-} = 2^{q - 1}$, so $g^{+} = 2^{q - 1}$ and $g^{-} = 2^{q - 2}$; the branches give $r/s = 4m2^{q}/4$ or $4m/2^{2 - q}$, equal to $x$, $m^{+}/s = 2^{q + 1}/4$ or $2/2^{2 - q}$, equal to $2^{q - 1}$, and $m^{-}/s = 2^{q - 2}$. For the largest finite number, $m = 2^{53} - 1$ and $g^{+} = 2^{q - 1}$ matches the virtual neighbor $2^{1024}$. $\square$

In every later step $r$, $m^{+}$, $m^{-}$ and $s$ are multiplied by the same powers of ten in a way that L3 and L4 record in $k$, and L5 multiplies the first three by $10$ once per digit. Define, after the $j$-th execution of L6, the integer $D_{j}$ whose decimal digits are the digits produced so far, the last one being $d$ before any adjustment in L9. The next lemma is the invariant.

Lemma 2 (invariant). After L3 and L4, $r/s = x \cdot 10^{-k}$ and $m^{\pm}/s = g^{\pm} \cdot 10^{-k}$. After the $j$-th execution of L6, $0 \le r < s$ and

Proof. L3 multiplies $s$ by $10^{k}$ when $k \ge 0$, and $r$, $m^{\pm}$ by $10^{-k}$ when $k < 0$; each iteration of L4 multiplies $s$ by $10$ and adds $1$ to $k$. This gives the first claim from Lemma 1. For the second, induct on $j$: before step $j$, $x \cdot 10^{j - 1 - k} = D_{j - 1} + r/s$ with $D_0 = 0$ and $0 \le r < s$ (for $j = 1$, $r/s = x\cdot 10^{-k} < 1$ by Lemma 3 below). L5 makes $r/s$ ten times larger, and L6 writes $10r = ds + r'$ with $0 \le r' < s$, so $d \le 9$ and $x \cdot 10^{j - k} = 10 D_{j - 1} + d + r'/s = D_{j} + r'/s$. The relation for $m^{\pm}$ is multiplied by $10$ on both sides. A step that continues (L8) keeps $d$ as the last digit, so $D_j$ is as defined. $\square$

Lemma 3 (the exponent, L3 and L4). After L4, $k$ is the least integer such that every point of $R$ is below $10^{k}$. In particular $x < 10^{k}$, and $R$ contains no number $\ge 10^{k}$.

Proof. Let $e_2 = q + \ell(m) - 1$, where $\ell(m)$ is the length of $m$ in binary, so $2^{e_2} \le x < 2^{e_2 + 1}$. The constant $c = 30103/100000$ satisfies $0 < c - \log_{10} 2 < 5 \cdot 10^{-9}$, and $|e_2| \le 1075$, so $|e_2 c - e_2\log_{10} 2| < 10^{-5}$. Hence the estimate $k_0 = \lfloor e_2 c\rfloor - 1 \le e_2 c - 1 < e_2 \log_{10} 2 \le \log_{10} x$, so $10^{k_0} < x$. By Lemma 2 applied before the digit loop, the test of L4, $r + m^{+} > s$ or (inclusive and $r + m^{+} = s$), says exactly that the upper end $x + g^{+}$ of $R$ is above $10^{k}$, or equal to it with the end included, that is, that $R$ has a point $\ge 10^{k}$. This property is monotone in $k$: it holds for $k_0$ (since $x > 10^{k_0}$ and $x \in R$) and fails for large $k$. L4 increments $k$ until it fails, so the final $k$ is the least integer for which it fails. The loop runs at most $3$ times, since $x + g^{+} \le 2^{e_2 + 1}$ gives $\log_{10}(x + g^{+}) \le (e_2 + 1)\log_{10} 2 < k_0 + 3.31$. $\square$

Lemma 4 (what the tests mean). After step $j$, let $y_{j}^{-} = D_{j} \cdot 10^{k - j}$ and $y_{j}^{+} = (D_{j} + 1)\cdot 10^{k - j}$. Then $y_{j}^{-} \le x < y_{j}^{+}$, these are the consecutive multiples of $10^{k - j}$ around $x$, and low holds if and only if $y_{j}^{-}$ is inside $R$, high if and only if $y_{j}^{+}$ is inside $R$.

Proof. The bracketing is Lemma 2 with $0 \le r < s$. Multiplying by $s \cdot 10^{k-j}$, the test $r < m^{-}$ reads $x - y_{j}^{-} < g^{-}$, that is $y_{j}^{-} > x - g^{-}$, and equality $r = m^{-}$ is the lower end itself, admitted only when inclusive. Since $y_{j}^{-} \le x$, this is exactly "$y_{j}^{-}$ is inside $R$" (for $D_j = 0$ the test fails, consistent with $0 \notin R$ because $g^{-} < x$). Likewise $r + m^{+} > s$ reads $y_{j}^{+} < x + g^{+}$, with equality at the upper end. $\square$

Lemma 5 (numbers with few digits). For $n \ge 1$, $R$ contains a number with at most $n$ significant digits if and only if $y_{n}^{-}$ or $y_{n}^{+}$ is inside $R$.

Proof. By Lemma 3, every point of $R$ is below $10^{k}$, and at $k - 1$ the property of L4 holds, so $R$ has a point $z_0 \ge 10^{k - 1}$. Suppose $y \in R$ has $n' \le n$ significant digits. If $y \ge 10^{k - 1}$, its leading digit is at position $k - 1$ and its last nonzero digit at a position $\ge k - n' \ge k - n$, so $y$ is a positive multiple of $10^{k - n}$. If $y < 10^{k - 1}$, then $R$, an interval containing $y$ and $z_0$, contains $10^{k - 1}$, again a positive multiple of $10^{k - n}$. So in both cases $R$ contains a positive multiple $z$ of $10^{k - n}$. If $z \le x$ then $0 < z \le y_{n}^{-} \le x$, and if $z > x$ then $x < y_{n}^{+} \le z$; since $R$ is an interval containing $x$ and $z$, it contains $y_{n}^{-}$ or $y_{n}^{+}$ respectively. Conversely, $y_{n}^{\pm} \in R$ is a positive multiple of $10^{k - n}$ below $10^{k}$, which has at most $n$ significant digits. $\square$

Theorem. Let the loop stop after step $j$ and let $N$ be the integer whose digits are returned, so the output denotes $y = N \cdot 10^{k - j}$. Then:

1. $y$ is inside $R$, so a correctly rounding reader (ties to even) maps $y$ back to $x$;
2. no number with fewer than $j$ significant digits is inside $R$, and $y$ has exactly $j$ significant digits, its first and last digits being nonzero;
3. $y$ is the multiple of $10^{k - j}$ inside $R$ nearest to $x$, with a tie broken to an even last digit; it is also the nearest to $x$ of all the numbers with $j$ significant digits inside $R$.

Proof. By Lemma 4, the loop continues at step $n$ exactly when neither $y_{n}^{-}$ nor $y_{n}^{+}$ is inside $R$, which by Lemma 5 means that $R$ contains no number with at most $n$ significant digits. So $j$ is the least $n$ for which $R$ contains a number with at most $n$ significant digits; this is claim 2 except for the shape of the output. L9 returns $y_{j}^{-}$ when only low holds, $y_{j}^{+}$ when only high holds, and one of them when both hold; in each case $y$ is inside $R$, which is claim 1. $y$ is a positive multiple of $10^{k - j}$ below $10^{k}$, so it has at most $j$ significant digits, and by the minimality of $j$ not fewer. Hence $N \ge 10^{j - 1}$ and $10 \nmid N$ (for $j = 1$, $1 \le N \le 9$). The returned string is $D_{j - 1}$ followed by $d$ or $d + 1$; if $d + 1 = 10$ then $N$ would be divisible by $10$, so the last digit is a single digit, and a leading zero in $D_{j}$ would force $N = D_j + 1 = 10^{j - 1}$, divisible by $10$ for $j \ge 2$; so the string is exactly the decimal numeral of $N$.

For claim 3, the multiples of $10^{k - j}$ nearest to $x$ on each side are $y_{j}^{-}$ and $y_{j}^{+}$, and any other one inside $R$ is farther from $x$. If both are inside, then $x - y_{j}^{-} = (r/s) 10^{k - j}$ by Lemma 2, so $y_{j}^{-}$ is nearer when $2r < s$, $y_{j}^{+}$ when $2r > s$, and they tie when $2r = s$; L9 then chooses $d$ if it is even and $d + 1$ otherwise, the even last digit. By the proof of Lemma 5, a number with $j$ significant digits inside $R$ that is not a multiple of $10^{k - j}$ lies below $10^{k - 1}$, and then $10^{k - 1} \in R$ and $j = 1$. Such a one-digit number $z \le 9 \cdot 10^{k - 2}$ could beat $y$ only if $x < 10^{k - 1}$; then $R$ contains $z$ and $10^{k - 1}$, so its width, which is at most $2^{q}$, is at least $10^{k - 2}$, and $m = x/2^{q} < 10^{k - 1}/10^{k - 2} = 10$. So $x$ is one of the subnormals $m \cdot 2^{-1074}$ with $m \le 9$. Among them only $m = 2$ has $x < 10^{k - 1}$: there $R = [3 \cdot 2^{-1075}, 5 \cdot 2^{-1075}] \approx [7.41, 12.36] \cdot 10^{-324}$, $k = -322$, the output is $10^{-323}$ at distance about $0.12 \cdot 10^{-324}$ from $x \approx 9.88 \cdot 10^{-324}$, and the other one-digit candidates $8 \cdot 10^{-324}$ and $9 \cdot 10^{-324}$ are farther. $\blacksquare$

Remarks. The rounding interval is that of a reader with round to nearest, ties to even; for a reader that breaks ties differently, set inclusive from that rule. The proof uses only exact integer arithmetic after L1, so it does not depend on the rounding mode of the machine.