state circuit: add prev value column and constrain it

[lispc]

We need to add an "initial row" before each uniq (tag, id, field_tag, storage_key) key tuple. Initial rows are rows having rwc == 0, and have same (tag, id, field_tag, storage_key) key tuple with following "real" rows.

The reason to add initial rows is to constrain the prev_value column and make it easier to connect evm circuit and state circuit later . In future, either we use "shuffle" or lookup to connect state circuit and evm circuit, they should have same "rw rows set(without order)". So prev_value should be constrained anyway, which are not constrained at all now.

With "initial rows", we can constrain like this:



if keys changed:
  
  assert rwc.cur() == 0 
  
  match tag: 
     
    STACK => assert prev_value.cur() == STACK_DEFAULT_VALUE,
     
    MEMORY => assert prev_value.cur() == MEMORY_DEFAULT_VALUE,
     
    STORAGE => // may need to connect mpt circuit,
     
    ...

else: 
   
  assert value.prev() == prev_value.cur() 

It can be started after https://github.com/appliedzkp/zkevm-specs/pull/201 merged

// in fact i have already a draft implementation

[ed255]

I have a few questions regarding this topic

1. Currently there's no prev_value row in the state circuit. My understanding is that when using the lookup (or shuffle) argument, we can define "virtual" columns made of expressions of actual columns; so an explicit column is not always needed.
2. In https://github.com/privacy-scaling-explorations/zkevm-specs/pull/200 I managed to find a way to remove the need of the initial rows with rwc=0 for the storage and account tags. I think there are many advantages if we manage to remove the need for those initial rows: we will have much more space available for actual rows coming from the EVM circuit, and we may require less constraints. Do you think we could avoid introducing these rwc=0 initialization rows and instead build an expression that sets the prev_value to a default value when the keys change? (where this default value can change depending on the tag).

For example it would look like this:



if keys changed:
  
  match tag: 
     
    STACK => prev_value_expr == STACK_DEFAULT_VALUE,
     
    MEMORY => prev_value_expr == MEMORY_DEFAULT_VALUE,
     
    STORAGE => prev_value_expr == row.committed_value()
    ...

else: 
   
  assert prev_value_expr = row_prev.value 

And that should already match 1 to 1 with the EVM operations, and there's no need to introduce an initialization row.

[lispc]

I now propose a middle branch (1) remove rwc==0 row , but (2) keep prev column

for (1) it seems it can be done. Here I constrain the prev col for state rw and access list rw. Removing rows is always good.

for (2) , evm circuit need to lookup the rw table. We either put prev_value col there, or try to "compute" prev_vlaue expression using existing rw columns. But the latter seems not easy, say we need some expression like "if_keys_changed" to compute prev_vlaue expression... It is not possible if we only keep the 10 data column in rw table without some aux column( like some is_zero advice columns)

if keys changed:
  
  match tag: 
     
    STACK => prev_value_col.cur() == STACK_DEFAULT_VALUE,
     // 0 here
    //MEMORY => prev_value_col.cur() == MEMORY_DEFAULT_VALUE,
  //   0 here
    TX_ACCESS_LIST_ACCOUNT_STORAGE => prev_value_col.cur() == TXAL_ACCOUNT_STORAGE_DEFAULT // false if eip 2930 disabled
    STORAGE => prev_value_col.cur() == committed_value 
    ...

else: 
   
  assert prev_value_col.cur() = value_col.prev() 

[ed255]

for (2) , evm circuit need to lookup the rw table. We either put prev_value col there, or try to "compute" prev_vlaue expression using existing rw columns. But the latter seems not easy, say we need some expression like "if_keys_changed" to compute prev_vlaue expression... It is not possible if we only keep the 10 data column in rw table without some aux column( like some is_zero advice columns)

I see what you mean. We need some extra column to store the witness used to prove that keys_diff != 0 (like the IsZero chip). But I don't think that would be a prev_value column. In either case the prev_value (be it a column or an expression), must be constrained to be a particular value using an expression of other columns and constants (for default values).

if keys changed:
  
  match tag: 
     
    //STACK => prev_value_col.cur() == STACK_DEFAULT_VALUE,
     // for stack and memory, it is not used in evm circuit. So they dont need to be constaint at all. 
    //MEMORY => prev_value_col.cur() == MEMORY_DEFAULT_VALUE,
     
    TX_ACCESS_LIST_ACCOUNT_STORAGE => prev_value_col.cur() == TXAL_ACCOUNT_STORAGE_DEFAULT
    STORAGE => prev_value_col.cur() == ?? // not sure, but committed storage is not prev storage
    ...

else: 
   
  assert prev_value_col.cur() = value_col.prev() 

I don't follow your comment for stack and memory, it is not used in evm circuit. So they dont need to be constaint at all.. The evm may perform a memory read at an address after an expansion; and we must constraint that the value is 0; so I think we need to constraint that for a first memory access (when keys change), the prev_value is 0.

About the storage, when the keys change, the committed storage is the previous value. For storage the keys used are: [txID, address, key], and the committed value is the value found in the storage before the tx begins, and that's the same as the previous value when the keys change.

[lispc]

(1) if i understand right, we have to 2 ways to constrain prev value：

(A) let evm circuit and state circuit both have rw table of 11 columns ( rw_counter, is_write, tag,id, address, field_tag, storage_key, value, aux1, aux2, value_prev), constrain the value_prev at state circuit side, and check rw table of evm circuit and state circuit are identical. This is what i proposed.

(B) keep state circuit as is, and let evm circuit have a 10 column rw table(without the value_prev col), and rw lookup will be like lookup(11_element_rw_values_of_opcodes, [ ..10_element_rw_table, a_value_prev_expression_computed_from_other_expressions ]) My point is, in order to compute the prev value expression, we need more aux columns in evm circuit like lexicographic_ordering_upper_limb_difference_is_zero and is_storage_key_unchanged (to calculate exp like not_first_access). Removing one value_prev col in evm circuit mean adding at least 2 other aux columns in evm circuit to support rw lookup

(2) As for the prev value for mem/stack/storage, agree and changed the above comments

[ed255]

(1) if i understand right, we have to 2 ways to constrain prev value：

(A) let evm circuit and state circuit both have rw table of 11 columns ( rw_counter, is_write, tag,id, address, field_tag, storage_key, value, aux1, aux2, value_prev), constrain the value_prev at state circuit side, and check rw table of evm circuit and state circuit are identical. This is what i proposed.

(B) keep state circuit as is, and let evm circuit have a 10 column rw table(without the value_prev col), and rw lookup will be like lookup(11_element_rw_values_of_opcodes, [ ..10_element_rw_table, a_value_prev_expression_computed_from_other_expressions ]) My point is, in order to compute the prev value expression, we need more aux columns in evm circuit like lexicographic_ordering_upper_limb_difference_is_zero and is_storage_key_unchanged (to calculate exp like not_first_access). Removing one value_prev col in evm circuit mean adding at least 2 other aux columns in evm circuit to support rw lookup

I agree on your analysis that we have 2 ways to approach this. And now I understand why you propose having the value_prev column (so that the total number of columns remains lower), I wasn't considering that. In general, anything that reduces the number of columns is better :)

(2) As for the prev value for mem/stack/storage, agree and changed the above comments

:+1:

[ed255]

@z2trillion @lispc do you think this issue has been resolved already with the current state of the state circuit?

[lispc]

i guess not? There is an initial_value in state circuit, but we have to constrain it with value_prev col and value_committed ciol in rw table later. After https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/621 and https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/670 and https://github.com/privacy-scaling-explorations/zkevm-circuits/issues/557 are done, we can revisit it.

I remember the most missing pieces the value_prev / value_committed of Rw::Account.

[ashWhiteHat]

Hi @lispc We already have value_prev and value_committed constraint. https://github.com/privacy-scaling-explorations/zkevm-specs/blob/master/src/zkevm_specs/state.py#L174

Could you close this issue and following issue accordingly? https://github.com/privacy-scaling-explorations/zkevm-circuits/issues/557

[lispc]

thanks! Currently @z2trillion is working on state-circuit and he will check this soon!

[ed255]

I found this reference in the circuits to this issue: https://github.com/privacy-scaling-explorations/zkevm-circuits/blob/9c4ce84699b1958216d50591c2a4bdaf8399020d/zkevm-circuits/src/state_circuit.rs#L511-L513

[aguzmant103]

Hey @z2trillion just following up, have you had a chance to check this issue?

[aguzmant103]

Notes: Synchronize State Circuit#364 is a blocker for this one so @ashWhiteHat working on this one first

[lispc]

I reviewed the codes again recently and i think in state circuit value.prev() is used to build constraints while value_prev.cur() is ignored. In evm circuit value_prev.cur() is used much. So we have to build some connection between value.prev() and value_prev.cur()