Index: /Papers/cppasm2012/cpp2012asm.tex
===================================================================
 /Papers/cppasm2012/cpp2012asm.tex (revision 2356)
+++ /Papers/cppasm2012/cpp2012asm.tex (revision 2357)
@@ 90,6 +90,6 @@
compiler (assembler) is to individually expand every pseudoinstruction in such a way
that all global constraints are satisfied and that the compiled program size
is minimal in size and faster in time. The problem is known to be particularly
complex for most CICS architectures (for instance, see~\cite{hyde:branch:2006}).
+is minimal in size and faster in time.
+This problem is known to be complex for most CISC architectures (see~\cite{hyde:branch:2006}).
To free the CerCo C compiler from having to consider complications relating to branch displacement, we have chosen to implement an optimising assembler, whose input language the compiler will target.
@@ 111,5 +111,5 @@
Note that the temporal tightness of the simulation is a fundamental prerequisite
of the correctness of the simulation because some functions of the MCS51notably timers and I/Odepend on the microprocessor's clock.
+of the correctness of the simulation because some functions of the MCS51timers and I/Odepend on the microprocessor's clock.
If the pseudo and concrete clock differ the result of an I/O operation may not be preserved.
@@ 146,7 +146,5 @@
with benefits on the size of the formalisation.
The rest of this paper is a detailed description of our proof that is, in minimal part, still a work in progress.

We provide the reader with a brief `roadmap' for the rest of the paper.
+The rest of this paper is a detailed description of our proof that is marginally still a work in progress.
In Section~\ref{sect.matita} we provide a brief overview of the Matita proof assistant for the unfamiliar reader.
In Section~\ref{sect.the.proof} we discuss the design and implementation of the proof proper.
@@ 668,11 +666,11 @@
Polymorphic variants nicely capture the absolutely unorthogonal instruction set of the MCS51 where every opcode must accept its own subset of the 11 addressing mode of the processor.
The second purpose is to single out the sources of incompleteness.
+The second purpose is to single out sources of incompleteness.
By abstracting our functions over the dependent type of correct policies, we were able to manifest the fact that the compiler never refuses to compile a program where a correct policy exists.
This also allowed to simplify the initial proof by dropping lemmas establishing that one function fails if and only if some previous function does so.
Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirelyin user spacethe proof methodology `Russell' of Sozeau~\cite{sozeau:subset:2006}.
However, not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way.
For example, it would be unnatural to see the proof that fetch and assembly commute as the specification of one of the two functions.
+Finally, dependent types, together with Matita's liberal system of coercions, allow us to simulate almost entirely in user space the proof methodology `Russell' of Sozeau~\cite{sozeau:subset:2006}.
+Not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way.
+It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions.
\subsection{Related work}
@@ 681,6 +679,5 @@
% piton
We are not the first to consider the correctness of an assembler for a nontrivial assembly language.
Perhaps the most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}.
This was a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two highlevel languagesa dialect of Lisp and $\mu$Gypsy~\cite{moore:grand:2005}.
+The most impressive piece of work in this domain is the Piton stack~\cite{moore:piton:1996}, a stack of verified components, written and verified in ACL2, ranging from a proprietary FM9001 microprocessor verified at the gate level, to assemblers and compilers for two highlevel languagesLisp and $\mu$Gypsy~\cite{moore:grand:2005}.
% jinja