diff --git a/evm/src/byte_packing/byte_packing_stark.rs b/evm/src/byte_packing/byte_packing_stark.rs index f97a2b28ab..aa6a2dcf88 100644 --- a/evm/src/byte_packing/byte_packing_stark.rs +++ b/evm/src/byte_packing/byte_packing_stark.rs @@ -47,7 +47,7 @@ use plonky2::util::transpose; use super::NUM_BYTES; use crate::byte_packing::columns::{ index_bytes, value_bytes, ADDR_CONTEXT, ADDR_SEGMENT, ADDR_VIRTUAL, BYTE_INDICES_COLS, IS_READ, - NUM_COLUMNS, RANGE_COUNTER, RC_COLS, SEQUENCE_END, SEQUENCE_LEN, TIMESTAMP, + NUM_COLUMNS, RANGE_COUNTER, RC_COLS, SEQUENCE_END, TIMESTAMP, }; use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer}; use crate::cross_table_lookup::Column; @@ -76,15 +76,16 @@ pub(crate) fn ctl_looked_data() -> Vec> { }) .collect(); - Column::singles([ - ADDR_CONTEXT, - ADDR_SEGMENT, - ADDR_VIRTUAL, - SEQUENCE_LEN, - TIMESTAMP, - ]) - .chain(outputs) - .collect() + // This will correspond to the actual sequence length when the `SEQUENCE_END` flag is on. + let sequence_len: Column = Column::linear_combination( + (0..NUM_BYTES).map(|i| (index_bytes(i), F::from_canonical_usize(i + 1))), + ); + + Column::singles([ADDR_CONTEXT, ADDR_SEGMENT, ADDR_VIRTUAL]) + .chain([sequence_len]) + .chain(Column::singles(&[TIMESTAMP])) + .chain(outputs) + .collect() } pub fn ctl_looked_filter() -> Column { @@ -202,7 +203,6 @@ impl, const D: usize> BytePackingStark { row[ADDR_VIRTUAL] = F::from_canonical_usize(virt + bytes.len() - 1); row[TIMESTAMP] = F::from_canonical_usize(timestamp); - row[SEQUENCE_LEN] = F::from_canonical_usize(bytes.len()); for (i, &byte) in bytes.iter().rev().enumerate() { if i == bytes.len() - 1 { @@ -354,27 +354,20 @@ impl, const D: usize> Stark for BytePackingSt current_sequence_end * next_filter * (next_sequence_start - one), ); - // The remaining length of a byte sequence must decrease by one or be zero. - let current_sequence_length = vars.local_values[SEQUENCE_LEN]; + // The active position in a byte sequence must increase by one on every row + // or be one on the next row (i.e. at the start of a new sequence). let current_position = self.get_active_position(vars.local_values); let next_position = self.get_active_position(vars.next_values); - let current_remaining_length = current_sequence_length - current_position; - let next_sequence_length = vars.next_values[SEQUENCE_LEN]; - let next_remaining_length = next_sequence_length - next_position; yield_constr.constraint_transition( - current_remaining_length * (current_remaining_length - next_remaining_length - one), - ); - - // At the start of a sequence, the remaining length must be equal to the starting length minus one - yield_constr.constraint( - current_sequence_start * (current_sequence_length - current_remaining_length - one), + next_filter * (next_position - one) * (next_position - current_position - one), ); - // The remaining length on the last row must be zero. - yield_constr.constraint_last_row(current_remaining_length); + // The last row must be the end of a sequence or a padding row. + yield_constr.constraint_last_row(current_filter * (current_sequence_end - one)); - // If the current remaining length is zero, the end flag must be one. - yield_constr.constraint(current_remaining_length * current_sequence_end); + // If the next position is one in an active row, the current end flag must be one. + yield_constr + .constraint_transition(next_filter * current_sequence_end * (next_position - one)); // The context, segment and timestamp fields must remain unchanged throughout a byte sequence. // The virtual address must decrement by one at each step of a sequence. @@ -489,36 +482,26 @@ impl, const D: usize> Stark for BytePackingSt let constraint = builder.mul_extension(next_filter, constraint); yield_constr.constraint_transition(builder, constraint); - // The remaining length of a byte sequence must decrease by one or be zero. - let current_sequence_length = vars.local_values[SEQUENCE_LEN]; - let next_sequence_length = vars.next_values[SEQUENCE_LEN]; + // The active position in a byte sequence must increase by one on every row + // or be one on the next row (i.e. at the start of a new sequence). let current_position = self.get_active_position_circuit(builder, vars.local_values); let next_position = self.get_active_position_circuit(builder, vars.next_values); - let current_remaining_length = - builder.sub_extension(current_sequence_length, current_position); - let next_remaining_length = builder.sub_extension(next_sequence_length, next_position); - let length_diff = builder.sub_extension(current_remaining_length, next_remaining_length); - let constraint = builder.mul_sub_extension( - current_remaining_length, - length_diff, - current_remaining_length, - ); + let position_diff = builder.sub_extension(next_position, current_position); + let is_new_or_inactive = builder.mul_sub_extension(next_filter, next_position, next_filter); + let constraint = + builder.mul_sub_extension(is_new_or_inactive, position_diff, is_new_or_inactive); yield_constr.constraint_transition(builder, constraint); - // At the start of a sequence, the remaining length must be equal to the starting length minus one - let current_sequence_length = vars.local_values[SEQUENCE_LEN]; - let length_diff = builder.sub_extension(current_sequence_length, current_remaining_length); + // The last row must be the end of a sequence or a padding row. let constraint = - builder.mul_sub_extension(current_sequence_start, length_diff, current_sequence_start); - yield_constr.constraint(builder, constraint); + builder.mul_sub_extension(current_filter, current_sequence_end, current_filter); + yield_constr.constraint_last_row(builder, constraint); - // The remaining length on the last row must be zero. - yield_constr.constraint_last_row(builder, current_remaining_length); - - // If the current remaining length is zero, the end flag must be one. - let constraint = builder.mul_extension(current_remaining_length, current_sequence_end); - yield_constr.constraint(builder, constraint); + // If the next position is one in an active row, the current end flag must be one. + let constraint = builder.mul_extension(next_filter, current_sequence_end); + let constraint = builder.mul_sub_extension(constraint, next_position, constraint); + yield_constr.constraint_transition(builder, constraint); // The context, segment and timestamp fields must remain unchanged throughout a byte sequence. // The virtual address must decrement by one at each step of a sequence. diff --git a/evm/src/byte_packing/columns.rs b/evm/src/byte_packing/columns.rs index f04f450c51..feb8f2e2c3 100644 --- a/evm/src/byte_packing/columns.rs +++ b/evm/src/byte_packing/columns.rs @@ -16,7 +16,8 @@ pub(crate) const fn index_bytes(i: usize) -> usize { BYTES_INDICES_START + i } -// Note: Those are used as filter for distinguishing active vs padding rows. +// Note: Those are used as filter for distinguishing active vs padding rows, +// and also to obtain the length of a sequence of bytes being processed. pub(crate) const BYTE_INDICES_COLS: Range = BYTES_INDICES_START..BYTES_INDICES_START + NUM_BYTES; @@ -25,12 +26,8 @@ pub(crate) const ADDR_SEGMENT: usize = ADDR_CONTEXT + 1; pub(crate) const ADDR_VIRTUAL: usize = ADDR_SEGMENT + 1; pub(crate) const TIMESTAMP: usize = ADDR_VIRTUAL + 1; -/// The total length of a sequence of bytes. -/// Cannot be greater than 32. -pub(crate) const SEQUENCE_LEN: usize = TIMESTAMP + 1; - // 32 byte limbs hold a total of 256 bits. -const BYTES_VALUES_START: usize = SEQUENCE_LEN + 1; +const BYTES_VALUES_START: usize = TIMESTAMP + 1; pub(crate) const fn value_bytes(i: usize) -> usize { debug_assert!(i < NUM_BYTES); BYTES_VALUES_START + i