Index: /Papers/itp2013/ccexec.tex
===================================================================
 /Papers/itp2013/ccexec.tex (revision 2631)
+++ /Papers/itp2013/ccexec.tex (revision 2632)
@@ 806,5 +806,6 @@
$s_1$ to $s_1'$ and $s_1 R s_2$ there exists an $s_2'$ such that
$s_1' R s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
$\tau_1 \approx \tau_2$.\\
+$\tau_1$ is similar to $\tau_2$. We call this particular form of forward
+simulation \emph{trace reconstruction}.
The statement just introduced, however, is too simplicistic and not provable
@@ 837,24 +838,72 @@
Therefore we now introduce an abstract notion of relation set between abstract
statuses and an abstract notion of 1to0ormany forward simulation. These
two definitions enjoy the following remarkable properties:
+statuses and an abstract notion of 1to0ormany forward simulation conditions.
+These two definitions enjoy the following remarkable properties:
\begin{enumerate}
\item they are generic enough to accomodate all passes of the CerCo compiler
 \item they allow to lift the 1to0ormany forward simulation to the
 structured traces preserving forward simulation we are interested in
+ \item the conjunction of the 1to0ormany forward simulation conditions are
+ just slightly stricter than the statement of a 1to0ormany forward
+ simulation in the classical case. In particular, they only require
+ the construction of very simple forms of structured traces made of
+ silent states only.
+ \item they allow to prove our main result of the paper: the 1to0ormany
+ forward simulation conditions are sufficient to prove the trace
+ reconstruction theorem
\end{enumerate}
The latter lifting is proved by the following theorem which has the
1to0ormany forward simulation statement as an hypothesis. Combined with
the results in the previous section, it has as a corollary that the cost
model can be computed on the object code and lifted to the source code to
reason on nonfunctional properties iff a simpler 1to0ormany forward
simulation is proved. The statement of the latter is way more complex than a
traditional 1to0ormany forward simulation statement, but proofs have now
about the same complexity. Indeed, it should be possible to largely reuse an
existent traditional forward simulation proof. The lifting theorem below,
proved once and for all in this paper, is the one that does all the job to
put the labelling approach in motion.

+Point 3. is the important one. First of all it means that we have reduced
+the complex problem of trace reconstruction to a much simpler one that,
+moreover, can be solved with slight adaptations of the forward simulation proof
+that is performed for a compiler that only cares about functional properties.
+Therefore we have successfully splitted as much as possible the proof of
+preservation of functional properties from that of nonfunctional ones.
+Secondly, combined with the results in the previous section, it implies
+that the cost model can be computed on the object code and lifted to the
+source code to reason on nonfunctional properties, assuming that
+the 1to0ormany forward simulation conditions are fullfilled for every
+compiler pass.
+
+\paragraph{Relation sets}
+
+We introduce now the four relations $\mathcal{S,C,L,R}$ between abstract
+statuses that are used to correlate the corresponding statues before and
+after a compiler pass. The first two are abstract and must be instantiated
+by every pass. The remaining two are derived relations.
+
+The $\mathcal{S}$ relation between states is the classical relation used
+in forward simulation proofs. It correlates the data of the status
+(e.g. registers, memory, etc.).
+
+The $\mathcal{C}$ relation correlates call states. It allows to track the
+position in the target code of every call in the source code.
+
+The $\mathcal{L}$ relation simply says that the two states are both label
+emitting states that emit the same label. It allows to track the position in
+the target code of every cost emitting statement in the source code.
+
+Finally the $\mathcal{R}$ relation is the more complex one. Two states
+$s_1$ and $s_2$ are $\mathcal{R}$ correlated if every time $s_1$ is the
+successors of a call state that is $\mathcal{C}$related to a call state
+$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$.
+We will require all pairs of states that follow a related call to be
+$\mathcal{R}$related. This is the fundamental requirement to grant
+that the target trace is well structured, i.e. that function calls are well
+nested and always return where they are supposed to.
+
+\begin{alltt}
+record status_rel (S1,S2 : abstract_status) : Type[1] := \{
+ \(\mathcal{S}\): S1 \(\to\) S2 \(\to\) Prop;
+ \(\mathcal{C}\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\)
+ (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop \}.
+
+definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
+
+definition \(\mathcal{R}\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
+ \(\forall\)s1_pre,s2_pre.
+ as_after_return s1_pre s1_ret \(\to\) s1_pre \(\mathcal{R}\) s2_pre \(\to\)
+ as_after_return s2_pre s2_ret.
+\end{alltt}
+
+\paragraph{1to0ormany forward simulation conditions}
\begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}]
For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and
@@ 1000,17 +1049,18 @@
\end{comment}
\begin{alltt}
record status_rel (S1,S2 : abstract_status) : Type[1] := \{
 \(\mathcal{S}\): S1 \(\to\) S2 \(\to\) Prop;
 \(\mathcal{C}\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\) (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop
 \}.

definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.

definition \(\mathcal{R}\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
 \(\forall\)s1_pre,s2_pre.
 as_after_return s1_pre s1_ret \(\to\) call_rel s1_pre s2_pre \(\to\)
 as_after_return s2_pre s2_ret.
\end{alltt}
+\paragraph{Main result: the 1to0ormany forward simulation conditions
+are sufficient to trace reconstruction}
+
+Let us assume that a relation set is given such that the 1to0ormany
+forward simulation conditions are satisfied. Under this assumption we
+can prove the following three trace reconstruction theorems by mutual
+structural induction over the traces given in input between the
+$s_1$ and $s_1'$ states.
+
+In particular, the \texttt{status\_simulation\_produce\_tlr} theorem
+applied to the \texttt{main} function of the program and equal
+$s_{2_b}$ and $s_2$ states shows that, for every initial state in the
+source code that induces a structured trace in the source code,
+the compiled code produces a similar structured trace.
\begin{theorem}[\texttt{status\_simulation\_produce\_tlr}]
@@ 1026,4 +1076,17 @@
$s_1' \mathcal{R} s_{2_m}$.
\end{theorem}
+
+The theorem states that a \texttt{trace\_label\_return} in the source code
+together with a precomputed preamble of silent states
+(the \texttt{trace\_any\_any}) in the target code induces a
+similar \texttt{trace\_label\_return} trace in the target code which can be
+followed by a sequence of silent states. Note that the statement does not
+require the produced \texttt{trace\_label\_return} trace to start with the
+precomputed preamble, even if this is likely to be the case in concrete
+implementations. The preamble in input is necessary for compositionality, e.g.
+because the 1to0ormany forward simulation conditions allow in the
+case of function calls to execute a preamble of silent instructions just after
+the function call.
+
\begin{theorem}[\texttt{status\_simulation\_produce\_tll}]
For every $s_1,s_1',s_{2_b},s_2$ s.t.
@@ 1045,4 +1108,11 @@
\end{itemize}
\end{theorem}
+
+The statement is similar to the previous one: a source
+\texttt{trace\_label\_label} and a given target preamble of silent states
+in the target code induce a similar \texttt{trace\_label\_label} in the
+target code, possibly followed by a sequence of silent moves that become the
+preamble for the next \texttt{trace\_label\_label} translation.
+
\begin{theorem}[\texttt{status\_simulation\_produce\_tal}]
For every $s_1,s_1',s_2$ s.t.
@@ 1065,4 +1135,7 @@
\end{itemize}
\end{theorem}
+
+The statement is also similar to the previous ones, but for the lack of
+the target code preamble.
\begin{comment}