Index: src/ASM/CPP2012-policy/proof.tex
===================================================================
--- src/ASM/CPP2012-policy/proof.tex	(revision 2064)
+++ src/ASM/CPP2012-policy/proof.tex	(revision 2065)
@@ -22,4 +22,59 @@
 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: