Modify proof section

1 files changed, 25 insertions, 19 deletions

diff --git a/proof.tex b/proof.tex
index 73052c0..22516f7 100644
--- a/proof.tex
+++ b/proof.tex
@@ -2,19 +2,29 @@
 
 Now that the Verilog semantics have been adapted to the CompCert model, we are in a position to formally prove the correctness of our C to Verilog compilation.  This section describes the main correctness theorem that was proven and the main ideas behind the proof.
 
-The main correctness theorem is the exact same correctness theorem as stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil} which states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has correct observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$, where behaviour can either be convergent, divergent or ``going wrong'' and is associated with a trace $t$ of any external function calls.  The following backwards simulation theorem describes this property, where $\Downarrow_{s}$ and $\Downarrow$ stand for simulation and execution respectively.
+The main correctness theorem is the exact same correctness theorem as stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil} which states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has safe observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$, meaning execution should either converge or diverge, but should not ``go wrong''.  Behaviour is also associated with a trace $t$ of any I/O events, however, as external function calls are not supported, this trace $t$ will always be empty for programs passing through \vericert{}.  The following backwards simulation theorem describes the correctness theorem, where $\Downarrow_{s}$ and $\Downarrow$ stand for simulation and execution respectively.
 
 \begin{theorem}
   Assuming that the translation from $C$ to Verilog $V$ succeeds, then if $V$ has behaviour $B$, $C$ should have the same behaviour $B$.
 
   \begin{equation*}
-    \forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow_{s} B \implies C \Downarrow B.
+    \forall C, V, B \in \texttt{Safe},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow_{s} B \implies C \Downarrow B.
   \end{equation*}
 \end{theorem}
 
-To prove this top-level theorem, we first have to build a specification of the translation algorith, with the properties that are needed to prove the simulation correct, which is described in Section~\ref{sec:proof:specification}. Next, a forward simulation has to be proven between the semantics of 3AC and HTL, and then between HTL and Verilog, which then implies that the forward simulation holds between C and Verilog.  Then, to prove the backward simulation, it suffices to show that the Verilog semantics are deterministic, which implies that there is only one possible behaviour for the Verilog output, and that it therefore also has to imply that $C$ has the same behaviour.
+\begin{proof}
+  The first observation that should be made is that instead of proving the backwards simulation, we can prove the forwards simulation, followed by a proof that the target semantics of the translation, which in our case is Verilog, is deterministic.  This means that there is only one possible behaviour $B$ for $V$, and that therefore the backwards simulation holds as well.
 
-\subsection{Specification}\label{sec:proof:specification}
+  The second observation that needs to be made is that to prove the forward simulation, it suffices to prove the forward simulations between each intermediate language, as they can be composed to prove the correctness of the whole HLS tool.
+
+  The forward simulation between 3AC and HTL is proven in Lemma~\ref{lemma:htl}, next the forward simulation between HTL and Verilog is shown in Lemma~\ref{lemma:verilog} and finally, the proof that Verilog is deterministic is given in Lemma~\ref{lemma:deterministic}.
+\end{proof}
+
+\subsection{Forward simulation between 3AC and HTL}\label{sec:proof:specification}
+
+As HTL is quite different to 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step.  In addition to that, the semantics of HTL are also quite different to the 3AC semantics, as instead of defining small-step semantics for each construct in Verilog, the semantics are instead defined over one clock cycle and mirror the semantics defined for Verilog.
+
+\subsubsection{Specification}
 
 To simplify the proof, instead of using the translation algorithm as an assumption, as was done in the backward simulation stated above, a specification of the translation can be constructed instead which contains all the properties that are needed to prove the correctness.  For example, for the translation from 3AC to HTL, the function implementing the translation from 3AC instructions to HTL Verilog statements is defined using the following function:
 
@@ -40,21 +50,15 @@ However, instead we can define a specification for the translation of instructio
 
 This specification can be built for the whole translation algorithm, until a specification of a function translation is obtained, which can then be used instead of the implementation if the following Theorem can be proven.
 
-\begin{theorem}
+\begin{lemma}\label{lemma:specification}
   If a 3AC function $c$ is translated correctly to a module $h$, then the specification of the translation should hold.
 
   \begin{equation*}
     \forall\ c\ h,\ \yhfunction{tr\_function} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_function}\ c\ h.
   \end{equation*}
-\end{theorem}
-
-\subsection{Forward Simulation}
+\end{lemma}
 
-The forward simulation between C and Verilog can be separated into forward simulations of each compiler pass, which can then be composed to provide a whole proof from C to Verilog.  Therefore, only the forward simulations from 3AC to HTL and from the HTL to Verilog need to be proven correct.
-
-\subsubsection{3AC to HTL forward simulation}
-
-As HTL is quite different to 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step.  In addition to that, the semantics of HTL are also quite different to the 3AC semantics, as instead of defining small-step semantics for each construct in Verilog, the semantics are instead defined over one clock cycle and mirror the semantics defined for Verilog.
+\subsubsection{Forward simulation}
 
 The first step in proving the forward simulation is to define a relation that matches an 3AC state to an HTL state, which shows when the states are equivalent.  This relation also defines assumptions that are made about the 3AC code that we receive, so that these assumptions can be used to prove the translations correct.  These assumptions then have to be proven to always hold assuming the HTL code was created by the translation algorithm.  Some of these assertions that need to be made about the 3AC and HTL code for a state to match are:
 
@@ -83,7 +87,7 @@ This \texttt{match\_states} predicate that is used to match the states of the 3A
 
 Using the \texttt{match\_states}, we can then define the forward simulation for the translation, shown as a simulation diagram below, where the 3AC state can be represented by $(R,M,\textit{pc})$, $R$ being the map of values for all current registers, $M$ being the current state of memory and \textit{pc} being the current program counter.  The state of HTL can also be represented by $\Gamma$, which can be split into $\Gamma_{r}$ for the current state of all registers in the module, and $\Gamma_{a}$, for the state of all arrays in the Verilog module, which represents the stack.  Finally, $\mathcal{I}$ stands for the other invariants that need to hold in the \texttt{match\_states} predicate:
 
-\begin{theorem}
+\begin{lemma}\label{lemma:simulation_diagram}
   Given the 3AC state $(R,M,\textit{pc})$ and the matching HTL state $(\Gamma_{r}, \Gamma_{a})$, assuming one step in the 3AC semantics  produces state $(R',M',\textit{pc}')$, there exists one or more steps in the HTL semantics that result in matching states $(\Gamma_{r}', \Gamma_{a}')$.
   \begin{center}
     \begin{tikzpicture}
@@ -100,11 +104,11 @@ Using the \texttt{match\_states}, we can then define the forward simulation for
       \end{scope}
     \end{tikzpicture}
   \end{center}
-\end{theorem}
+\end{lemma}
 
 \noindent where $\le$ means ``less defined'', meaning all locations in $R$ or $M$ need to be equal to $\Gamma_{r}$ and $\Gamma_{a}$ except in the cases where the values in memory are undefined.  The \texttt{match\_states} predicate can be shortened to the statement that $R$ needs to be ``less defined'' than $\Gamma_{r}$, $M$ needs to be ``less defined'' than $\Gamma_{a}$ and finally the program counter \textit{pc} needs to equal to the current value of the state register $\sigma$.
 
-\subsubsection{HTL to Verilog forward simulation}
+\subsection{HTL to Verilog forward simulation}
 
 The HTL to Verilog simulation is conceptually simple, as the only transformation is from the map representation of the code to the case statement representation.  As the representations are quite different though, to prove that they are equivalent the following observations have to be made.
 
@@ -116,15 +120,17 @@ Another problem with the representation of the state as an actual register is th
 
 Finally, to prove the backward simulation given the forward simulation, it has to be shown that if we generate hardware with a specific behaviour, that it is the only possible program with that behaviour.  This only has to be performed for the final intermediate language, which is Verilog, so that the backward simulation holds for the whole chain from Clight to Verilog.
 
-\begin{theorem}
+\begin{lemma}\label{lemma:deterministic}
   Semantics are deterministic if it can be shown that two behaviours $B_{1}$ and $B_{2}$ for the same program implies that the behaviours are the same.
 
   \begin{equation*}
     C \Downarrow B_{1} \land C \Downarrow B_{2} \implies B_{1} = B_{2}.
   \end{equation*}
-\end{theorem}
+\end{lemma}
 
-The Verilog semantics that are used are deterministic, as the order of operation of all the constructs is defined, and there is therefore only one way to evaluate the module and only one possible behaviour.  This was proven correct for the small-step semantics shown in Figure~\ref{fig:inferrence_module}.
+\begin{proof}
+  The Verilog semantics that are used are deterministic, as the order of operation of all the constructs is defined, and there is therefore only one way to evaluate the module and only one possible behaviour.  This was proven correct for the small-step semantics shown in Figure~\ref{fig:inferrence_module}.
+\end{proof}
 
 %\subsection{Coq Mechanisation}