Merge NOT and POP flags. (#1257)

* Merge NOT and POP flags

* Add comments

* Disable remaining memory channels for POP

* Apply comments

* Fix stack
This commit is contained in:
Linda Guiga 2023-10-30 14:05:54 -04:00 committed by GitHub
parent 4b40bc0313
commit af4935cde8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 220 additions and 29 deletions

View File

@ -12,11 +12,10 @@ pub struct OpsColumnsView<T: Copy> {
pub fp254_op: T, // Combines ADD_FP254, MUL_FP254 and SUB_FP254 flags.
pub eq_iszero: T, // Combines EQ and ISZERO flags.
pub logic_op: T, // Combines AND, OR and XOR flags.
pub not: T,
pub shift: T, // Combines SHL and SHR flags.
pub not_pop: T, // Combines NOT and POP flags.
pub shift: T, // Combines SHL and SHR flags.
pub keccak_general: T,
pub prover_input: T,
pub pop: T,
pub jumps: T, // Combines JUMP and JUMPI flags.
pub pc: T,
pub jumpdest: T,

View File

@ -8,17 +8,16 @@ use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer
use crate::cpu::columns::{CpuColumnsView, COL_MAP};
use crate::cpu::kernel::aggregator::KERNEL;
const NATIVE_INSTRUCTIONS: [usize; 16] = [
const NATIVE_INSTRUCTIONS: [usize; 15] = [
COL_MAP.op.binary_op,
COL_MAP.op.ternary_op,
COL_MAP.op.fp254_op,
COL_MAP.op.eq_iszero,
COL_MAP.op.logic_op,
COL_MAP.op.not,
COL_MAP.op.not_pop,
COL_MAP.op.shift,
COL_MAP.op.keccak_general,
COL_MAP.op.prover_input,
COL_MAP.op.pop,
// not JUMPS (possible need to jump)
COL_MAP.op.pc,
COL_MAP.op.jumpdest,

View File

@ -23,18 +23,17 @@ use crate::cpu::columns::{CpuColumnsView, COL_MAP};
/// behavior.
/// Note: invalid opcodes are not represented here. _Any_ opcode is permitted to decode to
/// `is_invalid`. The kernel then verifies that the opcode was _actually_ invalid.
const OPCODES: [(u8, usize, bool, usize); 15] = [
const OPCODES: [(u8, usize, bool, usize); 13] = [
// (start index of block, number of top bits to check (log2), kernel-only, flag column)
// ADD, MUL, SUB, DIV, MOD, LT, GT and BYTE flags are handled partly manually here, and partly through the Arithmetic table CTL.
// ADDMOD, MULMOD and SUBMOD flags are handled partly manually here, and partly through the Arithmetic table CTL.
// FP254 operation flags are handled partly manually here, and partly through the Arithmetic table CTL.
(0x14, 1, false, COL_MAP.op.eq_iszero),
// AND, OR and XOR flags are handled partly manually here, and partly through the Logic table CTL.
(0x19, 0, false, COL_MAP.op.not),
// NOT and POP are handled manually here.
// SHL and SHR flags are handled partly manually here, and partly through the Logic table CTL.
(0x21, 0, true, COL_MAP.op.keccak_general),
(0x49, 0, true, COL_MAP.op.prover_input),
(0x50, 0, false, COL_MAP.op.pop),
(0x56, 1, false, COL_MAP.op.jumps), // 0x56-0x57
(0x58, 0, false, COL_MAP.op.pc),
(0x5b, 0, false, COL_MAP.op.jumpdest),
@ -51,13 +50,14 @@ const OPCODES: [(u8, usize, bool, usize); 15] = [
/// List of combined opcodes requiring a special handling.
/// Each index in the list corresponds to an arbitrary combination
/// of opcodes defined in evm/src/cpu/columns/ops.rs.
const COMBINED_OPCODES: [usize; 6] = [
const COMBINED_OPCODES: [usize; 7] = [
COL_MAP.op.logic_op,
COL_MAP.op.fp254_op,
COL_MAP.op.binary_op,
COL_MAP.op.ternary_op,
COL_MAP.op.shift,
COL_MAP.op.m_op_general,
COL_MAP.op.not_pop,
];
/// Break up an opcode (which is 8 bits long) into its eight bits.
@ -146,6 +146,14 @@ pub fn eval_packed_generic<P: PackedField>(
* (opcode - P::Scalar::from_canonical_usize(0xfc_usize))
* lv.op.m_op_general;
yield_constr.constraint(m_op_constr);
// Manually check lv.op.not_pop.
// Both NOT and POP can be called outside of the kernel mode:
// there is no need to constrain them in that regard.
let not_pop_op = (opcode - P::Scalar::from_canonical_usize(0x19_usize))
* (opcode - P::Scalar::from_canonical_usize(0x50_usize))
* lv.op.not_pop;
yield_constr.constraint(not_pop_op);
}
pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
@ -248,4 +256,17 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
m_op_constr = builder.mul_extension(m_op_constr, lv.op.m_op_general);
yield_constr.constraint(builder, m_op_constr);
// Manually check lv.op.not_pop.
// Both NOT and POP can be called outside of the kernel mode:
// there is no need to constrain them in that regard.
let not_opcode = builder.constant_extension(F::Extension::from_canonical_usize(0x19_usize));
let pop_opcode = builder.constant_extension(F::Extension::from_canonical_usize(0x50_usize));
let not_constr = builder.sub_extension(opcode, not_opcode);
let pop_constr = builder.sub_extension(opcode, pop_opcode);
let mut not_pop_constr = builder.mul_extension(not_constr, pop_constr);
not_pop_constr = builder.mul_extension(lv.op.not_pop, not_pop_constr);
yield_constr.constraint(builder, not_pop_constr);
}

View File

@ -24,11 +24,10 @@ const SIMPLE_OPCODES: OpsColumnsView<Option<u32>> = OpsColumnsView {
fp254_op: KERNEL_ONLY_INSTR,
eq_iszero: G_VERYLOW,
logic_op: G_VERYLOW,
not: G_VERYLOW,
not_pop: None, // This is handled manually below
shift: G_VERYLOW,
keccak_general: KERNEL_ONLY_INSTR,
prover_input: KERNEL_ONLY_INSTR,
pop: G_BASE,
jumps: None, // Combined flag handled separately.
pc: G_BASE,
jumpdest: G_JUMPDEST,
@ -104,6 +103,13 @@ fn eval_packed_accumulate<P: PackedField>(
let ternary_op_cost = P::Scalar::from_canonical_u32(G_MID.unwrap())
- lv.opcode_bits[1] * P::Scalar::from_canonical_u32(G_MID.unwrap());
yield_constr.constraint_transition(lv.op.ternary_op * (gas_diff - ternary_op_cost));
// For NOT and POP.
// NOT is differentiated from POP by its first bit set to 1.
let not_pop_cost = (P::ONES - lv.opcode_bits[0])
* P::Scalar::from_canonical_u32(G_BASE.unwrap())
+ lv.opcode_bits[0] * P::Scalar::from_canonical_u32(G_VERYLOW.unwrap());
yield_constr.constraint_transition(lv.op.not_pop * (gas_diff - not_pop_cost));
}
fn eval_packed_init<P: PackedField>(
@ -232,6 +238,20 @@ fn eval_ext_circuit_accumulate<F: RichField + Extendable<D>, const D: usize>(
let gas_diff = builder.sub_extension(nv_lv_diff, ternary_op_cost);
let constr = builder.mul_extension(filter, gas_diff);
yield_constr.constraint_transition(builder, constr);
// For NOT and POP.
// NOT is differentiated from POP by its first bit set to 1.
let filter = lv.op.not_pop;
let one = builder.one_extension();
let mut not_pop_cost =
builder.mul_const_extension(F::from_canonical_u32(G_VERYLOW.unwrap()), lv.opcode_bits[0]);
let mut pop_cost = builder.sub_extension(one, lv.opcode_bits[0]);
pop_cost = builder.mul_const_extension(F::from_canonical_u32(G_BASE.unwrap()), pop_cost);
not_pop_cost = builder.add_extension(not_pop_cost, pop_cost);
let not_pop_gas_diff = builder.sub_extension(nv_lv_diff, not_pop_cost);
let not_pop_constr = builder.mul_extension(filter, not_pop_gas_diff);
yield_constr.constraint_transition(builder, not_pop_constr);
}
fn eval_ext_circuit_init<F: RichField + Extendable<D>, const D: usize>(

View File

@ -6,6 +6,7 @@ use plonky2::iop::ext_target::ExtensionTarget;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cpu::columns::CpuColumnsView;
use crate::cpu::stack;
const LIMB_SIZE: usize = 32;
const ALL_1_LIMB: u64 = (1 << LIMB_SIZE) - 1;
@ -18,12 +19,15 @@ pub fn eval_packed<P: PackedField>(
// This is simple: just do output = 0xffffffff - input.
let input = lv.mem_channels[0].value;
let output = nv.mem_channels[0].value;
let filter = lv.op.not;
let filter = lv.op.not_pop * lv.opcode_bits[0];
for (input_limb, output_limb) in input.into_iter().zip(output) {
yield_constr.constraint(
filter * (output_limb + input_limb - P::Scalar::from_canonical_u64(ALL_1_LIMB)),
);
}
// Stack constraints.
stack::eval_packed_one(lv, nv, filter, stack::BASIC_UNARY_OP.unwrap(), yield_constr);
}
pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
@ -34,7 +38,7 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
) {
let input = lv.mem_channels[0].value;
let output = nv.mem_channels[0].value;
let filter = lv.op.not;
let filter = builder.mul_extension(lv.op.not_pop, lv.opcode_bits[0]);
for (input_limb, output_limb) in input.into_iter().zip(output) {
let constr = builder.add_extension(output_limb, input_limb);
let constr = builder.arithmetic_extension(
@ -46,4 +50,14 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
);
yield_constr.constraint(builder, constr);
}
// Stack constraints.
stack::eval_ext_circuit_one(
builder,
lv,
nv,
filter,
stack::BASIC_UNARY_OP.unwrap(),
yield_constr,
);
}

View File

@ -20,6 +20,11 @@ pub(crate) struct StackBehavior {
disable_other_channels: bool,
}
pub(crate) const BASIC_UNARY_OP: Option<StackBehavior> = Some(StackBehavior {
num_pops: 1,
pushes: true,
disable_other_channels: true,
});
const BASIC_BINARY_OP: Option<StackBehavior> = Some(StackBehavior {
num_pops: 2,
pushes: true,
@ -30,6 +35,7 @@ const BASIC_TERNARY_OP: Option<StackBehavior> = Some(StackBehavior {
pushes: true,
disable_other_channels: true,
});
pub(crate) const JUMP_OP: Option<StackBehavior> = Some(StackBehavior {
num_pops: 1,
pushes: false,
@ -58,11 +64,7 @@ pub(crate) const STACK_BEHAVIORS: OpsColumnsView<Option<StackBehavior>> = OpsCol
fp254_op: BASIC_BINARY_OP,
eq_iszero: None, // EQ is binary, IS_ZERO is unary.
logic_op: BASIC_BINARY_OP,
not: Some(StackBehavior {
num_pops: 1,
pushes: true,
disable_other_channels: true,
}),
not_pop: None,
shift: Some(StackBehavior {
num_pops: 2,
pushes: true,
@ -74,12 +76,7 @@ pub(crate) const STACK_BEHAVIORS: OpsColumnsView<Option<StackBehavior>> = OpsCol
disable_other_channels: true,
}),
prover_input: None, // TODO
pop: Some(StackBehavior {
num_pops: 1,
pushes: false,
disable_other_channels: true,
}),
jumps: None, // Depends on whether it's a JUMP or a JUMPI.
jumps: None, // Depends on whether it's a JUMP or a JUMPI.
pc: Some(StackBehavior {
num_pops: 0,
pushes: true,
@ -256,6 +253,50 @@ pub fn eval_packed<P: PackedField>(
eval_packed_one(lv, nv, op, stack_behavior, yield_constr);
}
}
// Stack constraints for POP.
// The only constraints POP has are stack constraints.
// Since POP and NOT are combined into one flag and they have
// different stack behaviors, POP needs special stack constraints.
// Constrain `stack_inv_aux`.
let len_diff = lv.stack_len - P::Scalar::ONES;
yield_constr.constraint(
lv.op.not_pop
* (len_diff * lv.general.stack().stack_inv - lv.general.stack().stack_inv_aux),
);
// If stack_len != 1 and POP, read new top of the stack in nv.mem_channels[0].
let top_read_channel = nv.mem_channels[0];
let is_top_read = lv.general.stack().stack_inv_aux * (P::ONES - lv.opcode_bits[0]);
// Constrain `stack_inv_aux_2`. It contains `stack_inv_aux * (1 - opcode_bits[0])`.
yield_constr.constraint(lv.op.not_pop * (lv.general.stack().stack_inv_aux_2 - is_top_read));
let new_filter = lv.op.not_pop * lv.general.stack().stack_inv_aux_2;
yield_constr.constraint_transition(new_filter * (top_read_channel.used - P::ONES));
yield_constr.constraint_transition(new_filter * (top_read_channel.is_read - P::ONES));
yield_constr.constraint_transition(new_filter * (top_read_channel.addr_context - nv.context));
yield_constr.constraint_transition(
new_filter
* (top_read_channel.addr_segment
- P::Scalar::from_canonical_u64(Segment::Stack as u64)),
);
let addr_virtual = nv.stack_len - P::ONES;
yield_constr.constraint_transition(new_filter * (top_read_channel.addr_virtual - addr_virtual));
// If stack_len == 1 or NOT, disable the channel.
// If NOT or (len==1 and POP), then `stack_inv_aux_2` = 0.
yield_constr.constraint(
lv.op.not_pop * (lv.general.stack().stack_inv_aux_2 - P::ONES) * top_read_channel.used,
);
// Disable remaining memory channels.
for &channel in &lv.mem_channels[1..] {
yield_constr.constraint(lv.op.not_pop * (lv.opcode_bits[0] - P::ONES) * channel.used);
}
// Constrain the new stack length for POP.
yield_constr.constraint_transition(
lv.op.not_pop * (lv.opcode_bits[0] - P::ONES) * (nv.stack_len - lv.stack_len + P::ONES),
);
}
pub(crate) fn eval_ext_circuit_one<F: RichField + Extendable<D>, const D: usize>(
@ -473,4 +514,81 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
eval_ext_circuit_one(builder, lv, nv, op, stack_behavior, yield_constr);
}
}
// Stack constraints for POP.
// The only constraints POP has are stack constraints.
// Since POP and NOT are combined into one flag and they have
// different stack behaviors, POP needs special stack constraints.
// Constrain `stack_inv_aux`.
{
let len_diff = builder.add_const_extension(lv.stack_len, F::NEG_ONE);
let diff = builder.mul_sub_extension(
len_diff,
lv.general.stack().stack_inv,
lv.general.stack().stack_inv_aux,
);
let constr = builder.mul_extension(lv.op.not_pop, diff);
yield_constr.constraint(builder, constr);
}
// If stack_len != 4 and MSTORE, read new top of the stack in nv.mem_channels[0].
let top_read_channel = nv.mem_channels[0];
let is_top_read = builder.mul_extension(lv.general.stack().stack_inv_aux, lv.opcode_bits[0]);
let is_top_read = builder.sub_extension(lv.general.stack().stack_inv_aux, is_top_read);
// Constrain `stack_inv_aux_2`. It contains `stack_inv_aux * opcode_bits[0]`.
{
let diff = builder.sub_extension(lv.general.stack().stack_inv_aux_2, is_top_read);
let constr = builder.mul_extension(lv.op.not_pop, diff);
yield_constr.constraint(builder, constr);
}
let new_filter = builder.mul_extension(lv.op.not_pop, lv.general.stack().stack_inv_aux_2);
{
let constr = builder.mul_sub_extension(new_filter, top_read_channel.used, new_filter);
yield_constr.constraint_transition(builder, constr);
}
{
let constr = builder.mul_sub_extension(new_filter, top_read_channel.is_read, new_filter);
yield_constr.constraint_transition(builder, constr);
}
{
let diff = builder.sub_extension(top_read_channel.addr_context, nv.context);
let constr = builder.mul_extension(new_filter, diff);
yield_constr.constraint_transition(builder, constr);
}
{
let diff = builder.add_const_extension(
top_read_channel.addr_segment,
-F::from_canonical_u64(Segment::Stack as u64),
);
let constr = builder.mul_extension(new_filter, diff);
yield_constr.constraint_transition(builder, constr);
}
{
let addr_virtual = builder.add_const_extension(nv.stack_len, -F::ONE);
let diff = builder.sub_extension(top_read_channel.addr_virtual, addr_virtual);
let constr = builder.mul_extension(new_filter, diff);
yield_constr.constraint_transition(builder, constr);
}
// If stack_len == 1 or NOT, disable the channel.
{
let diff = builder.mul_sub_extension(
lv.op.not_pop,
lv.general.stack().stack_inv_aux_2,
lv.op.not_pop,
);
let constr = builder.mul_extension(diff, top_read_channel.used);
yield_constr.constraint(builder, constr);
}
// Disable remaining memory channels.
let filter = builder.mul_sub_extension(lv.op.not_pop, lv.opcode_bits[0], lv.op.not_pop);
for &channel in &lv.mem_channels[1..] {
let constr = builder.mul_extension(filter, channel.used);
yield_constr.constraint(builder, constr);
}
// Constrain the new stack length for POP.
let diff = builder.sub_extension(nv.stack_len, lv.stack_len);
let mut constr = builder.add_const_extension(diff, F::ONES);
constr = builder.mul_extension(filter, constr);
yield_constr.constraint_transition(builder, constr);
}

View File

@ -170,6 +170,17 @@ pub(crate) fn generate_pop<F: Field>(
) -> Result<(), ProgramError> {
let [(_, _)] = stack_pop_with_log_and_fill::<1, _>(state, &mut row)?;
let diff = row.stack_len - F::from_canonical_usize(1);
if let Some(inv) = diff.try_inverse() {
row.general.stack_mut().stack_inv = inv;
row.general.stack_mut().stack_inv_aux = F::ONE;
row.general.stack_mut().stack_inv_aux_2 = F::ONE;
state.registers.is_stack_top_read = true;
} else {
row.general.stack_mut().stack_inv = F::ZERO;
row.general.stack_mut().stack_inv_aux = F::ZERO;
}
state.traces.push_cpu(row);
Ok(())
@ -538,6 +549,17 @@ pub(crate) fn generate_not<F: Field>(
let result = !x;
push_no_write(state, result);
// This is necessary for the stack constraints for POP,
// since the two flags are combined.
let diff = row.stack_len - F::from_canonical_usize(1);
if let Some(inv) = diff.try_inverse() {
row.general.stack_mut().stack_inv = inv;
row.general.stack_mut().stack_inv_aux = F::ONE;
} else {
row.general.stack_mut().stack_inv = F::ZERO;
row.general.stack_mut().stack_inv_aux = F::ZERO;
}
state.traces.push_cpu(row);
Ok(())
}

View File

@ -164,7 +164,7 @@ fn fill_op_flag<F: Field>(op: Operation, row: &mut CpuColumnsView<F>) {
Operation::Push(1..) => &mut flags.push,
Operation::Dup(_) | Operation::Swap(_) => &mut flags.dup_swap,
Operation::Iszero | Operation::Eq => &mut flags.eq_iszero,
Operation::Not => &mut flags.not,
Operation::Not | Operation::Pop => &mut flags.not_pop,
Operation::Syscall(_, _, _) => &mut flags.syscall,
Operation::BinaryLogic(_) => &mut flags.logic_op,
Operation::BinaryArithmetic(arithmetic::BinaryOperator::AddFp254)
@ -176,7 +176,6 @@ fn fill_op_flag<F: Field>(op: Operation, row: &mut CpuColumnsView<F>) {
Operation::TernaryArithmetic(_) => &mut flags.ternary_op,
Operation::KeccakGeneral => &mut flags.keccak_general,
Operation::ProverInput => &mut flags.prover_input,
Operation::Pop => &mut flags.pop,
Operation::Jump | Operation::Jumpi => &mut flags.jumps,
Operation::Pc => &mut flags.pc,
Operation::Jumpdest => &mut flags.jumpdest,
@ -195,7 +194,7 @@ fn get_op_special_length(op: Operation) -> Option<usize> {
Operation::Push(1..) => STACK_BEHAVIORS.push,
Operation::Dup(_) | Operation::Swap(_) => STACK_BEHAVIORS.dup_swap,
Operation::Iszero => IS_ZERO_STACK_BEHAVIOR,
Operation::Not => STACK_BEHAVIORS.not,
Operation::Not | Operation::Pop => STACK_BEHAVIORS.not_pop,
Operation::Syscall(_, _, _) => STACK_BEHAVIORS.syscall,
Operation::Eq => EQ_STACK_BEHAVIOR,
Operation::BinaryLogic(_) => STACK_BEHAVIORS.logic_op,
@ -210,7 +209,6 @@ fn get_op_special_length(op: Operation) -> Option<usize> {
Operation::TernaryArithmetic(_) => STACK_BEHAVIORS.ternary_op,
Operation::KeccakGeneral => STACK_BEHAVIORS.keccak_general,
Operation::ProverInput => STACK_BEHAVIORS.prover_input,
Operation::Pop => STACK_BEHAVIORS.pop,
Operation::Jump => JUMP_OP,
Operation::Jumpi => JUMPI_OP,
Operation::Pc => STACK_BEHAVIORS.pc,