Changeset 1013


Ignore:
Timestamp:
Jun 21, 2011, 1:52:37 AM (8 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1012 r1013  
    345345\end{lstlisting}
    346346
    347 
    348 \begin{lstlisting}
    349 axiom assembly_ok: ∀program,assembled,costs,labels.
    350   Some $\ldots$ $\langle$labels, costs$\rangle$ = build_maps program $\rightarrow$
    351   Some $\ldots$ $\langle$assembled, costs$\rangle$ = assembly program $\rightarrow$
    352   let code_memory := load_code_memory assembled in
     347The following function, \texttt{build\_maps}, is used to construct a pair of mappings from program counters to labels and cost labels, respectively.
     348Cost labels are a technical device used in the CerCo prototype C compiler for proving that the compiler is cost preserving.
     349For our purposes in this paper, they can be safely ignored, though the interested reader may consult~\cite{amadio:certifying:2010} for an overview.
     350
     351The label map, on the other hand, records the position of labels that appear in an assembly program, so that the pseudoinstruction expansion process can replace them with real memory addresses:
     352\begin{lstlisting}
     353definition build_maps:
     354 $\forall$p. $\forall$pol: policy p.
     355 $\Sigma$res : ((BitVectorTrie Word 16) $\times$ (BitVectorTrie Word 16)).
     356   let $\langle$labels, costs$\rangle$ := res in
     357     $\forall$id. occurs_exactly_once id ($\pi_2$ p) $\rightarrow$
     358    let addr := address_of_word_labels_code_mem ($\pi_2$ p) id in
     359      lookup $\ldots$ id labels (zero $\ldots$) = sigma pseudo_program pol addr := $\ldots$
     360\end{lstlisting}
     361The rather complex type of \texttt{build\_maps} owes to our use of Matita's Russell facility to provide a strong specification for the function in the type (c.f. the use of sigma types, through which Russell is implemented in Matita).
     362In particular, we express that any label should only appear exactly in any assembly program, and looking up a label in the newly created map is the same as applying the \texttt{sigma} function, recording the correspondence between pseudo program counters and program counters.
     363
     364Using \texttt{build\_maps}, we can express the following lemma, expressing the correctness of the assembly function:
     365\begin{lstlisting}
     366lemma assembly_ok: $\forall$p,pol,assembled.
     367  let $\langle$labels, costs$\rangle$ := build_maps program pol in
     368  $\langle$assembled,costs$\rangle$ = assembly p pol $\rightarrow$
     369  let cmem := load_code_memory assembled in
    353370  let preamble := $\pi_1$ program in
    354   let datalabels := construct_datalabels preamble in
    355   let lk_labels :=
    356     $\lambda$x. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in
    357   let lk_dlabels := $\lambda$x. lookup ? ? x datalabels (zero ?) in
    358    ∀ppc,len,assembledi.
    359     let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in
    360     let assembly' := assembly_1_pseudoinstruction program ppc
    361       (sigma program ppc) lk_labels lk_dlabels pi in
    362     let newpc := (sigma program ppc) + len in
    363     let echeck :=
    364       encoding_check code_memory (sigma program ppc) slen assembledi in
    365      Some $\ldots$ $\langle$len, assembledi$\rangle$ = assembly' $\rightarrow$
    366       echeck $\wedge$ sigma program newppc = newpc.
    367 \end{lstlisting}
     371  let dlbls := construct_datalabels preamble in
     372  let addr := address_of_word_labels_code_mem ($\pi_2$ program) in
     373  let lk_lbls := λx. sigma program pol (addr x) in
     374  let lk_dlbls := λx. lookup $\ldots$ x datalabels (zero ?) in
     375  $\forall$ppc, pi, newppc.
     376  $\forall$prf: $\langle$pi, newppc$\rangle$ = fetch_pseudo_instruction ($\pi_2$ program) ppc.
     377  $\forall$len, assm.
     378  let spol := sigma program pol ppc in
     379  let spol_len := spol + len in
     380  let echeck := encoding_check cmem spol spol_len assm in
     381  let a1pi := assembly_1_pseudoinstruction in
     382  $\langle$len, assm$\rangle$ = a1pi p pol ppc lk_lbls lk_dlbls pi (refl $\ldots$) (refl $\ldots$) ? $\rightarrow$
     383    echeck $\wedge$ sigma p pol newppc = spol_len.
     384\end{lstlisting}
     385Suppose also we assemble our program \texttt{p} in accordance with a policy \texttt{pol} to obtain \texttt{assembled}, loading the assembled program into code memory \texttt{cmem}.
     386%dpm finish
    368387
    369388Theorem \texttt{fetch\_assembly} establishes that the \texttt{fetch} and \texttt{assembly1} functions interact correctly.
Note: See TracChangeset for help on using the changeset viewer.