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

commit as i need some money for the communists

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r969 r970  
    246246  | long_jump: jump_length.
    247247\end{lstlisting}
    248 
    249248A \texttt{jump\_expansion\_policy} is a map from \texttt{Word}s to \texttt{jump\_length}s, implemented as a trie.
    250249Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump.
     
    252251definition jump_expansion_policy := BitVectorTrie jump_length 16.
    253252\end{lstlisting}
    254 
    255253Next, we require a series of `sigma' functions.
    256254These 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.
     
    261259  pseudo_assembly_program $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$
    262260\end{lstlisting}
    263 
    264261We eventually lift this to functions from program counters to program counters:
    265262\begin{lstlisting}
     
    267264  pseudo_assembly_program $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$
    268265\end{lstlisting}
    269 
    270266Now, it's possible to define what a `good policy' is i.e. one that does not cause \texttt{sigma\_safe} to fail.
    271267As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled:
     
    273269definition policy_ok := $\lambda$p. sigma_safe p $\neq$ None $\ldots$.
    274270\end{lstlisting}
    275 
    276271Finally, we obtain \texttt{sigma}, a map from program counters to program counters, which is guranteed not to fail as we internally provide a that
    277272\begin{lstlisting}
    278273definition sigma: pseudo_assembly_program $\rightarrow$ Word $\rightarrow$ Word := $\ldots$
    279274\end{lstlisting}
    280 
    281275An \texttt{internal\_pseudo\_address\_map} positions in the memory of a \texttt{PseudoStatus} with a physical memory address.
    282276\begin{lstlisting}
    283277definition internal_pseudo_address_map := list (BitVector 8).
    284278\end{lstlisting}
    285 
    286279We 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}.
    287280Notice, the MCS-51's internal RAM is addressed with a 7-bit `byte'.
     
    302295 internal_pseudo_address_map → PseudoStatus → option Status
    303296\end{lstlisting}
    304 
    305297After fetching an assembly instruction we must update any \texttt{internal\_pseudo\hyp{}\_address\_map}s that may be laying around.
    306298This is done with the following function:
    307299\begin{lstlisting}
    308300definition next_internal_pseudo_address_map0:
    309  internal_pseudo_address_map → PseudoStatus → option internal_pseudo_address_map
    310 \end{lstlisting}
    311 
    312 Finally, we are able to state and prove our main theorem regarding
     301 internal_pseudo_address_map $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map
     302\end{lstlisting}
     303Finally, 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:
    313304\begin{lstlisting}
    314305lemma main_thm:
     
    321312              $\exists$n. execute n s = s''.
    322313\end{lstlisting}
     314The statement can be given an intuitive reading as follows.
     315
    323316
    324317% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.