Add notes

1 files changed, 3 insertions, 4 deletions

diff --git a/proof.tex b/proof.tex
index 1de5a56..2d1a42f 100644
--- a/proof.tex
+++ b/proof.tex
@@ -1,8 +1,7 @@
 \section{Proof}
 \label{sec:proof}
 
-\NR{Now that we have adapted the Verilog semantics 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 proofs.
+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 proofs.
 
 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.
 
@@ -14,7 +13,7 @@ To prove this top-level theorem, a forward simulation has to be done between eac
 
 \subsection{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 translation might be defined using the following function: $\yhfunction{transl\_{3ac}} (c) = \yhconstant{OK} (h)$, where $c$ is the 3AC input code and $h$\NR{is the output HTL code?}.  However, instead we can define a relation \texttt{tr\_htl} between the 3AC and HTL code, which contains all the properties about the translation that are needed, without any of the implementation.  If the following can be proven, it can then be used instead of the translation algorithm when performing the proof of correctness.
+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 translation might be defined using the following function: $\yhfunction{transl\_3ac\_htl} (c) = \yhconstant{OK} (h)$, where $c$ is the 3AC input code and $h$ is the generated HTL code.  However, instead we can define a relation \texttt{tr\_3ac\_htl} between the 3AC and HTL code, which contains all the properties about the translation that are needed, without any of the implementation.  If the following can be proven, it can then be used instead of the translation algorithm when performing the proof of correctness.
 
 \begin{equation*}
   \forall\ c\ h,\ \yhfunction{transl\_3ac} (c) = \yhconstant{OK}(h) \implies \yhfunction{tr\_htl}\ c\ h.
@@ -99,7 +98,7 @@ 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.
 
-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}
+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}.
 
 %\subsection{Coq Mechanisation}