Changeset 1023
 Timestamp:
 Jun 21, 2011, 12:23:31 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r1022 r1023 135 135 However, at the machine code level, conditional jumps are limited to jumping `locally', using a measly byte offset. 136 136 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'): 137 {\small{ 137 138 \begin{displaymath} 138 139 \begin{array}{r@{\quad}l@{\;\;}l@{\qquad}c@{\qquad}l@{\;\;}l} … … 143 144 & & & & \mathtt{MOV} & \mathtt{A}\;\;\mathtt{B} 144 145 \end{array} 145 \end{displaymath} 146 \end{displaymath}}} 146 147 In the translation, if \texttt{JZ} fails, we fall through to the \texttt{SJMP} which jumps over the \texttt{LJMP}. 147 148 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. … … 158 159 Yet one more question remains: how do we decide whether to expand a jump into an \texttt{SJMP} or an \texttt{LJMP}? 159 160 To understand, again, why this problem is not trivial, consider the following snippet of assembly code: 161 {\small{ 160 162 \begin{displaymath} 161 163 \begin{array}{r@{\qquad}r@{\quad}l@{\;\;}l@{\qquad}l} … … 166 168 \text{5:} & \mathtt{(0x100)} & \texttt{LJMP} & \texttt{0x100} & \text{\texttt{;; Jump backward 256.}} \\ 167 169 \end{array} 168 \end{displaymath} 170 \end{displaymath}}} 169 171 We observe that $100_{16} = 256_{10}$, and lies \emph{just} outside the range expressible in an 8bit byte (0255). 170 172 … … 191 193 In particular, in CerCo we are also interested in the completeness of the compilation process, whereas previous formalisations only focused on correctness. 192 194 193 The rest of this paper is a detailed description of our proof that is partly 194 still in progress. 195 The rest of this paper is a detailed description of our proof that is, in part, still a work in progress. 195 196 196 197 %  % … … 209 210 \label{sect.matita} 210 211 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 selfexplanatory, 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. 212 Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}. 213 In particular, it features dependent types that we heavily exploit in the formalisation. 214 The syntax of the statements and definitions in the paper should be selfexplanatory, at least to those exposed to dependent type theory. 215 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. 217 216 Those 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 lambdaabstraction, a local definition, 224 a case analysis), the system automatically propagates the coercion to the 225 subterms. 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. 217 Pairs are denoted with angular brackets, $\langle, \rangle$. 218 219 Matita features a liberal system of coercions. 220 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$. 221 The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$. 222 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 subterms 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$. 224 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. 225 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. 233 226 234 227 %  %
Note: See TracChangeset
for help on using the changeset viewer.