arthur.blot@ens-lyon.org
jean-michel.muller@ens-lyon.fr
Laurent.Thery@inria.fr
\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*}
\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*}
\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*}
\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*}
\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*}
\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*}
= Eq
\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*}
\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*}
$$\eta = 2^{-113.7}$$
= Gt
\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}$
$f(h) = 5^{16q} \cdot 5^{-r} \cdot 2^{-h}$
\begin{eqnarray*} -21 &\le q \le& 20 \\ 1 &\le r \le& 16 \end{eqnarray*}
\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*}
\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*}
\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*}
= Gt
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
Reference implementation
Proof and Computation
Errors and Simplifications
No counting argument
128 bits