From 1ca4427ae3d32cb48143b47333974c18fd263e47 Mon Sep 17 00:00:00 2001 From: adria0 Date: Fri, 10 Jun 2022 15:40:32 +0200 Subject: [PATCH 1/9] Implement `ADDMOD` --- zkevm-circuits/src/evm_circuit/execution.rs | 5 + .../src/evm_circuit/execution/addmod.rs | 294 ++++++++++++++++++ zkevm-circuits/src/evm_circuit/param.rs | 2 +- .../src/evm_circuit/util/math_gadget.rs | 230 ++++++++++++++ zkevm-circuits/src/evm_circuit/witness.rs | 1 + 5 files changed, 531 insertions(+), 1 deletion(-) create mode 100644 zkevm-circuits/src/evm_circuit/execution/addmod.rs diff --git a/zkevm-circuits/src/evm_circuit/execution.rs b/zkevm-circuits/src/evm_circuit/execution.rs index 4a4cdfefd3..f026ec13be 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; @@ -69,6 +70,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}; @@ -151,6 +153,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, @@ -344,6 +347,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!(), @@ -780,6 +784,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..c7b5350459 --- /dev/null +++ b/zkevm-circuits/src/evm_circuit/execution/addmod.rs @@ -0,0 +1,294 @@ +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}; +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, &r, &sum_areduced_b_overflow, sum_areduced_b.sum()], + ); + + 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 = (a_reduced + b) / n; + + 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, r, a_reduced_plus_b_overflow, a_reduced_plus_b], + )?; + + 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) -> bool { + 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).is_ok() + } + fn test_u32(a: u32, b: u32, c: u32, r: Option) -> bool { + test(a.into(), b.into(), c.into(), r.map(Word::from)) + } + + #[test] + fn addmod_simple() { + assert!(test_u32(1, 1, 10, None)); + assert!(test_u32(1, 1, 10, None)); + } + + #[test] + fn addmod_limits() { + assert!(test(Word::MAX, Word::MAX, 0.into(), None)); + assert!(test(Word::MAX, Word::MAX, 1.into(), None)); + assert!(test(Word::MAX, Word::MAX, Word::MAX, None)); + assert!(test(Word::MAX, 1.into(), 0.into(), None)); + assert!(test(Word::MAX, 1.into(), 1.into(), None)); + assert!(test(Word::MAX, 1.into(), Word::MAX, None)); + assert!(test(Word::MAX, 0.into(), 0.into(), None)); + assert!(test(Word::MAX, 0.into(), 1.into(), None)); + assert!(test(Word::MAX, 0.into(), Word::MAX, None)); + assert!(test(0.into(), 0.into(), 0.into(), None)); + assert!(test(0.into(), 0.into(), 1.into(), None)); + assert!(test(0.into(), 0.into(), Word::MAX, None)); + } + + #[test] + fn addmod_bad_r_on_nonzero_n() { + assert!(test_u32(7, 18, 10, Some(5))); + assert!(!test_u32(7, 18, 10, Some(6))); + } + + #[test] + fn addmod_bad_r_on_zero_n() { + assert!(test_u32(2, 3, 0, Some(0))); + assert!(!test_u32(2, 3, 0, Some(1))); + } + + #[test] + fn addmod_bad_r_bigger_n() { + assert!(test_u32(2, 3, 4, Some(1))); + assert!(!test_u32(2, 3, 4, Some(5))); + } +} diff --git a/zkevm-circuits/src/evm_circuit/param.rs b/zkevm-circuits/src/evm_circuit/param.rs index a4496dc771..5844be4833 100644 --- a/zkevm-circuits/src/evm_circuit/param.rs +++ b/zkevm-circuits/src/evm_circuit/param.rs @@ -3,7 +3,7 @@ use super::table::Table; // Step dimension pub(crate) const STEP_WIDTH: usize = 128; /// Step height -pub const MAX_STEP_HEIGHT: usize = 16; +pub const MAX_STEP_HEIGHT: usize = 17; pub(crate) const N_CELLS_STEP_STATE: usize = 11; /// Lookups done per row. diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs index 6e225f0213..f41250969e 100644 --- a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs +++ b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs @@ -1140,3 +1140,233 @@ impl ShrWordsGadget { Ok(()) } } + +#[derive(Clone, Debug)] +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. +/// +/// We execute a multi-limb multiplication as follows: +/// a and b is divided into 4 64-bit limbs, denoted as a0~a3 and b0~b3 +/// defined t0, t1, t2, t3, t4, t5, t6: +/// t0 = a0 * b0, +/// t1 = a0 * b1 + a1 * b0, +/// t2 = a0 * b2 + a2 * b0 + a1 * b1, +/// t3 = a0 * b3 + a3 * b0 + a2 * b1 + a1 * b2, +/// t4 = a1 * b3 + a2 * b2 + a3 * b1, +/// t5 = a2 * b3 + a3 * b2, +/// t6 = a3 * b3, +/// +/// The addend c as well as the the words that form the result d, e are divided +/// in 2 128-bit limbs each: c_lo, c_hi, d_lo, d_hi, e_lo, e_hi. +/// +/// so t0 ~ t1 include all contributions to the low 128-bit of product (e_lo), +/// with a maximum 65-bit carry (the part higher than 128-bit), denoted as +/// carry_0. Similarly, we define carry_1 as the carry of contributions to the +/// next 128-bit of the product (e_hi) with a maximum val of 66 bits. Finally, +/// we define carry_2 as the carry for the next 128 bits of the product (d_lo). +/// +/// We can slightly relax the constraint of carry_0/carry_1, carry_2 to 72-bit +/// and allocate 9 bytes for them each +/// +/// Finally we just prove: +/// t0 + t1 * 2^64 + c_lo = e_lo + carry_0 +/// t2 + t3 * 2^64 + c_hi + carry_0 = e_hi + carry_1 +/// t4 + t5 * 2^64 + carry_1 = d_lo + carry_2 +/// t6 + carry_2 = d_hi +#[derive(Clone, Debug)] +pub(crate) struct MulAddWords512Gadget { + carry_0: [Cell; 9], + carry_1: [Cell; 9], + carry_2: [Cell; 9], +} + +impl MulAddWords512Gadget { + pub(crate) fn construct(cb: &mut ConstraintBuilder, words: [&util::Word; 5]) -> Self { + let carry_0 = cb.query_bytes(); + let carry_1 = cb.query_bytes(); + let carry_2 = cb.query_bytes(); + let carry_0_expr = from_bytes::expr(&carry_0); + let carry_1_expr = from_bytes::expr(&carry_1); + let carry_2_expr = from_bytes::expr(&carry_2); + + // Split input words in limbs + let mut a_limbs = vec![]; + let mut b_limbs = vec![]; + for trunk in 0..4 { + let idx = (trunk * 8) as usize; + a_limbs.push(from_bytes::expr(&words[0].cells[idx..idx + 8])); + b_limbs.push(from_bytes::expr(&words[1].cells[idx..idx + 8])); + } + + let c_lo = from_bytes::expr(&words[2].cells[0..16]); + let c_hi = from_bytes::expr(&words[2].cells[16..32]); + let d_lo = from_bytes::expr(&words[3].cells[0..16]); + let d_hi = from_bytes::expr(&words[3].cells[16..32]); + let e_lo = from_bytes::expr(&words[4].cells[0..16]); + let e_hi = from_bytes::expr(&words[4].cells[16..32]); + + // Limb multiplication + let t0 = a_limbs[0].clone() * b_limbs[0].clone(); + let t1 = a_limbs[0].clone() * b_limbs[1].clone() + a_limbs[1].clone() * b_limbs[0].clone(); + let t2 = a_limbs[0].clone() * b_limbs[2].clone() + + a_limbs[1].clone() * b_limbs[1].clone() + + a_limbs[2].clone() * b_limbs[0].clone(); + let t3 = a_limbs[0].clone() * b_limbs[3].clone() + + a_limbs[1].clone() * b_limbs[2].clone() + + a_limbs[2].clone() * b_limbs[1].clone() + + a_limbs[3].clone() * b_limbs[0].clone(); + let t4 = a_limbs[1].clone() * b_limbs[3].clone() + + a_limbs[2].clone() * b_limbs[2].clone() + + a_limbs[3].clone() * b_limbs[1].clone(); + let t5 = a_limbs[2].clone() * b_limbs[3].clone() + a_limbs[3].clone() * b_limbs[2].clone(); + let t6 = a_limbs[3].clone() * b_limbs[3].clone(); + + cb.require_equal( + "(t0 + t1 ⋅ 2^64) + c_lo == e_lo + carry_0 ⋅ 2^128", + t0.expr() + t1.expr() * pow_of_two_expr(64) + c_lo, + e_lo + carry_0_expr.clone() * pow_of_two_expr(128), + ); + + cb.require_equal( + "(t2 + t3 ⋅ 2^64) + c_hi + carry_0 == e_hi + carry_1 ⋅ 2^128", + t2.expr() + t3.expr() * pow_of_two_expr(64) + c_hi + carry_0_expr, + e_hi + carry_1_expr.clone() * pow_of_two_expr(128), + ); + + cb.require_equal( + "(t4 + t5 ⋅ 2^64) + carry_1 == d_lo + carry_2 ⋅ 2^128", + t4.expr() + t5.expr() * pow_of_two_expr(64) + carry_1_expr, + d_lo + carry_2_expr.clone() * pow_of_two_expr(128), + ); + + cb.require_equal("t6 + carry_2 == d_hi", t6.expr() + carry_2_expr, d_hi); + + Self { + carry_0, + carry_1, + carry_2, + } + } + + pub(crate) fn assign( + &self, + region: &mut CachedRegion<'_, '_, F>, + offset: usize, + words: [Word; 5], + ) -> Result<(), Error> { + let (a, b, c, d, e) = (words[0], words[1], words[2], words[3], words[4]); + + let a_limbs = split_u256_limb64(&a); + let b_limbs = split_u256_limb64(&b); + let (c_lo, c_hi) = split_u256(&c); + let (d_lo, _d_hi) = split_u256(&d); + let (e_lo, e_hi) = split_u256(&e); + + let t0 = a_limbs[0] * b_limbs[0]; + let t1 = a_limbs[0] * b_limbs[1] + a_limbs[1] * b_limbs[0]; + let t2 = a_limbs[0] * b_limbs[2] + a_limbs[1] * b_limbs[1] + a_limbs[2] * b_limbs[0]; + let t3 = a_limbs[0] * b_limbs[3] + + a_limbs[1] * b_limbs[2] + + a_limbs[2] * b_limbs[1] + + a_limbs[3] * b_limbs[0]; + + let t4 = a_limbs[1] * b_limbs[3] + a_limbs[2] * b_limbs[2] + a_limbs[3] * b_limbs[1]; + let t5 = a_limbs[2] * b_limbs[3] + a_limbs[3] * b_limbs[2]; + + let carry_0 = ((t0 + (t1 << 64) + c_lo).saturating_sub(e_lo)) >> 128; + let carry_1 = ((t2 + (t3 << 64) + c_hi + carry_0).saturating_sub(e_hi)) >> 128; + let carry_2 = ((t4 + (t5 << 64) + carry_1).saturating_sub(d_lo)) >> 128; + + self.carry_0 + .iter() + .zip(carry_0.to_le_bytes().iter()) + .map(|(cell, byte)| cell.assign(region, offset, Some(F::from(*byte as u64)))) + .collect::, _>>()?; + + self.carry_1 + .iter() + .zip(carry_1.to_le_bytes().iter()) + .map(|(cell, byte)| cell.assign(region, offset, Some(F::from(*byte as u64)))) + .collect::, _>>()?; + + self.carry_2 + .iter() + .zip(carry_2.to_le_bytes().iter()) + .map(|(cell, byte)| cell.assign(region, offset, Some(F::from(*byte as u64)))) + .collect::, _>>()?; + Ok(()) + } +} diff --git a/zkevm-circuits/src/evm_circuit/witness.rs b/zkevm-circuits/src/evm_circuit/witness.rs index 8f0d70fc86..25fe3b0b6a 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::EQ | OpcodeId::LT | OpcodeId::GT => ExecutionState::CMP, OpcodeId::SLT | OpcodeId::SGT => ExecutionState::SCMP, From a70aaba6a7f15e6cfa501f4a91dba2f7e04f235e Mon Sep 17 00:00:00 2001 From: "adria0.eth" <5526331+adria0@users.noreply.github.com> Date: Mon, 20 Jun 2022 15:53:26 +0200 Subject: [PATCH 2/9] Apply suggestions from @ed255 code review --- zkevm-circuits/src/evm_circuit/util/math_gadget.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs index 3c8bb58137..4534abd0e4 100644 --- a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs +++ b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs @@ -1142,6 +1142,7 @@ impl ShrWordsGadget { } #[derive(Clone, Debug)] +/// CmpWordsGadget compares two words, exposing `eq` and `lt` pub(crate) struct CmpWordsGadget { comparison_lo: ComparisonGadget, comparison_hi: ComparisonGadget, @@ -1242,7 +1243,7 @@ impl CmpWordsGadget { /// and allocate 9 bytes for them each /// /// Finally we just prove: -// t0 + t1 * 2^64 + c_lo = e_lo + carry_0 * 2^128 +/// t0 + t1 * 2^64 + c_lo = e_lo + carry_0 * 2^128 /// t2 + t3 * 2^64 + c_hi + carry_0 = e_hi + carry_1 * 2^128 /// t4 + t5 * 2^64 + carry_1 = d_lo + carry_2 * 2^128 /// t6 + carry_2 = d_hi From 46994dfac7503d217dc94d6e74b1c7e02b630513 Mon Sep 17 00:00:00 2001 From: adria0 Date: Mon, 20 Jun 2022 15:58:03 +0200 Subject: [PATCH 3/9] fmt --- zkevm-circuits/src/evm_circuit/util/math_gadget.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs index 4534abd0e4..727b4cc425 100644 --- a/zkevm-circuits/src/evm_circuit/util/math_gadget.rs +++ b/zkevm-circuits/src/evm_circuit/util/math_gadget.rs @@ -1142,7 +1142,7 @@ impl ShrWordsGadget { } #[derive(Clone, Debug)] -/// CmpWordsGadget compares two words, exposing `eq` and `lt` +/// CmpWordsGadget compares two words, exposing `eq` and `lt` pub(crate) struct CmpWordsGadget { comparison_lo: ComparisonGadget, comparison_hi: ComparisonGadget, From b4cee201969e4290089474e94ad4a8c71f407bbc Mon Sep 17 00:00:00 2001 From: adria0 Date: Mon, 20 Jun 2022 16:40:13 +0200 Subject: [PATCH 4/9] added RUST_MIN_STACK --- .cargo/config.toml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.cargo/config.toml b/.cargo/config.toml index 855dab744c..7428d8453d 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -1,2 +1,5 @@ +[env] +RUST_MIN_STACK="16777216" + [target.'cfg(target_os="macos")'] rustflags = ["-C", "link-args=-framework CoreFoundation -framework Security"] From 13cd65a29b6390e8340e30a13c82625c24c9d0eb Mon Sep 17 00:00:00 2001 From: adria0 Date: Mon, 20 Jun 2022 16:40:30 +0200 Subject: [PATCH 5/9] fix order --- zkevm-circuits/src/evm_circuit/execution/addmod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/addmod.rs b/zkevm-circuits/src/evm_circuit/execution/addmod.rs index 8ad262be95..3ee2cb1c89 100644 --- a/zkevm-circuits/src/evm_circuit/execution/addmod.rs +++ b/zkevm-circuits/src/evm_circuit/execution/addmod.rs @@ -204,7 +204,7 @@ impl ExecutionGadget for AddModGadget { self.muladd_d_n_r.assign( region, offset, - [d, n, a_reduced_plus_b, a_reduced_plus_b_overflow], + [d, n, a_reduced_plus_b_overflow, a_reduced_plus_b], Some(r), )?; From 4ff67ef3073ca3ac04277e8aa74fa5f2b8b1bb0a Mon Sep 17 00:00:00 2001 From: adria0 Date: Mon, 20 Jun 2022 18:38:12 +0200 Subject: [PATCH 6/9] Add a_reduced + b requieres 512 bit. Improve tests. --- zkevm-circuits/src/evm_circuit/execution/addmod.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/addmod.rs b/zkevm-circuits/src/evm_circuit/execution/addmod.rs index 3ee2cb1c89..e2634abe49 100644 --- a/zkevm-circuits/src/evm_circuit/execution/addmod.rs +++ b/zkevm-circuits/src/evm_circuit/execution/addmod.rs @@ -17,7 +17,7 @@ use crate::{ }; use bus_mapping::evm::OpcodeId; -use eth_types::{Field, ToLittleEndian, U256}; +use eth_types::{Field, ToLittleEndian, U256, U512}; use halo2_proofs::plonk::Error; #[derive(Clone, Debug)] @@ -175,7 +175,9 @@ impl ExecutionGadget for AddModGadget { let (a_div_n, a_mod_n) = a.div_mod(n); k = a_div_n; a_reduced = a_mod_n; - d = (a_reduced + b) / 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; @@ -264,6 +266,7 @@ mod test { fn addmod_limits() { assert!(test(Word::MAX, Word::MAX, 0.into(), None)); assert!(test(Word::MAX, Word::MAX, 1.into(), None)); + assert!(test(Word::MAX - 1, Word::MAX, Word::MAX, None)); assert!(test(Word::MAX, Word::MAX, Word::MAX, None)); assert!(test(Word::MAX, 1.into(), 0.into(), None)); assert!(test(Word::MAX, 1.into(), 1.into(), None)); From e6ee7e5e76c285e6a6b0290a3f7613b257722f60 Mon Sep 17 00:00:00 2001 From: adria0 Date: Mon, 20 Jun 2022 18:38:12 +0200 Subject: [PATCH 7/9] Add a_reduced + b requieres 512 bit. Improve tests. --- zkevm-circuits/src/evm_circuit/execution/addmod.rs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/addmod.rs b/zkevm-circuits/src/evm_circuit/execution/addmod.rs index 3ee2cb1c89..e2634abe49 100644 --- a/zkevm-circuits/src/evm_circuit/execution/addmod.rs +++ b/zkevm-circuits/src/evm_circuit/execution/addmod.rs @@ -17,7 +17,7 @@ use crate::{ }; use bus_mapping::evm::OpcodeId; -use eth_types::{Field, ToLittleEndian, U256}; +use eth_types::{Field, ToLittleEndian, U256, U512}; use halo2_proofs::plonk::Error; #[derive(Clone, Debug)] @@ -175,7 +175,9 @@ impl ExecutionGadget for AddModGadget { let (a_div_n, a_mod_n) = a.div_mod(n); k = a_div_n; a_reduced = a_mod_n; - d = (a_reduced + b) / 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; @@ -264,6 +266,7 @@ mod test { fn addmod_limits() { assert!(test(Word::MAX, Word::MAX, 0.into(), None)); assert!(test(Word::MAX, Word::MAX, 1.into(), None)); + assert!(test(Word::MAX - 1, Word::MAX, Word::MAX, None)); assert!(test(Word::MAX, Word::MAX, Word::MAX, None)); assert!(test(Word::MAX, 1.into(), 0.into(), None)); assert!(test(Word::MAX, 1.into(), 1.into(), None)); From f67abb02792de8d68857b3eee642457de296ba4e Mon Sep 17 00:00:00 2001 From: adria0 Date: Tue, 21 Jun 2022 11:32:57 +0200 Subject: [PATCH 8/9] remove stack set --- .cargo/config.toml | 3 --- 1 file changed, 3 deletions(-) diff --git a/.cargo/config.toml b/.cargo/config.toml index 7428d8453d..855dab744c 100644 --- a/.cargo/config.toml +++ b/.cargo/config.toml @@ -1,5 +1,2 @@ -[env] -RUST_MIN_STACK="16777216" - [target.'cfg(target_os="macos")'] rustflags = ["-C", "link-args=-framework CoreFoundation -framework Security"] From 7e5a3f69c1ddf90a25f72b77d4d71d01e639f752 Mon Sep 17 00:00:00 2001 From: adria0 Date: Tue, 21 Jun 2022 11:33:32 +0200 Subject: [PATCH 9/9] make tests verbose on error --- .../src/evm_circuit/execution/addmod.rs | 58 +++++++++++-------- 1 file changed, 34 insertions(+), 24 deletions(-) diff --git a/zkevm-circuits/src/evm_circuit/execution/addmod.rs b/zkevm-circuits/src/evm_circuit/execution/addmod.rs index e2634abe49..449d6172c6 100644 --- a/zkevm-circuits/src/evm_circuit/execution/addmod.rs +++ b/zkevm-circuits/src/evm_circuit/execution/addmod.rs @@ -230,7 +230,12 @@ mod test { use eth_types::{bytecode, Word}; use mock::TestContext; - fn test(a: Word, b: Word, n: Word, r: Option) -> bool { + fn test( + a: Word, + b: Word, + n: Word, + r: Option, + ) -> Result<(), Vec> { let bytecode = bytecode! { PUSH32(n) PUSH32(b) @@ -250,50 +255,55 @@ mod test { .unwrap(); last.stack = Stack::from_vec(vec![r]); } - run_test_circuits(ctx, None).is_ok() + run_test_circuits(ctx, None) } - fn test_u32(a: u32, b: u32, c: u32, r: Option) -> bool { + 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!(test_u32(1, 1, 10, None)); - assert!(test_u32(1, 1, 11, None)); + assert_eq!(test_u32(1, 1, 10, None), Ok(())); + assert_eq!(test_u32(1, 1, 11, None), Ok(())); } #[test] fn addmod_limits() { - assert!(test(Word::MAX, Word::MAX, 0.into(), None)); - assert!(test(Word::MAX, Word::MAX, 1.into(), None)); - assert!(test(Word::MAX - 1, Word::MAX, Word::MAX, None)); - assert!(test(Word::MAX, Word::MAX, Word::MAX, None)); - assert!(test(Word::MAX, 1.into(), 0.into(), None)); - assert!(test(Word::MAX, 1.into(), 1.into(), None)); - assert!(test(Word::MAX, 1.into(), Word::MAX, None)); - assert!(test(Word::MAX, 0.into(), 0.into(), None)); - assert!(test(Word::MAX, 0.into(), 1.into(), None)); - assert!(test(Word::MAX, 0.into(), Word::MAX, None)); - assert!(test(0.into(), 0.into(), 0.into(), None)); - assert!(test(0.into(), 0.into(), 1.into(), None)); - assert!(test(0.into(), 0.into(), Word::MAX, None)); + 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!(test_u32(7, 18, 10, Some(5))); - assert!(!test_u32(7, 18, 10, Some(6))); + 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!(test_u32(2, 3, 0, Some(0))); - assert!(!test_u32(2, 3, 0, Some(1))); + 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!(test_u32(2, 3, 4, Some(1))); - assert!(!test_u32(2, 3, 4, Some(5))); + assert_eq!(test_u32(2, 3, 4, Some(1)), Ok(())); + assert_ne!(test_u32(2, 3, 4, Some(5)), Ok(())); } }