\section{The proof} In this section, we present the correctness proof for the algorithm in more detail. The main correctness statement is as follows (slightly simplified, here): \begin{lstlisting} 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$. That is, an instruction is placed consecutively after the previous one, and there are no overlaps. 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 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). 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, branch instructions might be encoded which do not coincide with the span between their location and their destination. Proof of termination rests on the fact that the encoding of branch instructions can only grow larger, which means that we must reach a fixed point after at most $2n$ iterations, with $n$ the number of branch instructions in the program. This worst case is reached if at every iteration, we change the encoding of exactly one branch instruction; since the encoding of any branch instructions can change first from short to absolute and then from absolute to long, there can be at most $2n$ changes. 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 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 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 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 $\rightarrow$ (i > |prefix| $\leftrightarrow$ bvt_lookup_opt $\ldots$ (bitvector_of_nat ? i) (\snd sigma) = None ?). \end{lstlisting} 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| $\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. \end{lstlisting} This invariant states that when we try to look up the jump length of a pseudo-address where there is no branch instruction, we will get the default value, a short jump. \begin{lstlisting} definition jump_increase := $\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 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 (with $op$ being the previous iteration, and $p$ the current one), jump lengths either remain equal or increase. It is needed for proving termination. \clearpage \begin{lstlisting} definition sigma_compact_unsafe := $\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 $\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 $\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$))) ] ]. \end{lstlisting} This is a temporary formulation of the main property\\ ({\tt sigma\_policy\_specification}); its main difference 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), 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 := $\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$ (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 | absolute_jump $\Rightarrow$ $\neg$is_relative_jump instr $\wedge$ \fst (absolute_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 (absolute_jump_cond pc_plus_jmp_length addr) = false ]. \end{lstlisting} This is a more direct safety property: it states that branch instructions are encoded properly, and that no wrong branch instructions are chosen. Note that we compute the distance using the memory address of the instruction 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} \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 $\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 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 $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. For instance, it is possible that we have replaced a short jump with an 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)$, 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 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 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 changed something during the iteration or not. If an iteration returns {\tt None}, we have the following invariant: \clearpage \begin{lstlisting} definition nec_plus_ultra := $\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). \end{lstlisting} 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 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 := $\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 $\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 $\Rightarrow$ False | Some x1 $\Rightarrow$ let $\langle$pc1,j1$\rangle$ := x1 in pc1 = pc + instruction_size ($\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$))) ($\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 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$. 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 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 64 Kb. Suppose that all the branch instructions in the previous iteration are 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 $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 64 Kb. This contradicts the earlier hypothesis, hence not all branch instructions in the previous iteration are encoded as 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 (we use the program size for convenience; we could also use the 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 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 property holds, or every iteration up to $2n$ is different. In the latter case, since the only changes between the iterations can be from shorter jumps to longer jumps, in iteration $2n$ every branch instruction must be encoded as a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached.