Add increment WIP

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 all `CpuGeneralColumn`s, helping to detect any limb overflow
+/// when incrementing by 1.
+#[repr(C)]
+#[derive(Copy, Clone)]
+pub(crate) struct CpuIncrView<T: Copy> {
+    /// 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<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/columns/ops.rs

@@ -39,6 +39,8 @@ pub(crate) struct OpsColumnsView<T: Copy> {
     pub m_op_general: T,
     /// Combines PC and PUSH0
     pub pc_push0: T,
+    /// Flag for INCR_N instructions.
+    pub incr: T,
 
     /// Flag for syscalls.
     pub syscall: T,

evm_arithmetization/src/cpu/contextops.rs

@@ -33,6 +33,7 @@ const KEEPS_CONTEXT: OpsColumnsView<bool> = OpsColumnsView {
     m_op_32bytes: true,
     exit_kernel: true,
     m_op_general: true,
+    incr: true,
     syscall: true,
     exception: true,
 };

evm_arithmetization/src/cpu/cpu_stark.rs

@@ -15,14 +15,13 @@ use starky::lookup::{Column, Filter};
 use starky::stark::Stark;
 
 use super::columns::CpuColumnsView;
-use super::halt;
 use super::kernel::constants::context_metadata::ContextMetadata;
 use super::membus::{NUM_CHANNELS, NUM_GP_CHANNELS};
 use crate::all_stark::{EvmStarkFrame, Table};
 use crate::cpu::columns::{COL_MAP, NUM_CPU_COLUMNS};
 use crate::cpu::{
-    byte_unpacking, clock, contextops, control_flow, decode, dup_swap, gas, jumps, membus, memio,
-    modfp254, pc, push0, shift, simple_logic, stack, syscalls_exceptions,
+    byte_unpacking, clock, contextops, control_flow, decode, dup_swap, gas, halt, incr, jumps,
+    membus, memio, modfp254, pc, push0, shift, simple_logic, stack, syscalls_exceptions,
 };
 use crate::memory::segments::Segment;
 use crate::memory::VALUE_LIMBS;
@@ -612,6 +611,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
         dup_swap::eval_packed(local_values, next_values, yield_constr);
         gas::eval_packed(local_values, next_values, yield_constr);
         halt::eval_packed(local_values, next_values, yield_constr);
+        incr::eval_packed(local_values, yield_constr);
         jumps::eval_packed(local_values, next_values, yield_constr);
         membus::eval_packed(local_values, yield_constr);
         memio::eval_packed(local_values, next_values, yield_constr);
@@ -647,6 +647,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
         dup_swap::eval_ext_circuit(builder, local_values, next_values, yield_constr);
         gas::eval_ext_circuit(builder, local_values, next_values, yield_constr);
         halt::eval_ext_circuit(builder, local_values, next_values, yield_constr);
+        incr::eval_ext_circuit(builder, local_values, yield_constr);
         jumps::eval_ext_circuit(builder, local_values, next_values, yield_constr);
         membus::eval_ext_circuit(builder, local_values, yield_constr);
         memio::eval_ext_circuit(builder, local_values, next_values, yield_constr);

evm_arithmetization/src/cpu/decode.rs

@@ -7,7 +7,7 @@ use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsume
 
 use crate::cpu::columns::{CpuColumnsView, COL_MAP};
 
-const OPCODES_LEN: usize = if cfg!(feature = "cdk_erigon") { 6 } else { 5 };
+const OPCODES_LEN: usize = if cfg!(feature = "cdk_erigon") { 7 } else { 6 };
 
 /// List of opcode blocks
 /// Each block corresponds to exactly one flag, and each flag corresponds to
@@ -46,7 +46,8 @@ const OPCODES: [(u8, usize, bool, usize); OPCODES_LEN] = [
     // JUMPDEST and KECCAK_GENERAL are handled manually here.
     (0x56, 1, false, COL_MAP.op.jumps),     // 0x56-0x57
     (0x80, 5, false, COL_MAP.op.dup_swap),  // 0x80-0x9f
-    (0xf6, 1, true, COL_MAP.op.context_op), //0xf6-0xf7
+    (0xe0, 2, true, COL_MAP.op.incr),       // 0xe0-0xe3
+    (0xf6, 1, true, COL_MAP.op.context_op), // 0xf6-0xf7
     (0xf9, 0, true, COL_MAP.op.exit_kernel),
     // MLOAD_GENERAL and MSTORE_GENERAL flags are handled manually here.
 ];

evm_arithmetization/src/cpu/gas.rs

@@ -37,6 +37,7 @@ const SIMPLE_OPCODES: OpsColumnsView<Option<u32>> = OpsColumnsView {
     m_op_32bytes: KERNEL_ONLY_INSTR,
     exit_kernel: None,
     m_op_general: KERNEL_ONLY_INSTR,
+    incr: KERNEL_ONLY_INSTR,
     syscall: None,
     exception: None,
 };

evm_arithmetization/src/cpu/incr.rs

@@ -0,0 +1,117 @@
+use itertools::izip;
+use plonky2::field::extension::Extendable;
+use plonky2::field::packed::PackedField;
+use plonky2::hash::hash_types::RichField;
+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<P: PackedField>(
+    filter: P,
+    ch_a: &MemoryChannelView<P>,
+    ch_b: &MemoryChannelView<P>,
+    helper_limbs: [P; VALUE_LIMBS],
+    yield_constr: &mut ConstraintConsumer<P>,
+) {
+    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<F: RichField + Extendable<D>, const D: usize>(
+    builder: &mut CircuitBuilder<F, D>,
+    filter: ExtensionTarget<D>,
+    ch_a: &MemoryChannelView<ExtensionTarget<D>>,
+    ch_b: &MemoryChannelView<ExtensionTarget<D>>,
+    helper_limbs: [ExtensionTarget<D>; VALUE_LIMBS],
+    yield_constr: &mut RecursiveConstraintConsumer<F, D>,
+) {
+    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);
+    }
+}
+
+/// Evaluates the constraints for the DUP and SWAP opcodes.
+pub(crate) fn eval_packed<P: PackedField>(
+    lv: &CpuColumnsView<P>,
+    yield_constr: &mut ConstraintConsumer<P>,
+) {
+    // 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);
+}
+
+/// Circuit version of `eval_packed`.
+/// Evaluates the constraints for the DUP and SWAP opcodes.
+pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
+    builder: &mut CircuitBuilder<F, D>,
+    lv: &CpuColumnsView<ExtensionTarget<D>>,
+    yield_constr: &mut RecursiveConstraintConsumer<F, D>,
+) {
+    // 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);
+        yield_constr.constraint(builder, constr);
+    }
+}

evm_arithmetization/src/cpu/kernel/asm/balance.asm

@@ -30,7 +30,7 @@ global balance:
     %mpt_read_state_trie
     // stack: account_ptr, retdest
     DUP1 ISZERO %jumpi(retzero) // If the account pointer is null, return 0.
-    %add_const(1)
+    INCR1
     // stack: balance_ptr, retdest
     %mload_trie_data
     // stack: balance, retdest

evm_arithmetization/src/cpu/kernel/asm/bignum/add.asm

@@ -40,12 +40,10 @@ add_loop:
     // stack: a_cur_addr, c[cur], carry_new,  base_addr, i, a_cur_loc, b_cur_loc, retdest
     %swap_mstore
     // stack: carry_new, base_addr, i, a_cur_loc, b_cur_loc, retdest
-    SWAP3
-    %increment
-    SWAP3
+    INCR4
     // stack: carry_new, base_addr, i, a_cur_loc + 1, b_cur_loc, retdest
     SWAP4
-    %increment
+    INCR1
     SWAP4
     // stack: carry_new, base_addr, i, a_cur_loc + 1, b_cur_loc + 1, retdest
     SWAP2

evm_arithmetization/src/cpu/kernel/asm/bignum/addmul.asm

@@ -87,11 +87,11 @@ addmul_loop:
     // stack: i-1, base_addr, carry_limb, a_cur_loc, b_cur_loc, val, retdest
     SWAP3
     // stack: a_cur_loc, base_addr, carry_limb, i-1, b_cur_loc, val, retdest
-    %increment
+    INCR1
     // stack: a_cur_loc+1, base_addr, carry_limb, i-1, b_cur_loc, val, retdest
     SWAP4
     // stack: b_cur_loc, base_addr, carry_limb, i-1, a_cur_loc+1, val, retdest
-    %increment
+    INCR1
     // stack: b_cur_loc+1, base_addr, carry_limb, i-1, a_cur_loc+1, val, retdest
     %stack (b, addr, c, i, a) -> (c, addr, i, a, b)
     // stack: carry_limb, base_addr, i-1, a_cur_loc+1, b_cur_loc+1, val, retdest

evm_arithmetization/src/cpu/kernel/asm/bignum/isone.asm

@@ -28,8 +28,6 @@ starts_with_one:
     // Starts with one, so check that the remaining limbs are zero.
     // stack: len, start_loc, retdest
     %decrement
-    SWAP1
-    %increment
-    SWAP1
+    INCR2
     // stack: len-1, start_loc+1, retdest
     %jump(iszero_bignum)

evm_arithmetization/src/cpu/kernel/asm/bignum/iszero.asm

@@ -21,7 +21,7 @@ iszero_loop:
     // stack: cur_val, cur_loc, end_loc, retdest
     %jumpi(neqzero)
     // stack: cur_loc, end_loc, retdest
-    %increment
+    INCR1
     // stack: cur_loc + 1, end_loc, retdest
     %stack (vals: 2) -> (vals, vals)
     // stack: cur_loc + 1, end_loc, cur_loc + 1, end_loc, retdest

evm_arithmetization/src/cpu/kernel/asm/bignum/modmul.asm

@@ -36,7 +36,7 @@ modmul_remainder_loop:
     DUP4 ADD // out_addr_i
     %swap_mstore
     // stack: i, base_addr, len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
-    %increment
+    INCR1
     DUP3
     DUP2
     // stack: i+1, len, i+1, base_addr, len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
@@ -89,7 +89,7 @@ modmul_quotient_loop:
     DUP4 ADD // s1_addr_i
     %swap_mstore
     // stack: i, base_addr, 2*len, len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
-    %increment
+    INCR1
     DUP3
     DUP2
     // stack: i+1, 2*len, i+1, base_addr, 2*len, len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
@@ -156,13 +156,12 @@ modmul_check_loop:
     SWAP1
     %decrement
     // stack: n-1, base_addr, i, j, retdest
+    INCR3
     SWAP2
-    %increment
     // stack: i+1, base_addr, n-1, j, retdest
-    SWAP3
-    %increment
-    // stack: j+1, base_addr, n-1, i+1, retdest
-    %stack (j, addr, n, i) -> (n, addr, n, i, j)
+    INCR4
+    // stack: i+1, base_addr, n-1, j+1, retdest
+    %stack (i, addr, n) -> (n, addr, n, i)
     // 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/bignum/mul.asm

@@ -47,11 +47,11 @@ mul_addmul_return:
     %decrement
     // stack: n-1, base_addr, len, a_start_loc, bi, output_cur, retdest
     SWAP4
-    %increment
+    INCR1
     SWAP4
     // stack: n-1, base_addr, len, a_start_loc, bi+1, output_cur, retdest
     SWAP5
-    %increment
+    INCR1
     SWAP5
     // stack: n-1, base_addr, len, a_start_loc, bi+1, output_cur+1, retdest
     DUP1

evm_arithmetization/src/cpu/kernel/asm/bloom_filter.asm

@@ -53,7 +53,7 @@ logs_bloom_loop:
     // stack: log_payload_len_ptr, i, logs_len, retdest
     
     // Add address to bloom filter.
-    %increment
+    INCR1
     // stack: addr_ptr, i, logs_len, retdest
     PUSH @SEGMENT_LOGS_DATA %build_kernel_address
     DUP1
@@ -63,12 +63,12 @@ logs_bloom_loop:
     // stack: is_topic, addr, full_addr_ptr, i, logs_len, retdest
     %add_to_bloom
     // stack: full_addr_ptr, i, logs_len, retdest
-    %increment
+    INCR1
     // stack: full_num_topics_ptr, i, logs_len, retdest
     DUP1
     MLOAD_GENERAL
     // stack: num_topics, full_num_topics_ptr, i, logs_len, retdest
-    SWAP1 %increment
+    INCR2 SWAP1
     // stack: full_topics_ptr, num_topics, i, logs_len, retdest
     PUSH 0
 
@@ -85,13 +85,13 @@ logs_bloom_topic_loop:
     // stack: is_topic, topic, j, topics_ptr, num_topics, i, logs_len, retdest
     %add_to_bloom
     // stack: j, topics_ptr, num_topics, i, logs_len, retdest
-    %increment
+    INCR1
     %jump(logs_bloom_topic_loop)
 
 logs_bloom_topic_end:
     // stack: num_topics, topics_ptr, num_topics, i, logs_len, retdest
     %pop3
-    %increment
+    INCR1
     %jump(logs_bloom_loop)
 
 logs_bloom_end: