Add memory checks for prover_input and range_checks for prover_input,…

… syscalls and exceptions

evm/src/all_stark.rs

@@ -108,7 +108,11 @@ pub(crate) fn all_cross_table_lookups<F: Field>() -> Vec<CrossTableLookup<F>> {
 
 fn ctl_arithmetic<F: Field>() -> CrossTableLookup<F> {
     CrossTableLookup::new(
-        vec![cpu_stark::ctl_arithmetic_rows()],
+        vec![
+            cpu_stark::ctl_arithmetic_rows(),
+            cpu_stark::ctl_sys_exc_check_rows(),
+            cpu_stark::ctl_prover_input_check_rows(),
+        ],
         arithmetic_stark::ctl_arithmetic_rows(),
     )
 }

evm/src/arithmetic/arithmetic_stark.rs

@@ -49,7 +49,7 @@ fn cpu_arith_data_link<F: Field>(ops: &[usize], regs: &[Range<usize>]) -> Vec<Co
 }
 
 pub fn ctl_arithmetic_rows<F: Field>() -> TableWithColumns<F> {
-    const ARITH_OPS: [usize; 14] = [
+    const ARITH_OPS: [usize; 15] = [
         columns::IS_ADD,
         columns::IS_SUB,
         columns::IS_MUL,
@@ -64,6 +64,7 @@ pub fn ctl_arithmetic_rows<F: Field>() -> TableWithColumns<F> {
         columns::IS_DIV,
         columns::IS_MOD,
         columns::IS_BYTE,
+        columns::IS_RANGE_CHECK,
     ];
 
     const REGISTER_MAP: [Range<usize>; 4] = [
@@ -90,7 +91,7 @@ pub struct ArithmeticStark<F, const D: usize> {
     pub f: PhantomData<F>,
 }
 
-const RANGE_MAX: usize = 1usize << 16; // Range check strict upper bound
+pub(crate) const RANGE_MAX: usize = 1usize << 16; // Range check strict upper bound
 
 impl<F: RichField, const D: usize> ArithmeticStark<F, D> {
     /// Expects input in *column*-major layout

evm/src/arithmetic/columns.rs

@@ -36,8 +36,9 @@ pub(crate) const IS_SUBMOD: usize = IS_SUBFP254 + 1;
 pub(crate) const IS_LT: usize = IS_SUBMOD + 1;
 pub(crate) const IS_GT: usize = IS_LT + 1;
 pub(crate) const IS_BYTE: usize = IS_GT + 1;
+pub(crate) const IS_RANGE_CHECK: usize = IS_BYTE + 1;
 
-pub(crate) const START_SHARED_COLS: usize = IS_BYTE + 1;
+pub(crate) const START_SHARED_COLS: usize = IS_RANGE_CHECK + 1;
 
 /// Within the Arithmetic Unit, there are shared columns which can be
 /// used by any arithmetic circuit, depending on which one is active
@@ -110,5 +111,6 @@ pub(crate) const MODULAR_DIV_DENOM_IS_ZERO: usize = AUX_REGISTER_2.end;
 pub(crate) const NUM_RANGE_CHECK_COLS: usize = 1 + 2 * NUM_SHARED_COLS;
 pub(crate) const RANGE_COUNTER: usize = START_SHARED_COLS + NUM_SHARED_COLS;
 pub(crate) const RC_COLS: Range<usize> = RANGE_COUNTER + 1..RANGE_COUNTER + 1 + 2 * NUM_SHARED_COLS;
+pub(crate) const NUM_CPU_LIMBS: usize = 8;
 
 pub const NUM_ARITH_COLUMNS: usize = START_SHARED_COLS + NUM_SHARED_COLS + NUM_RANGE_CHECK_COLS;

evm/src/arithmetic/mod.rs

@@ -1,6 +1,9 @@
 use ethereum_types::U256;
 use plonky2::field::types::PrimeField64;
 
+use self::columns::NUM_CPU_LIMBS;
+use crate::arithmetic::arithmetic_stark::RANGE_MAX;
+use crate::arithmetic::columns::{IS_RANGE_CHECK, NUM_SHARED_COLS, START_SHARED_COLS};
 use crate::extension_tower::BN_BASE;
 use crate::util::{addmod, mulmod, submod};
 
@@ -107,6 +110,7 @@ impl TernaryOperator {
     }
 }
 
+#[allow(clippy::enum_variant_names)]
 #[derive(Debug)]
 pub(crate) enum Operation {
     BinaryOperation {
@@ -122,6 +126,9 @@ pub(crate) enum Operation {
         input2: U256,
         result: U256,
     },
+    RangeCheckOperation {
+        values: [u32; NUM_CPU_LIMBS],
+    },
 }
 
 impl Operation {
@@ -151,10 +158,15 @@ impl Operation {
         }
     }
 
+    pub(crate) fn range_check(values: [u32; NUM_CPU_LIMBS]) -> Self {
+        Self::RangeCheckOperation { values }
+    }
+
     pub(crate) fn result(&self) -> U256 {
         match self {
             Operation::BinaryOperation { result, .. } => *result,
             Operation::TernaryOperation { result, .. } => *result,
+            _ => panic!("This function should not be called for range checks."),
         }
     }
 
@@ -179,6 +191,7 @@ impl Operation {
                 input2,
                 result,
             } => ternary_op_to_rows(operator.row_filter(), input0, input1, input2, result),
+            Operation::RangeCheckOperation { values } => range_check_to_rows(&values),
         }
     }
 }
@@ -232,3 +245,17 @@ fn binary_op_to_rows<F: PrimeField64>(
         }
     }
 }
+
+fn range_check_to_rows<F: PrimeField64>(values: &[u32; NUM_CPU_LIMBS]) -> (Vec<F>, Option<Vec<F>>) {
+    // Each value is 32 bits long, so we split them into two 16-bit limbs.
+    assert!(2 * values.len() <= NUM_SHARED_COLS);
+    let mut row = vec![F::ZERO; columns::NUM_ARITH_COLUMNS];
+    row[IS_RANGE_CHECK] = F::ONE;
+    for i in 0..values.len() {
+        let low_limb = values[i] % RANGE_MAX as u32;
+        let high_limb = values[i] / RANGE_MAX as u32;
+        row[START_SHARED_COLS + 2 * i] = F::from_canonical_u32(low_limb);
+        row[START_SHARED_COLS + 2 * i + 1] = F::from_canonical_u32(high_limb);
+    }
+    (row, None)
+}

evm/src/cpu/cpu_stark.rs

@@ -22,6 +22,29 @@ use crate::memory::{NUM_CHANNELS, VALUE_LIMBS};
 use crate::stark::Stark;
 use crate::vars::{StarkEvaluationTargets, StarkEvaluationVars};
 
+const OPS: [usize; 14] = [
+    COL_MAP.op.add,
+    COL_MAP.op.sub,
+    COL_MAP.op.mul,
+    COL_MAP.op.lt,
+    COL_MAP.op.gt,
+    COL_MAP.op.addfp254,
+    COL_MAP.op.mulfp254,
+    COL_MAP.op.subfp254,
+    COL_MAP.op.addmod,
+    COL_MAP.op.mulmod,
+    COL_MAP.op.submod,
+    COL_MAP.op.div,
+    COL_MAP.op.mod_,
+    COL_MAP.op.byte,
+];
+
+const EXTRA_OPS: [usize; 3] = [
+    COL_MAP.op.syscall,
+    COL_MAP.op.exception,
+    COL_MAP.op.prover_input,
+];
+
 pub fn ctl_data_keccak_sponge<F: Field>() -> Vec<Column<F>> {
     // When executing KECCAK_GENERAL, the GP memory channels are used as follows:
     // GP channel 0: stack[-1] = context
@@ -60,8 +83,9 @@ fn ctl_data_binops<F: Field>(ops: &[usize]) -> Vec<Column<F>> {
 
 /// Create the vector of Columns corresponding to the three inputs and
 /// one output of a ternary operation.
-fn ctl_data_ternops<F: Field>(ops: &[usize]) -> Vec<Column<F>> {
+fn ctl_data_ternops<F: Field>(ops: &[usize], extra_ops: &[usize]) -> Vec<Column<F>> {
     let mut res = Column::singles(ops).collect_vec();
+    res.push(Column::sum(extra_ops));
     res.extend(Column::singles(COL_MAP.mem_channels[0].value));
     res.extend(Column::singles(COL_MAP.mem_channels[1].value));
     res.extend(Column::singles(COL_MAP.mem_channels[2].value));
@@ -71,6 +95,33 @@ fn ctl_data_ternops<F: Field>(ops: &[usize]) -> Vec<Column<F>> {
     res
 }
 
+fn ctl_data_sys_exc_range_check<F: Field>(ops: &[usize], extra_ops: &[usize]) -> Vec<Column<F>> {
+    // All arithmetic flags are 0 when the operation is either a syscall or an exception
+    let mut res = Column::singles(ops).collect_vec();
+    res.push(Column::sum(extra_ops));
+    res.push(Column::single(
+        COL_MAP.mem_channels[NUM_GP_CHANNELS - 1].value[6],
+    ));
+    // Since we only need to check one limb, the rest of the columns are 0.
+    res.extend(vec![Column::zero(); VALUE_LIMBS * 4 - 1]);
+    res
+}
+
+fn ctl_data_prover_input_range_check<F: Field>(
+    ops: &[usize],
+    extra_ops: &[usize],
+) -> Vec<Column<F>> {
+    // All arithmetic flags are 0 when the operation is prover_input
+    let mut res = Column::singles(ops).collect_vec();
+    res.push(Column::sum(extra_ops));
+    res.extend(Column::singles(
+        COL_MAP.mem_channels[NUM_GP_CHANNELS - 1].value,
+    ));
+    // Since we only need to check one `U256`'s limbs, the rest of the columns are set to 0.
+    res.extend(vec![Column::zero(); VALUE_LIMBS * 3]);
+    res
+}
+
 pub fn ctl_data_logic<F: Field>() -> Vec<Column<F>> {
     ctl_data_binops(&[COL_MAP.op.and, COL_MAP.op.or, COL_MAP.op.xor])
 }
@@ -79,29 +130,39 @@ pub fn ctl_filter_logic<F: Field>() -> Column<F> {
     Column::sum([COL_MAP.op.and, COL_MAP.op.or, COL_MAP.op.xor])
 }
 
+pub fn ctl_sys_exc_check_rows<F: Field>() -> TableWithColumns<F> {
+    // Create the CPU Table whose columns are the gas value and the rest of the columns are 0.
+    let filter = Some(Column::sum([COL_MAP.op.syscall, COL_MAP.op.exception]));
+
+    TableWithColumns::new(
+        Table::Cpu,
+        ctl_data_sys_exc_range_check(&OPS, &EXTRA_OPS),
+        filter,
+    )
+}
+
+pub fn ctl_prover_input_check_rows<F: Field>() -> TableWithColumns<F> {
+    // Create the CPU Table whose columns are the gas value and the rest of the columns are 0.
+    let filter = Some(Column::single(COL_MAP.op.prover_input));
+
+    TableWithColumns::new(
+        Table::Cpu,
+        ctl_data_prover_input_range_check(&OPS, &EXTRA_OPS),
+        filter,
+    )
+}
+
 pub fn ctl_arithmetic_rows<F: Field>() -> TableWithColumns<F> {
-    const OPS: [usize; 14] = [
-        COL_MAP.op.add,
-        COL_MAP.op.sub,
-        COL_MAP.op.mul,
-        COL_MAP.op.lt,
-        COL_MAP.op.gt,
-        COL_MAP.op.addfp254,
-        COL_MAP.op.mulfp254,
-        COL_MAP.op.subfp254,
-        COL_MAP.op.addmod,
-        COL_MAP.op.mulmod,
-        COL_MAP.op.submod,
-        COL_MAP.op.div,
-        COL_MAP.op.mod_,
-        COL_MAP.op.byte,
-    ];
     // Create the CPU Table whose columns are those with the three
     // inputs and one output of the ternary operations listed in `ops`
     // (also `ops` is used as the operation filter). The list of
     // operations includes binary operations which will simply ignore
     // the third input.
-    TableWithColumns::new(Table::Cpu, ctl_data_ternops(&OPS), Some(Column::sum(OPS)))
+    TableWithColumns::new(
+        Table::Cpu,
+        ctl_data_ternops(&OPS, &EXTRA_OPS),
+        Some(Column::sum(OPS)),
+    )
 }
 
 pub const MEM_CODE_CHANNEL_IDX: usize = 0;

evm/src/cpu/stack.rs

@@ -75,7 +75,11 @@ const STACK_BEHAVIORS: OpsColumnsView<Option<StackBehavior>> = OpsColumnsView {
         pushes: true,
         disable_other_channels: true,
     }),
-    prover_input: None, // TODO
+    prover_input: Some(StackBehavior {
+        num_pops: 0,
+        pushes: true,
+        disable_other_channels: true,
+    }),
     pop: Some(StackBehavior {
         num_pops: 1,
         pushes: false,

evm/src/witness/operation.rs

@@ -163,6 +163,14 @@ pub(crate) fn generate_prover_input<F: Field>(
     let input = state.prover_input(input_fn);
     let write = stack_push_log_and_fill(state, &mut row, input)?;
 
+    let input_limbs: [u64; 4] = input.0;
+    let mut values = [0_u32; 8];
+    for (i, limb) in input_limbs.into_iter().enumerate() {
+        values[2 * i] = limb as u32;
+        values[2 * i + 1] = (limb >> 32) as u32;
+    }
+    let range_check_op = arithmetic::Operation::range_check(values);
+    state.traces.push_arithmetic(range_check_op);
     state.traces.push_memory(write);
     state.traces.push_cpu(row);
     Ok(())
@@ -577,6 +585,12 @@ pub(crate) fn generate_syscall<F: Field>(
         + (U256::from(u64::from(state.registers.is_kernel)) << 32)
         + (U256::from(state.registers.gas_used) << 192);
 
+    let mut values = [0_u32; 8];
+    let gas = state.registers.gas_used;
+    values[0] = gas as u32;
+    values[1] = (gas >> 32) as u32;
+
+    let range_check_op = arithmetic::Operation::range_check(values);
     // Set registers before pushing to the stack; in particular, we need to set kernel mode so we
     // can't incorrectly trigger a stack overflow. However, note that we have to do it _after_ we
     // make `syscall_info`, which should contain the old values.
@@ -588,6 +602,7 @@ pub(crate) fn generate_syscall<F: Field>(
 
     log::debug!("Syscall to {}", KERNEL.offset_name(new_program_counter));
 
+    state.traces.push_arithmetic(range_check_op);
     state.traces.push_memory(log_in0);
     state.traces.push_memory(log_in1);
     state.traces.push_memory(log_in2);
@@ -752,6 +767,11 @@ pub(crate) fn generate_exception<F: Field>(
     let exc_info =
         U256::from(state.registers.program_counter) + (U256::from(state.registers.gas_used) << 192);
 
+    let mut values = [0_u32; 8];
+    let gas = state.registers.gas_used;
+    values[0] = gas as u32;
+    values[1] = (gas >> 32) as u32;
+    let range_check_op = arithmetic::Operation::range_check(values);
     // Set registers before pushing to the stack; in particular, we need to set kernel mode so we
     // can't incorrectly trigger a stack overflow. However, note that we have to do it _after_ we
     // make `exc_info`, which should contain the old values.
@@ -762,7 +782,7 @@ pub(crate) fn generate_exception<F: Field>(
     let log_out = stack_push_log_and_fill(state, &mut row, exc_info)?;
 
     log::debug!("Exception to {}", KERNEL.offset_name(new_program_counter));
-
+    state.traces.push_arithmetic(range_check_op);
     state.traces.push_memory(log_in0);
     state.traces.push_memory(log_in1);
     state.traces.push_memory(log_in2);