Index: /Deliverables/D3.4/Report/meassim.svg
===================================================================
 /Deliverables/D3.4/Report/meassim.svg (revision 3158)
+++ /Deliverables/D3.4/Report/meassim.svg (revision 3158)
@@ 0,0 +1,362 @@
+
+
+
+
Index: /Deliverables/D3.4/Report/report.tex
===================================================================
 /Deliverables/D3.4/Report/report.tex (revision 3157)
+++ /Deliverables/D3.4/Report/report.tex (revision 3158)
@@ 448,14 +448,128 @@
\item transformation to \textsf{RTLabs} control flow graph
\end{enumerate}

TODO: layered approach  main part is the common measurable
preservation proof; finegrained version of normal simulation results
does rest.
+\todo{I keep mentioning forward sim results  I probably ought to say
+ something about determinancy} We have taken a common approach to
+each pass: first we build (or axiomatise) forward simulation results
+that are similar to normal compiler proofs, but slightly more
+finegrained so that we can see that the call structure and relative
+placement of cost labels is preserved.
+
+Then we instantiate a general result which shows that we can find a
+\emph{measurable} subtrace in the target of the pass that corresponds
+to the measurable subtract in the source. By repeated application of
+this result we can find a measurable subtrace of the execution of the
+\textsf{RTLabs} code, suitable for the construction of a structured
+trace (see Section~\ref{sec:structuredtrace}. This is essentially an
+extra layer on top of the simulation proofs that provides us with the
+extra information required for our intensional correctness proof.
\subsection{Generic measurable subtrace lifting proof}
Sketch properties required; need to preserve prefix as well as meas
subtrace; how to deal with untidy edges wrt to sim rel; anything to
say about obs, stack?
+Our generic proof is parametrised on a record containing smallstep
+semantics for the source and target language, a classification of
+states (the same form of classification is used when defining
+structured traces), a simulation relation which loosely respects the
+classification and cost labelling \todo{this isn't very helpful} and
+four simulation results:
+\begin{enumerate}
+\item a step from a `normal' state (which is not classified as a call
+ or return) which is not a cost label is simulated by zero or more
+ `normal' steps;
+\item a step from a `call' state followed by a cost label step is
+ simulated by a step from a `call' state, a corresponding label step,
+ then zero or more `normal' steps;
+\item a step from a `call' state not followed by a cost label
+ similarly (note that this case cannot occur in a welllabelled
+ program, but we do not have enough information locally to exploit
+ this); and
+\item a cost label step is simulated by a cost label step.
+\end{enumerate}
+Finally, we need to know that a successfully translated program will
+have an initial state in the simulation relation with the original
+program's initial state.
+
+\begin{figure}
+\begin{center}
+\includegraphics[width=0.5\linewidth]{meassim.pdf}
+\end{center}
+\caption{Tiling of simulation for a measurable subtrace}
+\label{fig:tiling}
+\end{figure}
+
+To find the measurable subtrace in the target program's execution we
+walk along the original program's execution trace applying the
+appropriate simulation result by induction on the number of steps.
+While the number of steps taken varies, the overall structure is
+preserved, as illustrated in Figure~\ref{fig:tiling}. By preserving
+the structure we also maintain the same intensional observables. One
+delicate point is that the cost label following a call must remain
+directly afterwards\footnote{The prototype compiler allowed some
+ straightline code to appear before the cost label until a later
+ stage of the compiler, but we must move the requirement forward to
+ fit with the structured traces.}
+% Damn it, I should have just moved the cost label forwards in RTLabs,
+% like the prototype does in RTL to ERTL; the result would have been
+% simpler. Or was there some reason not to do that?
+(both in the program code and in the execution trace), even if we
+introduce extra steps, for example to store parameters in memory in
+\textsf{Cminor}. Thus we have a version of the call simulation
+that deals with both in one result.
+
+In addition to the subtrace we are interested in measuring we must
+also prove that the earlier part of the trace is also preserved in
+order to use the simulation from the initial state. It also
+guarantees that we do not run out of stack space before the subtrace
+we are interested in. The lemmas for this prefix and the measurable
+subtrace are similar, following the pattern above. However, the
+measurable subtrace also requires us to rebuild the termination
+proof. This has a recursive form:
+\begin{lstlisting}[language=matita]
+let rec will_return_aux C (depth:nat)
+ (trace:list (cs_state … C × trace)) on trace : bool :=
+match trace with
+[ nil $\Rightarrow$ false
+ cons h tl $\Rightarrow$
+ let $\langle$s,tr$\rangle$ := h in
+ match cs_classify C s with
+ [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl
+  cl_return $\Rightarrow$
+ match depth with
+ [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true  _ $\Rightarrow$ false ]
+  S d $\Rightarrow$ will_return_aux C d tl
+ ]
+  _ $\Rightarrow$ will_return_aux C depth tl
+ ]
+].
+\end{lstlisting}
+The \lstinline'depth' is the number of return states we need to see
+before we have returned to the original function (initially zero) and
+\lstinline'trace' the measurable subtrace obtained from the running
+the semantics for the correct number of steps. This definition
+unfolds tail recursively for each step, and once the corresponding
+simulation result has been applied a new one for the target can be
+asserted by unfolding and applying the induction hypothesis on the
+shorter trace.
+
+This then gives us an overall result for any simulation fitting the
+requirements above (contained in the \lstinline'meas_sim' record):
+\begin{lstlisting}[language=matita]
+theorem measured_subtrace_preserved :
+ $\forall$MS:meas_sim.
+ $\forall$p1,p2,m,n,stack_cost,max.
+ ms_compiled MS p1 p2 $\rightarrow$
+ measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$
+ $\exists$m',n'.
+ measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$
+ observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
+\end{lstlisting}
+The stack space requirement that is embedded in \lstinline'measurable'
+is a consequence of the preservation of observables.
+
+TODO: how to deal with untidy edges wrt to sim rel; anything to
+say about obs?
+
+TODO: say something about termination measures; cost labels are
+statements/exprs in these languages; split call/return gives simpler
+simulations
\subsection{Simulation results for each pass}
@@ 472,5 +586,5 @@
\section{Existence of a structured trace}
\label{sec:structuretrace}
+\label{sec:structuredtrace}
TODO: design, basic structure from termination proof, how cost