diff options
Diffstat (limited to 'proof.tex')
| -rw-r--r-- | proof.tex | 30 |
1 files changed, 15 insertions, 15 deletions
@@ -18,17 +18,17 @@ To prove this statement, we therefore have to prove that the Verilog semantics a \subsection{Forward Simulation} -The forward simulation between C and Verilog can be separated into forward simulations of each compiler pass, which can then be composed to provide a whole proof from C to Verilog. We therefore only have to prove a forward simulation for the RTL to HTL translation, and for the HTL to Verilog translation. +The forward simulation between C and Verilog can be separated into forward simulations of each compiler pass, which can then be composed to provide a whole proof from C to Verilog. We therefore only have to prove a forward simulation for the 3AC to HTL translation, and for the HTL to Verilog translation. -\subsubsection{RTL to HTL forward simulation} +\subsubsection{3AC to HTL forward simulation} -As HTL is quite different to RTL, this first translation is the most involved translation and therefore requires a larger proof, as the translation from RTL instructions to Verilog statements needs to be proven correct. In addition to that, the semantics of HTL are also quite different to the RTL semantics, as instead of defining small-step semantics for each construct in Verilog, the semantics are instead defined over one clock cycle. +As HTL is quite different to 3AC, this first translation is the most involved translation and therefore requires a larger proof, as the translation from 3AC instructions to Verilog statements needs to be proven correct. 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. \begin{figure} \centering \begin{minted}{coq} Inductive match_states : - RTL.state -> HTL.state -> Prop := + 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) @@ -39,44 +39,44 @@ Inductive match_states : (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0)) (RSBP : reg_stack_based_pointers sp' rs) (ASBP : arr_stack_based_pointers sp' mem - (f.(RTL.fn_stacksize)) sp) - (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem) + (f.(3AC.fn_stacksize)) sp) + (BOUNDS : stack_bounds sp (f.(3AC.fn_stacksize)) mem) (CONST : match_constants m asr), match_states - (RTL.State sf f sp st rs mem) + (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 - (RTL.Returnstate stack v mem) + (3AC.Returnstate stack v mem) (HTL.Returnstate res v') | match_initial_call : forall f m m0 (TF : tr_module f m), match_states - (RTL.Callstate nil (AST.Internal f) nil m0) + (3AC.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil). \end{minted} - \caption{\texttt{match\_states} predicate used to match an RTL state to the equivalent HTL state.}\label{fig:match_states} + \caption{\texttt{match\_states} predicate used to match an 3AC state to the equivalent HTL state.}\label{fig:match_states} \end{figure} -The first step in proving the forward simulation is to define a relation that matches an RTL state to an HTL state, which shows when the states are equivalent. This relation also defines assumptions that are made about the RTL 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. The \texttt{match\_states} predicate that is used to match the states of the RTL 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. +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. The \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{RTL.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 RTL 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. 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\_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. 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 \texttt{nil}. \end{enumerate} Using the \texttt{match\_states}, we can then define the correctness theorem for the translation. \begin{align*} - &\forall\ (S_{1} : \texttt{RTL.state})\ t\ S_{2},\ S_{1} \xrightarrow{t} S_{2}\\ + &\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*} -$S_{1}$ and $S_{2}$ are RTL states and $R_{1}$ and $R_{2}$, HTL states and $\xrightarrow{t}$ is one step in the semantics of RTL and $\xrightarrow{t}_{+}$ is one or more steps in the semantics of HTL.\@ The correctness theorem then says that for all possible starting states $S_{1}$ and for the resulting state $S_{2}$ after one step in the semantics of RTL, for all HTL states $R_{1}$ that matches the state $S_{1}$, there should exist a state $R_{2}$ such that $R_{2}$ is the result of the simulation of the HTL semantics and that the states $S_{2}$ and $R_{2}$ should match as well. Using this property, the forward simulation can then be proven correct by also showing that the initial and final states of the simulation match as well. +$S_{1}$ and $S_{2}$ are 3AC states and $R_{1}$ and $R_{2}$, HTL states and $\xrightarrow{t}$ is one step in the semantics of 3AC and $\xrightarrow{t}_{+}$ is one or more steps in the semantics of HTL.\@ The correctness theorem then says that for all possible starting states $S_{1}$ and for the resulting state $S_{2}$ after one step in the semantics of 3AC, for all HTL states $R_{1}$ that matches the state $S_{1}$, there should exist a state $R_{2}$ such that $R_{2}$ is the result of the simulation of the HTL semantics and that the states $S_{2}$ and $R_{2}$ should match as well. Using this property, the forward simulation can then be proven correct by also showing that the initial and final states of the simulation match as well. \subsubsection{HTL to Verilog forward simulation} |