Add proof

1 files changed, 23 insertions, 3 deletions

diff --git a/proof.tex b/proof.tex
index aaac99c..91e980b 100644
--- a/proof.tex
+++ b/proof.tex
@@ -109,8 +109,6 @@ We can now define the simulation diagram for the translation. The 3AC state can
 
 \subsection{Forward simulation of RAM insertion}\label{sec:proof:ram_insertion}
 
-HTL can only represent a single state machine, it is therefore necessary to model the RAM abstractly to reason about the correctness of replacing the direct read and writes to the array to load and stores to a RAM.  The abstract specification used for the RAM is shown in Figure~\ref{fig_htl_ram_spec}, which defines how the RAM $r$ will behave with all the possible combinations of the input signals.
-
 \begin{figure}
   \centering
   \begin{minipage}{1.0\linewidth}
@@ -125,7 +123,29 @@ HTL can only represent a single state machine, it is therefore necessary to mode
   \caption{Specification for the memory implementation in HTL, where $r$ is the RAM, which is then implemented by equivalent Verilog code.}\label{fig:htl_ram_spec}
 \end{figure}
 
-This memory template can be represented using the following semantics shown in Figure~\ref{fig:htl_ram_spec}, which is then translated to the equivalent Verilog implementation shown in Figure~\ref{fig:verilog_ram_impl}.
+HTL can only represent a single state machine, it is therefore necessary to model the RAM abstractly to reason about the correctness of replacing the direct read and writes to the array by loads and stores to a RAM.  The specification used to model the RAM is shown in Figure~\ref{fig:htl_ram_spec}, which defines how the RAM $r$ will behave for all the possible combinations of the input signals.
+
+\subsubsection{From implementation to specification}
+
+The first step in proving the simulation correct is to build a specification of the algorithm.  The three possibilities of the transformation is that for each Verilog statement in the map at location $i$, either the statement is a load or a store, in which case it is translated to the equivalent signal representation, otherwise it is not changed.  An example of the specification for the store instruction is shown below, where $\sigma$ is state register, $r$ is the RAM, $d$ and $c$ are the input data-path and control logic maps and $i$ is the current state.  $n$ is the newly inserted state which only applies to the translation of loads.
+
+\begin{gather*}
+  \inferrule[Store Spec]{ d[i] = (r.mem\texttt{[}e_{1}\texttt{]} \texttt{ <= } e_{2}) \\ t = (r.u\_en \texttt{ <= } \neg r.u\_en; r.wr\_en \texttt{ <= } 1; r.d\_in \texttt{ <= } e_{2}; r.addr \texttt{ <= } e_{1})}%
+  {\yhfunction{spec\_ram}\ \ \sigma\ r\ d\ c\ \ d[i \mapsto t]\ \ c\ i\ n}
+\end{gather*}
+
+A similar specification is created for the load.  We then also prove that the implementation of the translation proves that the specification holds.
+
+\subsubsection{From specification to simulation}
+
+Another simulation proof is performed to prove that the insertion of the RAM is semantics preserving.  As in the simulation proof shown in Lemma~\ref{lemma:simulation_diagram}, some invariants need to be defined, which always hold at the start of the simulation and at the end of the simulation.  The invariants needed for the simulation of the RAM insertion are quite different to the previous invariants, so we can define these invariants $\mathcal{I}_{r}$ to be the following:
+
+\begin{itemize}
+  \item The association map for arrays $\Gamma_{a}$ always needs to have the same arrays present, and these arrays should never change in size.
+  \item The RAM should always be disabled at the start of the simulation, and at the end of the simulation step.  This is the reason for why the self-disabling RAM was needed.
+\end{itemize}
+
+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.
 
 \subsection{Forward simulation from HTL to Verilog}\label{sec:proof:htl_verilog}