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

Last change on this file since 2096 was 2096, checked in by mulligan, 9 years ago

Changes to the English for Jaap, and some tidying up and making consistent with the other CPP submission.

File size: 15.5 KB
1\section{The proof}
3In this section, we present the correctness proof for the algorithm in more
4detail.  The main correctness statement is as follows (slightly simplified, here):
9definition 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$))).
29Informally, this means that when fetching a pseudo-instruction at $ppc$, the
30translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
31of the instruction at $ppc$.  That is, an instruction is placed consecutively
32after the previous one, and there are no overlaps.
34Instructions are also stocked in
35order: the memory address of the instruction at $ppc$ should be smaller than
36the memory address of the instruction at $ppc+1$. There is one exeception to
37this rule: the instruction at the very end of the program, whose successor
38address can be zero (this is the case where the program size is exactly equal
39to the amount of memory).
41Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$.
43Since our computation is a least fixed point computation, we must prove
44termination in order to prove correctness: if the algorithm is halted after
45a number of steps without reaching a fixed point, the solution is not
46guaranteed to be correct. More specifically, branch instructions might be
47encoded which do not coincide with the span between their location and their
50Proof of termination rests on the fact that the encoding of branch
51instructions can only grow larger, which means that we must reach a fixed point
52after at most $2n$ iterations, with $n$ the number of branch instructions in
53the program. This worst case is reached if at every iteration, we change the
54encoding of exactly one branch instruction; since the encoding of any branch
55instructions can change first from short to absolute and then from absolute to
56long, there can be at most $2n$ changes.
58The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
59We have proven some invariants of the {\sc f} function from the previous
60section; these invariants are then used to prove properties that hold for every
61iteration of the fixed point computation; and finally, we can prove some
62properties of the fixed point.
64\subsection{Fold invariants}
66These are the invariants that hold during the fold of {\sc f} over the program,
67and that will later on be used to prove the properties of the iteration.
69Note that during the fixed point computation, the $\sigma$ function is
70implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking
71up the value of $x$ in the trie. Actually, during the fold, the value we
72pass along is a pair $\mathbb{N} \times \mathtt{ppc_pc_map}$. The first component
73is the number of bytes added to the program so far with respect to
74the previous iteration, and the second component, {\tt ppc\_pc\_map}, is a pair
75consisting of the current size of the program and our $\sigma$ function.
78definition 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 ?).
84This invariant states that any pseudo-address not yet examined is not
85present in the lookup trie.
88definition 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.
96This invariant states that when we try to look up the jump length of a
97pseudo-address where there is no branch instruction, we will get the default
98value, a short jump.
101definition 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.
111This invariant states that between iterations (with $op$ being the previous
112iteration, and $p$ the current one), jump lengths either remain equal or
113increase. It is needed for proving termination.
118definition 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  ].
133This is a temporary formulation of the main property
134({\tt sigma\_policy\_specification}); its main difference
135from the final version is that it uses {\tt instruction\_size\_jmplen} to
136compute the instruction size. This function uses $j$ to compute the span
137of branch instructions  (i.e. it uses the $\sigma$ function under construction),
138instead of looking at the distance between source and destination. This is
139because $\sigma$ is still under construction; later on we will prove that after
140the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
144definition 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    ].
170This is a more direct safety property: it states that branch instructions are
171encoded properly, and that no wrong branch instructions are chosen.
173Note that we compute the distance using the memory address of the instruction
174plus its size: this follows the behaviour of the MCS-51 microprocessor, which
175increases the program counter directly after fetching, and only then executes
176the branch instruction (by changing the program counter again).
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$)
185These two properties give the values of $\sigma$ for the start and end of the
186program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of
187instructions up until now, is equal to the maximum memory address so far.
190(added = 0 $\rightarrow$ policy_pc_equal prefix old_sigma policy))
191(policy_jump_equal prefix old_sigma policy $\rightarrow$ added = 0))
194And finally, two properties that deal with what happens when the previous
195iteration does not change with respect to the current one. $added$ is a
196variable that keeps track of the number of bytes we have added to the program
197size by changing the encoding of branch instructions. If $added$ is 0, the program
198has not changed and vice versa.
200We need to use two different formulations, because the fact that $added$ is 0
201does not guarantee that no branch instructions have changed.  For instance,
202it is possible that we have replaced a short jump with a absolute jump, which
203does not change the size of the branch instruction.
205Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
206whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$.
207This formulation is sufficient to prove termination and compactness.
209Proving these invariants is simple, usually by induction on the prefix length.
211\subsection{Iteration invariants}
213These are invariants that hold after the completion of an iteration. The main
214difference between these invariants and the fold invariants is that after the
215completion of the fold, we check whether the program size does not supersede
21664 Kb, the maximum memory size the MCS-51 can address.
218The type of an iteration therefore becomes an option type: {\tt None} in case
219the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
220otherwise. We also no longer use a natural number to pass along the number of
221bytes added to the program size, but a boolean that indicates whether we have
222changed something during the iteration or not.
224If an iteration returns {\tt None}, we have the following invariant:
227definition 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).
235This invariant is applied to $old\_sigma$; if our program becomes too large
236for memory, the previous iteration cannot have every branch instruction encoded
237as a long jump. This is needed later in the proof of termination.
239If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
240{\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase},
241and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
242retained without change.
244Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
248definition 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  ].
268This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
269computes the sizes of branch instructions by looking at the distance between
270position and destination using $\sigma$.
272In actual use, the invariant is qualified: $\sigma$ is compact if there have
273been no changes (i.e. the boolean passed along is {\tt true}). This is to
274reflect the fact that we are doing a least fixed point computation: the result
275is only correct when we have reached the fixed point.
277There is another, trivial, invariant if the iteration returns
278$\mathtt{Some}\ \sigma$:
281\fst p < 2^16
284The invariants that are taken directly from the fold invariants are trivial to
287The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None},
288then the program size must be greater than 64 Kb. However, since the
289previous iteration did not return {\tt None} (because otherwise we would
290terminate immediately), the program size in the previous iteration must have
291been smaller than 64 Kb.
293Suppose that all the branch instructions in the previous iteration are
294encoded as long jumps. This means that all branch instructions in this
295iteration are long jumps as well, and therefore that both iterations are equal
296in 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.
298But if all addresses are equal, the program sizes must be equal too, which
299means that the program size in the current iteration must be smaller than
30064 Kb. This contradicts the earlier hypothesis, hence not all branch
301instructions in the previous iteration are encoded as long jumps.
303The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
304the fact that we have reached a fixed point, i.e. the previous iteration and
305the current iteration are the same. This means that the results of
306{\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
308\subsection{Final properties}
310These are the invariants that hold after $2n$ iterations, where $n$ is the
311program size (we use the program size for convenience; we could also use the
312number of branch instructions, but this is more complex). Here, we only
313need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
314$\sigma(0) = 0$.
316Termination 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
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 branch instruction must be encoded as
322a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
323fixpoint is reached.
Note: See TracBrowser for help on using the repository browser.