# Changeset 1005

Ignore:
Timestamp:
Jun 20, 2011, 5:41:06 PM (8 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r1004 That is, the shrinking process is not just related to optimisation, but also the completeness of the assembler. Thinking more, it is easy to imagine knotty, circular configurations of jumps developing, each jump occurrence only being shrinkable if every other is. Finding a solution to this shrinking jumps' problem then involves us finding a method to break any vicious circularities that develop. How we went about resolving this problem affected the shape of our proof of correctness for the whole assembler in a rather profound way. We first attempted to synthesize a solution bottom up: starting with no solution, we gradually refine a solution using the same functions that implement the jump expansion. Abandoning this attempt, we instead split the policy'---the decision over how any particular jump should be expanded---from the implementation that actually expands assembly programs into machine code. Assuming the existence of a correct policy, we proved the implementation of the assembler correct. Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist. Policies do not exist in only a limited number of circumstances: namely, if a pseudoinstruction attempts to jump to a label that does not exist, or the program is too large to fit in code memory. The first case would constitute a serious compiler error, and hopefully certifying the rest of the compiler would rule this possibility out. The second case is unavoidable---certified compiler or not, trying to load a huge program into a small code memory will break \emph{something}. Further, we proved that the assembler fails to assemble an assembly program if and only if a correct policy does not exist. This is achieved by means of dependent types: the assembly function is total over a program, a policy and the proof that the policy is correct for the program. Policies do not exist in only a limited number of circumstances: namely, if a pseudoinstruction attempts to jump to a label that does not exist, or the program is too large to fit in code memory even after shrinking jumps according to the best policy. The first case is an example of compiler error because of ill-formedness of the input. It does not count for the compiler completeness. We plan to employ dependent types in CerCo to restrict the domain of the compiler to those programs that are semantically correct and should be compiled. In particular, in CerCo we are also interested in completeness of compilation whereas previous formalizations only focused on correctness. The rest of this paper is a detailed description of this proof.