# Changeset 976

Ignore:
Timestamp:
Jun 16, 2011, 12:02:07 PM (9 years ago)
Message:

more changes, rearranged paper to put lemmas/defns in correct order, leading up to main theorem

File:
1 edited

### Legend:

Unmodified
 r974 For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar. We take time here to explain one of Matita's syntactic idiosyncracies, however. The use of $\mathtt{\ldots}$' or $\mathtt{?}$' in an argument position denotes a type to be inferred automatically by unification. The use of $\mathtt{?}$' or $\mathtt{\ldots}$' in an argument position denotes a type or types to be inferred automatically by unification respectively. The use of $\mathtt{?}$' in the body of a definition, lemma or axiom denotes an incomplete term that is to be closed, by hand, using tactics. \subsection{Total correctness of the assembler} \label{subsect.total.correctness.of.the.assembler} Using our policies, we now work toward proving the total correctness of the assembler. By total correctness, we mean that the assembly process does not change the semantics of an assembly program. Naturally, this necessitates keeping some sort of correspondence between program counters at the assembly level, and program counters at the machine code level. For this, we use the \texttt{sigma} machinery defined at the end of Subsection~\ref{subsect.policies}. CSC: no options using policy \end{lstlisting} We expand pseudoinstructions using the function \texttt{expand\_pseudo\_instruction}. This function accepts a policy decision'---an element of type \texttt{jump\_length}---that is used when expanding a \texttt{Call}, \texttt{Jmp} or conditional jump to a label into the correct machine instruction. This \texttt{policy\_decision} is asssumed to originate from a policy as defined in Subsection~\ref{subsect.policies}. \begin{lstlisting} definition expand_pseudo_instruction: ∀lookup_labels, lookup_datalabels, pc, policy_decision. pseudo_instruciton $\rightarrow$ option list instruction := $\ldots$ \end{lstlisting} pseudo_instruction $\rightarrow$ option list instruction := $\ldots$ \end{lstlisting} Under the assumption that a correct policy exists, \texttt{expand\_pseudo\_instruction} should never fail, and therefore the option type may be dispensed with. This is because the only failure conditions for \texttt{expand\_pseudo\_instruction} result from trying to expand a pseudoinstruction into an impossible' combination of machine code instructions. For instance, if the policy decision dictates that we should expand a \texttt{Call} pseudoinstruction into a short jump', then we fail, as the MCS-51's instruction set only features instructions \texttt{ACALL} and \texttt{LCALL}. \begin{lstlisting} \end{lstlisting} Lemma \texttt{fetch\_assembly\_pseudo} establishes the correctness of expanding and then assembling pseudoinstructions: \begin{lstlisting} lemma fetch_assembly_pseudo: $\forall$program, ppc, lk_labels, lk_dlabels. let jexp := jump_expansion ppc program in let exp := expand_pseudo_instruction lookup_labels lookup_datalabels pc jexp pi expand_pseudo_instruction lk_labels lk_dlabels pc jexp pi let ass := assembly_1_pseudoinstruction program ppc pc lk_labels lk_dlabels pi in fetch_many code_memory (pc + len) pc instructions. \end{lstlisting} Here, \texttt{len} is the number of machine code instructions the pseudoinstruction at hand has been expanded into, \texttt{encoding\_check} is a recursive function that checks for any possible corruption of the code memory, resulting from expanding the pseudoinstruction. The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks. Intuitively, lemma \texttt{fetch\_assembly\_pseudo} can be read as follows. Suppose our policy \texttt{jump\_expansion} dictates that the pseudoinstruction indexed by the pseudo program counter \texttt{ppc} in assembly program \texttt{program} gives us the policy decision \texttt{jexp}. 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 \begin{lstlisting} theorem fetch_assembly: $\forall$pc, i, cmem, assembled. assembled = assembly1 i $\rightarrow$ let len := length ... assembled in let len := length $\ldots$ assembled in encoding_check cmem pc (pc + len) assembled $\rightarrow$ let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in let $\langle$instr_pc, ticks$\rangle$ := fetched in let $\langle$instr,pc'$\rangle$ := instr_pc in let $\langle$instr, pc'$\rangle$ := instr_pc in (eq_instruction instr i $\wedge$ eqb ticks (ticks_of_instruction instr) $\wedge$ theorem 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$ next_internal_pseudo_address_map M ps = Some $\ldots$ M' $\rightarrow$ status_of_pseudo_status M ps = Some $\ldots$ s $\rightarrow$ status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory ... ps)) ps) = Some ... s'' $\rightarrow$ (ticks_of (code_memory $\ldots$ ps)) ps) = Some $\ldots$ s'' $\rightarrow$ $\exists$n. execute n s = s''. \end{lstlisting} \label{sect.conclusions} \begin{itemize} \item use of dependent types to throw away wrong programs that would made the statement for completeness complex. E.g. misuse of addressing modes, jumps to non existent labels, etc. \item try to go for small reflection; avoid inductive predicates that require tactics (inversion, etc.) that do not work well with dependent types; small reflection usually does \item use coercions to simulate Russell; mix together the proof styles a la Russell (for situations with heavy dependent types) and the standard one \end{itemize} We have proved the total correctness of an assembler for MCS-51 assembly language. In particular, our assembly language featured labels, arbitrary conditional and unconditional jumps to labels, global data and instructions for moving this data into the MCS-51's single 16-bit register. \subsection{Use of dependent types and Russell}