Misc Corrections

text/accumulation.tex

@@ -100,7 +100,8 @@ \subsection{History and Queuing}
 We may now define the sequence of accumulatable work-reports in this block as $\mathbf{W}^*$:
 \begin{align}
   \using m &= \mathbf{H}_t \bmod \mathsf{E}\\
-  \mathbf{W}^* &\equiv \mathbf{W}^! \frown Q(\wideparen{\ready_{m\dots}} \concat \wideparen{\ready_{\dots m}} \concat \mathbf{W}^Q, \accumulatedcup)
+  \mathbf{W}^* &\equiv \mathbf{W}^! \frown Q(\mathbf{q}, \accumulatedcup \cup\;\srmap(\mathbf{W}^!)) \\
+  \quad\where \mathbf{q} &= E(\wideparen{\ready_{m\dots}} \concat \wideparen{\ready_{\dots m}} \concat \mathbf{W}^Q, \srmap(\mathbf{W}^!))
 \end{align}
 
 \subsection{Execution}
@@ -126,7 +127,7 @@ \subsection{Execution}
   \end{aligned}\right)
 \end{equation}
 
-We denote the set characterizing a \emph{deferred transfer} as $\defxfer$, noting that a transfer includes a memo component $m$ of $\mathsf{W}_T = 128$ octets, together with the service index of the sender $s$, the service index of the receiver $d$, the amount of tokens to be transferred $a$ and the gas limit $g$ for the transfer. Formally:
+We denote the set characterizing a \emph{deferred transfer} as $\defxfer$, noting that a transfer includes a memo component $m$ of $\mathsf{W}_T = 128$ octets, together with the service index of the sender $s$, the service index of the receiver $d$, the balance to be transferred $a$ and the gas limit $g$ for the transfer. Formally:
 \begin{align}
   \defxfer \equiv \ltuple\isa{s}{\N_S}\ts\isa{d}{\N_S}\ts\isa{a}{\N_B}\ts\isa{m}{\Y_{\mathsf{W}_T}}\ts\isa{g}{\N_G}\rtuple
 \end{align}

text/erasure_coding.tex

@@ -22,8 +22,8 @@ \subsection{Blob Encoding and Recovery}
 \begin{align}
   \forall n \in \N, k \in \N :\ &\spl_n(\mathbf{d} \in \Y_{k\cdot n}) \in \seq{\Y_n}_k \equiv \sq{\mathbf{d}_{0\dots+n}, \mathbf{d}_{n\dots+n}, \cdots, \mathbf{d}_{(k-1)n\dots+n}} \\
   \forall n \in \N, k \in \N :\ &\join_n(\mathbf{c} \in \seq{\Y_n}_k) \in \Y_{k\cdot n} \equiv \mathbf{c}_0 \concat \mathbf{c}_1 \concat \dots \\
-  \forall n \in \N, k \in \N :\ &\unzip_n(\mathbf{d} \in \Y_{k\cdot n}) \in \seq{\Y_n}_k \equiv \sq{ [\mathbf{d}_{j.k + i} \mid j \orderedin \N_n] \mid i \orderedin \N_k} \\
-  \forall n \in \N, k \in \N :\ &\lace_n(\mathbf{c} \in \seq{\Y_n}_k) \in \Y_{k\cdot n} \equiv \mathbf{d} \ \where \forall i \in \N_k, j \in \N_n: \mathbf{d}_{j.k + i} = (\mathbf{c}_i)_j
+  \forall n \in \N, k \in \N :\ &\unzip_n(\mathbf{d} \in \Y_{k\cdot n}) \in \seq{\Y_n}_k \equiv \sq{ [\mathbf{d}_{j\cdot k + i} \mid j \orderedin \N_n] \mid i \orderedin \N_k} \\
+  \forall n \in \N, k \in \N :\ &\lace_n(\mathbf{c} \in \seq{\Y_n}_k) \in \Y_{k\cdot n} \equiv \mathbf{d} \ \where \forall i \in \N_k, j \in \N_n: \mathbf{d}_{j\cdot k + i} = (\mathbf{c}_i)_j
 \end{align}
 
 We define the transposition operator hence:

text/pvm.tex

@@ -47,6 +47,7 @@ \subsection{Basic Definition}
     (\mathbf{p}, \imath, \gascounter, \registers, \mem) &\mapsto \begin{cases}
       \Psi(\mathbf{p}, \imath', \gascounter', \registers', \mem') &\when \varepsilon = \continue\\
       (\oog, \imath', \gascounter', \registers', \mem') &\when \gascounter' < 0\\
+      (\varepsilon, 0, \gascounter', \registers', \mem') &\when \varepsilon \in \{ \panic, \halt \}\\
       (\varepsilon, \imath', \gascounter', \registers', \mem') &\otherwise
     \end{cases} \\
     \where (\varepsilon, \imath', \gascounter', \registers', \mem') &= \Psi_1(\mathbf{c}, \mathbf{k}, \mathbf{j}, \imath, \gascounter, \registers, \mem)\\

text/pvm_invocations.tex

@@ -27,6 +27,7 @@ \subsection{Host-Call Result Constants}
   \item[$\mathtt{PANIC} = 1$] The invocation completed with a panic.
   \item[$\mathtt{FAULT} = 2$] The invocation completed with a page fault.
   \item[$\mathtt{HOST} = 3$] The invocation completed with a host-call fault.
+  \item[$\mathtt{OOG} = 4$] The invocation completed by running out of gas.
 \end{description}
 
 Note return codes for a host-call-request exit are any non-zero value less than $2^{32} - 13$.
@@ -130,8 +131,8 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
     &\to
     \tuple{\partialstate, \defxfers, \H\bm{?}, \N_G} \\
     (\mathbf{u}, s, g, \mathbf{o}) &\mapsto \begin{cases}
-      \tup{I(\mathbb{u}, s)_\mathbf{u}, [], \none, 0} &\when \mathbf{d}[s]_\mathbf{c} = \none \\
-      C(\Psi_M(\mathbf{d}[s]_\mathbf{c}, 10, g, \mathcal{E}(\var{\mathbf{o}}), F, \tup{I(\mathbb{u}, s), I(\mathbb{u}, s)})) &\otherwise
+      \tup{I(\mathbf{u}, s)_\mathbf{u}, [], \none, 0} &\when \mathbf{d}[s]_\mathbf{c} = \none \\
+      C(\Psi_M(\mathbf{d}[s]_\mathbf{c}, 10, g, \mathcal{E}(\var{\mathbf{o}}), F, \tup{I(\mathbf{u}, s), I(\mathbf{u}, s)})) &\otherwise
     \end{cases} \\
   \end{aligned}\right.
 \end{equation}
@@ -140,7 +141,7 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
   I(\mathbf{u} \in \mathbb{U}, s \in \N_S) &\equiv \tup{
     \is{\mathbf{d}}{\mathbf{d} \setminus \{ s \}},
     s,
-    \is{\mathbf{u}}{\tuple{\is{\mathbf{d}}{\{s \mapsto \mathbf{d}[s]\}}, \is{\mathbf{x}}{\mathbf{o}_\mathbf{x}}, \is{\mathbf{i}}{\mathbf{o}_\mathbf{i}}, \is{\mathbf{q}}{\mathbf{o}_\mathbf{q}}}},
+    \is{\mathbf{u}}{\tuple{\is{\mathbf{d}}{\{s \mapsto \mathbf{d}[s]\}}, \is{\mathbf{x}}{\mathbf{u}_\mathbf{x}}, \is{\mathbf{i}}{\mathbf{u}_\mathbf{i}}, \is{\mathbf{q}}{\mathbf{u}_\mathbf{q}}}},
     i,
     \is{\mathbf{t}}{[]}
   }\\
@@ -194,7 +195,7 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
 Concretely, we create the identifier from the Blake2 hash of the identifier of the creating service, the current random accumulator $\eta_0$ and the block's timeslot. Thus, within a service's accumulation it is almost certainly unique, but it is not necessarily unique across all services, nor at all times in the past. We utilize a \emph{check} function to find the first such index in this sequence which does not already represent a service:
 \begin{equation}
   \text{check}(i \in \N_S) \equiv \begin{cases}
-    i &\when i \not\in \keys{\mathbf{o}_\mathbf{d}} \\
+    i &\when i \not\in \keys{\mathbf{u}_\mathbf{d}} \\
     \text{check}((i - 2^8 + 1) \bmod (2^{32}-2^9) + 2^8)&\otherwise
   \end{cases}
 \end{equation}
@@ -411,9 +412,9 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
       \left\{ (s \mapsto g) \ \where \se_4(s) \concat \se_8(g) = \mathbf{d}_{o+12i\dots+12} \mid i \in \N_n \right\} &\when \mathbb{Z}_{o \dots+ 12n} \subset \mathbb{V}_{\memory} \\
       \error &\otherwise
     \end{cases} \\
-    (\registers'_7, \mathbf{x}'_p) &= \begin{cases}
+    (\registers'_7, (\mathbf{x}'_\mathbf{u})_\mathbf{x}) &= \begin{cases}
       (\mathtt{OK}, \tuple{m, a, v, \mathbf{g}}) &\when \mathbf{g} \ne \error \\
-      (\mathtt{OOB}, \mathbf{x}_p) &\otherwise
+      (\mathtt{OOB}, (\mathbf{x}_\mathbf{u})_\mathbf{x}) &\otherwise
     \end{cases}
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
@@ -427,10 +428,10 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
       \left[\memory_{o + 32i \dots+ 32} \mid i \orderedin \N_\mathsf{Q}\right] &\when \mathbb{Z}_{o \dots+ 32\mathsf{Q}} \subset \mathbb{V}_{\memory} \\
       \error &\otherwise
     \end{cases} \\
-    (\registers'_7, \mathbf{x}') &= \begin{cases}
-      (\mathtt{OK}, \mathbf{x} \exc \mathbf{x}'_\mathbf{c}[\registers_7] = \mathbf{c}) &\when \registers_7 < \mathsf{C} \wedge \mathbf{c} \ne \error \\
-      (\mathtt{OOB}, \mathbf{x}) &\when \mathbf{c} = \error \\
-      (\mathtt{CORE}, \mathbf{x}) &\otherwise \\
+    (\registers'_7, (\mathbf{x}'_\mathbf{u})_\mathbf{q}[\registers_7]) &= \begin{cases}
+      (\mathtt{OK}, \mathbf{c}) &\when \registers_7 < \mathsf{C} \wedge \mathbf{c} \ne \error \\
+      (\mathtt{OOB}, (\mathbf{x}_\mathbf{u})_\mathbf{q}[\registers_7]) &\when \mathbf{c} = \error \\
+      (\mathtt{CORE}, (\mathbf{x}_\mathbf{u})_\mathbf{q}[\registers_7]) &\otherwise \\
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
@@ -440,13 +441,13 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
   $g = 10$} &
   $\begin{aligned}
     \using o &= \registers_7 \\
-    \using \mathbf{v} &= \begin{cases}
+    \using \mathbf{i} &= \begin{cases}
       \left[\memory_{o + 336i \dots+ 336} \mid i \orderedin \N_\mathsf{V}\right] &\when \mathbb{Z}_{o \dots+ 336\mathsf{V}} \subset \mathbb{V}_{\memory} \\
       \error &\otherwise
     \end{cases} \\
-    (\registers'_7, \mathbf{x}') &= \begin{cases}
-      (\mathtt{OK}, \mathbf{x} \exc \mathbf{x}'_\mathbf{v} = \mathbf{v}) &\when \mathbf{v} \ne \error \\
-      (\mathtt{OOB}, \mathbf{x}) &\otherwise
+    (\registers'_7, (\mathbf{x}'_\mathbf{u})_\mathbf{i}) &= \begin{cases}
+      (\mathtt{OK}, \mathbf{i}) &\when \mathbf{v} \ne \error \\
+      (\mathtt{OOB}, (\mathbf{x}_\mathbf{u})_\mathbf{i}) &\otherwise
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
@@ -777,6 +778,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
       (\mathtt{WHO}, \registers_8, \mem, \mathbf{m}) &\otherwhen n \not\in \mathbf{m} \\
       (\mathtt{HOST}, h, \mem^*, \mathbf{m}^*) &\otherwhen c = \host \times h \\
       (\mathtt{FAULT}, x, \mem^*, \mathbf{m}^*) &\otherwhen c = \fault \times x \\
+      (\mathtt{OOG}, \registers_8, \mem^*, \mathbf{m}^*) &\otherwhen c = \oog \\
       (\mathtt{PANIC}, \registers_8, \mem^*, \mathbf{m}^*) &\otherwhen c = \panic \\
       (\mathtt{HALT}, \registers_8, \mem^*, \mathbf{m}^*) &\otherwhen c = \halt \\
     \end{cases} \\

text/serialization.tex

@@ -2,7 +2,7 @@ \section{Serialization Codec}\label{sec:serialization}
 
 \subsection{Common Terms}
 
-Our codec function $\mathcal{E}$ is used to serialize some term into a sequence of octets. We define the deserialization function $\de = \mathcal{E}^{-1}$ as the inverse of $\mathcal{E}$ and able to decode some sequence into the original value. The codec is designed such that exactly one value is encoded into any given sequence of octets, and in cases where this is not desirable then we use special codec functions.
+Our codec function $\mathcal{E}$ is used to serialize some term into a sequence of octets. We define the deserialization function $\de$ as the inverse of $\mathcal{E}$ and able to decode some sequence into the original value. The codec is designed such that exactly one value is encoded into any given sequence of octets, and in cases where this is not desirable then we use special codec functions.
 
 \subsubsection{Trivial Encodings}
 We define the serialization of $\varnothing$ as the empty sequence: