From 73356cf01d04c5a80cafd80eafd3efdfacb35227 Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Tue, 19 Sep 2023 10:53:07 -0400 Subject: [PATCH 1/3] Remove SEQUENCE_LEN in BytePackingStark --- evm/src/byte_packing/byte_packing_stark.rs | 79 ++++++++-------------- evm/src/byte_packing/columns.rs | 9 +-- 2 files changed, 30 insertions(+), 58 deletions(-) diff --git a/evm/src/byte_packing/byte_packing_stark.rs b/evm/src/byte_packing/byte_packing_stark.rs index f97a2b28ab..e299670592 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,17 @@ 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 current position in a byte sequence must increase by one on the next row + // or be one on the next row (i.e. a 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); - - // 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 +479,21 @@ 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 current position in a byte sequence must increase by one on the next row + // or be one on the next row (i.e. a 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, - ); - 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); + 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(current_sequence_start, length_diff, current_sequence_start); - yield_constr.constraint(builder, constraint); - - // The remaining length on the last row must be zero. - yield_constr.constraint_last_row(builder, current_remaining_length); + builder.mul_sub_extension(is_new_or_inactive, position_diff, is_new_or_inactive); + yield_constr.constraint_transition(builder, constraint); - // 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 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 From 8d53624c00349b056a1daa373e31d35bcc36fe22 Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Tue, 19 Sep 2023 11:05:47 -0400 Subject: [PATCH 2/3] Constrain last row --- evm/src/byte_packing/byte_packing_stark.rs | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/evm/src/byte_packing/byte_packing_stark.rs b/evm/src/byte_packing/byte_packing_stark.rs index e299670592..e73773914b 100644 --- a/evm/src/byte_packing/byte_packing_stark.rs +++ b/evm/src/byte_packing/byte_packing_stark.rs @@ -362,6 +362,9 @@ impl, const D: usize> Stark for BytePackingSt next_filter * (next_position - one) * (next_position - current_position - one), ); + // 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 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)); @@ -490,7 +493,12 @@ impl, const D: usize> Stark for BytePackingSt builder.mul_sub_extension(is_new_or_inactive, position_diff, is_new_or_inactive); yield_constr.constraint_transition(builder, constraint); - // If the next position is one in an active row, the end flag must be one. + // The last row must be the end of a sequence or a padding row. + let constraint = + builder.mul_sub_extension(current_filter, current_sequence_end, current_filter); + yield_constr.constraint_last_row(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); From 34643fd9d2fe0ba124fbb2e9669812cac0ef733c Mon Sep 17 00:00:00 2001 From: Robin Salen Date: Tue, 19 Sep 2023 19:51:01 -0400 Subject: [PATCH 3/3] Wording --- evm/src/byte_packing/byte_packing_stark.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/evm/src/byte_packing/byte_packing_stark.rs b/evm/src/byte_packing/byte_packing_stark.rs index e73773914b..aa6a2dcf88 100644 --- a/evm/src/byte_packing/byte_packing_stark.rs +++ b/evm/src/byte_packing/byte_packing_stark.rs @@ -354,8 +354,8 @@ impl, const D: usize> Stark for BytePackingSt current_sequence_end * next_filter * (next_sequence_start - one), ); - // The current position in a byte sequence must increase by one on the next row - // or be one on the next row (i.e. a start of a new sequence). + // 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); yield_constr.constraint_transition( @@ -482,8 +482,8 @@ impl, const D: usize> Stark for BytePackingSt let constraint = builder.mul_extension(next_filter, constraint); yield_constr.constraint_transition(builder, constraint); - // The current position in a byte sequence must increase by one on the next row - // or be one on the next row (i.e. a start of a new sequence). + // 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);