From 1714ac5544206c4d6b7de12fff5b151f94119935 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Thu, 19 May 2022 17:05:58 +0800 Subject: [PATCH 01/22] Add `ShlGadget`. --- zkevm-circuits/src/evm_circuit.rs | 1 + zkevm-circuits/src/evm_circuit/execution.rs | 5 + .../src/evm_circuit/execution/shl.rs | 128 ++++++++++++++++++ zkevm-circuits/src/evm_circuit/table.rs | 9 ++ zkevm-circuits/src/evm_circuit/witness.rs | 1 + zkevm-circuits/src/test_util.rs | 1 + 6 files changed, 145 insertions(+) create mode 100644 zkevm-circuits/src/evm_circuit/execution/shl.rs diff --git a/zkevm-circuits/src/evm_circuit.rs b/zkevm-circuits/src/evm_circuit.rs index 66d8cbfa93..b86f4b7a1f 100644 --- a/zkevm-circuits/src/evm_circuit.rs +++ b/zkevm-circuits/src/evm_circuit.rs @@ -493,6 +493,7 @@ pub mod test { FixedTableTag::Range1024, FixedTableTag::SignByte, FixedTableTag::ResponsibleOpcode, + FixedTableTag::Pow2, ], ) } diff --git a/zkevm-circuits/src/evm_circuit/execution.rs b/zkevm-circuits/src/evm_circuit/execution.rs index c63266a019..079acae16b 100644 --- a/zkevm-circuits/src/evm_circuit/execution.rs +++ b/zkevm-circuits/src/evm_circuit/execution.rs @@ -58,6 +58,7 @@ mod pc; mod pop; mod push; mod selfbalance; +mod shl; mod signed_comparator; mod signextend; mod sload; @@ -102,6 +103,7 @@ use pc::PcGadget; use pop::PopGadget; use push::PushGadget; use selfbalance::SelfbalanceGadget; +use shl::ShlGadget; use signed_comparator::SignedComparatorGadget; use signextend::SignextendGadget; use sload::SloadGadget; @@ -176,6 +178,7 @@ pub(crate) struct ExecutionConfig { pop_gadget: PopGadget, push_gadget: PushGadget, selfbalance_gadget: SelfbalanceGadget, + shl_gadget: ShlGadget, signed_comparator_gadget: SignedComparatorGadget, signextend_gadget: SignextendGadget, sload_gadget: SloadGadget, @@ -365,6 +368,7 @@ impl ExecutionConfig { pop_gadget: configure_gadget!(), push_gadget: configure_gadget!(), selfbalance_gadget: configure_gadget!(), + shl_gadget: configure_gadget!(), signed_comparator_gadget: configure_gadget!(), signextend_gadget: configure_gadget!(), sload_gadget: configure_gadget!(), @@ -803,6 +807,7 @@ impl ExecutionConfig { ExecutionState::BLOCKCTXU160 => assign_exec_step!(self.block_ctx_u160_gadget), ExecutionState::BLOCKCTXU256 => assign_exec_step!(self.block_ctx_u256_gadget), ExecutionState::SELFBALANCE => assign_exec_step!(self.selfbalance_gadget), + ExecutionState::SHL => assign_exec_step!(self.shl_gadget), ExecutionState::SIGNEXTEND => assign_exec_step!(self.signextend_gadget), ExecutionState::SLOAD => assign_exec_step!(self.sload_gadget), ExecutionState::SSTORE => assign_exec_step!(self.sstore_gadget), diff --git a/zkevm-circuits/src/evm_circuit/execution/shl.rs b/zkevm-circuits/src/evm_circuit/execution/shl.rs new file mode 100644 index 0000000000..03def32a4c --- /dev/null +++ b/zkevm-circuits/src/evm_circuit/execution/shl.rs @@ -0,0 +1,128 @@ +use crate::{ + evm_circuit::{ + execution::ExecutionGadget, + step::ExecutionState, + util::{ + common_gadget::SameContextGadget, + constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, + math_gadget::ShlWordsGadget, + CachedRegion, + }, + witness::{Block, Call, ExecStep, Transaction}, + }, + util::Expr, +}; +use bus_mapping::evm::OpcodeId; +use eth_types::Field; +use halo2_proofs::plonk::Error; + +#[derive(Clone, Debug)] +pub(crate) struct ShlGadget { + same_context: SameContextGadget, + shl_words: ShlWordsGadget, +} + +impl ExecutionGadget for ShlGadget { + const NAME: &'static str = "SHL"; + + const EXECUTION_STATE: ExecutionState = ExecutionState::SHL; + + fn configure(cb: &mut ConstraintBuilder) -> Self { + let opcode = cb.query_cell(); + + let a = cb.query_word(); + let shift = cb.query_word(); + + cb.stack_pop(shift.expr()); + cb.stack_pop(a.expr()); + let shl_words = ShlWordsGadget::construct(cb, a, shift); + cb.stack_push(shl_words.b().expr()); + + let step_state_transition = StepStateTransition { + rw_counter: Delta(3.expr()), + program_counter: Delta(1.expr()), + stack_pointer: Delta(1.expr()), + gas_left: Delta(-OpcodeId::SHL.constant_gas_cost().expr()), + ..Default::default() + }; + let same_context = SameContextGadget::construct(cb, opcode, step_state_transition); + + Self { + same_context, + shl_words, + } + } + + fn assign_exec_step( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + block: &Block, + _: &Transaction, + _: &Call, + step: &ExecStep, + ) -> Result<(), Error> { + self.same_context.assign_exec_step(region, offset, step)?; + let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; + let [shift, a, b] = indices.map(|idx| block.rws[idx].stack_value()); + self.shl_words.assign(region, offset, a, shift, b) + } +} + +#[cfg(test)] +mod test { + use crate::evm_circuit::test::rand_word; + use crate::test_util::run_test_circuits; + use eth_types::evm_types::OpcodeId; + use eth_types::{bytecode, Word}; + use mock::TestContext; + use rand::Rng; + + fn test_ok(opcode: OpcodeId, a: Word, shift: Word) { + let bytecode = bytecode! { + PUSH32(a) + PUSH32(shift) + #[start] + .write_op(opcode) + STOP + }; + assert_eq!( + run_test_circuits( + TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(), + None + ), + Ok(()) + ); + } + + #[test] + fn shl_gadget_simple() { + test_ok(OpcodeId::SHL, Word::from(0xABCD) << 240, 8.into()); + test_ok(OpcodeId::SHL, Word::from(0x1234) << 240, 7.into()); + test_ok(OpcodeId::SHL, Word::from(0x8765) << 240, 17.into()); + test_ok(OpcodeId::SHL, Word::from(0x4321) << 240, 0.into()); + } + + #[test] + fn shl_gadget_rand_normal_shift() { + let a = rand_word(); + let mut rng = rand::thread_rng(); + let shift = rng.gen_range(0..=255); + test_ok(OpcodeId::SHL, a, shift.into()); + } + + #[test] + fn shl_gadget_rand_overflow_shift() { + let a = rand_word(); + let shift = Word::from_big_endian(&[255_u8; 32]); + test_ok(OpcodeId::SHL, a, shift); + } + + // This case validates if the split is correct. + #[test] + fn shl_gadget_constant_shift() { + let a = rand_word(); + test_ok(OpcodeId::SHL, a, 8.into()); + test_ok(OpcodeId::SHL, a, 64.into()); + } +} diff --git a/zkevm-circuits/src/evm_circuit/table.rs b/zkevm-circuits/src/evm_circuit/table.rs index 423d4d6d25..8e5806544e 100644 --- a/zkevm-circuits/src/evm_circuit/table.rs +++ b/zkevm-circuits/src/evm_circuit/table.rs @@ -41,6 +41,7 @@ pub enum FixedTableTag { BitwiseOr, BitwiseXor, ResponsibleOpcode, + Pow2, } impl FixedTableTag { @@ -101,6 +102,14 @@ impl FixedTableTag { }) })) } + Self::Pow2 => Box::new((0..65).map(move |value| { + [ + tag, + F::from(value), + F::from_u128(1_u128 << value), + F::zero(), + ] + })), } } } diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index 9fa4d95563..4dc431bf51 100644 --- a/zkevm-circuits/src/evm_circuit/witness.rs +++ b/zkevm-circuits/src/evm_circuit/witness.rs @@ -1174,6 +1174,7 @@ impl From<&circuit_input_builder::ExecStep> for ExecutionState { OpcodeId::DIFFICULTY | OpcodeId::BASEFEE => ExecutionState::BLOCKCTXU256, OpcodeId::GAS => ExecutionState::GAS, OpcodeId::SELFBALANCE => ExecutionState::SELFBALANCE, + OpcodeId::SHL => ExecutionState::SHL, OpcodeId::SLOAD => ExecutionState::SLOAD, OpcodeId::SSTORE => ExecutionState::SSTORE, OpcodeId::CALLDATASIZE => ExecutionState::CALLDATASIZE, diff --git a/zkevm-circuits/src/test_util.rs b/zkevm-circuits/src/test_util.rs index b953f7150a..421ff7dfcb 100644 --- a/zkevm-circuits/src/test_util.rs +++ b/zkevm-circuits/src/test_util.rs @@ -34,6 +34,7 @@ pub fn get_fixed_table(conf: FixedTableConfig) -> Vec { FixedTableTag::Range1024, FixedTableTag::SignByte, FixedTableTag::ResponsibleOpcode, + FixedTableTag::Pow2, ] } FixedTableConfig::Complete => FixedTableTag::iter().collect(), From 558fd36e9ef95db1bd95d3e5be6b9234d54dbc01 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Thu, 19 May 2022 18:59:34 +0800 Subject: [PATCH 02/22] Add `ShlWordsGadget` to `math_gadget.rs`. --- .../src/evm_circuit/util/math_gadget.rs | 270 +++++++++++++++++- 1 file changed, 267 insertions(+), 3 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs index 8c1136c593..6d01408ba9 100644 --- a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs +++ b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs @@ -1,11 +1,16 @@ use super::CachedRegion; use crate::{ - evm_circuit::util::{ - self, constraint_builder::ConstraintBuilder, from_bytes, pow_of_two, pow_of_two_expr, - select, split_u256, split_u256_limb64, sum, Cell, + evm_circuit::{ + param::N_BYTES_U64, + table::{FixedTableTag, Lookup}, + util::{ + self, constraint_builder::ConstraintBuilder, from_bytes, pow_of_two, pow_of_two_expr, + select, split_u256, split_u256_limb64, sum, Cell, + }, }, util::Expr, }; +use array_init::array_init; use eth_types::{Field, ToLittleEndian, ToScalar, Word}; use halo2_proofs::plonk::{Error, Expression}; use std::convert::TryFrom; @@ -896,3 +901,262 @@ impl MulAddWordsGadget { self.overflow.clone() } } + +#[derive(Clone, Debug)] +pub(crate) struct ShlWordsGadget { + a: util::Word, + shift: util::Word, + b: util::Word, + // four 64-bit limbs of word `a` + a64s: [Cell; 4], + // four 64-bit limbs of word `b` + b64s: [Cell; 4], + // lower `64 - shf_mod64` bits + a64s_lo: [Cell; 4], + // higher `shf_mod64` bits + a64s_hi: [Cell; 4], + // shift[0] / 64 + shf_div64: Cell, + // shift[0] % 64 + shf_mod64: Cell, + // 1 << (64 - shf_mod64) + p_lo: Cell, + // 1 << shf_mod64 + p_hi: Cell, + // shift < 256 + shf_lt256: IsZeroGadget, + // shf_div64 == 0 + shf_div64_eq0: IsZeroGadget, + // shf_div64 == 1 + shf_div64_eq1: IsEqualGadget, + // shf_div64 == 2 + shf_div64_eq2: IsEqualGadget, + // a64s_hi[idx] < p_hi + a64s_hi_lt_p_hi: [LtGadget; 4], +} + +impl ShlWordsGadget { + pub(crate) fn construct( + cb: &mut ConstraintBuilder, + a: util::Word, + shift: util::Word, + ) -> Self { + let b = cb.query_word(); + let a64s = array_init(|_| cb.query_cell()); + let b64s = array_init(|_| cb.query_cell()); + let a64s_lo = array_init(|_| cb.query_cell()); + let a64s_hi = array_init(|_| cb.query_cell()); + let shf_div64 = cb.query_cell(); + let shf_mod64 = cb.query_cell(); + let p_lo = cb.query_cell(); + let p_hi = cb.query_cell(); + let shf_lt256 = IsZeroGadget::construct(cb, sum::expr(&shift.cells[1..32])); + for idx in 0..4 { + let offset = idx * N_BYTES_U64; + + // a64s constraint + cb.require_equal( + "a64s[idx] == from_bytes(a[8 * idx..8 * (idx + 1)])", + a64s[idx].expr(), + from_bytes::expr(&a.cells[offset..offset + N_BYTES_U64]), + ); + + // b64s constraint + cb.require_equal( + "b64s[idx] * shf_lt256 == from_bytes(b[8 * idx..8 * (idx + 1)])", + b64s[idx].expr() * shf_lt256.expr(), + from_bytes::expr(&b.cells[offset..offset + N_BYTES_U64]), + ); + + cb.require_equal( + "a64s[idx] == a64s_lo[idx] + a64s_hi[idx] * p_lo", + a64s[idx].expr(), + a64s_lo[idx].expr() + a64s_hi[idx].expr() * p_lo.expr(), + ); + } + + // a64s_hi[idx] < p_hi + let a64s_hi_lt_p_hi = array_init(|idx| { + let lt = LtGadget::construct(cb, a64s_hi[idx].expr(), p_hi.expr()); + cb.require_equal("a64s_hi[idx] < p_hi", lt.expr(), 1.expr()); + lt + }); + + // merge contraints + let shf_div64_eq0 = IsZeroGadget::construct(cb, shf_div64.expr()); + let shf_div64_eq1 = IsEqualGadget::construct(cb, shf_div64.expr(), 1.expr()); + let shf_div64_eq2 = IsEqualGadget::construct(cb, shf_div64.expr(), 2.expr()); + cb.require_equal( + "b64s[0] == shf_div64_eq0 * a64s_lo[0] * p_hi", + b64s[0].expr(), + shf_div64_eq0.expr() * a64s_lo[0].expr() * p_hi.expr(), + ); + cb.require_equal( + "b64s[1] == \ + shf_div64_eq0 * (a64s_hi[0] + a64s_lo[1] * p_hi) + \ + shf_div64_eq1 * a64s_lo[0] * p_hi", + b64s[1].expr(), + shf_div64_eq0.expr() * (a64s_hi[0].expr() + a64s_lo[1].expr() * p_hi.expr()) + + shf_div64_eq1.expr() * a64s_lo[0].expr() * p_hi.expr(), + ); + cb.require_equal( + "b64s[2] == \ + shf_div64_eq0 * (a64s_hi[1] + a64s_lo[2] * p_hi) + \ + shf_div64_eq1 * (a64s_hi[0] + a64s_lo[1] * p_hi) + \ + shf_div64_eq2 * a64s_lo[0] * p_hi", + b64s[2].expr(), + shf_div64_eq0.expr() * (a64s_hi[1].expr() + a64s_lo[2].expr() * p_hi.expr()) + + shf_div64_eq1.expr() * (a64s_hi[0].expr() + a64s_lo[1].expr() * p_hi.expr()) + + shf_div64_eq2.expr() * a64s_lo[0].expr() * p_hi.expr(), + ); + cb.require_equal( + "b64s[3] == \ + shf_div64_eq0 * (a64s_hi[2] + a64s_lo[3] * p_hi) + \ + shf_div64_eq1 * (a64s_hi[1] + a64s_lo[2] * p_hi) + \ + shf_div64_eq2 * (a64s_hi[0] + a64s_lo[1] * p_hi) + \ + (1 - shf_div64_eq0 - shf_div64_eq1 - shf_div64_eq2) * a64s_lo[0] * p_hi", + b64s[3].expr(), + shf_div64_eq0.expr() * (a64s_hi[2].expr() + a64s_lo[3].expr() * p_hi.expr()) + + shf_div64_eq1.expr() * (a64s_hi[1].expr() + a64s_lo[2].expr() * p_hi.expr()) + + shf_div64_eq2.expr() * (a64s_hi[0].expr() + a64s_lo[1].expr() * p_hi.expr()) + + (1.expr() - shf_div64_eq0.expr() - shf_div64_eq1.expr() - shf_div64_eq2.expr()) + * a64s_lo[0].expr() + * p_hi.expr(), + ); + + // shift constraint + cb.require_equal( + "shift[0] == shf_mod64 + shf_div64 * 64", + shift.cells[0].expr(), + shf_mod64.expr() + shf_div64.expr() * 64.expr(), + ); + + // p_lo == pow(2, 64 - shf_mod64) + cb.add_lookup( + "Pow2 lookup", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [64.expr() - shf_mod64.expr(), p_lo.expr(), 0.expr()], + }, + ); + + // p_hi == pow(2, shf_mod64) + cb.add_lookup( + "Pow2 lookup", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [shf_mod64.expr(), p_hi.expr(), 0.expr()], + }, + ); + + Self { + a, + shift, + b, + a64s, + b64s, + a64s_lo, + a64s_hi, + shf_div64, + shf_mod64, + p_lo, + p_hi, + shf_lt256, + shf_div64_eq0, + shf_div64_eq1, + shf_div64_eq2, + a64s_hi_lt_p_hi, + } + } + + pub(crate) fn assign( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + a: Word, + shift: Word, + b: Word, + ) -> Result<(), Error> { + self.assign_witness(region, offset, &a, &shift)?; + self.a.assign(region, offset, Some(a.to_le_bytes()))?; + self.shift + .assign(region, offset, Some(shift.to_le_bytes()))?; + self.b.assign(region, offset, Some(b.to_le_bytes()))?; + Ok(()) + } + + pub(crate) fn b(&self) -> &util::Word { + &self.b + } + + fn assign_witness( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + a: &Word, + shift: &Word, + ) -> Result<(), Error> { + let shf0 = shift.to_le_bytes()[0] as usize; + let shf_div64 = shf0 / 64; + let shf_mod64 = shf0 % 64; + let p_lo: u128 = 1 << (64 - shf_mod64); + let p_hi: u128 = 1 << shf_mod64; + let shf_lt256 = shift + .to_le_bytes() + .iter() + .fold(0, |acc, val| acc + *val as u128) + - shf0 as u128; + let a64s = a.0; + let mut a64s_lo = [0_u128; 4]; + let mut a64s_hi = [0_u128; 4]; + for idx in 0..4 { + a64s_lo[idx] = u128::from(a64s[idx]) % p_lo; + a64s_hi[idx] = u128::from(a64s[idx]) / p_lo; + } + let mut b64s = [0_u128; 4]; + b64s[shf_div64 as usize] = a64s_lo[0] * p_hi; + for k in 1..4 - shf_div64 { + b64s[k + shf_div64] = a64s_hi[k - 1] + a64s_lo[k] * p_hi; + } + self.a64s + .iter() + .zip(a64s.iter()) + .map(|(cell, val)| cell.assign(region, offset, Some(F::from(*val)))) + .collect::, _>>()?; + self.b64s + .iter() + .zip(b64s.iter()) + .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) + .collect::, _>>()?; + self.a64s_lo + .iter() + .zip(a64s_lo.iter()) + .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) + .collect::, _>>()?; + self.a64s_hi + .iter() + .zip(a64s_hi.iter()) + .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) + .collect::, _>>()?; + self.shf_div64 + .assign(region, offset, Some(F::from(shf_div64 as u64)))?; + self.shf_mod64 + .assign(region, offset, Some(F::from(shf_mod64 as u64)))?; + self.p_lo.assign(region, offset, Some(F::from_u128(p_lo)))?; + self.p_hi.assign(region, offset, Some(F::from_u128(p_hi)))?; + self.shf_lt256 + .assign(region, offset, F::from_u128(shf_lt256))?; + self.shf_div64_eq0 + .assign(region, offset, F::from(shf_div64 as u64))?; + self.shf_div64_eq1 + .assign(region, offset, F::from(shf_div64 as u64), F::from(1))?; + self.shf_div64_eq2 + .assign(region, offset, F::from(shf_div64 as u64), F::from(2))?; + self.a64s_hi_lt_p_hi + .iter() + .zip(a64s_hi.iter()) + .map(|(lt, val)| lt.assign(region, offset, F::from_u128(*val), F::from_u128(p_hi))) + .collect::, _>>()?; + Ok(()) + } +} From d738dd4be5b8f7db8a42bdbbdbe0a2c9ca4fd618 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Sun, 12 Jun 2022 16:52:50 +0800 Subject: [PATCH 03/22] Merge both opcode `SHL` and `SHR` into `MulDivModShlShrGadget. --- zkevm-circuits/src/evm_circuit/execution.rs | 22 +- .../src/evm_circuit/execution/mul_div_mod.rs | 238 ------------- .../execution/mul_div_mod_shl_shr.rs | 333 ++++++++++++++++++ zkevm-circuits/src/evm_circuit/step.rs | 16 +- zkevm-circuits/src/evm_circuit/witness.rs | 8 +- 5 files changed, 354 insertions(+), 263 deletions(-) delete mode 100644 zkevm-circuits/src/evm_circuit/execution/mul_div_mod.rs create mode 100644 zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs diff --git a/zkevm-circuits/src/evm_circuit/execution.rs b/zkevm-circuits/src/evm_circuit/execution.rs index 1ec5cddd91..2eda859d57 100644 --- a/zkevm-circuits/src/evm_circuit/execution.rs +++ b/zkevm-circuits/src/evm_circuit/execution.rs @@ -54,14 +54,12 @@ mod logs; mod memory; mod memory_copy; mod msize; -mod mul_div_mod; +mod mul_div_mod_shl_shr; mod origin; mod pc; mod pop; mod push; mod selfbalance; -mod shl; -mod shr; mod signed_comparator; mod signextend; mod sload; @@ -101,14 +99,12 @@ use logs::LogGadget; use memory::MemoryGadget; use memory_copy::CopyToMemoryGadget; use msize::MsizeGadget; -use mul_div_mod::MulDivModGadget; +use mul_div_mod_shl_shr::MulDivModShlShrGadget; use origin::OriginGadget; use pc::PcGadget; use pop::PopGadget; use push::PushGadget; use selfbalance::SelfbalanceGadget; -use shl::ShlGadget; -use shr::ShrGadget; use signed_comparator::SignedComparatorGadget; use signextend::SignextendGadget; use sload::SloadGadget; @@ -178,14 +174,12 @@ pub(crate) struct ExecutionConfig { log_gadget: LogGadget, memory_gadget: MemoryGadget, msize_gadget: MsizeGadget, - mul_div_mod_gadget: MulDivModGadget, + mul_div_mod_shl_shr_gadget: MulDivModShlShrGadget, origin_gadget: OriginGadget, pc_gadget: PcGadget, pop_gadget: PopGadget, push_gadget: PushGadget, selfbalance_gadget: SelfbalanceGadget, - shl_gadget: ShlGadget, - shr_gadget: ShrGadget, signed_comparator_gadget: SignedComparatorGadget, signextend_gadget: SignextendGadget, sload_gadget: SloadGadget, @@ -370,14 +364,12 @@ impl ExecutionConfig { log_gadget: configure_gadget!(), memory_gadget: configure_gadget!(), msize_gadget: configure_gadget!(), - mul_div_mod_gadget: configure_gadget!(), + mul_div_mod_shl_shr_gadget: configure_gadget!(), origin_gadget: configure_gadget!(), pc_gadget: configure_gadget!(), pop_gadget: configure_gadget!(), push_gadget: configure_gadget!(), selfbalance_gadget: configure_gadget!(), - shl_gadget: configure_gadget!(), - shr_gadget: configure_gadget!(), signed_comparator_gadget: configure_gadget!(), signextend_gadget: configure_gadget!(), sload_gadget: configure_gadget!(), @@ -807,7 +799,9 @@ impl ExecutionConfig { ExecutionState::LOG => assign_exec_step!(self.log_gadget), ExecutionState::MEMORY => assign_exec_step!(self.memory_gadget), ExecutionState::MSIZE => assign_exec_step!(self.msize_gadget), - ExecutionState::MUL_DIV_MOD => assign_exec_step!(self.mul_div_mod_gadget), + ExecutionState::MUL_DIV_MOD_SHL_SHR => { + assign_exec_step!(self.mul_div_mod_shl_shr_gadget) + } ExecutionState::ORIGIN => assign_exec_step!(self.origin_gadget), ExecutionState::PC => assign_exec_step!(self.pc_gadget), ExecutionState::POP => assign_exec_step!(self.pop_gadget), @@ -817,8 +811,6 @@ impl ExecutionConfig { ExecutionState::BLOCKCTXU160 => assign_exec_step!(self.block_ctx_u160_gadget), ExecutionState::BLOCKCTXU256 => assign_exec_step!(self.block_ctx_u256_gadget), ExecutionState::SELFBALANCE => assign_exec_step!(self.selfbalance_gadget), - ExecutionState::SHL => assign_exec_step!(self.shl_gadget), - ExecutionState::SHR => assign_exec_step!(self.shr_gadget), ExecutionState::SIGNEXTEND => assign_exec_step!(self.signextend_gadget), ExecutionState::SLOAD => assign_exec_step!(self.sload_gadget), ExecutionState::SSTORE => assign_exec_step!(self.sstore_gadget), diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod.rs deleted file mode 100644 index 4b2384a624..0000000000 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod.rs +++ /dev/null @@ -1,238 +0,0 @@ -use crate::{ - evm_circuit::{ - execution::ExecutionGadget, - step::ExecutionState, - util::{ - self, - common_gadget::SameContextGadget, - constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, - math_gadget::{IsZeroGadget, LtWordGadget, MulAddWordsGadget}, - select, sum, CachedRegion, - }, - witness::{Block, Call, ExecStep, Transaction}, - }, - util::Expr, -}; -use bus_mapping::evm::OpcodeId; -use eth_types::{Field, ToLittleEndian, U256}; -use halo2_proofs::plonk::Error; - -/// MulGadget verifies opcode MUL, DIV, and MOD. -/// For MUL, verify a * b = c (mod 2^256); -/// For DIV, verify a / b = c (mod 2^256); -/// For MOD, verify a % b = c (mod 2^256); -/// where a, b, c are 256-bit words. -#[derive(Clone, Debug)] -pub(crate) struct MulDivModGadget { - same_context: SameContextGadget, - /// Words a, b, c, d - pub words: [util::Word; 4], - /// Gadget that verifies a * b + c = d - mul_add_words: MulAddWordsGadget, - /// Check if divisor is zero for DIV and MOD - divisor_is_zero: IsZeroGadget, - /// Check if residue < divisor when divisor != 0 for DIV and MOD - lt_word: LtWordGadget, -} - -impl ExecutionGadget for MulDivModGadget { - const NAME: &'static str = "MUL_DIV_MOD"; - - const EXECUTION_STATE: ExecutionState = ExecutionState::MUL_DIV_MOD; - - fn configure(cb: &mut ConstraintBuilder) -> Self { - let opcode = cb.query_cell(); - - let is_mul = (OpcodeId::DIV.expr() - opcode.expr()) - * (OpcodeId::MOD.expr() - opcode.expr()) - * F::from(8).invert().unwrap(); - let is_div = (opcode.expr() - OpcodeId::MUL.expr()) - * (OpcodeId::MOD.expr() - opcode.expr()) - * F::from(4).invert().unwrap(); - let is_mod = (opcode.expr() - OpcodeId::MUL.expr()) - * (opcode.expr() - OpcodeId::DIV.expr()) - * F::from(8).invert().unwrap(); - let a = cb.query_word(); - let b = cb.query_word(); - let c = cb.query_word(); - let d = cb.query_word(); - - let mul_add_words = MulAddWordsGadget::construct(cb, [&a, &b, &c, &d]); - let divisor_is_zero = IsZeroGadget::construct(cb, sum::expr(&b.cells)); - let lt_word = LtWordGadget::construct(cb, &c, &b); - - // Pop a and b from the stack, push result on the stack - // The first pop is multiplier for MUL and dividend for DIV/MOD - // The second pop is multiplicand for MUL and divisor for DIV/MOD - // The push is product for MUL, quotient for DIV, and residue for MOD - // Note that for DIV/MOD, when divisor == 0, the push value is also 0. - cb.stack_pop(select::expr(is_mul.clone(), a.expr(), d.expr())); - cb.stack_pop(b.expr()); - cb.stack_push( - is_mul.clone() * d.expr() - + is_div * a.expr() * (1.expr() - divisor_is_zero.expr()) - + is_mod * c.expr() * (1.expr() - divisor_is_zero.expr()), - ); - - // Constraint for MUL case - cb.add_constraint( - "c == 0 for opcode MUL", - is_mul.clone() * sum::expr(&c.cells), - ); - - // Constraints for DIV and MOD cases - cb.condition(1.expr() - is_mul, |cb| { - cb.add_constraint( - "residue < divisor when divisor != 0 for opcode DIV/MOD", - (1.expr() - lt_word.expr()) * (1.expr() - divisor_is_zero.expr()), - ); - cb.require_zero("overflow == 0 for opcode DIV/MOD", mul_add_words.overflow()); - }); - - // State transition - let step_state_transition = StepStateTransition { - rw_counter: Delta(3.expr()), - program_counter: Delta(1.expr()), - stack_pointer: Delta(1.expr()), - gas_left: Delta(-OpcodeId::MUL.constant_gas_cost().expr()), - ..Default::default() - }; - let same_context = SameContextGadget::construct(cb, opcode, step_state_transition); - - Self { - words: [a, b, c, d], - same_context, - mul_add_words, - divisor_is_zero, - lt_word, - } - } - - fn assign_exec_step( - &self, - region: &mut CachedRegion<'_, '_, F>, - offset: usize, - block: &Block, - _: &Transaction, - _: &Call, - step: &ExecStep, - ) -> Result<(), Error> { - self.same_context.assign_exec_step(region, offset, step)?; - let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; - let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); - let (a, b, c, d) = match step.opcode.unwrap() { - OpcodeId::MUL => (pop1, pop2, U256::from(0), push), - OpcodeId::DIV => (push, pop2, pop1 - push * pop2, pop1), - OpcodeId::MOD => ( - if pop2.is_zero() { - U256::from(0) - } else { - pop1 / pop2 - }, - pop2, - if pop2.is_zero() { pop1 } else { push }, - pop1, - ), - _ => unreachable!(), - }; - self.words[0].assign(region, offset, Some(a.to_le_bytes()))?; - self.words[1].assign(region, offset, Some(b.to_le_bytes()))?; - self.words[2].assign(region, offset, Some(c.to_le_bytes()))?; - self.words[3].assign(region, offset, Some(d.to_le_bytes()))?; - self.mul_add_words.assign(region, offset, [a, b, c, d])?; - self.lt_word.assign(region, offset, c, b)?; - let b_sum = (0..32).fold(0, |acc, idx| acc + b.byte(idx) as u64); - self.divisor_is_zero - .assign(region, offset, F::from(b_sum))?; - Ok(()) - } -} - -#[cfg(test)] -mod test { - use crate::{evm_circuit::test::rand_word, test_util::run_test_circuits}; - use eth_types::evm_types::OpcodeId; - use eth_types::{bytecode, Word}; - use mock::TestContext; - - fn test_ok(opcode: OpcodeId, a: Word, b: Word) { - let bytecode = bytecode! { - PUSH32(b) - PUSH32(a) - #[start] - .write_op(opcode) - STOP - }; - - assert_eq!( - run_test_circuits( - TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(), - None - ), - Ok(()) - ); - } - - #[test] - fn mul_gadget_simple() { - test_ok(OpcodeId::MUL, 0x030201.into(), 0x060504.into()); - } - - #[test] - fn mul_gadget_overflow() { - let a = Word::from_dec_str("3402823669209384634633746074317682114560").unwrap(); // 2**128 * 10 - let b = Word::from_dec_str("34028236692093846346337460743176821145600").unwrap(); // 2**128 * 100 - test_ok(OpcodeId::MUL, a, b); - - let a = Word::from_dec_str("3402823669209384634633746074317682114560").unwrap(); // 2**128 * 10 - let b = Word::from_dec_str("34028236692093846346337460743176821145500").unwrap(); // (2**128 - 1) * 100 - test_ok(OpcodeId::MUL, a, b); - } - - #[test] - fn mul_gadget_rand() { - let a = rand_word(); - let b = rand_word(); - test_ok(OpcodeId::MUL, a, b); - } - - #[test] - fn div_gadget_simple() { - test_ok(OpcodeId::DIV, 0xFFFFFF.into(), 0xABC.into()); - test_ok(OpcodeId::DIV, 0xABC.into(), 0xFFFFFF.into()); - test_ok(OpcodeId::DIV, 0xFFFFFF.into(), 0xFFFFFFF.into()); - test_ok(OpcodeId::DIV, 0xABC.into(), 0.into()); - test_ok( - OpcodeId::DIV, - Word::from_big_endian(&[255u8; 32]), - 0xABCDEF.into(), - ); - } - - #[test] - fn div_gadget_rand() { - let dividend = rand_word(); - let divisor = rand_word(); - test_ok(OpcodeId::DIV, dividend, divisor); - } - - #[test] - fn mod_gadget_simple() { - test_ok(OpcodeId::MOD, 0xFFFFFF.into(), 0xABC.into()); - test_ok(OpcodeId::MOD, 0xABC.into(), 0xFFFFFF.into()); - test_ok(OpcodeId::MOD, 0xFFFFFF.into(), 0xFFFFFFF.into()); - test_ok(OpcodeId::MOD, 0xABC.into(), 0.into()); - test_ok( - OpcodeId::MOD, - Word::from_big_endian(&[255u8; 32]), - 0xABCDEF.into(), - ); - } - - #[test] - fn mod_gadget_rand() { - let dividend = rand_word(); - let divisor = rand_word(); - test_ok(OpcodeId::MOD, dividend, divisor); - } -} diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs new file mode 100644 index 0000000000..4356a6aaa1 --- /dev/null +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -0,0 +1,333 @@ +use crate::{ + evm_circuit::{ + execution::ExecutionGadget, + step::ExecutionState, + util::{ + self, + common_gadget::SameContextGadget, + constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, + math_gadget::{IsZeroGadget, LtWordGadget, MulAddWordsGadget}, + sum, CachedRegion, Cell, + }, + witness::{Block, Call, ExecStep, Transaction}, + }, + util::Expr, +}; +use bus_mapping::evm::OpcodeId; +use eth_types::{Field, ToLittleEndian, U256}; +use halo2_proofs::plonk::{Error, Expression}; + +/// MulDivModShlShrGadget verifies opcode MUL, DIV, MOD, SHL and SHR. +/// For MUL, verify pop1 * pop2 == push; +/// For DIV, verify pop1 / pop2 == push; +/// For MOD, verify pop1 % pop2 == push; +/// For SHL, verify pop1 * (2^pop2) == push; +/// For SHR, verify pop1 / (2^pop2) = push; +/// when pop1, pop2, push are 256-bit words. +#[derive(Clone, Debug)] +pub(crate) struct MulDivModShlShrGadget { + same_context: SameContextGadget, + /// Words quotient, divisor, remainder, dividend and + /// pop1 (used for shift value of SHL and SHR) + pub words: [util::Word; 5], + /// Gadget that verifies quotient * divisor + remainder = dividend + mul_add_words: MulAddWordsGadget, + /// Check if divisor is zero for opcode DIV, MOD and SHR + divisor_is_zero: IsZeroGadget, + /// Check if remainder is zero for opcode MUL and SHL + remainder_is_zero: IsZeroGadget, + /// Check if remainder < divisor when divisor != 0 + remainder_lt_divisor: LtWordGadget, +} + +impl ExecutionGadget for MulDivModShlShrGadget { + const NAME: &'static str = "MUL_DIV_MOD_SHL_SHR"; + + const EXECUTION_STATE: ExecutionState = ExecutionState::MUL_DIV_MOD_SHL_SHR; + + fn configure(cb: &mut ConstraintBuilder) -> Self { + let opcode = cb.query_cell(); + let is_mul = is_mul(&opcode); + let is_div = is_div(&opcode); + let is_mod = is_mod(&opcode); + let is_shl = is_shl(&opcode); + let is_shr = is_shr(&opcode); + + let quotient = cb.query_word(); + let divisor = cb.query_word(); + let remainder = cb.query_word(); + let dividend = cb.query_word(); + let pop1 = cb.query_word(); + + let mul_add_words = + MulAddWordsGadget::construct(cb, ["ient, &divisor, &remainder, ÷nd]); + let divisor_is_zero = IsZeroGadget::construct(cb, sum::expr(&divisor.cells)); + let remainder_is_zero = IsZeroGadget::construct(cb, sum::expr(&remainder.cells)); + let remainder_lt_divisor = LtWordGadget::construct(cb, &remainder, &divisor); + + // Based on different opcode cases, constrain stack pops and pushes as: + // - for `MUL`, two pops are quotient and divisor, and push is dividend. + // - for `DIV`, two pops are dividend and divisor, and push is quotient. + // - for `MOD`, two pops are dividend and divisor, and push is remainder. + // - for `SHL`, two pops are shift and quotient, and push is dividend. + // - for `SHR`, two pops are shift and dividend, and push is quotient. + cb.stack_pop(pop1.expr()); + cb.stack_pop( + (is_mul.clone() + is_div.clone() + is_mod.clone()) * divisor.expr() + + is_shl.clone() * quotient.expr() + + is_shr.clone() * dividend.expr(), + ); + cb.stack_push( + (is_mul.clone() + is_shl.clone()) * dividend.expr() + + (is_div.clone() + is_shr.clone()) + * quotient.expr() + * (1.expr() - divisor_is_zero.expr()) + + is_mod.clone() * remainder.expr() * (1.expr() - divisor_is_zero.expr()), + ); + + cb.require_zero( + "remainder < divisor when divisor != 0", + (1.expr() - divisor_is_zero.expr()) * (1.expr() - remainder_lt_divisor.expr()), + ); + + cb.require_zero( + "remainder == 0 for both opcode MUL and SHL", + (is_mul + is_shl) * (1.expr() - remainder_is_zero.expr()), + ); + + cb.require_zero( + "overflow == 0 for opcode DIV, MOD and SHR", + (is_div + is_mod + is_shr) * mul_add_words.overflow(), + ); + + let step_state_transition = StepStateTransition { + rw_counter: Delta(3.expr()), + program_counter: Delta(1.expr()), + stack_pointer: Delta(1.expr()), + gas_left: Delta(-OpcodeId::MUL.constant_gas_cost().expr()), + ..Default::default() + }; + + let same_context = SameContextGadget::construct(cb, opcode, step_state_transition); + + Self { + same_context, + words: [quotient, divisor, remainder, dividend, pop1], + mul_add_words, + divisor_is_zero, + remainder_is_zero, + remainder_lt_divisor, + } + } + + fn assign_exec_step( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + block: &Block, + _: &Transaction, + _: &Call, + step: &ExecStep, + ) -> Result<(), Error> { + self.same_context.assign_exec_step(region, offset, step)?; + let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; + let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); + + // Shift values are only used for opcode SHL and SHR. + let shf0 = pop1.to_le_bytes()[0]; + let shf_lt256 = pop1 + .to_le_bytes() + .iter() + .fold(0, |acc, val| acc + *val as u128) + - shf0 as u128; + + let (quotient, divisor, remainder, dividend) = match step.opcode.unwrap() { + OpcodeId::MUL => (pop1, pop2, U256::from(0), push), + OpcodeId::DIV => (push, pop2, pop1 - push * pop2, pop1), + OpcodeId::MOD => ( + if pop2.is_zero() { + U256::from(0) + } else { + pop1 / pop2 + }, + pop2, + if pop2.is_zero() { pop1 } else { push }, + pop1, + ), + OpcodeId::SHL => ( + pop2, + if shf_lt256 == 0 { + U256::from(1) << shf0 + } else { + U256::from(0) + }, + U256::from(0), + push, + ), + OpcodeId::SHR => { + let divisor = if shf_lt256 == 0 { + U256::from(1) << shf0 + } else { + U256::from(0) + }; + (push, divisor, pop2 - push * divisor, pop2) + } + _ => unreachable!(), + }; + self.words[0].assign(region, offset, Some(quotient.to_le_bytes()))?; + self.words[1].assign(region, offset, Some(divisor.to_le_bytes()))?; + self.words[2].assign(region, offset, Some(remainder.to_le_bytes()))?; + self.words[3].assign(region, offset, Some(dividend.to_le_bytes()))?; + self.words[4].assign(region, offset, Some(pop1.to_le_bytes()))?; + self.mul_add_words + .assign(region, offset, [quotient, divisor, remainder, dividend])?; + let divisor_sum = (0..32).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); + self.divisor_is_zero + .assign(region, offset, F::from(divisor_sum))?; + let remainder_sum = (0..32).fold(0, |acc, idx| acc + remainder.byte(idx) as u64); + self.remainder_is_zero + .assign(region, offset, F::from(remainder_sum))?; + self.remainder_lt_divisor + .assign(region, offset, remainder, divisor) + } +} + +// The opcode value for MUL, DIV, MOD, SHL and SHR are 2, 4, 6, 0x1b and 0x1c. +// When the opcode is MUL, the result of below formula is 5200: +// (DIV - opcode) * (MOD- opcode) * (SHL - opcode) * (SHR - opcode) +// To make `is_mul` be either 0 or 1, the result needs to be divided by 5200, +// which is equivalent to multiply it by inversion of 5200. +// And calculate `is_div`, `is_mod`, `is_shl` and `is_shr` respectively. +#[inline] +fn is_mul(opcode: &Cell) -> Expression { + (OpcodeId::DIV.expr() - opcode.expr()) + * (OpcodeId::MOD.expr() - opcode.expr()) + * (OpcodeId::SHL.expr() - opcode.expr()) + * (OpcodeId::SHR.expr() - opcode.expr()) + * F::from(5200).invert().unwrap() +} + +#[inline] +fn is_div(opcode: &Cell) -> Expression { + (opcode.expr() - OpcodeId::MUL.expr()) + * (OpcodeId::MOD.expr() - opcode.expr()) + * (OpcodeId::SHL.expr() - opcode.expr()) + * (OpcodeId::SHR.expr() - opcode.expr()) + * F::from(2208).invert().unwrap() +} + +#[inline] +fn is_mod(opcode: &Cell) -> Expression { + (opcode.expr() - OpcodeId::MUL.expr()) + * (opcode.expr() - OpcodeId::DIV.expr()) + * (OpcodeId::SHL.expr() - opcode.expr()) + * (OpcodeId::SHR.expr() - opcode.expr()) + * F::from(3696).invert().unwrap() +} + +#[inline] +fn is_shl(opcode: &Cell) -> Expression { + (opcode.expr() - OpcodeId::MUL.expr()) + * (opcode.expr() - OpcodeId::DIV.expr()) + * (opcode.expr() - OpcodeId::MOD.expr()) + * (OpcodeId::SHR.expr() - opcode.expr()) + * F::from(12075).invert().unwrap() +} + +#[inline] +fn is_shr(opcode: &Cell) -> Expression { + (opcode.expr() - OpcodeId::MUL.expr()) + * (opcode.expr() - OpcodeId::DIV.expr()) + * (opcode.expr() - OpcodeId::MOD.expr()) + * (opcode.expr() - OpcodeId::SHL.expr()) + * F::from(13728).invert().unwrap() +} + +#[cfg(test)] +mod test { + use crate::{evm_circuit::test::rand_word, test_util::run_test_circuits}; + use eth_types::evm_types::OpcodeId; + use eth_types::{bytecode, Word}; + use mock::TestContext; + + fn test_ok(opcode: OpcodeId, a: Word, b: Word) { + let bytecode = bytecode! { + PUSH32(b) + PUSH32(a) + #[start] + .write_op(opcode) + STOP + }; + + assert_eq!( + run_test_circuits( + TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(), + None + ), + Ok(()) + ); + } + + #[test] + fn mul_gadget_simple() { + test_ok(OpcodeId::MUL, 0x030201.into(), 0x060504.into()); + } + + #[test] + fn mul_gadget_overflow() { + let a = Word::from_dec_str("3402823669209384634633746074317682114560").unwrap(); // 2**128 * 10 + let b = Word::from_dec_str("34028236692093846346337460743176821145600").unwrap(); // 2**128 * 100 + test_ok(OpcodeId::MUL, a, b); + + let a = Word::from_dec_str("3402823669209384634633746074317682114560").unwrap(); // 2**128 * 10 + let b = Word::from_dec_str("34028236692093846346337460743176821145500").unwrap(); // (2**128 - 1) * 100 + test_ok(OpcodeId::MUL, a, b); + } + + #[test] + fn mul_gadget_rand() { + let a = rand_word(); + let b = rand_word(); + test_ok(OpcodeId::MUL, a, b); + } + + #[test] + fn div_gadget_simple() { + test_ok(OpcodeId::DIV, 0xFFFFFF.into(), 0xABC.into()); + test_ok(OpcodeId::DIV, 0xABC.into(), 0xFFFFFF.into()); + test_ok(OpcodeId::DIV, 0xFFFFFF.into(), 0xFFFFFFF.into()); + test_ok(OpcodeId::DIV, 0xABC.into(), 0.into()); + test_ok( + OpcodeId::DIV, + Word::from_big_endian(&[255u8; 32]), + 0xABCDEF.into(), + ); + } + + #[test] + fn div_gadget_rand() { + let dividend = rand_word(); + let divisor = rand_word(); + test_ok(OpcodeId::DIV, dividend, divisor); + } + + #[test] + fn mod_gadget_simple() { + test_ok(OpcodeId::MOD, 0xFFFFFF.into(), 0xABC.into()); + test_ok(OpcodeId::MOD, 0xABC.into(), 0xFFFFFF.into()); + test_ok(OpcodeId::MOD, 0xFFFFFF.into(), 0xFFFFFFF.into()); + test_ok(OpcodeId::MOD, 0xABC.into(), 0.into()); + test_ok( + OpcodeId::MOD, + Word::from_big_endian(&[255u8; 32]), + 0xABCDEF.into(), + ); + } + + #[test] + fn mod_gadget_rand() { + let dividend = rand_word(); + let divisor = rand_word(); + test_ok(OpcodeId::MOD, dividend, divisor); + } +} diff --git a/zkevm-circuits/src/evm_circuit/step.rs b/zkevm-circuits/src/evm_circuit/step.rs index f30ca9383f..9718a712dc 100644 --- a/zkevm-circuits/src/evm_circuit/step.rs +++ b/zkevm-circuits/src/evm_circuit/step.rs @@ -28,8 +28,8 @@ pub enum ExecutionState { CopyToLog, // Opcode successful cases STOP, - ADD_SUB, // ADD, SUB - MUL_DIV_MOD, // MUL, DIV, MOD + ADD_SUB, // ADD, SUB + MUL_DIV_MOD_SHL_SHR, // MUL, DIV, MOD, SHL, SHR SDIV, SMOD, ADDMOD, @@ -42,8 +42,6 @@ pub enum ExecutionState { BITWISE, // AND, OR, XOR NOT, BYTE, - SHL, - SHR, SAR, SHA3, ADDRESS, @@ -181,7 +179,13 @@ impl ExecutionState { match self { Self::STOP => vec![OpcodeId::STOP], Self::ADD_SUB => vec![OpcodeId::ADD, OpcodeId::SUB], - Self::MUL_DIV_MOD => vec![OpcodeId::MUL, OpcodeId::DIV, OpcodeId::MOD], + Self::MUL_DIV_MOD_SHL_SHR => vec![ + OpcodeId::MUL, + OpcodeId::DIV, + OpcodeId::MOD, + OpcodeId::SHL, + OpcodeId::SHR, + ], Self::SDIV => vec![OpcodeId::SDIV], Self::SMOD => vec![OpcodeId::SMOD], Self::ADDMOD => vec![OpcodeId::ADDMOD], @@ -194,8 +198,6 @@ impl ExecutionState { Self::BITWISE => vec![OpcodeId::AND, OpcodeId::OR, OpcodeId::XOR], Self::NOT => vec![OpcodeId::NOT], Self::BYTE => vec![OpcodeId::BYTE], - Self::SHL => vec![OpcodeId::SHL], - Self::SHR => vec![OpcodeId::SHR], Self::SAR => vec![OpcodeId::SAR], Self::SHA3 => vec![OpcodeId::SHA3], Self::ADDRESS => vec![OpcodeId::ADDRESS], diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index 543f6b45ca..8c0a797f41 100644 --- a/zkevm-circuits/src/evm_circuit/witness.rs +++ b/zkevm-circuits/src/evm_circuit/witness.rs @@ -1183,7 +1183,11 @@ impl From<&circuit_input_builder::ExecStep> for ExecutionState { } match op { OpcodeId::ADD | OpcodeId::SUB => ExecutionState::ADD_SUB, - OpcodeId::MUL | OpcodeId::DIV | OpcodeId::MOD => ExecutionState::MUL_DIV_MOD, + OpcodeId::MUL + | OpcodeId::DIV + | OpcodeId::MOD + | OpcodeId::SHL + | OpcodeId::SHR => ExecutionState::MUL_DIV_MOD_SHL_SHR, OpcodeId::EQ | OpcodeId::LT | OpcodeId::GT => ExecutionState::CMP, OpcodeId::SLT | OpcodeId::SGT => ExecutionState::SCMP, OpcodeId::SIGNEXTEND => ExecutionState::SIGNEXTEND, @@ -1214,8 +1218,6 @@ impl From<&circuit_input_builder::ExecStep> for ExecutionState { OpcodeId::DIFFICULTY | OpcodeId::BASEFEE => ExecutionState::BLOCKCTXU256, OpcodeId::GAS => ExecutionState::GAS, OpcodeId::SELFBALANCE => ExecutionState::SELFBALANCE, - OpcodeId::SHL => ExecutionState::SHL, - OpcodeId::SHR => ExecutionState::SHR, OpcodeId::SLOAD => ExecutionState::SLOAD, OpcodeId::SSTORE => ExecutionState::SSTORE, OpcodeId::CALLDATASIZE => ExecutionState::CALLDATASIZE, From eb89a002d72649059e412a4d132287a2b8f8e32c Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Sun, 12 Jun 2022 17:56:05 +0800 Subject: [PATCH 04/22] Add test cases. --- .../execution/mul_div_mod_shl_shr.rs | 120 ++++++++++-------- 1 file changed, 69 insertions(+), 51 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index 4356a6aaa1..f9c0f17c39 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -92,19 +92,25 @@ impl ExecutionGadget for MulDivModShlShrGadget { cb.require_zero( "remainder == 0 for both opcode MUL and SHL", - (is_mul + is_shl) * (1.expr() - remainder_is_zero.expr()), + (is_mul.clone() + is_shl.clone()) * (1.expr() - remainder_is_zero.expr()), ); cb.require_zero( "overflow == 0 for opcode DIV, MOD and SHR", - (is_div + is_mod + is_shr) * mul_add_words.overflow(), + (is_div.clone() + is_mod.clone() + is_shr.clone()) * mul_add_words.overflow(), ); + let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() + + is_div * OpcodeId::DIV.constant_gas_cost().expr() + + is_mod * OpcodeId::MOD.constant_gas_cost().expr() + + is_shl * OpcodeId::SHL.constant_gas_cost().expr() + + is_shr * OpcodeId::SHR.constant_gas_cost().expr(); + let step_state_transition = StepStateTransition { rw_counter: Delta(3.expr()), program_counter: Delta(1.expr()), stack_pointer: Delta(1.expr()), - gas_left: Delta(-OpcodeId::MUL.constant_gas_cost().expr()), + gas_left: Delta(-gas_cost), ..Default::default() }; @@ -250,10 +256,10 @@ mod test { use eth_types::{bytecode, Word}; use mock::TestContext; - fn test_ok(opcode: OpcodeId, a: Word, b: Word) { + fn test_ok(opcode: OpcodeId, pop1: Word, pop2: Word) { let bytecode = bytecode! { - PUSH32(b) - PUSH32(a) + PUSH32(pop1) + PUSH32(pop2) #[start] .write_op(opcode) STOP @@ -269,65 +275,77 @@ mod test { } #[test] - fn mul_gadget_simple() { - test_ok(OpcodeId::MUL, 0x030201.into(), 0x060504.into()); - } - - #[test] - fn mul_gadget_overflow() { - let a = Word::from_dec_str("3402823669209384634633746074317682114560").unwrap(); // 2**128 * 10 - let b = Word::from_dec_str("34028236692093846346337460743176821145600").unwrap(); // 2**128 * 100 - test_ok(OpcodeId::MUL, a, b); - - let a = Word::from_dec_str("3402823669209384634633746074317682114560").unwrap(); // 2**128 * 10 - let b = Word::from_dec_str("34028236692093846346337460743176821145500").unwrap(); // (2**128 - 1) * 100 - test_ok(OpcodeId::MUL, a, b); - } - - #[test] - fn mul_gadget_rand() { - let a = rand_word(); - let b = rand_word(); - test_ok(OpcodeId::MUL, a, b); + fn mul_gadget_tests() { + test_ok(OpcodeId::MUL, Word::from(0xABCD), Word::from(0x1234)); + test_ok(OpcodeId::MUL, Word::from(0xABCD), Word::from(0x1234) << 240); + test_ok( + OpcodeId::MUL, + Word::from(0xABCD) << 240, + Word::from(0x1234) << 240, + ); + let max_word = Word::from_big_endian(&[255_u8; 32]); + test_ok(OpcodeId::MUL, max_word, Word::from(0x1234)); + test_ok(OpcodeId::MUL, max_word, Word::from(0)); + test_ok(OpcodeId::MUL, rand_word(), rand_word()); } #[test] - fn div_gadget_simple() { - test_ok(OpcodeId::DIV, 0xFFFFFF.into(), 0xABC.into()); - test_ok(OpcodeId::DIV, 0xABC.into(), 0xFFFFFF.into()); - test_ok(OpcodeId::DIV, 0xFFFFFF.into(), 0xFFFFFFF.into()); - test_ok(OpcodeId::DIV, 0xABC.into(), 0.into()); + fn div_gadget_tests() { + test_ok(OpcodeId::DIV, Word::from(0xABCD), Word::from(0x1234)); + test_ok(OpcodeId::DIV, Word::from(0xABCD), Word::from(0x1234) << 240); test_ok( OpcodeId::DIV, - Word::from_big_endian(&[255u8; 32]), - 0xABCDEF.into(), + Word::from(0xABCD) << 240, + Word::from(0x1234) << 240, ); + let max_word = Word::from_big_endian(&[255_u8; 32]); + test_ok(OpcodeId::DIV, max_word, Word::from(0x1234)); + test_ok(OpcodeId::DIV, max_word, Word::from(0)); + test_ok(OpcodeId::DIV, rand_word(), rand_word()); } #[test] - fn div_gadget_rand() { - let dividend = rand_word(); - let divisor = rand_word(); - test_ok(OpcodeId::DIV, dividend, divisor); - } - - #[test] - fn mod_gadget_simple() { - test_ok(OpcodeId::MOD, 0xFFFFFF.into(), 0xABC.into()); - test_ok(OpcodeId::MOD, 0xABC.into(), 0xFFFFFF.into()); - test_ok(OpcodeId::MOD, 0xFFFFFF.into(), 0xFFFFFFF.into()); - test_ok(OpcodeId::MOD, 0xABC.into(), 0.into()); + fn mod_gadget_tests() { + test_ok(OpcodeId::MOD, Word::from(0xABCD), Word::from(0x1234)); + test_ok(OpcodeId::MOD, Word::from(0xABCD), Word::from(0x1234) << 240); test_ok( OpcodeId::MOD, - Word::from_big_endian(&[255u8; 32]), - 0xABCDEF.into(), + Word::from(0xABCD) << 240, + Word::from(0x1234) << 240, ); + let max_word = Word::from_big_endian(&[255_u8; 32]); + test_ok(OpcodeId::MOD, max_word, Word::from(0x1234)); + test_ok(OpcodeId::MOD, max_word, Word::from(0)); + test_ok(OpcodeId::MOD, rand_word(), rand_word()); + } + + #[test] + fn shl_gadget_tests() { + test_ok(OpcodeId::SHL, Word::from(0xABCD) << 240, Word::from(8)); + test_ok(OpcodeId::SHL, Word::from(0x1234) << 240, Word::from(7)); + test_ok(OpcodeId::SHL, Word::from(0x8765) << 240, Word::from(17)); + test_ok(OpcodeId::SHL, Word::from(0x4321) << 240, Word::from(0)); + test_ok(OpcodeId::SHL, Word::from(0xFFFF), Word::from(256)); + test_ok(OpcodeId::SHL, Word::from(0x12345), Word::from(256 + 8 + 1)); + let max_word = Word::from_big_endian(&[255_u8; 32]); + test_ok(OpcodeId::SHL, max_word, Word::from(63)); + test_ok(OpcodeId::SHL, max_word, Word::from(128)); + test_ok(OpcodeId::SHL, max_word, Word::from(129)); + test_ok(OpcodeId::SHL, rand_word(), rand_word()); } #[test] - fn mod_gadget_rand() { - let dividend = rand_word(); - let divisor = rand_word(); - test_ok(OpcodeId::MOD, dividend, divisor); + fn shr_gadget_tests() { + test_ok(OpcodeId::SHR, Word::from(0xABCD), Word::from(8)); + test_ok(OpcodeId::SHR, Word::from(0x1234), Word::from(7)); + test_ok(OpcodeId::SHR, Word::from(0x8765), Word::from(17)); + test_ok(OpcodeId::SHR, Word::from(0x4321), Word::from(0)); + test_ok(OpcodeId::SHR, Word::from(0xFFFF), Word::from(256)); + test_ok(OpcodeId::SHR, Word::from(0x12345), Word::from(256 + 8 + 1)); + let max_word = Word::from_big_endian(&[255_u8; 32]); + test_ok(OpcodeId::SHR, max_word, Word::from(63)); + test_ok(OpcodeId::SHR, max_word, Word::from(128)); + test_ok(OpcodeId::SHR, max_word, Word::from(129)); + test_ok(OpcodeId::SHR, rand_word(), rand_word()); } } From a57c20e550e6cdf5ddb571560ad77c3dde7440c2 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Sun, 12 Jun 2022 18:18:45 +0800 Subject: [PATCH 05/22] Delete old `SHL` and `SHR` gadgets. --- .../src/evm_circuit/execution/shl.rs | 128 ----- .../src/evm_circuit/execution/shr.rs | 128 ----- .../src/evm_circuit/util/math_gadget.rs | 524 +----------------- 3 files changed, 3 insertions(+), 777 deletions(-) delete mode 100644 zkevm-circuits/src/evm_circuit/execution/shl.rs delete mode 100644 zkevm-circuits/src/evm_circuit/execution/shr.rs diff --git a/zkevm-circuits/src/evm_circuit/execution/shl.rs b/zkevm-circuits/src/evm_circuit/execution/shl.rs deleted file mode 100644 index 03def32a4c..0000000000 --- a/zkevm-circuits/src/evm_circuit/execution/shl.rs +++ /dev/null @@ -1,128 +0,0 @@ -use crate::{ - evm_circuit::{ - execution::ExecutionGadget, - step::ExecutionState, - util::{ - common_gadget::SameContextGadget, - constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, - math_gadget::ShlWordsGadget, - CachedRegion, - }, - witness::{Block, Call, ExecStep, Transaction}, - }, - util::Expr, -}; -use bus_mapping::evm::OpcodeId; -use eth_types::Field; -use halo2_proofs::plonk::Error; - -#[derive(Clone, Debug)] -pub(crate) struct ShlGadget { - same_context: SameContextGadget, - shl_words: ShlWordsGadget, -} - -impl ExecutionGadget for ShlGadget { - const NAME: &'static str = "SHL"; - - const EXECUTION_STATE: ExecutionState = ExecutionState::SHL; - - fn configure(cb: &mut ConstraintBuilder) -> Self { - let opcode = cb.query_cell(); - - let a = cb.query_word(); - let shift = cb.query_word(); - - cb.stack_pop(shift.expr()); - cb.stack_pop(a.expr()); - let shl_words = ShlWordsGadget::construct(cb, a, shift); - cb.stack_push(shl_words.b().expr()); - - let step_state_transition = StepStateTransition { - rw_counter: Delta(3.expr()), - program_counter: Delta(1.expr()), - stack_pointer: Delta(1.expr()), - gas_left: Delta(-OpcodeId::SHL.constant_gas_cost().expr()), - ..Default::default() - }; - let same_context = SameContextGadget::construct(cb, opcode, step_state_transition); - - Self { - same_context, - shl_words, - } - } - - fn assign_exec_step( - &self, - region: &mut CachedRegion<'_, '_, F>, - offset: usize, - block: &Block, - _: &Transaction, - _: &Call, - step: &ExecStep, - ) -> Result<(), Error> { - self.same_context.assign_exec_step(region, offset, step)?; - let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; - let [shift, a, b] = indices.map(|idx| block.rws[idx].stack_value()); - self.shl_words.assign(region, offset, a, shift, b) - } -} - -#[cfg(test)] -mod test { - use crate::evm_circuit::test::rand_word; - use crate::test_util::run_test_circuits; - use eth_types::evm_types::OpcodeId; - use eth_types::{bytecode, Word}; - use mock::TestContext; - use rand::Rng; - - fn test_ok(opcode: OpcodeId, a: Word, shift: Word) { - let bytecode = bytecode! { - PUSH32(a) - PUSH32(shift) - #[start] - .write_op(opcode) - STOP - }; - assert_eq!( - run_test_circuits( - TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(), - None - ), - Ok(()) - ); - } - - #[test] - fn shl_gadget_simple() { - test_ok(OpcodeId::SHL, Word::from(0xABCD) << 240, 8.into()); - test_ok(OpcodeId::SHL, Word::from(0x1234) << 240, 7.into()); - test_ok(OpcodeId::SHL, Word::from(0x8765) << 240, 17.into()); - test_ok(OpcodeId::SHL, Word::from(0x4321) << 240, 0.into()); - } - - #[test] - fn shl_gadget_rand_normal_shift() { - let a = rand_word(); - let mut rng = rand::thread_rng(); - let shift = rng.gen_range(0..=255); - test_ok(OpcodeId::SHL, a, shift.into()); - } - - #[test] - fn shl_gadget_rand_overflow_shift() { - let a = rand_word(); - let shift = Word::from_big_endian(&[255_u8; 32]); - test_ok(OpcodeId::SHL, a, shift); - } - - // This case validates if the split is correct. - #[test] - fn shl_gadget_constant_shift() { - let a = rand_word(); - test_ok(OpcodeId::SHL, a, 8.into()); - test_ok(OpcodeId::SHL, a, 64.into()); - } -} diff --git a/zkevm-circuits/src/evm_circuit/execution/shr.rs b/zkevm-circuits/src/evm_circuit/execution/shr.rs deleted file mode 100644 index 49714fc652..0000000000 --- a/zkevm-circuits/src/evm_circuit/execution/shr.rs +++ /dev/null @@ -1,128 +0,0 @@ -use crate::{ - evm_circuit::{ - execution::ExecutionGadget, - step::ExecutionState, - util::{ - common_gadget::SameContextGadget, - constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, - math_gadget::ShrWordsGadget, - CachedRegion, - }, - witness::{Block, Call, ExecStep, Transaction}, - }, - util::Expr, -}; -use bus_mapping::evm::OpcodeId; -use eth_types::Field; -use halo2_proofs::plonk::Error; - -#[derive(Clone, Debug)] -pub(crate) struct ShrGadget { - same_context: SameContextGadget, - shr_words: ShrWordsGadget, -} - -impl ExecutionGadget for ShrGadget { - const NAME: &'static str = "SHR"; - - const EXECUTION_STATE: ExecutionState = ExecutionState::SHR; - - fn configure(cb: &mut ConstraintBuilder) -> Self { - let opcode = cb.query_cell(); - - let a = cb.query_word(); - let shift = cb.query_word(); - - cb.stack_pop(shift.expr()); - cb.stack_pop(a.expr()); - let shr_words = ShrWordsGadget::construct(cb, a, shift); - cb.stack_push(shr_words.b().expr()); - - let step_state_transition = StepStateTransition { - rw_counter: Delta(3.expr()), - program_counter: Delta(1.expr()), - stack_pointer: Delta(1.expr()), - gas_left: Delta(-OpcodeId::SHR.constant_gas_cost().expr()), - ..Default::default() - }; - let same_context = SameContextGadget::construct(cb, opcode, step_state_transition); - - Self { - same_context, - shr_words, - } - } - - fn assign_exec_step( - &self, - region: &mut CachedRegion<'_, '_, F>, - offset: usize, - block: &Block, - _: &Transaction, - _: &Call, - step: &ExecStep, - ) -> Result<(), Error> { - self.same_context.assign_exec_step(region, offset, step)?; - let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; - let [shift, a, b] = indices.map(|idx| block.rws[idx].stack_value()); - self.shr_words.assign(region, offset, a, shift, b) - } -} - -#[cfg(test)] -mod test { - use crate::evm_circuit::test::rand_word; - use crate::test_util::run_test_circuits; - use eth_types::evm_types::OpcodeId; - use eth_types::{bytecode, Word}; - use mock::TestContext; - use rand::Rng; - - fn test_ok(opcode: OpcodeId, a: Word, shift: Word) { - let bytecode = bytecode! { - PUSH32(a) - PUSH32(shift) - #[start] - .write_op(opcode) - STOP - }; - assert_eq!( - run_test_circuits( - TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(), - None - ), - Ok(()) - ); - } - - #[test] - fn shr_gadget_simple() { - test_ok(OpcodeId::SHR, 0xABCD.into(), 8.into()); - test_ok(OpcodeId::SHR, 0x1234.into(), 7.into()); - test_ok(OpcodeId::SHR, 0x8765.into(), 17.into()); - test_ok(OpcodeId::SHR, 0x4321.into(), 0.into()); - test_ok(OpcodeId::SHR, rand_word(), 127.into()); - test_ok(OpcodeId::SHR, rand_word(), 129.into()); - let rand_shift = rand::thread_rng().gen_range(0..=255); - test_ok(OpcodeId::SHR, rand_word(), rand_shift.into()); - } - - #[test] - fn shr_gadget_rand_overflow_shift() { - test_ok(OpcodeId::SHR, rand_word(), 256.into()); - test_ok(OpcodeId::SHR, rand_word(), 0x1234.into()); - test_ok( - OpcodeId::SHR, - rand_word(), - Word::from_big_endian(&[255_u8; 32]), - ); - } - - // This case validates if the split is correct. - #[test] - fn shr_gadget_constant_shift() { - let a = rand_word(); - test_ok(OpcodeId::SHR, a, 8.into()); - test_ok(OpcodeId::SHR, a, 64.into()); - } -} diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs index 0118f931a2..3e55898844 100644 --- a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs +++ b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs @@ -1,16 +1,11 @@ use super::CachedRegion; use crate::{ - evm_circuit::{ - param::N_BYTES_U64, - table::{FixedTableTag, Lookup}, - util::{ - self, constraint_builder::ConstraintBuilder, from_bytes, pow_of_two, pow_of_two_expr, - select, split_u256, split_u256_limb64, sum, Cell, - }, + evm_circuit::util::{ + self, constraint_builder::ConstraintBuilder, from_bytes, pow_of_two, pow_of_two_expr, + select, split_u256, split_u256_limb64, sum, Cell, }, util::Expr, }; -use array_init::array_init; use eth_types::{Field, ToLittleEndian, ToScalar, Word}; use halo2_proofs::plonk::{Error, Expression}; use std::convert::TryFrom; @@ -886,516 +881,3 @@ impl MulAddWordsGadget { self.overflow.clone() } } - -#[derive(Clone, Debug)] -pub(crate) struct ShlWordsGadget { - a: util::Word, - shift: util::Word, - b: util::Word, - // four 64-bit limbs of word `a` - a64s: [Cell; 4], - // four 64-bit limbs of word `b` - b64s: [Cell; 4], - // lower `64 - shf_mod64` bits - a64s_lo: [Cell; 4], - // higher `shf_mod64` bits - a64s_hi: [Cell; 4], - // shift[0] / 64 - shf_div64: Cell, - // shift[0] % 64 - shf_mod64: Cell, - // 1 << (64 - shf_mod64) - p_lo: Cell, - // 1 << shf_mod64 - p_hi: Cell, - // shift < 256 - shf_lt256: IsZeroGadget, - // shf_div64 == 0 - shf_div64_eq0: IsZeroGadget, - // shf_div64 == 1 - shf_div64_eq1: IsEqualGadget, - // shf_div64 == 2 - shf_div64_eq2: IsEqualGadget, - // a64s_hi[idx] < p_hi - a64s_hi_lt_p_hi: [LtGadget; 4], -} - -impl ShlWordsGadget { - pub(crate) fn construct( - cb: &mut ConstraintBuilder, - a: util::Word, - shift: util::Word, - ) -> Self { - let b = cb.query_word(); - let a64s = array_init(|_| cb.query_cell()); - let b64s = array_init(|_| cb.query_cell()); - let a64s_lo = array_init(|_| cb.query_cell()); - let a64s_hi = array_init(|_| cb.query_cell()); - let shf_div64 = cb.query_cell(); - let shf_mod64 = cb.query_cell(); - let p_lo = cb.query_cell(); - let p_hi = cb.query_cell(); - let shf_lt256 = IsZeroGadget::construct(cb, sum::expr(&shift.cells[1..32])); - for idx in 0..4 { - let offset = idx * N_BYTES_U64; - - // a64s constraint - cb.require_equal( - "a64s[idx] == from_bytes(a[8 * idx..8 * (idx + 1)])", - a64s[idx].expr(), - from_bytes::expr(&a.cells[offset..offset + N_BYTES_U64]), - ); - - // b64s constraint - cb.require_equal( - "b64s[idx] * shf_lt256 == from_bytes(b[8 * idx..8 * (idx + 1)])", - b64s[idx].expr() * shf_lt256.expr(), - from_bytes::expr(&b.cells[offset..offset + N_BYTES_U64]), - ); - - cb.require_equal( - "a64s[idx] == a64s_lo[idx] + a64s_hi[idx] * p_lo", - a64s[idx].expr(), - a64s_lo[idx].expr() + a64s_hi[idx].expr() * p_lo.expr(), - ); - } - - // a64s_hi[idx] < p_hi - let a64s_hi_lt_p_hi = array_init(|idx| { - let lt = LtGadget::construct(cb, a64s_hi[idx].expr(), p_hi.expr()); - cb.require_equal("a64s_hi[idx] < p_hi", lt.expr(), 1.expr()); - lt - }); - - // merge contraints - let shf_div64_eq0 = IsZeroGadget::construct(cb, shf_div64.expr()); - let shf_div64_eq1 = IsEqualGadget::construct(cb, shf_div64.expr(), 1.expr()); - let shf_div64_eq2 = IsEqualGadget::construct(cb, shf_div64.expr(), 2.expr()); - cb.require_equal( - "b64s[0] == shf_div64_eq0 * a64s_lo[0] * p_hi", - b64s[0].expr(), - shf_div64_eq0.expr() * a64s_lo[0].expr() * p_hi.expr(), - ); - cb.require_equal( - "b64s[1] == \ - shf_div64_eq0 * (a64s_hi[0] + a64s_lo[1] * p_hi) + \ - shf_div64_eq1 * a64s_lo[0] * p_hi", - b64s[1].expr(), - shf_div64_eq0.expr() * (a64s_hi[0].expr() + a64s_lo[1].expr() * p_hi.expr()) - + shf_div64_eq1.expr() * a64s_lo[0].expr() * p_hi.expr(), - ); - cb.require_equal( - "b64s[2] == \ - shf_div64_eq0 * (a64s_hi[1] + a64s_lo[2] * p_hi) + \ - shf_div64_eq1 * (a64s_hi[0] + a64s_lo[1] * p_hi) + \ - shf_div64_eq2 * a64s_lo[0] * p_hi", - b64s[2].expr(), - shf_div64_eq0.expr() * (a64s_hi[1].expr() + a64s_lo[2].expr() * p_hi.expr()) - + shf_div64_eq1.expr() * (a64s_hi[0].expr() + a64s_lo[1].expr() * p_hi.expr()) - + shf_div64_eq2.expr() * a64s_lo[0].expr() * p_hi.expr(), - ); - cb.require_equal( - "b64s[3] == \ - shf_div64_eq0 * (a64s_hi[2] + a64s_lo[3] * p_hi) + \ - shf_div64_eq1 * (a64s_hi[1] + a64s_lo[2] * p_hi) + \ - shf_div64_eq2 * (a64s_hi[0] + a64s_lo[1] * p_hi) + \ - (1 - shf_div64_eq0 - shf_div64_eq1 - shf_div64_eq2) * a64s_lo[0] * p_hi", - b64s[3].expr(), - shf_div64_eq0.expr() * (a64s_hi[2].expr() + a64s_lo[3].expr() * p_hi.expr()) - + shf_div64_eq1.expr() * (a64s_hi[1].expr() + a64s_lo[2].expr() * p_hi.expr()) - + shf_div64_eq2.expr() * (a64s_hi[0].expr() + a64s_lo[1].expr() * p_hi.expr()) - + (1.expr() - shf_div64_eq0.expr() - shf_div64_eq1.expr() - shf_div64_eq2.expr()) - * a64s_lo[0].expr() - * p_hi.expr(), - ); - - // shift constraint - cb.require_equal( - "shift[0] == shf_mod64 + shf_div64 * 64", - shift.cells[0].expr(), - shf_mod64.expr() + shf_div64.expr() * 64.expr(), - ); - - // p_lo == pow(2, 64 - shf_mod64) - cb.add_lookup( - "Pow2 lookup", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [64.expr() - shf_mod64.expr(), p_lo.expr(), 0.expr()], - }, - ); - - // p_hi == pow(2, shf_mod64) - cb.add_lookup( - "Pow2 lookup", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [shf_mod64.expr(), p_hi.expr(), 0.expr()], - }, - ); - - Self { - a, - shift, - b, - a64s, - b64s, - a64s_lo, - a64s_hi, - shf_div64, - shf_mod64, - p_lo, - p_hi, - shf_lt256, - shf_div64_eq0, - shf_div64_eq1, - shf_div64_eq2, - a64s_hi_lt_p_hi, - } - } - - pub(crate) fn assign( - &self, - region: &mut CachedRegion<'_, '_, F>, - offset: usize, - a: Word, - shift: Word, - b: Word, - ) -> Result<(), Error> { - self.assign_witness(region, offset, &a, &shift)?; - self.a.assign(region, offset, Some(a.to_le_bytes()))?; - self.shift - .assign(region, offset, Some(shift.to_le_bytes()))?; - self.b.assign(region, offset, Some(b.to_le_bytes()))?; - Ok(()) - } - - pub(crate) fn b(&self) -> &util::Word { - &self.b - } - - fn assign_witness( - &self, - region: &mut CachedRegion<'_, '_, F>, - offset: usize, - a: &Word, - shift: &Word, - ) -> Result<(), Error> { - let shf0 = shift.to_le_bytes()[0] as usize; - let shf_div64 = shf0 / 64; - let shf_mod64 = shf0 % 64; - let p_lo: u128 = 1 << (64 - shf_mod64); - let p_hi: u128 = 1 << shf_mod64; - let shf_lt256 = shift - .to_le_bytes() - .iter() - .fold(0, |acc, val| acc + *val as u128) - - shf0 as u128; - let a64s = a.0; - let mut a64s_lo = [0_u128; 4]; - let mut a64s_hi = [0_u128; 4]; - for idx in 0..4 { - a64s_lo[idx] = u128::from(a64s[idx]) % p_lo; - a64s_hi[idx] = u128::from(a64s[idx]) / p_lo; - } - let mut b64s = [0_u128; 4]; - b64s[shf_div64 as usize] = a64s_lo[0] * p_hi; - for k in 1..4 - shf_div64 { - b64s[k + shf_div64] = a64s_hi[k - 1] + a64s_lo[k] * p_hi; - } - self.a64s - .iter() - .zip(a64s.iter()) - .map(|(cell, val)| cell.assign(region, offset, Some(F::from(*val)))) - .collect::, _>>()?; - self.b64s - .iter() - .zip(b64s.iter()) - .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) - .collect::, _>>()?; - self.a64s_lo - .iter() - .zip(a64s_lo.iter()) - .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) - .collect::, _>>()?; - self.a64s_hi - .iter() - .zip(a64s_hi.iter()) - .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) - .collect::, _>>()?; - self.shf_div64 - .assign(region, offset, Some(F::from(shf_div64 as u64)))?; - self.shf_mod64 - .assign(region, offset, Some(F::from(shf_mod64 as u64)))?; - self.p_lo.assign(region, offset, Some(F::from_u128(p_lo)))?; - self.p_hi.assign(region, offset, Some(F::from_u128(p_hi)))?; - self.shf_lt256 - .assign(region, offset, F::from_u128(shf_lt256))?; - self.shf_div64_eq0 - .assign(region, offset, F::from(shf_div64 as u64))?; - self.shf_div64_eq1 - .assign(region, offset, F::from(shf_div64 as u64), F::from(1))?; - self.shf_div64_eq2 - .assign(region, offset, F::from(shf_div64 as u64), F::from(2))?; - self.a64s_hi_lt_p_hi - .iter() - .zip(a64s_hi.iter()) - .map(|(lt, val)| lt.assign(region, offset, F::from_u128(*val), F::from_u128(p_hi))) - .collect::, _>>()?; - Ok(()) - } -} - -/// Construction of word shift right for `a >> shift == b`. -#[derive(Clone, Debug)] -pub(crate) struct ShrWordsGadget { - a: util::Word, - shift: util::Word, - b: util::Word, - // four 64-bit limbs of word `a` - a64s: [Cell; 4], - // four 64-bit limbs of word `b` - b64s: [Cell; 4], - // Each of the four `a64s` limbs is split into two parts (`a64s_lo` and `a64s_hi`) at - // position `shf_mod64`. `a64s_lo` is the lower `shf_mod64` bits. - a64s_lo: [Cell; 4], - // `a64s_hi` is the higher `64 - shf_mod64` bits. - a64s_hi: [Cell; 4], - // shift[0] / 64 - shf_div64: Cell, - // shift[0] % 64 - shf_mod64: Cell, - // 1 << shf_mod64 - p_lo: Cell, - // 1 << (64 - shf_mod64) - p_hi: Cell, - // shift < 256 - shf_lt256: IsZeroGadget, - // shf_div64 == 0 - shf_div64_eq0: IsZeroGadget, - // shf_div64 == 1 - shf_div64_eq1: IsEqualGadget, - // shf_div64 == 2 - shf_div64_eq2: IsEqualGadget, - // a64s_lo[idx] < p_lo - a64s_lo_lt_p_lo: [LtGadget; 4], -} - -impl ShrWordsGadget { - pub(crate) fn construct( - cb: &mut ConstraintBuilder, - a: util::Word, - shift: util::Word, - ) -> Self { - let b = cb.query_word(); - let a64s = array_init(|_| cb.query_cell()); - let b64s = array_init(|_| cb.query_cell()); - let a64s_lo = array_init(|_| cb.query_cell()); - let a64s_hi = array_init(|_| cb.query_cell()); - let shf_div64 = cb.query_cell(); - let shf_mod64 = cb.query_cell(); - let p_lo = cb.query_cell(); - let p_hi = cb.query_cell(); - let shf_lt256 = IsZeroGadget::construct(cb, sum::expr(&shift.cells[1..32])); - for idx in 0..4 { - let offset = idx * N_BYTES_U64; - - // a64s constraint - cb.require_equal( - "a64s[idx] == from_bytes(a[8 * idx..8 * (idx + 1)])", - a64s[idx].expr(), - from_bytes::expr(&a.cells[offset..offset + N_BYTES_U64]), - ); - - // b64s constraint - cb.require_equal( - "b64s[idx] * shf_lt256 == from_bytes(b[8 * idx..8 * (idx + 1)])", - b64s[idx].expr() * shf_lt256.expr(), - from_bytes::expr(&b.cells[offset..offset + N_BYTES_U64]), - ); - - cb.require_equal( - "a64s[idx] == a64s_lo[idx] + a64s_hi[idx] * p_lo", - a64s[idx].expr(), - a64s_lo[idx].expr() + a64s_hi[idx].expr() * p_lo.expr(), - ); - } - - // a64s_lo[idx] < p_lo - let a64s_lo_lt_p_lo = array_init(|idx| { - let lt = LtGadget::construct(cb, a64s_lo[idx].expr(), p_lo.expr()); - cb.require_equal("a64s_lo[idx] < p_lo", lt.expr(), 1.expr()); - lt - }); - - // merge contraints - let shf_div64_eq0 = IsZeroGadget::construct(cb, shf_div64.expr()); - let shf_div64_eq1 = IsEqualGadget::construct(cb, shf_div64.expr(), 1.expr()); - let shf_div64_eq2 = IsEqualGadget::construct(cb, shf_div64.expr(), 2.expr()); - cb.require_equal( - "Constrain b64s[0]", - b64s[0].expr(), - (a64s_hi[0].expr() + a64s_lo[1].expr() * p_hi.expr()) * shf_div64_eq0.expr() - + (a64s_hi[1].expr() + a64s_lo[2].expr() * p_hi.expr()) * shf_div64_eq1.expr() - + (a64s_hi[2].expr() + a64s_lo[3].expr() * p_hi.expr()) * shf_div64_eq2.expr() - + a64s_hi[3].expr() - * (1.expr() - - shf_div64_eq0.expr() - - shf_div64_eq1.expr() - - shf_div64_eq2.expr()), - ); - cb.require_equal( - "Constrain b64s[1]", - b64s[1].expr(), - (a64s_hi[1].expr() + a64s_lo[2].expr() * p_hi.expr()) * shf_div64_eq0.expr() - + (a64s_hi[2].expr() + a64s_lo[3].expr() * p_hi.expr()) * shf_div64_eq1.expr() - + a64s_hi[3].expr() * shf_div64_eq2.expr(), - ); - cb.require_equal( - "Constrain b64s[2]", - b64s[2].expr(), - (a64s_hi[2].expr() + a64s_lo[3].expr() * p_hi.expr()) * shf_div64_eq0.expr() - + a64s_hi[3].expr() * shf_div64_eq1.expr(), - ); - cb.require_equal( - "Constrain b64s[3]", - b64s[3].expr(), - a64s_hi[3].expr() * shf_div64_eq0.expr(), - ); - - // shift constraint - cb.require_equal( - "shift[0] == shf_mod64 + shf_div64 * 64", - shift.cells[0].expr(), - shf_mod64.expr() + shf_div64.expr() * 64.expr(), - ); - - // p_lo == pow(2, shf_mod64) - cb.add_lookup( - "Pow2 lookup", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [shf_mod64.expr(), p_lo.expr(), 0.expr()], - }, - ); - - // p_hi == pow(2, 64 - shf_mod64) - cb.add_lookup( - "Pow2 lookup", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [64.expr() - shf_mod64.expr(), p_hi.expr(), 0.expr()], - }, - ); - - Self { - a, - shift, - b, - a64s, - b64s, - a64s_lo, - a64s_hi, - shf_div64, - shf_mod64, - p_lo, - p_hi, - shf_lt256, - shf_div64_eq0, - shf_div64_eq1, - shf_div64_eq2, - a64s_lo_lt_p_lo, - } - } - - pub(crate) fn assign( - &self, - region: &mut CachedRegion<'_, '_, F>, - offset: usize, - a: Word, - shift: Word, - b: Word, - ) -> Result<(), Error> { - self.assign_witness(region, offset, &a, &shift)?; - self.a.assign(region, offset, Some(a.to_le_bytes()))?; - self.shift - .assign(region, offset, Some(shift.to_le_bytes()))?; - self.b.assign(region, offset, Some(b.to_le_bytes()))?; - Ok(()) - } - - pub(crate) fn b(&self) -> &util::Word { - &self.b - } - - fn assign_witness( - &self, - region: &mut CachedRegion<'_, '_, F>, - offset: usize, - a: &Word, - shift: &Word, - ) -> Result<(), Error> { - let shf0 = shift.to_le_bytes()[0] as usize; - let shf_div64 = shf0 / 64; - let shf_mod64 = shf0 % 64; - let p_lo: u128 = 1 << shf_mod64; - let p_hi: u128 = 1 << (64 - shf_mod64); - let shf_lt256 = shift - .to_le_bytes() - .iter() - .fold(0, |acc, val| acc + *val as u128) - - shf0 as u128; - let a64s = a.0; - let mut a64s_lo = [0_u128; 4]; - let mut a64s_hi = [0_u128; 4]; - for idx in 0..4 { - a64s_lo[idx] = u128::from(a64s[idx]) % p_lo; - a64s_hi[idx] = u128::from(a64s[idx]) / p_lo; - } - let mut b64s = [0_u128; 4]; - b64s[3 - shf_div64 as usize] = a64s_hi[3]; - for k in 0..3 - shf_div64 { - b64s[k] = a64s_hi[k + shf_div64] + a64s_lo[k + shf_div64 + 1] * p_hi; - } - self.a64s - .iter() - .zip(a64s.iter()) - .map(|(cell, val)| cell.assign(region, offset, Some(F::from(*val)))) - .collect::, _>>()?; - self.b64s - .iter() - .zip(b64s.iter()) - .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) - .collect::, _>>()?; - self.a64s_lo - .iter() - .zip(a64s_lo.iter()) - .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) - .collect::, _>>()?; - self.a64s_hi - .iter() - .zip(a64s_hi.iter()) - .map(|(cell, val)| cell.assign(region, offset, Some(F::from_u128(*val)))) - .collect::, _>>()?; - self.shf_div64 - .assign(region, offset, Some(F::from(shf_div64 as u64)))?; - self.shf_mod64 - .assign(region, offset, Some(F::from(shf_mod64 as u64)))?; - self.p_lo.assign(region, offset, Some(F::from_u128(p_lo)))?; - self.p_hi.assign(region, offset, Some(F::from_u128(p_hi)))?; - self.shf_lt256 - .assign(region, offset, F::from_u128(shf_lt256))?; - self.shf_div64_eq0 - .assign(region, offset, F::from(shf_div64 as u64))?; - self.shf_div64_eq1 - .assign(region, offset, F::from(shf_div64 as u64), F::from(1))?; - self.shf_div64_eq2 - .assign(region, offset, F::from(shf_div64 as u64), F::from(2))?; - self.a64s_lo_lt_p_lo - .iter() - .zip(a64s_lo.iter()) - .map(|(lt, val)| lt.assign(region, offset, F::from_u128(*val), F::from_u128(p_lo))) - .collect::, _>>()?; - Ok(()) - } -} From df635e7c762d70f2d00a7b26e5f3d8c27fb0fc2a Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Tue, 14 Jun 2022 14:10:15 +0800 Subject: [PATCH 06/22] Use `generate_lagrange_base_polynomial` to check opcode (as `is_mul`) and sperate the word array to `quotient`, `divisor`, `remiander` and `dividend`. --- .../execution/mul_div_mod_shl_shr.rs | 117 +++++++----------- 1 file changed, 46 insertions(+), 71 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index f9c0f17c39..dd8899ef96 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -6,7 +6,9 @@ use crate::{ self, common_gadget::SameContextGadget, constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, - math_gadget::{IsZeroGadget, LtWordGadget, MulAddWordsGadget}, + math_gadget::{ + generate_lagrange_base_polynomial, IsZeroGadget, LtWordGadget, MulAddWordsGadget, + }, sum, CachedRegion, Cell, }, witness::{Block, Call, ExecStep, Transaction}, @@ -27,9 +29,12 @@ use halo2_proofs::plonk::{Error, Expression}; #[derive(Clone, Debug)] pub(crate) struct MulDivModShlShrGadget { same_context: SameContextGadget, - /// Words quotient, divisor, remainder, dividend and - /// pop1 (used for shift value of SHL and SHR) - pub words: [util::Word; 5], + quotient: util::Word, + divisor: util::Word, + remainder: util::Word, + dividend: util::Word, + /// Shift word used for opcode SHL and SHR + pop1: util::Word, /// Gadget that verifies quotient * divisor + remainder = dividend mul_add_words: MulAddWordsGadget, /// Check if divisor is zero for opcode DIV, MOD and SHR @@ -47,11 +52,11 @@ impl ExecutionGadget for MulDivModShlShrGadget { fn configure(cb: &mut ConstraintBuilder) -> Self { let opcode = cb.query_cell(); - let is_mul = is_mul(&opcode); - let is_div = is_div(&opcode); - let is_mod = is_mod(&opcode); - let is_shl = is_shl(&opcode); - let is_shr = is_shr(&opcode); + let is_mul = is_opcode(&opcode, OpcodeId::MUL); + let is_div = is_opcode(&opcode, OpcodeId::DIV); + let is_mod = is_opcode(&opcode, OpcodeId::MOD); + let is_shl = is_opcode(&opcode, OpcodeId::SHL); + let is_shr = is_opcode(&opcode, OpcodeId::SHR); let quotient = cb.query_word(); let divisor = cb.query_word(); @@ -118,7 +123,11 @@ impl ExecutionGadget for MulDivModShlShrGadget { Self { same_context, - words: [quotient, divisor, remainder, dividend, pop1], + quotient, + divisor, + remainder, + dividend, + pop1, mul_add_words, divisor_is_zero, remainder_is_zero, @@ -139,13 +148,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); - // Shift values are only used for opcode SHL and SHR. + // First byte of shift word used for opcode SHL and SHR let shf0 = pop1.to_le_bytes()[0]; - let shf_lt256 = pop1 - .to_le_bytes() - .iter() - .fold(0, |acc, val| acc + *val as u128) - - shf0 as u128; let (quotient, divisor, remainder, dividend) = match step.opcode.unwrap() { OpcodeId::MUL => (pop1, pop2, U256::from(0), push), @@ -162,7 +166,7 @@ impl ExecutionGadget for MulDivModShlShrGadget { ), OpcodeId::SHL => ( pop2, - if shf_lt256 == 0 { + if U256::from(shf0) == pop1 { U256::from(1) << shf0 } else { U256::from(0) @@ -171,7 +175,7 @@ impl ExecutionGadget for MulDivModShlShrGadget { push, ), OpcodeId::SHR => { - let divisor = if shf_lt256 == 0 { + let divisor = if U256::from(shf0) == pop1 { U256::from(1) << shf0 } else { U256::from(0) @@ -180,11 +184,16 @@ impl ExecutionGadget for MulDivModShlShrGadget { } _ => unreachable!(), }; - self.words[0].assign(region, offset, Some(quotient.to_le_bytes()))?; - self.words[1].assign(region, offset, Some(divisor.to_le_bytes()))?; - self.words[2].assign(region, offset, Some(remainder.to_le_bytes()))?; - self.words[3].assign(region, offset, Some(dividend.to_le_bytes()))?; - self.words[4].assign(region, offset, Some(pop1.to_le_bytes()))?; + + self.quotient + .assign(region, offset, Some(quotient.to_le_bytes()))?; + self.divisor + .assign(region, offset, Some(divisor.to_le_bytes()))?; + self.remainder + .assign(region, offset, Some(remainder.to_le_bytes()))?; + self.dividend + .assign(region, offset, Some(dividend.to_le_bytes()))?; + self.pop1.assign(region, offset, Some(pop1.to_le_bytes()))?; self.mul_add_words .assign(region, offset, [quotient, divisor, remainder, dividend])?; let divisor_sum = (0..32).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); @@ -198,55 +207,21 @@ impl ExecutionGadget for MulDivModShlShrGadget { } } -// The opcode value for MUL, DIV, MOD, SHL and SHR are 2, 4, 6, 0x1b and 0x1c. -// When the opcode is MUL, the result of below formula is 5200: -// (DIV - opcode) * (MOD- opcode) * (SHL - opcode) * (SHR - opcode) -// To make `is_mul` be either 0 or 1, the result needs to be divided by 5200, -// which is equivalent to multiply it by inversion of 5200. -// And calculate `is_div`, `is_mod`, `is_shl` and `is_shr` respectively. -#[inline] -fn is_mul(opcode: &Cell) -> Expression { - (OpcodeId::DIV.expr() - opcode.expr()) - * (OpcodeId::MOD.expr() - opcode.expr()) - * (OpcodeId::SHL.expr() - opcode.expr()) - * (OpcodeId::SHR.expr() - opcode.expr()) - * F::from(5200).invert().unwrap() -} - -#[inline] -fn is_div(opcode: &Cell) -> Expression { - (opcode.expr() - OpcodeId::MUL.expr()) - * (OpcodeId::MOD.expr() - opcode.expr()) - * (OpcodeId::SHL.expr() - opcode.expr()) - * (OpcodeId::SHR.expr() - opcode.expr()) - * F::from(2208).invert().unwrap() -} - -#[inline] -fn is_mod(opcode: &Cell) -> Expression { - (opcode.expr() - OpcodeId::MUL.expr()) - * (opcode.expr() - OpcodeId::DIV.expr()) - * (OpcodeId::SHL.expr() - opcode.expr()) - * (OpcodeId::SHR.expr() - opcode.expr()) - * F::from(3696).invert().unwrap() -} - -#[inline] -fn is_shl(opcode: &Cell) -> Expression { - (opcode.expr() - OpcodeId::MUL.expr()) - * (opcode.expr() - OpcodeId::DIV.expr()) - * (opcode.expr() - OpcodeId::MOD.expr()) - * (OpcodeId::SHR.expr() - opcode.expr()) - * F::from(12075).invert().unwrap() -} - #[inline] -fn is_shr(opcode: &Cell) -> Expression { - (opcode.expr() - OpcodeId::MUL.expr()) - * (opcode.expr() - OpcodeId::DIV.expr()) - * (opcode.expr() - OpcodeId::MOD.expr()) - * (opcode.expr() - OpcodeId::SHL.expr()) - * F::from(13728).invert().unwrap() +fn is_opcode(opcode: &Cell, opcode_id: OpcodeId) -> Expression { + generate_lagrange_base_polynomial( + opcode, + opcode_id.as_u8() as usize, + [ + OpcodeId::MUL, + OpcodeId::DIV, + OpcodeId::MOD, + OpcodeId::SHL, + OpcodeId::SHR, + ] + .into_iter() + .map(|op_id| op_id.as_u8() as usize), + ) } #[cfg(test)] From 0f5935186a9cd2853e8231efeb9990343b395547 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Tue, 14 Jun 2022 14:35:26 +0800 Subject: [PATCH 07/22] Add a constraint `pop1 == pop1.cells[0] when divisor != 0 for opcode SHL and SHR`. --- .../src/evm_circuit/execution/mul_div_mod_shl_shr.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index dd8899ef96..b61b4efd45 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -105,6 +105,13 @@ impl ExecutionGadget for MulDivModShlShrGadget { (is_div.clone() + is_mod.clone() + is_shr.clone()) * mul_add_words.overflow(), ); + cb.require_zero( + "pop1 == pop1.cells[0] when divisor != 0 for opcode SHL and SHR", + (is_shl.clone() + is_shr.clone()) + * (1.expr() - divisor_is_zero.expr()) + * (pop1.expr() - pop1.cells[0].expr()), + ); + let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() + is_div * OpcodeId::DIV.constant_gas_cost().expr() + is_mod * OpcodeId::MOD.constant_gas_cost().expr() From 7d187eddf4889b3022f3a3429252f63b1f0a1c58 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 15 Jun 2022 08:20:35 +0800 Subject: [PATCH 08/22] Add `shf_mod64` and `shf_div64` lookup constraints for opcode `SHL` and `SHR`. --- .../execution/mul_div_mod_shl_shr.rs | 77 ++++++++++++++++--- 1 file changed, 67 insertions(+), 10 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index b61b4efd45..76f193dc5a 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -2,14 +2,16 @@ use crate::{ evm_circuit::{ execution::ExecutionGadget, step::ExecutionState, + table::{FixedTableTag, Lookup}, util::{ self, common_gadget::SameContextGadget, constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, + from_bytes, math_gadget::{ generate_lagrange_base_polynomial, IsZeroGadget, LtWordGadget, MulAddWordsGadget, }, - sum, CachedRegion, Cell, + select, sum, CachedRegion, Cell, }, witness::{Block, Call, ExecStep, Transaction}, }, @@ -35,11 +37,19 @@ pub(crate) struct MulDivModShlShrGadget { dividend: util::Word, /// Shift word used for opcode SHL and SHR pop1: util::Word, + /// shift[0] / 64, will check if it is equal with high-16 bytes of divisor + /// for opcode SHL and SHR + shf_div64: Cell, + /// shift[0] % 64, will check if it is equal with low-16 bytes of divisor + /// for opcode SHL and SHR + shf_mod64: Cell, /// Gadget that verifies quotient * divisor + remainder = dividend mul_add_words: MulAddWordsGadget, - /// Check if divisor is zero for opcode DIV, MOD and SHR - divisor_is_zero: IsZeroGadget, - /// Check if remainder is zero for opcode MUL and SHL + /// Check if low-16 bytes of divisor is zero + divisor_lo_is_zero: IsZeroGadget, + /// Check if high-16 bytes of divisor is zero + divisor_hi_is_zero: IsZeroGadget, + /// Check if remainder is zero remainder_is_zero: IsZeroGadget, /// Check if remainder < divisor when divisor != 0 remainder_lt_divisor: LtWordGadget, @@ -63,10 +73,14 @@ impl ExecutionGadget for MulDivModShlShrGadget { let remainder = cb.query_word(); let dividend = cb.query_word(); let pop1 = cb.query_word(); + let shf_div64 = cb.query_cell(); + let shf_mod64 = cb.query_cell(); let mul_add_words = MulAddWordsGadget::construct(cb, ["ient, &divisor, &remainder, ÷nd]); - let divisor_is_zero = IsZeroGadget::construct(cb, sum::expr(&divisor.cells)); + let divisor_lo_is_zero = IsZeroGadget::construct(cb, sum::expr(&divisor.cells[..16])); + let divisor_hi_is_zero = IsZeroGadget::construct(cb, sum::expr(&divisor.cells[16..])); + let divisor_is_zero = divisor_lo_is_zero.expr() * divisor_hi_is_zero.expr(); let remainder_is_zero = IsZeroGadget::construct(cb, sum::expr(&remainder.cells)); let remainder_lt_divisor = LtWordGadget::construct(cb, &remainder, &divisor); @@ -112,6 +126,37 @@ impl ExecutionGadget for MulDivModShlShrGadget { * (pop1.expr() - pop1.cells[0].expr()), ); + // Constrain `divisor_lo = 2^shf_mod64` when `divisor_lo != 0`, and + // `divisor_hi = 2^shf_div64` when `divisor_hi != 0` for opcode SHL and SHR. + let divisor_lo = from_bytes::expr(&divisor.cells[..16]); + let divisor_hi = from_bytes::expr(&divisor.cells[16..]); + let is_valid_shf_lo = + (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_lo_is_zero.expr()); + let is_valid_shf_hi = + (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_hi_is_zero.expr()); + cb.add_lookup( + "Pow2 lookup of shf_mod64 and divisor_lo for opcode SHL and SHR", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [ + select::expr(is_valid_shf_lo.expr(), shf_mod64.expr(), 0.expr()), + select::expr(is_valid_shf_lo.expr(), divisor_lo.expr(), 1.expr()), + 0.expr(), + ], + }, + ); + cb.add_lookup( + "Pow2 lookup of shf_div64 and divisor_hi for opcode SHL and SHR", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [ + select::expr(is_valid_shf_hi.expr(), shf_div64.expr(), 0.expr()), + select::expr(is_valid_shf_hi.expr(), divisor_hi.expr(), 1.expr()), + 0.expr(), + ], + }, + ); + let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() + is_div * OpcodeId::DIV.constant_gas_cost().expr() + is_mod * OpcodeId::MOD.constant_gas_cost().expr() @@ -135,8 +180,11 @@ impl ExecutionGadget for MulDivModShlShrGadget { remainder, dividend, pop1, + shf_div64, + shf_mod64, mul_add_words, - divisor_is_zero, + divisor_lo_is_zero, + divisor_hi_is_zero, remainder_is_zero, remainder_lt_divisor, } @@ -155,8 +203,10 @@ impl ExecutionGadget for MulDivModShlShrGadget { let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); - // First byte of shift word used for opcode SHL and SHR + // Shift values are used for opcode SHL and SHR. let shf0 = pop1.to_le_bytes()[0]; + let shf_div64 = shf0 / 64; + let shf_mod64 = shf0 % 64; let (quotient, divisor, remainder, dividend) = match step.opcode.unwrap() { OpcodeId::MUL => (pop1, pop2, U256::from(0), push), @@ -201,11 +251,18 @@ impl ExecutionGadget for MulDivModShlShrGadget { self.dividend .assign(region, offset, Some(dividend.to_le_bytes()))?; self.pop1.assign(region, offset, Some(pop1.to_le_bytes()))?; + self.shf_div64 + .assign(region, offset, Some(u64::from(shf_div64).into()))?; + self.shf_mod64 + .assign(region, offset, Some(u64::from(shf_mod64).into()))?; self.mul_add_words .assign(region, offset, [quotient, divisor, remainder, dividend])?; - let divisor_sum = (0..32).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); - self.divisor_is_zero - .assign(region, offset, F::from(divisor_sum))?; + let divisor_lo_sum = (0..16).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); + let divisor_hi_sum = (16..32).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); + self.divisor_lo_is_zero + .assign(region, offset, F::from(divisor_lo_sum))?; + self.divisor_hi_is_zero + .assign(region, offset, F::from(divisor_hi_sum))?; let remainder_sum = (0..32).fold(0, |acc, idx| acc + remainder.byte(idx) as u64); self.remainder_is_zero .assign(region, offset, F::from(remainder_sum))?; From 45a37bd9b180d5f8aafb11535830173bb1221525 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 15 Jun 2022 08:25:18 +0800 Subject: [PATCH 09/22] Fix Infra doc issue. --- .../src/evm_circuit/execution/mul_div_mod_shl_shr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index 76f193dc5a..9dd87ecb19 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -37,10 +37,10 @@ pub(crate) struct MulDivModShlShrGadget { dividend: util::Word, /// Shift word used for opcode SHL and SHR pop1: util::Word, - /// shift[0] / 64, will check if it is equal with high-16 bytes of divisor + /// `shift[0] / 64`, will check if it is equal with high-16 bytes of divisor /// for opcode SHL and SHR shf_div64: Cell, - /// shift[0] % 64, will check if it is equal with low-16 bytes of divisor + /// `shift[0] % 64`, will check if it is equal with low-16 bytes of divisor /// for opcode SHL and SHR shf_mod64: Cell, /// Gadget that verifies quotient * divisor + remainder = dividend From dbcb8346c2f23e239a49e87892df684c9b26baa8 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 15 Jun 2022 09:29:05 +0800 Subject: [PATCH 10/22] Fix `shf_div64` and `shf_mod64` to `shf_div128` and `shf_mod128`. --- .../execution/mul_div_mod_shl_shr.rs | 48 +++++++++++-------- zkevm-circuits/src/evm_circuit/table.rs | 2 +- 2 files changed, 28 insertions(+), 22 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index 9dd87ecb19..67bb78a72c 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -37,12 +37,12 @@ pub(crate) struct MulDivModShlShrGadget { dividend: util::Word, /// Shift word used for opcode SHL and SHR pop1: util::Word, - /// `shift[0] / 64`, will check if it is equal with high-16 bytes of divisor + /// `shift[0] / 128`, will check if it is equal with high-16 bytes of + /// divisor for opcode SHL and SHR + shf_div128: Cell, + /// `shift[0] % 128`, will check if it is equal with low-16 bytes of divisor /// for opcode SHL and SHR - shf_div64: Cell, - /// `shift[0] % 64`, will check if it is equal with low-16 bytes of divisor - /// for opcode SHL and SHR - shf_mod64: Cell, + shf_mod128: Cell, /// Gadget that verifies quotient * divisor + remainder = dividend mul_add_words: MulAddWordsGadget, /// Check if low-16 bytes of divisor is zero @@ -73,8 +73,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { let remainder = cb.query_word(); let dividend = cb.query_word(); let pop1 = cb.query_word(); - let shf_div64 = cb.query_cell(); - let shf_mod64 = cb.query_cell(); + let shf_div128 = cb.query_cell(); + let shf_mod128 = cb.query_cell(); let mul_add_words = MulAddWordsGadget::construct(cb, ["ient, &divisor, &remainder, ÷nd]); @@ -126,8 +126,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { * (pop1.expr() - pop1.cells[0].expr()), ); - // Constrain `divisor_lo = 2^shf_mod64` when `divisor_lo != 0`, and - // `divisor_hi = 2^shf_div64` when `divisor_hi != 0` for opcode SHL and SHR. + // Constrain `divisor_lo = 2^shf_mod128` when `divisor_lo != 0`, and + // `divisor_hi = 2^shf_div128` when `divisor_hi != 0` for opcode SHL and SHR. let divisor_lo = from_bytes::expr(&divisor.cells[..16]); let divisor_hi = from_bytes::expr(&divisor.cells[16..]); let is_valid_shf_lo = @@ -135,22 +135,22 @@ impl ExecutionGadget for MulDivModShlShrGadget { let is_valid_shf_hi = (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_hi_is_zero.expr()); cb.add_lookup( - "Pow2 lookup of shf_mod64 and divisor_lo for opcode SHL and SHR", + "Pow2 lookup of shf_mod128 and divisor_lo for opcode SHL and SHR", Lookup::Fixed { tag: FixedTableTag::Pow2.expr(), values: [ - select::expr(is_valid_shf_lo.expr(), shf_mod64.expr(), 0.expr()), + select::expr(is_valid_shf_lo.expr(), shf_mod128.expr(), 0.expr()), select::expr(is_valid_shf_lo.expr(), divisor_lo.expr(), 1.expr()), 0.expr(), ], }, ); cb.add_lookup( - "Pow2 lookup of shf_div64 and divisor_hi for opcode SHL and SHR", + "Pow2 lookup of shf_div128 and divisor_hi for opcode SHL and SHR", Lookup::Fixed { tag: FixedTableTag::Pow2.expr(), values: [ - select::expr(is_valid_shf_hi.expr(), shf_div64.expr(), 0.expr()), + select::expr(is_valid_shf_hi.expr(), shf_div128.expr(), 0.expr()), select::expr(is_valid_shf_hi.expr(), divisor_hi.expr(), 1.expr()), 0.expr(), ], @@ -180,8 +180,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { remainder, dividend, pop1, - shf_div64, - shf_mod64, + shf_div128, + shf_mod128, mul_add_words, divisor_lo_is_zero, divisor_hi_is_zero, @@ -205,8 +205,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { // Shift values are used for opcode SHL and SHR. let shf0 = pop1.to_le_bytes()[0]; - let shf_div64 = shf0 / 64; - let shf_mod64 = shf0 % 64; + let shf_div128 = shf0 / 128; + let shf_mod128 = shf0 % 128; let (quotient, divisor, remainder, dividend) = match step.opcode.unwrap() { OpcodeId::MUL => (pop1, pop2, U256::from(0), push), @@ -251,10 +251,10 @@ impl ExecutionGadget for MulDivModShlShrGadget { self.dividend .assign(region, offset, Some(dividend.to_le_bytes()))?; self.pop1.assign(region, offset, Some(pop1.to_le_bytes()))?; - self.shf_div64 - .assign(region, offset, Some(u64::from(shf_div64).into()))?; - self.shf_mod64 - .assign(region, offset, Some(u64::from(shf_mod64).into()))?; + self.shf_div128 + .assign(region, offset, Some(u64::from(shf_div128).into()))?; + self.shf_mod128 + .assign(region, offset, Some(u64::from(shf_mod128).into()))?; self.mul_add_words .assign(region, offset, [quotient, divisor, remainder, dividend])?; let divisor_lo_sum = (0..16).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); @@ -375,16 +375,22 @@ mod test { #[test] fn shr_gadget_tests() { + /* test_ok(OpcodeId::SHR, Word::from(0xABCD), Word::from(8)); test_ok(OpcodeId::SHR, Word::from(0x1234), Word::from(7)); test_ok(OpcodeId::SHR, Word::from(0x8765), Word::from(17)); test_ok(OpcodeId::SHR, Word::from(0x4321), Word::from(0)); test_ok(OpcodeId::SHR, Word::from(0xFFFF), Word::from(256)); test_ok(OpcodeId::SHR, Word::from(0x12345), Word::from(256 + 8 + 1)); + */ let max_word = Word::from_big_endian(&[255_u8; 32]); + /* test_ok(OpcodeId::SHR, max_word, Word::from(63)); test_ok(OpcodeId::SHR, max_word, Word::from(128)); + */ test_ok(OpcodeId::SHR, max_word, Word::from(129)); + /* test_ok(OpcodeId::SHR, rand_word(), rand_word()); + */ } } diff --git a/zkevm-circuits/src/evm_circuit/table.rs b/zkevm-circuits/src/evm_circuit/table.rs index cc94351f49..8c2086e3b5 100644 --- a/zkevm-circuits/src/evm_circuit/table.rs +++ b/zkevm-circuits/src/evm_circuit/table.rs @@ -103,7 +103,7 @@ impl FixedTableTag { }) })) } - Self::Pow2 => Box::new((0..65).map(move |value| { + Self::Pow2 => Box::new((0..128).map(move |value| { [ tag, F::from(value), From de5caed702fb9bfcf1dd4ce8803b171d46c3635b Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 15 Jun 2022 09:30:25 +0800 Subject: [PATCH 11/22] Delete commenting for tests. --- .../src/evm_circuit/execution/mul_div_mod_shl_shr.rs | 6 ------ 1 file changed, 6 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index 67bb78a72c..0f7a981390 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -375,22 +375,16 @@ mod test { #[test] fn shr_gadget_tests() { - /* test_ok(OpcodeId::SHR, Word::from(0xABCD), Word::from(8)); test_ok(OpcodeId::SHR, Word::from(0x1234), Word::from(7)); test_ok(OpcodeId::SHR, Word::from(0x8765), Word::from(17)); test_ok(OpcodeId::SHR, Word::from(0x4321), Word::from(0)); test_ok(OpcodeId::SHR, Word::from(0xFFFF), Word::from(256)); test_ok(OpcodeId::SHR, Word::from(0x12345), Word::from(256 + 8 + 1)); - */ let max_word = Word::from_big_endian(&[255_u8; 32]); - /* test_ok(OpcodeId::SHR, max_word, Word::from(63)); test_ok(OpcodeId::SHR, max_word, Word::from(128)); - */ test_ok(OpcodeId::SHR, max_word, Word::from(129)); - /* test_ok(OpcodeId::SHR, rand_word(), rand_word()); - */ } } From b0655f175d30b8323d4026ffb5afbedbce46c345 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 15 Jun 2022 10:18:25 +0800 Subject: [PATCH 12/22] Fix contraint `divisor_hi == shf_div128`. --- .../execution/mul_div_mod_shl_shr.rs | 42 ++++++++++++------- 1 file changed, 27 insertions(+), 15 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index 0f7a981390..b1b551f0d9 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -126,25 +126,30 @@ impl ExecutionGadget for MulDivModShlShrGadget { * (pop1.expr() - pop1.cells[0].expr()), ); - // Constrain `divisor_lo = 2^shf_mod128` when `divisor_lo != 0`, and - // `divisor_hi = 2^shf_div128` when `divisor_hi != 0` for opcode SHL and SHR. + // Constrain `divisor_lo == 2^shf_mod128` when `divisor_lo != 0`, and + // `divisor_hi == shf_div128` for opcode SHL and SHR. let divisor_lo = from_bytes::expr(&divisor.cells[..16]); let divisor_hi = from_bytes::expr(&divisor.cells[16..]); - let is_valid_shf_lo = - (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_lo_is_zero.expr()); - let is_valid_shf_hi = - (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_hi_is_zero.expr()); - cb.add_lookup( - "Pow2 lookup of shf_mod128 and divisor_lo for opcode SHL and SHR", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [ - select::expr(is_valid_shf_lo.expr(), shf_mod128.expr(), 0.expr()), - select::expr(is_valid_shf_lo.expr(), divisor_lo.expr(), 1.expr()), - 0.expr(), - ], + cb.condition( + (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_lo_is_zero.expr()), + |cb| { + cb.add_lookup( + "Pow2 lookup of shf_mod128 and divisor_lo for opcode SHL and SHR", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [shf_mod128.expr(), divisor_lo.expr(), 0.expr()], + }, + ); }, ); + cb.condition(is_shl.clone() + is_shr.clone(), |cb| { + cb.require_equal( + "divisor_hi == shf_div128 for opcode SHL and SHR ", + divisor_hi.expr(), + shf_div128.expr(), + ); + }); + /* cb.add_lookup( "Pow2 lookup of shf_div128 and divisor_hi for opcode SHL and SHR", Lookup::Fixed { @@ -156,6 +161,7 @@ impl ExecutionGadget for MulDivModShlShrGadget { ], }, ); + */ let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() + is_div * OpcodeId::DIV.constant_gas_cost().expr() @@ -375,16 +381,22 @@ mod test { #[test] fn shr_gadget_tests() { + /* test_ok(OpcodeId::SHR, Word::from(0xABCD), Word::from(8)); test_ok(OpcodeId::SHR, Word::from(0x1234), Word::from(7)); test_ok(OpcodeId::SHR, Word::from(0x8765), Word::from(17)); test_ok(OpcodeId::SHR, Word::from(0x4321), Word::from(0)); test_ok(OpcodeId::SHR, Word::from(0xFFFF), Word::from(256)); test_ok(OpcodeId::SHR, Word::from(0x12345), Word::from(256 + 8 + 1)); + */ let max_word = Word::from_big_endian(&[255_u8; 32]); + /* test_ok(OpcodeId::SHR, max_word, Word::from(63)); + */ test_ok(OpcodeId::SHR, max_word, Word::from(128)); + /* test_ok(OpcodeId::SHR, max_word, Word::from(129)); test_ok(OpcodeId::SHR, rand_word(), rand_word()); + */ } } From 51bd0a2d7da9982796b311778615db7f45b9e90c Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 15 Jun 2022 10:26:22 +0800 Subject: [PATCH 13/22] Fix clippy issue. --- zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index b1b551f0d9..aedef819d2 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -11,7 +11,7 @@ use crate::{ math_gadget::{ generate_lagrange_base_polynomial, IsZeroGadget, LtWordGadget, MulAddWordsGadget, }, - select, sum, CachedRegion, Cell, + sum, CachedRegion, Cell, }, witness::{Block, Call, ExecStep, Transaction}, }, From b99dc14f9f2a5204cfe9ac79beae918c2c44adb0 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 15 Jun 2022 10:53:10 +0800 Subject: [PATCH 14/22] Fix comments. --- .../execution/mul_div_mod_shl_shr.rs | 21 +------------------ 1 file changed, 1 insertion(+), 20 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index aedef819d2..84b04a0bcf 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -40,7 +40,7 @@ pub(crate) struct MulDivModShlShrGadget { /// `shift[0] / 128`, will check if it is equal with high-16 bytes of /// divisor for opcode SHL and SHR shf_div128: Cell, - /// `shift[0] % 128`, will check if it is equal with low-16 bytes of divisor + /// `shift[0] % 128`, will lookup with low-16 bytes of divisor in Pow2 table /// for opcode SHL and SHR shf_mod128: Cell, /// Gadget that verifies quotient * divisor + remainder = dividend @@ -149,19 +149,6 @@ impl ExecutionGadget for MulDivModShlShrGadget { shf_div128.expr(), ); }); - /* - cb.add_lookup( - "Pow2 lookup of shf_div128 and divisor_hi for opcode SHL and SHR", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [ - select::expr(is_valid_shf_hi.expr(), shf_div128.expr(), 0.expr()), - select::expr(is_valid_shf_hi.expr(), divisor_hi.expr(), 1.expr()), - 0.expr(), - ], - }, - ); - */ let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() + is_div * OpcodeId::DIV.constant_gas_cost().expr() @@ -381,22 +368,16 @@ mod test { #[test] fn shr_gadget_tests() { - /* test_ok(OpcodeId::SHR, Word::from(0xABCD), Word::from(8)); test_ok(OpcodeId::SHR, Word::from(0x1234), Word::from(7)); test_ok(OpcodeId::SHR, Word::from(0x8765), Word::from(17)); test_ok(OpcodeId::SHR, Word::from(0x4321), Word::from(0)); test_ok(OpcodeId::SHR, Word::from(0xFFFF), Word::from(256)); test_ok(OpcodeId::SHR, Word::from(0x12345), Word::from(256 + 8 + 1)); - */ let max_word = Word::from_big_endian(&[255_u8; 32]); - /* test_ok(OpcodeId::SHR, max_word, Word::from(63)); - */ test_ok(OpcodeId::SHR, max_word, Word::from(128)); - /* test_ok(OpcodeId::SHR, max_word, Word::from(129)); test_ok(OpcodeId::SHR, rand_word(), rand_word()); - */ } } From d450aaf3998ace9e04fd0f816c4190de43fde9e9 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 15 Jun 2022 12:21:00 +0800 Subject: [PATCH 15/22] Fix to `shf_lo` and `shf_hi`. --- .../execution/mul_div_mod_shl_shr.rs | 65 +++++++++++-------- 1 file changed, 37 insertions(+), 28 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index 84b04a0bcf..0e1540abb5 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -37,12 +37,12 @@ pub(crate) struct MulDivModShlShrGadget { dividend: util::Word, /// Shift word used for opcode SHL and SHR pop1: util::Word, - /// `shift[0] / 128`, will check if it is equal with high-16 bytes of - /// divisor for opcode SHL and SHR - shf_div128: Cell, - /// `shift[0] % 128`, will lookup with low-16 bytes of divisor in Pow2 table - /// for opcode SHL and SHR - shf_mod128: Cell, + /// For opcode SHL and SHR, it is `shift[0]` if `shift[0]` is less than 128, + /// and 0 otherwise. + shf_lo: Cell, + /// For opcode SHL and SHR, it is `shift[0] - 128` if `shift[0]` is greater + /// than or equal to 128, and 0 otherwise. + shf_hi: Cell, /// Gadget that verifies quotient * divisor + remainder = dividend mul_add_words: MulAddWordsGadget, /// Check if low-16 bytes of divisor is zero @@ -73,8 +73,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { let remainder = cb.query_word(); let dividend = cb.query_word(); let pop1 = cb.query_word(); - let shf_div128 = cb.query_cell(); - let shf_mod128 = cb.query_cell(); + let shf_lo = cb.query_cell(); + let shf_hi = cb.query_cell(); let mul_add_words = MulAddWordsGadget::construct(cb, ["ient, &divisor, &remainder, ÷nd]); @@ -126,29 +126,34 @@ impl ExecutionGadget for MulDivModShlShrGadget { * (pop1.expr() - pop1.cells[0].expr()), ); - // Constrain `divisor_lo == 2^shf_mod128` when `divisor_lo != 0`, and - // `divisor_hi == shf_div128` for opcode SHL and SHR. + // For opcode SHL and SHR, Constrain `divisor_lo == 2^shf_lo` when + // `divisor_lo != 0`, and `divisor_hi == 2^shf_hi` when `divisor_hi != 0`. let divisor_lo = from_bytes::expr(&divisor.cells[..16]); let divisor_hi = from_bytes::expr(&divisor.cells[16..]); cb.condition( (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_lo_is_zero.expr()), |cb| { cb.add_lookup( - "Pow2 lookup of shf_mod128 and divisor_lo for opcode SHL and SHR", + "Pow2 lookup of shf_lo and divisor_lo for opcode SHL and SHR", Lookup::Fixed { tag: FixedTableTag::Pow2.expr(), - values: [shf_mod128.expr(), divisor_lo.expr(), 0.expr()], + values: [shf_lo.expr(), divisor_lo.expr(), 0.expr()], + }, + ); + }, + ); + cb.condition( + (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_hi_is_zero.expr()), + |cb| { + cb.add_lookup( + "Pow2 lookup of shf_hi and divisor_hi for opcode SHL and SHR", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [shf_hi.expr(), divisor_hi.expr(), 0.expr()], }, ); }, ); - cb.condition(is_shl.clone() + is_shr.clone(), |cb| { - cb.require_equal( - "divisor_hi == shf_div128 for opcode SHL and SHR ", - divisor_hi.expr(), - shf_div128.expr(), - ); - }); let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() + is_div * OpcodeId::DIV.constant_gas_cost().expr() @@ -173,8 +178,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { remainder, dividend, pop1, - shf_div128, - shf_mod128, + shf_lo, + shf_hi, mul_add_words, divisor_lo_is_zero, divisor_hi_is_zero, @@ -196,10 +201,14 @@ impl ExecutionGadget for MulDivModShlShrGadget { let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); - // Shift values are used for opcode SHL and SHR. + // Get the first byte of shift value for opcode SHL and SHR. And split it by 128 + // to avoid overflow. let shf0 = pop1.to_le_bytes()[0]; - let shf_div128 = shf0 / 128; - let shf_mod128 = shf0 % 128; + let (shf_lo, shf_hi) = if shf0 < 128 { + (shf0, 0) + } else { + (0, shf0 - 128) + }; let (quotient, divisor, remainder, dividend) = match step.opcode.unwrap() { OpcodeId::MUL => (pop1, pop2, U256::from(0), push), @@ -244,10 +253,10 @@ impl ExecutionGadget for MulDivModShlShrGadget { self.dividend .assign(region, offset, Some(dividend.to_le_bytes()))?; self.pop1.assign(region, offset, Some(pop1.to_le_bytes()))?; - self.shf_div128 - .assign(region, offset, Some(u64::from(shf_div128).into()))?; - self.shf_mod128 - .assign(region, offset, Some(u64::from(shf_mod128).into()))?; + self.shf_lo + .assign(region, offset, Some(u64::from(shf_lo).into()))?; + self.shf_hi + .assign(region, offset, Some(u64::from(shf_hi).into()))?; self.mul_add_words .assign(region, offset, [quotient, divisor, remainder, dividend])?; let divisor_lo_sum = (0..16).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); From 98c0ef3ab635490883729061b2c5cf81980066c0 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Sun, 19 Jun 2022 07:56:50 +0800 Subject: [PATCH 16/22] Fix `Pow2` lookup table and update to use `shf0` for lookup. --- .../execution/mul_div_mod_shl_shr.rs | 87 ++++++------------- zkevm-circuits/src/evm_circuit/table.rs | 14 +-- 2 files changed, 32 insertions(+), 69 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index 0e1540abb5..5799e887c2 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -37,18 +37,12 @@ pub(crate) struct MulDivModShlShrGadget { dividend: util::Word, /// Shift word used for opcode SHL and SHR pop1: util::Word, - /// For opcode SHL and SHR, it is `shift[0]` if `shift[0]` is less than 128, - /// and 0 otherwise. - shf_lo: Cell, - /// For opcode SHL and SHR, it is `shift[0] - 128` if `shift[0]` is greater - /// than or equal to 128, and 0 otherwise. - shf_hi: Cell, + /// First byte of shift value for opcode SHL and SHR + shf0: Cell, /// Gadget that verifies quotient * divisor + remainder = dividend mul_add_words: MulAddWordsGadget, - /// Check if low-16 bytes of divisor is zero - divisor_lo_is_zero: IsZeroGadget, - /// Check if high-16 bytes of divisor is zero - divisor_hi_is_zero: IsZeroGadget, + /// Check if divisor is zero + divisor_is_zero: IsZeroGadget, /// Check if remainder is zero remainder_is_zero: IsZeroGadget, /// Check if remainder < divisor when divisor != 0 @@ -73,14 +67,11 @@ impl ExecutionGadget for MulDivModShlShrGadget { let remainder = cb.query_word(); let dividend = cb.query_word(); let pop1 = cb.query_word(); - let shf_lo = cb.query_cell(); - let shf_hi = cb.query_cell(); + let shf0 = cb.query_cell(); let mul_add_words = MulAddWordsGadget::construct(cb, ["ient, &divisor, &remainder, ÷nd]); - let divisor_lo_is_zero = IsZeroGadget::construct(cb, sum::expr(&divisor.cells[..16])); - let divisor_hi_is_zero = IsZeroGadget::construct(cb, sum::expr(&divisor.cells[16..])); - let divisor_is_zero = divisor_lo_is_zero.expr() * divisor_hi_is_zero.expr(); + let divisor_is_zero = IsZeroGadget::construct(cb, sum::expr(&divisor.cells)); let remainder_is_zero = IsZeroGadget::construct(cb, sum::expr(&remainder.cells)); let remainder_lt_divisor = LtWordGadget::construct(cb, &remainder, &divisor); @@ -126,34 +117,19 @@ impl ExecutionGadget for MulDivModShlShrGadget { * (pop1.expr() - pop1.cells[0].expr()), ); - // For opcode SHL and SHR, Constrain `divisor_lo == 2^shf_lo` when - // `divisor_lo != 0`, and `divisor_hi == 2^shf_hi` when `divisor_hi != 0`. + // For opcode SHL and SHR, constrain `divisor_lo == 2^shf0` when + // `shf0 < 128`, and `divisor_hi == 2^(128 - shf0)` otherwise. let divisor_lo = from_bytes::expr(&divisor.cells[..16]); let divisor_hi = from_bytes::expr(&divisor.cells[16..]); - cb.condition( - (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_lo_is_zero.expr()), - |cb| { - cb.add_lookup( - "Pow2 lookup of shf_lo and divisor_lo for opcode SHL and SHR", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [shf_lo.expr(), divisor_lo.expr(), 0.expr()], - }, - ); - }, - ); - cb.condition( - (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_hi_is_zero.expr()), - |cb| { - cb.add_lookup( - "Pow2 lookup of shf_hi and divisor_hi for opcode SHL and SHR", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [shf_hi.expr(), divisor_hi.expr(), 0.expr()], - }, - ); - }, - ); + cb.condition(is_shl.clone() + is_shr.clone(), |cb| { + cb.add_lookup( + "Pow2 lookup of shf0, divisor_lo and divisor_hi for opcode SHL and SHR", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [shf0.expr(), divisor_lo.expr(), divisor_hi.expr()], + }, + ); + }); let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() + is_div * OpcodeId::DIV.constant_gas_cost().expr() @@ -178,11 +154,9 @@ impl ExecutionGadget for MulDivModShlShrGadget { remainder, dividend, pop1, - shf_lo, - shf_hi, + shf0, mul_add_words, - divisor_lo_is_zero, - divisor_hi_is_zero, + divisor_is_zero, remainder_is_zero, remainder_lt_divisor, } @@ -201,14 +175,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); - // Get the first byte of shift value for opcode SHL and SHR. And split it by 128 - // to avoid overflow. + // Get the first byte of shift value only for opcode SHL and SHR. let shf0 = pop1.to_le_bytes()[0]; - let (shf_lo, shf_hi) = if shf0 < 128 { - (shf0, 0) - } else { - (0, shf0 - 128) - }; let (quotient, divisor, remainder, dividend) = match step.opcode.unwrap() { OpcodeId::MUL => (pop1, pop2, U256::from(0), push), @@ -253,18 +221,13 @@ impl ExecutionGadget for MulDivModShlShrGadget { self.dividend .assign(region, offset, Some(dividend.to_le_bytes()))?; self.pop1.assign(region, offset, Some(pop1.to_le_bytes()))?; - self.shf_lo - .assign(region, offset, Some(u64::from(shf_lo).into()))?; - self.shf_hi - .assign(region, offset, Some(u64::from(shf_hi).into()))?; + self.shf0 + .assign(region, offset, Some(u64::from(shf0).into()))?; self.mul_add_words .assign(region, offset, [quotient, divisor, remainder, dividend])?; - let divisor_lo_sum = (0..16).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); - let divisor_hi_sum = (16..32).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); - self.divisor_lo_is_zero - .assign(region, offset, F::from(divisor_lo_sum))?; - self.divisor_hi_is_zero - .assign(region, offset, F::from(divisor_hi_sum))?; + let divisor_sum = (0..32).fold(0, |acc, idx| acc + divisor.byte(idx) as u64); + self.divisor_is_zero + .assign(region, offset, F::from(divisor_sum))?; let remainder_sum = (0..32).fold(0, |acc, idx| acc + remainder.byte(idx) as u64); self.remainder_is_zero .assign(region, offset, F::from(remainder_sum))?; diff --git a/zkevm-circuits/src/evm_circuit/table.rs b/zkevm-circuits/src/evm_circuit/table.rs index 8c2086e3b5..26f5bbc1d3 100644 --- a/zkevm-circuits/src/evm_circuit/table.rs +++ b/zkevm-circuits/src/evm_circuit/table.rs @@ -103,13 +103,13 @@ impl FixedTableTag { }) })) } - Self::Pow2 => Box::new((0..128).map(move |value| { - [ - tag, - F::from(value), - F::from_u128(1_u128 << value), - F::zero(), - ] + Self::Pow2 => Box::new((0..256).map(move |value| { + let (pow_lo, pow_hi) = if value < 128 { + (F::from_u128(1_u128 << value), F::from(0)) + } else { + (F::from(0), F::from_u128(1 << (value - 128))) + }; + [tag, F::from(value), pow_lo, pow_hi] })), } } From eaba99680fe2ae682b197530ed4307fe8c5e6be1 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Sun, 19 Jun 2022 08:22:51 +0800 Subject: [PATCH 17/22] Add missing limit `divisor != 0` for `Pow2` lookup. --- .../execution/mul_div_mod_shl_shr.rs | 21 +++++++++++-------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs index 5799e887c2..403cd391a5 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs @@ -121,15 +121,18 @@ impl ExecutionGadget for MulDivModShlShrGadget { // `shf0 < 128`, and `divisor_hi == 2^(128 - shf0)` otherwise. let divisor_lo = from_bytes::expr(&divisor.cells[..16]); let divisor_hi = from_bytes::expr(&divisor.cells[16..]); - cb.condition(is_shl.clone() + is_shr.clone(), |cb| { - cb.add_lookup( - "Pow2 lookup of shf0, divisor_lo and divisor_hi for opcode SHL and SHR", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [shf0.expr(), divisor_lo.expr(), divisor_hi.expr()], - }, - ); - }); + cb.condition( + (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_is_zero.expr()), + |cb| { + cb.add_lookup( + "Pow2 lookup of shf0, divisor_lo and divisor_hi for opcode SHL and SHR", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [shf0.expr(), divisor_lo.expr(), divisor_hi.expr()], + }, + ); + }, + ); let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() + is_div * OpcodeId::DIV.constant_gas_cost().expr() From 26999d2c0735466f337fbb1eb5ec6049d8c806b8 Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Tue, 2 Aug 2022 15:20:51 +0800 Subject: [PATCH 18/22] Revert to only merge both opcode `SHL` and `SHR`. --- zkevm-circuits/src/evm_circuit/execution.rs | 17 +- .../src/evm_circuit/execution/mul_div_mod.rs | 238 ++++++++++++++++++ .../{mul_div_mod_shl_shr.rs => shl_shr.rs} | 192 ++++---------- zkevm-circuits/src/evm_circuit/step.rs | 16 +- zkevm-circuits/src/evm_circuit/witness.rs | 7 +- 5 files changed, 299 insertions(+), 171 deletions(-) create mode 100644 zkevm-circuits/src/evm_circuit/execution/mul_div_mod.rs rename zkevm-circuits/src/evm_circuit/execution/{mul_div_mod_shl_shr.rs => shl_shr.rs} (53%) diff --git a/zkevm-circuits/src/evm_circuit/execution.rs b/zkevm-circuits/src/evm_circuit/execution.rs index 5842eab784..bde0c6aab0 100644 --- a/zkevm-circuits/src/evm_circuit/execution.rs +++ b/zkevm-circuits/src/evm_circuit/execution.rs @@ -54,7 +54,7 @@ mod jumpi; mod logs; mod memory; mod msize; -mod mul_div_mod_shl_shr; +mod mul_div_mod; mod mulmod; mod not; mod origin; @@ -64,6 +64,7 @@ mod push; mod r#return; mod sdiv_smod; mod selfbalance; +mod shl_shr; mod signed_comparator; mod signextend; mod sload; @@ -102,7 +103,7 @@ use jumpi::JumpiGadget; use logs::LogGadget; use memory::MemoryGadget; use msize::MsizeGadget; -use mul_div_mod_shl_shr::MulDivModShlShrGadget; +use mul_div_mod::MulDivModGadget; use mulmod::MulModGadget; use not::NotGadget; use origin::OriginGadget; @@ -112,6 +113,7 @@ use push::PushGadget; use r#return::ReturnGadget; use sdiv_smod::SignedDivModGadget; use selfbalance::SelfbalanceGadget; +use shl_shr::ShlShrGadget; use signed_comparator::SignedComparatorGadget; use signextend::SignextendGadget; use sload::SloadGadget; @@ -179,7 +181,7 @@ pub(crate) struct ExecutionConfig { log_gadget: LogGadget, memory_gadget: MemoryGadget, msize_gadget: MsizeGadget, - mul_div_mod_shl_shr_gadget: MulDivModShlShrGadget, + mul_div_mod_gadget: MulDivModGadget, mulmod_gadget: MulModGadget, not_gadget: NotGadget, origin_gadget: OriginGadget, @@ -205,6 +207,7 @@ pub(crate) struct ExecutionConfig { create2_gadget: DummyGadget, staticcall_gadget: DummyGadget, selfdestruct_gadget: DummyGadget, + shl_shr_gadget: ShlShrGadget, signed_comparator_gadget: SignedComparatorGadget, signextend_gadget: SignextendGadget, sload_gadget: SloadGadget, @@ -388,7 +391,7 @@ impl ExecutionConfig { log_gadget: configure_gadget!(), memory_gadget: configure_gadget!(), msize_gadget: configure_gadget!(), - mul_div_mod_shl_shr_gadget: configure_gadget!(), + mul_div_mod_gadget: configure_gadget!(), mulmod_gadget: configure_gadget!(), not_gadget: configure_gadget!(), origin_gadget: configure_gadget!(), @@ -414,6 +417,7 @@ impl ExecutionConfig { create2_gadget: configure_gadget!(), staticcall_gadget: configure_gadget!(), selfdestruct_gadget: configure_gadget!(), + shl_shr_gadget: configure_gadget!(), signed_comparator_gadget: configure_gadget!(), signextend_gadget: configure_gadget!(), sload_gadget: configure_gadget!(), @@ -838,9 +842,7 @@ impl ExecutionConfig { ExecutionState::LOG => assign_exec_step!(self.log_gadget), ExecutionState::MEMORY => assign_exec_step!(self.memory_gadget), ExecutionState::MSIZE => assign_exec_step!(self.msize_gadget), - ExecutionState::MUL_DIV_MOD_SHL_SHR => { - assign_exec_step!(self.mul_div_mod_shl_shr_gadget) - } + ExecutionState::MUL_DIV_MOD => assign_exec_step!(self.mul_div_mod_gadget), ExecutionState::MULMOD => assign_exec_step!(self.mulmod_gadget), ExecutionState::NOT => assign_exec_step!(self.not_gadget), ExecutionState::ORIGIN => assign_exec_step!(self.origin_gadget), @@ -872,6 +874,7 @@ impl ExecutionConfig { ExecutionState::STATICCALL => assign_exec_step!(self.staticcall_gadget), ExecutionState::SELFDESTRUCT => assign_exec_step!(self.selfdestruct_gadget), // end of dummy gadgets + ExecutionState::SHL_SHR => assign_exec_step!(self.shl_shr_gadget), ExecutionState::SIGNEXTEND => assign_exec_step!(self.signextend_gadget), ExecutionState::SLOAD => assign_exec_step!(self.sload_gadget), ExecutionState::SSTORE => assign_exec_step!(self.sstore_gadget), diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod.rs b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod.rs new file mode 100644 index 0000000000..4b2384a624 --- /dev/null +++ b/zkevm-circuits/src/evm_circuit/execution/mul_div_mod.rs @@ -0,0 +1,238 @@ +use crate::{ + evm_circuit::{ + execution::ExecutionGadget, + step::ExecutionState, + util::{ + self, + common_gadget::SameContextGadget, + constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, + math_gadget::{IsZeroGadget, LtWordGadget, MulAddWordsGadget}, + select, sum, CachedRegion, + }, + witness::{Block, Call, ExecStep, Transaction}, + }, + util::Expr, +}; +use bus_mapping::evm::OpcodeId; +use eth_types::{Field, ToLittleEndian, U256}; +use halo2_proofs::plonk::Error; + +/// MulGadget verifies opcode MUL, DIV, and MOD. +/// For MUL, verify a * b = c (mod 2^256); +/// For DIV, verify a / b = c (mod 2^256); +/// For MOD, verify a % b = c (mod 2^256); +/// where a, b, c are 256-bit words. +#[derive(Clone, Debug)] +pub(crate) struct MulDivModGadget { + same_context: SameContextGadget, + /// Words a, b, c, d + pub words: [util::Word; 4], + /// Gadget that verifies a * b + c = d + mul_add_words: MulAddWordsGadget, + /// Check if divisor is zero for DIV and MOD + divisor_is_zero: IsZeroGadget, + /// Check if residue < divisor when divisor != 0 for DIV and MOD + lt_word: LtWordGadget, +} + +impl ExecutionGadget for MulDivModGadget { + const NAME: &'static str = "MUL_DIV_MOD"; + + const EXECUTION_STATE: ExecutionState = ExecutionState::MUL_DIV_MOD; + + fn configure(cb: &mut ConstraintBuilder) -> Self { + let opcode = cb.query_cell(); + + let is_mul = (OpcodeId::DIV.expr() - opcode.expr()) + * (OpcodeId::MOD.expr() - opcode.expr()) + * F::from(8).invert().unwrap(); + let is_div = (opcode.expr() - OpcodeId::MUL.expr()) + * (OpcodeId::MOD.expr() - opcode.expr()) + * F::from(4).invert().unwrap(); + let is_mod = (opcode.expr() - OpcodeId::MUL.expr()) + * (opcode.expr() - OpcodeId::DIV.expr()) + * F::from(8).invert().unwrap(); + let a = cb.query_word(); + let b = cb.query_word(); + let c = cb.query_word(); + let d = cb.query_word(); + + let mul_add_words = MulAddWordsGadget::construct(cb, [&a, &b, &c, &d]); + let divisor_is_zero = IsZeroGadget::construct(cb, sum::expr(&b.cells)); + let lt_word = LtWordGadget::construct(cb, &c, &b); + + // Pop a and b from the stack, push result on the stack + // The first pop is multiplier for MUL and dividend for DIV/MOD + // The second pop is multiplicand for MUL and divisor for DIV/MOD + // The push is product for MUL, quotient for DIV, and residue for MOD + // Note that for DIV/MOD, when divisor == 0, the push value is also 0. + cb.stack_pop(select::expr(is_mul.clone(), a.expr(), d.expr())); + cb.stack_pop(b.expr()); + cb.stack_push( + is_mul.clone() * d.expr() + + is_div * a.expr() * (1.expr() - divisor_is_zero.expr()) + + is_mod * c.expr() * (1.expr() - divisor_is_zero.expr()), + ); + + // Constraint for MUL case + cb.add_constraint( + "c == 0 for opcode MUL", + is_mul.clone() * sum::expr(&c.cells), + ); + + // Constraints for DIV and MOD cases + cb.condition(1.expr() - is_mul, |cb| { + cb.add_constraint( + "residue < divisor when divisor != 0 for opcode DIV/MOD", + (1.expr() - lt_word.expr()) * (1.expr() - divisor_is_zero.expr()), + ); + cb.require_zero("overflow == 0 for opcode DIV/MOD", mul_add_words.overflow()); + }); + + // State transition + let step_state_transition = StepStateTransition { + rw_counter: Delta(3.expr()), + program_counter: Delta(1.expr()), + stack_pointer: Delta(1.expr()), + gas_left: Delta(-OpcodeId::MUL.constant_gas_cost().expr()), + ..Default::default() + }; + let same_context = SameContextGadget::construct(cb, opcode, step_state_transition); + + Self { + words: [a, b, c, d], + same_context, + mul_add_words, + divisor_is_zero, + lt_word, + } + } + + fn assign_exec_step( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + block: &Block, + _: &Transaction, + _: &Call, + step: &ExecStep, + ) -> Result<(), Error> { + self.same_context.assign_exec_step(region, offset, step)?; + let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; + let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); + let (a, b, c, d) = match step.opcode.unwrap() { + OpcodeId::MUL => (pop1, pop2, U256::from(0), push), + OpcodeId::DIV => (push, pop2, pop1 - push * pop2, pop1), + OpcodeId::MOD => ( + if pop2.is_zero() { + U256::from(0) + } else { + pop1 / pop2 + }, + pop2, + if pop2.is_zero() { pop1 } else { push }, + pop1, + ), + _ => unreachable!(), + }; + self.words[0].assign(region, offset, Some(a.to_le_bytes()))?; + self.words[1].assign(region, offset, Some(b.to_le_bytes()))?; + self.words[2].assign(region, offset, Some(c.to_le_bytes()))?; + self.words[3].assign(region, offset, Some(d.to_le_bytes()))?; + self.mul_add_words.assign(region, offset, [a, b, c, d])?; + self.lt_word.assign(region, offset, c, b)?; + let b_sum = (0..32).fold(0, |acc, idx| acc + b.byte(idx) as u64); + self.divisor_is_zero + .assign(region, offset, F::from(b_sum))?; + Ok(()) + } +} + +#[cfg(test)] +mod test { + use crate::{evm_circuit::test::rand_word, test_util::run_test_circuits}; + use eth_types::evm_types::OpcodeId; + use eth_types::{bytecode, Word}; + use mock::TestContext; + + fn test_ok(opcode: OpcodeId, a: Word, b: Word) { + let bytecode = bytecode! { + PUSH32(b) + PUSH32(a) + #[start] + .write_op(opcode) + STOP + }; + + assert_eq!( + run_test_circuits( + TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(), + None + ), + Ok(()) + ); + } + + #[test] + fn mul_gadget_simple() { + test_ok(OpcodeId::MUL, 0x030201.into(), 0x060504.into()); + } + + #[test] + fn mul_gadget_overflow() { + let a = Word::from_dec_str("3402823669209384634633746074317682114560").unwrap(); // 2**128 * 10 + let b = Word::from_dec_str("34028236692093846346337460743176821145600").unwrap(); // 2**128 * 100 + test_ok(OpcodeId::MUL, a, b); + + let a = Word::from_dec_str("3402823669209384634633746074317682114560").unwrap(); // 2**128 * 10 + let b = Word::from_dec_str("34028236692093846346337460743176821145500").unwrap(); // (2**128 - 1) * 100 + test_ok(OpcodeId::MUL, a, b); + } + + #[test] + fn mul_gadget_rand() { + let a = rand_word(); + let b = rand_word(); + test_ok(OpcodeId::MUL, a, b); + } + + #[test] + fn div_gadget_simple() { + test_ok(OpcodeId::DIV, 0xFFFFFF.into(), 0xABC.into()); + test_ok(OpcodeId::DIV, 0xABC.into(), 0xFFFFFF.into()); + test_ok(OpcodeId::DIV, 0xFFFFFF.into(), 0xFFFFFFF.into()); + test_ok(OpcodeId::DIV, 0xABC.into(), 0.into()); + test_ok( + OpcodeId::DIV, + Word::from_big_endian(&[255u8; 32]), + 0xABCDEF.into(), + ); + } + + #[test] + fn div_gadget_rand() { + let dividend = rand_word(); + let divisor = rand_word(); + test_ok(OpcodeId::DIV, dividend, divisor); + } + + #[test] + fn mod_gadget_simple() { + test_ok(OpcodeId::MOD, 0xFFFFFF.into(), 0xABC.into()); + test_ok(OpcodeId::MOD, 0xABC.into(), 0xFFFFFF.into()); + test_ok(OpcodeId::MOD, 0xFFFFFF.into(), 0xFFFFFFF.into()); + test_ok(OpcodeId::MOD, 0xABC.into(), 0.into()); + test_ok( + OpcodeId::MOD, + Word::from_big_endian(&[255u8; 32]), + 0xABCDEF.into(), + ); + } + + #[test] + fn mod_gadget_rand() { + let dividend = rand_word(); + let divisor = rand_word(); + test_ok(OpcodeId::MOD, dividend, divisor); + } +} diff --git a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs similarity index 53% rename from zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs rename to zkevm-circuits/src/evm_circuit/execution/shl_shr.rs index 403cd391a5..b5b1f02b24 100644 --- a/zkevm-circuits/src/evm_circuit/execution/mul_div_mod_shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs @@ -8,9 +8,7 @@ use crate::{ common_gadget::SameContextGadget, constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, from_bytes, - math_gadget::{ - generate_lagrange_base_polynomial, IsZeroGadget, LtWordGadget, MulAddWordsGadget, - }, + math_gadget::{IsZeroGadget, LtWordGadget, MulAddWordsGadget}, sum, CachedRegion, Cell, }, witness::{Block, Call, ExecStep, Transaction}, @@ -19,25 +17,22 @@ use crate::{ }; use bus_mapping::evm::OpcodeId; use eth_types::{Field, ToLittleEndian, U256}; -use halo2_proofs::plonk::{Error, Expression}; +use halo2_proofs::plonk::Error; -/// MulDivModShlShrGadget verifies opcode MUL, DIV, MOD, SHL and SHR. -/// For MUL, verify pop1 * pop2 == push; -/// For DIV, verify pop1 / pop2 == push; -/// For MOD, verify pop1 % pop2 == push; +/// ShlShrGadget verifies opcode SHL and SHR. /// For SHL, verify pop1 * (2^pop2) == push; /// For SHR, verify pop1 / (2^pop2) = push; /// when pop1, pop2, push are 256-bit words. #[derive(Clone, Debug)] -pub(crate) struct MulDivModShlShrGadget { +pub(crate) struct ShlShrGadget { same_context: SameContextGadget, quotient: util::Word, divisor: util::Word, remainder: util::Word, dividend: util::Word, - /// Shift word used for opcode SHL and SHR - pop1: util::Word, - /// First byte of shift value for opcode SHL and SHR + /// Shift word + shift: util::Word, + /// First byte of shift word shf0: Cell, /// Gadget that verifies quotient * divisor + remainder = dividend mul_add_words: MulAddWordsGadget, @@ -49,24 +44,21 @@ pub(crate) struct MulDivModShlShrGadget { remainder_lt_divisor: LtWordGadget, } -impl ExecutionGadget for MulDivModShlShrGadget { - const NAME: &'static str = "MUL_DIV_MOD_SHL_SHR"; +impl ExecutionGadget for ShlShrGadget { + const NAME: &'static str = "SHL_SHR"; - const EXECUTION_STATE: ExecutionState = ExecutionState::MUL_DIV_MOD_SHL_SHR; + const EXECUTION_STATE: ExecutionState = ExecutionState::SHL_SHR; fn configure(cb: &mut ConstraintBuilder) -> Self { let opcode = cb.query_cell(); - let is_mul = is_opcode(&opcode, OpcodeId::MUL); - let is_div = is_opcode(&opcode, OpcodeId::DIV); - let is_mod = is_opcode(&opcode, OpcodeId::MOD); - let is_shl = is_opcode(&opcode, OpcodeId::SHL); - let is_shr = is_opcode(&opcode, OpcodeId::SHR); + let is_shl = OpcodeId::SHR.expr() - opcode.expr(); + let is_shr = 1.expr() - is_shl.expr(); let quotient = cb.query_word(); let divisor = cb.query_word(); let remainder = cb.query_word(); let dividend = cb.query_word(); - let pop1 = cb.query_word(); + let shift = cb.query_word(); let shf0 = cb.query_cell(); let mul_add_words = @@ -75,76 +67,55 @@ impl ExecutionGadget for MulDivModShlShrGadget { let remainder_is_zero = IsZeroGadget::construct(cb, sum::expr(&remainder.cells)); let remainder_lt_divisor = LtWordGadget::construct(cb, &remainder, &divisor); - // Based on different opcode cases, constrain stack pops and pushes as: - // - for `MUL`, two pops are quotient and divisor, and push is dividend. - // - for `DIV`, two pops are dividend and divisor, and push is quotient. - // - for `MOD`, two pops are dividend and divisor, and push is remainder. - // - for `SHL`, two pops are shift and quotient, and push is dividend. - // - for `SHR`, two pops are shift and dividend, and push is quotient. - cb.stack_pop(pop1.expr()); - cb.stack_pop( - (is_mul.clone() + is_div.clone() + is_mod.clone()) * divisor.expr() - + is_shl.clone() * quotient.expr() - + is_shr.clone() * dividend.expr(), - ); + // Constrain stack pops and pushes as: + // - for SHL, two pops are shift and quotient, and push is dividend. + // - for SHR, two pops are shift and dividend, and push is quotient. + cb.stack_pop(shift.expr()); + cb.stack_pop(is_shl.expr() * quotient.expr() + is_shr.expr() * dividend.expr()); cb.stack_push( - (is_mul.clone() + is_shl.clone()) * dividend.expr() - + (is_div.clone() + is_shr.clone()) - * quotient.expr() - * (1.expr() - divisor_is_zero.expr()) - + is_mod.clone() * remainder.expr() * (1.expr() - divisor_is_zero.expr()), + is_shl.expr() * dividend.expr() + + is_shr.expr() * quotient.expr() * (1.expr() - divisor_is_zero.expr()), ); cb.require_zero( - "remainder < divisor when divisor != 0", - (1.expr() - divisor_is_zero.expr()) * (1.expr() - remainder_lt_divisor.expr()), + "shift == shift.cells[0] when divisor != 0", + (1.expr() - divisor_is_zero.expr()) * (shift.expr() - shift.cells[0].expr()), ); cb.require_zero( - "remainder == 0 for both opcode MUL and SHL", - (is_mul.clone() + is_shl.clone()) * (1.expr() - remainder_is_zero.expr()), + "remainder < divisor when divisor != 0", + (1.expr() - divisor_is_zero.expr()) * (1.expr() - remainder_lt_divisor.expr()), ); cb.require_zero( - "overflow == 0 for opcode DIV, MOD and SHR", - (is_div.clone() + is_mod.clone() + is_shr.clone()) * mul_add_words.overflow(), + "remainder == 0 for opcode SHL", + is_shl * (1.expr() - remainder_is_zero.expr()), ); cb.require_zero( - "pop1 == pop1.cells[0] when divisor != 0 for opcode SHL and SHR", - (is_shl.clone() + is_shr.clone()) - * (1.expr() - divisor_is_zero.expr()) - * (pop1.expr() - pop1.cells[0].expr()), + "overflow == 0 for opcode SHR", + is_shr * mul_add_words.overflow(), ); - // For opcode SHL and SHR, constrain `divisor_lo == 2^shf0` when - // `shf0 < 128`, and `divisor_hi == 2^(128 - shf0)` otherwise. + // Constrain divisor_lo == 2^shf0 when shf0 < 128, and + // divisor_hi == 2^(128 - shf0) otherwise. let divisor_lo = from_bytes::expr(&divisor.cells[..16]); let divisor_hi = from_bytes::expr(&divisor.cells[16..]); - cb.condition( - (is_shl.clone() + is_shr.clone()) * (1.expr() - divisor_is_zero.expr()), - |cb| { - cb.add_lookup( - "Pow2 lookup of shf0, divisor_lo and divisor_hi for opcode SHL and SHR", - Lookup::Fixed { - tag: FixedTableTag::Pow2.expr(), - values: [shf0.expr(), divisor_lo.expr(), divisor_hi.expr()], - }, - ); - }, - ); - - let gas_cost = is_mul * OpcodeId::MUL.constant_gas_cost().expr() - + is_div * OpcodeId::DIV.constant_gas_cost().expr() - + is_mod * OpcodeId::MOD.constant_gas_cost().expr() - + is_shl * OpcodeId::SHL.constant_gas_cost().expr() - + is_shr * OpcodeId::SHR.constant_gas_cost().expr(); + cb.condition(1.expr() - divisor_is_zero.expr(), |cb| { + cb.add_lookup( + "Pow2 lookup of shf0, divisor_lo and divisor_hi", + Lookup::Fixed { + tag: FixedTableTag::Pow2.expr(), + values: [shf0.expr(), divisor_lo.expr(), divisor_hi.expr()], + }, + ); + }); let step_state_transition = StepStateTransition { rw_counter: Delta(3.expr()), program_counter: Delta(1.expr()), stack_pointer: Delta(1.expr()), - gas_left: Delta(-gas_cost), + gas_left: Delta(-OpcodeId::SHL.constant_gas_cost().expr()), ..Default::default() }; @@ -156,7 +127,7 @@ impl ExecutionGadget for MulDivModShlShrGadget { divisor, remainder, dividend, - pop1, + shift, shf0, mul_add_words, divisor_is_zero, @@ -177,23 +148,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { self.same_context.assign_exec_step(region, offset, step)?; let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); - - // Get the first byte of shift value only for opcode SHL and SHR. let shf0 = pop1.to_le_bytes()[0]; - let (quotient, divisor, remainder, dividend) = match step.opcode.unwrap() { - OpcodeId::MUL => (pop1, pop2, U256::from(0), push), - OpcodeId::DIV => (push, pop2, pop1 - push * pop2, pop1), - OpcodeId::MOD => ( - if pop2.is_zero() { - U256::from(0) - } else { - pop1 / pop2 - }, - pop2, - if pop2.is_zero() { pop1 } else { push }, - pop1, - ), OpcodeId::SHL => ( pop2, if U256::from(shf0) == pop1 { @@ -214,7 +170,6 @@ impl ExecutionGadget for MulDivModShlShrGadget { } _ => unreachable!(), }; - self.quotient .assign(region, offset, Some(quotient.to_le_bytes()))?; self.divisor @@ -223,7 +178,8 @@ impl ExecutionGadget for MulDivModShlShrGadget { .assign(region, offset, Some(remainder.to_le_bytes()))?; self.dividend .assign(region, offset, Some(dividend.to_le_bytes()))?; - self.pop1.assign(region, offset, Some(pop1.to_le_bytes()))?; + self.shift + .assign(region, offset, Some(pop1.to_le_bytes()))?; self.shf0 .assign(region, offset, Some(u64::from(shf0).into()))?; self.mul_add_words @@ -239,23 +195,6 @@ impl ExecutionGadget for MulDivModShlShrGadget { } } -#[inline] -fn is_opcode(opcode: &Cell, opcode_id: OpcodeId) -> Expression { - generate_lagrange_base_polynomial( - opcode, - opcode_id.as_u8() as usize, - [ - OpcodeId::MUL, - OpcodeId::DIV, - OpcodeId::MOD, - OpcodeId::SHL, - OpcodeId::SHR, - ] - .into_iter() - .map(|op_id| op_id.as_u8() as usize), - ) -} - #[cfg(test)] mod test { use crate::{evm_circuit::test::rand_word, test_util::run_test_circuits}; @@ -281,51 +220,6 @@ mod test { ); } - #[test] - fn mul_gadget_tests() { - test_ok(OpcodeId::MUL, Word::from(0xABCD), Word::from(0x1234)); - test_ok(OpcodeId::MUL, Word::from(0xABCD), Word::from(0x1234) << 240); - test_ok( - OpcodeId::MUL, - Word::from(0xABCD) << 240, - Word::from(0x1234) << 240, - ); - let max_word = Word::from_big_endian(&[255_u8; 32]); - test_ok(OpcodeId::MUL, max_word, Word::from(0x1234)); - test_ok(OpcodeId::MUL, max_word, Word::from(0)); - test_ok(OpcodeId::MUL, rand_word(), rand_word()); - } - - #[test] - fn div_gadget_tests() { - test_ok(OpcodeId::DIV, Word::from(0xABCD), Word::from(0x1234)); - test_ok(OpcodeId::DIV, Word::from(0xABCD), Word::from(0x1234) << 240); - test_ok( - OpcodeId::DIV, - Word::from(0xABCD) << 240, - Word::from(0x1234) << 240, - ); - let max_word = Word::from_big_endian(&[255_u8; 32]); - test_ok(OpcodeId::DIV, max_word, Word::from(0x1234)); - test_ok(OpcodeId::DIV, max_word, Word::from(0)); - test_ok(OpcodeId::DIV, rand_word(), rand_word()); - } - - #[test] - fn mod_gadget_tests() { - test_ok(OpcodeId::MOD, Word::from(0xABCD), Word::from(0x1234)); - test_ok(OpcodeId::MOD, Word::from(0xABCD), Word::from(0x1234) << 240); - test_ok( - OpcodeId::MOD, - Word::from(0xABCD) << 240, - Word::from(0x1234) << 240, - ); - let max_word = Word::from_big_endian(&[255_u8; 32]); - test_ok(OpcodeId::MOD, max_word, Word::from(0x1234)); - test_ok(OpcodeId::MOD, max_word, Word::from(0)); - test_ok(OpcodeId::MOD, rand_word(), rand_word()); - } - #[test] fn shl_gadget_tests() { test_ok(OpcodeId::SHL, Word::from(0xABCD) << 240, Word::from(8)); diff --git a/zkevm-circuits/src/evm_circuit/step.rs b/zkevm-circuits/src/evm_circuit/step.rs index 09049494b4..b642fa2a6a 100644 --- a/zkevm-circuits/src/evm_circuit/step.rs +++ b/zkevm-circuits/src/evm_circuit/step.rs @@ -25,9 +25,10 @@ pub enum ExecutionState { EndBlock, // Opcode successful cases STOP, - ADD_SUB, // ADD, SUB - MUL_DIV_MOD_SHL_SHR, // MUL, DIV, MOD, SHL, SHR - SDIV_SMOD, // SDIV, SMOD + ADD_SUB, // ADD, SUB + MUL_DIV_MOD, // MUL, DIV, MOD + SDIV_SMOD, // SDIV, SMOD + SHL_SHR, // SHL, SHR ADDMOD, MULMOD, EXP, @@ -179,14 +180,9 @@ impl ExecutionState { match self { Self::STOP => vec![OpcodeId::STOP], Self::ADD_SUB => vec![OpcodeId::ADD, OpcodeId::SUB], - Self::MUL_DIV_MOD_SHL_SHR => vec![ - OpcodeId::MUL, - OpcodeId::DIV, - OpcodeId::MOD, - OpcodeId::SHL, - OpcodeId::SHR, - ], + Self::MUL_DIV_MOD => vec![OpcodeId::MUL, OpcodeId::DIV, OpcodeId::MOD], Self::SDIV_SMOD => vec![OpcodeId::SDIV, OpcodeId::SMOD], + Self::SHL_SHR => vec![OpcodeId::SHL, OpcodeId::SHR], Self::ADDMOD => vec![OpcodeId::ADDMOD], Self::MULMOD => vec![OpcodeId::MULMOD], Self::EXP => vec![OpcodeId::EXP], diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index a0bfc1c571..efa92e1519 100644 --- a/zkevm-circuits/src/evm_circuit/witness.rs +++ b/zkevm-circuits/src/evm_circuit/witness.rs @@ -1174,13 +1174,10 @@ impl From<&circuit_input_builder::ExecStep> for ExecutionState { match op { OpcodeId::ADD | OpcodeId::SUB => ExecutionState::ADD_SUB, OpcodeId::ADDMOD => ExecutionState::ADDMOD, - OpcodeId::MUL - | OpcodeId::DIV - | OpcodeId::MOD - | OpcodeId::SHL - | OpcodeId::SHR => ExecutionState::MUL_DIV_MOD_SHL_SHR, + OpcodeId::MUL | OpcodeId::DIV | OpcodeId::MOD => ExecutionState::MUL_DIV_MOD, OpcodeId::MULMOD => ExecutionState::MULMOD, OpcodeId::SDIV | OpcodeId::SMOD => ExecutionState::SDIV_SMOD, + OpcodeId::SHL | OpcodeId::SHR => ExecutionState::SHL_SHR, OpcodeId::EQ | OpcodeId::LT | OpcodeId::GT => ExecutionState::CMP, OpcodeId::SLT | OpcodeId::SGT => ExecutionState::SCMP, OpcodeId::SIGNEXTEND => ExecutionState::SIGNEXTEND, From 2823eabdd9892179e3f4b55ae9ffc2e0d73abdac Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 10 Aug 2022 11:01:13 +0800 Subject: [PATCH 19/22] Fix to always constrain `push` to zero if divisor == 0 (shift > 255). --- zkevm-circuits/src/evm_circuit/execution/shl_shr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs index b5b1f02b24..ac21c4036e 100644 --- a/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs @@ -73,8 +73,8 @@ impl ExecutionGadget for ShlShrGadget { cb.stack_pop(shift.expr()); cb.stack_pop(is_shl.expr() * quotient.expr() + is_shr.expr() * dividend.expr()); cb.stack_push( - is_shl.expr() * dividend.expr() - + is_shr.expr() * quotient.expr() * (1.expr() - divisor_is_zero.expr()), + (is_shl.expr() * dividend.expr() + is_shr.expr() * quotient.expr()) + * (1.expr() - divisor_is_zero.expr()), ); cb.require_zero( From d32d9d835b29898423f9b3a90cb9506ba619614e Mon Sep 17 00:00:00 2001 From: Steven Date: Fri, 26 Aug 2022 10:06:49 +0800 Subject: [PATCH 20/22] Update zkevm-circuits/src/evm_circuit/execution/shl_shr.rs Co-authored-by: z2trillion --- zkevm-circuits/src/evm_circuit/execution/shl_shr.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs index ac21c4036e..b832466eb4 100644 --- a/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs @@ -20,8 +20,8 @@ use eth_types::{Field, ToLittleEndian, U256}; use halo2_proofs::plonk::Error; /// ShlShrGadget verifies opcode SHL and SHR. -/// For SHL, verify pop1 * (2^pop2) == push; -/// For SHR, verify pop1 / (2^pop2) = push; +/// For SHL, verify pop1 * (2^pop2) % 2^256 == push; +/// For SHR, verify pop1 / (2^pop2) % 2^256 == push; /// when pop1, pop2, push are 256-bit words. #[derive(Clone, Debug)] pub(crate) struct ShlShrGadget { From 5bc73207ced3096ce8d35e69feaa621d71fc176f Mon Sep 17 00:00:00 2001 From: Steven Date: Wed, 31 Aug 2022 09:29:32 +0800 Subject: [PATCH 21/22] Simplify to compute with divisor. Co-authored-by: adria0.eth <5526331+adria0@users.noreply.github.com> --- .../src/evm_circuit/execution/shl_shr.rs | 28 ++++++------------- 1 file changed, 9 insertions(+), 19 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs index b832466eb4..d2fd7a14c3 100644 --- a/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs @@ -149,25 +149,15 @@ impl ExecutionGadget for ShlShrGadget { let indices = [step.rw_indices[0], step.rw_indices[1], step.rw_indices[2]]; let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); let shf0 = pop1.to_le_bytes()[0]; - let (quotient, divisor, remainder, dividend) = match step.opcode.unwrap() { - OpcodeId::SHL => ( - pop2, - if U256::from(shf0) == pop1 { - U256::from(1) << shf0 - } else { - U256::from(0) - }, - U256::from(0), - push, - ), - OpcodeId::SHR => { - let divisor = if U256::from(shf0) == pop1 { - U256::from(1) << shf0 - } else { - U256::from(0) - }; - (push, divisor, pop2 - push * divisor, pop2) - } + let divisor = if U256::from(shf0) == pop1 { + U256::from(1) << shf0 + } else { + U256::from(0) + }; + + let (quotient, remainder, dividend) = match step.opcode.unwrap() { + OpcodeId::SHL => (pop2, U256::from(0), push), + OpcodeId::SHR => (push, pop2 - push * divisor, pop2) _ => unreachable!(), }; self.quotient From e226ee9e77106909a8cedc2795773c1f1ed9acfc Mon Sep 17 00:00:00 2001 From: Steven Gu Date: Wed, 31 Aug 2022 09:32:50 +0800 Subject: [PATCH 22/22] Add missing comma. --- zkevm-circuits/src/evm_circuit/execution/shl_shr.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs index d2fd7a14c3..cde9ce89c5 100644 --- a/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs +++ b/zkevm-circuits/src/evm_circuit/execution/shl_shr.rs @@ -150,14 +150,14 @@ impl ExecutionGadget for ShlShrGadget { let [pop1, pop2, push] = indices.map(|idx| block.rws[idx].stack_value()); let shf0 = pop1.to_le_bytes()[0]; let divisor = if U256::from(shf0) == pop1 { - U256::from(1) << shf0 + U256::from(1) << shf0 } else { - U256::from(0) + U256::from(0) }; let (quotient, remainder, dividend) = match step.opcode.unwrap() { OpcodeId::SHL => (pop2, U256::from(0), push), - OpcodeId::SHR => (push, pop2 - push * divisor, pop2) + OpcodeId::SHR => (push, pop2 - push * divisor, pop2), _ => unreachable!(), }; self.quotient