Add more to proof

1 files changed, 2 insertions, 4 deletions

diff --git a/proof.tex b/proof.tex
index 292c364..6cfbaaa 100644
--- a/proof.tex
+++ b/proof.tex
@@ -62,7 +62,7 @@ This \texttt{match\_states} predicate that is used to match the states of the 3A
   \item \texttt{match\_initial\_state} matches the initial call to the main function, and cannot be used for any other function calls, as the stack frame is assumed to be empty.
 \end{enumerate}
 
-Using the \texttt{match\_states}, we can then define the correctness theorem for the translation, shown as a simulation diagram below:
+Using the \texttt{match\_states}, we can then define the forward simulation for the translation, shown as a simulation diagram below, where the 3AC state can be represented by $(R,M,\textit{pc})$, $R$ being the map of values for all current registers, $M$ being the current state of memory and \textit{pc} being the current program counter.  The state of HTL can also be represented by $\Gamma$, which can be split into $\Gamma_{r}$ for the current state of all registers in the module, and $\Gamma_{a}$, for the state of all arrays in the Verilog module, which represents the stack:
 
 \begin{center}
   \begin{tikzpicture}
@@ -80,13 +80,11 @@ Using the \texttt{match\_states}, we can then define the correctness theorem for
   \end{tikzpicture}
 \end{center}
 
-$S_{1}$ and $S_{2}$ are 3AC states and $R_{1}$ and $R_{2}$, HTL states and $\xrightarrow{t}$ is one step in the semantics of 3AC and $\xrightarrow{t}_{+}$ is one or more steps in the semantics of HTL.\@  The correctness theorem then says that for all possible starting states $S_{1}$ and for the resulting state $S_{2}$ after one step in the semantics of 3AC, for all HTL states $R_{1}$ that matches the state $S_{1}$, there should exist a state $R_{2}$ such that $R_{2}$ is the result of the simulation of the HTL semantics and that the states $S_{2}$ and $R_{2}$ should match as well.  Using this property, the forward simulation can then be proven correct by also showing that the initial and final states of the simulation match as well.
-
 \subsubsection{HTL to Verilog forward simulation}
 
 The HTL to Verilog simulation is quite 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, to prove that they are equivalent the following observations have to be made.
 
-The translation from maps to case statements is done by turning each node of the tree into a case expression with the statments in each being the same.  The main difficulty for the proof is that a structure that can be directly accessed is transformed into an inductive structure where a certain number of constructors need to be called to get to the correct case.  The proof of the translation from maps to case statements follows by induction over the list of elements in the map and the fact that each key in this list will be unique.  In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list.  The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list.  The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't.  In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore.  In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match.
+The translation from maps to case statements is done by turning each node of the tree into a case expression with the statements in each being the same.  The main difficulty for the proof is that a structure that can be directly accessed is transformed into an inductive structure where a certain number of constructors need to be called to get to the correct case.  The proof of the translation from maps to case statements follows by induction over the list of elements in the map and the fact that each key in this list will be unique.  In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list.  The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list.  The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't.  In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore.  In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match.
 
 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.