<style>
table {
white-space: nowrap;
}
</style>

## Introduciton

State circuit iterates over random read-write access records of EVM circuit to verify each data is consistent between different writes.

To verify if data is consistent, it first verify all access records are grouped by their unique identifier and sorted by order of access - a sequential counter named `rw_counter`, then verify the records between writes are consistent. It also verifies data is in correct format.

It then serves as a lookup table for EVM circuit to do consistent random read-write access.

## Different models

To have a complete random read-write access model, we can begin with the simplest one and extend it with features required by us step by step, for easier understanding.

### Read-only array

Let's begin with the simplest model, say there is a VM accessible to a read-only array as random access memory [^cairo], which consumes a program as witness for execution.

[^cairo]: Cairo also chooses to use read-only memory model, and **Ch8.5 - Read-write memory** explains things very clealy and I would recommend to have a look.

Say the memory size could be up to <code>2^64^-1</code>, since the index of memory access is witness in program, for only VM itself it's impractical to track such large chunk of witnesses and use a giant multiplexer to select the value at the index.

But without tracking witnesses, how do we know the random access memory is consistent in the execution trace? In PLONK (or [RAP](https://hackmd.io/@aztec-network/plonk-arithmetiization-air)) we could introduce challenge as randomness to achieve some "global" property, for example, poly <code>f~a~</code> is a shuffle of <code>f~b~</code>, which is required by us here. With such shuffle argument[^shuffle-argument], we could verify the random access memory is consistent.

[^shuffle-argument]: Or "multiset check" described in [Ariel's writeup](/@arielg/ByFgSDA7D). I say "shuffle argument" because I'm afraid "permutation argument" might sound like the one used in PLONK, which I think is abbreviation of "permutation argument **with** identity map", so I would say "shuffle argument" to avoid ambiguity.

In halo2 it uses both "permutation argument **with** identity map" and "permutation argument **without** identity map", [the former](https://zcash.github.io/halo2/design/proving-system/permutation.html) is also called copy constraint, and the latter is used as sub-argument in both copy constraint and lookup.

For simplicify, we ask prover to put memory index and value in different polys <code>f~index~</code> and <code>f~value~</code>, then we let the prover to read the value at the index directly without any constraint.

Then with <code>f~index~</code> and <code>f~value~</code> commited, we then ask prover to provide shuffle version of them <code>f’~index~</code> and <code>f’~value~</code>[^shuffle-on-random-linear-combination], and checks 2 things:

[^shuffle-on-random-linear-combination]: To make sure <code>f’~index~</code> and <code>f’~value~</code> are shuffle in the same way, we can use random linear combination trick to ensure it. For example, we check if <code>f = f~index~ + αf~value~</code> is a shuffle of <code>f’ = f’~index~ + αf’~value~</code>, instead of checking them respectively, where the <code>α</code> is randomness derived from transcript.

1. Indices in <code>f’~index~</code> are sorted (either ascendingly or descendingly) [^continuous-read-only-memory]
2. Values in <code>f’~value~</code> remain the same as long as index remains the same

[^continuous-read-only-memory]: In Cairo they are using even simpler model, they require the memory is continuous accessed (no any skip), then first check becomes "Indices in <code>f’~index~</code> is continuous". See **Ch9.7 - Nondeterministic continuous read-only memory** for the concrete constraints.

And both checks here could be simply implemented with "local" constraints without tracking all of witnesses at a gate, thanks to the shuffle argument.

### Read-write array

Most VMs are not designed to support a read-only array model, such as EVM. Since in our context we want to be as similar to EVM's original behavior as possible (not design a whole new VM to emulate EVM), so we need a read-write access to stack, memory, storage, etc...

But instead of extending read-only array model to support so many things, let's begin with extending the read-only memory with write feature.

So to support write, we add another poly <code>f~is_write~</code> to let the program specify if this access is a write. Then also ask prover to provide the shuffle of it as <code>f’~is_write~</code>, the checks now becomes:

1. Indices in <code>f’~index~</code> are sorted (either ascendingly or descendingly)
2. As long as index remains the same
2.1 Values in <code>f’~value~</code> remain the same when <code>f’~is_write~</code> is `false`
2.2 Values in <code>f’~value~</code> could be any value when <code>f’~is_write~</code> is `true`

But there is a problem, it seems that in VM prover can read a value that is actually written in the future, but the shuffled polys still pass the constraints, because there is no constraint on how prover shuffles the access to the same index.

This issue pops up because when we say "something is updatable", we are actually saying "something is updatable **over time**", the concept of time natually comes to play a important role.

To resolve this issue, we introduce another poly <code>f~rw_counter~</code> [^rw_counter], and ask prover to increase this counter every time when it does random access. Then add another constraint before second point:

[^rw_counter]: It's previously named `global_counter`, but I found there might be more counters in circuit, so to be more precise, I try to name it `rw_counter`. (I also considered about the name `timestamp`, but afraid that it woud be confused with the `timestamp` in block header)

1. ...
2. As long as index remains the same
2.0. Counters in <code>f’~rw_counter~</code> are sorted ascendingly.
2.1. ...

### Read-write dictionary

Finally, because EVM can access to several kinds of data in the execution of a block, so we need a dictionary rather than an array for easier usage.

Since we are operating on a large field, which have 254 bits to carry information, a naive approach is to encode as many information into <code>f~index~</code> as possible, and semantically turn <code>f~index~</code> into <code>f~key~</code>. For example, say we only have stack and memory, we can reserve the first bit as a domain separator to specify which kind of data we are accessing, and set the following 24 bits as call id, then set the following 40 bits as index of stack and memory.

Another approach is to introduce more polys, and add more layers of sorting (e.g. add <code>f~tag~</code>, <code>f~call_id~</code> and sort it in order of <code>f~tag~</code>, <code>f~call_id~</code>, <code>f~index~</code>).

Or we could even directly sort the random linear combination or these polys as the key (e.g. <code>f’~key~ = sorted(f~tag~ + βf~call_id~ + β^2^f~index~)</code>), but it might become annoying and more expensive to sort field elements instead of something with restricted range (e.g. 40 bits).

## Implementation

### Data kinds

Here is the list of different kinds of data EVM can access during the execution.

| Key 1 (Tag) | Key 2 | Key 3 | Key 4 | Value 1 | Aux 1 | Aux 2 |
| ---------------------------- | ----------------------- | ----------------------- | ------------------- | --------- | ------------------------- | ---------------- |
| `TxAccessListAccount` | `tx_id (24)` | `account_address (160)` | | `is_warm` | | |
| `TxAccessListAccountStorage` | `tx_id (24)` | `account_address (160)` | `storage_key (rlc)` | `is_warm` | | |
| `TxRefund` | `tx_id (24)` | | | `value` | | |
| `Account` | `account_address (160)` | `field_tag (~)` | | `value` | | |
| `AccountStorage` | `account_address (160)` | `storage_key (rlc)` | | `value` | `tx_id (24)` ¹ | `committed_value` |
| `CallContext` | `call_id (24)` | `field_tag (~)` | | `value` | | |
| `Stack` | `call_id (24)` | `stack_pointer (10)` | | `value` | | |
| `Memory` | `call_id (24)` | `memory_address (40)` | | `byte` | | |

<sub style="left: 1em; bottom: 1em">
Note: <br>
<strong>•</strong> <code>TxLog</code> and <code>AccountDestructed</code> are complicated so ignored for now. <br>
<strong>•</strong> The number following is tha max amount of bits the key could contain. <br>
<strong>•</strong> <code>~</code> means continous integer. <br>
<strong>•</strong> <code>rlc</code> means random linear combination of EVM word, and it's a field element. <br>
Also: <br>
<strong>1.</strong> Since the gas cost function of <code>SSTORE</code> not only takes current and previous value, but also takes the original value finalized in previous transaction, so we need to track the last <code>value</code> as <code>committed_value</code> when <code>tx_id</code> changes.
</sub>

Currently the implementation try to have each key as a column, and verify they are sorted by comparing the difference to previous row is positive (in range of the bits). But we never have such large range lookup table, so using [running sum](https://github.com/zcash/orchard/blob/main/src/circuit/gadget/utilities/lookup_range_check.rs#L17) trick to verify it by chunks seems inevitable. As for random linear combination, we can decomposite it into 32 bytes and then compare.

### Property of different kinds

Different kinds of data also have different properties we migt need to take extra care of:

| Tag | Initial value | Reversible ¹ | Write only persistent ² |
| ---------------------------- | ------------------ | ----------------------- | ---------------------------------- |
| `TxAccessListAccount` | `0` ³ | Yes | |
| `TxAccessListAccountStorage` | `0` | Yes | |
| `TxRefund` | `0` | | Yes |
| `Account` | `any` ⁴ | Yes | |
| `AccountStorage` | `any` | Yes | |
| `CallContext` | `any` ⁵ | | |
| `Stack` | `any` ⁶ | | |
| `Memory` | `0` ⁷ | | |

<sub style="left: 1em; bottom: 1em">
Note: <br>
<strong>1.</strong> When data is reversible, every write access to it might probably accompanied by a reversion write access in the future (with a larger <code>rw_counter</code> and value before the write). <br>
<strong>2.</strong> Some reversible data will not affect the further execution of a tx like <code>TxRefund</code>, <code>TxLog</code> and <code>AccountDestructed</code> (<code>SELFDESTRUCT</code> takes effect in the end of tx). So they will only be written when the call is persistent. <br>
<strong>3.</strong> <code>TxTxAccessList*</code> and <code>TxRefund</code> are always operated with a <code>diff</code>, so their initial values are constraint to be <code>0</code>. <br>
<strong>4.</strong> <code>Account*</code>'s initial value will be verified with previous state/storage trie, but how to connect this with MPT circuit is yet to be determined. <br>
<strong>5.</strong> <code>CallContext</code> is always operated properly, so no specific initial value, and we allow it to read before write <br>
<strong>6.</strong> <code>Stack</code> is always operated by push and pop defined in circuit, so there will not be read without write situation. <br>
<strong>7.</strong> <code>Memory</code> can be read without write because the memory is always expanded before execution implicitly, so their initial values are constraint to be <code>0</code>.
</sub>

### Reversible data

To achieve full equivalence with EVM, we need to support reversion.

In EVM circuit, current approach to support reversion is to ask prover tell us if the state updates in this call are persistent or not, and if not what's the `rw_counter` end of reversion, for reverting the state update at the same step.

So every time we encounter state update, we need to read the previous value first, and do the write in case we need reversion. To simplify this procedure, we can read the rotation of the <code>f~value~</code> to get access the value at previous row at the same time.

### Uniqueness of `rw_counter`

The way we connect EVM circuit and State circuit is going to use shuffle argument [^halo2-does-not-have-api-for-shuffle-argument]. However, this doesn't make sure the `rw_counter` in State circuit are unique because in EVM circuit we might have some "unconstraint cells" (unused cells) that can be loaded with any value, so we need to make sure they are filled with `0` (the blue part in the illustration below) with some constraint.


[^halo2-does-not-have-api-for-shuffle-argument]: Interestingly, in `halo2`, they don't provide shuffle argument as an external api, even it already uses it in subset argument. So when we want to implement a shuffle argument, we will need a new api to query extra challenge from transcript after we have commit both circuits (see [implementation](https://github.com/appliedzkp/halo2/pull/62) and [other potential usages](https://github.com/zcash/halo2/issues/527) if we have such api).

Another approach to make sure the blue part not showing in State circuit, we can introduce extra advice column `flag_rw`, which shows if this cell should exist in State circuit or not. To make this `flag_rw` have static cost, we can use "countdowner trick" which requires 2 extra advice column with few constraints.

Previously the way to make sure `rw_counter` is unique in State circuit is to count how many rows in State circuit with `rw_counter != 0`, and accumulate this value then populate it as public input, then share with EVM circuit. This approach requires 2 extra columns with 1 extra public input.

Not sure which approach has less complexity, still exploring. But in regard to aggregation, the less public input the better (even better if public inputs are not shared between circuits).

## Reference

- [Multiset checks in PLONK and Plookup](/@arielg/ByFgSDA7D)
- [The `halo2` Book](https://zcash.github.io/halo2/index.html)
- [Cairo - a Turing-complete STARK-friendly CPU architecture](https://eprint.iacr.org/2021/1063.pdf)