Changeset 3342


Ignore:
Timestamp:
Jun 11, 2013, 2:13:21 PM (4 years ago)
Author:
boender
Message:
  • completed reworking of proofs
Location:
src/ASM/CPP2012-policy
Files:
2 edited

Legend:

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

    r3338 r3342  
    11\documentclass[a4paper]{llncs}
    22\usepackage{algpseudocode}
     3%\usepackage{algorithmicx}
    34\usepackage{alltt}
    45\usepackage{amsfonts}
     
    3940the proofs.
    4041
    41 \keywords{formal verification, assembler, branch displacement optimisation}
     42\keywords{formal verification, interactive theorem proving, assembler, branch displacement optimisation}
    4243\end{abstract}
    4344
  • src/ASM/CPP2012-policy/proof.tex

    r3341 r3342  
    66
    77\begin{align*}
    8 \mathtt{sigma\_policy\_specification} \equiv
     8& \mathtt{sigma\_policy\_specification} \equiv
    99\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})
     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})
    2222\end{align*}
    2323
     
    6767pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component
    6868is 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 pair
    70 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| \leftrightarrow
    75         \mathtt{lookup\_opt}\ i\ sigma = \mathtt{None})
     69the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the
     70acual $\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})
    7676\end{align*}
    7777
     
    8080
    8181\begin{align*}
    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\ 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}
    8686\end{align*}
    8787
     
    9191
    9292\begin{align*}
    93         \mathtt{jump\_increase} \equiv \lambda pc.\lambda op\lambda p.
     93& \mathtt{jump\_increase} \equiv \lambda pc.\lambda op.\lambda p.
    9494        \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                 \mathtt{jmpleq}\ oj\ j
     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
    9898\end{align*}
    9999
     
    103103
    104104\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 \Rightarrow
    110         \mathbf{match}\ \mathtt{lookup\_opt}\ (n+1)\ sigma\ \mathbf{with}\notag\\
    111         \mathtt{None} \Rightarrow \mathrm{False} \notag\\
    112         \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow
     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
    113113                pc_1 = pc + \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
    114114\end{align*}
     
    125125
    126126\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         \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}
     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}
    147147\end{align*}
    148148
     
    155155the branch instruction (by changing the program counter again).
    156156
    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*}
    163161
    164162These two properties give the values of $\sigma$ for the start and end of the
     
    166164instructions up until now, is equal to the maximum memory address so far.
    167165
    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*}
    172170
    173171And finally, two properties that deal with what happens when the previous
     
    203201If an iteration returns {\tt None}, we have the following invariant:
    204202
    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*}
    214209
    215210This invariant is applied to $old\_sigma$; if our program becomes too large
     
    226221invariant:
    227222
    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
    248235
    249236This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
     
    257244
    258245There 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}$.
    264247
    265248The invariants that are taken directly from the fold invariants are trivial to
Note: See TracChangeset for help on using the changeset viewer.