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

add constraint for rw counter #532

Merged
merged 19 commits into from
Jun 21, 2023
Merged

add constraint for rw counter #532

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
61957a0
fix tx_log table issue
lightsing Jun 9, 2023
edc1e77
constraint rw_counter and rw_inc_left
lightsing Jun 9, 2023
168b4eb
constraint rw_counter
lightsing Jun 9, 2023
05bca77
Merge branch 'memory_opt' into fix/copycircuit-constraints
lightsing Jun 9, 2023
d65e329
simplify constraint
lightsing Jun 12, 2023
12a678c
Merge remote-tracking branch 'origin/fix/copycircuit-constraints' int…
lightsing Jun 12, 2023
b203274
add column is_mem_to_mem to reduce the degree
lightsing Jun 12, 2023
2c00a48
Merge remote-tracking branch 'origin/memory_opt' into fix/copycircuit…
lightsing Jun 12, 2023
7eaa301
replace other usage of memory to memory tag query
lightsing Jun 12, 2023
b94b67e
fix value_acc
lightsing Jun 12, 2023
543c099
Merge remote-tracking branch 'origin/memory_opt' into fix/copycircuit…
lightsing Jun 13, 2023
0e17439
fix merge
lightsing Jun 13, 2023
673c464
remove is_mem_to_mem
lightsing Jun 13, 2023
b2bcb86
fix build
lightsing Jun 13, 2023
d693437
apply review
lightsing Jun 14, 2023
016cf60
Merge remote-tracking branch 'origin/memory_opt' into fix/copycircuit…
lightsing Jun 14, 2023
9c72456
Merge branch 'memory_opt' into fix/copycircuit-constraints
lightsing Jun 20, 2023
4c8df54
Merge remote-tracking branch 'origin/memory_opt' into fix/copycircuit…
lightsing Jun 21, 2023
6b32f7e
fix merge
lightsing Jun 21, 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
2 changes: 1 addition & 1 deletion bus-mapping/src/evm/opcodes/calldataload.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -201,7 +201,7 @@ mod calldataload_tests {
// };
let code_a = generate_mock_call_bytecode(MockCallBytecodeParams {
address: addr_b,
pushdata,
pushdata: pushdata.clone(),
call_data_length,
call_data_offset,
..MockCallBytecodeParams::default()
Expand Down
124 changes: 81 additions & 43 deletions zkevm-circuits/src/copy_circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -289,9 +289,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
and::expr([
is_word_continue.is_lt(meta, None),
not_last_two_rows.expr(),
not::expr(tag.value_equals(CopyDataType::Padding, Rotation::cur())(
meta,
)),
non_pad_non_mask.is_lt(meta, None),
]),
|cb| {
cb.require_equal(
Expand All @@ -306,9 +304,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
and::expr([
not::expr(is_word_continue.is_lt(meta, None)),
not_last_two_rows.expr(),
not::expr(tag.value_equals(CopyDataType::Padding, Rotation::cur())(
meta,
)),
non_pad_non_mask.is_lt(meta, None),
]),
|cb| {
cb.require_equal(
Expand All @@ -324,27 +320,81 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
},
);

// addr change: for tx log, addr use addr_slot as index, not increase by 1
// for all cases, rw_counter + rwc_inc_left keeps same
cb.condition(
and::expr([
not::expr(meta.query_advice(is_last, Rotation::cur())),
non_pad_non_mask.is_lt(meta, None),
]),
|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([
is_word_continue.is_lt(meta, None),
not_last_two_rows.expr(),
non_pad_non_mask.is_lt(meta, None),
not::expr(tag.value_equals(CopyDataType::TxLog, Rotation::cur())(meta)),
]),
|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()),
Copy link

@naure naure Jun 13, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

What are the 1 and -1 here? It seems that it should be 0 in this case, in the middle of a word.

Copy link
Member Author

Choose a reason for hiding this comment

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

it's arranged as a read row, a write row, ...
for memory write it has its own rw counter by increase 1

Copy link

@naure naure Jun 14, 2023 •
edited
Loading

Choose a reason for hiding this comment

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

Still not clear to me, when can the counter go backwards (-1)?

The most important requirement of the copy circuit is this:

  • It looks up an RW operation for each of [rwc .. rwc + rwc_left]

Can this be made simpler or clearer how this is enforced?

Copy link
Member Author

Choose a reason for hiding this comment

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

check this https://docs.google.com/spreadsheets/d/1UyNBdtFM1a6V_amGEc5UhNKLu1eYW2NgXbmp8v-PYvw/edit?usp=sharing

rw counter starts from 0x7c for the first read step and then a write step of 0x7d, so for the next read row, it's need to be same as the fist read row.

constraint using this way is for simplify the condition and reduce the degree.

Copy link

Choose a reason for hiding this comment

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

@naure if you have no more comments, I will merge this PR into memory_opt soon.

0.expr(),
);
cb.require_equal(
"rows[0].addr + 1 == rows[2].addr",
meta.query_advice(addr, Rotation::cur()) + 1.expr(),
meta.query_advice(addr, Rotation(2)),
"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([
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)
]),
|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()),
);
}
);

// FIXME: // addr change: for tx log, addr use addr_slot as index, not increase by 1
// cb.condition(
// and::expr([
// not_last_two_rows.expr(),
// not::expr(tag.value_equals(CopyDataType::Padding, Rotation::cur())(
// meta,
// )),
// not::expr(tag.value_equals(CopyDataType::TxLog, Rotation::cur())(meta)),
// ]),
// |cb| {
// cb.require_equal(
// "rows[0].addr + 1 == rows[2].addr",
// meta.query_advice(addr, Rotation::cur()) + 1.expr(),
// meta.query_advice(addr, Rotation(2)),
// );
// },
// );

cb.condition(
not_last_two_rows
* (not::expr(tag.value_equals(CopyDataType::Padding, Rotation::cur())(
meta,
))),
not_last_two_rows.expr() * non_pad_non_mask.is_lt(meta, None),
|cb| {
cb.require_equal(
"rows[0].id == rows[2].id",
Expand Down Expand Up @@ -375,16 +425,6 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
cb.condition(
not::expr(meta.query_advice(is_last, Rotation::cur())),
|cb| {
// cb.require_equal(
// "rows[0].rw_counter + rw_diff == rows[1].rw_counter",
// meta.query_advice(rw_counter, Rotation::cur()) + rw_diff.clone(),
// meta.query_advice(rw_counter, Rotation::next()),
// );
// cb.require_equal(
// "rows[0].rwc_inc_left - rw_diff == rows[1].rwc_inc_left",
// meta.query_advice(rwc_inc_left, Rotation::cur()) - rw_diff.clone(),
// meta.query_advice(rwc_inc_left, Rotation::next()),
// );
cb.require_equal(
"rows[0].rlc_acc == rows[1].rlc_acc",
meta.query_advice(rlc_acc, Rotation::cur()),
Expand Down Expand Up @@ -497,9 +537,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
);
cb.condition(
not::expr(meta.query_advice(is_last, Rotation::next()))
* (not::expr(tag.value_equals(CopyDataType::Padding, Rotation::cur())(
meta,
))),
* (non_pad_non_mask.is_lt(meta, None)),
|cb| {
cb.require_equal(
"bytes_left == bytes_left_next + 1 for non-last step",
Expand All @@ -510,13 +548,12 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
);
// we use rlc to constraint the write == read specially for memory to memory case
// here only handle non memory to memory cases
let non_memory_to_memory =
not::expr(tag.value_equals(CopyDataType::Memory, Rotation::cur())(
meta,
)) * not::expr(tag.value_equals(CopyDataType::Memory, Rotation::next())(
meta,
));
cb.condition(non_memory_to_memory, |cb| {
cb.condition(
not::expr(and::expr([
meta.query_advice(is_memory, Rotation::cur()),
meta.query_advice(is_memory, Rotation::next()),
])),
|cb| {
cb.require_equal(
"write value == read value",
meta.query_advice(value, Rotation::cur()),
Expand All @@ -533,15 +570,15 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
and::expr([
not::expr(meta.query_advice(is_last, Rotation::next())),
not::expr(meta.query_advice(is_pad, Rotation::cur())),
not::expr(meta.query_advice(mask, Rotation::cur())),
not::expr(meta.query_advice(mask, Rotation(2))),
]),
|cb| {
// cb.require_equal(
// "value_acc(2) == value_acc(0) * r + value(2)",
// meta.query_advice(value_acc, Rotation(2)),
// meta.query_advice(value_acc, Rotation::cur()) * challenges.keccak_input()
// + meta.query_advice(value, Rotation(2)),
// );
cb.require_equal(
"value_acc(2) == value_acc(0) * r + value(2)",
meta.query_advice(value_acc, Rotation(2)),
meta.query_advice(value_acc, Rotation::cur()) * challenges.keccak_input()
+ meta.query_advice(value, Rotation(2)),
);
},
);
cb.condition(not::expr(meta.query_advice(mask, Rotation::cur())), |cb| {
Expand Down Expand Up @@ -1093,6 +1130,7 @@ impl<F: Field> CopyCircuitConfig<F> {
*offset,
|| Value::known(F::zero()),
)?;

// rwc_inc_left
region.assign_advice(
|| format!("assign rwc_inc_left {}", *offset),
Expand Down