Skip to content
This repository has been archived by the owner on Feb 21, 2024. It is now read-only.

Commit

Permalink
Remove full memory channel (0xPolygonZero#1450)
Browse files Browse the repository at this point in the history 
* Remove a full memory channel

* Remove unnecessary uses

* Revert PDF change

* Apply comments

* Apply more comments

* Move disabling functions to cpu_stark.rs

* Apply comments
  • Loading branch information
@hratoanina
hratoanina authored Jan 11, 2024
1 parent a78a29a commit f80ebe7
Show file tree
Hide file tree
Showing 11 changed files with 317 additions and 324 deletions.
Binary file modified evm/spec/zkevm.pdf
View file
Binary file not shown.
33 changes: 27 additions & 6 deletions evm/src/all_stark.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,11 @@ fn ctl_byte_packing<F: Field>() -> CrossTableLookup<F> {
cpu_stark::ctl_data_byte_packing_push(),
Some(cpu_stark::ctl_filter_byte_packing_push()),
);
let cpu_jumptable_read_looking = TableWithColumns::new(
Table::Cpu,
cpu_stark::ctl_data_jumptable_read(),
Some(cpu_stark::ctl_filter_syscall_exceptions()),
);
let byte_packing_looked = TableWithColumns::new(
Table::BytePacking,
byte_packing_stark::ctl_looked_data(),
Expand All @@ -145,6 +150,7 @@ fn ctl_byte_packing<F: Field>() -> CrossTableLookup<F> {
cpu_packing_looking,
cpu_unpacking_looking,
cpu_push_packing_looking,
cpu_jumptable_read_looking,
],
byte_packing_looked,
)
Expand Down Expand Up @@ -238,6 +244,16 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
cpu_stark::ctl_data_partial_memory::<F>(),
Some(cpu_stark::ctl_filter_partial_memory()),
);
let cpu_set_context_write = TableWithColumns::new(
Table::Cpu,
cpu_stark::ctl_data_memory_old_sp_write_set_context::<F>(),
Some(cpu_stark::ctl_filter_set_context()),
);
let cpu_set_context_read = TableWithColumns::new(
Table::Cpu,
cpu_stark::ctl_data_memory_new_sp_read_set_context::<F>(),
Some(cpu_stark::ctl_filter_set_context()),
);
let keccak_sponge_reads = (0..KECCAK_RATE_BYTES).map(|i| {
TableWithColumns::new(
Table::KeccakSponge,
Expand All @@ -252,12 +268,17 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
Some(byte_packing_stark::ctl_looking_memory_filter(i)),
)
});
let all_lookers = iter::once(cpu_memory_code_read)
.chain(cpu_memory_gp_ops)
.chain(iter::once(cpu_push_write_ops))
.chain(keccak_sponge_reads)
.chain(byte_packing_ops)
.collect();
let all_lookers = vec![
cpu_memory_code_read,
cpu_push_write_ops,
cpu_set_context_write,
cpu_set_context_read,
]
.into_iter()
.chain(cpu_memory_gp_ops)
.chain(keccak_sponge_reads)
.chain(byte_packing_ops)
.collect();
let memory_looked = TableWithColumns::new(
Table::Memory,
memory_stark::ctl_data(),
Expand Down
145 changes: 20 additions & 125 deletions evm/src/cpu/contextops.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,12 @@ use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;

use super::columns::ops::OpsColumnsView;
use super::cpu_stark::{disable_unused_channels, disable_unused_channels_circuit};
use super::membus::NUM_GP_CHANNELS;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cpu::columns::CpuColumnsView;
use crate::cpu::kernel::constants::context_metadata::ContextMetadata;
use crate::memory::segments::{Segment, SEGMENT_SCALING_FACTOR};
use crate::memory::segments::Segment;
use crate::memory::VALUE_LIMBS;

// If true, the instruction will keep the current context for the next row.
Expand Down Expand Up @@ -95,12 +96,7 @@ fn eval_packed_get<P: PackedField>(
yield_constr.constraint(filter * (nv.stack_len - (lv.stack_len + P::ONES)));

// Unused channels.
for i in 1..NUM_GP_CHANNELS {
if i != 3 {
let channel = lv.mem_channels[i];
yield_constr.constraint(filter * channel.used);
}
}
disable_unused_channels(lv, filter, vec![1], yield_constr);
yield_constr.constraint(filter * nv.mem_channels[0].used);
}

Expand Down Expand Up @@ -137,13 +133,7 @@ fn eval_ext_circuit_get<F: RichField + Extendable<D>, const D: usize>(
}

// Unused channels.
for i in 1..NUM_GP_CHANNELS {
if i != 3 {
let channel = lv.mem_channels[i];
let constr = builder.mul_extension(filter, channel.used);
yield_constr.constraint(builder, constr);
}
}
disable_unused_channels_circuit(builder, lv, filter, vec![1], yield_constr);
{
let constr = builder.mul_extension(filter, nv.mem_channels[0].used);
yield_constr.constraint(builder, constr);
Expand All @@ -158,40 +148,16 @@ fn eval_packed_set<P: PackedField>(
) {
let filter = lv.op.context_op * lv.opcode_bits[0];
let stack_top = lv.mem_channels[0].value;
let write_old_sp_channel = lv.mem_channels[1];
let read_new_sp_channel = lv.mem_channels[2];
// We need to unscale the context metadata segment and related field.
let ctx_metadata_segment = P::Scalar::from_canonical_usize(Segment::ContextMetadata.unscale());
let stack_size_field = P::Scalar::from_canonical_usize(ContextMetadata::StackSize.unscale());
let local_sp_dec = lv.stack_len - P::ONES;

// The next row's context is read from stack_top.
yield_constr.constraint(filter * (stack_top[2] - nv.context));
for (i, &limb) in stack_top.iter().enumerate().filter(|(i, _)| *i != 2) {
yield_constr.constraint(filter * limb);
}

// The old SP is decremented (since the new context was popped) and written to memory.
yield_constr.constraint(filter * (write_old_sp_channel.value[0] - local_sp_dec));
for &limb in &write_old_sp_channel.value[1..] {
yield_constr.constraint(filter * limb);
}
yield_constr.constraint(filter * (write_old_sp_channel.used - P::ONES));
yield_constr.constraint(filter * write_old_sp_channel.is_read);
yield_constr.constraint(filter * (write_old_sp_channel.addr_context - lv.context));
yield_constr.constraint(filter * (write_old_sp_channel.addr_segment - ctx_metadata_segment));
yield_constr.constraint(filter * (write_old_sp_channel.addr_virtual - stack_size_field));

// The old SP is decremented (since the new context was popped) and stored in memory.
// The new SP is loaded from memory.
yield_constr.constraint(filter * (read_new_sp_channel.value[0] - nv.stack_len));
for &limb in &read_new_sp_channel.value[1..] {
yield_constr.constraint(filter * limb);
}
yield_constr.constraint(filter * (read_new_sp_channel.used - P::ONES));
yield_constr.constraint(filter * (read_new_sp_channel.is_read - P::ONES));
yield_constr.constraint(filter * (read_new_sp_channel.addr_context - nv.context));
yield_constr.constraint(filter * (read_new_sp_channel.addr_segment - ctx_metadata_segment));
yield_constr.constraint(filter * (read_new_sp_channel.addr_virtual - stack_size_field));
// This is all done with CTLs: nothing is constrained here.

// Constrain stack_inv_aux_2.
let new_top_channel = nv.mem_channels[0];
Expand All @@ -200,17 +166,19 @@ fn eval_packed_set<P: PackedField>(
* (lv.general.stack().stack_inv_aux * lv.opcode_bits[0]
- lv.general.stack().stack_inv_aux_2),
);
// The new top is loaded in memory channel 3, if the stack isn't empty (see eval_packed).
// The new top is loaded in memory channel 2, if the stack isn't empty (see eval_packed).
for (&limb_new_top, &limb_read_top) in new_top_channel
.value
.iter()
.zip(lv.mem_channels[3].value.iter())
.zip(lv.mem_channels[2].value.iter())
{
yield_constr.constraint(
lv.op.context_op * lv.general.stack().stack_inv_aux_2 * (limb_new_top - limb_read_top),
);
}

// Unused channels.
disable_unused_channels(lv, filter, vec![1], yield_constr);
yield_constr.constraint(filter * new_top_channel.used);
}

Expand All @@ -224,17 +192,6 @@ fn eval_ext_circuit_set<F: RichField + Extendable<D>, const D: usize>(
) {
let filter = builder.mul_extension(lv.op.context_op, lv.opcode_bits[0]);
let stack_top = lv.mem_channels[0].value;
let write_old_sp_channel = lv.mem_channels[1];
let read_new_sp_channel = lv.mem_channels[2];
// We need to unscale the context metadata segment and related field.
let ctx_metadata_segment = builder.constant_extension(F::Extension::from_canonical_usize(
Segment::ContextMetadata.unscale(),
));
let stack_size_field = builder.constant_extension(F::Extension::from_canonical_usize(
ContextMetadata::StackSize.unscale(),
));
let one = builder.one_extension();
let local_sp_dec = builder.sub_extension(lv.stack_len, one);

// The next row's context is read from stack_top.
{
Expand All @@ -247,73 +204,9 @@ fn eval_ext_circuit_set<F: RichField + Extendable<D>, const D: usize>(
yield_constr.constraint(builder, constr);
}

// The old SP is decremented (since the new context was popped) and written to memory.
{
let diff = builder.sub_extension(write_old_sp_channel.value[0], local_sp_dec);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}
for &limb in &write_old_sp_channel.value[1..] {
let constr = builder.mul_extension(filter, limb);
yield_constr.constraint(builder, constr);
}
{
let constr = builder.mul_sub_extension(filter, write_old_sp_channel.used, filter);
yield_constr.constraint(builder, constr);
}
{
let constr = builder.mul_extension(filter, write_old_sp_channel.is_read);
yield_constr.constraint(builder, constr);
}
{
let diff = builder.sub_extension(write_old_sp_channel.addr_context, lv.context);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}
{
let diff = builder.sub_extension(write_old_sp_channel.addr_segment, ctx_metadata_segment);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}
{
let diff = builder.sub_extension(write_old_sp_channel.addr_virtual, stack_size_field);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}

// The old SP is decremented (since the new context was popped) and stored in memory.
// The new SP is loaded from memory.
{
let diff = builder.sub_extension(read_new_sp_channel.value[0], nv.stack_len);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}
for &limb in &read_new_sp_channel.value[1..] {
let constr = builder.mul_extension(filter, limb);
yield_constr.constraint(builder, constr);
}
{
let constr = builder.mul_sub_extension(filter, read_new_sp_channel.used, filter);
yield_constr.constraint(builder, constr);
}
{
let constr = builder.mul_sub_extension(filter, read_new_sp_channel.is_read, filter);
yield_constr.constraint(builder, constr);
}
{
let diff = builder.sub_extension(read_new_sp_channel.addr_context, nv.context);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}
{
let diff = builder.sub_extension(read_new_sp_channel.addr_segment, ctx_metadata_segment);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}
{
let diff = builder.sub_extension(read_new_sp_channel.addr_virtual, stack_size_field);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
}
// This is all done with CTLs: nothing is constrained here.

// Constrain stack_inv_aux_2.
let new_top_channel = nv.mem_channels[0];
Expand All @@ -326,18 +219,20 @@ fn eval_ext_circuit_set<F: RichField + Extendable<D>, const D: usize>(
let constr = builder.mul_extension(lv.op.context_op, diff);
yield_constr.constraint(builder, constr);
}
// The new top is loaded in memory channel 3, if the stack isn't empty (see eval_packed).
// The new top is loaded in memory channel 2, if the stack isn't empty (see eval_packed).
for (&limb_new_top, &limb_read_top) in new_top_channel
.value
.iter()
.zip(lv.mem_channels[3].value.iter())
.zip(lv.mem_channels[2].value.iter())
{
let diff = builder.sub_extension(limb_new_top, limb_read_top);
let prod = builder.mul_extension(lv.general.stack().stack_inv_aux_2, diff);
let constr = builder.mul_extension(lv.op.context_op, prod);
yield_constr.constraint(builder, constr);
}

// Unused channels.
disable_unused_channels_circuit(builder, lv, filter, vec![1], yield_constr);
{
let constr = builder.mul_extension(filter, new_top_channel.used);
yield_constr.constraint(builder, constr);
Expand All @@ -355,10 +250,10 @@ pub(crate) fn eval_packed<P: PackedField>(
eval_packed_set(lv, nv, yield_constr);

// Stack constraints.
// Both operations use memory channel 3. The operations are similar enough that
// Both operations use memory channel 2. The operations are similar enough that
// we can constrain both at the same time.
let filter = lv.op.context_op;
let channel = lv.mem_channels[3];
let channel = lv.mem_channels[2];
// For get_context, we check if lv.stack_len is 0. For set_context, we check if nv.stack_len is 0.
// However, for get_context, we can deduce lv.stack_len from nv.stack_len since the operation only pushes.
let stack_len = nv.stack_len - (P::ONES - lv.opcode_bits[0]);
Expand Down Expand Up @@ -396,10 +291,10 @@ pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
eval_ext_circuit_set(builder, lv, nv, yield_constr);

// Stack constraints.
// Both operations use memory channel 3. The operations are similar enough that
// Both operations use memory channel 2. The operations are similar enough that
// we can constrain both at the same time.
let filter = lv.op.context_op;
let channel = lv.mem_channels[3];
let channel = lv.mem_channels[2];
// For get_context, we check if lv.stack_len is 0. For set_context, we check if nv.stack_len is 0.
// However, for get_context, we can deduce lv.stack_len from nv.stack_len since the operation only pushes.
let diff = builder.add_const_extension(lv.opcode_bits[0], -F::ONE);
Expand Down
Loading

0 comments on commit f80ebe7

Please sign in to comment.