Commit 80ea974c authored by Benoit Viguier's avatar Benoit Viguier
Browse files

add diff explanations

parent 476e1285
......@@ -9,35 +9,32 @@
\lstinputlisting[language=diff]{tweetnacl.diff}
Below we provide the reasons of the diff.
As follow, we provide the explanations of the above changes to TweetNaCl's code.
\begin{itemize}
\item line 6-7: We tell VST that \TNaCle{long long} are aligned on 8 bytes.
\item lines 7-8: We tell the VST that \TNaCle{long long} are
aligned on 8 bytes.
\item line 13-20: This is change correspond to \TNaCle{car25519}.
We remove the unused variable \TNaCle{i64 c}, we remove the undefined behavior as explained in \sref{sec:Conclusion}.
\item lines 16-23: We remove the unused variable \TNaCle{i64 c} And the undefined behavior as explained in \sref{sec:Conclusion}.
\item line 24-29: The signature of
\end{itemize}
\item lines 29-31: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
@@ We remove the undefined behavior and
@@ simplify the carry propagation.
\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.
@@ b is a mask of 64 bits.
@@ For-loop indexes have to be int.
\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.
@@ For-loop indexes have to be int.
@@ b is a 64 bit mask.
@@ Initialize m to simplify verification.
\item lines 50-52: the VST does not allow computation in the argument before a function call. Additionaly \texttt{clightgen} does not extract the computation either. We add this small step to allow the VST to carry through the proof.
@@ Computations in arguments
@@ are not allowed in VST.
\item lines 60-62: The VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
@@ For-loop indexes have to be 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.
@@ gain 5 bytes.
\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.
@@ x only needs gf.
@@ For-loop indexes have to be int.
\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 arithmetics. As a result \TNaCle{x} can be constrained to only 16 \TNaCle{i64}, \ie \TNaCle{gf}.
@@ simplify
\end{itemize}
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