Changeset 3555 for Papers


Ignore:
Timestamp:
Apr 24, 2015, 1:04:26 PM (4 years ago)
Author:
mulligan
Message:

dominic, jaap taking another look at the paper

Location:
Papers/jar-assembler-2015
Files:
2 deleted
2 copied
1 moved

Legend:

Unmodified
Added
Removed
  • Papers/jar-assembler-2015/boender-jar-2015.tex

    r3554 r3555  
    11\documentclass[a4paper]{article}
     2
     3\usepackage{a4wide}
    24\usepackage{algpseudocode}
    35\usepackage{alltt}
     
    1214\usepackage{subcaption}
    1315
    14 \usepackage{kpfonts}
     16%\usepackage{kpfonts}
    1517\usepackage[T1]{fontenc}
    16 \usepackage[ttdefault=true]{AnonymousPro}
     18%\usepackage[ttdefault=true]{AnonymousPro}
    1719
    1820\newcommand{\All}[1]{\forall{#1}.\;}
     
    5355All 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 complexity-preserving compiler for a subset of the C programming language.
    5456
    55 Our optimisations complicate the proof of correctness of the assembler proper and therefore we employ the use of `policies', separating out decisions of how a pseudoinstruction should be expanded from the expansion process itself, simplifying our proofs.
     57Our 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.
    5658Our proof strategy also tracks `good' addresses, and only programs that use good addresses have their semantics preserved under assembly.
    5759This tracking offers increased flexibility over the traditional approach---where addresses are kept abstract and immutable---as we may experiment with some manipulations of machine addresses.
     
    6264\tableofcontents
    6365
    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 FET-Open 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 FET-Open grant number 243881.}
    6567
    6668\newpage
     
    7274\label{sect.introduction}
    7375
     76We present an overview of work formalising and proving correct an optimising assembler for a typical embedded microcontroller.
     77Though the work described herein is specialised to the 8-bit Intel MCS-51 series, we believe the design decisions and techniques developed for our proof of correctness are of general interest.
     78
    7479% Everybody
    7580
     
    8085\label{subsect.matita}
    8186
    82 In this Subsection we provide an overview of Matita, the host system for all proofs reported in this paper.
    83 
    8487Matita 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 tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order: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}.
     88The system features a full spectrum of dependent types and (co)inductive families, a system of coercions, a tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order:2007}, all of which we exploit in the formalisation described herein.
     89
     90Matita's syntax is similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML.
     91The type theory that Matita implements is broadly akin to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}.
    8892Nevertheless, we provide a brief explanation of the main syntactic and type-theoretic features of Matita that will be needed to follow the body of the paper:
    8993\begin{itemize}
    9094\item
    91 Non-recursive functions and definitions are introduced via the \texttt{definition} keyword whilst recursive functions are introduced with \texttt{let rec}.
     95Non-recursive functions and definitions are introduced via the \texttt{definition} keyword.
     96Recursive functions are introduced with \texttt{let rec}.
    9297Mutually recursive functions are separated via the \texttt{and} keyword.
    93 Matita checks that all recursive functions are terminating before being admitted.
     98Matita's termination checker ensures that all recursive functions are terminating before being admitted to maintain soundness of the system's logic.
    9499\item
    95100Matita has an infinite hierarchy of type universes.
     
    99104\item
    100105Matita's type theory plays host to a rich and expressive higher-order logic.
    101 Constant \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.
     106Constants \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.
    102107Two inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively.
     108
    103109As 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).
    104110We 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.
     111We use $\langle M,N \rangle$ for the pairing of $M$ and $N$.
     112\item
     113Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated by a bar.
    107114Mutually inductive data family declarations are separated via \texttt{with}.
    108 In the following declaration
     115In the following declaration:
    109116\begin{lstlisting}
    110117inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$
    111118\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 strictly-positive types before admitting an inductive family.
     119We 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}.
     120Matita's positivity checker ensures that constructors have strictly-positive types before admitting an inductive family to maintain soundness of the system's logic.
    114121\item
    115122Records are introduced with the \texttt{record} keyword.
     
    123130  | mk_R : nat -> R.
    124131\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.
    127132A record field's type may depend on fields declared earlier in the record.
    128133
    129 Record fields may be marked as coercions.
     134Records may be decomposed with projections.
     135Projections, one for each of field of a record, are registered in the global context.
     136In 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
     138Record fields may also be marked as coercions.
    130139In the following example
    131140\begin{lstlisting}
     
    136145}
    137146\end{lstlisting}
    138 the field \texttt{Carrier} is declared to be a coercion with `\texttt{:>}' with the effect that the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita.
     147the 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.
    139148Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set.
    140149\item
     
    145154Three consecutive dots, \texttt{$\ldots$}, denote multiple terms or types that have been omitted.
    146155\item
    147 Pattern matching is carried out with a \texttt{match} expression.
    148 We may sometimes fully annotate a \texttt{match} expression with its return type.
     156Data may be decomposed by pattern matching with a \texttt{match} expression.
     157We may fully annotate a \texttt{match} expression with its return type.
    149158This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions.
    150159In the following
     
    160169\item
    161170Matita 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).
     171It 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$.
    163172The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$.
    164173When 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 sub-terms.
     
    213222
    214223% DPM and CSC
    215 
     224One of the central data types in our formalisation is the \texttt{BitVector}.
     225\texttt{BitVector}s are fixed-length lists of bits (implemented as booleans) used to encode words and bytes:
    216226\begin{lstlisting}
    217227definition BitVector := $\lambda$n: nat. Vector bool n.
    218228\end{lstlisting}
    219 
     229Arithmetic in our formalisation is carried out on \texttt{BitVector} values.
     230
     231An MCS-51 byte is eight bits wide and an MCS-51 word is a double byte, or sixteen bits wide.
     232Some MCS-51 instructions require four, seven and eleven bit wide sub-bytes and sub-words respectively.
     233We capture these notions as definitions:
    220234\begin{lstlisting}
    221235definition Nibble := BitVector 4.
     
    225239definition Word11 := BitVector 11.
    226240\end{lstlisting}
    227 
     241A central design decision in our formalisation is the choice of how to encode memory.
     242The MCS-51 has various memory spaces and registers that can be addressed with bytes and words.
    228243\begin{lstlisting}
    229244inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] :=
     
    326341\newpage
    327342
    328 \bibliography{boender-jar-2014}
     343\bibliography{boender-jar-2015}
    329344
    330345\end{document}
Note: See TracChangeset for help on using the changeset viewer.