| | 24 | |
| | 25 | The invariants for the fold function. Note that during the fixed point |
| | 26 | computation, the $sigma$ functions are implemented as tries, so in order to |
| | 27 | compute $sigma(i)$, we lookup the value for $i$ in the corresponding trie. |
| | 28 | |
| | 29 | \begin{lstlisting} |
| | 30 | (out_of_program_none prefix policy) $\wedge$ |
| | 31 | (jump_not_in_policy prefix policy) $\wedge$ |
| | 32 | (policy_increase prefix old_sigma policy) $\wedge$ |
| | 33 | (policy_compact_unsafe prefix labels policy) $\wedge$ |
| | 34 | (policy_safe prefix labels added old_sigma policy) $\wedge$ |
| | 35 | (\fst (bvt_lookup $\ldots$ |
| | 36 | (bitvector_of_nat ? 0) (\snd policy) $\langle$0,short_jump$\rangle$) = 0) $\wedge$ |
| | 37 | (\fst policy = \fst (bvt_lookup $\ldots$ |
| | 38 | (bitvector_of_nat ? (|prefix|)) (\snd policy) $\langle$0,short_jump$\rangle$)) $\wedge$ |
| | 39 | (added = 0 → policy_pc_equal prefix old_sigma policy) $\wedge$ |
| | 40 | (policy_jump_equal prefix old_sigma policy → added = 0) |
| | 41 | \end{lstlisting} |
| | 42 | |
| | 43 | These invariants have the following meanings: |
| | 44 | |
| | 45 | \begin{itemize} |
| | 46 | \item {\tt out\_of\_program\_none} shows that if we try to lookup a value |
| | 47 | beyond the program, we will get an empty result; |
| | 48 | \item {\tt jump\_not\_in\_policy} shows that an instruction that is not a jump |
| | 49 | will have a {\tt short\_jump} as its associated jump length; |
| | 50 | \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; |
| | 51 | \item {\tt policy\_compact\_unsafe} shows that the policy is compact (instrucftions directly follow each other and do not overlap); |
| | 52 | \item {\tt policy\_safe} shows that jumps selected are appropriate for the |
| | 53 | distance between their position and their target, and the jumps selected are |
| | 54 | the smallest possible; |
| | 55 | \item Then there are two properties that fix the values of $\sigma(0)$ and |
| | 56 | $\sigma(n)$ (with $n$ the size of the program); |
| | 57 | \item And finally two predicates that link the value of $added$ to reaching |
| | 58 | of a fixed point. |
| | 59 | \end{itemize} |
| | 60 | |
| | 61 | \begin{lstlisting} |
| | 62 | ($\Sigma$x:bool × (option ppc_pc_map). |
| | 63 | let $\langle$no_ch,y$\rangle$ := x in |
| | 64 | match y with |
| | 65 | [ None ⇒ nec_plus_ultra program old_policy |
| | 66 | | Some p ⇒ (out_of_program_none program p) $\wedge$ |
| | 67 | (jump_not_in_policy program p) $\wedge$ |
| | 68 | (policy_increase program old_policy p) $\wedge$ |
| | 69 | (no_ch = true → policy_compact program labels p) $\wedge$ |
| | 70 | (\fst (bvt_lookup $\ldots$ |
| | 71 | (bitvector_of_nat ? 0) (\snd p) $\langle$0,short_jump$\rangle$) = 0) $\wedge$ |
| | 72 | (\fst p = \fst (bvt_lookup $\ldots$ |
| | 73 | (bitvector_of_nat ? (|program|)) (\snd p) $\langle$0,short_jump$\rangle$)) $\wedge$ |
| | 74 | (no_ch = true $\rightarrow$ policy_pc_equal program old_policy p) $\wedge$ |
| | 75 | (policy_jump_equal program old_policy p $\rightarrow$ no_ch = true) $\wedge$ |
| | 76 | (\fst p < 2^16) |
| | 77 | ]) |
| | 78 | \end{lstlisting} |
