diff options
| -rw-r--r-- | archive/proof.tex | 48 | ||||
| -rw-r--r-- | proof.tex | 69 |
2 files changed, 80 insertions, 37 deletions
diff --git a/archive/proof.tex b/archive/proof.tex index 6641c8d..34f2a38 100644 --- a/archive/proof.tex +++ b/archive/proof.tex @@ -1,3 +1,51 @@ +\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. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -2,13 +2,13 @@ Now that the Verilog semantics have been adapted to the CompCert model, we are in a position to formally prove the correctness of our C to Verilog compilation. This section describes the main correctness theorem that was proven and the main ideas behind the proof. -The main correctness theorem is the exact same correctness theorem as stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil} which states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has safe observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$, meaning execution should either converge or diverge, but should not ``go wrong''. Behaviour is also associated with a trace $t$ of any I/O events, however, as external function calls are not supported, this trace $t$ will always be empty for programs passing through \vericert{}. The following backwards simulation theorem describes the correctness theorem, where $\Downarrow_{s}$ and $\Downarrow$ stand for simulation and execution respectively. +The main correctness theorem is the exact same correctness theorem as stated in \compcert{}~\cite{leroy09_formal_verif_realis_compil} which states that for all Clight source programs $C$, if the translation from the source to the target Verilog code succeeds, assuming that $C$ has safe observable behaviour $B$ when executed, then the target Verilog code will simulate with the same behaviour $B$, meaning execution should either converge or diverge, but should not ``go wrong''. Behaviour is also associated with a trace $t$ of any I/O events, however, as external function calls are not supported, this trace $t$ will always be empty for programs passing through \vericert{}. The following backwards simulation theorem describes the correctness theorem, where $\Downarrow$ stands for simulation and execution respectively. \begin{theorem} Assuming that the translation from $C$ to Verilog $V$ succeeds, then if $V$ has behaviour $B$, $C$ should have the same behaviour $B$. \begin{equation*} - \forall C, V, B \in \texttt{Safe},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow_{s} B \implies C \Downarrow B. + \forall C, V, B \in \texttt{Safe},\, \yhfunction{HLS} (C) = \yhconstant{OK} (V) \land V \Downarrow B \implies C \Downarrow B. \end{equation*} \end{theorem} @@ -20,7 +20,7 @@ The main correctness theorem is the exact same correctness theorem as stated in The forward simulation between 3AC and HTL is proven in Lemma~\ref{lemma:htl}, next the forward simulation between HTL and Verilog is shown in Lemma~\ref{lemma:verilog} and finally, the proof that Verilog is deterministic is given in Lemma~\ref{lemma:deterministic}. \end{proof} -\subsection{Forward simulation between 3AC and HTL}\label{sec:proof:specification} +\subsection{Forward simulation between 3AC and HTL}\label{sec:proof:3ac_htl} As HTL is quite different to 3AC, this first translation is the most involved and therefore requires a larger proof, because the translation from 3AC instructions to Verilog statements needs to be proven correct in this step. 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 and mirror the semantics defined for Verilog. Lemma~\ref{lemma:htl} shows the theorem that needs to be proven in this section. @@ -33,26 +33,18 @@ As HTL is quite different to 3AC, this first translation is the most involved an \end{lemma} \begin{proof} - Follows by using a specification of the important properties $\yhfunction{tr\_htl}$ has + Follows by using a specification of the important properties $\yhfunction{tr\_htl}}$ which can be used as an assumption in the proof instead. The forward simulation is then proven by showing that the initial states and final states between the 3AC semantics and HTL semantics match, and then showing that the simulation diagram in Lemma~\ref{lemma:simulation_diagram} holds. \end{proof} -\subsubsection{Specification} +\subsubsection{Specification}\label{sec:proof:3ac_htl:specification} -To simplify the proof, instead of using the translation algorithm as an assumption, as was done in the backward simulation stated above, 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. +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 specification for the translation of 3AC instructions into HTL data path and control logic can be defined as follows: \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: +\noindent The \textit{control} and \textit{data} parts of the specification are the statements that the current 3AC instruction $i$ should translate to. A 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)} @@ -60,13 +52,11 @@ However, instead we can define a specification for the translation of instructio \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. + If a 3AC program $c$ is translated correctly to an HTL program $h$, then the specification of the translation holds. \begin{equation*} - \forall\ c\ h,\ \yhfunction{tr\_function} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_function}\ c\ h. + \forall\ c\ h,\ \yhfunction{tr\_htl} (c) = \yhconstant{OK}(h) \implies \yhfunction{spec\_htl}\ c\ h. \end{equation*} \end{lemma} @@ -75,10 +65,8 @@ This specification can be built for the whole translation algorithm, until a spe 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. Some of these assertions that need to be made about the 3AC and HTL code for a state to match are: \begin{itemize} - \item the 3AC register file $R$ needs to be ``less defined'' than the HTL register file $\Gamma_{r}$ and the RAM values represented by a Verilog array in $\Gamma_{a}$ need to match the 3AC function's stack contents, which are part of the memory $M$, - \item the \texttt{tr\_module} predicate needs to hold for the current 3AC function and HTL module. - \item the state is well formed, meaning the value of the state register matches the current value of the program counter, - \item the stack frames match. + \item the 3AC register file $R \le \Gamma_{r}$ needs to be ``less defined'' than the HTL register map $\Gamma_{r}$ and the RAM values represented by a Verilog array in $\Gamma_{a}$ need to match the 3AC function's stack contents, which are part of the memory $M$: $M \le \Gamma_{a}$, + \item the state is well formed, meaning the value of the state register matches the current value of the program counter: $\textit{pc} = \Gamma_{r}!\sigma$, \end{itemize} As well as some invariants $\mathcal{I}$ that have to hold for the current state to be valid: @@ -87,20 +75,14 @@ As well as some invariants $\mathcal{I}$ that have to hold for the current state \item all pointers in the program use the stack as a base pointer, \item that a load and store to a location outside of the bounds of the stack does not occur, and does not modify the \compcert{} memory. Even if it occurs in the program, as it is undefined behaviour we can prove that our behaviour is still correct given the input. \item that \textit{rst} and \textit{fin} are not modified and therefore stay at a constant 0 throughout execution. + \item that the stack frames match. \end{itemize} -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} - -Using the \texttt{match\_states}, we can then define the forward simulation for the translation, shown as a simulation diagram below, where the 3AC state can be represented by $(R,M,\textit{pc})$, $R$ being the map of values for all current registers, $M$ being the current state of memory and \textit{pc} being the current program counter. The state of HTL can also be represented by $\Gamma$, which can be split into $\Gamma_{r}$ for the current state of all registers in the module, and $\Gamma_{a}$, for the state of all arrays in the Verilog module, which represents the stack. Finally, $\mathcal{I}$ stands for the other invariants that need to hold in the \texttt{match\_states} predicate: +We can then define the simulation diagram for the translation, where the 3AC state can be represented by $(R,M,\textit{pc})$. The state of HTL can be represented by the maps $\Gamma_{r}$ for the current state of all registers in the module, and $\Gamma_{a}$, for the state of all arrays in the Verilog module, which represents the stack. Finally, $\mathcal{I}$ stands for the other invariants that need to hold for the states to match: \begin{lemma}\label{lemma:simulation_diagram} - Given the 3AC state $(R,M,\textit{pc})$ and the matching HTL state $(\Gamma_{r}, \Gamma_{a})$, assuming one step in the 3AC semantics produces state $(R',M',\textit{pc}')$, there exists one or more steps in the HTL semantics that result in matching states $(\Gamma_{r}', \Gamma_{a}')$. + Given the 3AC state $(R,M,\textit{pc})$ and the matching HTL state $(\Gamma_{r}, \Gamma_{a})$, assuming one step in the 3AC semantics produces state $(R',M',\textit{pc}')$, there exists one or more steps in the HTL semantics that result in matching states $(\Gamma_{r}', \Gamma_{a}')$. This is all under the assumption that the specification $\yhfunction{tr\_{htl}}$ holds for the translation. + \begin{center} \begin{tikzpicture} \begin{scope} @@ -118,15 +100,28 @@ Using the \texttt{match\_states}, we can then define the forward simulation for \end{center} \end{lemma} -\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$. +\begin{proof} + This simulation diagram is proven by induction over the operational semantics of 3AC, which allows us to find one or more steps in the HTL semantics that will produce the same final matching state. +\end{proof} \subsection{HTL to Verilog forward simulation} -The HTL to Verilog simulation is conceptually simple, as the only transformation is from the map representation of the code to the case statement representation. As the representations are quite different though, to prove that they are equivalent the following observations have to be made. +The HTL to Verilog simulation is conceptually simple, as the only transformation is from the map representation of the code to the case statement representation. As the representations are quite different though, the proof is more involved, as the semantics of a map structure are quite different to the semantics of the case statement they are converted to. -The translation from maps to case statements is done by turning each node of the tree into a case expression with the statements in each being the same. The main difficulty for the proof is that a structure that can be directly accessed is transformed into an inductive structure where a certain number of constructors need to be called to get to the correct case. The proof of the translation from maps to case statements follows by induction over the list of elements in the map and the fact that each key will be unique. In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list. The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list. The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't. In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore. In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match. +\begin{lemma}\label{lemma:verilog} + The forward simulation for this translation assumes that the Verilog $V$ was obtained from the HTL to Verilog translation function $\yhfunction{tr\_verilog}$, note that the translation can not fail for this step. + + \begin{align*} + &\forall h, V, B \in \texttt{Safe}, \\ + &\quad\yhfunction{tr\_verilog} (h) = V \land h \Downarrow B \implies V \Downarrow B. + \end{align*} +\end{lemma} -Another problem with the representation of the state as an actual register is that we have to make sure that the state does not overflow. Currently, the state register will always be 32 bits, meaning the maximum number of states can only be $2^{32} - 1$. We therefore have to prove that the state value will never go over that value. This means that during the translation we have to check for each state that it can fit into an integer. Finally, as we have to assume that there are $2^{32} - 1$ states, \vericert{} will error out when there are more instructions to be translated, which allows us to satisfy and prove that assumption correct. +\begin{proof} + The translation from maps to case statements is done by turning each node of the tree into a case expression with the statements in each being the same. The main difficulty for the proof is that a structure that can be directly accessed is transformed into an inductive structure where a certain number of constructors need to be called to get to the correct case. The proof of the translation from maps to case statements follows by induction over the list of elements in the map and the fact that each key will be unique. In addition to that, the statement that is currently being evaluated is guaranteed by the correctness of the list of elements to be in that list. The latter fact therefore eliminates the base case, as an empty list does not contain the element we know is in the list. The other two cases follow by the fact that either the key is equal to the evaluated value of the case expression, or it isn't. In the first case we can then evaluate the statement and get the state after the case expression, as the uniqueness of the key tells us that the key cannot show up in the list anymore. In the other case we can just apply the inductive hypothesis and remove the current case from the case statement, as it did not match. + + Another problem with the representation of the state as an actual register is that we have to make sure that the state does not overflow. Currently, the state register will always be 32 bits, meaning the maximum number of states can only be $2^{32} - 1$. We therefore have to prove that the state value will never go over that value. This means that during the translation we have to check for each state that it can fit into an integer. Finally, as we have to assume that there are $2^{32} - 1$ states, \vericert{} will error out when there are more instructions to be translated, which allows us to satisfy and prove that assumption correct. +\end{proof} \subsection{Deterministic Semantics} |