Changeset 495 for Deliverables/D4.1

Feb 11, 2011, 3:16:15 PM (11 years ago)

more added

1 edited


  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r494 r495  
     15  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
     16   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
     17   morekeywords={[3]type,of},
     18   mathescape=true,
     19  }
     21        keywordstyle=\color{red}\bfseries,
     22        keywordstyle=[2]\color{blue},
     23        keywordstyle=[3]\color{blue}\bfseries,
     24        commentstyle=\color{green},
     25        stringstyle=\color{blue},
     26        showspaces=false,showstringspaces=false}
    634\author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
    17 We summary the recent encoding of an executable formal model of the 8051/8052 microprocessor within Matita's internal logic.
     45We summarise our formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.
     46The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
     48We proceeded in two stages, first implementing in O'Caml a prototype emulator, where bugs could be `ironed out' quickly.
     49We then ported our O'Caml emulator to Matita's internal language.
     50Though mostly straight-forward, this porting presented multiple problems.
     51Of particular interest is how we handle the extreme non-orthoganality of the MSC-51's instruction set.
     52In O'Caml, this was handled through heavy use of polymorphic variants.
     53In Matita, we achieve the same effect through a novel use of dependent types.
     55Both the O'Caml and Matita emulators are `executable'.
     56Assembly programs may be animated within Matita, producing a trace of instructions executed.
     58Our formalisation is a major component of the ongoing EU-funded CerCo project.
    125166% SECTION                                                                      %
    127 \section{Development strategy}
    128 \label{sect.development.strategy}
     168\section{From O'Caml prototype to Matita formalisation}
     171Our implementation followed a two-layered approach.
     173\paragraph{O'Caml prototype}
     174Our implementation began with an emulator written in O'Caml.
     175This served the purpose of allowing us to `iron out' any bugs in the design of the emulator within a more permissive language.
     178\paragraph{Matita formalisation}
     198We provide an inductive data type representing all possible addressing modes of 8051 assembly.
     199This is the type that functions will pattern match against.
     203ninductive addressing_mode: Type[0] ≝
     204  DIRECT: Byte $\rightarrow$ addressing_mode
     205| INDIRECT: Bit $\rightarrow$ addressing_mode
     209However, we also wish to express in the type of our functions the \emph{impossibility} of pattern matching against certain constructors.
     210In order to do this, we introduce an inductive type of addressing mode `tags'.
     211The constructors of \texttt{addressing\_mode\_tag} are in one-one correspondence with the constructors of \texttt{addressing\_mode}:
     214ninductive addressing_mode_tag : Type[0] ≝
     215  direct: addressing_mode_tag
     216| indirect: addressing_mode_tag
     220We then provide a function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag}, as follows:
     223nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
     224  match d with
     225   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     226   | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     230We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
     233nlet rec is_in (n: Nat) (l: Vector addressing_mode_tag n) (A:addressing_mode) on l ≝
     234 match l return $\lambda$m.$\lambda$_ :Vector addressing_mode_tag m.Bool with
     235  [ VEmpty $\Rightarrow$ false
     236  | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$
     237     is_a he A $\vee$ is_in ? tl A ].
     240Here \texttt{VEmpty} and \texttt{VCons} are the two constructors of the \texttt{Vector} data type, and $\mathtt{\vee}$ is inclusive disjunction on Booleans.
     243nrecord subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
     245  subaddressing_modeel :> addressing_mode;
     246  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
     250We can now provide an inductive type of preinstructions with precise typings:
     253ninductive preinstruction (A: Type[0]): Type[0] ≝
     254   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
     255 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
     259Here $\llbracket - \rrbracket$ is syntax denoting a vector.
     260We see that the constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), and the second being one of a register, direct, indirect or data addressing mode.
     262The final, missing component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively.
     263The previous machinery allows us to state in the type of a function what addressing modes that function expects.
     264For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
     267ndefinition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
     268  $\lambda$s, v, a.
     269   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
     270     [ DPTR $\Rightarrow$ $\lambda$_: True.
     271       let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
     272       let status := set_8051_sfr s SFR_DPH bu in
     273       let status := set_8051_sfr status SFR_DPL bl in
     274         status
     275     | _ $\Rightarrow$ $\lambda$_: False.
     276       match K in False with
     277       [
     278       ]
     279     ] (subaddressing_modein $\ldots$ a).
     282All other cases are discharged by the catch-all at the bottom of the match expression.
     283Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
    149286% SECTION                                                                      %
Note: See TracChangeset for help on using the changeset viewer.