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

Last change on this file since 3338 was 3338, checked in by boender, 7 years ago
  • updated statement of main correctness statement (still needs work)
File size: 15.6 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):
8\mathrm{sigma\_policy\_specification} \equiv
9\lambda program.\lambda sigma.\lambda policy. \notag\\
10  sigma\ 0 = 0\ \wedge \notag\\
11        \mathbf{let}\ instr\_list \equiv code\ program\ \mathbf{in} \notag\\
12        \forall ppc.ppc < |instr\_list| \rightarrow \notag\\
13        \mathbf{let}\ pc \equiv sigma\ ppc\ \mathbf{in} \notag\\
14        \mathbf{let}\ instruction \equiv \mathrm{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
15        \mathbf{let}\ next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
16                next\_pc = pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\
17                (pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\
18                (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
19          \mathbf{let}\ instruction' \equiv \mathrm{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
20                \mathrm{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
21        pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})
24Informally, this means that when fetching a pseudo-instruction at $ppc$, the
25translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
26of the instruction at $ppc$.  That is, an instruction is placed consecutively
27after the previous one, and there are no overlaps.
29Instructions are also stocked in
30order: the memory address of the instruction at $ppc$ should be smaller than
31the memory address of the instruction at $ppc+1$. There is one exeception to
32this rule: the instruction at the very end of the program, whose successor
33address can be zero (this is the case where the program size is exactly equal
34to the amount of memory).
36Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$.
38Since our computation is a least fixed point computation, we must prove
39termination in order to prove correctness: if the algorithm is halted after
40a number of steps without reaching a fixed point, the solution is not
41guaranteed to be correct. More specifically, branch instructions might be
42encoded which do not coincide with the span between their location and their
45Proof of termination rests on the fact that the encoding of branch
46instructions can only grow larger, which means that we must reach a fixed point
47after at most $2n$ iterations, with $n$ the number of branch instructions in
48the program. This worst case is reached if at every iteration, we change the
49encoding of exactly one branch instruction; since the encoding of any branch
50instructions can change first from short to absolute and then from absolute to
51long, there can be at most $2n$ changes.
53The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
54We have proven some invariants of the {\sc f} function from the previous
55section; these invariants are then used to prove properties that hold for every
56iteration of the fixed point computation; and finally, we can prove some
57properties of the fixed point.
59\subsection{Fold invariants}
61These are the invariants that hold during the fold of {\sc f} over the program,
62and that will later on be used to prove the properties of the iteration.
64Note that during the fixed point computation, the $\sigma$ function is
65implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking
66up the value of $x$ in the trie. Actually, during the fold, the value we
67pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component
68is the number of bytes added to the program so far with respect to
69the previous iteration, and the second component, {\tt ppc\_pc\_map}, is a pair
70consisting of the current size of the program and our $\sigma$ function.
73definition out_of_program_none :=
74 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map.
75 $\forall$i.i < 2^16 $\rightarrow$ (i > |prefix| $\leftrightarrow$
76  bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?).
79This invariant states that any pseudo-address not yet examined is not
80present in the lookup trie.
83definition not_jump_default :=
84 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map.
85 $\forall$i.i < |prefix| $\rightarrow$
86  ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) $\rightarrow$
87  \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma)
88   $\langle$0,short_jump$\rangle$) = short_jump.
91This invariant states that when we try to look up the jump length of a
92pseudo-address where there is no branch instruction, we will get the default
93value, a short jump.
96definition jump_increase :=
97 $\lambda$prefix:list labelled_instruction.$\lambda$op:ppc_pc_map.$\lambda$p:ppc_pc_map.
98 $\forall$i.i $\leq$ |prefix| $\rightarrow$
99 let $\langle$opc,oj$\rangle$ :=
100  bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in
101 let $\langle$pc,j$\rangle$ :=
102  bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd p) $\langle$0,short_jump$\rangle$ in
103  jmpleq oj j.
106This invariant states that between iterations (with $op$ being the previous
107iteration, and $p$ the current one), jump lengths either remain equal or
108increase. It is needed for proving termination.
112definition sigma_compact_unsafe :=
113 $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map.
114 $\forall$n.n < |program| $\rightarrow$
115  match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
116  [ None $\Rightarrow$ False
117  | Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in
118    match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with
119    [ None $\Rightarrow$ False
120    | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in
121       pc1 = pc + instruction_size_jmplen j
122        (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)))
123    ]
124  ].
127This is a temporary formulation of the main property\\
128({\tt sigma\_policy\_specification}); its main difference
129from the final version is that it uses {\tt instruction\_size\_jmplen} to
130compute the instruction size. This function uses $j$ to compute the span
131of branch instructions  (i.e. it uses the $\sigma$ function under construction),
132instead of looking at the distance between source and destination. This is
133because $\sigma$ is still under construction; later on we will prove that after
134the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
138definition sigma_safe :=
139 $\lambda$prefix:list labelled_instruction.$\lambda$labels:label_map.$\lambda$added:$\mathbb{N}$.
140 $\lambda$old_sigma:ppc_pc_map.$\lambda$sigma:ppc_pc_map.
141 $\forall$i.i < |prefix| $\rightarrow$ let $\langle$pc,j$\rangle$ :=
142  bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in
143  let pc_plus_jmp_length := bitvector_of_nat ?  (\fst (bvt_lookup $\ldots$
144   (bitvector_of_nat ? (S i)) (\snd sigma) $\langle$0,short_jump$\rangle$)) in
145  let $\langle$label,instr$\rangle$ := nth i ? prefix $\langle$None ?, Comment [ ]$\rangle$ in
146   $\forall$dest.is_jump_to instr dest $\rightarrow$ 
147    let paddr := lookup_def $\ldots$ labels dest 0 in
148    let addr := bitvector_of_nat ? (if leb i paddr (* forward jump *)
149    then \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd old_sigma)
150     $\langle$0,short_jump$\rangle$) + added
151    else \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd sigma)
152     $\langle$0,short_jump$\rangle$)) in
153    match j with
154    [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$
155       \fst (short_jump_cond pc_plus_jmp_length addr) = true
156    | absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$
157       \fst (absolute_jump_cond pc_plus_jmp_length addr) = true $\wedge$
158       \fst (short_jump_cond pc_plus_jmp_length addr) = false
159    | long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false
160       $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
161    ].
164This is a more direct safety property: it states that branch instructions are
165encoded properly, and that no wrong branch instructions are chosen.
167Note that we compute the distance using the memory address of the instruction
168plus its size: this follows the behaviour of the MCS-51 microprocessor, which
169increases the program counter directly after fetching, and only then executes
170the branch instruction (by changing the program counter again).
173\fst (bvt_lookup $\ldots$ (bitvector_of_nat ? 0) (\snd policy)
174 $\langle$0,short_jump$\rangle$) = 0)
175\fst policy = \fst (bvt_lookup $\ldots$
176 (bitvector_of_nat ? (|prefix|)) (\snd policy) $\langle$0,short_jump$\rangle$)
179These two properties give the values of $\sigma$ for the start and end of the
180program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of
181instructions up until now, is equal to the maximum memory address so far.
184(added = 0 $\rightarrow$ policy_pc_equal prefix old_sigma policy))
185(policy_jump_equal prefix old_sigma policy $\rightarrow$ added = 0))
188And finally, two properties that deal with what happens when the previous
189iteration does not change with respect to the current one. $added$ is a
190variable that keeps track of the number of bytes we have added to the program
191size by changing the encoding of branch instructions. If $added$ is 0, the program
192has not changed and vice versa.
194We need to use two different formulations, because the fact that $added$ is 0
195does not guarantee that no branch instructions have changed.  For instance,
196it is possible that we have replaced a short jump with an absolute jump, which
197does not change the size of the branch instruction.
199Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
200whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$.
201This formulation is sufficient to prove termination and compactness.
203Proving these invariants is simple, usually by induction on the prefix length.
205\subsection{Iteration invariants}
207These are invariants that hold after the completion of an iteration. The main
208difference between these invariants and the fold invariants is that after the
209completion of the fold, we check whether the program size does not supersede
21064 Kb, the maximum memory size the MCS-51 can address.
212The type of an iteration therefore becomes an option type: {\tt None} in case
213the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
214otherwise. We also no longer use a natural number to pass along the number of
215bytes added to the program size, but a boolean that indicates whether we have
216changed something during the iteration or not.
218If an iteration returns {\tt None}, we have the following invariant:
222definition nec_plus_ultra :=
223 $\lambda$program:list labelled_instruction.$\lambda$p:ppc_pc_map.
224 ¬($\forall$i.i < |program| $\rightarrow$
225  is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$)) $\rightarrow$ 
226  \snd (bvt_lookup $\ldots$ (bitvector_of_nat 16 i) (\snd p) $\langle$0,short_jump$\rangle$) =
227   long_jump).
230This invariant is applied to $old\_sigma$; if our program becomes too large
231for memory, the previous iteration cannot have every branch instruction encoded
232as a long jump. This is needed later in the proof of termination.
234If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
235{\tt out\_of\_program\_none},\\
236{\tt not\_jump\_default}, {\tt jump\_increase},
237and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
238retained without change.
240Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
244definition sigma_compact :=
245 $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map.
246 $\forall$n.n < |program| $\rightarrow$
247  match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
248  [ None $\Rightarrow$ False
249  | Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in
250    match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with
251    [ None $\Rightarrow$ False
252    | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in
253      pc1 = pc + instruction_size
254       ($\lambda$id.bitvector_of_nat ? (lookup_def ?? labels id 0))
255       ($\lambda$ppc.bitvector_of_nat ?
256        (\fst (bvt_lookup $\ldots$ ppc (\snd sigma) $\langle$0,short_jump$\rangle$)))
257       ($\lambda$ppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc
258        (\snd sigma) $\langle$0,short_jump$\rangle$))) (bitvector_of_nat ? n)
259       (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$))
260    ]
261  ].
264This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
265computes the sizes of branch instructions by looking at the distance between
266position and destination using $\sigma$.
268In actual use, the invariant is qualified: $\sigma$ is compact if there have
269been no changes (i.e. the boolean passed along is {\tt true}). This is to
270reflect the fact that we are doing a least fixed point computation: the result
271is only correct when we have reached the fixed point.
273There is another, trivial, invariant if the iteration returns
274$\mathtt{Some}\ \sigma$:
277\fst p < 2^16
280The invariants that are taken directly from the fold invariants are trivial to
283The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None},
284then the program size must be greater than 64 Kb. However, since the
285previous iteration did not return {\tt None} (because otherwise we would
286terminate immediately), the program size in the previous iteration must have
287been smaller than 64 Kb.
289Suppose that all the branch instructions in the previous iteration are
290encoded as long jumps. This means that all branch instructions in this
291iteration are long jumps as well, and therefore that both iterations are equal
292in the encoding of their branch instructions. Per the invariant, this means that
293$added = 0$, and therefore that all addresses in both iterations are equal.
294But if all addresses are equal, the program sizes must be equal too, which
295means that the program size in the current iteration must be smaller than
29664 Kb. This contradicts the earlier hypothesis, hence not all branch
297instructions in the previous iteration are encoded as long jumps.
299The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
300the fact that we have reached a fixed point, i.e. the previous iteration and
301the current iteration are the same. This means that the results of
302{\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
304\subsection{Final properties}
306These are the invariants that hold after $2n$ iterations, where $n$ is the
307program size (we use the program size for convenience; we could also use the
308number of branch instructions, but this is more complex). Here, we only
309need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
310$\sigma(0) = 0$.
312Termination can now be proved using 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 branch instruction must be encoded as
318a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
319fixpoint is reached.
Note: See TracBrowser for help on using the repository browser.