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

Last change on this file since 2064 was 2064, checked in by boender, 7 years ago
  • more progress
File size: 2.9 KB
1\section{The proof}
3In this section, we will present the correctness proof of the algorithm in more
6Since our computation is a least fixed point computation, we must prove
7termination in order to prove correctness: if the algorithm is halted after
8a number of steps without reaching a fixed point, the solution is not
9guaranteed to be correct. More specifically, jumps might be encoded whose
10displacement is too great for the instruction chosen.
12Proof of termination rests on the fact that jumps can only increase, which
13means that we must reach a fixed point after at most $2n$ iterations, with
14$2n$ the number of jumps in the program. This worst case is reached if at every
15iteration, we change the encoding of exactly one jump; since a jump can change
16from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
17can be at most $2n$ changes.
19This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
20We have proven some invariants of the {\sc f} function from the previous
21section; these invariants are then used to prove properties that hold for every
22iteration of the fixed point computation; and finally, we can prove some
23properties of the fixed point.
25The main correctness statement, then, is as follows:
28definition jump_expansion':
29$\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (|l|) < 2^16).
30 option ($\Sigma$sigma:Word → Word $\times$ bool.
31  $\forall$ppc: Word.$\forall$ppc_ok.
32   let pc := \fst (sigma ppc) in
33   let labels := \fst (create_label_cost_map (\snd program)) in
34   let lookup_labels :=
35    $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
36   let instruction :=
37    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
38   let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
39    And (nat_of_bitvector $\ldots$ ppc $\leq$ |\snd program| →
40     next_pc = add ? pc (bitvector_of_nat $\ldots$
41      (instruction_size lookup_labels ($\lambda$x.\fst (sigma x))
42       ($\lambda$x.\snd (sigma x)) ppc instruction))
43    )
44    (Or (nat_of_bitvector $\ldots$ ppc < |\snd program| →
45     nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
46    (nat_of_bitvector $\ldots$ ppc = |\snd program| → next_pc = (zero $\ldots$))))
49Informally, this means that when fetching a pseudo-instruction at $ppc$, the
50translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
51of the instruction at $ppc$; i.e. an instruction is placed immediately
52after the previous one, and there are no overlaps.
54The other condition enforced is the fact that instructions are stocked in
55order: the memory address of the instruction at $ppc$ should be smaller than
56the memory address of the instruction at $ppc+1$. There is one exeception to
57this rule: the instruction at the very end of the program, whose successor
58address can be zero (this is the case where the program size is exactly equal
59to the amount of memory).
Note: See TracBrowser for help on using the repository browser.