source: src/ASM/CPP2012-policy/proof.tex @ 2086

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