Soundness Bug: SHL Opcode Missing Constraint

[kcharbo3]

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:

zkevm-circuits/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs

Line 151 in 27a9173

let shf0 = pop1.to_le_bytes()[0];

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

	// Constrain divisor_lo == 2^shf0 when shf0 < 128, and
	// divisor_hi == 2^(128 - shf0) otherwise.
	let divisor_lo = from_bytes::expr(&divisor.cells[..16]);
	let divisor_hi = from_bytes::expr(&divisor.cells[16..]);
	cb.condition(1.expr() - divisor_is_zero.expr(), |cb| {
	cb.add_lookup(
	"Pow2 lookup of shf0, divisor_lo and divisor_hi",
	Lookup::Fixed {
	tag: FixedTableTag::Pow2.expr(),
	values: [shf0.expr(), divisor_lo.expr(), divisor_hi.expr()],
	},
	);
	});

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.

[silathdiir]

Yes. It seems that we should add a constraint of shf0 == shift.cells[0].