Copy: remove LtChip

bus-mapping/src/circuit_input_builder/execution.rs

@@ -391,6 +391,7 @@ pub struct CopyEvent {
     /// Represents the start address at the source of the copy event.
     pub src_addr: u64,
     /// Represents the end address at the source of the copy event.
+    /// It must be `src_addr_end >= src_addr`.
     pub src_addr_end: u64,
     /// Represents the source type.
     pub src_type: CopyDataType,

gadgets/src/is_equal.rs

@@ -5,9 +5,10 @@ use halo2_proofs::{
     arithmetic::FieldExt,
     circuit::{Chip, Region, Value},
     plonk::{ConstraintSystem, Error, Expression, VirtualCells},
+    poly::Rotation,
 };
 
-use super::is_zero::{IsZeroChip, IsZeroInstruction};
+use super::is_zero::{IsZeroChip, IsZeroConfig, IsZeroInstruction};
 
 /// Instruction that the IsEqual chip needs to implement.
 pub trait IsEqualInstruction<F: FieldExt> {
@@ -25,11 +26,24 @@ pub trait IsEqualInstruction<F: FieldExt> {
 #[derive(Clone, Debug)]
 pub struct IsEqualConfig<F> {
     /// Stores an IsZero chip.
-    pub is_zero_chip: IsZeroChip<F>,
+    is_zero_config: IsZeroConfig<F>,
     /// Expression that denotes whether the chip evaluated to equal or not.
     pub is_equal_expression: Expression<F>,
 }
 
+impl<F: Field> IsEqualConfig<F> {
+    /// Returns the is_equal expression from inputs, at any rotation where q_enable=1.
+    pub fn expr_at(
+        &self,
+        meta: &mut VirtualCells<'_, F>,
+        at: Rotation,
+        lhs: Expression<F>,
+        rhs: Expression<F>,
+    ) -> Expression<F> {
+        self.is_zero_config.expr_at(meta, at, lhs - rhs)
+    }
+}
+
 /// Chip that compares equality between two expressions.
 #[derive(Clone, Debug)]
 pub struct IsEqualChip<F> {
@@ -52,7 +66,7 @@ impl<F: Field> IsEqualChip<F> {
         let is_equal_expression = is_zero_config.is_zero_expression.clone();
 
         IsEqualConfig {
-            is_zero_chip: IsZeroChip::construct(is_zero_config),
+            is_zero_config,
             is_equal_expression,
         }
     }
@@ -71,7 +85,11 @@ impl<F: Field> IsEqualInstruction<F> for IsEqualChip<F> {
         lhs: Value<F>,
         rhs: Value<F>,
     ) -> Result<(), Error> {
-        self.config.is_zero_chip.assign(region, offset, lhs - rhs)?;
+        IsZeroChip::construct(self.config.is_zero_config.clone()).assign(
+            region,
+            offset,
+            lhs - rhs,
+        )?;
 
         Ok(())
     }

gadgets/src/is_zero.rs

@@ -43,6 +43,16 @@ impl<F: Field> IsZeroConfig<F> {
         self.is_zero_expression.clone()
     }
 
+    /// Returns the is_zero expression from inputs, at any rotation where q_enable=1.
+    pub fn expr_at(
+        &self,
+        meta: &mut VirtualCells<'_, F>,
+        at: Rotation,
+        value: Expression<F>,
+    ) -> Expression<F> {
+        1.expr() - value * meta.query_advice(self.value_inv, at)
+    }
+
     /// Annotates columns of this gadget embedded within a circuit region.
     pub fn annotate_columns_in_region(&self, region: &mut Region<F>, prefix: &str) {
         [(self.value_inv, "GADGETS_IS_ZERO_inverse_witness")]

zkevm-circuits/src/copy_circuit.rs

@@ -19,7 +19,6 @@ use eth_types::{Field, Word};
 use gadgets::{
     binary_number::BinaryNumberChip,
     is_equal::{IsEqualChip, IsEqualConfig, IsEqualInstruction},
-    less_than::{LtChip, LtConfig, LtInstruction},
     util::{and, not, select, sum, Expr},
 };
 use halo2_proofs::{
@@ -94,10 +93,8 @@ pub struct CopyCircuitConfig<F> {
     /// The Copy Table contains the columns that are exposed via the lookup
     /// expressions
     pub copy_table: CopyTable,
-    /// Lt chip to check: src_addr < src_addr_end.
-    /// Since `src_addr` and `src_addr_end` are u64, 8 bytes are sufficient for
-    /// the Lt chip.
-    pub addr_lt_addr_end: LtConfig<F, 8>,
+    /// Detect when the address reaches the limit src_addr_end.
+    pub is_src_end: IsEqualConfig<F>,
     /// Whether this is the end of a word (last byte).
     pub is_word_end: IsEqualConfig<F>,
     /// non pad and non mask witness to reduce the degree of lookups.
@@ -183,7 +180,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
         bytecode_table.annotate_columns(meta);
         copy_table.annotate_columns(meta);
 
-        let addr_lt_addr_end = LtChip::configure(
+        let is_src_end = IsEqualChip::configure(
             meta,
             |meta| meta.query_selector(q_step),
             |meta| meta.query_advice(addr, Rotation::cur()),
@@ -282,7 +279,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
                 and::expr([
                     not::expr(meta.query_selector(q_step)),
                     is_first.expr(),
-                ]),
+                    ]),
             );
             cb.require_zero(
                 "is_last == 0 when q_step == 1",
@@ -291,14 +288,19 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
                     meta.query_selector(q_step),
                 ]),
             );
+
+            let is_pad_next = meta.query_advice(is_pad, Rotation(2));
+            let is_pad = meta.query_advice(is_pad, Rotation::cur());
+            cb.require_boolean("is_pad is boolean", is_pad.expr());
             cb.require_equal(
                 "non_pad_non_mask = !pad AND !mask",
                 meta.query_advice(non_pad_non_mask, Rotation::cur()),
                 and::expr([
-                    not::expr(meta.query_advice(is_pad, Rotation::cur())),
+                    not::expr(is_pad.expr()),
                     not::expr(meta.query_advice(mask, Rotation::cur())),
                 ]),
             );
+
             // On a masked row, the value is the value_prev.
             cb.condition(
                 meta.query_advice(mask, Rotation::cur()),
@@ -316,13 +318,18 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
 
             let is_last_step = meta.query_advice(is_last, Rotation::cur())
                 + meta.query_advice(is_last, Rotation::next());
+            let is_last = meta.query_advice(is_last, Rotation::cur());
+
+            // Prevent an event from spilling into the disabled rows. This also ensures that eventually is_last=1.
+            cb.require_zero(
+                "the next row is enabled",
+                (is_event.expr() - is_last.expr())
+                * not::expr(meta.query_fixed(q_enable, Rotation::next()))
+            );
 
             // Whether this row is part of an event but not the last step. When true, the next step is derived from the current step.
             let is_continue = is_event.expr() - is_last_step.expr();
 
-            // Prevent an event from spilling into the disabled rows. This also ensures that eventually is_last=1.
-            cb.require_zero("the next row is enabled", is_continue.expr() * not::expr(meta.query_fixed(q_enable, Rotation::next())));
-
             let is_word_end = is_word_end.is_equal_expression.expr();
 
             // Apply the same constraints for the RLCs of words before and after the write.
@@ -451,7 +458,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
                 let rwc_diff = is_rw_type.expr() * is_word_end.expr();
                 let next_value = meta.query_advice(rwc_inc_left, Rotation::cur()) - rwc_diff;
                 let update_or_finish = select::expr(
-                    meta.query_advice(is_last, Rotation::cur()),
+                    is_last.expr(),
                     0.expr(),
                     meta.query_advice(rwc_inc_left, Rotation::next()),
                 );
@@ -464,7 +471,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
 
             // Maintain rw_counter based on rwc_inc_left. Their sum remains constant in all cases.
             cb.condition(
-                not::expr(meta.query_advice(is_last, Rotation::cur())),
+                not::expr(is_last.expr()),
                 |cb| {
                     cb.require_equal(
                         "rows[0].rw_counter + rows[0].rwc_inc_left == rows[1].rw_counter + rows[1].rwc_inc_left",
@@ -517,7 +524,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
                     {
                         let current = meta.query_advice(value_acc, Rotation::cur());
                         // If source padding, replace the value with 0.
-                        let value_or_pad = meta.query_advice(value, Rotation(2)) * not::expr(meta.query_advice(is_pad, Rotation(2)));
+                        let value_or_pad = meta.query_advice(value, Rotation(2)) * not::expr(is_pad_next.expr());
                         let accumulated = current.expr() * challenges.keccak_input() + value_or_pad;
                         // If masked, copy the accumulator forward, otherwise update it.
                         let copy_or_acc = select::expr(mask_next, current, accumulated);
@@ -532,7 +539,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
 
             // Forward rlc_acc from the event to all rows.
             cb.condition(
-                not::expr(meta.query_advice(is_last, Rotation::cur())),
+                not::expr(is_last.expr()),
                 |cb| {
                     cb.require_equal(
                         "rows[0].rlc_acc == rows[1].rlc_acc",
@@ -590,15 +597,36 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
         meta.create_gate("verify step (q_step == 1)", |meta| {
             let mut cb = BaseConstraintBuilder::default();
 
-            cb.require_equal(
-                "is_pad == 1 - (src_addr < src_addr_end) for read row",
-                1.expr() - addr_lt_addr_end.is_lt(meta, None),
-                meta.query_advice(is_pad, Rotation::cur()),
-            );
-            cb.require_zero(
-                "is_pad == 0 for write row",
-                meta.query_advice(is_pad, Rotation::next()),
-            );
+            let [is_pad, is_pad_writer, is_pad_next] =
+                [Rotation::cur(), Rotation::next(), Rotation(2)]
+                    .map(|at| meta.query_advice(is_pad, at));
+
+            cb.require_zero("is_pad == 0 for write row", is_pad_writer);
+
+            let [is_src_end, is_src_end_next] = [Rotation::cur(), Rotation(2)].map(|at| {
+                let addr = meta.query_advice(addr, at);
+                let src_addr_end = meta.query_advice(src_addr_end, at);
+                is_src_end.expr_at(meta, at, addr, src_addr_end)
+            });
+
+            let is_first = meta.query_advice(is_first, Rotation::cur());
+            let not_last = not::expr(meta.query_advice(is_last, Rotation::next()));
+
+            // When and after the address reaches the limit src_addr_end, zero-padding is enabled.
+            cb.condition(is_first, |cb| {
+                cb.require_equal(
+                    "is_pad starts at src_addr == src_addr_end",
+                    is_pad.expr(),
+                    is_src_end.expr(),
+                );
+            });
+            cb.condition(not_last, |cb| {
+                cb.require_equal(
+                    "is_pad=1 when src_addr == src_addr_end, otherwise it keeps the previous value",
+                    select::expr(is_src_end_next, 1.expr(), is_pad.expr()),
+                    is_pad_next.expr(),
+                );
+            });
 
             cb.gate(and::expr([
                 meta.query_fixed(q_enable, Rotation::cur()),
@@ -718,7 +746,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
             is_memory,
             is_tx_log,
             q_enable,
-            addr_lt_addr_end,
+            is_src_end,
             is_word_end,
             non_pad_non_mask,
             copy_table,
@@ -737,7 +765,7 @@ impl<F: Field> CopyCircuitConfig<F> {
         region: &mut Region<F>,
         offset: &mut usize,
         tag_chip: &BinaryNumberChip<F, CopyDataType, 4>,
-        lt_chip: &LtChip<F, 8>,
+        is_src_end_chip: &IsEqualChip<F>,
         lt_word_end_chip: &IsEqualChip<F>,
         challenges: Challenges<Value<F>>,
         copy_event: &CopyEvent,
@@ -812,8 +840,13 @@ impl<F: Field> CopyCircuitConfig<F> {
 
             // lt chip
             if is_read {
-                let addr = unwrap_value(table_row[2].0);
-                lt_chip.assign(region, *offset, addr, F::from(copy_event.src_addr_end))?;
+                let addr = table_row[2].0;
+                is_src_end_chip.assign(
+                    region,
+                    *offset,
+                    addr,
+                    Value::known(F::from(copy_event.src_addr_end)),
+                )?;
             }
 
             lt_word_end_chip.assign(
@@ -893,7 +926,7 @@ impl<F: Field> CopyCircuitConfig<F> {
         );
 
         let tag_chip = BinaryNumberChip::construct(self.copy_table.tag);
-        let lt_chip = LtChip::construct(self.addr_lt_addr_end);
+        let is_src_end_chip = IsEqualChip::construct(self.is_src_end.clone());
         let lt_word_end_chip = IsEqualChip::construct(self.is_word_end.clone());
 
         layouter.assign_region(
@@ -929,7 +962,7 @@ impl<F: Field> CopyCircuitConfig<F> {
                         &mut region,
                         &mut offset,
                         &tag_chip,
-                        &lt_chip,
+                        &is_src_end_chip,
                         &lt_word_end_chip,
                         challenges,
                         copy_event,
@@ -943,7 +976,7 @@ impl<F: Field> CopyCircuitConfig<F> {
                         &mut offset,
                         false,
                         &tag_chip,
-                        &lt_chip,
+                        &is_src_end_chip,
                         &lt_word_end_chip,
                     )?;
                 }
@@ -953,15 +986,15 @@ impl<F: Field> CopyCircuitConfig<F> {
                     &mut offset,
                     true,
                     &tag_chip,
-                    &lt_chip,
+                    &is_src_end_chip,
                     &lt_word_end_chip,
                 )?;
                 self.assign_padding_row(
                     &mut region,
                     &mut offset,
                     true,
                     &tag_chip,
-                    &lt_chip,
+                    &is_src_end_chip,
                     &lt_word_end_chip,
                 )?;
 
@@ -977,7 +1010,7 @@ impl<F: Field> CopyCircuitConfig<F> {
         offset: &mut usize,
         is_last_two: bool,
         tag_chip: &BinaryNumberChip<F, CopyDataType, 4>,
-        lt_chip: &LtChip<F, 8>,
+        is_src_end_chip: &IsEqualChip<F>,
         lt_word_end_chip: &IsEqualChip<F>,
     ) -> Result<(), Error> {
         // q_enable
@@ -1138,8 +1171,13 @@ impl<F: Field> CopyCircuitConfig<F> {
         )?;
         // tag
         tag_chip.assign(region, *offset, &CopyDataType::Padding)?;
-        // Assign LT gadget
-        lt_chip.assign(region, *offset, F::zero(), F::one())?;
+        // Assign IsEqual gadgets
+        is_src_end_chip.assign(
+            region,
+            *offset,
+            Value::known(F::zero()),
+            Value::known(F::one()),
+        )?;
         lt_word_end_chip.assign(
             region,
             *offset,

zkevm-circuits/src/table.rs

@@ -37,7 +37,6 @@ use halo2_proofs::plonk::SecondPhase;
 
 use itertools::Itertools;
 use keccak256::plain::Keccak;
-use log::trace;
 use std::array;
 use strum_macros::{EnumCount, EnumIter};
 
@@ -1506,7 +1505,8 @@ impl CopyTable {
         copy_event: &CopyEvent,
         challenges: Challenges<Value<F>>,
     ) -> Vec<(CopyDataType, CopyTableRow<F>, CopyCircuitRow<F>)> {
-        trace!("assignments CopyEvent challenge  {challenges:?} ");
+        assert!(copy_event.src_addr_end >= copy_event.src_addr);
+
         let mut assignments = Vec::new();
         // rlc_acc
         let rlc_acc = {