Skip to content

Commit

Permalink
Bring back arith op
Browse files Browse the repository at this point in the history
  • Loading branch information
@Nashtare
Nashtare committed Oct 10, 2024
1 parent 8311359 commit e11b79e
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 140 deletions.
25 changes: 0 additions & 25 deletions evm_arithmetization/src/cpu/columns/general.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ pub(crate) union CpuGeneralColumnsView<T: Copy> {
shift: CpuShiftView<T>,
stack: CpuStackView<T>,
push: CpuPushView<T>,
incr: CpuIncrView<T>,
context_pruning: CpuContextPruningView<T>,
}

Expand Down Expand Up @@ -94,18 +93,6 @@ impl<T: Copy> CpuGeneralColumnsView<T> {
unsafe { &mut self.push }
}

/// View of the columns required for the incr operation.
/// SAFETY: Each view is a valid interpretation of the underlying array.
pub(crate) const fn incr(&self) -> &CpuIncrView<T> {
unsafe { &self.incr }
}

/// Mutable view of the columns required for the incr operation.
/// SAFETY: Each view is a valid interpretation of the underlying array.
pub(crate) fn incr_mut(&mut self) -> &mut CpuIncrView<T> {
unsafe { &mut self.incr }
}

/// View of the column for context pruning.
/// SAFETY: Each view is a valid interpretation of the underlying array.
pub(crate) const fn context_pruning(&self) -> &CpuContextPruningView<T> {
Expand Down Expand Up @@ -230,17 +217,6 @@ pub(crate) struct CpuPushView<T: Copy> {
_padding_columns: [T; NUM_SHARED_COLUMNS - 1],
}

/// View of all `CpuGeneralColumn`s, helping to detect any limb overflow
/// when incrementing by 1.
#[repr(C)]
#[derive(Copy, Clone)]
pub(crate) struct CpuIncrView<T: Copy> {
/// If limb `i` is 1, then we overflowed the first `i-1` limbs when adding
/// 1 (i.e. they are now 0). This means limb `1` is incremented by 1, and
/// higher limbs remain unchanged.
pub(crate) limbs: [T; NUM_SHARED_COLUMNS],
}

/// View of the first `CpuGeneralColumn` storing a flag for context pruning.
#[derive(Copy, Clone)]
pub(crate) struct CpuContextPruningView<T: Copy> {
Expand All @@ -267,5 +243,4 @@ const_assert!(size_of::<CpuJumpsView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuShiftView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuStackView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuPushView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuIncrView<u8>>() == NUM_SHARED_COLUMNS);
const_assert!(size_of::<CpuContextPruningView<u8>>() == NUM_SHARED_COLUMNS);
88 changes: 1 addition & 87 deletions evm_arithmetization/src/cpu/incr.rs
View file
Original file line number Diff line number Diff line change
@@ -1,79 +1,17 @@
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 plonky2::plonk::circuit_builder::CircuitBuilder;
use starky::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};

use crate::cpu::columns::{CpuColumnsView, MemoryChannelView};
use crate::memory::VALUE_LIMBS;

/// Constrain two channels such that their values `A` and `B` satisfy
/// `B = A + 1`, by using the `CpuIncrView` helper limbs.
fn channels_incremented_packed<P: PackedField>(
filter: P,
ch_a: &MemoryChannelView<P>,
ch_b: &MemoryChannelView<P>,
helper_limbs: [P; VALUE_LIMBS],
yield_constr: &mut ConstraintConsumer<P>,
) {
for (limb_a, limb_b, helper) in izip!(ch_a.value, ch_b.value, helper_limbs) {
// If there was an overflow on the current limb, `limb_b` will be 0, else
// we enforce proper increment.
yield_constr.constraint(filter * limb_b * (limb_b - limb_a - helper));
}
}

/// Constrain two channels such that their values `A` and `B` satisfy
/// `B = A + 1`, by using the `CpuIncrView` helper limbs.
fn channels_incremented_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>>,
helper_limbs: [ExtensionTarget<D>; VALUE_LIMBS],
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
for (limb_a, limb_b, helper) in izip!(ch_a.value, ch_b.value, helper_limbs) {
// If there was an overflow on the current limb, `limb_b` will be 0, else
// we enforce proper increment.
let diff = builder.sub_extension(limb_b, limb_a);
let diff = builder.sub_extension(diff, helper);
let constr = builder.mul_extension(limb_b, diff);
let constr = builder.mul_extension(filter, constr);
yield_constr.constraint(builder, constr);
}
}
use crate::cpu::columns::CpuColumnsView;

/// Evaluates the constraints for the DUP and SWAP opcodes.
pub(crate) fn eval_packed<P: PackedField>(
lv: &CpuColumnsView<P>,
yield_constr: &mut ConstraintConsumer<P>,
) {
// Constrain the helper columns.
{
// First limb is always 1.
yield_constr.constraint(lv.op.incr * (lv.general.incr().limbs[0] - P::ONES));

// 1s and 0s must be contiguous
for i in 1..VALUE_LIMBS - 1 {
yield_constr.constraint(
lv.op.incr
* (lv.general.incr().limbs[i] - P::ONES)
* lv.general.incr().limbs[i + 1],
);
}
}

channels_incremented_packed(
lv.op.incr,
&lv.mem_channels[1],
&lv.mem_channels[2],
lv.general.incr().limbs,
yield_constr,
);

// Disable the partial channel.
yield_constr.constraint(lv.op.incr * lv.partial_channel.used);
}
Expand All @@ -85,30 +23,6 @@ pub(crate) fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
lv: &CpuColumnsView<ExtensionTarget<D>>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
// Constrain the helper columns.
{
// First limb is always 1.
let constr = builder.mul_sub_extension(lv.op.incr, lv.general.incr().limbs[0], lv.op.incr);
yield_constr.constraint(builder, constr);

// 1s and 0s must be contiguous
for i in 1..VALUE_LIMBS - 1 {
let constr =
builder.mul_sub_extension(lv.op.incr, lv.general.incr().limbs[i], lv.op.incr);
let constr = builder.mul_extension(constr, lv.general.incr().limbs[i + 1]);
yield_constr.constraint(builder, constr);
}
}

channels_incremented_circuit(
builder,
lv.op.incr,
&lv.mem_channels[1],
&lv.mem_channels[2],
lv.general.incr().limbs,
yield_constr,
);

// Disable the partial channel.
{
let constr = builder.mul_extension(lv.op.incr, lv.partial_channel.used);
Expand Down
31 changes: 3 additions & 28 deletions evm_arithmetization/src/witness/operation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ use crate::cpu::simple_logic::eq_iszero::generate_pinv_diff;
use crate::cpu::stack::MAX_USER_STACK_SIZE;
use crate::extension_tower::BN_BASE;
use crate::memory::segments::Segment;
use crate::util::{u256_limbs, u256_to_usize};
use crate::util::u256_to_usize;
use crate::witness::errors::MemoryError::VirtTooLarge;
use crate::witness::errors::ProgramError;
use crate::witness::memory::{MemoryAddress, MemoryChannel, MemoryOp, MemoryOpKind};
Expand Down Expand Up @@ -648,33 +648,8 @@ pub(crate) fn generate_incr<F: RichField, T: Transition<F>>(
state.push_memory(log_out0);
state.push_memory(log_in0);

let in0_limbs = u256_limbs::<F>(in0);
let out0_limbs = u256_limbs::<F>(in0 + 1);
// This is necessary to properly constrain the increment over limbs without
// relying on the Arithmetic table.
for (i, limb) in row.general.incr_mut().limbs.iter_mut().enumerate() {
*limb = if in0_limbs[i] != out0_limbs[i] {
F::ONE
} else {
F::ZERO
}
}
// if n == 0 {
// println!(
// "TOP OF THE STACK: {:?}\n\t{:?}\n\t{:?}\n",
// row.general.incr().limbs,
// row.mem_channels[1],
// row.mem_channels[2],
// );
// } else {
// println!(
// "REGULAR CHANNEL: {:?}\n\t{:?}\n\t{:?}\n",
// row.general.incr().limbs,
// row.mem_channels[1],
// row.mem_channels[2]
// );
// }

let operation = arithmetic::Operation::binary(BinaryOperator::Add, in0, U256::one());
state.push_arithmetic(operation);
state.push_cpu(row);

Ok(())
Expand Down

0 comments on commit e11b79e

Please sign in to comment.