Changeset 3352


Ignore:
Timestamp:
Jun 14, 2013, 1:13:57 PM (4 years ago)
Author:
boender
Message:
  • nicified formulas
File:
1 edited

Legend:

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

    r3342 r3352  
    44detail.  The main correctness statement is as follows (slightly simplified, here):
    55
    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*}
    2322
    2423Informally, this means that when fetching a pseudo-instruction at $ppc$, the
     
    7069acual $\sigma$ trie.
    7170
    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\\
    7473& \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow
    7574 \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ sigma) = \mathtt{None})
    76 \end{align*}
     75\end{alignat*}
    7776
    7877This invariant states that any pseudo-address not yet examined is not
    7978present in the lookup trie.
    8079
    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\\
    8382& \forall i.i < |prefix| \rightarrow\notag\\
    8483& \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\
    8584& \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma) = \mathtt{short\_jump}
    86 \end{align*}
     85\end{alignat*}
    8786
    8887This invariant states that when we try to look up the jump length of a
     
    9089value, a short jump.
    9190
    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\ j
    98 \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*}
    9998
    10099This invariant states that between iterations (with $op$ being the previous
     
    102101increase. It is needed for proving termination.
    103102
    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*}
    115115
    116116This is a temporary formulation of the main property\\
     
    124124property.
    125125
    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*}
    148148
    149149This is a more direct safety property: it states that branch instructions are
     
    201201If an iteration returns {\tt None}, we have the following invariant:
    202202
    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\\
    205205&\neg(\forall i.i < |program|\ \rightarrow \notag\\
    206206& \mathtt{is\_jump}\ (\mathtt{nth}\ i\ program)\ \rightarrow \notag\\
    207207& \mathtt{lookup}\ i\ (\mathtt{snd}\ p) = \mathrm{long\_jump}).
    208 \end{align*}
     208\end{alignat*}
    209209
    210210This invariant is applied to $old\_sigma$; if our program becomes too large
     
    221221invariant:
    222222
    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*}
    234234
    235235
Note: See TracChangeset for help on using the changeset viewer.