# Changeset 2416 for Papers

Ignore:
Timestamp:
Oct 25, 2012, 12:30:01 PM (9 years ago)
Message:

Some more minor changes

Location:
Papers
Files:
3 edited

### Legend:

Unmodified
 r2380 the rest of the assembler works in order to build globally correct solutions. Proving their correctness is quite a complex task (see, for instance, the compaion paper~\cite{boender:correctness:2012}). the companion paper~\cite{boender:correctness:2012}). Nevertheless, the correctness of the whole assembler only depends on the correctness of the branch displacement algorithm. The cost returned by the assembler for a pseudoinstruction is set to be the cost of its expansion in clock cycles. For conditional jumps that are expanded as just shown, the costs of takin the true and false branches are different and as just shown, the costs of taking the true and false branches are different and both need to be returned. \texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always picking the locally best solution. In order to accomodate those optimal solutions that require local sub-optimal choices, the policy may also return a boolean used to force In order to accommodate those optimal solutions that require local sub-optimal choices, the policy may also return a Boolean used to force the translation of a \texttt{Jmp} into a \texttt{LJMP} even if $\delta < 128$. An essentially identical mechanism exists for call \texttt{a} by the policy and by the assembler must coincide. The latter is the sum of the size of all the expansions of the pseudo-instructions that preceed the one at address \texttt{a}: the assembler just concatenates all precede the one at address \texttt{a}: the assembler just concatenates all expansions sequentially. To grant this property, we impose a correctness criterion over policies. A policy is correct when Given a correct policy for the program to be assembled, the assembler never fails and returns some object code and a costing function. Under the condition that the policy is correct' for the program and the program is fully addressable by a 16-bit word, the object code is also fully addressable by a 16-bit word. Moreover, the result of assemblying the pseudoinstruction obtained fetching from the assembly address \texttt{ppc} is a list of bytes found in the generated object code starting from the object code address \texttt{policy(ppc)}. Moreover, the result of assembling the pseudoinstruction obtained fetching from the assembly address \texttt{ppc} is a list of bytes found in the generated object code starting from the object code address \texttt{policy(ppc)}. Essentially the type above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory. Our source files are available at~\url{http://cerco.cs.unibo.it}. We assumed several properties of library functions', e.g. modular arithmetic and datastructure manipulation. We axiomatised various small functions needed to complete the main theorems, as well as some routine' proof obligations of the theorems themselves, in focussing on the main meat of the theorems. We axiomatised various small functions needed to complete the main theorems, as well as some routine' proof obligations of the theorems themselves, in focusing on the main meat of the theorems. We believe that the proof strategy is sound and that all axioms can be closed, up to minor bugs that should have local fixes that do not affect the global proof strategy. The complete development is spread across 29 files with around 20,000 lines of Matita source. Relavent files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source. Relevant files are: \texttt{AssemblyProof.ma}, \texttt{AssemblyProofSplit.ma} and \texttt{AssemblyProofSplitSplit.ma}, consisting of approximately 4500 lines of Matita source. Numerous other lines of proofs are spread all over the development because of dependent types and the Russell proof style, which does not allow one to separate the code from the proofs. The low ratio between source lines and the number of lines of proof is unusual, but justified by the fact that the pseudo-assembly and the assembly language share most constructs and large swathes of the semantics are shared.
 r2414 \begin{minipage}[b]{0.45\linewidth} \begin{lstlisting} \end{lstlisting} \end{minipage} \subsection{Matita} \label{subsect.matita} Matita~\cite{asperti:user:2007} is a dependently-typed proof assistant developed in Bologna, implementing the Calculus of (Co)inductive Constructions, a type theory similar to that of Coq. Throughout this paper, all running examples are provided in Matita's proof script vernacular. This vernacular, similar to the syntax of OCaml or Coq, should be mostly straightforward. One possible source of confusion is our use of $?$ and $\ldots$, which correspond to a term, or terms, to be inferred automatically by unification, respectively. Any terms that cannot be inferred by unification from the surrounding context are left for the user to provide as proof obligations. Matita \subsection{Subtyping as instantiation vs subtyping as safe static cast}