Index: /src/ASM/CPP2011/cpp-2011.tex
===================================================================
--- /src/ASM/CPP2011/cpp-2011.tex (revision 1015)
+++ /src/ASM/CPP2011/cpp-2011.tex (revision 1016)
@@ -292,8 +292,9 @@
| long_jump: jump_length.
\end{lstlisting}
-A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s, implemented as a trie.
+A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s. Efficient implementations
+of policies are based on tries.
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.
+definition policy_type ≝ Word → jump_length.
\end{lstlisting}
Next, we require a series of `sigma' functions.
@@ -302,5 +303,5 @@
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
+definition sigma0: pseudo_assembly_program $\rightarrow$ policy_type
$\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
\end{lstlisting}
@@ -311,14 +312,18 @@
\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.
-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 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:
+ pseudo_assembly_program $\rightarrow$ policy_type $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
+\end{lstlisting}
+Now, it's possible to define what a `good policy' is for a program \texttt{p}.
+A policy \texttt{pol} is deemed good when it prevents \texttt{sigma\_safe} from failing on \texttt{p}. Failure is only possible when the policy prescribes
+short/middle jumps to too far locations or when the prouced object code does
+not fit in code memory. A \texttt{policy} for a program \texttt{p}
+is a policy that is good for \texttt{p}.
+\begin{lstlisting}
+definition policy_ok := $\lambda$pol.$\lambda$p. sigma_safe p $\neq$ None $\ldots$.
+definition policy ≝ λp. $\Sigma$jump_expansion:policy_type. policy_ok jump_expansion p.
+\end{lstlisting}
+Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters that takes in input a good policy and thus never fails. Note how
+we avoid failure here and in most of the remaining functions by restricting
+the domain using the dependent type \texttt{policy}.
\begin{lstlisting}
definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$