Index: /Papers/cpp-asm-2012/cpp-2012-asm.tex
===================================================================
--- /Papers/cpp-asm-2012/cpp-2012-asm.tex (revision 2344)
+++ /Papers/cpp-asm-2012/cpp-2012-asm.tex (revision 2345)
@@ -182,4 +182,47 @@
\label{sect.the.proof}
+The aim of the section is to explain the main ideas and steps of the certified
+proof of correctness for an optimizing assembler for the MCS-8051. The
+formalization is available at~\url{http://cerco.cs.unibo.it}.
+
+In Section~\ref{subsect.machine.code.semantics} we sketch an operational
+semantics (a realistic and efficient emulator) for the MCS-8051.
+We also introduce a syntax for decoded instructions that will be reused for
+the assembly language.
+
+In Section~\ref{subsect.assembly.code.semantics} we describe the assembly code
+language and operational semantics. The latter is parametric in the cost model
+that will be induced by the assembler. It fully reuses the semantics of the
+machine code on all ``real'' (i.e. non pseudo) instructions.
+
+Branch displacement policies are introduced in
+Section~\ref{subsect.the.assembler} where we
+also describe the assembler as a function over policies as previously described.
+
+The proof of correctness of the assembler consists in showing that the
+object code given in output together with a cost model for the source program
+simulates the source program executed using that cost model. The proof
+can be divided into two main lemmas. The first is correctness with respect
+to fetching, described in
+Section~\ref{subsect.total.correctness.of.the.assembler}. It roughly
+states that one step of fetching at the assembly level that returns the
+decoded instruction $I$ is simulated by
+$n$ steps of fetching at object level that return instructions
+$J_1,\ldots,J_n$, where $J_1,\ldots,J_n$ is, among the possible expansions
+of $I$, the one picked by the policy.
+The second lemma shows that $J_1,\ldots,J_n$ simulates $I$ but only if
+the $I$ is well-behaved, i.e. it manipulates addresses in ways that are
+anticipated in the correctness proof. To keep track of the well-behaved ways,
+we couple the assembly status with a map that records where addresses are
+currently stored in memory or in the registers. Then we introduce a dynamic
+checking function that inspects the assembly status and the map to determine
+if the operation is well behaved. A positive answer is the pre-condition of
+the lemma. The second lemma is part of
+Section~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}
+where we also establish \emph{total correctness} of our assembler as a
+composition of the two lemmas: programs that are well behaved when executed
+under the cost model induced by the compiler are correctly simulated by the
+compiled code.
+
% ---------------------------------------------------------------------------- %
% SECTION %