From 797ed3773deeffcf029eda2152fd3041593dcd4f Mon Sep 17 00:00:00 2001 From: Gav Date: Wed, 9 Oct 2024 12:44:09 +0100 Subject: [PATCH 1/7] Accumulation: Subtle fixes --- text/accumulation.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/text/accumulation.tex b/text/accumulation.tex index 0f0ce6f..b6de66f 100644 --- a/text/accumulation.tex +++ b/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(q, \accumulatedcup \cup\;\srmap(\mathbf{W}^!)) \\ + \quad\where q &= E(\wideparen{\ready_{m\dots}} \concat \wideparen{\ready_{\dots m}} \concat \mathbf{W}^Q, \srmap(\mathbf{W}^!)) \end{align} \subsection{Execution} From 8fea88a3d516d2813ef0a4ef60fa8a2530dcd925 Mon Sep 17 00:00:00 2001 From: Gav Date: Wed, 9 Oct 2024 14:17:54 +0100 Subject: [PATCH 2/7] Accumulation: bold q --- text/accumulation.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/accumulation.tex b/text/accumulation.tex index b6de66f..585b497 100644 --- a/text/accumulation.tex +++ b/text/accumulation.tex @@ -100,8 +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(q, \accumulatedcup \cup\;\srmap(\mathbf{W}^!)) \\ - \quad\where q &= E(\wideparen{\ready_{m\dots}} \concat \wideparen{\ready_{\dots m}} \concat \mathbf{W}^Q, \srmap(\mathbf{W}^!)) + \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} @@ -127,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} From b0ec87d0e7bb7b476d0b01eb12ab15a20ae81389 Mon Sep 17 00:00:00 2001 From: Gav Date: Wed, 9 Oct 2024 14:18:07 +0100 Subject: [PATCH 3/7] PVM Hostcalls: Fix u/o --- text/pvm_invocations.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex index d6abaf2..58fa598 100644 --- a/text/pvm_invocations.tex +++ b/text/pvm_invocations.tex @@ -130,8 +130,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 +140,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 +194,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} From fd7aee1ab73dbc16271f8136fe671cf42cc61725 Mon Sep 17 00:00:00 2001 From: Gav Date: Thu, 10 Oct 2024 12:42:55 +0100 Subject: [PATCH 4/7] PVM Hostcalls: Fix privileged ops --- text/pvm_invocations.tex | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex index 58fa598..b4e74b3 100644 --- a/text/pvm_invocations.tex +++ b/text/pvm_invocations.tex @@ -411,9 +411,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 +427,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 +440,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} From 5e027f268ff0e0864aeae3f2b2ef49eda4fcfed6 Mon Sep 17 00:00:00 2001 From: Gav Date: Thu, 10 Oct 2024 14:49:08 +0100 Subject: [PATCH 5/7] PVM: 0 instruction counter on panic & halt --- text/pvm.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/text/pvm.tex b/text/pvm.tex index d397310..8a26dd6 100644 --- a/text/pvm.tex +++ b/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)\\ From 88c2611ea4f1ef20fad4db6c7b5bce1a5689f176 Mon Sep 17 00:00:00 2001 From: Gav Date: Fri, 11 Oct 2024 16:43:11 +0100 Subject: [PATCH 6/7] Use cdot for j*k --- text/erasure_coding.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/erasure_coding.tex b/text/erasure_coding.tex index d8026f4..b437c4f 100644 --- a/text/erasure_coding.tex +++ b/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: From 6af4c9c3df4d7c5c26321fbe2d29dc885bfe67f5 Mon Sep 17 00:00:00 2001 From: Gav Date: Fri, 11 Oct 2024 17:56:30 +0100 Subject: [PATCH 7/7] PVM Hostcalls: Add OOG for invoke --- text/pvm_invocations.tex | 2 ++ text/serialization.tex | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex index b4e74b3..8670362 100644 --- a/text/pvm_invocations.tex +++ b/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$. @@ -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} \\ diff --git a/text/serialization.tex b/text/serialization.tex index 6151212..db7bb62 100644 --- a/text/serialization.tex +++ b/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: