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

\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}

\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}

\section{The RTLabs to RTL translation}
\label{sect.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)
% picture of sigma mapping memory to memory
TODO
\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}

\section{The RTL to ERTL translation}
\label{sect.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 &                         &                                                                                               &                         & FINISH ME
\end{diagram}
\end{displaymath}

\section{The ERTL to LTL translation}
\label{sect.ertl.ltl.translation}

\section{The LTL to LIN translation}
\label{sect.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}


\section{The LIN to ASM and ASM to MCS-51 machine code translations}
\label{sect.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.

\end{document}