source: Papers/itp-2013/ccexec2.tex @ 3442

Last change on this file since 3442 was 3369, checked in by sacerdot, 6 years ago

submitted

File size: 129.0 KB
RevLine 
[3366]1\documentclass[bookmarksdepth=2,bookmarksopen,envcountsame]{llncs}
[3343]2\usepackage{hyperref}
3\usepackage{graphicx}
4\usepackage{color}
5\usepackage{listings}
6\usepackage{bcprules}%\bcprulessavespace
7\usepackage{verbatim}
8\usepackage{alltt}
9\usepackage{subcaption}
10\usepackage{listings}
[3347]11\usepackage{amssymb,amsmath}
[3343]12% \usepackage{amsmath}
13\usepackage{multicol}
14
15\providecommand{\eqref}[1]{(\ref{#1})}
16
17% NB: might be worth removing this if changing class in favour of
18% a built-in definition.
19%\newtheorem{theorem}{Theorem}
[3366]20% \usepackage{aliascnt} %% this will make autoref give correct names
21% \def\mynewtheorem#1[#2]#3{%
22%   \newaliascnt{#1}{#2}%
23%   \newtheorem{#1}[#1]{#3}%
24%   \aliascntresetthe{#1}%
25%   \expandafter\def\csname #1autorefname\endcsname{#3}%
26% }
27% \let\proof\relax
28% \let\endproof\relax
29% \usepackage{amsthm}
30% theorem environments
31% \theoremstyle{definition}
32\spnewtheorem{condition}[theorem]{Condition}{\bfseries}{}
[3343]33
34\lstdefinelanguage{coq}
35  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
36   morekeywords={[2]if,then,else,forall,Prop,match,with,end,let},
37  }
38
39\lstdefinelanguage[mine]{C}[ANSI]{C}{
40  morekeywords={int8_t},
[3347]41  mathescape,
42  escapechar=\%
[3343]43}
44
[3347]45\newcommand\LSTfont{\tt\fontsize{8}{8.2}\selectfont}
46
47\lstset{language=[mine]C,basicstyle=\LSTfont,breaklines=false,
48%         keywordstyle=\color{red}\bfseries,
49%         keywordstyle=[2]\color{blue},
50%         commentstyle=\color{green},
51%         stringstyle=\color{blue},
[3343]52        showspaces=false,showstringspaces=false,
[3347]53%         xleftmargin=1em
54        }
[3343]55
56\usepackage{tikz}
57\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes}
58\makeatletter
59\pgfutil@ifundefined{pgf@arrow@code@implies}{% supply for lack of double arrow special arrow tip if it is not there%
60  \pgfarrowsdeclare{implies}{implies}%
61  {%
62  \pgfarrowsleftextend{2.2pt}%
63  \pgfarrowsrightextend{2.2pt}%
64  }%
65  {%
66    \pgfsetdash{}{0pt} % do not dash%
67    \pgfsetlinewidth{.33pt}%
68    \pgfsetroundjoin   % fix join%
69    \pgfsetroundcap    % fix cap%
70    \pgfpathmoveto{\pgfpoint{-1.5pt}{2.5pt}}%
71    \pgfpathcurveto{\pgfpoint{-.75pt}{1.5pt}}{\pgfpoint{0.5pt}{.5pt}}{\pgfpoint{2pt}{0pt}}%
72    \pgfpathcurveto{\pgfpoint{0.5pt}{-.5pt}}{\pgfpoint{-.75pt}{-1.5pt}}{\pgfpoint{-1.5pt}{-2.5pt}}%
73    \pgfusepathqstroke%
74  }%
75}{}%
76\makeatother
77
78\tikzset{state/.style={inner sep = 0, outer sep = 2pt, draw, fill},
79         every node/.style={inner sep=2pt},
80         every on chain/.style = {inner sep = 0, outer sep = 2pt},
81         join all/.style = {every on chain/.append style={join}},
82         on/.style={on chain={#1}, state},
83         m/.style={execute at begin node=$, execute at end node=$},
84         node distance=3mm,
85         is other/.style={circle, minimum size = 3pt, state},
86         other/.style={on, is other},
87         is jump/.style={diamond, minimum size = 6pt, state},
88         jump/.style={on, is jump},
89         is call/.style={regular polygon, regular polygon sides=3, minimum size=5pt, state},
90         call/.style={on=going below, is call, node distance=6mm, label=above left:$#1$},
91         is ret/.style={regular polygon, regular polygon sides=3, minimum size=5pt, shape border rotate=180, state},
92         ret/.style={on=going above, is ret, node distance=6mm},
93         chain/.style={start chain=#1 going left},
94         rev ar/.style={stealth-, thick},
95         ar/.style={-stealth, thick},
96         every join/.style={rev ar},
97         vcenter/.style={baseline={([yshift=-.5ex]current bounding box)}},
98         every picture/.style={thick},
99         double equal sign distance/.prefix style={double distance=1.5pt}, %% if already defined (newest version of pgf) it should be ignored%}
100         implies/.style={double, -implies, thin, double equal sign distance, shorten <=5pt, shorten >=5pt},
101         new/.style={densely dashed},
[3359]102         newn/.style={solid, fill=white},
[3343]103         rel/.style={font=\scriptsize, fill=white, inner sep=2pt},
104         diag/.style={row sep={11mm,between origins},
105                      column sep={11mm,between origins},
[3348]106                      every node/.style={execute at begin node=$, execute at end node=$},
107%                       every node/.style={draw, is other},
108                      },
[3343]109         small vgap/.style={row sep={7mm,between origins}},
[3348]110         small hgap/.style={column sep={7mm,between origins}},
111         small gap/.style={small vgap, small hgap},
[3343]112         % for article, maybe temporary
113         is jump/.style=is other,
114         is call/.style=is other,
115         is ret/.style=is other,
116}
117
118\def\L{\mathrel{\mathcal L}}
119\def\S{\mathrel{\mathcal S}}
120\def\R{\mathrel{\mathcal R}}
121\def\C{\mathrel{\mathcal C}}
[3366]122\def\LS{\mathrel{\mathcal{L_S}}}
[3343]123
[3347]124\def\Labels{\mathbb L}
125\def\Functions{\mathbb F}
126
[3343]127\newsavebox{\execbox}
128\savebox{\execbox}{\tikz[baseline=-.5ex]\draw [-stealth] (0,0) -- ++(1em, 0);}
[3359]129% \newcommand{\exec}{\ensuremath{\mathrel{\usebox{\execbox}}}}
130\newcommand{\exec}{\to}
[3347]131\let\ar\triangleright
[3359]132\renewcommand{\verb}{\lstinline[mathescape,basicstyle=\tt\selectfont,
133                                identifierstyle=\texttt]}
[3343]134
[3359]135\let\class\colon
[3343]136\let\andalso\quad
137
138\newcommand{\append}{\mathbin{@}}
139\newcommand{\iffdef}{\mathrel{:\Leftrightarrow}}
[3347]140\newcommand{\Deltacost}{\Delta\verb+cost+}
[3343]141
[3347]142\let\oldto\to
143\makeatletter
144\def\to{\@ifnextchar[{\new@to}{\oldto}}
145\def\new@to[#1]{\xrightarrow{#1}}
[3366]146% \def\st@ck#1[#2]{\stackrel{#2}{#1}}
147% \def\defst@ck#1#2{\def#1{\@ifnextchar[{\st@ck#2}{#2}}}
148\let\To\implies
149% \let\MeasTo\rightsquigarrow
[3347]150\makeatother
151
152
[3343]153\begin{document}
154\pagestyle{plain}
155
156\title{Certification of the Preservation of Structure by a Compiler's Back-end Pass\thanks{The project CerCo acknowledges the financial support of the Future and
157Emerging Technologies (FET) programme within the Seventh Framework
158Programme for Research of the European Commission, under FET-Open grant
159number: 243881}}
160\author{Paolo Tranquilli \and Claudio Sacerdoti Coen}
161\institute{Department of Computer Science and Engineering, University of Bologna,\\\email{Paolo.Tranquilli@unibo.it}, \email{Claudio.SacerdotiCoen@unibo.it}}
162\maketitle
163\begin{abstract}
164The labelling approach is a technique to lift cost models for non-functional
165properties of programs from the object code to the source code. It is based
166on the preservation of the structure of the high level program in every
167intermediate language used by the compiler. Such structure is captured by
168observables that are added to the semantics and that needs to be preserved
169by the forward simulation proof of correctness of the compiler. Additional
170special observables are required for function calls. In this paper we
171present a generic forward simulation proof that preserves all these observables.
172The proof statement is based on a new mechanised semantics that traces the
173structure of execution when the language is unstructured. The generic semantics
174and simulation proof have been mechanised in the interactive theorem prover
175Matita.
176\end{abstract}
177
178\section{Introduction}
179The \emph{labelling approach} has been introduced in~\cite{easylabelling} as
180a technique to \emph{lift} cost models for non-functional properties of programs
181from the object code to the source code. Examples of non-functional properties
182are execution time, amount of stack/heap space consumed and energy required for
[3355]183communication. The basic premise of the approach is that it is impossible to
[3343]184provide a \emph{uniform} cost model for an high level language that is preserved
185\emph{precisely} by a compiler. For instance, two instances of an assignment
186$x = y$ in the source code can be compiled very differently according to the
187place (registers vs stack) where $x$ and $y$ are stored at the moment of
188execution. Therefore a precise cost model must assign a different cost
189to every occurrence, and the exact cost can only be known after compilation.
190
191According to the labelling approach, the compiler is free to compile and optimise
192the source code without any major restriction, but it must keep trace
193of what happens to basic blocks during the compilation. The cost model is
194then computed on the object code. It assigns a cost to every basic block.
195Finally, the compiler propagates back the cost model to the source level,
196assigning a cost to each basic block of the source code.
197
198Implementing the labelling approach in a certified compiler
199allows to reason formally on the high level source code of a program to prove
200non-functional properties that are granted to be preserved by the compiler
201itself. The trusted code base is then reduced to 1) the interactive theorem
202prover (or its kernel) used in the certification of the compiler and
2032) the software used to certify the property on the source language, that
204can be itself certified further reducing the trusted code base.
205In~\cite{easylabelling} the authors provide an example of a simple
206certified compiler that implements the labelling approach for the
[3347]207imperative \verb+While+ language~\cite{while}, that does not have
[3343]208pointers and function calls.
209
210The labelling approach has been shown to scale to more interesting scenarios.
211In particular in~\cite{functionallabelling} it has been applied to a functional
212language and in~\cite{loopoptimizations} it has been shown that the approach
213can be slightly complicated to handle loop optimisations and, more generally,
214program optimisations that do not preserve the structure of basic blocks.
215On-going work also shows that the labelling approach is also compatible with
216the complex analyses required to obtain a cost model for object code
217on processors that implement advanced features like pipelining, superscalar
218architectures and caches.
219
[3355]220In the European Project CerCo (Certified Complexity\footnote{\url{http://cerco.cs.unibo.it}})~\cite{cerco} we are certifying a labelling approach based compiler for a large subset of C to
[3343]2218051 object code. The compiler is
222moderately optimising and implements a compilation chain that is largely
223inspired to that of CompCert~\cite{compcert1,compcert2}. Compared to work done in~\cite{easylabelling}, the main novelty and source of difficulties is due to the presence
224of function calls. Surprisingly, the addition of function calls require a
225revisitation of the proof technique given in~\cite{easylabelling}. In
226particular, at the core of the labelling approach there is a forward
[3347]227simulation proof that, in the case of \verb+While+, is only minimally
[3343]228more complex than the proof required for the preservation of the
229functional properties only. In the case of a programming language with
230function calls, instead, it turns out that the forward simulation proof for
[3355]231the back-end languages, which are unstructured, must grant a whole new set of invariants.
[3343]232
233In this paper we present a formalisation in the Matita interactive theorem
234prover~\cite{matita1,matita2} of a generic version of the simulation proof required for unstructured
235languages. All back-end languages of the CerCo compiler are unstructured
236languages, so the proof covers half of the correctness of the compiler.
237The statement of the generic proof is based on a new semantics
238for imperative unstructured languages that is based on \emph{structured
[3367]239execution fragments} and that restores the preservation of structure in the observables of
[3343]240the semantics. The generic proof allows to almost completely split the
241part of the simulation that deals with functional properties only from the
242part that deals with the preservation of structure.
243
[3366]244The plan of this paper is the following. In Section~\ref{sec:labelling} we
[3369]245summarise the labelling method. In Section~\ref{extension} we scale
[3368]246the method to unstructured languages with function calls. In
247Section~\ref{sec:simulation} we give the necessary condition for the
248correctness of the compiler (forward simulation proof).
[3369]249Section~\ref{sec:formalization} sketches the formalisation of the
[3368]250datastructures and proofs in Matita.
[3366]251Conclusions and future works are in Section~\ref{sec:conclusions}
[3343]252
253\section{The labelling approach}
[3366]254\label{sec:labelling}
[3347]255% \subsection{A brief introduction to the labelling approach}
[3356]256We briefly explain the labelling approach as introduced in~\cite{easylabelling}
257on the example in \autoref{examplewhile}.
[3347]258The user wants to analyse the execution time of the program (the black lines in
259\autoref{subfig:example_input}). He compiles the program using
[3344]260a special compiler that first inserts in the code three label emission
[3357]261statements (\verb+EMIT $L_i$+) to mark the beginning of basic blocks
[3356]262(\autoref{subfig:example_input});
[3347]263then the compiler compiles the code to machine code (\autoref{subfig:example_oc}),
264granting that the execution of the source and object
[3344]265code emits the same sequence of labels ($L_1; L_2; L_2; L_3$ in the example).
266This is achieved by keeping track of basic blocks during compilation, avoiding
[3369]267all optimisations that alter the control flow. The latter can be recovered with
[3356]268a more refined version of the labelling approach~\cite{loopoptimizations}, but in the
[3344]269present paper we stick to this simple variant for simplicity. Once the object
[3369]270code is produced, the compiler runs a static code analyser to associate to
[3344]271each label $L_1, \ldots, L_3$ the cost (in clock cycles) of the instructions
272that belong to the corresponding basic block. For example, the cost $k_1$
273associated to $L_1$ is the number of cycles required to execute the block
[3357]274$I_3$ and \verb+COND $l_2$+, while the cost $k_2$ associated to $L_2$ counts the
275cycles required by the block $I_4$, \verb+GOTO $l_1$+ and \verb+COND $l_2$+. The compiler also guarantees
[3344]276that every executed instruction is in the scope of some code emission label,
277that each scope does not contain loops (to associate a finite cost), and that
278both branches of a conditional statement are followed by a code emission
279statement. Under these assumptions it is true that the total execution cost
280of the program $\Delta_t$ is equal to the sum over the sequence of emitted
281labels of the cost associated to every label:
[3347]282$\Delta_t = k(L_1; L_2; L_2; L_3) = k_1 + k_2 + k_2 + k_3$.
[3344]283Finally, the compiler emits an instrumented version of the source code
[3347]284(\autoref{subfig:example_instrument}) where label emission statements are replaced
285by increments of a global variable \verb+cost+ that, before every increment, holds the
[3344]286exact number of clock cycles spent by the microprocessor so far:
[3347]287the difference $\Deltacost$ between the final and initial value of the
288internal clock is $\Deltacost = k_1 + k_2 + k_2 + k_3 = \Delta_t$. Finally, the
[3344]289user can employ any available method (e.g. Hoare logic, invariant generators,
[3347]290abstract interpretation and automated provers) to certify that $\Deltacost$
[3344]291never exceeds a certain bound~\cite{cerco}, which is now a functional property
292of the code.
[3356]293
294\vspace{-0.5cm}
295\begin{figure}[!h]
[3347]296\begin{subfigure}[t]{.32\linewidth}
297\begin{lstlisting}[moredelim={[is][\color{red}]{|}{|}}]
[3357]298|EMIT $L_1$;|
[3347]299$I_1$;
300for (i=0; i<2; i++) {
[3357]301  |EMIT $L_2$;|
[3347]302  $I_2$;
303}
[3357]304|EMIT $L_3$;|
[3347]305\end{lstlisting}
306\caption{The input program (black lines) with its labelling (red lines).}
307\label{subfig:example_input}
308\end{subfigure}
309\hfill
310\begin{subfigure}[t]{.23\linewidth}
311\begin{lstlisting}
[3357]312   EMIT $L_1$
313   $I_3$
314$l_1$:$\!$  COND $l_2$
315   EMIT $L_2$
316   $I_4$
317   GOTO $l_1$
318$l_2$:$\!$  EMIT $L_3$
[3347]319\end{lstlisting}
320\caption{The output labelled object code.}
321\label{subfig:example_oc}
322\end{subfigure}
323\hfill
324\begin{subfigure}[t]{.32\linewidth}
325\begin{lstlisting}
326cost += $k_1$;
327$I_1$;
328for (i=0; i<2; i++) {
[3357]329  cost += $k_2$;
[3347]330  $I_2$;
331}
332cost += $k_3$;           
333\end{lstlisting}
334\caption{The output instrumented code.}
335\label{subfig:example_instrument}
336\end{subfigure}
337% \begin{verbatim}
338% EMIT L_1;                         EMIT L_1         cost += k_1;
339% I_1;                              I_3              I_1;
340% for (i=0; i<2; i++) {        l_1: COND l_2         for (i=0; i<2; i++) {
341%   EMIT L_2;                       EMIT L_2           cost += k_2;           
342%   I_2;                            I_4                I_2;               
343%  }                                GOTO l_1          }                   
344% EMIT L_3;                    l_2: EMIT L_3         cost += k_3;           
345% \end{verbatim}
346\caption{The labelling approach applied to a simple program.\label{examplewhile}. The $I_i$ are sequences of instructions not containing jumps or loops. }
347\end{figure}
[3344]348
[3356]349\section{Extending the labelling approach to function calls}
[3368]350\label{extension}
[3347]351%
[3344]352Let's now consider a simple program written in C that contains a function
[3347]353pointer call inside the scope of the cost label $L_1$, in \autoref{subfig:call_input}.
[3344]354The labelling method works exactly as before, inserting
[3347]355code emission statements/\verb+cost+ variable increments at the beginning
[3344]356of every basic block and at the beginning of every function. The compiler
357still grants that the sequence of labels observed on the two programs are
[3347]358the same. A new difficulty appears when the compiler needs to statically
[3369]359analyse the object code to assign a cost to every label. What should the scope
[3347]360of the $L_1$ label be? After executing the $I_4$ block, the \verb+CALL+
[3344]361statement passes control to a function that cannot be determined statically.
362Therefore the cost of executing the body must be paid by some other label
363(hence the requirement that every function starts with a code emission
364statement). What label should pay for the cost for the block $I_5$? The only
365reasonable answer is $L_1$, i.e. \emph{the scope of labels should extend to the
[3347]366next label emission statement or the end of the function, stepping over function calls}.
367%
368\begin{figure}
369{}\hfill
370\begin{subfigure}[t]{.45\linewidth}
371\centering
372\begin{lstlisting}[xleftmargin=20pt]
373void main() {
[3356]374  EMIT $L_1$;
[3347]375  $I_1$;
376  (*f)();
377  $I_2$;
378}
[3356]379
[3347]380void g() {
[3356]381  EMIT $L_2$;
[3347]382  $I_3$;
383}
384\end{lstlisting}
385\caption{The input labelled C program.}
386\label{subfig:call_input}
387\end{subfigure}
388\hfill
389\begin{subfigure}[t]{.45\linewidth}
390\centering
391\begin{lstlisting}[xleftmargin=20pt]
392main:
[3356]393  EMIT $L_1$
[3347]394  $I_4$
395  CALL
396  $I_5$
397  RETURN
[3356]398
[3347]399g:
[3356]400  EMIT $L_2$
[3347]401  $I_6$
402  RETURN
403\end{lstlisting}
404\caption{The output labelled object code.}
405\label{subfig:call_output}
406\end{subfigure}
407\hfill{}
408\caption{An example compilation of a simple program with a function pointer
409         call.}
410\label{subfig:call_example}
411\end{figure}
[3344]412
[3369]413The latter definition of scope is adequate on the source level because
[3344]414C is a structured language that guarantees that every function call, if it
415returns, passes control to the first instruction that follows the call. However,
416this is not guaranteed for object code, the backend languages of a compiler
417and, more generally, for unstructured
418languages that use a writable control stack to store the return address of
419calls. For example, $I_6$ could increment by $1$ the return address on the
[3347]420stack so that the next \verb+RETURN+ would start at the second instruction
[3344]421of $I_5$. The compiler would still be perfectly correct if a random, dead
[3356]422code instruction was added after the \verb+CALL+ as the first instruction of $I_5$. More generally,
[3344]423\emph{there is no guarantee that a correct compiler that respects the functional
424behaviour of a program also respects the calling structure of the source code}.
425Without such an assumption, however, it may not be true that the execution cost
426of the program is the sum of the costs associated to the labels emitted. In our
427example, the cost of $I_5$ is paid by $L_1$, but in place of $I_5$ the processor could execute any other code after $g$ returns.
428
429Obviously, any reasonably written compiler produces object code that behaves
430as if the language was structured (i.e. by properly nesting function
431calls/returns and without tampering with the return addresses on the control
432stack). This property, however, is a property of the runs of object code
433programs, and not a property of the object code that can be easily statically
[3366]434verified (as the ones required in \autoref{sec:labelling} in absence of function calls).
[3344]435Therefore, we now need to single out those runs whose cost behaviour can be
436statically predicted, and we need to prove that every run of programs generated
437by our compiler are of that type. We call them \emph{structured} since their
438main property is to respect properties that hold for free on the source code
[3347]439because of structure. Moreover, in order to avoid proving
[3344]440too many preservation properties of our compiler, we drop the original
[3369]441requirements on the object code (all instructions must be in scope of some labels,
[3347]442no loops inside a scope, etc.) in favour of the corresponding requirement
443for structured runs (a structured run must start with a label emission, no
444instruction can be executed twice between two emissions, etc.).
[3344]445
446We will therefore proceed as follows. In the following section
4471) we formally introduce the notion of
[3367]448structured execution fragment, which captures structured runs in the style of labelled
[3344]449transition systems; 2) we show that on the object code we can correctly
450compute the execution time of a structured run from the sequence of labels
[3356]451observed; 3) we show that on the source code we can correctly compute the
[3344]452execution time of a program if the compiler produces object code whose
[3356]453runs are weakly similar to the source code runs and structured.
[3344]454
[3356]455The proof of correctness of such a compiler is harder than a traditional
456proof of preservation of functional properties, and a standard forward
[3366]457simulation argument does not work. In \autoref{sec:simulation} we present
[3356]458a refinement of forward simulation that grants all required correctness
459properties.
[3344]460
[3369]461All the definitions and theorems presented in the paper have been formalised
[3344]462in the interactive theorem prover Matita and are being used to certify
463the complexity preserving compiler developed in the CerCo project~\cite{cerco}.
[3369]464The formalisation heavily relies on algebraic and dependent types. In the
[3367]465first part of the paper
[3369]466we did not try to stay close to the formalisation. On the contrary,
[3344]467the definitions given in the paper are the result of a significant
468simplification effort for
469the sake of presentation and to make easier the re-implementation of the
470concepts in a proof assistant which is not based on the Calculus of Inductive
[3369]471Constructions. In any case the formalisation, briefly presented at the end of
[3367]472the paper, is heavily commented to allow the
[3369]473reader to understand the technical details of the formalisation.
[3344]474
475
[3347]476% @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
477%
478% We briefly sketch here a simplified version of the labelling approach as
479% introduced in~\cite{easylabelling}. The simplification strengthens the
480% sufficient conditions given in~\cite{easylabelling} to allow a simpler
481% explanation. The simplified conditions given here are also used in the
482% CerCo compiler to simplify the proof.
483%
484% Let $\mathcal{P}$ be a programming language whose semantics is given in
485% terms of observables: a run of a program yields a finite or infinite
486% stream of observables. We also assume for the time being that function
487% calls are not available in $\mathcal{P}$. We want to associate a cost
488% model to a program $P$ written in $\mathcal{P}$. The first step is to
489% extend the syntax of $\mathcal{P}$ with a new construct $\verb+emit L+$
490% where $L$ is a label distinct from all observables of $\mathcal{P}$.
491% The semantics of $\verb+emit L+$ is the emission of the observable
492% \verb+L+ that is meant to signal the beginning of a basic block.
493%
494% There exists an automatic procedure that injects into the program $P$ an
495% $\verb+emit L+$ at the beginning of each basic block, using a fresh
496% \verb+L+ for each block. In particular, the bodies of loops, both branches
497% of \verb+if-then-else+s and the targets of \verb+goto+s must all start
498% with an emission statement.
499%
500% Let now $C$ be a compiler from $\mathcal{P}$ to the object code $\mathcal{M}$,
501% that is organised in passes. Let $\mathcal{Q}_i$ be the $i$-th intermediate
502% language used by the compiler. We can easily extend every
503% intermediate language (and its semantics) with an $\verb+emit L+$ statement
504% as we did for $\mathcal{P}$. The same is possible for $\mathcal{M}$ too, with
505% the additional difficulty that the syntax of object code is given as a
506% sequence of bytes. The injection of an emission statement in the object code
507% can be done using a map that maps two consecutive code addresses with the
508% statement. The intended semantics is that, if $(pc_1,pc_2) \mapsto \verb+emit L+$ then the observable \verb+L+ is emitted after the execution of the
509% instruction stored at $pc_1$ and before the execution of the instruction
510% stored at $pc_2$. The two program counters are necessary because the
511% instruction stored at $pc_1$ can have multiple possible successors (e.g.
512% in case of a conditional branch or an indirect call). Dually, the instruction
513% stored at $pc_2$ can have multiple possible predecessors (e.g. if it is the
514% target of a jump).
515%
516% The compiler, to be functionally correct, must preserve the observational
517% equivalence, i.e. executing the program after each compiler pass should
518% yield the same stream of observables. After the injection of emission
519% statements, observables now capture both functional and non-functional
520% behaviours.
521% This correctness property is called in the literature a forward simulation
522% and is sufficient for correctness when the target language is
523% deterministic~\cite{compcert3}.
524% We also require a stronger, non-functional preservation property: after each
525% pass all basic blocks must start with an emission statement, and all labels
526% \verb+L+ must be unique.
527%
528% Now let $M$ be the object code obtained for the program $P$. Let us suppose
529% that we can statically inspect the code $M$ and associate to each basic block
530% a cost (e.g. the number of clock cycles required to execute all instructions
531% in the basic block, or an upper bound to that time). Every basic block is
532% labelled with an unique label \verb+L+, thus we can actually associate the
533% cost to \verb+L+. Let call it $k(\verb+L+)$.
534%
535% The function $k$ is defined as the cost model for the object code control
536% blocks. It can be equally used as well as the cost model for the source
537% control blocks. Indeed, if the semantics of $P$ is the stream
538% $L_1 L_2 \ldots$, then, because of forward simulation, the semantics of $M$ is
539% also $L_1 L_2 \ldots$ and its actual execution cost is $\Sigma_i k(L_i)$ because
540% every instruction belongs to a control block and every control block is
541% labelled. Thus it is correct to say that the execution cost of $P$ is also
542% $\Sigma_i k(L_i)$. In other words, we have obtained a cost model $k$ for
543% the blocks of the high level program $P$ that is preserved by compilation.
544%
545% How can the user profit from the high level cost model? Suppose, for instance,
546% that he wants to prove that the WCET of his program is bounded by $c$. It
547% is sufficient for him to prove that $\Sigma_i k(L_i) \leq c$, which is now
548% a purely functional property of the code. He can therefore use any technique
549% available to certify functional properties of the source code.
550% What is suggested in~\cite{easylabelling} is to actually instrument the
551% source code $P$ by replacing every label emission statement
552% $\verb+emit L+$ with the instruction $\verb+cost += k(L)+$ that increments
553% a global fresh variable \verb+cost+. The bound is now proved by establishing
554% the program invariant $\verb+cost+ \leq c$, which can be done for example
555% using the Frama-C~\cite{framaC} suite if the source code is some variant of
556% C.
557%
558% In order to extend the labelling approach to function calls we make
559% \verb+CALL f+ emit the observable \verb+f+ and \verb+RET+ emit a distinguished observable
560% \verb+ret+.
561%
562% For example the following execution history of the program in \autoref{fig:esempio}
[3359]563% $$I_1; \verb+CALL f+; \verb+COND l+; \verb+EMIT $L_2$+; I_3; \verb+RET+; I_2; \verb+RET+$$
[3347]564% emits the trace
565% $$\verb+main+, \verb+f+$$
566% \begin{figure}
567% \hfil
568% \begin{minipage}{.2\linewidth}
569% \begin{lstlisting}
570% main: $\!I_1$
571%       CALL f
572%       $I_2$
573%       RET
574% \end{lstlisting}
575% \end{minipage}
576% \begin{minipage}{.1\linewidth}
577% \begin{lstlisting}
578% main
579% main
580% main
581% main
582% \end{lstlisting}
583% \end{minipage}
584% \hfil
585% \begin{minipage}{.2\linewidth}
586% \begin{lstlisting}
587% f: $\!$COND l
[3359]588%    EMIT $L_2$
[3347]589%    RET
[3359]590% l: $\!$EMIT $L_3$
[3347]591%    $I_3$
592%    RET
593% \end{lstlisting}
594% \end{minipage}
595% \begin{minipage}{.1\linewidth}
596% \begin{lstlisting}
597% f
598%
[3359]599% $L_2$
[3347]600%
[3359]601% $L_3$
602% $L_3$
[3347]603% \end{lstlisting}
604% \end{minipage}
605% \hfil{}
606% \caption{}
607% \label{fig:esempio}
608% \end{figure}
609%
610%
611% \subsection{Labelling function calls}
612% We now want to extend the labelling approach to support function calls.
613% On the high level, \emph{structured} programming language $\mathcal{P}$ there
614% is not much to change.
615% When a function is invoked, the current basic block is temporarily exited
616% and the basic block the function starts with take control. When the function
617% returns, the execution of the original basic block is resumed. Thus the only
618% significant change is that basic blocks can now be nested. Let \verb+E+
619% be the label of the external block and \verb+I+ the label of a nested one.
620% Since the external starts before the internal, the semantics observed will be
621% \verb+E I+ and the cost associated to it on the source language will be
622% $k(\verb+E+) + k(\verb+I+)$, i.e. the cost of executing all instructions
623% in the block \verb+E+ first plus the cost of executing all the instructions in
624% the block \verb+I+. However, we know that some instructions in \verb+E+ are
625% executed after the last instruction in \verb+I+. This is actually irrelevant
626% because we are here assuming that costs are additive, so that we can freely
627% permute them\footnote{The additivity assumption fails on modern processors that have stateful subsystems, like caches and pipelines. The extension of the labelling approach to those systems is therefore non trivial and under development in the CerCo project.}. Note that, in the present discussion, we are assuming that
628% the function call terminates and yields back control to the basic block
629% \verb+E+. If the call diverges, the instrumentation
630% $\verb+cost += k(E)+$ executed at the beginning of \verb+E+ is still valid,
631% but just as an upper bound to the real execution cost: only precision is lost.
632%
633% Let now consider what happens when we move down the compilation chain to an
634% unstructured intermediate or final language. Here unstructured means that
635% the only control operators are conditional and unconditional jumps, function
636% calls and returns. Unlike a structured language, though, there is no guarantee
637% that a function will return control just after the function call point.
638% The semantics of the return statement, indeed, consists in fetching the
639% return address from some internal structure (typically the control stack) and
640% jumping directly to it. The code can freely manipulate the control stack to
641% make the procedure returns to whatever position. Indeed, it is also possible
642% to break the well nesting of function calls/returns.
643%
644% Is it the case that the code produced by a correct compiler must respect the
645% additional property that every function returns just after its function call
646% point? The answer is negative and the property is not implied by forward
647% simulation proofs. For instance, imagine to modify a correct compiler pass
648% by systematically adding one to the return address on the stack and by
649% putting a \verb+NOP+ (or any other instruction that takes one byte) after
650% every function call. The obtained code will be functionally indistinguishable,
651% and the added instructions will all be dead code.
652%
653% This lack of structure in the semantics badly interferes with the labelling
654% approach. The reason is the following: when a basic block labelled with
655% \verb+E+ contains a function call, it no longer makes any sense to associate
656% to a label \verb+E+ the sum of the costs of all the instructions in the block.
657% Indeed, there is no guarantee that the function will return into the block and
658% that the instructions that will be executed after the return will be the ones
659% we are paying for in the cost model.
660%
661% How can we make the labelling approach work in this scenario? We only see two
662% possible ways. The first one consists in injecting an emission statement after
663% every function call: basic blocks no longer contain function calls, but are now
664% terminated by them. This completely solves the problem and allows the compiler
665% to break the structure of function calls/returns at will. However, the
666% technique has several drawbacks. First of all, it greatly augments the number
667% of cost labels that are injected in the source code and that become
668% instrumentation statements. Thus, when reasoning on the source code to prove
669% non-functional properties, the user (or the automation tool) will have to handle
670% larger expressions. Second, the more labels are emitted, the more difficult it
671% becomes to implement powerful optimisations respecting the code structure.
672% Indeed, function calls are usually implemented in such a way that most registers
673% are preserved by the call, so that the static analysis of the block is not
674% interrupted by the call and an optimisation can involve both the code before
675% and after the function call. Third, instrumenting the source code may require
676% unpleasant modification of it. Take, for example, the code
677% \verb+f(g(x));+. We need to inject an emission statement/instrumentation
678% instruction just after the execution of \verb+g+. The only way to do that
679% is to rewrite the code as \verb+y = g(x); emit L; f(y);+ for some fresh
680% variable \verb+y+. It is pretty clear how in certain situations the obtained
681% code would be more obfuscated and then more difficult to manually reason on.
682%
683% For the previous reasons, in this paper and in the CerCo project we adopt a
684% different approach. We do not inject emission statements after every
685% function call. However, we want to propagate a strong additional invariant in
686% the forward simulation proof. The invariant is the propagation of the structure
687%  of the original high level code, even if the target language is unstructured.
688% The structure we want to propagate, that will become more clear in the next
689% section, comprises 1) the property that every function should return just after
690% the function call point, which in turns imply well nesting of function calls;
691% 2) the property that every basic block starts with a code emission statement.
692%
693% In the original labelling approach of~\cite{easylabelling}, the second property
694% was granted syntactically as a property of the generated code.
695% In our revised approach, instead, we will impose the property on the runs:
696% it will be possible to generate code that does not respect the syntactic
697% property, as soon as all possible runs respect it. For instance, dead code will no longer
698% be required to have all basic blocks correctly la. The switch is suggested
699% from the fact that the first of the two properties --- that related to
700% function calls/returns --- can only be defined as property of runs,
701% not of the static code. The switch is
702% beneficial to the proof because the original proof was made of two parts:
703% the forward simulation proof and the proof that the static property was granted.
704% In our revised approach the latter disappears and only the forward simulation
705% is kept.
706%
707% In order to capture the structure semantics so that it is preserved
708% by a forward simulation argument, we need to make the structure observable
709% in the semantics. This is the topic of the next section.
[3344]710
[3367]711\subsection{Structured execution fragments}
[3366]712\label{sec:semantics}
[3345]713
714Let's consider a generic unstructured language already equipped with a
715small step structured operational semantics (SOS). We introduce a
[3358]716deterministic labelled transition system $(S,\Lambda,\to)$
[3345]717that refines the
[3356]718SOS by observing function calls/returns and the beginning of basic blocks.
[3350]719$S$ is the set of states of the program and
[3347]720$\Lambda = \{ \tau, RET \} \cup \Labels \cup \Functions$
721where $\Functions$ is the set of names of functions that can occur in the
722program, $\Labels$ is a set of labels disjoint from $\Functions$
[3348]723and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$. Moreover there
724is an injective function $\ell : \Functions \to \Labels$ that tells the
725starting label of the body of each function, and $\ell(\Functions)\subseteq \Labels$
726denotes the image of this function.
[3347]727The transition function is defined as $s_1 \to[o] s_2$ if
[3350]728$s_1$ moves to $s_2$ according to the SOS and $o = f \in \Functions$ if
[3347]729the function $f$ is called, $o = RET$ if a \verb+RETURN+ is executed,
730$o = L \in \Labels$ if an \verb+EMIT $L$+ is executed to signal the
[3345]731beginning of a basic block, and $o = \tau$ in all other cases.
732Because we assume the language to be deterministic, the label emitted can
[3347]733actually be computed simply observing $s_1$. Finally, $S$ is also endowed with
[3350]734a relation $s\ar s'$ ($s'$ \emph{follows} $s$) that holds when the instruction
735to be executed in $s'$ follows syntactically the one in $s$ in the source program.
[3345]736
[3350]737In the rest of the paper we write $s_0 \to^{*} s_n$ for the finite execution
738fragment $T = s_0 \to[o_0] s_1 \to[o_1] \ldots \to[o_{n-1}] s_n$
739and, we call \emph{weak trace} of $T$ (denoted as $|T|$) the
740subsequence $o_{i_0} \ldots o_{i_m}$ of $o_0 \ldots o_{n-1}$ obtained dropping
741every internal action $\tau$.
742
743%Let $k$ be a cost model for observables actions that maps elements of
744%$\Lambda \setminus \{\tau\}$ to any commutative cost monoid
745%(e.g. natural numbers). We extend the domain of $k$ to executable fragments
746%by posing $k(T) = \Sigma_{o \in |T|} k(o)$.
747
748\paragraph{Structured execution fragments}
[3347]749Among all possible finite execution fragments we want to
[3345]750identify the ones that satisfy the requirements we sketched in the previous
[3347]751section. We say that an execution fragment
[3350]752$s_0 \to^{*} s_n$
753is \emph{structured} (and we denote it as $s_0 \To s_n$) iff the following conditions
[3347]754are met.
[3345]755\begin{enumerate}
[3347]756 \item For every $i$, if $s_i \to[f] s_{i+1}$ then there is a
757   label $L$ and a $k\ge i+2$ such that
[3348]758    $s_{i+1} \to[\ell(f)] s_{i+2} \To s_k \to[RET] s_{k+1}$, with
[3347]759    $s_i \ar s_{k+1}$.
[3348]760   In other words, $s_{i+1}$ must start execution with \verb+EMIT $\ell(f)$+
[3350]761   --- so that no instruction falls outside the scope of every label ---
[3347]762   and then continue with a structured fragment returning control
763   to the instruction immediately following the call.
[3350]764
765   The condition also enforces convergence of every function call, which is
766   necessary to bound the cost of the fragment. Note that
767   non convergent programs may still have structured execution fragments
768   that are worth measuring. For example, we can measure the reaction time
769   of a server implemented as an unbounded loop whose body waits for an
770   input, process it and performs an output before looping: the processing
[3367]771   steps form a structured fragment.
[3347]772 \item The number of $RET$'s in the fragment is equal to the number of
[3350]773   calls performed. In combination with the previous condition, this ensures
[3367]774   well-bracketing of function calls.
[3350]775 \item
776   \label{req3}
777   For every $i$ and $f$, if $s_{i+1}\to[\ell(f)]s_{i+2}$ then
778   $s_i\to[f]s_{i+1}$. This is a technical condition needed to ensure that a
779   label associated with a function is only used at the beginning of its
[3366]780   body. Its use will become clear in~\autoref{sec:simulation}.
[3347]781 \item For every $i$, if the instruction to be executed in $s_i$ is a
782   conditional branch, then there is an $L$ such that $s_{i+1} \to[L] s_{i+2}$ or, equivalently, that $s_{i+1}$ must start execution with an
783   \verb+EMIT $L$+. This captures the requirement that every branch which is
[3350]784   live code must start with a label emission. Otherwise, it would be possible
785   to have conditional instructions whose branches are assigned different
786   costs, making impossible to assign a single cost to the label whose scope
787   contains the jump.
[3345]788\end{enumerate}
[3368]789One might wonder why $f$ and $\ell(f)$, that always appear in this order, are not
[3350]790collapsed into a single observable. This would simplify some aspects of the
791formalisation at the price of others. For example, we should add special
792cases when the fragment starts at the beginning of a function body
793(e.g. the one of \texttt{main}) because in that case nobody would have emitted
[3356]794the observable $\ell(f)$. We plan to compare the two approaches in the future.
[3345]795
[3350]796\paragraph{Measurable execution fragments and their cost prediction.}
[3356]797The first main theorem of CerCo deals with the object code.
[3350]798It states that the execution cost of
799certain execution fragments, that we call \emph{measurable fragments}, can be
800computed from their weak trace by choosing the cost model $k$ that assigns to
801any label the cost (in clock cycles) of the instructions in its scope, and
802$0$ to function calls and $RET$ observables.
[3345]803
[3350]804\begin{theorem}
[3366]805 \label{thm:static}
[3367]806 for all measurable fragment $M = s_0 \to^{*} s_n$,\\
[3368]807 $$\Delta_t := \verb+clock+_{s_n} - \verb+clock+_{s_0} = \Sigma_{o \in |M|} k(o)$$
[3350]808\end{theorem}
[3345]809
[3350]810An execution fragment $s_0 \to^{*} s_n$ is
811measurable if it is structured (up to a possible final \texttt{RETURN}) and
812if it does not start or end in the middle of a basic block.
813Ending in the middle of a block would mean that the last label encountered
814would have pre-paid more instructions than the ones executed; starting in the
815middle would mean not paying any instruction up to the first label emission.
816
817Formally, $s_0 \to^{*} s_n$ is measurable iff $o_0 \in \Labels$ (or equivalently
[3347]818in $s_0$ the program must emit a label) and either
[3350]819$s_0 \To s_{n-1}$ and $s_{n-1}\to[RET]s_n$ or
820$s_0 \To s_n$ and $s_n$ must be a label emission statement.
[3345]821
[3356]822%\textbf{CSC: PROVA----------------------}
[3350]823% The theorem is proved by structural induction over the structured
824% trace, and is based on the invariant that
825% iff the function that computes the cost model has analysed the instruction
826% to be executed at $s_2$ after the one to be executed at $s_1$, and if
827% the structured trace starts with $s_1$, then eventually it will contain also
828% $s_2$. When $s_1$ is not a function call, the result holds trivially because
829% of the $s_1\exec s_2$ condition obtained by inversion on
830% the trace. The only non
831% trivial case is the one of function calls: the cost model computation function
832% does recursion on the first instruction that follows that function call; the
833% \verb+as_after_return+ condition of the \verb+tal_base_call+ and
834% \verb+tal_step_call+ grants exactly that the execution will eventually reach
835% this state.
836
837\paragraph{Weak similarity and cost invariance.}
[3346]838Given two deterministic unstructured programming languages with their own
[3350]839operational semantics, we say that two execution fragments are
840\emph{weakly trace equivalent} if their weak traces are equal.
[3346]841
[3368]842A compiler (pass) that preserves the program semantics also \emph{preserves weak
843traces and propagates measurability} iff for every measurable
[3367]844fragment $M_1 = s_1 \to^{*} s_1'$ of the source code, the corresponding
845execution fragment $M_2 = s_2 \to^{*} s_2'$ of the object code is measurable
846and $M_1$ and $M_2$ are weakly trace equivalent. The very intuitive notion of
[3350]847``corresponding fragment'' is made clear in the forward simulation proof of
848preservation of the semantics of the program by saying that $s_2$ and $s_1$
849are in a certain relation. Clearly the property holds for a compiler if it
850holds for each compiler pass.
851
[3366]852Having proved in~\autoref{thm:static} that the statically computed cost model is
[3350]853accurate for the object code, we get as a corollary that it is also accurate
854for the source code if the compiler preserves weak traces and
[3356]855propagates measurability. Thus, as prescribed by the CerCo's methodology~\cite{fopara}, it becomes possible to compute cost models
[3350]856on the object code, transfer it to the source code and then reason comfortably
857on the source code only.
858
[3366]859\begin{theorem}\label{thm:preservation}
[3350]860Given a compiler that preserves weak traces and propagates measurability,
[3368]861for all measurable execution fragment $M_1 = s_1 \to^{*} s_1'$ of the source
862code such that $M_2 = s_2 \to^{*} s_2'$ is the corresponding fragment of the
[3350]863object code,
864
[3368]865$$\Delta_t := \verb+clock+_{s_2'} - \verb+clock+_{s_2} = \Sigma_{o \in |M_2|} k(o) = \Sigma_{o \in |M_1|} k(o)$$
[3350]866\end{theorem}
867
[3356]868\section{Proving the compiler correctness}
[3366]869\label{sec:simulation}
870Because of \autoref{thm:preservation}, to certify a compiler for the labelling
[3368]871approach we need to prove that it respects the functional semantics of the
872program, preserves weak traces and propagates measurability.
873We achieve this by proving the three properties independently for each compiler
[3356]874pass.
[3358]875The first property is standard and can be proved by means of a forward simulation argument (see for example~\cite{compcert3}) that runs like this.
[3350]876First a relation between the corresponding
[3356]877source and target states is defined. Then a lemma establishes
[3350]878a local simulation condition: given two states in relation, if the source
879one performs one step then the target one performs zero or more steps and
[3369]880the two resulting states are synchronised again according to the relation.
[3356]881No requirements are imposed on the intermediate target states.
[3367]882Finally, the lemma is iterated over the execution fragment to establish the
[3350]883final result.
884
885In principle, preservation of weak traces could be easily shown with the same
886argument (and also at the same time). Surprisingly, propagation of
887measurability cannot. What makes the standard forward
888simulation proof work is the fact that usually a compiler pass performs some
889kind of local or global analysis of the code followed by a compositional, order
890preserving translation of every instruction. In order to produce structured
[3356]891traces, however, code emission cannot be fully compositional any longer,
[3367]892and requirements need to be enforced on intermediate target states too.
[3350]893
894For example, consider~requirement \ref{req3} that asks every function body
895to start with a label emission statement. Some compiler passes must
896add preambles to functions, for example to take care of the parameter passing
897convention. In order to not violate the requirement, the preamble must be
898inserted after the label emission. In the forward simulation proof, however,
899function call steps in the source language are simulated by the new function
900call followed by the execution of the preamble, and only at the end of the
901preamble the reached states are again in the expected relation. In the meantime,
902however, the object code has already performed the label emission statement,
903that still needs to be executed in the source code, breaking forward simulation.
904
905Another reason why the standard argument breaks is due to the requirement that
[3351]906function calls should yield back control after the calling point. Some passes
907need to translate a function call to a function call followed by some
908instructions (for example to restore caller-saved registers in the pass that
[3367]909sets the parameter convention). In the forward simulation proof, these
[3351]910instructions are taken care of when simulating the \texttt{RETURN} step:
911the state just after the return in the source code is matched by the state $s_2$
912after these steps in the object code. However, the aforementioned requirement
[3356]913does not involve $s_2$, but the intermediate state reached after the return in the object
914code. Therefore this requirement too
[3351]915cannot be enforced with the standard forward simulation argument.
[3350]916
[3351]917In this section we present now a modified forward simulation argument that
918can be used to prove at once that a compiler preserves the semantics of the
919program, its weak traces and that the compiler propagates measurability.
[3350]920
[3347]921% @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
[3343]922%
[3347]923% The program semantics adopted in the traditional labelling approach is based
924% on labelled deductive systems. Given a set of observables $\mathcal{O}$ and
925% a set of states $\S$, the semantics of one deterministic execution
926% step is
927% defined as a function $S \to S \times O^*$ where $O^*$ is a (finite) stream of
928% observables. The semantics is then lifted compositionally to multiple (finite
929% or infinite) execution steps.
930% Finally, the semantics of a a whole program execution is obtained by forgetting
931% about the final state (if any), yielding a function $S \to O^*$ that given an
932% initial status returns the finite or infinite stream of observables in output.
[3343]933%
[3347]934% We present here a new definition of semantics where the structure of execution,
935% as defined in the previous section, is now observable. The idea is to replace
936% the stream of observables with a structured data type that makes explicit
937% function call and returns and that grants some additional invariants by
938% construction. The data structure, called \emph{structured traces}, is
939% defined inductively for terminating programs and coinductively for diverging
940% ones. In the paper we focus only on the inductive structure, i.e. we assume
941% that all programs that are given a semantics are total. The Matita formalisation
942% also shows the coinductive definitions. The semantics of a program is then
943% defined as a function that maps an initial state into a structured trace.
944%
945% In order to have a definition that works on multiple intermediate languages,
946% we abstract the type of structure traces over an abstract data type of
947% abstract statuses, which we aptly call $\verb+abstract_status+$. The fields
948% of this record are the following.
949% \begin{itemize}
950%  \item \verb+S : Type[0]+, the type of states.
951%  \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate stating
952%  an execution step. We write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$.
953%  \item \verb+as_classifier : S $\to$ classification+, a function tagging all
954%  states with a class in
955%  $\{\verb+cl_return,cl_jump,cl_call,cl_other+\}$, depending on the instruction
956%  that is about to be executed (we omit tail-calls for simplicity). We will
957%  use $s \class c$ as a shorthand for both $\verb+as_classifier+~s=c$
958%  (if $c$ is a classification) and $\verb+as_classifier+~s\in c$
959%  (if $c$ is a set of classifications).
960%  \item \verb+as_label : S $\to$ option label+, telling whether the
961%  next instruction to be executed in $s$ is a cost emission statement,
962%  and if yes returning the associated cost label. Our shorthand for this function
963%  will be $\ell$, and we will also abuse the notation by using $\ell~s$ as a
964%  predicate stating that $s$ is labelled.
965%  \item \verb+as_call_ident : ($\Sigma$s:S. s $\class$ cl_call) $\to$ label+,
966%  telling the identifier of the function which is being called in a
967%  \verb+cl_call+ state. We will use the shorthand $s\uparrow f$ for
968%  $\verb+as_call_ident+~s = f$.
969%  \item \verb+as_after_return : ($\Sigma$s:S. s $\class$ cl_call) $\to$ S $\to$ Prop+,
970%  which holds on the \verb+cl_call+ state $s_1$ and a state $s_2$ when the
971%  instruction to be executed in $s_2$ follows the function call to be
972%  executed in (the witness of the $\Sigma$-type) $s_1$. We will use the notation
973%  $s_1\ar s_2$ for this relation.
974% \end{itemize}
975%
976% % \begin{alltt}
977% % record abstract_status := \{ S: Type[0];
978% %  as_execute: S \(\to\) S \(\to\) Prop;   as_classifier: S \(\to\) classification;
979% %  as_label: S \(\to\) option label;    as_called: (\(\Sigma\)s:S. c s = cl_call) \(\to\) label;
980% %  as_after_return: (\(\Sigma\)s:S. c s = cl_call) \(\to\) S \(\to\) Prop \}
981% % \end{alltt}
982%
983% The inductive type for structured traces is actually made by three multiple
984% inductive types with the following semantics:
985% \begin{enumerate}
986%  \item $(\verb+trace_label_return+~s_1~s_2)$ (shorthand $\verb+TLR+~s_1~s_2$)
987%    is a trace that begins in
988%    the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
989%    such that the instruction to be executed in $s_1$ is a label emission
990%    statement and the one to be executed in the state before $s_2$ is a return
991%    statement. Thus $s_2$ is the state after the return. The trace
992%    may contain other label emission statements. It captures the structure of
993%    the execution of function bodies: they must start with a cost emission
994%    statement and must end with a return; they are obtained by concatenating
995%    one or more basic blocks, all starting with a label emission
996%    (e.g. in case of loops).
997%  \item $(\verb+trace_any_label+~b~s_1~s_2)$ (shorthand $\verb+TAL+~b~s_1~s_2$)
998%    is a trace that begins in
999%    the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
1000%    such that the instruction to be executed in $s_2$/in the state before
1001%    $s_2$ is either a label emission statement or
1002%    or a return, according to the boolean $b$. It must not contain
1003%    any label emission statement. It captures the notion of a suffix of a
1004%    basic block.
1005%  \item $(\verb+trace_label_label+~b~s_1~s_2)$ (shorthand $\verb+TLL+~b~s_1~s_2$ is the special case of
1006%    $\verb+TAL+~b~s_1~s_2)$ such that the instruction to be
1007%    executed in $s_1$ is a label emission statement. It captures the notion of
1008%    a basic block.
1009% \end{enumerate}
1010%
1011% \begin{multicols}{3}
1012% \infrule[\verb+tlr_base+]
1013%  {\verb+TLL+~true~s_1~s_2}
1014%  {\verb+TLR+~s_1~s_2}
1015%
1016% \infrule[\verb+tlr_step+]
1017%  {\verb+TLL+~false~s_1~s_2 \andalso
1018%   \verb+TLR+~s_2~s_3
1019%  }
1020%  {\verb+TLR+~s_1~s_3}
1021%
1022% \infrule[\verb+tll_base+]
1023%  {\verb+TAL+~b~s_1~s_2 \andalso
1024%   \ell~s_1
1025%  }
1026%  {\verb+TLL+~b~s_1~s_2}
1027% \end{multicols}
1028%
1029% \infrule[\verb+tal_base_not_return+]
1030%  {s_1\exec s_2 \andalso
1031%   s_1\class\{\verb+cl_jump+, \verb+cl_other+\}\andalso
1032%   \ell~s_2
1033%  }
1034%  {\verb+TAL+~false~s_1~s_2}
1035%
1036% \infrule[\verb+tal_base_return+]
1037%  {s_1\exec s_2 \andalso
1038%   s_1 \class \verb+cl_return+
1039%  }
1040%  {\verb+TAL+~true~s_1~s_2}
1041%
1042% \infrule[\verb+tal_base_call+]
1043%  {s_1\exec s_2 \andalso
1044%   s_1 \class \verb+cl_call+ \andalso
1045%   s_1\ar s_3 \andalso
1046%   \verb+TLR+~s_2~s_3 \andalso
1047%   \ell~s_3
1048%  }
1049%  {\verb+TAL+~false~s_1~s_3}
1050%
1051% \infrule[\verb+tal_step_call+]
1052%  {s_1\exec s_2 \andalso
1053%   s_1 \class \verb+cl_call+ \andalso
1054%   s_1\ar s_3 \andalso
1055%   \verb+TLR+~s_2~s_3 \andalso
1056%   \verb+TAL+~b~s_3~s_4
1057%  }
1058%  {\verb+TAL+~b~s_1~s_4}
1059%
1060% \infrule[\verb+tal_step_default+]
1061%  {s_1\exec s_2 \andalso
1062%   \lnot \ell~s_2 \andalso
1063%   \verb+TAL+~b~s_2~s_3\andalso
1064%   s_1 \class \verb+cl_other+
1065%  }
1066%  {\verb+TAL+~b~s_1~s_3}
1067% \begin{comment}
1068% \begin{verbatim}
1069% inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
1070%   | tlr_base:
1071%       ∀status_before: S.
1072%       ∀status_after: S.
1073%         trace_label_label S ends_with_ret status_before status_after →
1074%         trace_label_return S status_before status_after
1075%   | tlr_step:
1076%       ∀status_initial: S.
1077%       ∀status_labelled: S.
1078%       ∀status_final: S.
1079%         trace_label_label S doesnt_end_with_ret status_initial status_labelled →
1080%         trace_label_return S status_labelled status_final →
1081%           trace_label_return S status_initial status_final
1082% with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
1083%   | tll_base:
1084%       ∀ends_flag: trace_ends_with_ret.
1085%       ∀start_status: S.
1086%       ∀end_status: S.
1087%         trace_any_label S ends_flag start_status end_status →
1088%         as_costed S start_status →
1089%           trace_label_label S ends_flag start_status end_status
1090% with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
1091%   (* Single steps within a function which reach a label.
1092%      Note that this is the only case applicable for a jump. *)
1093%   | tal_base_not_return:
1094%       ∀start_status: S.
1095%       ∀final_status: S.
1096%         as_execute S start_status final_status →
1097%         (as_classifier S start_status cl_jump ∨
1098%          as_classifier S start_status cl_other) →
1099%         as_costed S final_status →
1100%           trace_any_label S doesnt_end_with_ret start_status final_status
1101%   | tal_base_return:
1102%       ∀start_status: S.
1103%       ∀final_status: S.
1104%         as_execute S start_status final_status →
1105%         as_classifier S start_status cl_return →
1106%           trace_any_label S ends_with_ret start_status final_status
1107%   (* A call followed by a label on return. *)
1108%   | tal_base_call:
1109%       ∀status_pre_fun_call: S.
1110%       ∀status_start_fun_call: S.
1111%       ∀status_final: S.
1112%         as_execute S status_pre_fun_call status_start_fun_call →
1113%         ∀H:as_classifier S status_pre_fun_call cl_call.
1114%           as_after_return S «status_pre_fun_call, H» status_final →
1115%           trace_label_return S status_start_fun_call status_final →
1116%           as_costed S status_final →
1117%             trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
1118%   (* A call followed by a non-empty trace. *)
1119%   | tal_step_call:
1120%       ∀end_flag: trace_ends_with_ret.
1121%       ∀status_pre_fun_call: S.
1122%       ∀status_start_fun_call: S.
1123%       ∀status_after_fun_call: S.
1124%       ∀status_final: S.
1125%         as_execute S status_pre_fun_call status_start_fun_call →
1126%         ∀H:as_classifier S status_pre_fun_call cl_call.
1127%           as_after_return S «status_pre_fun_call, H» status_after_fun_call →
1128%           trace_label_return S status_start_fun_call status_after_fun_call →
1129%           ¬ as_costed S status_after_fun_call →
1130%           trace_any_label S end_flag status_after_fun_call status_final →
1131%             trace_any_label S end_flag status_pre_fun_call status_final
1132%   | tal_step_default:
1133%       ∀end_flag: trace_ends_with_ret.
1134%       ∀status_pre: S.
1135%       ∀status_init: S.
1136%       ∀status_end: S.
1137%         as_execute S status_pre status_init →
1138%         trace_any_label S end_flag status_init status_end →
1139%         as_classifier S status_pre cl_other →
1140%         ¬ (as_costed S status_init) →
1141%           trace_any_label S end_flag status_pre status_end.
1142% \end{verbatim}
1143% \end{comment}
1144% A \verb+trace_label_return+ is isomorphic to a list of
1145% \verb+trace_label_label+s that ends with a cost emission followed by a
1146% return terminated \verb+trace_label_label+.
1147% The interesting cases are those of $\verb+trace_any_label+~b~s_1~s_2$.
1148% A \verb+trace_any_label+ is a sequence of steps built by a syntax directed
1149% definition on the classification of $s_1$. The constructors of the datatype
1150% impose several invariants that are meant to impose a structure to the
1151% otherwise unstructured execution. In particular, the following invariants are
1152% imposed:
1153% \begin{enumerate}
1154%  \item the trace is never empty; it ends with a return iff $b$ is
1155%        true
1156%  \item a jump must always be the last instruction of the trace, and it must
1157%        be followed by a cost emission statement; i.e. the target of a jump
1158%        is always the beginning of a new basic block; as such it must start
1159%        with a cost emission statement
1160%  \item a cost emission statement can never occur inside the trace, only in
1161%        the status immediately after
1162%  \item the trace for a function call step is made of a subtrace for the
1163%        function body of type
1164%        $\verb+trace_label_return+~s_1~s_2$, possibly followed by the
1165%        rest of the trace for this basic block. The subtrace represents the
1166%        function execution. Being an inductive datum, it grants totality of
1167%        the function call. The status $s_2$ is the one that follows the return
1168%        statement. The next instruction of $s_2$ must follow the function call
1169%        instruction. As a consequence, function calls are also well nested.
1170% \end{enumerate}
1171%
1172% There are three mutual structural recursive functions, one for each of
1173% \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation
1174% $|\,.\,|$: the \emph{flattening} of the traces. These functions
1175% allow to extract from a structured trace the list of emitted cost labels.
1176% %  We only show here the type of one
1177% % of them:
1178% % \begin{alltt}
1179% % flatten_trace_label_return:
1180% %  \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\).
1181% %   trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S)
1182% % \end{alltt}
1183%
1184% \paragraph{Structured traces similarity and cost prediction invariance.}
1185%
1186% A compiler pass maps source to object code and initial states to initial
1187% states. The source code and initial state uniquely determine the structured
1188% trace of a program, if it exists. The structured trace fails to exists iff
1189% the structural conditions are violated by the program execution (e.g. a function
1190% body does not start with a cost emission statement). Let us assume that the
1191% target structured trace exists.
1192%
1193% What is the relation between the source and target structured traces?
1194% In general, the two traces can be arbitrarily different. However, we are
1195% interested only in those compiler passes that maps a trace $\tau_1$ to a trace
1196% $\tau_2$ such that
1197% \begin{equation}|\tau_1| = |\tau_2|.\label{th2}\end{equation}
1198% The reason is that the combination of~\eqref{th1} with~\eqref{th2} yields the
1199% corollary
1200% \begin{equation}\label{th3}
1201% \forall s_1,s_2. \forall \tau: \verb+TLR+~s_1~s_2.~
1202%   \verb+clock+~s_2 - \verb+clock+~s_1 =
1203%   \Sigma_{\alpha \in |\tau_1|}\;k(\alpha) =
1204%   \Sigma_{\alpha \in |\tau_2|}\;k(\alpha).
1205% \end{equation}
1206% This corollary states that the actual execution time of the program can be computed equally well on the source or target language. Thus it becomes possible to
1207% transfer the cost model from the target to the source code and reason on the
1208% source code only.
1209%
1210% We are therefore interested in conditions stronger than~\eqref{th2}.
1211% Therefore we introduce here a similarity relation between traces with
1212% the same structure. Theorem~\verb+tlr_rel_to_traces_same_flatten+
1213% in the Matita formalisation shows that~\eqref{th2} holds for every pair
1214% $(\tau_1,\tau_2)$ of similar traces.
1215%
1216% Intuitively, two traces are similar when one can be obtained from
1217% the other by erasing or inserting silent steps, i.e. states that are
1218% not \verb+as_costed+ and that are classified as \verb+cl_other+.
1219% Silent steps do not alter the structure of the traces.
1220% In particular,
1221% the relation maps function calls to function calls to the same function,
1222% label emission statements to emissions of the same label, concatenation of
1223% subtraces to concatenation of subtraces of the same length and starting with
1224% the same emission statement, etc.
1225%
1226% In the formalisation the three similarity relations --- one for each trace
1227% kind --- are defined by structural recursion on the first trace and pattern
1228% matching over the second. Here we turn
1229% the definition into the inference rules shown in \autoref{fig:txx_rel}
1230% for the sake of readability. We also omit from trace constructors all arguments,
1231% but those that are traces or that
1232% are used in the premises of the rules. By abuse of notation we denote all three
1233% relations by infixing $\approx$.
1234%
1235% \begin{figure}
1236% \begin{multicols}{2}
1237% \infrule
1238%  {tll_1\approx tll_2
1239%  }
1240%  {\verb+tlr_base+~tll_1 \approx \verb+tlr_base+~tll_2}
1241%
1242% \infrule
1243%  {tll_1 \approx tll_2 \andalso
1244%   tlr_1 \approx tlr_2
1245%  }
1246%  {\verb+tlr_step+~tll_1~tlr_1 \approx \verb+tlr_step+~tll_2~tlr_2}
1247% \end{multicols}
1248% \vspace{3ex}
1249% \begin{multicols}{2}
1250% \infrule
1251%  {\ell~s_1 = \ell~s_2 \andalso
1252%   tal_1\approx tal_2
1253%  }
1254%  {\verb+tll_base+~s_1~tal_1 \approx \verb+tll_base+~s_2~tal_2}
1255%
1256% \infrule
1257%  {tal_1\approx tal_2
1258%  }
1259%  {\verb+tal_step_default+~tal_1 \approx tal_2}
1260% \end{multicols}
1261% \vspace{3ex}
1262% \infrule
1263%  {}
1264%  {\verb+tal_base_not_return+\approx taa \append \verb+tal_base_not_return+}
1265% \vspace{1ex}
1266% \infrule
1267%  {}
1268%  {\verb+tal_base_return+\approx taa \append \verb+tal_base_return+}
1269% \vspace{1ex}
1270% \infrule
1271%  {tlr_1\approx tlr_2 \andalso
1272%   s_1 \uparrow f \andalso s_2\uparrow f
1273%  }
1274%  {\verb+tal_base_call+~s_1~tlr_1\approx taa \append \verb+tal_base_call+~s_2~tlr_2}
1275% \vspace{1ex}
1276% \infrule
1277%  {tlr_1\approx tlr_2 \andalso
1278%   s_1 \uparrow f \andalso s_2\uparrow f \andalso
1279%   \verb+tal_collapsable+~tal_2
1280%  }
1281%  {\verb+tal_base_call+~s_1~tlr_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2)}
1282% \vspace{1ex}
1283% \infrule
1284%  {tlr_1\approx tlr_2 \andalso
1285%   s_1 \uparrow f \andalso s_2\uparrow f \andalso
1286%   \verb+tal_collapsable+~tal_1
1287%  }
1288%  {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_base_call+~s_2~tlr_2)}
1289% \vspace{1ex}
1290% \infrule
1291%  {tlr_1 \approx tlr_2 \andalso
1292%   s_1 \uparrow f \andalso s_2\uparrow f\andalso
1293%   tal_1 \approx tal_2 \andalso
1294%  }
1295%  {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2}
1296% \caption{The inference rule for the relation $\approx$.}
1297% \label{fig:txx_rel}
1298% \end{figure}
1299% %
1300% \begin{comment}
1301% \begin{verbatim}
1302% let rec tlr_rel S1 st1 st1' S2 st2 st2'
1303%   (tlr1 : trace_label_return S1 st1 st1')
1304%   (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
1305% match tlr1 with
1306%   [ tlr_base st1 st1' tll1 ⇒
1307%     match tlr2 with
1308%     [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
1309%     | _ ⇒ False
1310%     ]
1311%   | tlr_step st1 st1' st1'' tll1 tl1 ⇒
1312%     match tlr2 with
1313%     [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
1314%       tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
1315%     | _ ⇒ False
1316%     ]
1317%   ]
1318% and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
1319%  (tll1 : trace_label_label S1 fl1 st1 st1')
1320%  (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
1321%   match tll1 with
1322%   [ tll_base fl1 st1 st1' tal1 H ⇒
1323%     match tll2 with
1324%     [ tll_base fl2 st2 st2 tal2 G ⇒
1325%       as_label_safe … («?, H») = as_label_safe … («?, G») ∧
1326%       tal_rel … tal1 tal2
1327%     ]
1328%   ]
1329% and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
1330%  (tal1 : trace_any_label S1 fl1 st1 st1')
1331%  (tal2 : trace_any_label S2 fl2 st2 st2')
1332%    on tal1 : Prop ≝
1333%   match tal1 with
1334%   [ tal_base_not_return st1 st1' _ _ _ ⇒
1335%     fl2 = doesnt_end_with_ret ∧
1336%     ∃st2mid,taa,H,G,K.
1337%     tal2 ≃ taa_append_tal ? st2 ??? taa
1338%       (tal_base_not_return ? st2mid st2' H G K)
1339%   | tal_base_return st1 st1' _ _ ⇒
1340%     fl2 = ends_with_ret ∧
1341%     ∃st2mid,taa,H,G.
1342%     tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
1343%       (tal_base_return ? st2mid st2' H G)
1344%   | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒
1345%     fl2 = doesnt_end_with_ret ∧
1346%     ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
1347%     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
1348%     (* we must allow a tal_base_call to be similar to a call followed
1349%       by a collapsable trace (trace_any_any followed by a base_not_return;
1350%       we cannot use trace_any_any as it disallows labels in the end as soon
1351%       as it is non-empty) *)
1352%     (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
1353%       tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
1354%     ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
1355%     ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
1356%       tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
1357%       tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
1358%   | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
1359%     ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
1360%     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
1361%     (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
1362%       tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
1363%       tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
1364%     ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
1365%     ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
1366%       tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
1367%       tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
1368%   | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
1369%     tal_rel … tl1 tal2 (* <- this makes it many to many *)
1370%   ].
1371% \end{verbatim}
1372% \end{comment}
1373% %
1374% In the preceding rules, a $taa$ is an inhabitant of the
1375% $\verb+trace_any_any+~s_1~s_2$ (shorthand $\verb+TAA+~s_1~s_2$),
1376% an inductive data type whose definition
1377% is not in the paper for lack of space. It is the type of valid
1378% prefixes (even empty ones) of \verb+TAL+'s that do not contain
1379% any function call. Therefore it
1380% is possible to concatenate (using ``$\append$'') a \verb+TAA+ to the
1381% left of a \verb+TAL+. A \verb+TAA+ captures
1382% a sequence of silent moves.
1383% The \verb+tal_collapsable+ unary predicate over \verb+TAL+'s
1384% holds when the argument does not contain any function call and it ends
1385% with a label (not a return). The intuition is that after a function call we
1386% can still perform a sequence of silent actions while remaining similar.
1387%
1388% As should be expected, even though the rules are asymmetric $\approx$ is in fact
1389% an equivalence relation.
[3366]1390%
1391This argument enjoys the following remarkable properties:
[3343]1392\begin{enumerate}
[3366]1393 \item it is generic enough to accommodate all passes of the CerCo compiler;
1394 \item the requested conditions are
[3343]1395       just slightly stricter than the statement of a 1-to-many forward
[3366]1396       simulation in the classical case;
1397%        . In particular, they only require
1398%        the construction of very simple forms of structured traces made of
1399%        silent states only.
1400 \item they allow to prove our main result of the paper: the conditions we will
1401 present are sufficient to prove the intensional preservation needed to prove
1402 the compiler correct (\autoref{thm:main}).
[3343]1403\end{enumerate}
[3366]1404The last point is the important one. First of all it means that we have reduced
1405the complex problem of preserving the structure of fragments to a much simpler one that,
[3343]1406moreover, can be solved with slight adaptations of the forward simulation proof
1407that is performed for a compiler that only cares about functional properties.
[3366]1408Therefore we have successfully split as much as possible the proof of
[3343]1409preservation of functional properties from that of non-functional ones.
1410
[3366]1411% @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
[3356]1412
[3343]1413\paragraph{Relation sets.}
[3349]1414Let $S_1$ and $S_2$ be two deterministic labelled transition systems as described
[3366]1415in \autoref{sec:semantics}. We introduce now the four relations $\mathcal{S,C,R,L}\subseteq S_1\times S_2$
[3349]1416between states of the two systems. The first two are abstract and must be instantiated
1417by every pass. The remaining two are derived.
[3343]1418
1419The $\S$ relation between states is the classical relation used
[3349]1420in forward simulation proofs. It correlates the data of the states
[3343]1421(e.g. registers, memory, etc.).
1422
[3349]1423The $\C$ relation correlates states that are about to execute calls.
1424It allows to track the position in the target code of every call in the source code.
[3343]1425
[3349]1426% The $\L$ relation simply says that the two states are both label
1427% emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$.
1428% It allows to track the position in
1429% the target code of every cost emitting statement in the source code.
[3343]1430
[3366]1431\begin{definition}[$\R$ and $\LS$]
1432\label{def:R_LS}
[3349]1433Two states
1434$s_1$ and $s_2$ are $\R$-related if every time $s_1$ is the
[3356]1435successor of a call state $s_1'$ that is $\C$-related to a call state
[3343]1436$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally:
1437$$s_1\R s_2 \iffdef \forall s_1',s_2'.s_1'\C s_2' \to s_1'\ar s_1 \to s_2' \ar s_2.$$
1438
[3349]1439We say states in $s_1\in S_1$ and $s_2\in S_2$ are label-related
[3366]1440(marked $s_1\LS s_2$) if
[3349]1441\begin{itemize}
1442\item they both emit the same label $L$;
1443\item if $L\in \ell(\Functions)$ then
1444there is a state $s_2'$ such that $s_2\to[L]\to[\tau *]s_2'$ with
1445 $s_1\S s_2'$, otherwise if $L\notin\ell(\Functions)$ then $s_1\S s_2$.
1446\end{itemize}
[3366]1447\end{definition}
1448We will require all pairs of states that return from related calls to be
[3367]1449$\R$-related. This, in combination with a dual requirement on function calls,
[3366]1450will grant that calls return exactly where they are supposed to be.
1451On the other hand the $\LS$ relation captures the fact that synchronisation on labels can be decoupled from
1452``semantic synchronisation'' (in particular at the start of functions). $s_1\LS s_2$
[3359]1453tells that the two state are synchronised as to labels, and $s_2$ will eventually
1454synchronise semantically using only silent execution steps (apart from the very first
1455emit).
[3349]1456
[3356]1457Given the relations $\S$ and $\C$, \autoref{fig:forwardsim} defines a set of
1458local simulation conditions that are sufficient to grant the correctness of
[3366]1459the compiler, as stated by the results that follow.
[3343]1460\begin{figure}
1461\centering
1462% \begin{subfigure}{.475\linewidth}
1463% \centering
1464% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
1465%                             every label/.style=overlay, node distance=10mm]
1466%     \matrix [diag] (m) {%
1467%          \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
1468%          \node (s2) {}; & \node (t2) {}; \\
1469%     };
1470%     \node [above=0 of t1, overlay] {$\alpha$};
1471%     {[-stealth]
1472%     \draw (s1) -- (t1);
1473%     \draw [new] (s2) -- node [above] {$*$} (t2);
1474%     }
1475%     \draw (s1) to node [rel] {$\S$} (s2);
1476%     \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
1477% \end{tikzpicture}
[3347]1478% \caption{The \verb+cl_jump+ case.}
[3343]1479% \label{subfig:cl_jump}
1480% \end{subfigure}
1481% &
1482\centering
[3349]1483\tikzset{diag/.append style=
1484         {every node/.append style={is other,
1485                                    text height=0,text depth=0,text width=0,
1486                                    text opacity=0}                                                         
1487         },
1488         }
[3348]1489\begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}]
[3343]1490    \matrix [diag] (m) {%
[3348]1491         \node (s1) {s_1}; & \node (t1) {s_1'};\\
[3359]1492         \node (s2) {s_2}; & \node [newn] (t2) {s_2'}; \\
[3343]1493    };
1494    {[-stealth]
[3348]1495    \draw (s1) -- node [above] {$\tau$} (t1);
1496    \draw [new] (s2) -- node [above] {$\tau *$} (t2);
[3343]1497    }
[3347]1498    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
[3348]1499    \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2);
[3343]1500\end{tikzpicture}
[3348]1501\qquad
1502\begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}]
1503    \matrix [diag] (m) {%
1504         \node (s1) {s_1}; & \node (t1) {s_1'};\\
[3360]1505         \node (s2) {s_2}; & \node  [newn](mid) {s_a}; & \node [newn] (t2) {s_2'}; \\
[3343]1506    };
1507    {[-stealth]
[3348]1508    \draw (s1) -- node [above] {$L$} (t1);
[3349]1509    \draw [new] (s2) -- node [above] {$L$} (mid);
1510    \draw [new] (mid) -- node [above] {$\tau *$} (t2);
[3348]1511    }
1512    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
1513    \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2);
1514\end{tikzpicture}
1515\text{ if $L\notin\ell(\Functions)$}
1516\qquad
1517\begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}]
1518    \matrix [diag] (m) {%
1519         \node (s1) {s_1}; & \node (t1) {s_1'};\\
1520         \node (s2) {s_2};\\
1521    };
1522    {[-stealth]
1523    \draw (s1) -- node [above] {$\ell(f)$} (t1);
1524    }
1525    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
1526    \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (s2);
1527\end{tikzpicture}
1528\\[10pt]
1529\begin{tikzpicture}
1530    \matrix [diag, small vgap] (m) {%
1531         &\node (t1) {s_1'}; \\
1532         \node (s1) {s_1}; \\
[3360]1533         && \node [newn] (l1) {s_b}; & \node [newn] (l2) {s_c}; & \node [newn] (t2) {s_2'};\\
1534         \node [newn] (s2) {s_2}; & \node [newn] (c) {s_a};\\   
[3348]1535    };
1536    {[-stealth]
[3347]1537    \draw (s1) -- node [above left] {$f$} (t1);
[3348]1538    \draw [new] (s2) -- node [above] {$\tau *$} (c);
1539    \draw [new] (c) -- node [above left] {$f$} (l1);
1540    \draw [new] (l1) -- node [above] {$\ell(f)$} (l2);
1541    \draw [new] (l2) -- node [above] {$\tau *$} (t2);
[3343]1542    }
[3347]1543    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
[3343]1544    \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2);
[3360]1545    \draw [new] (s1) to [bend left] node [rel] {$\C$} (c);
[3348]1546\end{tikzpicture}
1547\qquad\qquad
1548\begin{tikzpicture}
1549    \matrix [diag, small vgap] (m) {%
1550        \node (s1) {s_1}; \\
1551        &\node (t1) {s_1'}; \\
[3360]1552        \node (s2) {s_2}; & \node [newn] (c) {s_a};\\
1553        && \node [newn] (r) {s_b}; & \node [newn] (t2) {s_2'}; \\   
[3343]1554    };
1555    {[-stealth]
[3347]1556    \draw (s1) -- node [above right] {$RET$} (t1);
[3348]1557    \draw [new] (s2) -- node [above] {$\tau *$} (c);
[3347]1558    \draw [new] (c) -- node [below left] {$RET$} (r);
[3348]1559    \draw [new] (r) -- node [above] {$\tau *$} (t2);
[3343]1560    }
[3347]1561    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
[3348]1562    \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S$} (t2);
[3347]1563    \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
[3343]1564\end{tikzpicture}
[3366]1565\caption{Local simulation conditions. Each one states that the assumptions
1566         drawn solid imply the existence of the white states and the dashed relations.}
[3343]1567\label{fig:forwardsim}
1568\end{figure}
[3366]1569%
1570\begin{lemma}[Preservation of structured fragments]
[3359]1571If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
[3356]1572$T_1=s_1\To s_1'$ is a structured fragment not starting with a $\ell(f)$ emission,
1573and $s_1\S s_2$, then there is $T_2=s_2\To s_2'$ with $T\approx T'$ and $s_1'\S s_2'$.
[3349]1574\end{lemma}
[3366]1575\begin{theorem}[Preservation of measurable fragments]
1576\label{thm:main}
[3359]1577If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
[3366]1578$M_1 = s_1\to^* s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that
1579$s_1\LS s_2$, then there is a measurable $M_2 = s_2\to^* s_2'$ with $|M_1|=|M_2|$. Moreover,
[3359]1580there is a state $s_2''$ with $s_2'\to[\tau *]s_2''$ and $s_1'\S s_2''$.
[3349]1581\end{theorem}
[3366]1582In particular, the above theorem
1583applied to the \verb+main+ function of the program together with an assumption
1584stating that initial states are $\LS$-related shows that
1585for each measurable execution of the source code,
1586the compiled code produces a measurable execution with the same observables.
1587Combined with \autoref{thm:static} and by proving the conditions in
1588\autoref{fig:forwardsim} for every pass, the compiler is proved correct.
[3348]1589
[3366]1590
[3348]1591% \begin{figure}
1592% \centering
1593% \begin{tabular}{@{}c@{}c@{}c@{}}
1594% % \begin{subfigure}{.475\linewidth}
1595% % \centering
1596% % \begin{tikzpicture}[every join/.style={ar}, join all, thick,
1597% %                             every label/.style=overlay, node distance=10mm]
1598% %     \matrix [diag] (m) {%
1599% %          \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
1600% %          \node (s2) {}; & \node (t2) {}; \\
1601% %     };
1602% %     \node [above=0 of t1, overlay] {$\alpha$};
1603% %     {[-stealth]
1604% %     \draw (s1) -- (t1);
1605% %     \draw [new] (s2) -- node [above] {$*$} (t2);
1606% %     }
1607% %     \draw (s1) to node [rel] {$\S$} (s2);
1608% %     \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
1609% % \end{tikzpicture}
1610% % \caption{The \verb+cl_jump+ case.}
1611% % \label{subfig:cl_jump}
1612% % \end{subfigure}
1613% % &
1614% \begin{subfigure}{.25\linewidth}
1615% \centering
1616% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
1617%                             every label/.style=overlay, node distance=10mm]
1618%     \matrix [diag] (m) {%
1619%          \node (s1) {}; & \node (t1) {};\\
1620%          \node (s2) {}; & \node (t2) {}; \\
1621%     };
1622%     {[-stealth]
1623%     \draw (s1) -- (t1);
1624%     \draw [new] (s2) -- node [above] {$*$} (t2);
1625%     }
1626%     \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
1627%     \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2);
1628% \end{tikzpicture}
1629% \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.}
1630% \label{subfig:cl_other_jump}
1631% \end{subfigure}
1632% &
1633% \begin{subfigure}{.375\linewidth}
1634% \centering
1635% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
1636%                             every label/.style=overlay, node distance=10mm]
1637%     \matrix [diag, small gap] (m) {%
1638%          &\node (t1) {}; \\
1639%          \node (s1) [is call] {}; \\
1640%          && \node (l) {}; & \node (t2) {};\\
1641%          \node (s2) {}; & \node (c) [is call] {};\\   
1642%     };
1643%     {[-stealth]
1644%     \draw (s1) -- node [above left] {$f$} (t1);
1645%     \draw [new] (s2) -- node [above] {$*$} (c);
1646%     \draw [new] (c) -- node [below right] {$f$} (l);
1647%     \draw [new] (l) -- node [above] {$*$} (t2);
1648%     }
1649%     \draw (s1) to [bend right] node [rel] {$\S$} (s2);
1650%     \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2);
1651%     \draw [new] (t1) to [bend left] node [rel] {$\L$} (l);
1652%     \draw [new] (t1) to [bend right] node [rel] {$\C$} (c);
1653%     \end{tikzpicture}
1654% \caption{The \verb+cl_call+ case.}
1655% \label{subfig:cl_call}
1656% \end{subfigure}
1657% &
1658% \begin{subfigure}{.375\linewidth}
1659% \centering
1660% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
1661%                             every label/.style=overlay, node distance=10mm]
1662%     \matrix [diag, small gap] (m) {%
1663%         \node (s1) [is ret] {}; \\
1664%         &\node (t1) {}; \\
1665%         \node (s2) {}; & \node (c) [is ret] {};\\
1666%         && \node (r) {}; & \node (t2) {}; \\   
1667%     };
1668%     {[-stealth]
1669%     \draw (s1) -- node [above right] {$RET$} (t1);
1670%     \draw [new] (s2) -- node [above] {$*$} (c);
1671%     \draw [new] (c) -- node [below left] {$RET$} (r);
1672%     \draw [new] (r) -- node [above] {$*$} (t2);
1673%     }
1674%     \draw (s1) to [bend right] node [rel] {$\S$} (s2);
1675%     \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2);
1676%     \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
1677% \end{tikzpicture}
1678% \caption{The \verb+cl_return+ case.}
1679% \label{subfig:cl_return}
1680% \end{subfigure}
1681% \end{tabular}
1682% \caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.
1683%          Dashed lines
1684%          and arrows indicates how the diagrams must be closed when solid relations
1685%          are present.}
1686% \label{fig:forwardsim}
1687% \end{figure}
1688
[3349]1689% \paragraph{1-to-many forward simulation conditions.}
1690% \begin{condition}[Cases \verb+cl_other+ and \verb+cl_jump+]
1691%  For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
1692%  $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or
1693%  both $s_1\class\verb+cl_other+\}$ and $\ell~s_1'$,
1694%  there exists an $s_2'$ and a $\verb+trace_any_any_free+~s_2~s_2'$ called $taaf$
1695%  such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
1696% $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \verb+as_costed+.
1697% \end{condition}
1698%
1699% In the above condition depicted in \autoref{subfig:cl_other_jump},
1700% a $\verb+trace_any_any_free+~s_1~s_2$ (which from now on
1701% will be shorthanded as \verb+TAAF+) is an
1702% inductive type of structured traces that do not contain function calls or
1703% cost emission statements. Differently from a \verb+TAA+, the
1704% instruction to be executed in the lookahead state $s_2$ may be a cost emission
1705% statement.
1706%
1707% The intuition of the condition is that one step can be replaced with zero or more steps if it
1708% preserves the relation between the data and if the two final statuses are
1709% labelled in the same way. Moreover, we must take special care of the empty case
1710% to avoid collapsing two consecutive states that emit a label, missing one of the two emissions.
1711%
1712% \begin{condition}[Case \verb+cl_call+]
1713%  For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and
1714%  $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a
1715% $\verb+TAA+~s_2~s_a$, and a
1716% $\verb+TAAF+~s_b~s_2'$ such that:
1717% $s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of
1718% the two call states are the same, $s_1 \C s_a$,
1719% $s_a\exec s_b$, $s_1' \L s_b$ and
1720% $s_1' \S s_2'$.
1721% \end{condition}
1722%
1723% The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a
1724% sequence of silent actions before and after the function call itself.
1725% The old and new call states must be $\C$-related, the old and new
1726% states at the beginning of the function execution must be $\L$-related
1727% and, finally, the two initial and final states must be $\S$-related
1728% as usual.
1729%
1730% \begin{condition}[Case \verb+cl_return+]
1731%  For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$,
1732%  $s_1\exec s_1'$ and $s_1 \class \verb+cl_return+$, there exists $s_a, s_b, s_2'$, a
1733% $\verb+TAA+~s_2~s_a$, a
1734% $\verb+TAAF+~s_b~s_2'$ called $taaf$ such that:
1735% $s_a\class\verb+cl_return+$,
1736% $s_a\exec s_b$,
1737% $s_1' \R s_b$ and
1738% $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
1739% $taaf$ is non empty, or $\lnot \ell~s_a$.
1740% \end{condition}
1741%
1742% Similarly to the call condition, to simulate a return we can perform a
1743% sequence of silent actions before and after the return statement itself,
1744% as depicted in \autoref{subfig:cl_return}.
1745% The old and the new statements after the return must be $\R$-related,
1746% to grant that they returned to corresponding calls.
1747% The two initial and final states must be $\S$-related
1748% as usual and, moreover, they must exhibit the same labels. Finally, when
1749% the suffix is non empty we must take care of not inserting a new
1750% unmatched cost emission statement just after the return statement.
1751%
1752% \begin{comment}
1753% \begin{verbatim}
1754% definition status_simulation ≝
1755%   λS1 : abstract_status.
1756%   λS2 : abstract_status.
1757%   λsim_status_rel : status_rel S1 S2.
1758%     ∀st1,st1',st2.as_execute S1 st1 st1' →
1759%     sim_status_rel st1 st2 →
1760%     match as_classify … st1 with
1761%     [ None ⇒ True
1762%     | Some cl ⇒
1763%       match cl with
1764%       [ cl_call ⇒ ∀prf.
1765%         (*
1766%              st1' ------------S----------\
1767%               ↑ \                         \
1768%              st1 \--L--\                   \
1769%               | \       \                   \
1770%               S  \-C-\  st2_after_call →taa→ st2'
1771%               |       \     ↑
1772%              st2 →taa→ st2_pre_call
1773%         *)
1774%         ∃st2_pre_call.
1775%         as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
1776%         call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
1777%         ∃st2_after_call,st2'.
1778%         ∃taa2 : trace_any_any … st2 st2_pre_call.
1779%         ∃taa2' : trace_any_any … st2_after_call st2'.
1780%         as_execute … st2_pre_call st2_after_call ∧
1781%         sim_status_rel st1' st2' ∧
1782%         label_rel … st1' st2_after_call
1783%       | cl_return ⇒
1784%         (*
1785%              st1
1786%             / ↓
1787%            | st1'----------S,L------------\
1788%            S   \                           \
1789%             \   \-----R-------\            |     
1790%              \                 |           |
1791%              st2 →taa→ st2_ret |           |
1792%                           ↓   /            |
1793%                      st2_after_ret →taaf→ st2'
1794%
1795%            we also ask that st2_after_ret be not labelled if the taaf tail is
1796%            not empty
1797%         *)
1798%         ∃st2_ret,st2_after_ret,st2'.
1799%         ∃taa2 : trace_any_any … st2 st2_ret.
1800%         ∃taa2' : trace_any_any_free … st2_after_ret st2'.
1801%         (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
1802%         as_classifier … st2_ret cl_return ∧
1803%         as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
1804%         ret_rel … sim_status_rel st1' st2_after_ret ∧
1805%         label_rel … st1' st2'
1806%       | cl_other ⇒
1807%           (*         
1808%           st1 → st1'
1809%             |      \
1810%             S      S,L
1811%             |        \
1812%            st2 →taaf→ st2'
1813%           
[3369]1814%            the taaf can be empty (e.g. tunnelling) but we ask it must not be the
[3349]1815%            case when both st1 and st1' are labelled (we would be able to collapse
1816%            labels otherwise)
1817%          *)
1818%         ∃st2'.
1819%         ∃taa2 : trace_any_any_free … st2 st2'.
1820%         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
1821%         sim_status_rel st1' st2' ∧
1822%         label_rel … st1' st2'
1823%       | cl_jump ⇒
1824%         (* just like cl_other, but with a hypothesis more *)
1825%         as_costed … st1' →
1826%         ∃st2'.
1827%         ∃taa2 : trace_any_any_free … st2 st2'.
1828%         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
1829%         sim_status_rel st1' st2' ∧
1830%         label_rel … st1' st2'
1831%       ]
1832%     ].
1833% \end{verbatim}
1834% \end{comment}
[3343]1835
[3349]1836% \paragraph{Main result: the 1-to-many forward simulation conditions
1837% are sufficient to trace reconstruction}
1838%
1839% Let us assume that a relation set is given such that the 1-to-many
1840% forward simulation conditions are satisfied. Under this assumption we
1841% can prove the following three trace reconstruction theorems by mutual
1842% structural induction over the traces given in input between the
1843% $s_1$ and $s_1'$ states.
1844%
1845% In particular, the \verb+status_simulation_produce_tlr+ theorem
1846% applied to the \verb+main+ function of the program and equal
1847% $s_{2_b}$ and $s_2$ states shows that, for every initial state in the
1848% source code that induces a structured trace in the source code,
1849% the compiled code produces a similar structured trace.
1850%
1851% \begin{theorem}[\verb+status_simulation_produce_tlr+]
1852% For every $s_1,s_1',s_{2_b},s_2$ s.t.
1853% there is a $\verb+TLR+~s_1~s_1'$ called $tlr_1$ and a
1854% $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
1855% $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
1856% there is a $\verb+TLR+~s_{2_b}~s_{2_m}$ called $tlr_2$ and
1857% there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$
1858% s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$,
1859% and $tlr_1\approx tlr_2$
1860% and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1861% $s_1' \R s_{2_m}$.
1862% \end{theorem}
1863%
1864% The theorem states that a \verb+trace_label_return+ in the source code
1865% together with a precomputed preamble of silent states
1866% (the \verb+TAA+) in the target code induces a
1867% similar \verb+trace_label_return+ in the target code which can be
1868% followed by a sequence of silent states. Note that the statement does not
1869% require the produced \verb+trace_label_return+ to start with the
1870% precomputed preamble, even if this is likely to be the case in concrete
1871% implementations. The preamble in input is necessary for compositionality, e.g.
1872% because the 1-to-many forward simulation conditions allow in the
1873% case of function calls to execute a preamble of silent instructions just after
1874% the function call.
1875%
1876% Clearly similar results are also available for the other two types of structured
1877% traces (in fact, they are all proved simultaneously by mutual induction).
[3347]1878% \begin{theorem}[\verb+status_simulation_produce_tll+]
[3343]1879% For every $s_1,s_1',s_{2_b},s_2$ s.t.
[3347]1880% there is a $\verb+TLL+~b~s_1~s_1'$ called $tll_1$ and a
[3343]1881% $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
1882% $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
1883% \begin{itemize}
1884%  \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
[3347]1885%        and a trace $\verb+TLL+~b~s_{2_b}~s_{2_m}$ called $tll_2$
1886%        and a $\verb+TAAF+~s_{2_m}~s_2'$ called $taa_2$ s.t.
[3343]1887%        $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1888%        $s_1' \R s_{2_m}$ and
1889%        $tll_1\approx tll_2$ and
1890%        if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
1891%  \item else there exists $s_2'$ and a
[3347]1892%        $\verb+TLL+~b~s_{2_b}~s_2'$ called $tll_2$ such that
[3343]1893%        $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1894%        $tll_1\approx tll_2$.
1895% \end{itemize}
1896% \end{theorem}
1897%
1898% The statement is similar to the previous one: a source
[3347]1899% \verb+trace_label_label+ and a given target preamble of silent states
1900% in the target code induce a similar \verb+trace_label_label+ in the
[3343]1901% target code, possibly followed by a sequence of silent moves that become the
[3347]1902% preamble for the next \verb+trace_label_label+ translation.
[3343]1903%
[3347]1904% \begin{theorem}[\verb+status_simulation_produce_tal+]
[3343]1905% For every $s_1,s_1',s_2$ s.t.
[3347]1906% there is a $\verb+TAL+~b~s_1~s_1'$ called $tal_1$ and
[3343]1907% $s_1 \S s_2$
1908% \begin{itemize}
1909%  \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
[3347]1910%    and a trace $\verb+TAL+~b~s_2~s_{2_m}$ called $tal_2$ and a
1911%    $\verb+TAAF+~s_{2_m}~s_2'$ called $taa_2$ s.t.
[3343]1912%    $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1913%    $s_1' \R s_{2_m}$ and
1914%    $tal_1 \approx tal_2$ and
1915%    if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
1916%  \item else there exists $s_2'$ and a
[3347]1917%    $\verb+TAL+~b~s_2~s_2'$ called $tal_2$ such that
[3343]1918%    either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1919%        $tal_1\approx tal_2$
1920%    or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and
[3347]1921%    $\verb+tal_collapsable+~tal_1$ and $\lnot \ell~s_1$.
[3343]1922% \end{itemize}
1923% \end{theorem}
1924%
1925% The statement is also similar to the previous ones, but for the lack of
1926% the target code preamble.
1927
1928\begin{comment}
1929\begin{corollary}
1930For every $s_1,s_1',s_2$ s.t.
[3347]1931there is a $\verb+trace_label_return+~s_1~s_1'$ called $tlr_1$ and
[3343]1932$s_1 (\L \cap \S) s_2$
1933there exists $s_{2_m},s_2'$ s.t.
[3347]1934there is a $\verb+trace_label_return+~s_2~s_{2_m}$ called $tlr_2$ and
1935there is a $\verb+trace_any_any_free+~s_{2_m}~s_2'$ called $taaf$
1936s.t. if $taaf$ is non empty then $\lnot (\verb+as_costed+~s_{2_m})$,
1937and $\verb+tlr_rel+~tlr_1~tlr_2$
[3343]1938and $s_1' (\S \cap \L) s_2'$ and
1939$s_1' \R s_{2_m}$.
1940\end{corollary}
1941\end{comment}
1942
1943\begin{comment}
1944\begin{verbatim}
1945status_simulation_produce_tlr S1 S2 R
1946(* we start from this situation
1947     st1 →→→→tlr→→→→ st1'
1948      | \
1949      L  \---S--\
1950      |          \
1951   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
1952                        by the preceding call)
1953   
1954   and we produce
1955     st1 →→→→tlr→→→→ st1'
1956             \\      /  \
1957             //     R    \-L,S-\
1958             \\     |           \
1959   st2_lab →tlr→ st2_mid →taaf→ st2'
1960*)
1961  st1 st1' st2_lab st2
1962  (tlr1 : trace_label_return S1 st1 st1')
1963  (taa2_pre : trace_any_any S2 st2_lab st2)
1964  (sim_execute : status_simulation S1 S2 R)
1965  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
1966  ∃st2_mid.∃st2'.
1967  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
1968  ∃taa2 : trace_any_any_free … st2_mid st2'.
1969  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
1970  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
1971  tlr_rel … tlr1 tlr2
1972\end{verbatim}
1973\end{comment}
[3359]1974\section{The formalisation}
[3368]1975\label{sec:formalization}
1976As we already explained, for the sake of presentation we presented the formal
[3359]1977content of our results departing from the actual Matita formalisation. In this
1978section we explain the basis of the Matita development, heavily based on
[3367]1979inductive definitions and dependent types. The development consists of 3369 lines
1980of code and can be downloaded from
1981\begin{center}\url{http://cerco.cs.unibo.it/attachment/wiki/WikiStart/CPP2013.tar.gz}\end{center}
[3359]1982
1983\paragraph*{The main differences.} The main points where the development diverges
1984from the material presented in the previous sections are the following.
1985\begin{itemize}
[3368]1986 \item Rather than having a generic notion of fragment and predicates of
1987 structuredness and measurability, we use inductive definitions and
1988 dependent types to provide data types that satisfy the
1989 conditions by construction.
1990 Among other things this turns the proof of \autoref{thm:preservation}
[3367]1991 into a matter of
1992 structural induction, when it would require additional lemmas
[3359]1993 otherwise.
1994 \item As we are dealing with a deterministic labelling transition system, we
[3367]1995 purposely blur the distinction between labelling the transitions and labelling
[3359]1996 the states originating them, and opt in general for the latter in the actual
1997 definitions.
[3367]1998 \item As object code cannot have a separate emission instruction, we allow
1999 any instruction to be labelled, which implies that labels can be emitted
2000 alongside other observable events.
[3359]2001 \item A small difference lies in the naming conventions. In this paper we went
2002 with the tradition of labelled transition systems and named sequences of states
2003 and steps \emph{execution fragments}. In the development we named our structures
[3366]2004 \emph{traces} (that usually refer to the sequence of emitted labels only).
2005 In the remainder of this section we will use both names.
[3359]2006\end{itemize}
2007
2008\paragraph*{The main definitions.}
2009The notion of deterministic labelled transition system is captured in the development
2010via the abstract data type called $\verb+abstract_status+$. The fields
2011of this record are the following.
2012\begin{itemize}
2013 \item \verb+S : Type[0]+, the type of states.
[3368]2014 \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate modelling
[3359]2015 the execution. As in the previous sections, we write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$.
2016 \item \verb+as_classifier : S $\to$ classification+, a function tagging all
2017 states with a class in
2018 $\{$\verb+cl_return,cl_jump,cl_call,cl_other+$\}$, depending on the instruction
2019 that is about to be executed (we omit tail-calls for simplicity). We will
2020 use $s \class c$ as a shorthand for both $\verb+as_classifier+~s=c$
2021 (if $c$ is a classification) and $\verb+as_classifier+~s\in c$
2022 (if $c$ is a set of classifications). This partly replaces the labelling of execution
2023 steps.
2024 \item \verb+as_label : S $\to$ option label+, telling whether the
2025 next instruction to be executed in $s$ is a cost emission statement,
2026 and if yes returning the associated cost label. Our shorthand for this function
2027 will be $L$, and we will also abuse the notation by using $L~s$ as a
2028 predicate stating that $s$ is labelled.
2029 \item \verb+as_call_ident : ($\Sigma$s:S. s $\class$ cl_call) $\to$ label+,
2030 telling the identifier of the function which is being called in a
2031 \verb+cl_call+ state. We will use the shorthand $s\uparrow f$ for
2032 $\verb+as_call_ident+~s = f$.
2033 \item \verb+as_after_return : ($\Sigma$s:S. s $\class$ cl_call) $\to$ S $\to$ Prop+,
2034 which holds on the \verb+cl_call+ state $s_1$ and a state $s_2$ when the
2035 instruction to be executed in $s_2$ follows the function call to be
2036 executed in (the witness of the $\Sigma$-type) $s_1$, i.e. when $s_1\ar s_2$.
2037\end{itemize}
2038%
2039% % \begin{alltt}
2040% % record abstract_status := \{ S: Type[0];
2041% %  as_execute: S \(\to\) S \(\to\) Prop;   as_classifier: S \(\to\) classification;
2042% %  as_label: S \(\to\) option label;    as_called: (\(\Sigma\)s:S. c s = cl_call) \(\to\) label;
2043% %  as_after_return: (\(\Sigma\)s:S. c s = cl_call) \(\to\) S \(\to\) Prop \}
2044% % \end{alltt}
2045%
2046The inductive type for structured traces is actually made by three multiple
2047inductive types with the following semantics:
2048\begin{enumerate}
2049 \item $(\verb+trace_label_return+~s_1~s_2)$ (shorthand $\verb+TLR+~s_1~s_2$)
2050   is in fact what we called a measurable fragment ending in a return step.
2051%    is a trace that begins in
2052%    the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
2053%    such that the instruction to be executed in $s_1$ is a label emission
2054%    statement and the one to be executed in the state before $s_2$ is a return
2055%    statement. Thus $s_2$ is the state after the return. The trace
2056%    may contain other label emission statements. It captures the structure of
2057%    the execution of function bodies: they must start with a cost emission
2058%    statement and must end with a return; they are obtained by concatenating
2059%    one or more basic blocks, all starting with a label emission
2060%    (e.g. in case of loops).
2061 \item $(\verb+trace_label_label+~b~s_1~s_2)$ (shorthand $\verb+TLL+~b~s_1~s_2$)
2062   models basic blocks. It is the special case of a measurable fragment containing
2063   only its first label emission.
2064 \item $(\verb+trace_any_label+~b~s_1~s_2)$ (shorthand $\verb+TAL+~b~s_1~s_2$)
2065   is a structured fragment, possibly with a return step appended to it, that
2066   does not contain any label apart possibly from the first state.
2067\end{enumerate}
2068The above definition summarise the formal rules shown in \autoref{fig:traces}.
2069\begin{figure}
2070\begin{multicols}{3}
2071\infrule[\verb+tlr_base+]
2072 {\verb+TLL+~true~s_1~s_2}
2073 {\verb+TLR+~s_1~s_2}
2074
2075\infrule[\verb+tlr_step+]
2076 {\verb+TLL+~false~s_1~s_2 \andalso
2077  \verb+TLR+~s_2~s_3
2078 }
2079 {\verb+TLR+~s_1~s_3}
2080
2081\infrule[\verb+tll_base+]
2082 {\verb+TAL+~b~s_1~s_2 \andalso
2083  L~s_1
2084 }
2085 {\verb+TLL+~b~s_1~s_2}
2086\end{multicols}
2087
2088\infrule[\verb+tal_base_not_return+]
2089 {s_1\exec s_2 \andalso
2090  s_1\class\{\verb+cl_jump+, \verb+cl_other+\}\andalso
2091  L~s_2
2092 }
2093 {\verb+TAL+~false~s_1~s_2}
2094
2095\infrule[\verb+tal_base_return+]
2096 {s_1\exec s_2 \andalso
2097  s_1 \class \verb+cl_return+
2098 }
2099 {\verb+TAL+~true~s_1~s_2}
2100
2101\infrule[\verb+tal_base_call+]
2102 {s_1\exec s_2 \andalso
2103  s_1 \class \verb+cl_call+ \andalso
2104  s_1\ar s_3 \andalso
2105  \verb+TLR+~s_2~s_3 \andalso
2106  L~s_3
2107 }
2108 {\verb+TAL+~false~s_1~s_3}
2109
2110\infrule[\verb+tal_step_call+]
2111 {s_1\exec s_2 \andalso
2112  s_1 \class \verb+cl_call+ \andalso
2113  s_1\ar s_3 \andalso
2114  \verb+TLR+~s_2~s_3 \andalso
2115  \verb+TAL+~b~s_3~s_4
2116 }
2117 {\verb+TAL+~b~s_1~s_4}
2118
2119\infrule[\verb+tal_step_default+]
2120 {s_1\exec s_2 \andalso
2121  \lnot L~s_2 \andalso
2122  \verb+TAL+~b~s_2~s_3\andalso
2123  s_1 \class \verb+cl_other+
2124 }
2125 {\verb+TAL+~b~s_1~s_3}
2126\caption{The rules forming the inductive definitions of structured
2127         traces.}
2128\label{fig:traces}
2129\end{figure}
2130\begin{comment}
2131\begin{verbatim}
2132inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
2133  | tlr_base:
2134      ∀status_before: S.
2135      ∀status_after: S.
2136        trace_label_label S ends_with_ret status_before status_after →
2137        trace_label_return S status_before status_after
2138  | tlr_step:
2139      ∀status_initial: S.
2140      ∀status_labelled: S.
2141      ∀status_final: S.
2142        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
2143        trace_label_return S status_labelled status_final →
2144          trace_label_return S status_initial status_final
2145with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
2146  | tll_base:
2147      ∀ends_flag: trace_ends_with_ret.
2148      ∀start_status: S.
2149      ∀end_status: S.
2150        trace_any_label S ends_flag start_status end_status →
2151        as_costed S start_status →
2152          trace_label_label S ends_flag start_status end_status
2153with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
2154  (* Single steps within a function which reach a label.
2155     Note that this is the only case applicable for a jump. *)
2156  | tal_base_not_return:
2157      ∀start_status: S.
2158      ∀final_status: S.
2159        as_execute S start_status final_status →
2160        (as_classifier S start_status cl_jump ∨
2161         as_classifier S start_status cl_other) →
2162        as_costed S final_status →
2163          trace_any_label S doesnt_end_with_ret start_status final_status
2164  | tal_base_return:
2165      ∀start_status: S.
2166      ∀final_status: S.
2167        as_execute S start_status final_status →
2168        as_classifier S start_status cl_return →
2169          trace_any_label S ends_with_ret start_status final_status
2170  (* A call followed by a label on return. *)
2171  | tal_base_call:
2172      ∀status_pre_fun_call: S.
2173      ∀status_start_fun_call: S.
2174      ∀status_final: S.
2175        as_execute S status_pre_fun_call status_start_fun_call →
2176        ∀H:as_classifier S status_pre_fun_call cl_call.
2177          as_after_return S «status_pre_fun_call, H» status_final →
2178          trace_label_return S status_start_fun_call status_final →
2179          as_costed S status_final →
2180            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
2181  (* A call followed by a non-empty trace. *)
2182  | tal_step_call:
2183      ∀end_flag: trace_ends_with_ret.
2184      ∀status_pre_fun_call: S.
2185      ∀status_start_fun_call: S.
2186      ∀status_after_fun_call: S.
2187      ∀status_final: S.
2188        as_execute S status_pre_fun_call status_start_fun_call →
2189        ∀H:as_classifier S status_pre_fun_call cl_call.
2190          as_after_return S «status_pre_fun_call, H» status_after_fun_call →
2191          trace_label_return S status_start_fun_call status_after_fun_call →
2192          ¬ as_costed S status_after_fun_call →
2193          trace_any_label S end_flag status_after_fun_call status_final →
2194            trace_any_label S end_flag status_pre_fun_call status_final
2195  | tal_step_default:
2196      ∀end_flag: trace_ends_with_ret.
2197      ∀status_pre: S.
2198      ∀status_init: S.
2199      ∀status_end: S.
2200        as_execute S status_pre status_init →
2201        trace_any_label S end_flag status_init status_end →
2202        as_classifier S status_pre cl_other →
2203        ¬ (as_costed S status_init) →
2204          trace_any_label S end_flag status_pre status_end.
2205\end{verbatim}
2206\end{comment}
2207
2208
2209The equivalent of $|T|$ on fragments can be easily defined by mutual recursion
2210on the three types of traces defined in \autoref{fig:traces}.
[3360]2211
2212\paragraph{The forward simulation result.}
[3366]2213In the formalisation, the equivalent conditions of those
2214depicted in \autoref{fig:forwardsim} can be seen in \autoref{fig:forwardsim'}.
2215Again we must produce for each pass the relations $\S$ and $\C$. Another derived
2216relation is $\L$, which holds for states $s_1$ and $s_2$ when $L~s_1=L~s_2$.
2217%
2218Some details are skipped in the figure regarding the nature of the repeated steps depicted with
2219an asterisk.
2220There are three kinds of iterated steps without
2221calls nor returns involved in the conditions:
2222\begin{itemize}
2223 \item sequences where all states strictly after the first one are unlabelled;
2224 these are what can be safely prepended to \verb+TAL+'s, and are modelled
2225 by the inductive definition \verb+trace_any_any+ (\verb+TAA+) in the formalisation;
2226 \item sequences where all ``internal'' states strictly after the first and before the last
2227 are unlabelled; these are \verb+trace_any_any_free+ in the formalisation (\verb+TAAF+, which
2228 is just a \verb+TAA+ followed by a step);
2229 \item sequences where all states strictly before the last are unlabelled that we
2230 will call here \verb+trace_any_any_right+ (\verb+TAAR+); in the formalisation
2231 these are in fact \verb+TAAF+'s with an additional condition.
2232\end{itemize}
2233%
[3360]2234\begin{figure}
2235\centering
2236\tikzset{diag/.append style=
2237         {every node/.append style={is other,
2238                                    text height=0,text depth=0,text width=0,
2239                                    text opacity=0}                                                         
2240         },
2241         }
2242\begin{tabular}{@{}c@{}c@{}c@{}}
2243% \begin{subfigure}{.475\linewidth}
2244% \centering
2245% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
2246%                             every label/.style=overlay, node distance=10mm]
2247%     \matrix [diag] (m) {%
2248%          \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
2249%          \node (s2) {}; & \node (t2) {}; \\
2250%     };
2251%     \node [above=0 of t1, overlay] {$\alpha$};
2252%     {[-stealth]
2253%     \draw (s1) -- (t1);
2254%     \draw [new] (s2) -- node [above] {$*$} (t2);
2255%     }
2256%     \draw (s1) to node [rel] {$\S$} (s2);
2257%     \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
2258% \end{tikzpicture}
2259% \caption{The \verb+cl_jump+ case.}
2260% \label{subfig:cl_jump}
2261% \end{subfigure}
2262% &
[3366]2263\begin{subfigure}[b]{.25\linewidth}
[3360]2264\centering
2265\begin{tikzpicture}[every join/.style={ar}, join all, thick,
2266                            every label/.style=overlay, node distance=10mm]
2267    \matrix [diag] (m) {%
2268         \node (s1) {}; & \node (t1) {};\\
2269         \node (s2) {}; & \node [newn] (t2) {}; \\
2270    };
2271    {[-stealth]
2272    \draw (s1) -- (t1);
2273    \draw [new] (s2) -- node [above] {$*$} (t2);
2274    }
2275    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
2276    \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2);
2277\end{tikzpicture}
2278\caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.}
2279\label{subfig:cl_other_jump}
2280\end{subfigure}
2281&
[3366]2282\begin{subfigure}[b]{.375\linewidth}
[3360]2283\centering
2284\begin{tikzpicture}[every join/.style={ar}, join all, thick,
2285                            every label/.style=overlay, node distance=10mm]
2286    \matrix [diag, small gap] (m) {%
2287         &\node (t1) {}; \\
2288         \node (s1) {}; \\
2289         && \node [newn] (l) {}; & \node [newn] (t2) {};\\
2290         \node (s2) {}; & \node [newn] (c) {};\\   
2291    };
2292    {[-stealth]
2293    \draw (s1) -- node [above left] {$f$} (t1);
2294    \draw [new] (s2) -- node [above] {$*$} (c);
2295    \draw [new] (c) -- node [below right] {$f$} (l);
2296    \draw [new] (l) -- node [above] {$*$} (t2);
2297    }
2298    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
2299    \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2);
2300    \draw [new] (t1) to [bend left] node [rel] {$\L$} (l);
2301    \draw [new] (s1) to [bend left] node [rel] {$\C$} (c);
2302    \end{tikzpicture}
[3366]2303\caption{The \verb+cl_call+ case.\\\vspace{3.1ex}}
[3360]2304\label{subfig:cl_call}
2305\end{subfigure}
2306&
[3366]2307\begin{subfigure}[b]{.375\linewidth}
[3360]2308\centering
2309\begin{tikzpicture}[every join/.style={ar}, join all, thick,
2310                            every label/.style=overlay, node distance=10mm]
2311    \matrix [diag, small gap] (m) {%
2312        \node (s1) {}; \\
2313        &\node (t1) {}; \\
2314        \node (s2) {}; & \node [newn] (c) {};\\
2315        && \node [newn] (r) {}; & \node [newn] (t2) {}; \\   
2316    };
2317    {[-stealth]
2318    \draw (s1) -- (t1);
2319    \draw [new] (s2) -- node [above] {$*$} (c);
2320    \draw [new] (c) -- (r);
2321    \draw [new] (r) -- node [above] {$*$} (t2);
2322    }
2323    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
2324    \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2);
2325    \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
2326\end{tikzpicture}
[3366]2327\caption{The \verb+cl_return+ case.\\\vspace{3.1ex}}
[3360]2328\label{subfig:cl_return}
2329\end{subfigure}
2330\end{tabular}
[3366]2331\caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.}
2332\label{fig:forwardsim'}
[3360]2333\end{figure}
[3366]2334This prolification of different types of fragments is a downside of shifting
2335labelling from steps to states.
2336The actual conditions are as follows.
2337%
2338\begin{condition}[\verb+cl_other+ and \verb+cl_jump+, \autoref{subfig:cl_other_jump}]
2339\label{cond:other}
2340 For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
2341 $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or
2342 both $s_1\class\verb+cl_other+$ and $\ell~s_1'$,
2343 there exists an $s_2'$ and a $taaf:\verb+trace_any_any_free+~s_2~s_2'$
2344 such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
2345 $taaf$ is non empty, or one among $s_1$ and $s_1'$ is not labelled.
2346 The last condition is needed to prevent the collapsing of two
2347 label-emitting consecutive states.
2348\end{condition}
[3360]2349
[3366]2350% In the above condition depicted in ,
2351% a $\verb+trace_any_any_free+~s_1~s_2$ (which from now on
2352% will be shorthanded as \verb+TAAF+) is an
2353% inductive type of structured traces that do not contain function calls or
2354% cost emission statements. Differently from a \verb+TAA+, the
2355% instruction to be executed in the lookahead state $s_2$ may be a cost emission
2356% statement.
2357%
2358% The intuition of the condition is that one step can be replaced with zero or more steps if it
2359% preserves the relation between the data and if the two final statuses are
2360% labelled in the same way. Moreover, we must take special care of the empty case
2361% to avoid collapsing two consecutive states that emit a label, missing one of the two emissions.
2362%
2363\begin{condition}[\verb+cl_call+, \autoref{subfig:cl_call}]
2364\label{cond:call}
2365 For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and
2366 $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a
2367$\verb+TAA+~s_2~s_a$, and a
2368$\verb+TAAF+~s_b~s_2'$ such that:
2369$s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of
2370the two call states are the same, $s_1 \C s_a$,
2371$s_a\exec s_b$, $s_1' \L s_b$ and
2372$s_1' \S s_2'$.
2373\end{condition}
2374
2375% The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a
2376% sequence of silent actions before and after the function call itself.
2377% The old and new call states must be $\C$-related, the old and new
2378% states at the beginning of the function execution must be $\L$-related
2379% and, finally, the two initial and final states must be $\S$-related
2380% as usual.
2381
2382\begin{condition}[\verb+cl_return+, \autoref{subfig:cl_return}]
2383\label{cond:return}
2384 For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$,
2385 $s_1\exec s_1'$ and $s_1 \class \verb+cl_return+$, there exists $s_a, s_b, s_2'$, a
2386$\verb+TAA+~s_2~s_a$ and a
2387$\verb+TAAR+~s_b~s_2'$ such that:
2388$s_a\class\verb+cl_return+$,
2389$s_a\exec s_b$,
2390$s_1' \R s_b$ and
2391$s_1' \mathrel{{\S} \cap {\L}} s_2'$.
2392\end{condition}
2393
2394\paragraph{Main result.}
2395Let us assume that $\S$ and $\C$ are given such that
2396Conditions~\ref{cond:other}, \ref{cond:call} and~\ref{cond:return}
2397are satisfied. If we reword the
2398relation $\LS$ of \autoref{def:R_LS} by defining
2399$$s_1\LS s_2\iffdef s_1\L s_2\wedge \exists s_2', taa:\verb+TAA+~s_2~s_2'. s_1\S s_2',$$
2400we can prove the trace reconstruction theorem,
2401which is the analogue of \autoref{thm:main}.
2402%
2403\begin{theorem}[\verb+status_simulation_produce_tlr+]
2404\label{thm:main'}
2405For every $s_1,s_1',s_2$ s.t.
2406$s_1\LS s_2$ and there is a $tlr_1:\verb+TLR+~s_1~s_1'$,
2407then there exist $s_2'$ and $tlr_2:\verb+TLR+~s_2~s_2'$
2408with $|tlr_1|=|tlr_2|$. Moreover there are $s_2''$ and
2409a $\verb+TAAR+~s_2'~s_2''$ with $s_2'\mathrel{{\S}\cap{\L}} s_2''$.
2410\end{theorem}
2411% In particular, the \verb+status_simulation_produce_tlr+ theorem
2412% applied to the \verb+main+ function of the program and equal
2413% $s_{2_b}$ and $s_2$ states shows that, for every initial state in the
2414% source code that induces a structured trace in the source code,
2415% the compiled code produces a similar structured trace.
2416The theorem states that a \verb+trace_label_return+ in the source code
2417together with a precomputed preamble of silent states
2418(hidden in the definition of $\LS$) in the target code induces a
2419similar \verb+trace_label_return+ in the target code.
2420% Note that the statement does not
2421% require the produced \verb+trace_label_return+ to start with the
2422% precomputed preamble, even if this is likely to be the case in concrete
2423% implementations.
2424The preamble in input and the postamble in output are necessary for compositionality,
2425and follow directly from the the fact that points semantically related
2426may not correspond to points where the same observable events are fired, in particular
2427cost labels and $RET$'s that mark the borders of measurability.
2428
2429The proof proceeds by mutual structural induction on the traces involved.
2430In the actual formalisation, in place of $|tlr_1|=|tlr_2|$ we use a
2431recursively defined simulation relation between traces that implies the required
2432equality.
2433
2434\section{Conclusions and future works}
2435\label{sec:conclusions}
2436The labelling approach is a technique to implement compilers that induce on
2437the source code a non uniform cost model determined from the object code
2438produced. The cost model assigns a cost to each basic block of the program.
2439The main theorem of the approach says that there is an exact
2440correspondence between the sequence of basic blocks started in the source
2441and object code, and that no instruction in the source or object code is
2442executed outside a basic block. Thus the cost of object code execution
2443can be computed precisely on the source.
2444
2445In this paper we scaled the labelling approach to cover a programming language
2446with function calls. This introduces new difficulties when the language
2447is unstructured, i.e. it allows function calls to return anywhere in the code,
2448destroying the hope of a static prediction of the cost of basic blocks.
2449We restored static predictability by introducing a new semantics for unstructured
2450programs that single outs well structured executions. The latter are represented
[3368]2451by structured execution fragments, a generalisation of streams of observables that capture
[3366]2452several structural invariants of the execution, like well nesting of functions
2453or the fact that every basic block must start with a code emission statement.
2454We showed that structured traces are sufficiently well behaved to statically compute a precise cost model on the object code.
2455
2456We also proved that the cost model computed on the object code is also valid
2457on the source code if the compiler respects two requirements: the weak execution
2458traces of the source and target code must be the same and the object
2459code execution fragments are structured.
2460
2461To prove that a compiler respects the requirement we extended the notion
2462of forward simulation proof for a labelled transition system to grant
2463preservation of structured fragments. If the source language of the compiler
2464is structured, all its execution fragments are, allowing to deduce from
2465preservation of structure that object code fragments are structured too.
2466
2467Finally, we identified measurable execution fragments that are those whose
[3367]2468execution time (once compiled) can be exactly computed looking only at the
2469weak execution traces of the object
2470code. A final instrumentation pass on the source
[3366]2471code can then be used to turn the non functional property of having a certain
[3367]2472cost into the functional property that a certain global variable
[3366]2473incremented at the beginning of every block according to the induced cost model
2474has a certain value.
2475
2476All results presented in the paper are part of a larger certification of a
2477C compiler which is based on the labelling approach. The certification, done
2478in Matita, is the main deliverable of the FET-Open Certified Complexity (CerCo).
2479
2480The short term objective consists in the completion of the certification of
2481the CerCo compiler exploiting the main theorem of this paper. An alternative approach
2482to the same problem that we would like to investigate consists in labelling
[3367]2483every instruction that follows a call.
2484This would reduce the requirements of the proofs, with
2485% This would still require a form of structured
2486% execution fragments, stating that both returns and calls are always followed
2487% by a label emission.
2488the downside of polluting the instrumented code
[3366]2489with many cost annotations.
2490
2491\paragraph{Related works.}
2492CerCo is the first project that explicitly tries to induce a
2493precise cost model on the source code in order to establish non-functional
2494properties of programs on an high level language. Traditional certifications
2495of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation
2496of the functional properties.
2497
2498Usually forward simulations take the following form: for each transition
2499from $s_1$ to $s_2$ in the source code, there exists an equivalent sequence of
2500transitions in the target code of length $n$. The number $n$ of transition steps
2501in the target code can just be the witness of the existential statement.
2502An equivalent alternative when the proof of simulation is constructive consists
2503in providing an explicit function, called \emph{clock function} in the
2504literature~\cite{clockfunctions}, that computes $n$ from $s_1$. Every clock
2505function constitutes then a cost model for the source code, in the spirit of
2506what we are doing in CerCo. However, we believe our solution to be superior
2507in the following respects: 1) the machinery of the labelling approach is
2508insensible to the resource being measured. Indeed, any cost model computed on
2509the object code can be lifted to the source code (e.g. stack space used,
2510energy consumed, etc.) simply re-proving an analogue of~\autoref{thm:static}.
2511For example, in CerCo we transported to the source level not only the execution
2512time cost model, but also the amount of stack used by function calls.
2513On the contrary, clock functions only talk about
2514number of transition steps. In order to extend the approach with clock functions
2515to other resources, additional functions must be introduced. Moreover, the
2516additional functions would be handled differently in the proof.
25172) the cost models induced by the labelling approach have a simple presentation.
2518In particular, they associate a number to each basic block. More complex
2519models can be induced when the approach is scaled to cover, for instance,
2520loop optimisations~\cite{loopoptimizations}, but the costs are still meant to
2521be easy to understand and manipulate in an interactive theorem prover or
2522in Frama-C.
2523On the contrary, a clock function is a complex function of the state $s_1$
2524which, as a function, is an opaque object that is difficult to reify as
2525source code in order to reason on it.
2526
2527% e.g.
2528% because the 1-to-many forward simulation conditions allow in the
2529% case of function calls to execute a preamble of silent instructions just after
2530% the function call.
2531
2532% Similarly to the call condition, to simulate a return we can perform a
2533% sequence of silent actions before and after the return statement itself,
2534% as depicted in \autoref{subfig:cl_return}.
2535% The old and the new statements after the return must be $\R$-related,
2536% to grant that they returned to corresponding calls.
2537% The two initial and final states must be $\S$-related
2538% as usual and, moreover, they must exhibit the same labels. Finally, when
2539% the suffix is non empty we must take care of not inserting a new
2540% unmatched cost emission statement just after the return statement.
2541
2542
[3359]2543% There are three mutual structural recursive functions, one for each of
2544% \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation
2545% $|\,.\,|$: the \emph{flattening} of the traces. These functions
2546% allow to extract from a structured trace the list of emitted cost labels.
2547%  We only show here the type of one
2548% of them:
2549% \begin{alltt}
2550% flatten_trace_label_return:
2551%  \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\).
2552%   trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S)
2553% \end{alltt}
2554%
2555% \paragraph{Structured traces similarity and cost prediction invariance.}
2556%
2557% A compiler pass maps source to object code and initial states to initial
2558% states. The source code and initial state uniquely determine the structured
2559% trace of a program, if it exists. The structured trace fails to exists iff
2560% the structural conditions are violated by the program execution (e.g. a function
2561% body does not start with a cost emission statement). Let us assume that the
2562% target structured trace exists.
2563%
2564% What is the relation between the source and target structured traces?
2565% In general, the two traces can be arbitrarily different. However, we are
2566% interested only in those compiler passes that maps a trace $\tau_1$ to a trace
2567% $\tau_2$ such that
2568% \begin{equation}|\tau_1| = |\tau_2|.\label{th2}\end{equation}
2569% The reason is that the combination of~\eqref{th1} with~\eqref{th2} yields the
2570% corollary
2571% \begin{equation}\label{th3}
2572% \forall s_1,s_2. \forall \tau: \verb+TLR+~s_1~s_2.~
2573%   \verb+clock+~s_2 - \verb+clock+~s_1 =
2574%   \Sigma_{\alpha \in |\tau_1|}\;k(\alpha) =
2575%   \Sigma_{\alpha \in |\tau_2|}\;k(\alpha).
2576% \end{equation}
2577% This corollary states that the actual execution time of the program can be computed equally well on the source or target language. Thus it becomes possible to
2578% transfer the cost model from the target to the source code and reason on the
2579% source code only.
2580%
2581% We are therefore interested in conditions stronger than~\eqref{th2}.
2582% Therefore we introduce here a similarity relation between traces with
2583% the same structure. Theorem~\verb+tlr_rel_to_traces_same_flatten+
2584% in the Matita formalisation shows that~\eqref{th2} holds for every pair
2585% $(\tau_1,\tau_2)$ of similar traces.
2586%
2587% Intuitively, two traces are similar when one can be obtained from
2588% the other by erasing or inserting silent steps, i.e. states that are
2589% not \verb+as_costed+ and that are classified as \verb+cl_other+.
2590% Silent steps do not alter the structure of the traces.
2591% In particular,
2592% the relation maps function calls to function calls to the same function,
2593% label emission statements to emissions of the same label, concatenation of
2594% subtraces to concatenation of subtraces of the same length and starting with
2595% the same emission statement, etc.
2596%
2597% In the formalisation the three similarity relations --- one for each trace
2598% kind --- are defined by structural recursion on the first trace and pattern
2599% matching over the second. Here we turn
2600% the definition into the inference rules shown in \autoref{fig:txx_rel}
2601% for the sake of readability. We also omit from trace constructors all arguments,
2602% but those that are traces or that
2603% are used in the premises of the rules. By abuse of notation we denote all three
2604% relations by infixing $\approx$.
2605%
2606% \begin{figure}
2607% \begin{multicols}{2}
2608% \infrule
2609%  {tll_1\approx tll_2
2610%  }
2611%  {\verb+tlr_base+~tll_1 \approx \verb+tlr_base+~tll_2}
2612%
2613% \infrule
2614%  {tll_1 \approx tll_2 \andalso
2615%   tlr_1 \approx tlr_2
2616%  }
2617%  {\verb+tlr_step+~tll_1~tlr_1 \approx \verb+tlr_step+~tll_2~tlr_2}
2618% \end{multicols}
2619% \vspace{3ex}
2620% \begin{multicols}{2}
2621% \infrule
2622%  {L~s_1 = L~s_2 \andalso
2623%   tal_1\approx tal_2
2624%  }
2625%  {\verb+tll_base+~s_1~tal_1 \approx \verb+tll_base+~s_2~tal_2}
2626%
2627% \infrule
2628%  {tal_1\approx tal_2
2629%  }
2630%  {\verb+tal_step_default+~tal_1 \approx tal_2}
2631% \end{multicols}
2632% \vspace{3ex}
2633% \infrule
2634%  {}
2635%  {\verb+tal_base_not_return+\approx taa \append \verb+tal_base_not_return+}
2636% \vspace{1ex}
2637% \infrule
2638%  {}
2639%  {\verb+tal_base_return+\approx taa \append \verb+tal_base_return+}
2640% \vspace{1ex}
2641% \infrule
2642%  {tlr_1\approx tlr_2 \andalso
2643%   s_1 \uparrow f \andalso s_2\uparrow f
2644%  }
2645%  {\verb+tal_base_call+~s_1~tlr_1\approx taa \append \verb+tal_base_call+~s_2~tlr_2}
2646% \vspace{1ex}
2647% \infrule
2648%  {tlr_1\approx tlr_2 \andalso
2649%   s_1 \uparrow f \andalso s_2\uparrow f \andalso
2650%   \verb+tal_collapsable+~tal_2
2651%  }
2652%  {\verb+tal_base_call+~s_1~tlr_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2)}
2653% \vspace{1ex}
2654% \infrule
2655%  {tlr_1\approx tlr_2 \andalso
2656%   s_1 \uparrow f \andalso s_2\uparrow f \andalso
2657%   \verb+tal_collapsable+~tal_1
2658%  }
2659%  {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_base_call+~s_2~tlr_2)}
2660% \vspace{1ex}
2661% \infrule
2662%  {tlr_1 \approx tlr_2 \andalso
2663%   s_1 \uparrow f \andalso s_2\uparrow f\andalso
2664%   tal_1 \approx tal_2 \andalso
2665%  }
2666%  {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2}
2667% \caption{The inference rule for the relation $\approx$.}
2668% \label{fig:txx_rel}
2669% \end{figure}
2670% %
2671% \begin{comment}
2672% \begin{verbatim}
2673% let rec tlr_rel S1 st1 st1' S2 st2 st2'
2674%   (tlr1 : trace_label_return S1 st1 st1')
2675%   (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
2676% match tlr1 with
2677%   [ tlr_base st1 st1' tll1 ⇒
2678%     match tlr2 with
2679%     [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
2680%     | _ ⇒ False
2681%     ]
2682%   | tlr_step st1 st1' st1'' tll1 tl1 ⇒
2683%     match tlr2 with
2684%     [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
2685%       tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
2686%     | _ ⇒ False
2687%     ]
2688%   ]
2689% and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
2690%  (tll1 : trace_label_label S1 fl1 st1 st1')
2691%  (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
2692%   match tll1 with
2693%   [ tll_base fl1 st1 st1' tal1 H ⇒
2694%     match tll2 with
2695%     [ tll_base fl2 st2 st2 tal2 G ⇒
2696%       as_label_safe … («?, H») = as_label_safe … («?, G») ∧
2697%       tal_rel … tal1 tal2
2698%     ]
2699%   ]
2700% and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
2701%  (tal1 : trace_any_label S1 fl1 st1 st1')
2702%  (tal2 : trace_any_label S2 fl2 st2 st2')
2703%    on tal1 : Prop ≝
2704%   match tal1 with
2705%   [ tal_base_not_return st1 st1' _ _ _ ⇒
2706%     fl2 = doesnt_end_with_ret ∧
2707%     ∃st2mid,taa,H,G,K.
2708%     tal2 ≃ taa_append_tal ? st2 ??? taa
2709%       (tal_base_not_return ? st2mid st2' H G K)
2710%   | tal_base_return st1 st1' _ _ ⇒
2711%     fl2 = ends_with_ret ∧
2712%     ∃st2mid,taa,H,G.
2713%     tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
2714%       (tal_base_return ? st2mid st2' H G)
2715%   | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒
2716%     fl2 = doesnt_end_with_ret ∧
2717%     ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
2718%     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
2719%     (* we must allow a tal_base_call to be similar to a call followed
2720%       by a collapsable trace (trace_any_any followed by a base_not_return;
2721%       we cannot use trace_any_any as it disallows labels in the end as soon
2722%       as it is non-empty) *)
2723%     (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
2724%       tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
2725%     ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
2726%     ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
2727%       tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
2728%       tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
2729%   | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
2730%     ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
2731%     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
2732%     (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
2733%       tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
2734%       tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
2735%     ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
2736%     ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
2737%       tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
2738%       tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
2739%   | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
2740%     tal_rel … tl1 tal2 (* <- this makes it many to many *)
2741%   ].
2742% \end{verbatim}
2743% \end{comment}
2744% %
2745% In the preceding rules, a $taa$ is an inhabitant of the
2746% $\verb+trace_any_any+~s_1~s_2$ (shorthand $\verb+TAA+~s_1~s_2$),
2747% an inductive data type whose definition
2748% is not in the paper for lack of space. It is the type of valid
2749% prefixes (even empty ones) of \verb+TAL+'s that do not contain
2750% any function call. Therefore it
2751% is possible to concatenate (using ``$\append$'') a \verb+TAA+ to the
2752% left of a \verb+TAL+. A \verb+TAA+ captures
2753% a sequence of silent moves.
2754% The \verb+tal_collapsable+ unary predicate over \verb+TAL+'s
2755% holds when the argument does not contain any function call and it ends
2756% with a label (not a return). The intuition is that after a function call we
2757% can still perform a sequence of silent actions while remaining similar.
2758%
2759% As should be expected, even though the rules are asymmetric $\approx$ is in fact
2760% an equivalence relation.
[3343]2761\bibliographystyle{splncs03}
2762\bibliography{ccexec}
2763
2764% \appendix
2765% \section{Notes for the reviewers}
2766%
[3369]2767% The results described in the paper are part of a larger formalisation
[3343]2768% (the certification of the CerCo compiler). At the moment of the submission
[3369]2769% we need to single out from the CerCo formalisation the results presented here.
[3343]2770% Before the 16-th of February we will submit an attachment that contains the
[3369]2771% minimal subset of the CerCo formalisation that allows to prove those results.
[3343]2772% At that time it will also be possible to measure exactly the size of the
[3369]2773% formalisation described here. At the moment a rough approximation suggests
[3343]2774% about 2700 lines of Matita code.
2775%
2776% We will also attach the development version of the interactive theorem
[3369]2777% prover Matita that compiles the submitted formalisation. Another possibility
[3343]2778% is to backport the development to the last released version of the system
2779% to avoid having to re-compile Matita from scratch.
2780%
[3369]2781% The programming and certification style used in the formalisation heavily
[3343]2782% exploit dependent types. Dependent types are used: 1) to impose invariants
2783% by construction on the data types and operations (e.g. a traces from a state
2784% $s_1$ to a state $s_2$ can be concatenad to a trace from a state
2785% $s_2'$ to a state $s_3$ only if $s_2$ is convertible with $s_2'$); 2)
2786% to state and prove the theorems by using the Russell methodology of
2787% Matthieu Sozeau\footnote{Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237-252.
[3347]2788% }, better known in the Coq world as ``\verb+Program+'' and reimplemented in a simpler way in Matita using coercion propagations\footnote{Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi: A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Logical Methods in Computer Science 8(1) (2012)}. However, no result presented depends
[3343]2789% mandatorily on dependent types: it should be easy to adapt the technique
2790% and results presented in the paper to HOL.
2791%
2792% Finally, Matita and Coq are based on minor variations of the Calculus of
2793% (Co)Inductive Constructions. These variations do not affect the CerCo
[3369]2794% formalisation. Therefore a porting of the proofs and ideas to Coq would be
[3343]2795% rather straightforward.
2796
2797\end{document}
Note: See TracBrowser for help on using the repository browser.