\item[]\VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (RFC n p)}\\
In the memory share \texttt{sh}, the address \VSTe{v_q} points
to a list of integer values \VSTe{mVI (RFC n p)} where \VSTe{RFC n p} is the
result of the \TNaCle{crypto_scalarmult} of \VSTe{n} and \VSTe{p}.
\item[]\VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (RFC n p)}\\
\VSTe{PROP}: \VSTe{Zlength (RFC n p) = 32}\\
We show that the computation for \VSTe{RFC} fits in \TNaCle{u8[32]}.
\end{itemize}
computes the same result as \VSTe{RFC} in Coq provided that inputs are within
their respective bounds: arrays of 32 bytes.
The correctness of this specification is formally proven in Coq with
\coqe{Theorem body_crypto_scalarmult}.
\todo{Fix bleeding}
This specification (proven with VST) shows that \TNaCle{crypto_scalarmult} in C
% The Verifiable Software Toolchain uses a strongest postcondition strategy.
% The user must first write a formal specification of the function he wants to verify in Coq.
% This should be as close as possible to the C implementation behavior.
% This will simplify the proof and help with stepping through the Clight version of the software.
% With the range of inputs defined, VST mechanically steps through each instruction
% and ask the user to verify auxiliary goals such as array bound access, or absence of overflows/underflows.
% We call this specification a low level specification. A user will then have an easier
% time to prove that his low level specification matches a simpler higher level one.
% In order to further speed-up the verification process, it has to be know that to
% prove the specification \TNaCle{crypto_scalarmult}, a user only need the specification of e.g. \TNaCle{M}.
% This provide with multiple advantages: the verification by the Coq kernel can be done
% in parallel and multiple users can work on proving different functions at the same time.
% For the sake of completeness we proved all intermediate functions.
\subheading{Memory aliasing.}
%
The semicolon in the \VSTe{SEP} parts of the Hoare triples represents the \emph{separating conjunction} (often written as a star), which means that
the memory shares of \texttt{q}, \texttt{n} and \texttt{p} do not overlap.
In other words,
we only prove correctness of \TNaCle{crypto_scalarmult} when it is called without aliasing.
But for other TweetNaCl functions, like the multiplication function \texttt{M(o,a,b)}, we cannot ignore aliasing, as it is called in the ladder in an aliased manner.
In the VST, a simple specification of this function will assume that the pointer arguments
point to non-overlapping space in memory.
When called with three memory fragments (\texttt{o, a, b}),
the three of them will be consumed. However assuming this naive specification
when \texttt{M(o,a,a)} is called (squaring), the first two memory areas (\texttt{o, a})
are consumed and the VST will expect a third memory section (\texttt{a}) which does not \emph{exist} anymore.
Examples of such cases are illustrated in \fref{tikz:MemSame}.
\begin{figure}[h]%
\centering%
\include{tikz/memory_same_sh}%
\caption{Aliasing and Separation Logic}%
\label{tikz:MemSame}%
\end{figure}
As a result, a function must either have multiple specifications or specify which
aliasing case is being used.
The first option would require us to do very similar proofs multiple times for a same function.
We chose the second approach: for functions with 3 arguments, named hereafter \texttt{o, a, b},
we define an additional parameter $k$ with values in $\{0,1,2,3\}$:
\begin{itemize}
\item if $k=0$ then \texttt{o} and \texttt{a} are aliased.
\item if $k=1$ then \texttt{o} and \texttt{b} are aliased.
\item if $k=2$ then \texttt{a} and \texttt{b} are aliased.
\item else there is no aliasing.
\end{itemize}
In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not cover all cases (\eg all arguments are aliased) but it
\item[]\VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (RFC n p)}\\
In the memory share \texttt{sh}, the address \VSTe{v_q} points
to a list of integer values \VSTe{mVI (RFC n p)} where \VSTe{RFC n p} is the
result of the \TNaCle{crypto_scalarmult} of \VSTe{n} and \VSTe{p}.
\item[]\VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (RFC n p)}\\
\VSTe{PROP}: \VSTe{Zlength (RFC n p) = 32}\\
We show that the computation for \VSTe{RFC} fits in \TNaCle{u8[32]}.
\end{itemize}
computes the same result as \VSTe{RFC} in Coq provided that inputs are within
their respective bounds: arrays of 32 bytes.
The correctness of this specification is formally proven in Coq with
\coqe{Theorem body_crypto_scalarmult}.
\begin{sloppypar}
This specification (proven with VST) shows that \TNaCle{crypto_scalarmult} in C
\end{sloppypar}
% The Verifiable Software Toolchain uses a strongest postcondition strategy.
% The user must first write a formal specification of the function he wants to verify in Coq.
% This should be as close as possible to the C implementation behavior.
% This will simplify the proof and help with stepping through the Clight version of the software.
% With the range of inputs defined, VST mechanically steps through each instruction
% and ask the user to verify auxiliary goals such as array bound access, or absence of overflows/underflows.
% We call this specification a low level specification. A user will then have an easier
% time to prove that his low level specification matches a simpler higher level one.
% In order to further speed-up the verification process, it has to be know that to
% prove the specification \TNaCle{crypto_scalarmult}, a user only need the specification of e.g. \TNaCle{M}.
% This provide with multiple advantages: the verification by the Coq kernel can be done
% in parallel and multiple users can work on proving different functions at the same time.
% For the sake of completeness we proved all intermediate functions.
\subheading{Memory aliasing.}
%
The semicolon in the \VSTe{SEP} parts of the Hoare triples represents the \emph{separating conjunction} (often written as a star), which means that
the memory shares of \texttt{q}, \texttt{n} and \texttt{p} do not overlap.
In other words,
we only prove correctness of \TNaCle{crypto_scalarmult} when it is called without aliasing.
But for other TweetNaCl functions, like the multiplication function \texttt{M(o,a,b)}, we cannot ignore aliasing, as it is called in the ladder in an aliased manner.
In the VST, a simple specification of this function will assume that the pointer arguments
point to non-overlapping space in memory.
When called with three memory fragments (\texttt{o, a, b}),
the three of them will be consumed. However assuming this naive specification
when \texttt{M(o,a,a)} is called (squaring), the first two memory areas (\texttt{o, a})
are consumed and the VST will expect a third memory section (\texttt{a}) which does not \emph{exist} anymore.
Examples of such cases are illustrated in \fref{tikz:MemSame}.
\begin{figure}[h]%
\centering%
\include{tikz/memory_same_sh}%
\caption{Aliasing and Separation Logic}%
\label{tikz:MemSame}%
\end{figure}
As a result, a function must either have multiple specifications or specify which
aliasing case is being used.
The first option would require us to do very similar proofs multiple times for a same function.
We chose the second approach: for functions with 3 arguments, named hereafter \texttt{o, a, b},
we define an additional parameter $k$ with values in $\{0,1,2,3\}$:
\begin{itemize}
\item if $k=0$ then \texttt{o} and \texttt{a} are aliased.
\item if $k=1$ then \texttt{o} and \texttt{b} are aliased.
\item if $k=2$ then \texttt{a} and \texttt{b} are aliased.
\item else there is no aliasing.
\end{itemize}
In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not cover all cases (\eg all arguments are aliased) but it
\coqe{Inv25519}; \coqe{car25519} behave over \coqe{list Z} as their equivalent
over \coqe{Z} with \coqe{:GF} (in \Zfield), we prove that given the same inputs
\coqe{Crypto_Scalarmult} performs the same computation as \coqe{RFC}.
\end{sloppypar}
By proving that each function \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519} behave over \coqe{list Z}
as their equivalent over \coqe{Z} with \coqe{:GF} (in \Zfield), we prove that given the same inputs \coqe{Crypto_Scalarmult} performs the same computation as \coqe{RFC}.
