source: Papers/jar-cerco-2017/proof.tex

% Compiler proof
%   Structure of proof, and high-level discussion
%   Technical devices: structured traces, labelling, etc.
%   Assembler proof
%   Technical issues in front end (Brian?)
%   Main theorem statement

\section{Compiler proof}
\label{sect.compiler.proof}

\subsection{Labelling approach}

In this section, we will explore the labelling approach mentioned in the introduction in more detail.

The `labelling' approach to the problem of building
cost annotations is summarized in the following diagram.

\newcolumntype{M}[1]{>{\raggedright}m{#1}}

\-

\begin{tabular}{M{10cm}||M{4cm}}
$$
\xymatrix{
% Row 1
  L_1 \\
%
% Row 2
  L_{1,\ell} 
  \ar[u]^{\cl{I}}
  \ar@/^/[d]^{\w{er}_1} 
  \ar[r]^{\cl{C}_1} 
%
& L_{2,\ell} 
  \ar[d]^{\w{er}_2}  
%
& \ldots \hspace{0.3cm}\ar[r]^{\cl{C}_k} 
%
& L_{k+1, \ell} 
  \ar[d]^{\w{er}_{k+1}}  \\
%
% Row 3
  L_1                                  
  \ar@/^/[u]^{\cl{L}} 
  \ar[r]^{\cl{C}_1}
& L_2   
& \ldots\hspace{0.3cm}
  \ar[r]^{\cl{C}_{k}}
& L_{k+1}
}
$$
&
$$
\begin{array}{ccc}
\w{er}_{i+1} \comp \cl{C}_{i} &= &\cl{C}_{i} \comp \w{er}_{i} \\

\w{er}_{1} \comp \cl{L} &= &\w{id}_{L_{1}} \\ 

\w{An}_{1} &= &\cl{I} \comp \cl{L}  
\end{array}
$$
\end{tabular}

\-

For each language $L_i$ considered in the compilation process,
we define an extended {\em labelled} language $L_{i,\ell}$ and an
extended operational semantics. The labels are used to mark
certain points of the control. The semantics makes sure 
that whenever we cross a labelled control point a labelled and observable
transition is produced.

For each labelled language there is an obvious function $\w{er}_i$
erasing all labels and producing a program in the corresponding
unlabelled language.
The compilation functions $\cl{C}_i$ are extended from the unlabelled
to the labelled language so that they enjoy commutation 
with the erasure functions. Moreover, we lift the soundness properties of
the compilation functions from the unlabelled to the labelled languages
and transition systems.

A {\em labelling} $\cl{L}$  of the source language $L_1$ is just a function 
such that $\w{er}_{L_{1}} \comp \cl{L}$ is the identity function.
An {\em instrumentation} $\cl{I}$ of the source labelled language  $L_{1,\ell}$
is a function replacing the labels with suitable increments of, say, 
a fresh \w{cost} variable. Then an {\em annotation} $\w{An}_{1}$ of the 
source program can be derived simply as the composition of the labelling
and the instrumentation functions: $\w{An}_{1} = \cl{I}\comp \cl{L}$.

As for the direct approach, suppose $s$ is some adequate representation
of the state of a program. Let $S$ be a source program and suppose
that its annotation satisfies the following property:
\begin{equation}\label{STEP1}
(\w{An}_{1}(S),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]
\end{equation}
where $\delta$ is some non-negative number.
Then the definition of the instrumentation and the fact that
the soundness proofs of the compilation functions have been lifted
to the labelled languages allows to conclude that
\begin{equation}\label{step2}
(\cl{C}(L(S)),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)
\end{equation}
where $\cl{C} = \cl{C}_{k} \comp \cdots \comp \cl{C}_{1}$ and
$\lambda$ is a sequence (or a multi-set) of labels whose `cost'
corresponds to the number $\delta$ produced by the 
annotated program.
Then the commutation properties of erasure and compilation functions
allows to conclude that the {\em erasure} of the compiled
labelled code $\w{er}_{k+1}(\cl{C}(L(S)))$ is actually  equal to 
the compiled code $\cl{C}(S)$ we are interested in.
Given this, the following question arises: 

\begin{quote}
Under which conditions 
the sequence $\lambda$, {\em i.e.}, the increment $\delta$,
is a sound and possibly precise description of the
execution cost of the object code? 
\end{quote}

To answer this question, we observe that the object code we are interested in is some kind of assembly code 
and its control flow can be easily represented as a control flow
graph. The fact that we have to prove the soundness of the compilation
functions means that we have plenty of pieces of information
on the way the control flows in the compiled code, in particular as
far as procedure calls and returns are concerned.
These pieces of information allow to build a rather accurate representation
of the control flow of the compiled code at run time.

The idea is then to perform two simple checks on the control flow
graph. The first check is to verify that all loops go through a labelled node.
If this is the case then we can associate a finite cost with
every label and prove that the cost annotations are sound.
The second check amounts to verify that all paths starting from 
a label have the same cost. If this check is successful then we can
conclude that the cost annotations are precise. 

This approach, as published in~\cite{Ayache2012} is the one used in the CerCo project. However, it has some weaknesses, which we will describe in the next subsection. We also propose a method to resolve these weaknesses.

\subsection{Indexed labelling}

THe labelling approach as described above does not deal well with some optimisations the compiler might introduce, such as changes in the control flow. For example, the 8051 architecture does not have an instruction for
multi-word division, which means that a function containing loops has to be inserted into the code. In fact, this is symptomatic of a more general weakness: the inability to state different costs for different occurrences of labels,
where the difference might be originated by labels being duplicated along the compilation, or the costs being sensitive to the current state of execution.

We present a solution that addresses this weakness by introducing cost labels that are dependent on the iteration of their containing loop.
This is achieved by means of \emph{indexed labels}; all cost labels are decorated with formal indices coming from the loops containing such labels.
These indices allow us to keep track, even after multiple loop transformations, of which iteration of the original loop in the source code a particular label occurrence belongs to.
During the annotation stage of the source code, this information is presented to the user by means of \emph{dependent costs}.

Over the course of this section, we will use two specific types of optimisations to introduce the indexed labelling approach. We argue that these two types pose a good foundation for extending the labelling approach,
in order to cover more and more common optimisations, as well as gaining insight into how to integrate advanced cost estimation techniques, such as cache analysis, into the CerCo compiler.
Moreover loop peeling itself has the fortuitous property of enhancing and enabling other optimisations.
Experimentation with CerCo's untrusted prototype compiler, which implements constant propagation and partial redundancy elimination~\cite{PRE,muchnick}, show how loop peeling enhances those other optimisations.

\paragraph{Loop peeling}
Loop peeling consists in preceding the loop with a copy of its body, appropriately guarded.
This is used, in general, to trigger further optimisations, such as those that rely on execution information which can be computed at compile time, but which is erased by further iterations of the loop, or those that use the hoisted code to be more effective at eliminating redundant code.
Integrating this transformation in to the labelling approach would also allow the integration of the common case of cache analysis explained above; the analysis of cache hits and misses usually benefits from a form of \emph{virtual} loop peeling~\cite{cacheprediction}.

\paragraph{Loop unrolling}
This optimisation consists of the repetition of several copies of the body of the loop inside the loop itself (inserting appropriate guards, or avoiding them altogether if enough information about the loop's guard is available at compile time).
This can limit the number of (conditional or unconditional) jumps executed by the code and trigger further optimisations dealing with pipelining, if appropriate for the architecture.

\subsubsection{\imp{} with goto}\label{sec:defimp}
We briefly outline a toy language, \imp{} with \s{goto}s.
This language was designed in order to pose problems for the existing labelling approach, and as a testing ground for our new notion of indexed labels.

The syntax and operational semantics of \imp{} are presented in figure~\ref{fig:minimp}.
Note that we can augment the language with \s{break} and \s{continue} statements at no further expense.

\begin{figureplr}
$$\begin{gathered}
\begin{array}{nlBl>(R<)n}
\multicolumn{4}{C}{\bfseries Syntax}\\
\multicolumn{4}{ncn}{
  \ell,\ldots \hfill \text{(labels)} \hfill x,y,\ldots \hfill
\text{(identifiers)}
\hfill e,f,\ldots \hfill \text{(expression)}
}\\
P,S,T,\ldots &\gramm& \s{skip} \mid s;t
\mid \sop{if}e\sbin{then}s\sbin{else}t
\mid \sop{while} e \sbin{do} s \mid
  x \ass e
\\&\mid&
\ell : s \mid \sop{goto}\ell& \spanr{-2}{statements}\\
\\
\multicolumn{4}{C}{\bfseries Semantics}\\
K,\ldots  &\gramm& \s{halt} \mid S \cdot K & continuations
\end{array}
\\[15pt]
\s{find}(\ell,S,K) \ass
\left\{\begin{array}{lL}
\bot & if $S=\s{skip},\sop{goto} \ell'$ or $x\ass e$,\\
(T, K) & if $S=\ell:T$,\\
\s{find}(\ell,T,K) & otherwise, if $S = \ell':T$,\\
\s{find}(\ell,T_1,T_2\cdot K) & if defined and $S=T_1;T_2$,\\
\s{find}(\ell,T_1,K) & if defined and
$S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\
\s{find}(\ell,T_2,K) & otherwise, if $S=T_1;T_2$ or
$\sop{if}b\sbin{then}T_1\sbin{else}T_2$,\\
\s{find}(\ell,T,S\cdot K) & if $S = \sop{while}b\sbin{do}T$.
\end{array}\right.
\\[15pt]
\begin{array}{lBl}
(x:=e,K,s)  &\to_P& (\s{skip},K,s[v/x]) \qquad\mbox{if }(e,s)\eval v \\ \\

(S;T,K,s)  &\to_P& (S,T\cdot K,s) \\ \\

(\s{if} \ b \ \s{then} \ S \ \s{else} \ T,K,s)
&\to_P&\left\{
\begin{array}{ll}
(S,K,s) &\mbox{if }(b,s)\eval v \neq 0 \\
(T,K,s) &\mbox{if }(b,s)\eval 0
\end{array}
\right. \\ \\


(\s{while} \ b \ \s{do} \ S ,K,s)
&\to_P&\left\{
\begin{array}{ll}
(S,\s{while} \ b \ \s{do} \ S \cdot K,s) &\mbox{if }(b,s)\eval v \neq 0 \\
(\s{skip},K,s) &\mbox{if }(b,s)\eval 0
\end{array}
\right. \\ \\


(\s{skip},S\cdot K,s)  &\to_P&(S,K,s) \\ \\

(\ell : S, K, s)  &\to_P& (S,K,s) \\ \\

(\sop{goto}\ell,K,s)  &\to_P& (\s{find}(\ell,P,\s{halt}),s) \\ \\
\end{array}
\end{gathered}$$
\caption{The syntax and operational semantics of \imp.}
\label{fig:minimp}
\end{figureplr}

The precise grammar for expressions is not particularly relevant so we do not give one in full.
For the sake of conciseness we also treat boolean and arithmetic expressions together (with the usual \textsc{c} convention of an expression being true iff non-zero).
We may omit the \s{else} clause of a conditional if it leads to a \s{skip} statement.

We will presuppose that all programs are \emph{well-labelled}, \ie every label labels at most one occurrence of a statement in a program, and every \s{goto} points to a label actually present in the program.
The \s{find} helper function has the task of not only finding the labelled statement in the program, but also building the correct continuation.
The continuation built by \s{find} replaces the current continuation in the case of a jump.

\paragraph{Further down the compilation chain}
We abstract over the rest of the compilation chain.
We posit the existence of a suitable notion of `sequential instructions', wherein each instruction has a single natural successor to which we can add our own, for every language $L$ further down the compilation chain.

\subsubsection{Loop transformations}
We call a loop $L$ \emph{single-entry} in $P$ if there is no \s{goto} to $P$ outside of $L$ which jumps into $L$.\footnote{This is a reasonable aproximation: it defines a loop as multi-entry if it has an external but unreachable \s{goto} jumping into it.}
Many loop optimisations do not preserve the semantics of multi-entry loops in general, or are otherwise rendered ineffective.
Usually compilers implement a single-entry loop detection which avoids the multi-entry ones from being targeted by optimisations~\cite{muchnick,morgan}.
The loop transformations we present are local, \ie they target a single loop and transform it.
Which loops are targeted may be decided by some \emph{ad hoc} heuristic.
However, the precise details of which loops are targetted and how is not important here.

\paragraph{Loop peeling}
$$
\sop{while}b\sbin{do}S \mapsto \sop{if}b\sbin{then} S; \sop{while} b \sbin{do} S[\ell'_i/\ell_i]
$$
where $\ell'_i$ is a fresh label for any $\ell_i$ labelling a statement in $S$.
This relabelling is safe for \s{goto}s occurring outside the loop because of the single-entry condition.
Note that for \s{break} and \s{continue} statements, those should be replaced with \s{goto}s in the peeled body $S$.

\paragraph{Loop unrolling}
$$
\sop{while}b\sbin{do}S\mapsto
\sop{while} b \sbin{do} (S ;
  \sop{if} b \sbin{then} (S[\ell^1_i/\ell_i] ;
  \cdots
  \sop{if} b \sbin{then} S[\ell^n_i/\ell_i]) \cdots)
$$
where $\ell^j_i$ are again fresh labels for any $\ell_i$ labelling a statement in $S$.
This is a wilfully na\"{i}ve version of loop unrolling, which usually targets less general loops.
The problem this transformation poses to CerCo's labelling approach are independent of the sophistication of the actual transformation.

\begin{example}
In \autoref{fig:example1} we show a program (a wilfully inefficient computation of of the
sum of the first $n$ factorials) and a possible transformation of it, combining loop
peeling and loop unrolling.
\begin{figureplr}
$$
\fbox{$\begin{array}{l}
s\ass 0;\\
i\ass 0;\\
\sop{while}i<n\sbin{do}\\
\inde p\ass 1;\\
\inde j\ass 1;\\
\inde \sop{while}j \le i\sbin{do}\\
\inde \inde p\ass j*p\\
\inde \inde j\ass j+1;\\
\inde s\ass s+p;\\
\inde i\ass i+1;\\
\end{array}
$}
\mapsto
\fbox{$\begin{array}{l}
s\ass 0;\\
i\ass 0;\\
\tikztargetm{a}{\s{if}}\ i<n\sbin{then}\\
\inde p\ass 1;\\
\inde j\ass 1;\\
\inde \sop{while}j \le i\sbin{do}\\
\inde \inde p\ass j*p\\
\inde \inde j\ass j+1;\\
\inde s\ass s+p;\\
\inde i\ass i+1;\\
\inde \tikztargetm{d}{\s{while}}\ i<n\sbin{do}\\
\inde \inde p\ass 1;\\
\inde \inde j\ass 1;\\
\inde \inde \tikztargetm{b}{\s{if}}\ j \le i\sbin{then}\\
\inde \inde \inde p\ass j*p\\
\inde \inde \inde j\ass j+1;\\
\inde \inde \inde \sop{if}j \le i\sbin{then}\\
\inde \inde \inde \inde p\ass j*p\\
\inde \inde \inde \inde j\ass j+1;\\
\inde \inde \inde \inde \s{while}\ j \le i\sbin{do}\\
\inde \inde \inde \inde \inde p\ass j*p\\
\inde \inde \inde \inde \inde j\ass j+1;\\
\inde \inde \inde \inde \inde \sop{if}j \le i\sbin{then}\\
\inde \inde \inde \inde \inde \inde p\ass j*p\\
\inde \inde \inde \inde \inde \inde \tikztargetm{c}j\ass j+1;\\
\inde \inde s\ass s+p;\\
\inde \inde i\ass i+1;\\
\inde \inde \sop{if}i<n\sbin{then}\\
\inde \inde \inde p\ass 1;\\
\inde \inde \inde j\ass 1;\\
\inde \inde \inde \tikztargetm{e}{\s{while}}\ j < i\sbin{do}\\
\inde \inde \inde \inde p\ass j*p\\
\inde \inde \inde \inde j\ass j+1;\\
\inde \inde \inde \inde \s{if}\ j < i\sbin{then}\\
\inde \inde \inde \inde \inde p\ass j*p\\
\inde \inde \inde \inde \inde \tikztargetm{f}j\ass j+1;\\
\inde \inde \inde s\ass s+p;\\
\inde \inde \inde i\ass i+1\tikztargetm{g};{}
\end{array}
$}\tikztargetm{right}{}
\begin{tikzpicture}[overlay, remember picture, thick,
brace/.style = {decorate, decoration={brace, amplitude = 15pt}},
label/.style = {sloped, anchor = base, yshift = 17pt, font = \large}]
\draw [brace, transform canvas={xshift=5pt}] (b.north-|right) -- node[label]{peeled} (c.south-|right);
\draw [brace, transform canvas={xshift=30pt}] (b.north-|right) -- node[label]{unrolled} (c.south-|right);
\draw [brace, transform canvas={xshift=5pt}] (e.north-|right) -- node[label]{unrolled} (f.south-|right);
\draw [brace, transform canvas={xshift=55pt}] (d.north-|right) -- node[label]{unrolled} (g.south-|right);
\draw [brace, transform canvas={xshift=80pt}] (a.north-|right) -- node[label]{peeled} (g.south-|right);
\end{tikzpicture}
\hspace{85pt}{}
$$
\caption{An example of loop transformations done on an \imp{} program. Parentheses are omitted in favour of
blocks by indentation.}
\label{fig:example1}
\end{figureplr}
\end{example}

\subsubsection{Indexed labels}
\label{sec:indexedlabels}
This section presents the core of the new approach.
In brief points it amounts to the following:
\begin{enumerate}[\bfseries~\ref*{sec:indexedlabels}.1.]
\item
\label{en:outline1}
Enrich cost labels with formal indices corresponding, at the beginning of the process, to which iteration of the loop they belong to.
\item
\label{en:outline2}
Each time a loop transformation is applied and a cost labels is split in different occurrences, each of these will be reindexed so that every time they are emitted their position in the original loop will be reconstructed.
\item
\label{en:outline3}
Along the compilation chain, alongside the \s{emit} instruction we add other instructions updating the indices, so that iterations of the original loops can be rebuilt at the operational semantics level.
\item
\label{en:outline4}
The machinery computing the cost mapping will still work, but assigning costs to indexed cost labels, rather than to cost labels as we wish.
However, \emph{dependent costs} can be calculated, where dependency is on which iteration of the containing loops we are in.
\end{enumerate}

\subsubsection{Indexing the cost labels}
\label{ssec:indlabs}

\paragraph{Formal indices and $\iota\ell\imp$}
Let $i_0,i_1,\ldots$ be a sequence of distinguished fresh identifiers that will be used as loop indices.
A \emph{simple expression} is an affine arithmetical expression in one of these indices, that is $a*i_k+b$ with $a,b,k \in \mathbb N$.
Simple expressions $e_1=a_1*i_k+b_1$, $e_2=a2*i_k+b_2$ in the same index can be composed, yielding $e_1\circ e_2\ass (a_1a_2)*i_k + (a_1b2+b_1)$, and this operation has an identity element in $id_k \ass 1*i_k+0$.
Constants can be expressed as simple expressions, so that we identify a natural $c$ with $0*i_k+c$.

An \emph{indexing} (with metavariables $I$, $J$, \ldots) is a list of transformations of successive formal indices dictated by simple expressions, that is a mapping\footnote{Here we restrict each mapping to be a simple expression \emph{on the same index}.
This might not be the case if more loop optimisations are accounted for (for example, interchanging two nested loops).}
$$
i_0\mapsto a_0*i_0+b_0,\dots, i_{k-1} \mapsto a_{k-1}*i_{k-1}+b_{k-1}
$$

An \emph{indexed cost label} (metavariables $\alphab$, $\betab$, \ldots) is the combination of a cost label $\alpha$ and an indexing $I$, written $\alpha\la I\ra$.
The cost label underlying an indexed one is called its \emph{atom}.
All plain labels can be considered as indexed ones by taking an empty indexing.

\imp{} with indexed labels ($\iota\ell\imp$) is defined by adding to $\imp$ statements with indexed labels, and by having loops with formal indices attached to them:
$$
S,T,\ldots \gramm \cdots i_k:\sop{while}e\sbin{do}S\mid \alphab : S
$$
Note than unindexed loops still exist in the language: they will correspond to multi-entry loops which are ignored by indexing and optimisations.
We will discuss the semantics later.

\paragraph{Indexed labelling}
Given an $\imp$ program $P$, in order to index loops and assign indexed labels, we must first distinguish single-entry loops.
We sketch how this can be computed in the sequel.

A first pass of the program $P$ can easily compute two maps: $\s{loopof}_P$ from each label $\ell$ to the occurrence (\ie the path) of a $\s{while}$ loop containing $\ell$, or the empty path if none exists; and $\s{gotosof}_P$ from a label $\ell$ to the occurrences of \s{goto}s pointing to it.
Then the set $\s{multientry}_P$ of multi-entry loops of $P$ can be computed by
$$
\s{multientry}_P\ass\{\, p \mid \exists \ell,q.p =\s{loopof}_P(\ell),q\in\s{gotosof}_P(\ell), q \not\le p\,\}
$$
Here $\le$ is the prefix relation\footnote{Possible simplifications to this procedure include keeping track of just the while loops containing labels and \s{goto}s (rather than paths in the syntactic tree of the program), and making two passes while avoiding building the map to sets $\s{gotosof}$}.

Let $Id_k$ be the indexing of length $k$ made from identity simple expressions, \ie the sequence $i_0\mapsto id_0, \ldots , i_{k-1}\mapsto id_{k-1}$.
We define the tiered indexed labelling $\Ell^\iota_P (S,k)$ in program $P$ for occurrence $S$ of a statement in $P$ and a natural $k$ by recursion, setting:
$$
\Ell^\iota_P(S,k)\ass
\left\{
\begin{array}{lh{-100pt}l}
 (i_k:\sop{while}b\sbin{do}\alpha\la Id_{k+1}\ra : \Ell^\iota_P(T,k+1));\beta\la Id_k \ra : \s{skip}
\\& \text{if $S=\sop{while}b\sbin{do}T$ and $S\notin \s{multientry}_P$,}\\[3pt]
(\sop{while}b\sbin{do}\alpha\la Id_k \ra : \Ell^\iota_P(T,k));\beta\la Id_k \ra : \s{skip}
\\& \text{otherwise, if $S=\sop{while}b\sbin{do}T$,}\\[3pt]
\sop{if}b\sbin{then} \alpha\la Id_k \ra : \Ell^\iota_P(T_1,k) \sbin{else} \beta\la Id_k \ra : \Ell^\iota_P(T_2,k)
\\&\text{if $S=\sop{if}b\sbin{then}T_1\sbin{else}T_2$,}\\[3pt]
\ell:\alpha\la Id_k\ra : \Ell_P^\iota(T,k) & \text{if $S = \ell : T$,}\\[3pt]
\ldots
\end{array}
\right.
$$
Here, as usual, $\alpha$ and $\beta$ are fresh cost labels, and other cases just keep making the recursive calls on the substatements.
The \emph{indexed labelling} of a program $P$ is then defined as $\alpha\la \ra : \Ell^\iota_P(P,0)$, \ie a further fresh unindexed cost label is added at the start, and we start from level $0$.

In plainer words: each single-entry loop is indexed by $i_k$ where $k$ is the number of other single-entry loops containing this one, and all cost labels under the scope of a single-entry loop indexed by $i_k$ are indexed by all indices $i_0,\ldots,i_k$, without any transformation.

\subsubsection{Indexed labels and loop transformations}\label{ssec:looptrans}
We define the \emph{reindexing} $I \circ (i_k\mapsto a*i_k+b)$ as an operator on indexings by setting:
\begin{multline*}
(i_0\mapsto e_0,\ldots, i_k \mapsto e_k,\ldots,i_n\mapsto e_n)
\circ(i_k\mapsto a*i_k+b)
\ass\\
i_0\mapsto e_0,\ldots, i_k \mapsto e_k \circ(a*i_k+b),\ldots,i_n\mapsto e_n,
\end{multline*}
We further extend to indexed labels (by $\alpha\la I\ra\circ(i_k\mapsto e)\ass \alpha\la I\circ (i_k\mapsto e)\ra$) and also to statements in $\iota\ell\imp$ (by applying the above transformation to all indexed labels).

We can then redefine loop peeling and loop unrolling, taking into account indexed labels.
It will only be possible to apply the transformation to indexed loops, that is loops that are single-entry.
The attentive reader will notice that no assumptions are made on the labelling of the statements that are involved.
In particular the transformation can be repeated and composed at will.
Also, note that after erasing all labelling information (\ie indexed cost labels and loop indices) we recover exactly the same transformations presented in~\ref{sec:defimp}.

\paragraph{Indexed loop peeling}
$$
i_k:\sop{while}b\sbin{do}S\mapsto
\sop{if}b\sbin{then} S\circ (i_k\mapsto 0); i_k : \sop{while} b \sbin{do} S[\ell'_i/\ell_i]\circ(i_k\mapsto i_k + 1)
$$
As can be expected, the peeled iteration of the loop gets reindexed, always being the first iteration of the loop, while the iterations of the remaining loop are shifted by $1$. Notice that this transformation can lower the actual depth of some loops, however their index is left untouched.

\paragraph{Indexed loop unrolling}
$$
\begin{array}{l}
\begin{array}{ncn}
i_k:\sop{while}b\sbin{do}S\\
\tikz\node[rotate=-90,inner sep=0pt]{$\mapsto$};
\end{array}\\
i_k:\sop{while} b \sbin{do}\\
\quad (S\circ(i_k\mapsto n*i_k) ;\\
\quad \sop{if} b \sbin{then}\\
\quad\quad (S[\ell^1_i/\ell_i]\circ(i_k\mapsto n*i_k+1) ;\\
\quad\quad\quad \vdots \\
\quad\quad \quad \sop{if} b \sbin{then}\\
\quad \quad \quad \quad S[\ell^n_i/\ell_i]\circ(i_k\mapsto n*i_k+n-1)
)\cdots )
\end{array}
$$
Again, the reindexing is as expected: each copy of the unrolled body has its indices remapped so that when they are executed, the original iteration of the loop to which they correspond can be recovered.

\subsubsection{Semantics and compilation of indexed labels}
In order to make sense of loop indices, one must keep track of their values in the state.
A \emph{constant indexing} (metavariables $C,\ldots$) is an indexing which employs only constant simple expressions.
The evaluation of an indexing $I$ in a constant indexing $C$, noted $I|_C$, is defined by:
$$
I\circ(i_0\mapsto c_0,\ldots, i_{k-1}\mapsto c_{k-1}) \ass \alphab\circ(i_0\mapsto c_0)\circ\cdots\circ(i_{k-1}\mapsto c_{k-1})
$$
Here, we are using the definition of ${-}\circ{-}$ given in~\ref{ssec:indlabs}.
We consider the above defined only if the the resulting indexing is a constant one too\footnote{For example $(i_0\mapsto 2*i_0,i_1\mapsto i_1+1)|_{i_0\mapsto 2}$ is undefined, but $(i_0\mapsto 2*i_0,i_1\mapsto 0)|_{i_0\mapsto 2}= i_0\mapsto 4,i_1\mapsto 2$, is indeed a constant indexing, even if the domain of the original indexing is not covered by the constant one.}.
The definition is extended to indexed labels by $\alpha\la I\ra|_C\ass \alpha\la I|_C\ra$.

Constant indexings will be used to keep track of the exact iterations of the original code that the emitted labels belong to.
We thus define two basic actions to update constant indexings: $C[i_k{\uparrow}]$ increments the value of $i_k$ by one, and $C[i_k{\downarrow}0]$ resets it to $0$.

We are ready to update the definition of the operational semantics of indexed labelled \imp.
The emitted cost labels will now be ones indexed by constant indexings.
We add a special indexed loop construct for continuations that keeps track of active indexed loop indices:
$$
K,\ldots  \gramm \cdots | i_k:\sop{while} b \sbin {do} S \sbin{then}  K
$$
The difference between the regular stack concatenation $i_k:\sop{while}b\sbin{do}S\cdot K$ and the new constructor is that the latter indicates the loop is the active one in which we already are, while the former is a loop that still needs to be started\footnote{In the presence of \s{continue} and \s{break} statements active loops need to be kept track of in any case.}.
The \s{find} function is updated accordingly with the case
$$
\s{find}(\ell, i_k:\sop{while}b\sbin{do}S, K) \ass \s{find}(\ell, S, i_k: \sop{while}b\sbin{do}S\sbin{then}K)
$$
The state will now be a 4-tuple $(S,K,s,C)$ which adds a constant indexing to the triple of the regular semantics.
The small-step rules for all statements remain the same, without touching the $C$ parameter (in particular unindexed loops behave the same as usual), apart from the ones regarding cost-labels and indexed loops.
The remaining cases are:
$$\begin{aligned}
   (\alphab : S,K,s,C) &\to[\alphab|_C]_P (S,K,s,C)\\
   (i_k:\sop{while}b\sbin{do}S,K,C) &\to[\varepsilon]_P
    \begin{cases}
     (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\downarrow}0])
     \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
     \rlap{(\s{skip}, K, s, C)}\hskip 125pt \text{otherwise}
    \end{cases}\\
   (\s{skip}, i_k:\sop{while}b\sbin{do}S\sbin{then}K,C) &\to[\varepsilon]_P
    \begin{cases}
     (S,i_k:\sop{while}b\sbin{do}S\sbin{then} K,s,C[i_k{\uparrow}])
      \\\hskip 125pt \text{if $(b,s)\eval v\neq 0$,}\\
     \rlap{(\s{skip}, K, s, C)} \hskip 125pt \text{otherwise}
    \end{cases}
  \end{aligned}$$
Some explanations are in order:
\begin{itemize}
\item
Emitting a label always instantiates it with the current indexing.
\item
Hitting an indexed loop the first time initializes the corresponding index to 0; continuing the same loop increments the index as expected.
\item
The \s{find} function ignores the current indexing: this is correct under the assumption that all indexed loops are single entry, so that when we land inside an indexed loop with a \s{goto}, we are sure that its current index is right.
\item
The starting state with store $s$ for a program $P$ is $(P,\s{halt},s,(i_0\mapsto 0,\dots,i_{n-1}\mapsto 0)$ where $i_0,\ldots,i_{n-1}$ cover all loop indices of $P$\footnote{For a program which is the indexed labelling of an \imp{} one this corresponds to the maximum nesting of single-entry loops.
We can also avoid computing this value in advance if we define $C[i{\downarrow}0]$ to extend $C$'s domain as needed, so that the starting constant indexing can be the empty one.}.
\end{itemize}

\paragraph{Compilation}
Further down the compilation chain the loop structure is usually partially or completely lost.
We cannot rely on it anymore to keep track of the original source code iterations.
We therefore add, alongside the \s{emit} instruction, two other sequential instructions $\sop{ind_reset}k$ and $\sop{ind_inc}k$ whose sole effect is to reset to 0 (resp.\ increment by 1) the loop index $i_k$, as kept track of in a constant indexing accompanying the state.

The first step of compilation from $\iota\ell\imp$ consists of prefixing the translation of an indexed loop $i_k:\s{while}\ b\ \s{do}\ S$ with $\sop{ind_reset}k$ and postfixing the translation of its body $S$ with $\sop{ind_inc}k$.
Later in the compilation chain we must propagate the instructions dealing with cost labels.

We would like to stress the fact that this machinery is only needed to give a suitable semantics of observables on which preservation proofs can be done.
By no means are the added instructions and the constant indexing in the state meant to change the actual (let us say denotational) semantics of the programs.
In this regard the two new instruction have a similar role as the \s{emit} one.
A forgetful mapping of everything (syntax, states, operational semantics rules) can be defined erasing all occurrences of cost labels and loop indices, and the result will always be a regular version of the language considered.

\paragraph{Stating the preservation of semantics}
In fact, the statement of preservation of semantics does not change at all, if not for considering traces of evaluated indexed cost labels rather than traces of plain ones.

\subsubsection{Dependent costs in the source code}
\label{ssec:depcosts}
The task of producing dependent costs from constant costs induced by indexed labels is quite technical.
Before presenting it here, we would like to point out that the annotations produced by the procedure described in this Subsection, even if correct, can be enormous and unreadable.
In Section~\ref{sec:conc}, where we detail the actual implementation, we will also sketch how we mitigated this problem.

Having the result of compiling the indexed labelling $\Ell^\iota(P)$ of an \imp{} program $P$, we may still suppose that a cost mapping can be computed, but from indexed labels to naturals.
We want to annotate the source code, so we need a way to express and compute the costs of cost labels, \ie group the costs of indexed labels to ones of their atoms.
In order to do so we introduce \emph{dependent costs}.
Let us suppose that for the sole purpose of annotation, we have available in the language ternary expressions of the form
$$\tern e {f_1}{f_2},$$
and that we have access to common operators on integers such as equality, order and modulus.

\paragraph{Simple conditions}

First, we need to shift from \emph{transformations} of loop indices to \emph{conditions} on them.
We identify a set of conditions on natural numbers which are able to express the image of any composition of simple expressions.
\emph{Simple conditions} are of three possible forms:
\begin{itemize}
\item
Equality $i_k=n$ for some natural $n$.
\item
Inequality $i_k\ge n$ for some natural $n$.
\item
Modular equality together with inequality $i_k\bmod a = b\wedge i_k\ge n$ for naturals $a, b, n$.
\end{itemize}
The `always true' simple condition is given by $i_k\ge 0$.
We write $i_k\bmod a = b$ as a simple condition for $i_k\bmod a = b\wedge i_k\ge 0$.

Given a simple condition $p$ and a constant indexing $C$ we can easily define when $p$ holds for $C$ (written $p\circ C$).
A \emph{dependent cost expression} is an expression built solely out of integer constants and ternary expressions with simple conditions at their head.
Given a dependent cost expression $e$ where all of the loop indices appearing in it are in the domain of a constant indexing $C$, we can define the value $e\circ C\in \mathbb N$ by:
$$n\circ C\ass n,\qquad (\tern p e f)\circ C\ass
\begin{cases}
  e\circ C& \text{if $p\circ C$,}\\
  f\circ C& \text{otherwise.}
\end{cases}$$

\paragraph{From indexed costs to dependent ones}
Every simple expression $e$ corresponds to a simple condition $p(e)$ which expresses the set of values that $e$ can take.
Following is the definition of such a relation.
We recall that in this development, loop indices are always mapped to simple expressions over the same index.
If it was not the case, the condition obtained from an expression should be on the mapped index, not the indeterminate of the simple expression.
We leave all generalisations of what we present here for further work:
$$
p(a*i_k+b)\ass
\begin{cases}
i_k = b & \text{if $a = 0$,}\\
i_k \ge b & \text{if $a = 1$,}\\
i_k\bmod a = b' \wedge i_k \ge b & \text{otherwise, where $b' = b\bmod a$}.
\end{cases}
$$
Now, suppose we are given a mapping $\kappa$ from indexed labels to natural numbers.
We will transform it in a mapping (identified, via abuse of notation, with the same symbol $\kappa$) from atoms to \imp{} expressions built with ternary expressions which depend solely on loop indices.
To that end we define an auxiliary function $\kappa^\alpha_L$, parameterized by atoms and words of simple expressions, and defined on \emph{sets} of $n$-uples of simple expressions (with $n$ constant across each such set, \ie each set is made of words all with the same length).

We will employ a bijection between words of simple expressions and indexings, given by:\footnote{Lists of simple expressions are in fact how indexings are -represented in CerCo's current implementation of the compiler.}
$$
i_0\mapsto e_0,\ldots,i_{k-1}\mapsto e_{k-1} \cong e_0\cdots e_{k-1}.
$$
As usual, $\varepsilon$ denotes the empty word/indexing, and juxtaposition is used to denote word concatenation.

For every set $s$ of $n$-uples of simple expressions, we are in one of the following three exclusive cases:
\begin{itemize}
\item
$S=\emptyset$.
\item
$S=\{\varepsilon\}$.
\item
There is a simple expression $e$ such that $S$ can be decomposed in $eS'+S''$, with $S'\neq \emptyset$ and none of the words in $S''$ starting with $e$.
\end{itemize}
Here $eS'$ denotes prepending $e$ to all elements of $S'$ and $+$ is disjoint union.
This classification can serve as the basis of a definition by recursion on $n+\card S$ where $n$ is the size of tuples in $S$ and $\card S$ is its cardinality.
Indeed in the third case in $S'$ the size of tuples decreases strictly (and cardinality does not increase) while for $S''$ the size of tuples remains the same but cardinality strictly decreases.
The expression $e$ of the third case will be chosen as minimal for some total order\footnote{The specific order used does not change the correctness of the procedure, but different orders can give more or less readable results. A ``good'' order is the lexicographic one, with $a*i_k+b \le a'*i_k+b'$ if $a<a'$ or $a=a'$ and $b\le b'$.}.

Following is the definition of the auxiliary function $\kappa^\alpha_L$, which follows the recursion scheme presented above:
$$
\begin{aligned}
\kappa^\alpha_L(\emptyset) &\ass 0\\
\kappa^\alpha_L(\{\varepsilon\}) &\ass \kappa(\alpha\la L\ra) \\
\kappa^\alpha_L(eS'+S'') &\ass \tern{p(e)}{\kappa^\alpha_{Le}(S')}{\kappa^\alpha_L(S'')}
\end{aligned}
$$
\noindent
Finally, the wanted dependent cost mapping is defined by
$$
\kappa(\alpha)\ass\kappa^\alpha_\varepsilon(\{\,L\mid \alpha\la L\ra \text{ appears in the compiled code}\,\})
$$

\paragraph{Indexed instrumentation}
The \emph{indexed instrumentation} generalises the instrumentation presented in~\ref{sec:labelling}.
We described above how cost atoms can be mapped to dependent costs.
The instrumentation must also insert code dealing with the loop indices.
As instrumentation is done on the code produced by the labelling phase, all cost labels are indexed by identity indexings.
The relevant cases of the recursive definition (supposing $c$ is the cost variable) are then:
$$
\begin{aligned}
\mathcal I^\iota(\alpha\la Id_k\ra:S) &= c\ass c + \kappa(\alpha);\mathcal I^\iota(S)\\
\mathcal I^\iota(i_k : \sop{while}b\sbin{do}S) &=
  i_k \ass 0; \sop{while}b\sbin{do}(\mathcal I^\iota (S); i_k \ass i_k + 1)
\end{aligned}
$$

\subsubsection{A detailed example}\label{ssec:detailedex}
Take the program in \autoref{fig:example1}. Its initial labelling will be:
$$\begin{array}{l}
\alpha\la\ra : s\ass 0;\\
i\ass 0;\\
i_0:\sop{while}i<n\sbin{do}\\
\inde \beta\la i_0\ra : p\ass 1;\\
\inde j\ass 1;\\
\inde i_1:\sop{while}j \le i\sbin{do}\\
\inde \inde \gamma\la i_0, i_1\ra : p\ass j*p\\
\inde \inde j\ass j+1;\\
\inde \delta\la i_0\ra : s\ass s+p;\\
\inde i\ass i+1;\\
\epsilon\la\ra:\s{skip}
\end{array}
$$
(a single \s{skip} after the $\delta$ label has been suppressed, and we are using the identification
between indexings and tuples of simple expressions explained in \autoref{ssec:depcosts}).
Supposing for example, $n=3$
the trace of the program will be
$$\alpha\la\ra\,\beta\la 0 \ra\, \delta\la 0\ra\,\beta\la 1\ra\,\gamma\la 1,0\ra\,
\delta\la 1\ra\,\beta\la 2\ra\,\gamma\la 2,0\ra\,\gamma\la 2, 1\ra\,\delta\la 2\ra\,
\epsilon\la\ra$$
Now let as apply the transformations of \autoref{fig:example1} with the additional
information detailed in \autoref{ssec:looptrans}. The result is shown in
\autoref{fig:example2}.
\begin{figureplr}
$$
\begin{array}{l}
\mbox{\color{blue}\boldmath$\alpha\la\ra $}:s\ass 0;\\
i\ass 0;\\
\tikztargetm{a}{\s{if}}\ i<n\sbin{then}\\
\inde \mbox{\color{blue}\boldmath$\beta\la0\ra $}:p\ass 1;\\
\inde j\ass 1;\\
\inde i_1:\sop{while}j \le i\sbin{do}\\
\inde \inde \mbox{\color{blue}\boldmath$\gamma\la 0, i_1\ra $}:p\ass j*p\\
\inde \inde j\ass j+1;\\
\inde \mbox{\color{blue}\boldmath$\delta\la 0\ra $}: s\ass s+p;\\
\inde i\ass i+1;\\
\inde i_0:\tikztargetm{d}{\s{while}}\ i<n\sbin{do}\\
\inde \inde \mbox{\color{blue}\boldmath$\beta\la 2*i_0+1\ra $}:p\ass 1;\\
\inde \inde j\ass 1;\\
\inde \inde \tikztargetm{b}{\s{if}}\ j \le i\sbin{then}\\
\inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la  2*i_0+1, 0\ra $}:p\ass j*p\\
\inde \inde \inde j\ass j+1;\\
\inde \inde \inde \sop{if}j \le i\sbin{then}\\
\inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la  2*i_0+1, 1\ra $}: p\ass j*p\\
\inde \inde \inde \inde j\ass j+1;\\
\inde \inde \inde \inde i_1:\s{while}\ j \le i\sbin{do}\\
\inde \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la  2*i_0+1, 2*i_1 + 2 \ra $}:p\ass j*p\\
\inde \inde \inde \inde \inde j\ass j+1;\\
\inde \inde \inde \inde \inde \sop{if}j \le i\sbin{then}\\
\inde \inde \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la  2*i_0+1, 2*i_1 + 3\ra $}:p\ass j*p\\
\inde \inde \inde \inde \inde \inde \tikztargetm{c}j\ass j+1;\\
\inde \inde \mbox{\color{blue}\boldmath$\delta\la 2*i_0+1\ra$}: s\ass s+p;\\
\inde \inde i\ass i+1;\\
\inde \inde \sop{if}i<n\sbin{then}\\
\inde \inde \inde \mbox{\color{blue}\boldmath$\beta\la 2*i_0+2\ra $}:p\ass 1;\\
\inde \inde \inde j\ass 1;\\
\inde \inde \inde i_1:\tikztargetm{e}{\s{while}}\ j < i\sbin{do}\\
\inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la 2*i_0+2, 2*i_1\ra$}: p\ass j*p\\
\inde \inde \inde \inde j\ass j+1;\\
\inde \inde \inde \inde \s{if}\ j < i\sbin{then}\\
\inde \inde \inde \inde \inde \mbox{\color{blue}\boldmath$\gamma\la2*i_0+2, 2*i_1+1\ra$}: p\ass j*p\\
\inde \inde \inde \inde \inde \tikztargetm{f}j\ass j+1;\\
\inde \inde \inde \mbox{\color{blue}\boldmath$\delta\la 2*i_0+2\ra $}: s\ass s+p;\\
\inde \inde \inde i\ass i+1\tikztargetm{g};{}\\
\mbox{\color{blue}\boldmath$\epsilon\la\ra $}:\s{skip}
\end{array}$$
\caption{The result of applying reindexing loop transformations on the
program in \autoref{fig:example1}.}\label{fig:example2}
\end{figureplr}
One can check that the transformed code leaves the same trace when executed.

Now let us compute the dependent cost of $\gamma$, supposing no other loop transformations
are done. Ordering its indexings we
have the following list:
\begin{equation}
\label{eq:inds} 
\begin{aligned}
  &0, i_1\\
  &2*i_0+1, 0\\
  &2*i_0+1, 1\\
  &2*i_0+1, 2*i_1+2\\
  &2*i_0+1, 2*i_1+3\\
  &2*i_0+2, 2*i_1\\
  &2*i_0+2, 2*i_1+1
  \end{aligned}
\end{equation}

The resulting dependent cost will then be
\def\indetern#1#2#3{\begin{tabular}[t]{nL}(#1)\mathrel ?{}\\\hskip 15pt #2:{}\\\hskip 15pt #3\end{tabular}}
\def\tern#1#2#3{(#1)\mathrel ? #2:#3}
\begin{equation}\label{eq:ex}
\kappa^\iota(\gamma)=
\indetern{i_0 = 0}
  {\tern{i_1\ge 0}a0}
  {\indetern{i_0\bmod 2 = 1 \wedge i_0\ge 1}
    {\indetern{i_1=0}
      b
      {\indetern{i_1 = 1}
        c
        {\indetern{i_1\bmod 2 = 0 \wedge i_1\ge 2}
          d
          {\tern{i_1\bmod 2 = 1 \wedge i_1\ge 3}e0}
        }
      }
    }
    {\indetern{i_0\bmod 2 = 0 \wedge i_0\ge 2}
      {\indetern{i_1 \bmod 2 = 0 \wedge i_1 \ge 0}
        f
        {\tern{i_1 \bmod 2 = 1 \wedge i_1 \ge 1}g0}
      }
      0
    }
  }
\end{equation}
We will see later on \autopageref{pag:continued} how such an expression can be simplified.

\subsection{Notes on the implementation and further work}
\label{sec:conc}
Implementing the indexed label approach in CerCo's untrusted Ocaml prototype does not introduce many new challenges beyond what has already been presented for the toy language, \imp{} with \s{goto}s.
\s{Clight}, the \s{C} fragment source language of CerCo's compilation chain~\cite{D2.1}, has several more fetaures, but few demand changes in the indexed labelled approach.

\paragraph{Indexed loops \emph{vs}. index update instructions}
In our presentation we have indexed loops in $\iota\ell\imp$, while we hinted that later languages in the compilation chain would have specific index update instructions.
In CerCo's actual compilation chain from \s{Clight} to 8051 assembly, indexed loops are only in \s{Clight}, while from \s{Cminor} onward all languages have the same three cost-involving instructions: label emitting, index resetting and index incrementing.

\paragraph{Loop transformations in the front end}
We decided to implement the two loop transformations in the front end, namely in \s{Clight}.
This decision is due to user readability concerns: if costs are to be presented to the programmer, they should depend on structures written by the programmer himself.
If loop transformation were performed later it would be harder to create a correspondence between loops in the control flow graph and actual loops written in the source code.
However, another solution would be to index loops in the source code and then use these indices later in the compilation chain to pinpoint explicit loops of the source code: loop indices can be used to preserve such information, just like cost labels.

\paragraph{Break and continue statements}
\s{Clight}'s loop flow control statements for breaking and continuing a loop are equivalent to appropriate \s{goto} statements.
The only difference is that we are assured that they cannot cause loops to be multi-entry, and that when a transformation such as loop peeling is complete, they need to be replaced by actual \s{goto}s (which happens further down the compilation chain anyway).

\paragraph{Function calls}
Every internal function definition has its own space of loop indices.
Executable semantics must thus take into account saving and resetting the constant indexing of current loops upon hitting a function call, and restoring it upon return of control.
A peculiarity is that this cannot be attached to actions that save and restore frames: namely in the case of tail calls the constant indexing needs to be saved whereas the frame does not.

\paragraph{Cost-labelled expressions}
In labelled \s{Clight}, expressions also get cost labels, due to the presence of ternary conditional expressions (and lazy logical operators, which get translated to ternary expressions too).
Adapting the indexed labelled approach to cost-labelled expressions does not pose any particular problems.

\paragraph{Simplification of dependent costs}
As previously mentioned, the na\"{i}ve application of the procedure described in~\ref{ssec:depcosts} produces unwieldy cost annotations.
In our implementation several transformations are used to simplify such complex dependent costs.

Disjunctions of simple conditions are closed under all logical operations, and it can be computed whether such a disjunction implies a simple condition or its negation.
This can be used to eliminate useless branches of dependent costs, to merge branches that share the same value, and possibly to simplify the third case of simple condition.
Examples of the three transformations are respectively:
\begin{itemize}
\item $
\verb+(_i_0 == 0)?+x\verb+:(_i_0 >= 1)?+y\verb+:+z
\mapsto
\verb+(_i_0 == 0)?+x\verb+:+y,
$
\item $
c\texttt{?}x\verb+:(+d\texttt{?}x\texttt{:}y\verb+)+
\mapsto
\texttt{(}c\texttt{ || }d\texttt{)?}x\texttt{:}y,
$
\item \begin{tabular}[t]{np{\linewidth}n}
$\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0 && _i_0 >= 2)?+y\verb+:+z
\mapsto$ \\\hfill
$\verb+(_i_0 == 0)?+x\verb+:(_i_0 % 2 == 0)?+y\verb+:+z.
$\end{tabular}
\end{itemize}
The second transformation tends to accumulate disjunctions, to the detriment of readability.
A further transformation swaps two branches of the ternary expression if the negation of the condition can be expressed with fewer clauses.
For example:
$$ \verb+(_i_0 % 3 == 0 || _i_0 % 3 == 1)?+x\verb+:+y \mapsto
\verb+(_i_0 % 3 == 2)?+y\verb+:+x.
$$
Picking up again the example depicted in \autoref{ssec:detailedex}, \label{pag:continued}
we can see that the cost in \eqref{eq:ex} can be simplified to the following,
using some of the transformation described above:
$$
\kappa^\iota(\gamma)=
\indetern{i_0 = 0}
  a
  {\indetern{i_0\bmod 2 = 1}
    {\indetern{i_1=0}
      b
      {\indetern{i_1 = 1}
        c
        {\indetern{i_1\bmod 2 = 0}
          de
        }
      }
    }
    {\indetern{i_1 \bmod 2 = 0}
      fg
    }
  }
$$
One should keep in mind that the example was wilfully complicated, in practice
the cost expressions produced have rarely more clauses
than the number of nested loops containing the annotation.
\paragraph{Updates to the frama-C cost plugin}
Cerco's frama-C~\cite{framac} cost plugin\todo{is there a reference for this?}{} has been updated to take into account our new notion of dependent costs.
The frama-c framework expands ternary expressions to branch statements, introducing temporaries along the way.
This makes the task of analyzing ternary cost expressions rather daunting.
It was deemed necessary to provide an option in the compiler to use actual branch statements for cost annotations rather than ternary expressions, so that at least frama-C's use of temporaries in cost annotation could be avoided.
The cost analysis carried out by the plugin now takes into account such dependent costs.

The only limitation (which actually simplifies the code) is that, within a dependent cost, simple conditions with modulus on the same loop index should not be modulo different numbers.
This corresponds to a reasonable limitation on the number of times loop unrolling may be applied to the same loop: at most once.

%%% HERE BEGINS A NEW BIT

\section{Introduction}

The \cerco{} compiler produces a version of the source code containing
annotations describing the timing behaviour of the object code, as
well as the object code itself. It compiles C code, targeting
microcontrollers implementing the Intel 8051 architecture.  There are
two versions: first, an initial prototype was implemented in
\ocaml{}~\cite{d2.2}, then a version was formalised in the \matita{}
proof assistant~\cite{d3.2,d4.2} and extracted to \ocaml{} code to
produce an executable compiler.  In this document we present results
from Deliverable 3.4, the formalised proofs in \matita{} about the
front-end of the latter version of the compiler (culminating in the
\lstinline'front_end_correct' lemma), and describe how that fits
into the verification of the whole compiler.

A key part of this work was to layer the \emph{intensional} correctness
results that show that the costs produced are correct on top of the
proofs about the compiled code's \emph{extensional} behaviour (that is, the
functional correctness of the compiler).  Unfortunately, the ambitious
goal of completely verifying the entire compiler was not feasible
within the time available, but thanks to this separation of
extensional and intensional proofs we are able to axiomatise some extensional
simulation results which are similar to those in other compiler verification
projects and concentrate on the novel intensional proofs.  We were
also able to add stack space costs to obtain a stronger result.  The
proofs were made more tractable by introducing compile-time checks for
the `sound and precise' cost labelling properties rather than proving
that they are preserved throughout.

The overall statement of correctness says that the annotated program has the
same behaviour as the input, and that for any suitably well-structured part of
the execution (which we call \emph{measurable}), the object code will execute
the same behaviour taking precisely the time given by the cost annotations in
the annotated source program.

In the next section we recall the structure of the compiler and make the overall
statement more precise.  Following that, in Section~\ref{sec:fegoals} we
describe the statements we need to prove about the intermediate \textsf{RTLabs}
programs for the back-end proofs.
Section~\ref{sec:inputtolabelling} covers the compiler passes which produce the
annotated source program and Section~\ref{sec:measurablelifting} the rest
of the transformations in the front-end.  Then the compile-time checks
for good cost labelling are detailed in Section~\ref{sec:costchecks}
and the proofs that the structured traces required by the back-end
exist are discussed in Section~\ref{sec:structuredtrace}.

\section{The compiler and its correctness statement}

The uncertified prototype \ocaml{} \cerco{} compiler was originally described
in Deliverables 2.1 and 2.2.  Its design was replicated in the formal
\matita{} code, which was presented in Deliverables 3.2 and 4.2, for
the front-end and back-end respectively.

\begin{figure}
\begin{center}
\includegraphics[width=0.5\linewidth]{compiler-plain.pdf}
\end{center}
\caption{Languages in the \cerco{} compiler}
\label{fig:compilerlangs}
\end{figure}

The compiler uses a number of intermediate languages, as outlined the
middle two lines of Figure~\ref{fig:compilerlangs}.  The upper line
represents the front-end of the compiler, and the lower the back-end,
finishing with Intel 8051 binary code.  Not all of the front-end compiler passes
introduce a new language, and Figure~\ref{fig:summary} presents a
list of every pass involved.

\begin{figure}
\begin{center}
\begin{minipage}{.8\linewidth}
\begin{tabbing}
\quad \= $\downarrow$ \quad \= \kill
\textsf{C} (unformalised)\\
\> $\downarrow$ \> CIL parser (unformalised \ocaml)\\
\textsf{Clight}\\
%\> $\downarrow$ \> add runtime functions\\
\> $\downarrow$ \> \lstinline[language=C]'switch' removal\\
\> $\downarrow$ \> labelling\\
\> $\downarrow$ \> cast removal\\
\> $\downarrow$ \> stack variable allocation and control structure
 simplification\\
\textsf{Cminor}\\
%\> $\downarrow$ \> generate global variable initialization code\\
\> $\downarrow$ \> transform to RTL graph\\
\textsf{RTLabs}\\
\> $\downarrow$ \> check cost labelled properties of RTL graph\\
\> $\downarrow$ \> start of target specific back-end\\
\>\quad \vdots
\end{tabbing}
\end{minipage}
\end{center}
\caption{Front-end languages and compiler passes}
\label{fig:summary}
\end{figure}

\label{page:switchintro}
The annotated source code is produced by the cost labelling phase.
Note that there is a pass to replace C \lstinline[language=C]'switch'
statements before labelling --- we need to remove them because the
simple form of labelling used in the formalised compiler is not quite
capable of capturing their execution time costs, largely due to C's 
`fall-through' behaviour where execution from one branch continues in
the next unless there is an explicit \lstinline[language=C]'break'.

The cast removal phase which follows cost labelling simplifies
expressions to prevent unnecessary arithmetic promotion, which is
specified by the C standard but costly for an 8-bit target.  The
transformation to \textsf{Cminor} and subsequently \textsf{RTLabs}
bear considerable resemblance to some passes of the CompCert
compiler~\cite{Blazy-Leroy-Clight-09,Leroy-backend}, although we use a simpler \textsf{Cminor} where
all loops use \lstinline[language=C]'goto' statements, and the
\textsf{RTLabs} language retains a target-independent flavour.  The
back-end takes \textsf{RTLabs} code as input.

The whole compilation function returns the following information on success:
\begin{lstlisting}[language=Grafite]
  record compiler_output : Type[0] :=
   { c_labelled_object_code: labelled_object_code
   ; c_stack_cost: stack_cost_model
   ; c_max_stack: nat
   ; c_init_costlabel: costlabel
   ; c_labelled_clight: clight_program
   ; c_clight_cost_map: clight_cost_map
   }.
\end{lstlisting}
It consists of annotated 8051 object code, a mapping from function
identifiers to the function's stack space usage, the space available for the
stack after global variable allocation, a cost label covering the
execution time for the initialisation of global variables and the call
to the \lstinline[language=C]'main' function, the annotated source
code, and finally a mapping from cost labels to actual execution time
costs.

An \ocaml{} pretty printer is used to provide a concrete version of
the output code and annotated source code.  In the case of the
annotated source code, it also inserts the actual costs alongside the
cost labels, and optionally adds a global cost variable and
instrumentation to support further reasoning in external tools such as
Frama-C.

\subsection{Revisions to the prototype compiler}

Our focus on intensional properties prompted us to consider whether we
could incorporate stack space into the costs presented to the user.
We only allocate one fixed-size frame per function, so modelling this
was relatively simple.  It is the only form of dynamic memory
allocation provided by the compiler, so we were able to strengthen the
statement of the goal to guarantee successful execution whenever the
stack space obeys the \lstinline'c_max_stack' bound calculated by
subtracting the global variable requirements from the total memory
available.

The cost labelling checks at the end of Figure~\ref{fig:summary} have been
introduced to reduce the proof burden, and are described in
Section~\ref{sec:costchecks}.

The use of dependent types to capture simple intermediate language
invariants makes every front-end pass a total function, except
\textsf{Clight} to \textsf{Cminor} and the cost checks.  Hence various
well-formedness and type safety checks are performed only once between
\textsf{Clight} and \textsf{Cminor}, and the invariants rule out any
difficulties in the later stages.  With the benefit of hindsight we
would have included an initial checking phase to produce a
`well-formed' variant of \textsf{Clight}, conjecturing that this would
simplify various parts of the proofs for the \textsf{Clight} stages
which deal with potentially ill-formed code.

Following D2.2, we previously generated code for global variable
initialisation in \textsf{Cminor}, for which we reserved a cost label
to represent the execution time for initialisation.  However, the
back-end must also add an initial call to the main function, whose
cost must also be accounted for, so we decided to move the
initialisation code to the back-end and merge the costs.

\subsection{Main correctness statement}

[[relocated to specification section]]

\section{Correctness statement for the front-end}
\label{sec:fegoals}

The essential parts of the intensional proof were outlined during work
on a toy compiler in Task
2.1~\cite{springerlink:10.1007/978-3-642-32469-7_3}.  These are
\begin{enumerate}
\item functional correctness, in particular preserving the trace of
  cost labels,
\item the \emph{soundness} and \emph{precision} of the cost labelling
  on the object code, and
\item the timing analysis on the object code produces a correct
  mapping from cost labels to time.
\end{enumerate}

However, that toy development did not include function calls.  For the
full \cerco{} compiler we also need to maintain the invariant that
functions return to the correct program location in the caller, as we
mentioned in the previous section.  During work on the back-end timing
analysis (describe in more detail in the companion deliverable, D4.4)
the notion of a \emph{structured trace} was developed to enforce this
return property, and also most of the cost labelling properties too.

\begin{figure}
\begin{center}
\includegraphics[width=0.5\linewidth]{compiler.pdf}
\end{center}
\caption{The compiler and proof outline}
\label{fig:compiler}
\end{figure}

Jointly, we generalised the structured traces to apply to any of the
intermediate languages which have some idea of program counter.  This means
that they are introduced part way through the compiler, see
Figure~\ref{fig:compiler}.  Proving that a structured trace can be
constructed at \textsf{RTLabs} has several virtues:
\begin{itemize}
\item This is the first language where every operation has its own
  unique, easily addressable, statement.
\item Function calls and returns are still handled implicitly in the
  language and so the structural properties are ensured by the
  semantics.
\item Many of the back-end languages from \textsf{RTL} onwards share a common
  core set of definitions, and using structured traces throughout
  increases this uniformity.
\end{itemize}

\begin{figure}
\begin{center}
\includegraphics[width=0.6\linewidth]{strtraces.pdf}
\end{center}
\caption{Nesting of functions in structured traces}
\label{fig:strtrace}
\end{figure}
A structured trace is a mutually inductive data type which 
contains the steps from a normal program trace, but arranged into a
nested structure which groups entire function calls together and
aggregates individual steps between cost labels (or between the final
cost label and the return from the function), see
Figure~\ref{fig:strtrace}.  This captures the idea that the cost labels
only represent costs \emph{within} a function --- calls to other
functions are accounted for in the nested trace for their execution, and we
can locally regard function calls as a single step.

These structured traces form the core part of the intermediate results
that we must prove so that the back-end can complete the main
intensional result stated above.  In full, we provide the back-end
with
\begin{enumerate}
\item A normal trace of the \textbf{prefix} of the program's execution
  before reaching the measurable subtrace.  (This needs to be
  preserved so that we know that the stack space consumed is correct,
  and to set up the simulation results.)
\item The \textbf{structured trace} corresponding to the measurable
  subtrace.
\item An additional property about the structured trace that no
  `program counter' is \textbf{repeated} between cost labels.  Together with
  the structure in the trace, this takes over from showing that
  cost labelling is sound and precise.
\item A proof that the \textbf{observables} have been preserved.
\item A proof that the \textbf{stack limit} is still observed by the prefix and
  the structure trace.  (This is largely a consequence of the
  preservation of observables.)
\end{enumerate}
The \lstinline'front_end_correct' lemma in the
\lstinline'correctness.ma' file provides a record containing these.

Following the outline in Figure~\ref{fig:compiler}, we will first deal
with the transformations in \textsf{Clight} that produce the source
program with cost labels, then show that measurable traces can be
lifted to \textsf{RTLabs}, and finally show that we can construct the
properties listed above ready for the back-end proofs.

\section{Input code to cost labelled program}
\label{sec:inputtolabelling}

As explained on page~\pageref{page:switchintro}, the costs of complex
C \lstinline[language=C]'switch' statements cannot be represented with
the simple labelling used in the formalised compiler.  Our first pass
replaces these statements with simpler C code, allowing our second
pass to perform the cost labelling.  We show that the behaviour of
programs is unchanged by these passes using forward
simulations\footnote{All of our languages are deterministic, which can
be seen directly from their executable definitions.  Thus we know that
forward simulations are sufficient because the target cannot have any
other behaviour.}.

\subsection{Switch removal}

We compile away \lstinline[language=C]'switch' statements into more
basic \textsf{Clight} code.
Note that this transformation does not necessarily deteriorate the 
efficiency of the generated code. For instance, compilers such as GCC 
introduce balanced trees of ``if-then-else'' constructs for small 
switches. However, our implementation strategy is much simpler. Let 
us consider the following input statement.

\begin{lstlisting}[language=C]
   switch(e) {
   case v1:
     stmt1;
   case v2:
     stmt2;
   default:
     stmt_default;
   }
\end{lstlisting}

Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default}
may contain \lstinline[language=C]'break' statements, which have the 
effect of exiting the switch statement. In the absence of break, the 
execution falls through each case sequentially. In our implementation, 
we produce an equivalent sequence of ``if-then'' chained by gotos:
\begin{lstlisting}[language=C]
   fresh = e;
   if(fresh == v1) {
     $\llbracket$stmt1$\rrbracket$; 
     goto lbl_case2;
   };
   if(fresh == v2) {
     lbl_case2:
     $\llbracket$stmt2$\rrbracket$;
     goto lbl_case2;
   };
   $\llbracket$stmt_default$\rrbracket$;
   exit_label:
\end{lstlisting}

The proof had to tackle the following points:
\begin{itemize}
\item the source and target memories are not the same (due to the fresh variable),
\item the flow of control is changed in a non-local way (e.g. \textbf{goto} 
  instead of \textbf{break}).
\end{itemize}
In order to tackle the first point, we implemented a version of memory 
extensions similar to those of CompCert.

For the simulation we decided to prove a sufficient amount to give us
confidence in the definitions and approach, but to curtail the proof
because this pass does not contribute to the intensional correctness
result.  We tackled several simple cases, that do not interact with
the switch removal per se, to show that the definitions were usable,
and part of the switch case to check that the approach is
reasonable. This comprises propagating the memory extension through
each statement (except switch), as well as various invariants that are
needed for the switch case (in particular, freshness hypotheses). The
details of the evaluation process for the source switch statement and
its target counterpart can be found in the file
\lstinline'switchRemoval.ma', along more details on the transformation
itself.

Proving the correctness of the second point would require reasoning on the 
semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight} 
semantics, this is implemented as a function-wide lookup of the target label. 
The invariant we would need is the fact that a global label lookup on a freshly 
created goto is equivalent to a local lookup. This would in turn require the 
propagation of some freshness hypotheses on labels. As discussed, 
we decided to omit this part of the correctness proof.

\subsection{Cost labelling}

The simulation for the cost labelling pass is the simplest in the
front-end.  The main argument is that any step of the source program
is simulated by the same step of the labelled one, plus any extra
steps for the added cost labels.  The extra instructions do not change
the memory or local environments, although we have to keep track of
the extra instructions that appear in continuations, for example
during the execution of a \lstinline[language=C]'while' loop.

We do not attempt to capture any cost properties of the labelling\footnote{We describe how the cost properties are
established in Section~\ref{sec:costchecks}.} in
the simulation proof, which allows the proof to be oblivious to the choice
of cost labels.  Hence we do not have to reason about the threading of
name generation through the labelling function, greatly reducing the
amount of effort required.

%TODO: both give one-step-sim-by-many forward sim results; switch
%removal tricky, uses aux var to keep result of expr, not central to
%intensional correctness so curtailed proof effort once reasonable
%level of confidence in code gained; labelling much simpler; don't care
%what the labels are at this stage, just need to know when to go
%through extra steps.  Rolled up into a single result with a cofixpoint
%to obtain coinductive statement of equivalence (show).

\section{Finding corresponding measurable subtraces}
\label{sec:measurablelifting}

There follow the three main passes of the front-end:
\begin{enumerate}
\item simplification of casts in \textsf{Clight} code
\item \textsf{Clight} to \textsf{Cminor} translation, performing stack
  variable allocation and simplifying control structures
\item transformation to \textsf{RTLabs} control flow graph
\end{enumerate}
We have taken a common approach to
each pass: first we build (or axiomatise) forward simulation results
that are similar to normal compiler proofs, but which are slightly more
fine-grained so that we can see that the call structure and relative
placement of cost labels is preserved.

Then we instantiate a general result which shows that we can find a
\emph{measurable} subtrace in the target of the pass that corresponds
to the measurable subtrace in the source.  By repeated application of
this result we can find a measurable subtrace of the execution of the
\textsf{RTLabs} code, suitable for the construction of a structured
trace (see Section~\ref{sec:structuredtrace}).  This is essentially an
extra layer on top of the simulation proofs that provides us with the
additional information required for our intensional correctness proof.

\subsection{Generic measurable subtrace lifting proof}

Our generic proof is parametrised on a record containing small-step
semantics for the source and target language, a classification of
states (the same form of classification is used when defining
structured traces), a simulation relation which respects the
classification and cost labelling and
four simulation results.  The simulations are split by the starting state's
classification and whether it is a cost label, which will allow us to
observe that the call structure is preserved.  They are:
\begin{enumerate}
\item a step from a `normal' state (which is not classified as a call
  or return) which is not a cost label is simulated by zero or more
  `normal' steps;
\item a step from a `call' state followed by a cost label step is
  simulated by a step from a `call' state, a corresponding label step,
  then zero or more `normal' steps;
\item a step from a `call' state not followed by a cost label
  similarly (note that this case cannot occur in a well-labelled
  program, but we do not have enough information locally to exploit
  this); and
\item a cost label step is simulated by a cost label step.
\end{enumerate}
Finally, we need to know that a successfully translated program will
have an initial state in the simulation relation with the original
program's initial state.

The back-end has similar requirements for lifting simulations to
structured traces.  Fortunately, our treatment of calls and returns
can be slightly simpler because we have special call and return states
that correspond to function entry and return that are separate from
the actual instructions.  This was originally inherited from our port
of CompCert's \textsf{Clight} semantics, but proves useful here
because we only need to consider adding extra steps \emph{after} a
call or return state, because the instruction step deals with extra
steps that occur before.  The back-end makes all of the call and
return machinery explicit, and thus needs more complex statements
about extra steps before and after each call and return.

\begin{figure}
\begin{center}
\includegraphics[width=0.5\linewidth]{meassim.pdf}
\end{center}
\caption{Tiling of simulation for a measurable subtrace}
\label{fig:tiling}
\end{figure}

To find the measurable subtrace in the target program's execution we
walk along the original program's execution trace applying the
appropriate simulation result by induction on the number of steps.
While the number of steps taken varies, the overall structure is
preserved, as illustrated in Figure~\ref{fig:tiling}.  By preserving
the structure we also maintain the same intensional observables.  One
delicate point is that the cost label following a call must remain
directly afterwards\footnote{The prototype compiler allowed some
  straight-line code to appear before the cost label until a later
  stage of the compiler, but we must move the requirement forward to
  fit with the structured traces.}
% Damn it, I should have just moved the cost label forwards in RTLabs,
% like the prototype does in RTL to ERTL; the result would have been
% simpler.  Or was there some reason not to do that?
(both in the program code and in the execution trace), even if we
introduce extra steps, for example to store parameters in memory in
\textsf{Cminor}.  Thus we have a version of the call simulation
that deals with both the call and the cost label in one result.

In addition to the subtrace we are interested in measuring, we must
prove that the earlier part of the trace is also preserved in
order to use the simulation from the initial state.  This proof also
guarantees that we do not run out of stack space before the subtrace
we are interested in.  The lemmas for this prefix and the measurable
subtrace are similar, following the pattern above.  However, the
measurable subtrace also requires us to rebuild the termination
proof.  This is defined recursively:
\label{prog:terminationproof}
\begin{lstlisting}[language=Grafite]
  let rec will_return_aux C (depth:nat)
                               (trace:list (cs_state $...$ C $\times$ trace)) on trace : bool :=
  match trace with
  [ nil $\Rightarrow$ false
  | cons h tl $\Rightarrow$
    let $\langle$s,tr$\rangle$ := h in
    match cs_classify C s with
    [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl
    | cl_return $\Rightarrow$
        match depth with
        [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ]
        | S d $\Rightarrow$ will_return_aux C d tl
        ]
    | _ $\Rightarrow$ will_return_aux C depth tl
    ]
  ].
\end{lstlisting}
The \lstinline'depth' is the number of return states we need to see
before we have returned to the original function (initially zero) and
\lstinline'trace' the measurable subtrace obtained from the running
the semantics for the correct number of steps.  This definition
unfolds tail recursively for each step, and once the corresponding
simulation result has been applied a new one for the target can be
asserted by unfolding and applying the induction hypothesis on the
shorter trace.

Combining the lemmas about the prefix and the measurable subtrace
requires a little care because the states joining the two might not be
related in the simulation.  In particular, if the measurable subtrace
starts from the cost label at the beginning of the function there may
be some extra instructions in the target code to execute to complete
function entry before the states are back in the relation.  Hence we
carefully phrased the lemmas to allow for such extra steps.

Together, these then gives us an overall result for any simulation fitting the
requirements above (contained in the \lstinline'meas_sim' record):
\begin{lstlisting}[language=Grafite]
theorem measured_subtrace_preserved :
  $\forall$MS:meas_sim.
  $\forall$p1,p2,m,n,stack_cost,max.
  ms_compiled MS p1 p2 $\rightarrow$
  measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$
  $\exists$m',n'.
    measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$
    observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
\end{lstlisting}
The stack space requirement that is embedded in \lstinline'measurable'
is a consequence of the preservation of observables, because it is
determined by the functions called and returned from, which are observable.

\subsection{Simulation results for each pass}

We now consider the simulation results for the passes, each of which
is used to instantiate the
\lstinline[language=Grafite]'measured_subtrace_preserved' theorem to
construct the measurable subtrace for the next language.

\subsubsection{Cast simplification}

The parser used in \cerco{} introduces a lot of explicit type casts. 
If left as they are, these constructs can greatly hamper the 
quality of the generated code -- especially as the architecture 
we consider is an $8$-bit one. In \textsf{Clight}, casts are 
expressions. Hence, most of the work of this transformation 
proceeds on expressions. The transformation proceeds by recursively 
trying to coerce an expression to a particular integer type, which 
is in practice smaller than the original one. This functionality 
is implemented by two mutually recursive functions whose signature 
is the following.

\begin{lstlisting}[language=Grafite]
let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) 
  : $\Sigma$result:bool$\times$expr. 
    $\forall$ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) := $\ldots$

and simplify_inside (e:expr) : $\Sigma$result:expr. conservation e result := $\ldots$
\end{lstlisting}

The \textsf{simplify\_inside} acts as a wrapper for 
\textsf{simplify\_expr}. Whenever \textsf{simplify\_inside} encounters 
a \textsf{Ecast} expression, it tries to coerce the sub-expression 
to the desired type using \textsf{simplify\_expr}, which tries to 
perform the actual coercion. In return, \textsf{simplify\_expr} calls 
back \textsf{simplify\_inside} in some particular positions, where we
decided to be conservative in order to simplify the proofs. However, 
the current design allows to incrementally revert to a more aggressive 
version, by replacing recursive calls to \textsf{simplify\_inside} by 
calls to \textsf{simplify\_expr} \emph{and} proving the corresponding 
invariants -- where possible. 

The \textsf{simplify\_inv} invariant encodes either the conservation 
of the semantics during the transformation corresponding to the failure 
of the coercion (\textsf{Inv\_eq} constructor), or the successful 
downcast of the considered expression to the target type 
(\textsf{Inv\_coerce\_ok}).

\begin{lstlisting}[language=Grafite]
inductive simplify_inv 
  (ge : genv) (en : env) (m : mem) 
  (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool $\rightarrow$ Prop :=
| Inv_eq : $\forall$result_flag. $\ldots$
     simplify_inv ge en m e1 e2 target_sz target_sg result_flag
| Inv_coerce_ok : $\forall$src_sz,src_sg.
     typeof e1 = Tint src_sz src_sg $\rightarrow$
     typeof e2 = Tint target_sz target_sg $\rightarrow$     
     smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2) $\rightarrow$
     simplify_inv ge en m e1 e2 target_sz target_sg true.
\end{lstlisting}

The \textsf{conservation} invariant for \textsf{simplify\_inside} simply states the conservation 
of the semantics, as in the \textsf{Inv\_eq} constructor of the previous 
invariant.

\begin{lstlisting}[language=Grafite]
definition conservation := $\lambda$e,result. $\forall$ge,en,m. 
          res_sim ? (exec_expr ge en m e) (exec_expr ge en m result)
       $\wedge$ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
       $\wedge$ typeof e = typeof result.
\end{lstlisting}

This invariant is then easily lifted to statement evaluations.
The main problem encountered with this particular pass was dealing with 
inconsistently typed programs, a canonical case being a particular 
integer constant of a certain size typed with another size. This 
prompted the need to introduce numerous type checks, making
both the implementation and the proof more complex, even though more
comprehensive checks are made in the next stage.
%\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language}

\subsubsection{Clight to Cminor}

This pass is the last one operating on the \textsf{Clight} language.
Its input is a full \textsf{Clight} program, and its output is a
\textsf{Cminor} program. Note that we do not use an equivalent of
CompCert's \textsf{C\#minor} language: we translate directly to a
variant of \textsf{Cminor}. This presents the advantage of not
requiring the special loop constructs, nor the explicit block
structure. Another salient point of our approach is that a significant
number of the properties needed for the simulation proof were directly
encoded in dependently typed translation functions.  In particular,
freshness conditions and well-typedness conditions are included. The
main effects of the transformation from \textsf{Clight} to
\textsf{Cminor} are listed below.

\begin{itemize}
\item Variables are classified as being either globals, stack-allocated 
  locals or potentially register-allocated locals. The value of register-allocated 
  local variables is moved out of the modelled memory and stored in a 
  dedicated environment.
\item In \textsf{Clight}, each local variable has a dedicated memory block, whereas 
  stack-allocated locals are bundled together on a function-by-function basis.
\item Loops are converted to jumps.
\end{itemize}

The first two points require memory injections which are more flexible that those 
needed in the switch removal case. In the remainder of this section, we briefly 
discuss our implementation of memory injections, and then the simulation proof.

\paragraph{Memory injections.}

Our memory injections are modelled after the work of Blazy \& Leroy. 
However, the corresponding paper is based on the first version of the 
CompCert memory model~\cite{2008-Leroy-Blazy-memory-model}, whereas we use a much more concrete model, allowing byte-level
manipulations (as in the later version of CompCert's memory model). We proved 
roughly 80 \% of the required lemmas. Notably, some of the difficulties encountered were
due to overly relaxed conditions on pointer validity (fixed during development).
Some more side conditions had to be added to take care of possible overflows when converting 
from \textbf{Z} block bounds to $16$ bit pointer offsets (in practice, such overflows 
only occur in edge cases that are easily ruled out -- but this fact is not visible 
in memory injections). Concretely, some of the lemmas on the preservation of simulation of 
loads after writes were axiomatised, due to a lack of time.

\paragraph{Simulation proof.}

We proved the simulation result for expressions and a representative
selection of statements.  In particular we tackled
\lstinline[language=C]'while' statements to ensure that we correctly
translate loops because our approach differs from CompCert by
converting directly to \textsf{Cminor} \lstinline[language=C]'goto's
rather than maintaining a notion of loop in \textsf{Cminor}.  We also have a partial
proof for function entry, covering the setup of the memory injection,
but not function exit.  Exits, and the remaining statements, have been
axiomatised.

Careful management of the proof state was required because proof terms
are embedded in \textsf{Cminor} code to show that invariants are
respected.  These proof terms appear in the proof state when inverting
the translation functions, and they can be large and awkward.  While
generalising them away is usually sufficient, it can be difficult when
they appear under a binder.

%The correctness proof for this transformation was not completed. We proved the 
%simulation result for expressions and for some subset of the critical statement cases. 
%Notably lacking are the function entry and exit, where the memory injection is
%properly set up. As would be expected, a significant amount of work has to be performed 
%to show the conservation of all invariants at each simulation step.

%\todo{list cases, explain while loop, explain labeling problem}

\subsubsection{Cminor to RTLabs}

The translation from \textsf{Cminor} to \textsf{RTLabs} is a fairly
routine control flow graph (CFG) construction.  As such, we chose to
axiomatise the associated extensional simulation results.  However, we did prove several
properties of the generated programs:
\begin{itemize}
\item All statements are type correct with respect to the declared
  pseudo-register type environment.
\item The CFG is closed, and has a distinguished entry node and a
  unique exit node.
\end{itemize}

These properties rely on similar properties about type safety and the
presence of \lstinline[language=C]'goto'-labels for \textsf{Cminor} programs
which are checked at the preceding stage.  As a result, this
transformation is total and any compilation failures must occur when
the corresponding \textsf{Clight} source is available and a better
error message can be generated.

The proof obligations for these properties include many instances of
graph inclusion.  We automated these proofs using a small amount of
reflection, making the obligations much easier to handle.  One
drawback to enforcing invariants throughout is that temporarily
breaking them can be awkward.  For example, \lstinline'return'
statements were originally used as placeholders for
\lstinline[language=C]'goto' destinations that had not yet been
translated.  However, this made establishing the single exit node
property rather difficult, and a different placeholder was chosen
instead.  In other circumstances it is possible to prove a more
complex invariant then simplify it at the end of the transformation.

\section{Checking cost labelling properties}
\label{sec:costchecks}

Ideally, we would provide proofs that the cost labelling pass always
produces programs that are soundly and precisely labelled and that
each subsequent pass preserves these properties.  This would match our
use of dependent types to eliminate impossible sources of errors
during compilation, in particular retaining intermediate language type
information.

However, given the limited amount of time available we realised that
implementing a compile-time check for a sound and precise labelling of
the \textsf{RTLabs} intermediate code would reduce the proof burden
considerably.  This is similar in spirit to the use of translation
validation in certified compilation, which makes a similar trade-off
between the potential for compile-time failure and the volume of proof
required.

The check cannot be pushed into a later stage of the compiler because
much of the information is embedded into the structured traces.
However, if an alternative method was used to show that function
returns in the compiled code are sufficiently well-behaved, then we
could consider pushing the cost property checks into the timing
analysis itself.  We leave this as a possible area for future work.

\subsection{Implementation and correctness}
\label{sec:costchecksimpl}

For a cost labelling to be sound and precise we need a cost label at
the start of each function, after each branch and at least one in
every loop.  The first two parts are trivial to check by examining the
code.  In \textsf{RTLabs} the last part is specified by saying
that there is a bound on the number of successive instruction nodes in
the CFG that you can follow before you encounter a cost label, and
checking this is more difficult.

The implementation progresses through the set of nodes in the graph,
following successors until a cost label is found or a label-free cycle
is discovered (in which case the property does not hold and we return
an error).  This is made easier by the prior knowledge that every
successor of a branch instruction is a cost label, so we do not need
to search each branch.  When a label is found, we remove the chain of
program counters from the set and continue from another node in the
set until it is empty, at which point we know that there is a bound
for every node in the graph.

Directly reasoning about the function that implements this procedure would be
rather awkward, so an inductive specification of a single step of its
behaviour was written and proved to match the implementation.  This
was then used to prove the implementation sound and complete.

While we have not attempted to prove that the cost labelled properties
are established and preserved earlier in the compiler, we expect that
the effort for the \textsf{Cminor} to \textsf{RTLabs} stage alone
would be similar to the work outlined above, because it involves the
change from requiring a cost label at particular positions to
requiring cost labels to break loops in the CFG.  As there are another
three passes to consider (including the labelling itself), we believe
that using the check above is much simpler overall.

% TODO? Found some Clight to Cminor bugs quite quickly

\section{Existence of a structured trace}
\label{sec:structuredtrace}

The \emph{structured trace} idea introduced in
Section~\ref{sec:fegoals} enriches the execution trace of a program by
nesting function calls in a mixed-step style and embedding the cost
labelling properties of the program.  See Figure~\ref{fig:strtrace} on
page~\pageref{fig:strtrace} for an illustration of a structured trace.
It was originally designed to support the proof of correctness for the
timing analysis of the object code in the back-end, then generalised
to provide a common structure to use from the end of the front-end to
the object code.

To make the definition generic we abstract over the semantics of the
language,
\begin{lstlisting}[language=Grafite]
record abstract_status : Type[1] :=
  { as_status :> Type[0]
  ; as_execute : relation as_status
  ; as_pc : DeqSet
  ; as_pc_of : as_status $\rightarrow$ as_pc
  ; as_classify : as_status $\rightarrow$ status_class
  ; as_label_of_pc : as_pc $\rightarrow$ option costlabel
  ; as_after_return : ($\Sigma$s:as_status. as_classify s =  cl_call) $\rightarrow$ as_status $\rightarrow$ Prop
  ; as_result: as_status $\rightarrow$ option int
  ; as_call_ident : ($\Sigma$s:as_status.as_classify s = cl_call) $\rightarrow$ ident
  ; as_tailcall_ident : ($\Sigma$s:as_status.as_classify s = cl_tailcall) $\rightarrow$ ident
  }.
\end{lstlisting}
which requires a type of states, an execution relation\footnote{All of
  our semantics are executable, but using a relation was simpler in
  the abstraction.}, some notion of abstract
program counter with decidable equality, the classification of states,
and functions to extract the observable intensional information (cost
labels and the identity of functions that are called).  The
\lstinline'as_after_return' property links the state before a function
call with the state after return, providing the evidence that
execution returns to the correct place.  The precise form varies
between stages; in \textsf{RTLabs} it insists the CFG, the pointer to
the CFG node to execute next, and some call stack information is
preserved.

The structured traces are defined using three mutually inductive
types.  The core data structure is \lstinline'trace_any_label', which
captures some straight-line execution until the next cost label or the
return from the enclosing function.  Any function calls are embedded as
a single step, with its own trace nested inside and the before and
after states linked by \lstinline'as_after_return'; and states
classified as a `jump' (in particular branches) must be followed by a
cost label.

The second type, \lstinline'trace_label_label', is a
\lstinline'trace_any_label' where the initial state is cost labelled.
Thus a trace in this type identifies a series of steps whose cost is
entirely accounted for by the label at the start.

Finally, \lstinline'trace_label_return' is a sequence of
\lstinline'trace_label_label' values which end in the return from the
function.  These correspond to a measurable subtrace, and in
particular include executions of an entire function call (and so are
used for the nested calls in \lstinline'trace_any_label').

\subsection{Construction}

The construction of the structured trace replaces syntactic cost
labelling properties, which place requirements on where labels appear
in the program, with semantic properties that constrain the execution
traces of the program.  The construction begins by defining versions
of the sound and precise labelling properties on states and global
environments (for the code that appears in each of them) rather than
whole programs, and showing that these are preserved by steps of the
\textsf{RTLabs} semantics.

Then we show that each cost labelling property required by the
definition of structured traces is locally satisfied.  These proofs are
broken up by the classification of states.  Similarly, we prove a
step-by-step stack preservation result, which states that the
\textsf{RTLabs} semantics never changes the lower parts of the stack.

The core part of the construction of a structured trace is to use the
proof of termination from the measurable trace (defined on
page~\pageref{prog:terminationproof}) to `fold up' the execution into
the nested form.  The results outlined above fill in the proof
obligations for the cost labelling properties and the stack
preservation result shows that calls return to the correct location.

The structured trace alone is not sufficient to capture the property
that the program is soundly labelled.  While the structured trace
guarantees termination, it still permits a loop to be executed a
finite number of times without encountering a cost label.  We
eliminate this by proving that no `program counter' repeats within any
\lstinline'trace_any_label' section by showing that it is incompatible
with the property that there is a bound on the number of successor
instructions you can follow in the CFG before you encounter a cost
label (from Section~\ref{sec:costchecksimpl}).

\subsubsection{Complete execution structured traces}

The development of the construction above started relatively early,
before the measurable subtrace preservation proofs.  To be confident
that the traces were well-formed at that time, we also developed a
complete execution form that embeds the traces above.  This includes
non-terminating program executions, where an infinite number of the terminating
structured traces are embedded.  This construction confirmed that our
definition of structured traces was consistent, although we later
found that we did not require the whole execution version for the
compiler correctness results.

To construct these we need to know whether each function call will
eventually terminate, requiring the use of the excluded middle.  This
classical reasoning is local to the construction of whole program
traces and is not necessary for our main results.

\section{Conclusion}

In combination with the work on the CerCo back-end and by
concentrating on the novel intensional parts of the proof, we have
shown that it is possible to construct certifying compilers that
correctly report execution time and stack space costs.  The layering
of intensional correctness proofs on top of normal simulation results
provides a useful separation of concerns, and could permit the reuse
of existing results.

\section{Files}

The following table gives a high-level overview of the \matita{}
source files in Deliverable 3.4:

\bigskip

\begin{tabular}{rp{.7\linewidth}}
\lstinline'compiler.ma' & Top-level compiler definitions, in particular
\lstinline'front_end', and the whole compiler definition
\lstinline'compile'. \\
\lstinline'correctness.ma' & Correctness results: \lstinline'front_end_correct'
and \lstinline'correct', respectively. \\
\lstinline'Clight/*' & \textsf{Clight}: proofs for switch
removal, cost labelling, cast simplification and conversion to
\textsf{Cminor}. \\
\lstinline'Cminor/*' & \textsf{Cminor}: axioms of conversion to
\textsf{RTLabs}. \\
\lstinline'RTLabs/*' & \textsf{RTLabs}: definitions and proofs for
compile-time cost labelling checks, construction of structured traces.
\\
\lstinline'common/Measurable.ma' & Definitions for measurable
subtraces. \\
\lstinline'common/FEMeasurable.ma' & Generic measurable subtrace
lifting proof. \\
\lstinline'common/*' & Other common definitions relevant to many parts
of the compiler and proof. \\
\lstinline'utilities/*' & General purpose definitions used throughout,
including extensions to the standard \matita{} library.
\end{tabular}

\subsection{A brief overview of the backend compilation chain}
\label{subsect.brief.overview.backend.compilation.chain}

The Matita compiler's backend consists of five distinct intermediate languages: RTL, RTLntl, ERTL, LTL and LIN.
A sixth language, RTLabs, serves as the entry point of the backend and the exit point of the frontend.
RTL, RTLntl, ERTL and LTL are `control flow graph based' languages, whereas LIN is a linearised language, the final language before translation to assembly.

We now briefly discuss the properties of the intermediate languages, and discuss the various transformations that take place during the translation process:

\paragraph{RTLabs ((Abstract) Register Transfer Language)}
As mentioned, this is the final language of the compiler's frontend and the entry point for the backend.
This language uses pseudoregisters, not hardware registers.\footnote{There are an unbounded number of pseudoregisters.  Pseudoregisters are converted to hardware registers or stack positions during register allocation.}
Functions still use stackframes, where arguments are passed on the stack and results are stored in addresses.
During the pass to RTL instruction selection is carried out.

\paragraph{RTL (Register Transfer Language)}
This language uses pseudoregisters, not hardware registers.
Tailcall elimination is carried out during the translation from RTL to RTLntl.

\paragraph{RTLntl (Register Transfer Language --- No Tailcalls)}
This language is a pseudoregister, graph based language where all tailcalls are eliminated.
RTLntl is not present in the O'Caml compiler, the RTL language is reused for this purpose.

\paragraph{ERTL (Explicit Register Transfer Language)}
This is a language very similar to RTLntl.
However, the calling convention is made explicit, in that functions no longer receive and return inputs and outputs via a high-level mechanism, but rather use stack slots or hadware registers.
The ERTL to LTL pass performs the following transformations: liveness analysis, register colouring and register/stack slot allocation.

\paragraph{LTL (Linearisable Transfer Language)}
Another graph based language, but uses hardware registers instead of pseudoregisters.
Tunnelling (branch compression) should be implemented here.

\paragraph{LIN (Linearised)}
This is a linearised form of the LTL language; function graphs have been linearised into lists of statements.
All registers have been translated into hardware registers or stack addresses.
This is the final stage of compilation before translating directly into assembly language.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\section{The backend intermediate languages in Matita}
\label{sect.backend.intermediate.languages.matita}

We now discuss the encoding of the compiler backend languages in the Calculus of Constructions proper.
We pay particular heed to changes that we made from the O'Caml prototype.
In particular, many aspects of the backend languages have been unified into a single `joint' language.
We have also made heavy use of dependent types to reduce `spurious partiality' and to encode invariants.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Abstracting related languages}
\label{subsect.abstracting.related.languages}

The O'Caml compiler is written in the following manner.
Each intermediate language has its own dedicated syntax, notions of internal function, and so on.
Here, we make a distinction between `internal functions'---other functions that are explicitly written by the programmer---and `external functions', which belong to external library and require explictly linking.
In particular, IO can be seen as a special case of the `external function' mechanism.
Internal functions are represented as a record consisting of a sequential structure of statements, entry and exit points to this structure, and other book keeping devices.
This sequential structure can either be a control flow graph or a linearised list of statements, depending on the language.
Translations between intermediate language map syntaxes to syntaxes, and internal function representations to internal function representations explicitly.

This is a perfectly valid way to write a compiler, where everything is made explicit, but writing a \emph{verified} compiler poses new challenges.
In particular, we must look ahead to see how our choice of encodings will affect the size and complexity of the forthcoming proofs of correctness.
We now discuss some abstractions, introduced in the Matita code, which we hope will make our proofs shorter, amongst other benefits.

\paragraph{Changes between languages made explicit}
Due to the bureaucracy inherent in explicating each intermediate language's syntax in the O'Caml compiler, it can often be hard to see exactly what changes between each successive intermediate language.
By abstracting the syntax of the RTL, ERTL, LTL and LIN intermediate languages, we make these changes much clearer.

Our abstraction takes the following form:
\begin{lstlisting}[language=Grafite]
inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
  | COMMENT: String $\rightarrow$ joint_instruction p globals
  ...
  | INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals
  ...
  | OP1: Op1 $\rightarrow$ acc_a_reg p $\rightarrow$ acc_a_reg p $\rightarrow$ joint_instruction p globals
  ...
  | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
\end{lstlisting}
We first note that for the majority of intermediate languages, many instructions are shared.
However, these instructions expect different register types (either a pseudoregister or a hardware register) as arguments.
We must therefore parameterise the joint syntax with a record of parameters that will be specialised to each intermediate language.
In the type above, this parameterisation is realised with the \texttt{params\_\_} record.
As a result of this parameterisation, we have also added a degree of `type safety' to the intermediate languages' syntaxes.
In particular, we note that the \texttt{OP1} constructor expects quite a specific type, in that the two register arguments must both be what passes for the accumulator A in that language.
In some languages, for example LIN, this is the hardware accumulator, whilst in others this is any pseudoregister.
Contrast this with the \texttt{INT} constructor, which expects a \texttt{generic\_reg}, corresponding to an `arbitrary' register type.

Further, we note that some intermediate languages have language specific instructions (i.e. the instructions that change between languages).
We therefore add a new constructor to the syntax, \texttt{extension}, which expects a value of type \texttt{extend\_statements p}.
As \texttt{p} varies between intermediate languages, we can provide language specific extensions to the syntax of the joint language.
For example, ERTL's extended syntax consists of the following extra statements:
\begin{lstlisting}[language=Grafite]
inductive ertl_statement_extension: Type[0] :=
  | ertl_st_ext_new_frame: ertl_statement_extension
  | ertl_st_ext_del_frame: ertl_statement_extension
  | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension.
\end{lstlisting}
These are further packaged into an ERTL specific instance of \texttt{params\_\_} as follows:
\begin{lstlisting}[language=Grafite]
definition ertl_params__: params__ :=
  mk_params__ register register ... ertl_statement_extension.
\end{lstlisting}

\paragraph{Shared code, reduced proofs}
Many features of individual backend intermediate languages are shared with other intermediate languages.
For instance, RTLabs, RTL, ERTL and LTL are all graph based languages, where functions are represented as a control flow graph of statements that form their bodies.
Functions for adding statements to a graph, searching the graph, and so on, are remarkably similar across all languages, but are duplicated in the O'Caml code.

As a result, we chose to abstract the representation of internal functions for the RTL, ERTL, LTL and LIN intermediate languages into a `joint' representation.
This representation is parameterised by a record that dictates the layout of the function body for each intermediate language.
For instance, in RTL, the layout is graph like, whereas in LIN, the layout is a linearised list of statements.
Further, a generalised way of accessing the successor statement to the one currently under consideration is needed, and so forth.

Our joint internal function record looks like so:
\begin{lstlisting}[language=Grafite]
record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
{ 
  ...
  joint_if_params   : paramsT p;
  joint_if_locals   : localsT p;
  ...
  joint_if_code     : codeT ... p;
  ...
}.
\end{lstlisting}
In particular, everything that can vary between differing intermediate languages has been parameterised.
Here, we see the location where to fetch parameters, the listing of local variables, and the internal code representation has been parameterised.
Other particulars are also parameterised, though here omitted.

Hopefully this abstraction process will reduce the number of proofs that need to be written, dealing with internal functions of different languages characterised by parameters.

\paragraph{Dependency on instruction selection}
We note that the backend languages are all essentially `post instruction selection languages'.
The `joint' syntax makes this especially clear.
For instance, in the definition:
\begin{lstlisting}[language=Grafite]
inductive joint_instruction (p:params__) (globals: list ident): Type[0] :=
  ...
  | INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals
  | MOVE: pair_reg p $\rightarrow$ joint_instruction p globals
  ...
  | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals
  ...
  | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
\end{lstlisting}
The capitalised constructors---\texttt{INT}, \texttt{MOVE}, and so on---are all machine specific instructions.
Retargetting the compiler to another microprocessor, improving instruction selection, or simply enlarging the subset of the machine language that the compiler can use, would entail replacing these constructors with constructors that correspond to the instructions of the new target.
We feel that this makes which instructions are target dependent, and which are not (i.e. those language specific instructions that fall inside the \texttt{extension} constructor) much more explicit.
In the long term, we would really like to try to directly embed the target language in the syntax, in order to reuse the target language's semantics.

\paragraph{Independent development and testing}
We have essentially modularised the intermediate languages in the compiler backend.
As with any form of modularisation, we reap benefits in the ability to independently test and develop each intermediate language separately, with the benefit of fixing bugs just once.

\paragraph{Future reuse for other compiler projects}
Another advantage of our modularisation scheme is the ability to quickly use and reuse intermediate languages for other compiler projects.
For instance, in creating a cost-preserving compiler for a functional language, we may choose to target a linearised version of RTL directly.
Adding such an intermediate language would involve the addition of just a few lines of code.

\paragraph{Easy addition of new compiler passes}
Under our modularisation and abstraction scheme, new compiler passes can easily be injected into the backend.
We have a concrete example of this in the RTLntl language, an intermediate language that was not present in the original O'Caml code.
To specify a new intermediate language we must simply specify, through the use of the statement extension mechanism, what differs in the new intermediate language from the `joint' language, and configure a new notion of internal function record, by specialising parameters, to the new language.
As generic code for the `joint' language exists, for example to add statements to control flow graphs, this code can be reused for the new intermediate language.

\paragraph{Possible commutations of translation passes}
The backend translation passes of the CerCo compiler differ quite a bit from the CompCert compiler.
In the CompCert compiler, linearisation occurs much earlier in the compilation chain, and passes such as register colouring and allocation are carried out on a linearised form of program.
Contrast this with our own approach, where the code is represented as a graph for much longer.
Similarly, in CompCert the calling conventions are enforced after register allocation, whereas we do register allocation before enforcing the calling convention.

However, by abstracting the representation of intermediate functions, we are now much more free to reorder translation passes as we see fit.
The linearisation process, for instance, now no longer cares about the specific representation of code in the source and target languages.
It just relies on a common interface.
We are therefore, in theory, free to pick where we wish to linearise our representation.
This adds an unusual flexibility into the compilation process, and allows us to freely experiment with different orderings of translation passes.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Use of dependent types}
\label{subsect.use.of.dependent.types}

We see several potential ways in which a compiler can fail to compile a program:
\begin{enumerate}
\item
The program is malformed, and there is no hope of making sense of the program.
\item
The compiler is buggy, or an invariant in the compiler is invalidated.
\item
An incomplete heuristic in the compiler fails.
\item
The compiled code exhausts some bounded resource, for instance the processor's code memory.
\end{enumerate}
Standard compilers can fail for all the above reasons.
Certified compilers are only required to rule out the second class of failures, but they can still fail for all the remaining reasons.
In particular, a compiler that systematically refuses to compile any well formed program is a sound compiler.
On the contrary, we would like our certified compiler to fail only in the fourth case.
We plan to achieve this with the following strategy.

First, the compiler is abstracted over all incomplete heuristics, seen as total functions.
To obtain executable code, the compiler is eventually composed with implementations of the abstracted strategies, with the composition taking care of any potential failure of the heuristics in finding a solution.

Second, we reject all malformed programs using dependent types: only well-formed programs should typecheck and the compiler can be applied only to well-typed programs.

Finally, exhaustion of bounded resources can be checked only at the very end of compilation.
Therefore, all intermediate compilation steps are now total functions that cannot diverge, nor fail: these properties are directly guaranteed by the type system of Matita.

Presently, the plan is not yet fulfilled.
However, we are improving the implemented code according to our plan.
We are doing this by progressively strenghthening the code through the use of dependent types.
We detail the different ways in which dependent types have been used so far. 

First, we encode informal invariants, or uses of \texttt{assert false} in the O'Caml code, with dependent types, converting partial functions into total functions.
There are numerous examples of this throughout the backend.
For example, in the \texttt{RTLabs} to \texttt{RTL} transformation pass, many functions only `make sense' when lists of registers passed to them as arguments conform to some specific length.
For instance, the \texttt{translate\_negint} function, which translates a negative integer constant:
\begin{lstlisting}[language=Grafite]
definition translate_negint :=
  $\lambda$globals: list ident.
  $\lambda$destrs: list register.
  $\lambda$srcrs: list register.
  $\lambda$start_lbl: label.
  $\lambda$dest_lbl: label.
  $\lambda$def: rtl_internal_function globals.
  $\lambda$prf: |destrs| = |srcrs|. (* assert here *)
    ...
\end{lstlisting}
The last argument to the function, \texttt{prf}, is a proof that the lengths of the lists of source and destination registers are the same.
This was an assertion in the O'Caml code.

Secondly, we make use of dependent types to make the Matita code correct by construction, and eventually the proofs of correctness for the compiler easier to write.
For instance, many intermediate languages in the backend of the compiler, from RTLabs to LTL, are graph based languages.
Here, function definitions consist of a graph (i.e. a map from labels to statements) and a pair of labels denoting the entry and exit points of this graph.
Practically, we would always like to ensure that the entry and exit labels are present in the statement graph.
We ensure that this is so with a dependent sum type in the \texttt{joint\_internal\_function} record, which all graph based languages specialise to obtain their own internal function representation:
\begin{lstlisting}[language=Grafite]
record joint_internal_function (globals: list ident) (p: params globals): Type[0] :=
{
  ...
  joint_if_code     : codeT $\ldots$ p;
  joint_if_entry    : $\Sigma$l: label. lookup $\ldots$ joint_if_code l $\neq$ None $\ldots$;
  ...
}.
\end{lstlisting}
Here, \texttt{codeT} is a parameterised type representing the `structure' of the function's body (a graph in graph based languages, and a list in the linearised LIN language).
Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph. A similar device exists for the exit label.

We make use of dependent types also for another reason: experimentation.
Namely, CompCert makes little use of dependent types to encode invariants.
In contrast, we wish to make as much use of dependent types as possible, both to experiment with different ways of encoding compilers in a proof assistant, but also as a way of `stress testing' Matita's support for dependent types.

Moreover, at the moment we make practically no use of inductive predicates to specify compiler invariants and to describe the semantics of intermediate languages.
On the contrary, all predicates are computable functions.
Therefore, the proof style that we will adopt will be necessarily significantly different from, say, CompCert's one.
At the moment, in Matita `Russell-'-style reasoning (in the sense of~\cite{sozeau:subset:2006}) seems to be the best solution for working with computable functions.
This style is heavily based on the idea that all computable functions should be specified using dependent types to describe their pre- and post-conditions.
As a consequence, it is natural to add dependent types almost everywhere in the Matita compiler's codebase.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{What we do not implement}
\label{subsect.what.we.do.not.implement}

There are several classes of functionality that we have chosen not to implement in the backend languages:
\begin{itemize}
\item
\textbf{Datatypes and functions over these datatypes that are not supported by the compiler.}
In particular, the compiler does not support the floating point datatype, nor accompanying functions over that datatype.
At the moment, frontend languages within the compiler possess constructors corresponding to floating point code.
These are removed during instruction selection (in the RTLabs to RTL transformation) using a daemon.\footnote{A Girardism.  An axiom of type \texttt{False}, from which we can prove anything.}
However, at some point, we would like the front end of the compiler to recognise programs that use floating point code and reject them as being invalid.
\item
\textbf{Axiomatised components that will be implemented using external oracles.}
Several large, complex pieces of compiler infrastructure, most noticably register colouring and fixed point calculation during liveness analysis have been axiomatised.
This was already agreed upon before the start of the project, and is clearly marked in the project proposal, following comments by those involved with the CompCert project about the difficulty in formalising register colouring in that project.
Instead, these components are axiomatised, along with the properties that they need to satisfy in order for the rest of the compilation chain to be correct.
These axiomatised components are found in the ERTL to LTL pass.

It should be noted that these axiomatised components fall into the following pattern: whilst their implementation is complex, and their proof of correctness is difficult, we are able to quickly and easily verify that any answer that they provide is correct. Therefore, we plan to provide implementations in OCaml only,
and to provide certified verifiers in Matita.
At the moment, the implementation of the certified verifiers is left as future work.
\item
\textbf{A few non-computational proof obligations.}
A few difficult-to-close, but non-computational (i.e. they do not prevent us from executing the compiler inside Matita), proof obligations have been closed using daemons in the backend.
These proof obligations originate with our use of dependent types for expressing invariants in the compiler.
However, here, it should be mentioned that many open proof obligations are simply impossible to close until we start to obtain stronger invariants from the proof of correctness for the compiler proper.
In particular, in the RTLabs to RTL pass, several proof obligations relating to lists of registers stored in a `local environment' appear to fall into this pattern.
\item
\textbf{Branch compression (tunnelling).}
This was a feature of the O'Caml compiler.
It is not yet currently implemented in the Matita compiler.
This feature is only an optimisation, and will not affect the correctness of the compiler.
\item
\textbf{`Real' tailcalls}
For the time being, tailcalls in the backend are translated to `vanilla' function calls during the ERTL to LTL pass.
This follows the O'Caml compiler, which did not implement tailcalls, and did this simplification step.
`Real' tailcalls are being implemented in the O'Caml compiler, and when this implementation is complete, we aim to port this code to the Matita compiler.
\end{itemize}

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\section{Associated changes to O'Caml compiler}
\label{sect.associated.changes.to.ocaml.compiler}

At the moment, only bugfixes, but no architectural changes we have made in the Matita backend have made their way back into the O'Caml compiler.
We do not see the heavy process of modularisation and abstraction as making its way back into the O'Caml codebase, as this is a significant rewrite of the backend code that is supposed to yield the same code after instantiating parameters, anyway.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\section{Future work}
\label{sect.future.work}

As mentioned in Section~\ref{subsect.what.we.do.not.implement}, there are several unimplemented features in the compiler, and several aspects of the Matita code that can be improved in order to make currently partial functions total.
We summarise this future work here:
\begin{itemize}
\item
We plan to make use of dependent types to identify `floating point' free programs and make all functions total over such programs.
This will remove a swathe of uses of daemons.
This should be routine.
\item
We plan to move expansion of integer modulus, and other related functions, into the instruction selection (RTLabs to RTL) phase.
This will also help to remove a swathe of uses of daemons, as well as potentially introduce new opportunities for optimisations that we currently miss in expanding these instructions at the C-light level.
\item
We plan to close all existing proof obligations that are closed using daemons, arising from our use of dependent types in the backend.
However, many may not be closable until we have completed Deliverable D4.4, the certification of the whole compiler, as we may not have invariants strong enough at the present time.
\item
We plan to port the O'Caml compiler's implementation of tailcalls when this is completed, and eventually port the branch compression code currently in the O'Caml compiler to the Matita implementation.
This should not cause any major problems.
\item
We plan to validate the backend translations, removing any obvious bugs, by executing the translation inside Matita on small C programs.
This is not critical, as the certification process will find all bugs anyway.
\item We plan to provide certified validators for all results provided by
external oracles written in OCaml. At the moment, we have axiomatized oracles
for computing least fixpoints during liveness analysis, for colouring
registers and for branch displacement in the assembler code.
\end{itemize}

\section{The back-end intermediate languages' semantics in Matita}
\label{sect.backend.intermediate.languages.semantics.matita}

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Abstracting related languages}
\label{subsect.abstracting.related.languages}

As mentioned in the report for Deliverable D4.2, a systematic process of abstraction, over the OCaml code, has taken place in the Matita encoding.
In particular, we have merged many of the syntaxes of the intermediate languages (i.e. RTL, ERTL, LTL and LIN) into a single `joint' syntax, which is parameterised by various types.
Equivalent intermediate languages to those present in the OCaml code can be recovered by specialising this joint structure.

As mentioned in the report for Deliverable D4.2, there are a number of advantages that this process of abstraction brings, from code reuse to allowing us to get a clearer view of the intermediate languages and their structure.
However, the semantics of the intermediate languages allow us to concretely demonstrate this improvement in clarity, by noting that the semantics of the LTL and the semantics of the LIN languages are identical.
In particular, the semantics of both LTL and LIN are implemented in exactly the same way.
The only difference between the two languages is how the next instruction to be interpreted is fetched.
In LTL, this involves looking up in a graph, whereas in LTL, this involves fetching from a list of instructions.

As a result, we see that the semantics of LIN and LTL are both instances of a single, more general language that is parametric in how the next instruction is fetched.
Furthermore, any prospective proof that the semantics of LTL and LIN are identical is now almost trivial, saving a deal of work in Deliverable D4.4.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Type parameters, and their purpose}
\label{subsect.type.parameters.their.purpose}

We mentioned in the Deliverable D4.2 report that all joint languages are parameterised by a number of types, which are later specialised to each distinct intermediate language.
As this parameterisation process is also dependent on designs decisions in the language semantics, we have so far held off summarising the role of each parameter.

We begin the abstraction process with the \texttt{params\_\_} record.
This holds the types of the representations of the different register varieties in the intermediate languages:
\begin{lstlisting}[language=Grafite]
record params__: Type[1] :=
{
  acc_a_reg: Type[0];
  acc_b_reg: Type[0];
  dpl_reg: Type[0];
  dph_reg: Type[0];
  pair_reg: Type[0];
  generic_reg: Type[0];
  call_args: Type[0];
  call_dest: Type[0];
  extend_statements: Type[0]
}.
\end{lstlisting}
We summarise what these types mean, and how they are used in both the semantics and the translation process:
\begin{center}
\begin{tabular*}{\textwidth}{p{4cm}p{11cm}}
Type & Explanation \\
\hline
\texttt{acc\_a\_reg} & The type of the accumulator A register.  In some languages this is implemented as the hardware accumulator, whereas in others this is a pseudoregister.\\
\texttt{acc\_b\_reg} & Similar to the accumulator A field, but for the processor's auxilliary accumulator, B. \\
\texttt{dpl\_reg} & The type of the representation of the low eight bit register of the MCS-51's single 16 bit register, DPL.  Can be either a pseudoregister or the hardware DPL register. \\
\texttt{dph\_reg} & Similar to the DPL register but for the eight high bits of the 16-bit register. \\
\texttt{pair\_reg} & Various different `move' instructions have been merged into a single move instruction in the joint language.  A value can either be moved to or from the accumulator in some languages, or moved to and from an arbitrary pseudoregister in others.  This type encodes how we should move data around the registers and accumulators. \\
\texttt{generic\_reg} & The representation of generic registers (i.e. those that are not devoted to a specific task). \\
\texttt{call\_args} & The actual arguments passed to a function.  For some languages this is simply the number of arguments passed to the function. \\
\texttt{call\_dest} & The destination of the function call. \\
\texttt{extend\_statements} & Instructions that are specific to a particular intermediate language, and which cannot be abstracted into the joint language.
\end{tabular*}
\end{center}

As mentioned in the report for Deliverable D4.2, the record \texttt{params\_\_} is enough to be able to specify the instructions of the joint languages:
\begin{lstlisting}[language=Grafite]
inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
  | COMMENT: String $\rightarrow$ joint_instruction p globals
  | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
  ...
  | OP1: Op1 $\rightarrow$ acc_a_reg p $\rightarrow$ acc_a_reg p $\rightarrow$ joint_instruction p globals
  | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals
  ...
\end{lstlisting}
Here, we see that the instruction \texttt{OP1} (a unary operation on the accumulator A) can be given quite a specific type, through the use of the \texttt{params\_\_} data structure.

Joint statements can be split into two subclasses: those who simply pass the flow of control onto their successor statement, and those that jump to a potentially remote location in the program.
Naturally, as some intermediate languages are graph based, and others linearised, the passing act of passing control on to the `successor' instruction can either be the act of following a graph edge in a control flow graph, or incrementing an index into a list.
We make a distinction between instructions that pass control onto their immediate successors, and those that jump elsewhere in the program, through the use of \texttt{succ}, denoting the immediate successor of the current instruction, in the \texttt{params\_} record described below.
\begin{lstlisting}[language=Grafite]
record params_: Type[1] :=
{
  pars__ :> params__;
  succ: Type[0]
}.
\end{lstlisting}
The type \texttt{succ} corresponds to labels, in the case of control flow graph based languages, or is instantiated to the unit type for the linearised language, LIN.
Using \texttt{param\_} we can define statements of the joint language:
\begin{lstlisting}[language=Grafite]
inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
  | sequential: joint_instruction p globals $\rightarrow$ succ p $\rightarrow$ joint_statement p globals
  | GOTO: label $\rightarrow$ joint_statement p globals
  | RETURN: joint_statement p globals.
\end{lstlisting}
Note that in the joint language, instructions are `linear', in that they have an immediate successor.
Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program. The conditional jump instruction COND is `linear', since it
has an immediate successor, but it also takes an arbitrary location (a label)
to jump to.

For the semantics, we need further parametererised types.
In particular, we parameterise the result and parameter type of an internal function call in \texttt{params0}:
\begin{lstlisting}[language=Grafite]
record params0: Type[1] :=
{
  pars__' :> params__;
  resultT: Type[0];
  paramsT: Type[0]
}.
\end{lstlisting}
Here, \texttt{paramsT} and \texttt{resultT} typically are the (pseudo)registers that store the parameters and result of a function.

We further extend \texttt{params0} with a type for local variables in internal function calls:
\begin{lstlisting}[language=Grafite]
record params1 : Type[1] :=
{
  pars0 :> params0;
  localsT: Type[0]
}.
\end{lstlisting}
Again, we expand our parameters with types corresponding to the code representation (either a control flow graph or a list of statements).
Further, we hypothesise a generic method for looking up the next instruction in the graph, called \texttt{lookup}.
Note that \texttt{lookup} may fail, and returns an \texttt{option} type:
\begin{lstlisting}[language=Grafite]
record params (globals: list ident): Type[1] :=
{
  succ_ : Type[0];
  pars1 :> params1;
  codeT : Type[0];
  lookup: codeT $\rightarrow$ label $\rightarrow$ option (joint_statement (mk_params_ pars1 succ_) globals)
}.
\end{lstlisting}
We now have what we need to define internal functions for the joint language.
The first two `universe' fields are only used in the compilation process, for generating fresh names, and do not affect the semantics.
The rest of the fields affect both compilation and semantics.
In particular, we have a description of the result, parameters and the local variables of a function.
Note also that we have lifted the hypothesised \texttt{lookup} function from \texttt{params} into a dependent sigma type, which combines a label (the entry and exit points of the control flow graph or list) combined with a proof that the label is in the graph structure:
\begin{lstlisting}[language=Grafite]
record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
{
  joint_if_luniverse: universe LabelTag;
  joint_if_runiverse: universe RegisterTag;
  joint_if_result   : resultT p;
  joint_if_params   : paramsT p;
  joint_if_locals   : localsT p;
  joint_if_stacksize: nat;
  joint_if_code     : codeT ... p;
  joint_if_entry    : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ?;
  joint_if_exit     : $\Sigma$l: label. lookup ... joint_if_code l $\neq$ None ?
}.
\end{lstlisting}
Naturally, a question arises as to why we have chosen to split up the parameterisation into so many intermediate records, each slightly extending earlier ones.
The reason is because some intermediate languages share a host of parameters, and only differ on some others.
For instance, in instantiating the ERTL language, certain parameters are shared with RTL, whilst others are ERTL specific:
\begin{lstlisting}[language=Grafite]
...
definition ertl_params__: params__ :=
 mk_params__ register register register register (move_registers $\times$ move_registers)
  register nat unit ertl_statement_extension.
...
definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0.
definition ertl_params: $\forall$globals. params globals := rtl_ertl_params ertl_params0.
...
definition ertl_statement := joint_statement ertl_params_.

definition ertl_internal_function :=
  $\lambda$globals.joint_internal_function ... (ertl_params globals).
\end{lstlisting}
Here, \texttt{rtl\_ertl\_params1} are the common parameters of the ERTL and RTL languages:
\begin{lstlisting}[language=Grafite]
definition rtl_ertl_params1 := $\lambda$pars0. mk_params1 pars0 (list register).
\end{lstlisting}

The record \texttt{more\_sem\_params} bundles together functions that store and retrieve values in various forms of register:
\begin{lstlisting}[language=Grafite]
record more_sem_params (p:params_): Type[1] :=
{
  framesT: Type[0];
  empty_framesT: framesT;

  regsT: Type[0];
  empty_regsT: regsT;

  call_args_for_main: call_args p;
  call_dest_for_main: call_dest p;

  greg_store_: generic_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
  greg_retrieve_: regsT $\rightarrow$ generic_reg p $\rightarrow$ res beval;
  acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
  acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval;
  ...
  dpl_store_: dpl_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
  dpl_retrieve_: regsT $\rightarrow$ dpl_reg p $\rightarrow$ res beval;
  ...
  pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT;
}.
\end{lstlisting}
Here, the fields \texttt{empty\_framesT}, \texttt{empty\_regsT}, \texttt{call\_args\_for\_main} and \texttt{call\_dest\_for\_main} are used for state initialisation.

The fields \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively.
Similarly, \texttt{pair\_reg\_move} implements the generic move instruction of the joint language.
Here \texttt{framesT} is the type of stack frames, with \texttt{empty\_framesT} an empty stack frame.

The two hypothesised values \texttt{call\_args\_for\_main} and \texttt{call\_dest\_for\_main} deal with problems with the \texttt{main} function of the program, and how it is handled.
In particular, we need to know when the \texttt{main} function has finished executing.
But this is complicated, in C, by the fact that the \texttt{main} function is explicitly allowed to be recursive (disallowed in C++).
Therefore, to understand whether the exiting \texttt{main} function is really exiting, or just recursively calling itself, we need to remember the address to which \texttt{main} will return control once the initial call to \texttt{main} has finished executing.
This is done with \texttt{call\_dest\_for\_main}, whereas \texttt{call\_args\_for\_main} holds the \texttt{main} function's arguments.

We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}:
\begin{lstlisting}[language=Grafite]
record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] :=
{
  more_sparams1 :> more_sem_params p;

  succ_pc: succ p $\rightarrow$ address $\rightarrow$ res address;
  pointer_of_label: genv ... p $\rightarrow$ pointer $\rightarrow$
    label $\rightarrow$ res ($\Sigma$p:pointer. ptype p = Code);
  ...
  fetch_statement:
    genv ... p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
    res (joint_statement (mk_sem_params ... more_sparams1) globals);
  ...
  save_frame:
    address $\rightarrow$ nat $\rightarrow$ paramsT ... p $\rightarrow$ call_args p $\rightarrow$ call_dest p $\rightarrow$
    state (mk_sem_params ... more_sparams1) $\rightarrow$
    res (state (mk_sem_params ... more_sparams1));
  pop_frame:
    genv globals p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
    res ((state (mk_sem_params ... more_sparams1)));
  ...
  set_result:
    list val $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
    res (state (mk_sem_params ... more_sparams1));
  exec_extended:
    genv globals p $\rightarrow$ extend_statements (mk_sem_params ... more_sparams1) $\rightarrow$
    succ p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
    IO io_out io_in (trace $\times$ (state (mk_sem_params ... more_sparams1)))
 }.
\end{lstlisting}
The field \texttt{succ\_pc} takes an address, and a `successor' label, and returns the address of the instruction immediately succeeding the one at hand.

Here, \texttt{fetch\_statement} fetches the next statement to be executed.
The fields \texttt{save\_frame} and \texttt{pop\_frame} manipulate stack frames.
In particular, \texttt{save\_frame} creates a new stack frame on the top of the stack, saving the destination and parameters of a function, and returning an updated state.
The field \texttt{pop\_frame} destructively pops a stack frame from the stack, returning an updated state.
Further, \texttt{set\_result} saves the result of the function computation, and \texttt{exec\_extended} is a function that executes the extended statements, peculiar to each individual intermediate language.

We bundle \texttt{params} and \texttt{sem\_params} together into a single record.
This will be used in the function \texttt{eval\_statement} which executes a single statement of the joint language:
\begin{lstlisting}[language=Grafite]
record sem_params2 (globals: list ident): Type[1] :=
{
  p2 :> params globals;
  more_sparams2 :> more_sem_params2 globals p2
}.
\end{lstlisting}
\noindent
The \texttt{state} record holds the current state of the interpreter:
\begin{lstlisting}[language=Grafite]
record state (p: sem_params): Type[0] :=
{
  st_frms: framesT ? p;
  pc: address;
  sp: pointer;
  isp: pointer;
  carry: beval;
  regs: regsT ? p;
  m: bemem
}.
\end{lstlisting}
Here \texttt{st\_frms} represent stack frames, \texttt{pc} the program counter, \texttt{sp} the stack pointer, \texttt{isp} the internal stack pointer, \texttt{carry} the carry flag, \texttt{regs} the registers (hardware and pseudoregisters) and \texttt{m} external RAM.
Note that we have two stack pointers, as we have two stacks: the physical stack of the MCS-51 microprocessor, and an emulated stack in external RAM.
The MCS-51's own stack is minuscule, therefore it is usual to emulate a much larger, more useful stack in external RAM.
We require two stack pointers as the MCS-51's \texttt{PUSH} and \texttt{POP} instructions manipulate the physical stack, and not the emulated one.

We use the function \texttt{eval\_statement} to evaluate a single joint statement:
\begin{lstlisting}[language=Grafite]
definition eval_statement:
  $\forall$globals: list ident.$\forall$p:sem_params2 globals.
    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
...
\end{lstlisting}
We examine the type of this function.
Note that it returns a monadic action, \texttt{IO}, denoting that it may have an IO \emph{side effect}, where the program reads or writes to some external device or memory address.
Monads and their use are further discussed in Subsection~\ref{subsect.use.of.monads}.
Further, the function returns a new state, updated by the single step of execution of the program.
Finally, a \emph{trace} is also returned, which records externally observable `events', such as the calling of external functions and the emission of cost labels.

%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
% SECTION.                                                                    %
%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
\subsection{Use of monads}
\label{subsect.use.of.monads}

Monads are a categorical notion that have recently gained an amount of traction in functional programming circles.
In particular, it was noted by Moggi that monads could be used to sequence \emph{effectful} computations in a pure manner.
Here, `effectful computations' cover a lot of ground, from writing to files, generating fresh names, or updating an ambient notion of state.

A monad can be characterised by the following:
\begin{itemize}
\item
A data type, $M$.
For instance, the \texttt{option} type in OCaml or Matita.
\item
A way to `inject' or `lift' pure values into this data type (usually called \texttt{return}).
We call this function \texttt{return} and say that it must have type $\alpha \rightarrow M \alpha$, where $M$ is the name of the monad.
In our example, the `lifting' function for the \texttt{option} monad can be implemented as:
\begin{lstlisting}[language=Grafite]
let return x = Some x
\end{lstlisting}
\item
A way to `sequence' monadic functions together, to form another monadic function, usually called \texttt{bind}.
Bind has type $M \alpha \rightarrow (\alpha \rightarrow M \beta) \rightarrow M \beta$.
We can see that bind `unpacks' a monadic value, applies a function after unpacking, and `repacks' the new value in the monad.
In our example, the sequencing function for the \texttt{option} monad can be implemented as:
\begin{lstlisting}[language=Grafite]
let bind o f =
  match o with
    None -> None
    Some s -> f s
\end{lstlisting}
\item
A series of algebraic laws that relate \texttt{return} and \texttt{bind}, ensuring that the sequencing operation `does the right thing' by retaining the order of effects.
These \emph{monad laws} should also be useful in reasoning about monadic computations in the proof of correctness of the compiler.
\end{itemize}
In the semantics of both front and back-end intermediate languages, we make use of monads.
This monadic infrastructure is shared between the front-end and back-end languages.

In particular, an `IO' monad, signalling the emission of a cost label, or the calling of an external function, is heavily used in the semantics of the intermediate languages.
Here, the monad's sequencing operation ensures that cost label emissions and function calls are maintained in the correct order.
We have already seen how the \texttt{eval\_statement} function of the joint language is monadic, with type:
\begin{lstlisting}[language=Grafite]
definition eval_statement:
  $\forall$globals: list ident.$\forall$p:sem_params2 globals.
    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
...
\end{lstlisting}
If we examine the body of \texttt{eval\_statement}, we may also see how the monad sequences effects.
For instance, in the case for the \texttt{LOAD} statement, we have the following:
\begin{lstlisting}[language=Grafite]
definition eval_statement:
  $\forall$globals: list ident. $\forall$p:sem_params2 globals.
    genv globals p $\rightarrow$ state p $\rightarrow$ IO io_out io_in (trace $\times$ (state p)) :=
  $\lambda$globals, p, ge, st.
  ...
  match s with
  | LOAD dst addrl addrh $\Rightarrow$
    ! vaddrh $\leftarrow$ dph_retrieve ... st addrh;
    ! vaddrl $\leftarrow$ dpl_retrieve ... st addrl;
    ! vaddr $\leftarrow$ pointer_of_address $\langle$vaddrl,vaddrh$\rangle$;
    ! v $\leftarrow$ opt_to_res ... (msg FailedLoad) (beloadv (m ... st) vaddr);
    ! st $\leftarrow$ acca_store p ... dst v st;
    ! st $\leftarrow$ next ... l st ;
      ret ? $\langle$E0, st$\rangle$
\end{lstlisting}
Here, we employ a certain degree of syntactic sugaring.
The syntax
\begin{lstlisting}[language=Grafite]
  ...
! vaddrh $\leftarrow$ dph_retrieve ... st addrh;
! vaddrl $\leftarrow$ dpl_retrieve ... st addrl;
  ...
\end{lstlisting}
is sugaring for the \texttt{IO} monad's binding operation.
We can expand this sugaring to the following much more verbose code:
\begin{lstlisting}[language=Grafite]
  ...
  bind (dph_retrieve ... st addrh) ($\lambda$vaddrh. bind (dpl_retrieve ... st addrl)
    ($\lambda$vaddrl. ...))
\end{lstlisting}
Note also that the function \texttt{ret} is implementing the `lifting', or return function of the \texttt{IO} monad.

We believe the sugaring for the monadic bind operation makes the program much more readable, and therefore easier to reason about.
In particular, note that the functions \texttt{dph\_retrieve}, \texttt{pointer\_of\_address}, \texttt{acca\_store} and \texttt{next} are all monadic.

Note, however, that inside this monadic code, there is also another monad hiding.
The \texttt{res} monad signals failure, along with an error message.
The monad's sequencing operation ensures the order of error messages does not get rearranged.
The function \texttt{opt\_to\_res} lifts an option type into this monad, with an error message to be used in case of failure.
The \texttt{res} monad is then coerced into the \texttt{IO} monad, ensuring the whole code snippet typechecks.

\subsection{Memory models}
\label{subsect.memory.models}

Currently, the semantics of the front and back-end intermediate languages are built around two distinct memory models.
The front-end languages reuse the CompCert 1.6 memory model, whereas the back-end languages employ a version tailored to their needs.
This split between the memory models reflects the fact that the front-end and back-end languages have different requirements from their memory models.

In particular, the CompCert 1.6 memory model places quite heavy restrictions on where in memory one can read from.
To read a value in this memory model, you must supply an address, complete with the size of `chunk' to read following that address.
The read is only successful if you attempt to read at a genuine `value boundary', and read the appropriate amount of memory for that value.
As a result, with that memory model you are unable to read the third byte of a 32-bit integer value directly from memory, for instance.
This has some consequences for the compiler, namely an inability to write a \texttt{memcpy} routine.

However, the CerCo memory model operates differently, as we need to move data `piecemeal' between stacks in the back-end of the compiler.
As a result, the back-end memory model allows one to read data at any memory location, not just on value boundaries.
This has the advantage that we can successfully give a semantics to a \texttt{memcpy} routine in the back-end of the CerCo compiler (remembering that \texttt{memcpy} is nothing more than `read a byte, copy a byte' repeated in a loop), an advantage over CompCert.  However, the front-end of CerCo cannot because its memory model and values are the similar to CompCert 1.6.

More recent versions of CompCert's memory model have evolved in a similar direction, with a byte-by-byte representation of memory blocks.  However, there remains an important difference in the handling of pointer values in the rest of the formalisation.  In particular, in CompCert 1.10 only complete pointer values can be loaded in all of the languages in the compiler, whereas in CerCo we need to represent individual bytes of a pointer in the back-end to support our 8-bit target architecture. 

Right now, the two memory models are interfaced during the translation from RTLabs to RTL.
It is an open question whether we will unify the two memory models, using only the back-end, bespoke memory model throughout the compiler, as the CompCert memory model seems to work fine for the front-end, where such byte-by-byte copying is not needed.
However, should we decide to port the front-end to the new memory model, it has been written in such an abstract way that doing so would be relatively straightforward.