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