Remove new_stack_top_channel from StackBehavior (#1296)

This commit is contained in:
Linda Guiga 2023-10-26 17:52:54 -04:00 committed by GitHub
parent 3aeec83a05
commit 666a155d4a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 33 additions and 115 deletions

View File

@ -1,6 +1,7 @@
//! The initial phase of execution, where the kernel code is hashed while being written to memory.
//! The hash is then checked against a precomputed kernel hash.
use ethereum_types::U256;
use itertools::Itertools;
use plonky2::field::extension::Extendable;
use plonky2::field::packed::PackedField;
@ -52,6 +53,13 @@ pub(crate) fn generate_bootstrap_kernel<F: Field>(state: &mut GenerationState<F>
MemoryAddress::new(0, Segment::Code, 0),
KERNEL.code.clone(),
);
state.registers.stack_top = KERNEL
.code_hash
.iter()
.enumerate()
.fold(0.into(), |acc, (i, &elt)| {
acc + (U256::from(elt) << (224 - 32 * i))
});
state.traces.push_cpu(final_cpu_row);
log::info!("Bootstrapping took {} cycles", state.traces.clock());
}

View File

@ -14,7 +14,6 @@ use super::halt;
use crate::all_stark::Table;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cpu::columns::{COL_MAP, NUM_CPU_COLUMNS};
use crate::cpu::membus::NUM_GP_CHANNELS;
use crate::cpu::{
bootstrap_kernel, contextops, control_flow, decode, dup_swap, gas, jumps, membus, memio,
modfp254, pc, push0, shift, simple_logic, stack, stack_bounds, syscalls_exceptions,
@ -41,7 +40,7 @@ pub fn ctl_data_keccak_sponge<F: Field>() -> Vec<Column<F>> {
let timestamp = Column::linear_combination([(COL_MAP.clock, num_channels)]);
let mut cols = vec![context, segment, virt, len, timestamp];
cols.extend(COL_MAP.mem_channels[4].value.map(Column::single));
cols.extend(Column::singles_next_row(COL_MAP.mem_channels[0].value));
cols
}
@ -54,9 +53,7 @@ pub fn ctl_filter_keccak_sponge<F: Field>() -> Column<F> {
fn ctl_data_binops<F: Field>() -> Vec<Column<F>> {
let mut res = Column::singles(COL_MAP.mem_channels[0].value).collect_vec();
res.extend(Column::singles(COL_MAP.mem_channels[1].value));
res.extend(Column::singles(
COL_MAP.mem_channels[NUM_GP_CHANNELS - 1].value,
));
res.extend(Column::singles_next_row(COL_MAP.mem_channels[0].value));
res
}
@ -68,9 +65,7 @@ fn ctl_data_ternops<F: Field>() -> Vec<Column<F>> {
let mut res = Column::singles(COL_MAP.mem_channels[0].value).collect_vec();
res.extend(Column::singles(COL_MAP.mem_channels[1].value));
res.extend(Column::singles(COL_MAP.mem_channels[2].value));
res.extend(Column::singles(
COL_MAP.mem_channels[NUM_GP_CHANNELS - 1].value,
));
res.extend(Column::singles_next_row(COL_MAP.mem_channels[0].value));
res
}

View File

@ -27,13 +27,6 @@ pub fn generate_pinv_diff<F: Field>(val0: U256, val1: U256, lv: &mut CpuColumnsV
let num_unequal_limbs = izip!(val0_limbs, val1_limbs)
.map(|(limb0, limb1)| (limb0 != limb1) as usize)
.sum();
let equal = num_unequal_limbs == 0;
let output = &mut lv.mem_channels[2].value;
output[0] = F::from_bool(equal);
for limb in &mut output[1..] {
*limb = F::ZERO;
}
// Form `diff_pinv`.
// Let `diff = val0 - val1`. Consider `x[i] = diff[i]^-1` if `diff[i] != 0` and 0 otherwise.
@ -57,7 +50,7 @@ pub fn eval_packed<P: PackedField>(
let logic = lv.general.logic();
let input0 = lv.mem_channels[0].value;
let input1 = lv.mem_channels[1].value;
let output = lv.mem_channels[2].value;
let output = nv.mem_channels[0].value;
// EQ (0x14) and ISZERO (0x15) are differentiated by their first opcode bit.
let eq_filter = lv.op.eq_iszero * (P::ONES - lv.opcode_bits[0]);
@ -117,7 +110,7 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
let logic = lv.general.logic();
let input0 = lv.mem_channels[0].value;
let input1 = lv.mem_channels[1].value;
let output = lv.mem_channels[2].value;
let output = nv.mem_channels[0].value;
// EQ (0x14) and ISZERO (0x15) are differentiated by their first opcode bit.
let eq_filter = builder.mul_extension(lv.op.eq_iszero, lv.opcode_bits[0]);

View File

@ -14,7 +14,7 @@ pub fn eval_packed<P: PackedField>(
nv: &CpuColumnsView<P>,
yield_constr: &mut ConstraintConsumer<P>,
) {
not::eval_packed(lv, yield_constr);
not::eval_packed(lv, nv, yield_constr);
eq_iszero::eval_packed(lv, nv, yield_constr);
}
@ -24,6 +24,6 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
nv: &CpuColumnsView<ExtensionTarget<D>>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
not::eval_ext_circuit(builder, lv, yield_constr);
not::eval_ext_circuit(builder, lv, nv, yield_constr);
eq_iszero::eval_ext_circuit(builder, lv, nv, yield_constr);
}

View File

@ -6,18 +6,18 @@ use plonky2::iop::ext_target::ExtensionTarget;
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cpu::columns::CpuColumnsView;
use crate::cpu::membus::NUM_GP_CHANNELS;
const LIMB_SIZE: usize = 32;
const ALL_1_LIMB: u64 = (1 << LIMB_SIZE) - 1;
pub fn eval_packed<P: PackedField>(
lv: &CpuColumnsView<P>,
nv: &CpuColumnsView<P>,
yield_constr: &mut ConstraintConsumer<P>,
) {
// This is simple: just do output = 0xffffffff - input.
let input = lv.mem_channels[0].value;
let output = lv.mem_channels[NUM_GP_CHANNELS - 1].value;
let output = nv.mem_channels[0].value;
let filter = lv.op.not;
for (input_limb, output_limb) in input.into_iter().zip(output) {
yield_constr.constraint(
@ -29,10 +29,11 @@ pub fn eval_packed<P: PackedField>(
pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder<F, D>,
lv: &CpuColumnsView<ExtensionTarget<D>>,
nv: &CpuColumnsView<ExtensionTarget<D>>,
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
let input = lv.mem_channels[0].value;
let output = lv.mem_channels[NUM_GP_CHANNELS - 1].value;
let output = nv.mem_channels[0].value;
let filter = lv.op.not;
for (input_limb, output_limb) in input.into_iter().zip(output) {
let constr = builder.add_extension(output_limb, input_limb);

View File

@ -17,39 +17,33 @@ use crate::memory::segments::Segment;
pub(crate) struct StackBehavior {
pub(crate) num_pops: usize,
pub(crate) pushes: bool,
new_top_stack_channel: Option<usize>,
disable_other_channels: bool,
}
const BASIC_BINARY_OP: Option<StackBehavior> = Some(StackBehavior {
num_pops: 2,
pushes: true,
new_top_stack_channel: Some(NUM_GP_CHANNELS - 1),
disable_other_channels: true,
});
const BASIC_TERNARY_OP: Option<StackBehavior> = Some(StackBehavior {
num_pops: 3,
pushes: true,
new_top_stack_channel: Some(NUM_GP_CHANNELS - 1),
disable_other_channels: true,
});
pub(crate) const JUMP_OP: Option<StackBehavior> = Some(StackBehavior {
num_pops: 1,
pushes: false,
new_top_stack_channel: None,
disable_other_channels: false,
});
pub(crate) const JUMPI_OP: Option<StackBehavior> = Some(StackBehavior {
num_pops: 2,
pushes: false,
new_top_stack_channel: None,
disable_other_channels: false,
});
pub(crate) const MLOAD_GENERAL_OP: Option<StackBehavior> = Some(StackBehavior {
num_pops: 3,
pushes: true,
new_top_stack_channel: None,
disable_other_channels: false,
});
@ -67,45 +61,38 @@ pub(crate) const STACK_BEHAVIORS: OpsColumnsView<Option<StackBehavior>> = OpsCol
not: Some(StackBehavior {
num_pops: 1,
pushes: true,
new_top_stack_channel: Some(NUM_GP_CHANNELS - 1),
disable_other_channels: true,
}),
shift: Some(StackBehavior {
num_pops: 2,
pushes: true,
new_top_stack_channel: Some(NUM_GP_CHANNELS - 1),
disable_other_channels: false,
}),
keccak_general: Some(StackBehavior {
num_pops: 4,
pushes: true,
new_top_stack_channel: Some(NUM_GP_CHANNELS - 1),
disable_other_channels: true,
}),
prover_input: None, // TODO
pop: Some(StackBehavior {
num_pops: 1,
pushes: false,
new_top_stack_channel: None,
disable_other_channels: true,
}),
jumps: None, // Depends on whether it's a JUMP or a JUMPI.
pc: Some(StackBehavior {
num_pops: 0,
pushes: true,
new_top_stack_channel: None,
disable_other_channels: true,
}),
jumpdest: Some(StackBehavior {
num_pops: 0,
pushes: false,
new_top_stack_channel: None,
disable_other_channels: true,
}),
push0: Some(StackBehavior {
num_pops: 0,
pushes: true,
new_top_stack_channel: None,
disable_other_channels: true,
}),
push: None, // TODO
@ -113,39 +100,33 @@ pub(crate) const STACK_BEHAVIORS: OpsColumnsView<Option<StackBehavior>> = OpsCol
get_context: Some(StackBehavior {
num_pops: 0,
pushes: true,
new_top_stack_channel: None,
disable_other_channels: true,
}),
set_context: None, // SET_CONTEXT is special since it involves the old and the new stack.
mload_32bytes: Some(StackBehavior {
num_pops: 4,
pushes: true,
new_top_stack_channel: Some(4),
disable_other_channels: false,
}),
mstore_32bytes: Some(StackBehavior {
num_pops: 5,
pushes: false,
new_top_stack_channel: None,
disable_other_channels: false,
}),
exit_kernel: Some(StackBehavior {
num_pops: 1,
pushes: false,
new_top_stack_channel: None,
disable_other_channels: true,
}),
m_op_general: None,
syscall: Some(StackBehavior {
num_pops: 0,
pushes: true,
new_top_stack_channel: None,
disable_other_channels: false,
}),
exception: Some(StackBehavior {
num_pops: 0,
pushes: true,
new_top_stack_channel: None,
disable_other_channels: false,
}),
};
@ -153,13 +134,11 @@ pub(crate) const STACK_BEHAVIORS: OpsColumnsView<Option<StackBehavior>> = OpsCol
pub(crate) const EQ_STACK_BEHAVIOR: Option<StackBehavior> = Some(StackBehavior {
num_pops: 2,
pushes: true,
new_top_stack_channel: Some(2),
disable_other_channels: true,
});
pub(crate) const IS_ZERO_STACK_BEHAVIOR: Option<StackBehavior> = Some(StackBehavior {
num_pops: 1,
pushes: true,
new_top_stack_channel: Some(2),
disable_other_channels: true,
});
@ -256,18 +235,6 @@ pub(crate) fn eval_packed_one<P: PackedField>(
}
}
// Maybe constrain next stack_top.
// These are transition constraints: they don't apply to the last row.
if let Some(next_top_ch) = stack_behavior.new_top_stack_channel {
for (limb_ch, limb_top) in lv.mem_channels[next_top_ch]
.value
.iter()
.zip(nv.mem_channels[0].value.iter())
{
yield_constr.constraint_transition(filter * (*limb_ch - *limb_top));
}
}
// Unused channels
if stack_behavior.disable_other_channels {
// The first channel contains (or not) the top od the stack and is constrained elsewhere.
@ -478,20 +445,6 @@ pub(crate) fn eval_ext_circuit_one<F: RichField + Extendable<D>, const D: usize>
}
}
// Maybe constrain next stack_top.
// These are transition constraints: they don't apply to the last row.
if let Some(next_top_ch) = stack_behavior.new_top_stack_channel {
for (limb_ch, limb_top) in lv.mem_channels[next_top_ch]
.value
.iter()
.zip(nv.mem_channels[0].value.iter())
{
let diff = builder.sub_extension(*limb_ch, *limb_top);
let constr = builder.mul_extension(filter, diff);
yield_constr.constraint_transition(builder, constr);
}
}
// Unused channels
if stack_behavior.disable_other_channels {
// The first channel contains (or not) the top od the stack and is constrained elsewhere.

View File

@ -63,7 +63,7 @@ pub(crate) fn generate_binary_logic_op<F: Field>(
let [(in0, _), (in1, log_in1)] = stack_pop_with_log_and_fill::<2, _>(state, &mut row)?;
let operation = logic::Operation::new(op, in0, in1);
push_no_write(state, &mut row, operation.result, Some(NUM_GP_CHANNELS - 1));
push_no_write(state, operation.result);
state.traces.push_logic(operation);
state.traces.push_memory(log_in1);
@ -92,12 +92,7 @@ pub(crate) fn generate_binary_arithmetic_op<F: Field>(
}
}
push_no_write(
state,
&mut row,
operation.result(),
Some(NUM_GP_CHANNELS - 1),
);
push_no_write(state, operation.result());
state.traces.push_arithmetic(operation);
state.traces.push_memory(log_in1);
@ -114,12 +109,7 @@ pub(crate) fn generate_ternary_arithmetic_op<F: Field>(
stack_pop_with_log_and_fill::<3, _>(state, &mut row)?;
let operation = arithmetic::Operation::ternary(operator, input0, input1, input2);
push_no_write(
state,
&mut row,
operation.result(),
Some(NUM_GP_CHANNELS - 1),
);
push_no_write(state, operation.result());
state.traces.push_arithmetic(operation);
state.traces.push_memory(log_in1);
@ -151,7 +141,7 @@ pub(crate) fn generate_keccak_general<F: Field>(
log::debug!("Hashing {:?}", input);
let hash = keccak(&input);
push_no_write(state, &mut row, hash.into_uint(), Some(NUM_GP_CHANNELS - 1));
push_no_write(state, hash.into_uint());
keccak_sponge_log(state, base_address, input);
@ -493,7 +483,7 @@ pub(crate) fn generate_dup<F: Field>(
} else {
mem_read_gp_with_log_and_fill(2, other_addr, state, &mut row)
};
push_no_write(state, &mut row, val, None);
push_no_write(state, val);
state.traces.push_memory(log_read);
state.traces.push_cpu(row);
@ -515,7 +505,7 @@ pub(crate) fn generate_swap<F: Field>(
let [(in0, _)] = stack_pop_with_log_and_fill::<1, _>(state, &mut row)?;
let (in1, log_in1) = mem_read_gp_with_log_and_fill(1, other_addr, state, &mut row);
let log_out0 = mem_write_gp_log_and_fill(2, other_addr, state, &mut row, in0);
push_no_write(state, &mut row, in1, None);
push_no_write(state, in1);
state.traces.push_memory(log_in1);
state.traces.push_memory(log_out0);
@ -529,7 +519,7 @@ pub(crate) fn generate_not<F: Field>(
) -> Result<(), ProgramError> {
let [(x, _)] = stack_pop_with_log_and_fill::<1, _>(state, &mut row)?;
let result = !x;
push_no_write(state, &mut row, result, Some(NUM_GP_CHANNELS - 1));
push_no_write(state, result);
state.traces.push_cpu(row);
Ok(())
@ -548,7 +538,7 @@ pub(crate) fn generate_iszero<F: Field>(
generate_pinv_diff(x, U256::zero(), &mut row);
push_no_write(state, &mut row, result, None);
push_no_write(state, result);
state.traces.push_cpu(row);
Ok(())
}
@ -587,7 +577,7 @@ fn append_shift<F: Field>(
let operation = arithmetic::Operation::binary(operator, input0, input1);
state.traces.push_arithmetic(operation);
push_no_write(state, &mut row, result, Some(NUM_GP_CHANNELS - 1));
push_no_write(state, result);
state.traces.push_memory(log_in1);
state.traces.push_cpu(row);
Ok(())
@ -701,7 +691,7 @@ pub(crate) fn generate_eq<F: Field>(
generate_pinv_diff(in0, in1, &mut row);
push_no_write(state, &mut row, result, None);
push_no_write(state, result);
state.traces.push_memory(log_in1);
state.traces.push_cpu(row);
Ok(())
@ -749,7 +739,7 @@ pub(crate) fn generate_mload_general<F: Field>(
state,
&mut row,
);
push_no_write(state, &mut row, val, None);
push_no_write(state, val);
let diff = row.stack_len - F::from_canonical_usize(4);
if let Some(inv) = diff.try_inverse() {
@ -797,7 +787,7 @@ pub(crate) fn generate_mload_32bytes<F: Field>(
.collect_vec();
let packed_int = U256::from_big_endian(&bytes);
push_no_write(state, &mut row, packed_int, Some(4));
push_no_write(state, packed_int);
byte_packing_log(state, base_address, bytes);

View File

@ -68,31 +68,9 @@ pub(crate) fn fill_channel_with_value<F: Field>(row: &mut CpuColumnsView<F>, n:
}
/// Pushes without writing in memory. This happens in opcodes where a push immediately follows a pop.
/// The pushed value may be loaded in a memory channel, without creating a memory operation.
pub(crate) fn push_no_write<F: Field>(
state: &mut GenerationState<F>,
row: &mut CpuColumnsView<F>,
val: U256,
channel_opt: Option<usize>,
) {
pub(crate) fn push_no_write<F: Field>(state: &mut GenerationState<F>, val: U256) {
state.registers.stack_top = val;
state.registers.stack_len += 1;
if let Some(channel) = channel_opt {
let val_limbs: [u64; 4] = val.0;
let channel = &mut row.mem_channels[channel];
assert_eq!(channel.used, F::ZERO);
channel.used = F::ZERO;
channel.is_read = F::ZERO;
channel.addr_context = F::from_canonical_usize(0);
channel.addr_segment = F::from_canonical_usize(0);
channel.addr_virtual = F::from_canonical_usize(0);
for (i, limb) in val_limbs.into_iter().enumerate() {
channel.value[2 * i] = F::from_canonical_u32(limb as u32);
channel.value[2 * i + 1] = F::from_canonical_u32((limb >> 32) as u32);
}
}
}
/// Pushes and (maybe) writes the previous stack top in memory. This happens in opcodes which only push.
@ -122,7 +100,7 @@ pub(crate) fn push_with_write<F: Field>(
);
Some(res)
};
push_no_write(state, row, val, None);
push_no_write(state, val);
if let Some(log) = write {
state.traces.push_memory(log);
}