\noindent where $\le$ means ``less defined'', meaning all locations in $R$ or $M$ need to be equal to $\Gamma_{r}$ and $\Gamma_{a}$ except in the cases where the values in memory are undefined.  The \texttt{match\_states} predicate can be shortened to the statement that $R$ needs to be ``less defined'' than $\Gamma_{r}$, $M$ needs to be ``less defined'' than $\Gamma_{a}$ and finally the program counter \textit{pc} needs to equal to the current value of the state register $\sigma$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

This \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}
  \item \texttt{match\_state} is the main constructor which matches an \texttt{3AC.State} to a \texttt{HTL.State}, which during the normal execution of instructions in the function.
  \item \texttt{match\_returnstate} is the constructor used to match return statements in 3AC to HTL.\@  Even though function calls are not supported, there still has to be a notion of stack frames during the proof, as at the start of the program a stack frame is allocated, which then has to be deallocated (popped from the stack) when the main function returns its result.\YH{Maybe can remove because it's already mentioned in the semantics}  The only condition on matching the return state is that the return values must be \emph{less defined} (either equal to, or if the C value is undefined any acceptable value is possible).
  \item \texttt{match\_initial\_state} matches the initial call to the main function, and cannot be used for any other function calls, as the stack frame is assumed to be empty.
\end{enumerate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

To simplify the proof, instead of using the translation algorithm as an assumption, as was done in Lemma~\ref{lemma:htl}, a specification of the translation can be constructed instead which contains all the properties that are needed to prove the correctness.  For example, for the translation from 3AC to HTL, the function implementing the translation from 3AC instructions to HTL Verilog statements is defined using the following function:

\begin{minted}{coq}
tr_instr : 3AC.instruction -> state -> res state
\end{minted}

\noindent where the type \texttt{res} can either be an \texttt{Error}, or an \texttt{OK} with the translated resulting \texttt{state}, and the \texttt{state} is a collection of various results that are needed to build the final HTL code, such as the current data path, control logic and name of registers.

However, instead we can define a specification for the translation of instructions by defining a relation \texttt{spec\_tr\_instr}, containing all the properties about the instruction translation that are needed, without any of the implementation details of the \texttt{tr\_instr} function, such as the exact structure of the \texttt{state} or order in which statements are added to the data path or the control logic.

\begin{equation*}
  \yhfunction{spec\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ i\ \textit{data }\ \textit{control}
\end{equation*}

\noindent The \textit{control} and \textit{data} parts of the specification are the statements that the current 3AC instruction $i$ should translate to. A more specific example of a rule describing the translation of an \texttt{Iop} operation in 3AC is the following:

\begin{equation*}
  \inferrule[Iop]{\yhfunction{tr\_op } \textit{op }\ \vec{a} = \yhconstant{OK } e}{\yhfunction{spec\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ (\yhconstant{Iop } \textit{op }\ \vec{a}\ d\ n)\ (d\ \yhkeyword{<=}\ e)\ (\sigma\ \yhkeyword{<=}\ n)}
\end{equation*}

\noindent This rule describes the specification of the translation by describing the nonblocking assignments that are added to the data path and control logic, assuming that the translation of the operator was successful and resulted in expression $e$.

This specification can be built for the whole translation algorithm, until a specification of a function translation is obtained, which can then be used instead of the implementation if the following Theorem can be proven.

\begin{lemma}\label{lemma:specification}
  If a 3AC function $c$ is translated correctly to a module $h$, then the specification of the translation should hold.

  \begin{equation*}
    \forall\ c\ h,\ \yhfunction{tr\_function} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_function}\ c\ h.
  \end{equation*}
\end{lemma}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

One example is the translation of instructions, where the translation function might contain many implementation specific details, such as in which order instructions are added to the data path or the control path, whereas the specification describes only describes which instructions were added.  The specification, \texttt{tr\_instr} can then be described as follows, where \textit{fin}, \textit{rtrn}, $\sigma$ and \textit{stk} are the registers for the finished signal, return value, current state and stack respectively, $i$ is the 3AC instruction being translated, and \textit{data} and \textit{control} are the data-flow and control logic map respectively.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Firstly, as the input representation is a map, all the keys of the map will be unique, which will be translated to the matched expressions in the case statement.  In addition to that, the assumption is made that every possible evaluation of the state value will give a valid state, meaning the key will be present in the map.  Both of these observations mean that after the translation, for every possible value of the state, the case statement will be able to match an expression and enter the correct statement.  As each key is unique, if the state matches a case expression, then this also means that this is the only case expression that it could match, and it therefore has to be the correct case expression which contains the same statement as the map.

However, the proof of uniqueness of the keys only works if the translation function is \emph{injective}, meaning that the function will result in distinct outputs for all possible inputs.  Otherwise, the proof of uniqueness of the keys for the input would not translate to a uniqueness of possible case expression matches in the output.  However, in our case the translation function is actually not injective, even though it might at first seem like it, because the state is stored as an integer, whereas the map is addressable by any positive number.  This means that if the positive number is greater than the maximum value that can be stored in the integer, the overflow would result in the wrong states being accessed.  To make the function injective, we therefore have to prove that the input positive number is never greater than $2^{32}-1$ so that the uniqueness property also holds for the output.

\begin{align*}
  &\forall\ (S_{1} : \texttt{3AC.state})\ t\ S_{2},\ S_{1} \xrightarrow{t} S_{2}\\
  &\implies \forall\ (R_{1} : \texttt{HTL.state}),\ \texttt{match\_states}\ S_{1}\ R_{1}\\
  &\implies \exists R_{2},\ R_{1} \xrightarrow{t}_{+} R_{2} \land \texttt{match\_states}\ S_{2}\ R_{2}.
\end{align*}