1 | \section{The proof} |
---|
2 | |
---|
3 | In this section, we will present the correctness proof of the algorithm in more |
---|
4 | detail. |
---|
5 | |
---|
6 | The main correctness statement is as follows: |
---|
7 | |
---|
8 | \clearpage |
---|
9 | |
---|
10 | \begin{lstlisting} |
---|
11 | definition sigma_policy_specification :=: |
---|
12 | $\lambda$program: pseudo_assembly_program. |
---|
13 | $\lambda$sigma: Word → Word. |
---|
14 | $\lambda$policy: Word → bool. |
---|
15 | sigma (zero $\ldots$) = zero $\ldots$ $\wedge$ |
---|
16 | $\forall$ppc: Word.$\forall$ppc_ok. |
---|
17 | let instr_list := \snd program in |
---|
18 | let pc ≝ sigma ppc in |
---|
19 | let labels := \fst (create_label_cost_map (\snd program)) in |
---|
20 | let lookup_labels := |
---|
21 | $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in |
---|
22 | let instruction := |
---|
23 | \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in |
---|
24 | let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in |
---|
25 | (nat_of_bitvector $\ldots$ ppc ≤ |instr_list| → |
---|
26 | next_pc = add ? pc (bitvector_of_nat $\ldots$ |
---|
27 | (instruction_size lookup_labels sigma policy ppc instruction))) |
---|
28 | $\wedge$ |
---|
29 | ((nat_of_bitvector $\ldots$ ppc < |instr_list| → |
---|
30 | nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) |
---|
31 | $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| → next_pc = (zero $\ldots$))). |
---|
32 | \end{lstlisting} |
---|
33 | |
---|
34 | Informally, this means that when fetching a pseudo-instruction at $ppc$, the |
---|
35 | translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size |
---|
36 | of the instruction at $ppc$; i.e. an instruction is placed immediately |
---|
37 | after the previous one, and there are no overlaps. |
---|
38 | |
---|
39 | The other condition enforced is the fact that instructions are stocked in |
---|
40 | order: the memory address of the instruction at $ppc$ should be smaller than |
---|
41 | the memory address of the instruction at $ppc+1$. There is one exeception to |
---|
42 | this rule: the instruction at the very end of the program, whose successor |
---|
43 | address can be zero (this is the case where the program size is exactly equal |
---|
44 | to the amount of memory). |
---|
45 | |
---|
46 | And finally, we enforce that the program starts at address 0, i.e. |
---|
47 | $\sigma(0) = 0$. |
---|
48 | |
---|
49 | Since our computation is a least fixed point computation, we must prove |
---|
50 | termination in order to prove correctness: if the algorithm is halted after |
---|
51 | a number of steps without reaching a fixed point, the solution is not |
---|
52 | guaranteed to be correct. More specifically, branch instructions might be |
---|
53 | encoded who do not coincide with the span between their location and their |
---|
54 | destination. |
---|
55 | |
---|
56 | Proof of termination rests on the fact that the encoding of branch |
---|
57 | instructions can only grow larger, which means that we must reach a fixed point |
---|
58 | after at most $2n$ iterations, with $n$ the number of branch instructions in |
---|
59 | the program. This worst case is reached if at every iteration, we change the |
---|
60 | encoding of exactly one branch instruction; since the encoding of any branch |
---|
61 | instructions can change first from short to absolute and then from absolute to |
---|
62 | long, there can be at most $2n$ changes. |
---|
63 | |
---|
64 | This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}. |
---|
65 | We have proven some invariants of the {\sc f} function from the previous |
---|
66 | section; these invariants are then used to prove properties that hold for every |
---|
67 | iteration of the fixed point computation; and finally, we can prove some |
---|
68 | properties of the fixed point. |
---|
69 | |
---|
70 | \subsection{Fold invariants} |
---|
71 | |
---|
72 | These are the invariants that hold during the fold of {\sc f} over the program, |
---|
73 | and that will later on be used to prove the properties of the iteration. |
---|
74 | |
---|
75 | Note that during the fixed point computation, the $\sigma$ function is |
---|
76 | implemented as a trie for ease access; computing $\sigma(x)$ is done by looking |
---|
77 | up the value of $x$ in the trie. Actually, during the fold, the value we |
---|
78 | pass along is a couple $\mathbb{N} \times \mathtt{ppc_pc_map}$. The natural |
---|
79 | number is the number of bytes added to the program so far with respect to |
---|
80 | the previous iteration, and {\tt ppc\_pc\_map} is a couple of the current |
---|
81 | size of the program and our $\sigma$ function. |
---|
82 | |
---|
83 | \begin{lstlisting} |
---|
84 | definition out_of_program_none := |
---|
85 | $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. |
---|
86 | $\forall$i.i < 2^16 → (i > |prefix| $\leftrightarrow$ |
---|
87 | bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?). |
---|
88 | \end{lstlisting} |
---|
89 | |
---|
90 | This invariant states that every pseudo-address not yet treated cannot be |
---|
91 | found in the lookup trie. |
---|
92 | |
---|
93 | \begin{lstlisting} |
---|
94 | definition not_jump_default ≝ |
---|
95 | $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. |
---|
96 | $\forall$i.i < |prefix| → |
---|
97 | ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) → |
---|
98 | \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) |
---|
99 | $\langle$0,short_jump$\rangle$) = short_jump. |
---|
100 | \end{lstlisting} |
---|
101 | |
---|
102 | This invariant states that when we try to look up the jump length of a |
---|
103 | pseudo-address where there is no branch instruction, we will get the default |
---|
104 | value, a short jump. |
---|
105 | |
---|
106 | \begin{lstlisting} |
---|
107 | definition jump_increase := |
---|
108 | λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map. |
---|
109 | ∀i.i ≤ |prefix| → |
---|
110 | let $\langle$opc,oj$\rangle$ := |
---|
111 | bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in |
---|
112 | let $\langle$pc,j$\rangle$ := |
---|
113 | bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd p) $\langle$0,short_jump$\rangle$ in |
---|
114 | jmpleq oj j. |
---|
115 | \end{lstlisting} |
---|
116 | |
---|
117 | This invariant states that between iterations ($op$ being the previous |
---|
118 | iteration, and $p$ the current one), jump lengths either remain equal or |
---|
119 | increase. It is needed for proving termination. |
---|
120 | |
---|
121 | \clearpage |
---|
122 | |
---|
123 | \begin{lstlisting} |
---|
124 | definition sigma_compact_unsafe := |
---|
125 | λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
126 | ∀n.n < |program| → |
---|
127 | match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with |
---|
128 | [ None ⇒ False |
---|
129 | | Some x ⇒ let $\langle$pc,j$\rangle$ := x in |
---|
130 | match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
131 | [ None ⇒ False |
---|
132 | | Some x1 ⇒ let $\langle$pc1,j1$\rangle$ ≝ x1 in |
---|
133 | pc1 = pc + instruction_size_jmplen j |
---|
134 | (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$))) |
---|
135 | ] |
---|
136 | ]. |
---|
137 | \end{lstlisting} |
---|
138 | |
---|
139 | This is a temporary formulation of the main property |
---|
140 | ({\tt sigma\_policy\_specification}); its main difference |
---|
141 | with the final version is that it uses {\tt instruction\_size\_jmplen} to |
---|
142 | compute the instruction size. This function uses $j$ to compute the span |
---|
143 | of branch instructions (i.e. it uses the $\sigma$ function under construction), |
---|
144 | instead of looking at the distance between source and destination. This is |
---|
145 | because $\sigma$ is still under construction; later on we will prove that after |
---|
146 | the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main |
---|
147 | property. |
---|
148 | |
---|
149 | \begin{lstlisting} |
---|
150 | definition sigma_safe := |
---|
151 | λprefix:list labelled_instruction.λlabels:label_map.λadded:$\mathbb{N}$. |
---|
152 | λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. |
---|
153 | ∀i.i < |prefix| → let $\langle$pc,j$\rangle$ := |
---|
154 | bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in |
---|
155 | let pc_plus_jmp_length := bitvector_of_nat ? (\fst (bvt_lookup $\ldots$ |
---|
156 | (bitvector_of_nat ? (S i)) (\snd sigma) $\langle$0,short_jump$\rangle$)) in |
---|
157 | let $\langle$label,instr$\rangle$ := nth i ? prefix $\langle$None ?, Comment [ ]$\rangle$ in |
---|
158 | $\forall$dest.is_jump_to instr dest $\rightarrow$ |
---|
159 | let paddr := lookup_def $\ldots$ labels dest 0 in |
---|
160 | let addr := bitvector_of_nat ? (if leb i paddr (* forward jump *) |
---|
161 | then \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd old_sigma) |
---|
162 | $\langle$0,short_jump$\rangle$) + added |
---|
163 | else \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd sigma) |
---|
164 | $\langle$0,short_jump$\rangle$)) in |
---|
165 | match j with |
---|
166 | [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$ |
---|
167 | \fst (short_jump_cond pc_plus_jmp_length addr) = true |
---|
168 | | absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$ |
---|
169 | \fst (absolute_jump_cond pc_plus_jmp_length addr) = true $\wedge$ |
---|
170 | \fst (short_jump_cond pc_plus_jmp_length addr) = false |
---|
171 | | long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false |
---|
172 | $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = false |
---|
173 | ]. |
---|
174 | \end{lstlisting} |
---|
175 | |
---|
176 | This is a more direct safety property: it states that branch instructions are |
---|
177 | encoded properly, and that no wrong branch instructions are chosen. |
---|
178 | |
---|
179 | Note that we compute the distance using the memory address of the instruction |
---|
180 | plus its size: this is due to the behaviour of the MCS-51 architecture, which |
---|
181 | increases the program counter directly after fetching, and only then executes |
---|
182 | the branch instruction (by changing the program counter again). |
---|
183 | |
---|
184 | \begin{lstlisting} |
---|
185 | \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? 0) (\snd policy) |
---|
186 | $\langle$0,short_jump$\rangle$) = 0) |
---|
187 | \fst policy = \fst (bvt_lookup $\ldots$ |
---|
188 | (bitvector_of_nat ? (|prefix|)) (\snd policy) $\langle$0,short_jump$\rangle$) |
---|
189 | \end{lstlisting} |
---|
190 | |
---|
191 | These two properties give the values of $\sigma$ for the start and end of the |
---|
192 | program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of |
---|
193 | instructions up until now, is equal to the maximum memory address so far. |
---|
194 | |
---|
195 | \begin{lstlisting} |
---|
196 | (added = 0 → policy_pc_equal prefix old_sigma policy)) |
---|
197 | (policy_jump_equal prefix old_sigma policy → added = 0)) |
---|
198 | \end{lstlisting} |
---|
199 | |
---|
200 | And finally, two properties that deal with what happens when the previous |
---|
201 | iteration does not change with respect to the current one. $added$ is the |
---|
202 | variable that keeps track of the number of bytes we have added to the program |
---|
203 | size by changing the encoding of branch instructions; if this is 0, the program |
---|
204 | has not changed and vice versa. |
---|
205 | |
---|
206 | We need to use two different formulations, because the fact that $added$ is 0 |
---|
207 | does not guarantee that no branch instructions have changed: it is possible |
---|
208 | that we have replaced a short jump with a absolute jump, which does not change |
---|
209 | the size of the branch instruction. |
---|
210 | |
---|
211 | Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, |
---|
212 | whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$. |
---|
213 | This formulation is sufficient to prove termination and compactness. |
---|
214 | |
---|
215 | Proving these invariants is simple, usually by induction on the prefix length. |
---|
216 | |
---|
217 | \subsection{Iteration invariants} |
---|
218 | |
---|
219 | These are invariants that hold after the completion of an iteration. The main |
---|
220 | difference between these invariants and the fold invariants is that after the |
---|
221 | completion of the fold, we check whether the program size does not supersede |
---|
222 | 65 Kbytes (the maximum memory size the MCS-51 can address). |
---|
223 | |
---|
224 | The type of an iteration therefore becomes an option type: {\tt None} in case |
---|
225 | the program becomes larger than 65 KBytes, or $\mathtt{Some}\ \sigma$ |
---|
226 | otherwise. We also no longer use a natural number to pass along the number of |
---|
227 | bytes added to the program size, but a boolean that indicates whether we have |
---|
228 | changed something during the iteration or not. |
---|
229 | |
---|
230 | If an iteration returns {\tt None}, we have the following invariant: |
---|
231 | |
---|
232 | \begin{lstlisting} |
---|
233 | definition nec_plus_ultra := |
---|
234 | λprogram:list labelled_instruction.λp:ppc_pc_map. |
---|
235 | ¬(∀i.i < |program| → |
---|
236 | is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$)) → |
---|
237 | \snd (bvt_lookup $\ldots$ (bitvector_of_nat 16 i) (\snd p) $\langle$0,short_jump$\rangle$) = |
---|
238 | long_jump). |
---|
239 | \end{lstlisting} |
---|
240 | |
---|
241 | This invariant is applied to $old\_sigma$; if our program becomes too large |
---|
242 | for memory, the previous iteration cannot have every branch instruction encoded |
---|
243 | as a long jump. This is needed later on in the proof of termination. |
---|
244 | |
---|
245 | If the iteration returns $\mathtt{Some}\ \sigma$, the invariants |
---|
246 | {\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase}, |
---|
247 | and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are |
---|
248 | retained without change. |
---|
249 | |
---|
250 | Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper |
---|
251 | invariant: |
---|
252 | |
---|
253 | \begin{lstlisting} |
---|
254 | definition sigma_compact := |
---|
255 | λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. |
---|
256 | ∀n.n < |program| → |
---|
257 | match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with |
---|
258 | [ None ⇒ False |
---|
259 | | Some x ⇒ let $\langle$pc,j$\rangle$ := x in |
---|
260 | match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with |
---|
261 | [ None ⇒ False |
---|
262 | | Some x1 ⇒ let $\langle$pc1,j1$\rangle$ := x1 in |
---|
263 | pc1 = pc + instruction_size |
---|
264 | (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) |
---|
265 | (λppc.bitvector_of_nat ? |
---|
266 | (\fst (bvt_lookup $\ldots$ ppc (\snd sigma) $\langle$0,short_jump$\rangle$))) |
---|
267 | (λppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc |
---|
268 | (\snd sigma) $\langle$0,short_jump$\rangle$))) (bitvector_of_nat ? n) |
---|
269 | (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)) |
---|
270 | ] |
---|
271 | ]. |
---|
272 | \end{lstlisting} |
---|
273 | |
---|
274 | This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it |
---|
275 | computes the sizes of branch instructions by looking at the distance between |
---|
276 | position and destination using $\sigma$. |
---|
277 | |
---|
278 | In actual use, the invariant is qualified: $\sigma$ is compact if there have |
---|
279 | been no changes (i.e. the boolean passed along is {\tt true}). This is to |
---|
280 | reflect the fact that we are doing a least fixed point computation: the result |
---|
281 | is only correct when we have reached the fixed point. |
---|
282 | |
---|
283 | There is another, trivial, invariant if the iteration returns |
---|
284 | $\mathtt{Some}\ \sigma$: |
---|
285 | |
---|
286 | \begin{lstlisting} |
---|
287 | \fst p < 2^16 |
---|
288 | \end{lstlisting} |
---|
289 | |
---|
290 | The invariants that are taken directly from the fold invariants are trivial to |
---|
291 | prove. |
---|
292 | |
---|
293 | The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None}, |
---|
294 | then the program size must be greater than 65 Kbytes. However, since the |
---|
295 | previous iteration did not return {\tt None} (because otherwise we would |
---|
296 | terminate immediately), the program size in the previous iteration must have |
---|
297 | been smaller than 65 Kbytes. |
---|
298 | |
---|
299 | Suppose that all the branch instructions in the previous iteration are |
---|
300 | encodes as long jumps. This means that all branch instructions in this |
---|
301 | iteration are long jumps as well, and therefore that both iterations are equal |
---|
302 | in the encoding of their branch instructions. Per the invariant, this means that |
---|
303 | $added = 0$, and therefore that all addresses in both iterations are equal. |
---|
304 | But if all addresses are equal, the program sizes must be equal too, which |
---|
305 | means that the program size in the current iteration must be smaller than |
---|
306 | 65 Kbytes. This contradicts the earlier hypothesis, hence not all branch |
---|
307 | instructions in the previous iteration are encoded as long jumps. |
---|
308 | |
---|
309 | The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and |
---|
310 | the fact that we have reached a fixed point, i.e. the previous iteration and |
---|
311 | the current iteration are the same. This means that the results of |
---|
312 | {\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same. |
---|
313 | |
---|
314 | \subsection{Final properties} |
---|
315 | |
---|
316 | These are the invariants that hold after $2n$ iterations, where $n$ is the |
---|
317 | program size (we use the program size for convenience; we could also use the |
---|
318 | number of branch instructions, but this is more complicated). Here, we only |
---|
319 | need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that |
---|
320 | $\sigma(0) = 0$. |
---|
321 | |
---|
322 | Termination can now be proven through the fact that there is a $k \leq 2n$, with |
---|
323 | $n$ the length of the program, such that iteration $k$ is equal to iteration |
---|
324 | $k+1$. There are two possibilities: either there is a $k < 2n$ such that this |
---|
325 | property holds, or every iteration up to $2n$ is different. In the latter case, |
---|
326 | since the only changes between the iterations can be from shorter jumps to |
---|
327 | longer jumps, in iteration $2n$ every branch instruction must be encoded as |
---|
328 | a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the |
---|
329 | fixpoint is reached. |
---|