Update on Overleaf.

1 files changed, 4 insertions, 0 deletions

diff --git a/proof.tex b/proof.tex
index c68f841..fc15f42 100644
--- a/proof.tex
+++ b/proof.tex
@@ -22,6 +22,7 @@ The forward simulation between 3AC and HTL is stated in Lemma~\ref{lemma:htl} in
 
 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.
 
+\YH{Should this section state the lemma at the end maybe? With the proof complete?  Stating the forward simulation and specification first and then proving the top level lemma? Or is it better like this and I get rid of the proof of this  lemma?}
 \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.
 
@@ -106,10 +107,13 @@ We can then define the simulation diagram for the translation, where the 3AC sta
   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}
 
+\YH{Need to add explanation of proof of initial and final states, as these are needed to prove the full forward simulation as well}
+
 \subsection{HTL to Verilog forward simulation}\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.  As the representations are quite different though, 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.
 
+\YH{Maybe want to split this up into two lemmas?  One which states the proof about the map property of uniqueness of keys, and another proving the final theorem?}
 \begin{lemma}\label{lemma:verilog}
   The forward simulation for this translation assumes that the Verilog $V$ was obtained from the HTL to Verilog translation function $\yhfunction{tr\_verilog}$, note that the translation can not fail for this step.