Add more

1 files changed, 0 insertions, 36 deletions

diff --git a/proof.tex b/proof.tex
index a01b688..fcad541 100644
--- a/proof.tex
+++ b/proof.tex
@@ -25,42 +25,6 @@ The forward simulation between C and Verilog can be separated into forward simul
 
 As HTL is quite different to 3AC, this first translation is the most involved translation and therefore requires a larger proof, as the translation from 3AC instructions to Verilog statements needs to be proven correct.  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.
 
-\begin{figure}
-  \centering
-\begin{minted}{coq}
-Inductive match_states :
-  3AC.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp
-    sp' rs mem m st res
-    (MASSOC : match_assocmaps f rs asr)
-    (TF : tr_module f m)
-    (WF : state_st_wf m (HTL.State res m st asr asa))
-    (MF : match_frames sf res)
-    (MARR : match_arrs m f sp mem asa)
-    (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
-    (RSBP : reg_stack_based_pointers sp' rs)
-    (ASBP : arr_stack_based_pointers sp' mem
-              (f.(3AC.fn_stacksize)) sp)
-    (BOUNDS : stack_bounds sp (f.(3AC.fn_stacksize)) mem)
-    (CONST : match_constants m asr),
-    match_states
-      (3AC.State sf f sp st rs mem)
-      (HTL.State res m st asr asa)
-| match_returnstate : forall v v' stack mem res
-    (MF : match_frames stack res),
-    val_value_lessdef v v' ->
-    match_states
-      (3AC.Returnstate stack v mem)
-      (HTL.Returnstate res v')
-| match_initial_call :
-  forall f m m0 (TF : tr_module f m),
-    match_states
-      (3AC.Callstate nil (AST.Internal f) nil m0)
-      (HTL.Callstate nil m nil).
-\end{minted}
-  \caption{\texttt{match\_states} predicate used to match an 3AC state to the equivalent HTL state.}\label{fig:match_states}
-\end{figure}
-
 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.  The \texttt{match\_states} predicate that is used to match the states of the 3AC code to the HTL code is shown in Figure~\ref{fig:match_states}.  The type \texttt{match\_states} declared in Figure~\ref{fig:match_states} has three constructors.
 
 \begin{enumerate}