Changeset 976 for src/ASM/CPP2011

Timestamp:

Jun 16, 2011, 12:02:07 PM (10 years ago)

Author:

mulligan

Message:

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

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (8 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -178 +178 @@
 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.
 
@@ -288 +288 @@
 \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 
@@ -310 +315 @@
 \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}
@@ -337 +348 @@
 \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.
@@ -342 +354 @@
   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
@@ -350 +362 @@
         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$
@@ -398 +417 @@
 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}
@@ -417 +436 @@
 \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}