Comparing decimal64 and binary64


FastRelax Meeting June 2018

arthur.blot@ens-lyon.org

jean-michel.muller@ens-lyon.fr

Laurent.Thery@inria.fr

Inria

Comparing


\begin{align*} x &:= 7205759403792794 / 2^{56} \\ y &:= 1/10 \end{align*}

Decimal64


\begin{align*} x_{10} & = M_{10} \cdot 10^{e_{10} - 15}& \\ \end{align*} \begin{align*} -383 \leq & e_{10} \leq 384 \quad |M_{10}| \leq 10^{16} - 1 \end{align*}

Binary64


\begin{align*} x_2 & = M_2 \cdot 2^{e_2 - 52}& \\ \end{align*} \begin{align*} -1022 \leq & e_2 \leq 1023 \quad |M_2| \leq 2^{53} - 1 \\ \end{align*}

Normalisation

\begin{align*} x_{10} & = M_{10} \cdot 10^{e_{10} - 15}& \\ \end{align*}

\begin{align*} \nu & = 53 - \left \lfloor{\log_2(M_{10})}\right \rfloor& \\ \end{align*}

\begin{align*} n & = M_{10} 2 ^ \nu \qquad \qquad \qquad \,\,\,\, \\ \end{align*}

\begin{align*} g & = e_{10} - 15 \qquad \qquad \qquad \end{align*}

\begin{align*} x_{10} & = n \cdot 5^{g} 2^{g - \nu}& \quad\,\, \\ \end{align*}

Normalisation

\begin{align*} x_{2} & = M_{2} \cdot 2^{e_{2} - 52}& \\ \end{align*}

\begin{align*} m & = M_{2} \qquad \qquad \qquad \qquad \,\\ \end{align*}

\begin{align*} h & = \nu + e_2 - e_{10} - 37 & \\ \end{align*}

\begin{align*} x_{2} & = m \cdot 2^{h} 2^{g - \nu}& \\ \end{align*}

Normalisation

\begin{align*} x_{2} & = m \cdot 2^{h} 2^{g - \nu} \\ x_{10} & = \,\,n \cdot 5^{g} 2^{g - \nu} \\ \end{align*}

\begin{eqnarray*} 2 ^{52} & \le m \le & 2 ^{53} - 1 \\ 2 ^{53} & \le n \le & 2 ^{54} - 1 \\ -398 &\le g \le & 369\\ -1495 &\le h \le & 1422 \end{eqnarray*}

Comparing exponent


\begin{align*} m \cdot 2^{h} & \qquad & n \cdot 5^{g} \\ \end{align*}

\begin{equation*} \varphi(h) = \left \lfloor{h \cdot \log_5 2}\right \rfloor \end{equation*}

\begin{align*} \textit{If}\quad g < \varphi(h) & \quad \textit{then}\quad x_2 > x_{10} \\ \textit{If}\quad g > \varphi(h) & \quad \textit{then} \quad x_2 < x_{10} \end{align*}

Comparing exponent


\begin{equation*} \varphi(h) = \left \lfloor{h \cdot \log_5 2}\right \rfloor \end{equation*}

\begin{equation*} \lceil2^{19} \cdot \log_5 2\rfloor = 225799 \end{equation*}


\begin{equation*} \quad\qquad \varphi(h) = \left \lfloor{h \cdot 225799 \cdot 2^{-19}}\right \rfloor \end{equation*}

Comparing exponent


\begin{equation*} \lceil2^{19} \cdot \log_5 2\rfloor = 225799 \\ \left \lfloor{h \cdot \log_5 2}\right \rfloor = \left \lfloor{h \cdot 225799 \cdot 2^{-19}}\right \rfloor \end{equation*}

\begin{align*} 4306765 < 10000000 \cdot \log_5 2 < 4306766 \\ \end{align*} \begin{align*} \left\lfloor{x}\right\rfloor = y &\qquad\mbox{iff}& y \le x < y + 1 \\ \lceil x \rfloor = y &\qquad\mbox{if}& |x - y| < 1 / 2 \end{align*}

Comparing exponent


Comparing exponent


   = Eq


Finding Lower Bound


\begin{align*} m \cdot 2^{h} & \qquad & n \cdot 5^{g} \\ \end{align*}

\begin{equation*} \varphi(h) = \left \lfloor{h \cdot \log_5 2}\right \rfloor \end{equation*}

\begin{equation*} \varphi(h) = g \end{equation*}


\begin{equation*} f(h) = 5^{\varphi(h)} \cdot 2^{-h} \end{equation*}

Finding Lower Bound


\begin{align*} m \cdot 2^{h} & \qquad & n \cdot 5^{g} \\ \end{align*}

\begin{equation*} f(h) = 5^{\varphi(h)} \cdot 2^{-h} \end{equation*}

\begin{align*} f(h) \cdot n > m &\Rightarrow x_{10} > x_2 \\ f(h) \cdot n < m &\Rightarrow x_{10} < x_2 \\ f(h) \cdot n = m &\Rightarrow x_{10} = x_2 \end{align*}

Finding Lower Bound


$$\eta \le |{m/n - f(h)}|$$
\begin{eqnarray*} 2 ^{52} & \le m \le & 2 ^{53} - 1 \\ 2 ^{53} & \le n \le & 2 ^{54} - 1 \\ -787 &\le h \le & 716 \end{eqnarray*}

$$\eta = 2^{-113.7}$$

Finding Lower Bound


Finding Lower Bound


Finding Lower Bound


    = Gt

Bipartite table


\begin{equation*} f(h) = 5^{\varphi(h)} \cdot 2^{-h} \end{equation*}

\begin{equation*} q = \lfloor{\frac{\varphi(h)}{16} + 1}\rfloor \qquad\qquad r = 16q - \varphi(h) \quad \end{equation*}

$f(h) = 5^{16q} \cdot 5^{-r} \cdot 2^{-h}$

Bipartite table


$f(h) = 5^{16q} \cdot 5^{-r} \cdot 2^{-h}$

\begin{eqnarray*} -21 &\le q \le& 20 \\ 1 &\le r \le& 16 \end{eqnarray*}

Bipartite table


\begin{equation*} \psi(t) = \lfloor{t \cdot \log_2 5}\rfloor \end{equation*}


\begin{align*} \psi(t) &= \lfloor{\lceil{2^{12} \cdot \log_2 5}\rfloor \cdot t \cdot 2^{-12}}\rfloor & &\text{for $|t| \leq 204$} \\ \psi(16q) &= \lfloor{\lceil{2^{12} \cdot \log_2 5}\rfloor \cdot q \cdot 2^{-8}}\rfloor & &\text{for $|q| \leq 32$} \end{align*}

Bipartite table


\begin{align*} \theta_1(q) &= 5^{16q} \cdot 2^{-\psi(16q) + 127} \\ \theta_2(r) &= 5^r \cdot 2^{-\psi(r) + 63} \\ \sigma(h) & = \psi(r) - \psi(16q) + h \end{align*}


\begin{equation*} \Delta = \theta_1(q) \cdot n \cdot 2^{-64 + 8} - \theta_2(r) \cdot m \cdot 2^{8 + \sigma(h)} \end{equation*}

Bipartite table


\begin{equation*} \Delta = \theta_1(q) \cdot n \cdot 2^{-64 + 8} - \theta_2(r) \cdot m \cdot 2^{8 + \sigma(h)} \end{equation*}


$\textit{if}\quad x_2 \neq x_{10} \quad \textit{then} \quad |{\Delta}| \geq 2^{124} \eta$.


\begin{equation*} \tilde{\Delta} = \lfloor{\lceil{\theta_1(q)}\rceil \cdot n \cdot 2^{8 - 64}}\rfloor - \theta_2(r) \cdot m \cdot 2^{8 + \sigma(h)} \end{equation*}

Bipartite table


Bipartite table


Bipartite table


Bipartite table


    = Gt

Formalisation


https://gitlab.com/artart78/compbindec


   585 util.v
   266 compformula.v
   814 frac.v
  1175 rfrac.v
  3418 compbindec.v
  6258 total


Compilation Time : 15m44s

Conclusion


Reference implementation

Proof and Computation

Errors and Simplifications

No counting argument

128 bits