Feat/#1474 rw lookup index error

bus-mapping/src/evm/opcodes/create.rs

@@ -251,7 +251,6 @@ impl<const IS_CREATE2: bool> Opcode for Create<IS_CREATE2> {
                     (CallContextField::IsStatic, false.to_word()),
                     (CallContextField::IsCreate, true.to_word()),
                     (CallContextField::CodeHash, code_hash.to_word()),
-                    (CallContextField::Value, callee.value),
                 ] {
                     state.call_context_write(&mut exec_step, callee.call_id, field, value);
                 }

zkevm-circuits/src/evm_circuit/execution.rs

@@ -23,6 +23,7 @@ use crate::{
     table::LookupTable,
     util::{query_expression, Challenges, Expr},
 };
+use bus_mapping::operation::Target;
 use eth_types::{evm_unimplemented, Field};
 use gadgets::util::not;
 use halo2_proofs::{
@@ -1318,7 +1319,6 @@ impl<F: Field> ExecutionConfig<F> {
                 );
             }
         }
-        //}
         Ok(())
     }
 
@@ -1357,16 +1357,37 @@ impl<F: Field> ExecutionConfig<F> {
             // challenges not ready
             return;
         }
+
+        let mut copy_lookup_count = 0;
         let mut assigned_rw_values = Vec::new();
         for (name, v) in assigned_stored_expressions {
-            if name.starts_with("rw lookup ")
+            // If any `copy lookup` which dst_tag or src_tag is Memory in opcode execution,
+            // block.get_rws() contains memory operations but
+            // assigned_stored_expressions only has a single `copy lookup` expression without
+            // any rw memory lookup.
+            // So, we include `copy lookup` in assigned_rw_values as well, then we could verify
+            // those memory operations later.
+            if (name.starts_with("rw lookup ") || name.starts_with("copy lookup"))
                 && !v.is_zero_vartime()
                 && !assigned_rw_values.contains(&(name.clone(), *v))
             {
                 assigned_rw_values.push((name.clone(), *v));
+
+                if name.starts_with("copy lookup") {
+                    copy_lookup_count += 1;
+                }
             }
         }
 
+        // TODO: We should find a better way to avoid this kind of special case.
+        // #1489 is the issue for this refactor.
+        if copy_lookup_count > 1 {
+            log::warn!("The number of copy events is more than 1, it's not supported by current design. Stop checking this step: {:?}", 
+                step
+            );
+            return;
+        }
+
         let rlc_assignments: BTreeSet<_> = (0..step.rw_indices_len())
             .map(|index| block.get_rws(step, index))
             .map(|rw| {
@@ -1381,23 +1402,39 @@ impl<F: Field> ExecutionConfig<F> {
         // Check that every rw_lookup assigned from the execution steps in the EVM
         // Circuit is in the set of rw operations generated by the step.
         for (name, value) in assigned_rw_values.iter() {
+            if name.starts_with("copy lookup") {
+                continue;
+            }
             if !rlc_assignments.contains(value) {
                 log::error!("rw lookup error: name: {}, step: {:?}", *name, step);
             }
         }
+
+        // if copy_rw_counter_delta is zero, ignore `copy lookup` event.
+        if step.copy_rw_counter_delta == 0 && copy_lookup_count > 0 {
+            copy_lookup_count = 0;
+        }
+
         // Check that the number of rw operations generated from the bus-mapping
         // correspond to the number of assigned rw lookups by the EVM Circuit
-        // plus the number of rw lookups done by the copy circuit.
-        if step.rw_indices_len() != assigned_rw_values.len() + step.copy_rw_counter_delta as usize {
+        // plus the number of rw lookups done by the copy circuit
+        // minus the number of copy lookup event.
+        if step.rw_indices_len()
+            != assigned_rw_values.len() + step.copy_rw_counter_delta as usize - copy_lookup_count
+        {
             log::error!(
-                "step.rw_indices.len: {} != assigned_rw_values.len: {} + step.copy_rw_counter_delta: {} in step: {:?}", 
+                "step.rw_indices.len: {} != assigned_rw_values.len: {} + step.copy_rw_counter_delta: {} - copy_lookup_count: {} in step: {:?}", 
                 step.rw_indices_len(),
                 assigned_rw_values.len(),
                 step.copy_rw_counter_delta,
+                copy_lookup_count,
                 step
             );
         }
+
         let mut rev_count = 0;
+        let mut offset = 0;
+        let mut copy_lookup_processed = false;
         for (idx, assigned_rw_value) in assigned_rw_values.iter().enumerate() {
             let is_rev = if assigned_rw_value.0.contains(" with reversion") {
                 rev_count += 1;
@@ -1411,14 +1448,46 @@ impl<F: Field> ExecutionConfig<F> {
                 rev_count,
                 step.reversible_write_counter_delta
             );
+
             // In the EVM Circuit, reversion rw lookups are assigned after their
             // corresponding rw lookup, but in the bus-mapping they are
             // generated at the end of the step.
             let idx = if is_rev {
                 step.rw_indices_len() - rev_count
             } else {
-                idx - rev_count
+                idx - rev_count + offset - copy_lookup_processed as usize
             };
+
+            // TODO: can remove after #1483 fixed
+            // step.rw_indices_len() doesn't inclued copy_rw_counter_delta in some cases
+            // which will cuase out of boundary while calling rw_index().
+            // Beside, if this condition holds, `copy lookup` is the last element of
+            // assigned_rw_value. Therefore, can ignore it for now.
+            if idx > step.rw_indices_len() - 1 {
+                continue;
+            }
+
+            // If assigned_rw_value is a `copy lookup` event, the following
+            // `step.copy_rw_counter_delta` rw lookups must be memory operations.
+            if assigned_rw_value.0.starts_with("copy lookup") {
+                for i in 0..step.copy_rw_counter_delta as usize {
+                    let index = idx + i;
+                    let rw = block.get_rws(step, index);
+                    if rw.tag() != Target::Memory {
+                        log::error!(
+                                "incorrect rw memory witness from copy lookup.\n lookup name: \"{}\"\n {}th rw of step {:?}, rw: {:?}",
+                                assigned_rw_value.0,
+                                index,
+                                step.execution_state(),
+                                rw);
+                    }
+                }
+
+                offset = step.copy_rw_counter_delta as usize;
+                copy_lookup_processed = true;
+                continue;
+            }
+
             let rw = block.get_rws(step, idx);
             let table_assignments = rw.table_assignment_aux(evm_randomness);
             let rlc = table_assignments.rlc(lookup_randomness);

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

@@ -310,8 +310,7 @@ impl<F: Field, const IS_CREATE2: bool, const S: ExecutionState> ExecutionGadget<
                     }
 
                     cb.require_step_state_transition(StepStateTransition {
-                        // +1: move to new context
-                        rw_counter: Delta(cb.rw_counter_offset() + 1.expr()),
+                        rw_counter: Delta(cb.rw_counter_offset()),
                         call_id: To(callee_call_id.expr()),
                         is_root: To(false.expr()),
                         is_create: To(true.expr()),