# zkVM Memory Model with Continuations

## Notation

We fix a field $\mathbb F$ and multiplicative subgroup $\{x, x^2, \ldots\} = H \subset \mathbb F$. A "column" is a polynomial $P \in \mathbb F[X]$ of degree at most $|H|$. The elements of the column $P$ are $P(x), P(x^2), \ldots$. For notational convenient, we use the lowercase letter, e.g. `p`, to denote the value of column $P$ at a particular row, or element, of $H$.

## Memory Argument Supporting Continuations

The memory Stark contains the following 7 columns.

$$(Clk, Addr_{r}, R_{r}, Addr_{s}, R_{s}, Addr_w, R_{w})$$

Additionally, the Stark specifies two input memory columns and two output memory coulumns:

$$(Addr_{in}, V_{in})\;, (Addr_{out}, V_{out})$$

Row transition semantics: read memory from $Addr_r$ and $Addr_s$ into $R_r$ and $R_s$, write $R_w$ to $Addr_w$.

Each read for memory at `addr` must be consistent with

1. the previous (in terms of `clk`) write to `addr` if exist
2. input memory at `addr` otherwise

Note that we require all reads to be preceeded by either a write or a input memory declaration for that address.

The output memory $(Addr_{out}, V_{out})$ must contain all those memory locations that have been written to during this continuation. Furthermore, the value encoded must be the value of memory that is written to last (sorted by `clk`).

### Sketch of argument

#### Read consistency

Merge and sort the following tables by 1st to 3rd column.

$$
(Addr_{in}, 0, 1, V_{in}) \\
(Addr_{w}, Clk, 1, R_{w}) \\
(Addr_{r}, Clk, 0, R_{r}) \\
(Addr_{s}, Clk, 0, R_{s})
$$

Each region looks like follows.

| Addr | Clk | Mode | Value |
| - | - | - | - |
| addr | 0 | 1 | v |
| addr | c | 0 | v |
| addr | ... | 0 | v |
| addr | c' | 1 | v' |
| addr | c'' | 0 | v' |
| addr | ... | 0 | v' |

We require that the first row for each `addr` to have `mode = 1`, i.e. the memory at `addr` must be written to (either as a write or taken as input memory) before it can be read.

#### Output consistency

Sort just the local memory write table using the 1st and then 2nd column.

$$
(Addr_{w}, Clk, R_{w})
$$

We will select the last row for each address region. That is, we construct a subtable consists of rows for which the value of `clk` for each `addr` is the largest. Now, the output memory table is the resulting table minus the clock column.

#### Managing global, input, and output memory

In the above memory argument, each continuation only need to take input memory that it reads, and only exports memory that it writes.

We keep track of a global memory $(Addr_{global}, V_{global})$. Each time a new continuation is needed, a subtable of the global memory is selected to be the input memory for the continuation. After each continuation exits, the output memory is ``merged'' back into the global memory (selecting the output over old values).

#### Input selection

We simply choose a subtable out of the global memory right before the continuation. The difficulty is to ensure that all predefined memory that is to be used in a continuation is selected. To do this, we must show that the newly initialized memory for a continuation does not overwrite anything in the global memory. Consider the new memory initialization table
$$T_{init} = (Addr_{init}, 0)$$
We must show that the first column of it is disjoint from the current global memory.
Next, we select a subtable from the global memory
$$T_{prior} = (Addr_{prior}, V_{prior})$$
The input table is defined as $T_{init} \cup T_{prior}$ (merging of tables).

#### Merging of output memory into global memory

We can construct the table and sort by the 1st and then 2nd column.

$$
(Addr_{global}, 0, V_{global}) \\
(Addr_{out}, 1, V_{out})
$$

The additional bit in the 2nd column is then used to select the output over the previous memory value. Finally, we can select the subtable containing the latest memory values.

### Complexity

Let $m$ be the number of memory access (R/W) for a continuation, and let M be the number of total memory used for the entire computation.

- Read consistency: O(m)
- Output consistency: O(m)
- Input selection: O(M). Can we get this down to O(m)?
- Output merging: O(M). Can we get this down to O(m)?