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

Last change on this file since 1716 was 1716, checked in by mulligan, 8 years ago

proof outline, as requested by referees, being typed up in latex

File size: 3.0 KB
Line 
1\documentclass[a4paper, 10pt]{article}
2
3\usepackage{a4wide}
4\usepackage{amsfonts}
5\usepackage{amsmath}
6\usepackage{amssymb}
7\usepackage[english]{babel}
8\usepackage[colorlinks]{hyperref}
9\usepackage{microtype}
10
11\title{Proof outline for the correctness of the CerCo compiler}
12\date{\today}
13\author{The CerCo team}
14
15\begin{document}
16
17\maketitle
18
19\section{Introduction}
20\label{sect.introduction}
21
22\section{The RTLabs to RTL translation}
23\label{sect.rtlabs.rtl.translation}
24
25% dpm: type system and casting load (???)
26We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model:
27
28\begin{displaymath}
29\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
30\end{displaymath}
31
32We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}.
33
34\begin{displaymath}
35\mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha)
36\end{displaymath}
37
38where
39
40\begin{displaymath}
41\mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID}
42\end{displaymath}
43
44\begin{displaymath}
45\mathtt{BEMem} = \mathtt{Mem} \mathtt{Value}
46\end{displaymath}
47
48\begin{displaymath}
49\mathtt{Address} = \mathtt{BEValue} \times  \mathtt{BEValue} \\
50\end{displaymath}
51
52\begin{displaymath}
53\mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null})
54\end{displaymath}
55
56\begin{center}
57\begin{picture}(2, 2)
58% picture of sigma mapping memory to memory
59TODO
60\end{picture}
61\end{center}
62
63\begin{displaymath}
64\mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i
65\end{displaymath}
66
67\begin{displaymath}
68\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
69\end{displaymath}
70
71\begin{displaymath}
72\begin{array}{rll}
73\mathtt{State} & ::=  & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\
74               & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\
75               & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem}
76\end{array}
77\end{displaymath}
78
79\begin{displaymath}
80\mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS}
81\end{displaymath}
82
83\begin{displaymath}
84\mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State}
85\end{displaymath}
86
87\section{The RTL to ERTL translation}
88\label{sect.rtl.ertl.translation}
89
90\section{The ERTL to LTL translation}
91\label{sect.ertl.ltl.translation}
92
93\section{The LTL to LIN translation}
94\label{sect.ltl.lin.translation}
95
96\section{The LIN to ASM translation}
97\label{sect.lin.asm.translation}
98
99\section{The ASM to MCS-51 machine code translation}
100\label{sect.asm.mcs-51.machine.code.translation}
101
102\end{document}
Note: See TracBrowser for help on using the repository browser.