Changeset 969 for src

Timestamp:

Jun 15, 2011, 5:27:48 PM (10 years ago)

Author:

mulligan

Message:

more work on paper, nearly finished policy discussion

File:

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

src/ASM/CPP2011/cpp-2011.tex

@@ -9 +9 @@
 \usepackage{graphicx}
 \usepackage[colorlinks]{hyperref}
+\usepackage{hyphenat}
 \usepackage[utf8x]{inputenc}
 \usepackage{listings}
@@ -257 +258 @@
 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$
+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$
+definition sigma_safe:
+  pseudo_assembly_program $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
 \end{lstlisting}
 
@@ -270 +271 @@
 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:
- ∀p:pseudo_assembly_program.
-  ∀policy. policy_ok policy p. Word → Word
-\end{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$
+\end{lstlisting}
+
+An \texttt{internal\_pseudo\_address\_map} positions in the memory of a \texttt{PseudoStatus} with a physical memory address.
+\begin{lstlisting}
+definition internal_pseudo_address_map := list (BitVector 8).
+\end{lstlisting}
+
+We use \texttt{internal\_pseudo\_address\_map}s to convert the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}.
+Notice, the MCS-51's internal RAM is addressed with a 7-bit `byte'.
+% dpm: ugly English, fix
+The whole of the internal RAM space is addressed with bytes: the first bit is used to distinguish between the programmer addressing low and high internal memory.
 \begin{lstlisting}
 axiom low_internal_ram_of_pseudo_low_internal_ram:
- ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7.
-\end{lstlisting}
-
-CSC: no option using policy 
+  internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7.
+\end{lstlisting}
+A similar axiom exists for high internal RAM.
+
+Next, we are able to translate \texttt{PseudoStatus} records into \texttt{Status} records using \texttt{status\_of\_pseudo\_status}.
+Translating a \texttt{PseudoStatus}'s code memory requires we expand pseudoinstructions and then assemble to obtain a trie of bytes.
+This can fail, as mentioned, in a limited number of situations, related to improper use of labels in an assembly program.
+However, it is possible to `tighten' the type of \texttt{status\_of\_pseudo\_status}, removing the option type, by using the fact that if any `good policy' exists, assembly will never fail.
 \begin{lstlisting}
 definition status_of_pseudo_status:
@@ -291 +303 @@
 \end{lstlisting}
 
+After fetching an assembly instruction we must update any \texttt{internal\_pseudo\hyp{}\_address\_map}s that may be laying around.
+This is done with the following function:
 \begin{lstlisting}
 definition next_internal_pseudo_address_map0:
@@ -296 +310 @@
 \end{lstlisting}
 
-CSC: no 2nd, 3rd options using policy 
-\begin{lstlisting}
- ∀M,M',ps,s,s''.
-  next_internal_pseudo_address_map M ps = Some ... M' →
-  status_of_pseudo_status M ps = Some ... s →
-  status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory ... ps)) ps) = Some ... s'' →
-   ∃n. execute n s = s''.
-\end{lstlisting}
+Finally, we are able to state and prove our main theorem regarding 
+\begin{lstlisting}
+lemma main_thm:
+  ∀M,M',ps,s,s''.
+    next_internal_pseudo_address_map M ps = Some ... M' $\rightarrow$
+      status_of_pseudo_status M ps = Some ... s $\rightarrow$
+        status_of_pseudo_status M'
+          (execute_1_pseudo_instruction 
+            (ticks_of (code_memory ... ps)) ps) = Some ... s'' $\rightarrow$
+              $\exists$n. execute n s = s''.
+\end{lstlisting}
+
+% ---------------------------------------------------------------------------- %
+% SECTION                                                                      %
+% ---------------------------------------------------------------------------- %
+\subsection{Proof of correctness}
+\label{subsect.proof.of.correctness}
 
 CSC: no options using policy