Index: Deliverables/D1.2/CompilerProofOutline/outline.tex
===================================================================
 Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1759)
+++ Deliverables/D1.2/CompilerProofOutline/outline.tex (revision 1760)
@@ 383,8 +383,6 @@
\end{center}
Chunks for pointers are pairs made of the original pointer and the index of
the chunk. Therefore, when assembling the chunks together, we can always
recognize if all chunks refer to the same value or if the operation is
meaningless.
+Chunks for pointers are pairs made of the original pointer and the index of the chunk.
+Therefore, when assembling the chunks together, we can always recognize if all chunks refer to the same value or if the operation is meaningless.
The differing memory representations of values in the two memory models imply the need for a series of lemmas on the actions of \texttt{load} and \texttt{store} to ensure correctness.
@@ 395,11 +393,18 @@
That is, if we are successful in reading a value of size $s$ from memory at address $a$ in frontend memory, then we should successfully be able to read a value from memory in the backend memory at \emph{any} address from address $a$ up to and including address $a + i$, where $i \leq s$.
\begin{displaymath}
\sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M)
\end{displaymath}

\begin{displaymath}
\texttt{load}^* (\mathtt{store}\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
\end{displaymath}
+Next, we must show that \texttt{store} properly commutes with the $\sigma$map between memory spaces:
+\begin{displaymath}
+\sigma(\mathtt{store}\ a\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(a)\ \sigma(M)
+\end{displaymath}
+That is, if we store a value \texttt{v} in the frontend memory \texttt{M} at address \texttt{a} and transform the resulting memory with $\sigma$, then this is equivalent to storing a transformed value $\mathtt{\sigma(v)}$ at address $\mathtt{\sigma(a)}$ into the backend memory $\mathtt{\sigma(M)}$.
+
+Finally, we must prove that \texttt{load}, \texttt{store} and $\sigma$ all properly commute.
+Writing \texttt{load}$^*$ for multiple consecutive iterations of \texttt{load}, we must prove:
+\begin{displaymath}
+\texttt{load}^* (\mathtt{store}\ \sigma(a')\ \sigma(v)\ \sigma(M))\ \sigma(a)\ \sigma(M) = \mathtt{load}^*\ \sigma(s)\ \sigma(a)\ \sigma(M)
+\end{displaymath}
+That is, suppose we store a transformed value $\mathtt{\sigma(v)}$ into a backend memory $\mathtt{\sigma(M)}$ at address $\mathtt{\sigma(a')}$, using \texttt{store}, and then load the correct number of bytes (for the size of $\mathtt{\sigma(v)}$ at address $\sigma(a)$.
+Then, this should be equivalent to loading the correct number of bytes from address $\sigma(a)$ in an unaltered version of $\mathtt{\sigma(M)}$, \emph{providing} that the memory regions occupied by the two sequences of bytes at the two addresses do not overlap.
+This will entail more proof obligations, demonstrating that the $\sigma$map between memory spaces respects memory regions.
\begin{displaymath}