Index: /Deliverables/D1.2/CompilerProofOutline/outline.tex
===================================================================
 /Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1772)
+++ /Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1773)
@@ 317,4 +317,88 @@
\subsection{Graph translations}
+RTLabs and most intermediate languages in the backend have a graph
+representation:
+the code of each function is represented by a graph of instructions.
+The graph maps a set of labels (the names of the nodes) to the instruction
+stored at that label (the nodes of the graph).
+Instructions reference zero or more additional labels that are the immediate
+successors of the instruction: zero for return from functions; more than one
+for conditional jumps and calls; one in all other cases. The references
+from one instruction to its immediates are the arcs of the graph.
+
+Status of graph languages always have a program counter that holds a
+representation of a reference to the current instruction.
+
+A translation between two consecutive graph languages maps each instruction
+stored at location $l$ in the first graph and with immediate successors
+$\{l_1,\ldots,l_n\}$ to a subgraph of the output graph that has a single
+entry point at location $l$ and exit arcs to $\{l_1,\ldots,l_n\}$. Moreover,
+the labels of all non entry nodes in the subgraph are distinct from all the
+labels in the source graph.
+
+In order to simplify the translations and the relative proofs of forward
+simulation, after the release of D4.2 and D4.3, we have provided:
+\begin{itemize}
+ \item a new data type (called \texttt{blist}) that represents a
+ sequence of instructions to be added to the output graph.
+ The ``b'' in the name stands for binder, since a \texttt{blist} is
+ either empty, an extension of a \texttt{blist} with an instruction
+ at the front, or the generation of a fresh quantity followed by a
+ \texttt{blist}. The latter feature is used, for instance, to generate
+ fresh register names. The instructions in the list are unlabelled and
+ all of them but the last one are also sequential, like in a linear program.
+ \item a new iterator (called \texttt{b\_graph\_translate}) of type
+\begin{displaymath}
+\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist})
+\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
+\end{displaymath}
+ The iterator transform the input graph in the output graph by replacing
+ each node with the graph that corresponds to the linear \texttt{blist}
+ obtained by applying the function in input to the node label.
+\end{itemize}
+
+Using the iterator above, the code can be written in such a way that
+the programmer does not see any distinction between writing a transformation
+on linear or graph languages.
+
+In order to prove simulations for translations obtained using the iterator,
+we will prove the following theorem:
+
+\begin{align*}
+\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
+& \forall f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
+& \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (next \ l \ G_i)\ G_{\sigma}
+\end{align*}
+
+Here \texttt{subgraph} is a computational predicate that given a \texttt{blist}
+$[i_1, \ldots, i_n]$, an entry label $l$, an exit label $l'$ and a graph $G$
+expands to the fact that fetching from $G$ at address $l$ one retrieves a node
+$i_1$ with a successor $l_1$ that, when fetched, yields a node $i_2$ with a
+successor $l_2$ such that \ldots. The successor of $i_n$ is $l'$.
+
+Proving a forward simulation diagram of the following kind using the theorem
+above is now as simple as doing the same using standard small step operational
+semantics over linear languages.
+
+\begin{align*}
+\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
+& \forall s. \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
+& \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
+& s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
+\end{align*}
+
+Because of the fact that graph translation preserves entry and exit labels of
+translated statements, the state translation function $\sigma$ will simply
+preserve the value of the program counter. The program code, which is
+part of the state, is translated using the iterator.
+
+The proof is then roughly the following. Let $l$ be the program counter of the
+input state $s$. We proceed by cases on the current instruction of $s$.
+Let $[i_1, \ldots, i_n]$ be the \texttt{blist} associated to $l$ and $s$
+by the translation function. The witness required for the existential
+statement is simply $n$. By applying the theorem above we know that the
+next $n$ instructions that will be fetched from $s\ \sigma$ will be
+$[i_1, \ldots, i_n]$ and it is now sufficient to prove that they simulate
+the original instruction.
\subsection{The RTLabs to RTL translation}
@@ 583,25 +667,4 @@
\end{diagram}
\end{displaymath}

\subsection{The RTL to ERTL translation}
\label{subsect.rtl.ertl.translation}

\begin{displaymath}
\mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'})
\rightarrow \mathtt{graph} \rightarrow \mathtt{graph}
\end{displaymath}

\begin{align*}
\mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\
& \forall f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\
& \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma}
\end{align*}

\begin{align*}
\mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\
& \forall s. \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\
& \mathtt{let}\ l := pc\ s\ \mathtt{in} \\
& s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
\end{align*}
\begin{align*}