logos-storage/plonky2
1
0
Fork 0
mirror of https://github.com/logos-storage/plonky2.git synced 2026-08-24 22:21:47 +00:00
Code Issues Packages Projects Releases Wiki Activity

Remove extra rows in BytePackingStark (#1388)

Browse Source 
* Have at most one row per (un)packing operation in BytePackingStark

* Change specs

* Fix comment

* Fix tests and apply comments

* Fix log_opcodes
This commit is contained in:
Linda Guiga
2023-11-28 10:25:03 -05:00
committed by GitHub
parent ab70bc536d
commit 3440ba94e6
7 changed files with 74 additions and 277 deletions
Download Patch File Download Diff File Expand all files Collapse all files
evm/spec/tables/byte-packing.tex
+9 -4
View File
@@ -9,14 +9,13 @@ This allows faster memory copies between two memory locations, as well as faster
(see \href{https://github.com/0xPolygonZero/plonky2/blob/main/evm/src/cpu/kernel/asm/memory/memcpy.asm}{memcpy.asm} and
\href{https://github.com/0xPolygonZero/plonky2/blob/main/evm/src/cpu/kernel/asm/memory/memset.asm}{memset.asm} modules).
The `BytePackingStark' table will have $\ell$ rows per packing/unpacking operation, where $0 < \ell \leq 32$ is the length of the sequence being processed.
The `BytePackingStark' table has one row per packing/unpacking operation.
Each row contains the following columns:
\begin{enumerate}
\item 5 columns containing information on the initial memory address from which the sequence starts
(namely a flag differentiating read and write operations, address context, segment and offset values, as well as timestamp),
\item $f_{\texttt{end}}$, a flag indicating the end of a sequence,
\item 32 columns $b_i$ indicating the index of the byte being read/written at a given row,
\item 32 columns $b_i$ indicating the length of the byte sequence ($b_i = 1$ if the length is $i+1$, and $b_i = 0$ otherwise),
\item 32 columns $v_i$ indicating the values of the bytes that have been read or written during a sequence,
\item 2 columns $r_i$ needed for range-checking the byte values.
\end{enumerate}
@@ -26,7 +25,7 @@ Whenever a byte unpacking operation is called, the value $\texttt{val}$ is read
Whenever the operation is a byte packing, the bytes are read one by one from memory and stored in the $v_i$ columns of the BytePackingStark table.
Note that because of the different endianness on the memory and EVM sides, we generate rows starting with the final virtual address value (and the associated byte). We decrement the address at each row.
Note that because of the different endianness on the memory and EVM sides, we write bytes starting with the last one.
The $b_i$ columns hold a boolean value. $b_i = 1$ whenever we are currently reading or writing the i-th element in the byte sequence. $b_i = 0$ otherwise.
@@ -39,6 +38,8 @@ The read or written bytes need to be checked against both the cpu and the memory
\item the value (either written to or read from the stack)
\end{enumerate}
The address here corresponds to the address of the first byte.
On the other hand, we need to make sure that the read and write operations correspond to the values read or stored on the memory side. We therefore need a CTL for each byte, checking that the following values are identical in `MemoryStark' and `BytePackingStark':
\begin{enumerate}
\item a flag indicating whether the operation is a read or a write,
@@ -47,6 +48,10 @@ On the other hand, we need to make sure that the read and write operations corre
\item the timestamp
\end{enumerate}
Note that the virtual address has to be recomputed based on the length of the sequence of bytes. The virtual address for the $i$-th byte is written as:
$$ \texttt{virt} + \sum_{j=0}^{31} b_j * j - i$$
where $\sum_{j=0}^{31} b_j * j$ is equal to $\texttt{sequence\_length} - 1$.
\paragraph*{Note on range-check:} Range-checking is necessary whenever we do a memory unpacking operation that will
write values to memory. These values are constrained by the range-check to be 8-bit values, i.e. fitting between 0 and 255 included.
While range-checking values read from memory is not necessary, because we use the same $\texttt{byte\_values}$ columns for both read
evm/spec/zkevm.pdf
BIN
View File
Binary file not shown.
evm/src/byte_packing/byte_packing_stark.rs
+45 -256
View File
@@ -1,28 +1,22 @@
//! This crate enforces the correctness of reading and writing sequences
//! of bytes in Big-Endian ordering from and to the memory.
//!
//! The trace layout consists in N consecutive rows for an `N` byte sequence,
//! with the byte values being cumulatively written to the trace as they are
//! being processed.
//! The trace layout consists in one row for an `N` byte sequence (where 32 ≥ `N` > 0).
//!
//! At row `i` of such a group (starting from 0), the `i`-th byte flag will be activated
//! (to indicate which byte we are going to be processing), but all bytes with index
//! 0 to `i` may have non-zero values, as they have already been processed.
//! At each row the `i`-th byte flag will be activated to indicate a sequence of
//! length i+1.
//!
//! The length of a sequence is stored within each group of rows corresponding to that
//! sequence in a dedicated `SEQUENCE_LEN` column. At any row `i`, the remaining length
//! of the sequence being processed is retrieved from that column and the active byte flag
//! as:
//! The length of a sequence can be retrieved for CTLs as:
//!
//! remaining_length = sequence_length - \sum_{i=0}^31 b[i] * i
//! sequence_length = \sum_{i=0}^31 b[i] * (i + 1)
//!
//! where b[i] is the `i`-th byte flag.
//!
//! Because of the discrepancy in endianness between the different tables, the byte sequences
//! are actually written in the trace in reverse order from the order they are provided.
//! As such, the memory virtual address for a group of rows corresponding to a sequence starts
//! with the final virtual address, corresponding to the final byte being read/written, and
//! is being decremented at each step.
//! We only store the virtual address `virt` of the first byte, and the virtual address for byte `i`
//! can be recovered as:
//! virt_i = virt + sequence_length - 1 - i
//!
//! Note that, when writing a sequence of bytes to memory, both the `U256` value and the
//! corresponding sequence length are being read from the stack. Because of the endianness
@@ -44,10 +38,11 @@ use plonky2::timed;
use plonky2::util::timing::TimingTree;
use plonky2::util::transpose;
use super::columns::BYTE_VALUES_RANGE;
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_FREQUENCIES, SEQUENCE_END, TIMESTAMP,
index_len, value_bytes, ADDR_CONTEXT, ADDR_SEGMENT, ADDR_VIRTUAL, IS_READ, LEN_INDICES_COLS,
NUM_COLUMNS, RANGE_COUNTER, RC_FREQUENCIES, TIMESTAMP,
};
use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
use crate::cross_table_lookup::Column;
@@ -77,9 +72,8 @@ pub(crate) fn ctl_looked_data<F: Field>() -> Vec<Column<F>> {
})
.collect();
// This will correspond to the actual sequence length when the `SEQUENCE_END` flag is on.
let sequence_len: Column<F> = Column::linear_combination(
(0..NUM_BYTES).map(|i| (index_bytes(i), F::from_canonical_usize(i + 1))),
(0..NUM_BYTES).map(|i| (index_len(i), F::from_canonical_usize(i + 1))),
);
Column::singles([ADDR_CONTEXT, ADDR_SEGMENT, ADDR_VIRTUAL])
@@ -93,13 +87,25 @@ pub(crate) fn ctl_looked_data<F: Field>() -> Vec<Column<F>> {
pub(crate) fn ctl_looked_filter<F: Field>() -> Column<F> {
// The CPU table is only interested in our sequence end rows,
// since those contain the final limbs of our packed int.
Column::single(SEQUENCE_END)
Column::sum((0..NUM_BYTES).map(index_len))
}
/// Column linear combination for the `BytePackingStark` table reading/writing the `i`th byte sequence from `MemoryStark`.
pub(crate) fn ctl_looking_memory<F: Field>(i: usize) -> Vec<Column<F>> {
let mut res =
Column::singles([IS_READ, ADDR_CONTEXT, ADDR_SEGMENT, ADDR_VIRTUAL]).collect_vec();
let mut res = Column::singles([IS_READ, ADDR_CONTEXT, ADDR_SEGMENT]).collect_vec();
// Compute the virtual address: `ADDR_VIRTUAL` + `sequence_len` - 1 - i.
let sequence_len_minus_one = (0..NUM_BYTES)
.map(|j| (index_len(j), F::from_canonical_usize(j)))
.collect::<Vec<_>>();
let mut addr_virt_cols = vec![(ADDR_VIRTUAL, F::ONE)];
addr_virt_cols.extend(sequence_len_minus_one);
let addr_virt = Column::linear_combination_with_constant(
addr_virt_cols,
F::NEG_ONE * F::from_canonical_usize(i),
);
res.push(addr_virt);
// The i'th input byte being read/written.
res.push(Column::single(value_bytes(i)));
@@ -114,7 +120,7 @@ pub(crate) fn ctl_looking_memory<F: Field>(i: usize) -> Vec<Column<F>> {
/// CTL filter for reading/writing the `i`th byte of the byte sequence from/to memory.
pub(crate) fn ctl_looking_memory_filter<F: Field>(i: usize) -> Column<F> {
Column::single(index_bytes(i))
Column::sum((i..NUM_BYTES).map(index_len))
}
/// Information about a byte packing operation needed for witness generation.
@@ -165,12 +171,14 @@ impl<F: RichField + Extendable<D>, const D: usize> BytePackingStark<F, D> {
ops: Vec<BytePackingOp>,
min_rows: usize,
) -> Vec<[F; NUM_COLUMNS]> {
let base_len: usize = ops.iter().map(|op| op.bytes.len()).sum();
let base_len: usize = ops.iter().map(|op| usize::from(!op.bytes.is_empty())).sum();
let num_rows = core::cmp::max(base_len.max(BYTE_RANGE_MAX), min_rows).next_power_of_two();
let mut rows = Vec::with_capacity(num_rows);
for op in ops {
rows.extend(self.generate_rows_for_op(op));
if !op.bytes.is_empty() {
rows.push(self.generate_row_for_op(op));
}
}
for _ in rows.len()..num_rows {
@@ -180,7 +188,7 @@ impl<F: RichField + Extendable<D>, const D: usize> BytePackingStark<F, D> {
rows
}
fn generate_rows_for_op(&self, op: BytePackingOp) -> Vec<[F; NUM_COLUMNS]> {
fn generate_row_for_op(&self, op: BytePackingOp) -> [F; NUM_COLUMNS] {
let BytePackingOp {
is_read,
base_address,
@@ -194,34 +202,24 @@ impl<F: RichField + Extendable<D>, const D: usize> BytePackingStark<F, D> {
virt,
} = base_address;
let mut rows = Vec::with_capacity(bytes.len());
let mut row = [F::ZERO; NUM_COLUMNS];
row[IS_READ] = F::from_bool(is_read);
row[ADDR_CONTEXT] = F::from_canonical_usize(context);
row[ADDR_SEGMENT] = F::from_canonical_usize(segment);
// Because of the endianness, we start by the final virtual address value
// and decrement it at each step. Similarly, we process the byte sequence
// in reverse order.
row[ADDR_VIRTUAL] = F::from_canonical_usize(virt + bytes.len() - 1);
// We store the initial virtual segment. But the CTLs,
// we start with virt + sequence_len - 1.
row[ADDR_VIRTUAL] = F::from_canonical_usize(virt);
row[TIMESTAMP] = F::from_canonical_usize(timestamp);
row[index_len(bytes.len() - 1)] = F::ONE;
for (i, &byte) in bytes.iter().rev().enumerate() {
if i == bytes.len() - 1 {
row[SEQUENCE_END] = F::ONE;
}
row[value_bytes(i)] = F::from_canonical_u8(byte);
row[index_bytes(i)] = F::ONE;
rows.push(row);
// Update those fields for the next row
row[index_bytes(i)] = F::ZERO;
row[ADDR_VIRTUAL] -= F::ONE;
}
rows
row
}
fn generate_padding_row(&self) -> [F; NUM_COLUMNS] {
@@ -259,37 +257,6 @@ impl<F: RichField + Extendable<D>, const D: usize> BytePackingStark<F, D> {
}
}
}
/// There is only one `i` for which `local_values[index_bytes(i)]` is non-zero,
/// and `i+1` is the current position:
fn get_active_position<FE, P, const D2: usize>(&self, row: &[P; NUM_COLUMNS]) -> P
where
FE: FieldExtension<D2, BaseField = F>,
P: PackedField<Scalar = FE>,
{
(0..NUM_BYTES)
.map(|i| row[index_bytes(i)] * P::Scalar::from_canonical_usize(i + 1))
.sum()
}
/// Recursive version of `get_active_position`.
fn get_active_position_circuit(
&self,
builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder<F, D>,
row: &[ExtensionTarget<D>; NUM_COLUMNS],
) -> ExtensionTarget<D> {
let mut current_position = row[index_bytes(0)];
for i in 1..NUM_BYTES {
current_position = builder.mul_const_add_extension(
F::from_canonical_usize(i + 1),
row[index_bytes(i)],
current_position,
);
}
current_position
}
}
impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for BytePackingStark<F, D> {
@@ -326,7 +293,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for BytePackingSt
// We filter active columns by summing all the byte indices.
// Constraining each of them to be boolean is done later on below.
let current_filter = local_values[BYTE_INDICES_COLS].iter().copied().sum::<P>();
let current_filter = local_values[LEN_INDICES_COLS].iter().copied().sum::<P>();
yield_constr.constraint(current_filter * (current_filter - one));
// The filter column must start by one.
@@ -338,87 +305,13 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for BytePackingSt
// Each byte index must be boolean.
for i in 0..NUM_BYTES {
let idx_i = local_values[index_bytes(i)];
let idx_i = local_values[index_len(i)];
yield_constr.constraint(idx_i * (idx_i - one));
}
// The sequence start flag column must start by one.
let current_sequence_start = local_values[index_bytes(0)];
yield_constr.constraint_first_row(current_sequence_start - one);
// The sequence end flag must be boolean
let current_sequence_end = local_values[SEQUENCE_END];
yield_constr.constraint(current_sequence_end * (current_sequence_end - one));
// If filter is off, all flags and byte indices must be off.
let byte_indices = local_values[BYTE_INDICES_COLS].iter().copied().sum::<P>();
yield_constr.constraint(
(current_filter - one) * (current_is_read + current_sequence_end + byte_indices),
);
// Only padding rows have their filter turned off.
let next_filter = next_values[BYTE_INDICES_COLS].iter().copied().sum::<P>();
let next_filter = next_values[LEN_INDICES_COLS].iter().copied().sum::<P>();
yield_constr.constraint_transition(next_filter * (next_filter - current_filter));
// Unless the current sequence end flag is activated, the is_read filter must remain unchanged.
let next_is_read = next_values[IS_READ];
yield_constr
.constraint_transition((current_sequence_end - one) * (next_is_read - current_is_read));
// If the sequence end flag is activated, the next row must be a new sequence or filter must be off.
let next_sequence_start = next_values[index_bytes(0)];
yield_constr.constraint_transition(
current_sequence_end * next_filter * (next_sequence_start - one),
);
// 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(local_values);
let next_position = self.get_active_position(next_values);
yield_constr.constraint_transition(
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));
// 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.
let current_context = local_values[ADDR_CONTEXT];
let next_context = next_values[ADDR_CONTEXT];
let current_segment = local_values[ADDR_SEGMENT];
let next_segment = next_values[ADDR_SEGMENT];
let current_virtual = local_values[ADDR_VIRTUAL];
let next_virtual = next_values[ADDR_VIRTUAL];
let current_timestamp = local_values[TIMESTAMP];
let next_timestamp = next_values[TIMESTAMP];
yield_constr.constraint_transition(
next_filter * (next_sequence_start - one) * (next_context - current_context),
);
yield_constr.constraint_transition(
next_filter * (next_sequence_start - one) * (next_segment - current_segment),
);
yield_constr.constraint_transition(
next_filter * (next_sequence_start - one) * (next_timestamp - current_timestamp),
);
yield_constr.constraint_transition(
next_filter * (next_sequence_start - one) * (current_virtual - next_virtual - one),
);
// If not at the end of a sequence, each next byte must equal the current one
// when reading through the sequence, or the next byte index must be one.
for i in 0..NUM_BYTES {
let current_byte = local_values[value_bytes(i)];
let next_byte = next_values[value_bytes(i)];
let next_byte_index = next_values[index_bytes(i)];
yield_constr.constraint_transition(
(current_sequence_end - one) * (next_byte_index - one) * (next_byte - current_byte),
);
}
}
fn eval_ext_circuit(
@@ -448,7 +341,7 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for BytePackingSt
// We filter active columns by summing all the byte indices.
// Constraining each of them to be boolean is done later on below.
let current_filter = builder.add_many_extension(&local_values[BYTE_INDICES_COLS]);
let current_filter = builder.add_many_extension(&local_values[LEN_INDICES_COLS]);
let constraint = builder.mul_sub_extension(current_filter, current_filter, current_filter);
yield_constr.constraint(builder, constraint);
@@ -464,120 +357,16 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for BytePackingSt
// Each byte index must be boolean.
for i in 0..NUM_BYTES {
let idx_i = local_values[index_bytes(i)];
let idx_i = local_values[index_len(i)];
let constraint = builder.mul_sub_extension(idx_i, idx_i, idx_i);
yield_constr.constraint(builder, constraint);
}
// The sequence start flag column must start by one.
let current_sequence_start = local_values[index_bytes(0)];
let constraint = builder.add_const_extension(current_sequence_start, F::NEG_ONE);
yield_constr.constraint_first_row(builder, constraint);
// The sequence end flag must be boolean
let current_sequence_end = local_values[SEQUENCE_END];
let constraint = builder.mul_sub_extension(
current_sequence_end,
current_sequence_end,
current_sequence_end,
);
yield_constr.constraint(builder, constraint);
// If filter is off, all flags and byte indices must be off.
let byte_indices = builder.add_many_extension(&local_values[BYTE_INDICES_COLS]);
let constraint = builder.add_extension(current_sequence_end, byte_indices);
let constraint = builder.add_extension(constraint, current_is_read);
let constraint = builder.mul_sub_extension(constraint, current_filter, constraint);
yield_constr.constraint(builder, constraint);
// Only padding rows have their filter turned off.
let next_filter = builder.add_many_extension(&next_values[BYTE_INDICES_COLS]);
let next_filter = builder.add_many_extension(&next_values[LEN_INDICES_COLS]);
let constraint = builder.sub_extension(next_filter, current_filter);
let constraint = builder.mul_extension(next_filter, constraint);
yield_constr.constraint_transition(builder, constraint);
// Unless the current sequence end flag is activated, the is_read filter must remain unchanged.
let next_is_read = next_values[IS_READ];
let diff_is_read = builder.sub_extension(next_is_read, current_is_read);
let constraint =
builder.mul_sub_extension(diff_is_read, current_sequence_end, diff_is_read);
yield_constr.constraint_transition(builder, constraint);
// If the sequence end flag is activated, the next row must be a new sequence or filter must be off.
let next_sequence_start = next_values[index_bytes(0)];
let constraint = builder.mul_sub_extension(
current_sequence_end,
next_sequence_start,
current_sequence_end,
);
let constraint = builder.mul_extension(next_filter, constraint);
yield_constr.constraint_transition(builder, constraint);
// 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, local_values);
let next_position = self.get_active_position_circuit(builder, next_values);
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);
// 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);
// 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.
let current_context = local_values[ADDR_CONTEXT];
let next_context = next_values[ADDR_CONTEXT];
let current_segment = local_values[ADDR_SEGMENT];
let next_segment = next_values[ADDR_SEGMENT];
let current_virtual = local_values[ADDR_VIRTUAL];
let next_virtual = next_values[ADDR_VIRTUAL];
let current_timestamp = local_values[TIMESTAMP];
let next_timestamp = next_values[TIMESTAMP];
let addr_filter = builder.mul_sub_extension(next_filter, next_sequence_start, next_filter);
{
let constraint = builder.sub_extension(next_context, current_context);
let constraint = builder.mul_extension(addr_filter, constraint);
yield_constr.constraint_transition(builder, constraint);
}
{
let constraint = builder.sub_extension(next_segment, current_segment);
let constraint = builder.mul_extension(addr_filter, constraint);
yield_constr.constraint_transition(builder, constraint);
}
{
let constraint = builder.sub_extension(next_timestamp, current_timestamp);
let constraint = builder.mul_extension(addr_filter, constraint);
yield_constr.constraint_transition(builder, constraint);
}
{
let constraint = builder.sub_extension(current_virtual, next_virtual);
let constraint = builder.mul_sub_extension(addr_filter, constraint, addr_filter);
yield_constr.constraint_transition(builder, constraint);
}
// If not at the end of a sequence, each next byte must equal the current one
// when reading through the sequence, or the next byte index must be one.
for i in 0..NUM_BYTES {
let current_byte = local_values[value_bytes(i)];
let next_byte = next_values[value_bytes(i)];
let next_byte_index = next_values[index_bytes(i)];
let byte_diff = builder.sub_extension(next_byte, current_byte);
let constraint = builder.mul_sub_extension(byte_diff, next_byte_index, byte_diff);
let constraint =
builder.mul_sub_extension(constraint, current_sequence_end, constraint);
yield_constr.constraint_transition(builder, constraint);
}
}
fn constraint_degree(&self) -> usize {
evm/src/byte_packing/columns.rs
+13 -14
View File
@@ -6,24 +6,20 @@ use crate::byte_packing::NUM_BYTES;
/// 1 if this is a READ operation, and 0 if this is a WRITE operation.
pub(crate) const IS_READ: usize = 0;
/// 1 if this is the end of a sequence of bytes.
/// This is also used as filter for the CTL.
pub(crate) const SEQUENCE_END: usize = IS_READ + 1;
pub(super) const BYTES_INDICES_START: usize = SEQUENCE_END + 1;
// There are `NUM_BYTES` columns used to represent the index of the active byte
// for a given row of a byte (un)packing operation.
pub(crate) const fn index_bytes(i: usize) -> usize {
pub(super) const LEN_INDICES_START: usize = IS_READ + 1;
// There are `NUM_BYTES` columns used to represent the length of
// the input byte sequence for a (un)packing operation.
// index_len(i) is 1 iff the length is i+1.
pub(crate) const fn index_len(i: usize) -> usize {
debug_assert!(i < NUM_BYTES);
BYTES_INDICES_START + i
LEN_INDICES_START + i
}
// 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<usize> =
BYTES_INDICES_START..BYTES_INDICES_START + NUM_BYTES;
// Note: Those are used to obtain the length of a sequence of bytes being processed.
pub(crate) const LEN_INDICES_COLS: Range<usize> = LEN_INDICES_START..LEN_INDICES_START + NUM_BYTES;
pub(crate) const ADDR_CONTEXT: usize = BYTES_INDICES_START + NUM_BYTES;
pub(crate) const ADDR_CONTEXT: usize = LEN_INDICES_START + NUM_BYTES;
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;
@@ -32,12 +28,15 @@ pub(crate) const TIMESTAMP: usize = ADDR_VIRTUAL + 1;
const BYTES_VALUES_START: usize = TIMESTAMP + 1;
// There are `NUM_BYTES` columns used to store the values of the bytes
// that are being read/written for an (un)packing operation.
// If `index_bytes(i) == 1`, then all `value_bytes(j) for j <= i` may be non-zero.
pub(crate) const fn value_bytes(i: usize) -> usize {
debug_assert!(i < NUM_BYTES);
BYTES_VALUES_START + i
}
/// Range of columns containing the bytes values.
pub(crate) const BYTE_VALUES_RANGE: Range<usize> =
BYTES_VALUES_START..BYTES_VALUES_START + NUM_BYTES;
/// The counter column (used for the range check) starts from 0 and increments.
pub(crate) const RANGE_COUNTER: usize = BYTES_VALUES_START + NUM_BYTES;
/// The frequencies column used in logUp.
evm/src/witness/traces.rs
+5 -1
View File
@@ -69,7 +69,11 @@ impl<T: Copy> Traces<T> {
Operation::RangeCheckOperation { .. } => 1,
})
.sum(),
byte_packing_len: self.byte_packing_ops.iter().map(|op| op.bytes.len()).sum(),
byte_packing_len: self
.byte_packing_ops
.iter()
.map(|op| usize::from(!op.bytes.is_empty()))
.sum(),
cpu_len: self.cpu.len(),
keccak_len: self.keccak_inputs.len() * keccak::keccak_stark::NUM_ROUNDS,
keccak_sponge_len: self
evm/tests/empty_txn_list.rs
+1 -1
View File
@@ -79,7 +79,7 @@ fn test_empty_txn_list() -> anyhow::Result<()> {
let all_circuits = AllRecursiveCircuits::<F, C, D>::new(
&all_stark,
&[16..17, 11..12, 15..16, 14..15, 9..11, 12..13, 18..19], // Minimal ranges to prove an empty list
&[16..17, 10..11, 15..16, 14..15, 9..11, 12..13, 18..19], // Minimal ranges to prove an empty list
&config,
);
evm/tests/log_opcode.rs
+1 -1
View File
@@ -459,7 +459,7 @@ fn test_log_with_aggreg() -> anyhow::Result<()> {
// Preprocess all circuits.
let all_circuits = AllRecursiveCircuits::<F, C, D>::new(
&all_stark,
&[16..17, 17..19, 17..18, 14..15, 10..11, 12..13, 19..20],
&[16..17, 15..16, 17..18, 14..15, 10..11, 12..13, 19..20],
&config,
);