More proof changes

1 files changed, 13 insertions, 1 deletions

diff --git a/proof.tex b/proof.tex
index 22516f7..9bfb1a7 100644
--- a/proof.tex
+++ b/proof.tex
@@ -22,7 +22,19 @@ The main correctness theorem is the exact same correctness theorem as stated in
 
 \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.
+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.  Lemma~\ref{lemma:htl} shows the theorem that needs to be proven in this section.
+
+\begin{lemma}\label{lemma:htl}
+  Forward simulation of the 3AC and HTL intermediate language, assuming that the translation from 3AC to HTL succeeded using \texttt{tr\_htl} for the translation.
+
+  \begin{equation*}
+    \forall c, h, B \in \texttt{Safe}, \yhfunction{tr\_htl} (c) = \yhconstant{OK} (h) \land c \Downarrow B \implies h \Downarrow B.
+  \end{equation*}
+\end{lemma}
+
+\begin{proof}
+  Follows by using a specification of the important properties $\yhfunction{tr\_htl}}$ has
+\end{proof}
 
 \subsubsection{Specification}