Fix capitalisation of titles

1 files changed, 7 insertions, 7 deletions

diff --git a/proof.tex b/proof.tex
index 7d142d9..0d6d4b1 100644
--- a/proof.tex
+++ b/proof.tex
@@ -2,7 +2,7 @@
 
 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 full Coq proof is available in auxiliary material.
 
-\subsection{Main challenges in the proof}
+\subsection{Main Challenges in the Proof}
 
 The proof of correctness of the Verilog back end is quite different from the usual proofs performed in CompCert, mainly because of the difference in Verilog semantics compared to the standard CompCert intermediate languages and because of the translation of the memory model.
 
@@ -16,7 +16,7 @@ The proof of correctness of the Verilog back end is quite different from the usu
 Together, these differences mean that translating 3AC directly to Verilog is infeasible, as the differences in the semantics are too large.  Instead, HTL, which was introduced in Section~\ref{sec:design}, bridges the gap in the semantics between the two languages.  HTL still consists of maps, like many of the other CompCert languages, however, each state corresponds to a Verilog statement.
 %\JW{This is good text, but the problem is that it reads like you're introducing HTL here for the first time. In fact, the reader has already encountered HTL in Section 2. So this needs acknowledging.}\YH{Added that.}
 
-\subsection{Formulating the correctness theorem}
+\subsection{Formulating the Correctness Theorem}
 
 The main correctness theorem is analogous to that stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil}: for all Clight source programs $C$, if the translation to the target Verilog code succeeds, and $C$ has safe observable behaviour $B$ when executed, then the target Verilog code will have the same behaviour $B$. Here, a `safe' execution is one that either converges or diverges, but does not `go wrong'. If the program does admit some wrong behaviour (such as undefined behaviour in C), the correctness theorem does not apply. A behaviour, then, is either a final state (in the case of convergence) or divergence. In \compcert{}, a behaviour is also associated with a trace of I/O events, but since external function calls are not supported in \vericert{}, this trace will always be empty.  
 
@@ -40,7 +40,7 @@ How can we prove this theorem? First, note that the theorem is a `backwards simu
 To prove this forward simulation, it suffices to prove forward simulations between each pair of consecutive intermediate languages, as these results can be composed to prove the correctness of the whole HLS tool. 
 The forward simulation from 3AC to HTL is stated in Lemma~\ref{lemma:htl} (Section~\ref{sec:proof:3ac_htl}), the forward simulation for the RAM insertion is shown in Lemma~\ref{lemma:htl_ram} (Section~\ref{sec:proof:ram_insertion}), then the forward simulation between HTL and Verilog is shown in Lemma~\ref{lemma:verilog} (Section~\ref{sec:proof:htl_verilog}) and finally, the proof that Verilog is deterministic is given in Lemma~\ref{lemma:deterministic} (Section~\ref{sec:proof:deterministic}).
 
-\subsection{Forward simulation from 3AC to HTL}\label{sec:proof:3ac_htl}
+\subsection{Forward Simulation from 3AC to HTL}\label{sec:proof:3ac_htl}
 
 As HTL is quite far removed from 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.  Lemma~\ref{lemma:htl} shows the result that needs to be proven in this subsection.
 
@@ -127,7 +127,7 @@ We can now define the simulation diagram for the translation. The 3AC state can
   This simulation diagram is proven by induction over the operational semantics of 3AC, which allows us to find one or more steps in the HTL semantics that will produce the same final matching state.
 \end{proof}
 
-\subsection{Forward simulation of RAM insertion}\label{sec:proof:ram_insertion}
+\subsection{Forward Simulation of RAM Insertion}\label{sec:proof:ram_insertion}
 
 \begin{figure}
   \centering
@@ -145,7 +145,7 @@ We can now define the simulation diagram for the translation. The 3AC state can
 
 HTL can only represent a single state machine, it is therefore necessary to model the RAM abstractly to reason about the correctness of replacing the direct read and writes to the array by loads and stores to a RAM.  The specification used to model the RAM is shown in Figure~\ref{fig:htl_ram_spec}, which defines how the RAM $r$ will behave for all the possible combinations of the input signals.
 
-\subsubsection{From implementation to specification}
+\subsubsection{From Implementation to Specification}
 
 The first step in proving the simulation correct is to build a specification of the algorithm.  The three possibilities of the transformation is that for each Verilog statement in the map at location $i$, either the statement is a load or a store, in which case it is translated to the equivalent signal representation, otherwise it is not changed.  An example of the specification for the store instruction is shown below, where $\sigma$ is state register, $r$ is the RAM, $d$ and $c$ are the input data-path and control logic maps and $i$ is the current state.  $n$ is the newly inserted state which only applies to the translation of loads.
 
@@ -156,7 +156,7 @@ The first step in proving the simulation correct is to build a specification of
 
 A similar specification is created for the load.  We then also prove that the implementation of the translation proves that the specification holds.
 
-\subsubsection{From specification to simulation}
+\subsubsection{From Specification to Simulation}
 
 Another simulation proof is performed to prove that the insertion of the RAM is semantics preserving.  As in the simulation proof shown in Lemma~\ref{lemma:simulation_diagram}, some invariants need to be defined, which always hold at the start of the simulation and at the end of the simulation.  The invariants needed for the simulation of the RAM insertion are quite different to the previous invariants, so we can define these invariants $\mathcal{I}_{r}$ to be the following:
 
@@ -175,7 +175,7 @@ The other invariants and assumptions for defining two matching states in HTL are
   \end{align*}
 \end{lemma}
 
-\subsection{Forward simulation from HTL to Verilog}\label{sec:proof:htl_verilog}
+\subsection{Forward Simulation from HTL to Verilog}\label{sec:proof:htl_verilog}
 
 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.  The proof is more involved, as the semantics of a map structure are quite different to the semantics of the case-statement they are converted to.