# Changeset 2085 for src/ASM/CPP2012-policy/proof.tex

Ignore:
Timestamp:
Jun 15, 2012, 11:36:47 AM (8 years ago)
Message:
• rewrote introduction
• changed 'medium' to 'absolute'
• added a bit to conclusion (CompCert?, Piton, ...)
File:
1 edited

### Legend:

Unmodified
 r2084 The main correctness statement is as follows: \clearpage \begin{lstlisting} $2n$ the number of jumps in the program. This worst case is reached if at every iteration, we change the encoding of exactly one jump; since a jump can change from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there can be at most $2n$ changes. from short to absolute and from absolute to long, there can be at most $2n$ changes. This proof has been executed in the Russell'' style from~\cite{Sozeau2006}. iteration, and $p$ the current one), jump lengths either remain equal or increase. It is needed for proving termination. \clearpage \begin{lstlisting} [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$ \fst (short_jump_cond pc_plus_jmp_length addr) = true | medium_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$ \fst (medium_jump_cond pc_plus_jmp_length addr) = true $\wedge$ | absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true $\wedge$ \fst (short_jump_cond pc_plus_jmp_length addr) = false | long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false $\wedge$ \fst (medium_jump_cond pc_plus_jmp_length addr) = false $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = false ]. \end{lstlisting} We need to use two different formulations, because the fact that $added$ is 0 does not guarantee that no jumps have changed: it is possible that we have replaced a short jump with a medium jump, which does not change the size. replaced a short jump with a absolute jump, which does not change the size. Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, \begin{lstlisting} definition sigma_compact: list labelled_instruction → label_map → ppc_pc_map → Prop := λprogram.λlabels.λsigma. definition sigma_compact := λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. ∀n.n < |program| → match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with