# Changeset 969 for src/ASM/CPP2011

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

more work on paper, nearly finished policy discussion

File:
1 edited

### Legend:

Unmodified
 r968 \usepackage{graphicx} \usepackage[colorlinks]{hyperref} \usepackage{hyphenat} \usepackage[utf8x]{inputenc} \usepackage{listings} 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} 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: \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: \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