Changeset 1010

Timestamp:

Jun 20, 2011, 6:18:39 PM (9 years ago)

Author:

mulligan

Message:

more added, finished up to end of subsect 3.2

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (2 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -300 +300 @@
 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 pseudo program counters to program counters.
-This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails:
+This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction\_safe} fails, which happens if a jump pseudoinstruction is expanded incorrectly:
 \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:
+Here, the returned \texttt{BitVectorTrie} is a map between pseudo program counters and program counters, and is constructed by successively expanding pseudoinstructions and incrementing the two program counters the requisite amount to keep them in correct correspondence.
+The two natural numbers returned are the maximum values that the two program counters attained.
+
+We eventually lift this to functions from pseudo program counters to program counters, implemented as \texttt{Word}s:
 \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.
+Now, it's possible to define what a `good policy' is.
+A policy is deemed good when it prevents \texttt{sigma\_safe} from ever failing.
 As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
 \begin{lstlisting}
 definition policy_ok := $\lambda$p. sigma_safe 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 internally provide a that 
-\begin{lstlisting}
-definition sigma: pseudo_assembly_program $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
+Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters which incorporates, depending also on a policy.
+This is a thin shell around \texttt{sigma\_safe}, and dispenses with the option type via a proof that \texttt{sigma\_safe} never fails under the assumption that a supplied policy is correct:
+\begin{lstlisting}
+definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
 \end{lstlisting}
 
@@ -328 +333 @@
 Using our policies, we now work toward proving the total correctness of the assembler.
 By total correctness, we mean that the assembly process does not change the semantics of an assembly program.
-Naturally, this necessitates keeping some sort of correspondence between program counters at the assembly level, and program counters at the machine code level.
+Naturally, this necessitates keeping some sort of correspondence between addresses at the assembly level and addresses at the machine code level.
 For this, we use the \texttt{sigma} machinery defined at the end of Subsection~\ref{subsect.policies}.