\newpage
\appendix

\section{Appendix}

\begin{figure*}
  \centering
  \begin{minipage}{1.0\linewidth}
    \begin{align*}
      v\quad ::=&\; 32 \yhkeyword{'d} n\\
      \textit{op}\quad ::=&\; \yhkeyword{+ } | \yhkeywordsp{- } | \yhkeywordsp{* } \cdots \\
      e\quad ::=&\; v\;\; |\;\; x\;\; |\;\; e \yhkeyword{[} e \yhkeyword{]}\;\; |\;\; e\ \mathit{op}\ e\;\; |\;\; \yhkeyword{\textasciitilde} e\;\; |\;\; e \yhkeywordsp{? } e \yhkeywordsp{: } e\\
      s\quad ::=&\; s\ s\ |\ \epsilon\\[-2pt]
      |&\; \yhkeyword{if(} e \yhkeyword{) } s \yhkeywordsp{else } s\\[-2pt]
      |&\; \yhkeyword{case(} e \yhkeyword{) } e : s\ \{\ e : s\ \}\ [\ s\ ] \yhkeywordsp{endcase}\\[-2pt]
      |&\; e = e \yhkeyword{;}\\[-2pt]
      |&\; e \Leftarrow e \yhkeyword{;}\\
      d\quad ::=&\; \yhkeyword{[n-1:0] } r\ |\ \yhkeyword{[n-1:0] } r \yhkeywordsp{[m-1:0]}\\
      m\quad ::=&\; \yhkeyword{reg } d \yhkeyword{;}\ |\ \yhkeyword{input wire } d \yhkeyword{;}\ |\ \yhkeyword{output reg } d \yhkeyword{;}\\
      |&\; \yhkeywordsp{always @(posedge clk) } s \\
      m \text{ list}\quad ::=&\; \{ m \}
    \end{align*}
  \end{minipage}
  \caption{Verilog syntax for values $v$, expressions $e$, statements $s$ and module items $m$.}\label{fig:verilog_syntax}
\end{figure*}

\begin{figure*}
  \centering
  \begin{minipage}{1.0\linewidth}
    \begin{gather*}
      \label{eq:1}
      \inferrule[Skip]{ }{\textit{srun}\ \sigma\ \epsilon\ \sigma}\\
      %
      \inferrule[Seq]{\textit{srun}\ \sigma_{0}\ \textit{s}_{1}\ \sigma_{1} \\ \textit{srun}\ \sigma_{1}\ \textit{s}_{2}\ \sigma_{2}}{\textit{srun}\ \sigma_{0}\ (\textit{s}_{1}\ \textit{s}_{2})\ \sigma_{2}}\\
      %
      \inferrule[CondTrue]{\textit{erun}\ \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ c\ v_{c} \\ \yhfunction{valToB}\ v_{c} = \yhconstant{true} \\ \textit{srun}\ \sigma_{0}\ \textit{st}\ \sigma_{1}}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{if(} c \yhkeyword{) } \textit{st} \yhkeywordsp{else } \textit{sf})\ \sigma_{1}}\\
      %
      \inferrule[CondFalse]{\textit{erun}\ \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ c\ v_{\rm c} \\ \yhfunction{valToB}\ v_{\rm c} = \yhconstant{false} \\ \textit{srun}\ \sigma_{0}\ \textit{sf}\ \sigma_{1}}{\textit{srun}\ \sigma_{0}\ (\yhkeyword{if(} c \yhkeyword{) } \textit{st} \yhkeywordsp{else } \textit{sf})\ \sigma_{1}}\\
      %
      \inferrule[CaseNoMatch]{\textit{srun}\ \sigma_{0}\ (\yhkeyword{case(} e \yhkeyword{) } cs\ \textit{def} \yhkeywordsp{endcase})\ \sigma_{1} \\ \textit{erun}\  \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ me\ mve \\ \textit{erun}\  \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ e\ ve \\ mve \neq ve}{\textit{srun}\  \sigma_{0}\ (\yhkeyword{case(} e \yhkeyword{) } ((me : sc) :: cs)\ \textit{def} \yhkeywordsp{endcase})\ \sigma_{1}}\\
      %
      \inferrule[CaseMatch]{\textit{srun}\  \sigma_{0}\ sc\ \sigma_{1} \\ \textit{erun}\  \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ e\ ve \\ \textit{erun}\  \Gamma_{\rm r}^{0}\ \Gamma_{\rm a}^{0}\ me\ mve \\ mve = ve}{\textit{srun}\  \sigma_{0}\ (\yhkeyword{case(} e \yhkeyword{) } ((me : sc) :: cs)\ \textit{def} \yhkeywordsp{endcase})\ \sigma_{1}}\\
      %
      \inferrule[CaseDefault]{\textit{srun}\  \sigma_{0}\ s\ \sigma_{1}}{\textit{srun}\  \sigma_{0}\ (\yhkeyword{case(} e \yhkeyword{) } []\ (\yhconstant{Some}\ s) \yhkeywordsp{endcase})\ \sigma_{1}}\\
      %
      \inferrule[Blocking Reg]{\yhfunction{name}\ \textit{lhs} = \yhconstant{OK}\ n \\ \textit{erun}\  \Gamma_{\rm r}\ \Gamma_{\rm a}\ \textit{rhs}\ v_{\rm rhs}}{\textit{srun}\  (\Gamma_{\rm r},\Gamma_{\rm a},\Delta_{\rm r},\Delta_{\rm a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{\rm r} [n \mapsto v_{\rm rhs}], \Gamma_{\rm a}, \Delta_{\rm r}, \Delta_{\rm a})}\\
      %
      \inferrule[Nonblocking Reg]{\yhfunction{name}\ \textit{lhs} = \yhconstant{OK}\ n \\ \textit{erun}\  \Gamma_{\rm r}\ \Gamma_{\rm a}\ \textit{rhs}\ v_{\rm rhs}}{\textit{srun}\  (\Gamma_{\rm r}, \Gamma_{\rm a}, \Delta_{\rm r}, \Delta_{\rm a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{\rm r}, \Gamma_{\rm a}, \Delta_{\rm r} [n \mapsto v_{\rm rhs}], \Delta_{\rm a})}\\
      \inferrule[Blocking Array]{\yhkeyword{name}\ \textit{lhs} = \yhkeyword{OK}\ n \\ \textit{erun}\  \Gamma_{r}\ \Gamma_{a}\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r},\Gamma_{a},\Delta_{r},\Delta_{a})\ (\textit{lhs} = \textit{rhs})\ (\Gamma_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Gamma_{a}, \Delta_{r}, \Delta_{a})}\\
      %
      \inferrule[Nonblocking Array]{\yhkeyword{name}\ \textit{lhs} = \yhkeyword{OK}\ n \\ \textit{erun}\  \Gamma\ \textit{rhs}\ v_{\textit{rhs}}}{\textit{srun}\  (\Gamma_{r}, \Gamma_{a}, \Delta_{r}, \Delta_{a})\ (\textit{lhs} \Leftarrow \textit{rhs})\ (\Gamma_{r}, \Gamma_{a}, \Delta_{r} // \{n \rightarrow v_{\textit{rhs}}\}, \Delta_{a})}
    \end{gather*}
  \end{minipage}
  \caption{Inference rules for statements.}\label{fig:inference_statements}
\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"
%%% TeX-command-extra-options: "-shell-escape"
%%% End: