# Changeset 1029 for src/ASM/CPP2011

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

...

File:
1 edited

### Legend:

Unmodified
 r1028 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$. This 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. 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. In 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. % ---------------------------------------------------------------------------- % \begin{lstlisting} inductive jump_length: Type[0] := | short_jump: jump_length | medium_jump: jump_length | long_jump: jump_length. |short_jump:jump_length |medium_jump:jump_length |long_jump:jump_length. \end{lstlisting} lookup $\ldots$ id labels (zero $\ldots$) = sigma pseudo_program pol addr := $\ldots$ \end{lstlisting} 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). 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 and coercions, through which Russell is simulated in Matita). We 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. The \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: \begin{lstlisting} theorem fetch_assembly: $\forall$pc, i, cmem, assembled. assembled = assembly1 i $\rightarrow$ theorem fetch_assembly: $\forall$pc, i, cmem, assembled.  assembled=assembly1 i $\rightarrow$ let len := length $\ldots$ assembled in encoding_check cmem pc (pc + len) assembled $\rightarrow$ 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 (eq_instruction instr i $\wedge$ eqb ticks (ticks_of_instruction instr) $\wedge$ (eq_instruction instr i $\wedge$ eqb ticks (ticks_of_instruction instr) $\wedge$ eq_bv $\ldots$ pc' (pc + len)) = true. \end{lstlisting} lemma fetch_assembly_pseudo: ∀program.∀pol:policy program.∀ppc.∀code_memory. let pi := fst (fetch_pseudo_instruction (snd program) ppc) in let pi := $\pi_1$ (fetch_pseudo_instruction ($\pi_2$ program) ppc) in let instructions := expand_pseudo_instruction program pol ppc ... in let $\langle$len,assembled$\rangle$ := assembly_1_pseudoinstruction program pol ppc ... in 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{pol}. Further, suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{pol}, obtaining the list of machine code instructions \texttt{instructions}. Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{pol}, obtaining the list of machine code instructions \texttt{instructions}. Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{assembled}, a list of bytes. Then, 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. The 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. At first, the lemmas appears to nearly establish the correctness of the assembler: \begin{lstlisting} lemma fetch_assembly_pseudo2: ∀program,pol,ppc. let $\langle$labels,costs$\rangle$ := build_maps program pol in let assembled := \fst (assembly program pol) in let assembled := $\pi_1$ (assembly program pol) in let code_memory := load_code_memory assembled in let data_labels := construct_datalabels (\fst program) in let data_labels := construct_datalabels ($\pi_1$ program) in let lookup_labels := λx. sigma $\ldots$ pol (address_of_word_labels_code_mem (\snd program) x) in λx. sigma $\ldots$ pol (address_of_word_labels_code_mem ($\pi_2$ program) x) in let lookup_datalabels := λx. lookup ? ? x data_labels (zero ?) in let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction (\snd program) ppc in let instructions ≝ expand_pseudo_instruction program pol ppc ... in fetch_many code_memory (sigma program pol newppc) (sigma program pol ppc) instructions. let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in let instrs ≝ expand_pseudo_instruction program pol ppc ... in fetch_many code_memory (sigma $\ldots$ pol newppc) (sigma $\ldots$ pol ppc) instrs. \end{lstlisting} The fetched sequence corresponds to the expansion, according to \texttt{pol}, of the pseudoinstruction. At first, the lemmas appears to immediately imply the correctness of the assembler. However, 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. In particular, the two semantics differ on instructions that \emph{could} directly manipulate program addresses. \begin{lstlisting} axiom low_internal_ram_of_pseudo_low_internal_ram: internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7. internal_pseudo_address_map$\rightarrow$BitVectorTrie Byte 7$\rightarrow$BitVectorTrie Byte 7. \end{lstlisting} The \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. It 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. It thus decides the membership of a correct but not complete subset of well behaved programs. It thus decides the membership of a strict subset of the set of well behaved programs. \begin{lstlisting} definition next_internal_pseudo_address_map: internal_pseudo_address_map However, this comes at the expense of assembler completeness: the generated program may be too large to fit into code memory. In this respect, there is a trade-off between the completeness of the assembler and the efficiency of the assembled program. 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. The 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. Aside 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.