You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Jul 5, 2024. It is now read-only.
#1419 (comment), 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 and is_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 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
The text was updated successfully, but these errors were encountered:
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: #1332
Describe the bug
#1419 (comment), Han found that there is no constraint to enforce
is_first
to be1
and after discussion, there is no constraint foris_last
either. More investigating the constraints incopy_circuit
, we need to take care the row rotations more carefully. Takevalue_acc_rlc
as example, we take a value fromRotation(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
is_first
andis_last
to 1 at first and last row properly."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 ignoreis_pad
andis_code
for simplicity.*$value_acc_rlc[i] = $value_acc_rlc[i-1] + $byte[i] * r
The text was updated successfully, but these errors were encountered: