Add CTLs

evm_arithmetization/src/all_stark.rs

@@ -159,8 +159,10 @@ pub(crate) fn all_cross_table_lookups<F: Field>() -> Vec<CrossTableLookup<F>> {
 /// `CrossTableLookup` for `ArithmeticStark`, to connect it with the `Cpu`
 /// 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();
     CrossTableLookup::new(
-        vec![cpu_stark::ctl_arithmetic_base_rows()],
+        vec![cpu_arithmetic_looking, cpu_increment_looking],
         arithmetic_stark::ctl_arithmetic_rows(),
     )
 }

evm_arithmetization/src/cpu/cpu_stark.rs

@@ -16,6 +16,7 @@ use starky::stark::Stark;
 
 use super::columns::CpuColumnsView;
 use super::kernel::constants::context_metadata::ContextMetadata;
+use super::kernel::opcodes::get_opcode;
 use super::membus::{NUM_CHANNELS, NUM_GP_CHANNELS};
 use crate::all_stark::{EvmStarkFrame, Table};
 use crate::cpu::columns::{COL_MAP, NUM_CPU_COLUMNS};
@@ -130,6 +131,39 @@ 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.
+pub(crate) fn ctl_arithmetic_incr_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
+    columns.extend(Column::singles(COL_MAP.mem_channels[1].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
+    columns.extend(Column::singles(COL_MAP.mem_channels[2].value));
+
+    TableWithColumns::new(
+        *Table::Cpu,
+        columns,
+        Filter::new_simple(Column::single(COL_MAP.op.incr)),
+    )
+}
+
 /// Returns a column containing stale contexts.
 pub(crate) fn ctl_context_pruning_looked<F: Field>() -> TableWithColumns<F> {
     TableWithColumns::new(