Finish all target of read-write consistency check

[han0110]

In State circuit we need to verify kinds of access records are consistent between different writes.

The following should be described as part of specs/circuits/state.md:

• What's the data contained in different kinds of target
• For different kinds of target, what's the constraints of:
  • Grouping different unit
  • Writing value
• How to calculate the total meaningful access records

(Some of them have been described in state-proof.md but might be outdated)

[han0110]

For more detailed rationale, please refer to https://hackmd.io/VCGteyZEQFKUjHA_A72f1Q.

[ed255]

The state circuit is specified in https://github.com/appliedzkp/zkevm-specs/blob/master/specs/state-proof.md

* What's the data contained in different kinds of target

Done.

* For different kinds of target, what's the constraints of:

  * Grouping different unit
  * Writing value

Done

* How to calculate the total meaningful access records

TODO.

• [x] There's currently no constraints to count the number of rows with rwc != 0. This no longer applies

If I understood it correctly, @han0110 proposed the idea of using the shuffle argument to verify that the rwc values used in the EVM circuit match 1-1 with the rwc values used in the state circuit; so I understand that with this approach the count of rwc != 0 wouldn't be needed. Nevertheless in the state circuit we have many rows where rwc = 0, and I'm not sure if that poses a difficulty when using the shuffle argument.

Other TODOs:

• [ ] Define constraint rules for
  • [x] TxRefund
  • [x] TxAccessListAccount
  • [x] TxAccessListAccountStorage
  • [ ] AccountDestructed
• [x] Extend spec with new tags (and their corresponding constraints)
  • [x] TxLog
  • [x] TxReceipt
• [ ] MPT lookups
  • [x] Storage
  • [x] Account
  • [ ] AccountDestructed (the account destructed is effective at the end of the block, so we may need a second tag for checking the account deletion via MPT lookup)

[han0110]

Yes, in the approach using shuffle instead of lookup, we don't need to count how many row with rwc != 0. We only need to make sure rwc is strict monotonically increasing of the same key.

Nevertheless in the state circuit we have many rows where rwc = 0, and I'm not sure if that poses a difficulty when using the shuffle argument.

Such special rows with rwc = 0 will be masked to be 0 just like padding rows, and since rwc is constraint to be strict monotonically increasing, so prover can't have 2 continuous rwc = 0 row to forge a unexpected initial value. Then in EVM circuit, the only thing we need to do is make sure all rows with rwc != 0 is laid in the polynomial which should be the shuffle of rw_table. So I think it won't pose a difficulty then.

[ed255]

The approach to make sure the number of rw operations in state circuit and evm circuit are the same is resolved through the idea implemented in https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/558