Fix natural number flat encoding on the spec (#7263)

Author: SeungheonOh

doc/plutus-core-spec/flat-serialisation.tex

@@ -194,19 +194,34 @@ \subsection{Arrays}
 decoded list $l$ (from the remainder $s^{(k)}$) forms the final result.
 
 \subsection{Natural numbers}
-We encode natural numbers by splitting their binary representations into
-sequences of 7-bit blocks, then emitting these as a list with the \textbf{least
-  significant block first}:
+Every natural number $n$ of arbirary size can be uniquely written in the following form:
 
 $$
-\E_{\N} (s, \sum_{i=0}^{n-1}k_i2^{7i}) = \Elist_7(s, [k_0, \ldots, k_{n-1}])
+n = \sum_{i=0}^{n}k_i2^{7i} \text{ where for any $i$ with } 0 \leq i \leq n \text{, } 0 \leq k_i \leq 127  \text{ and } k_n \ne 0
 $$
-\noindent(where $k_i \in \Z$ and $0 \leq k_i \leq 127$).
+
+\noindent Here, each $k_i$ is 7 bit binary block; $k_0$ being the least significant block.
+
+$$
+\E_{\N} (s, \sum_{i=0}^{n}k_i2^{7i}) =
+\begin{cases}
+  \E_7(\Elist_7(s, []), k_{0}) & \text{if } n = 0 \\
+  \E_7(\Elist_7(s, [k_0, \ldots, k_{n-1}]), k_{n}) & \text{if } n \ne 0
+\end{cases}
+$$
+
 \noindent The decoder is
 $$
-\D_{\N}(s) = (s', \sum_{i=0}^{n-1}k_i2^{7i}) \quad \text{if $\Dlist_7(s) = (s', [k_0, \ldots, k_{n-1}])$}.
+\D_{\N}(s) =
+\begin{cases}
+  \text{let } \Dlist_7(s) = (s', ks) \\
+  D_7(s') & \text{if } ks = [] \\
+  (s'', \sum_{i=0}^{n}k_i2^{7i}) & \text{if } ks = [k_0, \ldots, k_{n-1}] \text{ and } \D_7(s') = (s'', k_{n})
+\end{cases}
 $$
 
+\noindent Intuitively, every 7 bit blocks except the last block are prefixed by 1 and the last block is prefixed by 0.
+
 \subsection{Integers}
 Signed integers are encoded by converting them to natural numbers using the
 zigzag encoding ($0 \mapsto 0, -1 \mapsto 1, 1 \mapsto 2, -2 \mapsto 3, 2