Improve Section 3.8 according to review comments

docs/formal-spec/chain.tex

@@ -741,14 +741,14 @@ \subsection{$\mathsf{TICKF}$ Transition}
 
 \clearpage
 
-\subsection{Chain Head Transition}
+\subsection{$\mathsf{CHAINHEAD}$ Transition}
 \label{sec:chainhead-trans}
 
-The $\mathsf{CHAINHEAD}$ transition rule is the main rule of the blockchain layer
+The Chain Head Transition rule ($\mathsf{CHAINHEAD}$) is the main rule of the blockchain layer
 part of the STS. It calls $\mathsf{TICKF}$, $\mathsf{TICKN}$, and $\mathsf{PRTCL}$,
 as sub-rules.
 
-The transition checks six things
+The transition checks the following things:
 (via $\fun{chainChecks}$ and $\fun{prtlSeqChecks}$ from Figure~\ref{fig:funcs:chainhead-helper}):
 \begin{itemize}
 \item The slot in the block header body is larger than the last slot recorded.
@@ -828,9 +828,9 @@ \subsection{Chain Head Transition}
   \begin{align*}
       & \fun{chainChecks} \in \N \to (\N,\N, \ProtVer) \to \BHeader \to \Bool \\
       & \fun{chainChecks}~\var{maxpv}~(\var{maxBHSize},~\var{maxBBSize},~\var{protocolVersion})~\var{bh} = \\
-      & ~~~~ m \leq \var{maxpv} \\
-      & ~~~~ \land~\headerSize{bh} \leq \var{maxBHSize} \\
-      & ~~~~ \land~\hBBodySize{(\headerBody{bh})} \leq \var{maxBBSize} \\
+      & ~~~~ m \overset{(\ref{itm:chainhead-failures-6})}{\leq} \var{maxpv} \\
+      & ~~~~ \land~\headerSize{bh} \overset{(\ref{itm:chainhead-failures-4})}{\leq} \var{maxBHSize} \\
+      & ~~~~ \land~\hBBodySize{(\headerBody{bh})} \overset{(\ref{itm:chainhead-failures-5})}{\leq} \var{maxBBSize} \\
       & ~~~~ \where (m,~\wcard)\leteq\var{protocolVersion}
   \end{align*}
   %
@@ -851,9 +851,9 @@ \subsection{Chain Head Transition}
           &
           lab = \Nothing
           \\
-          \var{s_\ell} < \var{slot}
-          \land \var{b_\ell} + 1 = \var{bn}
-          \land \var{ph} = \hBPrevHeader{bhb}
+          \var{s_\ell} \overset{(\ref{itm:chainhead-failures-1})}{<} \var{slot}
+          \land \var{b_\ell} + 1 \overset{(\ref{itm:chainhead-failures-2})}{=} \var{bn}
+          \land \var{ph} \overset{(\ref{itm:chainhead-failures-3})}{=} \hBPrevHeader{bhb}
           &
           lab = (b_\ell,~s_\ell,~\wcard) \\
         \end{cases} \\
@@ -885,7 +885,7 @@ \subsection{Chain Head Transition}
         \leteq\var{nes} \\
       (\var{e_2},~\wcard,~\wcard,~\var{es},~\wcard,~\var{pd})
         \leteq\var{forecast} \\
-        (\var{acnt},~\wcard,\var{ls},~\wcard,~\var{pp})\leteq\var{es}\\
+        (\wcard,~\wcard,~\wcard,~\wcard,~\var{pp})\leteq\var{es}\\
           \var{ne} \leteq  \var{e_1} \neq \var{e_2}\\
           \eta_{ph} \leteq \prevHashToNonce{(\lastAppliedHash{lab})} \\~\\
       \fun{chainChecks}~
@@ -954,21 +954,21 @@ \subsection{Chain Head Transition}
   \label{fig:rules:chainhead}
 \end{figure}
 
-The $\mathsf{CHAINHEAD}$ transition rule has six predicate failures:
-\begin{itemize}
-\item If the slot of the block header body is not larger than the last slot,
+The $\mathsf{CHAINHEAD}$ transition rule has the following predicate failures:
+\begin{enumerate}
+\item \label{itm:chainhead-failures-1} If the slot of the block header body is not larger than the last slot,
   there is a \emph{WrongSlotInterval} failure.
-\item If the block number does not increase by exactly one,
+\item \label{itm:chainhead-failures-2} If the block number does not increase by exactly one,
   there is a \emph{WrongBlockNo} failure.
-\item If the hash of the previous header of the block header body is not equal
+\item \label{itm:chainhead-failures-3} If the hash of the previous header of the block header body is not equal
   to the last header hash, there is a \emph{WrongBlockSequence} failure.
-\item If the size of the block header is larger than the maximally allowed size,
+\item \label{itm:chainhead-failures-4} If the size of the block header is larger than the maximally allowed size,
   there is a \emph{HeaderSizeTooLarge} failure.
-\item If the size of the block body is larger than the maximally allowed size,
+\item \label{itm:chainhead-failures-5} If the size of the block body is larger than the maximally allowed size,
   there is a \emph{BlockSizeTooLarge} failure.
-\item If the major component of the protocol version is larger than $\MaxMajorPV$,
+\item \label{itm:chainhead-failures-6} If the major component of the protocol version is larger than $\MaxMajorPV$,
   there is a \emph{ObsoleteNode} failure.
-\end{itemize}
+\end{enumerate}
 
 %%% Local Variables:
 %%% mode: latex