From 9393ba7e4d6475c99b8361d6b435245bb8861839 Mon Sep 17 00:00:00 2001
From: David Emett <david.emett@parity.io>
Date: Thu, 28 May 2026 17:03:58 +0100
Subject: [PATCH 1/2] WiP PVM working-set

---
 graypaper.tex                      |   6 +-
 preamble.tex                       |   9 +
 text/accounts.tex                  |   3 +-
 text/definitions.tex               |   2 +
 text/merklization.tex              |   1 +
 text/overview.tex                  |   8 +-
 text/pvm.tex                       | 327 +++++++++++++++++------------
 text/pvm_invocations.tex           | 115 +++++-----
 text/serialization.tex             |   2 +
 text/work_packages_and_reports.tex |   6 +-
 10 files changed, 286 insertions(+), 193 deletions(-)

diff --git a/graypaper.tex b/graypaper.tex
index cd387037..f8bcb70a 100644
--- a/graypaper.tex
+++ b/graypaper.tex
@@ -1,9 +1,9 @@
 \documentclass[9pt,oneside]{amsart}
 \input{preamble.tex}
 
-\pagecolor{verydarkgray}
-\color{white}
-\makegpbackground
+%\pagecolor{verydarkgray}
+%\color{white}
+%\makegpbackground
 
 \begin{document}
 
diff --git a/preamble.tex b/preamble.tex
index 91ee3f98..bd4fe208 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -311,6 +311,7 @@
 \newcommand*{\Z}{\mathbb{Z}}
 \newcommand*{\zerohash}{\hash[0]}
 \newcommand*{\valcount}{\mathbb{V}}
+\newcommand*{\workingsetsize}{\mathbb{w}}
 
 %%%%%%%%%%%%
 % Blob and bitstring
@@ -428,12 +429,17 @@
 \newcommand*{\ram¬value}{\mathbf{v}}
 \newcommand*{\ram¬access}{\mathbf{a}}
 
+\newcommand*{\pageid}{\mathbb{p}}
+\newcommand*{\pid¬machine}{m}
+\newcommand*{\pid¬index}{i}
+
 \newcommand*{\workpackage}{\mathbb{P}}
 \newcommand*{\wpX}{\mathbf{p}}
 \newcommand*{\wp¬authtoken}{\mathbf{j}}
 \newcommand*{\wp¬authcodehost}{h}
 \newcommand*{\wp¬authcodehash}{u}
 \newcommand*{\wp¬authconfig}{\mathbf{f}}
+\newcommand*{\wp¬authworkingsetsize}{w}
 \newcommand*{\wp¬context}{\¬context}
 \newcommand*{\wp¬workitems}{\mathbf{w}}
 % derived fields
@@ -447,6 +453,7 @@
 \newcommand*{\wi¬codehash}{\¬codehash}
 \newcommand*{\wi¬payload}{\¬payload}
 \newcommand*{\wi¬refgaslimit}{g}
+\newcommand*{\wi¬refworkingsetsize}{w}
 \newcommand*{\wi¬accgaslimit}{a} % O/L ¬authorizer
 \newcommand*{\wi¬exportcount}{\¬exportcount}
 \newcommand*{\wi¬importsegments}{\mathbf{i}}
@@ -519,6 +526,7 @@
 \newcommand*{\sa¬gratis}{f}
 \newcommand*{\sa¬minaccgas}{g}
 \newcommand*{\sa¬minmemogas}{m}
+\newcommand*{\sa¬accworkingsetsize}{w}
 \newcommand*{\sa¬codehash}{c} % Inconsistent with ¬codehash
 \newcommand*{\sa¬balance}{b}
 \newcommand*{\sa¬created}{r}
@@ -790,6 +798,7 @@
 \newcommand*{\gaschargedflag}{\tilde{\gascounter}}
 \newcommand*{\registers}{\varphi}
 \newcommand*{\memory}{\mu}
+\newcommand*{\workingset}{\mathfrak{w}}
 \newcommand*{\pvmreg}{\N_R}
 
 \newcommand*{\segoff}{\varsigma}
diff --git a/text/accounts.tex b/text/accounts.tex
index 6fc1c6dd..d60aa8d1 100644
--- a/text/accounts.tex
+++ b/text/accounts.tex
@@ -8,7 +8,7 @@ \section{Service Accounts}\label{sec:accounts}
   \accounts &\in \dictionary{\serviceid}{\serviceaccount}
 \end{align}
 
-The service account is defined as the tuple of storage dictionary $\sa¬storage$, preimage lookup dictionaries $\sa¬preimages$ and $\sa¬requests$, code hash $\sa¬codehash$, balance $\sa¬balance$ and gratis storage offset $\sa¬gratis$, as well as the two code gas limits $\sa¬minaccgas$ \& $\sa¬minmemogas$. We also record certain usage characteristics concerning the account: the time slot at creation $\sa¬created$, the time slot at the most recent accumulation $\sa¬lastacc$ and the parent service $\sa¬parent$. Formally:
+The service account is defined as the tuple of storage dictionary $\sa¬storage$, preimage lookup dictionaries $\sa¬preimages$ and $\sa¬requests$, code hash $\sa¬codehash$, balance $\sa¬balance$ and gratis storage offset $\sa¬gratis$, the two code gas limits $\sa¬minaccgas$ \& $\sa¬minmemogas$, and the working-set size for accumulation $\sa¬accworkingsetsize$. We also record certain usage characteristics concerning the account: the time slot at creation $\sa¬created$, the time slot at the most recent accumulation $\sa¬lastacc$ and the parent service $\sa¬parent$. Formally:
 \begin{align}\label{eq:serviceaccount}
   \serviceaccount \equiv \tuple{\ \begin{aligned}
     \sa¬storage &\in \dictionary{\blob}{\blob}\,,\
@@ -19,6 +19,7 @@ \section{Service Accounts}\label{sec:accounts}
     \sa¬balance \in \balance\,,\
     \sa¬minaccgas \in \gas\,,\\
     \sa¬minmemogas &\in \gas\,,\
+    \sa¬accworkingsetsize \in \workingsetsize\,,\
     \sa¬created \in \timeslot\,,\
     \sa¬lastacc \in \timeslot\,,\
     \sa¬parent \in \serviceid\\
diff --git a/text/definitions.tex b/text/definitions.tex
index fd6a5e15..40ebb902 100644
--- a/text/definitions.tex
+++ b/text/definitions.tex
@@ -47,6 +47,7 @@ \subsubsection{Custom Notation}
   \item[$\implications$] The set representing implications of accumulation. See equation \ref{eq:implications}.
   \item[$\ram$] The set of \textsc{pvm} $\mathbb{M}$emory (\textsc{ram}) states. See equation \ref{eq:pvmmemory}.
   \item[$\acconeout$] The set of single-service accumulation $\mathbb{O}$utputs. See equation \ref{eq:acconeout}.
+  \item[$\pageid$] The set of \textsc{pvm} memory $\mathbb{p}$age identifiers. See equation \ref{eq:pageid}.
   \item[$\workpackage$] The set of work-$\mathbb{P}$ackages. See equation \ref{eq:workpackage}.
   \item[$\workreport$] The set of work-$\mathbb{R}$eports. See equation \ref{eq:workreport}. \emph{Note used for the set of real numbers.}
   \item[$\partialstate$] The set representating a portion of overall $\mathbb{S}$tate, used during accumulation. See equation \ref{eq:partialstate}.
@@ -58,6 +59,7 @@ \subsubsection{Custom Notation}
   \item[$\edsignature{k}{m}$] The set of $\mathbb{V}$alid Ed25519 signatures of the key $k$ and message $m$. A subset of $\blob[64]$. See section \ref{sec:cryptography}.
   \item[$\bssignature{k}{c}{m}$] The set of $\mathbb{V}$alid Bandersnatch signatures of the public key $k$, context $c$ and message $m$. A subset of $\blob[96]$. See section \ref{sec:cryptography}.
   \item[$\bsringproof{r}{c}{m}$] The set of $\mathbb{V}$alid Bandersnatch Ring\textsc{vrf} proofs of the root $r$, context $c$ and message $m$. A subset of $\blob[784]$. See section \ref{sec:cryptography}.
+  \item[$\workingsetsize$] The set of valid $\mathbb{w}$orking-set sizes. See equation \ref{eq:workingsetsize}.
   \item[$\workitem$] The set of $\mathbb{W}$ork items. See equation \ref{eq:workitem}.
   \item[$\defxfer$] The set of deferred transfers. See equation \ref{eq:defxfer}.
   \item[$\avspec$] The set of availability specifications. See equation \ref{eq:avspec}.
diff --git a/text/merklization.tex b/text/merklization.tex
index edb3a823..4ad75117 100644
--- a/text/merklization.tex
+++ b/text/merklization.tex
@@ -87,6 +87,7 @@ \subsection{Serialization}
     \forall \kv{s}{\saX} \in \accounts: &&C(255, s) &\mapsto \encode{
       0,
       \saX_\sa¬codehash,
+      \encode[2]{\sa¬accworkingsetsize},
       \encode[8]{
         \saX_\sa¬balance,
         \saX_\sa¬minaccgas,
diff --git a/text/overview.tex b/text/overview.tex
index cdb9b576..aa88a70d 100644
--- a/text/overview.tex
+++ b/text/overview.tex
@@ -152,13 +152,14 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
       &\blob,\,\ \ &&\pvmreg\\
       &\gas,\,\ \ &&\bool\\
       &\sequence[13]{\pvmreg},\,\ \ &&\ram\\
+      &\optional{\N},\,\ \ &&\sequence{\optional{\pageid}}\\
     \end{alignedat}
   \,}
   \to
   \tuple{\,
     \begin{aligned}
       &\set{\halt, \panic, \oog} \cup \set{\fault,\host} \times \pvmreg, \pvmreg,\\
-      &\gas,\ \ \ \bool,\ \ \ \sequence[13]{\pvmreg},\ \ \ \ram
+      &\gas, \bool, \sequence[13]{\pvmreg}, \ram, \sequence{\optional{\pageid}}
     \end{aligned}
   \,}
 \end{equation}
@@ -189,6 +190,11 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
 
 We define two sets of indices for the \textsc{ram} $\memory$: $\readable{\memory}$ is the set of indices which may be read from; and $\writable{\memory}$ is the set of indices which may be written to.
 
+On contemporary CPUs, memory is accessed via a series of caches, with increasing capacity but also increasing access latency at each level. In order to be able to accurately predict memory access latency in the gas cost model, the size of the \emph{working-set} of memory pages $\workingset \in \sequence{\optional{\pageid}}$ is constrained. The size is chosen at machine creation time from the set $\workingsetsize$, with a smaller working-set, capable of fitting in a lower-level cache, reducing the predicted latency and thus effective gas cost of each memory access. Note however that every change to the working-set, although automatic and thus mostly invisible to the \textsc{pvm} programmer, incurs a significant gas cost. The smaller the working-set, the more likely each memory access is to ``miss'' and require such a change. The working-set size should be carefully chosen to balance these two factors. Note that the working-set covers both data \emph{and} code.
+\begin{equation}\label{eq:workingsetsize}
+    \workingsetsize \equiv \Nclamp{4}{8193}
+\end{equation}
+
 Invocation of the \textsc{pvm} has an exit-reason as the first item in the resultant tuple. It is either:
 \begin{itemize}
   \item Regular program termination caused by an explicit halt instruction, $\halt$.
diff --git a/text/pvm.tex b/text/pvm.tex
index 8fbb6d81..9e1274ca 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -31,19 +31,22 @@ \subsection{Basic Definition}
 \newcommand*{\smod}{\text{smod}}
 \newcommand*{\rtz}{\text{rtz}}
 \newcommand*{\gascostforblock}{\gascounter^{\Delta}}
+\newcommand*{\codepage}[1]{{#1}^\diamond}
+\newcommand*{\pageforinstruction}{\codepage{P}}
+\newcommand*{\gascostforpageaccess}{\gascounter^\workingset}
 \newcommand*{\startofbasicblock}{\mathfrak{L}}
-We declare the general \textsc{pvm} function $\Psi$. We assume a single-step invocation function define $\Psi_1$ and define the full \textsc{pvm} recursively as a sequence of such mutations up until the single-step mutation results in a halting condition. We additionally define the function $\deblob$ which extracts the instruction data, opcode bitmask and dynamic jump table from a \textsc{pvm} program blob, validates its structure, and verifies whether the given $\imath$ is a valid instruction counter location within the program:
+We declare the general \textsc{pvm} function $\Psi$. We assume a single-step invocation function $\Psi_1$ and define the full \textsc{pvm} recursively as a sequence of such mutations up until the single-step mutation results in a halting condition. We additionally define the function $\deblob$ which extracts the instruction data, opcode bitmask and dynamic jump table from a \textsc{pvm} program blob, validates its structure, and verifies whether the given $\imath$ is a valid instruction counter location within the program:
 \begin{align}
   \Psi&\colon \abracegroup{
-    \tuple{\blob, \pvmreg, \gas, \bool, \regs, \ram} &\to \tuple{\set{\halt, \panic, \oog} \cup \set{\fault, \host} \times \pvmreg, \pvmreg, \gas, \bool, \regs, \ram}\\
-    \tup{\pvm¬blob, \imath, \gascounter, \gaschargedflag, \registers, \mem} &\mapsto \begin{cases}
-      \Psi(\pvm¬blob, \imath', \gascounter', \gaschargedflag', \registers', \mem') &\when \varepsilon = \continue\\
-      \tup{\varepsilon, 0, \gascounter', \gaschargedflag', \registers', \mem'} &\when \varepsilon \in \set{ \panic, \halt }\\
-      \tup{\varepsilon, \imath, \gascounter', \gaschargedflag', \registers, \mem} &\otherwise
+    \tuple{\blob, \pvmreg, \gas, \bool, \regs, \ram, \optional{N}, \sequence{\optional{\pageid}}} &\to \tuple{\set{\halt, \panic, \oog} \cup \set{\fault, \host} \times \pvmreg, \pvmreg, \gas, \bool, \regs, \ram, \sequence{\optional{\pageid}}}\\
+    \tup{\pvm¬blob, \imath, \gascounter, \gaschargedflag, \registers, \mem, \pid¬machine, \workingset} &\mapsto \begin{cases}
+      \Psi(\pvm¬blob, \imath', \gascounter', \gaschargedflag', \registers', \mem', \pid¬machine, \workingset') &\when \varepsilon = \continue\\
+      \tup{\varepsilon, 0, \gascounter', \gaschargedflag', \registers', \mem', \workingset'} &\when \varepsilon \in \set{ \panic, \halt }\\
+      \tup{\varepsilon, \imath, \gascounter', \gaschargedflag', \registers, \mem, \workingset'} &\otherwise
     \end{cases} \\
-    \where \tup{\varepsilon, \imath', \gascounter', \gaschargedflag', \registers', \mem'} &= \begin{cases}
-      \Psi_1(\mathbf{c}, \mathbf{k}, \mathbf{j}, \imath, \gascounter, \gaschargedflag, \registers, \mem) &\when \tup{\mathbf{c}, \mathbf{k}, \mathbf{j}} = \deblob(\pvm¬blob, \imath) \\
-      \tup{\panic, \imath, \gascounter, \gaschargedflag, \registers, \mem} &\otherwise
+    \where \tup{\varepsilon, \imath', \gascounter', \gaschargedflag', \registers', \mem', \workingset'} &= \begin{cases}
+      \Psi_1(\mathbf{c}, \mathbf{k}, \mathbf{j}, \imath, \gascounter, \gaschargedflag, \registers, \mem, \pid¬machine, \workingset) &\when \tup{\mathbf{c}, \mathbf{k}, \mathbf{j}} = \deblob(\pvm¬blob, \imath) \\
+      \tup{\panic, \imath, \gascounter, \gaschargedflag, \registers, \mem, \workingset} &\otherwise
     \end{cases}
   }\\
   \deblob&\colon\abracegrouptwo{
@@ -150,49 +153,64 @@ \subsection{Single-Step State Transition}
 We must now define the single-step \textsc{pvm} state-transition function $\Psi_1$:
 \begin{equation}
   \Psi_1\colon \abracegroup{
-    \tuple{\blob, \bitstring, \sequence{\pvmreg}, \pvmreg, \gas, \bool, \regs, \ram} &\to \tuple{\set{\panic, \halt, \continue } \cup \set{\fault, \host} \times \pvmreg, \pvmreg, \gas, \bool, \regs, \ram}\\
-    \tup{\pvm¬blob, \mathbf{k}, \mathbf{j}, \imath, \gascounter, \gaschargedflag, \registers, \mem} &\mapsto \tup{\varepsilon^*, \imath^*, \gascounter^*, \gaschargedflag^*, \registers^*, \mem^*}
+    \tuple{\blob, \bitstring, \sequence{\pvmreg}, \pvmreg, \gas, \bool, \regs, \ram, \optional{\N}, \sequence{\optional{\pageid}}} &\to \tuple{\set{\panic, \halt, \oog, \continue} \cup \set{\fault, \host} \times \pvmreg, \pvmreg, \gas, \bool, \regs, \ram, \sequence{\optional{\pageid}}}\\
+    \tup{\mathbf{c}, \mathbf{k}, \mathbf{j}, \imath, \gascounter, \gaschargedflag, \registers, \mem, \pid¬machine, \workingset} &\mapsto \tup{\varepsilon^*, \imath^*, \gascounter^*, \gaschargedflag^*, \registers^*, \mem^*, \workingset^*}
   }
 \end{equation}
 
-On the very first step of execution, and every time the execution enters a new basic block or jumps back to the beginning of the current basic block, the gas counter of the machine is updated according to the gas cost function $\gascostforblock$~(\ref{eq:gascostforblock}) of the target basic block. No instruction is allowed to execute within a basic block unless the gas cost for the entire basic block has been charged in advance. In case there's not enough gas remaining to cover the full gas cost, the execution is interrupted and the gas counter remains unchanged. Formally:
+Before execution, the instruction must first be fetched from memory. This may require a change to the working-set and thus incur a gas charge. If there is insufficient gas to cover this charge, execution is interrupted. Working-set changes are discussed further and the functions $\gascostforpageaccess$ and $\pageforinstruction$ defined in section \ref{sec:workingsetchanges}.
+\begin{equation}
+    \begin{aligned}
+        \tup{\codepage{\varepsilon}, \codepage{\gascounter}, \codepage{\workingset}} &= \begin{cases}
+        \tup{\continue, \gascounter - g, w} &\when \gascounter \ge g \\
+        \tup{\oog, \gascounter, \workingset} &\otherwise
+    \end{cases} \\
+        \where (g, w) &= \gascostforpageaccess(\workingset, \tup{\pid¬machine, \is{\pid¬index}{\pageforinstruction(\mathbf{c}, \mathbf{k}, \imath)}})
+    \end{aligned}
+\end{equation}
 
+On the very first step of execution, and every time the execution enters a new basic block or jumps back to the beginning of the current basic block, the gas counter of the machine is updated according to the gas cost function $\gascostforblock$~(\ref{eq:gascostforblock}) of the target basic block. No instruction is allowed to execute within a basic block unless the gas cost for the entire basic block has been charged in advance. In case there's not enough gas remaining to cover the full gas cost, the execution is interrupted and the gas counter remains unchanged. Formally:
 \begin{equation}
-  \tup{\varepsilon^{\gascounter}, \gascounter^*, \gaschargedflag'} = \begin{cases}
-    \tup{\continue, \gascounter, \top} &\when \gaschargedflag = \top \\
-    \tup{\continue, \gascounter - \gascostforblock(\mathbf{c}, \mathbf{k}, \startofbasicblock(\imath)), \top} &\otherwhen \gascounter \ge \gascostforblock(\mathbf{c}, \mathbf{k}, \startofbasicblock(\imath)) \\
-    \tup{\oog, \gascounter, \bot} &\otherwise
+  \tup{\varepsilon^\basicblocks, \gascounter^\basicblocks} = \begin{cases}
+    \tup{\continue, \codepage{\gascounter}} &\when \gaschargedflag = \top \\
+    \tup{\continue, \codepage{\gascounter} - \gascostforblock(\mathbf{c}, \mathbf{k}, \len{\workingset}, \startofbasicblock(\imath))} &\otherwhen \codepage{\gascounter} \ge \gascostforblock(\mathbf{c}, \mathbf{k}, \len{\workingset}, \startofbasicblock(\imath)) \\
+    \tup{\oog, \codepage{\gascounter}} &\otherwise
   \end{cases}
 \end{equation}
 
 During the course of executing instructions \textsc{ram} may be accessed. When an index of \textsc{ram} below $2^{16}$ is required, the machine always panics immediately without further changes to its state regardless of the apparent (in)accessibility of the value. Otherwise, should the given index of \textsc{ram} not be accessible then machine state remains unchanged and the exit reason is a fault with the lowest inaccessible \emph{page address} to be read. 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 page address to be written which is inaccessible.
 
-Formally, let $\mathbf{r}$ and $\mathbf{w}$ be the set of indices by which $\mem$ must be subscripted for inspection and mutation respectively in order to calculate the result of $\Psi_1$. We define the memory-access exceptional execution state $\varepsilon^\mu$ as following:
+In addition to these accessibility checks, as with instruction fetches, \textsc{ram} reads and writes implicitly pull accessed pages into the working-set. If the gas cost of a working-set change cannot be covered by the available gas, execution halts immediately. Note that working-set changes are interleaved with accessibility checks; this can affect observed behaviour in cases of gas exhaustion.
+
+Formally, let $\mathbf{r}$ and $\mathbf{w}$ be the set of indices by which $\mem$ must be subscripted for inspection and mutation respectively in order to calculate the result of $\Psi_1$. We define the memory-access exceptional execution state $\varepsilon^\mu$, posterior gas balance $\gascounter^\mu$, and posterior working-set $\workingset^\mu$ as following:
 \begin{equation}
   \begin{aligned}
-    \varepsilon^{\mu} &= \begin{cases}
-      \continue &\when \mathbf{x} = \emptyset \\
-      \panic &\when \min(\mathbf{x}) \bmod 2^{32} < 2^{16} \\
-      \fault \times \Cpvmpagesize\floor{\min(\mathbf{x}) \bmod 2^{32} \div \Cpvmpagesize} &\otherwise
-    \end{cases}\\
-    \where \mathbf{x} &= \set{\build{x}{x \in \mathbf{r} \wedge x \bmod 2^{32} \not\in \readable\mem\ \vee\ x \in \mathbf{w} \wedge x \bmod 2^{32} \not\in \writable\mem}}
+    (\varepsilon^{\mu}, \gascounter^{\mu}, \workingset^{\mu}) &= A(\gascounter^\basicblocks, \codepage{\workingset},
+      \sqorderby{a_x}{\set{\build{(x, \is{r}{\top})}{x \in \mathbf{r}}} \cup \set{\build{(x, \is{r}{\bot})}{x \in \mathbf{w}}}}) \\
+    A(g, w, \sq{}) &= (\continue, g, w) \\
+    A(g, w, \sq{\tup{x, r}} \concat \mathbf{r}) &= \begin{aligned}
+      &\begin{cases}
+        (\panic, g, w) &\when y < 2^{16} \\
+        (\fault \times \pid¬index \Cpvmpagesize, g, w) &\otherwhen y \not\in
+          \set{\kv{\top}{\readable\mem}, \kv{\bot}{\writable\mem}}\subb{r} \\
+        (\oog, g, w) &\otherwhen g < g^\delta \\
+        A(g - g^\delta, w', \mathbf{r}) &\otherwise
+      \end{cases} \\
+      &\where y = x \bmod 2^{32} \\
+      &\also \pid¬index = \floor{\frac{y}{\Cpvmpagesize}} \\
+      &\also (g^\delta, w') = \gascostforpageaccess(w, \tup{\pid¬machine, \pid¬index})
+    \end{aligned}
   \end{aligned}
 \end{equation}
 
-We define the final execution state, the value of the instruction counter, the values of the registers and the memory as follows:
-\begin{align}
-  \tup{\varepsilon^*, \imath^*, \registers^*, \mem^*} &= \begin{cases}
-    \tup{\varepsilon^{\gascounter}, \imath, \registers, \mem} &\when \varepsilon^{\gascounter} \neq \continue \\
-    \tup{\varepsilon^{\mu}, \imath, \registers, \mem} &\otherwhen \varepsilon^{\mu} \neq \continue \\
-    \tup{\varepsilon, \imath', \registers', \mem'} &\otherwise
-  \end{cases}
-\end{align}
-
-We also have to adjust the state based on the executed instruction, to force a gas charge on the next step when necessary:
+We define the final execution state, the value of the instruction counter, the gas counter, the gas-charged flag, the values of the registers and the memory, and the working-set as follows:
 \begin{equation}
-  \gaschargedflag^* = \begin{cases}
-    \bot &\when \gaschargedflag' = \bot \lor (\mathbf{c}_\imath \in T \land \varepsilon^* \in \set{\continue} \cup \set{\host} \times \pvmreg) \\
-    \top &\otherwise
+  \tup{\varepsilon^*, \imath^*, \gascounter^*, \gaschargedflag^*, \registers^*, \mem^*, \workingset^*} = \begin{cases}
+    \tup{\codepage{\varepsilon}, \imath, \codepage{\gascounter}, \gaschargedflag, \registers, \mem, \codepage{\workingset}} &\when \codepage{\varepsilon} \ne \continue \\
+    \tup{\varepsilon^\basicblocks, \imath, \gascounter^\basicblocks, \bot, \registers, \mem, \codepage{\workingset}} &\otherwhen \varepsilon^\basicblocks \ne \continue \\
+    \tup{\varepsilon^\mu, \imath, \gascounter^\mu, \top, \registers, \mem, \workingset^\mu} &\otherwhen \varepsilon^\mu \ne \continue \\
+    \tup{\varepsilon, \imath', \gascounter^\mu, \top, \registers', \mem', \workingset^\mu} &\otherwhen \varepsilon \not\in \set{\continue} \cup \set{\host} \times \pvmreg \\
+    \tup{\varepsilon, \imath', \gascounter^\mu, \mathbf{c}_\imath \not\in T, \registers', \mem', \workingset^\mu} &\otherwise
   \end{cases}
 \end{equation}
 
@@ -752,39 +770,43 @@ \subsubsection{Instructions with Arguments of Three Registers}
 \subsection{Host Call Definition}
 
 An extended version of the \textsc{pvm} invocation which is able to progress an inner \emph{host-call} state-machine in the case of a host-call halt condition is defined as $\Psi_H$:
-\begin{align}
-  &\Psi_H^*\colon \abracegroup{
+\begin{gather}
+  \Psi_H^*\colon \abracegroup{
     \tuple{\begin{aligned}
-      &\blob, \pvmreg, \gas, \bool,\\&\regs, \ram, \contextmutator{X}, X
+      &\blob, \pvmreg, \gas, \bool,\\&\regs, \ram, \sequence{\optional{\pageid}}, \contextmutator{X}, X
     \end{aligned}
     }
     &\to
-    \tuple{\set{\panic, \oog, \halt} \cup \set{\fault} \times \pvmreg, \pvmreg, \signedgas, \bool, \regs, \ram, X}\\
-    \tup{\pvm¬blob, \imath, \gascounter, \gaschargedflag, \registers, \mem, f, \mathbf{x}} &\mapsto \begin{cases}
-      \multicolumn{2}{l}{\text{let }(\varepsilon', \imath', \gascounter', \gaschargedflag', \registers', \mem') = \Psi(\pvm¬blob, \imath, \gascounter, \gaschargedflag, \registers, \mem):} \\[8pt]
-      \tup{\varepsilon', \imath', \gascounter', \gaschargedflag', \registers', \mem', \mathbf{x}} &\when \varepsilon' \in \set{ \halt, \panic, \oog } \cup \set{\fault} \times \pvmreg \\[4pt]
+    \tuple{\set{\panic, \oog, \halt} \cup \set{\fault} \times \pvmreg, \pvmreg, \signedgas, \bool, \regs, \ram, \sequence{\optional{\pageid}}, X}\\
+    \tup{\pvm¬blob, \imath, \gascounter, \gaschargedflag, \registers, \mem, \workingset, f, \mathbf{x}} &\mapsto \begin{cases}
+      \multicolumn{2}{l}{\text{let }(\varepsilon', \imath', \gascounter', \gaschargedflag', \registers', \mem', \workingset') = \Psi(\pvm¬blob, \imath, \gascounter, \gaschargedflag, \registers, \mem, \none, \workingset):} \\[8pt]
+      \tup{\varepsilon', \imath', \gascounter', \gaschargedflag', \registers', \mem', \workingset', \mathbf{x}} &\when \varepsilon' \in \set{ \halt, \panic, \oog } \cup \set{\fault} \times \pvmreg \\[4pt]
       \begin{aligned}
-        &\Psi_H^*(\pvm¬blob, \imath'', \gascounter'', \gaschargedflag', \registers'', \mem'', f, \mathbf{x}'')\\[2pt]
+        &\Psi_H^*(\pvm¬blob, \imath'', \gascounter'', \gaschargedflag', \registers'', \mem'', \workingset'', f, \mathbf{x}'')\\[2pt]
         &\quad \where \imath'' = \imath' + 1 + \Fskip(\imath')
       \end{aligned}
        &\when \bigwedge\abracegroup[\;]{
         &\varepsilon' = \host \times h\\[2pt]
-        &\tup{\continue, \gascounter'', \registers'', \mem'', \mathbf{x}''} = f(h, \gascounter', \registers', \mem', \mathbf{x})
+        &\tup{\continue, \gascounter'', \registers'', \mem'', \workingset'', \mathbf{x}''} = f(h, \gascounter', \registers', \mem', \workingset', \mathbf{x})
       }\\[8pt]
-      \tup{\varepsilon'', \imath', \gascounter'', \gaschargedflag', \registers'', \mem'', \mathbf{x}''} &\when  \bigwedge\abracegroup[\;]{
+      \tup{\varepsilon'', \imath', \gascounter'', \gaschargedflag', \registers'', \mem'', \workingset'', \mathbf{x}''} &\when  \bigwedge\abracegroup[\;]{
         &\varepsilon' = \host \times h\\[2pt]
-        &\tup{\varepsilon'', \gascounter'', \registers'', \mem'', \mathbf{x}''} = f(h, \gascounter', \registers', \mem', \mathbf{x})\\[2pt]
+        &\tup{\varepsilon'', \gascounter'', \registers'', \mem'', \workingset'', \mathbf{x}''} = f(h, \gascounter', \registers', \mem', \workingset', \mathbf{x})\\[2pt]
         &\varepsilon'' \in \set{\panic, \halt, \oog}
       }\\[8pt]
     \end{cases} \\
     }\!\!\!\!\!\!\!\!\\
-    &\Psi_H(\pvm¬blob, \imath, \gascounter, \registers, \mem, f, \mathbf{x}) \equiv \Psi_H^*(\pvm¬blob, \imath, \gascounter, \bot, \registers, \mem, f, \mathbf{x})\\
-    &\contextmutator{X} \equiv \tuple{\N, \gas, \regs, \ram, X} \to \tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, X}
-\end{align}
+    \begin{aligned}
+      \Psi_H(\pvm¬blob, \imath, \gascounter, \registers, \mem, w, f, \mathbf{x}) &\equiv (\varepsilon, \imath', \gascounter', \registers', \mem', \mathbf{x}') \\
+      \where (\varepsilon, \imath', \gascounter', \gaschargedflag', \registers', \mem', \workingset', \mathbf{x}') &=
+        \Psi_H^*(\pvm¬blob, \imath, \gascounter, \bot, \registers, \mem, \sq{\none, \none, \dots}\sub{\dots w}, f, \mathbf{x})
+    \end{aligned}\\
+    \contextmutator{X} \equiv \tuple{\N, \gas, \regs, \ram, \sequence{\optional{\pageid}}, X} \to \tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \sequence{\optional{\pageid}}, X}
+\end{gather}
 
-As with $\Phi$, on exit the instruction counter references the instruction \emph{which caused the exit} and the machine state is that prior to this instruction. Should the machine be invoked again using this instruction counter and code, then the same instruction which caused the exit would be executed on the proper (prior) machine state.
+As with $\Psi$, on exit the instruction counter references the instruction \emph{which caused the exit} and the machine state is that prior to this instruction. Should the machine be invoked again using this instruction counter and code, then the same instruction which caused the exit would be executed on the proper (prior) machine state.
 
-With $\Phi_H$, host-calls (\ie \token{ecalli} instructions) are in effect handled internally with the state-mutator function provided as an argument, preventing the possibility of the result being a host-call fault. Note that in the case of a successful host-call transition, we must provide the new instruction counter value $\imath''$ explicitly alongside the fresh posterior state for said instruction.
+With $\Psi_H$, host-calls (\ie \token{ecalli} instructions) are in effect handled internally with the state-mutator function provided as an argument, preventing the possibility of the result being a host-call fault. Note that in the case of a successful host-call transition, we must provide the new instruction counter value $\imath''$ explicitly alongside the fresh posterior state for said instruction.
 
 \subsection{Standard Program Initialization}\label{sec:standardprograminit}
 The software programs which will run in each of the three instances where the \textsc{pvm} is utilized in the main document have a very typical setup pattern characteristic of an output of a compiler and linker. This means that \textsc{ram} has sections for program-specific read-only data, read-write (heap) data and the stack. An adjunct to this, very typical of our usage patterns is an extra read-only section via which invocation-specific data may be passed (\ie arguments). It thus makes sense to define this properly in a single initializer function. These sections are quantized into \emph{major zones}, and one major zone is always left unallocated between sections in order to reduce accidental overrun. Sections are padded with zeroes to the nearest \textsc{pvm} memory page boundary.
@@ -856,11 +878,11 @@ \subsection{Argument Invocation Definition}
 \begin{equation}
   \Psi_M\colon \abracegroup{
     \tuple{
-      \blob, \pvmreg, \gas, \blob[:\Cpvminitinputsize], \contextmutator{X}, X
+      \blob, \pvmreg, \gas, \blob[:\Cpvminitinputsize], \workingsetsize, \contextmutator{X}, X
     } &\to \tuple{\gas, \blob \cup \set{\panic, \oog}, X}\\
-    \tup{\jam¬blob, \imath, \gascounter, \mathbf{a}, f, \mathbf{x}} &\mapsto \begin{cases}
+    \tup{\jam¬blob, \imath, \gascounter, \mathbf{a}, w, f, \mathbf{x}} &\mapsto \begin{cases}
       \tup{0, \panic, \mathbf{x}} &\when Y(\jam¬blob, \mathbf{a}) = \none\\
-      R(\gascounter, \Psi_H(\pvm¬blob, \imath, \gascounter, \registers, \mem, f, \mathbf{x})) &\when Y(\jam¬blob, \mathbf{a}) = \tup{\pvm¬blob, \registers, \mem}\\
+      R(\gascounter, \Psi_H(\pvm¬blob, \imath, \gascounter, \registers, \mem, w, f, \mathbf{x})) &\when Y(\jam¬blob, \mathbf{a}) = \tup{\pvm¬blob, \registers, \mem}\\
       \multicolumn{2}{l}{
         \quad \where R \colon \tup{\gascounter, \tup{\begin{alignedat}{5}
           &\varepsilon,\, &&\imath',\, &&\gascounter',\\
@@ -878,7 +900,7 @@ \subsection{Argument Invocation Definition}
   }
 \end{equation}
 
-Note that the first tuple item is the amount of gas consumed by the operation, but never greater than the amount of gas provided for the operation.
+Note that the first tuple item is the amount of gas consumed by the operation, but never greater than the amount of gas provided for the operation. $w$ specifies the number of pages in the working-set; this determines gas costs but otherwise does not affect \textsc{pvm} behaviour. See section \ref{sec:workingsetchanges} for more details.
 
 \subsection{Gas Cost Model}\label{sec:gascostmodel}
 
@@ -909,6 +931,7 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
 \newcommand*{\cost¬execunits}{\check{x}}
 \newcommand*{\inst¬dstregs}{\check{r}}
 \newcommand*{\inst¬srcregs}{\check{s}}
+\newcommand*{\inst¬compiledsize}{\check{n}}
 
 % Types
 \newcommand*{\gas¬sim¬ty}{\mathbb{S}}
@@ -991,16 +1014,16 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
 
 We define the function $\inst¬srcregs(\mathbf{c}, \mathbf{k}, \imath)$ which returns the set of source registers read by the instruction at $\imath$, and the function $\inst¬dstregs(\mathbf{c}, \mathbf{k}, \imath)$ which returns the set of destination registers written by the instruction at $\imath$, as described by the equations in \ref{sec:instructiontables}. This is regardless of whether those registers would actually have been modified by that instruction when executed at runtime. \token{ecalli} is assumed to neither read nor write to any registers in this model.
 
-We also define the function $\cost¬cycles(\mathbf{c}, \mathbf{k}, \imath)$ which returns the number of cycles the instruction at $\imath$ needs to finish execution, $\cost¬decodeslots(\mathbf{c}, \mathbf{k}, \imath)$ which returns the number of decoding slots necessary to decode it, and $\cost¬execunits(\mathbf{c}, \mathbf{k}, \imath)$ which returns the number of virtual CPU execution units required to start its execution. These simply return the values as specified in \ref{sec:gascosttables}.
+We also define the function $\cost¬cycles(\mathbf{c}, \mathbf{k}, w, \imath)$ which returns the number of cycles the instruction at $\imath$ needs to finish execution, $\cost¬decodeslots(\mathbf{c}, \mathbf{k}, \imath)$ which returns the number of decoding slots necessary to decode it, and $\cost¬execunits(\mathbf{c}, \mathbf{k}, \imath)$ which returns the number of virtual CPU execution units required to start its execution. These simply return the values as specified in section \ref{sec:gascosttables}.
 
-The gas cost of a given basic block starting at instruction opcode index $\imath \in \basicblocks$ and given the instruction data $\mathbf{c}$ and the opcode bitmask $\mathbf{k}$ is defined by the number of virtual CPU cycles as determined by the gas cost model transition function, up until every instruction of the basic block it has ingested has been retired and the simulation has converged. Formally:
+The gas cost of a given basic block starting at instruction opcode index $\imath \in \basicblocks$ and given the instruction data $\mathbf{c}$, the opcode bitmask $\mathbf{k}$, and the size of the working-set $w$ is defined by the number of virtual CPU cycles as determined by the gas cost model transition function, up until every instruction of the basic block it has ingested has been retired and the simulation has converged. Formally:
 
 \begin{equation}\label{eq:gascostforblock}
   \gascostforblock\colon \abracegrouptwo{
-    \tup{\blob, \bitstring, \pvmreg} &\to \N\\
-    \tup{\mathbf{c}, \mathbf{k}, \imath} &\mapsto \max(\gas¬sim¬state^{\text{final}}_{\ctr¬cycles} - 3, 1)\\
+    \tuple{\blob, \bitstring, \workingsetsize, \pvmreg} &\to \N\\
+    \tup{\mathbf{c}, \mathbf{k}, w, \imath} &\mapsto \max(\gas¬sim¬state^{\text{final}}_{\ctr¬cycles} - 3, 1)\\
   }{
-    \where &\gas¬sim¬state^{\text{final}} &=&\text{ }\gas¬sim(\mathbf{c}, \mathbf{k}, \gas¬sim¬state^{\text{init}})\\
+    \where &\gas¬sim¬state^{\text{final}} &=&\text{ }\gas¬sim(\mathbf{c}, \mathbf{k}, w, \gas¬sim¬state^{\text{init}})\\
       &\gas¬sim¬state^{\text{init}} &=&\text{ }\tup{\imath, 0, \const¬maxdecodepercycle, \const¬maxstartpercycle, \tup{4, 4, 4, 1, 1}, \sq{}}
   }
 \end{equation}
@@ -1009,12 +1032,12 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
 
 \begin{equation}
   \gas¬sim\colon \abracegroup{
-    \tup{\blob, \bitstring, \gas¬sim¬ty} &\to \gas¬sim¬ty \\
-    \tup{\mathbf{c}, \mathbf{k}, \gas¬sim¬state} &\mapsto \begin{cases}
-      \gas¬sim(\mathbf{c}, \mathbf{k}, \gas¬sim'(\mathbf{c}, \mathbf{k}, \gas¬sim¬state)) &\when \gas¬sim¬state_{\imath} \neq \none \land \cost¬decodeslots(\mathbf{c}, \mathbf{k}, \gas¬sim¬state_{\imath}) \leq \gas¬sim¬state_{\remaining¬decodeslots} \land l < 32 \\
-      \gas¬sim(\mathbf{c}, \mathbf{k}, \gas¬sim''(\gas¬sim¬state)) &\otherwhen \find¬readytostart(\gas¬sim¬state) \neq \none \land \gas¬sim¬state_{\remaining¬startpercycle} > 0 \\
+    \tuple{\blob, \bitstring, \workingsetsize, \gas¬sim¬ty} &\to \gas¬sim¬ty \\
+    \tup{\mathbf{c}, \mathbf{k}, w, \gas¬sim¬state} &\mapsto \begin{cases}
+      \gas¬sim(\mathbf{c}, \mathbf{k}, w, \gas¬sim'(\mathbf{c}, \mathbf{k}, w, \gas¬sim¬state)) &\when \gas¬sim¬state_{\imath} \neq \none \land \cost¬decodeslots(\mathbf{c}, \mathbf{k}, \gas¬sim¬state_{\imath}) \leq \gas¬sim¬state_{\remaining¬decodeslots} \land l < 32 \\
+      \gas¬sim(\mathbf{c}, \mathbf{k}, w, \gas¬sim''(\gas¬sim¬state)) &\otherwhen \find¬readytostart(\gas¬sim¬state) \neq \none \land \gas¬sim¬state_{\remaining¬startpercycle} > 0 \\
       \gas¬sim¬state &\otherwhen \gas¬sim¬state_{\imath} = \none \land l = 0 \\
-      \gas¬sim(\mathbf{c}, \mathbf{k}, \gas¬sim'''(\gas¬sim¬state)) &\otherwise \\
+      \gas¬sim(\mathbf{c}, \mathbf{k}, w, \gas¬sim'''(\gas¬sim¬state)) &\otherwise \\
     \end{cases}\\
     \where l &= \len{\sq{\build{r}{ r \orderedin \in¬rob, r_{\rob¬state} \neq \none }}}
   }
@@ -1024,10 +1047,10 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
 
 \begin{equation}
   \gas¬sim'\colon \abracegroup{
-    \tup{\blob, \bitstring, \gas¬sim¬ty} &\to \gas¬sim¬ty \\
-    \tup{\mathbf{c}, \mathbf{k}, \gas¬sim¬state} &\mapsto \begin{cases}
+    \tuple{\blob, \bitstring, \workingsetsize, \gas¬sim¬ty} &\to \gas¬sim¬ty \\
+    \tup{\mathbf{c}, \mathbf{k}, w, \gas¬sim¬state} &\mapsto \begin{cases}
       \gas¬sim^{\text{mov}}(\mathbf{c}, \mathbf{k}, \gas¬sim¬state) &\when \imath < \len{\mathbf{c}} \land \mathbf{c}_{\imath} = \token{move\_reg} \\
-      \gas¬sim^{\text{dec}}(\mathbf{c}, \mathbf{k}, \gas¬sim¬state) &\otherwise
+      \gas¬sim^{\text{dec}}(\mathbf{c}, \mathbf{k}, w, \gas¬sim¬state) &\otherwise
     \end{cases}
   }
 \end{equation}
@@ -1036,7 +1059,7 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
 
 \begin{equation}
   \gas¬sim^{\text{mov}}\colon \abracegrouptwo{
-    \tup{\blob, \bitstring, \gas¬sim¬ty} &\to \gas¬sim¬ty \\
+    \tuple{\blob, \bitstring, \gas¬sim¬ty} &\to \gas¬sim¬ty \\
     \tup{\mathbf{c}, \mathbf{k}, \gas¬sim¬state} &\mapsto \gas¬sim¬state'
   }{
     \where \gas¬sim¬state' &= \gas¬sim¬state\text{ except:}\\
@@ -1056,8 +1079,8 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
 
 \begin{equation}
   \gas¬sim^{\text{dec}}\colon \abracegrouptwo{
-    \tup{\blob, \bitstring, \gas¬sim¬ty} &\to \gas¬sim¬ty \\
-    \tup{\mathbf{c}, \mathbf{k}, \gas¬sim¬state} &\mapsto \gas¬sim¬state'
+    \tuple{\blob, \bitstring, \workingsetsize, \gas¬sim¬ty} &\to \gas¬sim¬ty \\
+    \tup{\mathbf{c}, \mathbf{k}, w, \gas¬sim¬state} &\mapsto \gas¬sim¬state'
   }{
     \where \gas¬sim¬state' &= \gas¬sim¬state\text{ except:}\\
     \gas¬sim¬state'_{\imath} &= \begin{cases}
@@ -1068,7 +1091,7 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
     \gas¬sim¬state'_{\remaining¬decodeslots} &= \gas¬sim¬state_{\remaining¬decodeslots} - \cost¬decodeslots(\mathbf{c}, \mathbf{k}, \gas¬sim¬state_{\imath}) \\
     \rob &= \in¬rob\text{ except: } \forall j \in \in¬rob¬len : \rob¬entry¬field{\rob}{j}{\rob¬regs} = \in¬rob¬field{j}{\rob¬regs} \setminus \rob¬regs\\
     \rob¬regs &= \inst¬dstregs(\mathbf{c}, \mathbf{k}, \gas¬sim¬state_{\imath}) \\
-    \rob¬cyclesleft &= \cost¬cycles(\mathbf{c}, \mathbf{k}, \gas¬sim¬state_{\imath}) \\
+    \rob¬cyclesleft &= \cost¬cycles(\mathbf{c}, \mathbf{k}, w, \gas¬sim¬state_{\imath}) \\
     \rob¬execunits &= \cost¬execunits(\mathbf{c}, \mathbf{k}, \gas¬sim¬state_{\imath}) \\
     \rob¬deps &= \set{\build{i}{ i \in \in¬rob¬len, \inst¬srcregs(\mathbf{c}, \mathbf{k}, \gas¬sim¬state_{\imath}) \cap \in¬rob¬field{i}{\rob¬regs} \neq \emptyset }} \\
     \gas¬sim¬state'_{\rob} &= \rob \append \tuple{\state¬decoding, \rob¬cyclesleft, \rob¬deps, \rob¬regs, \rob¬execunits} \\
@@ -1131,6 +1154,51 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
   }
 \end{equation}
 
+\subsection{Working-Set Changes}\label{sec:workingsetchanges}
+
+In addition to the static gas cost of each basic block as calculated by $\gascostforblock$, gas is charged dynamically whenever a memory page outside of the current working-set is accessed. Such an access implicitly adds the accessed page to the working-set, pushing another page out if necessary. The function $\gascostforpageaccess$ determines the working-set change, if any, required to access a page $p \in \pageid$, and the corresponding gas cost.
+\begin{equation}
+  \gascostforpageaccess\colon \abracegroup{
+    \tuple{\sequence{\optional{\pageid}}, \pageid} &\to \tuple{\gas, \sequence{\optional{\pageid}}} \\
+    \tup{\workingset, p} &\mapsto \begin{cases}
+      (0, \workingset) &\when p \in \workingset \\
+      (\text{TODO}, \workingset\sub{1\dots} \append p) &\otherwise
+    \end{cases}
+  }
+\end{equation}
+
+This mechanism applies to explicit data accesses, via instructions such as \token{load\_u8}, as well as to the implicit reading of instructions by the machine. The instructions for a machine are not present in its \textsc{ram} $\memory$, and so instruction addresses cannot be mapped to regular page indices. For the sole purpose of this mechanism, we define a function $\pageforinstruction$ which maps instruction addresses to special page indices $\codepage{\N} \equiv \set{\build{\codepage{n}}{n \in \N}}$:
+\begin{equation}
+  \pageforinstruction\colon \abracegroup{
+    &\tuple{\blob, \bitstring, \pvmreg} \to \codepage{\N} \\
+    &\tup{\mathbf{c}, \mathbf{k}, \imath} \mapsto \codepage{\floor{\frac{A(0, 0)}{\Cpvmpagesize}}} \\
+    &\quad\where A(i, s) \equiv \begin{cases}
+      s - 1 &\when i > \imath \\
+      A(i + 1 + \text{skip}(i), B(s, N(i))) &\otherwise
+    \end{cases} \\
+    % Maximum compiled size of the instruction at address i, including any immediately
+    % preceding basic block preamble
+    &\quad\also N(i) \equiv \inst¬compiledsize(\mathbf{c}, \mathbf{k}, i) + \begin{cases}
+      \text{TODO} &\when i \in \basicblocks \\
+      0 &\otherwise
+    \end{cases} \\
+    % Bump s by n bytes, jumping to the next page boundary first if the n bytes would otherwise
+    % straddle it
+    &\quad\also B(s, n) \equiv \begin{cases}
+      s + n &\when n \le \Cpvmpagesize - (s \rem \Cpvmpagesize) \\
+      \Cpvmpagesize \floor{\frac{s}{\Cpvmpagesize}} + \Cpvmpagesize + n &\otherwise
+    \end{cases}
+  }
+\end{equation}
+
+$\pageforinstruction$ is defined under the assumption that \textsc{pvm} program code is translated into native code for execution. It utilises the function $\inst¬compiledsize(\mathbf{c}, \mathbf{k}, \imath)$, which returns the size of the native code translation of the \textsc{pvm} instruction at address $\imath$. The values returned by $\inst¬compiledsize$ are specified in section \ref{sec:gascosttables}. Allowance is also made by $\pageforinstruction$ for a small section of native code at the start of each basic block, to charge gas according to $\gascostforblock$.
+
+The working-set is shared with inner \textsc{pvm} instances. For this reason, page identifiers characterized by the set $\pageid$ consist of a machine identifier $\pid¬machine$ in addition to a page index $\pid¬index$. $\none$ is used to identify the top-level \textsc{pvm} instance.
+\begin{equation}
+  \label{eq:pageid}
+  \pageid \equiv \tuple{\isa{\pid¬machine}{\optional{\N}}, \isa{\pid¬index}{\N \cup \codepage{\N}}}
+\end{equation}
+
 \subsection{Gas Cost Tables}\label{sec:gascosttables}
 
 For some of the instructions their cost depends on whether the destination register overlaps with any of the source registers:
@@ -1160,15 +1228,16 @@ \subsection{Gas Cost Tables}\label{sec:gascosttables}
   }
 \end{equation}
 
-% NOTE: This is a *temporary* placeholder. We'll later replace this with a proper equation
-%       once we introduce gas metering of the paging mechanism and memory limits,
-%       so that's why I'm not inlining this into the table.
-The cost of memory accesses is defined as follows:
+The cost of memory accesses depends on the size of the working-set $w$ and is defined as follows:
 
 \begin{equation}
-  \mathfrak{m} \equiv 25
+  \mathfrak{m}\colon \abracegroup{
+      \workingsetsize &\to \N \\
+      w &\mapsto \text{TODO}
+  }
 \end{equation}
 
+% TODO: Should the cost of a branch also depend on the working-set size?
 The cost of a branch depends on whether any of its targets (either the jump target or the implicit fallthrough) point to an instruction byte which is equal to the opcode for the \token{unlikely} or the \token{trap} instruction; formally:
 
 \begin{equation}
@@ -1191,41 +1260,41 @@ \subsection{Gas Cost Tables}\label{sec:gascosttables}
 \newcommand*{\storecost}{25}
 \newcommand*{\branchcost}{$\mathfrak{b}$}
 
-\newcommand*{\simplealuthreeop}{1&\ifdstandsrcoverlap{1}{2}&1&0&0&0&0}
-\newcommand*{\simplealuthreeopthirtytwo}{2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0}
-\newcommand*{\simplealutwoop}{1&\ifdstandsrcoverlap{1}{2}&1&0&0&0&0}
-\newcommand*{\simplealutwoopthirtytwo}{2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0}
-\newcommand*{\trivialtwooponecycle}{1&1&1&0&0&0&0}
-\newcommand*{\trivialtwooptwocycles}{2&1&2&0&0&0&0}
-\newcommand*{\shiftsandrotates}{1&\ifdstandsrcoverlapshift{2}{3}&1&0&0&0&0}
-\newcommand*{\shiftsandrotatesthirtytwo}{2&\ifdstandsrcoverlapshift{3}{4}&1&0&0&0&0}
-\newcommand*{\shiftsandrotatesalt}{1&3&1&0&0&0&0}
-\newcommand*{\shiftsandrotatesaltthirtytwo}{2&4&1&0&0&0&0}
-\newcommand*{\regcomp}{3&3&1&0&0&0&0}
-\newcommand*{\regcompimm}{3&3&1&0&0&0&0}
-\newcommand*{\cmov}{2&2&1&0&0&0&0}
-\newcommand*{\cmovimm}{2&3&1&0&0&0&0}
-\newcommand*{\minmax}{3&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0}
-\newcommand*{\indirectload}{\loadcost&1&1&1&0&0&0}
-\newcommand*{\directload}{\loadcost&1&1&1&0&0&0}
-\newcommand*{\indirectstoreimm}{\storecost&1&1&0&1&0&0}
-\newcommand*{\indirectstore}{\storecost&1&1&0&1&0&0}
-\newcommand*{\storeimm}{\storecost&1&1&0&1&0&0}
-\newcommand*{\directstore}{\storecost&1&1&0&1&0&0}
-\newcommand*{\branch}{\branchcost&1&1&0&0&0&0}
-\newcommand*{\branchimm}{\branchcost&1&1&0&0&0&0}
-\newcommand*{\divrem}{60&4&1&0&0&0&1}
-\newcommand*{\finish}[1]{#1&1&0&0&0&0&0}
-
-In the following table the $\mathbf{c}$, $\mathbf{k}$, and $\imath$ arguments are omitted for clarity.
-
-\renewcommand*{\mrule}{\cmidrule(lr){1-8}}
-\begin{longtable}[t]{p{30mm} p{12mm} p{12mm} p{4mm} p{4mm} p{4mm} p{4mm} p{4mm}}
+\newcommand*{\simplealuthreeop}{1&\ifdstandsrcoverlap{1}{2}&1&0&0&0&0&?}
+\newcommand*{\simplealuthreeopthirtytwo}{2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0&?}
+\newcommand*{\simplealutwoop}{1&\ifdstandsrcoverlap{1}{2}&1&0&0&0&0&?}
+\newcommand*{\simplealutwoopthirtytwo}{2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0&?}
+\newcommand*{\trivialtwooponecycle}{1&1&1&0&0&0&0&?}
+\newcommand*{\trivialtwooptwocycles}{2&1&2&0&0&0&0&?}
+\newcommand*{\shiftsandrotates}{1&\ifdstandsrcoverlapshift{2}{3}&1&0&0&0&0&?}
+\newcommand*{\shiftsandrotatesthirtytwo}{2&\ifdstandsrcoverlapshift{3}{4}&1&0&0&0&0&?}
+\newcommand*{\shiftsandrotatesalt}{1&3&1&0&0&0&0&?}
+\newcommand*{\shiftsandrotatesaltthirtytwo}{2&4&1&0&0&0&0&?}
+\newcommand*{\regcomp}{3&3&1&0&0&0&0&?}
+\newcommand*{\regcompimm}{3&3&1&0&0&0&0&?}
+\newcommand*{\cmov}{2&2&1&0&0&0&0&?}
+\newcommand*{\cmovimm}{2&3&1&0&0&0&0&?}
+\newcommand*{\minmax}{3&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0&?}
+\newcommand*{\indirectload}{\loadcost&1&1&1&0&0&0&?}
+\newcommand*{\directload}{\loadcost&1&1&1&0&0&0&?}
+\newcommand*{\indirectstoreimm}{\storecost&1&1&0&1&0&0&?}
+\newcommand*{\indirectstore}{\storecost&1&1&0&1&0&0&?}
+\newcommand*{\storeimm}{\storecost&1&1&0&1&0&0&?}
+\newcommand*{\directstore}{\storecost&1&1&0&1&0&0&?}
+\newcommand*{\branch}{\branchcost&1&1&0&0&0&0&?}
+\newcommand*{\branchimm}{\branchcost&1&1&0&0&0&0&?}
+\newcommand*{\divrem}{60&4&1&0&0&0&1&?}
+\newcommand*{\finish}[1]{#1&1&0&0&0&0&0&?}
+
+In the following table the $\mathbf{c}$, $\mathbf{k}$, $w$, and $\imath$ arguments are omitted for clarity.
+
+\renewcommand*{\mrule}{\cmidrule(lr){1-9}}
+\begin{longtable}[t]{p{30mm} p{12mm} p{12mm} p{4mm} p{4mm} p{4mm} p{4mm} p{4mm} p{4mm}}
   \toprule
-  \thead{\textbf{Instruction}} & \thead{$\cost¬cycles$} & \thead{$\cost¬decodeslots$} & \thead{$\cost¬execunits_{\ALU}$} & \thead{$\cost¬execunits_{\LOAD}$} & \thead{$\cost¬execunits_{\STORE}$} & \thead{$\cost¬execunits_{\MUL}$} & \thead{$\cost¬execunits_{\DIV}$} \\
+  \thead{\textbf{Instruction}} & \thead{$\cost¬cycles$} & \thead{$\cost¬decodeslots$} & \thead{$\cost¬execunits_{\ALU}$} & \thead{$\cost¬execunits_{\LOAD}$} & \thead{$\cost¬execunits_{\STORE}$} & \thead{$\cost¬execunits_{\MUL}$} & \thead{$\cost¬execunits_{\DIV}$} & \thead{$\inst¬compiledsize$} \\
   \midrule
   \endhead
-  \token{move\_reg}&0&1&0&0&0&0&0 \\ \mrule
+  \token{move\_reg}&0&1&0&0&0&0&0&? \\ \mrule
 
   \token{and}&\simplealuthreeop \\ \mrule
   \token{xor}&\simplealuthreeop \\ \mrule
@@ -1366,30 +1435,30 @@ \subsection{Gas Cost Tables}\label{sec:gascosttables}
   \token{rem\_u\_64}&\divrem \\ \mrule
   \token{rem\_s\_64}&\divrem \\ \mrule
 
-  \token{and\_inv}&2&3&1&0&0&0&0\\ \mrule
-  \token{or\_inv}&2&3&1&0&0&0&0\\ \mrule
-  \token{xnor}&2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0\\ \mrule
-  \token{neg\_add\_imm\_64}&2&3&1&0&0&0&0\\ \mrule
-  \token{neg\_add\_imm\_32}&3&4&1&0&0&0&0\\ \mrule
-  \token{load\_imm}&1&1&0&0&0&0&0\\ \mrule
-  \token{load\_imm\_64}&1&2&0&0&0&0&0\\ \mrule
-
-  \token{mul\_64}&3&\ifdstandsrcoverlap{1}{2}&1&0&0&1&0\\ \mrule
-  \token{mul\_32}&4&\ifdstandsrcoverlap{2}{3}&1&0&0&1&0\\ \mrule
-  \token{mul\_imm\_64}&3&\ifdstandsrcoverlap{1}{2}&1&0&0&1&0\\ \mrule
-  \token{mul\_imm\_32}&4&\ifdstandsrcoverlap{2}{3}&1&0&0&1&0\\ \mrule
-  \token{mul\_upper\_s\_s}&4&4&1&0&0&1&0\\ \mrule
-  \token{mul\_upper\_u\_u}&4&4&1&0&0&1&0\\ \mrule
-  \token{mul\_upper\_s\_u}&6&4&1&0&0&1&0\\ \mrule
+  \token{and\_inv}&2&3&1&0&0&0&0&?\\ \mrule
+  \token{or\_inv}&2&3&1&0&0&0&0&?\\ \mrule
+  \token{xnor}&2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0&?\\ \mrule
+  \token{neg\_add\_imm\_64}&2&3&1&0&0&0&0&?\\ \mrule
+  \token{neg\_add\_imm\_32}&3&4&1&0&0&0&0&?\\ \mrule
+  \token{load\_imm}&1&1&0&0&0&0&0&?\\ \mrule
+  \token{load\_imm\_64}&1&2&0&0&0&0&0&?\\ \mrule
+
+  \token{mul\_64}&3&\ifdstandsrcoverlap{1}{2}&1&0&0&1&0&?\\ \mrule
+  \token{mul\_32}&4&\ifdstandsrcoverlap{2}{3}&1&0&0&1&0&?\\ \mrule
+  \token{mul\_imm\_64}&3&\ifdstandsrcoverlap{1}{2}&1&0&0&1&0&?\\ \mrule
+  \token{mul\_imm\_32}&4&\ifdstandsrcoverlap{2}{3}&1&0&0&1&0&?\\ \mrule
+  \token{mul\_upper\_s\_s}&4&4&1&0&0&1&0&?\\ \mrule
+  \token{mul\_upper\_u\_u}&4&4&1&0&0&1&0&?\\ \mrule
+  \token{mul\_upper\_s\_u}&6&4&1&0&0&1&0&?\\ \mrule
 
   \token{trap}&\finish{2} \\ \mrule
   \token{fallthrough}&\finish{2}\\ \mrule
-  \token{unlikely}&40&1&0&0&0&0&0\\ \mrule
+  \token{unlikely}&40&1&0&0&0&0&0&?\\ \mrule
   \token{jump}&\finish{15}\\ \mrule
   \token{load\_imm\_jump}&\finish{15}\\ \mrule
-  \token{jump\_ind}&22&1&0&0&0&0&0\\ \mrule
-  \token{load\_imm\_jump\_ind}&22&1&0&0&0&0&0\\ \mrule
+  \token{jump\_ind}&22&1&0&0&0&0&0&?\\ \mrule
+  \token{load\_imm\_jump\_ind}&22&1&0&0&0&0&0&?\\ \mrule
 
-  \token{ecalli}&100&4&1&0&0&0&0\\
+  \token{ecalli}&100&4&1&0&0&0&0&?\\
 \bottomrule
 \end{longtable}
diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index 58f116b2..07fcc0f8 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -40,16 +40,16 @@ \subsection{Is-Authorized Invocation}\label{sec:isauthorizedinvocation}
       \tup{\token{BAD}, 0} &\when \wpX_\wp¬authcode = \none \\
       \tup{\token{BIG}, 0} &\otherwhen \len{\wpX_\wp¬authcode} > \Cmaxauthcodesize \\
       \tup{\mathbf{r}, u} &\otherwise \\
-      \multicolumn{2}{l}{\where \tup{u, \mathbf{r}, \none} = \Psi_M(\wpX_\wp¬authcode, 0, \Cpackageauthgas, \encode[2]{c}, F, \none)}\\
+      \multicolumn{2}{l}{\where \tup{u, \mathbf{r}, \none} = \Psi_M(\wpX_\wp¬authcode, 0, \Cpackageauthgas, \encode[2]{c}, \wpX_\wp¬authworkingsetsize, F, \none)}\\
     \end{cases}\\
   } \\
   \label{eq:isauthorizedmutator}F \in \contextmutator{\emset} &\colon
-    \tup{n, \gascounter, \registers, \memory} \mapsto \begin{cases}
-      \Omega_G(\gascounter, \registers, \memory) &\when n = \mathtt{gas} \\
-      \Omega_\Gemini(\gascounter, \registers, \memory, \wpX_\wp¬authcode) &\when n = \mathtt{grow\_heap} \\
-      \Omega_Y(\gascounter, \registers, \memory, \wpX, \none, \none, \none, \none, \none, \none, \none) &\when n = \mathtt{fetch} \\
-      \tup{\oog, \gascounter', \registers', \memory} &\otherwhen \gascounter' < 0 \\
-      \tup{\continue, \gascounter', \registers', \memory} &\otherwise \\
+    \tup{n, \gascounter, \registers, \memory, \workingset} \mapsto \begin{cases}
+      \Omega_G(\gascounter, \registers, \memory, \workingset) &\when n = \mathtt{gas} \\
+      \Omega_\Gemini(\gascounter, \registers, \memory, \workingset, \wpX_\wp¬authcode) &\when n = \mathtt{grow\_heap} \\
+      \Omega_Y(\gascounter, \registers, \memory, \workingset, \wpX, \none, \none, \none, \none, \none, \none, \none) &\when n = \mathtt{fetch} \\
+      \tup{\oog, \gascounter', \registers', \memory, \workingset} &\otherwhen \gascounter' < 0 \\
+      \tup{\continue, \gascounter', \registers', \memory, \workingset} &\otherwise \\
       \multicolumn{2}{l}{\where \registers' = \registers \exc \registers'_7 = \mathtt{WHAT}} \\
       \multicolumn{2}{l}{\also \gascounter' = \gascounter - 10}
     \end{cases}
@@ -75,8 +75,8 @@ \subsection{Refine Invocation}\label{sec:refineinvocation}
 The Export host-call depends on two pieces of context; one sequence of segments (blobs of length $\Csegmentsize$) to which it may append, and the other an argument passed to the invocation function to dictate the number of segments prior which may assumed to have already been appended. The latter value ensures that an accurate segment index can be provided to the caller.
 
 Unlike the other invocation functions, the Refine invocation function implicitly draws upon some recent service account state item $\accounts$. The specific block from which this comes is not important, as long as it is no earlier than its work-package's lookup-anchor block. It explicitly accepts the work-package $p$ and the index of the work item to be refined, $i$ together with the core which is doing the refining $c$. Additionally, the authorizer trace $\mathbf{r}$ is provided together with all work items' import segments $\overline{\mathbf{i}}$ and an export segment offset $\segoff$. It results in a tuple of some error $\workerror$ or the refinement output blob (signalling success), the export sequence in the case of success and the gas used in evaluation. Formally:
-\begin{align}
-  &\Psi_R \colon \abracegroup{
+\begin{gather}
+  \Psi_R \colon \abracegroup{
     \label{eq:refinvocation}
     \tuple{\coreindex, \N, \workpackage, \blob, \sequence{\sequence{\segment}}, \N} &\to \tuple{\blob \cup \workerror, \sequence{\segment}, \gas} \\
     \tup{c, i, p, \mathbf{r}, \overline{\mathbf{i}}, \segoff} &\mapsto \begin{cases}
@@ -84,28 +84,28 @@ \subsection{Refine Invocation}\label{sec:refineinvocation}
       \tup{\token{BIG}, \sq{}, 0} &\otherwhen \len{\histlookup(\accounts\subb{w_\wi¬serviceindex}, (p_\wp¬context)_\wc¬lookupanchortime, w_\wi¬codehash)} > \Cmaxservicecodesize \\
       &\otherwise: \\
       &\quad\using \mathbf{a} = \encode{c, i, w_\wi¬serviceindex, \var{w_\wi¬payload}, \blake{p}}\;,\ \encode{\var{\mathbf{z}}, \jam¬blob} = \histlookup(\accounts\subb{w_\wi¬serviceindex}, (p_\wp¬context)_\wc¬lookupanchortime, w_\wi¬codehash)\\
-      &\quad\also \tup{u, \mathbf{o}, \tup{\mathbf{m}, \mathbf{e}}} = \Psi_M(\jam¬blob, 0, w_\wi¬refgaslimit, \mathbf{a}, F, \tup{\emptyset, \sq{}})\ \colon\\
+      &\quad\also \tup{u, \mathbf{o}, \tup{\mathbf{m}, \mathbf{e}}} = \Psi_M(\jam¬blob, 0, w_\wi¬refgaslimit, \mathbf{a}, w_\wi¬refworkingsetsize, F, \tup{\emptyset, \sq{}})\ \colon\\
       \tup{\mathbf{o}, \sq{}, u} &\quad\when \mathbf{o} \in \set{ \oog, \panic }  \\
       \tup{\mathbf{o}, \mathbf{e}, u} &\quad\otherwise \\
       \multicolumn{2}{l}{\where w = p_\wp¬workitems\subb{i}}
     \end{cases} \\
   } \\
   \label{eq:refinemutator}
-  &F \in \contextmutator{\tuple{\dictionary{\N}{\innerpvm}, \sequence{\segment}}} \colon
-    (n, \gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}) \mapsto \begin{cases}
-      \Omega_G(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{gas} \\
-      \Omega_\Gemini(\gascounter, \registers, \memory, \jam¬blob) &\when n = \mathtt{grow\_heap} \\
-      \Omega_Y(\gascounter, \registers, \memory, p, \zerohash, \mathbf{r}, i, \overline{\mathbf{i}}, \overline{\mathbf{x}}, \none, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{fetch}\\
-      \Omega_H(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}, w_\wi¬serviceindex, \accounts, (p_\wp¬context)_\wc¬lookupanchortime) &\when n = \mathtt{historical\_lookup}\\
-      \Omega_E(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}, \segoff) &\when n = \mathtt{export}\\
-      \Omega_M(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{machine}\\
-      \Omega_P(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{peek}\\
-      \Omega_O(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{poke}\\
-      \Omega_Z(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{pages}\\
-      \Omega_K(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{invoke}\\
-      \Omega_X(\gascounter, \registers, \memory, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{expunge}\\
-      \tup{\oog, \gascounter', \registers', \memory} &\otherwhen \gascounter' < 0\\
-      \tup{\continue, \gascounter', \registers', \memory} &\otherwise\\
+  F \in \contextmutator{\tuple{\dictionary{\N}{\innerpvm}, \sequence{\segment}}} \colon
+    (n, \gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}) \mapsto \begin{cases}
+      \Omega_G(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{gas} \\
+      \Omega_\Gemini(\gascounter, \registers, \memory, \workingset, \jam¬blob) &\when n = \mathtt{grow\_heap} \\
+      \Omega_Y(\gascounter, \registers, \memory, \workingset, p, \zerohash, \mathbf{r}, i, \overline{\mathbf{i}}, \overline{\mathbf{x}}, \none, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{fetch}\\
+      \Omega_H(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}, w_\wi¬serviceindex, \accounts, (p_\wp¬context)_\wc¬lookupanchortime) &\when n = \mathtt{historical\_lookup}\\
+      \Omega_E(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}, \segoff) &\when n = \mathtt{export}\\
+      \Omega_M(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{machine}\\
+      \Omega_P(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{peek}\\
+      \Omega_O(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{poke}\\
+      \Omega_Z(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{pages}\\
+      \Omega_K(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{invoke}\\
+      \Omega_X(\gascounter, \registers, \memory, \workingset, \tup{\mathbf{m}, \mathbf{e}}) &\when n = \mathtt{expunge}\\
+      \tup{\oog, \gascounter', \registers', \memory, \workingset} &\otherwhen \gascounter' < 0\\
+      \tup{\continue, \gascounter', \registers', \memory, \workingset} &\otherwise\\
       \multicolumn{2}{l}{\where \registers' = \registers \exc \registers'_7 = \mathtt{WHAT}} \\
       \multicolumn{2}{l}{\also \gascounter' = \gascounter - 10} \\
       \multicolumn{2}{l}{\also \overline{\mathbf{x}} = \sq{\build{
@@ -118,7 +118,7 @@ \subsection{Refine Invocation}\label{sec:refineinvocation}
         \wiX \orderedin p_\wp¬workitems
       }}}
     \end{cases}
-\end{align}
+\end{gather}
 
 \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
 
@@ -162,10 +162,11 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
         \is{\ao¬provisions}{\sq{}}
       }
         &\when \jam¬blob = \none \vee \len{\jam¬blob} > \Cmaxservicecodesize \\
-      C(\Psi_M(\jam¬blob, 5, g, \encode{t, s, \len{\mathbf{i}}}, F, I(\local¬postxferstate, s)^2))
+      C(\Psi_M(\jam¬blob, 5, g, \encode{t, s, \len{\mathbf{i}}}, w, F, I(\local¬postxferstate, s)^2))
         &\otherwise \\
       \begin{aligned}
         &\quad\where \jam¬blob = \local¬basestate_\ps¬accounts\subb{s}_\sa¬code\\
+        &\quad\also w = \local¬basestate_\ps¬accounts\subb{s}_\sa¬accworkingsetsize\\
         &\quad\also \local¬postxferstate = \local¬basestate \exc \local¬postxferstate_\ps¬accounts\subb{s}_\sa¬balance = \local¬basestate_\ps¬accounts\subb{s}_\sa¬balance + \sum_{r \in \mathbf{x}}r_\dx¬amount\\
         &\quad\also \mathbf{x} = \sq{\build{i}{
           i \orderedin \mathbf{i} ,
@@ -186,35 +187,35 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
     }\\
     &\qquad\where \im¬nextfreeid = \text{check}((\decode[4]{\blake{\encode{\im¬id, \entropyaccumulator', \H_\¬timeslot}}} \bmod (2^{32}-\Cminpublicindex-2^8)) + \Cminpublicindex) \\
   }\\
-  F \in \contextmutator{\implicationspair} &\colon \tup{n, \gascounter, \registers, \memory, \imXY} \mapsto \begin{cases}
-  \Omega_G(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{gas} \\
-    \Omega_\Gemini(\gascounter, \registers, \memory, \jam¬blob) &\when n = \mathtt{grow\_heap} \\
-    \Omega_Y(\gascounter, \registers, \memory, \none, \entropyaccumulator', \none, \none, \none, \none, \mathbf{i}, \imXY) &\when n = \mathtt{fetch}\\
-    G(\Omega_R(\gascounter, \registers, \memory, \imX_\im¬self, \imX_\im¬id, (\imX_\im¬state)_\ps¬accounts), \imXY) &\when n = \mathtt{read} \\
-    G(\Omega_W(\gascounter, \registers, \memory, \imX_\im¬self, \imX_\im¬id), \imXY) &\when n = \mathtt{write} \\
-    G(\Omega_L(\gascounter, \registers, \memory, \imX_\im¬self, \imX_\im¬id, (\imX_\im¬state)_\ps¬accounts), \imXY) &\when n = \mathtt{lookup} \\
-    G(\Omega_I(\gascounter, \registers, \memory, \imX_\im¬id, (\imX_\im¬state)_\ps¬accounts), \imXY) &\when n = \mathtt{info} \\
-    \Omega_B(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{bless}\\
-    \Omega_A(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{assign}\\
-    \Omega_D(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{designate}\\
-    \Omega_C(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{checkpoint} \\
-    \Omega_N(\gascounter, \registers, \memory, \imXY, \H_\¬timeslot) &\when n = \mathtt{new} \\
-    \Omega_U(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{upgrade} \\
-    \Omega_T(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{transfer} \\
-    \Omega_J(\gascounter, \registers, \memory, \imXY, \H_\¬timeslot) &\when n = \mathtt{eject} \\
-    \Omega_Q(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{query} \\
-    \Omega_S(\gascounter, \registers, \memory, \imXY, \H_\¬timeslot) &\when n = \mathtt{solicit} \\
-    \Omega_F(\gascounter, \registers, \memory, \imXY, \H_\¬timeslot) &\when n = \mathtt{forget} \\
-    \Omega_\Taurus(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{yield} \\
-    \Omega_\Aries(\gascounter, \registers, \memory, \imXY) &\when n = \mathtt{provide} \\
-    \tup{\oog, \gascounter', \registers', \memory, \imXY} &\otherwhen \gascounter' < 0\\
-    \tup{\continue, \gascounter', \registers', \memory, \imXY} &\otherwise\\
+  F \in \contextmutator{\implicationspair} &\colon \tup{n, \gascounter, \registers, \memory, \workingset, \imXY} \mapsto \begin{cases}
+  \Omega_G(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{gas} \\
+    \Omega_\Gemini(\gascounter, \registers, \memory, \workingset, \jam¬blob) &\when n = \mathtt{grow\_heap} \\
+    \Omega_Y(\gascounter, \registers, \memory, \workingset, \none, \entropyaccumulator', \none, \none, \none, \none, \mathbf{i}, \imXY) &\when n = \mathtt{fetch}\\
+    G(\Omega_R(\gascounter, \registers, \memory, \workingset, \imX_\im¬self, \imX_\im¬id, (\imX_\im¬state)_\ps¬accounts), \imXY) &\when n = \mathtt{read} \\
+    G(\Omega_W(\gascounter, \registers, \memory, \workingset, \imX_\im¬self, \imX_\im¬id), \imXY) &\when n = \mathtt{write} \\
+    G(\Omega_L(\gascounter, \registers, \memory, \workingset, \imX_\im¬self, \imX_\im¬id, (\imX_\im¬state)_\ps¬accounts), \imXY) &\when n = \mathtt{lookup} \\
+    G(\Omega_I(\gascounter, \registers, \memory, \workingset, \imX_\im¬id, (\imX_\im¬state)_\ps¬accounts), \imXY) &\when n = \mathtt{info} \\
+    \Omega_B(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{bless}\\
+    \Omega_A(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{assign}\\
+    \Omega_D(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{designate}\\
+    \Omega_C(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{checkpoint} \\
+    \Omega_N(\gascounter, \registers, \memory, \workingset, \imXY, \H_\¬timeslot) &\when n = \mathtt{new} \\
+    \Omega_U(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{upgrade} \\
+    \Omega_T(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{transfer} \\
+    \Omega_J(\gascounter, \registers, \memory, \workingset, \imXY, \H_\¬timeslot) &\when n = \mathtt{eject} \\
+    \Omega_Q(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{query} \\
+    \Omega_S(\gascounter, \registers, \memory, \workingset, \imXY, \H_\¬timeslot) &\when n = \mathtt{solicit} \\
+    \Omega_F(\gascounter, \registers, \memory, \workingset, \imXY, \H_\¬timeslot) &\when n = \mathtt{forget} \\
+    \Omega_\Taurus(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{yield} \\
+    \Omega_\Aries(\gascounter, \registers, \memory, \workingset, \imXY) &\when n = \mathtt{provide} \\
+    \tup{\oog, \gascounter', \registers', \memory, \workingset, \imXY} &\otherwhen \gascounter' < 0\\
+    \tup{\continue, \gascounter', \registers', \memory, \workingset, \imXY} &\otherwise\\
     \multicolumn{2}{l}{\where \registers' = \registers \exc \registers'_7 = \mathtt{WHAT}} \\
     \multicolumn{2}{l}{\also \gascounter' = \gascounter - 10}
   \end{cases} \\
   G&\colon\abracegroup{
-    \tuple{\tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \serviceaccount}, \implicationspair} &\to \tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \implicationspair} \\
-    \tup{\tup{\execst, \gascounter, \registers, \memory, \mathbf{s}}, \imXY} &\mapsto \tup{\execst, \gascounter, \registers, \memory, \tup{\imX^*, \imY}} \\
+    \tuple{\tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \sequence{\optional{\pageid}}, \serviceaccount}, \implicationspair} &\to \tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \implicationspair} \\
+    \tup{\tup{\execst, \gascounter, \registers, \memory, \workingset, \mathbf{s}}, \imXY} &\mapsto \tup{\execst, \gascounter, \registers, \memory, \workingset, \tup{\imX^*, \imY}} \\
     &\qquad \where \imX^* = \imX \exc \imX^*_\im¬self = \mathbf{s}
   }\\
   C&\colon\abracegroup{
@@ -272,16 +273,16 @@ \subsection{General Functions}\label{sec:generalfunctions}
 
 We come now to defining the host functions which are utilized by the \textsc{pvm} invocations. Generally, these map some \textsc{pvm} state, including invocation context, possibly together with some additional parameters, to a new \textsc{pvm} state.
 
-The general functions are all broadly of the form $\tup{\gascounter' \in \signedgas, \registers' \in \regs, \memory' \in \ram} = \Omega_\square(\gascounter \in \gas, \registers \in \regs, \memory \in \ram)$. Functions which have a result component which is equivalent to the corresponding argument may have said components elided in the description. Functions may also depend upon particular additional parameters.
+The general functions are all broadly of the form $\tup{\gascounter' \in \signedgas, \registers' \in \regs, \memory' \in \ram, \workingset' \in \sequence{\optional{\pageid}}} = \Omega_\square(\gascounter \in \gas, \registers \in \regs, \memory \in \ram, \workingset \in \sequence{\optional{\pageid}})$. Functions which have a result component which is equivalent to the corresponding argument may have said components elided in the description. Functions may also depend upon particular additional parameters.
 
 Unlike the Accumulate functions in appendix \ref{sec:accumulatefunctions}, these do not mutate an accumulation context. Some, such as $\mathtt{write}$ mutate a service account and both accept and return some $\mathbf{s} \in \serviceaccount$. Others are more general functions, such as $\mathtt{fetch}$ and do not assume any context but have a parameter list suffixed with an ellipsis to denote that the context parameter may be taken and is provided transparently into its result. This allows it to be easily utilized in multiple \textsc{pvm} invocations.
 
 Elements of \textsc{pvm} state are each assumed to remain unchanged by the host-call unless explicitly specified.
 \begin{align}
   \gascounter' &\equiv \gascounter - g\text{ unless $\gascounter'$ is explicitly defined below}\\
-  \tup{\execst', \registers', \memory', \mathbf{s}'} &\equiv \begin{cases}
-    \tup{\oog, \registers, \memory, \mathbf{s}} &\when \gascounter < g\\
-    \tup{\continue, \registers, \memory, \mathbf{s}} \text{ except as indicated below} &\otherwise
+  \tup{\execst', \registers', \memory', \workingset', \mathbf{s}'} &\equiv \begin{cases}
+    \tup{\oog, \registers, \memory, \workingset, \mathbf{s}} &\when \gascounter < g\\
+    \tup{\continue, \registers, \memory, \workingset, \mathbf{s}} \text{ except as indicated below} &\otherwise
   \end{cases}
 \end{align}
 
@@ -302,7 +303,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_\Gemini(\gascounter, \registers, \memory, \jam¬blob)$ \\
+  $\Omega_\Gemini(\gascounter, \registers, \memory, \workingset, \jam¬blob)$ \\
   \texttt{grow\_heap} = 1} &
   $\begin{aligned}
     % This hostcall can be used to expand the RW data region of memory, or to query its size.
diff --git a/text/serialization.tex b/text/serialization.tex
index 168b6a9c..b5708dc3 100644
--- a/text/serialization.tex
+++ b/text/serialization.tex
@@ -247,6 +247,7 @@ \subsection{Block Serialization}
   \encode{\wpX \in \workpackage} &\equiv \encode{
     \encode[4]{\wpX_\wp¬authcodehost},
     \wpX_\wp¬authcodehash,
+    \encode[2]{\wpX_\wp¬authworkingsetsize},
     \wpX_\wp¬context,
     \var{\wpX_\wp¬authtoken},
     \var{\wpX_\wp¬authconfig},
@@ -257,6 +258,7 @@ \subsection{Block Serialization}
     \encode[4]{\wiX_\wi¬serviceindex},
     \wiX_\wi¬codehash,
     \encode[8]{\wiX_\wi¬refgaslimit},
+    \encode[2]{\wiX_\wi¬refworkingsetsize},
     \encode[8]{\wiX_\wi¬accgaslimit},
     \encode[2]{\wiX_\wi¬exportcount},
     \var{\wiX_\wi¬payload},
diff --git a/text/work_packages_and_reports.tex b/text/work_packages_and_reports.tex
index 755800d5..648f2460 100644
--- a/text/work_packages_and_reports.tex
+++ b/text/work_packages_and_reports.tex
@@ -58,7 +58,7 @@ \subsubsection{Data Collection and Justification}
 
 \subsection{Packages and Items}\label{sec:packagesanditems}
 
-We begin by defining a \emph{work-package}, of set $\workpackage$, and its constituent \emph{work-item}s, of set $\workitem$. A work-package includes a simple blob acting as an authorization token $\wp¬authtoken$, the index of the service which hosts the authorization code $\wp¬authcodehost$, an authorization code hash $\wp¬authcodehash$ and a configuration blob $\wp¬authconfig$, a context $\wp¬context$ and a sequence of work items $\wp¬workitems$:
+We begin by defining a \emph{work-package}, of set $\workpackage$, and its constituent \emph{work-item}s, of set $\workitem$. A work-package includes a simple blob acting as an authorization token $\wp¬authtoken$, the index of the service which hosts the authorization code $\wp¬authcodehost$, an authorization code hash $\wp¬authcodehash$ and a configuration blob $\wp¬authconfig$, a working-set size for execution of the authorization code $\wpX_\wp¬authworkingsetsize$, a context $\wp¬context$ and a sequence of work items $\wp¬workitems$:
 \begin{equation}
   \label{eq:workpackage}
   \workpackage \equiv \tuple{
@@ -66,18 +66,20 @@ \subsection{Packages and Items}\label{sec:packagesanditems}
     \isa{\wp¬authcodehost}{\serviceid},\
     \isa{\wp¬authcodehash}{\hash},\
     \isa{\wp¬authconfig}{\blob},\
+    \isa{\wp¬authworkingsetsize}{\workingsetsize},\
     \isa{\wp¬context}{\workcontext},\
     \isa{\wp¬workitems}{\sequence[1:\Cmaxpackageitems]{\workitem}}
   }
 \end{equation}
 
-A work item includes: $\wi¬serviceindex$ the identifier of the service to which it relates, the code hash of the service at the time of reporting $\wi¬codehash$ (whose preimage must be available from the perspective of the lookup anchor block), a payload blob $\wi¬payload$, gas limits for Refinement and Accumulation $\wi¬refgaslimit$ \& $\wi¬accgaslimit$, and the three elements of its manifest, a sequence of imported data segments $\wi¬importsegments$ which identify a prior exported segment through an index and the identity of an exporting work-package, $\wi¬extrinsics$, a sequence of extrinsic data hashes and lengths and $\wi¬exportcount$ the number of data segments exported by this work item.
+A work item includes: $\wi¬serviceindex$ the identifier of the service to which it relates, the code hash of the service at the time of reporting $\wi¬codehash$ (whose preimage must be available from the perspective of the lookup anchor block), a payload blob $\wi¬payload$, gas limits for Refinement and Accumulation $\wi¬refgaslimit$ \& $\wi¬accgaslimit$, a working-set size for Refinement $\wi¬refworkingsetsize$, and the three elements of its manifest, a sequence of imported data segments $\wi¬importsegments$ which identify a prior exported segment through an index and the identity of an exporting work-package, $\wi¬extrinsics$, a sequence of extrinsic data hashes and lengths and $\wi¬exportcount$ the number of data segments exported by this work item.
 \begin{equation}\label{eq:workitem}
   \workitem \equiv \tuple{\begin{aligned}
     &\isa{\wi¬serviceindex}{\serviceid},
     \isa{\wi¬codehash}{\hash},
     \isa{\wi¬payload}{\blob},
     \isa{\wi¬refgaslimit}{\gas},
+    \isa{\wi¬refworkingsetsize}{\workingsetsize},
     \isa{\wi¬accgaslimit}{\gas},
     \isa{\wi¬exportcount}{\N}, \\
     &\isa{\wi¬importsegments}{\sequence{\tuple{\hash \cup (\hash^\boxplus),\N}}},

From b4144739a58bcb86d3d1650eea00204baf41e85c Mon Sep 17 00:00:00 2001
From: Jan Bujak <jan@parity.io>
Date: Wed, 8 Jul 2026 09:39:38 +0000
Subject: [PATCH 2/2] Flesh out working-set spec

---
 graypaper.tex                      |   6 +-
 preamble.tex                       |  14 +
 text/definitions.tex               |   8 +
 text/merklization.tex              |   2 +-
 text/overview.tex                  |  12 +-
 text/pvm.tex                       | 552 +++++++++++++++++++++++------
 text/pvm_invocations.tex           | 208 ++++++-----
 text/work_packages_and_reports.tex |   2 +-
 8 files changed, 595 insertions(+), 209 deletions(-)

diff --git a/graypaper.tex b/graypaper.tex
index f8bcb70a..cd387037 100644
--- a/graypaper.tex
+++ b/graypaper.tex
@@ -1,9 +1,9 @@
 \documentclass[9pt,oneside]{amsart}
 \input{preamble.tex}
 
-%\pagecolor{verydarkgray}
-%\color{white}
-%\makegpbackground
+\pagecolor{verydarkgray}
+\color{white}
+\makegpbackground
 
 \begin{document}
 
diff --git a/preamble.tex b/preamble.tex
index 50e5e859..e612d568 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -287,6 +287,13 @@
 \newcommand*{\Cpvminitinputsize}{\mathsf{Z}_I}
 \newcommand*{\Cpvmpagesize}{\mathsf{Z}_P}
 \newcommand*{\Cpvminitzonesize}{\mathsf{Z}_Z}
+\newcommand*{\Cpvmgaspagefault}{\mathsf{G}_F}
+\newcommand*{\Cpvmgaspagealloc}{\mathsf{G}_A}
+\newcommand*{\Cpvmgaspagezero}{\mathsf{G}_Z}
+\newcommand*{\Cpvmgaspagecopy}{\mathsf{G}_C}
+\newcommand*{\Cpvmgasdeliver}{\mathsf{G}_D}
+\newcommand*{\Cpvmminworkingset}{\mathsf{W}_{\text{min}}}
+\newcommand*{\Cpvmmaxworkingset}{\mathsf{W}_{\text{max}}}
 \newcommand*{\Cgasunknown}{\mathsf{M}_\none}
 \newcommand*{\CgasG}{\mathsf{M}_G}
 \newcommand*{\CgasGeminiconst}{\mathsf{M}_{\Gemini,c}}
@@ -479,6 +486,10 @@
 \newcommand*{\ram}{\mathbb{M}}
 \newcommand*{\ram¬value}{\mathbf{v}}
 \newcommand*{\ram¬access}{\mathbf{a}}
+\newcommand*{\ram¬frames}{\mathbf{f}}
+\newcommand*{\frame¬present}{\top}
+\newcommand*{\frame¬missing¬zero}{\bot_{\mathrm{z}}}
+\newcommand*{\frame¬missing¬copy}{\bot_{\mathrm{c}}}
 
 \newcommand*{\pageid}{\mathbb{p}}
 \newcommand*{\pid¬machine}{m}
@@ -863,6 +874,9 @@
 \newcommand*{\contextmutator}[1]{\Omega\ang{#1}}
 \newcommand*{\fnmemgas}{\mathcal{G}}
 
+\newcommand*{\wscharge¬internal}{\Theta}
+\newcommand*{\wscharge¬extwrite}{\Theta^{\downarrow}}
+
 %%%%%%%%%%%%
 % Other stuff
 
diff --git a/text/definitions.tex b/text/definitions.tex
index 6cb3497c..f0c593d9 100644
--- a/text/definitions.tex
+++ b/text/definitions.tex
@@ -248,6 +248,7 @@ \subsubsection{Virtual Machine components}
   \item[$\memory$] The memory sequence; a member of the set $\ram$.
   \item[$\gascounter$] The gas counter.
   \item[$\registers$] The registers.
+  \item[$\workingset$] The working-set of resident page identifiers. See appendix \ref{sec:workingsetchanges}.
   \item[$\zeta$] The instruction sequence.
   \item[$\varpi$] The sequence of basic blocks of the program.
   \item[$\imath$] The instruction counter.
@@ -294,6 +295,13 @@ \subsubsection{Constants}
   \item[$\Cmaxpackageexports = 3,072$] The maximum number of exports in a work-package. See equation \ref{eq:limitworkpackagebandwidth}.
   \item[$\mathsf{X}$] Context strings, see below.
   \item[$\Cepochtailstart = 500$] The number of slots into an epoch at which ticket-submission ends. See sections \ref{sec:slotkeysequence}, \ref{sec:epochmarker} and \ref{sec:safrolextandtickets}.
+  \item[$\Cpvmgaspagealloc = 300$] The gas cost of provisioning (and eventually deallocating) a physical frame for a \textsc{pvm} \textsc{ram} page. See appendix \ref{sec:workingsetchanges}.
+  \item[$\Cpvmgaspagecopy = 300$] The gas cost of populating a freshly provisioned \textsc{pvm} \textsc{ram} page from its initial image. See appendix \ref{sec:workingsetchanges}.
+  \item[$\Cpvmgasdeliver = 500$] The gas cost, per 1024 octets, of the eventual read-back, from the node's state or context, of data that a host-call writes into a machine's \textsc{ram}. See appendix \ref{sec:generalfunctions}.
+  \item[$\Cpvmgaspagefault = 1000$] The base gas cost of inserting a page into the \textsc{pvm} working-set. See appendix \ref{sec:workingsetchanges}.
+  \item[$\Cpvmgaspagezero = 200$] The gas cost of zero-filling a freshly provisioned \textsc{pvm} \textsc{ram} page. See appendix \ref{sec:workingsetchanges}.
+  \item[$\Cpvmmaxworkingset = 7168$] The maximum \textsc{pvm} working-set size, in pages. See equation \ref{eq:workingsetsize}.
+  \item[$\Cpvmminworkingset = 16$] The minimum \textsc{pvm} working-set size, in pages. See equation \ref{eq:workingsetsize}.
   \item[$\Cpvmdynaddralign = 2$] The \textsc{pvm} dynamic address alignment factor. See equation \ref{eq:jumptablealignment}.
   \item[$\Cpvminitinputsize = 2^{24}$] The standard \textsc{pvm} program initialization input data size. See equation \ref{sec:standardprograminit}.
   \item[$\Cpvmpagesize = 2^{12}$] The \textsc{pvm} memory page size. See equation \ref{eq:pvmmemory}.
diff --git a/text/merklization.tex b/text/merklization.tex
index 1169c267..ca63b807 100644
--- a/text/merklization.tex
+++ b/text/merklization.tex
@@ -87,7 +87,7 @@ \subsection{Serialization}
     \forall \kv{s}{\saX} \in \accounts: &&C(255, s) &\mapsto \encode{
       0,
       \saX_\sa¬codehash,
-      \encode[2]{\sa¬accworkingsetsize},
+      \encode[2]{\saX_\sa¬accworkingsetsize},
       \encode[8]{
         \saX_\sa¬balance,
         \saX_\sa¬minaccgas,
diff --git a/text/overview.tex b/text/overview.tex
index aa88a70d..0ec75bec 100644
--- a/text/overview.tex
+++ b/text/overview.tex
@@ -177,12 +177,14 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
 \begin{align}\label{eq:pvmmemory}
   \ram &\equiv \tuple{
     \isa{\ram¬value}{\blob[2^{32}]},
-    \isa{\ram¬access}{\sequence[p]{\set{\text{W}, \text{R}, \none}}}
-  }\,,\ p = \frac{2^{32}}{\Cpvmpagesize}\\
+    \isa{\ram¬access}{\sequence[p]{\set{\text{W}, \text{R}, \none}}},
+    \isa{\ram¬frames}{\sequence[p]{\set{\frame¬present, \frame¬missing¬zero, \frame¬missing¬copy}}}
+  }\\
+  p &= \frac{2^{32}}{\Cpvmpagesize} \notag\\
   \Cpvmpagesize &= 2^{12}
 \end{align}
 
-The \textsc{pvm} assumes a simple pageable \textsc{ram} of 32-bit addressable octets situated in pages of $\Cpvmpagesize = 4096$ octets where each page may be either immutable, mutable or inaccessible. The \textsc{ram} definition $\ram$ includes two components: a value $\ram¬value$ and access $\ram¬access$. If the component is unspecified while being subscripted then the value component may be assumed. Within the context of the virtual machine, $\memory \in \ram$ 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 $\Cpvmpagesize = 4096$ octets where each page may be either immutable, mutable or inaccessible. The \textsc{ram} definition $\ram$ includes three components: a value $\ram¬value$, access $\ram¬access$, and frames $\ram¬frames$. If the component is unspecified while being subscripted then the value component may be assumed. The frames component records, per page, whether a physical frame has been allocated for it ($\frame¬present$) by the working-set gas model of appendix \ref{sec:workingsetchanges}, or, if not, whether first provisioning one would require copying the page from the program's initial image ($\frame¬missing¬copy$) or merely zeroing it ($\frame¬missing¬zero$). It influences gas costs only and has no effect on the semantics of reads and writes. Within the context of the virtual machine, $\memory \in \ram$ is typically used to denote \textsc{ram}.
 \begin{align}
   \readable{\memory} &\equiv \set{\build{i}{\memory_\ram¬access\subb{\floor{\nicefrac{i}{\Cpvmpagesize}}} \ne \none}} \\
   \writable{\memory} &\equiv \set{\build{i}{\memory_\ram¬access\subb{\floor{\nicefrac{i}{\Cpvmpagesize}}} = \text{W} }}
@@ -190,9 +192,9 @@ \subsection{The Virtual Machine and Gas}\label{sec:virtualmachineandgas}
 
 We define two sets of indices for the \textsc{ram} $\memory$: $\readable{\memory}$ is the set of indices which may be read from; and $\writable{\memory}$ is the set of indices which may be written to.
 
-On contemporary CPUs, memory is accessed via a series of caches, with increasing capacity but also increasing access latency at each level. In order to be able to accurately predict memory access latency in the gas cost model, the size of the \emph{working-set} of memory pages $\workingset \in \sequence{\optional{\pageid}}$ is constrained. The size is chosen at machine creation time from the set $\workingsetsize$, with a smaller working-set, capable of fitting in a lower-level cache, reducing the predicted latency and thus effective gas cost of each memory access. Note however that every change to the working-set, although automatic and thus mostly invisible to the \textsc{pvm} programmer, incurs a significant gas cost. The smaller the working-set, the more likely each memory access is to ``miss'' and require such a change. The working-set size should be carefully chosen to balance these two factors. Note that the working-set covers both data \emph{and} code.
+On contemporary CPUs, memory is accessed via a series of caches, with increasing capacity but also increasing access latency at each level. In order to be able to accurately predict memory access latency in the gas cost model, the size of the \emph{working-set} of memory pages $\workingset \in \sequence{\optional{\pageid}}$ is constrained. The size is chosen at machine creation time from the set $\workingsetsize$, with a smaller working-set, capable of fitting in a lower-level cache, reducing the predicted latency and thus effective gas cost of each memory access. Every change to the working-set, although automatic and thus mostly invisible to the \textsc{pvm} programmer, incurs a significant gas cost. The smaller the working-set, the more likely each memory access is to ``miss'' and require such a change. The working-set size should be carefully chosen to balance these two factors. The working-set covers data, jump-table, and also code pages.
 \begin{equation}\label{eq:workingsetsize}
-    \workingsetsize \equiv \Nclamp{4}{8193}
+    \workingsetsize \equiv \set{\build{n \in \N}{\Cpvmminworkingset \le n \le \Cpvmmaxworkingset}}
 \end{equation}
 
 Invocation of the \textsc{pvm} has an exit-reason as the first item in the resultant tuple. It is either:
diff --git a/text/pvm.tex b/text/pvm.tex
index 9e1274ca..f659e4bd 100644
--- a/text/pvm.tex
+++ b/text/pvm.tex
@@ -25,20 +25,38 @@ \subsection{Basic Definition}
 \renewcommand*{\S}{\token{S}}
 \newcommand*{\A}{\token{A}}
 \newcommand*{\basicblocks}{\varpi}
+\newcommand*{\phase¬gas}{\mathrm{G}}
+\newcommand*{\phase¬fetch}{\mathrm{F}}
+\newcommand*{\phase¬djump}{\mathrm{J}}
+\newcommand*{\phase¬mem}{\mathrm{M}}
 \newcommand*{\instructions}{\zeta}
 \newcommand*{\immed}{\nu}
 \newcommand*{\deblob}{\text{deblob}}
 \newcommand*{\smod}{\text{smod}}
 \newcommand*{\rtz}{\text{rtz}}
 \newcommand*{\gascostforblock}{\gascounter^{\Delta}}
-\newcommand*{\codepage}[1]{{#1}^\diamond}
-\newcommand*{\pageforinstruction}{\codepage{P}}
+\newcommand*{\datatag}{\text{\textsc{d}}}
+\newcommand*{\codetag}{\text{\textsc{c}}}
+\newcommand*{\jumptag}{\text{\textsc{j}}}
+\newcommand*{\datapage}[1]{{\datatag \times #1}}
+\newcommand*{\codepage}[1]{{\codetag \times #1}}
+\newcommand*{\jumppage}[1]{{\jumptag \times #1}}
+\newcommand*{\codefam}[1]{{#1}^\diamond}
+\newcommand*{\pageforinstruction}{\codefam{P}}
+\newcommand*{\preamblepages}{\codefam{Q}}
+\newcommand*{\codeoffset}{\codefam{o}}
+\newcommand*{\codepages}{\codefam{S}}
+\newcommand*{\bbpreamblesize}{\codefam{B}}
+\newcommand*{\codepagecharge}{\codefam{C}}
+\newcommand*{\branchsize}{\codefam{J}}
 \newcommand*{\gascostforpageaccess}{\gascounter^\workingset}
+\newcommand*{\pagefaultcost}{\mathfrak{c}}
+\newcommand*{\spannedpages}{\Pi}
 \newcommand*{\startofbasicblock}{\mathfrak{L}}
 We declare the general \textsc{pvm} function $\Psi$. We assume a single-step invocation function $\Psi_1$ and define the full \textsc{pvm} recursively as a sequence of such mutations up until the single-step mutation results in a halting condition. We additionally define the function $\deblob$ which extracts the instruction data, opcode bitmask and dynamic jump table from a \textsc{pvm} program blob, validates its structure, and verifies whether the given $\imath$ is a valid instruction counter location within the program:
 \begin{align}
   \Psi&\colon \abracegroup{
-    \tuple{\blob, \pvmreg, \gas, \bool, \regs, \ram, \optional{N}, \sequence{\optional{\pageid}}} &\to \tuple{\set{\halt, \panic, \oog} \cup \set{\fault, \host} \times \pvmreg, \pvmreg, \gas, \bool, \regs, \ram, \sequence{\optional{\pageid}}}\\
+    \tuple{\blob, \pvmreg, \gas, \bool, \regs, \ram, \optional{\N}, \sequence{\optional{\pageid}}} &\to \tuple{\set{\halt, \panic, \oog} \cup \set{\fault, \host} \times \pvmreg, \pvmreg, \gas, \bool, \regs, \ram, \sequence{\optional{\pageid}}}\\
     \tup{\pvm¬blob, \imath, \gascounter, \gaschargedflag, \registers, \mem, \pid¬machine, \workingset} &\mapsto \begin{cases}
       \Psi(\pvm¬blob, \imath', \gascounter', \gaschargedflag', \registers', \mem', \pid¬machine, \workingset') &\when \varepsilon = \continue\\
       \tup{\varepsilon, 0, \gascounter', \gaschargedflag', \registers', \mem', \workingset'} &\when \varepsilon \in \set{ \panic, \halt }\\
@@ -158,65 +176,89 @@ \subsection{Single-Step State Transition}
   }
 \end{equation}
 
-Before execution, the instruction must first be fetched from memory. This may require a change to the working-set and thus incur a gas charge. If there is insufficient gas to cover this charge, execution is interrupted. Working-set changes are discussed further and the functions $\gascostforpageaccess$ and $\pageforinstruction$ defined in section \ref{sec:workingsetchanges}.
+Before execution, the instruction must be fetched from memory. This is done lazily, using the machine's paging hardware: each fetch of a code page not resident in the working-set is a page fault which charges gas according to $\gascostforpageaccess$ and inserts the page. We define $\codepagecharge$, which charges in order for a sequence of pages, each inserted at the base fault cost $\Cpvmgaspagefault$, halting if the gas runs out:
 \begin{equation}
-    \begin{aligned}
-        \tup{\codepage{\varepsilon}, \codepage{\gascounter}, \codepage{\workingset}} &= \begin{cases}
-        \tup{\continue, \gascounter - g, w} &\when \gascounter \ge g \\
-        \tup{\oog, \gascounter, \workingset} &\otherwise
+  \begin{aligned}
+    \codepagecharge(g, w, \mathbf{p}) &= \begin{cases}
+      \tup{\continue, g, w} &\when \mathbf{p} = \sq{} \\
+      \tup{\oog, g, w} &\otherwhen g < g^\delta \\
+      \codepagecharge(g - g^\delta, w', \mathbf{p}\sub{1\dots}) &\otherwise
     \end{cases} \\
-        \where (g, w) &= \gascostforpageaccess(\workingset, \tup{\pid¬machine, \is{\pid¬index}{\pageforinstruction(\mathbf{c}, \mathbf{k}, \imath)}})
-    \end{aligned}
+    \where (g^\delta, w') &= \gascostforpageaccess(w, \tup{\pid¬machine, \is{\pid¬index}{\mathbf{p}_0}}, \Cpvmgaspagefault)
+  \end{aligned}
 \end{equation}
 
-On the very first step of execution, and every time the execution enters a new basic block or jumps back to the beginning of the current basic block, the gas counter of the machine is updated according to the gas cost function $\gascostforblock$~(\ref{eq:gascostforblock}) of the target basic block. No instruction is allowed to execute within a basic block unless the gas cost for the entire basic block has been charged in advance. In case there's not enough gas remaining to cover the full gas cost, the execution is interrupted and the gas counter remains unchanged. Formally:
+On the very first step of execution, and every time execution enters a new basic block or jumps back to the beginning of the current one, the block's gas-metering preamble is fetched (charging for its code pages) and then the gas cost of the entire block~(\ref{eq:gascostforblock}) is charged in advance; no instruction may execute until both are paid. If at any point there is insufficient gas, execution is interrupted and the gas counter is left at its last value. Formally:
 \begin{equation}
-  \tup{\varepsilon^\basicblocks, \gascounter^\basicblocks} = \begin{cases}
-    \tup{\continue, \codepage{\gascounter}} &\when \gaschargedflag = \top \\
-    \tup{\continue, \codepage{\gascounter} - \gascostforblock(\mathbf{c}, \mathbf{k}, \len{\workingset}, \startofbasicblock(\imath))} &\otherwhen \codepage{\gascounter} \ge \gascostforblock(\mathbf{c}, \mathbf{k}, \len{\workingset}, \startofbasicblock(\imath)) \\
-    \tup{\oog, \codepage{\gascounter}} &\otherwise
-  \end{cases}
+  \begin{aligned}
+    \tup{\varepsilon^\phase¬gas, \gascounter^\phase¬gas, \workingset^\phase¬gas} &= \begin{cases}
+      \tup{\continue, \gascounter, \workingset} &\when \gaschargedflag = \top \\
+      \tup{\varepsilon', \gascounter', \workingset'} &\otherwhen \varepsilon' \ne \continue \\
+      \tup{\continue, \gascounter' - g^\phase¬gas, \workingset'} &\otherwhen \gascounter' \ge g^\phase¬gas \\
+      \tup{\oog, \gascounter', \workingset'} &\otherwise
+    \end{cases} \\
+    \where \tup{\varepsilon', \gascounter', \workingset'} &= \codepagecharge(\gascounter, \workingset, \preamblepages(\mathbf{c}, \mathbf{k}, \startofbasicblock(\imath))) \\
+    \also g^\phase¬gas &= \gascostforblock(\mathbf{c}, \mathbf{k}, \len{\workingset}, \startofbasicblock(\imath))
+  \end{aligned}
 \end{equation}
 
+The instruction's own native code is then fetched, charging for the code pages it spans:
+\begin{equation}
+  \tup{\varepsilon^\phase¬fetch, \gascounter^\phase¬fetch, \workingset^\phase¬fetch} = \codepagecharge(\gascounter^\phase¬gas, \workingset^\phase¬gas, \pageforinstruction(\mathbf{c}, \mathbf{k}, \imath))
+\end{equation}
+
+An instruction that resolves its target through the jump-table reads an 8-octet entry from a native jump-table, laid out at a stride of eight octets per dynamic address unit; the entry for a target address $a$ thus lies on the jump-table page $\jumppage{\floor{\nicefrac{8a}{\Cpvmpagesize}}}$, where jump-table pages $\jumptag \times \N$ form their own class of page index, distinct from the \textsc{ram} and code pages of the same machine. This read is charged like any other access. No charge arises for the special halt address (its vector is permanently resident), nor where the entry's page lies wholly beyond the table (execution panics without any table access being made), however a charge \emph{is} made for a misaligned, zero or invalid-entry target whose page is within reach of the table, as the entry must be read before it can be found invalid. Formally:
+\begin{equation}
+  \begin{aligned}
+    \tup{\varepsilon^\phase¬djump, \gascounter^\phase¬djump, \workingset^\phase¬djump} &= \codepagecharge(\gascounter^\phase¬fetch, \workingset^\phase¬fetch, \mathbf{p}^\phase¬djump) \\
+    \where \mathbf{p}^\phase¬djump &= \begin{cases}
+      \sq{} &\when a^\circ = \none \vee a^\circ = 2^{32} - 2^{16} \vee \floor{\nicefrac{8a^\circ}{\Cpvmpagesize}} > \floor{\nicefrac{8\Cpvmdynaddralign\len{\mathbf{j}}}{\Cpvmpagesize}} \\
+      \sq{\jumppage{\floor{\nicefrac{8a^\circ}{\Cpvmpagesize}}}} &\otherwise
+    \end{cases}
+  \end{aligned}
+\end{equation}
+where $a^\circ \in \optional{\N}$ is the dynamic-jump target address which the instruction at $\imath$ resolves through the jump-table --- that is, the argument passed to its $\token{djump}$ (section \ref{sec:instructiontables}) --- or $\none$ where the instruction performs no dynamic jump.
+
 During the course of executing instructions \textsc{ram} may be accessed. When an index of \textsc{ram} below $2^{16}$ is required, the machine always panics immediately without further changes to its state regardless of the apparent (in)accessibility of the value. Otherwise, should the given index of \textsc{ram} not be accessible then machine state remains unchanged and the exit reason is a fault with the lowest inaccessible \emph{page address} to be read. 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 page address to be written which is inaccessible.
 
-In addition to these accessibility checks, as with instruction fetches, \textsc{ram} reads and writes implicitly pull accessed pages into the working-set. If the gas cost of a working-set change cannot be covered by the available gas, execution halts immediately. Note that working-set changes are interleaved with accessibility checks; this can affect observed behaviour in cases of gas exhaustion.
+In addition to these accessibility checks, as with instruction fetches, \textsc{ram} reads and writes implicitly pull accessed pages into the working-set, allocating a frame for the page (recorded in $\mem_\ram¬frames$) where none yet exists. If the gas cost of a working-set change cannot be covered by the available gas, execution is interrupted. Charges made (and frames allocated) for the earlier pages of a step persist even where a later access of the same step faults or exhausts gas.
 
-Formally, let $\mathbf{r}$ and $\mathbf{w}$ be the set of indices by which $\mem$ must be subscripted for inspection and mutation respectively in order to calculate the result of $\Psi_1$. We define the memory-access exceptional execution state $\varepsilon^\mu$, posterior gas balance $\gascounter^\mu$, and posterior working-set $\workingset^\mu$ as following:
+Formally, let $\mathbf{r}$ and $\mathbf{w}$ be the set of indices by which $\mem$ must be subscripted for inspection and mutation respectively in order to calculate the result of $\Psi_1$. We define the memory-access exceptional execution state $\varepsilon^\phase¬mem$, posterior gas balance $\gascounter^\phase¬mem$, posterior working-set $\workingset^\phase¬mem$, and posterior \textsc{ram} $\mem^\phase¬mem$ (which may differ from $\mem$ in its frames component only) as following:
 \begin{equation}
   \begin{aligned}
-    (\varepsilon^{\mu}, \gascounter^{\mu}, \workingset^{\mu}) &= A(\gascounter^\basicblocks, \codepage{\workingset},
-      \sqorderby{a_x}{\set{\build{(x, \is{r}{\top})}{x \in \mathbf{r}}} \cup \set{\build{(x, \is{r}{\bot})}{x \in \mathbf{w}}}}) \\
-    A(g, w, \sq{}) &= (\continue, g, w) \\
-    A(g, w, \sq{\tup{x, r}} \concat \mathbf{r}) &= \begin{aligned}
-      &\begin{cases}
-        (\panic, g, w) &\when y < 2^{16} \\
-        (\fault \times \pid¬index \Cpvmpagesize, g, w) &\otherwhen y \not\in
-          \set{\kv{\top}{\readable\mem}, \kv{\bot}{\writable\mem}}\subb{r} \\
-        (\oog, g, w) &\otherwhen g < g^\delta \\
-        A(g - g^\delta, w', \mathbf{r}) &\otherwise
-      \end{cases} \\
-      &\where y = x \bmod 2^{32} \\
-      &\also \pid¬index = \floor{\frac{y}{\Cpvmpagesize}} \\
-      &\also (g^\delta, w') = \gascostforpageaccess(w, \tup{\pid¬machine, \pid¬index})
-    \end{aligned}
+    (\varepsilon^\phase¬mem, \gascounter^\phase¬mem, \workingset^\phase¬mem, \mem^\phase¬mem) &= A(\gascounter^\phase¬djump, \workingset^\phase¬djump, \mem,
+      \sqorderby{x}{\set{\build{(x, \is{r}{\top})}{x \in \mathbf{r}}} \cup \set{\build{(x, \is{r}{\bot})}{x \in \mathbf{w}}}}) \\
+    A(g, w, \mem, \mathbf{p}) &= \begin{cases}
+      (\continue, g, w, \mem) &\when \mathbf{p} = \sq{} \\
+      (\panic, g, w, \mem) &\otherwhen y < 2^{16} \\
+      (\fault \times i \cdot \Cpvmpagesize, g, w, \mem) &\otherwhen y \not\in
+        \set{\kv{\top}{\readable\mem}, \kv{\bot}{\writable\mem}}\subb{r} \\
+      (\oog, g, w, \mem) &\otherwhen g < g^\delta \\
+      A(g - g^\delta, w', \mem', \mathbf{p}\sub{1\dots}) &\otherwise
+    \end{cases} \\
+    \where \tup{x, r} &= \mathbf{p}_0 \\
+    \also y &= x \bmod 2^{32} \\
+    \also i &= \floor{\frac{y}{\Cpvmpagesize}} \\
+    \also (g^\delta, w') &= \gascostforpageaccess(w, \tup{\pid¬machine, \datapage{i}}, \pagefaultcost(\mem, i)) \\
+    \also \mem' &= \mem \exc \mem'_\ram¬frames\subb{i} = \frame¬present
   \end{aligned}
 \end{equation}
 
 We define the final execution state, the value of the instruction counter, the gas counter, the gas-charged flag, the values of the registers and the memory, and the working-set as follows:
 \begin{equation}
   \tup{\varepsilon^*, \imath^*, \gascounter^*, \gaschargedflag^*, \registers^*, \mem^*, \workingset^*} = \begin{cases}
-    \tup{\codepage{\varepsilon}, \imath, \codepage{\gascounter}, \gaschargedflag, \registers, \mem, \codepage{\workingset}} &\when \codepage{\varepsilon} \ne \continue \\
-    \tup{\varepsilon^\basicblocks, \imath, \gascounter^\basicblocks, \bot, \registers, \mem, \codepage{\workingset}} &\otherwhen \varepsilon^\basicblocks \ne \continue \\
-    \tup{\varepsilon^\mu, \imath, \gascounter^\mu, \top, \registers, \mem, \workingset^\mu} &\otherwhen \varepsilon^\mu \ne \continue \\
-    \tup{\varepsilon, \imath', \gascounter^\mu, \top, \registers', \mem', \workingset^\mu} &\otherwhen \varepsilon \not\in \set{\continue} \cup \set{\host} \times \pvmreg \\
-    \tup{\varepsilon, \imath', \gascounter^\mu, \mathbf{c}_\imath \not\in T, \registers', \mem', \workingset^\mu} &\otherwise
+    \tup{\varepsilon^\phase¬gas, \imath, \gascounter^\phase¬gas, \bot, \registers, \mem, \workingset^\phase¬gas} &\when \varepsilon^\phase¬gas \ne \continue \\
+    \tup{\varepsilon^\phase¬fetch, \imath, \gascounter^\phase¬fetch, \top, \registers, \mem, \workingset^\phase¬fetch} &\otherwhen \varepsilon^\phase¬fetch \ne \continue \\
+    \tup{\varepsilon^\phase¬djump, \imath, \gascounter^\phase¬djump, \top, \registers, \mem, \workingset^\phase¬djump} &\otherwhen \varepsilon^\phase¬djump \ne \continue \\
+    \tup{\varepsilon^\phase¬mem, \imath, \gascounter^\phase¬mem, \top, \registers, \mem^\phase¬mem, \workingset^\phase¬mem} &\otherwhen \varepsilon^\phase¬mem \ne \continue \\
+    \tup{\varepsilon, \imath', \gascounter^\phase¬mem, \top, \registers', \mem', \workingset^\phase¬mem} &\otherwhen \varepsilon \not\in \set{\continue} \cup \set{\host} \times \pvmreg \\
+    \tup{\varepsilon, \imath', \gascounter^\phase¬mem, \mathbf{c}_\imath \not\in T, \registers', \mem', \workingset^\phase¬mem} &\otherwise
   \end{cases}
 \end{equation}
 
 We define $\varepsilon$ together with the posterior values of regular execution (denoted as prime) of each of the items of the machine state as being in accordance with the table below. When transitioning machine state for an instruction, a number of conditions typically hold true and instructions are defined essentially by their exceptions to these rules. Specifically, the machine does not halt, the instruction counter increments by one and \textsc{ram} \& registers are unchanged. Formally:
 \begin{equation}
-  \varepsilon = \continue,\quad \imath' = \imath + 1 + \Fskip(\imath),\quad \registers' = \registers,\quad\mem' = \mem \text{ except as indicated }
+  \varepsilon = \continue,\quad \imath' = \imath + 1 + \Fskip(\imath),\quad \registers' = \registers,\quad\mem' = \mem^\phase¬mem \text{ except as indicated }
 \end{equation}
 
 We define signed/unsigned transitions for various octet widths:
@@ -872,6 +914,14 @@ \subsection{Standard Program Initialization}\label{sec:standardprograminit}
     \end{cases}
 \end{equation}
 
+No page begins with an allocated frame. The cost of provisioning each page's frame falls on whichever access first touches it (see appendix \ref{sec:workingsetchanges}), and depends on whether that page's initial content must be copied from the program image or is merely zeroed:
+\begin{equation}
+  \forall j \in \Nmax{\nicefrac{2^{32}}{\Cpvmpagesize}} : \mem_\ram¬frames\subb{j} = \begin{cases}
+    \frame¬missing¬copy &\when \Nrange{j\Cpvmpagesize}{\Cpvmpagesize} \cap \mathcal{I} \ne \emptyset \\
+    \frame¬missing¬zero &\otherwise
+  \end{cases}\ ,\quad \mathcal{I} = \Nrange{\Cpvminitzonesize}{\len{\mathbf{o}}} \cup \Nrange{2\Cpvminitzonesize + \rnq{\len{\mathbf{o}}}}{\len{\mathbf{w}}} \cup \Nrange{2^{32} - \Cpvminitzonesize - \Cpvminitinputsize}{\len{\mathbf{a}}}
+\end{equation}
+
 \subsection{Argument Invocation Definition}
 
 The three instances where the \textsc{pvm} is utilized each expect to be able to pass argument data in and receive some return data back. We thus define the common \textsc{pvm} program-argument invocation function $\Psi_M$:
@@ -1156,47 +1206,76 @@ \subsection{Gas Cost Model}\label{sec:gascostmodel}
 
 \subsection{Working-Set Changes}\label{sec:workingsetchanges}
 
-In addition to the static gas cost of each basic block as calculated by $\gascostforblock$, gas is charged dynamically whenever a memory page outside of the current working-set is accessed. Such an access implicitly adds the accessed page to the working-set, pushing another page out if necessary. The function $\gascostforpageaccess$ determines the working-set change, if any, required to access a page $p \in \pageid$, and the corresponding gas cost.
+In addition to the static gas cost of each basic block as calculated by $\gascostforblock$, gas is charged dynamically whenever a memory page outside of the current working-set is accessed. Such an access implicitly adds the accessed page to the working-set, pushing another page out if necessary. The working-set is a first-in first-out buffer of fixed length, and each insertion drops the oldest entry. A dropped page ceases to be resident, and re-accessing it later incurs a further working-set charge. This affects only gas, never the contents or accessibility of the page, so (given enough gas) the working-set has no effect on execution semantics. The function $\gascostforpageaccess$ determines the working-set change, if any, required to access a page $p \in \pageid$ whose insertion cost is $c$, and the corresponding gas cost.
 \begin{equation}
   \gascostforpageaccess\colon \abracegroup{
-    \tuple{\sequence{\optional{\pageid}}, \pageid} &\to \tuple{\gas, \sequence{\optional{\pageid}}} \\
-    \tup{\workingset, p} &\mapsto \begin{cases}
+    \tuple{\sequence{\optional{\pageid}}, \pageid, \N} &\to \tuple{\gas, \sequence{\optional{\pageid}}} \\
+    \tup{\workingset, p, c} &\mapsto \begin{cases}
       (0, \workingset) &\when p \in \workingset \\
-      (\text{TODO}, \workingset\sub{1\dots} \append p) &\otherwise
+      (c, \workingset\sub{1\dots} \append p) &\otherwise
     \end{cases}
   }
 \end{equation}
 
-This mechanism applies to explicit data accesses, via instructions such as \token{load\_u8}, as well as to the implicit reading of instructions by the machine. The instructions for a machine are not present in its \textsc{ram} $\memory$, and so instruction addresses cannot be mapped to regular page indices. For the sole purpose of this mechanism, we define a function $\pageforinstruction$ which maps instruction addresses to special page indices $\codepage{\N} \equiv \set{\build{\codepage{n}}{n \in \N}}$:
+The insertion cost of a code or a jump-table page is always the base page-fault cost $\Cpvmgaspagefault$, covering the fault itself together with the mapping and unmapping work implied by insertion and eviction. The insertion cost of \textsc{ram} pages additionally depend on whether a physical frame has previously been allocated for them, as recorded by the frames component $\ram¬frames$ of the \textsc{ram} (\ref{eq:pvmmemory}). Upon a page's first-ever access a frame must be provisioned, paying $\Cpvmgaspagealloc$ (which accounts both for its allocation and for its eventual deallocation when the machine is destroyed), as well as the cost of populating the page: $\Cpvmgaspagezero$ where the page is zero-sourced (the frame has to be merely cleared), and $\Cpvmgaspagecopy$ where it is copy-sourced (its content must be copied from the program's initial image). Which applies is a fixed property of the page's provenance, recorded as $\frame¬missing¬zero$ or $\frame¬missing¬copy$ in $\ram¬frames$ when the machine is laid out (\ref{eq:memlayout}), and does \emph{not} depend on the page's current contents. Once allocated, a frame persists regardless of eviction from the working-set, and re-insertion pays only the base cost. Formally, the insertion cost of the \textsc{ram} page with index $i$ of a machine with \textsc{ram} $\mu$ is given by $\pagefaultcost$:
+\begin{equation}\label{eq:pagefaultcost}
+  \pagefaultcost\colon \abracegroup{
+    \tuple{\ram, \N} &\to \N \\
+    \tup{\mu, i} &\mapsto \begin{cases}
+      \Cpvmgaspagefault &\when \mu_\ram¬frames\subb{i} = \frame¬present \\
+      \Cpvmgaspagefault + \Cpvmgaspagealloc + \Cpvmgaspagezero &\otherwhen \mu_\ram¬frames\subb{i} = \frame¬missing¬zero \\
+      \Cpvmgaspagefault + \Cpvmgaspagealloc + \Cpvmgaspagecopy &\otherwise
+    \end{cases}
+  }
+\end{equation}
+
+A successful charge for a \textsc{ram} page always sets the page's entry in $\ram¬frames$ to $\frame¬present$. In case the charge cannot be met, machine state is left unchanged. This mechanism applies to explicit data accesses (via load/store instructions), as well as to the implicit reading of instructions by the machine. The instructions for a machine are not present in its \textsc{ram} $\memory$, and so instruction addresses cannot be mapped to regular page indices; instead they are mapped to special code-page indices $\codetag \times \N$. Assuming the native code is laid out contiguously from offset zero, we first define $\bbpreamblesize(\imath)$, the size of the gas-metering stub emitted before an instruction which begins a basic block (to charge that block's gas according to $\gascostforblock$):
 \begin{equation}
-  \pageforinstruction\colon \abracegroup{
-    &\tuple{\blob, \bitstring, \pvmreg} \to \codepage{\N} \\
-    &\tup{\mathbf{c}, \mathbf{k}, \imath} \mapsto \codepage{\floor{\frac{A(0, 0)}{\Cpvmpagesize}}} \\
-    &\quad\where A(i, s) \equiv \begin{cases}
-      s - 1 &\when i > \imath \\
-      A(i + 1 + \text{skip}(i), B(s, N(i))) &\otherwise
-    \end{cases} \\
-    % Maximum compiled size of the instruction at address i, including any immediately
-    % preceding basic block preamble
-    &\quad\also N(i) \equiv \inst¬compiledsize(\mathbf{c}, \mathbf{k}, i) + \begin{cases}
-      \text{TODO} &\when i \in \basicblocks \\
-      0 &\otherwise
-    \end{cases} \\
-    % Bump s by n bytes, jumping to the next page boundary first if the n bytes would otherwise
-    % straddle it
-    &\quad\also B(s, n) \equiv \begin{cases}
-      s + n &\when n \le \Cpvmpagesize - (s \rem \Cpvmpagesize) \\
-      \Cpvmpagesize \floor{\frac{s}{\Cpvmpagesize}} + \Cpvmpagesize + n &\otherwise
+  \bbpreamblesize(\imath) \equiv \begin{cases}
+    10 &\when \imath \in \basicblocks \\
+    0 &\otherwise
+  \end{cases}
+\end{equation}
+
+From this, $\codeoffset$ gives the byte offset at which the native code of the instruction at address $\imath$ begins, including any preceding basic-block preamble:
+\begin{equation}
+  \codeoffset\colon \abracegroup{
+    \tuple{\blob, \bitstring, \pvmreg} &\to \N \\
+    \tup{\mathbf{c}, \mathbf{k}, \imath} &\mapsto L(\mathbf{c}, \mathbf{k}, \imath, 0) \\
+    \where L(\mathbf{c}, \mathbf{k}, \imath, p) &\equiv \begin{cases}
+      0 &\when p = \imath \\
+      \inst¬compiledsize(\mathbf{c}, \mathbf{k}, p) + \bbpreamblesize(p) + L(\mathbf{c}, \mathbf{k}, \imath, p + 1 + \Fskip(p)) &\otherwise
     \end{cases}
   }
 \end{equation}
 
-$\pageforinstruction$ is defined under the assumption that \textsc{pvm} program code is translated into native code for execution. It utilises the function $\inst¬compiledsize(\mathbf{c}, \mathbf{k}, \imath)$, which returns the size of the native code translation of the \textsc{pvm} instruction at address $\imath$. The values returned by $\inst¬compiledsize$ are specified in section \ref{sec:gascosttables}. Allowance is also made by $\pageforinstruction$ for a small section of native code at the start of each basic block, to charge gas according to $\gascostforblock$.
+The instruction's own native code occupies the byte range after its block's preamble (if any), and the preamble, where present, the range before it. $\spannedpages(o, z)$ gives the ascending pages spanned by the $z$-byte range at $o$, $\codepages$ tags them as code pages, and $\pageforinstruction$ and $\preamblepages$ apply this to the instruction's own range and to its preamble's:
+\begin{align}
+  \spannedpages(o, z) &\equiv\label{eq:pagespan} \begin{cases}
+    \sq{} &\when z = 0 \\
+    \sqorderby{p}{\set{\build{p}{\floor{\frac{o}{\Cpvmpagesize}} \le p \le \floor{\frac{o + z - 1}{\Cpvmpagesize}}}}} &\otherwise
+  \end{cases} \\
+  \codepages(o, z) &\equiv \sq{\build{\codepage{p}}{p \orderedin \spannedpages(o, z)}} \\
+  \pageforinstruction(\mathbf{c}, \mathbf{k}, \imath) &\equiv \codepages(\codeoffset(\mathbf{c}, \mathbf{k}, \imath) + \bbpreamblesize(\imath),\ \inst¬compiledsize(\mathbf{c}, \mathbf{k}, \imath)) \\
+  \preamblepages(\mathbf{c}, \mathbf{k}, \imath) &\equiv \codepages(\codeoffset(\mathbf{c}, \mathbf{k}, \imath),\ \bbpreamblesize(\imath))
+\end{align}
+
+These are defined under the assumption that \textsc{pvm} program code is translated into native code for execution. The function $\inst¬compiledsize(\mathbf{c}, \mathbf{k}, \imath)$ (defined in \ref{sec:compiledsizes}) returns the size of the native code translation of the \textsc{pvm} instruction at address $\imath$.
 
-The working-set is shared with inner \textsc{pvm} instances. For this reason, page identifiers characterized by the set $\pageid$ consist of a machine identifier $\pid¬machine$ in addition to a page index $\pid¬index$. $\none$ is used to identify the top-level \textsc{pvm} instance.
+The working-set is shared with inner \textsc{pvm} instances. For this reason, page identifiers characterized by the set $\pageid$ consist of a machine identifier $\pid¬machine$ in addition to a page index $\pid¬index$, the latter a page number paired with one of the disjoint class tags $\datatag$, $\codetag$ or $\jumptag$, for \textsc{ram}, code and jump-table pages respectively. $\none$ is used to identify the top-level \textsc{pvm} instance.
 \begin{equation}
   \label{eq:pageid}
-  \pageid \equiv \tuple{\isa{\pid¬machine}{\optional{\N}}, \isa{\pid¬index}{\N \cup \codepage{\N}}}
+  \pageid \equiv \tuple{\isa{\pid¬machine}{\optional{\N}}, \isa{\pid¬index}{\set{\datatag, \codetag, \jumptag} \times \N}}
+\end{equation}
+
+The working-set size is fixed for the duration of an invocation, drawn from the valid sizes $\workingsetsize$~(\ref{eq:workingsetsize}). The lower bound $\Cpvmminworkingset$ guarantees forward progress: it exceeds the most pages any single step can need resident at once, so a step is never forced to evict a page it still requires. The upper bound $\Cpvmmaxworkingset$ keeps the resident set within the last-level cache of reference hardware, which is what justifies the pricing of resident accesses set out later in the gas cost tables~(\ref{eq:loadcost}).
+
+An entry is removed when the page it identifies ceases to exist: on expunging an inner machine, or deallocating or resetting \textsc{ram} pages through the $\mathtt{pages}$ host-call (appendix \ref{sec:refinefunctions}). The removed pages are replaced by $\none$ in-place. We write the removal of a page set $\mathbf{s} \subseteq \pageid$ as set-subtraction:
+\begin{equation}
+  \workingset \setminus \mathbf{s} \equiv \sq{\build{\begin{cases}
+    \none &\when e \in \mathbf{s} \\
+    e &\otherwise
+  \end{cases}}{e \orderedin \workingset}}
 \end{equation}
 
 \subsection{Gas Cost Tables}\label{sec:gascosttables}
@@ -1228,16 +1307,19 @@ \subsection{Gas Cost Tables}\label{sec:gascosttables}
   }
 \end{equation}
 
-The cost of memory accesses depends on the size of the working-set $w$ and is defined as follows:
+The cost of memory loads depends on the size of the working-set $w$: the resident set always fits within the last-level cache, but a larger one exceeds the reach of the address-translation caches, making the worst-case resident access dearer. It is defined as follows:\footnote{These values are provisional, pending calibration; see appendix \ref{sec:workingsetchanges}.}
 
-\begin{equation}
+\begin{equation}\label{eq:loadcost}
   \mathfrak{m}\colon \abracegroup{
       \workingsetsize &\to \N \\
-      w &\mapsto \text{TODO}
+      w &\mapsto \begin{cases}
+        25 &\when w \le 2^9 \\
+        37 &\when w \le 2^{12} \\
+        48 &\otherwise
+      \end{cases}
   }
 \end{equation}
 
-% TODO: Should the cost of a branch also depend on the working-set size?
 The cost of a branch depends on whether any of its targets (either the jump target or the implicit fallthrough) point to an instruction byte which is equal to the opcode for the \token{unlikely} or the \token{trap} instruction; formally:
 
 \begin{equation}
@@ -1255,46 +1337,47 @@ \subsection{Gas Cost Tables}\label{sec:gascosttables}
 \end{equation}
 
 \newcommand*{\ifdstandsrcoverlap}[2]{$\mathfrak{P}(#1, #2)$}
+\newcommand*{\srcdsteq}[1]{\mathfrak{D}_{#1}}
 \newcommand*{\ifdstandsrcoverlapshift}[2]{$\mathfrak{P}_{S}(#1, #2)$}
 \newcommand*{\loadcost}{$\mathfrak{m}$}
 \newcommand*{\storecost}{25}
 \newcommand*{\branchcost}{$\mathfrak{b}$}
 
-\newcommand*{\simplealuthreeop}{1&\ifdstandsrcoverlap{1}{2}&1&0&0&0&0&?}
-\newcommand*{\simplealuthreeopthirtytwo}{2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0&?}
-\newcommand*{\simplealutwoop}{1&\ifdstandsrcoverlap{1}{2}&1&0&0&0&0&?}
-\newcommand*{\simplealutwoopthirtytwo}{2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0&?}
-\newcommand*{\trivialtwooponecycle}{1&1&1&0&0&0&0&?}
-\newcommand*{\trivialtwooptwocycles}{2&1&2&0&0&0&0&?}
-\newcommand*{\shiftsandrotates}{1&\ifdstandsrcoverlapshift{2}{3}&1&0&0&0&0&?}
-\newcommand*{\shiftsandrotatesthirtytwo}{2&\ifdstandsrcoverlapshift{3}{4}&1&0&0&0&0&?}
-\newcommand*{\shiftsandrotatesalt}{1&3&1&0&0&0&0&?}
-\newcommand*{\shiftsandrotatesaltthirtytwo}{2&4&1&0&0&0&0&?}
-\newcommand*{\regcomp}{3&3&1&0&0&0&0&?}
-\newcommand*{\regcompimm}{3&3&1&0&0&0&0&?}
-\newcommand*{\cmov}{2&2&1&0&0&0&0&?}
-\newcommand*{\cmovimm}{2&3&1&0&0&0&0&?}
-\newcommand*{\minmax}{3&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0&?}
-\newcommand*{\indirectload}{\loadcost&1&1&1&0&0&0&?}
-\newcommand*{\directload}{\loadcost&1&1&1&0&0&0&?}
-\newcommand*{\indirectstoreimm}{\storecost&1&1&0&1&0&0&?}
-\newcommand*{\indirectstore}{\storecost&1&1&0&1&0&0&?}
-\newcommand*{\storeimm}{\storecost&1&1&0&1&0&0&?}
-\newcommand*{\directstore}{\storecost&1&1&0&1&0&0&?}
-\newcommand*{\branch}{\branchcost&1&1&0&0&0&0&?}
-\newcommand*{\branchimm}{\branchcost&1&1&0&0&0&0&?}
-\newcommand*{\divrem}{60&4&1&0&0&0&1&?}
-\newcommand*{\finish}[1]{#1&1&0&0&0&0&0&?}
+\newcommand*{\simplealuthreeop}{1&\ifdstandsrcoverlap{1}{2}&1&0&0&0&0}
+\newcommand*{\simplealuthreeopthirtytwo}{2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0}
+\newcommand*{\simplealutwoop}{1&\ifdstandsrcoverlap{1}{2}&1&0&0&0&0}
+\newcommand*{\simplealutwoopthirtytwo}{2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0}
+\newcommand*{\trivialtwooponecycle}{1&1&1&0&0&0&0}
+\newcommand*{\trivialtwooptwocycles}{2&1&2&0&0&0&0}
+\newcommand*{\shiftsandrotates}{1&\ifdstandsrcoverlapshift{2}{3}&1&0&0&0&0}
+\newcommand*{\shiftsandrotatesthirtytwo}{2&\ifdstandsrcoverlapshift{3}{4}&1&0&0&0&0}
+\newcommand*{\shiftsandrotatesalt}{1&3&1&0&0&0&0}
+\newcommand*{\shiftsandrotatesaltthirtytwo}{2&4&1&0&0&0&0}
+\newcommand*{\regcomp}{3&3&1&0&0&0&0}
+\newcommand*{\regcompimm}{3&3&1&0&0&0&0}
+\newcommand*{\cmov}{2&2&1&0&0&0&0}
+\newcommand*{\cmovimm}{2&3&1&0&0&0&0}
+\newcommand*{\minmax}{3&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0}
+\newcommand*{\indirectload}{\loadcost&1&1&1&0&0&0}
+\newcommand*{\directload}{\loadcost&1&1&1&0&0&0}
+\newcommand*{\indirectstoreimm}{\storecost&1&1&0&1&0&0}
+\newcommand*{\indirectstore}{\storecost&1&1&0&1&0&0}
+\newcommand*{\storeimm}{\storecost&1&1&0&1&0&0}
+\newcommand*{\directstore}{\storecost&1&1&0&1&0&0}
+\newcommand*{\branch}{\branchcost&1&1&0&0&0&0}
+\newcommand*{\branchimm}{\branchcost&1&1&0&0&0&0}
+\newcommand*{\divrem}{60&4&1&0&0&0&1}
+\newcommand*{\finish}[1]{#1&1&0&0&0&0&0}
 
 In the following table the $\mathbf{c}$, $\mathbf{k}$, $w$, and $\imath$ arguments are omitted for clarity.
 
-\renewcommand*{\mrule}{\cmidrule(lr){1-9}}
-\begin{longtable}[t]{p{30mm} p{12mm} p{12mm} p{4mm} p{4mm} p{4mm} p{4mm} p{4mm} p{4mm}}
+\renewcommand*{\mrule}{\cmidrule(lr){1-8}}
+\begin{longtable}[t]{p{30mm} p{12mm} p{12mm} p{4mm} p{4mm} p{4mm} p{4mm} p{4mm}}
   \toprule
-  \thead{\textbf{Instruction}} & \thead{$\cost¬cycles$} & \thead{$\cost¬decodeslots$} & \thead{$\cost¬execunits_{\ALU}$} & \thead{$\cost¬execunits_{\LOAD}$} & \thead{$\cost¬execunits_{\STORE}$} & \thead{$\cost¬execunits_{\MUL}$} & \thead{$\cost¬execunits_{\DIV}$} & \thead{$\inst¬compiledsize$} \\
+  \thead{\textbf{Instruction}} & \thead{$\cost¬cycles$} & \thead{$\cost¬decodeslots$} & \thead{$\cost¬execunits_{\ALU}$} & \thead{$\cost¬execunits_{\LOAD}$} & \thead{$\cost¬execunits_{\STORE}$} & \thead{$\cost¬execunits_{\MUL}$} & \thead{$\cost¬execunits_{\DIV}$} \\
   \midrule
   \endhead
-  \token{move\_reg}&0&1&0&0&0&0&0&? \\ \mrule
+  \token{move\_reg}&0&1&0&0&0&0&0 \\ \mrule
 
   \token{and}&\simplealuthreeop \\ \mrule
   \token{xor}&\simplealuthreeop \\ \mrule
@@ -1435,30 +1518,265 @@ \subsection{Gas Cost Tables}\label{sec:gascosttables}
   \token{rem\_u\_64}&\divrem \\ \mrule
   \token{rem\_s\_64}&\divrem \\ \mrule
 
-  \token{and\_inv}&2&3&1&0&0&0&0&?\\ \mrule
-  \token{or\_inv}&2&3&1&0&0&0&0&?\\ \mrule
-  \token{xnor}&2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0&?\\ \mrule
-  \token{neg\_add\_imm\_64}&2&3&1&0&0&0&0&?\\ \mrule
-  \token{neg\_add\_imm\_32}&3&4&1&0&0&0&0&?\\ \mrule
-  \token{load\_imm}&1&1&0&0&0&0&0&?\\ \mrule
-  \token{load\_imm\_64}&1&2&0&0&0&0&0&?\\ \mrule
-
-  \token{mul\_64}&3&\ifdstandsrcoverlap{1}{2}&1&0&0&1&0&?\\ \mrule
-  \token{mul\_32}&4&\ifdstandsrcoverlap{2}{3}&1&0&0&1&0&?\\ \mrule
-  \token{mul\_imm\_64}&3&\ifdstandsrcoverlap{1}{2}&1&0&0&1&0&?\\ \mrule
-  \token{mul\_imm\_32}&4&\ifdstandsrcoverlap{2}{3}&1&0&0&1&0&?\\ \mrule
-  \token{mul\_upper\_s\_s}&4&4&1&0&0&1&0&?\\ \mrule
-  \token{mul\_upper\_u\_u}&4&4&1&0&0&1&0&?\\ \mrule
-  \token{mul\_upper\_s\_u}&6&4&1&0&0&1&0&?\\ \mrule
+  \token{and\_inv}&2&3&1&0&0&0&0\\ \mrule
+  \token{or\_inv}&2&3&1&0&0&0&0\\ \mrule
+  \token{xnor}&2&\ifdstandsrcoverlap{2}{3}&1&0&0&0&0\\ \mrule
+  \token{neg\_add\_imm\_64}&2&3&1&0&0&0&0\\ \mrule
+  \token{neg\_add\_imm\_32}&3&4&1&0&0&0&0\\ \mrule
+  \token{load\_imm}&1&1&0&0&0&0&0\\ \mrule
+  \token{load\_imm\_64}&1&2&0&0&0&0&0\\ \mrule
+
+  \token{mul\_64}&3&\ifdstandsrcoverlap{1}{2}&1&0&0&1&0\\ \mrule
+  \token{mul\_32}&4&\ifdstandsrcoverlap{2}{3}&1&0&0&1&0\\ \mrule
+  \token{mul\_imm\_64}&3&\ifdstandsrcoverlap{1}{2}&1&0&0&1&0\\ \mrule
+  \token{mul\_imm\_32}&4&\ifdstandsrcoverlap{2}{3}&1&0&0&1&0\\ \mrule
+  \token{mul\_upper\_s\_s}&4&4&1&0&0&1&0\\ \mrule
+  \token{mul\_upper\_u\_u}&4&4&1&0&0&1&0\\ \mrule
+  \token{mul\_upper\_s\_u}&6&4&1&0&0&1&0\\ \mrule
 
   \token{trap}&\finish{2} \\ \mrule
   \token{fallthrough}&\finish{2}\\ \mrule
-  \token{unlikely}&40&1&0&0&0&0&0&?\\ \mrule
+  \token{unlikely}&40&1&0&0&0&0&0\\ \mrule
   \token{jump}&\finish{15}\\ \mrule
   \token{load\_imm\_jump}&\finish{15}\\ \mrule
-  \token{jump\_ind}&22&1&0&0&0&0&0&?\\ \mrule
-  \token{load\_imm\_jump\_ind}&22&1&0&0&0&0&0&?\\ \mrule
+  \token{jump\_ind}&22&1&0&0&0&0&0\\ \mrule
+  \token{load\_imm\_jump\_ind}&22&1&0&0&0&0&0\\ \mrule
 
-  \token{ecalli}&100&4&1&0&0&0&0&?\\
+  \token{ecalli}&100&4&1&0&0&0&0\\
 \bottomrule
 \end{longtable}
+
+\subsection{Compiled Sizes}\label{sec:compiledsizes}
+
+$\inst¬compiledsize$ is given by the following table. $\srcdsteq{i}$ holds when the destination register coincides with the $i$-th source register; $\reg_b$ is the base register used by a load or store for address computation; and $t_1 = 3$ and $t_2 = 4$ are the two guest registers (\textsc{pvm}'s $\mathtt{T1}$ and $\mathtt{T2}$) whose underlying native registers force, respectively, a displacement byte and an index byte in native addressing. The decoded immediates $\immed_X, \immed_Y$ are as defined in section \ref{sec:instructiontables}. The direct branch and jump instructions are an exception: each consists of a fixed prefix (a register comparison or an immediate load) followed by a relative jump to its target basic block, and the translator encodes that jump in a compact 2-byte form precisely when the target has \emph{already} been translated (it lies at or before $\imath$, a backward branch) and is within a signed byte's reach; otherwise a longer form is used. Their size is therefore layout-dependent, given by $\branchsize(t, p, r, R)$ for a branch whose target is basic block $t$, whose fixed prefix is $p$ bytes, and whose trailing jump occupies $r$ bytes when short and $R$ when long:
+\begin{equation}
+  \branchsize(t, p, r, R) \equiv p + \begin{cases}
+    r &\when t \le \imath \;\wedge\; -128 \le \Delta \le 127 \\
+    R &\otherwise
+  \end{cases}
+  \quad\where \Delta = \codeoffset(\mathbf{c}, \mathbf{k}, t) - \left(\codeoffset(\mathbf{c}, \mathbf{k}, \imath) + \bbpreamblesize(\imath) + p + r\right)
+\end{equation}
+For the register-immediate branches the comparison prefix $q$ is smaller when the immediate fits in a signed byte:
+\begin{equation}
+  q = \begin{cases} 4 &\when -128 \le \signed{\immed_X} \le 127 \\ 7 &\otherwise \end{cases}
+\end{equation}
+
+\renewcommand*{\mrule}{\cmidrule(lr){1-2}}
+\newcommand*{\csbranch}{$\branchsize(\immed_X, 3, 2, 6)$}
+\newcommand*{\csbranchimm}{$\branchsize(\immed_Y, q, 2, 6)$}
+\newcommand*{\srcone}[2]{$\begin{cases}
+    #1 &\when \srcdsteq{1} \\
+    #2 &\otherwise
+  \end{cases}$}
+\newcommand*{\srctwo}[2]{$\begin{cases}
+    #1 &\when \srcdsteq{1} \lor \srcdsteq{2} \\
+    #2 &\otherwise
+  \end{cases}$}
+\newcommand*{\srcimm}[3]{$\begin{cases}
+    #1 &\when \srcdsteq{1} \land {-}128 \le \signed{\immed_X} \le 127 \\
+    #2 &\when \srcdsteq{1} \lor {-}128 \le \signed{\immed_X} \le 127 \\
+    #3 &\otherwise
+  \end{cases}$}
+\newcommand*{\setltimm}{$\begin{cases}
+    12 &\when \srcdsteq{1} \land {-}128 \le \signed{\immed_X} \le 127 \\
+    15 &\when \srcdsteq{1} \\
+    11 &\when \lnot \srcdsteq{1} \land {-}128 \le \signed{\immed_X} \le 127 \\
+    14 &\otherwise
+  \end{cases}$}
+\newcommand*{\indbase}[5]{$\begin{cases}
+    #1 &\when \reg_b \notin \set{t_1, t_2} \land \immed_X = 0 \\
+    #2 &\when (\reg_b \ne t_2 \land {-}128 \le \signed{\immed_X} \le 127) \lor (\reg_b = t_2 \land \immed_X = 0) \\
+    #3 &\when \reg_b \ne t_2 \\
+    #4 &\when \reg_b = t_2 \land {-}128 \le \signed{\immed_X} \le 127 \\
+    #5 &\otherwise
+  \end{cases}$}
+\newcommand*{\loadsx}[2]{$\begin{cases}
+    #1 &\when \signed{\immed_X} < 0 \\
+    #2 &\otherwise
+  \end{cases}$}
+{\footnotesize
+\begin{longtable}{p{30mm} l}
+  \toprule
+  \thead{\textbf{Instruction}} & \thead{$\inst¬compiledsize$} \\
+  \midrule
+  \endhead
+  \token{move\_reg}&3 \\ \mrule
+  \token{and}&\srctwo{3}{6} \\ \mrule
+  \token{xor}&\srctwo{3}{6} \\ \mrule
+  \token{or}&\srctwo{3}{6} \\ \mrule
+  \token{add\_64}&\srctwo{3}{6} \\ \mrule
+  \token{sub\_64}&\srcone{3}{6} \\ \mrule
+  \token{add\_32}&\srctwo{6}{9} \\ \mrule
+  \token{sub\_32}&\srcone{6}{9} \\ \mrule
+  \token{and\_imm}&\srcimm{4}{7}{10} \\ \mrule
+  \token{xor\_imm}&\srcimm{4}{7}{10} \\ \mrule
+  \token{or\_imm}&\srcimm{4}{7}{10} \\ \mrule
+  \token{add\_imm\_64}&\srcimm{4}{7}{10} \\ \mrule
+  \token{shlo\_r\_imm\_64}&\srcone{4}{7} \\ \mrule
+  \token{shar\_r\_imm\_64}&\srcone{4}{7} \\ \mrule
+  \token{shlo\_l\_imm\_64}&\srcone{4}{7} \\ \mrule
+  \token{rot\_r\_64\_imm}&\srcone{4}{7} \\ \mrule
+  \token{reverse\_bytes}&\srcone{3}{6} \\ \mrule
+  \token{add\_imm\_32}&\srcimm{7}{10}{13} \\ \mrule
+  \token{shlo\_r\_imm\_32}&\srcone{7}{10} \\ \mrule
+  \token{shar\_r\_imm\_32}&\srcone{7}{10} \\ \mrule
+  \token{shlo\_l\_imm\_32}&\srcone{7}{10} \\ \mrule
+  \token{rot\_r\_32\_imm}&\srcone{7}{10} \\ \mrule
+  \token{count\_set\_bits\_64}&5 \\ \mrule
+  \token{count\_set\_bits\_32}&5 \\ \mrule
+  \token{leading\_zero\_bits\_64}&5 \\ \mrule
+  \token{leading\_zero\_bits\_32}&5 \\ \mrule
+  \token{sign\_extend\_8}&4 \\ \mrule
+  \token{sign\_extend\_16}&4 \\ \mrule
+  \token{zero\_extend\_16}&4 \\ \mrule
+  \token{trailing\_zero\_bits\_64}&5 \\ \mrule
+  \token{trailing\_zero\_bits\_32}&5 \\ \mrule
+  \token{shlo\_l\_64}&\srcone{6}{9} \\ \mrule
+  \token{shlo\_r\_64}&\srcone{6}{9} \\ \mrule
+  \token{shar\_r\_64}&\srcone{6}{9} \\ \mrule
+  \token{rot\_l\_64}&\srcone{6}{9} \\ \mrule
+  \token{rot\_r\_64}&\srcone{6}{9} \\ \mrule
+  \token{shlo\_l\_32}&\srcone{9}{12} \\ \mrule
+  \token{shlo\_r\_32}&\srcone{9}{12} \\ \mrule
+  \token{shar\_r\_32}&\srcone{9}{12} \\ \mrule
+  \token{rot\_l\_32}&\srcone{9}{12} \\ \mrule
+  \token{rot\_r\_32}&\srcone{9}{12} \\ \mrule
+  \token{shlo\_l\_imm\_alt\_64}&13 \\ \mrule
+  \token{shlo\_r\_imm\_alt\_64}&13 \\ \mrule
+  \token{shar\_r\_imm\_alt\_64}&13 \\ \mrule
+  \token{rot\_r\_64\_imm\_alt}&13 \\ \mrule
+  \token{shlo\_l\_imm\_alt\_32}&15 \\ \mrule
+  \token{shlo\_r\_imm\_alt\_32}&15 \\ \mrule
+  \token{shar\_r\_imm\_alt\_32}&15 \\ \mrule
+  \token{rot\_r\_32\_imm\_alt}&15 \\ \mrule
+  \token{set\_lt\_u}&\srctwo{11}{10} \\ \mrule
+  \token{set\_lt\_s}&\srctwo{11}{10} \\ \mrule
+  \token{set\_lt\_u\_imm}&\setltimm \\ \mrule
+  \token{set\_lt\_s\_imm}&\setltimm \\ \mrule
+  \token{set\_gt\_u\_imm}&\setltimm \\ \mrule
+  \token{set\_gt\_s\_imm}&\setltimm \\ \mrule
+  \token{cmov\_iz}&\srcone{0}{7} \\ \mrule
+  \token{cmov\_nz}&\srcone{0}{7} \\ \mrule
+  \token{cmov\_iz\_imm}&14 \\ \mrule
+  \token{cmov\_nz\_imm}&14 \\ \mrule
+  \token{max}&\srctwo{7}{10} \\ \mrule
+  \token{max\_u}&\srctwo{7}{10} \\ \mrule
+  \token{min}&\srctwo{7}{10} \\ \mrule
+  \token{min\_u}&\srctwo{7}{10} \\ \mrule
+  \token{load\_ind\_u8}&\indbase{5}{6}{9}{7}{10} \\ \mrule
+  \token{load\_ind\_i8}&\indbase{5}{6}{9}{7}{10} \\ \mrule
+  \token{load\_ind\_u16}&\indbase{5}{6}{9}{7}{10} \\ \mrule
+  \token{load\_ind\_i16}&\indbase{5}{6}{9}{7}{10} \\ \mrule
+  \token{load\_ind\_u32}&\indbase{4}{5}{8}{6}{9} \\ \mrule
+  \token{load\_ind\_i32}&\indbase{4}{5}{8}{6}{9} \\ \mrule
+  \token{load\_ind\_u64}&\indbase{4}{5}{8}{6}{9} \\ \mrule
+  \token{load\_u8}&\loadsx{10}{9} \\ \mrule
+  \token{load\_i8}&\loadsx{10}{9} \\ \mrule
+  \token{load\_u16}&\loadsx{10}{9} \\ \mrule
+  \token{load\_i16}&\loadsx{10}{9} \\ \mrule
+  \token{load\_u32}&\loadsx{9}{8} \\ \mrule
+  \token{load\_i32}&\loadsx{9}{8} \\ \mrule
+  \token{load\_u64}&\loadsx{9}{8} \\ \mrule
+  \token{store\_imm\_ind\_u8}&\indbase{5}{6}{9}{7}{10} \\ \mrule
+  \token{store\_imm\_ind\_u16}&\indbase{7}{8}{11}{9}{12} \\ \mrule
+  \token{store\_imm\_ind\_u32}&\indbase{8}{9}{12}{10}{13} \\ \mrule
+  \token{store\_imm\_ind\_u64}&\indbase{8}{9}{12}{10}{13} \\ \mrule
+  \token{store\_ind\_u8}&\indbase{4}{5}{8}{6}{9} \\ \mrule
+  \token{store\_ind\_u16}&\indbase{5}{6}{9}{7}{10} \\ \mrule
+  \token{store\_ind\_u32}&\indbase{4}{5}{8}{6}{9} \\ \mrule
+  \token{store\_ind\_u64}&\indbase{4}{5}{8}{6}{9} \\ \mrule
+  \token{store\_imm\_u8}&\loadsx{10}{9} \\ \mrule
+  \token{store\_imm\_u16}&\loadsx{12}{11} \\ \mrule
+  \token{store\_imm\_u32}&\loadsx{13}{12} \\ \mrule
+  \token{store\_imm\_u64}&\loadsx{13}{12} \\ \mrule
+  \token{store\_u8}&\loadsx{9}{8} \\ \mrule
+  \token{store\_u16}&\loadsx{10}{9} \\ \mrule
+  \token{store\_u32}&\loadsx{9}{8} \\ \mrule
+  \token{store\_u64}&\loadsx{9}{8} \\ \mrule
+  \token{div\_u\_32}&15 \\ \mrule
+  \token{div\_s\_32}&15 \\ \mrule
+  \token{rem\_u\_32}&15 \\ \mrule
+  \token{rem\_s\_32}&15 \\ \mrule
+  \token{div\_u\_64}&15 \\ \mrule
+  \token{div\_s\_64}&15 \\ \mrule
+  \token{rem\_u\_64}&15 \\ \mrule
+  \token{rem\_s\_64}&15 \\ \mrule
+  \token{and\_inv}&5 \\ \mrule
+  \token{or\_inv}&$\begin{cases}
+    6 &\when \srcdsteq{2} \land \lnot \srcdsteq{1} \\
+    9 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{xnor}&\srctwo{6}{9} \\ \mrule
+  \token{neg\_add\_imm\_64}&$\begin{cases}
+    3 &\when \srcdsteq{1} \land \immed_X = 0 \\
+    7 &\when \srcdsteq{1} \land {-}128 \le \signed{\immed_X} \le 127 \\
+    6 &\when \lnot \srcdsteq{1} \land \immed_X = 0 \\
+    10 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{neg\_add\_imm\_32}&$\begin{cases}
+    6 &\when \srcdsteq{1} \land \immed_X = 0 \\
+    10 &\when \srcdsteq{1} \land {-}128 \le \signed{\immed_X} \le 127 \\
+    13 &\when \srcdsteq{1} \\
+    9 &\when \lnot \srcdsteq{1} \land \immed_X = 0 \\
+    12 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{load\_imm}&$\begin{cases}
+    7 &\when \signed{\immed_X} \le 0 \\
+    6 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{load\_imm\_64}&$\begin{cases}
+    6 &\when \immed_X < 2^{32} \\
+    10 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{mul\_64}&\srctwo{4}{7} \\ \mrule
+  \token{mul\_32}&\srctwo{7}{10} \\ \mrule
+  \token{mul\_imm\_64}&$\begin{cases}
+    4 &\when {-}128 \le \signed{\immed_X} \le 127 \\
+    7 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{mul\_imm\_32}&$\begin{cases}
+    7 &\when {-}128 \le \signed{\immed_X} \le 127 \\
+    10 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{mul\_upper\_s\_s}&16 \\ \mrule
+  \token{mul\_upper\_u\_u}&13 \\ \mrule
+  \token{mul\_upper\_s\_u}&29 \\ \mrule
+  \token{trap}&13 \\ \mrule
+  \token{fallthrough}&0 \\ \mrule
+  \token{unlikely}&0 \\ \mrule
+  \token{branch\_eq}&\csbranch \\ \mrule
+  \token{branch\_ne}&\csbranch \\ \mrule
+  \token{branch\_lt\_u}&\csbranch \\ \mrule
+  \token{branch\_lt\_s}&\csbranch \\ \mrule
+  \token{branch\_ge\_u}&\csbranch \\ \mrule
+  \token{branch\_ge\_s}&\csbranch \\ \mrule
+  \token{branch\_eq\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_ne\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_lt\_u\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_le\_u\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_ge\_u\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_gt\_u\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_lt\_s\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_le\_s\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_ge\_s\_imm}&\csbranchimm \\ \mrule
+  \token{branch\_gt\_s\_imm}&\csbranchimm \\ \mrule
+  \token{jump}&$\branchsize(\immed_X, 0, 2, 5)$ \\ \mrule
+  \token{load\_imm\_jump}&$\branchsize(\immed_Y, 7, 2, 5)$ \\ \mrule
+  \token{jump\_ind}&$\begin{cases}
+    11 &\when \immed_X = 0 \\
+    13 &\when \reg_b \ne t_2 \land {-}128 \le \signed{\immed_X} \le 127 \\
+    16 &\when \reg_b \ne t_2 \\
+    14 &\when \reg_b = t_2 \land {-}128 \le \signed{\immed_X} \le 127 \\
+    17 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{load\_imm\_jump\_ind}&$\begin{cases}
+    18 &\when \immed_Y = 0 \\
+    20 &\when \reg_b \ne t_2 \land {-}128 \le \signed{\immed_Y} \le 127 \\
+    23 &\when \reg_b \ne t_2 \\
+    21 &\when \reg_b = t_2 \land {-}128 \le \signed{\immed_Y} \le 127 \\
+    24 &\otherwise
+  \end{cases}$ \\ \mrule
+  \token{ecalli}&29 \\
+  \bottomrule
+\end{longtable}
+}
diff --git a/text/pvm_invocations.tex b/text/pvm_invocations.tex
index f8757fd5..176b64f7 100644
--- a/text/pvm_invocations.tex
+++ b/text/pvm_invocations.tex
@@ -213,7 +213,7 @@ \subsection{Accumulate Invocation}\label{sec:accumulateinvocation}
     \multicolumn{2}{l}{\also \gascounter' = \gascounter - \Cgasunknown}
   \end{cases} \\
   G&\colon\abracegroup{
-    \tuple{\tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \sequence{\optional{\pageid}}, \serviceaccount}, \implicationspair} &\to \tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \implicationspair} \\
+    \tuple{\tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \sequence{\optional{\pageid}}, \serviceaccount}, \implicationspair} &\to \tuple{\set{\continue, \halt, \panic, \oog}, \gas, \regs, \ram, \sequence{\optional{\pageid}}, \implicationspair} \\
     \tup{\tup{\execst, \gascounter, \registers, \memory, \workingset, \mathbf{s}}, \imXY} &\mapsto \tup{\execst, \gascounter, \registers, \memory, \workingset, \tup{\imX^*, \imY}} \\
     &\qquad \where \imX^* = \imX \exc \imX^*_\im¬self = \mathbf{s}
   }\\
@@ -291,6 +291,52 @@ \subsection{General Functions}\label{sec:generalfunctions}
 \end{equation}
 With base cost $c$, total gas is $c + \fnmemgas(L, \ell)$. The host-call table below uses this formula for all memory-sized terms.
 
+Host-call inspections and mutations of a machine's \textsc{ram} may carry a memory-hierarchy cost beyond the nominal $g$ of the tables below, depending on what lies at the other end of the transfer. Where that end is itself a \textsc{pvm} machine the access is charged through the working-set, via $\wscharge¬internal$, as an ordinary \textsc{pvm} memory access would be:
+\begin{equation}
+  \begin{aligned}
+    \wscharge¬internal(g, w, \mem, \mathbf{m}, \mathbf{a}) &= \begin{cases}
+      \tup{\continue, g, w, \mem, \mathbf{m}} &\when \mathbf{a} = \sq{} \\
+      \tup{\oog, g, w, \mem, \mathbf{m}} &\otherwhen g < g^\delta \\
+      \wscharge¬internal(g - g^\delta, w', \mem', \mathbf{m}', \mathbf{a}\sub{1\dots}) &\otherwise
+    \end{cases} \\
+    \where \tup{m, x} &= \mathbf{a}_0\,,\quad i = \floor{\nicefrac{x}{\Cpvmpagesize}}\,,\quad \mu = \begin{cases} \mem &\when m = \none \\ \mathbf{m}\subb{m}_\pg¬ram &\otherwise \end{cases} \\
+    \also (g^\delta, w') &= \gascostforpageaccess(w, \tup{m, \datapage{i}}, \pagefaultcost(\mu, i)) \\
+    \also \tup{\mem', \mathbf{m}'} &= \begin{cases}
+      \tup{\mem \exc \mem'_\ram¬frames\subb{i} = \frame¬present,\ \mathbf{m}} &\when m = \none \\
+      \tup{\mem,\ \mathbf{m} \exc (\mathbf{m}'\subb{m}_\pg¬ram)_\ram¬frames\subb{i} = \frame¬present} &\otherwise
+    \end{cases}
+  \end{aligned}
+\end{equation}
+
+In cases where access exchanges data between the invoking machine's \textsc{ram} and the node's state or context (which lies outside any machine's paged memory and so is never resident in a working-set) the exact mechanism depends on the \emph{direction} of the data transfer.
+
+Octets \emph{read out of} a machine's \textsc{ram} neither provision a frame nor alter the working-set, and carry no charge beyond the host-call's nominal $\fnmemgas$ term.
+
+Octets \emph{written into} a machine's \textsc{ram} likewise stay out of the working-set (so the machine faults ordinarily on its next access to any of them), however they \emph{do} provision a new frame where none yet exists, paying the allocation-and-fill cost a first-touch fault would, less the base $\Cpvmgaspagefault$ (which is deferred to that eventual fault). Such data, having bypassed the working-set, is not resident when the machine reads it back; this read-back premium is not levied separately but folded into the nominal per-octet cost of each delivering host-call, whose memory rate is accordingly raised by $\Cpvmgasdeliver$ (gas per 1024 octets). The accessibility check, the provisioning and the write are the work of the shared function $\wscharge¬extwrite$ which writes $l$ octets of a value $\mathbf{v}$ from offset $f$ into the invoking machine's \textsc{ram} at $o$, charging against the post-nominal gas $g_0$:
+\begin{equation}
+  \begin{aligned}
+    \wscharge¬extwrite(g_0, \registers, \memory, o, \mathbf{v}, f, l) &\equiv \begin{cases}
+      \tup{\panic, \registers_7, \memory, g_0} &\when \mathbf{v} = \error \vee \Nrange{o}{l} \not\subseteq \writable{\memory} \\
+      \tup{\continue, \mathtt{NONE}, \memory, g_0} &\otherwhen \mathbf{v} = \none \\
+      \tup{\oog, \registers_7, \memory^\uparrow, \gascounter^\uparrow} &\otherwhen \varepsilon^\uparrow = \oog \\
+      \tup{\continue, \len{\mathbf{v}}, \memory^\uparrow \exc (\memory^\uparrow)\subrange{o}{l} = \mathbf{v}\subrange{f}{l}, \gascounter^\uparrow} &\otherwise
+    \end{cases} \\
+    \where \tup{\varepsilon^\uparrow, \gascounter^\uparrow, \memory^\uparrow} &= P(g_0, \memory, \mathbf{i}) \\
+    \also \mathbf{i} &= \spannedpages(o, l)~(\ref{eq:pagespan}) \\
+    \also P(g, \mem, \mathbf{i}) &= \begin{cases}
+      \tup{\continue, g, \mem} &\when \mathbf{i} = \sq{} \\
+      \tup{\oog, g, \mem} &\otherwhen g < g^\delta \\
+      P(g - g^\delta, \mem', \mathbf{i}\sub{1\dots}) &\otherwise
+    \end{cases} \\
+    \also g^\delta &= \pagefaultcost(\mem, \mathbf{i}_0) - \Cpvmgaspagefault \\
+    \also \mem' &= \mem \exc \mem'_\ram¬frames\subb{\mathbf{i}_0} = \frame¬present
+  \end{aligned}
+\end{equation}
+
+Such an access touches the octets of its range one at a time in ascending order of address, each octet an access of its containing page. Accessibility is checked before any charge, so these charges never fault, though they may exhaust gas.
+
+Should the gas run out mid-way, the result is $\oog$; the gas counter and the frames provisioned so far retain the charges already made, though no octets are written into \textsc{ram}. As $\oog$ discards the whole invocation's output, the surrounding context is immaterial and taken as its prior value. All of this is levied after the nominal $g$ of the tables below. In the descriptions that follow, the working-set argument and result are elided except where a function threads them explicitly.
+
 \aboverulesep = 1.5mm \belowrulesep = 2mm
 
 \begin{longtable}{p{5cm} p{11cm}}
@@ -344,7 +390,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
   \makecell*[l]{
   $\Omega_Y(\gascounter, \registers, \memory, p, n, \mathbf{r}, i, \overline{\mathbf{i}}, \overline{\mathbf{x}}, \mathbf{i}, \dots)$ \\
   \texttt{fetch} = 2 \\
-  $g = \CgasYc{c} + \fnmemgas(\CgasYl{c}, z)$} &
+  $g = \CgasYc{c} + \fnmemgas(\CgasYl{c} + \Cpvmgasdeliver, z)$} &
   $\begin{aligned}
     \using c &= \begin{cases}
       \registers_{10} &\when \registers_{10} < 16 \\
@@ -406,17 +452,13 @@ \subsection{General Functions}\label{sec:generalfunctions}
     \using \sq{o, f_0, z} &= \registers\subrange{7}{3} \\
     \using f &= \min(f_0, \len{\mathbf{v}}) \\
     \using l &= \min(z, \len{\mathbf{v}} - f) \\
-    \tup{\execst', \registers'_7, \memory'\subrange{o}{l}} &\equiv \begin{cases}
-      \tup{\panic, \registers_7, \memory\subrange{o}{l}} &\when \Nrange{o}{l} \not\subseteq \writable{\memory} \\
-      \tup{\continue, \mathtt{NONE}, \memory\subrange{o}{l}} &\otherwhen \mathbf{v} = \none \\
-      \tup{\continue, \len{\mathbf{v}}, \mathbf{v}\subrange{f}{l}} &\otherwise \\
-    \end{cases}
+    \tup{\execst', \registers'_7, \memory', \gascounter'} &\equiv \wscharge¬extwrite(\gascounter - g, \registers, \memory, o, \mathbf{v}, f, l)
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
   $\Omega_L(\gascounter, \registers, \memory, \mathbf{s}, s, \mathbf{d})$ \\
   \texttt{lookup} = 3 \\
-  $g = \CgasLconst + \fnmemgas(\CgasLlinear, z) $} &
+  $g = \CgasLconst + \fnmemgas(\CgasLlinear + \Cpvmgasdeliver, z) $} &
   $\begin{aligned}
     \using \mathbf{a} &= \begin{cases}
       \mathbf{s} &\when \registers_7 \in \set{ s, 2^{64} - 1 } \\
@@ -432,17 +474,13 @@ \subsection{General Functions}\label{sec:generalfunctions}
     \end{cases} \\
     \using f &= \min(\registers_{10}, \len{\mathbf{v}}) \\
     \using l &= \min(z, \len{\mathbf{v}} - f) \\
-    \tup{\execst', \registers'_7, \memory'\subrange{o}{l}} &\equiv \begin{cases}
-      \tup{\panic, \registers_7, \memory\subrange{o}{l}} &\when \mathbf{v} = \error \vee \Nrange{o}{l} \not\subseteq \writable{\memory}\\
-      \tup{\continue, \mathtt{NONE}, \memory\subrange{o}{l}} &\otherwhen \mathbf{v} = \none \\
-      \tup{\continue, \len{\mathbf{v}}, \mathbf{v}\subrange{f}{l}} &\otherwise \\
-    \end{cases}
+    \tup{\execst', \registers'_7, \memory', \gascounter'} &\equiv \wscharge¬extwrite(\gascounter - g, \registers, \memory, o, \mathbf{v}, f, l)
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
   $\Omega_R(\gascounter, \registers, \memory, \mathbf{s}, s, \mathbf{d})$ \\
   \texttt{read} = 4 \\
-  $g = \CgasRconst + \fnmemgas(\CgasRkeylinear, k_Z) + \fnmemgas(\CgasRvallinear, v_Z) $} &
+  $g = \CgasRconst + \fnmemgas(\CgasRkeylinear, k_Z) + \fnmemgas(\CgasRvallinear + \Cpvmgasdeliver, v_Z) $} &
   $\begin{aligned}
     \using s^* &= \begin{cases}
       s &\when \registers_7 = 2^{64} - 1 \\
@@ -462,11 +500,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
     \end{cases} \\
     \using f &= \min(\registers_{11}, \len{\mathbf{v}}) \\
     \using l &= \min(v_Z, \len{\mathbf{v}} - f) \\
-    \tup{\execst', \registers'_7, \memory'\subrange{o}{l}} &\equiv \begin{cases}
-      \tup{\panic, \registers_7, \memory\subrange{o}{l}} &\when \mathbf{v} = \error \vee \Nrange{o}{l} \not\subseteq \writable{\memory}\\
-      \tup{\continue, \mathtt{NONE}, \memory\subrange{o}{l}} &\otherwhen \mathbf{v} = \none \\
-      \tup{\continue, \len{\mathbf{v}}, \mathbf{v}\subrange{f}{l}} &\otherwise \\
-    \end{cases}
+    \tup{\execst', \registers'_7, \memory', \gascounter'} &\equiv \wscharge¬extwrite(\gascounter - g, \registers, \memory, o, \mathbf{v}, f, l)
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
@@ -498,7 +532,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
   \makecell*[l]{
   $\Omega_I(\gascounter, \registers, \memory, s, \mathbf{d})$ \\
   \texttt{info} = 6 \\
-  $g = \CgasI$} &
+  $g = \CgasI + \fnmemgas(\Cpvmgasdeliver, \registers_{10})$} &
   $\begin{aligned}
     \using \mathbf{a} &= \begin{cases}
       \mathbf{d}\subb{s} &\when \registers_7 = 2^{64} - 1 \\
@@ -517,11 +551,7 @@ \subsection{General Functions}\label{sec:generalfunctions}
     \end{cases} \\
     \using f &= \min(\registers_{9}, \len{\mathbf{v}}) \\
     \using l &= \min(\registers_{10}, \len{\mathbf{v}} - f) \\
-    \tup{\execst', \registers'_7, \memory'\subrange{o}{l}} &\equiv \begin{cases}
-      \tup{\panic, \registers_7, \memory\subrange{o}{l}} &\when \mathbf{v} = \error \vee \Nrange{o}{l} \not\subseteq \writable{\memory}\\
-      \tup{\continue, \mathtt{NONE}, \memory\subrange{o}{l}} &\otherwhen \mathbf{v} = \none \\
-      \tup{\continue, \len{\mathbf{v}}, \mathbf{v}\subrange{f}{l}} &\otherwise \\
-    \end{cases}
+    \tup{\execst', \registers'_7, \memory', \gascounter'} &\equiv \wscharge¬extwrite(\gascounter - g, \registers, \memory, o, \mathbf{v}, f, l)
   \end{aligned}$ \\
   \bottomrule
 \end{longtable}
@@ -531,9 +561,9 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
 These assume some refine context pair $\tup{\mathbf{m}, \mathbf{e}} \in \tuple{\dictionary{\N}{\innerpvm}, \sequence{\segment}}$, which are both initially empty. Other than the gas-counter which is explicitly defined, elements of \textsc{pvm} state are each assumed to remain unchanged by the host-call unless explicitly specified.
 \begin{align}
   \gascounter' &\equiv \gascounter - g\\
-  \tup{\execst', \registers', \memory'} &\equiv \begin{cases}
-    \tup{\oog, \registers, \memory} &\when \gascounter < g\\
-    \tup{\continue, \registers, \memory} \text{ except as indicated below} &\otherwise
+  \tup{\execst', \registers', \memory', \workingset'} &\equiv \begin{cases}
+    \tup{\oog, \registers, \memory, \workingset} &\when \gascounter < g\\
+    \tup{\continue, \registers, \memory, \workingset} \text{ except as indicated below} &\otherwise
   \end{cases}
 \end{align}
 
@@ -546,7 +576,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \makecell*[l]{
   $\Omega_H(\gascounter, \registers, \memory, s, \mathbf{d}, t)$ \\
   \texttt{historical\_lookup} = 7 \\
-  $g = \CgasHconst + \fnmemgas(\CgasHlinear, z)$} &
+  $g = \CgasHconst + \fnmemgas(\CgasHlinear + \Cpvmgasdeliver, z)$} &
   $\begin{aligned}
     \using \mathbf{a} &= \begin{cases}
       \mathbf{d}\subb{s} &\when \registers_7 = 2^{64} - 1 \wedge s \in \keys{\mathbf{d}} \\
@@ -562,11 +592,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
     \end{cases} \\
     \using f &= \min(\registers_{10}, \len{\mathbf{v}}) \\
     \using l &= \min(z, \len{\mathbf{v}} - f) \\
-    \tup{\execst', \registers'_7, \memory'\subrange{o}{l}} &\equiv \begin{cases}
-      \tup{\panic, \registers_7, \memory\subrange{o}{l}} &\when \mathbf{v} = \error \vee \Nrange{o}{l} \not\subseteq \writable{\memory}\\
-      \tup{\continue, \mathtt{NONE}, \memory\subrange{o}{l}} &\otherwhen \mathbf{v} = \none \\
-      \tup{\continue, \len{\mathbf{v}}, \mathbf{v}\subrange{f}{l}} &\otherwise \\
-    \end{cases}
+    \tup{\execst', \registers'_7, \memory', \gascounter'} &\equiv \wscharge¬extwrite(\gascounter - g, \registers, \memory, o, \mathbf{v}, f, l)
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
@@ -598,7 +624,7 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
       \error &\otherwise
     \end{cases} \\
     \using n &= \min(n \in \N : n \not\in \keys{\mathbf{m}}) \\
-    \using \mathbf{u} &= \tup{\is{\ram¬value}{[0, 0, \dots]},\is{\ram¬access}{[\none, \none, \dots]}} \\
+    \using \mathbf{u} &= \tup{\is{\ram¬value}{[0, 0, \dots]},\is{\ram¬access}{[\none, \none, \dots]},\is{\ram¬frames}{[\frame¬missing¬zero, \frame¬missing¬zero, \dots]}} \\
     \tup{\execst', \registers'_7, \mathbf{m}} &\equiv \begin{cases}
       \tup{\continue, \mathtt{FULL}, \mathbf{m}} &\when \len{\mathbf{m}} \ge 63 \\
       \tup{\panic, \registers_7, \mathbf{m}} &\otherwhen \mathbf{p} = \error \\
@@ -608,37 +634,45 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_P(\gascounter, \registers, \memory, \mathbf{m})$ \\
+  $\Omega_P(\gascounter, \registers, \memory, \workingset, \mathbf{m})$ \\
   \texttt{peek} = 10 \\
   $g = \CgasPconst + \fnmemgas(\CgasPlinear, z)$ }&
   $\begin{aligned}
     \using \sq{n, o, s, z} &= \registers\subrange{7}{4} \\
-    \tup{\execst', \registers'_7, \mem'} &\equiv \begin{cases}
-      \tup{\panic, \registers_7, \mem} &\when \Nrange{o}{z} \not\subseteq \writable{\memory} \\
-      \tup{\continue, \mathtt{WHO}, \mem} &\otherwhen n \not\in \keys{\mathbf{m}} \\
-      \tup{\continue, \mathtt{OOB}, \mem} &\otherwhen \Nrange{s}{z} \not\subseteq \readable{\mathbf{m}\subb{n}_\pg¬ram} \\
-      \tup{\continue, \mathtt{OK}, \mem'} &\otherwise \\
-      \multicolumn{2}{l}{\where \mem' = \mem \exc \mem\subrange{o}{z} = (\mathbf{m}\subb{n}_\pg¬ram)\subrange{s}{z}}
-    \end{cases} \\
+    \using c &= \max\left(\set{\build{k}{k \le z \wedge \Nrange{s}{k} \subseteq \readable{\mathbf{m}\subb{n}_\pg¬ram}}}\right) \\
+    \using \kappa(\tup{m, x}) &= \begin{cases} 2(x - s) &\when m = n \\ 2(x - o) + 1 &\otherwise \end{cases} \\
+    \using \mathbf{a} &= \sqorderby{\kappa(\tup{m, x})}{\tup{m, x} \in \set{\build{\tup{n, s+k}}{k \in \Nmax{c}}} \cup \set{\build{\tup{\none, o+k}}{k \in \Nmax{c}}}} \\
+    \using \tup{\varepsilon^\dagger, \gascounter^\dagger, \workingset^\dagger, \mem^\dagger, \mathbf{m}^\dagger} &= \wscharge¬internal(\gascounter - g, \workingset, \mem, \mathbf{m}, \mathbf{a}) \\
+    \using \mem^\ddagger &= \mem^\dagger \exc (\mem^\dagger)\subrange{o}{c} = (\mathbf{m}\subb{n}_\pg¬ram)\subrange{s}{c} \\
+    \tup{\execst', \registers'_7, \mem', \mathbf{m}', \workingset', \gascounter'} &\equiv \begin{cases}
+      \tup{\panic, \registers_7, \mem, \mathbf{m}, \workingset, \gascounter - g} &\when \Nrange{o}{z} \not\subseteq \writable{\memory} \\
+      \tup{\continue, \mathtt{WHO}, \mem, \mathbf{m}, \workingset, \gascounter - g} &\otherwhen n \not\in \keys{\mathbf{m}} \\
+      \tup{\oog, \registers_7, \mem^\dagger, \mathbf{m}^\dagger, \workingset^\dagger, \gascounter^\dagger} &\otherwhen \varepsilon^\dagger = \oog \\
+      \tup{\continue, c, \mem^\ddagger, \mathbf{m}^\dagger, \workingset^\dagger, \gascounter^\dagger} &\otherwise
+    \end{cases}
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_O(\gascounter, \registers, \memory, \mathbf{m})$ \\
+  $\Omega_O(\gascounter, \registers, \memory, \workingset, \mathbf{m})$ \\
   \texttt{poke} = 11 \\
   $g = \CgasOconst + \fnmemgas(\CgasOlinear, z)$ }&
   $\begin{aligned}
     \using \sq{n, s, o, z} &= \registers\subrange{7}{4} \\
-    \tup{\execst', \registers'_7, \mathbf{m}'} &\equiv \begin{cases}
-      \tup{\panic, \registers_7, \mathbf{m}} &\when \Nrange{s}{z} \not\subseteq \readable{\memory} \\
-      \tup{\continue, \mathtt{WHO}, \mathbf{m}} &\otherwhen n \not\in \keys{\mathbf{m}} \\
-      \tup{\continue, \mathtt{OOB}, \mathbf{m}} &\otherwhen \Nrange{o}{z} \not\subseteq \writable{\mathbf{m}\subb{n}_\pg¬ram} \\
-      \tup{\continue, \mathtt{OK}, \mathbf{m}'}  &\otherwise \\
-      \multicolumn{2}{l}{\where \mathbf{m}' = \mathbf{m} \exc (\mathbf{m}'\subb{n}_\pg¬ram)\subrange{o}{z} = \mem\subrange{s}{z}}
-    \end{cases} \\
+    \using c &= \max\left(\set{\build{k}{k \le z \wedge \Nrange{o}{k} \subseteq \writable{\mathbf{m}\subb{n}_\pg¬ram}}}\right) \\
+    \using \kappa(\tup{m, x}) &= \begin{cases} 2(x - s) &\when m = \none \\ 2(x - o) + 1 &\otherwise \end{cases} \\
+    \using \mathbf{a} &= \sqorderby{\kappa(\tup{m, x})}{\tup{m, x} \in \set{\build{\tup{\none, s+k}}{k \in \Nmax{c}}} \cup \set{\build{\tup{n, o+k}}{k \in \Nmax{c}}}} \\
+    \using \tup{\varepsilon^\dagger, \gascounter^\dagger, \workingset^\dagger, \mem^\dagger, \mathbf{m}^\dagger} &= \wscharge¬internal(\gascounter - g, \workingset, \mem, \mathbf{m}, \mathbf{a}) \\
+    \using \mathbf{m}^\ddagger &= \mathbf{m}^\dagger \exc (\mathbf{m}^\ddagger\subb{n}_\pg¬ram)\subrange{o}{c} = \mem\subrange{s}{c} \\
+    \tup{\execst', \registers'_7, \mem', \mathbf{m}', \workingset', \gascounter'} &\equiv \begin{cases}
+      \tup{\panic, \registers_7, \mem, \mathbf{m}, \workingset, \gascounter - g} &\when \Nrange{s}{z} \not\subseteq \readable{\memory} \\
+      \tup{\continue, \mathtt{WHO}, \mem, \mathbf{m}, \workingset, \gascounter - g} &\otherwhen n \not\in \keys{\mathbf{m}} \\
+      \tup{\oog, \registers_7, \mem^\dagger, \mathbf{m}^\dagger, \workingset^\dagger, \gascounter^\dagger} &\otherwhen \varepsilon^\dagger = \oog \\
+      \tup{\continue, c, \mem^\dagger, \mathbf{m}^\ddagger, \workingset^\dagger, \gascounter^\dagger} &\otherwise
+    \end{cases}
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_Z(\gascounter, \registers, \memory, \mathbf{m})$ \\
+  $\Omega_Z(\gascounter, \registers, \memory, \workingset, \mathbf{m})$ \\
   \texttt{pages} = 12 \\
   $g =  \begin{cases} \CgasZfreeconst + c \cdot \CgasZfreelinear &\when r = 0 \\ \CgasZallocconst + c \cdot \CgasZalloclinear &\when r \in \set{1, 2} \\ \CgasZsetmodeconst + c \cdot \CgasZsetmodelinear &\when r \in \set{3, 4} \\ \CgasZinvalid &\otherwise \end{cases} $ }&
   $\begin{aligned}
@@ -656,29 +690,38 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
        \sq{\none, \none, \dots} &\when r = 0 \\
        \sq{\mathrm{R}, \mathrm{R}, \dots} &\when r = 1 \vee r = 3 \\
        \sq{\mathrm{W}, \mathrm{W}, \dots} &\when r = 2 \vee r = 4 \\
+      \end{cases} \\
+      (\mathbf{u}'_\ram¬frames)\subrange{p}{c} = \begin{cases}
+       \sq{\frame¬missing¬zero, \frame¬missing¬zero, \dots} &\when r < 3 \\
+       (\mathbf{u}_\ram¬frames)\subrange{p}{c} &\otherwise
       \end{cases}
     \end{cases}\\
-    \tup{\registers'_7, \mathbf{m}'} &\equiv \begin{cases}
-      \tup{\mathtt{WHO}, \mathbf{m}} &\when \mathbf{u} = \error \\
-      \tup{\mathtt{HUH}, \mathbf{m}} &\otherwhen r > 4 \vee p < 16 \vee p+c \ge \nicefrac{2^{32}}{\Cpvmpagesize} \\
-      \tup{\mathtt{HUH}, \mathbf{m}} &\otherwhen r > 2 \wedge (\mathbf{u}_\ram¬access)\subrange{p}{c} \ni \none \\
-      \tup{\mathtt{OK}, \mathbf{m}'} &\otherwise\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'\subb{n}_\pg¬ram = \mathbf{u}' \\
+    \tup{\registers'_7, \mathbf{m}', \workingset'} &\equiv \begin{cases}
+      \tup{\mathtt{WHO}, \mathbf{m}, \workingset} &\when \mathbf{u} = \error \\
+      \tup{\mathtt{HUH}, \mathbf{m}, \workingset} &\otherwhen r > 4 \vee p < 16 \vee p+c \ge \nicefrac{2^{32}}{\Cpvmpagesize} \\
+      \tup{\mathtt{HUH}, \mathbf{m}, \workingset} &\otherwhen r > 2 \wedge (\mathbf{u}_\ram¬access)\subrange{p}{c} \ni \none \\
+      \tup{\mathtt{OK}, \mathbf{m}', \workingset^\dagger} &\otherwise\,,\ \where \mathbf{m}' = \mathbf{m} \exc \mathbf{m}'\subb{n}_\pg¬ram = \mathbf{u}' \\
+    \end{cases} \\
+    \where \workingset^\dagger &= \begin{cases}
+      \workingset \setminus \set{\build{\tup{n, \datapage{i}}}{p \le i < p + c}} &\when r < 3 \\
+      \workingset &\otherwise
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_K(\gascounter, \registers, \memory, \mathbf{m})$ \\
+  $\Omega_K(\gascounter, \registers, \memory, \workingset, \mathbf{m})$ \\
   \texttt{invoke} = 13 \\
   $g = \CgasK + g_R$} &
   $\begin{aligned}
     \using \sq{n, o} &= \registers_{7, 8} \\
+    \using \arg &= \sq{\build{\tup{\none, x}}{x \orderedin \Nrange{o}{112}}} \\
     \using \tup{g_R, \mathbf{w}} &= \begin{cases}
       \tup{g_R, \mathbf{w}}: \encode[8]{g_R} \concat \encode[8]{\mathbf{w}} = \mem\subrange{o}{112} &\when \Nrange{o}{112} \subseteq \writable{\mem} \\
-      %\tup{\decode[8]{\memr\subrange{o}{8}}, \sq{\build{\decode[4]{\memr\subrange{o+8+8x}{8}}}{x \orderedin \Nmax{13}}}} &\when \Nrange{o}{60} \subset \writable_\mem} \\
       \tup{0, \error} &\otherwise
     \end{cases} \\
-    \using \tup{c, i', g_R', \pg¬gaschargedflag', \mathbf{w}', \mathbf{u}'} &= \Psi(\mathbf{m}\subb{n}_\pg¬code, \mathbf{m}\subb{n}_\pg¬pc, g_R, \mathbf{m}\subb{n}_{\pg¬gaschargedflag}, \mathbf{w}, \mathbf{m}\subb{n}_\pg¬ram)\\
-    \using \mem^* &= \mem \exc \mem^*\subrange{o}{112} = \encode[8]{g_R'} \concat \encode[8]{\mathbf{w}'}\\
+    \using \tup{\varepsilon_r, \gascounter_1, \workingset_1, \mem_1, \mathbf{m}_1} &= \wscharge¬internal(\gascounter - g, \workingset, \mem, \mathbf{m}, \arg) \\
+    \using \tup{c, i', g_R', \pg¬gaschargedflag', \mathbf{w}', \mathbf{u}', \workingset^*} &= \Psi(\mathbf{m}\subb{n}_\pg¬code, \mathbf{m}\subb{n}_\pg¬pc, g_R, \mathbf{m}\subb{n}_{\pg¬gaschargedflag}, \mathbf{w}, \mathbf{m}\subb{n}_\pg¬ram, n, \workingset_1)\\
+    \using \mem^* &= \mem_1 \exc \mem^*\subrange{o}{112} = \encode[8]{g_R'} \concat \encode[8]{\mathbf{w}'}\\
     \using \mathbf{m}^* &= \mathbf{m} \exc \begin{cases}
       \mathbf{m}^*\subb{n}_\pg¬ram = \mathbf{u}'\\
       \mathbf{m}^*\subb{n}_\pg¬pc = \begin{cases}
@@ -687,30 +730,29 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
       \end{cases}\\
       \mathbf{m}^*\subb{n}_{\pg¬gaschargedflag} = \pg¬gaschargedflag'\\
     \end{cases}\\
-    \gascounter' &\equiv \begin{cases}
-      \gascounter - g &\when \mathbf{w} = \error \vee n \not\in \keys{\mathbf{m}} \vee \gascounter < g \\
-      \gascounter - g + g_R' &\otherwise
-    \end{cases}\\
-    \tup{\execst', \registers'_7, \registers'_8, \mem', \mathbf{m}'} &\equiv \begin{cases}
-      \tup{\panic, \registers_7, \registers_8, \mem, \mathbf{m}} &\when \mathbf{w} = \error \\
-      \tup{\continue, \mathtt{WHO}, \registers_8, \mem, \mathbf{m}} &\otherwhen n \not\in \mathbf{m} \\
-      \tup{\continue, \mathtt{HOST}, h, \mem^*, \mathbf{m}^*} &\otherwhen c = \host \times h \\
-      \tup{\continue, \mathtt{FAULT}, x, \mem^*, \mathbf{m}^*} &\otherwhen c = \fault \times x \\
-      \tup{\continue, \mathtt{OOG}, \registers_8, \mem^*, \mathbf{m}^*} &\otherwhen c = \oog \\
-      \tup{\continue, \mathtt{PANIC}, \registers_8, \mem^*, \mathbf{m}^*} &\otherwhen c = \panic \\
-      \tup{\continue, \mathtt{HALT}, \registers_8, \mem^*, \mathbf{m}^*} &\otherwhen c = \halt \\
+    \using \tup{\varepsilon_w, \gascounter_3, \workingset_3, \mem^{**}, \mathbf{m}_2} &= \wscharge¬internal(\gascounter_1 + g_R', \workingset^*, \mem^*, \mathbf{m}^*, \arg) \\
+    \tup{\execst', \registers'_7, \registers'_8, \mem', \workingset', \mathbf{m}', \gascounter'} &\equiv \begin{cases}
+      \tup{\panic, \registers_7, \registers_8, \mem, \workingset, \mathbf{m}, \gascounter - g} &\when \mathbf{w} = \error \\
+      \tup{\continue, \mathtt{WHO}, \registers_8, \mem, \workingset, \mathbf{m}, \gascounter - g} &\otherwhen n \not\in \mathbf{m} \\
+      \tup{\oog, \registers_7, \registers_8, \mem_1, \workingset_1, \mathbf{m}, \gascounter_1} &\otherwhen \varepsilon_r = \oog \\
+      \tup{\oog, \registers_7, \registers_8, \mem^{**}, \workingset_3, \mathbf{m}^*, \gascounter_3} &\otherwhen \varepsilon_w = \oog \\
+      \tup{\continue, \mathtt{HOST}, h, \mem^{**}, \workingset_3, \mathbf{m}^*, \gascounter_3} &\otherwhen c = \host \times h \\
+      \tup{\continue, \mathtt{FAULT}, x, \mem^{**}, \workingset_3, \mathbf{m}^*, \gascounter_3} &\otherwhen c = \fault \times x \\
+      \tup{\continue, \mathtt{OOG}, \registers_8, \mem^{**}, \workingset_3, \mathbf{m}^*, \gascounter_3} &\otherwhen c = \oog \\
+      \tup{\continue, \mathtt{PANIC}, \registers_8, \mem^{**}, \workingset_3, \mathbf{m}^*, \gascounter_3} &\otherwhen c = \panic \\
+      \tup{\continue, \mathtt{HALT}, \registers_8, \mem^{**}, \workingset_3, \mathbf{m}^*, \gascounter_3} &\otherwhen c = \halt \\
     \end{cases} \\
   \end{aligned}$\\
   \cmidrule(lr){1-1}\cmidrule(lr){2-2}
   \makecell*[l]{
-  $\Omega_X(\gascounter, \registers, \memory, \mathbf{m})$ \\
+  $\Omega_X(\gascounter, \registers, \memory, \workingset, \mathbf{m})$ \\
   \texttt{expunge} = 14 \\
   $g = \CgasX$} &
   $\begin{aligned}
     \using n &= \registers_7 \\
-    \tup{\registers'_7, \mathbf{m}'} &\equiv \begin{cases}
-      \tup{\mathtt{WHO}, \mathbf{m}} &\when n \not\in \keys{\mathbf{m}} \\
-      \tup{\mathbf{m}\subb{n}_\pg¬pc, \mathbf{m} \setminus n} &\otherwise \\
+    \tup{\registers'_7, \mathbf{m}', \workingset'} &\equiv \begin{cases}
+      \tup{\mathtt{WHO}, \mathbf{m}, \workingset} &\when n \not\in \keys{\mathbf{m}} \\
+      \tup{\mathbf{m}\subb{n}_\pg¬pc, \mathbf{m} \setminus n, \workingset \setminus \set{\build{\tup{n, i}}{i \in \set{\datatag, \codetag, \jumptag} \times \N}}} &\otherwise \\
     \end{cases} \\
   \end{aligned}$\\
   \bottomrule
@@ -718,14 +760,14 @@ \subsection{Refine Functions}\label{sec:refinefunctions}
 
 \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
 
-This defines a number of functions broadly of the form $(\gascounter' \in \signedgas, \registers' \in \regs, \memory', \tup{\imX', \mathbf{y}'}) = \Omega_\square(\gascounter \in \gas, \registers \in \regs, \memory \in \ram, \imXY \in \implications^2, \dots)$. Functions which have a result component which is equivalent to the corresponding argument may have said components elided in the description. Functions may also depend upon particular additional parameters.
+This defines a number of functions broadly of the form $(\gascounter' \in \signedgas, \registers' \in \regs, \memory', \workingset' \in \sequence{\optional{\pageid}}, \tup{\imX', \mathbf{y}'}) = \Omega_\square(\gascounter \in \gas, \registers \in \regs, \memory \in \ram, \workingset \in \sequence{\optional{\pageid}}, \imXY \in \implications^2, \dots)$. Functions which have a result component which is equivalent to the corresponding argument may have said components elided in the description. Functions may also depend upon particular additional parameters.
 
-Other than the gas-counter which is explicitly defined, elements of \textsc{pvm} state are each assumed to remain unchanged by the host-call unless explicitly specified.
+Other than the gas-counter which is explicitly defined, elements of \textsc{pvm} state are each assumed to remain unchanged by the host-call unless explicitly specified. The working-set charging convention of appendix \ref{sec:generalfunctions} applies to all memory inspections and mutations made by these functions, and the working-set argument and result are elided from the individual descriptions.
 \begin{align}
   \gascounter' &\equiv \gascounter - g\\
-  \tup{\execst', \registers', \memory', \imX', \mathbf{y}'} &\equiv \begin{cases}
-    \tup{\oog, \registers, \memory, \mathbf{x}, \mathbf{y}} &\when \gascounter < g\\
-    \tup{\continue, \registers, \memory, \mathbf{x}, \mathbf{y}} \text{ except as indicated below} &\otherwise
+  \tup{\execst', \registers', \memory', \workingset', \imX', \mathbf{y}'} &\equiv \begin{cases}
+    \tup{\oog, \registers, \memory, \workingset, \mathbf{x}, \mathbf{y}} &\when \gascounter < g\\
+    \tup{\continue, \registers, \memory, \workingset, \mathbf{x}, \mathbf{y}} \text{ except as indicated below} &\otherwise
   \end{cases}
 \end{align}
 
@@ -819,9 +861,11 @@ \subsection{Accumulate Functions}\label{sec:accumulatefunctions}
         \sa¬codehash,
         \is{\mathbf{\sa¬storage}}{\emset},
         \is{\mathbf{\sa¬requests}}{\set{\kv{\tup{c, l}}{\sq{}}}},
+        % TODO: Should be configurable, but we're out of argument registers. Pass a pointer to struct instead?
         \is{\sa¬balance}{\mathbf{a}_\sa¬minbalance},
         \sa¬minaccgas,
         \sa¬minmemogas,
+        \is{\sa¬accworkingsetsize}{\Cpvmmaxworkingset},
         \is{\mathbf{\sa¬preimages}}{\emset},
         \is{\sa¬created}{t},
         \sa¬gratis,
diff --git a/text/work_packages_and_reports.tex b/text/work_packages_and_reports.tex
index 648f2460..832e64fe 100644
--- a/text/work_packages_and_reports.tex
+++ b/text/work_packages_and_reports.tex
@@ -58,7 +58,7 @@ \subsubsection{Data Collection and Justification}
 
 \subsection{Packages and Items}\label{sec:packagesanditems}
 
-We begin by defining a \emph{work-package}, of set $\workpackage$, and its constituent \emph{work-item}s, of set $\workitem$. A work-package includes a simple blob acting as an authorization token $\wp¬authtoken$, the index of the service which hosts the authorization code $\wp¬authcodehost$, an authorization code hash $\wp¬authcodehash$ and a configuration blob $\wp¬authconfig$, a working-set size for execution of the authorization code $\wpX_\wp¬authworkingsetsize$, a context $\wp¬context$ and a sequence of work items $\wp¬workitems$:
+We begin by defining a \emph{work-package}, of set $\workpackage$, and its constituent \emph{work-item}s, of set $\workitem$. A work-package includes a simple blob acting as an authorization token $\wp¬authtoken$, the index of the service which hosts the authorization code $\wp¬authcodehost$, an authorization code hash $\wp¬authcodehash$ and a configuration blob $\wp¬authconfig$, a working-set size for execution of the authorization code $\wp¬authworkingsetsize$, a context $\wp¬context$ and a sequence of work items $\wp¬workitems$:
 \begin{equation}
   \label{eq:workpackage}
   \workpackage \equiv \tuple{