Changeset 2082
 Timestamp:
 Jun 14, 2012, 4:26:23 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r2080 r2082 4 4 detail. 5 5 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: 6 The main correctness statement is as follows: 81 7 82 8 \begin{lstlisting} … … 96 22 let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in 97 23 (nat_of_bitvector $\ldots$ ppc ≤ instr_list → 98 next_pc = add 16pc (bitvector_of_nat $\ldots$24 next_pc = add ? pc (bitvector_of_nat $\ldots$ 99 25 (instruction_size lookup_labels sigma policy ppc instruction))) 100 26 $\wedge$ … … 118 44 And finally, we enforce that the program starts at address 0, i.e. 119 45 $\sigma(0) = 0$. 46 47 Since our computation is a least fixed point computation, we must prove 48 termination in order to prove correctness: if the algorithm is halted after 49 a number of steps without reaching a fixed point, the solution is not 50 guaranteed to be correct. More specifically, jumps might be encoded whose 51 displacement is too great for the instruction chosen. 52 53 Proof of termination rests on the fact that jumps can only increase, which 54 means 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 56 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}, there 58 can be at most $2n$ changes. 59 60 This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}. 61 We have proven some invariants of the {\sc f} function from the previous 62 section; these invariants are then used to prove properties that hold for every 63 iteration of the fixed point computation; and finally, we can prove some 64 properties of the fixed point. 65 66 \subsection{Fold invariants} 67 68 These are the invariants that hold during the fold of {\sc f} over the program, 69 and that will later on be used to prove the properties of the iteration. 70 71 Note that during the fixed point computation, the $\sigma$ function is 72 implemented as a trie for ease access; computing $\sigma(x)$ is done by looking 73 up the value of $x$ in the trie. Actually, during the fold, the value we 74 pass along is a couple $\mathbb{N} \times \mathtt{ppc_pc_map}$. The natural 75 number is the number of bytes added to the program so far with respect to 76 the previous iteration, and {\tt ppc\_pc\_map} is a couple of the current 77 size of the program and our $\sigma$ function. 78 79 \begin{lstlisting} 80 definition 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 86 This invariant states that every pseudoaddress not yet treated cannot be 87 found in the lookup trie. 88 89 \begin{lstlisting} 90 definition 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 98 This invariant states that when we try to look up the jump length of a 99 pseudoaddress where there is no jump, we will get the default value, a short 100 jump. 101 102 \begin{lstlisting} 103 definition 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 113 This invariant states that between iterations ($op$ being the previous 114 iteration, and $p$ the current one), jump lengths either remain equal or 115 increase. It is needed for proving termination. 116 117 \begin{lstlisting} 118 definition 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 133 This is a temporary formulation of the main property 134 ({\tt sigma\_policy\_specification}); its main difference 135 with the final version is that it uses {\tt instruction\_size\_jmplen} to 136 compute the instruction size. This function uses $j$ to compute the size 137 of jumps (i.e. it uses the $\sigma$ function under construction), instead 138 of 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 140 final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main 141 property. 142 143 \begin{lstlisting} 144 definition 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 170 This is a more direct safety property: it states that jump instructions are 171 encoded properly, and that no wrong jump instructions are chosen. 172 173 Note that we compute the distance using the memory address of the instruction 174 plus its size: this is due to the behaviour of the MCS51 architecture, which 175 increases the program counter directly after fetching, and only then executes 176 the 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 185 These two properties give the values of $\sigma$ for the start and end of the 186 program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of 187 instructions 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 194 And finally, two properties that deal with what happens when the previous 195 iteration does not change with respect to the current one. $added$ is the 196 variable that keeps track of the number of bytes we have added to the program 197 size by changing jumps; if this is 0, the program has not changed and vice 198 versa. 199 200 We need to use two different formulations, because the fact that $added$ is 0 201 does not guarantee that no jumps have changed: it is possible that we have 202 replaced a short jump with a medium jump, which does not change the size. 203 204 Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, 205 whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$. 206 This formulation is sufficient to prove termination and compactness. 207 208 Proving these invariants is simple, usually by induction on the prefix length. 209 210 \subsection{Iteration invariants} 211 212 These are invariants that hold after the completion of an iteration. The main 213 difference between these invariants and the fold invariants is that after the 214 completion of the fold, we check whether the program size does not supersede 215 65 Kbytes (the maximum memory size the MCS51 can address). 216 217 The type of an iteration therefore becomes an option type: {\tt None} in case 218 the program becomes larger than 65 KBytes, or $\mathtt{Some}\ \sigma$ 219 otherwise. We also no longer use a natural number to pass along the number of 220 bytes added to the program size, but a boolean that indicates whether we have 221 changed something during the iteration or not. 222 223 If an iteration returns {\tt None}, we have the following invariant: 224 225 \begin{lstlisting} 226 definition 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 234 This invariant is applied to $old\_sigma$; if our program becomes too large 235 for memory, the previous iteration cannot have every jump encoded as a long 236 jump. This is needed later on in the proof of termination. 237 238 If the iteration returns $\mathtt{Some}\ \sigma$, the invariants 239 {\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase}, 240 and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are 241 retained without change. 242 243 Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper 244 invariant: 245 246 \begin{lstlisting} 247 definition 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 267 This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it 268 computes the sizes of jump instructions by looking at the distance between 269 position and destination using $\sigma$. 270 271 In actual use, the invariant is qualified: $\sigma$ is compact if there have 272 been no changes (i.e. the boolean passed along is {\tt true}). This is to 273 reflect the fact that we are doing a least fixed point computation: the result 274 is only correct when we have reached the fixed point. 275 276 There 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 283 The invariants that are taken directly from the fold invariants are trivial to 284 prove. 285 286 The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None}, 287 then the program size must be greater than 65 Kbytes. However, since the 288 previous iteration did not return {\tt None} (because otherwise we would 289 terminate immediately), the program size in the previous iteration must have 290 been smaller than 65 Kbytes. 291 292 Suppose that all the jumps in the previous iteration are long jumps. This means 293 that all jumps in this iteration are long jumps as well, and therefore that 294 both iterations are equal in jumps. Per the invariant, this means that 295 $added = 0$, and therefore that all addresses in both iterations are equal. 296 But if all addresses are equal, the program sizes must be equal too, which 297 means that the program size in the current iteration must be smaller than 298 65 Kbytes. This contradicts the earlier hypothesis, hence not all jumps in 299 the previous iteration are long jumps. 300 301 The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and 302 the fact that we have reached a fixed point, i.e. the previous iteration and 303 the 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 308 These are the invariants that hold after $2n$ iterations, where $n$ is the 309 program 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.