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