Evaluate the offline memory argument

The [offline memory argument](https://www.cs.ubc.ca/~will/papers/memcheck.pdf) can be introduced in the setting of a storage-bound client seeking the help of an untrusted storage provider in order to implement either read-only-memory (ROM) or read-write memory (RAM).

# ROM
The interaction between the client and the server can be described in three stages:

1. The client sends write requests at the start of the interaction of the form $\{\left(i, t[i], c_{ini,i}\right)\}_{i\in[M]}$ where $M$ is the size of memory, $i$ is a memory address, $t[i]$ is the value to be stored in $i$ and $c_{ini, i}$ represents a global timestamp at which the operation happened. We can take $c_{ini, i} = 0$ for all $i$ in what follows. Note that in the case of ROM, this is the only time that a write request changes the values $v_i$ stored at cell $i$.
2. During the course of the session between the client and the server, the client maintains two sets in its head, a read set $\mathsf{R}$ and write set $\mathsf{W}$, both sets are initially empty. Now, each time the client makes a read request at address $i$ and it receives a claimed $\left(i, v_i, c_i\right)$, it:
1. Updates $\mathsf{R} = \mathsf{R} \cup \lbrace \left(i, v_i, c_{prev,i} \right)\rbrace$
2. Updates $\mathsf{W} = \mathsf{R} \cup \lbrace \left(i, v_i, c_{cur,i} \right) \rbrace$
3. Checks that $c_{prev,i} < c_{cur,i}$

The server from its side also updates $\left(i, v_i, c_{prev,i} \right)$ to $\left(i, v_i, c_{cur,i} \right)$ in its database.
3. To conclude the session, the client makes a linear scan of the memory to read $\lbrace\left(i, v_i, c_{fin,i}\right)\rbrace_{i\in[M]}$

The main result says that the server was honest during the session if and only if $`\mathsf{R}\cup\{\left(i, v_i, c_{fin,i}\right)\}_{i\in[M]}=\mathsf{W}\cup\lbrace\left(i, t[i], c_{ini,i}\right)\rbrace_{i\in[M]}`$ where the equality is multi-set equality.

Note that the protocol as described above doesn't solve the initially stated problem as storing the plain sets would require more storage by the client than storing the initial table $t[i]$.
To solve this, the client samples two random values $\alpha$ and $\tau$, and keeps track of a fingerprint of the sets above. For example, if we denote the fingerprint for the set $\mathsf{R}$ by $\mathcal{R}$ then $\mathcal{R}$ is initialized to $1$ and is updated as $\mathcal{R} = \mathcal{R} \cdot \left( \tau + i + v_i \alpha + c_i \alpha^2\right)$. This is nothing but the original idea of doing multi-set checks using incremental multi-set hashing. Now, the client stores only two digests which it compares for equality at the end.

# RAM

The interaction between the client and the server can also be described as consisting of three stages:
1. Exactly the same as in the case of ROM
2. Now each time the client makes a write request $\left(i, v_{new, i}, c_{cur,i}\right)$ at address `i`, it receives the old tuple $\left(i, v_{old, i}, c_{prev,i}\right)$. Read requests are handled as in the ROM case with $v_{new, i} = v_{old, i}$. The clients then:
1. Updates $`\mathsf{R} = \mathsf{R} \cup \{ \left(i, v_{old, i}, c_{prev,i} \right)\}`$
2. Updates $`\mathsf{W} = \mathsf{R} \cup \{ \left(i, v_{new, i}, c_{cur,i} \right)\}`$
3. Checks that $c_{prev,i} < c_{cur,i}$

The server from its side also updates $\left(i, v_{old, i}, c_{prev,i} \right)$ to $\left(i, v_{new, i}, c_{cur,i} \right)$ in its database.
3. To conclude the session, the client makes a linear scan of the memory to read $`\{\left(i, v_i, c_{fin,i}\right)\}_{i\in[M]}`$

The main result again says that the server was honest if and only if $`\mathsf{R} \cup \{\left(i, v_i, c_{fin,i}\right)\}_{i\in[M]} = \mathsf{W} \cup \{\left(i, t[i], c_{ini,i}\right)\}_{i\in[M]}`$ where the equality is multi-set equality.

# Implementation
In a STARK, and in the multi-table setting, each table/chiplet will be responsible for managing its memory operations. The memory itself will not live in a centralized memory chiplet anymore but will live on a bus, call it memory bus. Suppose that a chiplet only needs element read-only memory access, then it will contain
1. A column containing the address read at the current row
2. A column containing the read value i.e., $v_i$
3. A column the contains the timestamp when the address in question was last accessed
4. A couple of columns to witness that the current timestamp is greater than the timestamp in the previous point
Now for each row, there will be two interactions with the bus, an interaction to push to the bus of the form $\left(i, v_i, c_{prev,i} \right)$ and one to pull of the form $\left(i, v_{new, i}, c_{cur,i} \right)$.

In order to close the circle, we need to make pull requests to the bus of the form $`\{\left(i, v_i, c_{fin,i}\right)\}_{i\in[M]}`$ and push requests of the form $`\{\left(i, t[i], c_{ini,i}\right)\}_{i\in[M]}`$. One of the ways[^1] this is done is by introducing a chiplet, call it boundary chiplet, which does this and it contains

1. A column for the address which starts at 0 and goes all the way to $M-1$
2. A column for the value stored at the address
3. A column for the final timestamp at which the address was accessed. Note that the we don't need a column for the initial time stamp as it is throughout equal to 0.

The boundary chiplet will have in its AIR definition a (randomized) boundary constraint involving the ROM table.

For RAM, things are pretty similar but with the following differences

1. The chiplet making use of RAM will, in addition to the above columns, need to have columns to hold the previous data contained at the memory address we are reading from or writing to.
2. The boundary chiplet will now also contain a column to hold the initial data, which most probably will be 0 and hence can be omitted, and a column to hold the final data at the address.

Note that the boundary chiplet need only contain the touched addresses during the course of the VM execution but there should be a mechanism to enforce that each address appears in the boundary chiplet at most once. Here we can use either sorting or Bezout to guarantee this.

# Open questions
The above suggests that the offline memory argument is very powerful in the multi-table/multi-chiplet paradigm of VMs. One of the things that are still not clear to me is how to support, in an efficient way, both element and word access at the same time, like we currently do in the VM.

[^1]: All credit for this idea goes to the OpenVM folks as far as I know.