Add algorithm

1 files changed, 7 insertions, 3 deletions

diff --git a/proof.tex b/proof.tex
index 1284458..b458767 100644
--- a/proof.tex
+++ b/proof.tex
@@ -16,7 +16,7 @@ To prove this the first observation that should be made is that instead of provi
 
 The second observation that needs to be made is that to prove the forward simulation, it suffices to prove the forward simulations between each intermediate language, as they can be composed to prove the correctness of the whole HLS tool.
 
-The forward simulation between 3AC and HTL is proven in Lemma~\ref{lemma:htl}, next the forward simulation between HTL and Verilog is shown in Lemma~\ref{lemma:verilog} and finally, the proof that Verilog is deterministic is given in Lemma~\ref{lemma:deterministic}.
+The forward simulation between 3AC and HTL is stated in Lemma~\ref{lemma:htl} in Section~\ref{sec:proof:3ac_htl}, next the forward simulation between HTL and Verilog is shown in Lemma~\ref{lemma:verilog} in Section~\ref{sec:proof:htl_verilog} and finally, the proof that Verilog is deterministic is given in Lemma~\ref{lemma:deterministic} in Section~\ref{sec:proof:deterministic}.
 
 \subsection{Forward simulation between 3AC and HTL}\label{sec:proof:3ac_htl}
 
@@ -58,6 +58,10 @@ To simplify the proof, instead of using the translation algorithm as an assumpti
   \end{equation*}
 \end{lemma}
 
+\begin{proof}
+  Follows from the definition of the specification and therefore should match the implementation of the algorithm.
+\end{proof}
+
 \subsubsection{Forward simulation}
 
 The first step in proving the forward simulation is to define a relation that matches an 3AC state to an HTL state, which shows when the states are equivalent.  This relation also defines assumptions that are made about the 3AC code that we receive, so that these assumptions can be used to prove the translations correct.  These assumptions then have to be proven to always hold assuming the HTL code was created by the translation algorithm.  Some of these assertions that need to be made about the 3AC and HTL code for a state to match are:
@@ -102,7 +106,7 @@ 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}
 
-\subsection{HTL to Verilog forward simulation}
+\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.
 
@@ -121,7 +125,7 @@ The HTL to Verilog simulation is conceptually simple, as the only transformation
   Another problem with the representation of the state as an actual register is that we have to make sure that the state does not overflow.  Currently, the state register will always be 32 bits, meaning the maximum number of states can only be $2^{32} - 1$.  We therefore have to prove that the state value will never go over that value.  This means that during the translation we have to check for each state that it can fit into an integer.  Finally, as we have to assume that there are $2^{32} - 1$ states, \vericert{} will error out when there are more instructions to be translated, which allows us to satisfy and prove that assumption correct.
 \end{proof}
 
-\subsection{Deterministic Semantics}
+\subsection{Deterministic Semantics}\label{sec:proof:deterministic}
 
 Finally, to prove the backward simulation given the forward simulation, it has to be shown that if we generate hardware with a specific behaviour, that it is the only possible program with that behaviour.  This only has to be performed for the final intermediate language, which is Verilog, so that the backward simulation holds for the whole chain from Clight to Verilog.