# Changeset 970

Ignore:
Timestamp:
Jun 15, 2011, 5:59:18 PM (10 years ago)
Message:

commit as i need some money for the communists

Location:
src/ASM/CPP2011
Files:
2 edited

### Legend:

Unmodified
 r969 | long_jump: jump_length. \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. 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. 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} 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: 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'. internal_pseudo_address_map → PseudoStatus → option Status \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: internal_pseudo_address_map → PseudoStatus → option internal_pseudo_address_map \end{lstlisting} Finally, we are able to state and prove our main theorem regarding internal_pseudo_address_map $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} Finally, we are able to state and prove our main theorem relating the execution of a single assembly instruction and the execution of (possibly) many machine code instructions: \begin{lstlisting} lemma main_thm: $\exists$n. execute n s = s''. \end{lstlisting} The statement can be given an intuitive reading as follows. % ---------------------------------------------------------------------------- %