mirror of
https://github.com/logos-storage/plonky2.git
synced 2026-01-07 16:23:12 +00:00
Memory load/store constraints (#839)
This commit is contained in:
parent
b5a06f92fa
commit
95eeed46f0
@ -11,8 +11,8 @@ use plonky2::hash::hash_types::RichField;
|
|||||||
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
|
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
|
||||||
use crate::cpu::columns::{CpuColumnsView, COL_MAP, NUM_CPU_COLUMNS};
|
use crate::cpu::columns::{CpuColumnsView, COL_MAP, NUM_CPU_COLUMNS};
|
||||||
use crate::cpu::{
|
use crate::cpu::{
|
||||||
bootstrap_kernel, control_flow, decode, dup_swap, jumps, membus, modfp254, shift, simple_logic,
|
bootstrap_kernel, control_flow, decode, dup_swap, jumps, membus, memio, modfp254, shift,
|
||||||
stack, stack_bounds, syscalls,
|
simple_logic, stack, stack_bounds, syscalls,
|
||||||
};
|
};
|
||||||
use crate::cross_table_lookup::Column;
|
use crate::cross_table_lookup::Column;
|
||||||
use crate::memory::segments::Segment;
|
use crate::memory::segments::Segment;
|
||||||
@ -146,6 +146,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
|
|||||||
dup_swap::eval_packed(local_values, yield_constr);
|
dup_swap::eval_packed(local_values, yield_constr);
|
||||||
jumps::eval_packed(local_values, next_values, &mut dummy_yield_constr);
|
jumps::eval_packed(local_values, next_values, &mut dummy_yield_constr);
|
||||||
membus::eval_packed(local_values, yield_constr);
|
membus::eval_packed(local_values, yield_constr);
|
||||||
|
memio::eval_packed(local_values, yield_constr);
|
||||||
modfp254::eval_packed(local_values, yield_constr);
|
modfp254::eval_packed(local_values, yield_constr);
|
||||||
shift::eval_packed(local_values, yield_constr);
|
shift::eval_packed(local_values, yield_constr);
|
||||||
simple_logic::eval_packed(local_values, yield_constr);
|
simple_logic::eval_packed(local_values, yield_constr);
|
||||||
@ -172,6 +173,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
|
|||||||
dup_swap::eval_ext_circuit(builder, local_values, yield_constr);
|
dup_swap::eval_ext_circuit(builder, local_values, yield_constr);
|
||||||
jumps::eval_ext_circuit(builder, local_values, next_values, &mut dummy_yield_constr);
|
jumps::eval_ext_circuit(builder, local_values, next_values, &mut dummy_yield_constr);
|
||||||
membus::eval_ext_circuit(builder, local_values, yield_constr);
|
membus::eval_ext_circuit(builder, local_values, yield_constr);
|
||||||
|
memio::eval_ext_circuit(builder, local_values, yield_constr);
|
||||||
modfp254::eval_ext_circuit(builder, local_values, yield_constr);
|
modfp254::eval_ext_circuit(builder, local_values, yield_constr);
|
||||||
shift::eval_ext_circuit(builder, local_values, yield_constr);
|
shift::eval_ext_circuit(builder, local_values, yield_constr);
|
||||||
simple_logic::eval_ext_circuit(builder, local_values, yield_constr);
|
simple_logic::eval_ext_circuit(builder, local_values, yield_constr);
|
||||||
|
|||||||
171
evm/src/cpu/memio.rs
Normal file
171
evm/src/cpu/memio.rs
Normal file
@ -0,0 +1,171 @@
|
|||||||
|
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 crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
|
||||||
|
use crate::cpu::columns::CpuColumnsView;
|
||||||
|
use crate::cpu::membus::NUM_GP_CHANNELS;
|
||||||
|
|
||||||
|
fn get_addr<T: Copy>(lv: &CpuColumnsView<T>) -> (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<P: PackedField>(
|
||||||
|
lv: &CpuColumnsView<P>,
|
||||||
|
yield_constr: &mut ConstraintConsumer<P>,
|
||||||
|
) {
|
||||||
|
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<F: RichField + Extendable<D>, const D: usize>(
|
||||||
|
builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder<F, D>,
|
||||||
|
lv: &CpuColumnsView<ExtensionTarget<D>>,
|
||||||
|
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
|
||||||
|
) {
|
||||||
|
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<P: PackedField>(
|
||||||
|
lv: &CpuColumnsView<P>,
|
||||||
|
yield_constr: &mut ConstraintConsumer<P>,
|
||||||
|
) {
|
||||||
|
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<F: RichField + Extendable<D>, const D: usize>(
|
||||||
|
builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder<F, D>,
|
||||||
|
lv: &CpuColumnsView<ExtensionTarget<D>>,
|
||||||
|
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
|
||||||
|
) {
|
||||||
|
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<P: PackedField>(
|
||||||
|
lv: &CpuColumnsView<P>,
|
||||||
|
yield_constr: &mut ConstraintConsumer<P>,
|
||||||
|
) {
|
||||||
|
eval_packed_load(lv, yield_constr);
|
||||||
|
eval_packed_store(lv, yield_constr);
|
||||||
|
}
|
||||||
|
|
||||||
|
pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
|
||||||
|
builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder<F, D>,
|
||||||
|
lv: &CpuColumnsView<ExtensionTarget<D>>,
|
||||||
|
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
|
||||||
|
) {
|
||||||
|
eval_ext_circuit_load(builder, lv, yield_constr);
|
||||||
|
eval_ext_circuit_store(builder, lv, yield_constr);
|
||||||
|
}
|
||||||
@ -7,6 +7,7 @@ mod dup_swap;
|
|||||||
mod jumps;
|
mod jumps;
|
||||||
pub mod kernel;
|
pub mod kernel;
|
||||||
pub(crate) mod membus;
|
pub(crate) mod membus;
|
||||||
|
mod memio;
|
||||||
mod modfp254;
|
mod modfp254;
|
||||||
mod shift;
|
mod shift;
|
||||||
pub(crate) mod simple_logic;
|
pub(crate) mod simple_logic;
|
||||||
|
|||||||
@ -76,8 +76,16 @@ const STACK_BEHAVIORS: OpsColumnsView<Option<StackBehavior>> = OpsColumnsView {
|
|||||||
set_context: None, // TODO
|
set_context: None, // TODO
|
||||||
consume_gas: None, // TODO
|
consume_gas: None, // TODO
|
||||||
exit_kernel: None, // TODO
|
exit_kernel: None, // TODO
|
||||||
mload_general: None, // TODO
|
mload_general: Some(StackBehavior {
|
||||||
mstore_general: None, // TODO
|
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 {
|
syscall: Some(StackBehavior {
|
||||||
num_pops: 0,
|
num_pops: 0,
|
||||||
pushes: true,
|
pushes: true,
|
||||||
|
|||||||
@ -125,11 +125,12 @@ fn simulate_cpu<F: RichField + Extendable<D>, const D: usize>(state: &mut Genera
|
|||||||
log::info!("CPU halted after {} cycles", state.traces.clock());
|
log::info!("CPU halted after {} cycles", state.traces.clock());
|
||||||
}
|
}
|
||||||
already_in_halt_loop |= in_halt_loop;
|
already_in_halt_loop |= in_halt_loop;
|
||||||
|
|
||||||
|
transition(state);
|
||||||
|
|
||||||
if already_in_halt_loop && state.traces.clock().is_power_of_two() {
|
if already_in_halt_loop && state.traces.clock().is_power_of_two() {
|
||||||
log::info!("CPU trace padded to {} cycles", state.traces.clock());
|
log::info!("CPU trace padded to {} cycles", state.traces.clock());
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
|
||||||
transition(state);
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|||||||
@ -518,14 +518,19 @@ pub(crate) fn generate_mload_general<F: Field>(
|
|||||||
let [(context, log_in0), (segment, log_in1), (virt, log_in2)] =
|
let [(context, log_in0), (segment, log_in1), (virt, log_in2)] =
|
||||||
stack_pop_with_log_and_fill::<3, _>(state, &mut row)?;
|
stack_pop_with_log_and_fill::<3, _>(state, &mut row)?;
|
||||||
|
|
||||||
let val = state
|
let (val, log_read) = mem_read_gp_with_log_and_fill(
|
||||||
.memory
|
3,
|
||||||
.get(MemoryAddress::new_u256s(context, segment, virt));
|
MemoryAddress::new_u256s(context, segment, virt),
|
||||||
|
state,
|
||||||
|
&mut row,
|
||||||
|
);
|
||||||
|
|
||||||
let log_out = stack_push_log_and_fill(state, &mut row, val)?;
|
let log_out = stack_push_log_and_fill(state, &mut row, val)?;
|
||||||
|
|
||||||
state.traces.push_memory(log_in0);
|
state.traces.push_memory(log_in0);
|
||||||
state.traces.push_memory(log_in1);
|
state.traces.push_memory(log_in1);
|
||||||
state.traces.push_memory(log_in2);
|
state.traces.push_memory(log_in2);
|
||||||
|
state.traces.push_memory(log_read);
|
||||||
state.traces.push_memory(log_out);
|
state.traces.push_memory(log_out);
|
||||||
state.traces.push_cpu(row);
|
state.traces.push_cpu(row);
|
||||||
Ok(())
|
Ok(())
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user