Ignore:
Timestamp:
May 16, 2011, 4:32:36 PM (8 years ago)
Author:
mulligan
Message:

more changes to get everything to fit correctly. gone past 8 pg limit

File:
1 edited

Legend:

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

    r808 r809  
    3636   mathescape=true,
    3737  }
    38 \lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
     38\lstset{language=matita-ocaml,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
    3939        keywordstyle=\bfseries, %\color{red}\bfseries,
    4040        keywordstyle=[2]\bfseries, %\color{blue},
     
    336336type nibble = [`Sixteen] vect
    337337type byte = [`Eight] vect
    338 $\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w
    339 $\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b
     338let split_word w = split_nth 4 w
     339let split_byte b = split_nth 2 b
    340340\end{lstlisting}}
    341341\end{minipage}
     
    371371\begin{lstlisting}
    372372let rec split (A: Type[0]) (m,n: nat) on m:
    373    Vector A (plus m n) $\rightarrow$ (Vector A m) $\times$ (Vector A n) := ...
     373   Vector A (m + n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ...
    374374\end{lstlisting}
    375375
     
    391391inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
    392392  Leaf: A $\rightarrow$ BitVectorTrie A 0
    393 | Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
     393| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$
     394  BitVectorTrie A (S n)
    394395| Stub: ∀n. BitVectorTrie A n.
    395396\end{lstlisting}
     
    438439The internal state of the Matita emulator is represented as a record:
    439440\begin{lstlisting}
    440 record Status: Type[0] ≝ {
     441record Status: Type[0] :=
     442{
    441443  code_memory: BitVectorTrie Byte 16;
    442444  low_internal_ram: BitVectorTrie Byte 7;
     
    445447  program_counter: Word;
    446448  special_function_registers_8051: Vector Byte 19;
    447   special_function_registers_8052: Vector Byte 5;
    448   ...  }.
     449  ...
     450}.
    449451\end{lstlisting}
    450452This record encapsulates the current memory contents, the program counter, the state of the current SFRs, and so on.
     
    463465These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary between particular implementations.
    464466\begin{lstlisting}
    465 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat
     467definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$
     468  instruction $\times$ Word $\times$ nat
    466469\end{lstlisting}
    467470Instruction are assembled to bit encodings by \texttt{assembly1}:
     
    473476A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced.
    474477\begin{lstlisting}
    475 definition assembly:
    476   assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16))
     478definition assembly: assembly_program $\rightarrow$
     479  option (list Byte $\times$ (BitVectorTrie String 16))
    477480\end{lstlisting}
    478481A single fetch-decode-execute cycle is performed by \texttt{execute\_1}:
     
    483486\texttt{execute\_1}:
    484487\begin{lstlisting}
    485 let rec execute (n: nat) (s: Status) on n: Status := ...
     488let rec execute (n: nat) (s: Status): Status := ...
    486489\end{lstlisting}
    487490This differs from the O'Caml emulator, which executed a program indefinitely.
     
    512515\begin{lstlisting}
    513516type 'addr preinstruction =
    514  [ `ADD of acc * [ reg | direct | indirect | data ]
     517[ `ADD of acc * [ reg | direct | indirect | data ]
    515518...
    516  | `MOV of
    517     (acc * [ reg | direct | indirect | data ],
    518      [ reg | indirect ] * [ acc | direct | data ],
    519      direct * [ acc | reg | direct | indirect | data ],
    520      dptr * data16,
    521      carry * bit,
    522      bit * carry
    523      ) union6
     519| `MOV of
     520   (acc * [ reg| direct | indirect | data ],
     521   [ reg | indirect ] * [ acc | direct | data ],
     522   direct * [ acc | reg | direct | indirect | data ],
     523   dptr * data16,
     524   carry * bit,
     525   bit * carry
     526   ) union6
    524527...
    525528\end{lstlisting}
     
    538541We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against:
    539542\begin{lstlisting}
    540 inductive addressing_mode: Type[0]
     543inductive addressing_mode: Type[0] :=
    541544  DIRECT: Byte $\rightarrow$ addressing_mode
    542545| INDIRECT: Bit $\rightarrow$ addressing_mode
     
    547550The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}:
    548551\begin{lstlisting}
    549 inductive addressing_mode_tag : Type[0]
     552inductive addressing_mode_tag : Type[0] :=
    550553  direct: addressing_mode_tag
    551554| indirect: addressing_mode_tag
     
    554557The \texttt{is\_a} function checks if an \texttt{addressing\_mode} matches an \texttt{addressing\_mode\_tag}:
    555558\begin{lstlisting}
    556 let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d :=
    557   match d with
    558    [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
    559    | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     559let rec is_a
     560  (d: addressing_mode_tag)
     561  (A: addressing_mode) on d :=
     562match d with
     563[ direct $\Rightarrow$
     564  match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     565| indirect $\Rightarrow$
     566  match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
    560567...
    561568\end{lstlisting}
     
    564571A \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:
    565572\begin{lstlisting}
    566 record subaddressing_mode n (l: Vector addressing_mode_tag (S n)): Type[0] :=
    567  { subaddressing_modeel :> addressing_mode;
    568    subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) }.
     573record subaddressing_mode
     574  (n: nat)
     575  (l: Vector addressing_mode_tag (S n)): Type[0] :=
     576{
     577  subaddressing_modeel :> addressing_mode;
     578  subaddressing_modein:
     579    bool_to_Prop (is_in ? l subaddressing_modeel)
     580}.
    569581\end{lstlisting}
    570582An 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:
    571583\begin{lstlisting}
    572584inductive preinstruction (A: Type[0]): Type[0] ≝
    573    ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
    574  | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
     585  ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$
     586       preinstruction A
     587| ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$
     588        preinstruction A
    575589...
    576590\end{lstlisting}
     
    593607For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
    594608\begin{lstlisting}
    595 definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝ $~\lambda$s, v, a.
    596    match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
    597      [ DPTR $\Rightarrow$ $\lambda$_: True.
    598        let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
    599        let status := set_8051_sfr s SFR_DPH bu in
    600        let status := set_8051_sfr status SFR_DPL bl in
    601          status
    602      | _ $\Rightarrow$ $\lambda$_: False. $\bot$ ]
    603        $~$(subaddressing_modein $\ldots$ a).
     609definition set_arg_16:
     610  Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a.
     611match a return
     612   $\lambda$x. bool_to_Prop (is_in ? $\llbracket$dptr$\rrbracket$ x) $\rightarrow$ ? with
     613  [ DPTR $\Rightarrow$ $\lambda$_: True.
     614    let $\langle$bu, bl$\rangle$ := split $\ldots$ eight eight v in
     615    let status := set_8051_sfr s SFR_DPH bu in
     616    let status := set_8051_sfr status SFR_DPL bl in
     617      status
     618  | _ $\Rightarrow$ $\lambda$_: False. $\bot$
     619  ] $~$(subaddressing_modein $\ldots$ a).
    604620\end{lstlisting}
    605621We give a proof (the expression \texttt{(subaddressing\_modein} $\ldots$ \texttt{a)}) that the argument $a$ is in the set $\llbracket$ \texttt{dptr} $\rrbracket$ to the \texttt{match} expression.
     
    633649\begin{lstlisting}
    634650type line =
    635   [ `P1 of byte | `P3 of byte
    636   | `SerialBuff of
    637      [ `Eight of byte
    638      | `Nine of BitVectors.bit * byte ]
    639   ]
     651[ `P1 of byte | `P3 of byte
     652| `SerialBuff of
     653   [ `Eight of byte
     654   | `Nine of BitVectors.bit * byte ]
     655]
    640656type continuation =
    641   [`In of time * line *
    642           epsilon * continuation] option *
    643   [`Out of (time -> line -> time * continuation)]
     657[`In of time * line *
     658  epsilon * continuation] option *
     659[`Out of (time -> line -> time * continuation)]
    644660\end{lstlisting}
    645661At 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.
Note: See TracChangeset for help on using the changeset viewer.