From 9a6d0670c3a6351b4fc070b4891ef2355963aa8a Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 1 Nov 2024 11:39:24 +0100
Subject: [PATCH 01/31] Version

---
 VERSION      | 2 +-
 preamble.tex | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/VERSION b/VERSION
index c8a5397..79a2734 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-0.4.5
\ No newline at end of file
+0.5.0
\ No newline at end of file
diff --git a/preamble.tex b/preamble.tex
index 8cbe34e..001177e 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -179,7 +179,7 @@
 \newcommand*{\registers}{\omega}
 \newcommand*{\memory}{\mu}
 
-\newcommand*{\jamdraftversion}{\input{VERSION}\!\!\!\! Bangkok}
+\newcommand*{\jamdraftversion}{\input{VERSION}\!\!\!\!}
 \newcommand*{\jamdraftversionstring}{\jamdraftversion}
 
 \newcommand*{\makegpbackground}{

From 69bb8d6a70370fc2e8224e33f951764befce7d4c Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 5 Nov 2024 06:30:26 +0000
Subject: [PATCH 02/31] Definitions: Q is exact, not a maximum.

---
 text/definitions.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/text/definitions.tex b/text/definitions.tex
index 7017e26..6d692e6 100644
--- a/text/definitions.tex
+++ b/text/definitions.tex
@@ -271,7 +271,7 @@ \subsubsection{Constants}
   \item[$\mathsf{N} = 2$] The number of ticket entries per validator.
   \item[$\mathsf{O} = 8$] The maximum number of items in the authorizations pool.
   \item[$\mathsf{P} = 6$] The slot period, in seconds.
-  \item[$\mathsf{Q} = 80$] The maximum number of items in the authorizations queue.
+  \item[$\mathsf{Q} = 80$] The number of items in the authorizations queue.
   \item[$\mathsf{R} = 10$] The rotation period of validator-core assignments, in timeslots.
   \item[$\mathsf{S} = 1024$] The maximum number of entries in the accumulation queue.
   \item[$\mathsf{U} = 5$] The period in timeslots after which reported but unavailable work may be replaced.

From 06109a81b252d14725605b8b62df295c76586814 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 5 Nov 2024 06:31:20 +0000
Subject: [PATCH 03/31] PVM Hostcalls: Fix gas spec for quit

---
 text/pvm_invocations.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 013f9f2..63251f8 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -532,7 +532,7 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
   \makecell*[l]{
   $\Omega_Q(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y}))$ \\
   \texttt{quit} = 12 \\
-  $g = 10 + \registers_8 + 2^{32}\cdot\registers_9 $} &
+  $g = 10$} &
   $\begin{aligned}
     \using [d, o] &= \registers_{7,8} \\
     \using a &= (\mathbf{x}_\mathbf{s})_b - (\mathbf{x}_\mathbf{s})_t + \mathsf{B}_S \\

From ee24ee1b59c3d4dfaaa6d2c0f4b3bdbd51ff4a97 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 5 Nov 2024 06:35:55 +0000
Subject: [PATCH 04/31] Reporting: Fix usage of theta

---
 text/reporting_assurance.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/text/reporting_assurance.tex b/text/reporting_assurance.tex
index 1ed0b59..f03d070 100644
--- a/text/reporting_assurance.tex
+++ b/text/reporting_assurance.tex
@@ -284,7 +284,7 @@ \subsubsection{Contextual Validity of Reports}\label{sec:contextualvalidity}
 
 We require that the work-package of the report not be the work-package of some other report made in the past. We ensure that the work-package not appear anywhere within our pipeline. Formally:
 \begin{align}
-  &\using \mathbf{q} = \{(w_x)_p \mid \mathbf{q} \in \ready, w \in \keys{\mathbf{q}}\} \\
+  &\using \mathbf{q} = \{(w_x)_p \mid \mathbf{q} \in \ready, (w, \mathbf{d}) \in \mathbf{q}\} \\
   &\using \mathbf{a} = \{((i_w)_x)_p \mid i \in \rho, i \ne \none\}\\
   &\forall p \in \mathbf{p}, p \not\in \bigcup_{x \in \beta}\keys{x_\mathbf{p}} \cup \bigcup_{x \in \accumulated}x \cup \mathbf{q} \cup \mathbf{a}
 \end{align}

From 896430a35c6247175d0fdf41d2e791bacd2686e7 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 5 Nov 2024 10:17:39 +0000
Subject: [PATCH 05/31] Merklisation: Make the byte selection explicit for
 solicits.

---
 text/merklization.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/text/merklization.tex b/text/merklization.tex
index 28f7527..a4d54f9 100644
--- a/text/merklization.tex
+++ b/text/merklization.tex
@@ -42,7 +42,7 @@ \subsection{Serialization}
     \forall (s \mapsto \mathbf{a}) \in \delta: &&C(255, s) &\mapsto \mathbf{a}_c \concat \se_8(\mathbf{a}_b, \mathbf{a}_g, \mathbf{a}_m, \mathbf{a}_l) \concat \se_4(\mathbf{a}_i) \;, \\
     \forall (s \mapsto \mathbf{a}) \in \delta, (k \mapsto \mathbf{v}) \in \mathbf{a}_\mathbf{s}: &&C(s, \se_4(2^{32}-1) \frown k_{0\dots 28}) &\mapsto \mathbf{v} \;, \\
     \forall (s \mapsto \mathbf{a}) \in \delta, (h \mapsto \mathbf{p}) \in \mathbf{a}_\mathbf{p}: &&C(s, \se_4(2^{32}-2) \frown h_{1\dots 29}) &\mapsto \mathbf{p} \;, \\
-    \forall (s \mapsto \mathbf{a}) \in \delta, (\tup{h, l} \mapsto \mathbf{t}) \in \mathbf{a}_\mathbf{l}: &&C(s, \se_4(l) \concat \mathcal{H}(h)) &\mapsto \se(\var{[\se_4(x) \mid x \orderedin \mathbf{t}]})
+    \forall (s \mapsto \mathbf{a}) \in \delta, (\tup{h, l} \mapsto \mathbf{t}) \in \mathbf{a}_\mathbf{l}: &&C(s, \se_4(l) \concat \mathcal{H}(h)_{2\dots 30}) &\mapsto \se(\var{[\se_4(x) \mid x \orderedin \mathbf{t}]})
   \end{aligned}\right.
 \end{equation}
 

From ba29a408547237dd2b8641cbfea4ca18ae0ace70 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 11:50:16 +0000
Subject: [PATCH 06/31] Numbering is by section

---
 preamble.tex     | 4 ++++
 text/ratings.tex | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/preamble.tex b/preamble.tex
index 8cbe34e..e9c1e06 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -30,6 +30,10 @@
 \usepackage{ifthen}
 \usepackage{hyperref}
 \usepackage{changepage}
+
+\numberwithin{equation}{section}
+\renewcommand{\theequation}{\thesection.\arabic{equation}}
+
 \strictpagecheck
 \addbibresource{biblio.bib}
 
diff --git a/text/ratings.tex b/text/ratings.tex
index 92ffd86..b689046 100644
--- a/text/ratings.tex
+++ b/text/ratings.tex
@@ -53,7 +53,7 @@ \section{Validator Activity Statistics}\label{sec:bookkeeping}
         \end{cases}\\
         \pi'_0[v]_g &\equiv \mathbf{a}[v]_g + (\kappa'_v \in \mathbf{R})\\
         \pi'_0[v]_a &\equiv \mathbf{a}[v]_a + (\exists a \in \xtassurances : a_v = v)
-    \end{aligned}\right.
+    \end{aligned}\right.\!\!\!\!
 \end{align}
 
 Note that $\mathbf{R}$ is the \emph{Reporters} set, as defined in equation \ref{eq:guarantorsig}.

From 938fe4510d4bfe11cc1f03eaa3ba2f2b6dbe2fe3 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 11:53:08 +0000
Subject: [PATCH 07/31] PVM Invocations: u_d not d

---
 text/pvm_invocations.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 63251f8..3f75796 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -131,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(\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
+      \tup{I(\mathbf{u}, s)_\mathbf{u}, [], \none, 0} &\when \mathbf{u}_\mathbf{d}[s]_\mathbf{c} = \none \\
+      C(\Psi_M(\mathbf{u}_\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}

From 3c4d4a009e44ad4130a7b7dddf53ea35465485ff Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 11:57:03 +0000
Subject: [PATCH 08/31] Intro: Edits

---
 text/intro.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/text/intro.tex b/text/intro.tex
index a43ffb6..3934b96 100644
--- a/text/intro.tex
+++ b/text/intro.tex
@@ -4,7 +4,7 @@ \subsection{Nomenclature}
 
 %As its namesake paper pointed out, the name \emph{Polkadot} means several things depending on context. It might mean variously the product vision set forth in said paper of a scalable heterogeneous multichain; the decentralized blockchain network and service which came to be along with its state and history; or possibly the protocol and technology-base utilized in order to maintain and run this network and others such as \emph{Kusama}.
 
-In this paper, we introduce a decentralized, crypto-economic protocol to which the Polkadot Network could conceivably transition itself in a major revision. Following this eventuality (which must not be taken for granted since Polkadot is a decentralized network) this protocol might also become known as \emph{Polkadot} or some derivation thereof. However, at this stage this is not the case, therefore our proposed protocol will for the present be known as \Jam.
+In this paper, we introduce a decentralized, crypto-economic protocol to which the Polkadot Network will transition itself in a major revision on the basis of approval by its governance apparatus.
 
 An early, unrefined, version of this protocol was first proposed in Polkadot Fellowship \textsc{rfc}\oldstylenums{31}, known as \emph{CoreJam}. CoreJam takes its name after the collect/refine/join/accumulate model of computation at the heart of its service proposition. While the CoreJam \textsc{rfc} suggested an incomplete, scope-limited alteration to the Polkadot protocol, \Jam refers to a complete and coherent overall blockchain protocol.
 

From 9c9c66bac987a80ff3b472cc0ad7daa866f5891a Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 12:04:44 +0000
Subject: [PATCH 09/31] Have the segment-count in the Availability Specifier

---
 text/reporting_assurance.tex       | 5 +++--
 text/serialization.tex             | 2 +-
 text/work_packages_and_reports.tex | 3 ++-
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/text/reporting_assurance.tex b/text/reporting_assurance.tex
index f03d070..3880cc1 100644
--- a/text/reporting_assurance.tex
+++ b/text/reporting_assurance.tex
@@ -53,13 +53,14 @@ \subsubsection{Refinement Context}
 \end{equation}
 
 \subsubsection{Availability}
-We define the set of \emph{availability specifications}, $\mathbb{S}$, as the tuple of the work-package's hash $h$, an auditable work bundle length $l$ (see section \ref{sec:availabiltyspecifier} for more clarity on what this is), together with an erasure-root $u$ and a segment-root $e$. Work-results include this availability specification in order to ensure they are able to correctly reconstruct and audit the purported ramifications of any reported work-package. Formally:
+We define the set of \emph{availability specifications}, $\mathbb{S}$, as the tuple of the work-package's hash $h$, an auditable work bundle length $l$ (see section \ref{sec:availabiltyspecifier} for more clarity on what this is), together with an erasure-root $u$, a segment-root $e$ and segment-count $n$. Work-results include this availability specification in order to ensure they are able to correctly reconstruct and audit the purported ramifications of any reported work-package. Formally:
 \begin{align}
   \mathbb{S} &\equiv \tuple{
     \isa{h}{\H}\ts
     \isa{l}{\N_L}\ts
     \isa{u}{\H}\ts
-    \isa{e}{\H}
+    \isa{e}{\H}\ts
+    \isa{n}{\N}
   }
 \end{align}
 
diff --git a/text/serialization.tex b/text/serialization.tex
index 97e2e27..1e957cc 100644
--- a/text/serialization.tex
+++ b/text/serialization.tex
@@ -140,7 +140,7 @@ \subsection{Block Serialization}
   \se(\mathbf{H}) &= \se_U(\mathbf{H})\concat\se(\mathbf{H}_s) \\
   \se_U(\mathbf{H}) &= \se(\mathbf{H}_p,\mathbf{H}_r,\mathbf{H}_x)\concat\se_4(\mathbf{H}_t)\concat\se(\maybe{\mathbf{H}_e},\maybe{\mathbf{H}_w},\var{\mathbf{H}_o},\se_2(\mathbf{H}_i),\mathbf{H}_v)\\
   \se(x \in \mathbb{X}) &\equiv \se(x_a, x_s, x_b, x_l)\concat\se_4(x_t)\concat\se(\var{x_\mathbf{p}})\\
-  \se(x \in \mathbb{S}) &\equiv \se(x_h) \concat \se_4(x_l)\concat\se(x_u, x_e) \\
+  \se(x \in \mathbb{S}) &\equiv \se(x_h) \concat \se_4(x_l)\concat\se(x_u, x_e) \concat \se_2(x_n) \\
   \se(x \in \mathbb{L}) &\equiv \se_4(x_s)\concat\se(x_c, x_l)\concat\se_8(x_g)\concat\se(O(x_\mathbf{o}))\\
   \se(x \in \mathbb{W}) &\equiv \se(x_s, x_x, x_c, x_a, \var{x_\mathbf{o}}, \var{x_\mathbf{l}}, \var{x_\mathbf{r}}) \\
   \se(x \in \mathbb{P}) &\equiv \se(\var{x_\wp¬authtoken}, \se_4(x_\wp¬authcodehost), x_\wp¬authcodehash, \var{x_\wp¬authparam}, x_\wp¬context, \var{x_\wp¬workitems}) \\
diff --git a/text/work_packages_and_reports.tex b/text/work_packages_and_reports.tex
index 254ac65..5480d5e 100644
--- a/text/work_packages_and_reports.tex
+++ b/text/work_packages_and_reports.tex
@@ -249,7 +249,8 @@ \subsubsection{Availability Specifier}\label{sec:availabiltyspecifier}
       h,\,
       \is{l}{|\mathbf{b}|},\,
       u,\,
-      \is{e}{\mathcal{M}(\mathbf{s})}
+      \is{e}{\mathcal{M}(\mathbf{s})},\,
+      \is{n}{|\mathbf{s}|}
     }
   \end{aligned}\right.\!\!\!\!\!
 \end{equation}

From 889609ede103a35d2a6f49f4c5734e0cd9cea4c3 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 12:51:06 +0000
Subject: [PATCH 10/31] Extrinsic Commitment should be hash of hashes

---
 text/header.tex        | 11 +++++++----
 text/overview.tex      |  4 ++--
 text/serialization.tex | 18 +++++++++---------
 3 files changed, 18 insertions(+), 15 deletions(-)

diff --git a/text/header.tex b/text/header.tex
index 0b91839..5dad391 100644
--- a/text/header.tex
+++ b/text/header.tex
@@ -19,10 +19,13 @@ \section{The Header}\label{sec:header}
 
 We only require implementations to store headers of ancestors which were authored in the previous $\mathsf{L} = $ 24 hours of any block $\mathbf{B}$ they wish to validate.
 
-The extrinsic hash is the hash of the block's extrinsic data. Given any block $\mathbf{B} = (\mathbf{H}, \mathbf{E})$, then formally:
-\begin{equation}
-  \mathbf{H}_x \in \H \,,\quad \mathbf{H}_x \equiv \mathcal{H}(\mathcal{E}(\mathbf{E}))
-\end{equation}
+The extrinsic hash is a Merkle commitment to the block's extrinsic data, taking care to allow for the possibility of reports to individually have their inclusion proven. Given any block $\mathbf{B} = (\mathbf{H}, \mathbf{E})$, then formally:
+\begin{align}
+  \mathbf{H}_x &\in \H \ ,\quad
+  \mathbf{H}_x \equiv \mathcal{H}(\se(\mathcal{H}^\#(\mathbf{a}))) \\
+  \where \mathbf{a} &= [\se_T(\xttickets), \se_P(\xtpreimages), g, \se_A(\xtassurances), \se_D(\xtdisputes)] \\
+  \also g &= \se(\mathcal{H}^\#(\se^\#_g(\xtguarantees)))
+\end{align}
 
 A block may only be regarded as valid once the time-slot index $\mathbf{H}_t$ is in the past. It is always strictly greater than that of its parent. Formally:
 \begin{equation}
diff --git a/text/overview.tex b/text/overview.tex
index 3e7362b..9f76afa 100644
--- a/text/overview.tex
+++ b/text/overview.tex
@@ -21,10 +21,10 @@ \subsection{The Block}
 
 \begin{description}
   \item[tickets] Tickets, used for the mechanism which manages the selection of validators for the permissioning of block authoring. This component is denoted $\xttickets$.
-  \item[judgments] Votes, by validators, on dispute(s) arising between them presently taking place. This is denoted $\xtdisputes$.
   \item[preimages] Static data which is presently being requested to be available for workloads to be able to fetch on demand. This is denoted $\xtpreimages$.
-  \item[availability] Assurances by each validator concerning which of the input data of workloads they have correctly received and are storing locally. This is denoted $\xtassurances$.
   \item[reports] Reports of newly completed workloads whose accuracy is guaranteed by specific validators. This is denoted $\xtguarantees$.
+  \item[availability] Assurances by each validator concerning which of the input data of workloads they have correctly received and are storing locally. This is denoted $\xtassurances$.
+  \item[disputes] Information relating to disputes between validators over the validity of reports. This is denoted $\xtdisputes$.
 \end{description}
 
 \subsection{The State}
diff --git a/text/serialization.tex b/text/serialization.tex
index 1e957cc..5d8cdd7 100644
--- a/text/serialization.tex
+++ b/text/serialization.tex
@@ -128,15 +128,15 @@ \subsection{Block Serialization}
 
 A block $\mathbf{B}$ is serialized as a tuple of its elements in regular order, as implied in equations \ref{eq:block}, \ref{eq:extrinsic} and \ref{eq:header}. For the header, we define both the regular serialization and the unsigned serialization $\se_U$. Formally:
 \begin{align}
-  \se(\mathbf{B}) &= \se\,\left\lparen\;\begin{aligned}
-    &\mathbf{H},\ 
-    \var{\xttickets},\ 
-    \var{[(r, \se_4(a), [(v, \se_2(i), s) \mid (v, i, s) \orderedin \mathbf{j}]) \mid (r, a, \mathbf{j}) \orderedin \mathbf{v}]}, \var{\mathbf{c}}, \var{\mathbf{f}},\ \\
-    &\var{[\tup{s, \var{p}} \mid \tup{s, p} \orderedin \xtpreimages]},\ 
-    \var{[\tup{a, f, \se_2(v), s} \mid \tup{a, f, v, s} \orderedin \xtassurances]},\ \\
-    &\var{[\tup{w, \se_4(t), \var{a}} \mid \tup{w, t, a} \orderedin \xtguarantees]}
-  \end{aligned}\;\right\rparen \\
-  \nonumber &\quad \where \xtdisputes \equiv (\mathbf{v}, \mathbf{c}, \mathbf{f}) \\
+  \se(\mathbf{B}) &= \se\,\left\lparen
+    \mathbf{H},\ \se_T(\xttickets),\ \se_P(\xtpreimages),\ \se_G(\xtguarantees),\ \se_A(\xtassurances),\ \se_D(\xtdisputes)
+  \right\rparen \\
+  \se_T(\xttickets) &= \se(\var{\xttickets}) \\
+  \se_P(\xtpreimages) &= \se(\var{[\tup{s, \var{p}} \mid \tup{s, p} \orderedin \xtpreimages]}) \\
+  \se_G(\xtguarantees) &= \se(\var{\se_g^\#(\xtguarantees)}) \\
+  \se_g(\tup{w, t, a}) &= \se(\tup{w, \se_4(t), \var{a}}) \\
+  \se_A(\xtassurances) &= \se(\var{[\tup{a, f, \se_2(v), s} \mid \tup{a, f, v, s} \orderedin \xtassurances]}) \\
+  \se_D((\mathbf{v}, \mathbf{c}, \mathbf{f})) &= \se(\var{[(r, \se_4(a), [(v, \se_2(i), s) \mid (v, i, s) \orderedin \mathbf{j}]) \mid (r, a, \mathbf{j}) \orderedin \mathbf{v}]}, \var{\mathbf{c}}, \var{\mathbf{f}}) \\
   \se(\mathbf{H}) &= \se_U(\mathbf{H})\concat\se(\mathbf{H}_s) \\
   \se_U(\mathbf{H}) &= \se(\mathbf{H}_p,\mathbf{H}_r,\mathbf{H}_x)\concat\se_4(\mathbf{H}_t)\concat\se(\maybe{\mathbf{H}_e},\maybe{\mathbf{H}_w},\var{\mathbf{H}_o},\se_2(\mathbf{H}_i),\mathbf{H}_v)\\
   \se(x \in \mathbb{X}) &\equiv \se(x_a, x_s, x_b, x_l)\concat\se_4(x_t)\concat\se(\var{x_\mathbf{p}})\\

From b3287888b345faa3ac5b53937495918f68271e5d Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 13:20:47 +0000
Subject: [PATCH 11/31] Post-Accumulate Preimage Integration

---
 preamble.tex          |  5 ++++
 text/accumulation.tex | 69 ++++++++++++++++++++++++-------------------
 text/overview.tex     |  8 ++---
 3 files changed, 47 insertions(+), 35 deletions(-)

diff --git a/preamble.tex b/preamble.tex
index 3e11e8f..20c477a 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -179,6 +179,11 @@
 \newcommand*{\defxfers}{\seq{\defxfer}}
 \newcommand*{\beefycommitmap}{\mathbf{C}}
 
+\newcommand*{\accountspre}{\delta}
+\newcommand*{\accountspostacc}{\delta^\dagger}
+\newcommand*{\accountspostxfer}{\delta^\ddagger}
+\newcommand*{\accountspostpreimage}{\delta'}
+
 \newcommand*{\gascounter}{\varrho}
 \newcommand*{\registers}{\omega}
 \newcommand*{\memory}{\mu}
diff --git a/text/accumulation.tex b/text/accumulation.tex
index 06933e5..08ffa19 100644
--- a/text/accumulation.tex
+++ b/text/accumulation.tex
@@ -5,34 +5,12 @@
 
 \section{Accumulation}\label{sec:accumulation}
 
-Accumulation may be defined as some function whose arguments are $\mathbf{W}$ and $\delta$ together with selected portions of (at times partially transitioned) state and which yields the posterior service state $\delta'$ together with additional state elements $\iota'$, $\varphi'$ and $\chi'$.
+Accumulation may be defined as some function whose arguments are $\mathbf{W}$ and $\delta$ together with selected portions of (at times partially transitioned) state and which yields the posterior service state $\accountspostpreimage$ together with additional state elements $\iota'$, $\varphi'$ and $\chi'$.
 
 The proposition of accumulation is in fact quite simple: we merely wish to execute the \emph{Accumulate} logic of the service code of each of the services which has at least one work output, passing to it the work outputs and useful contextual information. However, there are three main complications. Firstly, we must define the execution environment of this logic and in particular the host functions available to it. Secondly, we must define the amount of gas to be allowed for each service's execution. Finally, we must determine the nature of transfers within Accumulate which, as we will see, leads to the need for a second entry-point, \emph{on-transfer}.
 
 
 
-\subsection{Preimage Integration}
-
-Prior to accumulation, we must first integrate all preimages provided in the lookup extrinsic. The lookup extrinsic is a sequence of pairs of service indices and data. These pairs must be ordered and without duplicates (equation \ref{eq:preimagesareordered} requires this). The data must have been solicited by a service but not yet be provided. Formally:
-\begin{align}
-  \xtpreimages &\in \lseq \ltuple\N_S\ts\Y\rtuple \rseq \\
-  \label{eq:preimagesareordered}\xtpreimages &= \orderuniqby{i}{i \in \xtpreimages} \\
-  \forall \tup{s\ts\mathbf{p}} \in \xtpreimages &: \left\{\ 
-    \begin{aligned}
-      &\keys{\delta[s]_\mathbf{p}}\ \not\ni\ \mathcal{H}(\mathbf{p})\ ,\\
-      &\delta[s]_\mathbf{l}[\tup{\mathcal{H}(\mathbf{p}), |\mathbf{p}|}]\ =\ []
-    \end{aligned}
-  \right.
-\end{align}
-
-We define $\delta^\dagger$ as the state after the integration of the preimages:
-\begin{align}
-    \delta^\dagger = \delta \text{ ex. } \forall \tup{s\ts\mathbf{p}} \in \xtpreimages : \left\{\,\begin{aligned}
-      \quad\delta^\dagger[s]_\mathbf{p}[\mathcal{H}(\mathbf{p})] &= \mathbf{p} \\
-      \delta^\dagger[s]_\mathbf{l}[\mathcal{H}(\mathbf{p}), |\mathbf{p}|] &= [\tau']
-    \end{aligned}\right.\!\!
-\end{align}
-
 
 
 
@@ -115,7 +93,7 @@ \subsection{Execution}
 
 Only once all such accumulation is executed do we integrate the results and thus define the relevant posterior state items. In doing so we also integrate the consequences of any \emph{deferred-transfers} implied by accumulation.
 
-Our formalisms begin by defining $\partialstate$ as a characterization (\ie values capable of representing) of state components which are both needed and mutable by the accumulation process. This comprises the service accounts state (as in $\delta$), the upcoming validator keys $\iota$, the queue of work-reports $\varphi$ and the privileges state $\chi$. Formally:
+Our formalisms begin by defining $\partialstate$ as a characterization (\ie values capable of representing) of state components which are both needed and mutable by the accumulation process. This comprises the service accounts state (as in $\accountspre$), the upcoming validator keys $\iota$, the queue of work-reports $\varphi$ and the privileges state $\chi$. Formally:
 \begin{equation}
   \label{eq:partialstate}
   \partialstate \equiv \left(\begin{aligned}
@@ -172,7 +150,7 @@ \subsection{Execution}
   \end{aligned}\right.
 \end{equation}
 
-We note that all newly added service indices, defined in the above context as $\bigcup_{s \in \mathbf{s}}\keys{(\Delta_1(\mathbf{o}, \mathbf{w}, s)_\mathbf{o})_\mathbf{d}} \setminus \mathbf{s}$, must not conflict with the indices of existing services $\keys{\delta}$ or other newly added services. This should never happen, since new indices are explicitly selected to avoid such conflicts, but in the unlikely event it happens, the block must be considered invalid.
+We note that all newly added service indices, defined in the above context as $\bigcup_{s \in \mathbf{s}}\keys{(\Delta_1(\mathbf{o}, \mathbf{w}, s)_\mathbf{o})_\mathbf{d}} \setminus \mathbf{s}$, must not conflict with the indices of existing services $\keys{\accountspre}$ or other newly added services. This should never happen, since new indices are explicitly selected to avoid such conflicts, but in the unlikely event it happens, the block must be considered invalid.
 
 The single-service accumulation function, $\Delta_1$, transforms an initial state-context, sequence of work-reports and a service index into an alterations state-context, a sequence of \emph{transfers}, a possible accumulation-output and the actual \textsc{pvm} gas used. This function wrangles the work-items of a particular service from a set of work-reports and invokes \textsc{pvm} execution with said data:
 \begin{align}
@@ -205,11 +183,11 @@ \subsection{Execution}
 
 \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 second intermediate state of the service-accounts $\delta^\ddagger$ and the \textsc{Beefy} commitment map $\beefycommitmap$:
+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, \delta^\dagger, \iota, \varphi), \chi_\mathbf{g}) \\
-  (\chi', \delta^\ddagger, \iota', \varphi') &\equiv \mathbf{o}
+  \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}
 \end{align}
 
 Note that the accumulation commitment map $\beefycommitmap$ is 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.
@@ -222,12 +200,12 @@ \subsection{Deferred Transfers and State Integration}
   \end{aligned}\right.
 \end{align}
 
-The posterior state $\delta'$ may then be defined as the second intermediate state with all the deferred effects of the transfers applied:
+The second intermediate state $\accountspostxfer$ may then be defined with all the deferred effects of the transfers applied:
 \begin{equation}
-  \delta' = \{ s \mapsto \Psi_T(\delta^\ddagger, s, R(\mathbf{t}, s)) \mid (s \mapsto a) \in \delta^\ddagger \}
+  \accountspostxfer = \{ s \mapsto \Psi_T(\accountspostacc, s, R(\mathbf{t}, s)) \mid (s \mapsto a) \in \accountspostacc \}
 \end{equation}
 
-Note that $\Psi_T$ is defined in appendix \ref{sec:ontransferinvocation} such that it results in $\delta^\ddagger[d]$, \ie no difference to the account's intermediate state, if $R(d) = []$, \ie said account received no transfers.
+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.
 
 We define the final state of the ready queue and the accumulated map by integrating those work-reports which were accumulated in this block and shifting any from the prior state with the oldest such items being dropped entirely:
 \begin{align}
@@ -239,3 +217,32 @@ \subsection{Deferred Transfers and State Integration}
     E(\ready^\circlearrowleft_{m - i}, \accumulated'_{\mathsf{E} - 1}) &\when i \ge \tau' - \tau
   \end{cases}
 \end{align}
+
+
+
+
+
+
+
+
+\subsection{Preimage Integration}
+
+After accumulation, we must integrate all preimages provided in the lookup extrinsic to arrive at the posterior account state. The lookup extrinsic is a sequence of pairs of service indices and data. These pairs must be ordered and without duplicates (equation \ref{eq:preimagesareordered} requires this). The data must have been solicited by a service but not yet be provided. Formally:
+\begin{align}
+  \xtpreimages &\in \lseq \ltuple\N_S\ts\Y\rtuple \rseq \\
+  \label{eq:preimagesareordered}\xtpreimages &= \orderuniqby{i}{i \in \xtpreimages} \\
+  \forall \tup{s\ts\mathbf{p}} \in \xtpreimages &: \left\{\ 
+    \begin{aligned}
+      &\keys{\delta[s]_\mathbf{p}}\ \not\ni\ \mathcal{H}(\mathbf{p})\ ,\\
+      &\delta[s]_\mathbf{l}[\tup{\mathcal{H}(\mathbf{p}), |\mathbf{p}|}]\ =\ []
+    \end{aligned}
+  \right.
+\end{align}
+
+We define $\accountspostpreimage$ as the state after the integration of the preimages:
+\begin{align}
+  \accountspostpreimage = \accountspostxfer \text{ ex. } \forall \tup{s\ts\mathbf{p}} \in \xtpreimages : \left\{\,\begin{aligned}
+      \quad\accountspostpreimage[s]_\mathbf{p}[\mathcal{H}(\mathbf{p})] &= \mathbf{p} \\
+      \accountspostpreimage[s]_\mathbf{l}[\mathcal{H}(\mathbf{p}), |\mathbf{p}|] &= [\tau']
+    \end{aligned}\right.\!\!\!\!
+\end{align}
diff --git a/text/overview.tex b/text/overview.tex
index 9f76afa..84c1406 100644
--- a/text/overview.tex
+++ b/text/overview.tex
@@ -54,17 +54,17 @@ \subsubsection{State Transition Dependency Graph}
   \kappa' &\prec (\mathbf{H}, \tau, \kappa, \gamma) \\
   \lambda' &\prec (\mathbf{H}, \tau, \lambda, \kappa) \\
   \psi' &\prec (\xtdisputes, \psi) \\
-  \delta^\dagger &\prec (\xtpreimages, \delta, \tau') \label{eq:deltadagger} \\
   \rho^\dagger &\prec (\xtdisputes, \rho) \label{eq:rhodagger} \\
   \rho^\ddagger &\prec (\xtassurances, \rho^\dagger) \label{eq:rhoddagger} \\
   \rho' &\prec (\xtguarantees, \rho^\ddagger, \kappa, \tau') \\
   \mathbf{W}^* &\prec (\xtassurances, \rho') \\
-  (\ready', \accumulated', \delta', \chi', \iota', \varphi', \beefycommitmap) &\prec (\mathbf{W}^*, \ready, \accumulated, \delta^\dagger, \chi, \iota, \varphi) \\
+  (\ready', \accumulated', \accountspostxfer, \chi', \iota', \varphi', \beefycommitmap) &\prec (\mathbf{W}^*, \ready, \accumulated, \accountspre, \chi, \iota, \varphi) \\
+  \accountspostpreimage &\prec (\xtpreimages, \accountspostxfer, \tau') \label{eq:accountspostpreimage} \\
   \alpha' &\prec (\mathbf{H}, \xtguarantees, \varphi', \alpha) \\
-  \pi' &\prec (\xtguarantees, \xtpreimages, \xtassurances, \xttickets, \tau, \kappa', \pi, \mathbf{H})\!\!\!\!
+  \pi' &\prec (\xtguarantees, \xtpreimages, \xtassurances, \xttickets, \tau, \kappa', \pi, \mathbf{H})\!\!\!\!\!\!\!\!
 \end{align}
 
-The only synchronous entanglements are visible through the intermediate components superscripted with a dagger and defined in equations \ref{eq:betadagger}, \ref{eq:deltadagger} and \ref{eq:rhoddagger}. The latter two mark a merge and join in the dependency graph and, concretely, imply that the preimage lookup extrinsic must be folded into state before the availability extrinsic may be fully processed and accumulation of work happen.
+The only synchronous entanglements are visible through the intermediate components superscripted with a dagger and defined in equations \ref{eq:betadagger}, \ref{eq:accountspostpreimage} and \ref{eq:rhoddagger}. The latter two mark a merge and join in the dependency graph and, concretely, imply that the preimage lookup extrinsic must be folded into state before the availability extrinsic may be fully processed and accumulation of work happen.
 
 \subsection{Which History?}
 

From 8a3c0e87b7eda8b5ac98d24203d399e2a300edff Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 13:35:47 +0000
Subject: [PATCH 12/31] Availability may apply only to timely reports

---
 text/reporting_assurance.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/text/reporting_assurance.tex b/text/reporting_assurance.tex
index 3880cc1..702ddad 100644
--- a/text/reporting_assurance.tex
+++ b/text/reporting_assurance.tex
@@ -117,9 +117,10 @@ \subsubsection{The Assurances Extrinsic}
   &\mathsf{X}_A \equiv \token{\$jam\_available}
 \end{align}
 
-A bit may only be set if the corresponding core has a report pending availability on it:
+A bit may only be set if the corresponding core has a report pending availability on it which has not timed out:
 \begin{align}
-  \forall a \in \xtassurances : \forall c \in \N_\mathsf{C} : a_f[c] \implies \rho^\dagger[c] \ne \none
+  &\forall a \in \xtassurances, c \in \N_\mathsf{C} :\\
+  &\quad a_f[c] \Rightarrow \rho^\dagger[c] \ne \none \wedge \mathbf{H}_t \le \rho^\dagger[c]_t + \mathsf{U}
 \end{align}
 
 \subsubsection{Available Reports}

From 9f69cee0d6fdaa0fadb780cf82a11dba77d248ea Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 13:55:40 +0000
Subject: [PATCH 13/31] PVM memory retains accessibility only in discrete
 pages.

---
 text/definitions.tex     |  3 ++-
 text/overview.tex        | 14 +++++++++-----
 text/pvm.tex             |  8 ++++----
 text/pvm_invocations.tex |  2 +-
 4 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/text/definitions.tex b/text/definitions.tex
index 6d692e6..7599cbe 100644
--- a/text/definitions.tex
+++ b/text/definitions.tex
@@ -287,7 +287,8 @@ \subsubsection{Constants}
   \item[$\mathsf{Y} = 500$] The number of slots into an epoch at which ticket-submission ends.
   \item[$\mathsf{Z}_A = 2$] The \textsc{pvm} dynamic address alignment factor. See equation \ref{eq:jumptablealignment}.
   \item[$\mathsf{Z}_I = 2^{24}$] The standard \textsc{pvm} program initialization input data size. See equation \ref{sec:standardprograminit}.
-  \item[$\mathsf{Z}_P = 2^{14}$] The standard \textsc{pvm} program initialization page size. See section \ref{sec:standardprograminit}.
+  \item[$\mathsf{Z}_G = 2^{14}$] The standard \textsc{pvm} program initialization page size. See section \ref{sec:standardprograminit}.
+  \item[$\mathsf{Z}_P = 2^{12}$] The \textsc{pvm} memory page size. See equation \ref{eq:pvmmemory}.
   \item[$\mathsf{Z}_Q = 2^{16}$] The standard \textsc{pvm} program initialization segment size. See section \ref{sec:standardprograminit}.
 \end{description}
 
diff --git a/text/overview.tex b/text/overview.tex
index 84c1406..f4c2584 100644
--- a/text/overview.tex
+++ b/text/overview.tex
@@ -172,14 +172,18 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
 It is left as a rather important implementation detail to ensure that the amount of time taken while computing the function $\Psi(\dots, \gascounter, \dots)$ has a maximum computation time approximately proportional to the value of $\gascounter$ regardless of other operands.
 
 The \textsc{pvm} is a very simple \textsc{risc} \emph{register machine} and as such has 13 registers, each of which is a 32-bit quantity, denoted as $\N_R$, a natural less than $2^{32}$.\footnote{This is three fewer than \textsc{risc-v}'s 16, however the amount that program code output by compilers uses is 13 since two are reserved for operating system use and the third is fixed as zero} Within the context of the \textsc{pvm}, $\registers \in \seq{\N_R}_{13}$ is typically used to denote the registers.
-\begin{align}
-  \mathbb{M} &\equiv \ltuple\isa{\mathbf{V}}{\Y_{2^{32}}}\ts\isa{\mathbf{A}}{\lseq\{\text{W}, \text{R}, \none\}\rseq_{2^{32}}}\rtuple
+\begin{align}\label{eq:pvmmemory}
+  \mathbb{M} &\equiv \tuple{
+    \isa{\mathbf{V}}{\Y_{2^{32}}},
+    \isa{\mathbf{A}}{\seq{\{\text{W}, \text{R}, \none\}}_p}
+  }\,,\ p = \frac{2^{32}}{\mathsf{Z}_P}\\
+  \mathsf{Z}_P &= 2^{12}
 \end{align}
 
-The \textsc{pvm} assumes a simple pageable \textsc{ram} of 32-bit addressable octets where each octet may be either immutable, mutable or inaccessible. The \textsc{ram} definition $\mathbb{M}$ includes two components: a value $\mathbf{V}$ and access $\mathbf{A}$. If the component is unspecified while being subscripted then the value component may be assumed. Within the context of the virtual machine, $\memory \in \mathbb{M}$ is typically used to denote \textsc{ram}.
+The \textsc{pvm} assumes a simple pageable \textsc{ram} of 32-bit addressable octets situated in pages of $2^p = 4096$ octets where each page may be either immutable, mutable or inaccessible. The \textsc{ram} definition $\mathbb{M}$ includes two components: a value $\mathbf{V}$ and access $\mathbf{A}$. If the component is unspecified while being subscripted then the value component may be assumed. Within the context of the virtual machine, $\memory \in \mathbb{M}$ is typically used to denote \textsc{ram}.
 \begin{align}
-  \mathbb{V}_{\memory} \equiv \{i \mid \memory_\mathbf{A}[i] \ne \none \} \qquad
-  \mathbb{V}^*_{\memory} \equiv \{i \mid \memory_\mathbf{A}[i] = \text{W} \}
+  \mathbb{V}_{\memory} &\equiv \{i \mid \memory_\mathbf{A}[\floor{\nicefrac{i}{\mathsf{Z}_P}}] \ne \none \} \\
+  \mathbb{V}^*_{\memory} &\equiv \{i \mid \memory_\mathbf{A}[\floor{\nicefrac{i}{\mathsf{Z}_P}}] = \text{W} \}
 \end{align}
 
 We define two sets of indices for the \textsc{ram} $\memory$: $\mathbb{V}_{\memory}$ is the set of indices which may be read from; and $\mathbb{V}^*_{\memory}$ is the set of indices which may be written to.
diff --git a/text/pvm.tex b/text/pvm.tex
index c32f1da..b995bc8 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -637,9 +637,9 @@ \subsection{Standard Program Initialization}\label{sec:standardprograminit}
 With conditions:
 \begin{align}\label{eq:conditions}
   &\using \mathcal{E}_3(|\mathbf{o}|) \concat \mathcal{E}_3(|\mathbf{w}|) \concat \mathcal{E}_2(z) \concat \mathcal{E}_3(s) \concat \mathbf{o} \concat \mathbf{w} \concat \mathcal{E}_4(|\mathbf{c}|) \concat \mathbf{c} = \mathbf{p}\\
-  &\mathsf{Z}_P = 2^{14}\ ,\quad\mathsf{Z}_Q = 2^{16}\ ,\quad\mathsf{Z}_I = 2^{24}\\
-  &\using \rnp{x \in \N} \equiv \mathsf{Z}_P\left\lceil \frac{x}{\mathsf{Z}_P} \right\rceil\quad,\qquad\rnq{x \in \N} \equiv \mathsf{Z}_Q\left\lceil \frac{x}{\mathsf{Z}_Q} \right\rceil\\
-  &5\mathsf{Z}_Q + Q(|\mathbf{o}|) + Q(|\mathbf{w}| + z\mathsf{Z}_P) + Q(s) + \mathsf{Z}_I \leq 2^{32}
+  &\mathsf{Z}_G = 2^{14}\ ,\quad\mathsf{Z}_Q = 2^{16}\ ,\quad\mathsf{Z}_I = 2^{24}\\
+  &\using \rnp{x \in \N} \equiv \mathsf{Z}_G\left\lceil \frac{x}{\mathsf{Z}_G} \right\rceil\quad,\qquad\rnq{x \in \N} \equiv \mathsf{Z}_Q\left\lceil \frac{x}{\mathsf{Z}_Q} \right\rceil\\
+  &5\mathsf{Z}_Q + Q(|\mathbf{o}|) + Q(|\mathbf{w}| + z\mathsf{Z}_G) + Q(s) + \mathsf{Z}_I \leq 2^{32}
 \end{align}
 Thus, if the above conditions cannot be satisfied with unique values, then the result is $\none$, otherwise it is a tuple of $\mathbf{c}$ as above and $\mem$, $\registers$ such that:
 \begin{equation}\label{eq:memlayout}
@@ -659,7 +659,7 @@ \subsection{Standard Program Initialization}\label{sec:standardprograminit}
     &(0, W) &&\ \when
         2\mathsf{Z}_Q + \rnq{|\mathbf{o}|} + |\mathbf{w}|
             &\ \leq i < \ &&
-                2\mathsf{Z}_Q + \rnq{|\mathbf{o}|} + \rnp{|\mathbf{w}|} + z\mathsf{Z}_P\\
+                2\mathsf{Z}_Q + \rnq{|\mathbf{o}|} + \rnp{|\mathbf{w}|} + z\mathsf{Z}_G\\
     &(0, W) &&\ \when
         2^{32} - 2\mathsf{Z}_Q - \mathsf{Z}_I - \rnp{s}
             &\ \leq i < \ &&
diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 3f75796..19ff02d 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -743,7 +743,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \end{cases}\\
     \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
       (\mathbf{u}'_\mathbf{V})_{b\dots+l} = \mathbf{s} \\
-      (\mathbf{u}'_\mathbf{A})_{b\dots+l} = [\mathrm{W}, \mathrm{W}, ...]
+      (\mathbf{u}'_\mathbf{A})_{\floor{\nicefrac{b}{\mathsf{Z}_P}}\dots\floor{\nicefrac{b+l-1}{\mathsf{Z}_P}} + 1} = [\mathrm{W}, \mathrm{W}, ...]
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
       (\mathtt{OOB}, \mathbf{m}) &\when \mathbf{s} = \error \\

From 21e264d72c2f353892fe69adc54eeb98f05611b7 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 14:10:18 +0000
Subject: [PATCH 14/31] Introduce zero-memory and void-memory hostcalls

---
 text/definitions.tex     |  8 +++---
 text/pvm_invocations.tex | 55 ++++++++++++++++++++++++++++++++++------
 2 files changed, 52 insertions(+), 11 deletions(-)

diff --git a/text/definitions.tex b/text/definitions.tex
index 7599cbe..c42a2ea 100644
--- a/text/definitions.tex
+++ b/text/definitions.tex
@@ -96,9 +96,10 @@ \subsection{Functions}
   \item[$\Omega$] Virtual machine host-call functions. See appendix \ref{sec:virtualmachineinvocations}. %	Ω
   \begin{description}
     \item[$\Omega_A$] Assign-core host-call.
+    \item[$\Omega_B$] Empower-service host-call.
     \item[$\Omega_C$] Checkpoint host-call.
     \item[$\Omega_D$] Designate-validators host-call.
-    \item[$\Omega_E$] Empower-service host-call.
+    \item[$\Omega_E$] Export segment host-call.
     \item[$\Omega_F$] Forget-preimage host-call.
     \item[$\Omega_G$] Gas-remaining host-call.
     \item[$\Omega_H$] Historical-lookup-preimage host-call.
@@ -114,10 +115,11 @@ \subsection{Functions}
     \item[$\Omega_R$] Read-storage host-call.
     \item[$\Omega_T$] Transfer host-call.
     \item[$\Omega_U$] Upgrade-service host-call.
+    \item[$\Omega_V$] Void inner-\textsc{pvm} memory host-call.
     \item[$\Omega_W$] Write-storage host-call.
     \item[$\Omega_X$] Expunge-\textsc{pvm} host-call.
     \item[$\Omega_Y$] Import segment host-call.
-    \item[$\Omega_Z$] Export segment host-call.
+    \item[$\Omega_Z$] Zero inner-\textsc{pvm} memory host-call.
   \end{description}
 \end{description}
 
@@ -224,7 +226,7 @@ \subsubsection{State components}
   \end{description}
   \item[$\chi$] The privileged service indices. %	χ
   \begin{description}
-    \item[$\chi_m$] The index of the empower service.
+    \item[$\chi_m$] The index of the blessed service.
     \item[$\chi_v$] The index of the designate service.
     \item[$\chi_a$] The index of the assign service.
     \item[$\chi_\mathbf{g}$] The always-accumulate service indices and their basic gas allowance.
diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 19ff02d..0149f33 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -89,7 +89,7 @@ \subsection{Refine Invocation}\label{sec:refineinvocation}
     (n, \gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\mapsto \begin{cases}
       \Omega_H(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}), s, \delta, \mathbf{c}_t) &\when n = \mathtt{historical\_lookup}\\
       \Omega_Y(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}), \mathbf{i}) &\when n = \mathtt{import}\\
-      \Omega_Z(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}), \segoff) &\when n = \mathtt{export}\\
+      \Omega_E(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}), \segoff) &\when n = \mathtt{export}\\
       \Omega_G(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{gas}\\
       \Omega_M(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{machine}\\
       \Omega_P(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{peek}\\
@@ -152,7 +152,7 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
     G(\Omega_L(\gascounter, \registers, \memory, \mathbf{s}, \mathbf{x}_s, \mathbf{d}), (\mathbf{x}, \mathbf{y})) &\when n = \mathtt{lookup} \\
     \Omega_G(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y})) &\when n = \mathtt{gas} \\
     \Omega_I(\gascounter, \registers, \memory, \mathbf{x}_s, \mathbf{d}, (\mathbf{x}, \mathbf{y})) &\when n = \mathtt{info} \\
-    \Omega_E(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y})) &\when n = \mathtt{empower}\\
+    \Omega_B(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y})) &\when n = \mathtt{bless}\\
     \Omega_A(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y})) &\when n = \mathtt{assign}\\
     \Omega_D(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y})) &\when n = \mathtt{designate}\\
     \Omega_C(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y})) &\when n = \mathtt{checkpoint} \\
@@ -403,8 +403,8 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \endhead
   \makecell*[l]{
-  $\Omega_E(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y}))$ \\
-  \texttt{empower} = 5 \\
+  $\Omega_B(\gascounter, \registers, \memory, (\mathbf{x}, \mathbf{y}))$ \\
+  \texttt{bless} = 5 \\
   $g = 10$}&
   $\begin{aligned}
     \using [m, a, v, o, n] &= \registers_{7 \dots 12} \\
@@ -674,7 +674,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_Z(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}), \segoff)$ \\
+  $\Omega_E(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}), \segoff)$ \\
   \texttt{export} = 17 \\
   $g = 10$} &
   $\begin{aligned}
@@ -728,8 +728,28 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
+  $\Omega_Z(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
+  \texttt{zero} = 20 \\
+  $g = 10$} &
+  $\begin{aligned}
+    \using [n, b, l] &= \registers_{7 \dots 10} \\
+    \using \mathbf{u} &= \begin{cases}
+      \mathbf{m}[n]_\mathbf{u} &\when n \in \keys{\mathbf{m}} \\
+      \error &\otherwise\\
+    \end{cases} \\
+    \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
+      (\mathbf{u}'_\mathbf{V})_{b\dots+l} = [0, 0, \dots] \\
+      (\mathbf{u}'_\mathbf{A})_{\floor{\nicefrac{b}{\mathsf{Z}_P}}\dots\floor{\nicefrac{b+l-1}{\mathsf{Z}_P}} + 1} = [\mathrm{W}, \mathrm{W}, \dots]
+    \end{cases}\\
+    (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
+      (\mathtt{WHO}, \mathbf{m}) &\otherwhen \mathbf{u} = \error \\
+      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}' &\otherwise \\
+    \end{cases} \\
+  \end{aligned}$\\
+  \cmidrule(lr){1-1}\cmidrule(lr){2-2}
+  \makecell*[l]{
   $\Omega_O(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
-  \texttt{poke} = 20 \\
+  \texttt{poke} = 21 \\
   $g = 10$} &
   $\begin{aligned}
     \using [n, a, b, l] &= \registers_{7 \dots 11} \\
@@ -753,8 +773,27 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
+  $\Omega_V(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
+  \texttt{void} = 22 \\
+  $g = 10$} &
+  $\begin{aligned}
+    \using [n, b, l] &= \registers_{7 \dots 10} \\
+    \using \mathbf{u} &= \begin{cases}
+      \mathbf{m}[n]_\mathbf{u} &\when n \in \keys{\mathbf{m}} \\
+      \error &\otherwise\\
+    \end{cases} \\
+    \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
+      (\mathbf{u}'_\mathbf{A})_{\floor{\nicefrac{b}{\mathsf{Z}_P}}\dots\floor{\nicefrac{b+l-1}{\mathsf{Z}_P}} + 1} = [\none, \none, \dots]
+    \end{cases}\\
+    (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
+      (\mathtt{WHO}, \mathbf{m}) &\otherwhen \mathbf{u} = \error \\
+      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}' &\otherwise \\
+    \end{cases} \\
+  \end{aligned}$\\
+  \cmidrule(lr){1-1}\cmidrule(lr){2-2}
+  \makecell*[l]{
   $\Omega_K(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
-  \texttt{invoke} = 21 \\
+  \texttt{invoke} = 23 \\
   $g = 10$} &
   $\begin{aligned}
     \using [n, o] &= \registers_{7, 8} \\
@@ -784,7 +823,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
   $\Omega_X(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
-  \texttt{expunge} = 22 \\
+  \texttt{expunge} = 24 \\
   $g = 10$} &
   $\begin{aligned}
     \using n &= \registers_7 \\

From e99944e1d950d33fc617086783a11781c9f2757d Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Fri, 8 Nov 2024 14:11:06 +0000
Subject: [PATCH 15/31] Enable zero & void hostcalls

---
 text/pvm_invocations.tex | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 0149f33..bce5317 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -93,7 +93,9 @@ \subsection{Refine Invocation}\label{sec:refineinvocation}
       \Omega_G(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{gas}\\
       \Omega_M(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{machine}\\
       \Omega_P(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{peek}\\
+      \Omega_Z(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{zero}\\
       \Omega_O(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{poke}\\
+      \Omega_V(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{void}\\
       \Omega_K(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{invoke}\\
       \Omega_X(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e})) &\when n = \mathtt{expunge}\\
       (\gascounter - 10, [\registers_0, \dots, \registers_6, \mathtt{WHAT}, \registers_8, \dots], \memory) &\otherwise

From 5c5d9227837a6a1fb85def9935e72ec5d2dab31b Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 12 Nov 2024 14:40:00 +0700
Subject: [PATCH 16/31] Preamble

---
 preamble.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/preamble.tex b/preamble.tex
index 20c477a..9b0d96d 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -203,7 +203,7 @@
 }
 \input{context.tex}
 
-\title[JAM: Join-Accumulate Machine \\ {\smaller \textbf{Draft \jamdraftversionstring\ -\ \today}}]{Join-Accumulate Machine: A Semi-Coherent Scalable Trustless VM \\ {\smaller Draft \jamdraftversionstring\ -\ \today}}
+\title[JAM: Join-Accumulate Machine \\ {\smaller \textbf{Draft \jamdraftversionstring\ -\ \today}}]{Join-Accumulate Machine: A Mostly-Coherent Trustless Supercomputer \\ {\smaller Draft \jamdraftversionstring\ -\ \today}}
 \author{
   Dr. Gavin Wood\\
   Founder, Polkadot \& Ethereum\\%, Parity, Web3 Foundation, Fellowship\\

From 7c3b8ee5134431e271119961062ce3ca1e98df27 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 12 Nov 2024 08:53:02 +0000
Subject: [PATCH 17/31] Preimages made recently invalid don't invalidate the
 block

---
 text/accumulation.tex | 27 ++++++++++++++++-----------
 text/overview.tex     |  2 +-
 2 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/text/accumulation.tex b/text/accumulation.tex
index 08ffa19..b246960 100644
--- a/text/accumulation.tex
+++ b/text/accumulation.tex
@@ -154,8 +154,10 @@ \subsection{Execution}
 
 The single-service accumulation function, $\Delta_1$, transforms an initial state-context, sequence of work-reports and a service index into an alterations state-context, a sequence of \emph{transfers}, a possible accumulation-output and the actual \textsc{pvm} gas used. This function wrangles the work-items of a particular service from a set of work-reports and invokes \textsc{pvm} execution with said data:
 \begin{align}
-  &\mathbb{O} \equiv \tuple{\isa{o}{\Y \cup \mathbb{J}}, \isa{l}{\H}, \isa{k}{\H}, \isa{a}{\Y}} \\
-  &\Delta_1 \colon \left\{\;\begin{aligned}
+  &\mathbb{O} \equiv \tuple{\isa{o}{\Y \cup \mathbb{J}}, \isa{l}{\H}, \isa{k}{\H}, \isa{a}{\Y}}
+\end{align}
+\begin{align}
+    &\Delta_1 \colon \left\{\;\begin{aligned}
     &\begin{aligned}
       (\partialstate, \seq{\mathbb{W}}, \dict{\N_S}{\N_G}, \N_S) &\to \tuple{
         \begin{aligned}
@@ -227,21 +229,24 @@ \subsection{Deferred Transfers and State Integration}
 
 \subsection{Preimage Integration}
 
-After accumulation, we must integrate all preimages provided in the lookup extrinsic to arrive at the posterior account state. The lookup extrinsic is a sequence of pairs of service indices and data. These pairs must be ordered and without duplicates (equation \ref{eq:preimagesareordered} requires this). The data must have been solicited by a service but not yet be provided. Formally:
+After accumulation, we must integrate all preimages provided in the lookup extrinsic to arrive at the posterior account state. The lookup extrinsic is a sequence of pairs of service indices and data. These pairs must be ordered and without duplicates (equation \ref{eq:preimagesareordered} requires this). The data must have been solicited by a service but not yet provided in the \emph{prior} state. Formally:
 \begin{align}
   \xtpreimages &\in \lseq \ltuple\N_S\ts\Y\rtuple \rseq \\
   \label{eq:preimagesareordered}\xtpreimages &= \orderuniqby{i}{i \in \xtpreimages} \\
-  \forall \tup{s\ts\mathbf{p}} \in \xtpreimages &: \left\{\ 
-    \begin{aligned}
-      &\keys{\delta[s]_\mathbf{p}}\ \not\ni\ \mathcal{H}(\mathbf{p})\ ,\\
-      &\delta[s]_\mathbf{l}[\tup{\mathcal{H}(\mathbf{p}), |\mathbf{p}|}]\ =\ []
-    \end{aligned}
-  \right.
+  R(\mathbf{d}, s, h, l) &\equiv
+  h \not\in \mathbf{d}[s]_\mathbf{p} \wedge
+    \mathbf{d}[s]_\mathbf{l}[\tup{h, l}] = []\\
+  \forall \tup{s, \mathbf{p}} &\in \xtpreimages : R(\accountspre, s, \mathcal{H}(\mathbf{p}), |\mathbf{p}|)
 \end{align}
 
-We define $\accountspostpreimage$ as the state after the integration of the preimages:
+We disregard, without prejudice, any preimages which due to the effects of accumulation are no longer useful. We define $\accountspostpreimage$ as the state after the integration of the still-relevant preimages:
 \begin{align}
-  \accountspostpreimage = \accountspostxfer \text{ ex. } \forall \tup{s\ts\mathbf{p}} \in \xtpreimages : \left\{\,\begin{aligned}
+  \using \mathbf{P} = \{
+    (s, \mathbf{p})
+    \mid
+      \tup{s, \mathbf{p}} \in \xtpreimages, R(\accountspostxfer, s, \mathcal{H}(\mathbf{p}), |\mathbf{p}|)
+    \}\\
+  \accountspostpreimage = \accountspostxfer \text{ ex. } \forall \tup{s\ts\mathbf{p}} \in \mathbf{P} : \left\{\,\begin{aligned}
       \quad\accountspostpreimage[s]_\mathbf{p}[\mathcal{H}(\mathbf{p})] &= \mathbf{p} \\
       \accountspostpreimage[s]_\mathbf{l}[\mathcal{H}(\mathbf{p}), |\mathbf{p}|] &= [\tau']
     \end{aligned}\right.\!\!\!\!
diff --git a/text/overview.tex b/text/overview.tex
index f4c2584..5d88949 100644
--- a/text/overview.tex
+++ b/text/overview.tex
@@ -64,7 +64,7 @@ \subsubsection{State Transition Dependency Graph}
   \pi' &\prec (\xtguarantees, \xtpreimages, \xtassurances, \xttickets, \tau, \kappa', \pi, \mathbf{H})\!\!\!\!\!\!\!\!
 \end{align}
 
-The only synchronous entanglements are visible through the intermediate components superscripted with a dagger and defined in equations \ref{eq:betadagger}, \ref{eq:accountspostpreimage} and \ref{eq:rhoddagger}. The latter two mark a merge and join in the dependency graph and, concretely, imply that the preimage lookup extrinsic must be folded into state before the availability extrinsic may be fully processed and accumulation of work happen.
+The only synchronous entanglements are visible through the intermediate components superscripted with a dagger and defined in equations \ref{eq:betadagger}, \ref{eq:accountspostpreimage} and \ref{eq:rhoddagger}. The latter two mark a merge and join in the dependency graph and, concretely, imply that the availability extrinsic may be fully processed and accumulation of work happen before the preimage lookup extrinsic is folded into state.
 
 \subsection{Which History?}
 

From 86569be7a31aae9853f58ab3cc7e9af9528761cd Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 12 Nov 2024 08:55:10 +0000
Subject: [PATCH 18/31] voiding inner PVM RAM should zero it

---
 text/pvm_invocations.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index bce5317..6f73f2f 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -785,6 +785,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
       \error &\otherwise\\
     \end{cases} \\
     \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
+      (\mathbf{u}'_\mathbf{V})_{b\dots+l} = [0, 0, \dots] \\
       (\mathbf{u}'_\mathbf{A})_{\floor{\nicefrac{b}{\mathsf{Z}_P}}\dots\floor{\nicefrac{b+l-1}{\mathsf{Z}_P}} + 1} = [\none, \none, \dots]
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}

From 60cef5b31cf48e80d00af3699915114db338a1bb Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 12 Nov 2024 11:25:07 +0000
Subject: [PATCH 19/31] Reframe size-synchrony antagonism for size-coherency

---
 text/intro.tex | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/text/intro.tex b/text/intro.tex
index 3934b96..5116465 100644
--- a/text/intro.tex
+++ b/text/intro.tex
@@ -27,19 +27,20 @@ \subsection{Driving Factors}
 
 As a declared Web3 technology, we make an implicit assumption of the first two items. Interestingly, items \ref{enum:performance} and \ref{enum:coherency} are antagonistic according to an information theoretic principle which we are sure must already exist in some form but are nonetheless unaware of a name for it. For argument's sake we shall name it \emph{size-synchrony antagonism}.
 
-\subsection{Scaling under Size-Synchrony Antagonism}
+\subsection{Scaling under Size-Coherency Antagonism}
 
-Size-synchrony antagonism is a simple principle implying that as the state-space of information systems grow, then the system necessarily becomes less synchronous. The argument goes:
+Size-coherency antagonism is a simple principle implying that as the state-space of information systems grow, then the system necessarily becomes less coherent. It is a direct implication of of principle that causality is limited by speed. The maximum speed allowed by physics is $C$ the speed of light in a vacuum, however other information systems may have lower bounds: In biological system this is largely determined by various chemical processes whereas in electronic systems is it determined by the speed of electrons in various substances. Distributed software systems will tend to have much lower bounds still, being dependent on a substrate of software, hardware and packet-switched networks of varying reliability.
 
+The argument goes:
 \begin{enumerate}
   \item The more state a system utilizes for its data-processing, the greater the amount of space this state must occupy.
   \item The more space used, then the greater the mean and variance of distances between state-components.
-  \item As the mean and variance increase, then interactions become slower and subsystems must manage the possibility that distances between interdependent components of state could be materially different, requiring asynchrony.
+  \item As the mean and variance increase, then time for causal resolution (i.e. all correct implications of an event to be felt) becomes divergent across the system, causing incoherence.
 \end{enumerate}
 
-This assumes perfect coherency of the system's state. Setting the question of overall security aside for a moment, we can avoid this rule by applying the \emph{divide and conquer} maxim and fragmenting the state of a system, sacrificing its coherency. We might for example create two independent smaller-state systems rather than one large-state system. This pattern applies a step-curve to the principle; intra-system processing has low size and high synchrony, inter-system processing has high size but low synchrony. It is the principle behind meta-networks such as Polkadot, Cosmos and the predominant vision of a scaled Ethereum (all to be discussed in depth shortly).
+Setting the question of overall security aside for a moment, we can manage incoherence by fragmenting the system into causally-independent subsystems, each of which is small enough to be coherent. In a resource-rich environment, a bacterium may split into two rather than growing to double its size. This pattern is rather a crude means of dealing with incoherency under growth: intra-system processing has low size and high synchrony, inter-system processing supports higher overall sizes but with only low synchrony. It is the principle behind meta-networks such as Polkadot, Cosmos and the predominant vision of a scaled Ethereum (all to be discussed in depth shortly).
 
-The present work explores a middle-ground in the antagonism, avoiding the persistent fragmentation of state-space of the system as with existing approaches. We do this by introducing a new model of computation which pipelines a highly scalable element to a highly synchronous element. Asynchrony is not avoided, but we do open the possibility for a greater degree of granularity over how it is traded against size. In particular fragmentation can be made ephemeral rather than persistent, drawing upon a coherent state and fragmenting it only for as long as it takes to execute any given piece of processing on it.
+The present work explores a middle-ground in the antagonism, avoiding the persistent fragmentation of state-space of the system as with existing approaches. We do this by introducing a new model of computation which pipelines a highly scalable element to a highly synchronous element while retaining a storage facility which is \emph{mostly coherent}. Asynchrony is not avoided, but we do open the possibility for a greater degree of granularity over how it is traded against size. In particular fragmentation can be made ephemeral rather than persistent, drawing upon a coherent state and fragmenting it only for as long as it takes to execute any given piece of processing on it.
 
 Unlike with \textsc{snark}-based L2-blockchain techniques for scaling, this model draws upon crypto-economic mechanisms and inherits their low-cost and high-performance profiles and averts a bias toward centralization.
 

From 89ac1c84a9b778f135e49b82a160c368325ec72c Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 12 Nov 2024 14:38:00 +0000
Subject: [PATCH 20/31] Update memory layout in terms of accessibility (now
 indexed by page)

---
 text/pvm.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/text/pvm.tex b/text/pvm.tex
index b995bc8..16d9434 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -643,7 +643,7 @@ \subsection{Standard Program Initialization}\label{sec:standardprograminit}
 \end{align}
 Thus, if the above conditions cannot be satisfied with unique values, then the result is $\none$, otherwise it is a tuple of $\mathbf{c}$ as above and $\mem$, $\registers$ such that:
 \begin{equation}\label{eq:memlayout}
-  \forall i \in \N_R : \mem_i = \left\{\begin{alignedat}{5}
+  \forall i \in \N_R : ((\mem_\mathbf{V})_i, (\mem_\mathbf{A})_{\floor{\nicefrac{i}{\mathsf{Z}_P}}}) = \left\{\begin{alignedat}{5}
     &\tup{\is{\mathbf{V}}{\mathbf{o}_{i - \mathsf{Z}_Q}}\ts\is{\mathbf{A}}{R}} &&\ \when
         \mathsf{Z}_Q
             &\ \leq i < \ &&

From 080c768d6bf2de499d2ecfca511848467d086d63 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 12 Nov 2024 15:13:31 +0000
Subject: [PATCH 21/31] Rewire the zero/void hostcalls

---
 text/pvm_invocations.tex | 51 +++++++++++++++++-----------------------
 1 file changed, 22 insertions(+), 29 deletions(-)

diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 6f73f2f..941a726 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -716,59 +716,52 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \texttt{peek} = 19 \\
   $g = 10$} &
   $\begin{aligned}
-    \using [n, a, b, l] &= \registers_{7 \dots 11} \\
+    \using [n, o, s, l] &= \registers_{7 \dots 11} \\
     \using \mathbf{s} &= \begin{cases}
       \none &\when n \not\in \keys{\mathbf{m}}\\
-      \error &\when \N_{b\dots+l} \not\in \mathbb{V}_{\mathbf{m}[n]_\mathbf{u}} \\
-      \mathbf{m}[n]_{\mathbf{u}_{b\dots+l}} &\otherwise
+      \mathbf{m}[n]_{\mathbf{u}_{s\dots+l}} &\when \N_{s\dots+l} \in \mathbb{V}_{\mathbf{m}[n]_\mathbf{u}} \wedge \N_{o\dots+l} \in \mathbb{V}^*_\lambda \\
+      \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mem') &\equiv \begin{cases}
       (\mathtt{OOB}, \mem) &\when \mathbf{s} = \error \\
       (\mathtt{WHO}, \mem) &\when \mathbf{s} = \none \\
-      (\mathtt{OK}, \mem') \ \where \mem' = \mem \exc \mem'_{a\dots+l} = \mathbf{s} &\otherwise
+      (\mathtt{OK}, \mem') \ \where \mem' = \mem \exc \mem'_{o\dots+l} = \mathbf{s} &\otherwise
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_Z(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
-  \texttt{zero} = 20 \\
+  $\Omega_O(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
+  \texttt{poke} = 20 \\
   $g = 10$} &
   $\begin{aligned}
-    \using [n, b, l] &= \registers_{7 \dots 10} \\
-    \using \mathbf{u} &= \begin{cases}
-      \mathbf{m}[n]_\mathbf{u} &\when n \in \keys{\mathbf{m}} \\
-      \error &\otherwise\\
-    \end{cases} \\
-    \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
-      (\mathbf{u}'_\mathbf{V})_{b\dots+l} = [0, 0, \dots] \\
-      (\mathbf{u}'_\mathbf{A})_{\floor{\nicefrac{b}{\mathsf{Z}_P}}\dots\floor{\nicefrac{b+l-1}{\mathsf{Z}_P}} + 1} = [\mathrm{W}, \mathrm{W}, \dots]
+    \using [n, s, o, l] &= \registers_{7 \dots 11} \\
+    \using \mathbf{s} &= \begin{cases}
+      \none &\when n \not\in \keys{\mathbf{m}} \\
+      \mem_{s\dots+l} &\when \N_{s\dots+l} \in \mathbb{V}_\mathbf{u} \wedge \N_{o\dots+l} \in \mathbb{V}^*_\memory \\
+      \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
-      (\mathtt{WHO}, \mathbf{m}) &\otherwhen \mathbf{u} = \error \\
-      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}' &\otherwise \\
+      (\mathtt{OOB}, \mathbf{m}) &\when \mathbf{s} = \error \\
+      (\mathtt{WHO}, \mathbf{m}) &\when \mathbf{s} = \none \\
+      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc (\mathbf{m}'[n]_\mathbf{u})_{o\dots+l} = \mathbf{s} = \mathbf{u}' &\otherwise \\
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_O(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
-  \texttt{poke} = 21 \\
+  $\Omega_Z(\gascounter, \registers, \memory, (\mathbf{m}, \mathbf{e}))$ \\
+  \texttt{zero} = 21 \\
   $g = 10$} &
   $\begin{aligned}
-    \using [n, a, b, l] &= \registers_{7 \dots 11} \\
+    \using [n, p, c] &= \registers_{7 \dots 10} \\
     \using \mathbf{u} &= \begin{cases}
       \mathbf{m}[n]_\mathbf{u} &\when n \in \keys{\mathbf{m}} \\
       \error &\otherwise\\
     \end{cases} \\
-    \using \mathbf{s} &= \begin{cases}
-      \mem_{a\dots+l} &\when \N_{a\dots+l} \in \mathbb{V}_\mathbf{u}\\
-      \error &\otherwise
-    \end{cases}\\
     \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
-      (\mathbf{u}'_\mathbf{V})_{b\dots+l} = \mathbf{s} \\
-      (\mathbf{u}'_\mathbf{A})_{\floor{\nicefrac{b}{\mathsf{Z}_P}}\dots\floor{\nicefrac{b+l-1}{\mathsf{Z}_P}} + 1} = [\mathrm{W}, \mathrm{W}, ...]
+      (\mathbf{u}'_\mathbf{V})_{p\mathsf{Z}_P\dots+c\mathsf{Z}_P} = [0, 0, \dots] \\
+      (\mathbf{u}'_\mathbf{A})_{p\dots c} = [\mathrm{W}, \mathrm{W}, \dots]
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
-      (\mathtt{OOB}, \mathbf{m}) &\when \mathbf{s} = \error \\
       (\mathtt{WHO}, \mathbf{m}) &\otherwhen \mathbf{u} = \error \\
       (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}' &\otherwise \\
     \end{cases} \\
@@ -779,14 +772,14 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \texttt{void} = 22 \\
   $g = 10$} &
   $\begin{aligned}
-    \using [n, b, l] &= \registers_{7 \dots 10} \\
+    \using [n, p, c] &= \registers_{7 \dots 10} \\
     \using \mathbf{u} &= \begin{cases}
       \mathbf{m}[n]_\mathbf{u} &\when n \in \keys{\mathbf{m}} \\
       \error &\otherwise\\
     \end{cases} \\
     \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
-      (\mathbf{u}'_\mathbf{V})_{b\dots+l} = [0, 0, \dots] \\
-      (\mathbf{u}'_\mathbf{A})_{\floor{\nicefrac{b}{\mathsf{Z}_P}}\dots\floor{\nicefrac{b+l-1}{\mathsf{Z}_P}} + 1} = [\none, \none, \dots]
+      (\mathbf{u}'_\mathbf{V})_{p\mathsf{Z}_P\dots+c\mathsf{Z}_P} = [0, 0, \dots] \\
+      (\mathbf{u}'_\mathbf{A})_{p\dots c} = [\none, \none, \dots]
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
       (\mathtt{WHO}, \mathbf{m}) &\otherwhen \mathbf{u} = \error \\

From 2b432feac1f5869e253722bcbfb6670f3ab56f64 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 12 Nov 2024 15:19:12 +0000
Subject: [PATCH 22/31] Fixes

---
 text/pvm_invocations.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 941a726..9e66067 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -719,7 +719,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \using [n, o, s, l] &= \registers_{7 \dots 11} \\
     \using \mathbf{s} &= \begin{cases}
       \none &\when n \not\in \keys{\mathbf{m}}\\
-      \mathbf{m}[n]_{\mathbf{u}_{s\dots+l}} &\when \N_{s\dots+l} \in \mathbb{V}_{\mathbf{m}[n]_\mathbf{u}} \wedge \N_{o\dots+l} \in \mathbb{V}^*_\lambda \\
+      \mathbf{m}[n]_{\mathbf{u}_{s\dots+l}} &\when \N_{s\dots+l} \in \mathbb{V}_{\mathbf{m}[n]_\mathbf{u}} \wedge \N_{o\dots+l} \in \mathbb{V}^*_\memory \\
       \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mem') &\equiv \begin{cases}
@@ -737,13 +737,13 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \using [n, s, o, l] &= \registers_{7 \dots 11} \\
     \using \mathbf{s} &= \begin{cases}
       \none &\when n \not\in \keys{\mathbf{m}} \\
-      \mem_{s\dots+l} &\when \N_{s\dots+l} \in \mathbb{V}_\mathbf{u} \wedge \N_{o\dots+l} \in \mathbb{V}^*_\memory \\
+      \mem_{s\dots+l} &\when \N_{s\dots+l} \in \mathbb{V}_\memory \wedge \N_{o\dots+l} \in \mathbb{V}^*_{\mathbf{m}[n]_\mathbf{u}} \\
       \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
       (\mathtt{OOB}, \mathbf{m}) &\when \mathbf{s} = \error \\
       (\mathtt{WHO}, \mathbf{m}) &\when \mathbf{s} = \none \\
-      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc (\mathbf{m}'[n]_\mathbf{u})_{o\dots+l} = \mathbf{s} = \mathbf{u}' &\otherwise \\
+      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc (\mathbf{m}'[n]_\mathbf{u})_{o\dots+l} = \mathbf{s} &\otherwise \\
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}

From 229bd734ac60467aa821452c94c96d5bd1c4c425 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Tue, 12 Nov 2024 16:54:11 +0000
Subject: [PATCH 23/31] For extrinsic commitment, hash the bare report, not the
 guaranteed report.

---
 text/header.tex        | 4 ++--
 text/serialization.tex | 3 +--
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/text/header.tex b/text/header.tex
index 5dad391..d3a7559 100644
--- a/text/header.tex
+++ b/text/header.tex
@@ -23,8 +23,8 @@ \section{The Header}\label{sec:header}
 \begin{align}
   \mathbf{H}_x &\in \H \ ,\quad
   \mathbf{H}_x \equiv \mathcal{H}(\se(\mathcal{H}^\#(\mathbf{a}))) \\
-  \where \mathbf{a} &= [\se_T(\xttickets), \se_P(\xtpreimages), g, \se_A(\xtassurances), \se_D(\xtdisputes)] \\
-  \also g &= \se(\mathcal{H}^\#(\se^\#_g(\xtguarantees)))
+  \where \mathbf{a} &= [\se_T(\xttickets), \se_P(\xtpreimages), \mathbf{g}, \se_A(\xtassurances), \se_D(\xtdisputes)] \\
+  \also \mathbf{g} &= \se(\var{[\se(\mathcal{H}(w), \se_4(t), \var{a}) \mid (w, t, a) \orderedin \xtguarantees]})
 \end{align}
 
 A block may only be regarded as valid once the time-slot index $\mathbf{H}_t$ is in the past. It is always strictly greater than that of its parent. Formally:
diff --git a/text/serialization.tex b/text/serialization.tex
index 5d8cdd7..5de11df 100644
--- a/text/serialization.tex
+++ b/text/serialization.tex
@@ -133,8 +133,7 @@ \subsection{Block Serialization}
   \right\rparen \\
   \se_T(\xttickets) &= \se(\var{\xttickets}) \\
   \se_P(\xtpreimages) &= \se(\var{[\tup{s, \var{p}} \mid \tup{s, p} \orderedin \xtpreimages]}) \\
-  \se_G(\xtguarantees) &= \se(\var{\se_g^\#(\xtguarantees)}) \\
-  \se_g(\tup{w, t, a}) &= \se(\tup{w, \se_4(t), \var{a}}) \\
+  \se_G(\xtguarantees) &= \se(\var{[\tup{w, \se_4(t), \var{a}} \mid \tup{w, t, a} \orderedin \xtguarantees]}) \\
   \se_A(\xtassurances) &= \se(\var{[\tup{a, f, \se_2(v), s} \mid \tup{a, f, v, s} \orderedin \xtassurances]}) \\
   \se_D((\mathbf{v}, \mathbf{c}, \mathbf{f})) &= \se(\var{[(r, \se_4(a), [(v, \se_2(i), s) \mid (v, i, s) \orderedin \mathbf{j}]) \mid (r, a, \mathbf{j}) \orderedin \mathbf{v}]}, \var{\mathbf{c}}, \var{\mathbf{f}}) \\
   \se(\mathbf{H}) &= \se_U(\mathbf{H})\concat\se(\mathbf{H}_s) \\

From e4f4f3f1ab3e0649058cbeb269f25f7cee3a84b6 Mon Sep 17 00:00:00 2001
From: Gavin Wood <gavin@parity.io>
Date: Tue, 12 Nov 2024 18:56:56 +0000
Subject: [PATCH 24/31] 64-bit PVM (#136)

* 64-bit registers

* Initial alterations to PVM

* Instructions with Arguments of One Register & One Immediate.

* Instructions with Arguments of One Register, One Immediate and One Offset

* Instructions with Arguments of Two Registers & One Immediate.

* Instructions with Arguments of Three Registers.

* Instructions with Arguments of One Extended Width Immediate

* Renumber instructions simply

* PVM: Simplify expression

* Wording, subseqeq for memory access tests not in

* otherwhen is when

* Don't forget the +

* Don't forget the + again
---
 text/intro.tex           |   6 +-
 text/overview.tex        |   8 +-
 text/pvm.tex             | 273 ++++++++++++++++++++++++---------------
 text/pvm_invocations.tex |  18 +--
 4 files changed, 182 insertions(+), 123 deletions(-)

diff --git a/text/intro.tex b/text/intro.tex
index 5116465..50b127d 100644
--- a/text/intro.tex
+++ b/text/intro.tex
@@ -29,7 +29,7 @@ \subsection{Driving Factors}
 
 \subsection{Scaling under Size-Coherency Antagonism}
 
-Size-coherency antagonism is a simple principle implying that as the state-space of information systems grow, then the system necessarily becomes less coherent. It is a direct implication of of principle that causality is limited by speed. The maximum speed allowed by physics is $C$ the speed of light in a vacuum, however other information systems may have lower bounds: In biological system this is largely determined by various chemical processes whereas in electronic systems is it determined by the speed of electrons in various substances. Distributed software systems will tend to have much lower bounds still, being dependent on a substrate of software, hardware and packet-switched networks of varying reliability.
+Size-coherency antagonism is a simple principle implying that as the state-space of information systems grow, then the system necessarily becomes less coherent. It is a direct implication of principle that causality is limited by speed. The maximum speed allowed by physics is $C$ the speed of light in a vacuum, however other information systems may have lower bounds: In biological system this is largely determined by various chemical processes whereas in electronic systems is it determined by the speed of electrons in various substances. Distributed software systems will tend to have much lower bounds still, being dependent on a substrate of software, hardware and packet-switched networks of varying reliability.
 
 The argument goes:
 \begin{enumerate}
@@ -38,9 +38,9 @@ \subsection{Scaling under Size-Coherency Antagonism}
   \item As the mean and variance increase, then time for causal resolution (i.e. all correct implications of an event to be felt) becomes divergent across the system, causing incoherence.
 \end{enumerate}
 
-Setting the question of overall security aside for a moment, we can manage incoherence by fragmenting the system into causally-independent subsystems, each of which is small enough to be coherent. In a resource-rich environment, a bacterium may split into two rather than growing to double its size. This pattern is rather a crude means of dealing with incoherency under growth: intra-system processing has low size and high synchrony, inter-system processing supports higher overall sizes but with only low synchrony. It is the principle behind meta-networks such as Polkadot, Cosmos and the predominant vision of a scaled Ethereum (all to be discussed in depth shortly).
+Setting the question of overall security aside for a moment, we can manage incoherence by fragmenting the system into causally-independent subsystems, each of which is small enough to be coherent. In a resource-rich environment, a bacterium may split into two rather than growing to double its size. This pattern is rather a crude means of dealing with incoherency under growth: intra-system processing has low size and total coherence, inter-system processing supports higher overall sizes but without coherence. It is the principle behind meta-networks such as Polkadot, Cosmos and the predominant vision of a scaled Ethereum (all to be discussed in depth shortly). Such systems typically rely on asynchronous and simplistic communication with ``settlement areas'' which provide a small-scoped coherent state-space to manage specific interactions such as a token transfer.
 
-The present work explores a middle-ground in the antagonism, avoiding the persistent fragmentation of state-space of the system as with existing approaches. We do this by introducing a new model of computation which pipelines a highly scalable element to a highly synchronous element while retaining a storage facility which is \emph{mostly coherent}. Asynchrony is not avoided, but we do open the possibility for a greater degree of granularity over how it is traded against size. In particular fragmentation can be made ephemeral rather than persistent, drawing upon a coherent state and fragmenting it only for as long as it takes to execute any given piece of processing on it.
+The present work explores a middle-ground in the antagonism, avoiding the persistent fragmentation of state-space of the system as with existing approaches. We do this by introducing a new model of computation which pipelines a highly scalable, \emph{mostly coherent} element to a synchronous, fully coherent element. Asynchrony is not avoided, but we bound it to the length of the pipeline and substitute the crude partitioning we see in scalable systems so far with a form of ``cache affinity'' as it typically seen in multi-\textsc{cpu} systems with a shared \textsc{ram}.
 
 Unlike with \textsc{snark}-based L2-blockchain techniques for scaling, this model draws upon crypto-economic mechanisms and inherits their low-cost and high-performance profiles and averts a bias toward centralization.
 
diff --git a/text/overview.tex b/text/overview.tex
index 5d88949..17964b6 100644
--- a/text/overview.tex
+++ b/text/overview.tex
@@ -140,9 +140,9 @@ \subsection{Economics}
 
 \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
 
-In the present work, we presume the definition of a \emph{Polka Virtual Machine} (\textsc{pvm}). This virtual machine is based around the \textsc{risc-v} instruction set architecture, specifically the \textsc{rv}\oldstylenums{32}\textsc{em} variant, and is the basis for introducing permissionless logic into our state-transition function.
+In the present work, we presume the definition of a \emph{Polka Virtual Machine} (\textsc{pvm}). This virtual machine is based around the \textsc{risc-v} instruction set architecture, specifically the \textsc{rv}\oldstylenums{64}\textsc{em} variant, and is the basis for introducing permissionless logic into our state-transition function.
 
-The \textsc{pvm} is comparable to the \textsc{evm} defined in the Yellow Paper, but somewhat simpler: the complex instructions for cryptographic operations are missing as are those which deal with environmental interactions. Overall it is far less opinionated since it alters a pre-existing general purpose design, \textsc{risc-v}, and optimizes it for our needs. This gives us excellent pre-existing tooling, since \textsc{pvm} remains essentially compatible with \textsc{risc-v}, including support from the compiler toolkit \textsc{llvm} and languages such as Rust and C++. Furthermore, the instruction set simplicity which \textsc{risc-v} and \textsc{pvm} share, together with the register size (32-bit), active number (13) and endianness (little) make it especially well-suited for creating efficient recompilers on to common hardware architectures.
+The \textsc{pvm} is comparable to the \textsc{evm} defined in the Yellow Paper, but somewhat simpler: the complex instructions for cryptographic operations are missing as are those which deal with environmental interactions. Overall it is far less opinionated since it alters a pre-existing general purpose design, \textsc{risc-v}, and optimizes it for our needs. This gives us excellent pre-existing tooling, since \textsc{pvm} remains essentially compatible with \textsc{risc-v}, including support from the compiler toolkit \textsc{llvm} and languages such as Rust and C++. Furthermore, the instruction set simplicity which \textsc{risc-v} and \textsc{pvm} share, together with the register size (64-bit), active number (13) and endianness (little) make it especially well-suited for creating efficient recompilers on to common hardware architectures.
 
 The \textsc{pvm} is fully defined in appendix \ref{sec:virtualmachine}, but for contextualization we will briefly summarize the basic invocation function $\Psi$ which computes the resultant state of a \textsc{pvm} instance initialized with some registers ($\lseq\N_R\rseq_{13}$) and \textsc{ram} ($\mathbb{M}$) and has executed for up to some amount of gas ($\N_G$), a number of approximately time-proportional computational steps:
 \begin{equation}
@@ -166,12 +166,12 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
 \begin{equation}\label{eq:gasregentry}
   \Z_G \equiv \mathbb{Z}_{-2^{63}\dots2^{63}}\ ,\quad
   \N_G \equiv \mathbb{N}_{2^{64}}\ ,\quad
-  \N_R \equiv \N_{2^{32}}
+  \N_R \equiv \N_{2^{64}}
 \end{equation}
 
 It is left as a rather important implementation detail to ensure that the amount of time taken while computing the function $\Psi(\dots, \gascounter, \dots)$ has a maximum computation time approximately proportional to the value of $\gascounter$ regardless of other operands.
 
-The \textsc{pvm} is a very simple \textsc{risc} \emph{register machine} and as such has 13 registers, each of which is a 32-bit quantity, denoted as $\N_R$, a natural less than $2^{32}$.\footnote{This is three fewer than \textsc{risc-v}'s 16, however the amount that program code output by compilers uses is 13 since two are reserved for operating system use and the third is fixed as zero} Within the context of the \textsc{pvm}, $\registers \in \seq{\N_R}_{13}$ is typically used to denote the registers.
+The \textsc{pvm} is a very simple \textsc{risc} \emph{register machine} and as such has 13 registers, each of which is a 64-bit quantity, denoted as $\N_R$, a natural less than $2^{64}$.\footnote{This is three fewer than \textsc{risc-v}'s 16, however the amount that program code output by compilers uses is 13 since two are reserved for operating system use and the third is fixed as zero} Within the context of the \textsc{pvm}, $\registers \in \seq{\N_R}_{13}$ is typically used to denote the registers.
 \begin{align}\label{eq:pvmmemory}
   \mathbb{M} &\equiv \tuple{
     \isa{\mathbf{V}}{\Y_{2^{32}}},
diff --git a/text/pvm.tex b/text/pvm.tex
index 16d9434..b9c8b7f 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -17,14 +17,14 @@ \subsection{Basic Definition}
 \newcommand*{\instrlen}{\ell}
 \newcommand*{\bitsfunc}[1]{\mathcal{B}_{#1}}
 \newcommand*{\unbitsfunc}[1]{\bitsfunc{#1}^{-1}}
-\newcommand*{\bits}[1]{\bitsn{4}{#1}}
-\newcommand*{\unbits}[1]{\unbitsn{4}{#1}}
+\newcommand*{\bits}[1]{\bitsn{8}{#1}}
+\newcommand*{\unbits}[1]{\unbitsn{8}{#1}}
 \newcommand*{\bitsn}[2]{\bitsfunc{#1}(#2)}
 \newcommand*{\unbitsn}[2]{\unbitsfunc{#1}(#2)}
 \newcommand*{\signfunc}[1]{\mathcal{Z}_{#1}}
 \newcommand*{\unsignfunc}[1]{\signfunc{#1}^{-1} }
-\newcommand*{\signed}[1]{\signedn{4}{#1}}
-\newcommand*{\unsigned}[1]{\unsignedn{4}{#1}}
+\newcommand*{\signed}[1]{\signedn{8}{#1}}
+\newcommand*{\unsigned}[1]{\unsignedn{8}{#1}}
 \newcommand*{\signedn}[2]{\signfunc{#1}(#2)}
 \newcommand*{\unsignedn}[2]{\unsignfunc{#1}(#2)}
 %\newcommand*{\signed}[1]{{{}^{\mathord{\mp}}#1}}
@@ -142,7 +142,7 @@ \subsection{Single-Step State Transition}
   \varepsilon = \continue,\quad \imath' = \imath + 1 + \Fskip(\imath),\quad \gascounter' = \gascounter - \gas,\quad \registers' = \registers,\quad\mem' = \mem \text{ except as indicated }
 \end{equation}
 
-Where \textsc{ram} must be inspected and yet access is not possible, then machine state is unchanged, and the exit reason is a fault with the lowest address to be read which is inaccessible. More formally, let $\mathbf{a}$ be the set of indices in to which $\mem$ must be subscripted in order to calculate the result of $\Psi_1$. If $\mathbf{a} \not\subset \mathbb{V}_\mem$ then let $\varepsilon=\fault \times \text{min}(\mathbf{a} \setminus \mathbb{V}_\mem)$.
+Where \textsc{ram} must be inspected and yet access is not possible, then machine state is unchanged, and the exit reason is a fault with the lowest address to be read which is inaccessible. More formally, let $\mathbf{a}$ be the set of indices, modulo $2^{32}$, in to which $\mem$ must be subscripted in order to calculate the result of $\Psi_1$. If $\mathbf{a} \not\subset \mathbb{V}_\mem$ then let $\varepsilon=\fault \times \text{min}(\mathbf{a} \setminus \mathbb{V}_\mem)$.
 
 Similarly, where \textsc{ram} must be mutated and yet mutable access is not possible, then machine state is unchanged, and the exit reason is a fault with the lowest address to be read which is inaccessible. More formally, let $\mathbf{a}$ be the set of indices in to which $\mem'$ must be subscripted in order to calculate the result of $\Psi_1$. If $\mathbf{a} \not\subset \mathbb{V}^*_\mem$ then let $\varepsilon=\fault \times \text{min}(\mathbf{a} \setminus \mathbb{V}^*_\mem)$.
 
@@ -175,9 +175,9 @@ \subsection{Single-Step State Transition}
 
 Immediate arguments are encoded in little-endian format with the most-significant bit being the sign bit. They may be compactly encoded by eliding more significant octets. Elided octets are assumed to be zero if the \textsc{msb} of the value is zero, and 255 otherwise. This allows for compact representation of both positive and negative encoded values. We thus define the signed extension function operating on an input of $n$ octets as $\sext_n$:
 \begin{align}\label{eq:signedextension}
-  \sext_{n\in\{0, 1, 2, 3, 4\}}\colon\left\{\begin{aligned}
-    \N_{2^{8n}} &\to \N_{2^{32}}\\
-    x &\mapsto x + \ffrac{x}{2^{8n-1}}(2^{32}-2^{8n})
+  \sext_{n \in \{0, 1, 2, 3, 4\}}\colon\left\{\begin{aligned}
+    \N_{2^{8n}} &\to \N_R\\
+    x &\mapsto x + \ffrac{x}{2^{8n-1}}(2^{64}-2^{8n})
   \end{aligned}\right.
 \end{align}
 
@@ -220,7 +220,7 @@ \subsubsection{Instructions without Arguments}
   \endhead
   0&\token{trap}&0&$\varepsilon = \panic$\\
   \mrule
-  17&\token{fallthrough}&0&\\
+  1&\token{fallthrough}&0&\\
   \bottomrule
 \end{longtable}
 
@@ -238,7 +238,24 @@ \subsubsection{Instructions with Arguments of One Immediate}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  78&\token{ecalli}&0&$\varepsilon = \host \times \immed_X$\\
+  10&\token{ecalli}&0&$\varepsilon = \host \times \immed_X$\\
+\bottomrule
+\end{longtable}
+
+\subsubsection{Instructions with Arguments of One Extended Width Immediate}
+\begin{equation}
+\begin{aligned}
+  \immed_X \equiv \de_8(\instructions_{\imath+1\dots+8}))
+\end{aligned}
+\end{equation}
+
+\renewcommand*{\mrule}{\cmidrule(lr){1-4}}
+\begin{longtable}{p{8mm} p{25mm} p{5mm} p{100mm}}
+  \toprule
+  \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
+  \midrule
+  \endhead
+  20&\token{load\_imm}&0&$\reg'_A = \immed_X$\\ \mrule
 \bottomrule
 \end{longtable}
 
@@ -258,9 +275,10 @@ \subsubsection{Instructions with Arguments of Two Immediates}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  62&\token{store\_imm\_u8}&0&${\mem'}^\circlearrowleft_{\immed_X} = \immed_Y \bmod 2^8 $\\ \mrule
-  79&\token{store\_imm\_u16}&0&${\mem'}^\circlearrowleft_{\immed_X\dots+2} = \se_2(\immed_Y \bmod 2^{16})$\\ \mrule
-  38&\token{store\_imm\_u32}&0&${\mem'}^\circlearrowleft_{\immed_X\dots+4} = \se_4(\immed_Y)$\\
+  30&\token{store\_imm\_u8}&0&$\memwr_{\immed_X} = \immed_Y \bmod 2^8 $\\ \mrule
+  31&\token{store\_imm\_u16}&0&$\memwr_{\immed_X\dots+2} = \se_2(\immed_Y \bmod 2^{16})$\\ \mrule
+  32&\token{store\_imm\_u32}&0&$\memwr_{\immed_X\dots+4} = \se_4(\immed_Y \bmod 2^{32})$\\ \mrule
+  33&\token{store\_imm\_u64}&0&$\memwr_{\immed_X\dots+8} = \se_8(\immed_Y)$\\
 \bottomrule
 \end{longtable}
 
@@ -278,7 +296,7 @@ \subsubsection{Instructions with Arguments of One Offset}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  5&\token{jump}&0&$\token{branch}(\immed_X, \top)$\\
+  40&\token{jump}&0&$\token{branch}(\immed_X, \top)$\\
 \bottomrule
 \end{longtable}
 
@@ -299,16 +317,19 @@ \subsubsection{Instructions with Arguments of One Register \& One Immediate}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  19&\token{jump\_ind}&0&$\token{djump}((\reg_A + \immed_X) \bmod 2^{32})$\\ \mrule
-  4&\token{load\_imm}&0&$\reg'_A = \immed_X$\\ \mrule
-  60&\token{load\_u8}&0&$\reg'_A = \mem_{\immed_X}$\\ \mrule
-  74&\token{load\_i8}&0&$\reg'_A = \unsigned{\signedn{1}{\mem_{\immed_X}}}$\\ \mrule
-  76&\token{load\_u16}&0&$\reg'_A = \de_2(\memr_{\immed_X\dots+2})$\\ \mrule
-  66&\token{load\_i16}&0&$\reg'_A = \unsigned{\signedn{2}{\de_2(\memr_{\immed_X\dots+2})}}$\\ \mrule
-  10&\token{load\_u32}&0&$\reg'_A = \de_4(\memr_{\immed_X\dots+4})$\\ \mrule
-  71&\token{store\_u8}&0&$\memwr_{\immed_X} = \reg_A \bmod 2^8$\\ \mrule
-  69&\token{store\_u16}&0&$\memwr_{\immed_X\dots+2} = \se_2(\reg_A \bmod 2^{16})$\\ \mrule
-  22&\token{store\_u32}&0&$\memwr_{\immed_X\dots+4} = \se_4(\reg_A)$\\
+  50&\token{jump\_ind}&0&$\token{djump}((\reg_A + \immed_X) \bmod 2^{32})$\\ \mrule
+  51&\token{load\_imm}&0&$\reg'_A = \immed_X$\\ \mrule
+  52&\token{load\_u8}&0&$\reg'_A = \memr_{\immed_X}$\\ \mrule
+  53&\token{load\_i8}&0&$\reg'_A = \sext_1(\memr_{\immed_X})$\\ \mrule
+  54&\token{load\_u16}&0&$\reg'_A = \de_2(\memr_{\immed_X\dots+2})$\\ \mrule
+  55&\token{load\_i16}&0&$\reg'_A = \sext_2(\de_2(\memr_{\immed_X\dots+2}))$\\ \mrule
+  56&\token{load\_u32}&0&$\reg'_A = \de_4(\memr_{\immed_X\dots+4})$\\ \mrule
+  57&\token{load\_i32}&0&$\reg'_A = \sext_4(\de_4(\memr_{\immed_X\dots+4}))$\\ \mrule
+  58&\token{load\_u64}&0&$\reg'_A = \de_8(\memr_{\immed_X\dots+8})$\\ \mrule
+  59&\token{store\_u8}&0&$\memwr_{\immed_X} = \reg_A \bmod 2^8$\\ \mrule
+  60&\token{store\_u16}&0&$\memwr_{\immed_X\dots+2} = \se_2(\reg_A \bmod 2^{16})$\\ \mrule
+  61&\token{store\_u32}&0&$\memwr_{\immed_X\dots+4} = \se_4(\reg_A \bmod 2^{32})$\\ \mrule
+  62&\token{store\_u64}&0&$\memwr_{\immed_X\dots+8} = \se_8(\reg_A)$\\
 \bottomrule
 \end{longtable}
 
@@ -331,9 +352,10 @@ \subsubsection{Instructions with Arguments of One Register \& Two Immediates}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  26&\token{store\_imm\_ind\_u8}&0&$\memwr_{\reg_A + \immed_X} = \immed_Y \bmod 2^8$\\ \mrule
-  54&\token{store\_imm\_ind\_u16}&0&$\memwr_{\reg_A + \immed_X \dots+ 2} = \se_2(\immed_Y \bmod 2^{16})$\\ \mrule
-  13&\token{store\_imm\_ind\_u32}&0&$\memwr_{\reg_A + \immed_X \dots+ 4} = \se_4(\immed_Y)$\\
+  70&\token{store\_imm\_ind\_u8}&0&$\memwr_{\reg_A + \immed_X} = \immed_Y \bmod 2^8$\\ \mrule
+  71&\token{store\_imm\_ind\_u16}&0&$\memwr_{\reg_A + \immed_X \dots+ 2} = \se_2(\immed_Y \bmod 2^{16})$\\ \mrule
+  72&\token{store\_imm\_ind\_u32}&0&$\memwr_{\reg_A + \immed_X \dots+ 4} = \se_4(\immed_Y)$\\
+  73&\token{store\_imm\_ind\_u64}&0&$\memwr_{\reg_A + \immed_X \dots+ 8} = \se_8(\immed_Y)$\\
   \bottomrule
 \end{longtable}
 
@@ -356,17 +378,17 @@ \subsubsection{Instructions with Arguments of One Register, One Immediate and On
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  6&\token{load\_imm\_jump}&0&$\token{branch}(\immed_Y, \top)\ ,\qquad \reg_A' = \immed_X$\\ \mrule
-  7&\token{branch\_eq\_imm}&0&$\token{branch}(\immed_Y, \reg_A = \immed_X)$\\ \mrule
-  15&\token{branch\_ne\_imm}&0&$\token{branch}(\immed_Y, \reg_A \ne \immed_X)$\\ \mrule
-  44&\token{branch\_lt\_u\_imm}&0&$\token{branch}(\immed_Y, \reg_A < \immed_X)$\\ \mrule
-  59&\token{branch\_le\_u\_imm}&0&$\token{branch}(\immed_Y, \reg_A \le \immed_X)$\\ \mrule
-  52&\token{branch\_ge\_u\_imm}&0&$\token{branch}(\immed_Y, \reg_A \ge \immed_X)$\\ \mrule
-  50&\token{branch\_gt\_u\_imm}&0&$\token{branch}(\immed_Y, \reg_A > \immed_X)$\\ \mrule
-  32&\token{branch\_lt\_s\_imm}&0&$\token{branch}(\immed_Y, \signed{\reg_A} < \signed{\immed_X})$\\ \mrule
-  46&\token{branch\_le\_s\_imm}&0&$\token{branch}(\immed_Y, \signed{\reg_A} \le \signed{\immed_X})$\\ \mrule
-  45&\token{branch\_ge\_s\_imm}&0&$\token{branch}(\immed_Y, \signed{\reg_A} \ge \signed{\immed_X})$\\ \mrule
-  53&\token{branch\_gt\_s\_imm}&0&$\token{branch}(\immed_Y, \signed{\reg_A} > \signed{\immed_X})$\\
+  80&\token{load\_imm\_jump}&0&$\token{branch}(\immed_Y, \top)\ ,\qquad \reg_A' = \immed_X$\\ \mrule
+  81&\token{branch\_eq\_imm}&0&$\token{branch}(\immed_Y, \reg_A = \immed_X)$\\ \mrule
+  82&\token{branch\_ne\_imm}&0&$\token{branch}(\immed_Y, \reg_A \ne \immed_X)$\\ \mrule
+  83&\token{branch\_lt\_u\_imm}&0&$\token{branch}(\immed_Y, \reg_A < \immed_X)$\\ \mrule
+  84&\token{branch\_le\_u\_imm}&0&$\token{branch}(\immed_Y, \reg_A \le \immed_X)$\\ \mrule
+  85&\token{branch\_ge\_u\_imm}&0&$\token{branch}(\immed_Y, \reg_A \ge \immed_X)$\\ \mrule
+  86&\token{branch\_gt\_u\_imm}&0&$\token{branch}(\immed_Y, \reg_A > \immed_X)$\\ \mrule
+  87&\token{branch\_lt\_s\_imm}&0&$\token{branch}(\immed_Y, \signed{\reg_A} < \signed{\immed_X})$\\ \mrule
+  88&\token{branch\_le\_s\_imm}&0&$\token{branch}(\immed_Y, \signed{\reg_A} \le \signed{\immed_X})$\\ \mrule
+  89&\token{branch\_ge\_s\_imm}&0&$\token{branch}(\immed_Y, \signed{\reg_A} \ge \signed{\immed_X})$\\ \mrule
+  90&\token{branch\_gt\_s\_imm}&0&$\token{branch}(\immed_Y, \signed{\reg_A} > \signed{\immed_X})$\\
   \bottomrule
 \end{longtable}
 
@@ -388,12 +410,12 @@ \subsubsection{Instructions with Arguments of Two Registers}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  82&\token{move\_reg}&0&$\reg'_D = \reg_A$\\ \mrule
-  87&\token{sbrk}&0&$\begin{aligned}
+  100&\token{move\_reg}&0&$\reg'_D = \reg_A$\\ \mrule
+  101&\token{sbrk}&0&$\begin{aligned}
     \reg'_D \equiv &\min(x \in \N_R): \\
     &x \ge h\\
-    &\N_{x\dots+\reg_A} \not\in \mathbb{V}_{\memory}\\
-    &\N_{x\dots+\reg_A} \in \mathbb{V}^*_{\memory'}
+    &\N_{x\dots+\reg_A} \not\subseteq \mathbb{V}_{\memory}\\
+    &\N_{x\dots+\reg_A} \subseteq \mathbb{V}^*_{\memory'}
   \end{aligned}$\\
 \bottomrule
 \end{longtable}
@@ -420,40 +442,51 @@ \subsubsection{Instructions with Arguments of Two Registers \& One Immediate}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  16&\token{store\_ind\_u8}&0&$\memwr_{\reg_B + \immed_X} = \reg_A \bmod 2^8$\\ \mrule
-  29&\token{store\_ind\_u16}&0&$\memwr_{\reg_B + \immed_X \dots+ 2} = \se_2(\reg_A \bmod 2^{16})$\\ \mrule
-  3&\token{store\_ind\_u32}&0&$\memwr_{\reg_B + \immed_X \dots+ 4} = \se_4(\reg_A)$\\ \mrule
-  11&\token{load\_ind\_u8}&0&$\reg'_A = \mem_{\reg_B + \immed_X}$\\ \mrule
-  21&\token{load\_ind\_i8}&0&$\reg'_A = \unsigned{\signedn{1}{\mem_{\reg_B + \immed_X}}}$\\ \mrule
-  37&\token{load\_ind\_u16}&0&$\reg'_A = \de_2(\memr_{\reg_B + \immed_X\dots+2})$\\ \mrule
-  33&\token{load\_ind\_i16}&0&$\reg'_A = \unsigned{\signedn{2}{\de_2(\memr_{\reg_B + \immed_X\dots+2})}}$\\ \mrule
-  1&\token{load\_ind\_u32}&0&$\reg'_A = \de_4(\memr_{\reg_B + \immed_X\dots+4})$\\ \mrule
-  2&\token{add\_imm}&0&$\reg'_A = (\reg_B + \immed_X) \bmod 2^{32}$\\ \mrule
-  18&\token{and\_imm}&0&$\forall i \in \N_{32} : \bits{\reg'_A}_i = \bits{\reg_B}_i \wedge \bits{\immed_X}_i$\\ \mrule
-  31&\token{xor\_imm}&0&$\forall i \in \N_{32} : \bits{\reg'_A}_i = \bits{\reg_B}_i \oplus \bits{\immed_X}_i$\\ \mrule
-  49&\token{or\_imm}&0&$\forall i \in \N_{32} : \bits{\reg'_A}_i = \bits{\reg_B}_i \vee \bits{\immed_X}_i$\\ \mrule
-  35&\token{mul\_imm}&0&$\reg'_A = (\reg_B \cdot \immed_X) \bmod 2^{32}$\\ \mrule
-  65&\token{mul\_upper\_s\_s\_imm}&0&$\reg'_A = \unsigned{\floor{(\signed{\reg_B} \cdot \signed{\immed_X}) \div 2^{32}}}$\\ \mrule
-  63&\token{mul\_upper\_u\_u\_imm}&0&$\reg'_A = \floor{(\reg_B \cdot \immed_X) \div 2^{32}}$\\ \mrule
-  27&\token{set\_lt\_u\_imm}&0&$\reg'_A = \reg_B < \immed_X$\\ \mrule
-  56&\token{set\_lt\_s\_imm}&0&$\reg'_A = \signed{\reg_B} < \signed{\immed_X}$\\ \mrule
-  9&\token{shlo\_l\_imm}&0&$\reg'_A = (\reg_B \cdot 2^{\immed_X \bmod 32}) \bmod 2^{32}$\\ \mrule
-  14&\token{shlo\_r\_imm}&0&$\reg'_A = \floor{\reg_B \div 2^{\immed_X \bmod 32}}$\\ \mrule
-  25&\token{shar\_r\_imm}&0&$\reg'_A = \unsigned{\floor{\signed{\reg_B} \div 2^{\immed_X \bmod 32}}}$\\ \mrule
-  40&\token{neg\_add\_imm}&0&$\reg'_A = (\immed_X + 2^{32} - \reg_B) \bmod 2^{32}$\\ \mrule
-  39&\token{set\_gt\_u\_imm}&0&$\reg'_A = \reg_B > \immed_X$\\ \mrule
-  61&\token{set\_gt\_s\_imm}&0&$\reg'_A = \signed{\reg_B} > \signed{\immed_X}$\\ \mrule
-  75&\token{shlo\_l\_imm\_alt}&0&$\reg'_A = (\immed_X \cdot 2^{\reg_B \bmod 32}) \bmod 2^{32}$\\ \mrule
-  72&\token{shlo\_r\_imm\_alt}&0&$\reg'_A = \floor{\immed_X \div 2^{\reg_B \bmod 32}}$\\ \mrule
-  80&\token{shar\_r\_imm\_alt}&0&$\reg'_A = \unsigned{\floor{\signed{\immed_X} \div 2^{\reg_B \bmod 32}}}$\\ \mrule
-  85&\token{cmov\_iz\_imm}&0&$\reg'_A = \begin{cases}
+  110&\token{store\_ind\_u8}&0&$\memwr_{\reg_B + \immed_X} = \reg_A \bmod 2^8$\\ \mrule
+  111&\token{store\_ind\_u16}&0&$\memwr_{\reg_B + \immed_X \dots+ 2} = \se_2(\reg_A \bmod 2^{16})$\\ \mrule
+  112&\token{store\_ind\_u32}&0&$\memwr_{\reg_B + \immed_X \dots+ 4} = \se_4(\reg_A \bmod 2^{32})$\\ \mrule
+  113&\token{store\_ind\_u64}&0&$\memwr_{\reg_B + \immed_X \dots+ 8} = \se_8(\reg_A)$\\ \mrule
+  114&\token{load\_ind\_u8}&0&$\reg'_A = \memr_{\reg_B + \immed_X}$\\ \mrule
+  115&\token{load\_ind\_i8}&0&$\reg'_A = \unsigned{\signedn{1}{\memr_{\reg_B + \immed_X}}}$\\ \mrule
+  116&\token{load\_ind\_u16}&0&$\reg'_A = \de_2(\memr_{\reg_B + \immed_X\dots+2})$\\ \mrule
+  117&\token{load\_ind\_i16}&0&$\reg'_A = \unsigned{\signedn{2}{\de_2(\memr_{\reg_B + \immed_X\dots+2})}}$\\ \mrule
+  118&\token{load\_ind\_u32}&0&$\reg'_A = \de_4(\memr_{\reg_B + \immed_X\dots+4})$\\ \mrule
+  119&\token{load\_ind\_i32}&0&$\reg'_A = \unsigned{\signedn{4}{\de_4(\memr_{\reg_B + \immed_X\dots+4})}}$\\ \mrule
+  120&\token{load\_ind\_u64}&0&$\reg'_A = \de_8(\memr_{\reg_B + \immed_X\dots+8})$\\ \mrule
+  121&\token{add\_imm\_32}&0&$\reg'_A = \sext_4((\reg_B + \immed_X) \bmod 2^{32})$\\ \mrule
+  122&\token{and\_imm}&0&$\forall i \in \N_{64} : \bits{\reg'_A}_i = \bits{\reg_B}_i \wedge \bits{\immed_X}_i$\\ \mrule
+  123&\token{xor\_imm}&0&$\forall i \in \N_{64} : \bits{\reg'_A}_i = \bits{\reg_B}_i \oplus \bits{\immed_X}_i$\\ \mrule
+  124&\token{or\_imm}&0&$\forall i \in \N_{64} : \bits{\reg'_A}_i = \bits{\reg_B}_i \vee \bits{\immed_X}_i$\\ \mrule
+  125&\token{mul\_imm\_32}&0&$\reg'_A = \sext_4((\reg_B \cdot \immed_X) \bmod 2^{32})$\\ \mrule
+  126&\token{set\_lt\_u\_imm}&0&$\reg'_A = \reg_B < \immed_X$\\ \mrule
+  127&\token{set\_lt\_s\_imm}&0&$\reg'_A = \signed{\reg_B} < \signed{\immed_X}$\\ \mrule
+  128&\token{shlo\_l\_imm\_32}&0&$\reg'_A = \sext_4((\reg_B \cdot 2^{\immed_X \bmod 32}) \bmod 2^{32})$\\ \mrule
+  129&\token{shlo\_r\_imm\_32}&0&$\reg'_A = \sext_4(\floor{\reg_B \bmod 2^{32} \div 2^{\immed_X \bmod 32}})$\\ \mrule
+  130&\token{shar\_r\_imm\_32}&0&$\reg'_A = \unsigned{\floor{\signedn{4}{\reg_B \bmod 2^{32} } \div 2^{\immed_X \bmod 32}}}$\\ \mrule
+  131&\token{neg\_add\_imm\_32}&0&$\reg'_A = \sext_4((\immed_X + 2^{32} - \reg_B) \bmod 2^{32})$\\ \mrule
+  132&\token{set\_gt\_u\_imm}&0&$\reg'_A = \reg_B > \immed_X$\\ \mrule
+  133&\token{set\_gt\_s\_imm}&0&$\reg'_A = \signed{\reg_B} > \signed{\immed_X}$\\ \mrule
+  134&\token{shlo\_l\_imm\_alt\_32}&0&$\reg'_A = \sext_4((\immed_X \cdot 2^{\reg_B \bmod 32}) \bmod 2^{32})$\\ \mrule
+  135&\token{shlo\_r\_imm\_alt\_32}&0&$\reg'_A = \sext_4(\floor{\immed_X \div 2^{\reg_B \bmod 32}})$\\ \mrule
+  136&\token{shar\_r\_imm\_alt\_32}&0&$\reg'_A = \unsigned{\floor{\signedn{4}{\immed_X} \div 2^{\reg_B \bmod 32}}}$\\ \mrule
+  137&\token{cmov\_iz\_imm}&0&$\reg'_A = \begin{cases}
     \immed_X &\when \reg_B = 0\\
     \reg_A &\otherwise
   \end{cases}$\\ \mrule
-  86&\token{cmov\_nz\_imm}&0&$\reg'_A = \begin{cases}
+  138&\token{cmov\_nz\_imm}&0&$\reg'_A = \begin{cases}
     \immed_X &\when \reg_B \ne 0\\
     \reg_A &\otherwise
-  \end{cases}$\\ \bottomrule
+  \end{cases}$\\ \mrule
+  139&\token{add\_imm\_64}&0&$\reg'_A = (\reg_B + \immed_X) \bmod 2^{64}$\\ \mrule
+  140&\token{mul\_imm\_64}&0&$\reg'_A = (\reg_B \cdot \immed_X) \bmod 2^{64}$\\ \mrule
+  141&\token{shlo\_l\_imm\_64}&0&$\reg'_A = \sext_8((\reg_B \cdot 2^{\immed_X \bmod 64}) \bmod 2^{64})$\\ \mrule
+  142&\token{shlo\_r\_imm\_64}&0&$\reg'_A = \sext_8(\floor{\reg_B \div 2^{\immed_X \bmod 64}})$\\ \mrule
+  143&\token{shar\_r\_imm\_64}&0&$\reg'_A = \unsigned{\floor{\signed{\reg_B} \div 2^{\immed_X \bmod 64}}}$\\ \mrule
+  144&\token{neg\_add\_imm\_64}&0&$\reg'_A = (\immed_X + 2^{64} - \reg_B) \bmod 2^{64}$\\ \mrule
+  145&\token{shlo\_l\_imm\_alt\_64}&0&$\reg'_A = (\immed_X \cdot 2^{\reg_B \bmod 64}) \bmod 2^{64}$\\ \mrule
+  146&\token{shlo\_r\_imm\_alt\_64}&0&$\reg'_A = \floor{\immed_X \div 2^{\reg_B \bmod 64}}$\\ \mrule
+  147&\token{shar\_r\_imm\_alt\_64}&0&$\reg'_A = \unsigned{\floor{\signed{\immed_X} \div 2^{\reg_B \bmod 64}}}$\\ \mrule
+  \bottomrule
 \end{longtable}
 
 \subsubsection{Instructions with Arguments of Two Registers \& One Offset}
@@ -476,12 +509,12 @@ \subsubsection{Instructions with Arguments of Two Registers \& One Offset}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-24&\token{branch\_eq}&0&$\token{branch}(\immed_X, \reg_A = \reg_B)$\\ \mrule
-30&\token{branch\_ne}&0&$\token{branch}(\immed_X, \reg_A \ne \reg_B)$\\ \mrule
-47&\token{branch\_lt\_u}&0&$\token{branch}(\immed_X, \reg_A < \reg_B)$\\ \mrule
-48&\token{branch\_lt\_s}&0&$\token{branch}(\immed_X, \signed{\reg_A} < \signed{\reg_B})$\\ \mrule
-41&\token{branch\_ge\_u}&0&$\token{branch}(\immed_X, \reg_A \ge \reg_B)$\\ \mrule
-43&\token{branch\_ge\_s}&0&$\token{branch}(\immed_X, \signed{\reg_A} \ge \signed{\reg_B})$\\
+150&\token{branch\_eq}&0&$\token{branch}(\immed_X, \reg_A = \reg_B)$\\ \mrule
+151&\token{branch\_ne}&0&$\token{branch}(\immed_X, \reg_A \ne \reg_B)$\\ \mrule
+152&\token{branch\_lt\_u}&0&$\token{branch}(\immed_X, \reg_A < \reg_B)$\\ \mrule
+153&\token{branch\_lt\_s}&0&$\token{branch}(\immed_X, \signed{\reg_A} < \signed{\reg_B})$\\ \mrule
+154&\token{branch\_ge\_u}&0&$\token{branch}(\immed_X, \reg_A \ge \reg_B)$\\ \mrule
+155&\token{branch\_ge\_s}&0&$\token{branch}(\immed_X, \signed{\reg_A} \ge \signed{\reg_B})$\\
 \bottomrule
 \end{longtable}
 
@@ -508,7 +541,7 @@ \subsubsection{Instruction with Arguments of Two Registers and Two Immediates}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-42&\token{load\_imm\_jump\_ind}&0&$
+  160&\token{load\_imm\_jump\_ind}&0&$
     \token{djump}((\reg_B + \immed_Y) \bmod 2^{32}) \ ,\qquad
     \reg_A' = \immed_X
   $\\
@@ -536,43 +569,69 @@ \subsubsection{Instructions with Arguments of Three Registers}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  8&\token{add}&0&$\reg'_D = (\reg_A + \reg_B) \bmod 2^{32}$\\ \mrule
-  20&\token{sub}&0&$\reg'_D = (\reg_A + 2^{32} - \reg_B) \bmod 2^{32}$\\ \mrule
-  23&\token{and}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \wedge \bits{\reg_B}_i$\\ \mrule
-  28&\token{xor}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \oplus \bits{\reg_B}_i$\\ \mrule
-  12&\token{or}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \vee \bits{\reg_B}_i$\\ \mrule
-  34&\token{mul}&0&$\reg'_D = (\reg_A \cdot \reg_B) \bmod 2^{32}$\\ \mrule
-  67&\token{mul\_upper\_s\_s}&0&$\reg'_D = \unsigned{\floor{(\signed{\reg_A} \cdot \signed{\reg_B}) \div 2^{32}}}$\\ \mrule
-  57&\token{mul\_upper\_u\_u}&0&$\reg'_D = \floor{(\reg_A \cdot \reg_B) \div 2^{32}}$\\ \mrule
-  81&\token{mul\_upper\_s\_u}&0&$\reg'_D = \unsigned{\floor{(\signed{\reg_A} \cdot \reg_B) \div 2^{32}}}$\\ \mrule
-  68&\token{div\_u}&0&$\reg'_D = \begin{cases}
-    2^{32} - 1 &\when \reg_B = 0\\
+  170&\token{add\_32}&0&$\reg'_D = \sext_4((\reg_A + \reg_B) \bmod 2^{32})$\\ \mrule
+  171&\token{sub\_32}&0&$\reg'_D = \sext_4((\reg_A + 2^{32} - \reg_B) \bmod 2^{32})$\\ \mrule
+  172&\token{mul\_32}&0&$\reg'_D = \sext_4((\reg_A \cdot \reg_B) \bmod 2^{32})$\\ \mrule
+  173&\token{div\_u\_32}&0&$\reg'_D = \begin{cases}
+    2^{64} - 1 &\when \reg_B = 0\\
+    \sext_4(\floor{\reg_A \div \reg_B}) &\otherwise
+  \end{cases}$\\ \mrule
+  174&\token{div\_s\_32}&0&$\reg'_D = \begin{cases}
+    2^{64} - 1 &\when \reg_B = 0\\
+    \reg_A &\when \signedn{4}{\reg_A} = -2^{31} \wedge \signedn{4}{\reg_B} = -1\\
+    \unsigned{\floor{\signedn{4}{\reg_A} \div \signedn{4}{\reg_B}}} &\otherwise
+  \end{cases}$\\ \mrule
+  175&\token{rem\_u\_32}&0&$\reg'_D = \begin{cases}
+    \reg_A &\when \reg_B = 0\\
+    \reg_A \bmod \reg_B &\otherwise
+  \end{cases}$\\ \mrule
+  176&\token{rem\_s\_32}&0&$\reg'_D = \begin{cases}
+    \reg_A &\when \reg_B = 0\\
+    0 &\when \signed{\reg_A} = -2^{31} \wedge \signed{\reg_B} = -1\\
+    \unsigned{\signed{\reg_A} \bmod \signed{\reg_B}} &\otherwise
+  \end{cases}$\\ \mrule
+  177&\token{shlo\_l\_32}&0&$\reg'_D = (\reg_A \cdot 2^{\reg_B \bmod 32}) \bmod 2^{32}$\\ \mrule
+  178&\token{shlo\_r\_32}&0&$\reg'_D = \floor{\reg_A \div 2^{\reg_B \bmod 32}}$\\ \mrule
+  179&\token{shar\_r\_32}&0&$\reg'_D = \unsigned{\floor{\signed{\reg_A} \div 2^{\reg_B \bmod 32}}}$\\ \mrule
+
+  180&\token{add\_64}&0&$\reg'_D = (\reg_A + \reg_B) \bmod 2^{64}$\\ \mrule
+  181&\token{sub\_64}&0&$\reg'_D = (\reg_A + 2^{64} - \reg_B) \bmod 2^{64}$\\ \mrule
+  182&\token{mul\_64}&0&$\reg'_D = (\reg_A \cdot \reg_B) \bmod 2^{64}$\\ \mrule
+  183&\token{div\_u\_64}&0&$\reg'_D = \begin{cases}
+    2^{64} - 1 &\when \reg_B = 0\\
     \floor{\reg_A \div \reg_B} &\otherwise
   \end{cases}$\\ \mrule
-  64&\token{div\_s}&0&$\reg'_D = \begin{cases}
-    2^{32} - 1 &\when \reg_B = 0\\
-    \reg_A &\when \signed{\reg_A} = -2^{31} \wedge \signed{\reg_B} = -1\\
+  184&\token{div\_s\_64}&0&$\reg'_D = \begin{cases}
+    2^{64} - 1 &\when \reg_B = 0\\
+    \reg_A &\when \signed{\reg_A} = -2^{63} \wedge \signed{\reg_B} = -1\\
     \unsigned{\floor{\signed{\reg_A} \div \signed{\reg_B}}} &\otherwise
   \end{cases}$\\ \mrule
-  73&\token{rem\_u}&0&$\reg'_D = \begin{cases}
+  185&\token{rem\_u\_64}&0&$\reg'_D = \begin{cases}
     \reg_A &\when \reg_B = 0\\
     \reg_A \bmod \reg_B &\otherwise
   \end{cases}$\\ \mrule
-  70&\token{rem\_s}&0&$\reg'_D = \begin{cases}
+  186&\token{rem\_s\_64}&0&$\reg'_D = \begin{cases}
     \reg_A &\when \reg_B = 0\\
-    0 &\when \signed{\reg_A} = -2^{31} \wedge \signed{\reg_B} = -1\\
+    0 &\when \signed{\reg_A} = -2^{63} \wedge \signed{\reg_B} = -1\\
     \unsigned{\signed{\reg_A} \bmod \signed{\reg_B}} &\otherwise
   \end{cases}$\\ \mrule
-  36&\token{set\_lt\_u}&0&$\reg'_D = \reg_A < \reg_B$\\ \mrule
-  58&\token{set\_lt\_s}&0&$\reg'_D = \signed{\reg_A} < \signed{\reg_B}$\\ \mrule
-  55&\token{shlo\_l}&0&$\reg'_D = (\reg_A \cdot 2^{\reg_B \bmod 32}) \bmod 2^{32}$\\ \mrule
-  51&\token{shlo\_r}&0&$\reg'_D = \floor{\reg_A \div 2^{\reg_B \bmod 32}}$\\ \mrule
-  77&\token{shar\_r}&0&$\reg'_D = \unsigned{\floor{\signed{\reg_A} \div 2^{\reg_B \bmod 32}}}$\\ \mrule
-  83&\token{cmov\_iz}&0&$\reg'_D = \begin{cases}
+  187&\token{shlo\_l\_64}&0&$\reg'_D = (\reg_A \cdot 2^{\reg_B \bmod 64}) \bmod 2^{64}$\\ \mrule
+  188&\token{shlo\_r\_64}&0&$\reg'_D = \floor{\reg_A \div 2^{\reg_B \bmod 64}}$\\ \mrule
+  189&\token{shar\_r\_64}&0&$\reg'_D = \unsigned{\floor{\signed{\reg_A} \div 2^{\reg_B \bmod 64}}}$\\ \mrule
+
+  190&\token{and}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \wedge \bits{\reg_B}_i$\\ \mrule
+  191&\token{xor}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \oplus \bits{\reg_B}_i$\\ \mrule
+  192&\token{or}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \vee \bits{\reg_B}_i$\\ \mrule
+  193&\token{mul\_upper\_s\_s}&0&$\reg'_D = \unsigned{\floor{(\signed{\reg_A} \cdot \signed{\reg_B}) \div 2^{64}}}$\\ \mrule
+  194&\token{mul\_upper\_u\_u}&0&$\reg'_D = \floor{(\reg_A \cdot \reg_B) \div 2^{64}}$\\ \mrule
+  195&\token{mul\_upper\_s\_u}&0&$\reg'_D = \unsigned{\floor{(\signed{\reg_A} \cdot \reg_B) \div 2^{64}}}$\\ \mrule
+  196&\token{set\_lt\_u}&0&$\reg'_D = \reg_A < \reg_B$\\ \mrule
+  197&\token{set\_lt\_s}&0&$\reg'_D = \signed{\reg_A} < \signed{\reg_B}$\\ \mrule
+  198&\token{cmov\_iz}&0&$\reg'_D = \begin{cases}
     \reg_A &\when \reg_B = 0\\
     \reg_D &\otherwise
   \end{cases}$\\ \mrule
-  84&\token{cmov\_nz}&0&$\reg'_D = \begin{cases}
+  199&\token{cmov\_nz}&0&$\reg'_D = \begin{cases}
     \reg_A &\when \reg_B \ne 0\\
     \reg_D &\otherwise
   \end{cases}$\\
@@ -637,13 +696,13 @@ \subsection{Standard Program Initialization}\label{sec:standardprograminit}
 With conditions:
 \begin{align}\label{eq:conditions}
   &\using \mathcal{E}_3(|\mathbf{o}|) \concat \mathcal{E}_3(|\mathbf{w}|) \concat \mathcal{E}_2(z) \concat \mathcal{E}_3(s) \concat \mathbf{o} \concat \mathbf{w} \concat \mathcal{E}_4(|\mathbf{c}|) \concat \mathbf{c} = \mathbf{p}\\
-  &\mathsf{Z}_G = 2^{14}\ ,\quad\mathsf{Z}_Q = 2^{16}\ ,\quad\mathsf{Z}_I = 2^{24}\\
-  &\using \rnp{x \in \N} \equiv \mathsf{Z}_G\left\lceil \frac{x}{\mathsf{Z}_G} \right\rceil\quad,\qquad\rnq{x \in \N} \equiv \mathsf{Z}_Q\left\lceil \frac{x}{\mathsf{Z}_Q} \right\rceil\\
-  &5\mathsf{Z}_Q + Q(|\mathbf{o}|) + Q(|\mathbf{w}| + z\mathsf{Z}_G) + Q(s) + \mathsf{Z}_I \leq 2^{32}
+  &\mathsf{Z}_P = 2^{14}\ ,\quad\mathsf{Z}_Q = 2^{16}\ ,\quad\mathsf{Z}_I = 2^{24}\\
+  &\using \rnp{x \in \N} \equiv \mathsf{Z}_P\left\lceil \frac{x}{\mathsf{Z}_P} \right\rceil\quad,\qquad\rnq{x \in \N} \equiv \mathsf{Z}_Q\left\lceil \frac{x}{\mathsf{Z}_Q} \right\rceil\\
+  &5\mathsf{Z}_Q + Q(|\mathbf{o}|) + Q(|\mathbf{w}| + z\mathsf{Z}_P) + Q(s) + \mathsf{Z}_I \leq 2^{32}
 \end{align}
 Thus, if the above conditions cannot be satisfied with unique values, then the result is $\none$, otherwise it is a tuple of $\mathbf{c}$ as above and $\mem$, $\registers$ such that:
 \begin{equation}\label{eq:memlayout}
-  \forall i \in \N_R : ((\mem_\mathbf{V})_i, (\mem_\mathbf{A})_{\floor{\nicefrac{i}{\mathsf{Z}_P}}}) = \left\{\begin{alignedat}{5}
+  \forall i \in \N_{2^{32}} : ((\mem_\mathbf{V})_i, (\mem_\mathbf{A})_{\floor{\nicefrac{i}{\mathsf{Z}_P}}}) = \left\{\begin{alignedat}{5}
     &\tup{\is{\mathbf{V}}{\mathbf{o}_{i - \mathsf{Z}_Q}}\ts\is{\mathbf{A}}{R}} &&\ \when
         \mathsf{Z}_Q
             &\ \leq i < \ &&
@@ -659,7 +718,7 @@ \subsection{Standard Program Initialization}\label{sec:standardprograminit}
     &(0, W) &&\ \when
         2\mathsf{Z}_Q + \rnq{|\mathbf{o}|} + |\mathbf{w}|
             &\ \leq i < \ &&
-                2\mathsf{Z}_Q + \rnq{|\mathbf{o}|} + \rnp{|\mathbf{w}|} + z\mathsf{Z}_G\\
+                2\mathsf{Z}_Q + \rnq{|\mathbf{o}|} + \rnp{|\mathbf{w}|} + z\mathsf{Z}_P\\
     &(0, W) &&\ \when
         2^{32} - 2\mathsf{Z}_Q - \mathsf{Z}_I - \rnp{s}
             &\ \leq i < \ &&
diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 9e66067..6d7b05a 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -683,7 +683,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \using p &= \registers_7 \\
     \using z &= \min(\registers_8, \mathsf{W}_E\mathsf{W}_S) \\
     \using \mathbf{x} &= \begin{cases}
-      \mathcal{P}_{\mathsf{W}_E\mathsf{W}_S}(\mem_{p\dots+z}) &\when \N_{p\dots+z} \in \mathbb{V}_\memory\\
+      \mathcal{P}_{\mathsf{W}_E\mathsf{W}_S}(\memr_{p\dots+z}) &\when \N_{p\dots+z} \subseteq \mathbb{V}_\memory\\
       \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mathbf{e}') &\equiv \begin{cases}
@@ -719,13 +719,13 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \using [n, o, s, l] &= \registers_{7 \dots 11} \\
     \using \mathbf{s} &= \begin{cases}
       \none &\when n \not\in \keys{\mathbf{m}}\\
-      \mathbf{m}[n]_{\mathbf{u}_{s\dots+l}} &\when \N_{s\dots+l} \in \mathbb{V}_{\mathbf{m}[n]_\mathbf{u}} \wedge \N_{o\dots+l} \in \mathbb{V}^*_\memory \\
+      (\mathbf{m}[n]_\mathbf{u})_{s\dots+l} &\when \N_{s\dots+l} \subseteq \mathbb{V}_{\mathbf{m}[n]_\mathbf{u}} \wedge \N_{o\dots+l} \subseteq \mathbb{V}^*_\memory \\
       \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mem') &\equiv \begin{cases}
       (\mathtt{OOB}, \mem) &\when \mathbf{s} = \error \\
       (\mathtt{WHO}, \mem) &\when \mathbf{s} = \none \\
-      (\mathtt{OK}, \mem') \ \where \mem' = \mem \exc \mem'_{o\dots+l} = \mathbf{s} &\otherwise
+      (\mathtt{OK}, \mem') \ \where \mem' = \mem \exc \memwr_{o\dots+l} = \mathbf{s} &\otherwise
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
@@ -737,7 +737,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \using [n, s, o, l] &= \registers_{7 \dots 11} \\
     \using \mathbf{s} &= \begin{cases}
       \none &\when n \not\in \keys{\mathbf{m}} \\
-      \mem_{s\dots+l} &\when \N_{s\dots+l} \in \mathbb{V}_\memory \wedge \N_{o\dots+l} \in \mathbb{V}^*_{\mathbf{m}[n]_\mathbf{u}} \\
+      \memr_{s\dots+l} &\when \N_{s\dots+l} \subseteq \mathbb{V}_\memory \wedge \N_{o\dots+l} \subseteq \mathbb{V}^*_{\mathbf{m}[n]_\mathbf{u}} \\
       \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
@@ -759,10 +759,10 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \end{cases} \\
     \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
       (\mathbf{u}'_\mathbf{V})_{p\mathsf{Z}_P\dots+c\mathsf{Z}_P} = [0, 0, \dots] \\
-      (\mathbf{u}'_\mathbf{A})_{p\dots c} = [\mathrm{W}, \mathrm{W}, \dots]
+      (\mathbf{u}'_\mathbf{A})_{p\dots+c} = [\mathrm{W}, \mathrm{W}, \dots]
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
-      (\mathtt{WHO}, \mathbf{m}) &\otherwhen \mathbf{u} = \error \\
+      (\mathtt{WHO}, \mathbf{m}) &\when \mathbf{u} = \error \\
       (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}' &\otherwise \\
     \end{cases} \\
   \end{aligned}$\\
@@ -779,10 +779,10 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \end{cases} \\
     \using \mathbf{u}' &= \mathbf{u} \exc \begin{cases}
       (\mathbf{u}'_\mathbf{V})_{p\mathsf{Z}_P\dots+c\mathsf{Z}_P} = [0, 0, \dots] \\
-      (\mathbf{u}'_\mathbf{A})_{p\dots c} = [\none, \none, \dots]
+      (\mathbf{u}'_\mathbf{A})_{p\dots+c} = [\none, \none, \dots]
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
-      (\mathtt{WHO}, \mathbf{m}) &\otherwhen \mathbf{u} = \error \\
+      (\mathtt{WHO}, \mathbf{m}) &\when \mathbf{u} = \error \\
       (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}' &\otherwise \\
     \end{cases} \\
   \end{aligned}$\\
@@ -794,7 +794,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   $\begin{aligned}
     \using [n, o] &= \registers_{7, 8} \\
     \using (g, \mathbf{w}) &= \begin{cases}
-      (\de_8(\mem_{o\dots+8}), [\de_4(\mem_{o+8+4x\dots+4}) \mid x \orderedin \N_{13}]) &\when \N_{o \dots+ 60} \subset \mathbb{V}^*_{\mem} \\
+      (\de_8(\memr_{o\dots+8}), [\de_4(\memr_{o+8+4x\dots+4}) \mid x \orderedin \N_{13}]) &\when \N_{o \dots+ 60} \subset \mathbb{V}^*_{\mem} \\
       (\error, \error) &\otherwise
     \end{cases} \\
     \using (c, i', g', \mathbf{w}', \mathbf{u}') &= \Psi(\mathbf{m}[n]_\mathbf{p}, \mathbf{m}[n]_i, g, \mathbf{w}, \mathbf{m}[n]_\mathbf{u})\\

From c16a55d0d5ea4b06657eb2ab3a44880c8f5a5185 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Wed, 13 Nov 2024 17:02:49 +0000
Subject: [PATCH 25/31] 64-bit PVM corrections

---
 text/pvm.tex | 44 +++++++++++++++++++++++---------------------
 1 file changed, 23 insertions(+), 21 deletions(-)

diff --git a/text/pvm.tex b/text/pvm.tex
index b9c8b7f..4a52a9f 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -242,11 +242,11 @@ \subsubsection{Instructions with Arguments of One Immediate}
 \bottomrule
 \end{longtable}
 
-\subsubsection{Instructions with Arguments of One Extended Width Immediate}
+\subsubsection{Instructions with Arguments of One Register and One Extended Width Immediate}
 \begin{equation}
-\begin{aligned}
-  \immed_X \equiv \de_8(\instructions_{\imath+1\dots+8}))
-\end{aligned}
+  \using r_A = \min(12, \instructions_{\imath+1} \bmod 16) \,,\quad
+  \reg'_A \equiv \reg'_{r_A} \,,\quad
+  \immed_X \equiv \de_8(\instructions_{\imath+1\dots+8})
 \end{equation}
 
 \renewcommand*{\mrule}{\cmidrule(lr){1-4}}
@@ -255,7 +255,7 @@ \subsubsection{Instructions with Arguments of One Extended Width Immediate}
   \thead{$\instructions_\imath$} & \thead{\textbf{Name}} & \thead{$\gas$} & \thead{\textbf{Mutations}} \\
   \midrule
   \endhead
-  20&\token{load\_imm}&0&$\reg'_A = \immed_X$\\ \mrule
+  20&\token{load\_imm\_64}&0&$\reg'_A = \immed_X$\\ \mrule
 \bottomrule
 \end{longtable}
 
@@ -354,7 +354,7 @@ \subsubsection{Instructions with Arguments of One Register \& Two Immediates}
   \endhead
   70&\token{store\_imm\_ind\_u8}&0&$\memwr_{\reg_A + \immed_X} = \immed_Y \bmod 2^8$\\ \mrule
   71&\token{store\_imm\_ind\_u16}&0&$\memwr_{\reg_A + \immed_X \dots+ 2} = \se_2(\immed_Y \bmod 2^{16})$\\ \mrule
-  72&\token{store\_imm\_ind\_u32}&0&$\memwr_{\reg_A + \immed_X \dots+ 4} = \se_4(\immed_Y)$\\
+  72&\token{store\_imm\_ind\_u32}&0&$\memwr_{\reg_A + \immed_X \dots+ 4} = \se_4(\immed_Y)$\\ \mrule
   73&\token{store\_imm\_ind\_u64}&0&$\memwr_{\reg_A + \immed_X \dots+ 8} = \se_8(\immed_Y)$\\
   \bottomrule
 \end{longtable}
@@ -570,29 +570,31 @@ \subsubsection{Instructions with Arguments of Three Registers}
   \midrule
   \endhead
   170&\token{add\_32}&0&$\reg'_D = \sext_4((\reg_A + \reg_B) \bmod 2^{32})$\\ \mrule
-  171&\token{sub\_32}&0&$\reg'_D = \sext_4((\reg_A + 2^{32} - \reg_B) \bmod 2^{32})$\\ \mrule
+  171&\token{sub\_32}&0&$\reg'_D = \sext_4((\reg_A + 2^{32} - (\reg_B \bmod 2^{32})) \bmod 2^{32})$\\ \mrule
   172&\token{mul\_32}&0&$\reg'_D = \sext_4((\reg_A \cdot \reg_B) \bmod 2^{32})$\\ \mrule
   173&\token{div\_u\_32}&0&$\reg'_D = \begin{cases}
     2^{64} - 1 &\when \reg_B = 0\\
-    \sext_4(\floor{\reg_A \div \reg_B}) &\otherwise
+    \floor{(\reg_A \bmod 2^{32}) \div (\reg_B \bmod 2^{32})} &\otherwise
   \end{cases}$\\ \mrule
   174&\token{div\_s\_32}&0&$\reg'_D = \begin{cases}
-    2^{64} - 1 &\when \reg_B = 0\\
-    \reg_A &\when \signedn{4}{\reg_A} = -2^{31} \wedge \signedn{4}{\reg_B} = -1\\
-    \unsigned{\floor{\signedn{4}{\reg_A} \div \signedn{4}{\reg_B}}} &\otherwise
+    2^{64} - 1 &\when b = 0\\
+    a &\when a = -2^{31} \wedge b = -1\\
+    \unsigned{\floor{a \div b}} &\otherwise \\[2pt]
+    \multicolumn{2}{l}{\quad \where a = \signedn{4}{\reg_A \bmod 2^{32}}\,,\ b = \signedn{4}{\reg_B \bmod 2^{32}}}\\
   \end{cases}$\\ \mrule
   175&\token{rem\_u\_32}&0&$\reg'_D = \begin{cases}
-    \reg_A &\when \reg_B = 0\\
-    \reg_A \bmod \reg_B &\otherwise
+    \reg_A &\when \reg_B \bmod 2^{32} = 0\\
+    (\reg_A \bmod 2^{32}) \bmod (\reg_B \bmod 2^{32}) &\otherwise
   \end{cases}$\\ \mrule
   176&\token{rem\_s\_32}&0&$\reg'_D = \begin{cases}
-    \reg_A &\when \reg_B = 0\\
-    0 &\when \signed{\reg_A} = -2^{31} \wedge \signed{\reg_B} = -1\\
-    \unsigned{\signed{\reg_A} \bmod \signed{\reg_B}} &\otherwise
+    \unsigned{a} &\when b = 0 \\
+    0 &\when a = -2^{31} \wedge b = -1 \\
+    \unsigned{a \bmod b} &\otherwise \\[2pt]
+    \multicolumn{2}{l}{\quad \where a = \signedn{4}{\reg_A \bmod 2^{32}}\,,\ b = \signedn{4}{\reg_B \bmod 2^{32}}}\\
   \end{cases}$\\ \mrule
   177&\token{shlo\_l\_32}&0&$\reg'_D = (\reg_A \cdot 2^{\reg_B \bmod 32}) \bmod 2^{32}$\\ \mrule
-  178&\token{shlo\_r\_32}&0&$\reg'_D = \floor{\reg_A \div 2^{\reg_B \bmod 32}}$\\ \mrule
-  179&\token{shar\_r\_32}&0&$\reg'_D = \unsigned{\floor{\signed{\reg_A} \div 2^{\reg_B \bmod 32}}}$\\ \mrule
+  178&\token{shlo\_r\_32}&0&$\reg'_D = \floor{(\reg_A \bmod 2^{32}) \div 2^{\reg_B \bmod 32}}$\\ \mrule
+  179&\token{shar\_r\_32}&0&$\reg'_D = \unsigned{\floor{\signedn{4}{\reg_A \bmod 2^{32}} \div 2^{\reg_B \bmod 32}}}$\\ \mrule
 
   180&\token{add\_64}&0&$\reg'_D = (\reg_A + \reg_B) \bmod 2^{64}$\\ \mrule
   181&\token{sub\_64}&0&$\reg'_D = (\reg_A + 2^{64} - \reg_B) \bmod 2^{64}$\\ \mrule
@@ -619,9 +621,9 @@ \subsubsection{Instructions with Arguments of Three Registers}
   188&\token{shlo\_r\_64}&0&$\reg'_D = \floor{\reg_A \div 2^{\reg_B \bmod 64}}$\\ \mrule
   189&\token{shar\_r\_64}&0&$\reg'_D = \unsigned{\floor{\signed{\reg_A} \div 2^{\reg_B \bmod 64}}}$\\ \mrule
 
-  190&\token{and}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \wedge \bits{\reg_B}_i$\\ \mrule
-  191&\token{xor}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \oplus \bits{\reg_B}_i$\\ \mrule
-  192&\token{or}&0&$\forall i \in \N_{32} : \bits{\reg'_D}_i = \bits{\reg_A}_i \vee \bits{\reg_B}_i$\\ \mrule
+  190&\token{and}&0&$\forall i \in \N_{64} : \bits{\reg'_D}_i = \bits{\reg_A}_i \wedge \bits{\reg_B}_i$\\ \mrule
+  191&\token{xor}&0&$\forall i \in \N_{64} : \bits{\reg'_D}_i = \bits{\reg_A}_i \oplus \bits{\reg_B}_i$\\ \mrule
+  192&\token{or}&0&$\forall i \in \N_{64} : \bits{\reg'_D}_i = \bits{\reg_A}_i \vee \bits{\reg_B}_i$\\ \mrule
   193&\token{mul\_upper\_s\_s}&0&$\reg'_D = \unsigned{\floor{(\signed{\reg_A} \cdot \signed{\reg_B}) \div 2^{64}}}$\\ \mrule
   194&\token{mul\_upper\_u\_u}&0&$\reg'_D = \floor{(\reg_A \cdot \reg_B) \div 2^{64}}$\\ \mrule
   195&\token{mul\_upper\_s\_u}&0&$\reg'_D = \unsigned{\floor{(\signed{\reg_A} \cdot \reg_B) \div 2^{64}}}$\\ \mrule

From e243b855233add701d3f28b4354bc68824673690 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Thu, 14 Nov 2024 10:11:27 +0000
Subject: [PATCH 26/31] `zero` error checking

---
 text/overview.tex        | 2 +-
 text/pvm_invocations.tex | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/text/overview.tex b/text/overview.tex
index 17964b6..95d254c 100644
--- a/text/overview.tex
+++ b/text/overview.tex
@@ -193,7 +193,7 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
   \item Regular program termination caused by an explicit halt instruction, $\halt$.
   \item Irregular program termination caused by some exceptional circumstance, $\panic$.
   \item Exhaustion of gas, $\oog$.
-  \item A page fault (attempt to access some address in \textsc{ram} which is not accessible), $\fault$. This includes the address at fault.
+  \item A page fault (attempt to access some address in \textsc{ram} which is not accessible), $\fault$. This includes the address of the page at fault.
   \item An attempt at progressing a host-call, $\host$. This allows for the progression and integration of a context-dependent state-machine beyond the regular \textsc{pvm}.
 \end{itemize}
 
diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 6d7b05a..cc1cf76 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -762,6 +762,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
       (\mathbf{u}'_\mathbf{A})_{p\dots+c} = [\mathrm{W}, \mathrm{W}, \dots]
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
+      (\mathtt{OOB}, \mathbf{m}) &\when p < 16 \vee p+c \ge \nicefrac{2^{32}}{\mathsf{Z}_P} \\
       (\mathtt{WHO}, \mathbf{m}) &\when \mathbf{u} = \error \\
       (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}' &\otherwise \\
     \end{cases} \\

From 8836f67d5122ea11fc40e34f6b6c16d98452f674 Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Thu, 14 Nov 2024 10:16:12 +0000
Subject: [PATCH 27/31] Host call results are at top of 2^64 range.

---
 text/pvm_invocations.tex | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index cc1cf76..2c0ed25 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -8,16 +8,16 @@ \section{Virtual Machine Invocations}\label{sec:virtualmachineinvocations}
 \subsection{Host-Call Result Constants}
 
 \begin{description}
-  \item[$\mathtt{NONE} = 2^{32} - 1$] The return value indicating an item does not exist.
-  \item[$\mathtt{WHAT} = 2^{32} - 2$] Name unknown.
-  \item[$\mathtt{OOB} = 2^{32} - 3$] The return value for when a memory index is provided for reading/writing which is not accessible.
-  \item[$\mathtt{WHO} = 2^{32} - 4$] Index unknown.
-  \item[$\mathtt{FULL} = 2^{32} - 5$] Storage full.
-  \item[$\mathtt{CORE} = 2^{32} - 6$] Core index unknown.
-  \item[$\mathtt{CASH} = 2^{32} - 7$] Insufficient funds.
-  \item[$\mathtt{LOW} = 2^{32} - 8$] Gas limit too low.
-  \item[$\mathtt{HIGH} = 2^{32} - 9$] Gas limit too high.
-  \item[$\mathtt{HUH} = 2^{32} - 10$] The item is already solicited or cannot be forgotten.
+  \item[$\mathtt{NONE} = 2^{64} - 1$] The return value indicating an item does not exist.
+  \item[$\mathtt{WHAT} = 2^{64} - 2$] Name unknown.
+  \item[$\mathtt{OOB} = 2^{64} - 3$] The return value for when a memory index is provided for reading/writing which is not accessible.
+  \item[$\mathtt{WHO} = 2^{64} - 4$] Index unknown.
+  \item[$\mathtt{FULL} = 2^{64} - 5$] Storage full.
+  \item[$\mathtt{CORE} = 2^{64} - 6$] Core index unknown.
+  \item[$\mathtt{CASH} = 2^{64} - 7$] Insufficient funds.
+  \item[$\mathtt{LOW} = 2^{64} - 8$] Gas limit too low.
+  \item[$\mathtt{HIGH} = 2^{64} - 9$] Gas limit too high.
+  \item[$\mathtt{HUH} = 2^{64} - 10$] The item is already solicited or cannot be forgotten.
   \item[$\mathtt{OK} = 0$] The return value indicating general success.
 \end{description}
 
@@ -30,7 +30,7 @@ \subsection{Host-Call Result Constants}
   \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$.
+Note return codes for a host-call-request exit are any non-zero value less than $2^{64} - 13$.
 
 \subsection{Is-Authorized Invocation}\label{sec:isauthorizedinvocation}
 

From 759a0edb0c513af19feb6e8713d6a61ead437f9a Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Thu, 14 Nov 2024 10:40:46 +0000
Subject: [PATCH 28/31] Some other host-call improvements for 64-bit

---
 text/pvm_invocations.tex | 50 ++++++++++++++++++----------------------
 1 file changed, 22 insertions(+), 28 deletions(-)

diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 2c0ed25..3763cb1 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -264,8 +264,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
   \texttt{gas} = 0 \\
   $g = 10$} &
   $\begin{aligned}
-    \registers'_7 &\equiv \gascounter' \bmod 2^{32} \\
-    \registers'_8 &\equiv \left\lfloor \gascounter' \div 2^{32}\right\rfloor
+    \registers'_7 &\equiv \gascounter'
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
@@ -273,7 +272,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
   \texttt{lookup} = 1 \\
   $g = 10$} &
   $\begin{aligned}
-    \using \mathbf{a} &= \begin{cases} \mathbf{s} &\when \registers_7 \in \{ s, 2^{32} - 1 \} \\ \mathbf{d}[\registers_7] &\otherwise \end{cases} \\
+    \using \mathbf{a} &= \begin{cases} \mathbf{s} &\when \registers_7 \in \{ s, 2^{64} - 1 \} \\ \mathbf{d}[\registers_7] &\otherwise \end{cases} \\
     \using [h_o, b_o, b_z] &= \registers_{8..11} \\
     \using h &= \begin{cases}
       \mathcal{H}(\memory_{h_o\dots+32}) &\when \mathbb{Z}_{h_o \dots+ 32} \subset \mathbb{V}_{\memory} \\
@@ -303,7 +302,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
   % gas cost for cold reads dependent on trie depth.
   $\begin{aligned}
     \using \mathbf{a} &= \begin{cases}
-      \mathbf{s} &\when \registers_7 \in \{ s, 2^{32} - 1 \} \\
+      \mathbf{s} &\when \registers_7 \in \{ s, 2^{64} - 1 \} \\
       \mathbf{d}[\registers_7] &\otherwhen \registers_7 \in \keys{\mathbf{d}} \\
       \none &\otherwise
     \end{cases} \\
@@ -364,7 +363,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
   $g = 10$} &
   $\begin{aligned}
     \using \mathbf{t} &= \begin{cases}
-      \mathbf{d}[s] &\when \registers_7 = 2^{32} - 1 \\
+      \mathbf{d}[s] &\when \registers_7 = 2^{64} - 1 \\
       \mathbf{d}[\registers_7] &\otherwise
     \end{cases} \\
     \using o &= \registers_8 \\
@@ -459,8 +458,7 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
   $g = 10$} &
   $\begin{aligned}
     \mathbf{y'} &\equiv \mathbf{x} \\
-    \registers'_7 &\equiv \gascounter' \bmod 2^{32} \\
-    \registers'_8 &\equiv \left\lfloor \gascounter' \div 2^{32}\right\rfloor
+    \registers'_7 &\equiv \gascounter'
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
@@ -468,15 +466,13 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
   \texttt{new} = 9 \\
   $g = 10$} &
   $\begin{aligned}
-    \using [o, l, g_l, g_h&, m_l, m_h] = \registers_{7..13} \\
+    \using [o, l, g&, m] = \registers_{7..11} \\
     \using c &= \begin{cases}
       \memory_{o\dots+32} &\when \N_{o\dots+32} \subset \mathbb{V}_{\memory} \\
       \error &\otherwise
     \end{cases}\\
-    \using g &= 2^{32}\cdot g_h + g_l \\
-    \using m &= 2^{32}\cdot m_h + m_l \\
     \using \mathbf{a} \in \mathbb{A} \cup \{\error\} &= \begin{cases}
-      (c, \mathbf{s}: \{\}, \mathbf{l}: \{ (c, l) \mapsto [] \}, b: \mathbf{a}_t, g, m) &\when c \ne \error\\
+      \tup{c, \is{\mathbf{s}}{\{\}}, \is{\mathbf{l}}{\{ (c, l) \mapsto [] \}}, \is{b}{\mathbf{a}_t}, g, m} &\when c \ne \error\\
       \error &\otherwise
     \end{cases} \\
     \using \mathbf{s} &= \mathbf{x}_\mathbf{s} \exc \mathbf{s}_b = (\mathbf{x}_\mathbf{s})_b - \mathbf{a}_t \\
@@ -494,13 +490,11 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
     $g = 10$
   } &
   $\begin{aligned}
-    \using [o, g_h, g_l, m_h, m_l] &= \registers_{7..12} \\
+    \using [o, g, m] &= \registers_{7..10} \\
     \using c &= \begin{cases}
       \memory_{o\dots+32} &\when \N_{o \dots+ 32} \subset \mathbb{V}_{\memory} \\
       \error &\otherwise
     \end{cases} \\
-    \using g &= 2^{32}\cdot g_h + g_l \\
-    \using m &= 2^{32}\cdot m_h + m_l \\
     (\registers'_7, (\mathbf{x}'_\mathbf{s})_c, (\mathbf{x}'_\mathbf{s})_g, (\mathbf{x}'_\mathbf{s})_m) &\equiv \begin{cases}
       (\mathtt{OK}, c, g, m) &\when c \ne \error\\
       (\mathtt{OOB}, (\mathbf{x}_\mathbf{s})_c, (\mathbf{x}_\mathbf{s})_g, (\mathbf{x}_\mathbf{s})_m) &\otherwise
@@ -512,12 +506,10 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
   \texttt{transfer} = 11 \\
   $g = 10 + \registers_8 + 2^{32}\cdot\registers_9 $} &
   $\begin{aligned}
-    \using [d, a_l, a_h, g_l, g_h, o] &= \registers_{7..13},  \\
-    \using a &= 2^{32}\cdot a_h + a_l \\
-    \using g &= 2^{32}\cdot g_h + g_l \\
+    \using [d, a, g, o] &= \registers_{7..11},  \\
     \using \mathbf{d} &= \mathbf{x}_\mathbf{d} \cup (\mathbf{x}_\mathbf{u})_\mathbf{d}\\
     \using \mathbf{t} \in \mathbb{T} \cup \{\error\} &= \begin{cases}
-      (\mathbf{x}_s, d, a, m, g): m = \memory_{o\dots+\mathsf{W}_T} &\when \N_{o\dots+\mathsf{W}_T} \subset \mathbb{V}_{\memory} \\
+      \tup{\is{s}{\mathbf{x}_s}, d, a, \is{m}{\memory_{o\dots+\mathsf{W}_T}}, g} &\when \N_{o\dots+\mathsf{W}_T} \subset \mathbb{V}_{\memory} \\
       \error &\otherwise
     \end{cases} \\
     \using b &= (\mathbf{x}_\mathbf{s})_b - a \\
@@ -541,8 +533,8 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
     \using g &= \gascounter \\
     \using \mathbf{d} &= \mathbf{x}_\mathbf{d} \cup (\mathbf{x}_\mathbf{u})_\mathbf{d}\\
     \using \mathbf{t} \in \mathbb{T} \cup \{\error,\none\} &= \begin{cases}
-      \none &\when d \in \{ \mathbf{x}_s, 2^{32} - 1 \} \\
-      (\mathbf{x}_s, d, a, m, g): \se(m) = \memory_{o\dots+\mathsf{W}_T} &\otherwhen \N_{o\dots+\mathsf{W}_T} \subset \mathbb{V}_{\memory} \\
+      \none &\when d \in \{ \mathbf{x}_s, 2^{64} - 1 \} \\
+      \tup{\is{s}{\mathbf{x}_s}, d, a, \is{m}{\memory_{o\dots+\mathsf{W}_T}}, g} &\otherwhen \N_{o\dots+\mathsf{W}_T} \subset \mathbb{V}_{\memory} \\
       \error &\otherwise
     \end{cases} \\
     (\varepsilon', \registers'_7, (\mathbf{x}'_\mathbf{u})_\mathbf{d}, \mathbf{x}'_\mathbf{t}) &\equiv \begin{cases}
@@ -632,7 +624,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   $g = 10$} &
   $\begin{aligned}
     \using \mathbf{a} &= \begin{cases}
-      \mathbf{d}[s] &\when \registers_7 = 2^{32} - 1 \wedge s \in \keys{\mathbf{d}} \\
+      \mathbf{d}[s] &\when \registers_7 = 2^{64} - 1 \wedge s \in \keys{\mathbf{d}} \\
       \mathbf{d}[\registers_7] &\when \registers_7 \in \keys{\mathbf{d}} \\
       \none &\otherwise
     \end{cases} \\
@@ -716,16 +708,16 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \texttt{peek} = 19 \\
   $g = 10$} &
   $\begin{aligned}
-    \using [n, o, s, l] &= \registers_{7 \dots 11} \\
+    \using [n, o, s, z] &= \registers_{7 \dots 11} \\
     \using \mathbf{s} &= \begin{cases}
       \none &\when n \not\in \keys{\mathbf{m}}\\
-      (\mathbf{m}[n]_\mathbf{u})_{s\dots+l} &\when \N_{s\dots+l} \subseteq \mathbb{V}_{\mathbf{m}[n]_\mathbf{u}} \wedge \N_{o\dots+l} \subseteq \mathbb{V}^*_\memory \\
+      (\mathbf{m}[n]_\mathbf{u})_{s\dots+z} &\when \N_{s\dots+z} \subseteq \mathbb{V}_{\mathbf{m}[n]_\mathbf{u}} \wedge \N_{o\dots+z} \subseteq \mathbb{V}^*_\memory \\
       \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mem') &\equiv \begin{cases}
       (\mathtt{OOB}, \mem) &\when \mathbf{s} = \error \\
       (\mathtt{WHO}, \mem) &\when \mathbf{s} = \none \\
-      (\mathtt{OK}, \mem') \ \where \mem' = \mem \exc \memwr_{o\dots+l} = \mathbf{s} &\otherwise
+      (\mathtt{OK}, \mem') \ \where \mem' = \mem \exc \memwr_{o\dots+z} = \mathbf{s} &\otherwise
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
@@ -734,16 +726,16 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \texttt{poke} = 20 \\
   $g = 10$} &
   $\begin{aligned}
-    \using [n, s, o, l] &= \registers_{7 \dots 11} \\
+    \using [n, s, o, z] &= \registers_{7 \dots 11} \\
     \using \mathbf{s} &= \begin{cases}
       \none &\when n \not\in \keys{\mathbf{m}} \\
-      \memr_{s\dots+l} &\when \N_{s\dots+l} \subseteq \mathbb{V}_\memory \wedge \N_{o\dots+l} \subseteq \mathbb{V}^*_{\mathbf{m}[n]_\mathbf{u}} \\
+      \memr_{s\dots+z} &\when \N_{s\dots+z} \subseteq \mathbb{V}_\memory \wedge \N_{o\dots+z} \subseteq \mathbb{V}^*_{\mathbf{m}[n]_\mathbf{u}} \\
       \error &\otherwise
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
       (\mathtt{OOB}, \mathbf{m}) &\when \mathbf{s} = \error \\
       (\mathtt{WHO}, \mathbf{m}) &\when \mathbf{s} = \none \\
-      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc (\mathbf{m}'[n]_\mathbf{u})_{o\dots+l} = \mathbf{s} &\otherwise \\
+      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc (\mathbf{m}'[n]_\mathbf{u})_{o\dots+z} = \mathbf{s} &\otherwise \\
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
@@ -784,7 +776,9 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \end{cases}\\
     (\registers'_7, \mathbf{m}') &\equiv \begin{cases}
       (\mathtt{WHO}, \mathbf{m}) &\when \mathbf{u} = \error \\
-      (\mathtt{OK}, \mathbf{m}')\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}' &\otherwise \\
+      (\mathtt{OOB}, \mathbf{m}) &\when p + c \ge 2^{32} \vee \exists i \in \N_{p\dots+c} : (\mathbf{u}_\mathbf{A})_i = \none \\
+      (\mathtt{OK}, \mathbf{m}')\,,\ &\otherwise \\
+      \multicolumn{2}{l}{\where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'[n]_\mathbf{u} = \mathbf{u}'}
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}

From 4167d6a0b4b4ed07c6870c12bb618cf2d44cee0b Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Thu, 14 Nov 2024 10:42:12 +0000
Subject: [PATCH 29/31] Fix div_u_32 zero shortcut

---
 text/pvm.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/text/pvm.tex b/text/pvm.tex
index 4a52a9f..2c91b75 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -573,7 +573,7 @@ \subsubsection{Instructions with Arguments of Three Registers}
   171&\token{sub\_32}&0&$\reg'_D = \sext_4((\reg_A + 2^{32} - (\reg_B \bmod 2^{32})) \bmod 2^{32})$\\ \mrule
   172&\token{mul\_32}&0&$\reg'_D = \sext_4((\reg_A \cdot \reg_B) \bmod 2^{32})$\\ \mrule
   173&\token{div\_u\_32}&0&$\reg'_D = \begin{cases}
-    2^{64} - 1 &\when \reg_B = 0\\
+    2^{64} - 1 &\when \reg_B \bmod 2^{32} = 0\\
     \floor{(\reg_A \bmod 2^{32}) \div (\reg_B \bmod 2^{32})} &\otherwise
   \end{cases}$\\ \mrule
   174&\token{div\_s\_32}&0&$\reg'_D = \begin{cases}

From d1cd1d4a92f06ed7c8285d288402a586829633ec Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Thu, 14 Nov 2024 10:44:37 +0000
Subject: [PATCH 30/31] Sign extend 32 bit arithmetic ops

---
 text/pvm.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/text/pvm.tex b/text/pvm.tex
index 2c91b75..345677b 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -592,8 +592,8 @@ \subsubsection{Instructions with Arguments of Three Registers}
     \unsigned{a \bmod b} &\otherwise \\[2pt]
     \multicolumn{2}{l}{\quad \where a = \signedn{4}{\reg_A \bmod 2^{32}}\,,\ b = \signedn{4}{\reg_B \bmod 2^{32}}}\\
   \end{cases}$\\ \mrule
-  177&\token{shlo\_l\_32}&0&$\reg'_D = (\reg_A \cdot 2^{\reg_B \bmod 32}) \bmod 2^{32}$\\ \mrule
-  178&\token{shlo\_r\_32}&0&$\reg'_D = \floor{(\reg_A \bmod 2^{32}) \div 2^{\reg_B \bmod 32}}$\\ \mrule
+  177&\token{shlo\_l\_32}&0&$\reg'_D = \sext_4((\reg_A \cdot 2^{\reg_B \bmod 32}) \bmod 2^{32})$\\ \mrule
+  178&\token{shlo\_r\_32}&0&$\reg'_D = \sext_4(\floor{(\reg_A \bmod 2^{32}) \div 2^{\reg_B \bmod 32}})$\\ \mrule
   179&\token{shar\_r\_32}&0&$\reg'_D = \unsigned{\floor{\signedn{4}{\reg_A \bmod 2^{32}} \div 2^{\reg_B \bmod 32}}}$\\ \mrule
 
   180&\token{add\_64}&0&$\reg'_D = (\reg_A + \reg_B) \bmod 2^{64}$\\ \mrule

From 4b088f4d6decc6499ddde868ca4dfbd973e3aa9a Mon Sep 17 00:00:00 2001
From: Gav <gavin@parity.io>
Date: Thu, 14 Nov 2024 11:03:16 +0000
Subject: [PATCH 31/31] rem_u_32 signed ext

---
 text/pvm.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/text/pvm.tex b/text/pvm.tex
index 345677b..eb838e5 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -583,8 +583,8 @@ \subsubsection{Instructions with Arguments of Three Registers}
     \multicolumn{2}{l}{\quad \where a = \signedn{4}{\reg_A \bmod 2^{32}}\,,\ b = \signedn{4}{\reg_B \bmod 2^{32}}}\\
   \end{cases}$\\ \mrule
   175&\token{rem\_u\_32}&0&$\reg'_D = \begin{cases}
-    \reg_A &\when \reg_B \bmod 2^{32} = 0\\
-    (\reg_A \bmod 2^{32}) \bmod (\reg_B \bmod 2^{32}) &\otherwise
+    \sext_4(\reg_A) &\when \reg_B \bmod 2^{32} = 0\\
+    \sext_4((\reg_A \bmod 2^{32}) \bmod (\reg_B \bmod 2^{32})) &\otherwise
   \end{cases}$\\ \mrule
   176&\token{rem\_s\_32}&0&$\reg'_D = \begin{cases}
     \unsigned{a} &\when b = 0 \\