1 | \section{The proof} |
---|
2 | |
---|
3 | In this section, we will present the correctness proof of the algorithm in more |
---|
4 | detail. |
---|
5 | |
---|
6 | Since our computation is a least fixed point computation, we must prove |
---|
7 | termination in order to prove correctness: if the algorithm is halted after |
---|
8 | a number of steps without reaching a fixed point, the solution is not |
---|
9 | guaranteed to be correct. More specifically, jumps might be encoded whose |
---|
10 | displacement is too great for the instruction chosen. |
---|
11 | |
---|
12 | Proof of termination rests on the fact that jumps can only increase, which |
---|
13 | means that we must reach a fixed point after at most $2n$ iterations, with |
---|
14 | $2n$ the number of jumps in the program. This worst case is reached if at every |
---|
15 | iteration, we change the encoding of exactly one jump; since a jump can change |
---|
16 | from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there |
---|
17 | can be at most $2n$ changes. |
---|
18 | |
---|
19 | This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}. |
---|
20 | We have proven some invariants of the {\sc f} function from the previous |
---|
21 | section; these invariants are then used to prove properties that hold for every |
---|
22 | iteration of the fixed point computation; and finally, we can prove some |
---|
23 | properties of the fixed point. |
---|
24 | |
---|
25 | The main correctness statement, then, is as follows: |
---|
26 | |
---|
27 | \begin{lstlisting} |
---|
28 | definition jump_expansion': |
---|
29 | $\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (|l|) < 2^16). |
---|
30 | option ($\Sigma$sigma:Word → Word $\times$ bool. |
---|
31 | $\forall$ppc: Word.$\forall$ppc_ok. |
---|
32 | let pc := \fst (sigma ppc) in |
---|
33 | let labels := \fst (create_label_cost_map (\snd program)) in |
---|
34 | let lookup_labels := |
---|
35 | $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in |
---|
36 | let instruction := |
---|
37 | \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in |
---|
38 | let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in |
---|
39 | And (nat_of_bitvector $\ldots$ ppc $\leq$ |\snd program| → |
---|
40 | next_pc = add ? pc (bitvector_of_nat $\ldots$ |
---|
41 | (instruction_size lookup_labels ($\lambda$x.\fst (sigma x)) |
---|
42 | ($\lambda$x.\snd (sigma x)) ppc instruction)) |
---|
43 | ) |
---|
44 | (Or (nat_of_bitvector $\ldots$ ppc < |\snd program| → |
---|
45 | nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) |
---|
46 | (nat_of_bitvector $\ldots$ ppc = |\snd program| → next_pc = (zero $\ldots$)))) |
---|
47 | \end{lstlisting} |
---|
48 | |
---|
49 | Informally, this means that when fetching a pseudo-instruction at $ppc$, the |
---|
50 | translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size |
---|
51 | of the instruction at $ppc$; i.e. an instruction is placed immediately |
---|
52 | after the previous one, and there are no overlaps. |
---|
53 | |
---|
54 | The other condition enforced is the fact that instructions are stocked in |
---|
55 | order: the memory address of the instruction at $ppc$ should be smaller than |
---|
56 | the memory address of the instruction at $ppc+1$. There is one exeception to |
---|
57 | this rule: the instruction at the very end of the program, whose successor |
---|
58 | address can be zero (this is the case where the program size is exactly equal |
---|
59 | to the amount of memory). |
---|