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

memory_opt_length: constrain length and mask #628

Merged
merged 2 commits into from
Jul 13, 2023
Merged

memory_opt_length: constrain length and mask #628

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
7c917ff
memory_opt_length: track both source and destination lengths. Simplif…
Jul 12, 2023
7c80c99
memory_opt_length: constrain the shape of the mask
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
114 changes: 52 additions & 62 deletions zkevm-circuits/src/copy_circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
let id = copy_table.id;
let addr = copy_table.addr;
let src_addr_end = copy_table.src_addr_end;
let bytes_left = copy_table.bytes_left;
let real_bytes_left = copy_table.real_bytes_left;
let word_index = meta.advice_column();
let mask = meta.advice_column();
Expand Down Expand Up @@ -280,7 +279,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
"is_last is boolean",
meta.query_advice(is_last, Rotation::cur()),
);
cb.require_boolean("mask is boolean", meta.query_advice(mask, Rotation::cur()));
cb.require_zero(
"is_first == 0 when q_step == 0",
and::expr([
Expand Down Expand Up @@ -347,6 +345,9 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
for rot in [Rotation::cur(), Rotation::next()] {
cb.require_zero("word_index starts at 0", meta.query_advice(word_index, rot));

let back_mask = meta.query_advice(mask, rot) - meta.query_advice(front_mask, rot);
cb.require_zero("back_mask starts at 0", back_mask);

cb.require_equal(
"value_acc init to the first value, or 0 if padded or masked",
meta.query_advice(value_acc, rot),
Expand All @@ -367,12 +368,12 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
cb.condition(is_continue.expr(),
|cb| {

// Update the index into the current or next word.
let inc_or_reset = select::expr(
is_word_end.expr(),
0.expr(),
meta.query_advice(word_index, Rotation::cur()) + 1.expr(),
);

cb.require_equal(
"word_index increments or resets to 0",
inc_or_reset,
Expand Down Expand Up @@ -447,43 +448,72 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
}
);

// 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.
// Otherwise, mask=0.
let mask_next = meta.query_advice(mask, Rotation(2));
let mask = meta.query_advice(mask, Rotation::cur());
let front_mask_next = meta.query_advice(front_mask, Rotation(2));
let front_mask = meta.query_advice(front_mask, Rotation::cur());
let back_mask_next = mask_next.expr() - front_mask_next.expr();
let back_mask = mask.expr() - front_mask.expr();
cb.require_boolean("mask is boolean", mask.expr());
cb.require_boolean("front_mask is boolean", front_mask.expr());
cb.require_boolean("back_mask is boolean", back_mask.expr());

cb.require_zero("front_mask=1 implies mask=1",
and::expr([
front_mask.expr(),
not::expr(meta.query_advice(mask, Rotation::cur())),
]),
);
// The front mask comes before the back mask, with at least 1 non-masked byte in-between.
cb.condition(is_continue.expr(),
|cb| {
cb.require_boolean("front_mask cannot go from 0 back to 1", front_mask.expr() - front_mask_next);
cb.require_boolean("back_mask cannot go from 1 back to 0", back_mask_next.expr() - back_mask);
cb.require_zero("front_mask is not immediately followed by back_mask",
and::expr([
front_mask.expr(),
back_mask_next.expr(),
]),
);
});

// The first word must not be completely masked.
cb.condition(is_word_end.expr(), |cb| {
// The first 31 bytes may be front_mask, but at least the 32nd byte is not masked.
// The first 31 bytes may be front_mask, but not the last byte of the first word.
cb.require_zero("front_mask = 0 by the end of the first word", front_mask.expr());

/* Note: other words may be completely masked, because reader and writer may have different word counts. A fully masked word is a no-op, not contributing to value_acc, and its word_rlc equals word_rlc_prev.
cb.require_zero(
"back_mask=0 at the start of the next word",
and::expr([
is_continue.expr(),
back_mask_next.expr(),
]),
);*/
});

// Decrement the real_bytes_left 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());
cb.require_equal(
"real_bytes_left[2] == real_bytes_left[0] - !mask, or 0 at the end",
real_bytes_left_next,
next_or_finish,
);
}

// Derive the next step from the current step.
cb.condition(is_continue.expr(),
|cb| {

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.
// The address is incremented by 1, except in the front mask. There must be the right amount
// of front mask until the row matches up with the initial address of the event.
let addr_diff = not::expr(front_mask.expr());
cb.require_equal(
"rows[0].addr + !front_mask == rows[2].addr",
meta.query_advice(addr, Rotation::cur()) + addr_diff,
meta.query_advice(addr, Rotation(2)),
);

// 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",
Expand All @@ -508,8 +538,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
let value_or_pad = meta.query_advice(value, Rotation(2)) * not::expr(meta.query_advice(is_pad, Rotation(2)));
let accumulated = current.expr() * challenges.keccak_input() + value_or_pad;
// If masked, copy the accumulator forward, otherwise update it.
let mask = meta.query_advice(mask, Rotation(2));
let copy_or_acc = select::expr(mask, current, accumulated);
let copy_or_acc = select::expr(mask_next, current, accumulated);
cb.require_equal(
"value_acc(2) == value_acc(0) * r + value(2), or copy value_acc(0)",
copy_or_acc,
Expand All @@ -534,7 +563,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
cb.gate(meta.query_fixed(q_enable, Rotation::cur()))
});

meta.create_gate("Last Step, check rlc_acc", |meta| {
meta.create_gate("Last Step", |meta| {
let mut cb = BaseConstraintBuilder::default();

cb.require_equal(
Expand Down Expand Up @@ -579,38 +608,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
meta.create_gate("verify step (q_step == 1)", |meta| {
let mut cb = BaseConstraintBuilder::default();

cb.require_zero(
"bytes_left == 1 for last step",
and::expr([
meta.query_advice(is_last, Rotation::next()),
1.expr() - meta.query_advice(bytes_left, Rotation::cur()),
]),
);
cb.require_zero(
"real_bytes_left == 0 for last step",
and::expr([
meta.query_advice(is_last, Rotation::next()),
meta.query_advice(real_bytes_left, Rotation::next()),
]),
);

cb.condition(
not::expr(meta.query_advice(is_last, Rotation::next())),
|cb| {
cb.require_equal(
"real_bytes_left[0] == real_bytes_left[2] + !mask",
meta.query_advice(real_bytes_left, Rotation::cur()),
meta.query_advice(real_bytes_left, Rotation(2))
+ not::expr(meta.query_advice(mask, Rotation::cur())),
);
cb.require_equal(
"real_bytes_left[1] == real_bytes_left[2]",
meta.query_advice(real_bytes_left, Rotation::next()),
meta.query_advice(real_bytes_left, Rotation(2)),
);
},
);

cb.require_equal(
"is_pad == 1 - (src_addr < src_addr_end) for read row",
1.expr() - addr_lt_addr_end.is_lt(meta, None),
Expand Down Expand Up @@ -1066,13 +1063,6 @@ impl<F: Field> CopyCircuitConfig<F> {
*offset,
|| Value::known(F::one()),
)?;
// bytes_left
region.assign_advice(
|| format!("assign bytes_left {}", *offset),
self.copy_table.bytes_left,
*offset,
|| Value::known(F::zero()),
)?;
// real_bytes_left
region.assign_advice(
|| format!("assign bytes_left {}", *offset),
Expand Down
38 changes: 17 additions & 21 deletions zkevm-circuits/src/table.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1459,12 +1459,10 @@ pub struct CopyTable {
/// The end of the source buffer for the copy event. Any data read from an
/// address greater than or equal to this value will be 0.
pub src_addr_end: Column<Advice>,
/// The number of bytes left to be copied.
pub bytes_left: Column<Advice>,
/// The number of non-masked bytes left to be copied.
pub real_bytes_left: Column<Advice>,
/// mask indicates the byte is actual coped or padding to memory word
pub value_wrod_rlc: Column<Advice>,
pub value_wrod_rlc: Column<Advice>, // TODO: rm
/// mask indicates the byte is actual coped or padding to memory word
//pub mask: Column<Advice>,
/// An accumulator value in the RLC representation. This is used for
Expand All @@ -1482,7 +1480,7 @@ pub struct CopyTable {
pub tag: BinaryNumberConfig<CopyDataType, 4>,
}

type CopyTableRow<F> = [(Value<F>, &'static str); 9];
type CopyTableRow<F> = [(Value<F>, &'static str); 8];
type CopyCircuitRow<F> = [(Value<F>, &'static str); 11];

impl CopyTable {
Expand All @@ -1495,10 +1493,8 @@ impl CopyTable {
tag: BinaryNumberChip::configure(meta, q_enable, None),
addr: meta.advice_column(),
src_addr_end: meta.advice_column(),
bytes_left: meta.advice_column(),
real_bytes_left: meta.advice_column(),
value_wrod_rlc: meta.advice_column(),
//mask: meta.advice_column(),
value_wrod_rlc: meta.advice_column(), // TODO: rm
rlc_acc: meta.advice_column_in(SecondPhase),
rw_counter: meta.advice_column(),
rwc_inc_left: meta.advice_column(),
Expand Down Expand Up @@ -1535,12 +1531,13 @@ impl CopyTable {

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

let mut real_length_left = copy_event
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 {
Expand Down Expand Up @@ -1655,9 +1652,6 @@ impl CopyTable {
copy_event.dst_type
};

// bytes_left (final padding word length )
let bytes_left = u64::try_from(full_length * 2 - step_idx).unwrap() / 2;

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

// is_code
Expand Down Expand Up @@ -1685,9 +1679,12 @@ impl CopyTable {
(id, "id"),
(Value::known(addr), "addr"),
(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)),
Value::known(F::from(if is_read_step {
src_bytes_left
} else {
dst_bytes_left
} as u64)),
"real_bytes_left",
),
(
Expand Down Expand Up @@ -1762,7 +1759,10 @@ impl CopyTable {
}

if is_read_step && !copy_step.mask {
real_length_left -= 1;
src_bytes_left -= 1;
}
if !is_read_step && !copy_step.mask {
dst_bytes_left -= 1;
}
}
assignments
Expand Down Expand Up @@ -1832,9 +1832,7 @@ impl<F: Field> LookupTable<F> for CopyTable {
self.id.into(),
self.addr.into(),
self.src_addr_end.into(),
self.bytes_left.into(),
self.real_bytes_left.into(),
//self.value_wrod_rlc.into(),
self.rlc_acc.into(),
self.rw_counter.into(),
self.rwc_inc_left.into(),
Expand All @@ -1848,7 +1846,6 @@ impl<F: Field> LookupTable<F> for CopyTable {
String::from("id"),
String::from("addr"),
String::from("src_addr_end"),
String::from("bytes_left"),
String::from("real_bytes_left"),
String::from("rlc_acc"),
String::from("rw_counter"),
Expand All @@ -1867,11 +1864,10 @@ impl<F: Field> LookupTable<F> for CopyTable {
meta.query_advice(self.addr, Rotation::cur()), // src_addr
meta.query_advice(self.src_addr_end, Rotation::cur()), // src_addr_end
meta.query_advice(self.addr, Rotation::next()), // dst_addr
//meta.query_advice(self.bytes_left, Rotation::cur()), // length
meta.query_advice(self.real_bytes_left, Rotation::cur()), // real_length
meta.query_advice(self.rlc_acc, Rotation::cur()), // rlc_acc
meta.query_advice(self.rw_counter, Rotation::cur()), // rw_counter
meta.query_advice(self.rwc_inc_left, Rotation::cur()), // rwc_inc_left
meta.query_advice(self.rlc_acc, Rotation::cur()), // rlc_acc
meta.query_advice(self.rw_counter, Rotation::cur()), // rw_counter
meta.query_advice(self.rwc_inc_left, Rotation::cur()), // rwc_inc_left
]
}
}
Expand Down