From 7b77f9c9141c25216c5b689327a9d76b74aeb359 Mon Sep 17 00:00:00 2001
From: naure <naure@users.noreply.github.com>
Date: Fri, 2 Jun 2023 14:34:57 +0200
Subject: [PATCH] Fix RLC is_lt_128 (#1449)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

### Description

In the RLC gadget, the indicator `is_lt_128` must be equivalent to
`value < 128`.

However, currently only the `true` case is handled. This PR handles both
`true` and `false` cases.

### Issue Link

Scroll internal.

### Type of change

- [x] Bug fix (non-breaking change which fixes an issue)

---------

Co-authored-by: Aurélien Nicolas <info@nau.re>
Co-authored-by: Han <tinghan0110@gmail.com>
---
 .../src/evm_circuit/util/math_gadget/rlp.rs   | 21 +++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

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<F: Field> RlpU64Gadget<F> {
                 .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<F: Field> RlpU64Gadget<F> {
             });
         }
 
-        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,