Index: /src/ASM/CPP2012policy/proof.tex
===================================================================
 /src/ASM/CPP2012policy/proof.tex (revision 2081)
+++ /src/ASM/CPP2012policy/proof.tex (revision 2082)
@@ 4,79 +4,5 @@
detail.
Since our computation is a least fixed point computation, we must prove
termination in order to prove correctness: if the algorithm is halted after
a number of steps without reaching a fixed point, the solution is not
guaranteed to be correct. More specifically, jumps might be encoded whose
displacement is too great for the instruction chosen.

Proof of termination rests on the fact that jumps can only increase, which
means that we must reach a fixed point after at most $2n$ iterations, with
$2n$ the number of jumps in the program. This worst case is reached if at every
iteration, we change the encoding of exactly one jump; since a jump can change
from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
can be at most $2n$ changes.

This proof has been executed in 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
iteration of the fixed point computation; and finally, we can prove some
properties of the fixed point.

The invariants for the fold function. Note that during the fixed point
computation, the $sigma$ functions are implemented as tries, so in order to
compute $sigma(i)$, we lookup the value for $i$ in the corresponding trie.

\begin{lstlisting}
(out_of_program_none prefix policy) $\wedge$
(jump_not_in_policy prefix policy) $\wedge$
(policy_increase prefix old_sigma policy) $\wedge$
(policy_compact_unsafe prefix labels policy) $\wedge$
(policy_safe prefix labels added old_sigma policy) $\wedge$
(\fst (bvt_lookup $\ldots$
 (bitvector_of_nat ? 0) (\snd policy) $\langle$0,short_jump$\rangle$) = 0) $\wedge$
(\fst policy = \fst (bvt_lookup $\ldots$
 (bitvector_of_nat ? (prefix)) (\snd policy) $\langle$0,short_jump$\rangle$)) $\wedge$
(added = 0 → policy_pc_equal prefix old_sigma policy) $\wedge$
(policy_jump_equal prefix old_sigma policy → added = 0)
\end{lstlisting}

These invariants have the following meanings:

\begin{itemize}
 \item {\tt out\_of\_program\_none} shows that if we try to lookup a value
beyond the program, we will get an empty result;
 \item {\tt jump\_not\_in\_policy} shows that an instruction that is not a jump
will have a {\tt short\_jump} as its associated jump length;
 \item {\tt policy\_increase} shows that between iterations, jumps either increase (i.e. from {\tt short\_jump} to {\tt medium\_jump} or from {\tt medium\_jump} to {\tt long\_jump}) or remain equal;
 \item {\tt policy\_compact\_unsafe} shows that the policy is compact (instrucftions directly follow each other and do not overlap);
 \item {\tt policy\_safe} shows that jumps selected are appropriate for the
distance between their position and their target, and the jumps selected are
the smallest possible;
 \item Then there are two properties that fix the values of $\sigma(0)$ and
$\sigma(n)$ (with $n$ the size of the program);
 \item And finally two predicates that link the value of $added$ to reaching
of a fixed point.
\end{itemize}

\begin{lstlisting}
($\Sigma$x:bool × (option ppc_pc_map).
 let $\langle$no_ch,y$\rangle$ := x in
 match y with
 [ None ⇒ nec_plus_ultra program old_policy
  Some p ⇒ (out_of_program_none program p) $\wedge$
 (jump_not_in_policy program p) $\wedge$
 (policy_increase program old_policy p) $\wedge$
 (no_ch = true → policy_compact program labels p) $\wedge$
 (\fst (bvt_lookup $\ldots$
 (bitvector_of_nat ? 0) (\snd p) $\langle$0,short_jump$\rangle$) = 0) $\wedge$
 (\fst p = \fst (bvt_lookup $\ldots$
 (bitvector_of_nat ? (program)) (\snd p) $\langle$0,short_jump$\rangle$)) $\wedge$
 (no_ch = true $\rightarrow$ policy_pc_equal program old_policy p) $\wedge$
 (policy_jump_equal program old_policy p $\rightarrow$ no_ch = true) $\wedge$
 (\fst p < 2^16)
 ])
\end{lstlisting}

The main correctness statement, then, is as follows:
+The main correctness statement is as follows:
\begin{lstlisting}
@@ 96,5 +22,5 @@
let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
(nat_of_bitvector $\ldots$ ppc ≤ instr_list →
 next_pc = add 16 pc (bitvector_of_nat $\ldots$
+ next_pc = add ? pc (bitvector_of_nat $\ldots$
(instruction_size lookup_labels sigma policy ppc instruction)))
$\wedge$
@@ 118,2 +44,267 @@
And 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
+termination in order to prove correctness: if the algorithm is halted after
+a number of steps without reaching a fixed point, the solution is not
+guaranteed to be correct. More specifically, jumps might be encoded whose
+displacement is too great for the instruction chosen.
+
+Proof of termination rests on the fact that jumps can only increase, which
+means that we must reach a fixed point after at most $2n$ iterations, with
+$2n$ the number of jumps in the program. This worst case is reached if at every
+iteration, we change the encoding of exactly one jump; since a jump can change
+from {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
+can be at most $2n$ changes.
+
+This proof has been executed in 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
+iteration of the fixed point computation; and finally, we can prove some
+properties of the fixed point.
+
+\subsection{Fold invariants}
+
+These are the invariants that hold during the fold of {\sc f} over the program,
+and that will later on be used to prove the properties of the iteration.
+
+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
+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.
+
+\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$
+ bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?).
+\end{lstlisting}
+
+This invariant states that every pseudoaddress not yet treated cannot be
+found 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$)) →
+ \snd (bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd sigma)
+ $\langle$0,short_jump$\rangle$) = short_jump.
+\end{lstlisting}
+
+This invariant states that when we try to look up the jump length of a
+pseudoaddress where there is no jump, we will get the default value, a short
+jump.
+
+\begin{lstlisting}
+definition jump_increase :=
+ λprefix:list labelled_instruction.λop:ppc_pc_map.λp:ppc_pc_map.
+ ∀i.i ≤ prefix →
+ let $\langle$opc,oj$\rangle$ :=
+ bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd op) $\langle$0,short_jump$\rangle$ in
+ let $\langle$pc,j$\rangle$ :=
+ bvt_lookup $\ldots$ (bitvector_of_nat ? i) (\snd p) $\langle$0,short_jump$\rangle$ in
+ jmpleq oj j.
+\end{lstlisting}
+
+This invariant states that between iterations ($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 →
+ match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
+ [ None ⇒ False
+  Some x ⇒ 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
+ pc1 = pc + instruction_size_jmplen j
+ (\snd (nth n ? program $\langle$None ?, Comment []$\rangle$)))
+ ]
+ ].
+\end{lstlisting}
+
+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
+compute the instruction size. This function uses $j$ to compute the size
+of jumps (i.e. it uses the $\sigma$ function under construction), instead
+of looking at the distance between source and destination. This is because
+$\sigma$ is still under construction; later on we will prove that after the
+final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
+property.
+
+\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$ :=
+ 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$
+ (bitvector_of_nat ? (S i)) (\snd sigma) $\langle$0,short_jump$\rangle$)) in
+ let $\langle$label,instr$\rangle$ := nth i ? prefix $\langle$None ?, Comment [ ]$\rangle$ in
+ $\forall$dest.is_jump_to instr dest $\rightarrow$
+ let paddr := lookup_def $\ldots$ labels dest 0 in
+ let addr := bitvector_of_nat ? (if leb i paddr (* forward jump *)
+ then \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd old_sigma)
+ $\langle$0,short_jump$\rangle$) + added
+ else \fst (bvt_lookup $\ldots$ (bitvector_of_nat ? paddr) (\snd sigma)
+ $\langle$0,short_jump$\rangle$)) in
+ match j with
+ [ short_jump $\Rightarrow$ $\neg$is_call instr $\wedge$
+ \fst (short_jump_cond pc_plus_jmp_length addr) = true
+  medium_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$
+ \fst (medium_jump_cond pc_plus_jmp_length addr) = true $\wedge$
+ \fst (short_jump_cond pc_plus_jmp_length addr) = false
+  long_jump $\Rightarrow$ \fst (short_jump_cond pc_plus_jmp_length addr) = false
+ $\wedge$ \fst (medium_jump_cond pc_plus_jmp_length addr) = false
+ ].
+\end{lstlisting}
+
+This is a more direct safety property: it states that jump instructions are
+encoded properly, and that no wrong jump instructions are chosen.
+
+Note that we compute the distance using the memory address of the instruction
+plus its size: this is due to the behaviour of the MCS51 architecture, which
+increases the program counter directly after fetching, and only then executes
+the jump.
+
+\begin{lstlisting}
+\fst (bvt_lookup $\ldots$ (bitvector_of_nat ? 0) (\snd policy)
+ $\langle$0,short_jump$\rangle$) = 0)
+\fst policy = \fst (bvt_lookup $\ldots$
+ (bitvector_of_nat ? (prefix)) (\snd policy) $\langle$0,short_jump$\rangle$)
+\end{lstlisting}
+
+These two properties give the values of $\sigma$ for the start and end of the
+program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of
+instructions up until now, is equal to the maximum memory address so far.
+
+\begin{lstlisting}
+(added = 0 → policy_pc_equal prefix old_sigma policy))
+(policy_jump_equal prefix old_sigma policy → 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
+variable that keeps track of the number of bytes we have added to the program
+size by changing jumps; if this 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 jumps have changed: it is possible that we have
+replaced a short jump with a medium jump, which does not change the size.
+
+Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
+whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$.
+This formulation is sufficient to prove termination and compactness.
+
+Proving these invariants is simple, usually by induction on the prefix length.
+
+\subsection{Iteration invariants}
+
+These are invariants that hold after the completion of an iteration. The main
+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 MCS51 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$
+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
+changed something during the iteration or not.
+
+If an iteration returns {\tt None}, we have the following invariant:
+
+\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$)) →
+ \snd (bvt_lookup $\ldots$ (bitvector_of_nat 16 i) (\snd p) $\langle$0,short_jump$\rangle$) =
+ long_jump).
+\end{lstlisting}
+
+This invariant is applied to $old\_sigma$; if our program becomes too large
+for memory, the previous iteration cannot have every jump encoded as a long
+jump. This is needed later on in the proof of termination.
+
+If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
+{\tt out\_of\_program\_none}, {\tt not\_jump\_default}, {\tt jump\_increase},
+and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
+retained without change.
+
+Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
+invariant:
+
+\begin{lstlisting}
+definition sigma_compact: list labelled_instruction → label_map → ppc_pc_map → Prop :=
+ λprogram.λlabels.λsigma.
+ ∀n.n < program →
+ match bvt_lookup_opt $\ldots$ (bitvector_of_nat ? n) (\snd sigma) with
+ [ None ⇒ False
+  Some x ⇒ 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
+ pc1 = pc + instruction_size
+ (λid.bitvector_of_nat ? (lookup_def ?? labels id 0))
+ (λ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
+ (\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
+computes the sizes of jump instructions by looking at the distance between
+position and destination using $\sigma$.
+
+In actual use, the invariant is qualified: $\sigma$ is compact if there have
+been no changes (i.e. the boolean passed along is {\tt true}). This is to
+reflect the fact that we are doing a least fixed point computation: the result
+is only correct when we have reached the fixed point.
+
+There is another, trivial, invariant if the iteration returns
+$\mathtt{Some}\ \sigma$:
+
+\begin{lstlisting}
+\fst p < 2^16
+\end{lstlisting}
+
+The invariants that are taken directly from the fold invariants are trivial to
+prove.
+
+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
+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.
+
+Suppose that all the jumps in the previous iteration are long jumps. This means
+that all jumps in this iteration are long jumps as well, and therefore that
+both iterations are equal in jumps. Per the invariant, this means that
+$added = 0$, and therefore that all addresses in both iterations are equal.
+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 jumps in
+the previous iteration are long jumps.
+
+The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
+the fact that we have reached a fixed point, i.e. the previous iteration and
+the current iteration are the same. This means that the results of
+{\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
+
+\subsection{Final properties}
+
+These are the invariants that hold after $2n$ iterations, where $n$ is the
+program size. Here, we only need {\tt out\_of\_program\_none},
+{\tt sigma\_compact} and the fact that $\sigma(0) = 0$.