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