Ignore:
Timestamp:
Sep 9, 2011, 9:49:44 AM (9 years ago)
Author:
mulligan
Message:

got paper down to 15 and a half pages with nothing much added to document

File:
1 edited

Legend:

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

    r1190 r1199  
    3636   mathescape=true,
    3737  }
    38 \lstset{language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
     38\lstset{language=matita-ocaml,basicstyle=\scriptsize\tt,columns=flexible,breaklines=false,
    3939        keywordstyle=\bfseries, %\color{red}\bfseries,
    4040        keywordstyle=[2]\bfseries, %\color{blue},
     
    5454}
    5555
     56\setlength{\belowcaptionskip}{0pt}
     57\setlength{\textfloatsep}{1em}
     58
    5659\begin{document}
    5760
    5861\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
    5962\authorrunning{D. P. Mulligan \and C. Sacerdoti Coen}
    60 \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
    61 %\and
    62 %  \IEEEauthorblockN{Claudio Sacerdoti Coen}
    63 %  \IEEEauthorblockA{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
    64 %}
     63\institute{\vspace{-2em}}
     64% \institute{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
    6565
    6666\bibliographystyle{plain}
     
    8282\end{abstract}
    8383
    84 \begin{keywords}
    85 Hardware formalisation, Matita, dependent types, CerCo
    86 \end{keywords}
     84%\begin{keywords}
     85%Hardware formalisation, Matita, dependent types, CerCo
     86%\end{keywords}
    8787
    8888%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    395395inductive BitVectorTrie(A: Type[0]):nat $\rightarrow$ Type[0] :=
    396396  Leaf: A $\rightarrow$ BitVectorTrie A 0
    397 | Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$
    398   BitVectorTrie A (S n)
     397| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
    399398| Stub: ∀n. BitVectorTrie A n.
    400399\end{lstlisting}
     
    473472These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary between particular implementations.
    474473\begin{lstlisting}[frame=single]
    475 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$
    476   instruction $\times$ Word $\times$ nat
     474definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat
    477475\end{lstlisting}
    478476Instruction are assembled to bit encodings by \texttt{assembly1}:
     
    484482A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced.
    485483\begin{lstlisting}[frame=single]
    486 definition assembly: assembly_program $\rightarrow$
    487   option (list Byte $\times$ (BitVectorTrie String 16))
     484definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16))
    488485\end{lstlisting}
    489486A single fetch-decode-execute cycle is performed by \texttt{execute\_1}:
     
    523520[ `ADD of acc * [ reg | direct | indirect | data ]
    524521...
    525 | `MOV of
    526    (acc * [ reg| direct | indirect | data ],
     522| `MOV of (acc * [ reg| direct | indirect | data ],
    527523   [ reg | indirect ] * [ acc | direct | data ],
    528524   direct * [ acc | reg | direct | indirect | data ],
     
    535531Here, \texttt{union6} is a disjoint union type, defined as follows:
    536532\begin{lstlisting}
    537 type ('a,'b,'c,'d,'e,'f) union6 =
    538   [ `U1 of 'a | ... | `U6 of 'f ]
     533type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a | ... | `U6 of 'f ]
    539534\end{lstlisting}
    540535The types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
     
    566561  $\lambda$d: addressing_mode_tag. $\lambda$A: addressing_mode.
    567562match d with
    568 [ direct $\Rightarrow$
    569   match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
    570 | indirect $\Rightarrow$
    571   match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     563[ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     564| indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
    572565...
    573566\end{lstlisting}
     
    577570A \texttt{subaddressing\_mode} is an \emph{ad hoc} non-empty $\Sigma$-type of \texttt{addressing\_mode}s in a set of tags:
    578571\begin{lstlisting}[frame=single]
    579 record subaddressing_mode
    580   (n: nat)
    581   (l: Vector addressing_mode_tag (S n)): Type[0] :=
    582 {
     572record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] := {
    583573  subaddressing_modeel :> addressing_mode;
    584   subaddressing_modein:
    585     bool_to_Prop (is_in $\ldots$ l subaddressing_modeel)
     574  subaddressing_modein: bool_to_Prop (is_in $\ldots$ l subaddressing_modeel)
    586575}.
    587576\end{lstlisting}
     
    589578\begin{lstlisting}[frame=single]
    590579inductive preinstruction (A: Type[0]): Type[0] ≝
    591   ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$
    592        preinstruction A
    593 | ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$
    594         preinstruction A
     580  ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ preinstruction A
     581| ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ preinstruction A
    595582...
    596583\end{lstlisting}
     
    656643type line =
    657644[ `P1 of byte | `P3 of byte
    658 | `SerialBuff of
    659    [ `Eight of byte
    660    | `Nine of BitVectors.bit * byte ]  ]
     645| `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]  ]
     646
    661647type continuation =
    662 [`In of time * line *
    663   epsilon * continuation] option *
     648[`In of time * line * epsilon * continuation] option *
    664649[`Out of (time -> line -> time * continuation)]
    665650\end{lstlisting}
Note: See TracChangeset for help on using the changeset viewer.