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 invariants for the fold function. Note that during the fixed point |
---|
26 | computation, the $sigma$ functions are implemented as tries, so in order to |
---|
27 | compute $sigma(i)$, we lookup the value for $i$ in the corresponding trie. |
---|
28 | |
---|
29 | \begin{lstlisting} |
---|
30 | (out_of_program_none prefix policy) $\wedge$ |
---|
31 | (jump_not_in_policy prefix policy) $\wedge$ |
---|
32 | (policy_increase prefix old_sigma policy) $\wedge$ |
---|
33 | (policy_compact_unsafe prefix labels policy) $\wedge$ |
---|
34 | (policy_safe prefix labels added old_sigma policy) $\wedge$ |
---|
35 | (\fst (bvt_lookup $\ldots$ |
---|
36 | (bitvector_of_nat ? 0) (\snd policy) $\langle$0,short_jump$\rangle$) = 0) $\wedge$ |
---|
37 | (\fst policy = \fst (bvt_lookup $\ldots$ |
---|
38 | (bitvector_of_nat ? (|prefix|)) (\snd policy) $\langle$0,short_jump$\rangle$)) $\wedge$ |
---|
39 | (added = 0 → policy_pc_equal prefix old_sigma policy) $\wedge$ |
---|
40 | (policy_jump_equal prefix old_sigma policy → added = 0) |
---|
41 | \end{lstlisting} |
---|
42 | |
---|
43 | These invariants have the following meanings: |
---|
44 | |
---|
45 | \begin{itemize} |
---|
46 | \item {\tt out\_of\_program\_none} shows that if we try to lookup a value |
---|
47 | beyond the program, we will get an empty result; |
---|
48 | \item {\tt jump\_not\_in\_policy} shows that an instruction that is not a jump |
---|
49 | will have a {\tt short\_jump} as its associated jump length; |
---|
50 | \item {\tt policy\_increase} shows that between iterations, jumps either increase (i.e. from {\tt short\_jump} to {\tt medium\_jump} or from {\tt medium\_jump} to {\tt long\_jump}) or remain equal; |
---|
51 | \item {\tt policy\_compact\_unsafe} shows that the policy is compact (instrucftions directly follow each other and do not overlap); |
---|
52 | \item {\tt policy\_safe} shows that jumps selected are appropriate for the |
---|
53 | distance between their position and their target, and the jumps selected are |
---|
54 | the smallest possible; |
---|
55 | \item Then there are two properties that fix the values of $\sigma(0)$ and |
---|
56 | $\sigma(n)$ (with $n$ the size of the program); |
---|
57 | \item And finally two predicates that link the value of $added$ to reaching |
---|
58 | of a fixed point. |
---|
59 | \end{itemize} |
---|
60 | |
---|
61 | \begin{lstlisting} |
---|
62 | ($\Sigma$x:bool × (option ppc_pc_map). |
---|
63 | let $\langle$no_ch,y$\rangle$ := x in |
---|
64 | match y with |
---|
65 | [ None ⇒ nec_plus_ultra program old_policy |
---|
66 | | Some p ⇒ (out_of_program_none program p) $\wedge$ |
---|
67 | (jump_not_in_policy program p) $\wedge$ |
---|
68 | (policy_increase program old_policy p) $\wedge$ |
---|
69 | (no_ch = true → policy_compact program labels p) $\wedge$ |
---|
70 | (\fst (bvt_lookup $\ldots$ |
---|
71 | (bitvector_of_nat ? 0) (\snd p) $\langle$0,short_jump$\rangle$) = 0) $\wedge$ |
---|
72 | (\fst p = \fst (bvt_lookup $\ldots$ |
---|
73 | (bitvector_of_nat ? (|program|)) (\snd p) $\langle$0,short_jump$\rangle$)) $\wedge$ |
---|
74 | (no_ch = true $\rightarrow$ policy_pc_equal program old_policy p) $\wedge$ |
---|
75 | (policy_jump_equal program old_policy p $\rightarrow$ no_ch = true) $\wedge$ |
---|
76 | (\fst p < 2^16) |
---|
77 | ]) |
---|
78 | \end{lstlisting} |
---|
79 | |
---|
80 | The main correctness statement, then, is as follows: |
---|
81 | |
---|
82 | \begin{lstlisting} |
---|
83 | definition sigma_policy_specification :=: |
---|
84 | $\lambda$program: pseudo_assembly_program. |
---|
85 | $\lambda$sigma: Word → Word. |
---|
86 | $\lambda$policy: Word → bool. |
---|
87 | sigma (zero $\ldots$) = zero $\ldots$ $\wedge$ |
---|
88 | $\forall$ppc: Word.$\forall$ppc_ok. |
---|
89 | let instr_list := \snd program in |
---|
90 | let pc ≝ sigma ppc in |
---|
91 | let labels := \fst (create_label_cost_map (\snd program)) in |
---|
92 | let lookup_labels := |
---|
93 | $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in |
---|
94 | let instruction := |
---|
95 | \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in |
---|
96 | let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in |
---|
97 | (nat_of_bitvector $\ldots$ ppc ≤ |instr_list| → |
---|
98 | next_pc = add 16 pc (bitvector_of_nat $\ldots$ |
---|
99 | (instruction_size lookup_labels sigma policy ppc instruction))) |
---|
100 | $\wedge$ |
---|
101 | ((nat_of_bitvector $\ldots$ ppc < |instr_list| → |
---|
102 | nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) |
---|
103 | $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| → next_pc = (zero $\ldots$))). |
---|
104 | \end{lstlisting} |
---|
105 | |
---|
106 | Informally, this means that when fetching a pseudo-instruction at $ppc$, the |
---|
107 | translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size |
---|
108 | of the instruction at $ppc$; i.e. an instruction is placed immediately |
---|
109 | after the previous one, and there are no overlaps. |
---|
110 | |
---|
111 | The other condition enforced is the fact that instructions are stocked in |
---|
112 | order: the memory address of the instruction at $ppc$ should be smaller than |
---|
113 | the memory address of the instruction at $ppc+1$. There is one exeception to |
---|
114 | this rule: the instruction at the very end of the program, whose successor |
---|
115 | address can be zero (this is the case where the program size is exactly equal |
---|
116 | to the amount of memory). |
---|
117 | |
---|
118 | And finally, we enforce that the program starts at address 0, i.e. |
---|
119 | $\sigma(0) = 0$. |
---|