# source:src/ASM/CPP2013-policy/proof.tex@3363

Last change on this file since 3363 was 3363, checked in by boender, 6 years ago
• renamed directory
File size: 16.0 KB
RevLine
[2064]1\section{The proof}
2
[2096]3In this section, we present the correctness proof for the algorithm in more
[3362]4detail.  The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}.
[2064]5
[3362]6\label{sigmapolspec}
[3361]7\begin{figure}[t]
[3352]8\begin{alignat*}{6}
9\mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv 10\lambda program.\lambda sigma.\lambda policy.$} \notag\\
11  & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\
12        & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}$} \notag\\
13        &&& \omit\rlap{$\forall ppc.ppc < |instr\_list| \rightarrow$} \notag\\
14        &&& \mathbf{let}\ && pc \equiv sigma\ ppc\ \mathbf{in} \notag\\
15        &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\
16        &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\
17        &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\
18  &&&&& (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\
19  &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\
20        &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\
21        &&&&&\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\
22        &&&&& pc + (\mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}))
23\end{alignat*}
[3361]24\caption{Main correctness statement\label{statement}}
25\end{figure}
[2064]26
27Informally, this means that when fetching a pseudo-instruction at $ppc$, the
28translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
[2096]29of the instruction at $ppc$.  That is, an instruction is placed consecutively
[2064]30after the previous one, and there are no overlaps.
31
[2096]32Instructions are also stocked in
[2064]33order: the memory address of the instruction at $ppc$ should be smaller than
[3353]34the memory address of the instruction at $ppc+1$. There is one exception to
[2064]35this rule: the instruction at the very end of the program, whose successor
36address can be zero (this is the case where the program size is exactly equal
37to the amount of memory).
[2080]38
[2096]39Finally, we enforce that the program starts at address 0, i.e. $\sigma(0) = 0$.
[2082]40
41Since our computation is a least fixed point computation, we must prove
42termination in order to prove correctness: if the algorithm is halted after
43a number of steps without reaching a fixed point, the solution is not
[2091]44guaranteed to be correct. More specifically, branch instructions might be
[2096]45encoded which do not coincide with the span between their location and their
[2091]46destination.
[2082]47
[2091]48Proof of termination rests on the fact that the encoding of branch
49instructions can only grow larger, which means that we must reach a fixed point
50after at most $2n$ iterations, with $n$ the number of branch instructions in
51the program. This worst case is reached if at every iteration, we change the
52encoding of exactly one branch instruction; since the encoding of any branch
53instructions can change first from short to absolute and then from absolute to
54long, there can be at most $2n$ changes.
[2082]55
[2096]56The proof has been carried out using the Russell'' style from~\cite{Sozeau2006}.
[2082]57We have proven some invariants of the {\sc f} function from the previous
58section; these invariants are then used to prove properties that hold for every
59iteration of the fixed point computation; and finally, we can prove some
60properties of the fixed point.
61
62\subsection{Fold invariants}
63
[3362]64In this section, we present the invariants that hold during the fold of {\sc f}
65over the program. These will be used later on to prove the properties of the
66iteration.
[2082]67
68Note that during the fixed point computation, the $\sigma$ function is
[3362]69implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by
70looking up the value of $x$ in the trie. Actually, during the fold, the value
71we pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first
72component is the number of bytes added to the program so far with respect to
[3342]73the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the
[3362]74actual $\sigma$ trie.
[2082]75
[3352]76\begin{alignat*}{2}
77\mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\
[3342]78& \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow
79 \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ sigma) = \mathtt{None})
[3352]80\end{alignat*}
[2082]81
[3362]82The first invariant states that any pseudo-address not yet examined is not
[2096]83present in the lookup trie.
[2082]84
[3352]85\begin{alignat*}{2}
86\mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\
[3342]87& \forall i.i < |prefix| \rightarrow\notag\\
88& \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\
89& \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma) = \mathtt{short\_jump}
[3352]90\end{alignat*}
[2082]91
92This invariant states that when we try to look up the jump length of a
[2091]93pseudo-address where there is no branch instruction, we will get the default
94value, a short jump.
[2082]95
[3352]96\begin{alignat*}{4}
97\mathtt{jump} & \omit\rlap{$\mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.$} \notag\\
98        & \omit\rlap{$\forall i.i < |prefix| \rightarrow$} \notag\\
99&       \mathbf{let}\  && oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\
100&       \mathbf{let}\ && j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in} \notag\\
101&&&     \mathtt{jmpleq}\ oj\ j
102\end{alignat*}
[2082]103
[2096]104This invariant states that between iterations (with $op$ being the previous
[2082]105iteration, and $p$ the current one), jump lengths either remain equal or
106increase. It is needed for proving termination.
107
[3362]108\begin{figure}[ht]
[3352]109\begin{alignat*}{6}
110\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\
111& \omit\rlap{$\forall n.n < |prefix| \rightarrow$}\notag\\
112& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
113&&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\
114&&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\
115&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
116&&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\
117&&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow
118                pc_1 = pc + \notag\\
119&&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix)
120\end{alignat*}
[3362]121\caption{Temporary safety property}
122\label{sigmacompactunsafe}
123\end{figure}
[2082]124
[3362]125We can now proceed with the lemmas that are needed for algorithm safety.
126The lemma in Figure~\ref{sigmacompactunsafe} is a temporary formulation of
127the main property\\ ({\tt sigma\_policy\_specification}). Its main difference
[2096]128from the final version is that it uses {\tt instruction\_size\_jmplen} to
[2091]129compute the instruction size. This function uses $j$ to compute the span
130of branch instructions  (i.e. it uses the $\sigma$ function under construction),
131instead of looking at the distance between source and destination. This is
132because $\sigma$ is still under construction; later on we will prove that after
133the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
[2082]134property.
135
[3362]136\begin{figure}[ht]
[3352]137\begin{alignat*}{6}
138\mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\
139& \omit\rlap{$\forall i.i < |prefix| \rightarrow$} \notag\\
140& \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\
141& \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\
142& \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv$}\notag\\
143&&& \omit\rlap{$\mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\
144&&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
145&&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
146&&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\
147&&&&&   \langle j, pc\_plus\_jl, addr \rangle\notag\\
148&&&\mathbf{else} \notag\\
149&&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\
150&&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
151&&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\
152&&&&&\langle j, pc\_plus\_jl, addr \rangle\notag\\
153&&&\omit\rlap{$\mathbf{in}$}\notag\\
154&&&\mathbf{match} && \ j\ \mathbf{with} \notag\\
155&&&&&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\
156&&&&&\mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\
157&&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True}
158\end{alignat*}
[3362]159\caption{Safety property}
160\label{sigmasafe}
161\end{figure}
[2082]162
[3362]163The lemma in figure~\ref{sigmasafe} is a more direct safety property. It states
164that branch instructions are encoded properly, and that no wrong branch
165instructions are chosen.
[2082]166
167Note that we compute the distance using the memory address of the instruction
[3362]168plus its size. This follows the behaviour of the MCS-51 microprocessor, which
[2082]169increases the program counter directly after fetching, and only then executes
[2091]170the branch instruction (by changing the program counter again).
[2082]171
[3362]172We now encode some final, simple, properties to make sure that our policy
173remains consistent, and to keep track of whether the fixed point has been
174reached.
175
[3342]176\begin{align*}
177& \mathtt{lookup}\ 0\ (\mathtt{snd}\ policy) = 0 \notag\\
178& \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ policy) = \mathtt{fst}\ policy
179\end{align*}
[2082]180
181These two properties give the values of $\sigma$ for the start and end of the
182program; $\sigma(0) = 0$ and $\sigma(n)$, where $n$ is the number of
183instructions up until now, is equal to the maximum memory address so far.
184
[3342]185\begin{align*}
186& added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_sigma\ policy \notag\\
187& \mathtt{policy\_jump\_equal}\ prefix\ old\_sigma\ policy\ \rightarrow\ added = 0
188\end{align*}
[2082]189
190And finally, two properties that deal with what happens when the previous
[2096]191iteration does not change with respect to the current one. $added$ is a
[2082]192variable that keeps track of the number of bytes we have added to the program
[2096]193size by changing the encoding of branch instructions. If $added$ is 0, the program
[2091]194has not changed and vice versa.
[2082]195
196We need to use two different formulations, because the fact that $added$ is 0
[2096]197does not guarantee that no branch instructions have changed.  For instance,
[2098]198it is possible that we have replaced a short jump with an absolute jump, which
[2096]199does not change the size of the branch instruction.
[2082]200
201Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
202whereas {\tt policy\_jump\_equal} states that $old\_sigma_2(x) = sigma_2(x)$.
203This formulation is sufficient to prove termination and compactness.
204
205Proving these invariants is simple, usually by induction on the prefix length.
206
207\subsection{Iteration invariants}
208
209These are invariants that hold after the completion of an iteration. The main
210difference between these invariants and the fold invariants is that after the
211completion of the fold, we check whether the program size does not supersede
[2096]21264 Kb, the maximum memory size the MCS-51 can address.
[2082]213
214The type of an iteration therefore becomes an option type: {\tt None} in case
[2096]215the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$
[3362]216otherwise. We also no longer pass along the number of bytes added to the
217program size, but a boolean that indicates whether we have changed something
218during the iteration or not.
[2082]219
220If an iteration returns {\tt None}, we have the following invariant:
221
[3352]222\begin{alignat*}{2}
223\mathtt{nec} & \mathtt{\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\
[3342]224&\neg(\forall i.i < |program|\ \rightarrow \notag\\
225& \mathtt{is\_jump}\ (\mathtt{nth}\ i\ program)\ \rightarrow \notag\\
226& \mathtt{lookup}\ i\ (\mathtt{snd}\ p) = \mathrm{long\_jump}).
[3352]227\end{alignat*}
[2082]228
229This invariant is applied to $old\_sigma$; if our program becomes too large
[2091]230for memory, the previous iteration cannot have every branch instruction encoded
[2096]231as a long jump. This is needed later in the proof of termination.
[2082]232
233If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
[2099]234{\tt out\_of\_program\_none},\\
235{\tt not\_jump\_default}, {\tt jump\_increase},
[2082]236and the two invariants that deal with $\sigma(0)$ and $\sigma(n)$ are
237retained without change.
238
239Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper
240invariant:
241
[3352]242\begin{alignat*}{6}
243\mathtt{sigma} & \omit\rlap{$\mathtt{\_compact} \equiv \lambda program.\lambda sigma.$} \notag\\
244& \omit\rlap{$\forall n.n < |program|\ \rightarrow$} \notag\\
245& \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\
246&&& \omit\rlap{$\mathrm{None}\ \Rightarrow\ \mathrm{False}$}\notag\\
247&&& \omit\rlap{$\mathrm{Some}\ \langle pc, j \rangle \Rightarrow$}\notag\\
248&&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\
249&&&&&   \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\
250&&&&& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\
251&&&&& \ \ pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program)
252\end{alignat*}
[2082]253
[3342]254
[2096]255This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it
[2091]256computes the sizes of branch instructions by looking at the distance between
[2082]257position and destination using $\sigma$.
258
259In actual use, the invariant is qualified: $\sigma$ is compact if there have
260been no changes (i.e. the boolean passed along is {\tt true}). This is to
261reflect the fact that we are doing a least fixed point computation: the result
262is only correct when we have reached the fixed point.
263
[3362]264There is another, trivial, invariant in case the iteration returns
265$\mathtt{Some}\ \sigma$: it must hold that $\mathtt{fst}\ sigma < 2^{16}$.
266We need this invariant to make sure that addresses do not overflow.
[2082]267
268The invariants that are taken directly from the fold invariants are trivial to
269prove.
270
[3362]271The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},
[2096]272then the program size must be greater than 64 Kb. However, since the
[2082]273previous iteration did not return {\tt None} (because otherwise we would
274terminate immediately), the program size in the previous iteration must have
[2096]275been smaller than 64 Kb.
[2082]276
[2091]277Suppose that all the branch instructions in the previous iteration are
[2096]278encoded as long jumps. This means that all branch instructions in this
[2091]279iteration are long jumps as well, and therefore that both iterations are equal
280in the encoding of their branch instructions. Per the invariant, this means that
[2082]281$added = 0$, and therefore that all addresses in both iterations are equal.
282But if all addresses are equal, the program sizes must be equal too, which
283means that the program size in the current iteration must be smaller than
[2096]28464 Kb. This contradicts the earlier hypothesis, hence not all branch
[2091]285instructions in the previous iteration are encoded as long jumps.
[2082]286
287The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
288the fact that we have reached a fixed point, i.e. the previous iteration and
289the current iteration are the same. This means that the results of
290{\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same.
291
292\subsection{Final properties}
293
294These are the invariants that hold after $2n$ iterations, where $n$ is the
[2091]295program size (we use the program size for convenience; we could also use the
[2096]296number of branch instructions, but this is more complex). Here, we only
[2091]297need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
298$\sigma(0) = 0$.
[2084]299
[2096]300Termination can now be proved using the fact that there is a $k \leq 2n$, with
[2084]301$n$ the length of the program, such that iteration $k$ is equal to iteration
302$k+1$. There are two possibilities: either there is a $k < 2n$ such that this
303property holds, or every iteration up to $2n$ is different. In the latter case,
304since the only changes between the iterations can be from shorter jumps to
[2091]305longer jumps, in iteration $2n$ every branch instruction must be encoded as
306a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
[3362]307fixed point is reached.
Note: See TracBrowser for help on using the repository browser.