Index: /src/ASM/CPP2012-policy/proof.tex
===================================================================
--- /src/ASM/CPP2012-policy/proof.tex	(revision 2080)
+++ /src/ASM/CPP2012-policy/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 pseudo-address 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
+pseudo-address 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 MCS-51 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 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$
+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$.