diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget/rlp.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget/rlp.rs index 1cae8e56cf..6a5a2154c1 100644 --- a/zkevm-circuits/src/evm_circuit/util/math_gadget/rlp.rs +++ b/zkevm-circuits/src/evm_circuit/util/math_gadget/rlp.rs @@ -46,10 +46,15 @@ impl RlpU64Gadget { .map(|(byte, indicator)| byte.expr() * indicator.expr()), ); let most_significant_byte_is_zero = IsZeroGadget::construct(cb, most_significant_byte); + let is_lt_128 = cb.query_bool(); let value = expr_from_bytes(&value_rlc.cells); cb.condition(most_significant_byte_is_zero.expr(), |cb| { cb.require_zero("if most significant byte is 0, value is 0", value.clone()); + cb.require_zero( + "if most significant byte is 0, value is less than 128", + 1.expr() - is_lt_128.expr(), + ); }); for (i, is_most_significant) in is_most_significant_byte.iter().enumerate() { @@ -67,10 +72,18 @@ impl RlpU64Gadget { }); } - let is_lt_128 = cb.query_bool(); - cb.condition(is_lt_128.expr(), |cb| { - cb.range_lookup(value, 128); - }); + // If is_lt_128, then value < 128, checked by a lookup. + + // Otherwise, then value >= 128, checked as follows: + // - Either the first byte is not the most significant, and there is a more significant one; + // - Or the first byte is the most significant, and it is >= 128. value ∈ [128, 256) (value + // - 128) ∈ [0, 128) + let byte_128 = value_rlc.cells[0].expr() - 128.expr(); + let is_first = is_most_significant_byte[0].expr(); + let byte_128_or_zero = byte_128 * is_first; + + let value_lt_128 = select::expr(is_lt_128.expr(), value, byte_128_or_zero); + cb.range_lookup(value_lt_128, 128); Self { value_rlc,