4.3-numbers.tex 2.25 KB
 Benoit Viguier committed Jan 14, 2020 1 2 3 4 \subsection{Number representation and C implementation} \label{subsec:num-repr-rfc} As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented  Benoit Viguier committed Feb 06, 2020 5 in $2^{16}$ and we use a direct mapping to represent that array as a list  Benoit Viguier committed Jan 14, 2020 6 integers in Coq. However, in order to show the correctness of the basic operations,  Benoit Viguier committed Feb 14, 2020 7 we need to convert this number to an integer.  Benoit Viguier committed Jan 14, 2020 8 We reuse the mapping  Benoit Viguier committed Feb 06, 2020 9 $\text{\coqe{ZofList}} : \Z \rightarrow \texttt{list}~\Z \rightarrow \Z$ from \sref{sec:Coq-RFC}  Benoit Viguier committed Jan 14, 2020 10 11 12 13 14 15 16 17 and define a notation where $n$ is $16$, placing us with a radix of $2^{16}$. \begin{lstlisting}[language=Coq] Notation "Z16.lst A" := (ZofList 16 A). \end{lstlisting} To facilitate working in $\Zfield$, we define the \coqe{:GF} notation. \begin{lstlisting}[language=Coq] Notation "A :GF" := (A mod (2^255-19)). \end{lstlisting}  Benoit Viguier committed Feb 14, 2020 18 Later in \sref{subsec:Zmodp}, we formally define $\Ffield$ as a field.  Benoit Viguier committed Jan 14, 2020 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 Equivalence between operations in $\Zfield$ (\ie under \coqe{:GF}) and in $\Ffield$ are easily proven. Using these two definitions, we prove intermediate lemmas such as the correctness of the multiplication \Coqe{Low.M} where \Coqe{Low.M} replicates the computations and steps done in C. \begin{lemma} \label{lemma:mult_correct} \Coqe{Low.M} correctly implements the multiplication over $\Zfield$. \end{lemma} And specified in Coq as follows: \begin{lstlisting}[language=Coq] Lemma mult_GF_Zlength : forall (a:list Z) (b:list Z), Zlength a = 16 -> Zlength b = 16 -> (Z16.lst (Low.M a b)) :GF = (Z16.lst a * Z16.lst b) :GF. \end{lstlisting} However for our purpose, simple functional correctness is not enough. We also need to define the bounds under which the operation is correct, allowing us to chain them, guaranteeing us the absence of overflow. \begin{lemma} \label{lemma:mult_bounded} if all the values of the input arrays are constrained between $-2^{26}$ and $2^{26}$, then the output of \coqe{Low.M} will be constrained between $-38$ and $2^{16} + 38$. \end{lemma} And seen in Coq as follows: \begin{lstlisting}[language=Coq] Lemma M_bound_Zlength : forall (a:list Z) (b:list Z), Zlength a = 16 -> Zlength b = 16 -> Forall (fun x => -2^26 < x < 2^26) a -> Forall (fun x => -2^26 < x < 2^26) b -> Forall (fun x => -38 <= x < 2^16 + 38) (Low.M a b). \end{lstlisting}