Proofs: Grisu

A result certified by Grisu3 is the shortest and nearest decimal, and the fallback is exact full

This proof shows: correctness.

Setting. Binary64, $x > 0$ finite, $x = f \cdot 2^{e}$ as decoded by L1. Let $x^{\pm}$ be the neighbors of $x$ (with $x^{+} = 2^{1024}$ for the largest finite number), $M^{+} = (x + x^{+})/2$, $M^{-} = (x^{-} + x)/2$, and let $R$ be the rounding interval with ends $M^{-}$ and $M^{+}$, closed when $f$ is even and open otherwise (ties to even). We prove: if grisu3(x) returns digits $N$ and an exponent $t$, then $y = N \cdot 10^{t}$ lies strictly inside $(M^{-}, M^{+})$, so every reader that rounds to nearest maps $y$ to $x$; no number with fewer significant digits lies in the closed interval $[M^{-}, M^{+}]$; and $y$ is the multiple of $10^{t}$ in $R$ nearest to $x$. Then we prove the fallback correct.

Lemma 1 (the boundaries are exact, L2). $(2f + 1)2^{e - 1} = M^{+}$, and $M^{-}$ equals $(4f - 1) 2^{e - 2}$ if $x$ is a power of two above the smallest normal and $(2f - 1)2^{e - 1}$ otherwise; all three numbers $x$, $M^{+}$, $M^{-}$ are represented exactly with significands below $2^{64}$ and a common exponent after the shifts of L2.

Proof. The spacing of floats around $x$ is $2^{e}$ on both sides, except below a power of two $2^{52} \cdot 2^{e}$ with $e > -1074$, where it is $2^{e - 1}$; the midpoints follow. The significands have at most $55$ binary digits, and normalizing $M^{+}$ to $64$ digits and shifting $M^{-}$ to the same exponent keeps $M^{-} < M^{+} < 2^{64} \cdot 2^{\text{exponent}}$. $\square$

Lemma 2 (scaling errors, L3 to L5). Let $10^{K}$ be the cached power and $\mathbf{1} = 2^{-e_2}$, where $e_2 \in [-60, -32]$ is the common binary exponent of the three products. Measure everything in units of $2^{e_2}$, and let $w^{*} = x 10^{K} 2^{-e_2}$, $h^{*} = M^{+} 10^{K} 2^{-e_2}$, $\ell^{*} = M^{-} 10^{K} 2^{-e_2}$ be the exact scaled values. Then the computed integers satisfy $|w - w^{*}| < 1$, $|\mathit{high} - h^{*}| < 1$ and $|\mathit{low} - \ell^{*}| < 1$. Consequently $\mathit{too\_low} < \ell^{*}$ and $h^{*} < \mathit{too\_high}$.

Proof. The table entry is $c_f = 10^{K} 2^{-c_e}(1 + \text{error})$ with $|c_f - 10^{K}2^{-c_e}| \le \tfrac12$. For a 64-bit significand $a$, $a c_f 2^{-64}$ differs from the exact $a \cdot 10^{K} 2^{-c_e - 64}$ by at most $a \cdot \tfrac12 \cdot 2^{-64} < \tfrac12$, and _times rounds $a c_f 2^{-64}$ to an integer with error at most $\tfrac12$. The sum is below $1$. Then $\mathit{too\_low} = \mathit{low} - 1 < \ell^{*}$ and $\mathit{too\_high} = \mathit{high} + 1 > h^{*}$. $\square$

So the scaled closed interval $[\ell^{*}, h^{*}]$ lies strictly inside the unsafe interval $(\mathit{too\_low}, \mathit{too\_high})$, and every point $c$ with $\mathit{too\_low} + 2 \le c \le \mathit{too\_high} - 2$ lies strictly inside $(\ell^{*}, h^{*})$, since $\ell^{*} < \mathit{low} + 1 = \mathit{too\_low} + 2$ and $h^{*} > \mathit{high} - 1 = \mathit{too\_high} - 2$.

Lemma 3 (digit generation, L6 and L7). Let the loop stop when the digits produced so far form the integer $D$ and the current position is $10^{\kappa}$, and let $\Delta = 10^{\kappa}\mathbf{1}$ (the weight of the last digit in units). Then $c = D\Delta$ is the largest multiple of $\Delta$ that is at most $\mathit{too\_high}$, $c > \mathit{too\_low}$, and for every coarser power $\Delta' = 10^{\kappa'}\mathbf{1}$ with $\kappa' > \kappa$ there is no multiple of $\Delta'$ in $(\mathit{too\_low}, \mathit{too\_high}]$.

Proof. The integer part of $\mathit{too\_high}/\mathbf{1}$ is integrals, below $2^{32}$, and its decimal digits are produced from the left; after each digit, rest is $\mathit{too\_high}$ minus the truncation of $\mathit{too\_high}$ to the current position, so the truncation is the largest multiple of the current $\Delta$ that is at most $\mathit{too\_high}$. In the fractional phase, all of fractionals, unit, unsafe and the distance passed to _round_weed are multiplied by $10$ at each step, which is the same as measuring in units of $2^{e_2}/10^{j}$ after $j$ fractional digits, and the same statement holds. The loop continues while $\mathit{rest} \ge \mathit{unsafe} = \mathit{too\_high} - \mathit{too\_low}$, that is, while the truncation is at most $\mathit{too\_low}$; then no multiple of that $\Delta'$ lies in $(\mathit{too\_low}, \mathit{too\_high}]$, because the largest one below $\mathit{too\_high}$ is already not above $\mathit{too\_low}$. For powers coarser than the first digit, the only multiples at most $\mathit{too\_high}$ are $\le 0 < \mathit{too\_low}$. It stops at the first position with $\mathit{rest} < \mathit{unsafe}$, that is, $c > \mathit{too\_low}$. All quantities stay below $2^{64}$: $\mathit{too\_high} < 2^{64}$, $\mathbf{1} \le 2^{60}$, and in the fractional phase the loop only continues while $\mathit{unsafe} \le \mathit{fractionals} < \mathbf{1}$, so $10\,\mathit{unsafe} < 2^{64}$. $\square$

Lemma 4 (fewest digits). No number with fewer significant digits than $N$ lies in $[M^{-}, M^{+}]$.

Proof. Scaling by $10^{K} 2^{-e_2}$ maps decimals to decimals with the same significant digits up to the power of ten, and $[M^{-}, M^{+}]$ to $[\ell^{*}, h^{*}] \subset (\mathit{too\_low}, \mathit{too\_high})$. Suppose $z$ in this interval has fewer significant digits than the accepted $c$. If $z$ and $c$ have the same leading position, then $z$ is a multiple of a coarser power $\Delta'$, which Lemma 3 excludes. If the leading position of $z$ is lower, then $z < 10^{L} \le c$ for the leading power $10^{L}$ of $c$ (in units), so $10^{L}$ lies in the interval between $z$ and $c$, inside $(\mathit{too\_low}, \mathit{too\_high})$; it is a multiple of $10^{L}$, which is coarser than $\Delta$ unless $c$ has one digit, and then $z$ cannot have fewer. Both cases contradict Lemma 3. A leading position of $z$ above that of $c$ is impossible, since $z < \mathit{too\_high} < 10^{L + 1}$ by Lemma 3 applied to $\Delta' = 10^{L+1}$. $\square$

Lemma 5 (rounding, L8 to L10). If _round_weed returns true, the final candidate $c$ lies strictly inside $(\ell^{*}, h^{*})$ and is the multiple of $\Delta$ nearest to $w^{*}$ among those in $[\ell^{*}, h^{*}]$, strictly nearer than any other.

Proof. Write $c = \mathit{too\_high} - \mathit{rest}$ and let $u$ be the current unit. The distance $\mathit{too\_high} - w$ is passed in, so by Lemma 2, $w^{*}$ lies in the open interval $(w_{\mathrm{lo}}, w_{\mathrm{hi}})$ with $w_{\mathrm{hi}} = \mathit{too\_high} - \mathit{small} = w + u$ and $w_{\mathrm{lo}} = \mathit{too\_high} - \mathit{big} = w - u$. The loop of L8 replaces $c$ by $c - \Delta$ while (i) $c > w_{\mathrm{hi}}$, (ii) $c - \Delta \ge \mathit{too\_low}$, and (iii) $c - \Delta$ is above $w_{\mathrm{hi}}$ or at least as close to $w_{\mathrm{hi}}$ as $c$ (the two forms of the third condition are $\mathit{rest} + \Delta < \mathit{small}$ and $c - w_{\mathrm{hi}} \ge w_{\mathrm{hi}} - (c - \Delta)$). Hence at the end of the loop, $c + \Delta$ is either the initial candidate's successor, which exceeds $\mathit{too\_high} > h^{*}$, or a former candidate that is not closer to $w_{\mathrm{hi}}$ than $c$, and therefore strictly farther than $c$ from every point below $w_{\mathrm{hi}}$, in particular from $w^{*}$. L9 returns false unless one of the conditions fails for $w_{\mathrm{lo}}$: (i') $c \le w_{\mathrm{lo}}$, or (ii') $c - \Delta < \mathit{too\_low} < \ell^{*}$, or (iii') $c - \Delta$ is not strictly closer to $w_{\mathrm{lo}}$ than $c$. In case (i'), $c < w^{*}$ and every smaller multiple is farther; in case (ii'), no smaller multiple is in $[\ell^{*}, h^{*}]$; in case (iii'), $c$ is at least as close to $w_{\mathrm{lo}}$ as $c - \Delta$, so strictly closer to every point above $w_{\mathrm{lo}}$, in particular to $w^{*}$. So no other multiple of $\Delta$ in $[\ell^{*}, h^{*}]$ is as close to $w^{*}$ as $c$. Finally, the test $2u \le \mathit{rest} \le \mathit{unsafe} - 4u$ means $\mathit{too\_low} + 4u \le c \le \mathit{too\_high} - 2u$; in units of $u$, Lemma 2 gives $\ell^{*} < \mathit{too\_low} + 2u$ and $h^{*} > \mathit{too\_high} - 2u$, so $\ell^{*} < c < h^{*}$. $\square$

Theorem. If grisu3(x) returns $(N, t)$, then $y = N 10^{t}$ lies in the open interval $(M^{-}, M^{+})$, no number with fewer significant digits lies in $[M^{-}, M^{+}]$, $y$ has nonzero first and last digits, and $y$ is the strictly nearest to $x$ among the multiples of $10^{t}$ in $R$. In particular to_string agrees with any correct shortest-nearest printer whenever grisu3 succeeds.

Proof. Undo the scaling: the accepted $c$ corresponds to $y = N 10^{\kappa - K}$ and $t = \kappa - K$. Lemmas 4 and 5 give the claims about the interval, the length and the nearest choice. The first digit is nonzero by construction. If the last digit were $0$, $y$ would be a multiple of $10^{t + 1}$ inside the interval, contradicting Lemma 4. The last digit never goes below $0$ in L8: a candidate whose last digit is $0$ is a multiple of $10\Delta$, and by Lemma 3 none lies in $(\mathit{too\_low}, \mathit{too\_high}]$, so such a candidate equals $\mathit{too\_low}$, condition (ii) stops the loop there, and the final test rejects it. $\blacksquare$

The fallback. exact_shortest computes $R$ with exact rationals and searches the powers $10^{t}$ downward from a power of ten above $M^{+}$. For each $t$, the multiples of $10^{t}$ nearest to $x$ are $\lfloor x/10^{t}\rfloor 10^{t}$ and the next one; $R$ is an interval containing $x$, so it contains a multiple of $10^{t}$ if and only if it contains one of these two. The first $t$ for which one is inside is the coarsest, and by the argument of Lemma 4 the number chosen has the fewest significant digits; among the two candidates it takes the nearer, and the even one in a tie. As in the analysis of Dragon4, a shortest number that is not a multiple of $10^{t}$ can exist only if $R$ straddles a power of ten and contains a one-digit number below it, which needs a relative width of $R$ above $10\%$, that is a subnormal $m 2^{-1074}$ with $m \le 9$; for these nine values the tests compare the output with Python's repr directly. So shortest(x) is always the shortest, nearest decimal, ties to even. $\blacksquare$