Soundness Bug: SHL Opcode Missing Constraint
kcharbo3 opened this issue · 1 comments
The SHL opcode circuit takes in shf0
as input, which is supposed to be the first byte of the shift
input. However, I don't see any constraints that forces shf0
to actually be the first byte. It is assigned correctly in the assign_exec_step
function:
But I don't believe this actually constrains it (unless I'm missing a hidden copy constraint).
Without this constraint, the divisor is not properly constrained via lookup to actually be 2^shift
. So the following constraint is useless if shf0
is not the first byte.
zkevm-circuits/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs
Lines 100 to 112 in 27a9173
This would allow a malicious prover to satisfy the constraints with:
q = 2
d = 4
r = 0
div = 8
shift = 1
So 2 1 SHL
would output 8
successfully. This is incorrect as 2 1 SHL
should be constrained to output 4
. Here the divisor was not constrained to 2^1
, so the malicious prover used 2^2 instead
to get their desired output of 8
.
Yes. It seems that we should add a constraint of shf0 == shift.cells[0]
.