diff --git a/zkevm-circuits/src/evm_circuit/execution.rs b/zkevm-circuits/src/evm_circuit/execution.rs index 0e29a474e5..b927b4d817 100644 --- a/zkevm-circuits/src/evm_circuit/execution.rs +++ b/zkevm-circuits/src/evm_circuit/execution.rs @@ -23,6 +23,7 @@ use std::{collections::HashMap, convert::TryInto, iter}; use strum::IntoEnumIterator; mod add_sub; +mod addmod; mod begin_tx; mod bitwise; mod block_ctx; @@ -71,6 +72,7 @@ mod stop; mod swap; use add_sub::AddSubGadget; +use addmod::AddModGadget; use begin_tx::BeginTxGadget; use bitwise::BitwiseGadget; use block_ctx::{BlockCtxU160Gadget, BlockCtxU256Gadget, BlockCtxU64Gadget}; @@ -155,6 +157,7 @@ pub(crate) struct ExecutionConfig { end_tx_gadget: EndTxGadget, // opcode gadgets add_sub_gadget: AddSubGadget, + addmod_gadget: AddModGadget, bitwise_gadget: BitwiseGadget, byte_gadget: ByteGadget, call_gadget: CallGadget, @@ -350,6 +353,7 @@ impl ExecutionConfig { end_tx_gadget: configure_gadget!(), // opcode gadgets add_sub_gadget: configure_gadget!(), + addmod_gadget: configure_gadget!(), bitwise_gadget: configure_gadget!(), byte_gadget: configure_gadget!(), call_gadget: configure_gadget!(), @@ -788,6 +792,7 @@ impl ExecutionConfig { ExecutionState::EndBlock => assign_exec_step!(self.end_block_gadget), // opcode ExecutionState::ADD_SUB => assign_exec_step!(self.add_sub_gadget), + ExecutionState::ADDMOD => assign_exec_step!(self.addmod_gadget), ExecutionState::BITWISE => assign_exec_step!(self.bitwise_gadget), ExecutionState::BYTE => assign_exec_step!(self.byte_gadget), ExecutionState::CALL => assign_exec_step!(self.call_gadget), diff --git a/zkevm-circuits/src/evm_circuit/execution/addmod.rs b/zkevm-circuits/src/evm_circuit/execution/addmod.rs new file mode 100644 index 0000000000..449d6172c6 --- /dev/null +++ b/zkevm-circuits/src/evm_circuit/execution/addmod.rs @@ -0,0 +1,309 @@ +use crate::{ + evm_circuit::{ + execution::ExecutionGadget, + step::ExecutionState, + util::{ + common_gadget::SameContextGadget, + constraint_builder::{ConstraintBuilder, StepStateTransition, Transition::Delta}, + math_gadget::{ + AddWordsGadget, CmpWordsGadget, IsZeroGadget, MulAddWords512Gadget, + MulAddWordsGadget, + }, + not, CachedRegion, Word, + }, + witness::{Block, Call, ExecStep, Transaction}, + }, + util::Expr, +}; + +use bus_mapping::evm::OpcodeId; +use eth_types::{Field, ToLittleEndian, U256, U512}; +use halo2_proofs::plonk::Error; + +#[derive(Clone, Debug)] +pub(crate) struct AddModGadget { + same_context: SameContextGadget, + + a: Word, + b: Word, + r: Word, + n: Word, + + k: Word, + d: Word, + a_reduced: Word, + + muladd_k_n_areduced: MulAddWordsGadget, + + sum_areduced_b: AddWordsGadget, + sum_areduced_b_overflow: Word, + muladd_d_n_r: MulAddWords512Gadget, + + n_is_zero: IsZeroGadget, + cmp_r_n: CmpWordsGadget, + cmp_areduced_n: CmpWordsGadget, +} + +impl ExecutionGadget for AddModGadget { + const NAME: &'static str = "ADDMOD"; + + const EXECUTION_STATE: ExecutionState = ExecutionState::ADDMOD; + + fn configure(cb: &mut ConstraintBuilder) -> Self { + let opcode = cb.query_cell(); + + // values got from stack (original r is modified if n==0) + let a = cb.query_word(); + let b = cb.query_word(); + let n = cb.query_word(); + let r = cb.query_word(); + + // auxiliar witness + let k = cb.query_word(); + let a_reduced = cb.query_word(); + let d = cb.query_word(); + + let n_is_zero = IsZeroGadget::construct(cb, n.clone().expr()); + + // 1. check k * N + a_reduced == a without overflow + let muladd_k_n_areduced = MulAddWordsGadget::construct(cb, [&k, &n, &a_reduced, &a]); + cb.require_zero( + "k * N + a_reduced does not overflow", + muladd_k_n_areduced.overflow(), + ); + + // 2. check d * N + r == a_reduced + b, only checking carry if n != 0 + let sum_areduced_b = { + let sum = cb.query_word(); + AddWordsGadget::construct(cb, [a_reduced.clone(), b.clone()], sum) + }; + let sum_areduced_b_overflow = cb.query_word(); + let muladd_d_n_r = MulAddWords512Gadget::construct( + cb, + [&d, &n, &sum_areduced_b_overflow, sum_areduced_b.sum()], + Some(&r), + ); + + cb.require_equal( + "check a_reduced + b 512 bit carry if n != 0", + sum_areduced_b_overflow.expr(), + sum_areduced_b.carry().clone().unwrap().expr() * not::expr(n_is_zero.expr()), + ); + + let cmp_r_n = CmpWordsGadget::construct(cb, &r, &n); + let cmp_areduced_n = CmpWordsGadget::construct(cb, &a_reduced, &n); + + // 3. r < n and a_reduced < n if n > 0 + cb.require_zero( + "{r 0", + 2.expr() - (cmp_r_n.lt.expr() + cmp_areduced_n.lt.expr() + 2.expr() * n_is_zero.expr()), + ); + + // pop/push values + // take care that if n==0 pushed value for r should be zero also + cb.stack_pop(a.expr()); + cb.stack_pop(b.expr()); + cb.stack_pop(n.expr()); + cb.stack_push(r.expr() * not::expr(n_is_zero.expr())); + + // State transition + let step_state_transition = StepStateTransition { + rw_counter: Delta(4.expr()), + program_counter: Delta(1.expr()), + stack_pointer: Delta(2.expr()), + gas_left: Delta(-OpcodeId::ADDMOD.constant_gas_cost().expr()), + ..StepStateTransition::default() + }; + let same_context = SameContextGadget::construct(cb, opcode, step_state_transition); + + Self { + a, + b, + r, + n, + k, + d, + a_reduced, + muladd_d_n_r, + muladd_k_n_areduced, + same_context, + cmp_r_n, + cmp_areduced_n, + n_is_zero, + sum_areduced_b, + sum_areduced_b_overflow, + } + } + + 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)?; + + // get stack values + let [mut r, n, b, a] = [3, 2, 1, 0] + .map(|idx| step.rw_indices[idx]) + .map(|idx| block.rws[idx].stack_value()); + + // assing a,b & n stack values + self.a.assign(region, offset, Some(a.to_le_bytes()))?; + self.b.assign(region, offset, Some(b.to_le_bytes()))?; + self.n.assign(region, offset, Some(n.to_le_bytes()))?; + + // compute a_reduced,k,d,a_reduced_plus_b,a_reduced_plus_b_overflow,r values + let a_reduced; + let k; + let d; + let a_reduced_plus_b; + let a_reduced_plus_b_overflow; + + if n.is_zero() { + k = U256::zero(); + a_reduced = a; + d = U256::zero(); + r = a.overflowing_add(b).0; + + a_reduced_plus_b = a_reduced.overflowing_add(b).0; + a_reduced_plus_b_overflow = U256::zero(); + } else { + let (a_div_n, a_mod_n) = a.div_mod(n); + k = a_div_n; + a_reduced = a_mod_n; + d = ((U512::from(a_reduced) + U512::from(b)) / U512::from(n)) + .try_into() + .unwrap(); + + let (sum, overflow) = a_reduced.overflowing_add(b); + a_reduced_plus_b = sum; + a_reduced_plus_b_overflow = if overflow { U256::one() } else { U256::zero() }; + }; + + // rest of values and gadgets + + self.r.assign(region, offset, Some(r.to_le_bytes()))?; + self.k.assign(region, offset, Some(k.to_le_bytes()))?; + self.d.assign(region, offset, Some(d.to_le_bytes()))?; + self.a_reduced + .assign(region, offset, Some(a_reduced.to_le_bytes()))?; + + self.muladd_k_n_areduced + .assign(region, offset, [k, n, a_reduced, a])?; + + self.sum_areduced_b + .assign(region, offset, [a_reduced, b], a_reduced_plus_b)?; + + self.sum_areduced_b_overflow.assign( + region, + offset, + Some(a_reduced_plus_b_overflow.to_le_bytes()), + )?; + self.muladd_d_n_r.assign( + region, + offset, + [d, n, a_reduced_plus_b_overflow, a_reduced_plus_b], + Some(r), + )?; + + self.cmp_r_n.assign(region, offset, r, n)?; + self.cmp_areduced_n.assign(region, offset, a_reduced, n)?; + + self.n_is_zero.assign( + region, + offset, + Word::random_linear_combine(n.to_le_bytes(), block.randomness), + )?; + + Ok(()) + } +} + +#[cfg(test)] +mod test { + use crate::test_util::run_test_circuits; + use eth_types::evm_types::Stack; + use eth_types::{bytecode, Word}; + use mock::TestContext; + + fn test( + a: Word, + b: Word, + n: Word, + r: Option, + ) -> Result<(), Vec> { + let bytecode = bytecode! { + PUSH32(n) + PUSH32(b) + PUSH32(a) + ADDMOD + STOP + }; + + let mut ctx = TestContext::<2, 1>::simple_ctx_with_bytecode(bytecode).unwrap(); + if let Some(r) = r { + let mut last = ctx + .geth_traces + .first_mut() + .unwrap() + .struct_logs + .last_mut() + .unwrap(); + last.stack = Stack::from_vec(vec![r]); + } + run_test_circuits(ctx, None) + } + fn test_u32( + a: u32, + b: u32, + c: u32, + r: Option, + ) -> Result<(), Vec> { + test(a.into(), b.into(), c.into(), r.map(Word::from)) + } + + #[test] + fn addmod_simple() { + assert_eq!(test_u32(1, 1, 10, None), Ok(())); + assert_eq!(test_u32(1, 1, 11, None), Ok(())); + } + + #[test] + fn addmod_limits() { + assert_eq!(test(Word::MAX, Word::MAX, 0.into(), None), Ok(())); + assert_eq!(test(Word::MAX, Word::MAX, 1.into(), None), Ok(())); + assert_eq!(test(Word::MAX - 1, Word::MAX, Word::MAX, None), Ok(())); + assert_eq!(test(Word::MAX, Word::MAX, Word::MAX, None), Ok(())); + assert_eq!(test(Word::MAX, 1.into(), 0.into(), None), Ok(())); + assert_eq!(test(Word::MAX, 1.into(), 1.into(), None), Ok(())); + assert_eq!(test(Word::MAX, 1.into(), Word::MAX, None), Ok(())); + assert_eq!(test(Word::MAX, 0.into(), 0.into(), None), Ok(())); + assert_eq!(test(Word::MAX, 0.into(), 1.into(), None), Ok(())); + assert_eq!(test(Word::MAX, 0.into(), Word::MAX, None), Ok(())); + assert_eq!(test(0.into(), 0.into(), 0.into(), None), Ok(())); + assert_eq!(test(0.into(), 0.into(), 1.into(), None), Ok(())); + assert_eq!(test(0.into(), 0.into(), Word::MAX, None), Ok(())); + } + + #[test] + fn addmod_bad_r_on_nonzero_n() { + assert_eq!(test_u32(7, 18, 10, Some(5)), Ok(())); + assert_ne!(test_u32(7, 18, 10, Some(6)), Ok(())); + } + + #[test] + fn addmod_bad_r_on_zero_n() { + assert_eq!(test_u32(2, 3, 0, Some(0)), Ok(())); + assert_ne!(test_u32(2, 3, 0, Some(1)), Ok(())); + } + + #[test] + fn addmod_bad_r_bigger_n() { + assert_eq!(test_u32(2, 3, 4, Some(1)), Ok(())); + assert_ne!(test_u32(2, 3, 4, Some(5)), Ok(())); + } +} diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs index 5db3965eb0..727b4cc425 100644 --- a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs +++ b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs @@ -1141,6 +1141,81 @@ impl ShrWordsGadget { } } +#[derive(Clone, Debug)] +/// CmpWordsGadget compares two words, exposing `eq` and `lt` +pub(crate) struct CmpWordsGadget { + comparison_lo: ComparisonGadget, + comparison_hi: ComparisonGadget, + pub eq: Expression, + pub lt: Expression, +} + +impl CmpWordsGadget { + pub(crate) fn construct( + cb: &mut ConstraintBuilder, + a: &util::Word, + b: &util::Word, + ) -> Self { + // `a[0..16] <= b[0..16]` + let comparison_lo = ComparisonGadget::construct( + cb, + from_bytes::expr(&a.cells[0..16]), + from_bytes::expr(&b.cells[0..16]), + ); + + let (lt_lo, eq_lo) = comparison_lo.expr(); + + // `a[16..32] <= b[16..32]` + let comparison_hi = ComparisonGadget::construct( + cb, + from_bytes::expr(&a.cells[16..32]), + from_bytes::expr(&b.cells[16..32]), + ); + let (lt_hi, eq_hi) = comparison_hi.expr(); + + // `a < b` when: + // - `a[16..32] < b[16..32]` OR + // - `a[16..32] == b[16..32]` AND `a[0..16] < b[0..16]` + let lt = select::expr(lt_hi, 1.expr(), eq_hi.clone() * lt_lo); + + // `a == b` when both parts are equal + let eq = eq_hi * eq_lo; + + Self { + comparison_lo, + comparison_hi, + lt, + eq, + } + } + + pub(crate) fn assign( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + a: Word, + b: Word, + ) -> Result<(), Error> { + // `a[0..1] <= b[0..16]` + self.comparison_lo.assign( + region, + offset, + from_bytes::value(&a.to_le_bytes()[0..16]), + from_bytes::value(&b.to_le_bytes()[0..16]), + )?; + + // `a[16..32] <= b[16..32]` + self.comparison_hi.assign( + region, + offset, + from_bytes::value(&a.to_le_bytes()[16..32]), + from_bytes::value(&b.to_le_bytes()[16..32]), + )?; + + Ok(()) + } +} + /// Construct the gadget that checks a * b + c == d * 2**256 + e /// where a, b, c, d, e are 256-bit words. /// diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index b706222de1..0e41b6e638 100644 --- a/zkevm-circuits/src/evm_circuit/witness.rs +++ b/zkevm-circuits/src/evm_circuit/witness.rs @@ -1183,6 +1183,7 @@ 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 => ExecutionState::MUL_DIV_MOD, OpcodeId::MULMOD => ExecutionState::MULMOD, OpcodeId::EQ | OpcodeId::LT | OpcodeId::GT => ExecutionState::CMP,