\section{Proof}

This section describes the main correctness theorem that was proven and the main ideas behind the proofs.

The main correctness theorem states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has correct observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$.  The following theorem describes this property.

\begin{equation*}
  \forall C, V, B \notin \texttt{Wrong},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land C \Downarrow B \implies V \Downarrow_{s} B.
\end{equation*}

However, this forward simulation might still allow for wrong behaviour of the target code in cases where there are multiple possible behaviours in the target language.  This means that there may be cases where it executes correctly, however, there may also be other behaviours that are also valid.  However, if the target language is deterministic, meaning there is only one possible behaviour for all possible states, then this implies that the backwards simulation also holds.

To prove this statement, we therefore have to prove that the Verilog semantics are deterministic and that the forward simulation between the C and the Verilog holds as well.

\subsection{Forward Simulation}

The forward simulation between C and Verilog can be separated into proofs by forward simulation of each compiler pass

\subsection{Coq Mechanisation}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: