Ignore:
Timestamp:
Jun 15, 2012, 3:25:21 PM (7 years ago)
Author:
mulligan
Message:

Changes to the English for Jaap, and some tidying up and making consistent with the other CPP submission.

File:
1 edited

Legend:

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

    r2091 r2096  
    11\section{The proof}
    22
    3 In this section, we will present the correctness proof of the algorithm in more
    4 detail.
    5 
    6 The main correctness statement is as follows:
     3In this section, we present the correctness proof for the algorithm in more
     4detail.  The main correctness statement is as follows (slightly simplified, here):
    75
    86\clearpage
    97
    108\begin{lstlisting}
    11 definition sigma_policy_specification :=:
    12 $\lambda$program: pseudo_assembly_program.
    13 $\lambda$sigma: Word → Word.
    14 $\lambda$policy: Word → bool.
    15  sigma (zero $\ldots$) = zero $\ldots$ $\wedge$
    16  $\forall$ppc: Word.$\forall$ppc_ok.
    17  let instr_list := \snd program in
    18  let pc ≝ sigma ppc in
    19  let labels := \fst (create_label_cost_map (\snd program)) in
    20  let lookup_labels :=
    21   $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
    22  let instruction :=
    23   \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
    24  let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
    25   (nat_of_bitvector $\ldots$ ppc ≤ |instr_list| →
    26    next_pc = add ? pc (bitvector_of_nat $\ldots$
    27    (instruction_size lookup_labels sigma policy ppc instruction)))
    28   $\wedge$     
    29   ((nat_of_bitvector $\ldots$ ppc < |instr_list| →
    30    nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
    31   $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| → next_pc = (zero $\ldots$))).
     9definition sigma_policy_specification :=
     10 $\lambda$program: pseudo_assembly_program.
     11 $\lambda$sigma: Word $\rightarrow$ Word.
     12 $\lambda$policy: Word $\rightarrow$ bool.
     13  sigma (zero $\ldots$) = zero $\ldots$ $\wedge$
     14  $\forall$ppc: Word.$\forall$ppc_ok.
     15  let $\langle$preamble, instr_list$\rangle$ := program in
     16  let pc := sigma ppc in
     17  let instruction :=
     18   \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in
     19  let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
     20   (nat_of_bitvector $\ldots$ ppc $\leq$ |instr_list| $\rightarrow$
     21    next_pc = add ? pc (bitvector_of_nat $\ldots$
     22    (instruction_size $\ldots$ sigma policy ppc instruction)))
     23   $\wedge$     
     24   ((nat_of_bitvector $\ldots$ ppc < |instr_list| $\rightarrow$
     25    nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
     26   $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| $\rightarrow$ next_pc = (zero $\ldots$))).
    3227\end{lstlisting}
    3328
    3429Informally, this means that when fetching a pseudo-instruction at $ppc$, the
    3530translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
    36 of the instruction at $ppc$; i.e. an instruction is placed immediately
     31of the instruction at $ppc$.  That is, an instruction is placed consecutively
    3732after the previous one, and there are no overlaps.
    3833
    39 The other condition enforced is the fact that instructions are stocked in
     34Instructions are also stocked in
    4035order: the memory address of the instruction at $ppc$ should be smaller than
    4136the memory address of the instruction at $ppc+1$. There is one exeception to
     
    4439to the amount of memory).
    4540
    46 And finally, we enforce that the program starts at address 0, i.e.
    47 $\sigma(0) = 0$.
     41Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$.
    4842
    4943Since our computation is a least fixed point computation, we must prove
     
    5145a number of steps without reaching a fixed point, the solution is not
    5246guaranteed to be correct. More specifically, branch instructions might be
    53 encoded who do not coincide with the span between their location and their
     47encoded which do not coincide with the span between their location and their
    5448destination.
    5549
     
    6256long, there can be at most $2n$ changes.
    6357
    64 This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
     58The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}.
    6559We have proven some invariants of the {\sc f} function from the previous
    6660section; these invariants are then used to prove properties that hold for every
     
    7468
    7569Note that during the fixed point computation, the $\sigma$ function is
    76 implemented as a trie for ease access; computing $\sigma(x)$ is done by looking
     70implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking
    7771up the value of $x$ in the trie. Actually, during the fold, the value we
    78 pass along is a couple $\mathbb{N} \times \mathtt{ppc_pc_map}$. The natural
    79 number is the number of bytes added to the program so far with respect to
    80 the previous iteration, and {\tt ppc\_pc\_map} is a couple of the current
    81 size of the program and our $\sigma$ function.
     72pass along is a pair $\mathbb{N} \times \mathtt{ppc_pc_map}$. The first component
     73is the number of bytes added to the program so far with respect to
     74the previous iteration, and the second component, {\tt ppc\_pc\_map}, is a pair
     75consisting of the current size of the program and our $\sigma$ function.
    8276
    8377\begin{lstlisting}
    8478definition out_of_program_none :=
    8579 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map.
    86  $\forall$i.i < 2^16 (i > |prefix| $\leftrightarrow$
     80 $\forall$i.i < 2^16 $\rightarrow$ (i > |prefix| $\leftrightarrow$
    8781  bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?).
    8882\end{lstlisting}
    8983
    90 This invariant states that every pseudo-address not yet treated cannot be
    91 found in the lookup trie.
    92 
    93 \begin{lstlisting}
    94 definition not_jump_default
     84This invariant states that any pseudo-address not yet examined is not
     85present in the lookup trie.
     86
     87\begin{lstlisting}
     88definition not_jump_default :=
    9589 $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map.
    96  $\forall$i.i < |prefix|
    97   ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$))
     90 $\forall$i.i < |prefix| $\rightarrow$
     91  ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) $\rightarrow$
    9892  \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma)
    9993   $\langle$0,short_jump$\rangle$) = short_jump.
     
    106100\begin{lstlisting}
    107101definition jump_increase :=
    108  λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map.
    109  ∀i.i ≤ |prefix| →
     102 $\lambda$prefix:list labelled_instruction.$\lambda$op:ppc_pc_map.$\lambda$p:ppc_pc_map.
     103 $\forall$i.i $\leq$ |prefix| $\rightarrow$
    110104 let $\langle$opc,oj$\rangle$ :=
    111105  bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in
     
    115109\end{lstlisting}
    116110
    117 This invariant states that between iterations ($op$ being the previous
     111This invariant states that between iterations (with $op$ being the previous
    118112iteration, and $p$ the current one), jump lengths either remain equal or
    119113increase. It is needed for proving termination.
     
    123117\begin{lstlisting}
    124118definition sigma_compact_unsafe :=
    125  λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
    126  ∀n.n < |program| →
     119 $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map.
     120 $\forall$n.n < |program| $\rightarrow$
    127121  match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
    128   [ None False
    129   | Some x let $\langle$pc,j$\rangle$ := x in
     122  [ None $\Rightarrow$ False
     123  | Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in
    130124    match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with
    131     [ None False
    132     | Some x1 ⇒ let $\langle$pc1,j1$\rangle$ ≝ x1 in
     125    [ None $\Rightarrow$ False
     126    | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in
    133127       pc1 = pc + instruction_size_jmplen j
    134128        (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)))
     
    139133This is a temporary formulation of the main property
    140134({\tt sigma\_policy\_specification}); its main difference
    141 with the final version is that it uses {\tt instruction\_size\_jmplen} to
     135from the final version is that it uses {\tt instruction\_size\_jmplen} to
    142136compute the instruction size. This function uses $j$ to compute the span
    143137of branch instructions  (i.e. it uses the $\sigma$ function under construction),
     
    149143\begin{lstlisting}
    150144definition sigma_safe :=
    151  λprefix:list labelled_instruction.λlabels:label_map.λadded:$\mathbb{N}$.
    152  λold_sigma:ppc_pc_map.λsigma:ppc_pc_map.
    153  ∀i.i < |prefix| → let $\langle$pc,j$\rangle$ :=
     145 $\lambda$prefix:list labelled_instruction.$\lambda$labels:label_map.$\lambda$added:$\mathbb{N}$.
     146 $\lambda$old_sigma:ppc_pc_map.$\lambda$sigma:ppc_pc_map.
     147 $\forall$i.i < |prefix| $\rightarrow$ let $\langle$pc,j$\rangle$ :=
    154148  bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in
    155149  let pc_plus_jmp_length := bitvector_of_nat ?  (\fst (bvt_lookup $\ldots$
     
    178172
    179173Note that we compute the distance using the memory address of the instruction
    180 plus its size: this is due to the behaviour of the MCS-51 architecture, which
     174plus its size: this follows the behaviour of the MCS-51 microprocessor, which
    181175increases the program counter directly after fetching, and only then executes
    182176the branch instruction (by changing the program counter again).
     
    194188
    195189\begin{lstlisting}
    196 (added = 0 policy_pc_equal prefix old_sigma policy))
    197 (policy_jump_equal prefix old_sigma policy added = 0))
     190(added = 0 $\rightarrow$ policy_pc_equal prefix old_sigma policy))
     191(policy_jump_equal prefix old_sigma policy $\rightarrow$ added = 0))
    198192\end{lstlisting}
    199193
    200194And finally, two properties that deal with what happens when the previous
    201 iteration does not change with respect to the current one. $added$ is the
     195iteration does not change with respect to the current one. $added$ is a
    202196variable that keeps track of the number of bytes we have added to the program
    203 size by changing the encoding of branch instructions; if this is 0, the program
     197size by changing the encoding of branch instructions. If $added$ is 0, the program
    204198has not changed and vice versa.
    205199
    206200We need to use two different formulations, because the fact that $added$ is 0
    207 does not guarantee that no branch instructions have changed: it is possible
    208 that we have replaced a short jump with a absolute jump, which does not change
    209 the size of the branch instruction.
     201does not guarantee that no branch instructions have changed.  For instance,
     202it is possible that we have replaced a short jump with a absolute jump, which
     203does not change the size of the branch instruction.
    210204
    211205Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
     
    220214difference between these invariants and the fold invariants is that after the
    221215completion of the fold, we check whether the program size does not supersede
    222 65 Kbytes (the maximum memory size the MCS-51 can address).
     21664 Kb, the maximum memory size the MCS-51 can address.
    223217
    224218The type of an iteration therefore becomes an option type: {\tt None} in case
    225 the program becomes larger than 65 KBytes, or $\mathtt{Some}\ \sigma$
     219the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
    226220otherwise. We also no longer use a natural number to pass along the number of
    227221bytes added to the program size, but a boolean that indicates whether we have
     
    232226\begin{lstlisting}
    233227definition nec_plus_ultra :=
    234  λprogram:list labelled_instruction.λp:ppc_pc_map.
    235  ¬(∀i.i < |program| →
    236   is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$))
     228 $\lambda$program:list labelled_instruction.$\lambda$p:ppc_pc_map.
     229 ¬($\forall$i.i < |program| $\rightarrow$
     230  is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$)) $\rightarrow$
    237231  \snd (bvt_lookup $\ldots$ (bitvector_of_nat 16 i) (\snd p) $\langle$0,short_jump$\rangle$) =
    238232   long_jump).
     
    241235This invariant is applied to $old\_sigma$; if our program becomes too large
    242236for memory, the previous iteration cannot have every branch instruction encoded
    243 as a long jump. This is needed later on in the proof of termination.
     237as a long jump. This is needed later in the proof of termination.
    244238
    245239If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
     
    253247\begin{lstlisting}
    254248definition sigma_compact :=
    255  λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map.
    256  ∀n.n < |program| →
     249 $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map.
     250 $\forall$n.n < |program| $\rightarrow$
    257251  match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
    258   [ None False
    259   | Some x let $\langle$pc,j$\rangle$ := x in
     252  [ None $\Rightarrow$ False
     253  | Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in
    260254    match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with
    261     [ None False
    262     | Some x1 let $\langle$pc1,j1$\rangle$ := x1 in
     255    [ None $\Rightarrow$ False
     256    | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in
    263257      pc1 = pc + instruction_size
    264        (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
    265        (λppc.bitvector_of_nat ?
     258       ($\lambda$id.bitvector_of_nat ? (lookup_def ?? labels id 0))
     259       ($\lambda$ppc.bitvector_of_nat ?
    266260        (\fst (bvt_lookup $\ldots$ ppc (\snd sigma) $\langle$0,short_jump$\rangle$)))
    267        (λppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc
     261       ($\lambda$ppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc
    268262        (\snd sigma) $\langle$0,short_jump$\rangle$))) (bitvector_of_nat ? n)
    269263       (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$))
     
    272266\end{lstlisting}
    273267
    274 This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it
     268This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
    275269computes the sizes of branch instructions by looking at the distance between
    276270position and destination using $\sigma$.
     
    292286
    293287The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None},
    294 then the program size must be greater than 65 Kbytes. However, since the
     288then the program size must be greater than 64 Kb. However, since the
    295289previous iteration did not return {\tt None} (because otherwise we would
    296290terminate immediately), the program size in the previous iteration must have
    297 been smaller than 65 Kbytes.
     291been smaller than 64 Kb.
    298292
    299293Suppose that all the branch instructions in the previous iteration are
    300 encodes as long jumps. This means that all branch instructions in this
     294encoded as long jumps. This means that all branch instructions in this
    301295iteration are long jumps as well, and therefore that both iterations are equal
    302296in the encoding of their branch instructions. Per the invariant, this means that
     
    304298But if all addresses are equal, the program sizes must be equal too, which
    305299means that the program size in the current iteration must be smaller than
    306 65 Kbytes. This contradicts the earlier hypothesis, hence not all branch
     30064 Kb. This contradicts the earlier hypothesis, hence not all branch
    307301instructions in the previous iteration are encoded as long jumps.
    308302
     
    316310These are the invariants that hold after $2n$ iterations, where $n$ is the
    317311program size (we use the program size for convenience; we could also use the
    318 number of branch instructions, but this is more complicated). Here, we only
     312number of branch instructions, but this is more complex). Here, we only
    319313need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
    320314$\sigma(0) = 0$.
    321315
    322 Termination can now be proven through the fact that there is a $k \leq 2n$, with
     316Termination can now be proved using the fact that there is a $k \leq 2n$, with
    323317$n$ the length of the program, such that iteration $k$ is equal to iteration
    324318$k+1$. There are two possibilities: either there is a $k < 2n$ such that this
Note: See TracChangeset for help on using the changeset viewer.