# Changeset 813 for Deliverables/D4.1/ITP-Paper

Ignore:
Timestamp:
May 16, 2011, 6:07:52 PM (9 years ago)
Message:

added boxing of matita code to distinguish from o'caml

File:
1 edited

### Legend:

Unmodified
 r812 Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq. Matita's internal language is similar to O'Caml's. The symbols \texttt{?}' or \texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively. Matita's internal language is similar to O'Caml's; we frame Matita code to distinguish the two. In Matita, \texttt{?}' or \texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively. A full account of the formalisation can be found in~\cite{cerco-report:2011}. In Matita, we are able to use the full power of dependent types to always work with vectors of a known size: \begin{lstlisting} \begin{lstlisting}[frame=single] inductive Vector (A: Type[0]): nat $\rightarrow$ Type[0] ≝ VEmpty: Vector A O We define \texttt{BitVector} as 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} \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) := ... We picked a modified form of trie of fixed height $h$. Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$: \begin{lstlisting} \begin{lstlisting}[frame=single] inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝ Leaf: A $\rightarrow$ BitVectorTrie A 0 The internal state of the Matita emulator is represented as a record: \begin{lstlisting} \begin{lstlisting}[frame=single] record Status: Type[0] := { An updated program counter, along with its concrete cost in processor cycles, is also returned. These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary between particular implementations. \begin{lstlisting} \begin{lstlisting}[frame=single] definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat \end{lstlisting} Instruction are assembled to bit encodings by \texttt{assembly1}: \begin{lstlisting} \begin{lstlisting}[frame=single] definition assembly1: instruction $\rightarrow$ list Byte \end{lstlisting} Pseudoinstructions and labels are eliminated in favour of instructions from the MCS-51 instruction set. A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced. \begin{lstlisting} \begin{lstlisting}[frame=single] definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) \end{lstlisting} A single fetch-decode-execute cycle is performed by \texttt{execute\_1}: \begin{lstlisting} \begin{lstlisting}[frame=single] definition execute_1: Status $\rightarrow$ Status \end{lstlisting} The \texttt{execute} functions performs a fixed number of cycles by iterating \texttt{execute\_1}: \begin{lstlisting} \begin{lstlisting}[frame=single] let rec execute (n: nat) (s: Status): Status := ... \end{lstlisting} We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against: \begin{lstlisting} \begin{lstlisting}[frame=single] inductive addressing_mode: Type[0] := DIRECT: Byte $\rightarrow$ addressing_mode In order to do this, we introduced an inductive type of addressing mode `tags'. The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}: \begin{lstlisting} \begin{lstlisting}[frame=single] inductive addressing_mode_tag : Type[0] := direct: addressing_mode_tag \end{lstlisting} The \texttt{is\_a} function checks if an \texttt{addressing\_mode} matches an \texttt{addressing\_mode\_tag}: \begin{lstlisting} \begin{lstlisting}[frame=single] let rec is_a (d: addressing_mode_tag) 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: \begin{lstlisting} \begin{lstlisting}[frame=single] record subaddressing_mode (n: nat) \end{lstlisting} An implicit coercion is provided to promote vectors of tags (denoted with $\llbracket - \rrbracket$) to the corresponding \texttt{subaddressing\_mode} so that we can use a syntax close to that of O'Caml to specify \texttt{preinstruction}s: \begin{lstlisting} \begin{lstlisting}[frame=single] inductive preinstruction (A: Type[0]): Type[0] ≝ ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ This allows us to skip impossible cases. For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}: \begin{lstlisting} \begin{lstlisting}[frame=single] definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a.