Activity statistics

graypaper.tex

@@ -29,7 +29,7 @@
 \input{text/judgments.tex}
 \input{text/reporting_assurance.tex}
 \input{text/accumulation.tex}
-\input{text/ratings.tex}
+\input{text/statistics.tex}
 \input{text/work_packages_and_reports.tex}
 \input{text/guaranteeing.tex}
 \input{text/assurance.tex}

preamble.tex

@@ -140,6 +140,7 @@
 \newcommand*{\tuple}[1]{\ltuple#1\rtuple}
 \newcommand*{\floor}[1]{\left\lfloor#1\right\rfloor}
 \newcommand*{\ceil}[1]{\left\lceil#1\right\rceil}
+\newcommand*{\len}[1]{\left|#1\right|}
 \newcommand*{\fnfrac}[2]{\left\lfloor\nicefrac{#1}{#2}\right\rfloor}
 \newcommand*{\ffrac}[2]{\left\lfloor\frac{#1}{#2}\right\rfloor}
 \newcommand*{\transpose}{{}^\text{T}}
@@ -176,6 +177,7 @@
 \newcommand*{\wr¬srlookup}{\mathbf{l}}
 \newcommand*{\wr¬authoutput}{\mathbf{o}} % TODO: Consider renaming to \mathbf{u} to free up \mathbf{o}
 \newcommand*{\wr¬results}{\mathbf{r}} % TODO: Consider renaming to avoid overloading \mathbf{r} reports vs results; maybe \mathbf{t} for results
+\newcommand*{\wr¬authgasused}{g}
 
 % TODO: Standardize and fully check this:
 % p P: work Packages

text/accumulation.tex

@@ -1,6 +1,7 @@
 \newcommand*{\srmap}{P}
 \newcommand*{\opers}{O}
 \newcommand*{\servouts}{B}
+\newcommand*{\gasused}{U}
 \newcommand*{\accumulatedcup}{\overbrace{\accumulated}}
 
 \section{Accumulation}\label{sec:accumulation}
@@ -111,34 +112,34 @@ \subsection{Execution}
 
 Finally, we denote the set of service/hash pairs, utilized as a service-indexed commitment to the accumulation output, as $\servouts$:
 \begin{equation}
-  \servouts \equiv \{(\N_S, \H)\}
+  \servouts \equiv \{(\N_S, \H)\} \qquad \gasused \equiv \seq{\tup{\N_S, \N_G}}
 \end{equation}
 
 We define the outer accumulation function $\Delta_+$ which transforms a gas-limit, a sequence of work-reports, an initial partial-state and a dictionary of services enjoying free accumulation, into a tuple of the number of work-results accumulated, a posterior state-context, the resultant deferred-transfers and accumulation-output pairings:
 \begin{equation}
   \Delta_+\colon\left\{\begin{aligned}
-    &(\N_G, \seq{\mathbb{W}}, \partialstate, \dict{\N_S}{\N_G}) \to (\N, \partialstate, \defxfers, \servouts) \\
+    &(\N_G, \seq{\mathbb{W}}, \partialstate, \dict{\N_S}{\N_G}) \to (\N, \partialstate, \defxfers, \servouts, \gasused) \\
     &(g, \mathbf{w}, \mathbf{o}, \mathbf{f}) \!\mapsto\! \begin{cases}
       (0, \mathbf{o}, [], \{\}) &
         \when i = 0 \\
-      (i + j, \mathbf{o}', \mathbf{t}^* \!\!\concat \mathbf{t}, \mathbf{b}^* \!\cup \mathbf{b})\!\!\!\! &
-        \otherwise\!\!\!\!\!\!\!\! \\
+      (i + j, \mathbf{o}', \mathbf{t}^* \!\!\concat \mathbf{t}, \mathbf{b}^* \!\cup \mathbf{b}, \mathbf{u}^* \!\!\concat \mathbf{u})\!\!\!\! &
+        \text{o/w}\!\!\!\!\!\!\!\! \\
     \end{cases} \\
     &\quad\where i = \max(\N_{|\mathbf{w}| + 1}): \sum_{w \in \mathbf{w}_{\dots i}}\sum_{r \in w_\mathbf{r}}(r_g) \le g \\
-    &\quad\also (g^*, \mathbf{o}^*, \mathbf{t}^*, \mathbf{b}^*) = \Delta_*(\mathbf{o}, \mathbf{w}_{\dots i}, \mathbf{f}) \\
-    &\quad\also (j, \mathbf{o}', \mathbf{t}, \mathbf{b}) = \Delta_+(g - g^*, \mathbf{w}_{i\dots}, \mathbf{o}^*, \{\})
+    &\quad\also (\mathbf{u}^*, \mathbf{o}^*, \mathbf{t}^*, \mathbf{b}^*) = \Delta_*(\mathbf{o}, \mathbf{w}_{\dots i}, \mathbf{f}) \\
+    &\quad\also (j, \mathbf{o}', \mathbf{t}, \mathbf{b}, \mathbf{u}) = \Delta_+(g - \!\!\!\!\sum_{(s, u) \in \mathbf{u}^*}\!\!\!\!u, \mathbf{w}_{i\dots}, \mathbf{o}^*, \{\})
   \end{aligned}\right.
 \end{equation}
 
 We come to define the parallelized accumulation function $\Delta_*$ which, with the help of the single-service accumulation function $\Delta_1$, transforms an initial state-context, together with a sequence of work-reports and a dictionary of privileged always-accumulate services, into a tuple of the total gas utilized in \textsc{pvm} execution $u$, a posterior state-context $(\mathbf{x}', \mathbf{d}', \mathbf{i}', \mathbf{q}')$ and the resultant accumulation-output pairings $\mathbf{b}$ and deferred-transfers $\wideparen{\mathbf{t}}$:
 \begin{equation}
   \Delta_*\colon\left\{\;\begin{aligned}
-    &(\partialstate, \seq{\mathbb{W}}, \dict{\N_S}{\N_G}) \to (\N_G, \partialstate, \defxfers, \servouts) \\
-    &(\mathbf{o}, \mathbf{w}, \mathbf{f}) \mapsto (u, ((\mathbf{d} \cup \mathbf{n}) \setminus \mathbf{m}, \mathbf{i}', \mathbf{q}', \mathbf{x}'), \wideparen{\mathbf{t}}, \mathbf{b})\!\!\!\!\!\!\\
+    &(\partialstate, \seq{\mathbb{W}}, \dict{\N_S}{\N_G}) \to (\partialstate, \defxfers, \servouts, \gasused) \\
+    &(\mathbf{o}, \mathbf{w}, \mathbf{f}) \mapsto (((\mathbf{d} \cup \mathbf{n}) \setminus \mathbf{m}, \mathbf{i}', \mathbf{q}', \mathbf{x}'), \wideparen{\mathbf{t}}, \mathbf{b}, \mathbf{u})\!\!\!\!\!\!\\
     &\text{where:}\\
     &\ \begin{aligned}
       \mathbf{s} &= \{ \mathbf{r}_s \mid w \in \mathbf{w}, \mathbf{r} \in w_\mathbf{r} \} \cup \keys{\mathbf{f}} \\
-      u &= \sum_{s \in \mathbf{s}}(\Delta_1(\mathbf{o}, \mathbf{w}, \mathbf{f}, s)_u) \\
+      \mathbf{u} &= [(s, \Delta_1(\mathbf{o}, \mathbf{w}, \mathbf{f}, s)_u) \mid s \orderedin \mathbf{s}] \\
       \mathbf{b} &= \{ (s, b) \mid s \in \mathbf{s},\, b = \Delta_1(\mathbf{o}, \mathbf{w}, \mathbf{f}, s)_b,\, b \ne \none \} \\
       \mathbf{t} &= [\Delta_1(\mathbf{o}, \mathbf{w}, \mathbf{f}, s)_\mathbf{t} \mid s \orderedin \mathbf{s}] \\
       &(\mathbf{d}, \mathbf{i}, \mathbf{q}, (m, a, v, \mathbf{z})) = \mathbf{o} \\
@@ -168,7 +169,10 @@ \subsection{Execution}
     &\Delta_1 \colon \left\{\;\begin{aligned}
     &\begin{aligned}
       (\partialstate, \seq{\mathbb{W}}, \dict{\N_S}{\N_G}, \N_S) &\to \tup{
-        \partialstate, \defxfers, \H\bm{?}, \N_G
+        \begin{alignedat}{3}
+          \isa{\mathbf{o}&}{\partialstate}\,,\;\isa{&\mathbf{t}&}{\defxfers}\,,\\
+          \isa{b&}{\H\bm{?}}\,,\;\isa{&u&}{\N_G}
+        \end{alignedat}
       } \\
       (\mathbf{o}, \mathbf{w}, \mathbf{f}, s) &\mapsto \Psi_A(\mathbf{o}, \tau', s, g, \mathbf{p})
     \end{aligned} \\
@@ -198,25 +202,42 @@ \subsection{Deferred Transfers and State Integration}
 
 Given the result of the top-level $\Delta_+$, we may define the posterior state $\chi'$, $\varphi'$ and $\iota'$ as well as the first intermediate state of the service-accounts $\accountspostacc$ and the \textsc{Beefy} commitment map $\beefycommitmap$:
 \begin{align}
-  \using g &= \max\left(\mathsf{G}_T, \mathsf{G}_A\cdot \mathsf{C} + \sum_{x \in \mathcal{V}(\chi_\mathbf{g})}(x)\right)\\
-  \using (n, \mathbf{o}, \mathbf{t}, \beefycommitmap) &= \Delta_+(g, \mathbf{W}^*, (\chi, \accountspre, \iota, \varphi), \chi_\mathbf{g}) \\
-  (\chi', \accountspostacc, \iota', \varphi') &\equiv \mathbf{o}
+  \using &g = \max\left(\mathsf{G}_T, \mathsf{G}_A\cdot \mathsf{C} + \textstyle \sum_{x \in \mathcal{V}(\chi_\mathbf{g})}(x)\right)\\
+  \using &(n, \mathbf{o}, \mathbf{t}, \beefycommitmap, \mathbf{u}) = \Delta_+(g, \mathbf{W}^*, (\chi, \accountspre, \iota, \varphi), \chi_\mathbf{g}) \\
+  &(\chi', \accountspostacc, \iota', \varphi') \equiv \mathbf{o}
+\end{align}
+
+We compose $\mathbf{I}$, our accumulation statistics, which is a mapping from the service indices which were accumulated to the amount of gas used throughout accumulation and the number of work-reports accumulated. Formally:
+\begin{align}
+  &\mathbf{I} \in \dict{\N_S}{\tuple{\N_G, \N}} \\
+  &\textstyle \mathbf{I} \equiv \left\{ s \mapsto \tup{\sum_{(s, u) \in \mathbf{u}}(u), \len{N(s)}} \;\middle\mid\; N(s) \ne [] \right\} \\
+  \where &N(s) \equiv \sq{r \mid w \orderedin \mathbf{W}^*_{\dots n} , r \orderedin w_\mathbf{r} , r_s = s }
 \end{align}
 
 Note that the accumulation commitment map $\beefycommitmap$ is a set of pairs of indices of the output-yielding accumulated services to their accumulation result. This is utilized in equation \ref{eq:buildbeefymap}, when determining the accumulation-result tree root for the present block, useful for the \textsc{Beefy} protocol.
 
 We have denoted the sequence of implied transfers as $\mathbf{t}$, ordered internally according to the source service's execution. We define a selection function $R$, which maps a sequence of deferred transfers and a desired destination service index into the sequence of transfers targeting said service, ordered primarily according to the source service index and secondarily their order within $\mathbf{t}$. Formally:
-\begin{align}
+\begin{equation}
   R\colon \left\{\;\begin{aligned}
     (\defxfers, \N_S) &\to \defxfers \\
     (\mathbf{t}, d) &\mapsto \left[\,t \mid s \orderedin \N_S,\ t \orderedin \mathbf{t},\ t_s = s,\ t_d = d\,\right]
-  \end{aligned}\right.
-\end{align}
+  \end{aligned}\right.\!\!\!\!
+\end{equation}
 
 The second intermediate state $\accountspostxfer$ may then be defined with all the deferred effects of the transfers applied:
-\begin{equation}
-  \accountspostxfer = \{ s \mapsto \Psi_T(\accountspostacc, \tau', s, R(\mathbf{t}, s)) \mid (s \mapsto a) \in \accountspostacc \}
-\end{equation}
+\begin{align}
+  \mathbf{x} &= \{ s \mapsto \Psi_T(\accountspostacc, \tau', s, R(\mathbf{t}, s)) \mid (s \mapsto a) \in \accountspostacc \} \\
+  \accountspostxfer &\equiv \{ s \mapsto a \mid (s \mapsto \tup{a, u}) \in \mathbf{x} \}
+\end{align}
+
+Furthermore we build the deferred transfers statistics value $\mathbf{X}$ as the number of transfers and the total gas used in transfer processing for each \emph{destination} service index. Formally:
+\begin{align}
+  &\mathbf{X} \in \dict{\N_S}{\tuple{\N, \N_G}} \\
+  &\textstyle \mathbf{X} \equiv \left\{ d \mapsto \tup{\len{R(\mathbf{t}, d)}, u} \;\middle\vert\; \begin{aligned}
+    R(\mathbf{t}, d) &\ne [],\\ \exists a: \mathbf{x}[d] &= (a, u)
+  \end{aligned}
+  \right\}
+\end{align}
 
 Note that $\Psi_T$ is defined in appendix \ref{sec:ontransferinvocation} such that it results in $\accountspostacc[d]$, \ie no difference to the account's intermediate state, if $R(d) = []$, \ie said account received no transfers.
 

text/definitions.tex

@@ -175,13 +175,15 @@ \subsubsection{Block-context Terms}
   \item[$\mathbf{G}$] The mapping from cores to guarantor keys. See section \ref{sec:coresandvalidators}.
   \item[$\mathbf{G^*}$] The mapping from cores to guarantor keys for the previous rotation. See section \ref{sec:coresandvalidators}.
   \item[$\mathbf{H}$] The block header. See equation \ref{eq:header}.
+  \item[$\mathbf{I}$] The sequence of work-reports which were accumulated this in this block. See equation \ref{eq:accumulatedreports}.
   \item[$\mathbf{Q}$] The selection of ready work-reports which a validator determined they must audit. See equation \ref{eq:auditselection}.
   \item[$\mathbf{R}$] The set of Ed25519 guarantor keys who made a work-report. See equation \ref{eq:guarantorsig}.
   \item[$\mathbf{S}$] The set of indices of services which have been accumulated (``progressed'') in the block. See equation \ref{eq:servicestoaccumulate}.
   \item[$\mathbf{T}$] The ticketed condition, true if the block was sealed with a ticket signature rather than a fallback. See equations \ref{eq:ticketconditiontrue} and \ref{eq:ticketconditionfalse}.
   \item[$\mathbf{U}$] The audit condition, equal to $\top$ once the block is audited. See section \ref{sec:auditing}.
   \item[$\mathbf{V}$] The set of verdicts in the present block. See equation \ref{eq:verdicts}.\\
   \item[$\mathbf{W}$] The sequence of work-reports which have now become available and ready for accumulation. See equation \ref{eq:availableworkreports}.
+  \item[$\mathbf{X}$] The sequence of transfers implied by the block's accumulations. See equation \ref{eq:deferredtransfers}.\\
 \end{description}
 
 Without any superscript, the block is assumed to the block being imported or, if no block is being imported, the head of the best chain (see section \ref{sec:bestchain}). Explicit block-contextualizing superscripts include:

text/pvm.tex

@@ -825,18 +825,29 @@ \subsection{Standard Program Initialization}\label{sec:standardprograminit}
 \subsection{Argument Invocation Definition}
 
 The four instances where the \textsc{pvm} is utilized each expect to be able to pass argument data in and receive some return data back. We thus define the common \textsc{pvm} program-argument invocation function $\Psi_M$:
-\begin{align}
-  \Psi_M&\colon \left\{\begin{aligned}
-    (\Y, \N_R, \N_G, \Y_{:\mathsf{Z}_I}, \Omega\langle X \rangle, X) &\to (\mathbb{Z}_G, \Y \cup \{\panic, \oog\}, X)\\
+\begin{equation}
+  \Psi_M\colon \left\{\begin{aligned}
+    \left(
+      \Y, \N_R, \N_G, \Y_{:\mathsf{Z}_I}, \Omega\langle X \rangle, X
+    \right) &\to (\N_G, \Y \cup \{\panic, \oog\}, X)\\
     (\mathbf{p}, \imath, \gascounter, \mathbf{a}, f, \mathbf{x}) &\mapsto \begin{cases}
-      (\gascounter, \panic, \mathbf{x}) &\when Y(\mathbf{p}) = \none\\
-      R(\Psi_H(\mathbf{c}, \imath, \gascounter, \registers, \mem, f, \mathbf{x})) &\when Y(\mathbf{p}) = (\mathbf{c}, \registers, \mem)
+      (0, \panic, \mathbf{x}) &\when Y(\mathbf{p}) = \none\\
+      R(\gascounter, \Psi_H(\mathbf{c}, \imath, \gascounter, \registers, \mem, f, \mathbf{x})) &\when Y(\mathbf{p}) = (\mathbf{c}, \registers, \mem)\\
+      \multicolumn{2}{l}{
+        \quad \where R \colon (\gascounter, \tup{\begin{alignedat}{5}
+          &\varepsilon,\, &&\imath',\, &&\gascounter',\\
+          &\registers',\, &&\mem',\, &&\mathbf{x}'
+        \end{alignedat}
+        }) \mapsto \begin{cases}
+          (u, \oog, \mathbf{x}') &\when \varepsilon = \oog \\
+          (u, \memory'_{\registers'_{7}\dots+\registers'_{8}}, \mathbf{x}') &\when \varepsilon = \halt \wedge \mathbb{N}_{\registers'_{7}\dots+\registers'_{8}} \subset \mathbb{V}_{\mem'} \\
+          (u, [], \mathbf{x}') &\when \varepsilon = \halt \wedge \mathbb{N}_{\registers'_{7}\dots+\registers'_{8}} \not\subset \mathbb{V}_{\mem'} \\
+          (u, \panic, \mathbf{x}') &\otherwise \\
+          \multicolumn{2}{l}{\quad \where u = \gascounter - \max(\gascounter', 0)}
+        \end{cases}
+      }\!\!\!\!\!\!\!\!
     \end{cases}
-  \end{aligned}\right.\\
-  \where R&\colon (\varepsilon, \imath', \gascounter', \registers', \mem', \mathbf{x}') \mapsto \begin{cases}
-    (\gascounter', \oog, \mathbf{x}') &\when \varepsilon = \oog \\
-    (\gascounter', \memory'_{\registers'_{7}\dots+\registers'_{8}}, \mathbf{x}') &\when \varepsilon = \halt \wedge \mathbb{N}_{\registers'_{7}\dots+\registers'_{8}} \subset \mathbb{V}_{\mem'} \\
-    (\gascounter', [], \mathbf{x}') &\when \varepsilon = \halt \wedge \mathbb{N}_{\registers'_{7}\dots+\registers'_{8}} \not\subset \mathbb{V}_{\mem'} \\
-    (\gascounter', \panic, \mathbf{x}') &\otherwise \\
-  \end{cases}
-\end{align}
+  \end{aligned}\right.
+\end{equation}
+
+Note that the first tuple item is the amount of gas consumed by the operation, but never greater than the amount of gas provided for the operation.

text/pvm_invocations.tex

@@ -128,7 +128,7 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
     \tuple{\partialstate, \defxfers, \H\bm{?}, \N_G} \\
     (\mathbf{u}, t, s, g, \mathbf{o}) &\mapsto \begin{cases}
       \tup{I(\mathbf{u}, s)_\mathbf{u}, [], \none, 0} &\when \mathbf{u}_\mathbf{d}[s]_\mathbf{c} = \none \\
-      C(g, \Psi_M(\mathbf{u}_\mathbf{d}[s]_\mathbf{c}, 5, g, \se(t, s, \var{\mathbf{o}}), F, \tup{I(\mathbf{u}, s), I(\mathbf{u}, s)})) &\otherwise
+      C(\Psi_M(\mathbf{u}_\mathbf{d}[s]_\mathbf{c}, 5, g, \se(t, s, \var{\mathbf{o}}), F, \tup{I(\mathbf{u}, s), I(\mathbf{u}, s)})) &\otherwise
     \end{cases} \\
   \end{aligned}\right.\\
   I&\colon\left\{\begin{aligned}
@@ -169,25 +169,25 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
     &\qquad \where \mathbf{x}^* = \mathbf{x} \exc (\mathbf{x}^*_\mathbf{u})_\mathbf{d}[\mathbf{x}^*_s] = \mathbf{s}
   \end{aligned}\right.\\
   C&\colon\left\{\begin{aligned}
-    (\N_G, \Z_G, \mathbb{Y} \cup \{\oog, \panic\}, (\mathbf{X}, \mathbf{X})) &\to (\partialstate, \defxfers, \H\bm{?}, \N_G) \\
-    (g, r, \mathbf{o}, (\mathbf{x}, \mathbf{y})) &\mapsto \begin{cases}
+    (\N_G, \mathbb{Y} \cup \{\oog, \panic\}, (\mathbf{X}, \mathbf{X})) &\to (\partialstate, \defxfers, \H\bm{?}, \N_G) \\
+    (u, \mathbf{o}, (\mathbf{x}, \mathbf{y})) &\mapsto \begin{cases}
       \tup{
         \mathbf{y}_\mathbf{u},
         \mathbf{y}_\mathbf{t},
         \mathbf{y}_y,
-        g - \max(r, 0)
+        u
       } & \when \mathbf{o} \in \{\oog, \panic\} \\
       \tup{
         \mathbf{x}_\mathbf{u},
         \mathbf{x}_\mathbf{t},
         \mathbf{o},
-        g - \max(r, 0)
+        u
       } & \otherwhen \mathbf{o} \in \H \\
       \tup{
         \mathbf{x}_\mathbf{u},
         \mathbf{x}_\mathbf{t},
         \mathbf{x}_y,
-        g - \max(r, 0)
+        u
       } & \otherwise \\
     \end{cases}
   \end{aligned}\right.
@@ -212,14 +212,19 @@ \subsection{On-Transfer Invocation}\label{sec:ontransferinvocation}
 We define the On-Transfer service-account invocation function as $\Psi_T$; it is somewhat similar to the Accumulation Invocation except that the only state alteration it facilitates are basic alteration to the storage of the subject account. No further transfers may be made, no privileged operations are possible, no new accounts may be created nor other operations done on the subject account itself. The function is defined as:
 \begin{align}
   \Psi_T &: \begin{cases}
-    (\dict{\N_S}{\mathbb{A}}, \N_T, \N_S, \seq{\mathbb{T}}) &\to \mathbb{A} \\
+    (\dict{\N_S}{\mathbb{A}}, \N_T, \N_S, \seq{\mathbb{T}}) &\to \tuple{\mathbb{A}, \N_G} \\
     (\mathbf{d}, t, s, \mathbf{t}) &\mapsto \begin{cases}
-    \mathbf{s} &\when \mathbf{s}_\mathbf{c} = \none \vee \mathbf{t} = [] \\
-    \mathbf{s}' \ \where (g, \mathbf{r}, \mathbf{s}') =\Psi_M(\mathbf{s}_\mathbf{c}, 10, \sum_{r \in \mathbf{t}}{(r_g)}, \se(t, s, \var{\mathbf{t}}), F, \mathbf{s}) &\otherwise
+    \tup{\mathbf{s}, 0} &\when \mathbf{s}_\mathbf{c} = \none \vee \mathbf{t} = [] \\
+    \tup{\mathbf{s}', u} &\otherwise \\
+    \multicolumn{2}{l}{
+\begin{aligned}
+        \quad\where (u, \mathbf{r}, \mathbf{s}') &= \Psi_M(\mathbf{s}_\mathbf{c}, 10, \sum_{r \in \mathbf{t}}{(r_g)}, \se(t, s, \var{\mathbf{t}}), F, \mathbf{s}) \\
+        \quad\also \mathbf{s} &= \mathbf{d}[s]\exc\mathbf{s}_b = \mathbf{d}[s]_b + \sum_{r \in \mathbf{t}}{r_a}
+\end{aligned}
+    }
     \end{cases} \\
   \end{cases} \\
-  \where \mathbf{s} &= \mathbf{d}[s]\exc\mathbf{s}_b = \mathbf{d}[s]_b + \sum_{r \in \mathbf{t}}{r_a} \\
-  F \in \Omega\ang{\mathbb{A}}\colon (n, \gascounter, \registers, \memory, \mathbf{s}) &\equiv \begin{cases}
+  \also F &\in \Omega\ang{\mathbb{A}}\colon (n, \gascounter, \registers, \memory, \mathbf{s}) \equiv \begin{cases}
     \Omega_L(\gascounter, \registers, \memory, \mathbf{s}, s, \mathbf{d}) &\when n = \mathtt{lookup} \\
     \Omega_R(\gascounter, \registers, \memory, \mathbf{s}, s, \mathbf{d}) &\when n = \mathtt{read} \\
     \Omega_W(\gascounter, \registers, \memory, \mathbf{s}, s) &\when n = \mathtt{write} \\