# Changeset 2096 for src/ASM/CPP2012-policy/proof.tex

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

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

File:
1 edited

### Legend:

Unmodified
 r2091 \section{The proof} In this section, we will present the correctness proof of the algorithm in more detail. The main correctness statement is as follows: In this section, we present the correctness proof for the algorithm in more detail.  The main correctness statement is as follows (slightly simplified, here): \clearpage \begin{lstlisting} definition sigma_policy_specification :=: $\lambda$program: pseudo_assembly_program. $\lambda$sigma: Word → Word. $\lambda$policy: Word → bool. sigma (zero $\ldots$) = zero $\ldots$ $\wedge$ $\forall$ppc: Word.$\forall$ppc_ok. let instr_list := \snd program in let pc ≝ sigma ppc in let labels := \fst (create_label_cost_map (\snd program)) in let lookup_labels := $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in let instruction := \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in (nat_of_bitvector $\ldots$ ppc ≤ |instr_list| → next_pc = add ? pc (bitvector_of_nat $\ldots$ (instruction_size lookup_labels sigma policy ppc instruction))) $\wedge$ ((nat_of_bitvector $\ldots$ ppc < |instr_list| → nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| → next_pc = (zero $\ldots$))). definition sigma_policy_specification := $\lambda$program: pseudo_assembly_program. $\lambda$sigma: Word $\rightarrow$ Word. $\lambda$policy: Word $\rightarrow$ bool. sigma (zero $\ldots$) = zero $\ldots$ $\wedge$ $\forall$ppc: Word.$\forall$ppc_ok. let $\langle$preamble, instr_list$\rangle$ := program in let pc := sigma ppc in let instruction := \fst (fetch_pseudo_instruction instr_list ppc ppc_ok) in let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in (nat_of_bitvector $\ldots$ ppc $\leq$ |instr_list| $\rightarrow$ next_pc = add ? pc (bitvector_of_nat $\ldots$ (instruction_size $\ldots$ sigma policy ppc instruction))) $\wedge$ ((nat_of_bitvector $\ldots$ ppc < |instr_list| $\rightarrow$ nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc) $\vee$ (nat_of_bitvector $\ldots$ ppc = |instr_list| $\rightarrow$ next_pc = (zero $\ldots$))). \end{lstlisting} Informally, this means that when fetching a pseudo-instruction at $ppc$, the translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size of the instruction at $ppc$; i.e. an instruction is placed immediately of the instruction at $ppc$.  That is, an instruction is placed consecutively after the previous one, and there are no overlaps. The other condition enforced is the fact that instructions are stocked in Instructions are also stocked in order: the memory address of the instruction at $ppc$ should be smaller than the memory address of the instruction at $ppc+1$. There is one exeception to to the amount of memory). And finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$. Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$. Since our computation is a least fixed point computation, we must prove a number of steps without reaching a fixed point, the solution is not guaranteed to be correct. More specifically, branch instructions might be encoded who do not coincide with the span between their location and their encoded which do not coincide with the span between their location and their destination. long, there can be at most $2n$ changes. This proof has been executed in the Russell'' style from~\cite{Sozeau2006}. The proof has been carried out using the Russell'' style from~\cite{Sozeau2006}. We have proven some invariants of the {\sc f} function from the previous section; these invariants are then used to prove properties that hold for every Note that during the fixed point computation, the $\sigma$ function is implemented as a trie for ease access; computing $\sigma(x)$ is done by looking implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by looking up the value of $x$ in the trie. Actually, during the fold, the value we pass along is a couple $\mathbb{N} \times \mathtt{ppc_pc_map}$. The natural number is the number of bytes added to the program so far with respect to the previous iteration, and {\tt ppc\_pc\_map} is a couple of the current size of the program and our $\sigma$ function. pass along is a pair $\mathbb{N} \times \mathtt{ppc_pc_map}$. The first component is the number of bytes added to the program so far with respect to the previous iteration, and the second component, {\tt ppc\_pc\_map}, is a pair consisting of the current size of the program and our $\sigma$ function. \begin{lstlisting} definition out_of_program_none := $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. $\forall$i.i < 2^16 → (i > |prefix| $\leftrightarrow$ $\forall$i.i < 2^16 $\rightarrow$ (i > |prefix| $\leftrightarrow$ bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?). \end{lstlisting} This invariant states that every pseudo-address not yet treated cannot be found in the lookup trie. \begin{lstlisting} definition not_jump_default ≝ This invariant states that any pseudo-address not yet examined is not present in the lookup trie. \begin{lstlisting} definition not_jump_default := $\lambda$prefix:list labelled_instruction.$\lambda$sigma:ppc_pc_map. $\forall$i.i < |prefix| → ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) → $\forall$i.i < |prefix| $\rightarrow$ ¬is_jump (\snd (nth i ? prefix $\langle$None ?, Comment []$\rangle$)) $\rightarrow$ \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$) = short_jump. \begin{lstlisting} definition jump_increase := λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map. ∀i.i ≤ |prefix| → $\lambda$prefix:list labelled_instruction.$\lambda$op:ppc_pc_map.$\lambda$p:ppc_pc_map. $\forall$i.i $\leq$ |prefix| $\rightarrow$ let $\langle$opc,oj$\rangle$ := bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in \end{lstlisting} This invariant states that between iterations ($op$ being the previous This invariant states that between iterations (with $op$ being the previous iteration, and $p$ the current one), jump lengths either remain equal or increase. It is needed for proving termination. \begin{lstlisting} definition sigma_compact_unsafe := λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. ∀n.n < |program| → $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map. $\forall$n.n < |program| $\rightarrow$ match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with [ None ⇒ False | Some x ⇒ let $\langle$pc,j$\rangle$ := x in [ None $\Rightarrow$ False | Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with [ None ⇒ False | Some x1 ⇒ let $\langle$pc1,j1$\rangle$ ≝ x1 in [ None $\Rightarrow$ False | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in pc1 = pc + instruction_size_jmplen j (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$))) This is a temporary formulation of the main property ({\tt sigma\_policy\_specification}); its main difference with the final version is that it uses {\tt instruction\_size\_jmplen} to from the final version is that it uses {\tt instruction\_size\_jmplen} to compute the instruction size. This function uses $j$ to compute the span of branch instructions  (i.e. it uses the $\sigma$ function under construction), \begin{lstlisting} definition sigma_safe := λprefix:list labelled_instruction.λlabels:label_map.λadded:$\mathbb{N}$. λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. ∀i.i < |prefix| → let $\langle$pc,j$\rangle$ := $\lambda$prefix:list labelled_instruction.$\lambda$labels:label_map.$\lambda$added:$\mathbb{N}$. $\lambda$old_sigma:ppc_pc_map.$\lambda$sigma:ppc_pc_map. $\forall$i.i < |prefix| $\rightarrow$ let $\langle$pc,j$\rangle$ := bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma) $\langle$0,short_jump$\rangle$ in let pc_plus_jmp_length := bitvector_of_nat ?  (\fst (bvt_lookup $\ldots$ Note that we compute the distance using the memory address of the instruction plus its size: this is due to the behaviour of the MCS-51 architecture, which plus its size: this follows the behaviour of the MCS-51 microprocessor, which increases the program counter directly after fetching, and only then executes the branch instruction (by changing the program counter again). \begin{lstlisting} (added = 0 → policy_pc_equal prefix old_sigma policy)) (policy_jump_equal prefix old_sigma policy → added = 0)) (added = 0 $\rightarrow$ policy_pc_equal prefix old_sigma policy)) (policy_jump_equal prefix old_sigma policy $\rightarrow$ added = 0)) \end{lstlisting} And finally, two properties that deal with what happens when the previous iteration does not change with respect to the current one. $added$ is the iteration does not change with respect to the current one. $added$ is a variable that keeps track of the number of bytes we have added to the program size by changing the encoding of branch instructions; if this is 0, the program size by changing the encoding of branch instructions. If $added$ is 0, the program has not changed and vice versa. We need to use two different formulations, because the fact that $added$ is 0 does not guarantee that no branch instructions have changed: it is possible that we have replaced a short jump with a absolute jump, which does not change the size of the branch instruction. does not guarantee that no branch instructions have changed.  For instance, it is possible that we have replaced a short jump with a absolute jump, which does not change the size of the branch instruction. Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$, difference between these invariants and the fold invariants is that after the completion of the fold, we check whether the program size does not supersede 65 Kbytes (the maximum memory size the MCS-51 can address). 64 Kb, the maximum memory size the MCS-51 can address. The type of an iteration therefore becomes an option type: {\tt None} in case the program becomes larger than 65 KBytes, or $\mathtt{Some}\ \sigma$ the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$ otherwise. We also no longer use a natural number to pass along the number of bytes added to the program size, but a boolean that indicates whether we have \begin{lstlisting} definition nec_plus_ultra := λprogram:list labelled_instruction.λp:ppc_pc_map. ¬(∀i.i < |program| → is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$)) → $\lambda$program:list labelled_instruction.$\lambda$p:ppc_pc_map. ¬($\forall$i.i < |program| $\rightarrow$ is_jump (\snd (nth i ? program $\langle$None ?, Comment []$\rangle$)) $\rightarrow$ \snd (bvt_lookup $\ldots$ (bitvector_of_nat 16 i) (\snd p) $\langle$0,short_jump$\rangle$) = long_jump). This invariant is applied to $old\_sigma$; if our program becomes too large for memory, the previous iteration cannot have every branch instruction encoded as a long jump. This is needed later on in the proof of termination. as a long jump. This is needed later in the proof of termination. If the iteration returns $\mathtt{Some}\ \sigma$, the invariants \begin{lstlisting} definition sigma_compact := λprogram:list labelled_instruction.λlabels:label_map.λsigma:ppc_pc_map. ∀n.n < |program| → $\lambda$program:list labelled_instruction.$\lambda$labels:label_map.$\lambda$sigma:ppc_pc_map. $\forall$n.n < |program| $\rightarrow$ match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with [ None ⇒ False | Some x ⇒ let $\langle$pc,j$\rangle$ := x in [ None $\Rightarrow$ False | Some x $\Rightarrow$ let $\langle$pc,j$\rangle$ := x in match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? (S n)) (\snd sigma) with [ None ⇒ False | Some x1 ⇒ let $\langle$pc1,j1$\rangle$ := x1 in [ None $\Rightarrow$ False | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in pc1 = pc + instruction_size (λid.bitvector_of_nat ? (lookup_def ?? labels id 0)) (λppc.bitvector_of_nat ? ($\lambda$id.bitvector_of_nat ? (lookup_def ?? labels id 0)) ($\lambda$ppc.bitvector_of_nat ? (\fst (bvt_lookup $\ldots$ ppc (\snd sigma) $\langle$0,short_jump$\rangle$))) (λppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc ($\lambda$ppc.jmpeqb long_jump (\snd (bvt_lookup $\ldots$ ppc (\snd sigma) $\langle$0,short_jump$\rangle$))) (bitvector_of_nat ? n) (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)) \end{lstlisting} This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it computes the sizes of branch instructions by looking at the distance between position and destination using $\sigma$. The proof of {\tt nec\_plus\_ultra} works as follows: if we return {\tt None}, then the program size must be greater than 65 Kbytes. However, since the then the program size must be greater than 64 Kb. However, since the previous iteration did not return {\tt None} (because otherwise we would terminate immediately), the program size in the previous iteration must have been smaller than 65 Kbytes. been smaller than 64 Kb. Suppose that all the branch instructions in the previous iteration are encodes as long jumps. This means that all branch instructions in this encoded as long jumps. This means that all branch instructions in this iteration are long jumps as well, and therefore that both iterations are equal in the encoding of their branch instructions. Per the invariant, this means that But if all addresses are equal, the program sizes must be equal too, which means that the program size in the current iteration must be smaller than 65 Kbytes. This contradicts the earlier hypothesis, hence not all branch 64 Kb. This contradicts the earlier hypothesis, hence not all branch instructions in the previous iteration are encoded as long jumps. These are the invariants that hold after $2n$ iterations, where $n$ is the program size (we use the program size for convenience; we could also use the number of branch instructions, but this is more complicated). Here, we only number of branch instructions, but this is more complex). Here, we only need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that $\sigma(0) = 0$. Termination can now be proven through the fact that there is a $k \leq 2n$, with Termination can now be proved using the fact that there is a $k \leq 2n$, with $n$ the length of the program, such that iteration $k$ is equal to iteration $k+1$. There are two possibilities: either there is a $k < 2n$ such that this