Add more proof section

1 files changed, 11 insertions, 5 deletions

diff --git a/proof.tex b/proof.tex
index 85dbefd..c0b7a27 100644
--- a/proof.tex
+++ b/proof.tex
@@ -10,22 +10,28 @@ The main correctness theorem states that for all Clight source programs $C$, if
 
 To prove this top-level theorem, a forward simulation has to be done between each intermediate language, which implies that the forward simulation between the C and Verilog also holds.  To then prove the backward simulation, it suffices to show that the Verilog semantics are deterministic, which implies that there is only one possible behaviour for the Verilog output, and that it therefore also has to imply that $C$ has the same behaviour.
 
-\subsection{Model}
+\subsection{Specification}
 
-%\JW{I think some of the following material belongs in a later section. In the current section, I think we should aim at the casual reader who is interested in understanding things like the overall structure of the tool, which IR language you branch off from, and what the key ideas/difficulties involved are. I think intimidating inference rules with loads of new symbols should be saved for a later section -- the kind of section that really is only going to be read by people who are actually interested in reproducing or building upon your work. So things like `One thing to note is that the comparison is signed ... by default all operators in Verilog are unsigned ... so we force the operators to be signed' very much belong in the current section; you just don't need a scary inference rule first.}
+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}} (c) = \yhconstant{OK} (h)$, where $c$ is the 3AC input code and $h$.  However, instead we can define a relation \texttt{tr\_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.
 
-The translation can be described by a relational specification, which can be described by the following relation, 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.
+\begin{equation*}
+  \forall\ c\ h,\ \yhfunction{transl\_3ac} (c) = \yhconstant{OK}(h) \implies \yhfunction{tr\_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.
 
 \begin{equation*}
   \yhfunction{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ i\ \textit{data }\ \textit{control}
 \end{equation*}
 
-\noindent An example of a rule describing the translation of an operation is the following:
+\noindent An 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{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ (\yhconstant{Iop } \textit{op }\ \vec{a}\ d\ n)\ (d \Leftarrow e)\ (\sigma \Leftarrow n)}
+  \inferrule[Iop]{\yhfunction{tr\_op } \textit{op }\ \vec{a} = \yhconstant{OK } e}{\yhfunction{tr\_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.
+
 \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 3AC to HTL translation, and for the HTL to Verilog translation.