Redo spec of state circuit

[ed255]

• Update the state proof document
• Write the spec of the state circuit in python from scratch following
  the current rw_table design.
• Add a minimal state circuit test
• List of changes:
  • Renamed key and aux columns so start with index 0, in order to
    make it more readable when working with code were we have arrays
    called keys. This way key0 == keys[0].
  • Add a new key column so that we have a cloumn exclusive for
    address keys, which allows us to reuse the key order constraints
    for addresses for all operations.
  • Add the boilerplate for the missing operations
  • Remove value2 column (used for valuePrev) in some Write
    operations

[miha-stopar]

Nice!! Only a couple of nitpicks and questions.

[ed255]

Another doubt I have for the state circuit is how to extract the number of operations that have happened, so that the prover can't introduce extra operations that are not used in the EVM circuit.

1. What forbids adding 2 rows of different operations with the same rw_counter?
2. How does the EVM circuit know the number of operations (the highest rwc_counter value)?

We must take into account that for State Tree operations we're introducing artificial writes with rw_counter=0 which must not be accounted for, so the number of rows is different than the number of operations.

One idea that comes to my mind is to add an advice column that counts the number of rows with rw_counter != 0. Then in the padding rows, constraint that rw_counter == 0. This way the EVM circuit can do a lookup to any padding row to read the number of operations from this new column.

What do people think of this?

[barryWhiteHat]

What forbids adding 2 rows of different operations with the same rw_counter?

NOthing but the below check confirms that every row has to be used by the evm proof.

How does the EVM circuit know the number of operations (the highest rwc_counter value)?

I was thinking to count the number of elements in the RW table in the zkevm and then the l1 smartcontract confirm that the polynomial contains exactly that many elements. I know Han has been thinking about this more so maybe has a better idea :)

[han0110]

How does the EVM circuit know the number of operations (the highest rwc_counter value)?

Originally Barry proposes to use degree check (by underlying PCS) on the rw_table, but I think that it needs prover to provide an shuffle argument to argue that (low_degree_rw_table || zero_padding) == shuffle(rw_table), because we might have some artificial row that exist in between meaningful rows that rw_counter != 0. (e.g. to prove [(rw_counter=1, ...), (rw_counter=0, ...), (rw_counter=30, ...)] have only 2 meaningful elements, prover needs to provide [(rw_counter=1, ...), (rw_counter=30, ...)], and verifier verifies it has degree 1, and the padded version of it is also a shuffle of the rw_table generated by State circuit).

My naive thought is to let both State circuit and EVM circuit to consume the same public input total_rw, and the former verifies it matches the sum of row that rw_counter != 0, the latter verifies it matches the latest step's rw_counter. I think this approach is easier to implement (already supported by current halo2), but not sure if it's sound as the previous approach or not.

[han0110]

All look great, only with some outdated docs are wrong and should be removed.

[barryWhiteHat]

My naive thought is to let both State circuit and EVM circuit to consume the same public input total_rw, and the former verifies it matches the sum of row that rw_counter != 0, the latter verifies it matches the latest step's rw_counter. I think this approach is easier to implement (already supported by current halo2), but not sure if it's sound as the previous approach or not.

At the point when we are implmenting the l1 verifier we can consider these two options. For now as long as we have a solution we are confident will work i think we are good to go.

[ed255]

I have added tests for situations that don't pass the constraints.

Should I update tables.py to remove the value_prev column in the rw_table?

[ed255]

Should I update tables.py to remove the value_prev column in the rw_table?

After a discussion with Han I understood that the value_prev will not be removed from rw_table (I've reverted the deletion of the column from tables.md).

Nevertheless one of the changes I made is to introduce a new key column so that address values stay in a single column. If this change is approved, tables.py needs to be updated to include a new key column.

[han0110]

LGTM!

[miha-stopar]

LGTM! Thanks!