Index: src/ASM/CPP2012asm/cpp2012asm.tex
===================================================================
 src/ASM/CPP2012asm/cpp2012asm.tex (revision 2068)
+++ src/ASM/CPP2012asm/cpp2012asm.tex (revision 2069)
@@ 359,7 +359,15 @@
\subsection{Correctness of the assembler with respect to fetching}
\label{subsect.total.correctness.of.the.assembler}

Using our policies, we now work toward proving the total correctness of the assembler.
By `total correctness', we mean that the assembly process never fails when provided with a correct policy and that the process does not change the semantics of a certain class of well behaved assembly programs.
+
+The aim of this section is to prove the following informal statement:
+when we fetch an assembly pseudoinstruction $I$ at address $ppc$, then
+we can fetch the expanded pseudoinstruction(s) $[J^1;\ldots;J^n] = fetch\_pseudo\_instruction \ldots I~ppc$ from
+$\sigma(ppc)$ in the code memory obtained loading the assembled object code.
+
+This constitutes the first major step in the proof of correctness of the
+assembler, the next one being the simulation of $I$ by $[J^1;\ldots;J^n]$
+(see Section~\ref{???}).
We can express the following lemma, expressing the correctness of the assembly function (slightly simplified):