Changeset 1023

Ignore:
Timestamp:
Jun 21, 2011, 12:23:31 PM (8 years ago)
Message:

changes to english in matita section, shrunk diagrams in introduction to save space

File:
1 edited

Legend:

Unmodified
 r1022 However, at the machine code level, conditional jumps are limited to jumping locally', using a measly byte offset. To translate a jump to a label, a single conditional jump pseudoinstruction may be translated into a block of three real instructions as follows (here, \texttt{JZ} is jump if accumulator is zero'): {\small{ \begin{displaymath} \begin{array}{r@{\quad}l@{\;\;}l@{\qquad}c@{\qquad}l@{\;\;}l} &              &                            &                 & \mathtt{MOV}  & \mathtt{A}\;\;\mathtt{B} \end{array} \end{displaymath} \end{displaymath}}} In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}. Naturally, if \texttt{label} is close enough, a conditional jump pseudoinstruction is mapped directly to a conditional jump machine instruction; the above translation only applies if \texttt{label} is not sufficiently local. Yet one more question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}? To understand, again, why this problem is not trivial, consider the following snippet of assembly code: {\small{ \begin{displaymath} \begin{array}{r@{\qquad}r@{\quad}l@{\;\;}l@{\qquad}l} \text{5:} & \mathtt{(0x100)}  & \texttt{LJMP} & \texttt{-0x100}  & \text{\texttt{;; Jump backward 256.}} \\ \end{array} \end{displaymath} \end{displaymath}}} We observe that $100_{16} = 256_{10}$, and lies \emph{just} outside the range expressible in an 8-bit byte (0--255). In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness. The rest of this paper is a detailed description of our proof that is partly still in progress. The rest of this paper is a detailed description of our proof that is, in part, still a work in progress. % ---------------------------------------------------------------------------- % \label{sect.matita} Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. In particular, it features dependent types that we heavily exploit in the formalization. The syntax of the statements and definitions in the paper should be self-explanatory, at least to those exposed to dependent type theory. We only remark the use of of $\mathtt{?}$' or $\mathtt{\ldots}$' for omitting single terms or sequences of terms to be inferred automatically by the system, respectively. Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. In particular, it features dependent types that we heavily exploit in the formalisation. The syntax of the statements and definitions in the paper should be self-explanatory, at least to those exposed to dependent type theory. We only remark the use of of $\mathtt{?}$' or $\mathtt{\ldots}$' for omitting single terms or sequences of terms to be inferred automatically by the system, respectively. Those that are not inferred are left to the user as proof obligations. Pairs are denoted with angular brackets. Matita features a liberal system of coercions. In particular, it is possible to define a uniform coercion $\lambda x.\langle x,?\rangle$ from every type $T$ to the dependent product $\Sigma x:T.P~x$. The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$. When a coercion must be applied to a complex term (a lambda-abstraction, a local definition, a case analysis), the system automatically propagates the coercion to the sub-terms. For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$. This is significant when the coercion opens a proof obligation, since the user will be presented with multiple, but simpler proof obligations in the right context. Matita supports in this way the proof methodology developed by Sozeau in~\cite{russell}, but with an implementation that is lighter than the one of Coq and more integrated in the system. Pairs are denoted with angular brackets, $\langle-, -\rangle$. Matita features a liberal system of coercions. It is possible to define a uniform coercion $\lambda x.\langle x,?\rangle$ from every type $T$ to the dependent product $\Sigma x:T.P~x$. The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$. When a coercion must be applied to a complex term (a $\lambda$-abstraction, a local definition, or a case analysis), the system automatically propagates the coercion to the sub-terms For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$. This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context. In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated than that of Coq. % ---------------------------------------------------------------------------- %