Index: /src/ASM/CPP2011/cpp2011.tex
===================================================================
 /src/ASM/CPP2011/cpp2011.tex (revision 967)
+++ /src/ASM/CPP2011/cpp2011.tex (revision 968)
@@ 213,5 +213,8 @@
Notice, here, that the emulation function for pseudoprograms takes an additional argument.
This is a function that maps program counters (for the pseudoprogram) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion.
We require \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in the number of clock ticks needed for execution.
+We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions.
+If we change how we expand conditional jumps to labels, for instance, then the costing needs to change, hence \texttt{execute\_1\_pseudo\_instruction}'s parametricity in the costing.
+
+The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the `true branch' and `false branch' may differ in the number of clock ticks needed for execution.
This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}.
During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es.
@@ 233,6 +236,9 @@
\label{subsect.policies}
\begin{lstlisting}
inductive jump_length: Type[0] ≝
+Policies exist to dictate how conditional and unconditional jumps at the assembly level should be expanded into machine code instructions.
+Using policies, we are able to completely decouple the decision over how jumps are expanded with the act of expansion, simplifying our proofs.
+As mentioned, the MCS51 instruction set includes three different jump instructions: \texttt{SJMP}, \texttt{AJMP} and \texttt{LJMP}; call these `short', `medium' and `long' jumps, respectively:
+\begin{lstlisting}
+inductive jump_length: Type[0] :=
 short_jump: jump_length
 medium_jump: jump_length
@@ 240,12 +246,32 @@
\end{lstlisting}
\begin{lstlisting}
definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
\end{lstlisting}

\begin{lstlisting}
definition policy_ok := λpolicy.λp. sigma_safe policy p <> None ....
\end{lstlisting}

+A \texttt{jump\_expansion\_policy} is a map from \texttt{Word}s to \texttt{jump\_length}s, implemented as a trie.
+Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump.
+\begin{lstlisting}
+definition jump_expansion_policy := BitVectorTrie jump_length 16.
+\end{lstlisting}
+
+Next, we require a series of `sigma' functions.
+These functions map assembly program counters to their machine code counterparts, establishing the correspondence between `positions' in an assembly program and `positions' in a machine code program.
+At the heart of this process is \texttt{sigma0} which traverses an assembly program building maps from program counter to program counter.
+This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails:
+\begin{lstlisting}
+definition sigma0: pseudo_assembly_program
+ $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
+\end{lstlisting}
+
+We eventually lift this to functions from program counters to program counters:
+\begin{lstlisting}
+definition sigma_safe: pseudo_assembly_program
+ $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
+\end{lstlisting}
+
+Now, it's possible to define what a `good policy' is i.e. one that does not cause \texttt{sigma\_safe} to fail.
+As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
+\begin{lstlisting}
+definition policy_ok := $\lambda$policy. $\lambda$p. sigma_safe policy p $\neq$ None $\ldots$.
+\end{lstlisting}
+
+Finally, we obtain \texttt{sigma}, a map from program counters to program counters, which is guranteed not to fail, as we must provide a proof that our policy at hand is a `good policy'.
\begin{lstlisting}
definition sigma: