Jun 7, 2013, 5:13:45 PM (7 years ago)
  • updated statement of main correctness statement (still needs work)
1 edited


  • src/ASM/CPP2012-policy/proof.tex

    r2099 r3338  
    44detail.  The main correctness statement is as follows (slightly simplified, here):
    6 \begin{lstlisting}
    7 definition sigma_policy_specification :=
    8  $\lambda$program: pseudo_assembly_program.
    9  $\lambda$sigma: Word $\rightarrow$ Word.
    10  $\lambda$policy: Word $\rightarrow$ bool.
    11   sigma (zero $\ldots$) = zero $\ldots$ $\wedge$
    12   $\forall$ppc: Word.$\forall$ppc_ok.
    13   let $\langle$preamble, instr_list$\rangle$ := program in
    14   let pc := sigma ppc in
    15   let instruction :=
    16    \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
    17   let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
    18    (nat_of_bitvector $\ldots$ ppc $\leq$ |instr_list| $\rightarrow$
    19     next_pc = add ? pc (bitvector_of_nat $\ldots$
    20     (instruction_size $\ldots$ sigma policy ppc instruction)))
    21    $\wedge$     
    22    ((nat_of_bitvector $\ldots$ ppc < |instr_list| $\rightarrow$
    23     nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
    24    $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| $\rightarrow$ next_pc = (zero $\ldots$))).
    25 \end{lstlisting}
     8\mathrm{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 \mathrm{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 + \mathrm{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\
     17                (pc + \mathrm{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 \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})
    2724Informally, this means that when fetching a pseudo-instruction at $ppc$, the
    6865implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking
    6966up the value of $x$ in the trie. Actually, during the fold, the value we
    70 pass along is a pair $\mathbb{N} \times \mathtt{ppc_pc_map}$. The first component
     67pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first component
    7168is the number of bytes added to the program so far with respect to
    7269the previous iteration, and the second component, {\tt ppc\_pc\_map}, is a pair
Note: See TracChangeset for help on using the changeset viewer.