diff options
| -rw-r--r-- | archive/proof.tex | 9 | ||||
| -rw-r--r-- | proof.tex | 7 |
2 files changed, 12 insertions, 4 deletions
diff --git a/archive/proof.tex b/archive/proof.tex new file mode 100644 index 0000000..9e962b7 --- /dev/null +++ b/archive/proof.tex @@ -0,0 +1,9 @@ +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*} @@ -1,5 +1,4 @@ -\section{Proof} -\label{sec:proof} +\section{Proof}\label{sec:proof} 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 proofs. @@ -13,10 +12,10 @@ To prove this top-level theorem, a forward simulation has to be done between eac \subsection{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 translation might be defined using the following function: $\yhfunction{transl\_3ac\_htl} (c) = \yhconstant{OK} (h)$, where $c$ is the 3AC input code and $h$ is the generated HTL code. However, instead we can define a relation \texttt{tr\_3ac\_htl} between the 3AC and HTL code, which contains all the properties about the translation that are needed, without any of the implementation. If the following can be proven, it can then be used instead of the translation algorithm when performing the proof of correctness. +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 translation might be defined using the following function: $\yhfunction{transl\_3ac\_htl} (c) = \yhconstant{OK} (h)$, where $c$ is the 3AC input code and $h$ is the generated HTL code. However, instead we can define a relation \texttt{spec\_3ac\_htl} between the 3AC and HTL code, which contains all the properties about the translation that are needed, without any of the implementation. If the following can be proven, it can then be used instead of the translation algorithm when performing the proof of correctness. \begin{equation*} - \forall\ c\ h,\ \yhfunction{transl\_3ac} (c) = \yhconstant{OK}(h) \implies \yhfunction{tr\_htl}\ c\ h. + \forall\ c\ h,\ \yhfunction{transl\_3ac\_htl} (c) = \yhconstant{OK}(h) \implies \texttt{spec\_3ac\_htl}\ c\ h. \end{equation*} 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. |