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

fix typos

parent f01fc3f8
......@@ -4,7 +4,7 @@
Any formal system relies on a trusted base. In this section we describe our
chain of trust.
\subsection{Trusted Core Base of the proof}
\subsection{Trusted Code Base of the proof}
Our proof relies on a trusted base, i.e. a foundation of specifications
and implementations that must stay correct with respect to their specifications.
......@@ -24,9 +24,9 @@ Lemma f_ext: forall (A B:Type),
\end{lstlisting}
\item \textbf{Verifiable Software Toolchain}. This framework developed at
Princeton allows a user to prove that a \texttt{CLight} code matches pure Coq
Princeton allows a user to prove that a Clight code matches pure Coq
specification. However one must trust the framework properly captures and
map the CLight behavior to the basic pure Coq functions.
map the Clight behavior to the basic pure Coq functions.
% At the beginning of the project we found inconsistency and reported them to the authors.
\item \textbf{CompCert}. The formally proven compiler. We trust that the Clight
......
......@@ -71,7 +71,7 @@ By instantiating $\K$ with $\Zfield$, and the parameters of Curve25519 ($a = 486
we define a mid-level specification.
Additionally we also provide a low-level specification close to the \texttt{C} code
(over lists of $\Z$). We show this specification to be equivalent to the
\textit{semantic version} of C (\texttt{CLight}) with VST.
\textit{semantic version} of C (Clight) with VST.
This low level specification gives us the soundness assurance.
By showing that operations over instances ($\K = \Zfield$, $\Z$, list of $\Z$) are
equivalent, we bridge the gap between the low level and the high level specification
......@@ -218,7 +218,7 @@ The location of the proof of this Hoare triple can be found in Appendix~\ref{app
% 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.
% 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
......@@ -410,7 +410,7 @@ Function pow_fn_rev (a:Z) (b:Z)
\end{lstlisting}
This \Coqe{Function} requires a proof of termination. It is done by proving the
well-foundedness of the decreasing argument: \Coqe{measure Z.to_nat a}. Calling
\Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as the \texttt{Clight} definition.
\Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as the Clight definition.
\begin{lstlisting}[language=Coq]
Definition Inv25519 (x:list Z) : list Z :=
pow_fn_rev 254 254 x x.
......
......@@ -350,7 +350,7 @@ memory shared such as being disjoint.
We discuss this limitation further in \sref{subsec:with-VST}.
The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework
which uses Separation logic to prove the functional correctness of C programs.
The first step consists of translating the source code into CLight,
The first step consists of translating the source code into Clight,
an intermediate representation used by CompCert.
For such purpose we use the parser CompCert: \texttt{clightgen}.
In second step we define the Hoare triple encapsulating the specification of the
......
......@@ -49,7 +49,7 @@ In this folder the reader will find multiple levels of implementation of X25519.
Here the reader will find four folders.
\begin{itemize}
\item \textbf{\texttt{c}} contains the C Verifiable implementation of TweetNaCl.
\texttt{clightgen} will generate the appropriate translation into CLight.
\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}} defines as Hoare triple the specification of the
......
......@@ -11,7 +11,7 @@
\draw (0.5,1) node [textstyle, anchor=west, draw=black, thick, minimum width=3cm,minimum height=0.5cm] (clight) {\texttt{tptr tlong}};
\draw (0,1) node [anchor=east] (clightdef) {\texttt{CLight}};
\draw (0,1) node [anchor=east] (clightdef) {Clight};
\draw [thick, ->] (longlong.north) -- (clight.south);
......
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