zkevm-circuits
zkevm-circuits copied to clipboard
Handle `is_first` and `is_last` constraint in copy_circuit
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
- Enforce
is_first
andis_last
to 1 at first and last row properly. - 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 fromRotation(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_pad
and 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
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