Changeset 3341


Ignore:
Timestamp:
Jun 7, 2013, 6:26:15 PM (4 years ago)
Author:
boender
Message:
  • more notation stuff (still needs work!)
File:
1 edited

Legend:

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

    r3338 r3341  
    66
    77\begin{align*}
    8 \mathrm{sigma\_policy\_specification} \equiv
     8\mathtt{sigma\_policy\_specification} \equiv
    99\lambda program.\lambda sigma.\lambda policy. \notag\\
    1010  sigma\ 0 = 0\ \wedge \notag\\
     
    1212        \forall ppc.ppc < |instr\_list| \rightarrow \notag\\
    1313        \mathbf{let}\ pc \equiv sigma\ ppc\ \mathbf{in} \notag\\
    14         \mathbf{let}\ instruction \equiv \mathrm{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
     14        \mathbf{let}\ instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
    1515        \mathbf{let}\ next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
    16                 next\_pc = pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\
    17                 (pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\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\\
    1818                (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
    19           \mathbf{let}\ instruction' \equiv \mathrm{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
    20                 \mathrm{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
    21         pc + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16})
     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
     
    7070consisting of the current size of the program and our $\sigma$ function.
    7171
    72 \begin{lstlisting}
    73 definition out_of_program_none :=
    74  $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map.
    75  $\forall$i.i < 2^16 $\rightarrow$ (i > |prefix| $\leftrightarrow$
    76   bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?).
    77 \end{lstlisting}
     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})
     76\end{align*}
    7877
    7978This invariant states that any pseudo-address not yet examined is not
    8079present in the lookup trie.
    8180
    82 \begin{lstlisting}
    83 definition not_jump_default :=
    84  $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map.
    85  $\forall$i.i < |prefix| $\rightarrow$
    86   ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) $\rightarrow$
    87   \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma)
    88    $\langle$0,short_jump$\rangle$) = short_jump.
    89 \end{lstlisting}
     81\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}
     86\end{align*}
    9087
    9188This invariant states that when we try to look up the jump length of a
     
    9390value, a short jump.
    9491
    95 \begin{lstlisting}
    96 definition jump_increase :=
    97  $\lambda$prefix:list labelled_instruction.$\lambda$op:ppc_pc_map.$\lambda$p:ppc_pc_map.
    98  $\forall$i.i $\leq$ |prefix| $\rightarrow$
    99  let $\langle$opc,oj$\rangle$ :=
    100   bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in
    101  let $\langle$pc,j$\rangle$ :=
    102   bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd p) $\langle$0,short_jump$\rangle$ in
    103   jmpleq oj j.
    104 \end{lstlisting}
     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\ op\ \mathbf{in} \notag\\
     96        \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ p\ \mathbf{in} \notag\\
     97                \mathtt{jmpleq}\ oj\ j
     98\end{align*}
    10599
    106100This invariant states that between iterations (with $op$ being the previous
     
    108102increase. It is needed for proving termination.
    109103
    110 \clearpage
    111 \begin{lstlisting}
    112 definition sigma_compact_unsafe :=
    113  $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map.
    114  $\forall$n.n < |program| $\rightarrow$
    115   match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
    116   [ None $\Rightarrow$ False
    117   | Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in
    118     match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with
    119     [ None $\Rightarrow$ False
    120     | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in
    121        pc1 = pc + instruction_size_jmplen j
    122         (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)))
    123     ]
    124   ].
    125 \end{lstlisting}
     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 \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
     113                pc_1 = pc + \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
     114\end{align*}
    126115
    127116This is a temporary formulation of the main property\\
     
    135124property.
    136125
    137 \begin{lstlisting}
    138 definition sigma_safe :=
    139  $\lambda$prefix:list labelled_instruction.$\lambda$labels:label_map.$\lambda$added:$\mathbb{N}$.
    140  $\lambda$old_sigma:ppc_pc_map.$\lambda$sigma:ppc_pc_map.
    141  $\forall$i.i < |prefix| $\rightarrow$ let $\langle$pc,j$\rangle$ :=
    142   bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in
    143   let pc_plus_jmp_length := bitvector_of_nat ?  (\fst (bvt_lookup $\ldots$
    144    (bitvector_of_nat ? (S i)) (\snd sigma) $\langle$0,short_jump$\rangle$)) in
    145   let $\langle$label,instr$\rangle$ := nth i ? prefix $\langle$None ?, Comment [ ]$\rangle$ in
    146    $\forall$dest.is_jump_to instr dest $\rightarrow$
    147     let paddr := lookup_def $\ldots$ labels dest 0 in
    148     let addr := bitvector_of_nat ? (if leb i paddr (* forward jump *)
    149     then \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd old_sigma)
    150      $\langle$0,short_jump$\rangle$) + added
    151     else \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd sigma)
    152      $\langle$0,short_jump$\rangle$)) in
    153     match j with
    154     [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$
    155        \fst (short_jump_cond pc_plus_jmp_length addr) = true
    156     | absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$
    157        \fst (absolute_jump_cond pc_plus_jmp_length addr) = true $\wedge$
    158        \fst (short_jump_cond pc_plus_jmp_length addr) = false
    159     | long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false
    160        $\wedge$ \fst (absolute_jump_cond pc_plus_jmp_length addr) = false
    161     ].
    162 \end{lstlisting}
     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        \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*}
    163148
    164149This is a more direct safety property: it states that branch instructions are
Note: See TracChangeset for help on using the changeset viewer.