From 85c773e3e77aedb6a51dafd9dfa424afe69cc942 Mon Sep 17 00:00:00 2001 From: DreamWuGit Date: Mon, 13 May 2024 12:11:12 +0800 Subject: [PATCH] feat: copy circuit support overlap copy range (#1255) * draft buss mapping for mcopy * rename to mcopy.rs * add mcopy.rs * add helper gen_copy_steps_for_memory_to_memory * add MCOPY in opcode_ids * handle opcode_id others as_u8, constant_gas etc. * draft mcopy gadgets * add gadget to execution config * remove unused fields * update buss mapping test * update gadget tests * remove unnecessary testing stuff * update ExecutionState * add cancun config * update buss mapping test * remove commented codes * enable multi copy case * fix buss mapping tests * update gas cost * remove tx id lookup * fix memory_word_size * update word size if no copy happens * add copy circuit test * remove debug log * fmt align * minor update * add OOGMemoryCopy test for mcopy * make oog memorycopy include mcopy opcode * revert temp debug changes * add more test data * minor updates * fmt adjust * fix clippy * add testool * fix memory word * increase fix table rows detected by ci * update testool * remove unused import * clippy update * fix large dest memory addr * refactor to use memory_expansion for dest_addr * handle dest_addr < src_addr * update per cargo check * intermediate clean up * fix testool * fix u64 overflow * update oog memorycopy to cover src_offset overflow case * fix clippy; fix codehash.txt * remove debug codes * fix clippy * reverted commented for testing * remove outdated comment and todo for overlap case * add unit test for overlap copy range case * add is_memory_copy column * assign is_memory_copy * change rw_counter of copy table * add is_memory_copy condition for rw_counter constraint * update constraint for rwc_inc_left * fix rwc_inc_left constraint for mcopy * enable other tests * fix clippy * fix bussmapping test * add is_copy_id_equals checking id changes * add constraint for is_memory_copy condition * remove comments * fix is_copy_id_equals_chip * format comment * remove old id_next * rename is_copy_id_equals to is_id_unchange_chip * merge combine_copy_slot_bytes_mcopy to combine_copy_slot_bytes * clean up * update comments * fmt align * add constraint: is_memory_copy is bool --------- Co-authored-by: Zhuo Zhang --- .../circuit_input_builder/input_state_ref.rs | 14 +++- bus-mapping/src/evm/opcodes/mcopy.rs | 60 +++++++++----- zkevm-circuits/src/copy_circuit.rs | 78 +++++++++++++++++-- .../src/copy_circuit/copy_gadgets.rs | 59 ++++++++++++-- .../src/evm_circuit/execution/mcopy.rs | 10 ++- zkevm-circuits/src/table.rs | 33 +++++++- 6 files changed, 208 insertions(+), 46 deletions(-) diff --git a/bus-mapping/src/circuit_input_builder/input_state_ref.rs b/bus-mapping/src/circuit_input_builder/input_state_ref.rs index 5b963aaac3..8cf11f2017 100644 --- a/bus-mapping/src/circuit_input_builder/input_state_ref.rs +++ b/bus-mapping/src/circuit_input_builder/input_state_ref.rs @@ -2252,7 +2252,7 @@ impl<'a> CircuitInputStateRef<'a> { Ok((read_steps, write_steps, prev_bytes)) } - // generates copy steps for memory to memory case. + // generates copy steps for memory to memory case(mcopy). pub(crate) fn gen_copy_steps_for_memory_to_memory( &mut self, exec_step: &mut ExecStep, @@ -2288,10 +2288,13 @@ impl<'a> CircuitInputStateRef<'a> { let mut src_chunk_index = src_range.start_slot().0; let mut dst_chunk_index = dst_range.start_slot().0; let mut prev_bytes: Vec = vec![]; + // memory word reads from source and writes to destination word let call_id = self.call()?.call_id; - for (read_chunk, write_chunk) in read_slot_bytes.chunks(32).zip(write_slot_bytes.chunks(32)) - { + + // first all reads done and then do writing, this is different from other copy cases + // (read step--> write step --> read step --> write step ...). + for read_chunk in read_slot_bytes.chunks(32) { self.push_op( exec_step, RW::READ, @@ -2303,7 +2306,9 @@ impl<'a> CircuitInputStateRef<'a> { )?; trace!("read chunk: {call_id} {src_chunk_index} {read_chunk:?}"); src_chunk_index += 32; + } + for write_chunk in write_slot_bytes.chunks(32) { self.write_chunk_for_copy_step( exec_step, write_chunk, @@ -2419,7 +2424,7 @@ fn combine_copy_slot_bytes( copy_length: usize, src_data: &[impl Into + Clone], dst_memory: &mut Memory, - is_memory_copy: bool, // indicates memroy --> memory copy type. + is_memory_copy: bool, // indicates memroy --> memory copy(mcopy) type. ) -> (MemoryWordRange, MemoryWordRange, Vec) { let mut src_range = MemoryWordRange::align_range(src_addr, copy_length); let mut dst_range = MemoryWordRange::align_range(dst_addr, copy_length); @@ -2427,6 +2432,7 @@ fn combine_copy_slot_bytes( // Extend call memory. // if is_memory_copy=true, both dst_addr and src_addr are memory address + // expand from larger address. if is_memory_copy && dst_addr < src_addr { dst_memory.extend_for_range(src_addr.into(), copy_length.into()); } else { diff --git a/bus-mapping/src/evm/opcodes/mcopy.rs b/bus-mapping/src/evm/opcodes/mcopy.rs index 4628c0206b..dba31ddb29 100644 --- a/bus-mapping/src/evm/opcodes/mcopy.rs +++ b/bus-mapping/src/evm/opcodes/mcopy.rs @@ -108,8 +108,11 @@ mod mcopy_tests { #[test] fn mcopy_opcode_impl() { + // zero size copy test_ok(0x40, 0x50, 0x0); - test_ok(0x40, 0x50, 0x02); + // simple size copy + test_ok(0x40, 0x60, 0x02); + // large size copy test_ok(0x60, 0x80, 0xA0); test_ok(0x90, 0x200, 0xE9); } @@ -173,25 +176,33 @@ mod mcopy_tests { // add RW table memory word reads. let read_end = src_offset + copy_size; let read_slot_start = src_offset - src_offset % 32; - let read_slot_end = read_end - read_end % 32; - let read_word_ops = if read_slot_end == read_slot_start && copy_size != 0 { - // read within one slot. - 1 + let read_slot_end = if read_end % 32 == 0 { + read_end - read_end % 32 } else { + read_end - read_end % 32 + 32 + }; + + let read_word_ops = if copy_size != 0 { (read_slot_end - read_slot_start) / 32 + } else { + 0 }; let write_end = dest_offset + copy_size; let write_slot_start = dest_offset - dest_offset % 32; - let write_slot_end = write_end - write_end % 32; - let write_word_ops = if write_slot_end == write_slot_start && copy_size != 0 { - // write within one slot - 1 + let write_slot_end = if write_end % 32 == 0 { + write_end - write_end % 32 } else { + write_end - write_end % 32 + 32 + }; + + let write_word_ops = if copy_size != 0 { (write_slot_end - write_slot_start) / 32 + } else { + 0 }; - let word_ops = read_word_ops + write_word_ops; + let word_ops = read_word_ops.max(write_word_ops) * 2; let read_bytes = builder.block.copy_events[0] .copy_bytes @@ -222,30 +233,37 @@ mod mcopy_tests { .collect::>(), (0..word_ops) .map(|idx| { - // rw_index as read or write operation's index. - let rw_index = idx / 2 + idx % 2; - if idx % 2 == 0 { - // first read op + // index that first write op starts from, since read and write ops have + // same length, so write_index starts from half of word_ops count. + let write_index = word_ops / 2; + if idx < write_index { + // first all read ops ( RW::READ, MemoryOp::new_write( expected_call_id, - MemoryAddress(read_slot_start + rw_index * 32), - Word::from(&read_bytes[rw_index * 32..(rw_index + 1) * 32]), + MemoryAddress(read_slot_start + idx * 32), + Word::from(&read_bytes[idx * 32..(idx + 1) * 32]), // previous value is same to value for reading operation - Word::from(&read_bytes[rw_index * 32..(rw_index + 1) * 32]), + Word::from(&read_bytes[idx * 32..(idx + 1) * 32]), ), ) } else { - // second write op + // then all write ops ( RW::WRITE, MemoryOp::new_write( expected_call_id, - MemoryAddress(write_slot_start + (rw_index - 1) * 32), - Word::from(&write_bytes[(rw_index - 1) * 32..rw_index * 32]), + MemoryAddress(write_slot_start + (idx - write_index) * 32), + Word::from( + &write_bytes + [(idx - write_index) * 32..(idx - write_index + 1) * 32], + ), // get previous value - Word::from(&prev_bytes[(rw_index - 1) * 32..rw_index * 32]), + Word::from( + &prev_bytes + [(idx - write_index) * 32..(idx - write_index + 1) * 32], + ), ), ) } diff --git a/zkevm-circuits/src/copy_circuit.rs b/zkevm-circuits/src/copy_circuit.rs index 65d73c72ac..d710f91570 100644 --- a/zkevm-circuits/src/copy_circuit.rs +++ b/zkevm-circuits/src/copy_circuit.rs @@ -20,6 +20,8 @@ use gadgets::{ is_equal::{IsEqualChip, IsEqualConfig, IsEqualInstruction}, util::{not, select, Expr}, }; + +use crate::copy_circuit::util::number_or_hash_to_field; use halo2_proofs::{ circuit::{Layouter, Region, Value}, plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector}, @@ -46,10 +48,10 @@ use crate::{ use self::copy_gadgets::{ constrain_address, constrain_bytes_left, constrain_event_rlc_acc, constrain_first_last, - constrain_forward_parameters, constrain_is_pad, constrain_mask, constrain_masked_value, - constrain_must_terminate, constrain_non_pad_non_mask, constrain_rw_counter, - constrain_rw_word_complete, constrain_tag, constrain_value_rlc, constrain_word_index, - constrain_word_rlc, + constrain_forward_parameters, constrain_is_memory_copy, constrain_is_pad, constrain_mask, + constrain_masked_value, constrain_must_terminate, constrain_non_pad_non_mask, + constrain_rw_counter, constrain_rw_word_complete, constrain_tag, constrain_value_rlc, + constrain_word_index, constrain_word_rlc, }; /// The current row. @@ -97,6 +99,8 @@ pub struct CopyCircuitConfig { pub is_bytecode: Column, /// Booleans to indicate what copy data type exists at the current row. pub is_memory: Column, + /// Booleans to indicate if mcopy data type exists at the current row. + pub is_memory_copy: Column, /// Booleans to indicate what copy data type exists at the current row. pub is_tx_log: Column, /// Booleans to indicate if `CopyDataType::AccessListAddresses` exists at @@ -110,6 +114,8 @@ pub struct CopyCircuitConfig { /// The Copy Table contains the columns that are exposed via the lookup /// expressions pub copy_table: CopyTable, + /// Detect if copy src_id equals dst_id for current row and next row. + pub is_id_unchange: IsEqualConfig, /// Detect when the address reaches the limit src_addr_end. pub is_src_end: IsEqualConfig, /// Whether this is the end of a word (last byte). @@ -167,7 +173,7 @@ impl SubCircuitConfig for CopyCircuitConfig { let value_word_rlc_prev = meta.advice_column_in(SecondPhase); let value_acc = meta.advice_column_in(SecondPhase); - let [is_pad, is_tx_calldata, is_bytecode, is_memory, is_tx_log, is_access_list_address, is_access_list_storage_key] = + let [is_pad, is_tx_calldata, is_bytecode, is_memory, is_memory_copy, is_tx_log, is_access_list_address, is_access_list_storage_key] = array_init(|_| meta.advice_column()); let is_first = copy_table.is_first; let id = copy_table.id; @@ -189,6 +195,13 @@ impl SubCircuitConfig for CopyCircuitConfig { bytecode_table.annotate_columns(meta); copy_table.annotate_columns(meta); + let is_id_unchange = IsEqualChip::configure( + meta, + |meta| meta.query_selector(q_step) * not::expr(meta.query_advice(is_last, CURRENT)), + |meta| meta.query_advice(id, CURRENT), + |meta| meta.query_advice(id, NEXT_ROW), + ); + let is_src_end = IsEqualChip::configure( meta, |meta| meta.query_selector(q_step), @@ -345,16 +358,29 @@ impl SubCircuitConfig for CopyCircuitConfig { is_word_end.expr(), ); + let is_memory_copy = meta.query_advice(is_memory_copy, CURRENT); + constrain_rw_counter( cb, meta, - is_last.expr(), + is_last_col, is_rw_type.expr(), is_row_end.expr(), + is_memory_copy.expr(), rw_counter, rwc_inc_left, ); + // constrain is_memory_copy = src_id == dst_id && src_type == dst_type == + // memory + constrain_is_memory_copy( + cb, + meta, + is_last_col, + &is_id_unchange, + is_memory, + is_memory_copy, + ); constrain_rw_word_complete(cb, is_last_step, is_rw_word_type.expr(), is_word_end); } @@ -566,11 +592,13 @@ impl SubCircuitConfig for CopyCircuitConfig { is_tx_calldata, is_bytecode, is_memory, + is_memory_copy, is_tx_log, is_access_list_address, is_access_list_storage_key, q_enable, copy_table, + is_id_unchange, is_src_end, is_word_end, non_pad_non_mask, @@ -589,6 +617,7 @@ impl CopyCircuitConfig { region: &mut Region, offset: &mut usize, tag_chip: &BinaryNumberChip, + is_id_unchange: &IsEqualChip, is_src_end_chip: &IsEqualChip, lt_word_end_chip: &IsEqualChip, challenges: Challenges>, @@ -665,6 +694,20 @@ impl CopyCircuitConfig { )?; } + let (id, id_next) = if is_read { + (©_event.src_id, ©_event.dst_id) + } else { + (©_event.dst_id, ©_event.src_id) + }; + + // assign id, id_next + is_id_unchange.assign( + region, + *offset, + number_or_hash_to_field(id, challenges.evm_word()), + number_or_hash_to_field(id_next, challenges.evm_word()), + )?; + lt_word_end_chip.assign( region, *offset, @@ -700,6 +743,16 @@ impl CopyCircuitConfig { *offset, || Value::known(F::from(tag.eq(&CopyDataType::Memory))), )?; + let is_memory_copy = copy_event.src_id == copy_event.dst_id + && copy_event.src_type.eq(&CopyDataType::Memory) + && copy_event.dst_type.eq(&CopyDataType::Memory); + region.assign_advice( + || format!("is_memory_copy at row: {}", *offset), + self.is_memory_copy, + *offset, + || Value::known(F::from(is_memory_copy)), + )?; + region.assign_advice( || format!("is_tx_log at row: {}", *offset), self.is_tx_log, @@ -750,6 +803,7 @@ impl CopyCircuitConfig { let filler_rows = max_copy_rows - copy_rows_needed - DISABLED_ROWS; let tag_chip = BinaryNumberChip::construct(self.copy_table.tag); + let is_id_unchange = IsEqualChip::construct(self.is_id_unchange.clone()); let is_src_end_chip = IsEqualChip::construct(self.is_src_end.clone()); let lt_word_end_chip = IsEqualChip::construct(self.is_word_end.clone()); @@ -785,6 +839,7 @@ impl CopyCircuitConfig { &mut region, &mut offset, &tag_chip, + &is_id_unchange, &is_src_end_chip, <_word_end_chip, challenges, @@ -792,13 +847,13 @@ impl CopyCircuitConfig { )?; log::trace!("offset after {}th copy event: {}", ev_idx, offset); } - for _ in 0..filler_rows { self.assign_padding_row( &mut region, &mut offset, true, &tag_chip, + &is_id_unchange, &is_src_end_chip, <_word_end_chip, )?; @@ -811,6 +866,7 @@ impl CopyCircuitConfig { &mut offset, false, &tag_chip, + &is_id_unchange, &is_src_end_chip, <_word_end_chip, )?; @@ -828,6 +884,7 @@ impl CopyCircuitConfig { offset: &mut usize, enabled: bool, tag_chip: &BinaryNumberChip, + is_id_unchange_chip: &IsEqualChip, is_src_end_chip: &IsEqualChip, lt_word_end_chip: &IsEqualChip, ) -> Result<(), Error> { @@ -974,6 +1031,12 @@ impl CopyCircuitConfig { // tag tag_chip.assign(region, *offset, &CopyDataType::Padding)?; // Assign IsEqual gadgets + is_id_unchange_chip.assign( + region, + *offset, + Value::known(F::zero()), + Value::known(F::one()), + )?; is_src_end_chip.assign( region, *offset, @@ -997,6 +1060,7 @@ impl CopyCircuitConfig { self.is_tx_calldata, self.is_bytecode, self.is_memory, + self.is_memory_copy, self.is_tx_log, self.is_access_list_address, self.is_access_list_storage_key, diff --git a/zkevm-circuits/src/copy_circuit/copy_gadgets.rs b/zkevm-circuits/src/copy_circuit/copy_gadgets.rs index 2dee65f004..be22e937dd 100644 --- a/zkevm-circuits/src/copy_circuit/copy_gadgets.rs +++ b/zkevm-circuits/src/copy_circuit/copy_gadgets.rs @@ -494,25 +494,48 @@ pub fn constrain_address( pub fn constrain_rw_counter( cb: &mut BaseConstraintBuilder, meta: &mut VirtualCells<'_, F>, - is_last: Expression, // The last row. + is_last_col: Column, is_rw_type: Expression, is_row_end: Expression, + is_memory_copy: Expression, rw_counter: Column, rwc_inc_left: Column, ) { // Decrement rwc_inc_left for the next row, when an RW operation happens. let rwc_diff = is_rw_type.expr() * is_row_end.expr(); let new_value = meta.query_advice(rwc_inc_left, CURRENT) - rwc_diff; + let is_last = meta.query_advice(is_last_col, CURRENT); + let is_last_two = meta.query_advice(is_last_col, NEXT_ROW); + // At the end, it must reach 0. let update_or_finish = select::expr( - not::expr(is_last.expr()), + not::expr(is_last.clone()), meta.query_advice(rwc_inc_left, NEXT_ROW), 0.expr(), ); - cb.require_equal( - "rwc_inc_left[2] == rwc_inc_left[0] - rwc_diff, or 0 at the end", - new_value, - update_or_finish, + + let update_or_finish_mcopy = meta.query_advice(rwc_inc_left, NEXT_STEP); + cb.condition(not::expr(is_memory_copy.clone()), |cb| { + cb.require_equal( + "rwc_inc_left[1] == rwc_inc_left[0] - rwc_diff, or 0 at the end", + new_value.clone(), + update_or_finish, + ); + }); + + // handle is_memory_copy case: for all read steps, `rwc_inc_left` decrease by 1 or 0, + // for all write steps, `rwc_inc_left` decrease by 1 or 0 as well. this is not the same as + // normal case( `rwc_inc_left` decrease by 1 or 0 for consecutive read steps--> write step + // --> read step -->write step ...). + cb.condition( + is_memory_copy * not::expr(is_last_two) * not::expr(is_last.clone()), + |cb| { + cb.require_equal( + "rwc_inc_left[2] == rwc_inc_left[0] - rwc_diff, or 0 at the end", + new_value, + update_or_finish_mcopy, + ); + }, ); // Maintain rw_counter based on rwc_inc_left. Their sum remains constant in all cases. @@ -525,6 +548,30 @@ pub fn constrain_rw_counter( }); } +/// validate `is_memory_copy` column is set correctly . +pub fn constrain_is_memory_copy( + cb: &mut BaseConstraintBuilder, + meta: &mut VirtualCells<'_, F>, + is_last_col: Column, + is_id_unchange: &IsEqualConfig, + is_memory: Column, + is_memory_copy: Expression, +) { + let is_memory_cur = meta.query_advice(is_memory, CURRENT); + let is_memory_next = meta.query_advice(is_memory, NEXT_ROW); + let is_last = meta.query_advice(is_last_col, CURRENT); + + // at any case, `is_memory_copy` is bool type. + cb.require_boolean("is_memory_copy is always bool", is_memory_copy.clone()); + cb.condition(not::expr(is_last.clone()), |cb| { + cb.require_equal( + "is_memory_copy == is_memory_cur * is_memory_next * is_id_unchange", + is_memory_copy.clone(), + is_memory_cur * is_memory_next * is_id_unchange.expr(), + ); + }); +} + /// Ensure the word operation completes for RW. pub fn constrain_rw_word_complete( cb: &mut BaseConstraintBuilder, diff --git a/zkevm-circuits/src/evm_circuit/execution/mcopy.rs b/zkevm-circuits/src/evm_circuit/execution/mcopy.rs index 5179d38b26..0d7e4079d2 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mcopy.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mcopy.rs @@ -177,7 +177,7 @@ impl ExecutionGadget for MCopyGadget { mod test { use crate::test_util::CircuitTestBuilder; use bus_mapping::circuit_input_builder::CircuitsParams; - use eth_types::{address, bytecode, Address, Bytecode, Word}; + use eth_types::{address, bytecode, word, Address, Bytecode, Word}; use mock::TestContext; use std::sync::LazyLock; @@ -187,8 +187,8 @@ mod test { fn test_ok(src_offset: Word, dest_offset: Word, length: usize) { let mut code = Bytecode::default(); code.append(&bytecode! { - // prepare memory values by mstore - PUSH10(0x6040ef28) + // prepare memory values(non zero values, zero value easily cause unpredictable fake pass) by mstore + PUSH32(word!("0x0102030405060708090a0b0c0d0e0f000102030405060708090a")) PUSH2(0x20) MSTORE PUSH32(length) @@ -245,7 +245,9 @@ mod test { test_ok(Word::from("0x40"), Word::from("0x40"), 0xE4); test_ok(Word::from("0x0"), Word::from("0x100"), 0x20); - // TODO: add src and dest overlap case later, test tool found that case failed. + // src and dest copy range overlap case, test tool found that case failed. + // this test can repro issue: "non-first access reads don't change value" + test_ok(Word::from("0x0"), Word::from("0x20"), 0x40); } // mcopy OOG cases added in ./execution/error_oog_memory_copy.rs diff --git a/zkevm-circuits/src/table.rs b/zkevm-circuits/src/table.rs index b4b246daf0..5d442071e1 100644 --- a/zkevm-circuits/src/table.rs +++ b/zkevm-circuits/src/table.rs @@ -1837,6 +1837,14 @@ impl CopyTable { let mut rw_counter = copy_event.rw_counter_start(); let mut rwc_inc_left = copy_event.rw_counter_delta(); + // for memory copy (mcopy) case, first half of ops are reading, the other half are + // writing parts, so for write ops, `rw_counter_write` starts from half too. + let mut rw_counter_write = rw_counter + rwc_inc_left / 2; + let mut rwc_inc_left_write = rwc_inc_left - rwc_inc_left / 2; + + let is_memory_copy = copy_event.src_id == copy_event.dst_id + && copy_event.src_type.eq(&CopyDataType::Memory) + && copy_event.dst_type.eq(&CopyDataType::Memory); let mut reader = CopyThread { tag: copy_event.src_type, @@ -1963,6 +1971,14 @@ impl CopyTable { F::from(thread.addr) }; + // rw_counter value in `rw_counter` copytable column. + let (rw_counter_in_column, rwc_inc_left_in_column) = if is_memory_copy && !is_read_step + { + (rw_counter_write, rwc_inc_left_write) + } else { + (rw_counter, rwc_inc_left) + }; + assignments.push(( thread.tag, [ @@ -1972,8 +1988,11 @@ impl CopyTable { (Value::known(F::from(thread.addr_end)), "src_addr_end"), (Value::known(F::from(thread.bytes_left)), "real_bytes_left"), (rlc_acc, "rlc_acc"), - (Value::known(F::from(rw_counter)), "rw_counter"), - (Value::known(F::from(rwc_inc_left)), "rwc_inc_left"), + (Value::known(F::from(rw_counter_in_column)), "rw_counter"), + ( + Value::known(F::from(rwc_inc_left_in_column)), + "rwc_inc_left", + ), ], [ (Value::known(F::from(is_last)), "is_last"), @@ -2001,8 +2020,14 @@ impl CopyTable { let is_row_end = is_access_list || (step_idx / 2) % 32 == 31; // Update the RW counter. if is_row_end && thread.is_rw { - rw_counter += 1; - rwc_inc_left -= 1; + // if write step in memory_copy case, and update rw_counter_write + if is_memory_copy && !is_read_step { + rw_counter_write += 1; + rwc_inc_left_write -= 1; + } else { + rw_counter += 1; + rwc_inc_left -= 1; + } } } assignments