Index: /src/ASM/CPP2011/cpp2011.tex
===================================================================
 /src/ASM/CPP2011/cpp2011.tex (revision 1027)
+++ /src/ASM/CPP2011/cpp2011.tex (revision 1028)
@@ 278,14 +278,15 @@
This process is iterated for each pseudoinstruction, before the lists are flattened into a single bit list representation of the original assembly program.
%By inspecting the above diagram, it would appear that the best way to proceed with a proof that the assembly process does not change the semantics of an assembly program is via a decomposition of the problem into two subproblems.
+By inspecting the above diagram, it would appear that the best way to proceed with a proof that the assembly process does not change the semantics of an assembly program is by proving the same independently for
+\texttt{expand\_pseudo\_instruction} and for \texttt{assembly1}.
%Namely, we first expand any and all pseudoinstructions into lists of machine instructions, and provide a proof that this process does not change our program's semantics.
%Finally, we assemble all machine code instructions into machine codelists of bytesand prove once more that this process does not have an adverse effect on a program's semantics.
%By composition, we then have that the whole assembly process is semantics preserving.

This is a tempting approach to the proof, but ultimately the wrong approach.
In particular, to expand a pseudoinstruction we need to know the address at which the expanded instructions will be located, for instance to determine if a short jump is possible.
+In particular, to expand a pseudoinstruction we need to know the address at which the expanded instructions will be located, for instance to know if a short jump is possible.
That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded.
Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness.
Therefore we will have lemmas proving correctness for \texttt{assembly1}, and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone.
+Thus, we must assemble each pseudoinstruction into machine code before moving on, and this must be eventually reflected in the proof too.
+Therefore we will have lemmas proving correctness for \texttt{assembly1}, and for the composition of \texttt{assembly1} and
+\texttt{expand\_pseudo\_instruction}, but not for \texttt{expand\_pseudo\_instruction} alone.
%  %