zkevm-circuits icon indicating copy to clipboard operation
zkevm-circuits copied to clipboard

Handle `is_first` and `is_last` constraint in copy_circuit

Open KimiWu123 opened this issue 1 year ago • 1 comments

Describe the bug

https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/1419#discussion_r1201689532, Han found that there is no constraint to enforce is_first to be 1 and after discussion, there is no constraint for is_last either. More investigating the constraints in copy_circuit, we need to take care the row rotations more carefully. Take value_acc_rlc as example, we take a value from Rotation(2), but we didn't ensure the current row is not the last copy step (which means the next two row could be a next copy event or this copy step is the end of this table).

Conclusion

  1. Enforce is_first and is_last to 1 at first and last row properly.
  2. Constraints "bytes_left == bytes_left_next + 1 for non-last step" and "value_acc_rlc(2) == value_acc_rlc(0) * r + value(2)" access values from Rotation(2)

Just draw a simple example to visualize the relationship of each row in copy_circuit

*Assuming q_enable == true for every row, and ignore is_padand is_code for simplicity.

q_step is_last value value_acc_rlc copy_table.is_first copy_table.bytes_left copy_table.tag/id/src_addr_end
1 0 $byte[0] $byte[0] 1 n TxCalldata/$txID/$cdLength
0 0 $byte[0] $byte[0] 0 - Memory/$callID/-
...
1 0 $byte[i] $value_acc_rlc[i] 0 n - i TxCalldata/$txID/$cdLength
0 0 $byte[i] $value_acc_rlc[i] 0 - Memory/$callID/-
...
1 0 $byte[n-1] $value_acc_rlc[n-1] 0 1 TxCalldata/$txID/$cdLength
0 1 $byte[n-1] $value_acc_rlc[n-1] 0 - Memory/$callID/-

*$value_acc_rlc[i] = $value_acc_rlc[i-1] + $byte[i] * r

KimiWu123 avatar May 24 '23 08:05 KimiWu123

On a side note, I think it would be interesting to develop a framework to write and evaluate state machine-like circuits so that we spot these underconstraints faster. In this case we could see that there are 4 possible states: First, Middle, Last, FirstAndLast. Each state has some associated expression:

  • First: is_first=1 and is_last=0
  • Middle: is_first=0 and is_last=0
  • Last: is_first=0 and is_last=1
  • FirstAndLast: is_first=1 and is_last=1

Then we have transition conditions which constraint what the current or next state is considering signals in the current state; and in this case they are missing. A similar thing happened in the Bytecode Circuit: https://github.com/privacy-scaling-explorations/zkevm-circuits/issues/1332

ed255 avatar May 24 '23 10:05 ed255