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

memory_opt_word_end: replace broken LtChip with IsEqualChip #617

Merged
merged 9 commits into from
Jul 12, 2023
Merged

memory_opt_word_end: replace broken LtChip with IsEqualChip #617

Changes from all commits
Commits
Show all changes
9 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
57ef58e
memory_opt_word_end: replace broken LtChip with IsEqualChip
Jul 12, 2023
2d1cfe2
memory_opt_continue: remove redundant conditation
Jul 12, 2023
6cb09c1
Merge branch 'memory_opt_continue' into memory_opt_word_end
Jul 12, 2023
a0dab3a
Merge branch 'memory_opt' into memory_opt_word_end
Jul 12, 2023
2dfc24f
Merge branch 'memory_opt_continue' into memory_opt_word_end
naure Jul 12, 2023
bc739e7
Merge branch 'memory_opt_word_end' of github.com:scroll-tech/zkevm-ci…
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
57 changes: 37 additions & 20 deletions zkevm-circuits/src/copy_circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ use eth_types::{Field, Word};

use gadgets::{
binary_number::BinaryNumberChip,
is_equal::{IsEqualChip, IsEqualConfig, IsEqualInstruction},
less_than::{LtChip, LtConfig, LtInstruction},
util::{and, not, or, select, sum, Expr},
};
Expand Down Expand Up @@ -99,8 +100,8 @@ pub struct CopyCircuitConfig<F> {
/// Since `src_addr` and `src_addr_end` are u64, 8 bytes are sufficient for
/// the Lt chip.
pub addr_lt_addr_end: LtConfig<F, 8>,
/// Whether this row is a continuation of a word (not last byte).
pub is_word_continue: LtConfig<F, 1>,
/// Whether this is the end of a word (last byte).
pub is_word_end: IsEqualConfig<F>,
/// non pad and non mask gadget
pub non_pad_non_mask: LtConfig<F, 1>,
// External tables
Expand Down Expand Up @@ -191,9 +192,9 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
|meta| meta.query_advice(src_addr_end, Rotation::cur()),
);

let is_word_continue = LtChip::configure(
let is_word_end = IsEqualChip::configure(
meta,
|meta| meta.query_selector(q_step), // TODO: always enable.
|meta| meta.query_fixed(q_enable, Rotation::cur()),
|meta| meta.query_advice(word_index, Rotation::cur()),
|_meta| 31.expr(),
);
Expand Down Expand Up @@ -281,9 +282,10 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
meta.create_gate("verify row", |meta| {
let mut cb = BaseConstraintBuilder::default();

let is_first = meta.query_advice(is_first, Rotation::cur());
cb.require_boolean(
"is_first is boolean",
meta.query_advice(is_first, Rotation::cur()),
is_first.expr(),
);
cb.require_boolean(
"is_last is boolean",
Expand All @@ -294,7 +296,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
"is_first == 0 when q_step == 0",
and::expr([
not::expr(meta.query_selector(q_step)),
meta.query_advice(is_first, Rotation::cur()),
is_first.expr(),
]),
);
cb.require_zero(
Expand All @@ -321,10 +323,20 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
// 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());

cb.condition(is_first.expr(),
|cb| {
cb.require_zero("reader word_index starts at 0", meta.query_advice(word_index, Rotation::cur()));
cb.require_zero("writer word_index starts at 0", meta.query_advice(word_index, Rotation::next()));
},
);

cb.condition(
and::expr([
is_continue.expr(),
is_word_continue.is_lt(meta, None),
not_word_end.expr(),
]),
|cb| {
cb.require_equal(
Expand All @@ -338,7 +350,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
cb.condition(
and::expr([
is_continue.expr(),
not::expr(is_word_continue.is_lt(meta, None)),
is_word_end.expr(),
]),
|cb| {
cb.require_equal(
Expand Down Expand Up @@ -368,7 +380,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
// for all cases, rows[0].rw_counter + diff == rows[1].rw_counter
cb.condition(
and::expr([
is_word_continue.is_lt(meta, None),
not_word_end.expr(),
not_last_two_rows.expr(),
]),
|cb| {
Expand All @@ -391,7 +403,7 @@ 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([
not::expr(is_word_continue.is_lt(meta, None)),
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(),
Expand All @@ -416,7 +428,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
]),
);

cb.condition(not::expr(is_word_continue.is_lt(meta, None)), |cb| {
cb.condition(is_word_end.expr(), |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());
});
Expand Down Expand Up @@ -664,7 +676,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
meta.lookup_any("Memory word lookup", |meta| {
let cond = meta.query_fixed(q_enable, Rotation::cur())
* meta.query_advice(is_memory, Rotation::cur())
* not::expr(is_word_continue.is_lt(meta, None));
* is_word_end.is_equal_expression.expr();

let addr_slot = meta.query_advice(addr, Rotation::cur()) - 31.expr();

Expand All @@ -691,7 +703,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
meta.lookup_any("TxLog word lookup", |meta| {
let cond = meta.query_fixed(q_enable, Rotation::cur())
* meta.query_advice(is_tx_log, Rotation::cur())
* not::expr(is_word_continue.is_lt(meta, None));
* is_word_end.is_equal_expression.expr();

let addr_slot = meta.query_advice(addr, Rotation::cur()) - 31.expr();

Expand Down Expand Up @@ -774,7 +786,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
is_tx_log,
q_enable,
addr_lt_addr_end,
is_word_continue,
is_word_end,
non_pad_non_mask,
copy_table,
tx_table,
Expand All @@ -793,7 +805,7 @@ impl<F: Field> CopyCircuitConfig<F> {
offset: &mut usize,
tag_chip: &BinaryNumberChip<F, CopyDataType, 4>,
lt_chip: &LtChip<F, 8>,
lt_word_end_chip: &LtChip<F, 1>,
lt_word_end_chip: &IsEqualChip<F>,
non_pad_non_mask_chip: &LtChip<F, 1>,
challenges: Challenges<Value<F>>,
copy_event: &CopyEvent,
Expand Down Expand Up @@ -883,8 +895,8 @@ impl<F: Field> CopyCircuitConfig<F> {
lt_word_end_chip.assign(
region,
*offset,
F::from((step_idx as u64 / 2) % 32), // word index
F::from(31u64),
Value::known(F::from((step_idx as u64 / 2) % 32)), // word index
Value::known(F::from(31u64)),
)?;

let pad = unwrap_value(circuit_row[7].0);
Expand Down Expand Up @@ -959,7 +971,7 @@ impl<F: Field> CopyCircuitConfig<F> {

let tag_chip = BinaryNumberChip::construct(self.copy_table.tag);
let lt_chip = LtChip::construct(self.addr_lt_addr_end);
let lt_word_end_chip: LtChip<F, 1> = LtChip::construct(self.is_word_continue);
let lt_word_end_chip = IsEqualChip::construct(self.is_word_end.clone());
let non_pad_non_mask_chip: LtChip<F, 1> = LtChip::construct(self.non_pad_non_mask);

layouter.assign_region(
Expand Down Expand Up @@ -1046,7 +1058,7 @@ impl<F: Field> CopyCircuitConfig<F> {
is_last_two: bool,
tag_chip: &BinaryNumberChip<F, CopyDataType, 4>,
lt_chip: &LtChip<F, 8>,
lt_word_end_chip: &LtChip<F, 1>,
lt_word_end_chip: &IsEqualChip<F>,
non_pad_non_mask_chip: &LtChip<F, 1>,
) -> Result<(), Error> {
if !is_last_two {
Expand Down Expand Up @@ -1209,7 +1221,12 @@ impl<F: Field> CopyCircuitConfig<F> {
tag_chip.assign(region, *offset, &CopyDataType::Padding)?;
// Assign LT gadget
lt_chip.assign(region, *offset, F::zero(), F::one())?;
lt_word_end_chip.assign(region, *offset, F::zero(), F::from(31u64))?;
lt_word_end_chip.assign(
region,
*offset,
Value::known(F::zero()),
Value::known(F::from(31u64)),
)?;
non_pad_non_mask_chip.assign(region, *offset, F::one(), F::one())?;
for column in [
self.is_precompiled,
Expand Down