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

Last change on this file since 2065 was 2065, checked in by boender, 9 years ago
  • committed another draft
File size: 5.6 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 invariants for the fold function. Note that during the fixed point
26computation, the $sigma$ functions are implemented as tries, so in order to
27compute $sigma(i)$, we lookup the value for $i$ in the corresponding trie.
30(out_of_program_none prefix policy) $\wedge$
31(jump_not_in_policy prefix policy) $\wedge$
32(policy_increase prefix old_sigma policy) $\wedge$
33(policy_compact_unsafe prefix labels policy) $\wedge$
34(policy_safe prefix labels added old_sigma policy) $\wedge$
35(\fst (bvt_lookup $\ldots$
36  (bitvector_of_nat ? 0) (\snd policy) $\langle$0,short_jump$\rangle$) = 0) $\wedge$
37(\fst policy = \fst (bvt_lookup $\ldots$
38  (bitvector_of_nat ? (|prefix|)) (\snd policy) $\langle$0,short_jump$\rangle$)) $\wedge$
39(added = 0 → policy_pc_equal prefix old_sigma policy) $\wedge$
40(policy_jump_equal prefix old_sigma policy → added = 0)
43These invariants have the following meanings:
46        \item {\tt out\_of\_program\_none} shows that if we try to lookup a value
47beyond the program, we will get an empty result;
48        \item {\tt jump\_not\_in\_policy} shows that an instruction that is not a jump
49will have a {\tt short\_jump} as its associated jump length;
50        \item {\tt policy\_increase} shows that between iterations, jumps either increase (i.e. from {\tt short\_jump} to {\tt medium\_jump} or from {\tt medium\_jump} to {\tt long\_jump}) or remain equal;
51        \item {\tt policy\_compact\_unsafe} shows that the policy is compact (instrucftions directly follow each other and do not overlap);
52        \item {\tt policy\_safe} shows that jumps selected are appropriate for the
53distance between their position and their target, and the jumps selected are
54the smallest possible;
55        \item Then there are two properties that fix the values of $\sigma(0)$ and
56$\sigma(n)$ (with $n$ the size of the program);
57        \item And finally two predicates that link the value of $added$ to reaching
58of a fixed point.
62($\Sigma$x:bool × (option ppc_pc_map).
63 let $\langle$no_ch,y$\rangle$ := x in
64 match y with
65 [ None ⇒ nec_plus_ultra program old_policy
66 | Some p ⇒ (out_of_program_none program p) $\wedge$
67    (jump_not_in_policy program p) $\wedge$
68    (policy_increase program old_policy p) $\wedge$
69    (no_ch = true → policy_compact program labels p) $\wedge$
70    (\fst (bvt_lookup $\ldots$
71      (bitvector_of_nat ? 0) (\snd p) $\langle$0,short_jump$\rangle$) = 0) $\wedge$
72    (\fst p = \fst (bvt_lookup $\ldots$
73      (bitvector_of_nat ? (|program|)) (\snd p) $\langle$0,short_jump$\rangle$)) $\wedge$
74    (no_ch = true $\rightarrow$ policy_pc_equal program old_policy p) $\wedge$
75    (policy_jump_equal program old_policy p $\rightarrow$ no_ch = true) $\wedge$
76    (\fst p < 2^16)
77 ])
80The main correctness statement, then, is as follows:
83definition jump_expansion':
84$\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (|l|) < 2^16).
85 option ($\Sigma$sigma:Word → Word $\times$ bool.
86  $\forall$ppc: Word.$\forall$ppc_ok.
87   let pc := \fst (sigma ppc) in
88   let labels := \fst (create_label_cost_map (\snd program)) in
89   let lookup_labels :=
90    $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
91   let instruction :=
92    \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
93   let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
94    And (nat_of_bitvector $\ldots$ ppc $\leq$ |\snd program| →
95     next_pc = add ? pc (bitvector_of_nat $\ldots$
96      (instruction_size lookup_labels ($\lambda$x.\fst (sigma x))
97       ($\lambda$x.\snd (sigma x)) ppc instruction))
98    )
99    (Or (nat_of_bitvector $\ldots$ ppc < |\snd program| →
100     nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
101    (nat_of_bitvector $\ldots$ ppc = |\snd program| → next_pc = (zero $\ldots$))))
104Informally, this means that when fetching a pseudo-instruction at $ppc$, the
105translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
106of the instruction at $ppc$; i.e. an instruction is placed immediately
107after the previous one, and there are no overlaps.
109The other condition enforced is the fact that instructions are stocked in
110order: the memory address of the instruction at $ppc$ should be smaller than
111the memory address of the instruction at $ppc+1$. There is one exeception to
112this rule: the instruction at the very end of the program, whose successor
113address can be zero (this is the case where the program size is exactly equal
114to the amount of memory).
Note: See TracBrowser for help on using the repository browser.