Fix more

1 files changed, 7 insertions, 2 deletions

diff --git a/proof.tex b/proof.tex
index 5f7dc16..1a04fc7 100644
--- a/proof.tex
+++ b/proof.tex
@@ -18,7 +18,7 @@ The theorem is a `backwards simulation' result (from target to source), followin
 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. 
-The forward simulation from 3AC to HTL is stated in Lemma~\ref{lemma:htl} (Section~\ref{sec:proof:3ac_htl}), 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}).
+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}
 
@@ -147,8 +147,13 @@ 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}
+\begin{lemma}[Forward simulation from HTL to Verilog]\label{lemma:htl_ram}
+  Given an HTL program, the forward simulation relation should hold after inserting the RAM.
 
+  \begin{align*}
+    &\forall h, B \in \texttt{Safe}, \yhfunction{spec\_ram} (h) = h' \land h \Downarrow B \implies h' \Downarrow B.
+  \end{align*}
+\end{lemma}
 
 \subsection{Forward simulation from HTL to Verilog}\label{sec:proof:htl_verilog}