logos-storage/plonky2
1
0
Fork 0
mirror of https://github.com/logos-storage/plonky2.git synced 2026-01-07 00:03:10 +00:00
Code Issues Packages Projects Releases Wiki Activity

Add missing constraints for DUP/SWAP (#1310)

Browse Source
This commit is contained in:
Hamy Ratoanina 2023-10-26 09:59:02 -04:00 committed by GitHub
parent 44af80f244
commit 3aeec83a05
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 43 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

51
evm/src/cpu/dup_swap.rs
View File

@ -6,6 +6,7 @@ use plonky2::hash::hash_types::RichField;
use plonky2::iop::ext_target::ExtensionTarget;
use plonky2::plonk::circuit_builder::CircuitBuilder;
use super::membus::NUM_GP_CHANNELS;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cpu::columns::{CpuColumnsView, MemoryChannelView};
use crate::memory::segments::Segment;
@ -129,7 +130,13 @@ fn eval_packed_dup<P: PackedField>(
// Constrain nv.stack_len.
yield_constr.constraint_transition(filter * (nv.stack_len - lv.stack_len - P::ONES));
// TODO: Constrain unused channels?
// Disable next top.
yield_constr.constraint(filter * nv.mem_channels[0].used);
// Constrain unused channels.
for i in 3..NUM_GP_CHANNELS {
yield_constr.constraint(filter * lv.mem_channels[i].used);
}
}
fn eval_ext_circuit_dup<F: RichField + Extendable<D>, const D: usize>(
@ -175,11 +182,23 @@ fn eval_ext_circuit_dup<F: RichField + Extendable<D>, const D: usize>(
constrain_channel_ext_circuit(builder, true, filter, n, read_channel, lv, yield_constr);
// Constrain nv.stack_len.
let diff = builder.sub_extension(nv.stack_len, lv.stack_len);
let constr = builder.mul_sub_extension(filter, diff, filter);
yield_constr.constraint_transition(builder, constr);
{
let diff = builder.sub_extension(nv.stack_len, lv.stack_len);
let constr = builder.mul_sub_extension(filter, diff, filter);
yield_constr.constraint_transition(builder, constr);
}
// TODO: Constrain unused channels?
// Disable next top.
{
let constr = builder.mul_extension(filter, nv.mem_channels[0].used);
yield_constr.constraint(builder, constr);
}
// Constrain unused channels.
for i in 3..NUM_GP_CHANNELS {
let constr = builder.mul_extension(filter, lv.mem_channels[i].used);
yield_constr.constraint(builder, constr);
}
}
fn eval_packed_swap<P: PackedField>(
@ -203,10 +222,16 @@ fn eval_packed_swap<P: PackedField>(
channels_equal_packed(filter, in2_channel, &nv.mem_channels[0], yield_constr);
constrain_channel_packed(true, filter, n_plus_one, in2_channel, lv, yield_constr);
// Constrain nv.stack_len;
// Constrain nv.stack_len.
yield_constr.constraint(filter * (nv.stack_len - lv.stack_len));
// TODO: Constrain unused channels?
// Disable next top.
yield_constr.constraint(filter * nv.mem_channels[0].used);
// Constrain unused channels.
for i in 3..NUM_GP_CHANNELS {
yield_constr.constraint(filter * lv.mem_channels[i].used);
}
}
fn eval_ext_circuit_swap<F: RichField + Extendable<D>, const D: usize>(
@ -259,7 +284,17 @@ fn eval_ext_circuit_swap<F: RichField + Extendable<D>, const D: usize>(
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint(builder, constr);
// TODO: Constrain unused channels?
// Disable next top.
{
let constr = builder.mul_extension(filter, nv.mem_channels[0].used);
yield_constr.constraint(builder, constr);
}
// Constrain unused channels.
for i in 3..NUM_GP_CHANNELS {
let constr = builder.mul_extension(filter, lv.mem_channels[i].used);
yield_constr.constraint(builder, constr);
}
}
pub fn eval_packed<P: PackedField>(