Skip to content

Commit

Permalink
feat: copy circuit support overlap copy range (#1255)
Browse files Browse the repository at this point in the history 
* 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 <mycinbrin@gmail.com>
  • Loading branch information
@DreamWuGit @lispc
DreamWuGit and lispc authored May 13, 2024
1 parent 1cb76ea commit 85c773e
Show file tree
Hide file tree
Showing 6 changed files with 208 additions and 46 deletions.
14 changes: 10 additions & 4 deletions bus-mapping/src/circuit_input_builder/input_state_ref.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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<u8> = 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,
Expand All @@ -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,
Expand Down Expand Up @@ -2419,14 +2424,15 @@ fn combine_copy_slot_bytes(
copy_length: usize,
src_data: &[impl Into<u8> + 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<u8>) {
let mut src_range = MemoryWordRange::align_range(src_addr, copy_length);
let mut dst_range = MemoryWordRange::align_range(dst_addr, copy_length);
src_range.ensure_equal_length(&mut dst_range);

// 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 {
Expand Down
60 changes: 39 additions & 21 deletions bus-mapping/src/evm/opcodes/mcopy.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -222,30 +233,37 @@ mod mcopy_tests {
.collect::<Vec<(RW, MemoryOp)>>(),
(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],
),
),
)
}
Expand Down
78 changes: 71 additions & 7 deletions zkevm-circuits/src/copy_circuit.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand All @@ -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.
Expand Down Expand Up @@ -97,6 +99,8 @@ pub struct CopyCircuitConfig<F> {
pub is_bytecode: Column<Advice>,
/// Booleans to indicate what copy data type exists at the current row.
pub is_memory: Column<Advice>,
/// Booleans to indicate if mcopy data type exists at the current row.
pub is_memory_copy: Column<Advice>,
/// Booleans to indicate what copy data type exists at the current row.
pub is_tx_log: Column<Advice>,
/// Booleans to indicate if `CopyDataType::AccessListAddresses` exists at
Expand All @@ -110,6 +114,8 @@ pub struct CopyCircuitConfig<F> {
/// 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<F>,
/// 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).
Expand Down Expand Up @@ -167,7 +173,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
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;
Expand All @@ -189,6 +195,13 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
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),
Expand Down Expand Up @@ -345,16 +358,29 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
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);
}

Expand Down Expand Up @@ -566,11 +592,13 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
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,
Expand All @@ -589,6 +617,7 @@ impl<F: Field> CopyCircuitConfig<F> {
region: &mut Region<F>,
offset: &mut usize,
tag_chip: &BinaryNumberChip<F, CopyDataType, { CopyDataType::N_BITS }>,
is_id_unchange: &IsEqualChip<F>,
is_src_end_chip: &IsEqualChip<F>,
lt_word_end_chip: &IsEqualChip<F>,
challenges: Challenges<Value<F>>,
Expand Down Expand Up @@ -665,6 +694,20 @@ impl<F: Field> CopyCircuitConfig<F> {
)?;
}

let (id, id_next) = if is_read {
(&copy_event.src_id, &copy_event.dst_id)
} else {
(&copy_event.dst_id, &copy_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,
Expand Down Expand Up @@ -700,6 +743,16 @@ impl<F: Field> CopyCircuitConfig<F> {
*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,
Expand Down Expand Up @@ -750,6 +803,7 @@ impl<F: Field> CopyCircuitConfig<F> {
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());

Expand Down Expand Up @@ -785,20 +839,21 @@ impl<F: Field> CopyCircuitConfig<F> {
&mut region,
&mut offset,
&tag_chip,
&is_id_unchange,
&is_src_end_chip,
&lt_word_end_chip,
challenges,
copy_event,
)?;
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,
&lt_word_end_chip,
)?;
Expand All @@ -811,6 +866,7 @@ impl<F: Field> CopyCircuitConfig<F> {
&mut offset,
false,
&tag_chip,
&is_id_unchange,
&is_src_end_chip,
&lt_word_end_chip,
)?;
Expand All @@ -828,6 +884,7 @@ impl<F: Field> CopyCircuitConfig<F> {
offset: &mut usize,
enabled: bool,
tag_chip: &BinaryNumberChip<F, CopyDataType, { CopyDataType::N_BITS }>,
is_id_unchange_chip: &IsEqualChip<F>,
is_src_end_chip: &IsEqualChip<F>,
lt_word_end_chip: &IsEqualChip<F>,
) -> Result<(), Error> {
Expand Down Expand Up @@ -974,6 +1031,12 @@ impl<F: Field> CopyCircuitConfig<F> {
// 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,
Expand All @@ -997,6 +1060,7 @@ impl<F: Field> CopyCircuitConfig<F> {
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,
Expand Down
Loading

0 comments on commit 85c773e

Please sign in to comment.