AddFix more things

1 files changed, 5 insertions, 1 deletions

diff --git a/proof.tex b/proof.tex
index 39a39d2..bc1d95f 100644
--- a/proof.tex
+++ b/proof.tex
@@ -13,7 +13,8 @@ The main correctness theorem is analogous to that stated in \compcert{}~\cite{le
   \end{equation*}
 \end{theorem}
 
-The theorem is a `backwards simulation' result (from target to source). The theorem does not demand the `if' direction too, because compilers are permitted to resolve any non-determinism present in their source programs.
+The theorem is a `backwards simulation' result (from target to source), following the terminology used in the \compcert{} literature.  The theorem does not demand the `if' direction too, because compilers are permitted to resolve any non-determinism present in their source programs.
+
 In practice, Clight programs are all deterministic, as are the Verilog programs in the fragment we consider. This means that we can prove the correctness theorem above by first inverting it to become a forwards simulation result, following standard \compcert{} practice.
 
 The second observation that needs to be made is that to prove this forward simulation, it suffices to prove forward simulations between each intermediate language, as these results can be composed to prove the correctness of the whole HLS tool. 
@@ -146,6 +147,9 @@ Another simulation proof is performed to prove that the insertion of the RAM is
 
 The other invariants and assumptions for defining two matching states in HTL are quite similar to the simulation performed in Lemma~\ref{lemma:simulation_diagram}, such as ensuring that the states have the same value, and that the values in the registers are less-defined.  In particular, the less-defined relation matches up all the registers, except for the new registers introduced by the RAM.
 
+\begin{lemma}\label{lemma:simulation_diagram_ram}
+
+
 \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.