Changeset 2082


Ignore:
Timestamp:
Jun 14, 2012, 4:26:23 PM (5 years ago)
Author:
boender
Message:
  • reworked and extended presentation of invariants
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-policy/proof.tex

    r2080 r2082  
    44detail.
    55
    6 Since our computation is a least fixed point computation, we must prove
    7 termination in order to prove correctness: if the algorithm is halted after
    8 a number of steps without reaching a fixed point, the solution is not
    9 guaranteed to be correct. More specifically, jumps might be encoded whose
    10 displacement is too great for the instruction chosen.
    11 
    12 Proof of termination rests on the fact that jumps can only increase, which
    13 means 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
    15 iteration, we change the encoding of exactly one jump; since a jump can change
    16 from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
    17 can be at most $2n$ changes.
    18 
    19 This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
    20 We have proven some invariants of the {\sc f} function from the previous
    21 section; these invariants are then used to prove properties that hold for every
    22 iteration of the fixed point computation; and finally, we can prove some
    23 properties of the fixed point.
    24 
    25 The invariants for the fold function. Note that during the fixed point
    26 computation, the $sigma$ functions are implemented as tries, so in order to
    27 compute $sigma(i)$, we lookup the value for $i$ in the corresponding trie.
    28 
    29 \begin{lstlisting}
    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)
    41 \end{lstlisting}
    42 
    43 These invariants have the following meanings:
    44 
    45 \begin{itemize}
    46         \item {\tt out\_of\_program\_none} shows that if we try to lookup a value
    47 beyond the program, we will get an empty result;
    48         \item {\tt jump\_not\_in\_policy} shows that an instruction that is not a jump
    49 will 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
    53 distance between their position and their target, and the jumps selected are
    54 the 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
    58 of a fixed point.
    59 \end{itemize}
    60 
    61 \begin{lstlisting}
    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  ])
    78 \end{lstlisting}
    79 
    80 The main correctness statement, then, is as follows:
     6The main correctness statement is as follows:
    817
    828\begin{lstlisting}
     
    9622 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
    9723  (nat_of_bitvector $\ldots$ ppc ≤ |instr_list| →
    98    next_pc = add 16 pc (bitvector_of_nat $\ldots$
     24   next_pc = add ? pc (bitvector_of_nat $\ldots$
    9925   (instruction_size lookup_labels sigma policy ppc instruction)))
    10026  $\wedge$     
     
    11844And finally, we enforce that the program starts at address 0, i.e.
    11945$\sigma(0) = 0$.
     46
     47Since our computation is a least fixed point computation, we must prove
     48termination in order to prove correctness: if the algorithm is halted after
     49a number of steps without reaching a fixed point, the solution is not
     50guaranteed to be correct. More specifically, jumps might be encoded whose
     51displacement is too great for the instruction chosen.
     52
     53Proof of termination rests on the fact that jumps can only increase, which
     54means that we must reach a fixed point after at most $2n$ iterations, with
     55$2n$ the number of jumps in the program. This worst case is reached if at every
     56iteration, we change the encoding of exactly one jump; since a jump can change
     57from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
     58can be at most $2n$ changes.
     59
     60This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
     61We have proven some invariants of the {\sc f} function from the previous
     62section; these invariants are then used to prove properties that hold for every
     63iteration of the fixed point computation; and finally, we can prove some
     64properties of the fixed point.
     65
     66\subsection{Fold invariants}
     67
     68These are the invariants that hold during the fold of {\sc f} over the program,
     69and that will later on be used to prove the properties of the iteration.
     70
     71Note that during the fixed point computation, the $\sigma$ function is
     72implemented as a trie for ease access; computing $\sigma(x)$ is done by looking
     73up the value of $x$ in the trie. Actually, during the fold, the value we
     74pass along is a couple $\mathbb{N} \times \mathtt{ppc_pc_map}$. The natural
     75number is the number of bytes added to the program so far with respect to
     76the previous iteration, and {\tt ppc\_pc\_map} is a couple of the current
     77size of the program and our $\sigma$ function.
     78
     79\begin{lstlisting}
     80definition out_of_program_none :=
     81 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map.
     82 $\forall$i.i < 2^16 → (i > |prefix| $\leftrightarrow$
     83  bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?).
     84\end{lstlisting}
     85
     86This invariant states that every pseudo-address not yet treated cannot be
     87found in the lookup trie.
     88
     89\begin{lstlisting}
     90definition not_jump_default ≝
     91 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map.
     92 $\forall$i.i < |prefix| →
     93  ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) →
     94  \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma)
     95   $\langle$0,short_jump$\rangle$) = short_jump.
     96\end{lstlisting}
     97
     98This invariant states that when we try to look up the jump length of a
     99pseudo-address where there is no jump, we will get the default value, a short
     100jump.
     101
     102\begin{lstlisting}
     103definition jump_increase :=
     104 λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map.
     105 ∀i.i ≤ |prefix| →
     106 let $\langle$opc,oj$\rangle$ :=
     107  bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in
     108 let $\langle$pc,j$\rangle$ :=
     109  bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd p) $\langle$0,short_jump$\rangle$ in
     110  jmpleq oj j.
     111\end{lstlisting}
     112
     113This invariant states that between iterations ($op$ being the previous
     114iteration, and $p$ the current one), jump lengths either remain equal or
     115increase. It is needed for proving termination.
     116
     117\begin{lstlisting}
     118definition sigma_compact_unsafe :=
     119 λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
     120 ∀n.n < |program| →
     121  match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
     122  [ None ⇒ False
     123  | Some x ⇒ let $\langle$pc,j$\rangle$ := x in
     124    match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with
     125    [ None ⇒ False
     126    | Some x1 ⇒ let $\langle$pc1,j1$\rangle$ ≝ x1 in
     127       pc1 = pc + instruction_size_jmplen j
     128        (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)))
     129    ]
     130  ].
     131\end{lstlisting}
     132
     133This is a temporary formulation of the main property
     134({\tt sigma\_policy\_specification}); its main difference
     135with the final version is that it uses {\tt instruction\_size\_jmplen} to
     136compute the instruction size. This function uses $j$ to compute the size
     137of jumps (i.e. it uses the $\sigma$ function under construction), instead
     138of looking at the distance between source and destination. This is because
     139$\sigma$ is still under construction; later on we will prove that after the
     140final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
     141property.
     142
     143\begin{lstlisting}
     144definition sigma_safe :=
     145 λprefix:list labelled_instruction.λlabels:label_map.λadded:$\mathbb{N}$.
     146 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map.
     147 ∀i.i < |prefix| → let $\langle$pc,j$\rangle$ :=
     148  bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in
     149  let pc_plus_jmp_length := bitvector_of_nat ?  (\fst (bvt_lookup $\ldots$
     150   (bitvector_of_nat ? (S i)) (\snd sigma) $\langle$0,short_jump$\rangle$)) in
     151  let $\langle$label,instr$\rangle$ := nth i ? prefix $\langle$None ?, Comment [ ]$\rangle$ in
     152   $\forall$dest.is_jump_to instr dest $\rightarrow$
     153    let paddr := lookup_def $\ldots$ labels dest 0 in
     154    let addr := bitvector_of_nat ? (if leb i paddr (* forward jump *)
     155    then \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd old_sigma)
     156     $\langle$0,short_jump$\rangle$) + added
     157    else \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd sigma)
     158     $\langle$0,short_jump$\rangle$)) in
     159    match j with
     160    [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$
     161       \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$
     164       \fst (short_jump_cond pc_plus_jmp_length addr) = false
     165    | long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false
     166       $\wedge$ \fst (medium_jump_cond pc_plus_jmp_length addr) = false
     167    ].
     168\end{lstlisting}
     169
     170This is a more direct safety property: it states that jump instructions are
     171encoded properly, and that no wrong jump instructions are chosen.
     172
     173Note that we compute the distance using the memory address of the instruction
     174plus its size: this is due to the behaviour of the MCS-51 architecture, which
     175increases the program counter directly after fetching, and only then executes
     176the jump.
     177
     178\begin{lstlisting}
     179\fst (bvt_lookup $\ldots$ (bitvector_of_nat ? 0) (\snd policy)
     180 $\langle$0,short_jump$\rangle$) = 0)
     181\fst policy = \fst (bvt_lookup $\ldots$
     182 (bitvector_of_nat ? (|prefix|)) (\snd policy) $\langle$0,short_jump$\rangle$)
     183\end{lstlisting}
     184
     185These two properties give the values of $\sigma$ for the start and end of the
     186program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of
     187instructions up until now, is equal to the maximum memory address so far.
     188
     189\begin{lstlisting}
     190(added = 0 → policy_pc_equal prefix old_sigma policy))
     191(policy_jump_equal prefix old_sigma policy → added = 0))
     192\end{lstlisting}
     193
     194And finally, two properties that deal with what happens when the previous
     195iteration does not change with respect to the current one. $added$ is the
     196variable that keeps track of the number of bytes we have added to the program
     197size by changing jumps; if this is 0, the program has not changed and vice
     198versa.
     199
     200We need to use two different formulations, because the fact that $added$ is 0
     201does not guarantee that no jumps have changed: it is possible that we have
     202replaced a short jump with a medium jump, which does not change the size.
     203
     204Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
     205whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$.
     206This formulation is sufficient to prove termination and compactness.
     207
     208Proving these invariants is simple, usually by induction on the prefix length.
     209
     210\subsection{Iteration invariants}
     211
     212These are invariants that hold after the completion of an iteration. The main
     213difference between these invariants and the fold invariants is that after the
     214completion of the fold, we check whether the program size does not supersede
     21565 Kbytes (the maximum memory size the MCS-51 can address).
     216
     217The type of an iteration therefore becomes an option type: {\tt None} in case
     218the program becomes larger than 65 KBytes, or $\mathtt{Some}\ \sigma$
     219otherwise. We also no longer use a natural number to pass along the number of
     220bytes added to the program size, but a boolean that indicates whether we have
     221changed something during the iteration or not.
     222
     223If an iteration returns {\tt None}, we have the following invariant:
     224
     225\begin{lstlisting}
     226definition nec_plus_ultra :=
     227 λprogram:list labelled_instruction.λp:ppc_pc_map.
     228 ¬(∀i.i < |program| →
     229  is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$)) →
     230  \snd (bvt_lookup $\ldots$ (bitvector_of_nat 16 i) (\snd p) $\langle$0,short_jump$\rangle$) =
     231   long_jump).
     232\end{lstlisting}
     233
     234This invariant is applied to $old\_sigma$; if our program becomes too large
     235for memory, the previous iteration cannot have every jump encoded as a long
     236jump. This is needed later on in the proof of termination.
     237
     238If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
     239{\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase},
     240and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
     241retained without change.
     242
     243Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
     244invariant:
     245
     246\begin{lstlisting}
     247definition sigma_compact: list labelled_instruction → label_map → ppc_pc_map → Prop :=
     248 λprogram.λlabels.λsigma.
     249 ∀n.n < |program| →
     250  match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
     251  [ None ⇒ False
     252  | Some x ⇒ let $\langle$pc,j$\rangle$ := x in
     253    match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with
     254    [ None ⇒ False
     255    | Some x1 ⇒ let $\langle$pc1,j1$\rangle$ := x1 in
     256      pc1 = pc + instruction_size
     257       (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
     258       (λppc.bitvector_of_nat ?
     259        (\fst (bvt_lookup $\ldots$ ppc (\snd sigma) $\langle$0,short_jump$\rangle$)))
     260       (λppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc
     261        (\snd sigma) $\langle$0,short_jump$\rangle$))) (bitvector_of_nat ? n)
     262       (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$))
     263    ]
     264  ].
     265\end{lstlisting}
     266
     267This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it
     268computes the sizes of jump instructions by looking at the distance between
     269position and destination using $\sigma$.
     270
     271In actual use, the invariant is qualified: $\sigma$ is compact if there have
     272been no changes (i.e. the boolean passed along is {\tt true}). This is to
     273reflect the fact that we are doing a least fixed point computation: the result
     274is only correct when we have reached the fixed point.
     275
     276There is another, trivial, invariant if the iteration returns
     277$\mathtt{Some}\ \sigma$:
     278
     279\begin{lstlisting}
     280\fst p < 2^16
     281\end{lstlisting}
     282
     283The invariants that are taken directly from the fold invariants are trivial to
     284prove.
     285
     286The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None},
     287then the program size must be greater than 65 Kbytes. However, since the
     288previous iteration did not return {\tt None} (because otherwise we would
     289terminate immediately), the program size in the previous iteration must have
     290been smaller than 65 Kbytes.
     291
     292Suppose that all the jumps in the previous iteration are long jumps. This means
     293that all jumps in this iteration are long jumps as well, and therefore that
     294both iterations are equal in jumps. Per the invariant, this means that
     295$added = 0$, and therefore that all addresses in both iterations are equal.
     296But if all addresses are equal, the program sizes must be equal too, which
     297means that the program size in the current iteration must be smaller than
     29865 Kbytes. This contradicts the earlier hypothesis, hence not all jumps in
     299the previous iteration are long jumps.
     300
     301The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
     302the fact that we have reached a fixed point, i.e. the previous iteration and
     303the current iteration are the same. This means that the results of
     304{\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
     305
     306\subsection{Final properties}
     307
     308These are the invariants that hold after $2n$ iterations, where $n$ is the
     309program size. Here, we only need {\tt out\_of\_program\_none},
     310{\tt sigma\_compact} and the fact that $\sigma(0) = 0$.
Note: See TracChangeset for help on using the changeset viewer.