Skip to content
This repository was archived by the owner on Jul 5, 2024. It is now read-only.

[CREATE Part A (updated)] Modification to Copy Circuit #1419

Merged
KimiWu123 merged 11 commits into from
May 25, 2023
Merged

[CREATE Part A (updated)] Modification to Copy Circuit #1419

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
808d41e
feat: copy circuit maintains accumulator value and value RLC for memo…
roynalnaruto Apr 14, 2023
328a51d
Follow table definition split into files
ed255 May 19, 2023
55aebf9
fix for review comment
KimiWu123 May 22, 2023
bd2fb54
fix missing changes due to file moving
KimiWu123 May 22, 2023
516d7b7
fix: incorrect import
KimiWu123 May 22, 2023
d2bdc68
feat: adding value check in the first row of each copy event
KimiWu123 May 23, 2023
d591f47
chore: remove extra condition check
KimiWu123 May 23, 2023
b696d4a
fix: (!a & !b) should be eq !(a | b)
KimiWu123 May 23, 2023
4f66a8a
Merge branch 'main' into feat/create-part-a
KimiWu123 May 24, 2023
52d480a
fix: reduce final gate degree
KimiWu123 May 25, 2023
f2b97ec
feat: move 'value' from phase 2 to phase 1
KimiWu123 May 25, 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 mock/src/test_ctx.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,7 @@ pub use external_tracer::LoggerConfig;
/// // Now we can start generating the traces and items we need to inspect
/// // the behaviour of the generated env.
/// ```
#[derive(Debug)]
#[derive(Debug, Clone)]
pub struct TestContext<const NACC: usize, const NTX: usize> {
/// chain id
pub chain_id: Word,
Expand Down
132 changes: 78 additions & 54 deletions zkevm-circuits/src/copy_circuit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,8 @@ pub struct CopyCircuitConfig<F> {
pub is_last: Column<Advice>,
/// The value copied in this copy step.
pub value: Column<Advice>,
/// Random linear combination accumulator value.
pub value_acc_rlc: Column<Advice>,

@ed255 ed255 May 24, 2023

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Is this related to #971 ?
I see that now the rlc is accumulated in value_acc_rlc and then exposed in the table via rlc_acc, so rlc values never appear in the value column. So probably the issue is solved here.

@KimiWu123 KimiWu123 May 25, 2023

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

This was @roynalnaruto's fix and not sure the reason behind. But it seems solved the issue you mentioned.

@han0110 han0110 May 25, 2023

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

I think to have an extra value_acc_rlc is to support memory <-> bytecode copy and rlc at the same time without changing other parts too much.

And it seems to also resolve #971, so we could try to move the phase of value from second to first and see if it works as expected.

/// Whether the row is padding.
pub is_pad: Column<Advice>,
/// In case of a bytecode tag, this denotes whether or not the copied byte
Expand Down Expand Up @@ -107,7 +109,8 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
) -> Self {
let q_step = meta.complex_selector();
let is_last = meta.advice_column();
let value = meta.advice_column_in(SecondPhase);
let value = meta.advice_column();
let value_acc_rlc = meta.advice_column_in(SecondPhase);
let is_code = meta.advice_column();
let is_pad = meta.advice_column();
let is_first = copy_table.is_first;
Expand Down Expand Up @@ -225,23 +228,36 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
rw_diff,
);
});
cb.condition(
and::expr([
meta.query_advice(is_last, Rotation::cur()),
tag.value_equals(CopyDataType::RlcAcc, Rotation::cur())(meta),
]),
|cb| {
cb.require_equal(
"value == rlc_acc at the last row for RlcAcc",
meta.query_advice(value, Rotation::cur()),
meta.query_advice(rlc_acc, Rotation::cur()),
);
},
);

cb.gate(meta.query_fixed(q_enable, Rotation::cur()))
});

meta.create_gate(
"Last Step (check value accumulator) Memory => Bytecode or RlcAcc",
|meta: &mut halo2_proofs::plonk::VirtualCells<F>| {
let mut cb = BaseConstraintBuilder::default();

cb.require_equal(
"value_acc_rlc == rlc_acc on the last row",
meta.query_advice(value_acc_rlc, Rotation::next()),
meta.query_advice(rlc_acc, Rotation::next()),
);

cb.gate(and::expr([
meta.query_fixed(q_enable, Rotation::cur()),
meta.query_advice(is_last, Rotation::next()),
// To build a selector expression just having 0 when false and != 0 when true
// is enough, so we could replace the `or` by a `+`. This
// would give 2 when both expressions are true
// but it's fine.
and::expr([
tag.value_equals(CopyDataType::Memory, Rotation::cur())(meta),
tag.value_equals(CopyDataType::Bytecode, Rotation::next())(meta),
]) + tag.value_equals(CopyDataType::RlcAcc, Rotation::next())(meta),
]))
},
);

meta.create_gate("verify step (q_step == 1)", |meta| {
let mut cb = BaseConstraintBuilder::default();

Expand All @@ -253,10 +269,10 @@ 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,
))),
not::expr(or::expr([
meta.query_advice(is_last, Rotation::next()),
tag.value_equals(CopyDataType::Padding, Rotation::cur())(meta),
])),
|cb| {
cb.require_equal(
"bytes_left == bytes_left_next + 1 for non-last step",
Expand All @@ -265,25 +281,38 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
);
},
);
cb.condition(meta.query_advice(is_first, Rotation::cur()), |cb| {
cb.require_equal(
"value == value_acc_rlc at every first copy event",
meta.query_advice(value, Rotation::cur()),
meta.query_advice(value_acc_rlc, Rotation::cur()),
);
});
cb.require_equal(
"write value == read value",
meta.query_advice(value, Rotation::cur()),
meta.query_advice(value, Rotation::next()),
);
cb.require_equal(
"value_acc_rlc is same for read-write rows",
meta.query_advice(value_acc_rlc, Rotation::cur()),
meta.query_advice(value_acc_rlc, Rotation::next()),
);
cb.condition(
not::expr(tag.value_equals(CopyDataType::RlcAcc, Rotation::next())(
meta,
)),
and::expr([
not::expr(meta.query_advice(is_last, Rotation::next())),
not::expr(meta.query_advice(is_pad, Rotation::cur())),
]),
Comment thread
han0110 marked this conversation as resolved.
|cb| {
cb.require_equal(
"write value == read value (if not rlc acc)",
meta.query_advice(value, Rotation::cur()),
meta.query_advice(value, Rotation::next()),
"value_acc_rlc(2) == value_acc_rlc(0) * r + value(2)",
meta.query_advice(value_acc_rlc, Rotation(2)),
meta.query_advice(value_acc_rlc, Rotation::cur())
* challenges.keccak_input()
+ meta.query_advice(value, Rotation(2)),
Comment thread
han0110 marked this conversation as resolved.
);
},
);
cb.condition(meta.query_advice(is_first, Rotation::cur()), |cb| {
cb.require_equal(
"write value == read value (is_first == 1)",
meta.query_advice(value, Rotation::cur()),
meta.query_advice(value, Rotation::next()),
);
});
cb.require_zero(
"value == 0 when is_pad == 1 for read",
and::expr([
Expand All @@ -301,26 +330,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
meta.query_advice(is_pad, Rotation::next()),
);

cb.gate(meta.query_selector(q_step))
});

meta.create_gate("verify_step (q_step == 0)", |meta| {
let mut cb = BaseConstraintBuilder::default();

cb.require_equal(
"rows[2].value == rows[0].value * r + rows[1].value",
meta.query_advice(value, Rotation(2)),
meta.query_advice(value, Rotation::cur()) * challenges.keccak_input()
+ meta.query_advice(value, Rotation::next()),
);

cb.gate(and::expr([
meta.query_fixed(q_enable, Rotation::cur()),
not::expr(meta.query_selector(q_step)),
not::expr(meta.query_advice(is_last, Rotation::cur())),
tag.value_equals(CopyDataType::RlcAcc, Rotation::cur())(meta),
not::expr(meta.query_advice(is_pad, Rotation::cur())),
]))
cb.gate(and::expr([meta.query_selector(q_step)]))
});

meta.lookup_any("Memory lookup", |meta| {
Expand Down Expand Up @@ -405,6 +415,7 @@ impl<F: Field> SubCircuitConfig<F> for CopyCircuitConfig<F> {
q_step,
is_last,
value,
value_acc_rlc,
is_pad,
is_code,
q_enable,
Expand Down Expand Up @@ -466,9 +477,15 @@ impl<F: Field> CopyCircuitConfig<F> {
)?;

// is_last, value, is_pad, is_code
for (column, &(value, label)) in [self.is_last, self.value, self.is_pad, self.is_code]
.iter()
.zip_eq(circuit_row)
for (column, &(value, label)) in [
self.is_last,
self.value,
self.value_acc_rlc,
self.is_pad,
self.is_code,
]
.iter()
.zip_eq(circuit_row)
{
region.assign_advice(
|| format!("{} at row: {}", label, *offset),
Expand Down Expand Up @@ -621,6 +638,13 @@ impl<F: Field> CopyCircuitConfig<F> {
*offset,
|| Value::known(F::ZERO),
)?;
// value_acc_rlc
region.assign_advice(
|| format!("assign value_acc_rlc {}", *offset),
self.value_acc_rlc,
*offset,
|| Value::known(F::ZERO),
)?;
// rlc_acc
region.assign_advice(
|| format!("assign rlc_acc {}", *offset),
Expand Down
29 changes: 20 additions & 9 deletions zkevm-circuits/src/evm_circuit/execution/return_revert.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ pub(crate) struct ReturnRevertGadget<F> {
opcode: Cell<F>,

range: MemoryAddressGadget<F>,
deployed_code_rlc: Cell<F>,

is_success: Cell<F>,
restore_context: RestoreContextGadget<F>,
Expand Down Expand Up @@ -94,11 +95,12 @@ impl<F: Field> ExecutionGadget<F> for ReturnRevertGadget<F> {

let is_contract_deployment =
is_create.clone() * is_success.expr() * not::expr(copy_rw_increase_is_zero.expr());
let (caller_id, address, reversion_info, code_hash) =
let (caller_id, address, reversion_info, code_hash, deployed_code_rlc) =
cb.condition(is_contract_deployment.clone(), |cb| {
// We don't need to place any additional constraints on code_hash because the
// copy circuit enforces that it is the hash of the bytes in the copy lookup.
let code_hash = cb.query_cell_phase2();
let deployed_code_rlc = cb.query_cell_phase2();
cb.copy_table_lookup(
cb.curr.state.call_id.expr(),
CopyDataType::Memory.expr(),
Expand All @@ -108,7 +110,7 @@ impl<F: Field> ExecutionGadget<F> for ReturnRevertGadget<F> {
range.address(),
0.expr(),
range.length(),
0.expr(),
deployed_code_rlc.expr(),
copy_rw_increase.expr(),
);

Expand All @@ -127,7 +129,13 @@ impl<F: Field> ExecutionGadget<F> for ReturnRevertGadget<F> {
Some(&mut reversion_info),
);

(caller_id, address, reversion_info, code_hash)
(
caller_id,
address,
reversion_info,
code_hash,
deployed_code_rlc,
)
});

// Case B in the specs.
Expand Down Expand Up @@ -218,6 +226,7 @@ impl<F: Field> ExecutionGadget<F> for ReturnRevertGadget<F> {
Self {
opcode,
range,
deployed_code_rlc,
is_success,
copy_length,
copy_rw_increase,
Expand Down Expand Up @@ -279,6 +288,11 @@ impl<F: Field> ExecutionGadget<F> for ReturnRevertGadget<F> {
let values: Vec<_> = (3..3 + length.as_usize())
.map(|index| block.get_rws(step, index).memory_value())
.collect();
self.deployed_code_rlc.assign(
region,
offset,
region.keccak_rlc(&values.iter().rev().cloned().collect::<Vec<u8>>()),
)?;
let mut code_hash = CodeDB::hash(&values).to_fixed_bytes();
code_hash.reverse();
self.code_hash.assign(
Expand Down Expand Up @@ -614,10 +628,8 @@ mod test {
PUSH1(0) // dest offset
RETURNDATACOPY
});

let block: GethData = TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode.clone())
.unwrap()
.into();
let test_ctx = TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode.clone()).unwrap();
let block: GethData = test_ctx.clone().into();

// collect return opcode, retrieve next step, assure both contract create
// successfully
Expand Down Expand Up @@ -648,8 +660,7 @@ mod test {
.iter()
.for_each(|size| assert_eq!(size, &Word::zero()));

let text_ctx = TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap();
CircuitTestBuilder::new_from_test_ctx(text_ctx).run();
CircuitTestBuilder::new_from_test_ctx(test_ctx).run();
}

#[test]
Expand Down
13 changes: 13 additions & 0 deletions zkevm-circuits/src/evm_circuit/util.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -193,10 +193,23 @@ impl<'r, 'b, F: Field> CachedRegion<'r, 'b, F> {
.evm_word()
.map(|r| rlc::value(&n.to_le_bytes(), r))
}

pub fn keccak_rlc(&self, le_bytes: &[u8]) -> Value<F> {
self.challenges
.keccak_input()
.map(|r| rlc::value(le_bytes, r))
}

pub fn empty_code_hash_rlc(&self) -> Value<F> {
self.word_rlc(CodeDB::empty_code_hash().to_word())
}

pub fn code_hash(&self, n: U256) -> Value<F> {
self.challenges
.evm_word()
.map(|r| rlc::value(&n.to_le_bytes(), r))
}

/// Constrains a cell to have a constant value.
///
/// Returns an error if the cell is in a column where equality has not been
Expand Down
Loading