Commit 14db2cb4 authored by Freek Wiedijk's avatar Freek Wiedijk
Browse files

check -> Peter's suggestion

trust about CompCert
parent 7827a51b
......@@ -45,7 +45,7 @@ of an asymmetric cryptographic primitive.
In the last step we prove that the Coq implementation matches
the mathematical definition of X25519 as given in~\cite[Sec.~2]{Ber06}.
This gives a check that there are no transcription errors
This provides additional confidence that there are no transcription errors
in our formalized version of X25519.
We do this by extending the Coq library
for elliptic curves~\cite{BartziaS14} by Bartzia and Strub to
......
......@@ -25,14 +25,17 @@ Lemma f_ext: forall (A B:Type),
Princeton allows a user to prove that a Clight code matches pure Coq
specification.
\item \textbf{CompCert}. The formally proven compiler. We trust that the Clight
model captures correctly the C17 standard.
Our proof also assumes that the TweetNaCl code will behave as expected if
compiled under CompCert.
\item \textbf{CompCert}. The formally proven compiler. We trust that the CompCert Clight semantics in Coq
correctly captures the C17 standard.
When compiling with CompCert we actually only need to trust CompCert's \emph{assembly} semantics, because CompCert compilation has been proved correct.
But when compiling with a generic C compiler like Clang or GCC, we need to trust the Clight semantics to match the C17 standard, as well as
that the compiler will compile the TweetNaCl code according to that standard.
% Our proof also assumes that the TweetNaCl code will behave as expected if
% compiled under CompCert.
% We do not provide guarantees for other C compilers such as Clang or GCC.
\item \textbf{\texttt{clightgen}}. The tool making the translation from \textbf{C} to
\textbf{Clight}. It is the first step of the compilation.
\item \textbf{\texttt{clightgen}}. The tool making the translation from {C} to
{Clight}. It is the first step of the compilation.
VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
This required us to rewrite the lines into:
\begin{lstlisting}[language=C]
......
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