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

Copy: fix conditions #616

Merged
merged 4 commits into from
Jul 12, 2023
Merged

Copy: fix conditions #616

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
69fbc92
memory_opt_counters: replace incorrect non_pad_non_mask with is_continue
Jul 11, 2023
a6e299e
memory_opt_counters: constraints on front_mask
Jul 12, 2023
de86658
Merge branch 'memory_opt' into memory_opt_continue
DreamWuGit Jul 12, 2023
2d1cfe2
memory_opt_continue: remove redundant conditation
Jul 12, 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
155 changes: 86 additions & 69 deletions zkevm-circuits/src/copy_circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,8 @@ pub struct CopyCircuitConfig<F> {
/// In case of a bytecode tag, this denotes whether or not the copied byte
/// is an opcode or push data byte.
pub is_code: Column<Advice>,
/// Whether this row is part of an event (versus filler rows).
pub is_event: Column<Advice>,
/// Indicates whether or not the copy event copies bytes to a precompiled call or copies bytes
/// from a precompiled call back to caller.
pub is_precompiled: Column<Advice>,
Expand Down Expand Up @@ -152,7 +154,8 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {

let value_acc = meta.advice_column_in(SecondPhase);
let is_code = meta.advice_column();
let (is_precompiled, is_tx_calldata, is_bytecode, is_memory, is_tx_log) = (
let (is_event, is_precompiled, is_tx_calldata, is_bytecode, is_memory, is_tx_log) = (
meta.advice_column(),
meta.advice_column(),
meta.advice_column(),
meta.advice_column(),
Expand Down Expand Up @@ -204,8 +207,10 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
},
|_meta| 1.expr(),
);

meta.create_gate("decode tag", |meta| {
let enabled = meta.query_fixed(q_enable, Rotation::cur());
let is_event = meta.query_advice(is_event, Rotation::cur());
let is_precompile = meta.query_advice(is_precompiled, Rotation::cur());
let is_tx_calldata = meta.query_advice(is_tx_calldata, Rotation::cur());
let is_bytecode = meta.query_advice(is_bytecode, Rotation::cur());
Expand Down Expand Up @@ -250,6 +255,15 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
)(meta),
]);
vec![
// If a row is not enabled (fixed), it is not in an event.
// TODO: not currently possible due to API limitations.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

what does API limitations mean ?

Copy link
Author

@naure naure Jul 12, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The Halo2 library has the concept of blinding rows, and it checks that no constraints are enabled on blinding rows. However, that is incorrect in our case and that is a soundness bug. To fix separately.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

for blinding rows , q_enable will be false such that constraint not checking on those rows. why think it is a problem ?

Copy link
Author

@naure naure Jul 12, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because then nothing is checked and the blinding rows could contain an incorrect event or a part of it.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

blinding rows filled with random data, essentially no need to constrain it. it is not specific with copy circuit. all other circuit can have blinding rows with any data.

// (1.expr() - enabled.expr()) * is_event.expr(),

// If a row is anything but padding (filler of the table), it is in an event.
enabled.expr()
* ((1.expr() - is_event.expr())
- tag.value_equals(CopyDataType::Padding, Rotation::cur())(meta)),
// Match boolean indicators to their respective tag values.
enabled.expr() * (is_precompile - precompiles),
enabled.expr()
* (is_tx_calldata
Expand All @@ -276,7 +290,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
meta.query_advice(is_last, Rotation::cur()),
);
cb.require_boolean("mask is boolean", meta.query_advice(mask, Rotation::cur()));
cb.require_boolean("front_mask is boolean", meta.query_advice(front_mask, Rotation::cur()));
cb.require_zero(
"is_first == 0 when q_step == 0",
and::expr([
Expand All @@ -292,15 +305,26 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
]),
);

// Whether this row is part of an event.
let is_event = meta.query_advice(is_event, Rotation::cur());

// 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()
- 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());

cb.condition(
and::expr([
is_continue.expr(),
is_word_continue.is_lt(meta, None),
not_last_two_rows.expr(),
non_pad_non_mask.is_lt(meta, None),
]),
|cb| {
cb.require_equal(
Expand All @@ -313,9 +337,8 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {

cb.condition(
and::expr([
is_continue.expr(),
not::expr(is_word_continue.is_lt(meta, None)),
not_last_two_rows.expr(),
non_pad_non_mask.is_lt(meta, None),
]),
|cb| {
cb.require_equal(
Expand All @@ -331,12 +354,9 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
},
);

// for all cases, rw_counter + rwc_inc_left keeps same
// for all cases, rw_counter + rwc_inc_left stays the same
cb.condition(
and::expr([
not::expr(meta.query_advice(is_last, Rotation::cur())),
non_pad_non_mask.is_lt(meta, None),
]),
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",
Expand All @@ -350,7 +370,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
and::expr([
is_word_continue.is_lt(meta, None),
not_last_two_rows.expr(),
non_pad_non_mask.is_lt(meta, None),
]),
|cb| {
let is_memory2memory = and::expr([
Expand All @@ -372,13 +391,10 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
// for all cases, rw_counter increase by 1 on word end for write step
cb.condition(
and::expr([
// exclude tx_calldata --> bytecode, which doesn't affect rw counter
not::expr(meta.query_advice(is_tx_calldata, Rotation::cur()) +
meta.query_advice(is_bytecode, Rotation::cur())),
not::expr(is_word_continue.is_lt(meta, None)),
not::expr(meta.query_advice(is_last, Rotation::cur())),
not::expr(meta.query_selector(q_step)),
non_pad_non_mask.is_lt(meta, None)
not::expr(meta.query_selector(q_step)), // TODO: rm
is_word.expr(),
]),
|cb| {
cb.require_equal(
Expand All @@ -389,23 +405,43 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
}
);

// The address is incremented by 1, except in the front mask because the row address has not caught up with the address of the event yet.
cb.condition(not_last_two_rows.expr(),
|cb| {
let front_mask_next = meta.query_advice(front_mask, Rotation(2));
let front_mask = meta.query_advice(front_mask, Rotation::cur());
cb.require_boolean("front_mask is boolean", front_mask.expr());

cb.require_zero("front_mask=1 implies mask=1",
and::expr([
front_mask.expr(),
not::expr(meta.query_advice(mask, Rotation::cur())),
]),
);

cb.condition(not::expr(is_word_continue.is_lt(meta, None)), |cb| {
// The first 31 bytes may be front_mask, but at least the 32nd byte is not masked.
cb.require_zero("front_mask = 0 by the end of the first word", front_mask.expr());
});

cb.condition(is_continue.expr(),
|cb| {

let addr_diff = not::expr(meta.query_advice(front_mask, Rotation::cur()));
cb.require_boolean("front_mask can go from 1 to 0", front_mask.expr() - front_mask_next);

// The address is incremented by 1, except in the front mask because the row address has not caught up with the address of the event yet.
let addr_diff = not::expr(front_mask.expr());
cb.require_equal(
"rows[0].addr + 1 == rows[2].addr",
"rows[0].addr + !front_mask == rows[2].addr",
meta.query_advice(addr, Rotation::cur()) + addr_diff,
meta.query_advice(addr, Rotation(2)),
);
},
);

cb.condition(
not_last_two_rows.expr() * non_pad_non_mask.is_lt(meta, None),
|cb| {
// The byte count including mask always decrements.
cb.require_equal(
"bytes_left == bytes_left_next + 1 for non-last step",
meta.query_advice(bytes_left, Rotation::cur()),
meta.query_advice(bytes_left, Rotation(2)) + 1.expr(),
);

// Forward other fields to the next step.
cb.require_equal(
"rows[0].id == rows[2].id",
meta.query_advice(id, Rotation::cur()),
Expand All @@ -416,7 +452,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
tag.value(Rotation::cur())(meta),
tag.value(Rotation(2))(meta),
);

cb.require_equal(
"rows[0].src_addr_end == rows[2].src_addr_end for non-last step",
meta.query_advice(src_addr_end, Rotation::cur()),
Expand Down Expand Up @@ -562,10 +597,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
);

cb.condition(
and::expr([
not::expr(meta.query_advice(is_last, Rotation::cur())),
not::expr(meta.query_advice(is_last, Rotation::next())),
]),
not::expr(meta.query_advice(is_last, Rotation::next())),
|cb| {
cb.require_equal(
"real_bytes_left[0] == real_bytes_left[2] + !mask",
Expand All @@ -580,33 +612,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
);
},
);
cb.condition(
not::expr(meta.query_advice(is_last, Rotation::next()))
* (non_pad_non_mask.is_lt(meta, None)),
|cb| {
cb.require_equal(
"bytes_left == bytes_left_next + 1 for non-last step",
meta.query_advice(bytes_left, Rotation::cur()),
meta.query_advice(bytes_left, Rotation(2)) + 1.expr(),
);
},
);
// we use rlc to constraint the write == read specially for memory to memory case
// here only handle non memory to memory nor to log cases
// cb.condition(
// not::expr(and::expr([
// meta.query_advice(is_memory, Rotation::cur()),
// meta.query_advice(is_memory, Rotation::next())
// + meta.query_advice(is_tx_log, Rotation::next()),
// ])),
// |cb| {
// cb.require_equal(
// "write value == read value",
// meta.query_advice(value, Rotation::cur()),
// meta.query_advice(value, Rotation::next()),
// );
// },
// );

cb.require_equal(
"value_acc is same for read-write rows",
Expand Down Expand Up @@ -761,6 +766,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
value_acc,
is_pad,
is_code,
is_event,
is_precompiled,
is_tx_calldata,
is_bytecode,
Expand Down Expand Up @@ -812,16 +818,12 @@ impl<F: Field> CopyCircuitConfig<F> {
.iter()
.zip_eq(table_row)
{
// Leave sr_addr_end and bytes_left unassigned when !is_read
if !is_read && (label == "src_addr_end" || label == "bytes_left") {
} else {
region.assign_advice(
|| format!("{label} at row: {offset}"),
column,
*offset,
|| value,
)?;
}
region.assign_advice(
|| format!("{label} at row: {offset}"),
column,
*offset,
|| value,
)?;
}

// q_step
Expand All @@ -835,6 +837,13 @@ impl<F: Field> CopyCircuitConfig<F> {
*offset,
|| Value::known(F::one()),
)?;
// is_event = true
region.assign_advice(
|| format!("is_event at row: {}", *offset),
self.is_event,
*offset,
|| Value::known(F::one()),
)?;

// is_last, value, is_pad, is_code
for (column, &(value, label)) in [
Expand Down Expand Up @@ -965,6 +974,7 @@ impl<F: Field> CopyCircuitConfig<F> {
region.name_column(|| "front_mask", self.front_mask);
region.name_column(|| "is_code", self.is_code);
region.name_column(|| "is_pad", self.is_pad);
region.name_column(|| "is_event", self.is_event);

let mut offset = 0;
for (ev_idx, copy_event) in copy_events.iter().enumerate() {
Expand Down Expand Up @@ -1053,6 +1063,13 @@ impl<F: Field> CopyCircuitConfig<F> {
}
}

// is_event = false
region.assign_advice(
|| format!("is_event at row: {}", *offset),
self.is_event,
*offset,
|| Value::known(F::zero()),
)?;
// is_first
region.assign_advice(
|| format!("assign is_first {}", *offset),
Expand Down
21 changes: 12 additions & 9 deletions zkevm-circuits/src/table.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1536,13 +1536,14 @@ impl CopyTable {
let mut rlc_acc_read = Value::known(F::zero());
let mut rlc_acc_write = Value::known(F::zero());

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

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

let read_steps = copy_event.copy_bytes.bytes.iter();
let copy_steps = if let Some(ref write_steps) = copy_event.copy_bytes.aux_bytes {
Expand Down Expand Up @@ -1598,7 +1599,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 == copy_event.copy_bytes.bytes.len() * 2 - 1 {
let is_last = if step_idx == full_length * 2 - 1 {
Value::known(F::one())
} else {
Value::known(F::zero())
Expand Down Expand Up @@ -1653,12 +1654,11 @@ impl CopyTable {
};

// bytes_left (final padding word length )
let bytes_left =
u64::try_from(copy_event.copy_bytes.bytes.len() * 2 - step_idx).unwrap() / 2;
let bytes_left = u64::try_from(full_length * 2 - step_idx).unwrap() / 2;
// value
let value = Value::known(F::from(copy_step.value as u64));

word_index = (step_idx as u64 / 2) % 32;
let word_index = (step_idx as u64 / 2) % 32;

// value_acc
if is_read_step && !copy_step.mask {
Expand All @@ -1681,16 +1681,19 @@ impl CopyTable {
F::from(addr)
};

let addr_end = if is_read_step {
copy_event.src_addr_end
} else {
copy_event.dst_addr + full_length as u64
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This won’t be verified but here only for regularity.

};

assignments.push((
tag,
[
(is_first, "is_first"),
(id, "id"),
(Value::known(addr), "addr"),
(
Value::known(F::from(copy_event.src_addr_end)),
"src_addr_end",
),
(Value::known(F::from(addr_end)), "src_addr_end"),
(Value::known(F::from(bytes_left)), "bytes_left"),
(
Value::known(F::from(real_length_left as u64)),
Expand Down