Add more

1 files changed, 36 insertions, 0 deletions

diff --git a/appendix.tex b/appendix.tex
index 1e3cdb3..39dd72d 100644
--- a/appendix.tex
+++ b/appendix.tex
@@ -70,6 +70,42 @@
   \label{fig:inferrence_module}
 \end{figure*}
 
+\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}
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "main"