Changeset 1023 for src/ASM/CPP2011


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1022 r1023  
    135135However, at the machine code level, conditional jumps are limited to jumping `locally', using a measly byte offset.
    136136To 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'):
     137{\small{
    137138\begin{displaymath}
    138139\begin{array}{r@{\quad}l@{\;\;}l@{\qquad}c@{\qquad}l@{\;\;}l}
     
    143144       &              &                            &                 & \mathtt{MOV}  & \mathtt{A}\;\;\mathtt{B}
    144145\end{array}
    145 \end{displaymath}
     146\end{displaymath}}}
    146147In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}.
    147148Naturally, 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.
     
    158159Yet one more question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}?
    159160To understand, again, why this problem is not trivial, consider the following snippet of assembly code:
     161{\small{
    160162\begin{displaymath}
    161163\begin{array}{r@{\qquad}r@{\quad}l@{\;\;}l@{\qquad}l}
     
    166168\text{5:} & \mathtt{(0x100)}  & \texttt{LJMP} & \texttt{-0x100}  & \text{\texttt{;; Jump backward 256.}} \\
    167169\end{array}
    168 \end{displaymath}
     170\end{displaymath}}}
    169171We observe that $100_{16} = 256_{10}$, and lies \emph{just} outside the range expressible in an 8-bit byte (0--255).
    170172
     
    191193In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness.
    192194
    193 The rest of this paper is a detailed description of our proof that is partly
    194 still in progress.
     195The rest of this paper is a detailed description of our proof that is, in part, still a work in progress.
    195196
    196197% ---------------------------------------------------------------------------- %
     
    209210\label{sect.matita}
    210211
    211 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
    212 types that we heavily exploit in the formalization. The syntax of the
    213 statements and definitions in the paper should be self-explanatory, at least
    214 to those exposed to dependent type theory. We only remark the use of
    215 of `$\mathtt{?}$' or `$\mathtt{\ldots}$' for omitting single terms or
    216 sequences of terms to be inferred automatically by the system, respectively.
     212Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
     213In particular, it features dependent types that we heavily exploit in the formalisation.
     214The syntax of the statements and definitions in the paper should be self-explanatory, at least to those exposed to dependent type theory.
     215We 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.
    217216Those that are not inferred are left to the user as proof obligations.
    218 Pairs are denoted with angular brackets.
    219 
    220 Matita features a liberal system of coercions. In particular, it is possible
    221 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
    222 obligation that asks the user to prove that $P$ holds for $x$. When a coercion
    223 must be applied to a complex term (a lambda-abstraction, a local definition,
    224 a case analysis), the system automatically propagates the coercion to the
    225 sub-terms. For instance, to apply a coercion to force $\lambda x.M : A \to B$
    226 to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from
    227 $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$. This is
    228 significant when the coercion opens a proof obligation, since the user
    229 will be presented with multiple, but simpler proof obligations in the right
    230 context. Matita supports in this way the proof methodology developed by
    231 Sozeau in~\cite{russell}, but with an implementation that is lighter than the
    232 one of Coq and more integrated in the system.
     217Pairs are denoted with angular brackets, $\langle-, -\rangle$.
     218
     219Matita features a liberal system of coercions.
     220It 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$.
     221The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$.
     222When 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
     223 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$.
     224This 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.
     225In 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.
    233226
    234227% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.