Changeset 3342
 Timestamp:
 Jun 11, 2013, 2:13:21 PM (6 years ago)
 Location:
 src/ASM/CPP2012policy
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/main.tex
r3338 r3342 1 1 \documentclass[a4paper]{llncs} 2 2 \usepackage{algpseudocode} 3 %\usepackage{algorithmicx} 3 4 \usepackage{alltt} 4 5 \usepackage{amsfonts} … … 39 40 the proofs. 40 41 41 \keywords{formal verification, assembler, branch displacement optimisation}42 \keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation} 42 43 \end{abstract} 43 44 
src/ASM/CPP2012policy/proof.tex
r3341 r3342 6 6 7 7 \begin{align*} 8 \mathtt{sigma\_policy\_specification} \equiv8 & \mathtt{sigma\_policy\_specification} \equiv 9 9 \lambda program.\lambda sigma.\lambda policy. \notag\\ 10 sigma\ 0 = 0\ \wedge \notag\\11 \mathbf{let}\ instr\_list \equiv code\ program\ \mathbf{in} \notag\\12 \forall ppc.ppc < instr\_list \rightarrow \notag\\13 \mathbf{let}\ pc \equiv sigma\ ppc\ \mathbf{in} \notag\\14 \mathbf{let}\ instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\15 \mathbf{let}\ next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\16 next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\17 18 19 20 \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\21 pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})10 & sigma\ 0 = 0\ \wedge \notag\\ 11 & \mathbf{let} \ instr\_list \equiv code\ program\ \mathbf{in} \notag\\ 12 & \forall ppc.ppc < instr\_list \rightarrow \notag\\ 13 & \mathbf{let}\ pc \equiv sigma\ ppc\ \mathbf{in} \notag\\ 14 & \mathbf{let}\ instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\ 15 & \mathbf{let}\ next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\ 16 & next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\ 17 & (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\ 18 & (\forall ppc'.ppc' < instr\_list \rightarrow ppc < ppc' \rightarrow \notag\\ 19 & \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\ 20 &\ mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\ 21 & pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}) 22 22 \end{align*} 23 23 … … 67 67 pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component 68 68 is the number of bytes added to the program so far with respect to 69 the previous iteration, and the second component, {\tt ppc\_pc\_map}, is a pair70 consisting of the current size of the program and our $\sigma$ function.71 72 \begin{align*} 73 \mathtt{out\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\74 \forall i.i < 2^{16} \rightarrow (i > prefix \leftrightarrow75 \mathtt{lookup\_opt}\ i\ sigma= \mathtt{None})69 the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the 70 acual $\sigma$ trie. 71 72 \begin{align*} 73 & \mathtt{out\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\ 74 & \forall i.i < 2^{16} \rightarrow (i > prefix \leftrightarrow 75 \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ sigma) = \mathtt{None}) 76 76 \end{align*} 77 77 … … 80 80 81 81 \begin{align*} 82 \mathtt{not\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\83 \forall i.i < prefix \rightarrow\notag\\84 85 \mathtt{lookup}\ i\ sigma= \mathtt{short\_jump}82 & \mathtt{not\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\ 83 & \forall i.i < prefix \rightarrow\notag\\ 84 & \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\ 85 & \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma) = \mathtt{short\_jump} 86 86 \end{align*} 87 87 … … 91 91 92 92 \begin{align*} 93 \mathtt{jump\_increase} \equiv \lambda pc.\lambda op\lambda p.93 & \mathtt{jump\_increase} \equiv \lambda pc.\lambda op.\lambda p. 94 94 \forall i.i < prefix \rightarrow\notag\\ 95 \mathbf{let}\ oj \equiv \mathtt{lookup}\ i\ op\ \mathbf{in} \notag\\96 \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ p\ \mathbf{in} \notag\\97 95 & \mathbf{let}\ oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\ 96 & \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in} \notag\\ 97 & \mathtt{jmpleq}\ oj\ j 98 98 \end{align*} 99 99 … … 103 103 104 104 \begin{align*} 105 \mathtt{sigma\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.\notag\\106 \forall n.n < prefix \rightarrow\notag\\107 \mathbf{match}\ \mathtt{lookup\_opt}\ n\ sigma\ \mathbf{with}\notag\\108 \mathtt{None} \Rightarrow \mathrm{False} \notag\\109 \mathtt{Some}\ \langle pc, j \rangle \Rightarrow110 \mathbf{match}\ \mathtt{lookup\_opt}\ (n+1)\ sigma\ \mathbf{with}\notag\\111 112 105 & \mathtt{sigma\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.\notag\\ 106 & \forall n.n < prefix \rightarrow\notag\\ 107 & \mathbf{match}\ \mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\ 108 & \mathtt{None} \Rightarrow \mathrm{False} \notag\\ 109 & \mathtt{Some}\ \langle pc, j \rangle \Rightarrow 110 \mathbf{match}\ \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\ 111 & \mathtt{None} \Rightarrow \mathrm{False} \notag\\ 112 & \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow 113 113 pc_1 = pc + \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix) 114 114 \end{align*} … … 125 125 126 126 \begin{align*} 127 \mathtt{sigma\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma\notag\\128 \forall i.i < prefix \rightarrow \notag\\129 \mathbf{let}\ instr \equiv \mathtt{nth}\ i\ prefix\ \mathbf{in}\notag\\130 \forall dest\_label.\mathtt{is\_jump\_to\_instr}\ dest\_label \rightarrow\notag\\131 \mathbf{let}\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in} \notag\\132 \mathbf{let}\ \langle j, src, dest \rangle \equiv\notag\\133 \mathbf{if}\ paddr\ \leq\ i\ \mathbf{then}\notag\\134 \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ sigma\ \mathbf{in} \notag\\135 \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ sigma\ \mathbf{in}\notag\\136 \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ sigma\ \mathbf{in}\notag\\137 \langle j, pc\_plus\_jl, addr \rangle\notag\\138 \mathbf{else}\\139 \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ sigma\ \mathbf{in} \notag\\140 \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ old\_sigma\ \mathbf{in}\notag\\141 \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ old\_sigma\ \mathbf{in}\notag\\142 143 144 145 146 127 & \mathtt{sigma\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma\notag\\ 128 & \forall i.i < prefix \rightarrow \notag\\ 129 & \mathbf{let}\ instr \equiv \mathtt{nth}\ i\ prefix\ \mathbf{in}\notag\\ 130 & \forall dest\_label.\mathtt{is\_jump\_to\_instr}\ dest\_label \rightarrow\notag\\ 131 & \mathbf{let}\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in} \notag\\ 132 & \mathbf{let}\ \langle j, src, dest \rangle \equiv\notag\\ 133 & \mathbf{if}\ paddr\ \leq\ i\ \mathbf{then}\notag\\ 134 & \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\ 135 & \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\ 136 & \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\ 137 & \langle j, pc\_plus\_jl, addr \rangle\notag\\ 138 &\mathbf{else} \notag\\ 139 &\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\ 140 &\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\ 141 &\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\ 142 &\langle j, pc\_plus\_jl, addr \rangle\ \mathbf{in}\notag\\ 143 &\mathbf{match}\ j\ \mathbf{with} \notag\\ 144 &\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\ 145 &\mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\ 146 &\mathrm{long\_jump} \Rightarrow \mathrm{True} 147 147 \end{align*} 148 148 … … 155 155 the branch instruction (by changing the program counter again). 156 156 157 \begin{lstlisting} 158 \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? 0) (\snd policy) 159 $\langle$0,short_jump$\rangle$) = 0) 160 \fst policy = \fst (bvt_lookup $\ldots$ 161 (bitvector_of_nat ? (prefix)) (\snd policy) $\langle$0,short_jump$\rangle$) 162 \end{lstlisting} 157 \begin{align*} 158 & \mathtt{lookup}\ 0\ (\mathtt{snd}\ policy) = 0 \notag\\ 159 & \mathtt{lookup}\ prefix\ (\mathtt{snd}\ policy) = \mathtt{fst}\ policy 160 \end{align*} 163 161 164 162 These two properties give the values of $\sigma$ for the start and end of the … … 166 164 instructions up until now, is equal to the maximum memory address so far. 167 165 168 \begin{ lstlisting}169 (added = 0 $\rightarrow$ policy_pc_equal prefix old_sigma policy)) 170 (policy_jump_equal prefix old_sigma policy $\rightarrow$ added = 0)) 171 \end{ lstlisting}166 \begin{align*} 167 & added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_sigma\ policy \notag\\ 168 & \mathtt{policy\_jump\_equal}\ prefix\ old\_sigma\ policy\ \rightarrow\ added = 0 169 \end{align*} 172 170 173 171 And finally, two properties that deal with what happens when the previous … … 203 201 If an iteration returns {\tt None}, we have the following invariant: 204 202 205 \clearpage 206 \begin{lstlisting} 207 definition nec_plus_ultra := 208 $\lambda$program:list labelled_instruction.$\lambda$p:ppc_pc_map. 209 ¬($\forall$i.i < program $\rightarrow$ 210 is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$)) $\rightarrow$ 211 \snd (bvt_lookup $\ldots$ (bitvector_of_nat 16 i) (\snd p) $\langle$0,short_jump$\rangle$) = 212 long_jump). 213 \end{lstlisting} 203 \begin{align*} 204 & \mathtt{nec\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\ 205 &\neg(\forall i.i < program\ \rightarrow \notag\\ 206 & \mathtt{is\_jump}\ (\mathtt{nth}\ i\ program)\ \rightarrow \notag\\ 207 & \mathtt{lookup}\ i\ (\mathtt{snd}\ p) = \mathrm{long\_jump}). 208 \end{align*} 214 209 215 210 This invariant is applied to $old\_sigma$; if our program becomes too large … … 226 221 invariant: 227 222 228 \begin{lstlisting} 229 definition sigma_compact := 230 $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map. 231 $\forall$n.n < program $\rightarrow$ 232 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with 233 [ None $\Rightarrow$ False 234  Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in 235 match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with 236 [ None $\Rightarrow$ False 237  Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in 238 pc1 = pc + instruction_size 239 ($\lambda$id.bitvector_of_nat ? (lookup_def ?? labels id 0)) 240 ($\lambda$ppc.bitvector_of_nat ? 241 (\fst (bvt_lookup $\ldots$ ppc (\snd sigma) $\langle$0,short_jump$\rangle$))) 242 ($\lambda$ppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc 243 (\snd sigma) $\langle$0,short_jump$\rangle$))) (bitvector_of_nat ? n) 244 (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)) 245 ] 246 ]. 247 \end{lstlisting} 223 \begin{align*} 224 & \mathtt{sigma\_compact} \equiv \lambda program.\lambda sigma. \notag\\ 225 & \forall n.n < program\ \rightarrow \notag\\ 226 & \mathbf{match}\ \mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\ 227 & \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\ 228 & \mathrm{Some}\ \langle pc, j \rangle \Rightarrow\notag\\ 229 & \mathbf{match}\ \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\ 230 & \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\ 231 & \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\ 232 & pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program) 233 \end{align*} 234 248 235 249 236 This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it … … 257 244 258 245 There is another, trivial, invariant if the iteration returns 259 $\mathtt{Some}\ \sigma$: 260 261 \begin{lstlisting} 262 \fst p < 2^16 263 \end{lstlisting} 246 $\mathtt{Some}\ \sigma$: $\mathtt{fst}\ sigma = 2^{16}$. 264 247 265 248 The invariants that are taken directly from the fold invariants are trivial to
Note: See TracChangeset
for help on using the changeset viewer.