Skip to content
This repository was archived by the owner on Apr 18, 2025. It is now read-only.

memory_opt_rwc: fix and simplify RW counter logic #631

Merged
merged 2 commits into from
Jul 13, 2023
Merged

memory_opt_rwc: fix and simplify RW counter logic #631

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6c55b2b
memory_opt_rwc: fix and simplify RW counter logic
Jul 13, 2023
6ebdfed
memory_opt_rwc: simplify CopyEvent rw functions
Jul 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
74 changes: 19 additions & 55 deletions bus-mapping/src/circuit_input_builder/execution.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -415,70 +415,34 @@ pub type CopyEventSteps = Vec<(u8, bool, bool)>;
pub type CopyEventPrevBytes = Vec<u8>;

impl CopyEvent {
/// rw counter at step index
pub fn rw_counter(&self, step_index: usize) -> u64 {
u64::try_from(self.rw_counter_start.0).unwrap() + self.rw_counter_increase(step_index)
}

/// rw counter at step index
pub fn rw_counter_step(&self, step_index: usize) -> u64 {
let mut rw_counter = u64::try_from(self.rw_counter_start.0).unwrap();
let rw_counter_increase = self.rw_counter_increase(step_index);
rw_counter += rw_counter_increase;

// step_index == self.bytes.len() when caculate total rw increasing.
if self.dst_type == CopyDataType::TxLog
&& step_index != self.copy_bytes.bytes.len() * 2
&& step_index % 64 == 63
{
// log writing
rw_counter += 1;
}

rw_counter
/// The full length of the event, including masked segments.
pub fn full_length(&self) -> u64 {
self.copy_bytes.bytes.len() as u64
}

/// rw counter increase left at step index
pub fn rw_counter_increase_left(&self, step_index: usize) -> u64 {
if self.rw_counter_step(self.copy_bytes.bytes.len() * 2) < self.rw_counter_step(step_index)
{
panic!("prev rw_counter_step > total tw_counter");
}
// self.rw_counter_step(self.bytes.len() * 2) - self.rw_counter_step(step_index)
self.rw_counter_step(self.copy_bytes.bytes.len() * 2) - self.rw_counter_step(step_index)
/// The length of the copied data, excluding masked segments.
pub fn copy_length(&self) -> u64 {
self.copy_bytes.bytes.iter().filter(|&step| !step.2).count() as u64
}

/// Number of rw operations performed by this copy event
pub fn rw_counter_delta(&self) -> u64 {
self.rw_counter_increase(self.copy_bytes.bytes.len() * 2)
/// Whether the source performs RW lookups in the state circuit.
pub fn is_source_rw(&self) -> bool {
self.src_type == CopyDataType::Memory
}

// increase in rw counter from the start of the copy event to step index
fn rw_counter_increase(&self, step_index: usize) -> u64 {
if let (CopyDataType::Memory, CopyDataType::Memory) = (self.src_type, self.dst_type) {
return step_index as u64 % 2 + 2 * (step_index as u64 / 64);
}
let source_rw_increase = match self.src_type {
CopyDataType::Bytecode | CopyDataType::TxCalldata | CopyDataType::Precompile(_) => 0,
CopyDataType::Memory => (step_index as u64 / 2) / 32,
CopyDataType::RlcAcc | CopyDataType::TxLog | CopyDataType::Padding => unreachable!(),
};
let destination_rw_increase = match self.dst_type {
CopyDataType::RlcAcc | CopyDataType::Bytecode | CopyDataType::Precompile(_) => 0,
CopyDataType::Memory => (step_index as u64 / 2) / 32,
CopyDataType::TxLog => u64::try_from(step_index).unwrap() / 2 / 32,
CopyDataType::TxCalldata | CopyDataType::Padding => unreachable!(),
};
/// Whether the destination performs RW lookups in the state circuit.
pub fn is_destination_rw(&self) -> bool {
self.dst_type == CopyDataType::Memory || self.dst_type == CopyDataType::TxLog
}

source_rw_increase + destination_rw_increase
/// The RW counter of the first RW lookup performed by this copy event.
pub fn rw_counter_start(&self) -> u64 {
usize::from(self.rw_counter_start) as u64
}

// increase in rw counter for tx log specially
fn rw_counter_increase_log(&self, step_index: usize) -> u64 {
match self.dst_type {
CopyDataType::TxLog => u64::try_from(step_index).unwrap() / 2,
_ => unreachable!(),
}
/// The number of RW lookups performed by this copy event.
pub fn rw_counter_delta(&self) -> u64 {
(self.is_source_rw() as u64 + self.is_destination_rw() as u64) * (self.full_length() / 32)
}
}

Expand Down
99 changes: 34 additions & 65 deletions zkevm-circuits/src/copy_circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -321,16 +321,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
- meta.query_advice(is_last, Rotation::cur())
- meta.query_advice(is_last, Rotation::next());

// Whether this row is not the last step, or not part of an event at all.
let not_last_two_rows = 1.expr()
- meta.query_advice(is_last, Rotation::cur())
- meta.query_advice(is_last, Rotation::next());

// Whether this row is part of a memory or log word.
let is_word = meta.query_advice(is_memory, Rotation::cur()) + meta.query_advice(is_tx_log, Rotation::cur());

let is_word_end = is_word_end.is_equal_expression.expr();
let not_word_end = not::expr(is_word_end.expr());

// Apply the same constraints for the RLCs of words before and after the write.
let word_rlc_both = [
Expand Down Expand Up @@ -397,57 +388,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
},
);

// for all cases, rw_counter + rwc_inc_left stays the same
cb.condition(
not::expr(meta.query_advice(is_last, Rotation::cur())),
|cb| {
cb.require_equal(
"rows[0].rw_counter + rows[0].rwc_inc_left == rows[1].rw_counter + rows[1].rwc_inc_left",
meta.query_advice(rw_counter, Rotation::cur()) + meta.query_advice(rwc_inc_left, Rotation::cur()),
meta.query_advice(rw_counter, Rotation::next()) + meta.query_advice(rwc_inc_left, Rotation::next()),
);
}
);
// for all cases, rows[0].rw_counter + diff == rows[1].rw_counter
cb.condition(
and::expr([
not_word_end.expr(),
not_last_two_rows.expr(),
]),
|cb| {
let is_memory2memory = and::expr([
meta.query_advice(is_memory, Rotation::cur()),
meta.query_advice(is_memory, Rotation::next()),
]);
let diff = select::expr(
is_memory2memory,
select::expr(meta.query_selector(q_step), 1.expr(), -(1.expr())),
0.expr(),
);
cb.require_equal(
"rows[0].rw_counter + diff == rows[1].rw_counter",
meta.query_advice(rw_counter, Rotation::cur()) + diff.expr(),
meta.query_advice(rw_counter, Rotation::next()),
);
}
);
// for all cases, rw_counter increase by 1 on word end for write step
cb.condition(
and::expr([
is_word_end.expr(),
not::expr(meta.query_advice(is_last, Rotation::cur())),
not::expr(meta.query_selector(q_step)), // TODO: rm
is_word.expr(),
]),
|cb| {
cb.require_equal(
"rows[0].rw_counter + 1 == rows[1].rw_counter",
meta.query_advice(rw_counter, Rotation::cur()) + 1.expr(),
meta.query_advice(rw_counter, Rotation::next()),
);
}
);

// Split the mask into front and back segments.
// If front_mask=1, then mask=1 and back_mask=0.
// If back_mask=1, then mask=1 and front_mask=0.
Expand Down Expand Up @@ -490,17 +430,46 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
);*/
});

// Decrement the real_bytes_left on non-masked rows. At the end, it must reach 0.
// Decrement real_bytes_left for the next step, on non-masked rows. At the end, it must reach 0.
{
let real_bytes_left_next = meta.query_advice(real_bytes_left, Rotation::cur()) - not::expr(mask.expr());
let next_or_finish = select::expr(is_continue.expr(), meta.query_advice(real_bytes_left, Rotation(2)), 0.expr());
let next_value = meta.query_advice(real_bytes_left, Rotation::cur()) - not::expr(mask.expr());
let update_or_finish = select::expr(is_continue.expr(), meta.query_advice(real_bytes_left, Rotation(2)), 0.expr());
cb.require_equal(
"real_bytes_left[2] == real_bytes_left[0] - !mask, or 0 at the end",
real_bytes_left_next,
next_or_finish,
next_value,
update_or_finish,
);
}

// Decrement rwc_inc_left for the next row, when an RW operation happens. At the end, it must reach 0.
{
let is_rw_type = meta.query_advice(is_memory, Rotation::cur()) + meta.query_advice(is_tx_log, Rotation::cur());
let rwc_diff = is_rw_type * 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()),
0.expr(),
meta.query_advice(rwc_inc_left, Rotation::next()),
);
cb.require_equal(
"rwc_inc_left[2] == rwc_inc_left[0] - rwc_diff, or 0 at the end",
next_value,
update_or_finish,
);
}

// 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())),
|cb| {
cb.require_equal(
"rows[0].rw_counter + rows[0].rwc_inc_left == rows[1].rw_counter + rows[1].rwc_inc_left",
meta.query_advice(rw_counter, Rotation::cur()) + meta.query_advice(rwc_inc_left, Rotation::cur()),
meta.query_advice(rw_counter, Rotation::next()) + meta.query_advice(rwc_inc_left, Rotation::next()),
);
}
);

// Derive the next step from the current step.
cb.condition(is_continue.expr(),
|cb| {
Expand Down
43 changes: 21 additions & 22 deletions zkevm-circuits/src/table.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1529,16 +1529,6 @@ impl CopyTable {
let mut src_value_acc = Value::known(F::zero());
let mut dst_value_acc = Value::known(F::zero());

let full_length = copy_event.copy_bytes.bytes.len();

let mut src_bytes_left = copy_event
.copy_bytes
.bytes
.iter()
.filter(|&step| !step.2)
.count();
let mut dst_bytes_left = src_bytes_left;

let read_steps = copy_event.copy_bytes.bytes.iter();
let copy_steps = if let Some(ref write_steps) = copy_event.copy_bytes.aux_bytes {
read_steps.zip(write_steps.iter())
Expand All @@ -1552,12 +1542,18 @@ impl CopyTable {
.clone()
.unwrap_or(vec![]);

let mut src_bytes_left = copy_event.copy_length();
let mut dst_bytes_left = src_bytes_left;

let mut src_addr = copy_event.src_addr;
let mut dst_addr = copy_event.dst_addr;

let mut src_front_mask = true;
let mut dst_front_mask = true;

let mut rw_counter = copy_event.rw_counter_start();
let mut rwc_inc_left = copy_event.rw_counter_delta();

for (step_idx, (is_read_step, mut copy_step)) in copy_steps
.flat_map(|(read_step, write_step)| {
let read_step = CopyStep {
Expand Down Expand Up @@ -1594,7 +1590,7 @@ impl CopyTable {
// is_first
let is_first = Value::known(if step_idx == 0 { F::one() } else { F::zero() });
// is last
let is_last = if step_idx == full_length * 2 - 1 {
let is_last = if step_idx as u64 == copy_event.full_length() * 2 - 1 {
Value::known(F::one())
} else {
Value::known(F::zero())
Expand Down Expand Up @@ -1669,7 +1665,7 @@ impl CopyTable {
let addr_end = if is_read_step {
copy_event.src_addr_end
} else {
copy_event.dst_addr + full_length as u64
copy_event.dst_addr + copy_event.full_length()
};

assignments.push((
Expand All @@ -1684,7 +1680,7 @@ impl CopyTable {
src_bytes_left
} else {
dst_bytes_left
} as u64)),
})),
"real_bytes_left",
),
(
Expand All @@ -1698,14 +1694,8 @@ impl CopyTable {
},
"rlc_acc",
),
(
Value::known(F::from(copy_event.rw_counter_step(step_idx))),
"rw_counter",
),
(
Value::known(F::from(copy_event.rw_counter_increase_left(step_idx))),
"rwc_inc_left",
),
(Value::known(F::from(rw_counter)), "rw_counter"),
(Value::known(F::from(rwc_inc_left)), "rwc_inc_left"),
],
[
(is_last, "is_last"),
Expand Down Expand Up @@ -1757,13 +1747,22 @@ impl CopyTable {
if !is_read_step && !dst_front_mask {
dst_addr += 1;
}

// Decrement the number of steps left.
if is_read_step && !copy_step.mask {
src_bytes_left -= 1;
}
if !is_read_step && !copy_step.mask {
dst_bytes_left -= 1;
}
// Update the RW counter.
let is_word_end = (step_idx / 2) % 32 == 31;
if is_word_end
&& (is_read_step && copy_event.is_source_rw()
|| !is_read_step && copy_event.is_destination_rw())
{
rw_counter += 1;
rwc_inc_left -= 1;
}
}
assignments
}
Expand Down