Add theorem

2 files changed, 14 insertions, 8 deletions

diff --git a/main.tex b/main.tex
index 0ba45e2..24b0808 100644
--- a/main.tex
+++ b/main.tex
@@ -86,6 +86,8 @@
 \newcommand{\compcert}{Comp\-Cert}
 \newcommand{\legup}{Leg\-Up}
 
+\newtheorem{theorem}{Theorem}
+
 \begin{document}
 
 %% Title information
diff --git a/proof.tex b/proof.tex
index 210092b..9b09e54 100644
--- a/proof.tex
+++ b/proof.tex
@@ -23,22 +23,26 @@ tr_instr : 3AC.instruction -> state -> res state
 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\_tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ i\ \textit{data }\ \textit{control}
+  \yhfunction{spec\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ i\ \textit{data }\ \textit{control}
 \end{equation*}
 
-\noindent An 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 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{tr\_instr } \textit{fin rtrn }\ \sigma\ \textit{stk }\ (\yhconstant{Iop } \textit{op }\ \vec{a}\ d\ n)\ (d\ \yhkeyword{<=}\ e)\ (\sigma\ \yhkeyword{<=}\ n)}
+  \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.
+\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$.
 
-If the following can be proven, it can then be used instead of the translation algorithm when performing the proof of correctness.
+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{equation*}
-  \forall\ c\ h,\ \yhfunction{transl\_3ac\_htl} (c) = \yhconstant{OK}(h) \implies \texttt{spec\_3ac\_htl}\ c\ h.
-\end{equation*}
+\begin{theorem}
+  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{theorem}
 
 \subsection{Forward Simulation}