root/src/ASM/CPP2012-policy/proof.tex @ 2064

\section{The proof}

In this section, we will present the correctness proof of the algorithm in more
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 main correctness statement, then, is as follows:

\begin{lstlisting}
definition jump_expansion':
$\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (|l|) < 2^16).
 option ($\Sigma$sigma:Word → Word $\times$ bool.
  $\forall$ppc: Word.$\forall$ppc_ok.
   let pc := \fst (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
    And (nat_of_bitvector $\ldots$ ppc $\leq$ |\snd program| →
     next_pc = add ? pc (bitvector_of_nat $\ldots$
      (instruction_size lookup_labels ($\lambda$x.\fst (sigma x))
       ($\lambda$x.\snd (sigma x)) ppc instruction))
    )
    (Or (nat_of_bitvector $\ldots$ ppc < |\snd program| →
     nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
    (nat_of_bitvector $\ldots$ ppc = |\snd program| → 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
after the previous one, and there are no overlaps.

The other condition enforced is the fact that instructions are 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
this rule: the instruction at the very end of the program, whose successor
address can be zero (this is the case where the program size is exactly equal
to the amount of memory).