Update

evm_arithmetization/src/all_stark.rs

@@ -175,9 +175,14 @@ pub(crate) fn all_cross_table_lookups<F: Field>() -> Vec<CrossTableLookup<F>> {
 /// module.
 fn ctl_arithmetic<F: Field>() -> CrossTableLookup<F> {
     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(),
     )
 }

evm_arithmetization/src/cpu/columns/general.rs

@@ -15,6 +15,7 @@ pub(crate) union CpuGeneralColumnsView<T: Copy> {
     shift: CpuShiftView<T>,
     stack: CpuStackView<T>,
     push: CpuPushView<T>,
+    incr: CpuIncrView<T>,
     context_pruning: CpuContextPruningView<T>,
 }
 
@@ -93,6 +94,18 @@ impl<T: Copy> CpuGeneralColumnsView<T> {
         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<T> {
+        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<T> {
+        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<T> {
@@ -217,6 +230,17 @@ pub(crate) struct CpuPushView<T: Copy> {
     _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<T: Copy> {
+    /// 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<T: Copy> {
@@ -243,4 +267,5 @@ const_assert!(size_of::<CpuJumpsView<u8>>() == NUM_SHARED_COLUMNS);
 const_assert!(size_of::<CpuShiftView<u8>>() == NUM_SHARED_COLUMNS);
 const_assert!(size_of::<CpuStackView<u8>>() == NUM_SHARED_COLUMNS);
 const_assert!(size_of::<CpuPushView<u8>>() == NUM_SHARED_COLUMNS);
+const_assert!(size_of::<CpuIncrView<u8>>() == NUM_SHARED_COLUMNS);
 const_assert!(size_of::<CpuContextPruningView<u8>>() == NUM_SHARED_COLUMNS);

evm_arithmetization/src/cpu/cpu_stark.rs

@@ -132,7 +132,52 @@ pub(crate) fn ctl_arithmetic_base_rows<F: Field>() -> TableWithColumns<F> {
 }
 
 /// 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<F: Field>() -> TableWithColumns<F> {
+    // 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<F: Field>() -> TableWithColumns<F> {
     // Instead of taking single columns, we reconstruct the entire opcode value
     // directly.
@@ -160,7 +205,13 @@ pub(crate) fn ctl_arithmetic_incr_op<F: Field>() -> TableWithColumns<F> {
     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![],
+        ),
     )
 }
 

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<P: PackedField>(
+pub(crate) fn channels_equal_packed<P: PackedField>(
     filter: P,
     ch_a: &MemoryChannelView<P>,
     ch_b: &MemoryChannelView<P>,
@@ -23,7 +23,7 @@ fn channels_equal_packed<P: PackedField>(
 }
 
 /// Constrain two channels to have equal values.
-fn channels_equal_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
+pub(crate) fn channels_equal_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
     builder: &mut CircuitBuilder<F, D>,
     filter: ExtensionTarget<D>,
     ch_a: &MemoryChannelView<ExtensionTarget<D>>,

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<P: PackedField>(
     lv: &CpuColumnsView<P>,
     nv: &CpuColumnsView<P>,
     yield_constr: &mut ConstraintConsumer<P>,
 ) {
-    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<P: PackedField>(
     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<F: RichField + Extendable<D>, const D: usize>(
     builder: &mut CircuitBuilder<F, D>,
     lv: &CpuColumnsView<ExtensionTarget<D>>,
     nv: &CpuColumnsView<ExtensionTarget<D>>,
     yield_constr: &mut RecursiveConstraintConsumer<F, D>,
 ) {
-    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<F: RichField + Extendable<D>, 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);
 }

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

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
 

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

evm_arithmetization/src/witness/operation.rs

@@ -605,25 +605,36 @@ pub(crate) fn generate_incr<F: RichField, T: Transition<F>>(
     mut row: CpuColumnsView<F>,
 ) -> 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);