# Changeset 819

Ignore:
Timestamp:
May 19, 2011, 4:45:58 PM (8 years ago)
Message:

Final changes. Under 8 pages.

Location:
Deliverables/D4.1/ITP-Paper
Files:
2 edited

### Legend:

Unmodified
 r817 author = {Jun Yan and Wei Zhang}, title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches}, booktitle = {Proceedings of the $\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications}, booktitle = {$\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications}, pages = {80--89}, year = {2008} author = {Robert Atkey}, title = {{CoqJVM}: An executable specification of the {Java Virtual Machine} using dependent types}, booktitle = {Proceedings of the Conference of the {TYPES} Project}, booktitle = {Conference of the {TYPES} Project}, pages = {18--32}, year = {2007} title = {Designing a {CPU} model: from a pseudo-formal document to fast code}, author = {Fr\'ed\'eric Blanqui and Claude Helmstetter and Vania Joloboff and Jean-Fran\c{c}ois Monin and Xiaomu Shi}, booktitle = {Proceedings of the $\mathrm{3^{rd}}$ Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools}, booktitle = {$\mathrm{3^{rd}}$ Workshop on Rapid Simulation and Performance Evaluation: Methods and Tools}, year = {2010} } author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy}, title = {Formal Verification of a {C} Compiler Front-End}, booktitle = {Proceedings of the International Symposium on Formal Methods}, booktitle = {International Symposium on Formal Methods}, pages = {460--475}, year = {2006} author = {Adam Chlipala}, title = {A verified compiler for an impure functional language}, booktitle = {Proceedings of the $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages}, booktitle = {$\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages}, pages = {93--106}, year = {2010} author = {Anthony Fox and Magnus O. Myreen}, title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture}, booktitle = {Proceedings of the $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving}, booktitle = {$\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving}, pages = {243--258}, year = {2010} author = {Daan Leijen and Erik Meijer}, title = {Domain specific embedded compilers}, booktitle = {Proceedings of the $\mathrm{2^{nd}}$ Conference on Domain Specific Languages}, booktitle = {$\mathrm{2^{nd}}$ Conference on Domain Specific Languages}, pages = {109--122}, year = {1999} author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave}, title = {The semantics of {x86-CC} multiprocessor machine code}, booktitle = {Proceedings of the $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages}, booktitle = {$\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages}, pages = {379--391}, year = {2009} author = {Matthieu Sozeau}, title = {Subset coercions in {Coq}}, booktitle = {Proceedings of the Conference of the {TYPES} Project}, booktitle = {Conference of the {TYPES} Project}, pages = {237--252}, year = {2006} author = {Hongwei Xi and Chiyan Chen and Gang Chen}, title = {Guarded recursive datatype constructors}, booktitle = {Proceedings of the $\mathrm{30^{th}}$ Annual Symposium on Principles of Programming Languages}, booktitle = {$\mathrm{30^{th}}$ Annual Symposium on Principles of Programming Languages}, pages = {224--235}, year = {2003} @misc { cerco-code:2011, title = {{CerCo Deliverable D4.1}: Matita and O'Caml code}, howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1_Code.tar.gz}}, { cerco-report-code:2011, title = {{CerCo Deliverable D4.1}: executable formal semantics of machine code}, howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf} and \url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1_Code.tar.gz}}, year = {2011}, key = {{CerCo-code}} } @misc { cerco-report:2011, title = {{CerCo Deliverable D4.1}:: executable formal semantics of machine code}, howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf}}, year = {2011}, key = {{CerCo-report}} key = {{CerCo-report-code}} } @misc { sdcc:2010, title = {Small Device {C} Compiler {(SDCC)} 3.0.0}, title = {Small Device {C} Compiler 3.0.0}, howpublished = {\url{http://sdcc.sourceforge.net/}}, year = {2010},
 r817 \documentclass[10pt, final, conference]{IEEEtran} \documentclass[10pt, final, conference, letter]{IEEEtran} \usepackage{amsfonts} number: 243881} \bibliographystyle{plain} \bibliographystyle{IEEEtran} \begin{document} However, the Matita emulator is intended to be used as a target for a certified, complexity preserving C compiler, as part of the EU-funded CerCo project. As a result, not all features of the MCS-51 are formalised in the Matita emulator. %The formalisation proceeded in two stages, first implementing an O'Caml prototype, for quickly ironing out' bugs, and then porting the O'Caml emulator to Matita. %Though mostly straight-forward, this porting presented multiple problems. %Of particular interest is how the unorthoganality of the MSC-51's instruction set is handled. %In O'Caml, this was handled with polymorphic variants. %In Matita, we achieved the same effect with a non-standard use of dependent types. Both the O'Caml and Matita emulators are executable'. Assembly programs may be animated within Matita, producing a trace of instructions executed. The majority of programs are written in high level languages and then compiled into low level ones. Specifications are therefore also given at a high level and correctness can be proved by reasoning on the program's source code. The code that is actually run, however, is not the high level source code that we reason on, but low level code generated by the compiler. The code that is actually run is not the high level source code that we reason on, but low level code generated by the compiler. A few questions now arise: \begin{itemize*} To what extent can you trust your compiler in preserving those properties? \end{itemize*} These questions, and others like them, motivate a current hot topic' in computer science research: \emph{compiler verification} (for instance~\cite{chlipala:verified:2010,leroy:formal:2009}, and many others). These and other questions motivate a current hot topic' in computer science research: \emph{compiler verification} (e.g.~\cite{chlipala:verified:2010,leroy:formal:2009}, and so on). So far, the field has only been focused on the first and last questions. Much attention has been placed on verifying compiler correctness with respect to extensional properties of programs. A user can certify that deadlines' are met whilst wringing as many clock cycles from the processor---using a cost model that does not over-estimate---as possible. We also see our approach as being relevant to compiler verification (and construction). \emph{An optimisation specified only extensionally is only half specified}. Though the optimisation may preserve the denotational semantics of a program, there is no guarantee that intensional properties of the program improve. Our approach is also relevant to compiler verification and construction. \emph{An optimisation specified only extensionally is only half specified}; the optimisation may preserve the denotational semantics of a program, but there is no guarantee that intensional properties of the program improve. Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints. A compiler could reject a source program targetting an embedded system when the size of the compiled code exceeds the available ROM size. Preservation of a program's semantics may only be required for those programs that do not exhaust the stack or heap. The statement of completeness of the compiler must therefore take into account a realistic cost model. The statement of completeness of the compiler must take into account a realistic cost model. With the CerCo methodology, we assume we can assign to object code exact and realistic costs for sequential blocks of instructions. Bit memory, followed by a small amount of stack space, resides in the memory space immediately following the register banks. What remains of IRAM may be treated as general purpose memory. A schematic view of IRAM layout is also provided in Figure~\ref{fig.memory.layout}. A schematic view of IRAM is also provided in Figure~\ref{fig.memory.layout}. External RAM (XRAM), limited to a maximum size of 64 kilobytes, is optional, and may be provided on or off chip, depending on the vendor. Two 8-bit general purpose accumulators, A and B, are provided. Communication with the device is handled by an inbuilt UART serial port and controller. Communication with the device is handled by a UART serial port and controller. This can operate in numerous modes. Serial baud rate is determined by one of two 16-bit timers included with the 8051, which can be set to multiple modes of operation. We box Matita code to distinguish it from O'Caml code. In Matita, \texttt{?}' or \texttt{$\ldots$}' denote arguments to be inferred automatically. A full account of the formalisation can be found in~\cite{cerco-report:2011}. All source code is available from the CerCo project website~\cite{cerco-code:2011}. In Matita \texttt{$?$}' and  \texttt{$\ldots$}' are arguments to be inferred automatically. A full account of the formalisation can be found in~\cite{cerco-report-code:2011}. All source code is available from the CerCo project website~\cite{cerco-report-code:2011}. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | VCons: $\forall$n: nat. A $\rightarrow$ Vector A n $\rightarrow$ Vector A (S n). \end{lstlisting} We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}. \texttt{BitVector} is a specialization of \texttt{Vector} to \texttt{bool}. We may use Matita's type system to provide precise typings for functions that are polymorphic in the size without code duplication: \begin{lstlisting}[frame=single] let rec split (A: Type[0]) (m,n: nat) on m: Vector A (m + n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ... Vector A (m+n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ... \end{lstlisting} Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$: \begin{lstlisting}[frame=single] inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝ inductive BitVectorTrie(A: Type[0]):nat $\rightarrow$ Type[0] := Leaf: A $\rightarrow$ BitVectorTrie A 0 | Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ Performing a lookup in memory is now straight-forward. The only subtlety over normal trie lookup is how we handle \texttt{Stub}. We traverse a path, and upon encountering \texttt{Stub}, we return a default value\footnote{All manufacturer data sheets that we consulted were silent on the subject of what should be returned if we attempt to access uninitialized memory.  We defaulted to simply returning zero, though our \texttt{lookup} function is parametric in this choice.  We do not believe that this is an outrageous decision, as SDCC for instance generates code which first zeroes out' all memory in a preamble before executing the program proper.  This is in line with the C standard, which guarantees that all global variables will be zero initialized piecewise.}. \texttt{BitVectorTrie} and \texttt{Vector} datastructures, and related functions, can be used in the formalising other microprocessors. We traverse a path, and upon encountering \texttt{Stub}, we return a default value. All manufacturer data sheets that we consulted were silent on the subject of what should be returned if we attempt to access uninitialized memory. We defaulted to simply returning zero, though our \texttt{lookup} function is parametric in this choice. We believe that this is reasonable, as SDCC for instance generates code which first zeroes' memory in a preamble before executing the program proper. This is in line with the C standard, which guarantees that all global variables will be zero initialized piecewise. \texttt{BitVectorTrie} and \texttt{Vector}, and related functions, can be used in the formalisation of other microprocessors. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \label{subsect.anatomy.matita.emulator} The internal state of the Matita emulator is represented as a record: \begin{lstlisting}[frame=single] record Status: Type[0] := { The Matita emulator's internal state is a record: \begin{lstlisting}[frame=single] record Status: Type[0] := { code_memory: BitVectorTrie Byte 16; low_internal_ram: BitVectorTrie Byte 7; program_counter: Word; special_function_registers_8051: Vector Byte 19; ... }. ... }. \end{lstlisting} This record encapsulates the current memory contents, the program counter, the state of the current SFRs, and so on. A callback function was also accepted as an argument, which witnessed' the execution as it happened. Due to Matita's termination requirement, \texttt{execute} cannot execute a program indefinitely. An alternative approach would be to produce an infinite stream of statuses representing an execution trace. Matita supports infinite streams through co-inductive types. An alternative would be to produce an infinite stream of statuses representing an execution trace using Matita's co-inductive types. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \label{subsect.instruction.set.unorthogonality} A peculiarity of the MCS-51 is its unorthogonal instruction set. For instance, the \texttt{MOV} instruction can be invoked using one of 16 combinations of addressing modes out of a possible 361. A peculiarity of the MCS-51 is its unorthogonal instruction set; \texttt{MOV} can be invoked using one of 16 combinations of addressing modes out of a total of 361, for instance. % Show example of pattern matching with polymorphic variants [ U1 of 'a | ... | U6 of 'f ] \end{lstlisting} For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed. The types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed. This polymorphic variant machinery worked well: it introduced a certain level of type safety (for instance, the type of \texttt{MOV} above guarantees it cannot be invoked with arguments in the \texttt{carry} and \texttt{data16} addressing modes, respectively), and also allowed us to pattern match against instructions, when necessary. However, this polymorphic variant machinery is \emph{not} present in Matita. We needed some way to produce the same effect, which Matita supported. For this task, we used dependent types. We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against: We used dependent types. We provided an inductive data type representing all addressing modes, a type that functions will pattern match against: \begin{lstlisting}[frame=single] inductive addressing_mode: Type[0] := The \texttt{is\_a} function checks if an \texttt{addressing\_mode} matches an \texttt{addressing\_mode\_tag}: \begin{lstlisting}[frame=single] let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d := definition is_a := $\lambda$d: addressing_mode_tag. $\lambda$A: addressing_mode. match d with [ direct $\Rightarrow$ ... \end{lstlisting} The \texttt{is\_in} function checks if an \texttt{addressing\_mode} matches a set of tags represented as a vector. It simply extends the \texttt{is\_a} function in the obvious manner. A \texttt{subaddressing\_mode} is an \emph{ad hoc} non-empty $\Sigma$-type of \texttt{addressing\_mode}s constrained to be in a set of tags: The \texttt{is\_in} function checks if an \texttt{addressing\_mode} matches a set of tags represented as a vector. It simply extends the \texttt{is\_a} function in the obvious manner. A \texttt{subaddressing\_mode} is an \emph{ad hoc} non-empty $\Sigma$-type of \texttt{addressing\_mode}s in a set of tags: \begin{lstlisting}[frame=single] record subaddressing_mode subaddressing_modeel :> addressing_mode; subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) bool_to_Prop (is_in $\ldots$ l subaddressing_modeel) }. \end{lstlisting} % One of these coercions opens up a proof obligation which needs discussing % Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on The final 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. The first is a forgetful coercion, while the second opens a proof obligation wherein we must prove that the provided value is in the admissible set. These coercions were first introduced by PVS to implement subset types~\cite{shankar:principles:1999}, and later in Coq as part of Russell~\cite{sozeau:subset:2006}. In Matita all coercions can open proof obligations. Finally, type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{Vector addressing\_mode\_tag} to \texttt{Type$\lbrack0\rbrack$}, are required. The first opens a proof obligation wherein we must prove that the provided value is in the admissible set, simulating PVS subset types~\cite{shankar:principles:1999}. %PVS introduced subset types, and these later featured in Coq as part of Russell~\cite{sozeau:subset:2006}. %All coercions in Matita can open proof obligations. Proof obligations require us to state and prove a few auxilliary lemmas related to the transitivity of subtyping. We tried other dependently and non-dependently typed solutions before settling on this approach. As we need a large number of different combinations of addressing modes to describe the whole instruction set, it is infeasible to declare a datatype for each one of these combinations. As we need a large number of different combinations of addressing modes to describe the instruction set, it is infeasible to declare a datatype for each one of these combinations. The current solution is closest to the corresponding O'Caml code, to the point that the translation from O'Caml to Matita is almost syntactical. We would like to investigate the possibility of changing the code extraction procedure of Matita so that it recognises this programming pattern and outputs O'Caml code using polymorphic variants. % We would like to investigate the possibility of changing the code extraction procedure of Matita so that it recognises this programming pattern and outputs O'Caml code using polymorphic variants. % Talk about extraction to O'Caml code, which hopefully will allow us to extract back to using polymorphic variants, or when extracting vectors we could extract using phantom types This field is only logical, since it does not represent any quantity stored in the physical processor, and is used to keep track of the current processor time'. Before every execution step, \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute. The emulator then executes the instruction, followed by the code implementing the timers and I/O\footnote{Though it isn't fully specified by the manufacturer's data sheets if I/O is handled at the beginning or the end of each cycle.}. In order to model I/O, we also store in \texttt{status} a \emph{continuation} which is a description of the behaviour of the environment: The emulator executes the instruction then the code implementing timers and I/O (it isn't specified by the data sheets if I/O is handled at the beginning or the end of each cycle.) To model I/O, we store in \texttt{status} a \emph{continuation} which is a description of the behaviour of the environment: \begin{lstlisting} type line = | SerialBuff of [ Eight of byte | Nine of BitVectors.bit * byte ] ] | Nine of BitVectors.bit * byte ]  ] type continuation = [In of time * line * [Out of (time -> line -> time * continuation)] \end{lstlisting} At each moment, the second projection of the continuation $k$ describes how the environment will react to an output event performed in the future by the processor. The second projection of the continuation $k$ describes how the environment will react to an output event performed in the future by the processor. Suppose $\pi_2(k)(\tau,o) = \langle \tau',k' \rangle$. If the emulator at time $\tau$ starts an asynchronous output $o$ either on the P1 or P3 output lines, or on the UART, then the environment will receive the output at time $\tau'$. We leave the computation of the delay time to the environment. We use only the P1 and P3 lines despite the MCS-51 having 4 output lines, P0--P3. We use only the P1 and P3 lines despite the MCS-51 having~4 output lines, P0--P3. This is because P0 and P2 become inoperable if XRAM is present (we assume it is). As mentioned in Subsection~\ref{subsect.labels.pseudoinstructions} we introduced a notion of \emph{cost label}. Cost labels are inserted by the prototype C compiler at specific locations in the object code. Roughly, for those familiar with control flow graphs, they are inserted at the start of every basic block. Cost labels are used to calculate a precise costing for a program by marking the location of basic blocks. Cost labels are used to calculate a precise costing for a program by marking the start of basic blocks. During the assembly phase, where labels and pseudoinstructions are eliminated, a map is generated associating cost labels with memory locations. This map is later used in a separate analysis which computes the cost of a program by traversing through a program, fetching one instruction at a time, and computing the cost of blocks. %\end{figure} We spent considerable effort attempting to ensure that what we have formalised is an accurate model of the MCS-51 microprocessor. We attempted to ensure that what we have formalised is an accurate model of the MCS-51 microprocessor. We made use of multiple data sheets, each from a different manufacturer. We further used MCU 8051 IDE as a reference, which allows a user to step through an assembly program one instruction at a time. Using these execution traces, we were able to step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator. With these execution traces, we could step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator. We partially validated the assembler by proving in Matita that on all defined opcodes the \texttt{assembly\_1} and \texttt{fetch} functions are inverse. The Matita formalisation was largely copied from the O'Caml source code, apart from the changes already mentioned. However, as the Matita emulator is executable, we could perform further validation by comparing the trace of a program's execution in the Matita emulator with the trace of the same program in the O'Caml emulator. The Matita formalisation was largely copied from the O'Caml source code apart from the changes already mentioned. As the Matita emulator is executable we could perform further validation by comparing the trace of a program's execution in the Matita and O'Caml emulators. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Work closely related to our own can be found in~\cite{fox:trustworthy:2010}. Here, the authors describe the formalisation, in HOL4, of the ARMv7 instruction set architecture. They further point to an excellent list of references to related work in the literature for the interested reader. They further point to an excellent list of references to related work in the literature. This formalisation also considers the machine code level, opposed to their formalisation, which only considering an abstract assembly language. In particular, instruction decoding is explicitly modeled inside HOL4's logic. Instruction decoding is explicitly modeled inside HOL4's logic. We go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction into machine code. The CLI Stack consists of the design and verification of a whole chain of artifacts including a 32-bit microprocessor, the Piton assembler and two compilers for high-level languages. Like CerCo, the CLI Stack compilers gave the cost of high-level instructions in processor cycles. However, unlike CerCo, both the CLI Stack high-level languages ($\mu$Gypsy and Nqthm Pure Lisp) and FM9001 microprocessor were not commercial products, but artificial' designs created for the purpose of verification (see~\cite{moore:grand:2005}). However, unlike CerCo, both the CLI Stack high-level languages ($\mu$Gypsy and Nqthm Lisp) and FM9001 microprocessor were not commercial products, but designs created for the purpose of verification (see~\cite{moore:grand:2005}). The CompCert C compiler is extracted to O'Caml using Coq's code extraction facility. Finally~\cite{sarkar:semantics:2009} provides an executable semantics for x86-CC multiprocessor machine code. This machine code exhibits a high degree of non-uniformity similar to the MCS-51. However, only a small subset of the instruction set is considered, and they over-approximate the possibilities of unorthogonality of the instruction set, largely dodging the problems we had to face. This machine code exhibits a degree of non-uniformity similar to the MCS-51. Only a small subset of the instruction set is considered, and they over-approximate the possibilities of unorthogonality of the instruction set, largely dodging the problems we had to face. Further, it seems that the definition of the decode function is potentially error prone. A small domain specific language of patterns is formalised in HOL4. This is similar to the specification language of the x86 instruction set found in manufacturer's data sheets. A domain specific language of patterns is formalised in HOL4, similar to the specification language of the x86 instruction set found in manufacturer's data sheets. A decode function is implemented by copying lines from data sheets into the proof script, which are then partially evaluated to obtain a compiler. We are currently considering implementing a similar domain specific language in Matita. Our cost model assigns costs to blocks of instructions by tracing the way that blocks are compiled, and by computing exact costs on generated machine language. To perform this accurately, we have provided an executable semantics for the MCS-51 family of processors. The formalisation was done twice, first in O'Caml and then in Matita, and captures the exact timings of the processor (according to a Siemen's data sheet). Moreover, the O'Caml formalisation also considers timers and I/O. Adding support for I/O and timers in Matita is on-going work that will not present any major problem, and was delayed only because the addition is not immediately useful for the formalisation of the CerCo compiler. An O'Caml and Matita formalisation was provided, and both capture the exact timings of the MCS-51 (according to a Siemen's data sheet). The O'Caml formalisation also considers timers and I/O. Adding support for I/O and timers in Matita is on-going work that will not present any problem, and was delayed only because the addition is not immediately useful for the formalisation of the CerCo compiler. The formalisation is done at machine level and not at assembly level; we also formalise fetching and decoding. Our main difficulty in formalising the MCS-51 was the unorthogonality of its memory model and instruction set. These problems are easily handled in O'Caml by using advanced language features like polymorphic variants and phantom types, simulating Generalized Abstract Data Types~\cite{xi:guarded:2003}. Importantly, we discovered the best manner of using dependent types to recover the same flexibility, to reduce spurious partiality, and to grant invariants that will be later useful in other formalisations in the CerCo project. These problems are handled in O'Caml by using language features like polymorphic variants and phantom types, simulating Generalized Abstract Data Types~\cite{xi:guarded:2003}. Importantly, we searched for a manner of using dependent types to recover the same flexibility, reduce spurious partiality, and grant invariants that will be later useful in other formalisations in CerCo. The formalisation has been partially verified by computing execution traces on selected programs and comparing them with an existing emulator. Finally, we are aware of having over-specified the processor in several places, by fixing a behaviour hopefully consistent with the real machine, where manufacturer data sheets are ambiguous or under-specified. \bibliography{itp-2011.bib} \bibliography{IEEEabrv,itp-2011} \end{document}