Index: /Deliverables/D1.2/CompilerProofOutline/outline.tex
===================================================================
--- /Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1768)
+++ /Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1769)
@@ -316,4 +316,6 @@
\end{center}
+\subsection{Graph translations}
+
\subsection{The RTLabs to RTL translation}
\label{subsect.rtlabs.rtl.translation}
@@ -489,7 +491,13 @@
The forward simulation proof for all steps that do not involve function
-calls is trivial because $\sigma$ does not alter the memory or the
-pseudo-registers. We outline here the invocation of functions and return
-from a function.
+calls are lengthy, but unsurprising. They consists in simulating a
+front-end operation on front-end pseudo-registers and the front-end memory
+with sequences of back-end operations on the back-end pseudo-registers
+and back-end memory. The properties of $\sigma$ presented before that relate
+values and memories needs to be heavily exploited.
+
+The simulation of invocation of functions and returns from functions is
+less obvious. We sketch here what happens on the source code and on its
+translation.
\begin{displaymath}