Commit 34254bcc authored by Freek Wiedijk's avatar Freek Wiedijk
Browse files

some more small changes

parent 14db2cb4
......@@ -273,9 +273,9 @@ with their respective formula (\lref{lemma:xADD} and \lref{lemma:xDBL}),
we define a ladder \coqe{opt_montgomery} (in which $\K$ has not been fixed yet),
similar to the one used in
TweetNaCl.
(This definition is closely related to \coqe{montgomery_rec} that was used
This definition is closely related to \coqe{montgomery_rec} that was used
in the definition of \coqe{RFC}, and is easily proved to correspond to it.
In Coq this correspondence proof is hidden in the proof of \coqe{RFC_Correct} shown above.)
In Coq this correspondence proof is hidden in the proof of \coqe{RFC_Correct} shown above.
%\ref to the def of montgomery_rec? relevant lemma(s) that show(s) these are "the same"?
We prove its correctness for any point whose \xcoord is not 0.
......@@ -465,7 +465,7 @@ Theorem x_is_on_curve_or_twist:
\subsubsection{Curve25519 over \F{p^2}}
The quadratic extension $\F{p^2}$ is defined as $\F{p}[\sqrt{2}]$ by~\cite{Ber06}.
The theory of finite fields already had been formalized in the Mathematical Components
The theory of finite fields already has been formalized in the Mathematical Components
library,
%ref?
but this formalization is rather abstract, and we need concrete representations of field
......
......@@ -25,11 +25,14 @@ 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 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.
\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 only need to trust CompCert's {assembly} semantics, because CompCert has been formally proven correct.
However, when compiling with other C compilers like Clang or GCC, we need to trust that the CompCert's Clight semantics matches 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.
......
Markdown is supported
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