From b7105bf6915d63ccd3b553929ebf55207aabc154 Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Wed, 13 Nov 2024 18:55:56 -0500 Subject: [PATCH] Update --- evm_arithmetization/src/all_stark.rs | 9 +- .../src/cpu/columns/general.rs | 25 ++++++ evm_arithmetization/src/cpu/cpu_stark.rs | 55 +++++++++++- evm_arithmetization/src/cpu/dup_swap.rs | 4 +- evm_arithmetization/src/cpu/incr.rs | 85 +++++++++++++++---- .../src/cpu/kernel/asm/bignum/modmul.asm | 9 +- .../src/cpu/kernel/asm/core/exception.asm | 2 +- .../src/cpu/kernel/asm/hash/ripemd/update.asm | 2 - evm_arithmetization/src/witness/operation.rs | 43 ++++++---- 9 files changed, 186 insertions(+), 48 deletions(-) diff --git a/evm_arithmetization/src/all_stark.rs b/evm_arithmetization/src/all_stark.rs index 36157be75..64819ff03 100644 --- a/evm_arithmetization/src/all_stark.rs +++ b/evm_arithmetization/src/all_stark.rs @@ -175,9 +175,14 @@ pub(crate) fn all_cross_table_lookups() -> Vec> { /// module. fn ctl_arithmetic() -> CrossTableLookup { let cpu_arithmetic_looking = cpu_stark::ctl_arithmetic_base_rows(); - let cpu_increment_looking = cpu_stark::ctl_arithmetic_incr_op(); + let cpu_incr1_looking = cpu_stark::ctl_arithmetic_incr1_op(); + let cpu_incr_other_looking = cpu_stark::ctl_arithmetic_incr_op(); CrossTableLookup::new( - vec![cpu_arithmetic_looking, cpu_increment_looking], + vec![ + cpu_arithmetic_looking, + cpu_incr1_looking, + cpu_incr_other_looking, + ], arithmetic_stark::ctl_arithmetic_rows(), ) } diff --git a/evm_arithmetization/src/cpu/columns/general.rs b/evm_arithmetization/src/cpu/columns/general.rs index 97f8b8f49..0b7c18820 100644 --- a/evm_arithmetization/src/cpu/columns/general.rs +++ b/evm_arithmetization/src/cpu/columns/general.rs @@ -15,6 +15,7 @@ pub(crate) union CpuGeneralColumnsView { shift: CpuShiftView, stack: CpuStackView, push: CpuPushView, + incr: CpuIncrView, context_pruning: CpuContextPruningView, } @@ -93,6 +94,18 @@ 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 { @@ -217,6 +230,17 @@ pub(crate) struct CpuPushView { _padding_columns: [T; NUM_SHARED_COLUMNS - 1], } +/// View of the first `CpuGeneralColumn` storing the sum of the first 2 opcode +/// bits to filter out `INCR1` instruction from the other ones (INCR2-INCR4). +#[repr(C)] +#[derive(Copy, Clone)] +pub(crate) struct CpuIncrView { + /// Product of `incr` flag with the sum of the first 2 opcode bits. + pub(crate) is_not_incr1: T, + /// Reserve the unused columns. + _padding_columns: [T; NUM_SHARED_COLUMNS - 1], +} + /// View of the first `CpuGeneralColumn` storing a flag for context pruning. #[derive(Copy, Clone)] pub(crate) struct CpuContextPruningView { @@ -243,4 +267,5 @@ 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/cpu_stark.rs b/evm_arithmetization/src/cpu/cpu_stark.rs index 33955eeaf..a61616b32 100644 --- a/evm_arithmetization/src/cpu/cpu_stark.rs +++ b/evm_arithmetization/src/cpu/cpu_stark.rs @@ -132,7 +132,52 @@ pub(crate) fn ctl_arithmetic_base_rows() -> TableWithColumns { } /// Returns the `TableWithColumns` for the CPU rows calling arithmetic -/// `ADD` operations through the `INCR` privileged instructions. +/// `ADD` operations through the `INCR1` privileged instruction. +/// +/// It requires a different CTL than `INCR2`-`INCR4` as it does not incur any +/// memory reads. +pub(crate) fn ctl_arithmetic_incr1_op() -> TableWithColumns { + // Instead of taking single columns, we reconstruct the entire opcode value + // directly. + let mut columns = vec![Column::constant(F::from_canonical_u8(get_opcode("ADD")))]; + + // Read value: current top of the stack + columns.extend(Column::singles(COL_MAP.mem_channels[0].value)); + + // Fixed second operand (`U256::one()`) + { + columns.push(Column::constant(F::ONE)); + for _ in 1..VALUE_LIMBS { + columns.push(Column::constant(F::ZERO)); + } + } + + // Ignored third operand, `ADD` is a binary operation + for _ in 0..VALUE_LIMBS { + columns.push(Column::constant(F::ZERO)); + } + + // Returned value: next top of the stack + columns.extend(Column::singles_next_row(COL_MAP.mem_channels[0].value)); + + TableWithColumns::new( + *Table::Cpu, + columns, + Filter::new( + vec![( + Column::single(COL_MAP.op.incr), + Column::linear_combination_with_constant( + [(COL_MAP.general.incr().is_not_incr1, -F::ONE)], + F::ONE, + ), + )], + vec![], + ), + ) +} + +/// Returns the `TableWithColumns` for the CPU rows calling arithmetic +/// `ADD` operations through the `INCR2`-`INCR4` privileged instructions. pub(crate) fn ctl_arithmetic_incr_op() -> TableWithColumns { // Instead of taking single columns, we reconstruct the entire opcode value // directly. @@ -160,7 +205,13 @@ pub(crate) fn ctl_arithmetic_incr_op() -> TableWithColumns { TableWithColumns::new( *Table::Cpu, columns, - Filter::new_simple(Column::single(COL_MAP.op.incr)), + Filter::new( + vec![( + Column::single(COL_MAP.op.incr), + Column::single(COL_MAP.general.incr().is_not_incr1), + )], + vec![], + ), ) } diff --git a/evm_arithmetization/src/cpu/dup_swap.rs b/evm_arithmetization/src/cpu/dup_swap.rs index 90cbd5c9e..ab48cd320 100644 --- a/evm_arithmetization/src/cpu/dup_swap.rs +++ b/evm_arithmetization/src/cpu/dup_swap.rs @@ -11,7 +11,7 @@ use crate::cpu::columns::{CpuColumnsView, MemoryChannelView}; use crate::memory::segments::Segment; /// Constrain two channels to have equal values. -fn channels_equal_packed( +pub(crate) fn channels_equal_packed( filter: P, ch_a: &MemoryChannelView

, ch_b: &MemoryChannelView

, @@ -23,7 +23,7 @@ fn channels_equal_packed( } /// Constrain two channels to have equal values. -fn channels_equal_ext_circuit, const D: usize>( +pub(crate) fn channels_equal_ext_circuit, const D: usize>( builder: &mut CircuitBuilder, filter: ExtensionTarget, ch_a: &MemoryChannelView>, diff --git a/evm_arithmetization/src/cpu/incr.rs b/evm_arithmetization/src/cpu/incr.rs index 9104a7c62..6640235ca 100644 --- a/evm_arithmetization/src/cpu/incr.rs +++ b/evm_arithmetization/src/cpu/incr.rs @@ -6,23 +6,34 @@ use plonky2::iop::ext_target::ExtensionTarget; use plonky2::plonk::circuit_builder::CircuitBuilder; use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; -use super::dup_swap::{constrain_channel_ext_circuit, constrain_channel_packed}; +use super::dup_swap::{ + channels_equal_ext_circuit, channels_equal_packed, constrain_channel_ext_circuit, + constrain_channel_packed, +}; use crate::cpu::columns::CpuColumnsView; -/// Evaluates the constraints for the DUP and SWAP opcodes. +/// Evaluates the constraints for the INCR opcodes. pub(crate) fn eval_packed( lv: &CpuColumnsView

, nv: &CpuColumnsView

, yield_constr: &mut ConstraintConsumer

, ) { - let filter = lv.op.incr; + let base_filter = lv.op.incr; - let n = lv.opcode_bits[0] - + lv.opcode_bits[1] * P::Scalar::from_canonical_u64(2) - + lv.opcode_bits[2] * P::Scalar::from_canonical_u64(4); + // Constrain the helper column + yield_constr.constraint( + base_filter + * (lv.general.incr().is_not_incr1 - lv.opcode_bits[0]) + * (lv.general.incr().is_not_incr1 - lv.opcode_bits[1]), + ); + + let filter = base_filter * lv.general.incr().is_not_incr1; + let filter_incr1 = base_filter * (lv.general.incr().is_not_incr1 - P::ONES); - // Disable the partial channel. - yield_constr.constraint(lv.op.incr * lv.partial_channel.used); + let n = lv.opcode_bits[0] + lv.opcode_bits[1] * P::Scalar::from_canonical_u64(2); + + // Disable the partial channel for all instructions. + yield_constr.constraint(base_filter * lv.partial_channel.used); // Constrain the input channel's address, `is_read` and `used` fields. let read_channel = &lv.mem_channels[1]; @@ -32,30 +43,55 @@ pub(crate) fn eval_packed( let write_channel = &lv.mem_channels[2]; constrain_channel_packed(false, filter, n, write_channel, lv, yield_constr); - // Constrain the unchanged stack len. - yield_constr.constraint_transition(filter * (nv.stack_len - lv.stack_len)); + // Constrain the unchanged stack len for all instructions. + yield_constr.constraint_transition(base_filter * (nv.stack_len - lv.stack_len)); + + // Constrain the unchanged stack top for INCR2-INCR4. + channels_equal_packed( + filter, + &lv.mem_channels[0], + &nv.mem_channels[0], + yield_constr, + ); + + // Disable regular read and write channels for INCR1. + yield_constr.constraint(filter_incr1 * lv.mem_channels[1].used); + yield_constr.constraint(filter_incr1 * lv.mem_channels[2].used); } /// Circuit version of `eval_packed`. -/// Evaluates the constraints for the DUP and SWAP opcodes. +/// Evaluates the constraints for the INCR opcodes. pub(crate) fn eval_ext_circuit, const D: usize>( builder: &mut CircuitBuilder, lv: &CpuColumnsView>, nv: &CpuColumnsView>, yield_constr: &mut RecursiveConstraintConsumer, ) { - let filter = lv.op.incr; + let base_filter = lv.op.incr; + + // Constrain the helper column + { + let diff_bit1 = builder.sub_extension(lv.general.incr().is_not_incr1, lv.opcode_bits[0]); + let diff_bit2 = builder.sub_extension(lv.general.incr().is_not_incr1, lv.opcode_bits[1]); + let constr = builder.mul_extension(base_filter, diff_bit1); + let constr = builder.mul_extension(constr, diff_bit2); + yield_constr.constraint(builder, constr); + } + + let filter = builder.mul_extension(base_filter, lv.general.incr().is_not_incr1); + let filter_incr1 = + builder.mul_sub_extension(base_filter, lv.general.incr().is_not_incr1, base_filter); - let n = lv.opcode_bits[..3].iter().enumerate().fold( + let n = lv.opcode_bits[..2].iter().enumerate().fold( builder.zero_extension(), |cumul, (i, &bit)| { builder.mul_const_add_extension(F::from_canonical_u64(1 << i), bit, cumul) }, ); - // Disable the partial channel. + // Disable the partial channel for all instructions. { - let constr = builder.mul_extension(lv.op.incr, lv.partial_channel.used); + let constr = builder.mul_extension(base_filter, lv.partial_channel.used); yield_constr.constraint(builder, constr); } @@ -67,10 +103,25 @@ pub(crate) fn eval_ext_circuit, const D: usize>( let write_channel = &lv.mem_channels[2]; constrain_channel_ext_circuit(builder, false, filter, n, write_channel, lv, yield_constr); - // Constrain the unchanged stack len. + // Constrain the unchanged stack len for all instructions. { let diff = builder.sub_extension(nv.stack_len, lv.stack_len); - let constr = builder.mul_extension(filter, diff); + let constr = builder.mul_extension(base_filter, diff); yield_constr.constraint_transition(builder, constr); } + + // Constrain the unchanged stack top for INCR2-INCR4. + channels_equal_ext_circuit( + builder, + filter, + &lv.mem_channels[0], + &nv.mem_channels[0], + yield_constr, + ); + + // Disable regular read and write channels for INCR1. + let constr = builder.mul_extension(filter_incr1, lv.mem_channels[1].used); + yield_constr.constraint(builder, constr); + let constr = builder.mul_extension(filter_incr1, lv.mem_channels[2].used); + yield_constr.constraint(builder, constr); } diff --git a/evm_arithmetization/src/cpu/kernel/asm/bignum/modmul.asm b/evm_arithmetization/src/cpu/kernel/asm/bignum/modmul.asm index 17b770816..901a0fc9e 100644 --- a/evm_arithmetization/src/cpu/kernel/asm/bignum/modmul.asm +++ b/evm_arithmetization/src/cpu/kernel/asm/bignum/modmul.asm @@ -156,12 +156,9 @@ modmul_check_loop: SWAP1 %decrement // stack: n-1, base_addr, i, j, retdest - INCR3 - SWAP2 - // stack: i+1, base_addr, n-1, j, retdest - INCR4 - // stack: i+1, base_addr, n-1, j+1, retdest - %stack (i, addr, n) -> (n, addr, n, i) + INCR3 INCR4 + // stack: n-1, base_addr, i+1, j+1, retdest + %stack (n, addr) -> (n, addr, n) // stack: n-1, base_addr, n-1, i+1, j+1, retdest %jumpi(modmul_check_loop) // end of modmul_check_loop diff --git a/evm_arithmetization/src/cpu/kernel/asm/core/exception.asm b/evm_arithmetization/src/cpu/kernel/asm/core/exception.asm index 1de3eac3f..c95549a83 100644 --- a/evm_arithmetization/src/cpu/kernel/asm/core/exception.asm +++ b/evm_arithmetization/src/cpu/kernel/asm/core/exception.asm @@ -420,7 +420,7 @@ min_stack_len_for_opcode: BYTES 3 // 0xe2, INCR3 BYTES 4 // 0xe3, INCR4 - %rep 12 // 0xe5-0xef, invalid + %rep 12 // 0xe4-0xef, invalid BYTES 0 %endrep diff --git a/evm_arithmetization/src/cpu/kernel/asm/hash/ripemd/update.asm b/evm_arithmetization/src/cpu/kernel/asm/hash/ripemd/update.asm index a05a36d69..20b8f469c 100644 --- a/evm_arithmetization/src/cpu/kernel/asm/hash/ripemd/update.asm +++ b/evm_arithmetization/src/cpu/kernel/asm/hash/ripemd/update.asm @@ -121,8 +121,6 @@ buffer_update: // stack: get , set , times , retdest INCR1 INCR2 - SWAP1 - SWAP1 SWAP2 %decrement SWAP2 diff --git a/evm_arithmetization/src/witness/operation.rs b/evm_arithmetization/src/witness/operation.rs index 7561a22c7..7b105901d 100644 --- a/evm_arithmetization/src/witness/operation.rs +++ b/evm_arithmetization/src/witness/operation.rs @@ -605,25 +605,36 @@ pub(crate) fn generate_incr>( mut row: CpuColumnsView, ) -> Result<(), ProgramError> { let generation_state = state.get_mut_generation_state(); - let offset = generation_state - .registers - .stack_len - .checked_sub(1 + (n as usize)) - .ok_or(ProgramError::StackUnderflow)?; - let addr = MemoryAddress::new(generation_state.registers.context, Segment::Stack, offset); - - let (val, log_in0) = mem_read_gp_with_log_and_fill(1, addr, generation_state, &mut row); - let new_val = val.overflowing_add(1.into()).0; - // Write the read value, incremented by 1. - let log_out0 = mem_write_gp_log_and_fill(2, addr, generation_state, &mut row, new_val); + let val = if n == 0 { + let val = generation_state.registers.stack_top; - // Manually increment the top of the stack if calling INCR1. - if n == 0 { + // Manually increment the top of the stack if calling INCR1. generation_state.registers.stack_top += U256::one(); - } - state.push_memory(log_in0); - state.push_memory(log_out0); + + val + } else { + let offset = generation_state + .registers + .stack_len + .checked_sub(1 + (n as usize)) + .ok_or(ProgramError::StackUnderflow)?; + let addr = MemoryAddress::new(generation_state.registers.context, Segment::Stack, offset); + + let (val, log_in0) = mem_read_gp_with_log_and_fill(1, addr, generation_state, &mut row); + let new_val = val.overflowing_add(1.into()).0; + + // Write the read value, incremented by 1. + let log_out0 = mem_write_gp_log_and_fill(2, addr, generation_state, &mut row, new_val); + + // Set the general helper column. + row.general.incr_mut().is_not_incr1 = F::ONE; + + state.push_memory(log_in0); + state.push_memory(log_out0); + + val + }; let operation = arithmetic::Operation::binary(BinaryOperator::Add, val, U256::one()); state.push_arithmetic(operation);