From 95eeed46f02239f400b0272779f6e4dcb1a6bbc6 Mon Sep 17 00:00:00 2001 From: Jacqueline Nabaglo Date: Fri, 9 Dec 2022 10:35:00 -0800 Subject: [PATCH] Memory load/store constraints (#839) --- evm/src/cpu/cpu_stark.rs | 6 +- evm/src/cpu/memio.rs | 171 +++++++++++++++++++++++++++++++++++ evm/src/cpu/mod.rs | 1 + evm/src/cpu/stack.rs | 20 ++-- evm/src/generation/mod.rs | 5 +- evm/src/witness/operation.rs | 11 ++- 6 files changed, 201 insertions(+), 13 deletions(-) create mode 100644 evm/src/cpu/memio.rs diff --git a/evm/src/cpu/cpu_stark.rs b/evm/src/cpu/cpu_stark.rs index 7f5f4b3e..aa48bb37 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, dup_swap, jumps, membus, modfp254, shift, simple_logic, - stack, stack_bounds, syscalls, + bootstrap_kernel, control_flow, decode, dup_swap, jumps, membus, memio, modfp254, shift, + simple_logic, stack, stack_bounds, syscalls, }; use crate::cross_table_lookup::Column; use crate::memory::segments::Segment; @@ -146,6 +146,7 @@ impl, const D: usize> Stark for CpuStark, const D: usize> Stark for CpuStark(lv: &CpuColumnsView) -> (T, T, T) { + let addr_context = lv.mem_channels[0].value[0]; + let addr_segment = lv.mem_channels[1].value[0]; + let addr_virtual = lv.mem_channels[2].value[0]; + (addr_context, addr_segment, addr_virtual) +} + +fn eval_packed_load( + lv: &CpuColumnsView

, + yield_constr: &mut ConstraintConsumer

, +) { + let filter = lv.op.mload_general; + + let (addr_context, addr_segment, addr_virtual) = get_addr(lv); + + let load_channel = lv.mem_channels[3]; + let push_channel = lv.mem_channels[NUM_GP_CHANNELS - 1]; + yield_constr.constraint(filter * (load_channel.used - P::ONES)); + yield_constr.constraint(filter * (load_channel.is_read - P::ONES)); + yield_constr.constraint(filter * (load_channel.addr_context - addr_context)); + yield_constr.constraint(filter * (load_channel.addr_segment - addr_segment)); + yield_constr.constraint(filter * (load_channel.addr_virtual - addr_virtual)); + for (load_limb, push_limb) in izip!(load_channel.value, push_channel.value) { + yield_constr.constraint(filter * (load_limb - push_limb)); + } + + // Disable remaining memory channels, if any. + for &channel in &lv.mem_channels[4..NUM_GP_CHANNELS - 1] { + yield_constr.constraint(filter * channel.used); + } +} + +fn eval_ext_circuit_load, const D: usize>( + builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder, + lv: &CpuColumnsView>, + yield_constr: &mut RecursiveConstraintConsumer, +) { + let filter = lv.op.mload_general; + + let (addr_context, addr_segment, addr_virtual) = get_addr(lv); + + let load_channel = lv.mem_channels[3]; + let push_channel = lv.mem_channels[NUM_GP_CHANNELS - 1]; + { + let constr = builder.mul_sub_extension(filter, load_channel.used, filter); + yield_constr.constraint(builder, constr); + } + { + let constr = builder.mul_sub_extension(filter, load_channel.is_read, filter); + yield_constr.constraint(builder, constr); + } + for (channel_field, target) in izip!( + [ + load_channel.addr_context, + load_channel.addr_segment, + load_channel.addr_virtual, + ], + [addr_context, addr_segment, addr_virtual] + ) { + let diff = builder.sub_extension(channel_field, target); + let constr = builder.mul_extension(filter, diff); + yield_constr.constraint(builder, constr); + } + for (load_limb, push_limb) in izip!(load_channel.value, push_channel.value) { + let diff = builder.sub_extension(load_limb, push_limb); + let constr = builder.mul_extension(filter, diff); + yield_constr.constraint(builder, constr); + } + + // Disable remaining memory channels, if any. + for &channel in &lv.mem_channels[4..NUM_GP_CHANNELS - 1] { + let constr = builder.mul_extension(filter, channel.used); + yield_constr.constraint(builder, constr); + } +} + +fn eval_packed_store( + lv: &CpuColumnsView

, + yield_constr: &mut ConstraintConsumer

, +) { + let filter = lv.op.mstore_general; + + let (addr_context, addr_segment, addr_virtual) = get_addr(lv); + + let value_channel = lv.mem_channels[3]; + let store_channel = lv.mem_channels[4]; + yield_constr.constraint(filter * (store_channel.used - P::ONES)); + yield_constr.constraint(filter * store_channel.is_read); + yield_constr.constraint(filter * (store_channel.addr_context - addr_context)); + yield_constr.constraint(filter * (store_channel.addr_segment - addr_segment)); + yield_constr.constraint(filter * (store_channel.addr_virtual - addr_virtual)); + for (value_limb, store_limb) in izip!(value_channel.value, store_channel.value) { + yield_constr.constraint(filter * (value_limb - store_limb)); + } + + // Disable remaining memory channels, if any. + for &channel in &lv.mem_channels[5..] { + yield_constr.constraint(filter * channel.used); + } +} + +fn eval_ext_circuit_store, const D: usize>( + builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder, + lv: &CpuColumnsView>, + yield_constr: &mut RecursiveConstraintConsumer, +) { + let filter = lv.op.mstore_general; + + let (addr_context, addr_segment, addr_virtual) = get_addr(lv); + + let value_channel = lv.mem_channels[3]; + let store_channel = lv.mem_channels[4]; + { + let constr = builder.mul_sub_extension(filter, store_channel.used, filter); + yield_constr.constraint(builder, constr); + } + { + let constr = builder.mul_extension(filter, store_channel.is_read); + yield_constr.constraint(builder, constr); + } + for (channel_field, target) in izip!( + [ + store_channel.addr_context, + store_channel.addr_segment, + store_channel.addr_virtual, + ], + [addr_context, addr_segment, addr_virtual] + ) { + let diff = builder.sub_extension(channel_field, target); + let constr = builder.mul_extension(filter, diff); + yield_constr.constraint(builder, constr); + } + for (value_limb, store_limb) in izip!(value_channel.value, store_channel.value) { + let diff = builder.sub_extension(value_limb, store_limb); + let constr = builder.mul_extension(filter, diff); + yield_constr.constraint(builder, constr); + } + + // Disable remaining memory channels, if any. + for &channel in &lv.mem_channels[5..] { + let constr = builder.mul_extension(filter, channel.used); + yield_constr.constraint(builder, constr); + } +} + +pub fn eval_packed( + lv: &CpuColumnsView

, + yield_constr: &mut ConstraintConsumer

, +) { + eval_packed_load(lv, yield_constr); + eval_packed_store(lv, yield_constr); +} + +pub fn eval_ext_circuit, const D: usize>( + builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder, + lv: &CpuColumnsView>, + yield_constr: &mut RecursiveConstraintConsumer, +) { + eval_ext_circuit_load(builder, lv, yield_constr); + eval_ext_circuit_store(builder, lv, yield_constr); +} diff --git a/evm/src/cpu/mod.rs b/evm/src/cpu/mod.rs index 3a2df351..d4ff95c8 100644 --- a/evm/src/cpu/mod.rs +++ b/evm/src/cpu/mod.rs @@ -7,6 +7,7 @@ mod dup_swap; mod jumps; pub mod kernel; pub(crate) mod membus; +mod memio; mod modfp254; mod shift; pub(crate) mod simple_logic; diff --git a/evm/src/cpu/stack.rs b/evm/src/cpu/stack.rs index 08ab3044..3c358d24 100644 --- a/evm/src/cpu/stack.rs +++ b/evm/src/cpu/stack.rs @@ -72,12 +72,20 @@ const STACK_BEHAVIORS: OpsColumnsView> = OpsColumnsView { push: None, // TODO dup: None, swap: None, - get_context: None, // TODO - set_context: None, // TODO - consume_gas: None, // TODO - exit_kernel: None, // TODO - mload_general: None, // TODO - mstore_general: None, // TODO + get_context: None, // TODO + set_context: None, // TODO + consume_gas: None, // TODO + exit_kernel: None, // TODO + mload_general: Some(StackBehavior { + num_pops: 3, + pushes: true, + disable_other_channels: false, + }), + mstore_general: Some(StackBehavior { + num_pops: 4, + pushes: false, + disable_other_channels: false, + }), syscall: Some(StackBehavior { num_pops: 0, pushes: true, diff --git a/evm/src/generation/mod.rs b/evm/src/generation/mod.rs index 8b662a6d..858bb111 100644 --- a/evm/src/generation/mod.rs +++ b/evm/src/generation/mod.rs @@ -125,11 +125,12 @@ fn simulate_cpu, const D: usize>(state: &mut Genera log::info!("CPU halted after {} cycles", state.traces.clock()); } already_in_halt_loop |= in_halt_loop; + + transition(state); + if already_in_halt_loop && state.traces.clock().is_power_of_two() { log::info!("CPU trace padded to {} cycles", state.traces.clock()); break; } - - transition(state); } } diff --git a/evm/src/witness/operation.rs b/evm/src/witness/operation.rs index 8c04c071..d58ad186 100644 --- a/evm/src/witness/operation.rs +++ b/evm/src/witness/operation.rs @@ -518,14 +518,19 @@ pub(crate) fn generate_mload_general( let [(context, log_in0), (segment, log_in1), (virt, log_in2)] = stack_pop_with_log_and_fill::<3, _>(state, &mut row)?; - let val = state - .memory - .get(MemoryAddress::new_u256s(context, segment, virt)); + let (val, log_read) = mem_read_gp_with_log_and_fill( + 3, + MemoryAddress::new_u256s(context, segment, virt), + state, + &mut row, + ); + let log_out = stack_push_log_and_fill(state, &mut row, val)?; state.traces.push_memory(log_in0); state.traces.push_memory(log_in1); state.traces.push_memory(log_in2); + state.traces.push_memory(log_read); state.traces.push_memory(log_out); state.traces.push_cpu(row); Ok(())