feat(wcp): make ct max deterministic

wcp/heartbeat.tex

@@ -4,6 +4,7 @@
 	\item \If $\wcpStamp_{i} = 0$ \Then
 		\[
 			\left\{ \begin{array}{lcl}
+				\INST_{i}  & = & 0 \sanityCheck   \\
 				\maxCt_{i} & = & 0 \quad (\trash) \\
 				\ct_{i}    & = & 0 \quad (\trash) \\
 			\end{array} \right.
@@ -16,8 +17,19 @@
 			\item \If $\ct_{i} \neq \maxCt_{i}$ \Then $\ct_{i + 1} = 1 + \ct_{i}$
 			\item \If $\ct_{i} =    \maxCt_{i}$ \Then $\wcpStamp_{i + 1} = 1 + \wcpStamp_{i}$
 		\end{enumerate}
+	\label{wcp: heartbeat: smallness of ct max}
 	\item $\ct_{i} \neq \llarge$
+	\label{wcp: heartbeat: determinism of ct max}
+	\item \If $\ct_{i} \neq 0 $ \Then: 
+	\begin{enumerate}
+			\item \Or $\acc{1}_{i-1} \neq 0$
+			\item \Or $\acc{2}_{i-1} \neq 0$
+			\item \Or $\acc{3}_{i-1} \neq 0$
+			\item \Or $\acc{4}_{i-1} \neq 0$
+	\end{enumerate}	
 	\item $\ct_{N} = \maxCt_{N}$.
 \end{enumerate}
-\saNote{} We don't explicitly impose anything on the value of $\maxCt_i$ when $\vli_i \equiv 1$.
-But the above forces us to have at all times $0 \leq \ct_{i} \leq \maxCt_{i} < \llarge$, at the very least whenever $\wcpStamp_{i} \neq 0$ if the implementation omits the constraints marked with $(\trash)$.
+\saNote{} When $\vli_i \equiv 1$, the value of $\maxCt_i$ is imposed:
+- \ref{wcp: heartbeat: smallness of ct max} imposes the smallness of $\maxCt$: $0 \leq \ct_{i} \leq \maxCt_{i} < \llarge$
+- \ref{wcp: heartbeat: determinism of ct max} imposes the determinism of $\maxCt$: at least one of the four byte decomposition starts with a nonzero value on the first row (ie when $\ct_{i} = 0$) thus imposing that the byte decomposition takes exactly max($\argOneHi$, $\argOneLo$, $\argTwoHi$, $\argTwoLo$) byteSize. 
+