Potential predicate failure for BBODY rule

IntersectMBO · Jul 29, 2019 · 0815947 · 0815947
1 parent 0815e1d
commit 0815947
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/shelley/chain-and-ledger/formal-spec/chain.tex b/shelley/chain-and-ledger/formal-spec/chain.tex
@@ -1314,6 +1314,12 @@ \subsection{Block Body Transition}
   \label{fig:rules:bbody}
 \end{figure}
 
+The BBODY rule has one predicate failure:
+\begin{itemize}
+\item if the size of the block body in the header is not equal to the real size
+  of the block body, there is a \em{WrongBlockBodySize} failure.
+\end{itemize}
+
 \clearpage
 
 \subsection{Chain Transition}