Changeset 813 for Deliverables
 Timestamp:
 May 16, 2011, 6:07:52 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r812 r813 303 303 304 304 Matita~\cite{asperti:user:2007} is a proof assistant based on the Calculus of Coinductive constructions, similar to Coq. 305 Matita's internal language is similar to O'Caml's .306 The symbols`\texttt{?}' or `\texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively.305 Matita's internal language is similar to O'Caml's; we frame Matita code to distinguish the two. 306 In Matita, `\texttt{?}' or `\texttt{$\ldots$}' denote an argument or arguments to be inferred, respectively. 307 307 308 308 A full account of the formalisation can be found in~\cite{cercoreport:2011}. … … 362 362 363 363 In Matita, we are able to use the full power of dependent types to always work with vectors of a known size: 364 \begin{lstlisting} 364 \begin{lstlisting}[frame=single] 365 365 inductive Vector (A: Type[0]): nat $\rightarrow$ Type[0] ≝ 366 366 VEmpty: Vector A O … … 369 369 We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}. 370 370 We may use Matita's type system to provide precise typings for functions that are polymorphic in the size without code duplication: 371 \begin{lstlisting} 371 \begin{lstlisting}[frame=single] 372 372 let rec split (A: Type[0]) (m,n: nat) on m: 373 373 Vector A (m + n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ... … … 388 388 We picked a modified form of trie of fixed height $h$. 389 389 Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$: 390 \begin{lstlisting} 390 \begin{lstlisting}[frame=single] 391 391 inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝ 392 392 Leaf: A $\rightarrow$ BitVectorTrie A 0 … … 438 438 439 439 The internal state of the Matita emulator is represented as a record: 440 \begin{lstlisting} 440 \begin{lstlisting}[frame=single] 441 441 record Status: Type[0] := 442 442 { … … 464 464 An updated program counter, along with its concrete cost in processor cycles, is also returned. 465 465 These costs are taken from a Siemens Semiconductor Group data sheet for the MCS51~\cite{siemens:2011}, and will likely vary between particular implementations. 466 \begin{lstlisting} 466 \begin{lstlisting}[frame=single] 467 467 definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ 468 468 instruction $\times$ Word $\times$ nat 469 469 \end{lstlisting} 470 470 Instruction are assembled to bit encodings by \texttt{assembly1}: 471 \begin{lstlisting} 471 \begin{lstlisting}[frame=single] 472 472 definition assembly1: instruction $\rightarrow$ list Byte 473 473 \end{lstlisting} … … 475 475 Pseudoinstructions and labels are eliminated in favour of instructions from the MCS51 instruction set. 476 476 A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced. 477 \begin{lstlisting} 477 \begin{lstlisting}[frame=single] 478 478 definition assembly: assembly_program $\rightarrow$ 479 479 option (list Byte $\times$ (BitVectorTrie String 16)) 480 480 \end{lstlisting} 481 481 A single fetchdecodeexecute cycle is performed by \texttt{execute\_1}: 482 \begin{lstlisting} 482 \begin{lstlisting}[frame=single] 483 483 definition execute_1: Status $\rightarrow$ Status 484 484 \end{lstlisting} 485 485 The \texttt{execute} functions performs a fixed number of cycles by iterating 486 486 \texttt{execute\_1}: 487 \begin{lstlisting} 487 \begin{lstlisting}[frame=single] 488 488 let rec execute (n: nat) (s: Status): Status := ... 489 489 \end{lstlisting} … … 540 540 541 541 We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against: 542 \begin{lstlisting} 542 \begin{lstlisting}[frame=single] 543 543 inductive addressing_mode: Type[0] := 544 544 DIRECT: Byte $\rightarrow$ addressing_mode … … 549 549 In order to do this, we introduced an inductive type of addressing mode `tags'. 550 550 The constructors of \texttt{addressing\_mode\_tag} are in onetoone correspondence with the constructors of \texttt{addressing\_mode}: 551 \begin{lstlisting} 551 \begin{lstlisting}[frame=single] 552 552 inductive addressing_mode_tag : Type[0] := 553 553 direct: addressing_mode_tag … … 556 556 \end{lstlisting} 557 557 The \texttt{is\_a} function checks if an \texttt{addressing\_mode} matches an \texttt{addressing\_mode\_tag}: 558 \begin{lstlisting} 558 \begin{lstlisting}[frame=single] 559 559 let rec is_a 560 560 (d: addressing_mode_tag) … … 570 570 571 571 A \texttt{subaddressing\_mode} is an \emph{ad hoc} nonempty $\Sigma$type of \texttt{addressing\_mode}s constrained to be in a set of tags: 572 \begin{lstlisting} 572 \begin{lstlisting}[frame=single] 573 573 record subaddressing_mode 574 574 (n: nat) … … 581 581 \end{lstlisting} 582 582 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: 583 \begin{lstlisting} 583 \begin{lstlisting}[frame=single] 584 584 inductive preinstruction (A: Type[0]): Type[0] ≝ 585 585 ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ … … 606 606 This allows us to skip impossible cases. 607 607 For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}: 608 \begin{lstlisting} 608 \begin{lstlisting}[frame=single] 609 609 definition set_arg_16: 610 610 Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a.
Note: See TracChangeset
for help on using the changeset viewer.