mirror of
https://github.com/logos-storage/plonky2.git
synced 2026-01-03 14:23:07 +00:00
Constraints for dup/swap (#743)
* Constraints for dup/swap * Minor comments * Daniel comments * More comments
This commit is contained in:
Jacqueline Nabaglo
GitHub
parent
7d7afe711d
commit
d5cf53c227
@ -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<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
|
||||
bootstrap_kernel::eval_bootstrap_kernel(vars, yield_constr);
|
||||
control_flow::eval_packed_generic(local_values, next_values, yield_constr);
|
||||
decode::eval_packed_generic(local_values, yield_constr);
|
||||
dup_swap::eval_packed(local_values, yield_constr);
|
||||
jumps::eval_packed(local_values, next_values, yield_constr);
|
||||
membus::eval_packed(local_values, yield_constr);
|
||||
simple_logic::eval_packed(local_values, yield_constr);
|
||||
@ -166,6 +167,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
|
||||
bootstrap_kernel::eval_bootstrap_kernel_circuit(builder, vars, yield_constr);
|
||||
control_flow::eval_ext_circuit(builder, local_values, next_values, yield_constr);
|
||||
decode::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, yield_constr);
|
||||
membus::eval_ext_circuit(builder, local_values, yield_constr);
|
||||
simple_logic::eval_ext_circuit(builder, local_values, yield_constr);
|
||||
|
||||
254
evm/src/cpu/dup_swap.rs
Normal file
254
evm/src/cpu/dup_swap.rs
Normal file
@ -0,0 +1,254 @@
|
||||
use itertools::izip;
|
||||
use plonky2::field::extension::Extendable;
|
||||
use plonky2::field::packed::PackedField;
|
||||
use plonky2::field::types::Field;
|
||||
use plonky2::hash::hash_types::RichField;
|
||||
use plonky2::iop::ext_target::ExtensionTarget;
|
||||
use plonky2::plonk::circuit_builder::CircuitBuilder;
|
||||
|
||||
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
|
||||
use crate::cpu::columns::{CpuColumnsView, MemoryChannelView};
|
||||
use crate::cpu::membus::NUM_GP_CHANNELS;
|
||||
use crate::memory::segments::Segment;
|
||||
|
||||
/// Constrain two channels to have equal values.
|
||||
fn channels_equal_packed<P: PackedField>(
|
||||
filter: P,
|
||||
ch_a: &MemoryChannelView<P>,
|
||||
ch_b: &MemoryChannelView<P>,
|
||||
yield_constr: &mut ConstraintConsumer<P>,
|
||||
) {
|
||||
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<F: RichField + Extendable<D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
filter: ExtensionTarget<D>,
|
||||
ch_a: &MemoryChannelView<ExtensionTarget<D>>,
|
||||
ch_b: &MemoryChannelView<ExtensionTarget<D>>,
|
||||
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
|
||||
) {
|
||||
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<P: PackedField>(
|
||||
is_read: bool,
|
||||
filter: P,
|
||||
offset: P,
|
||||
channel: &MemoryChannelView<P>,
|
||||
lv: &CpuColumnsView<P>,
|
||||
yield_constr: &mut ConstraintConsumer<P>,
|
||||
) {
|
||||
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<F: RichField + Extendable<D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
is_read: bool,
|
||||
filter: ExtensionTarget<D>,
|
||||
offset: ExtensionTarget<D>,
|
||||
channel: &MemoryChannelView<ExtensionTarget<D>>,
|
||||
lv: &CpuColumnsView<ExtensionTarget<D>>,
|
||||
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
|
||||
) {
|
||||
{
|
||||
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<P: PackedField>(
|
||||
n: P,
|
||||
lv: &CpuColumnsView<P>,
|
||||
yield_constr: &mut ConstraintConsumer<P>,
|
||||
) {
|
||||
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<F: RichField + Extendable<D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
n: ExtensionTarget<D>,
|
||||
lv: &CpuColumnsView<ExtensionTarget<D>>,
|
||||
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
|
||||
) {
|
||||
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<P: PackedField>(
|
||||
n: P,
|
||||
lv: &CpuColumnsView<P>,
|
||||
yield_constr: &mut ConstraintConsumer<P>,
|
||||
) {
|
||||
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<F: RichField + Extendable<D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
n: ExtensionTarget<D>,
|
||||
lv: &CpuColumnsView<ExtensionTarget<D>>,
|
||||
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
|
||||
) {
|
||||
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<P: PackedField>(
|
||||
lv: &CpuColumnsView<P>,
|
||||
yield_constr: &mut ConstraintConsumer<P>,
|
||||
) {
|
||||
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<F: RichField + Extendable<D>, const D: usize>(
|
||||
builder: &mut CircuitBuilder<F, D>,
|
||||
lv: &CpuColumnsView<ExtensionTarget<D>>,
|
||||
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
|
||||
) {
|
||||
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);
|
||||
}
|
||||
@ -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;
|
||||
|
||||
@ -34,6 +34,11 @@ const BASIC_TERNARY_OP: Option<StackBehavior> = 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<Option<StackBehavior>> = OpsColumnsView {
|
||||
stop: None, // TODO
|
||||
add: BASIC_BINARY_OP,
|
||||
@ -106,29 +111,29 @@ const STACK_BEHAVIORS: OpsColumnsView<Option<StackBehavior>> = 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<P: PackedField>(
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user