Changeset 3555
 Timestamp:
 Apr 24, 2015, 1:04:26 PM (5 years ago)
 Location:
 Papers/jarassembler2015
 Files:

 2 deleted
 2 copied
 1 moved
Legend:
 Unmodified
 Added
 Removed

Papers/jarassembler2015/boenderjar2015.tex
r3554 r3555 1 1 \documentclass[a4paper]{article} 2 3 \usepackage{a4wide} 2 4 \usepackage{algpseudocode} 3 5 \usepackage{alltt} … … 12 14 \usepackage{subcaption} 13 15 14 \usepackage{kpfonts}16 %\usepackage{kpfonts} 15 17 \usepackage[T1]{fontenc} 16 \usepackage[ttdefault=true]{AnonymousPro}18 %\usepackage[ttdefault=true]{AnonymousPro} 17 19 18 20 \newcommand{\All}[1]{\forall{#1}.\;} … … 53 55 All proofs are checked by the Matita theorem prover, and the work forms a major component of the Certified Complexity (`CerCo') project, aiming to produce a verified concrete complexitypreserving compiler for a subset of the C programming language. 54 56 55 Our optimisations complicate the proof of correctness of the assembler proper and therefore we employ the use of `policies', separating out decisionsof how a pseudoinstruction should be expanded from the expansion process itself, simplifying our proofs.57 Our optimisations complicate the proof of correctness of the assembler proper and therefore we employ the use of `policies', separating out the decision of how a pseudoinstruction should be expanded from the expansion process itself, simplifying our proofs. 56 58 Our proof strategy also tracks `good' addresses, and only programs that use good addresses have their semantics preserved under assembly. 57 59 This tracking offers increased flexibility over the traditional approachwhere addresses are kept abstract and immutableas we may experiment with some manipulations of machine addresses. … … 62 64 \tableofcontents 63 65 64 \blfootnote{Research supported by the CerCo project, within the Future and Emerging Technologies (FET) programme of the Seventh Framework Programme for Research of the European Commission, under FETOpen grant number 243881 }66 \blfootnote{Research supported by the CerCo project, within the Future and Emerging Technologies (FET) programme of the Seventh Framework Programme for Research of the European Commission, under FETOpen grant number 243881.} 65 67 66 68 \newpage … … 72 74 \label{sect.introduction} 73 75 76 We present an overview of work formalising and proving correct an optimising assembler for a typical embedded microcontroller. 77 Though the work described herein is specialised to the 8bit Intel MCS51 series, we believe the design decisions and techniques developed for our proof of correctness are of general interest. 78 74 79 % Everybody 75 80 … … 80 85 \label{subsect.matita} 81 86 82 In this Subsection we provide an overview of Matita, the host system for all proofs reported in this paper.83 84 87 Matita is a theorem prover based on a variant of the Calculus of Coinductive Constructions~\cite{asperti:user:2007}. 85 The system features a full spectrum of dependent types and (co)inductive families, a sophisticated system of uniform coercions, a tacticdriven proof construction engine~\cite{sacerdoticoen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higherorder:2007} all of which we exploit in the formalisation described herein. 86 87 Matita's syntax is largely similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML, and the type theory that Matita implements is very similar to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}. 88 The system features a full spectrum of dependent types and (co)inductive families, a system of coercions, a tacticdriven proof construction engine~\cite{sacerdoticoen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higherorder:2007}, all of which we exploit in the formalisation described herein. 89 90 Matita's syntax is similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML. 91 The type theory that Matita implements is broadly akin to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}. 88 92 Nevertheless, we provide a brief explanation of the main syntactic and typetheoretic features of Matita that will be needed to follow the body of the paper: 89 93 \begin{itemize} 90 94 \item 91 Nonrecursive functions and definitions are introduced via the \texttt{definition} keyword whilst recursive functions are introduced with \texttt{let rec}. 95 Nonrecursive functions and definitions are introduced via the \texttt{definition} keyword. 96 Recursive functions are introduced with \texttt{let rec}. 92 97 Mutually recursive functions are separated via the \texttt{and} keyword. 93 Matita checks that all recursive functions are terminating before being admitted.98 Matita's termination checker ensures that all recursive functions are terminating before being admitted to maintain soundness of the system's logic. 94 99 \item 95 100 Matita has an infinite hierarchy of type universes. … … 99 104 \item 100 105 Matita's type theory plays host to a rich and expressive higherorder logic. 101 Constant \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.106 Constants \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively. 102 107 Two inductive families in \texttt{Prop} encode conjunction and disjunction$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively. 108 103 109 As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$type). 104 110 We write $\All{x : \phi}\psi$ for the dependent function space, and abbreviate this as $\phi \rightarrow \psi$ when $x \not\in fv(\psi)$ as usual. 105 \item 106 Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated with a bar. 111 We use $\langle M,N \rangle$ for the pairing of $M$ and $N$. 112 \item 113 Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated by a bar. 107 114 Mutually inductive data family declarations are separated via \texttt{with}. 108 In the following declaration 115 In the following declaration: 109 116 \begin{lstlisting} 110 117 inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$ 111 118 \end{lstlisting} 112 we call $P_i$ for $0 \leq i \leq n$ the \deffont{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \deffont{indices} of \texttt{I}.113 Matita checks that constructors have strictlypositive types before admitting an inductive family.119 We call $P_i$ for $0 \leq i \leq n$ the \deffont{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \deffont{indices} of \texttt{I}. 120 Matita's positivity checker ensures that constructors have strictlypositive types before admitting an inductive family to maintain soundness of the system's logic. 114 121 \item 115 122 Records are introduced with the \texttt{record} keyword. … … 123 130  mk_R : nat > R. 124 131 \end{lstlisting} 125 The declaration of a record \texttt{R} causes a \deffont{constructor} function \texttt{mk\_R} to be entered into the global context as a side effect.126 \deffont{Projections}, one for each of the record's fields, are also registered in the global context, and in the example record above \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection.127 132 A record field's type may depend on fields declared earlier in the record. 128 133 129 Record fields may be marked as coercions. 134 Records may be decomposed with projections. 135 Projections, one for each of field of a record, are registered in the global context. 136 In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection and $mk\_R$ of type $nat \rightarrow R$ is registered as a constructor. 137 138 Record fields may also be marked as coercions. 130 139 In the following example 131 140 \begin{lstlisting} … … 136 145 } 137 146 \end{lstlisting} 138 the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}' with the effectthat the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita.147 the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}'.with the operational effect being that the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita. 139 148 Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set. 140 149 \item … … 145 154 Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted. 146 155 \item 147 Pattern matching is carried outwith a \texttt{match} expression.148 We may sometimesfully annotate a \texttt{match} expression with its return type.156 Data may be decomposed by pattern matching with a \texttt{match} expression. 157 We may fully annotate a \texttt{match} expression with its return type. 149 158 This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions. 150 159 In the following … … 160 169 \item 161 170 Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions). 162 It is possible to define a uniform coercion $\lam{x}\langle x, ?\rangle$ from every type $T$ to the dependent product $\Sigma{x : T}. P x$ (here $\langle \_,\_ \rangle$ is Matita's sugared syntax for pairs).171 It is possible to define a uniform coercion $\lam{x}\langle x, ?\rangle$ from every type $T$ to the dependent product $\Sigma{x : T}. P x$. 163 172 The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$. 164 173 When a coercion is to be applied to a complex term (for example, a $\lambda$abstraction, a local definition, or a case analysis), the system automatically propagates the coercion to the subterms. … … 213 222 214 223 % DPM and CSC 215 224 One of the central data types in our formalisation is the \texttt{BitVector}. 225 \texttt{BitVector}s are fixedlength lists of bits (implemented as booleans) used to encode words and bytes: 216 226 \begin{lstlisting} 217 227 definition BitVector := $\lambda$n: nat. Vector bool n. 218 228 \end{lstlisting} 219 229 Arithmetic in our formalisation is carried out on \texttt{BitVector} values. 230 231 An MCS51 byte is eight bits wide and an MCS51 word is a double byte, or sixteen bits wide. 232 Some MCS51 instructions require four, seven and eleven bit wide subbytes and subwords respectively. 233 We capture these notions as definitions: 220 234 \begin{lstlisting} 221 235 definition Nibble := BitVector 4. … … 225 239 definition Word11 := BitVector 11. 226 240 \end{lstlisting} 227 241 A central design decision in our formalisation is the choice of how to encode memory. 242 The MCS51 has various memory spaces and registers that can be addressed with bytes and words. 228 243 \begin{lstlisting} 229 244 inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] := … … 326 341 \newpage 327 342 328 \bibliography{boenderjar201 4}343 \bibliography{boenderjar2015} 329 344 330 345 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.