diff --git a/evm/src/cpu/cpu_stark.rs b/evm/src/cpu/cpu_stark.rs index 7ee204ca..b11ff9f5 100644 --- a/evm/src/cpu/cpu_stark.rs +++ b/evm/src/cpu/cpu_stark.rs @@ -11,8 +11,8 @@ use plonky2::hash::hash_types::RichField; use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; use crate::cpu::columns::{CpuColumnsView, COL_MAP, NUM_CPU_COLUMNS}; use crate::cpu::{ - bootstrap_kernel, control_flow, decode, jumps, membus, simple_logic, stack, stack_bounds, - syscalls, + bootstrap_kernel, control_flow, decode, dup_swap, jumps, membus, simple_logic, stack, + stack_bounds, syscalls, }; use crate::cross_table_lookup::Column; use crate::memory::segments::Segment; @@ -147,6 +147,7 @@ impl, const D: usize> Stark for CpuStark, const D: usize> Stark for CpuStark( + filter: P, + ch_a: &MemoryChannelView

, + ch_b: &MemoryChannelView

, + yield_constr: &mut ConstraintConsumer

, +) { + for (limb_a, limb_b) in izip!(ch_a.value, ch_b.value) { + yield_constr.constraint(filter * (limb_a - limb_b)); + } +} + +/// Constrain two channels to have equal values. +fn channels_equal_ext_circuit, const D: usize>( + builder: &mut CircuitBuilder, + filter: ExtensionTarget, + ch_a: &MemoryChannelView>, + ch_b: &MemoryChannelView>, + yield_constr: &mut RecursiveConstraintConsumer, +) { + for (limb_a, limb_b) in izip!(ch_a.value, ch_b.value) { + let diff = builder.sub_extension(limb_a, limb_b); + let constr = builder.mul_extension(filter, diff); + yield_constr.constraint(builder, constr); + } +} + +/// Set `used`, `is_read`, and address for channel. +/// +/// `offset` is the stack index before this instruction is executed, e.g. `0` for the top of the +/// stack. +fn constrain_channel_packed( + is_read: bool, + filter: P, + offset: P, + channel: &MemoryChannelView

, + lv: &CpuColumnsView

, + yield_constr: &mut ConstraintConsumer

, +) { + yield_constr.constraint(filter * (channel.used - P::ONES)); + yield_constr.constraint(filter * (channel.is_read - P::Scalar::from_bool(is_read))); + yield_constr.constraint(filter * (channel.addr_context - lv.context)); + yield_constr.constraint( + filter * (channel.addr_segment - P::Scalar::from_canonical_u64(Segment::Stack as u64)), + ); + // Top of the stack is at `addr = lv.stack_len - 1`. + let addr_virtual = lv.stack_len - P::ONES - offset; + yield_constr.constraint(filter * (channel.addr_virtual - addr_virtual)); +} + +/// Set `used`, `is_read`, and address for channel. +/// +/// `offset` is the stack index before this instruction is executed, e.g. `0` for the top of the +/// stack. +fn constrain_channel_ext_circuit, const D: usize>( + builder: &mut CircuitBuilder, + is_read: bool, + filter: ExtensionTarget, + offset: ExtensionTarget, + channel: &MemoryChannelView>, + lv: &CpuColumnsView>, + yield_constr: &mut RecursiveConstraintConsumer, +) { + { + let constr = builder.mul_sub_extension(filter, channel.used, filter); + yield_constr.constraint(builder, constr); + } + { + let constr = if is_read { + builder.mul_sub_extension(filter, channel.is_read, filter) + } else { + builder.mul_extension(filter, channel.is_read) + }; + yield_constr.constraint(builder, constr); + } + { + let diff = builder.sub_extension(channel.addr_context, lv.context); + let constr = builder.mul_extension(filter, diff); + yield_constr.constraint(builder, constr); + } + { + let constr = builder.arithmetic_extension( + F::ONE, + -F::from_canonical_u64(Segment::Stack as u64), + filter, + channel.addr_segment, + filter, + ); + yield_constr.constraint(builder, constr); + } + { + let constr = builder.add_extension(channel.addr_virtual, offset); + let constr = builder.sub_extension(constr, lv.stack_len); + let constr = builder.mul_add_extension(filter, constr, filter); + yield_constr.constraint(builder, constr); + } +} + +fn eval_packed_dup( + n: P, + lv: &CpuColumnsView

, + yield_constr: &mut ConstraintConsumer

, +) { + let filter = lv.is_cpu_cycle * lv.op.dup; + + let in_channel = &lv.mem_channels[0]; + let out_channel = &lv.mem_channels[NUM_GP_CHANNELS - 1]; + + channels_equal_packed(filter, in_channel, out_channel, yield_constr); + + constrain_channel_packed(true, filter, n, in_channel, lv, yield_constr); + constrain_channel_packed( + false, + filter, + P::Scalar::NEG_ONE.into(), + out_channel, + lv, + yield_constr, + ); +} + +fn eval_ext_circuit_dup, const D: usize>( + builder: &mut CircuitBuilder, + n: ExtensionTarget, + lv: &CpuColumnsView>, + yield_constr: &mut RecursiveConstraintConsumer, +) { + let neg_one = builder.constant_extension(F::NEG_ONE.into()); + + let filter = builder.mul_extension(lv.is_cpu_cycle, lv.op.dup); + + let in_channel = &lv.mem_channels[0]; + let out_channel = &lv.mem_channels[NUM_GP_CHANNELS - 1]; + + channels_equal_ext_circuit(builder, filter, in_channel, out_channel, yield_constr); + + constrain_channel_ext_circuit(builder, true, filter, n, in_channel, lv, yield_constr); + constrain_channel_ext_circuit( + builder, + false, + filter, + neg_one, + out_channel, + lv, + yield_constr, + ); +} + +fn eval_packed_swap( + n: P, + lv: &CpuColumnsView

, + yield_constr: &mut ConstraintConsumer

, +) { + let n_plus_one = n + P::ONES; + + let filter = lv.is_cpu_cycle * lv.op.swap; + + let in1_channel = &lv.mem_channels[0]; + let in2_channel = &lv.mem_channels[1]; + let out1_channel = &lv.mem_channels[NUM_GP_CHANNELS - 2]; + let out2_channel = &lv.mem_channels[NUM_GP_CHANNELS - 1]; + + channels_equal_packed(filter, in1_channel, out1_channel, yield_constr); + channels_equal_packed(filter, in2_channel, out2_channel, yield_constr); + + constrain_channel_packed(true, filter, P::ZEROS, in1_channel, lv, yield_constr); + constrain_channel_packed(true, filter, n_plus_one, in2_channel, lv, yield_constr); + constrain_channel_packed(false, filter, n_plus_one, out1_channel, lv, yield_constr); + constrain_channel_packed(false, filter, P::ZEROS, out2_channel, lv, yield_constr); +} + +fn eval_ext_circuit_swap, const D: usize>( + builder: &mut CircuitBuilder, + n: ExtensionTarget, + lv: &CpuColumnsView>, + yield_constr: &mut RecursiveConstraintConsumer, +) { + let zero = builder.zero_extension(); + let one = builder.one_extension(); + let n_plus_one = builder.add_extension(n, one); + + let filter = builder.mul_extension(lv.is_cpu_cycle, lv.op.swap); + + let in1_channel = &lv.mem_channels[0]; + let in2_channel = &lv.mem_channels[1]; + let out1_channel = &lv.mem_channels[NUM_GP_CHANNELS - 2]; + let out2_channel = &lv.mem_channels[NUM_GP_CHANNELS - 1]; + + channels_equal_ext_circuit(builder, filter, in1_channel, out1_channel, yield_constr); + channels_equal_ext_circuit(builder, filter, in2_channel, out2_channel, yield_constr); + + constrain_channel_ext_circuit(builder, true, filter, zero, in1_channel, lv, yield_constr); + constrain_channel_ext_circuit( + builder, + true, + filter, + n_plus_one, + in2_channel, + lv, + yield_constr, + ); + constrain_channel_ext_circuit( + builder, + false, + filter, + n_plus_one, + out1_channel, + lv, + yield_constr, + ); + constrain_channel_ext_circuit(builder, false, filter, zero, out2_channel, lv, yield_constr); +} + +pub fn eval_packed( + lv: &CpuColumnsView

, + yield_constr: &mut ConstraintConsumer

, +) { + 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) + + lv.opcode_bits[3] * P::Scalar::from_canonical_u64(8); + + eval_packed_dup(n, lv, yield_constr); + eval_packed_swap(n, lv, yield_constr); +} + +pub fn eval_ext_circuit, const D: usize>( + builder: &mut CircuitBuilder, + lv: &CpuColumnsView>, + yield_constr: &mut RecursiveConstraintConsumer, +) { + let n = lv.opcode_bits[..4].iter().enumerate().fold( + builder.zero_extension(), + |cumul, (i, &bit)| { + builder.mul_const_add_extension(F::from_canonical_u64(1 << i), bit, cumul) + }, + ); + + eval_ext_circuit_dup(builder, n, lv, yield_constr); + eval_ext_circuit_swap(builder, n, lv, yield_constr); +} diff --git a/evm/src/cpu/mod.rs b/evm/src/cpu/mod.rs index c5b7dd32..bde06585 100644 --- a/evm/src/cpu/mod.rs +++ b/evm/src/cpu/mod.rs @@ -3,6 +3,7 @@ pub(crate) mod columns; mod control_flow; pub mod cpu_stark; pub(crate) mod decode; +mod dup_swap; mod jumps; pub mod kernel; pub(crate) mod membus; diff --git a/evm/src/cpu/stack.rs b/evm/src/cpu/stack.rs index 3186b5ae..9bc08091 100644 --- a/evm/src/cpu/stack.rs +++ b/evm/src/cpu/stack.rs @@ -34,6 +34,11 @@ const BASIC_TERNARY_OP: Option = Some(StackBehavior { disable_other_channels: true, }); +// AUDITORS: If the value below is `None`, then the operation must be manually checked to ensure +// that every general-purpose memory channel is either disabled or has its read flag and address +// propertly constrained. The same applies when `disable_other_channels` is set to `false`, +// except the first `num_pops` and the last `pushes as usize` channels have their read flag and +// address constrained automatically in this file. const STACK_BEHAVIORS: OpsColumnsView> = OpsColumnsView { stop: None, // TODO add: BASIC_BINARY_OP, @@ -106,29 +111,29 @@ const STACK_BEHAVIORS: OpsColumnsView> = OpsColumnsView { get_receipt_root: None, // TODO set_receipt_root: None, // TODO push: None, // TODO - dup: None, // TODO - swap: None, // TODO - log0: None, // TODO - log1: None, // TODO - log2: None, // TODO - log3: None, // TODO - log4: None, // TODO - create: None, // TODO - call: None, // TODO - callcode: None, // TODO - return_: None, // TODO - delegatecall: None, // TODO - create2: None, // TODO - get_context: None, // TODO - set_context: None, // TODO - consume_gas: None, // TODO - exit_kernel: None, // TODO - staticcall: None, // TODO - mload_general: None, // TODO - mstore_general: None, // TODO - revert: None, // TODO - selfdestruct: None, // TODO - invalid: None, // TODO + dup: None, + swap: None, + log0: None, // TODO + log1: None, // TODO + log2: None, // TODO + log3: None, // TODO + log4: None, // TODO + create: None, // TODO + call: None, // TODO + callcode: None, // TODO + return_: None, // TODO + delegatecall: None, // TODO + create2: None, // TODO + get_context: None, // TODO + set_context: None, // TODO + consume_gas: None, // TODO + exit_kernel: None, // TODO + staticcall: None, // TODO + mload_general: None, // TODO + mstore_general: None, // TODO + revert: None, // TODO + selfdestruct: None, // TODO + invalid: None, // TODO }; fn eval_packed_one(