Changeset 976

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

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

1 edited


  • src/ASM/CPP2011/cpp-2011.tex

    r974 r976  
    178178For those familiar with Coq, Matita's syntax and mode of operation should be entirely familiar.
    179179We take time here to explain one of Matita's syntactic idiosyncracies, however.
    180 The use of `$\mathtt{\ldots}$' or `$\mathtt{?}$' in an argument position denotes a type to be inferred automatically by unification.
     180The use of `$\mathtt{?}$' or `$\mathtt{\ldots}$' in an argument position denotes a type or types to be inferred automatically by unification respectively.
    181181The 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.
    288288\subsection{Total correctness of the assembler}
     291Using our policies, we now work toward proving the total correctness of the assembler.
     292By total correctness, we mean that the assembly process does not change the semantics of an assembly program.
     293Naturally, this necessitates keeping some sort of correspondence between program counters at the assembly level, and program counters at the machine code level.
     294For this, we use the \texttt{sigma} machinery defined at the end of Subsection~\ref{subsect.policies}.
    291296CSC: no options using policy
     317We expand pseudoinstructions using the function \texttt{expand\_pseudo\_instruction}.
     318This 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.
     319This \texttt{policy\_decision} is asssumed to originate from a policy as defined in Subsection~\ref{subsect.policies}.
    313321definition expand_pseudo_instruction:
    314322  ∀lookup_labels, lookup_datalabels, pc, policy_decision.
    315     pseudo_instruciton $\rightarrow$ option list instruction := $\ldots$
    316 \end{lstlisting}
     323    pseudo_instruction $\rightarrow$ option list instruction := $\ldots$
     325Under the assumption that a correct policy exists, \texttt{expand\_pseudo\_instruction} should never fail, and therefore the option type may be dispensed with.
     326This 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.
     327For 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}.
     350Lemma \texttt{fetch\_assembly\_pseudo} establishes the correctness of expanding and then assembling pseudoinstructions:
    340352lemma fetch_assembly_pseudo: $\forall$program, ppc, lk_labels, lk_dlabels.
    342354  let jexp := jump_expansion ppc program in
    343355  let exp :=
    344     expand_pseudo_instruction lookup_labels lookup_datalabels pc jexp pi
     356    expand_pseudo_instruction lk_labels lk_dlabels pc jexp pi
    345357  let ass :=
    346358    assembly_1_pseudoinstruction program ppc pc lk_labels lk_dlabels pi in
    350362        fetch_many code_memory (pc + len) pc instructions.
     364Here, \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.
     365The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks.
     367Intuitively, lemma \texttt{fetch\_assembly\_pseudo} can be read as follows.
     368Suppose 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}.
     369Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{jexp}, obtaining an (optional) list of machine code instructions \texttt{exp}.
     370Suppose we also
    354373theorem fetch_assembly: $\forall$pc, i, cmem, assembled.
    355374  assembled = assembly1 i $\rightarrow$
    356   let len := length ... assembled in
     375  let len := length $\ldots$ assembled in
    357376    encoding_check cmem pc (pc + len) assembled $\rightarrow$
    358377    let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in
    359378    let $\langle$instr_pc, ticks$\rangle$ := fetched in
    360     let $\langle$instr,pc'$\rangle$ := instr_pc in
     379    let $\langle$instr, pc'$\rangle$ := instr_pc in
    361380      (eq_instruction instr i $\wedge$
    362381       eqb ticks (ticks_of_instruction instr) $\wedge$
    398417theorem main_thm:
    399418  ∀M,M',ps,s,s''.
    400     next_internal_pseudo_address_map M ps = Some ... M' $\rightarrow$
    401       status_of_pseudo_status M ps = Some ... s $\rightarrow$
     419    next_internal_pseudo_address_map M ps = Some $\ldots$ M' $\rightarrow$
     420      status_of_pseudo_status M ps = Some $\ldots$ s $\rightarrow$
    402421        status_of_pseudo_status M'
    403422          (execute_1_pseudo_instruction
    404             (ticks_of (code_memory ... ps)) ps) = Some ... s'' $\rightarrow$
     423            (ticks_of (code_memory $\ldots$ ps)) ps) = Some $\ldots$ s'' $\rightarrow$
    405424              $\exists$n. execute n s = s''.
    419   \begin{itemize}
    420    \item use of dependent types to throw away wrong programs that would made
    421     the statement for completeness complex. E.g. misuse of addressing modes,
    422     jumps to non existent labels, etc.
    423    \item try to go for small reflection; avoid inductive predicates that require
    424     tactics (inversion, etc.) that do not work well with dependent types; small
    425     reflection usually does
    426    \item use coercions to simulate Russell; mix together the proof styles
    427     a la Russell (for situations with heavy dependent types) and the standard
    428     one
    429   \end{itemize}
     438We have proved the total correctness of an assembler for MCS-51 assembly language.
     439In 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.
    431441\subsection{Use of dependent types and Russell}
Note: See TracChangeset for help on using the changeset viewer.