source: Deliverables/D1.2/CompilerProofOutline/outline.tex @ 1741

\documentclass[a4paper, 10pt]{article}

\usepackage{a4wide}
\usepackage{amsfonts}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage[english]{babel}
\usepackage{color}
\usepackage{diagrams}
\usepackage{graphicx}
\usepackage[colorlinks]{hyperref}
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{microtype}
\usepackage{skull}
\usepackage{stmaryrd}
\usepackage{wasysym}

\lstdefinelanguage{matita-ocaml} {
  mathescape=true
}
\lstset{
  language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
  showspaces=false, showstringspaces=false, extendedchars=false,
  inputencoding=utf8x, tabsize=2
}

\title{Proof outline for the correctness of the CerCo compiler}
\date{\today}
\author{The CerCo team}

\begin{document}

\maketitle

\section{Introduction}
\label{sect.introduction}

In the last project review of the CerCo project, the project reviewers expressed the opinion that it would be a good idea to attempt to write down some of the statements of the correctness theorems that we intend to prove about the complexity preserving compiler.
This document provides a very high-level, pen-and-paper sketch of what we view as the best path to completing the correctness proof for the compiler.
In particular, for every translation between two intermediate languages, in both the front- and back-ends, we identify the key translation steps, and identify some invariants that we view as being important for the correctness proof.

\section{Front-end: Clight to RTLabs}

The front-end of the CerCo compiler consists of several stages:

\begin{center}
\begin{minipage}{.8\linewidth}
\begin{tabbing}
\quad \= $\downarrow$ \quad \= \kill
\textsf{Clight}\\
\> $\downarrow$ \> cast removal\\
\> $\downarrow$ \> add runtime functions\footnote{Following the last project
meeting we intend to move this transformation to the back-end}\\
\> $\downarrow$ \> cost labelling\\
\> $\downarrow$ \> loop optimizations\footnote{\label{lab:opt2}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation)\\
\> $\downarrow$ \> partial redundancy elimination$^{\mbox{\scriptsize \ref{lab:opt2}}}$ (an endo-transformation)\\
\> $\downarrow$ \> stack variable allocation and control structure
 simplification\\
\textsf{Cminor}\\
\> $\downarrow$ \> generate global variable initialisation code\\
\> $\downarrow$ \> transform to RTL graph\\
\textsf{RTLabs}\\
\> $\downarrow$ \> \\
\>\,\vdots
\end{tabbing}
\end{minipage}
\end{center}

Here, by `endo-transformation', we mean a mapping from language back to itself:
the loop optimization step maps the Clight language to itself.

%Our overall statements of correctness with respect to costs will
%require a correctly labelled program
There are three layers in most of the proofs proposed:
\begin{enumerate}
\item invariants closely tied to the syntax and transformations using
  dependent types,
\item a forward simulation proof, and
\item syntactic proofs about the cost labelling.
\end{enumerate}
The first will support both function correctness and allow us to show
the totality of some of the compiler stages (that is, these stages of
the compiler cannot fail).  The second provides the main functional
correctness result, and the last will be crucial for applying
correctness results about the costings from the back-end.

We will also prove that a suitably labelled RTLabs trace can be turned
into a \emph{structured trace} which splits the execution trace into
cost-label-to-cost-label chunks with nested function calls.  This
structure was identified during work on the correctness of the
back-end cost analysis as retaining important information about the
structure of the execution that is difficult to reconstruct later in
the compiler.

\subsection{Clight Cast removal}

This removes some casts inserted by the parser to make arithmetic
promotion explicit when they are superfluous (such as
\lstinline[language=C]'c = (short)((int)a + (int)b);').

The transformation only affects Clight expressions, recursively
detecting casts that can be safely eliminated.  The semantics provides
a big-step definition for expression, so we should be able to show a
lock-step forward simulation using a lemma showing that cast
elimination does not change the evaluation of expressions.  This lemma
will follow from a structural induction on the source expression.  We
have already proved a few of the underlying arithmetic results
necessary to validate the approach.

\subsection{Clight cost labelling}

This adds cost labels before and after selected statements and
expressions, and the execution traces ought to be equivalent modulo
cost labels.  Hence it requires a simple forward simulation with a
limited amount of stuttering whereever a new cost label is introduced.
A bound can be given for the amount of stuttering allowed can be given
based on the statement or continuation to be evaluated next.

We also intend to show three syntactic properties about the cost
labelling:
\begin{itemize}
\item every function starts with a cost label,
\item every branching instruction is followed by a label (note that
  exiting a loop is treated as a branch), and
\item the head of every loop (and any \lstinline'goto' destination) is
  a cost label.
\end{itemize}
These can be shown by structural induction on the source term.

\subsection{Clight to Cminor translation}

This translation is the first to introduce some invariants, with the
proofs closely tied to the implementation by dependent typing.  These
are largely complete and show that the generated code enjoys:
\begin{itemize}
\item some minimal type safety shown by explicit checks on the
  Cminor types during the transformation (a little more work remains
  to be done here, but follows the same form);
\item that variables named in the parameter and local variable
  environments are distinct from one another, again by an explicit
  check;
\item that variables used in the generated code are present in the
  resulting environment (either by checking their presence in the
  source environment, or from a list of freshly temporary variables);
  and
\item that all \lstinline[language=C]'goto' labels are present (by
  checking them against a list of source labels and proving that all
  source labels are preserved).
\end{itemize}

The simulation will be similar to the relevant stages of CompCert
(Clight to Csharpminor and Csharpminor to Cminor --- in the event that
the direct proof is unwieldy we could introduce a corresponding
intermediate language).  During early experimentation with porting
CompCert definitions to the Matita proof assistant we found little
difficulty reproving the results for the memory model, so we plan to
port the memory injection properties and use them to relate Clight
in-memory variables with either a local variable valuation or a stack
slot, depending on how it was classified.

This should be sufficient to show the equivalence of (big-step)
expression evaluation.  The simulation can then be shown by relating
corresponding blocks of statement and continuations with their Cminor
counterparts and proving that a few steps reaches the next matching
state.

The syntactic properties required for cost labels remain similar and a
structural induction on the function bodies should be sufficient to
show that they are preserved.

\subsection{Cminor global initialisation code}

This short phase replaces the global variable initialisation data with
code that executes when the program starts.  Each piece of
initialisation data in the source is matched by a new statement
storing that data.  As each global variable is allocated a distinct
memory block, the program state after the initialisation statements
will be the same as the original program's state at the start of
execution, and will proceed in the same manner afterwards.

% Actually, the above is wrong...
% ... this ought to be in a fresh main function with a fresh cost label

\subsection{Cminor to RTLabs translation}

In this part of the compiler we transform the program's functions into
control flow graphs.  It is closely related to CompCert's Cminorsel to
RTL transformation, albeit with target-independent operations.

We already enforce several invariants with dependent types: some type
safety is enforced mostly using the type information from Cminor; and
that the graph is closed (by showing that each successor was recently
added, or corresponds to a \lstinline[language=C]'goto' label which
are all added before the end).  Note that this relies on a
monotonicity property; CompCert maintains a similar property in a
similar way while building RTL graphs.  We will also add a result
showing that all of the pseudo-register names are distinct for use by
later stages using the same method as Cminor.

The simulation will relate Cminor states to RTLabs states about to
execute the corresponding code (with a corresponding continuation).
Each Cminor statement becomes zero or more RTLabs statements, with a
decreasing measure based on the statement and continuations similar to
CompCert's.  We may also follow CompCert in using a relational
specification of this stage so as to abstract away from the functional
(and highly dependently typed) definition.

The first two labelling properties remain as before; we will show that
cost labels are preserved, so the function entry point will be a cost
label, and successors that are cost labels map still map to cost
labels, preserving the condition on branches.  We replace the property
for loops with the notion that we will always reach a cost label or
the end of the function by following a bounded number of successors.
This can be easily seen in Cminor using the requirement for cost
labels at the head of loops and after gotos.  It remains to show that
this is preserved by the translation to RTLabs.  % how?

\subsection{RTLabs structured trace generation}

This proof-only step incorporates the function call structure and cost
labelling properties into the execution trace.  As the function calls
are nested within the trace, we need to distinguish between
terminating and non-terminating function calls.

Thus we use the excluded middle (specialised to a function termination
property) to do this.  Terminating functions are built by following
the trace, breaking it into chunks between cost labels and recursively
processing function calls.  The main difficulties here are the
non-structurally recursive nature of the function (instead we use the
size of the termination proof as a measure) and using the properties
on RTLabs cost labelling to create the correct structure.  We also
show that the lower stack frames are preserved during function calls
in order to prove that after returning from a function call we execute
the correct code.  This part of the work has already been constructed,
but still requires a simple proof to show that flattening the structured
trace recreates the original flat trace.

The non-terminating case uses the excluded middle to decide whether to
use the function described above to construct an inductive terminating
structured trace, or a coinductive version for non-termination.  It
follows the trace like the terminating version to build up chunks of
trace from cost-label to cost-label (which, by the finite distance to
a cost label property shown before, can be represented by an inductive
type), unless it encounters a non-terminating function in which case
it corecursively processes that.  This part of the trace
transformation is currently under construction, and will also need a
flattening result to show that it is correct.

\section{Backend: RTLabs to machine code}
\label{sect.backend.rtlabs.machine.code}

The compiler backend consists of the following intermediate languages, and stages of translation:

\begin{center}
\begin{minipage}{.8\linewidth}
\begin{tabbing}
\quad \=\,\vdots\= \\
\> $\downarrow$ \>\\
\> $\downarrow$ \quad \= \kill
\textsf{RTLabs}\\
\> $\downarrow$ \> copy propagation\footnote{\label{lab:opt}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation) \\
\> $\downarrow$ \> instruction selection\\
\textsf{RTL}\\
\> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\
\> $\downarrow$ \> calling convention made explicit \\
\> $\downarrow$ \> layout of activation records \\
\textsf{ERTL}\\
\> $\downarrow$ \> register allocation and spilling\\
\> $\downarrow$ \> dead code elimination\\
\textsf{LTL}\\
\> $\downarrow$ \> function linearisation\\
\> $\downarrow$ \> branch compression (an endo-transformation) \\
\textsf{LIN}\\
\> $\downarrow$ \> relabeling\\
\textsf{ASM}\\
\> $\downarrow$ \> pseudoinstruction expansion\\
\textsf{MCS-51 machine code}\\
\end{tabbing}
\end{minipage}
\end{center}

\subsection{The RTLabs to RTL translation}
\label{subsect.rtlabs.rtl.translation}

% dpm: type system and casting load (???)
We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model:

\begin{displaymath}
\mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{int}_i \mid \mathtt{ptr}_i
\end{displaymath}

We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.

\begin{displaymath}
\mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha)
\end{displaymath}

where

\begin{displaymath}
\mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
\end{displaymath}

\begin{displaymath}
\mathtt{BEMem} = \mathtt{Mem} \mathtt{Value}
\end{displaymath}

\begin{displaymath}
\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
\end{displaymath}

\begin{displaymath}
\mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null})
\end{displaymath}

\begin{center}
\begin{picture}(2, 2)
\put(0,-20){\framebox(25,25)[c]{\texttt{v}}}
\put(26,-20){\framebox(25,25)[c]{\texttt{4}}}
\put(51,-20){\framebox(25,25)[c]{\texttt{cont}}}
\put(76,-20){\framebox(25,25)[c]{\texttt{cont}}}
\put(101,-20){\framebox(25,25)[c]{\texttt{cont}}}
\end{picture}
\end{center}

\begin{displaymath}
\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
\end{displaymath}

\begin{displaymath}
\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
\end{displaymath}

\begin{displaymath}
\begin{array}{rll}
\mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
\end{array}
\end{displaymath}

\begin{displaymath}
\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
\end{displaymath}

\begin{displaymath}
\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
\end{displaymath}

\begin{displaymath}
\sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{Frame})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem}))
\end{displaymath}

\begin{displaymath}
\sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step}
\end{displaymath}

\begin{displaymath}
\sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step}
\end{displaymath}

Return one step commuting diagram:

\begin{displaymath}
\begin{diagram}
s & \rTo^{\text{one step of execution}} & s'   \\
  & \rdTo                             & \dTo \\
  &                                   & \llbracket s'' \rrbracket
\end{diagram}
\end{displaymath}

Call one step commuting diagram:

\begin{displaymath}
\begin{diagram}
s & \rTo^{\text{one step of execution}} & s'   \\
  & \rdTo                             & \dTo \\
  &                                   & \llbracket s'' \rrbracket
\end{diagram}
\end{displaymath}

\begin{displaymath}
\begin{diagram}
\mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME)
\end{diagram}
\end{displaymath}

\begin{displaymath}
\begin{array}{rcl}
\mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\
\mathtt{RETURN}                                                      & \longrightarrow & \mathtt{RETURN} \\
\end{array} 
\end{displaymath}

\begin{displaymath}
\begin{array}{rcl}
\sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\
\sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register}
\end{array} 
\end{displaymath}

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

\begin{displaymath}
\begin{diagram}
& & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\
& \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\
\skull & & & & \mathtt{regs} = [\mathtt{params}/-] \\
& & & & \mathtt{sp} = \mathtt{ALLOC} \\
& & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\
\end{diagram}
\end{displaymath}

\begin{align*}
\llbracket \mathtt{RETURN} \rrbracket \\
\mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
v*                    & := m(\mathtt{rv\_regs}) \\
\mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
\mathtt{regs}[v* / \mathtt{dst}] \\
\end{align*}

\begin{displaymath}
\begin{diagram}
s    & \rTo^1 & s' & \rTo^1 & s'' \\
\dTo &        &    & \rdTo  & \dTo \\
\llbracket s \rrbracket & \rTo(1,3)^1 & & & \llbracket s'' \rrbracket \\ 
\mathtt{CALL} \\
\end{diagram}
\end{displaymath}

\begin{displaymath}
\begin{diagram}
s    & \rTo^1 & s' & \rTo^1 & s'' \\
\dTo &        &    & \rdTo  & \dTo \\
\  & \rTo(1,3) & & & \ \\
\mathtt{RETURN} \\
\end{diagram}
\end{displaymath}

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

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

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

\begin{align*}
\mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
\mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
\mathtt{graph} & \mapsto \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
& \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
\end{align*}

\begin{displaymath}
\begin{diagram}
\mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
\dTo & & \dTo \\
\underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
\underbrace{\ldots}_{\mathtt{prologue}} \\
\end{diagram}
\end{displaymath}

\begin{displaymath}
\begin{diagram}
\mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
\dTo & & \dTo \\
\underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
\underbrace{\ldots} \\
\end{diagram}
\end{displaymath}

\begin{align*}
\mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\
                       & \mathtt{pop\ ra}; \\
                       & \mathtt{save\ callee\_saved}; \\
                                                                                         & \mathtt{get\_params} \\
                                                                                         & \ \ \mathtt{reg\_params}: \mathtt{move} \\
                                                                                         & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\
\end{align*}

\begin{align*}
\mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\
                                                                                         & \mathtt{restore\_registers}; \\
                       & \mathtt{push\ ra}; \\
                       & \mathtt{delete\_frame}; \\
                       & \mathtt{save return} \\
\end{align*}

\begin{displaymath}
\mathtt{CALL}\ id \mapsto \mathtt{set\_params};\ \mathtt{CALL}\ id;\ \mathtt{fetch\_result}
\end{displaymath}

\subsection{The ERTL to LTL translation}
\label{subsect.ertl.ltl.translation}

\subsection{The LTL to LIN translation}
\label{subsect.ltl.lin.translation}

We require a map, $\sigma$, from LTL statuses, where program counters are represented as labels in a graph data structure, to LIN statuses, where program counters are natural numbers:
\begin{displaymath}
\mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N}
\end{displaymath}

The LTL to LIN translation pass also linearises the graph data structure into a list of instructions.
Pseudocode for the linearisation process is as follows:

\begin{lstlisting}
let rec linearise graph visited required generated todo :=
  match todo with
  | l::todo ->
    if l $\in$ visited then
      let generated := generated $\cup\ \{$ Goto l $\}$ in
      let required := required $\cup$ l in
        linearise graph visited required generated todo
    else
      -- Get the instruction at label `l' in the graph
      let lookup := graph(l) in
      let generated := generated $\cup\ \{$ lookup $\}$ in
      -- Find the successor of the instruction at label `l' in the graph
      let successor := succ(l, graph) in
      let todo := successor::todo in
        linearise graph visited required generated todo
  | []      -> (required, generated)
\end{lstlisting}

It is easy to see that this linearisation process eventually terminates.
In particular, the size of the visited label set is monotonically increasing, and is bounded above by the size of the graph that we are linearising.

The initial call to \texttt{linearise} sees the \texttt{visited}, \texttt{required} and \texttt{generated} sets set to the empty set, and \texttt{todo} initialized with the singleton list consisting of the entry point of the graph.
We envisage needing to prove the following invariants on the linearisation function above:

\begin{enumerate}
\item
$\mathtt{visited} \approx \mathtt{generated}$, where $\approx$ is \emph{multiset} equality, as \texttt{generated} is a set of instructions where instructions may mention labels multiple times, and \texttt{visited} is a set of labels,
\item
$\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$,
\item
$\mathtt{required} \subseteq \mathtt{visited}$,
\item
$\mathtt{visited} \cap \mathtt{todo} = \emptyset$.
\end{enumerate}

The invariants collectively imply the following properties, crucial to correctness, about the linearisation process:

\begin{enumerate}
\item
Every graph node is visited at most once,
\item
Every instruction that is generated is generated due to some graph node being visited,
\item
The successor instruction of every instruction that has been visited already will eventually be visited too.
\end{enumerate}

Note, because the LTL to LIN transformation is the first time the program is linearised, we must discover a notion of `well formed program' suitable for linearised forms.
In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions:

\begin{enumerate}
\item
For every jump to a label in a linearised program, the target label exists at some point in the program,
\item
Each label is unique, appearing only once in the program,
\item
The final instruction of a program must be a return.
\end{enumerate}

We assume that these properties will be easy consequences of the invariants on the linearisation function defined above.

The final condition above is potentially a little opaque, so we explain further.
First, the only instructions that can reasonably appear in final position at the end of a program are returns or backward jumps, as any other instruction would cause execution to `fall out' of the end of the program (for example, when a function invoked with \texttt{CALL} returns, it returns to the next instruction past the \texttt{CALL} that invoked it).
However, in LIN, though each function's graph has been linearised, the entire program is not yet fully linearised into a list of instructions, but rather, a list of `functions', each consisting of a linearised body along with other data.
Each well-formed function must end with a call to \texttt{RET}, and therefore the only correct instruction that can terminate a LIN program is a \texttt{RET} instruction.

\subsection{The LIN to ASM and ASM to MCS-51 machine code translations}
\label{subsect.lin.asm.translation}

The LIN to ASM translation step is trivial, being almost the identity function.
The only non-trivial feature of the LIN to ASM translation is that all labels are `named apart' so that there is no chance of freshly generated labels from different namespaces clashing with labels from another namespace.

The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.

\section{Estimated effort}
Based on the rough analysis performed so far we can now estimate the total
effort for the certification of the compiler. We obtain the estimation by
combining, for each pass: 1) the number of lines of code to be certified;
2) the ratio number of lines of proof on number of lines of code from
CompCert project~\cite{compcert} for the CompCert pass that is closer to
ours; 3) an estimation of the complexity of the pass according to the
analysis above.

\begin{tabular}{lrll}
Pass origin & Code lines & CompCert ratio & Estimated effort \\
Clight & \\
Cminor & \\
RTLabs & 1252 & 1.17 \permil & 1.5 \\
RTL    &  469 & 2.90 \permil & 1.4 \\
ERTL   &  789 & 2.79 \permil & 2.2 \\
LTL    &      & \\
LIN    &  354 & 7.34 \permil & 2.6 \\
ASM    &      & \\
\end{tabular}

\end{document}