Commit e6f3cab8 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more play with spacing + for loops are back

parent a83ec5b2
......@@ -186,40 +186,40 @@ is enough for our needs.
% This is not the case here: you compute idx 255 before 254...
% Can we shorten the next paragraph?
% \subheading{Verifying \texttt{for} loops.}
% Final states of \texttt{for} loops are usually computed by simple recursive functions.
% However, we must define invariants which are true for each iteration step.
%
% Assume that we want to prove a decreasing loop where indexes go from 3 to 0.
% Define a function $g : \N \rightarrow State \rightarrow State $ which takes as
% input an integer for the index and a state, then returns a state.
% It simulates the body of the \texttt{for} loop.
% Define the recursion: $f : \N \rightarrow State \rightarrow State $ which
% iteratively applies $g$ with decreasing index:
% \begin{equation*}
% f ( i , s ) =
% \begin{cases}
% s & \text{if } s = 0 \\
% f( i - 1 , g ( i - 1 , s )) & \text{otherwise}
% \end{cases}
% \end{equation*}
% Then we have:
% \begin{align*}
% f(4,s) &= g(0,g(1,g(2,g(3,s))))
% \end{align*}
% To prove the correctness of $f(4,s)$, we need to prove that intermediate steps
% $g(3,s)$; $g(2,g(3,s))$; $g(1,g(2,g(3,s)))$; $g(0,g(1,g(2,g(3,s))))$ are correct.
% Due to the computation order of recursive function, our loop invariant for
% $i\in\{0,1,2,3,4\}$ cannot use $f(i)$.
% To solve this, we define an auxiliary function with an accumulator such that
% given $i\in\{0,1,2,3,4\}$, it will compute the first $i$ steps of the loop.
%
% We then prove for the complete number of steps, the function with the accumulator
% and without returns the same result.
% We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
%
% Using this formalization, we prove that the 255 steps of the Montgomery ladder
% in C provide the same computations as in \coqe{RFC}.
\subheading{Verifying \texttt{for} loops.}
Final states of \texttt{for} loops are usually computed by simple recursive functions.
However, we must define invariants which are true for each iteration step.
Assume that we want to prove a decreasing loop where indexes go from 3 to 0.
Define a function $g : \N \rightarrow State \rightarrow State $ which takes as
input an integer for the index and a state, then returns a state.
It simulates the body of the \texttt{for} loop.
Define the recursion: $f : \N \rightarrow State \rightarrow State $ which
iteratively applies $g$ with decreasing index:
\begin{equation*}
f ( i , s ) =
\begin{cases}
s & \text{if } s = 0 \\
f( i - 1 , g ( i - 1 , s )) & \text{otherwise}
\end{cases}
\end{equation*}
Then we have:
\begin{align*}
f(4,s) &= g(0,g(1,g(2,g(3,s))))
\end{align*}
To prove the correctness of $f(4,s)$, we need to prove that intermediate steps
$g(3,s)$; $g(2,g(3,s))$; $g(1,g(2,g(3,s)))$; $g(0,g(1,g(2,g(3,s))))$ are correct.
Due to the computation order of recursive function, our loop invariant for
$i\in\{0,1,2,3,4\}$ cannot use $f(i)$.
To solve this, we define an auxiliary function with an accumulator such that
given $i\in\{0,1,2,3,4\}$, it will compute the first $i$ steps of the loop.
We then prove for the complete number of steps, the function with the accumulator
and without returns the same result.
We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
Using this formalization, we prove that the 255 steps of the Montgomery ladder
in C provide the same computations as in \coqe{RFC}.
% %
......
......@@ -29,7 +29,7 @@ Lemma f_ext: forall (A B:Type),
% 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.
When compiling with CompCert we only need to trust CompCert's {assembly} semantics, because it 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.
......@@ -52,7 +52,9 @@ o[i] = aux1 + aux2;
factors out function calls and assignments from inside subexpressions.
The changes required for C code to make it verifiable are now minimal.
\item Last but not the least, we must trust the \textbf{Coq kernel} and its
\item Finally,
% Last but not the least,
we must trust the \textbf{Coq kernel} and its
associated libraries; the \textbf{Ocaml compiler} on which we compiled Coq;
the \textbf{Ocaml Runtime} and the \textbf{CPU}. Those are common to all proofs
done with this architecture \cite{2015-Appel,coq-faq}.
......
......@@ -38,7 +38,7 @@
{\color{red} \bf TODO: #1}
}
\newenvironment{informaltheorem}{\bigskip\itshape\noindent}{\bigskip}
\newenvironment{informaltheorem}{\medskip\itshape\noindent}{\medskip}
......@@ -381,8 +381,8 @@ literate=
keywordstyle=[4]\color{doc@lstfunctions},
keywordstyle=[5]\color{doc@lstnumbers},
%
aboveskip=6pt,
belowskip=6pt,
aboveskip=5pt,
belowskip=5pt,
extendedchars=true,
inputencoding=utf8,
upquote=true, %
......
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