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

Last change on this file since 2084 was 2084, checked in by boender, 9 years ago
  • changed bibliography style
  • added CerCo? thanks
  • some words of conclusion
File size: 14.6 KB
1\section{The proof}
3In this section, we will present the correctness proof of the algorithm in more
6The main correctness statement is as follows:
9definition 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$))).
32Informally, this means that when fetching a pseudo-instruction at $ppc$, the
33translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
34of the instruction at $ppc$; i.e. an instruction is placed immediately
35after the previous one, and there are no overlaps.
37The other condition enforced is the fact that instructions are stocked in
38order: the memory address of the instruction at $ppc$ should be smaller than
39the memory address of the instruction at $ppc+1$. There is one exeception to
40this rule: the instruction at the very end of the program, whose successor
41address can be zero (this is the case where the program size is exactly equal
42to the amount of memory).
44And finally, we enforce that the program starts at address 0, i.e.
45$\sigma(0) = 0$.
47Since our computation is a least fixed point computation, we must prove
48termination in order to prove correctness: if the algorithm is halted after
49a number of steps without reaching a fixed point, the solution is not
50guaranteed to be correct. More specifically, jumps might be encoded whose
51displacement is too great for the instruction chosen.
53Proof of termination rests on the fact that jumps can only increase, which
54means 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
56iteration, we change the encoding of exactly one jump; since a jump can change
57from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
58can be at most $2n$ changes.
60This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
61We have proven some invariants of the {\sc f} function from the previous
62section; these invariants are then used to prove properties that hold for every
63iteration of the fixed point computation; and finally, we can prove some
64properties of the fixed point.
66\subsection{Fold invariants}
68These are the invariants that hold during the fold of {\sc f} over the program,
69and that will later on be used to prove the properties of the iteration.
71Note that during the fixed point computation, the $\sigma$ function is
72implemented as a trie for ease access; computing $\sigma(x)$ is done by looking
73up the value of $x$ in the trie. Actually, during the fold, the value we
74pass along is a couple $\mathbb{N} \times \mathtt{ppc_pc_map}$. The natural
75number is the number of bytes added to the program so far with respect to
76the previous iteration, and {\tt ppc\_pc\_map} is a couple of the current
77size of the program and our $\sigma$ function.
80definition 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 ?).
86This invariant states that every pseudo-address not yet treated cannot be
87found in the lookup trie.
90definition 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.
98This invariant states that when we try to look up the jump length of a
99pseudo-address where there is no jump, we will get the default value, a short
103definition 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.
113This invariant states that between iterations ($op$ being the previous
114iteration, and $p$ the current one), jump lengths either remain equal or
115increase. It is needed for proving termination.
118definition 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  ].
133This is a temporary formulation of the main property
134({\tt sigma\_policy\_specification}); its main difference
135with the final version is that it uses {\tt instruction\_size\_jmplen} to
136compute the instruction size. This function uses $j$ to compute the size
137of jumps (i.e. it uses the $\sigma$ function under construction), instead
138of 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
140final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
144definition 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    ].
170This is a more direct safety property: it states that jump instructions are
171encoded properly, and that no wrong jump instructions are chosen.
173Note that we compute the distance using the memory address of the instruction
174plus its size: this is due to the behaviour of the MCS-51 architecture, which
175increases the program counter directly after fetching, and only then executes
176the jump.
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 → policy_pc_equal prefix old_sigma policy))
191(policy_jump_equal prefix old_sigma policy → 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 the
196variable that keeps track of the number of bytes we have added to the program
197size by changing jumps; if this is 0, the program has not changed and vice
200We need to use two different formulations, because the fact that $added$ is 0
201does not guarantee that no jumps have changed: it is possible that we have
202replaced a short jump with a medium jump, which does not change the size.
204Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
205whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$.
206This formulation is sufficient to prove termination and compactness.
208Proving these invariants is simple, usually by induction on the prefix length.
210\subsection{Iteration invariants}
212These are invariants that hold after the completion of an iteration. The main
213difference between these invariants and the fold invariants is that after the
214completion of the fold, we check whether the program size does not supersede
21565 Kbytes (the maximum memory size the MCS-51 can address).
217The type of an iteration therefore becomes an option type: {\tt None} in case
218the program becomes larger than 65 KBytes, or $\mathtt{Some}\ \sigma$
219otherwise. We also no longer use a natural number to pass along the number of
220bytes added to the program size, but a boolean that indicates whether we have
221changed something during the iteration or not.
223If an iteration returns {\tt None}, we have the following invariant:
226definition 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).
234This invariant is applied to $old\_sigma$; if our program becomes too large
235for memory, the previous iteration cannot have every jump encoded as a long
236jump. This is needed later on in the proof of termination.
238If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
239{\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase},
240and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
241retained without change.
243Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
247definition 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  ].
267This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it
268computes the sizes of jump instructions by looking at the distance between
269position and destination using $\sigma$.
271In actual use, the invariant is qualified: $\sigma$ is compact if there have
272been no changes (i.e. the boolean passed along is {\tt true}). This is to
273reflect the fact that we are doing a least fixed point computation: the result
274is only correct when we have reached the fixed point.
276There is another, trivial, invariant if the iteration returns
277$\mathtt{Some}\ \sigma$:
280\fst p < 2^16
283The invariants that are taken directly from the fold invariants are trivial to
286The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None},
287then the program size must be greater than 65 Kbytes. However, since the
288previous iteration did not return {\tt None} (because otherwise we would
289terminate immediately), the program size in the previous iteration must have
290been smaller than 65 Kbytes.
292Suppose that all the jumps in the previous iteration are long jumps. This means
293that all jumps in this iteration are long jumps as well, and therefore that
294both iterations are equal in jumps. Per the invariant, this means that
295$added = 0$, and therefore that all addresses in both iterations are equal.
296But if all addresses are equal, the program sizes must be equal too, which
297means that the program size in the current iteration must be smaller than
29865 Kbytes. This contradicts the earlier hypothesis, hence not all jumps in
299the previous iteration are long jumps.
301The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
302the fact that we have reached a fixed point, i.e. the previous iteration and
303the current iteration are the same. This means that the results of
304{\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
306\subsection{Final properties}
308These are the invariants that hold after $2n$ iterations, where $n$ is the
309program size. Here, we only need {\tt out\_of\_program\_none},
310{\tt sigma\_compact} and the fact that $\sigma(0) = 0$.
312Termination 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
315property holds, or every iteration up to $2n$ is different. In the latter case,
316since the only changes between the iterations can be from shorter jumps to
317longer jumps, in iteration $2n$ every jump must be long. In this case,
318iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached.
Note: See TracBrowser for help on using the repository browser.