 Timestamp:
 Jun 14, 2013, 1:13:57 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2012policy/proof.tex
r3342 r3352 4 4 detail. The main correctness statement is as follows (slightly simplified, here): 5 5 6 7 \begin{align*} 8 & \mathtt{sigma\_policy\_specification} \equiv 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 & (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 \end{align*} 6 \begin{alignat*}{6} 7 \mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv 8 \lambda program.\lambda sigma.\lambda policy.$} \notag\\ 9 & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\ 10 & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}$} \notag\\ 11 &&& \omit\rlap{$\forall ppc.ppc < instr\_list \rightarrow$} \notag\\ 12 &&& \mathbf{let}\ && pc \equiv sigma\ ppc\ \mathbf{in} \notag\\ 13 &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\ 14 &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\ 15 &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\ 16 &&&&& (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\ 17 &&&&& (\forall ppc'.ppc' < instr\_list \rightarrow ppc < ppc' \rightarrow \notag\\ 18 &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\ 19 &&&&&\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\ 20 &&&&& pc + (\mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})) 21 \end{alignat*} 23 22 24 23 Informally, this means that when fetching a pseudoinstruction at $ppc$, the … … 70 69 acual $\sigma$ trie. 71 70 72 \begin{align *}73 & \mathtt{out\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\71 \begin{alignat*}{2} 72 \mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\ 74 73 & \forall i.i < 2^{16} \rightarrow (i > prefix \leftrightarrow 75 74 \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ sigma) = \mathtt{None}) 76 \end{align *}75 \end{alignat*} 77 76 78 77 This invariant states that any pseudoaddress not yet examined is not 79 78 present in the lookup trie. 80 79 81 \begin{align *}82 & \mathtt{not\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\80 \begin{alignat*}{2} 81 \mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\ 83 82 & \forall i.i < prefix \rightarrow\notag\\ 84 83 & \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\ 85 84 & \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma) = \mathtt{short\_jump} 86 \end{align *}85 \end{alignat*} 87 86 88 87 This invariant states that when we try to look up the jump length of a … … 90 89 value, a short jump. 91 90 92 \begin{align *}93 & \mathtt{jump\_increase} \equiv \lambda pc.\lambda op.\lambda p. 94 \forall i.i < prefix \rightarrow\notag\\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\ j98 \end{align *}91 \begin{alignat*}{4} 92 \mathtt{jump} & \omit\rlap{$\mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.$} \notag\\ 93 & \omit\rlap{$\forall i.i < prefix \rightarrow$} \notag\\ 94 & \mathbf{let}\ && oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\ 95 & \mathbf{let}\ && j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in} \notag\\ 96 &&& \mathtt{jmpleq}\ oj\ j 97 \end{alignat*} 99 98 100 99 This invariant states that between iterations (with $op$ being the previous … … 102 101 increase. It is needed for proving termination. 103 102 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\ (\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 pc_1 = pc + \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix) 114 \end{align*} 103 \begin{alignat*}{6} 104 \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\ 105 & \omit\rlap{$\forall n.n < prefix \rightarrow$}\notag\\ 106 & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\ 107 &&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\ 108 &&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\ 109 &&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\ 110 &&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\ 111 &&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow 112 pc_1 = pc + \notag\\ 113 &&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix) 114 \end{alignat*} 115 115 116 116 This is a temporary formulation of the main property\\ … … 124 124 property. 125 125 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\ (\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 \end{align *}126 \begin{alignat*}{6} 127 \mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\ 128 & \omit\rlap{$\forall i.i < prefix \rightarrow$} \notag\\ 129 & \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\ 130 & \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\ 131 & \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv$}\notag\\ 132 &&& \omit\rlap{$\mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\ 133 &&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\ 134 &&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\ 135 &&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\ 136 &&&&& \langle j, pc\_plus\_jl, addr \rangle\notag\\ 137 &&&\mathbf{else} \notag\\ 138 &&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\ 139 &&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\ 140 &&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\ 141 &&&&&\langle j, pc\_plus\_jl, addr \rangle\notag\\ 142 &&&\omit\rlap{$\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 \end{alignat*} 148 148 149 149 This is a more direct safety property: it states that branch instructions are … … 201 201 If an iteration returns {\tt None}, we have the following invariant: 202 202 203 \begin{align *}204 & \mathtt{nec\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\203 \begin{alignat*}{2} 204 \mathtt{nec} & \mathtt{\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\ 205 205 &\neg(\forall i.i < program\ \rightarrow \notag\\ 206 206 & \mathtt{is\_jump}\ (\mathtt{nth}\ i\ program)\ \rightarrow \notag\\ 207 207 & \mathtt{lookup}\ i\ (\mathtt{snd}\ p) = \mathrm{long\_jump}). 208 \end{align *}208 \end{alignat*} 209 209 210 210 This invariant is applied to $old\_sigma$; if our program becomes too large … … 221 221 invariant: 222 222 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 *}223 \begin{alignat*}{6} 224 \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact} \equiv \lambda program.\lambda sigma.$} \notag\\ 225 & \omit\rlap{$\forall n.n < program\ \rightarrow$} \notag\\ 226 & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\ 227 &&& \omit\rlap{$\mathrm{None}\ \Rightarrow\ \mathrm{False}$}\notag\\ 228 &&& \omit\rlap{$\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{alignat*} 234 234 235 235
Note: See TracChangeset
for help on using the changeset viewer.