# Changeset 1012

Ignore:
Timestamp:
Jun 21, 2011, 12:33:55 AM (8 years ago)
Message:

just a few things left to change

File:
1 edited

### Legend:

Unmodified
 r1011 pseudo_instruction $\rightarrow$ list instruction := $\ldots$ \end{lstlisting} \begin{lstlisting} \end{lstlisting} % dpm todo Theorem \texttt{fetch\_assembly} establishes that the \texttt{fetch} and \texttt{assembly1} functions interact correctly. The \texttt{fetch} function, as its name implies, fetches the instruction indexed by the program counter in the code memory, while \texttt{assembly1} maps a single instruction to its byte encoding: \begin{lstlisting} theorem fetch_assembly: $\forall$pc, i, cmem, assembled. eq_bv $\ldots$ pc' (pc + len)) = true. \end{lstlisting} In particular, we read \texttt{fetch\_assembly} as follows. Given an instruction, \texttt{i}, we first assemble the instruction to obtain \texttt{assembled}, checking that the assembled instruction was stored in code memory correctly. Fetching from code memory, we obtain \texttt{fetched}, a tuple consisting of the instruction, new program counter, and the number of ticks this instruction will take to execute. Deconstructing these tuples, we finally check that the fetched instruction is the same instruction that we began with, and the number of ticks this instruction will take to execute is the same as the result returned by a lookup function, \texttt{ticks\_of\_instruction}, devoted to tracking this information. Or, in plainer words, assembling and then immediately fetching again gets you back to where you started. Lemma \texttt{fetch\_assembly\_pseudo} establishes a basic relationship between \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}: Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{jexp}, obtaining an (optional) list of machine code instructions \texttt{exp}. Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{ass}, a list of bytes. Then, under the assumption that neither the expansion of the pseudoinstruction to obtain \texttt{exp}, nor the assembly of the pseudoinstruction to obtain \texttt{ass}, failed, we check with \texttt{fetch\_many} that the number of machine instructions that were fetched matches the number of instruction that \texttt{expand\_pseudo\_instruction} expanded. Then, we check with \texttt{fetch\_many} that the number of machine instructions that were fetched matches the number of instruction that \texttt{expand\_pseudo\_instruction} expanded. At first sight, Lemma \texttt{fetch\_assembly\_pseudo2} appears to nearly establish the correctness of the assembler: $\exists$instrs. Some ? instrs = instructions' $\wedge$ fetched instrs. \end{lstlisting} Intuitively, we may read \texttt{fetch\_assembly\_pseudo2} as follows. Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{code\_memory}. In particular, \texttt{fetch\_assembly\_pseudo2} says nothing about how memory addresses evolve during assembly. Memory addresses in one memory space may be mapped to memory addresses in a completely different memory space during assembly. To handle this problem, we need some more machinery. To handle this problem, we need some more machinery in order to track how memory addresses are moved around, and to record a correspondence between addresses at the pseudo assembly level and the machine code level. We use an \texttt{internal\_pseudo\_address\_map} for this purpose. An \texttt{internal\_pseudo\_address\_map} associates positions in the memory of a \texttt{PseudoStatus} with a physical memory address: An \texttt{internal\_pseudo\_address\_map} associates memory addresses in the lower internal RAM of a \texttt{PseudoStatus} with a physical memory address at the machine code level: \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}. We use a map associating memory addresses, of type \texttt{internal\_pseudo\_address\_map}, to convert the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}. The actual conversion process is performed by \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram}:\footnote{An associated set of axioms describe how \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} behaves.  This is a form of parametricity.  We don't care about the particulars of the conversion functions, as long as they behave in accordance with our axioms.} \begin{lstlisting} axiom low_internal_ram_of_pseudo_low_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: internal_pseudo_address_map → PseudoStatus → option Status \end{lstlisting} This should never fail, providing that our policy is correct: \begin{lstlisting} definition status_of_pseudo_status: internal_pseudo_address_map $\rightarrow$ $\forall$ps:PseudoStatus. policy (code_memory $\ldots$ ps) $\rightarrow$ 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: $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} The function \texttt{ticks\_of} computes how long---in clock cycles---a pseudoinstruction will take to execute when expanded in accordance with a given policy. The function returns a pair of natural numbers, needed for recording the execution times of each branch of a conditional jump. \begin{lstlisting} definition ticks_of: $\forall$p:pseudo_assembly_program. policy p $\rightarrow$ Word $\rightarrow$ nat $\times$ nat := $\ldots$ \end{lstlisting} Finally, we are able to state and prove our main theorem. This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions. That is, the assembly process preserves the semantics of an assembly program, as it is translated into machine code: This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions, as long . That is, the assembly process preserves the semantics of an assembly program, as it is translated into machine code, as long as we are able to track memory addresses properly: \begin{lstlisting} theorem main_thm: The statement can be given an intuitive reading as follows. Suppose our \texttt{PseudoStatus}, \texttt{ps}, can be successfully converted into a \texttt{Status}, \texttt{s}. Suppose further that, after executing a single assembly instruction and converting the resulting \texttt{PseudoStatus} into a \texttt{Status}, we obtain \texttt{s''}, being careful to track the number of ticks executed. Suppose further that, after executing a single assembly instruction and converting the resulting \texttt{PseudoStatus} into a \texttt{Status}, making sure to map memory addresses at the pseudo assembly level to memory addresses at the machine level correctly, we obtain \texttt{s''}, being careful to track the number of ticks executed with \texttt{ticks\_of}. Then, there exists some number \texttt{n}, so that executing \texttt{n} machine code instructions in \texttt{Status} \texttt{s} gives us \texttt{Status} \texttt{s''}. Theorem \texttt{main\_thm} establishes the correctness of the assembly process. The bulk of the proof described herein is contained in a single file, \texttt{AssemblyProof.ma}, consisting of approximately 3000 lines of Matita source. We admit to using a number of axioms in our development. We do not believe the use of these axioms has been particularly onerous---very few concern anything more interesting than, say, stating that converting from a natural number to a bitvector and back again is the identity---and what axioms remain are rapidly being closed as work continues. \bibliography{cpp-2011.bib}