Commit 04419dc3 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

add description of the archive

parent b813f4aa
\subsection{Organization of the proof files}
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 more recent
versions of Coq; VST; CompCert etc. exist, however to avoid dealing with backward
breaking compatibilities we decided to freeze our dependencies.
\subheading{Associated files}
The archive containing the proof is composed of two folders \textbf{\texttt{packages}}
and \textbf{\texttt{proofs}}.
It aims to be used at the same time as an \emph{opam} repository to manage
the dependencies of the proof and to provide the code.
The actual proofs can be found in the \textbf{\texttt{proofs}} folder in which
the reader will find the \textbf{\texttt{spec}} and \textbf{\texttt{vst}}.
This folder makes sure that we are using the correct version of
Verifiable Software Toolchain (version 2.0) and CompCert (version 3.2).
Additionaly it pins the version of the elliptic curves library by Bartzia and Strub
and allows us to use the theorem of quadratic reciprocity.
In this folder the reader will find multiple levels of implementation of X25519.
\item \textbf{\texttt{Libs/}} contains basic libraries and tools to help use
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
instanciated with different operations.
\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.
\item \textbf{\texttt{Low/}} provides a second list-based implementation of
the basic operations \TNaCle{A}, \TNaCle{Z}, \TNaCle{M} \ldots and the ladder.
Those functions are proven to provide the same results as the ones in
\texttt{Mid/}, however their implementation are closer to \texttt{C} in order
facilitate the proof of equivalence with TweetNaCl code.
Here the reader will find four folders.
\item \textbf{\texttt{c}} contains the C Verifiable implementation of TweetNaCl.
\texttt{clightgen} will generate the appropriate translation into CLight.
\item \textbf{\texttt{init}} contains basic lemmas and memory manipulation
shortcuts to handle the aliasing cases.
\item \textbf{\texttt{spec}} contains the Hoare triple definitions of each
functions used in \TNaCle{crypto_scalarmult}.
\item \textbf{\texttt{proofs}} contains the proofs of the Hoare triple and
thus the proof that TweetNaCl code is sound and correct.
......@@ -70,7 +70,7 @@
> FOR(i,31) t[i]= 0;
> FOR(i,16) {
@@ introduce an auxiliary variable to
@@ simplify verification.
@@ simplify verification (loop invariants).
> aux = a[i];
> FOR(j,16) t[i+j]+=aux*b[j];
> }
......@@ -68,6 +68,7 @@ The Netherlands}
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