1 | \documentclass{llncs} |
---|
2 | |
---|
3 | \usepackage{amsmath} |
---|
4 | \usepackage[english]{babel} |
---|
5 | \usepackage[colorlinks]{hyperref} |
---|
6 | \usepackage[utf8x]{inputenc} |
---|
7 | \usepackage{listings} |
---|
8 | |
---|
9 | \newlength{\mylength} |
---|
10 | \newenvironment{frametxt}% |
---|
11 | {\setlength{\fboxsep}{5pt} |
---|
12 | \setlength{\mylength}{\linewidth}% |
---|
13 | \addtolength{\mylength}{-2\fboxsep}% |
---|
14 | \addtolength{\mylength}{-2\fboxrule}% |
---|
15 | \Sbox |
---|
16 | \minipage{\mylength}% |
---|
17 | \setlength{\abovedisplayskip}{0pt}% |
---|
18 | \setlength{\belowdisplayskip}{0pt}% |
---|
19 | }% |
---|
20 | {\endminipage\endSbox |
---|
21 | \[\fbox{\TheSbox}\]} |
---|
22 | |
---|
23 | %\lstdefinelanguage{matita-ocaml} |
---|
24 | % {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to}, |
---|
25 | % morekeywords={[2]whd,normalize,elim,cases,destruct}, |
---|
26 | % morekeywords={[3]type,of,val,assert,let,function}, |
---|
27 | % mathescape=true, |
---|
28 | % } |
---|
29 | %\lstset{language=matita-ocaml,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false, |
---|
30 | % keywordstyle=\bfseries, %\color{red}\bfseries, |
---|
31 | % keywordstyle=[2]\bfseries, %\color{blue}, |
---|
32 | % keywordstyle=[3]\bfseries, %\color{blue}\bfseries, |
---|
33 | %% commentstyle=\color{green}, |
---|
34 | %% stringstyle=\color{blue}, |
---|
35 | % showspaces=false,showstringspaces=false} |
---|
36 | %\DeclareUnicodeCharacter{8797}{:=} |
---|
37 | %\DeclareUnicodeCharacter{8797}{:=} |
---|
38 | %\DeclareUnicodeCharacter{10746}{++} |
---|
39 | %\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}} |
---|
40 | %\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} |
---|
41 | |
---|
42 | %\lstset{ |
---|
43 | % extendedchars=false, |
---|
44 | % inputencoding=utf8x, |
---|
45 | % tabsize=1 |
---|
46 | %} |
---|
47 | |
---|
48 | \renewcommand{\verb}{\lstinline} |
---|
49 | \def\lstlanguagefiles{lst-grafite.tex} |
---|
50 | \lstset{language=Grafite} |
---|
51 | |
---|
52 | \title{On the correctness of an assembler for the Intel MCS-51 microprocessor} |
---|
53 | \author{Jaap Boender \and Dominic P. Mulligan \and Claudio Sacerdoti Coen} |
---|
54 | \institute{Dipartimento di Scienze dell'Informazione, Universit\'a di Bologna} |
---|
55 | |
---|
56 | \bibliographystyle{splncs03} |
---|
57 | |
---|
58 | \begin{document} |
---|
59 | |
---|
60 | \maketitle |
---|
61 | |
---|
62 | \begin{abstract} |
---|
63 | We consider the formalisation of an assembler for the Intel MCS-51 8-bit microprocessor in the Matita proof assistant. |
---|
64 | This formalisation forms a major component of the EU-funded CerCo project, concering the construction and formalisation of a concrete complexity preserving compiler for a large subset of the C programming language. |
---|
65 | ... |
---|
66 | \end{abstract} |
---|
67 | |
---|
68 | % ---------------------------------------------------------------------------- % |
---|
69 | % SECTION % |
---|
70 | % ---------------------------------------------------------------------------- % |
---|
71 | \section{Introduction} |
---|
72 | \label{sect.introduction} |
---|
73 | |
---|
74 | We consider the formalisation of an assembler for the Intel MCS-51 8-bit microprocessor in the Matita proof assistant~\cite{asperti:user:2007}. |
---|
75 | This formalisation forms a major component of the EU-funded CerCo project~\cite{cerco:2011}, concering the construction and formalisation of a concrete complexity preserving compiler for a large subset of the C programming language. |
---|
76 | |
---|
77 | The MCS-51 dates from the early 1980s and commonly called the 8051/8052. |
---|
78 | Despite the microprocessor's age, derivatives are still widely manufactured by a number of semiconductor foundries. |
---|
79 | As a result the processor is widely used, especially in embedded systems development, where well-tested, cheap, predictable microprocessors find their niche. |
---|
80 | |
---|
81 | The MCS-51 has a relative paucity of features compared to its more modern brethren. |
---|
82 | In particular, the MCS-51 does not possess a cache or any instruction pipelining that would make predicting the concrete cost of executing a single instruction an involved process. |
---|
83 | Instead, each semiconductor foundry that produces an MCS-51 derivative is able to provide accurate timing information in clock cycles for each instruction in their derivative's instruction set. |
---|
84 | It is important to stress that this timing information, unlike in more sophisticated processors, is not an estimate, it is a definition. |
---|
85 | For the MCS-51, if a manufacturer states that a particular opcode takes three clock cycles to execute, then that opcode \emph{always} takes three clock cycles to execute. |
---|
86 | |
---|
87 | This predicability of timing information is especially attractive to the CerCo consortium. |
---|
88 | We are in the process of constructing a certified, concrete complexity compiler for a realistic processor, and not for building and formalising the worst case execution time (WCET) tools that would be necessary to achieve the same result with, for example, a modern ARM or PowerPC microprocessor. |
---|
89 | |
---|
90 | However, the MCS-51's paucity of features is a double edged sword. |
---|
91 | In particular, the MCS-51 features relatively miniscule memory spaces (including read-only code memory, stack and internal/external random access memory) by modern standards. |
---|
92 | As a result our compiler, to have any sort of hope of successfully compiling realistic C programs, ought to produce `tight' machine code. |
---|
93 | This is not simple. |
---|
94 | |
---|
95 | We here focus on a single issue in the MCS-51's instruction set: unconditional jumps. |
---|
96 | The MCS-51 features three conditional jump instructions: \texttt{LJMP} and \texttt{SJMP}---`long jump' and `short jump' respectively---and an 11-bit oddity of the MCS-51, \texttt{AJMP}, that the prototype CerCo compiler~\cite{cerco-report-code:2011} ignores for simplicity's sake.\footnote{Ignoring \texttt{AJMP} and its analogue \texttt{ACALL} is not idiosyncratic. The Small Device C Compiler (SDCC)~\cite{sdcc:2011}, the leading open source C compiler for the MCS-51, also seemingly does not produce \texttt{AJMP} and \texttt{ACALL} instructions. Their utility in a modern context remains unclear.} |
---|
97 | Each of these three instructions expects arguments in different sizes and behaves in different ways. |
---|
98 | \texttt{SJMP} may only perform a `local jump' whereas \texttt{LJMP} may jump to any address in the MCS-51's memory space. |
---|
99 | Consequently, the size of each opcode is different, and to squeeze as much code as possible into the MCS-51's limited code memory, the smallest possible opcode should be selected. |
---|
100 | |
---|
101 | The prototype CerCo C compiler does not attempt to select the smallest jump opcode in this manner, as this was thought to unneccessarily complicate the compilation chain. |
---|
102 | Instead, the compiler targets an assembly language, complete with pseudoinstructions including bespoke \texttt{Jmp} and \texttt{Call} instructions. |
---|
103 | Labels, conditional jumps to labels, a program preamble containing global data and a \texttt{MOV} instruction for moving this global data into the MCS-51's one 16-bit register also feature. |
---|
104 | This latter feature will ease any later consideration of separate compilation in the CerCo compiler. |
---|
105 | An assembler is used to expand pseudoinstructions into MCS-51 machine code. |
---|
106 | |
---|
107 | However, this assembly process is not trivial, for numerous reasons. |
---|
108 | For example, our conditional jumps to labels behave differently from their machine code counterparts. |
---|
109 | At the machine code level, conditional jumps may only jump to a relative offset, expressed in a byte, of the current program counter, limiting their range. |
---|
110 | However, at the assembly level, conditional jumps may jump to a label that appears anywhere in the program, significantly liberalising the use of conditional jumps and further simplifying the design of the CerCo compiler. |
---|
111 | |
---|
112 | Further, trying to na\"ively relate assembly programs with their machine code counterparts simply does not work. |
---|
113 | Machine code programs that fetch from code memory and programs that combine the program counter with constant shifts do not make sense at the assembly level. |
---|
114 | More generally, memory addresses can only be compared with other memory addresses. |
---|
115 | However, checking that memory addresses are only compared against each other at the assembly level is in fact undecidable. |
---|
116 | In short, the full preservation of the semantics of the two languages is impossible. |
---|
117 | |
---|
118 | Yet more complications are added by the peculiarities of the CerCo project itself. |
---|
119 | As mentioned, the CerCo consortium is in the business of constructing a verified compiler for the C programming language. |
---|
120 | However, unlike CompCert~\cite{compcert:2011,leroy:formal:2009,leroy:formally:2009}---which currently represents the state of the art for `industrial grade' verified compilers---CerCo considers not just the \emph{intensional correctness} of the compiler, but also its \emph{extensional correctness}. |
---|
121 | That is, CompCert focusses solely on the preservation of the \emph{meaning} of a program during the compilation process, guaranteeing that the program's meaning does not change as it is gradually transformed into assembly code. |
---|
122 | However in any realistic compiler (even the CompCert compiler!) there is no guarantee that the program's time properties are preserved during the compilation process; a compiler's `optimisations' could, in theory, even conspire to degrade the concrete complexity of certain classes of programs. |
---|
123 | CerCo aims to expand the current state of the art by producing a compiler where this temporal degradation is guaranteed not to happen. |
---|
124 | |
---|
125 | In order to achieve this CerCo imposes a cost model on programs, or more specifically, on simple blocks of instructions. |
---|
126 | This cost model is induced by the compilation process itself, and its non-compositional nature allows us to assign different costs to identical blocks of instructions depending on how they are compiled. |
---|
127 | In short, we aim to obtain a very precise costing for a program by embracing the compilation process, not ignoring it. |
---|
128 | This, however, complicates the proof of correctness for the compiler proper: for every translation pass from intermediate language to intermediate language, we must prove that not only has the meaning of a program been preserved, but also its complexity characteristics. |
---|
129 | This also applies for the translation from assembly language to machine code. |
---|
130 | |
---|
131 | How do we assign a cost to a pseudoinstruction? |
---|
132 | As mentioned, conditional jumps at the assembly level can jump to a label appearing anywhere in the program. |
---|
133 | However, at the machine code level, conditional jumps are limited to jumping `locally', using a measly byte offset. |
---|
134 | To translate a jump to a label, a single conditional jump pseudoinstruction may be translated into a block of three real instructions, as follows (here, \texttt{JZ} is `jump if accumulator is zero'): |
---|
135 | \begin{displaymath} |
---|
136 | \begin{array}{r@{\quad}l@{\;\;}l@{\qquad}c@{\qquad}l@{\;\;}l} |
---|
137 | & \mathtt{JZ} & label & & \mathtt{JZ} & \text{size of \texttt{SJMP} instruction} \\ |
---|
138 | & \ldots & & \text{translates to} & \mathtt{SJMP} & \text{size of \texttt{LJMP} instruction} \\ |
---|
139 | label: & \mathtt{MOV} & \mathtt{A}\;\;\mathtt{B} & \Longrightarrow & \mathtt{LJMP} & \text{address of \textit{label}} \\ |
---|
140 | & & & & \ldots & \\ |
---|
141 | & & & & \mathtt{MOV} & \mathtt{A}\;\;\mathtt{B} |
---|
142 | \end{array} |
---|
143 | \end{displaymath} |
---|
144 | In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}. |
---|
145 | Naturally, if \textit{label} is close enough, a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \textit{label} is not sufficiently local. |
---|
146 | This leaves the problem, addressed below, of calculating whether a label is indeed `close enough' for the simpler translation to be used. |
---|
147 | |
---|
148 | Crucially, the above translation demonstrates the difficulty in predicting how many clock cycles a pseudoinstruction will take to execute. |
---|
149 | A conditional jump may be mapped to a single machine instruction or a block of three. |
---|
150 | Perhaps more insidious, the number of cycles needed to execute the instructions in the two branches of a translated conditional jump may be different. |
---|
151 | Depending on the particular MCS-51 derivative at hand, an \texttt{SJMP} could in theory take a different number of clock cycles to execute than an \texttt{LJMP}. |
---|
152 | These issues must also be dealt with in order to prove that the translation pass preserves the concrete complexity of the code. |
---|
153 | |
---|
154 | The question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}? |
---|
155 | To understand why this problem is not trivial, consider the following snippet of assembly code: |
---|
156 | \begin{displaymath} |
---|
157 | \text{dpm: finish me} |
---|
158 | \end{displaymath} |
---|
159 | |
---|
160 | As our example shows, given an occurence $l$ of an \texttt{LJMP} instruction, it may be possible to shrink $l$ to an occurence of an \texttt{SJMP} providing we can shrink any \texttt{LJMP}s that exist between $l$ and its target location. |
---|
161 | However, shrinking these \texttt{LJMP}s may in turn depend on shrinking $l$ to an \texttt{SJMP}, as it is perfectly possible to jump backwards. |
---|
162 | In short, unless we can somehow break this loop of circularity, and similar knotty configurations of jumps, we are stuck with a suboptimal solution to the expanding jumps problem. |
---|
163 | |
---|
164 | How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way. |
---|
165 | We first attempted to synthesize a solution bottom up: starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion. |
---|
166 | Using this technique, solutions can fail to exist, and the proof quickly descends into a diabolical quagmire. |
---|
167 | |
---|
168 | Abandoning this attempt, we instead split the `policy'---the decision over how any particular jump should be expanded---from the implementation that actually expands assembly programs into machine code. |
---|
169 | Assuming the existence of a correct policy, we proved the implementation of the assembler correct. |
---|
170 | Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist. |
---|
171 | Policies do not exist in only a limited number of circumstances: namely, if a pseudoinstruction attempts to jump to a label that does not exist, or the program is too large to fit in code memory. |
---|
172 | The first case would constitute a serious compiler error, and hopefully certifying the rest of the compiler would rule this possibility out. |
---|
173 | The second case is unavoidable---certified compiler or not, trying to load a huge program into a small code memory will break \emph{something}. |
---|
174 | |
---|
175 | The rest of this paper is a detailed description of this proof. |
---|
176 | |
---|
177 | % ---------------------------------------------------------------------------- % |
---|
178 | % SECTION % |
---|
179 | % ---------------------------------------------------------------------------- % |
---|
180 | \subsection{Overview of the paper} |
---|
181 | \label{subsect.overview.of.the.paper} |
---|
182 | In Section~\ref{sect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader. |
---|
183 | In Section~\ref{sect.the.proof} we discuss the design and implementation of the proof proper. |
---|
184 | In Section~\ref{sect.conclusions} we conclude. |
---|
185 | |
---|
186 | % ---------------------------------------------------------------------------- % |
---|
187 | % SECTION % |
---|
188 | % ---------------------------------------------------------------------------- % |
---|
189 | \section{Matita} |
---|
190 | \label{sect.matita} |
---|
191 | |
---|
192 | |
---|
193 | % ---------------------------------------------------------------------------- % |
---|
194 | % SECTION % |
---|
195 | % ---------------------------------------------------------------------------- % |
---|
196 | \section{The proof} |
---|
197 | \label{sect.the.proof} |
---|
198 | |
---|
199 | \begin{itemize} |
---|
200 | \item use of dependent types to throw away wrong programs that would made |
---|
201 | the statement for completeness complex. E.g. misuse of addressing modes, |
---|
202 | jumps to non existent labels, etc. |
---|
203 | \item try to go for small reflection; avoid inductive predicates that require |
---|
204 | tactics (inversion, etc.) that do not work well with dependent types; small |
---|
205 | reflection usually does |
---|
206 | \item use coercions to simulate Russell; mix together the proof styles |
---|
207 | a la Russell (for situations with heavy dependent types) and the standard |
---|
208 | one |
---|
209 | \end{itemize} |
---|
210 | |
---|
211 | \begin{lstlisting} |
---|
212 | definition execute_1_pseudo_instruction: PseudoStatus → PseudoStatus |
---|
213 | \end{lstlisting} |
---|
214 | |
---|
215 | \begin{lstlisting} |
---|
216 | definition execute: nat → Status → Status |
---|
217 | \end{lstlisting} |
---|
218 | |
---|
219 | \begin{lstlisting} |
---|
220 | inductive jump_length: Type[0] ≝ |
---|
221 | | short_jump: jump_length |
---|
222 | | medium_jump: jump_length |
---|
223 | | long_jump: jump_length. |
---|
224 | |
---|
225 | definition jump_expansion_policy ≝ BitVectorTrie jump_length 16. |
---|
226 | \end{lstlisting} |
---|
227 | |
---|
228 | \begin{lstlisting} |
---|
229 | definition policy_ok := λpolicy.λp. sigma_safe policy p <> None .... |
---|
230 | \end{lstlisting} |
---|
231 | |
---|
232 | \begin{lstlisting} |
---|
233 | definition sigma: |
---|
234 | ∀p:pseudo_assembly_program. |
---|
235 | ∀policy. policy_ok policy p. Word → Word |
---|
236 | \end{lstlisting} |
---|
237 | |
---|
238 | \begin{lstlisting} |
---|
239 | axiom low_internal_ram_of_pseudo_low_internal_ram: |
---|
240 | ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. |
---|
241 | \end{lstlisting} |
---|
242 | |
---|
243 | CSC: no option using policy |
---|
244 | \begin{lstlisting} |
---|
245 | definition status_of_pseudo_status: |
---|
246 | internal_pseudo_address_map → PseudoStatus → option Status |
---|
247 | \end{lstlisting} |
---|
248 | |
---|
249 | \begin{lstlisting} |
---|
250 | definition next_internal_pseudo_address_map0: |
---|
251 | internal_pseudo_address_map → PseudoStatus → option internal_pseudo_address_map |
---|
252 | \end{lstlisting} |
---|
253 | |
---|
254 | CSC: no 2nd, 3rd options using policy |
---|
255 | \begin{lstlisting} |
---|
256 | ∀M,M',ps,s,s''. |
---|
257 | next_internal_pseudo_address_map M ps = Some ... M' → |
---|
258 | status_of_pseudo_status M ps = Some ... s → |
---|
259 | status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory ... ps)) ps) = Some ... s'' → |
---|
260 | ∃n. execute n s = s''. |
---|
261 | \end{lstlisting} |
---|
262 | |
---|
263 | CSC: no options using policy |
---|
264 | \begin{lstlisting} |
---|
265 | lemma fetch_assembly_pseudo2: |
---|
266 | ∀program,assembled,costs,labels. |
---|
267 | Some ... LANGLElabels,costsRANGLE = build_maps program → |
---|
268 | Some ... LANGLEassembled,costsRANGLE = assembly program → |
---|
269 | ∀ppc. |
---|
270 | let code_memory ≝ load_code_memory assembled in |
---|
271 | let preamble ≝ \fst program in |
---|
272 | let data_labels ≝ construct_datalabels preamble in |
---|
273 | let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in |
---|
274 | let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in |
---|
275 | let expansion ≝ jump_expansion ppc program in |
---|
276 | let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in |
---|
277 | ∃instructions. |
---|
278 | Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧ |
---|
279 | fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. |
---|
280 | \end{lstlisting} |
---|
281 | |
---|
282 | \begin{lstlisting} |
---|
283 | definition expand_pseudo_instruction: |
---|
284 | ∀lookup_labels.∀lookup_datalabels.∀pc.∀policy_decision. (sigma program ppc) expansion. pseudo_instruciton -> list instruction. |
---|
285 | \end{lstlisting} |
---|
286 | |
---|
287 | \begin{lstlisting} |
---|
288 | axiom assembly_ok_to_expand_pseudo_instruction_ok: |
---|
289 | ∀program,assembled,costs. |
---|
290 | Some ... LANGLEassembled,costsRANGLE = assembly program → |
---|
291 | ∀ppc. |
---|
292 | let code_memory ≝ load_code_memory assembled in |
---|
293 | let preamble ≝ \fst program in |
---|
294 | let data_labels ≝ construct_datalabels preamble in |
---|
295 | let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in |
---|
296 | let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in |
---|
297 | let expansion ≝ jump_expansion ppc program in |
---|
298 | let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in |
---|
299 | ∃instructions. |
---|
300 | Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi. |
---|
301 | \end{lstlisting} |
---|
302 | |
---|
303 | \begin{lstlisting} |
---|
304 | axiom assembly_ok: |
---|
305 | ∀program,assembled,costs,labels. |
---|
306 | Some ... LANGLElabels,costsRANGLE = build_maps program → |
---|
307 | Some ... LANGLEassembled,costsRANGLE = assembly program → |
---|
308 | let code_memory ≝ load_code_memory assembled in |
---|
309 | let preamble ≝ \fst program in |
---|
310 | let datalabels ≝ construct_datalabels preamble in |
---|
311 | let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in |
---|
312 | let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in |
---|
313 | ∀ppc,len,assembledi. |
---|
314 | let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in |
---|
315 | Some ... LANGLElen,assemblediRANGLE = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi → |
---|
316 | encoding_check code_memory (sigma program ppc) (bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len)) assembledi ∧ |
---|
317 | sigma program newppc = bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len). |
---|
318 | \end{lstlisting} |
---|
319 | |
---|
320 | \begin{lstlisting} |
---|
321 | lemma fetch_assembly_pseudo: |
---|
322 | ∀program,ppc,lookup_labels,lookup_datalabels. |
---|
323 | ∀pi,code_memory,len,assembled,instructions,pc. |
---|
324 | let expansion ≝ jump_expansion ppc program in |
---|
325 | Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi → |
---|
326 | Some ... LANGLElen,assembledRANGLE = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi → |
---|
327 | encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled → |
---|
328 | fetch_many code_memory (bitvector_of_nat ... (pc + len)) (bitvector_of_nat ... pc) instructions. |
---|
329 | \end{lstlisting} |
---|
330 | |
---|
331 | \begin{lstlisting} |
---|
332 | theorem fetch_assembly: |
---|
333 | ∀pc,i,code_memory,assembled. |
---|
334 | assembled = assembly1 i → |
---|
335 | let len ≝ length ... assembled in |
---|
336 | encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled → |
---|
337 | let fetched ≝ fetch code_memory (bitvector_of_nat ... pc) in |
---|
338 | let LANGLEinstr_pc, ticksRANGLE ≝ fetched in |
---|
339 | let LANGLEinstr,pc'RANGLE ≝ instr_pc in |
---|
340 | (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv ... pc' (bitvector_of_nat ... (pc + len))) = true. |
---|
341 | \end{lstlisting} |
---|
342 | |
---|
343 | % ---------------------------------------------------------------------------- % |
---|
344 | % SECTION % |
---|
345 | % ---------------------------------------------------------------------------- % |
---|
346 | \section{Conclusions} |
---|
347 | \label{sect.conclusions} |
---|
348 | |
---|
349 | \subsection{Use of dependent types and Russell} |
---|
350 | \label{subsect.use.of.dependent.types.and.Russell} |
---|
351 | |
---|
352 | Our formalisation makes sparing use of dependent types. |
---|
353 | In certain datastructures, such as tries and vectors, they are used to guarantee invariants. |
---|
354 | However, we have currently shyed away from making extensive use of dependent types and inductive predicates in the proof of correctness for the assembler itself. |
---|
355 | This is because complex dependent types and inductive predicates tend not to co\"operate particularly well with tactics such as inversion. |
---|
356 | |
---|
357 | However, there are certain cases where the use of dependent types is unavoidable. |
---|
358 | For instance, when proving that the \texttt{build\_maps} function is correct, a function that collates the cost and data labels of an assembly program into map datastructures. |
---|
359 | In cases such as these we make use of Matita's implementation of Russell~\cite{}. |
---|
360 | |
---|
361 | \subsection{Related work} |
---|
362 | \label{subsect.related.work} |
---|
363 | |
---|
364 | \bibliography{cpp-2011.bib} |
---|
365 | |
---|
366 | \end{document} |
---|