Changeset 1029 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 21, 2011, 2:23:42 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r1028 r1029  
    224224 For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$.
    225225This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
    226 In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq.
     226In this way, Matita supports the ``Russell'' proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq.
    227227
    228228% ---------------------------------------------------------------------------- %
     
    301301\begin{lstlisting}
    302302inductive jump_length: Type[0] :=
    303   | short_jump: jump_length
    304   | medium_jump: jump_length
    305   | long_jump: jump_length.
     303  |short_jump:jump_length |medium_jump:jump_length |long_jump:jump_length.
    306304\end{lstlisting}
    307305
     
    384382      lookup $\ldots$ id labels (zero $\ldots$) = sigma pseudo_program pol addr := $\ldots$
    385383\end{lstlisting}
    386 The 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).
     384The 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 and coercions, through which Russell is simulated in Matita).
    387385We express that for all labels that appear exactly once in any assembly program, the newly created map used in the implementation, and the stronger \texttt{sigma} function used in the specification, agree.
    388386
     
    415413The \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:
    416414\begin{lstlisting}
    417 theorem fetch_assembly: $\forall$pc, i, cmem, assembled.
    418   assembled = assembly1 i $\rightarrow$
     415theorem fetch_assembly: $\forall$pc, i, cmem, assembled.  assembled=assembly1 i $\rightarrow$
    419416  let len := length $\ldots$ assembled in
    420     encoding_check cmem pc (pc + len) assembled $\rightarrow$
     417  encoding_check cmem pc (pc + len) assembled $\rightarrow$
    421418    let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in
    422419    let $\langle$instr_pc, ticks$\rangle$ := fetched in
    423420    let $\langle$instr, pc'$\rangle$ := instr_pc in
    424       (eq_instruction instr i $\wedge$
    425        eqb ticks (ticks_of_instruction instr) $\wedge$
     421      (eq_instruction instr i $\wedge$ eqb ticks (ticks_of_instruction instr) $\wedge$
    426422       eq_bv $\ldots$ pc' (pc + len)) = true.
    427423\end{lstlisting}
     
    436432lemma fetch_assembly_pseudo:
    437433 ∀program.∀pol:policy program.∀ppc.∀code_memory.
    438   let pi := fst (fetch_pseudo_instruction (snd program) ppc) in
     434  let pi := $\pi_1$ (fetch_pseudo_instruction ($\pi_2$ program) ppc) in
    439435  let instructions := expand_pseudo_instruction program pol ppc ... in
    440436  let $\langle$len,assembled$\rangle$ := assembly_1_pseudoinstruction program pol ppc ... in
     
    447443
    448444Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} can be read as follows.
    449 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{pol}.
    450 Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{pol}, obtaining the list of machine code instructions \texttt{instructions}.
     445Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{pol}, obtaining the list of machine code instructions \texttt{instructions}.
    451446Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{assembled}, a list of bytes.
    452447Then, 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.
    453448
    454449The final lemma in this series is \texttt{fetch\_assembly\_pseudo2} that combines the Lemma \texttt{fetch\_aasembly\_pseudo} with the correctness of the functions that load object code into the processor's memory.
    455 At first, the lemmas appears to nearly establish the correctness of the assembler:
    456450\begin{lstlisting}
    457451lemma fetch_assembly_pseudo2:
    458452 ∀program,pol,ppc.
    459453  let $\langle$labels,costs$\rangle$ := build_maps program pol in
    460   let assembled := \fst (assembly program pol) in
     454  let assembled := $\pi_1$ (assembly program pol) in
    461455  let code_memory := load_code_memory assembled in
    462   let data_labels := construct_datalabels (\fst program) in
     456  let data_labels := construct_datalabels ($\pi_1$ program) in
    463457  let lookup_labels :=
    464     λx. sigma $\ldots$ pol (address_of_word_labels_code_mem (\snd program) x) in
     458    λx. sigma $\ldots$ pol (address_of_word_labels_code_mem ($\pi_2$ program) x) in
    465459  let lookup_datalabels := λx. lookup ? ? x data_labels (zero ?) in
    466   let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction (\snd program) ppc in
    467   let instructions ≝ expand_pseudo_instruction program pol ppc ... in
    468    fetch_many code_memory (sigma program pol newppc)
    469      (sigma program pol ppc) instructions.
     460  let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in
     461  let instrs ≝ expand_pseudo_instruction program pol ppc ... in
     462   fetch_many code_memory (sigma $\ldots$ pol newppc) (sigma $\ldots$ pol ppc) instrs.
    470463\end{lstlisting}
    471464
     
    475468The fetched sequence corresponds to the expansion, according to \texttt{pol}, of the pseudoinstruction.
    476469
     470At first, the lemmas appears to immediately imply the correctness of the assembler.
    477471However, this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process since it does not establish the correspondence between the semantics of a pseudo-instruction and that of its expansion.
    478472In particular, the two semantics differ on instructions that \emph{could} directly manipulate program addresses.
     
    513507\begin{lstlisting}
    514508axiom low_internal_ram_of_pseudo_low_internal_ram:
    515   internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7.
     509 internal_pseudo_address_map$\rightarrow$BitVectorTrie Byte 7$\rightarrow$BitVectorTrie Byte 7.
    516510\end{lstlisting}
    517511
     
    526520The \texttt{next\_internal\_pseudo\_address\_map} function is responsible for run time monitoring of the behaviour of assembly programs, in order to detect well behaved ones.
    527521It returns a map that traces memory addresses in internal RAM after execution of the next pseudoinstruction, failing when the instruction tampers with memory addresses in unanticipated (but potentially correct) ways.
    528 It thus decides the membership of a correct but not complete subset of well behaved programs.
     522It thus decides the membership of a strict subset of the set of well behaved programs.
    529523\begin{lstlisting}
    530524definition next_internal_pseudo_address_map: internal_pseudo_address_map
     
    581575However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory.
    582576In this respect, there is a trade-off between the completeness of the assembler and the efficiency of the assembled program.
    583 The definition and proof of an complete, optimal (in the sense that jump pseudoinstructions are expanded to the smallest possible opcode) and correct jump expansion policy is ongoing work.
     577The definition and proof of a complete, optimal (in the sense that jump pseudoinstructions are expanded to the smallest possible opcode) and correct jump expansion policy is ongoing work.
    584578
    585579Aside from their application in verified compiler projects such as CerCo and CompCert, verified assemblers such as ours could also be applied to the verification of operating system kernels.
Note: See TracChangeset for help on using the changeset viewer.