From e11b79e4f598f63a1c4780316c2aefb0f0e4d0d4 Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Thu, 26 Sep 2024 21:36:23 -0400 Subject: [PATCH] Bring back arith op --- .../src/cpu/columns/general.rs | 25 ------ evm_arithmetization/src/cpu/incr.rs | 88 +------------------ evm_arithmetization/src/witness/operation.rs | 31 +------ 3 files changed, 4 insertions(+), 140 deletions(-) diff --git a/evm_arithmetization/src/cpu/columns/general.rs b/evm_arithmetization/src/cpu/columns/general.rs index 067a810b9..97f8b8f49 100644 --- a/evm_arithmetization/src/cpu/columns/general.rs +++ b/evm_arithmetization/src/cpu/columns/general.rs @@ -15,7 +15,6 @@ pub(crate) union CpuGeneralColumnsView { shift: CpuShiftView, stack: CpuStackView, push: CpuPushView, - incr: CpuIncrView, context_pruning: CpuContextPruningView, } @@ -94,18 +93,6 @@ impl CpuGeneralColumnsView { unsafe { &mut self.push } } - /// View of the columns required for the incr operation. - /// SAFETY: Each view is a valid interpretation of the underlying array. - pub(crate) const fn incr(&self) -> &CpuIncrView { - unsafe { &self.incr } - } - - /// Mutable view of the columns required for the incr operation. - /// SAFETY: Each view is a valid interpretation of the underlying array. - pub(crate) fn incr_mut(&mut self) -> &mut CpuIncrView { - unsafe { &mut self.incr } - } - /// View of the column for context pruning. /// SAFETY: Each view is a valid interpretation of the underlying array. pub(crate) const fn context_pruning(&self) -> &CpuContextPruningView { @@ -230,17 +217,6 @@ pub(crate) struct CpuPushView { _padding_columns: [T; NUM_SHARED_COLUMNS - 1], } -/// View of all `CpuGeneralColumn`s, helping to detect any limb overflow -/// when incrementing by 1. -#[repr(C)] -#[derive(Copy, Clone)] -pub(crate) struct CpuIncrView { - /// If limb `i` is 1, then we overflowed the first `i-1` limbs when adding - /// 1 (i.e. they are now 0). This means limb `1` is incremented by 1, and - /// higher limbs remain unchanged. - pub(crate) limbs: [T; NUM_SHARED_COLUMNS], -} - /// View of the first `CpuGeneralColumn` storing a flag for context pruning. #[derive(Copy, Clone)] pub(crate) struct CpuContextPruningView { @@ -267,5 +243,4 @@ const_assert!(size_of::>() == NUM_SHARED_COLUMNS); const_assert!(size_of::>() == NUM_SHARED_COLUMNS); const_assert!(size_of::>() == NUM_SHARED_COLUMNS); const_assert!(size_of::>() == NUM_SHARED_COLUMNS); -const_assert!(size_of::>() == NUM_SHARED_COLUMNS); const_assert!(size_of::>() == NUM_SHARED_COLUMNS); diff --git a/evm_arithmetization/src/cpu/incr.rs b/evm_arithmetization/src/cpu/incr.rs index 9a6ae551e..daeaddfd3 100644 --- a/evm_arithmetization/src/cpu/incr.rs +++ b/evm_arithmetization/src/cpu/incr.rs @@ -1,4 +1,3 @@ -use itertools::izip; use plonky2::field::extension::Extendable; use plonky2::field::packed::PackedField; use plonky2::hash::hash_types::RichField; @@ -6,74 +5,13 @@ use plonky2::iop::ext_target::ExtensionTarget; use plonky2::plonk::circuit_builder::CircuitBuilder; use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use crate::cpu::columns::{CpuColumnsView, MemoryChannelView}; -use crate::memory::VALUE_LIMBS; - -/// Constrain two channels such that their values `A` and `B` satisfy -/// `B = A + 1`, by using the `CpuIncrView` helper limbs. -fn channels_incremented_packed( - filter: P, - ch_a: &MemoryChannelView

, - ch_b: &MemoryChannelView

, - helper_limbs: [P; VALUE_LIMBS], - yield_constr: &mut ConstraintConsumer

, -) { - for (limb_a, limb_b, helper) in izip!(ch_a.value, ch_b.value, helper_limbs) { - // If there was an overflow on the current limb, `limb_b` will be 0, else - // we enforce proper increment. - yield_constr.constraint(filter * limb_b * (limb_b - limb_a - helper)); - } -} - -/// Constrain two channels such that their values `A` and `B` satisfy -/// `B = A + 1`, by using the `CpuIncrView` helper limbs. -fn channels_incremented_circuit, const D: usize>( - builder: &mut CircuitBuilder, - filter: ExtensionTarget, - ch_a: &MemoryChannelView>, - ch_b: &MemoryChannelView>, - helper_limbs: [ExtensionTarget; VALUE_LIMBS], - yield_constr: &mut RecursiveConstraintConsumer, -) { - for (limb_a, limb_b, helper) in izip!(ch_a.value, ch_b.value, helper_limbs) { - // If there was an overflow on the current limb, `limb_b` will be 0, else - // we enforce proper increment. - let diff = builder.sub_extension(limb_b, limb_a); - let diff = builder.sub_extension(diff, helper); - let constr = builder.mul_extension(limb_b, diff); - let constr = builder.mul_extension(filter, constr); - yield_constr.constraint(builder, constr); - } -} +use crate::cpu::columns::CpuColumnsView; /// Evaluates the constraints for the DUP and SWAP opcodes. pub(crate) fn eval_packed( lv: &CpuColumnsView

, yield_constr: &mut ConstraintConsumer

, ) { - // Constrain the helper columns. - { - // First limb is always 1. - yield_constr.constraint(lv.op.incr * (lv.general.incr().limbs[0] - P::ONES)); - - // 1s and 0s must be contiguous - for i in 1..VALUE_LIMBS - 1 { - yield_constr.constraint( - lv.op.incr - * (lv.general.incr().limbs[i] - P::ONES) - * lv.general.incr().limbs[i + 1], - ); - } - } - - channels_incremented_packed( - lv.op.incr, - &lv.mem_channels[1], - &lv.mem_channels[2], - lv.general.incr().limbs, - yield_constr, - ); - // Disable the partial channel. yield_constr.constraint(lv.op.incr * lv.partial_channel.used); } @@ -85,30 +23,6 @@ pub(crate) fn eval_ext_circuit, const D: usize>( lv: &CpuColumnsView>, yield_constr: &mut RecursiveConstraintConsumer, ) { - // Constrain the helper columns. - { - // First limb is always 1. - let constr = builder.mul_sub_extension(lv.op.incr, lv.general.incr().limbs[0], lv.op.incr); - yield_constr.constraint(builder, constr); - - // 1s and 0s must be contiguous - for i in 1..VALUE_LIMBS - 1 { - let constr = - builder.mul_sub_extension(lv.op.incr, lv.general.incr().limbs[i], lv.op.incr); - let constr = builder.mul_extension(constr, lv.general.incr().limbs[i + 1]); - yield_constr.constraint(builder, constr); - } - } - - channels_incremented_circuit( - builder, - lv.op.incr, - &lv.mem_channels[1], - &lv.mem_channels[2], - lv.general.incr().limbs, - yield_constr, - ); - // Disable the partial channel. { let constr = builder.mul_extension(lv.op.incr, lv.partial_channel.used); diff --git a/evm_arithmetization/src/witness/operation.rs b/evm_arithmetization/src/witness/operation.rs index 2e095cf41..d89c625c7 100644 --- a/evm_arithmetization/src/witness/operation.rs +++ b/evm_arithmetization/src/witness/operation.rs @@ -19,7 +19,7 @@ use crate::cpu::simple_logic::eq_iszero::generate_pinv_diff; use crate::cpu::stack::MAX_USER_STACK_SIZE; use crate::extension_tower::BN_BASE; use crate::memory::segments::Segment; -use crate::util::{u256_limbs, u256_to_usize}; +use crate::util::u256_to_usize; use crate::witness::errors::MemoryError::VirtTooLarge; use crate::witness::errors::ProgramError; use crate::witness::memory::{MemoryAddress, MemoryChannel, MemoryOp, MemoryOpKind}; @@ -648,33 +648,8 @@ pub(crate) fn generate_incr>( state.push_memory(log_out0); state.push_memory(log_in0); - let in0_limbs = u256_limbs::(in0); - let out0_limbs = u256_limbs::(in0 + 1); - // This is necessary to properly constrain the increment over limbs without - // relying on the Arithmetic table. - for (i, limb) in row.general.incr_mut().limbs.iter_mut().enumerate() { - *limb = if in0_limbs[i] != out0_limbs[i] { - F::ONE - } else { - F::ZERO - } - } - // if n == 0 { - // println!( - // "TOP OF THE STACK: {:?}\n\t{:?}\n\t{:?}\n", - // row.general.incr().limbs, - // row.mem_channels[1], - // row.mem_channels[2], - // ); - // } else { - // println!( - // "REGULAR CHANNEL: {:?}\n\t{:?}\n\t{:?}\n", - // row.general.incr().limbs, - // row.mem_channels[1], - // row.mem_channels[2] - // ); - // } - + let operation = arithmetic::Operation::binary(BinaryOperator::Add, in0, U256::one()); + state.push_arithmetic(operation); state.push_cpu(row); Ok(())