Commit bd36aef0 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more of Freek's comment

parent aca27411
......@@ -15,26 +15,26 @@ As follow, we provide the explanations of the above changes to TweetNaCl's code.
\item lines 7-8: We tell the VST that \TNaCle{long long} are
aligned on 8 bytes.
\item lines 16-23: We remove the unused variable \TNaCle{i64 c} And the undefined behavior as explained in \sref{sec:Conclusion}.
\item lines 16-23: We remove the the undefined behavior as explained in \sref{sec:Conclusion}.
\item lines 29-31: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
\item lines 29-31; lines 60-62: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
\item lines 39 \& 41: We Initialize \TNaCle{m} with \TNaCle{0}.
This change allows us to prove the functional correctness of \TNaCle{pack25519} without having to deal with an array containing
a mix of uninitialized and initialized values.
A hand iteration over the loop trivially shows that no uninitialized values are used.
\item lines 40 \& 42: We replace \TNaCle{FOR(i,16) t[i]=n[i];} by \TNaCle{set25519(t,n);}. The semantic of operation done is the same once \TNaCle{set25519} is inlined. This small change is purely cosmetic but stays in the spirit of tweetnacl: keeping a small code size while being auditable.
\item lines 40 \& 42; lines 70 \& 71: We replace the \TNaCle{FOR} loop by \TNaCle{set25519}. The code is the same once the function is inlined. This small change is purely cosmetic but stays in the spirit of tweetnacl: keeping a small code size while being auditable.
\item lines 50-52: the VST does not allow computation in the argument before a function call. Additionally \texttt{clightgen} does not extract the computation either. We add this small step to allow the VST to carry through the proof.
\item lines 60-62: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
% \item lines 60-62: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
\item lines 70-71: We replace \TNaCle{FOR(a,16) c[a]=i[a];} by \TNaCle{set25519(c,i);}. The semantic of operation done is the same once \TNaCle{set25519} is inlined. This small change is purely cosmetic but stays in the spirit of tweetnacl: keeping a small code size while being auditable.
% \item lines 70-71: We replace \TNaCle{FOR(a,16) c[a]=i[a];} by \TNaCle{set25519(c,i);}. The semantic of operation done is the same once \TNaCle{set25519} is inlined. This small change is purely cosmetic but stays in the spirit of tweetnacl: keeping a small code size while being auditable.
\item lines 79-82: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.\\
In the function calls of \TNaCle{sel25519}, the specifications requires the use of \TNaCle{int}, the value of \TNaCle{r} being either \TNaCle{0} or \TNaCle{1}, we consider this change safe.
\item Lines 90-101: The \TNaCle{for} loop does not add any benefits to the code. By removing it we simplify the source and the verification steps as we do not need to deal with pointer arithmetic. As a result \TNaCle{x} can be constrained to only 16 \TNaCle{i64}, \ie \TNaCle{gf}.
\item Lines 90-101: The \TNaCle{for} loop does not add any benefits to the code. By removing it we simplify the source and the verification steps as we do not need to deal with pointer arithmetic. As a result, \TNaCle{x} can be limited to only 16 \TNaCle{i64}, \ie \TNaCle{gf}.
\end{itemize}
......@@ -2,7 +2,7 @@
\label{appendix:proof-folders}
\subheading{Requirements}
Our proofs requires the use of \emph{Coq.8.8.2} for the proofs and
Our proofs requires the use of \emph{Coq 8.8.2} for the proofs and
\emph{Opam 2.0} to manage the dependencies. We are aware that there exists more
recent versions of Coq; VST; CompCert etc. however to avoid dealing with backward
breaking compatibility we decided to freeze our dependencies.
......@@ -29,12 +29,12 @@ In this folder the reader will find multiple levels of implementation of X25519.
reason with lists and decidable procedures.
\item \textbf{\texttt{ListsOp/}} defines operators on list such as
\Coqe{ZofList} and related lemmas using \eg \VSTe{Forall}.
\item \textbf{\texttt{High/}} contains the theory of Montgomery curves,
twists, quadratic extensions and ladder.
It also proves the correctness of the ladder over $\F{\p}$.
\item \textbf{\texttt{Gen/}} defines a generic Montgomery ladder which can be
instantiated with different operations. This ladder is the stub for the
following implementations.
\item \textbf{\texttt{High/}} contains the theory of Montgomery curves,
twists, quadratic extensions and ladder.
It also proves the correctness of the ladder over $\F{\p}$.
\item \textbf{\texttt{Mid/}} provides a list-based implementation of the
basic operations \TNaCle{A}, \TNaCle{Z}, \TNaCle{M} \ldots~and the ladder. It
makes the link with the theory of Montgomery curves.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment