Changeset 2085 for src/ASM/CPP2012policy/proof.tex
 Timestamp:
 Jun 15, 2012, 11:36:47 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r2084 r2085 5 5 6 6 The main correctness statement is as follows: 7 8 \clearpage 7 9 8 10 \begin{lstlisting} … … 55 57 $2n$ the number of jumps in the program. This worst case is reached if at every 56 58 iteration, we change the encoding of exactly one jump; since a jump can change 57 from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there58 c an be at most $2n$ changes.59 from short to absolute and from absolute to long, there can be at most $2n$ 60 changes. 59 61 60 62 This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}. … … 114 116 iteration, and $p$ the current one), jump lengths either remain equal or 115 117 increase. It is needed for proving termination. 118 119 \clearpage 116 120 117 121 \begin{lstlisting} … … 160 164 [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$ 161 165 \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$166  absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$ 167 \fst (absolute_jump_cond pc_plus_jmp_length addr) = true $\wedge$ 164 168 \fst (short_jump_cond pc_plus_jmp_length addr) = false 165 169  long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false 166 $\wedge$ \fst ( medium_jump_cond pc_plus_jmp_length addr) = false170 $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = false 167 171 ]. 168 172 \end{lstlisting} … … 200 204 We need to use two different formulations, because the fact that $added$ is 0 201 205 does not guarantee that no jumps have changed: it is possible that we have 202 replaced a short jump with a mediumjump, which does not change the size.206 replaced a short jump with a absolute jump, which does not change the size. 203 207 204 208 Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, … … 245 249 246 250 \begin{lstlisting} 247 definition sigma_compact : list labelled_instruction → label_map → ppc_pc_map → Prop:=248 λprogram .λlabels.λsigma.251 definition sigma_compact := 252 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. 249 253 ∀n.n < program → 250 254 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
Note: See TracChangeset
for help on using the changeset viewer.