logos-storage/plonky2
1
0
Fork 0
mirror of https://github.com/logos-storage/plonky2.git synced 2026-01-03 06:13:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

Use logUp for CTLs (#1398)

Browse Source 
* Use LogUp for CTLs

* Update specs

* Invert in batch

* Reorder framework sections
This commit is contained in:
Hamy Ratoanina 2023-12-04 16:26:10 -05:00 committed by GitHub
parent cb2a22a5f6
commit 6c3e3c0e8c
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 126 additions and 133 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

33
evm/spec/framework.tex
View File

@ -30,14 +30,13 @@ After computing $(2^{32} - 1) n_1$, which can be done with a shift and subtracti
At this point we have reduced $n$ to a \texttt{u64}. This partial reduction is adequate for most purposes, but if we needed the result in canonical form, we would perform a final conditional subtraction.
\subsection{Cross-table lookups}
\label{ctl}
The various STARK tables carry out independent operations, but on shared values. We need to check that the shared values are identical in all the STARKs that require them. This is where cross-table lookups (CTLs) come in handy.
Suppose STARK $S_1$ requires an operation -- say $Op$ -- that is carried out by another STARK $S_2$. Then $S_1$ writes the input and output of $Op$ in its own table, and provides the inputs to $S_2$. $S_2$ also writes the inputs and outputs in its rows, and the table's constraints check that $Op$ is carried out correctly. We then need to ensure that the inputs and outputs are the same in $S_1$ and $S_2$.
In other words, we need to ensure that the rows -- reduced to the input and output columns -- of $S_1$ calling $Op$ are permutations of the rows of $S_2$ that carry out $Op$.
In other words, we need to ensure that the rows -- reduced to the input and output columns -- of $S_1$ calling $Op$ are permutations of the rows of $S_2$ that carry out $Op$. Our CTL protocol is also based on logUp and is similar to our range-checks.
To prove this, the first step is to only select the rows of interest in $S_1$ and $S_2$, and filter out the rest. Let $f^1$ be the filter for $S_1$ and $f^2$ the filter for $S_2$. $f^1$ and $f^2$ are constrained to be in $\{0, 1\}$. $f^1 = 1$ (resp. $f^2 = 1$) whenever the row at hand carries out $Op$ in $S_1$ (resp. in $S_2$), and 0 otherwise. Let also $(\alpha, \beta)$ be two random challenges.
@ -45,32 +44,36 @@ The idea is to create subtables $S_1'$ and $S_2'$ of $S_1$ and $S_2$ respectivel
Let $\{c^{1, i}\}_{i=1}^m$ be the columns in $S_1'$ an $\{c^{2,i}\}_{i=1}^m$ be the columns in $S_2'$.
The prover defines a ``running product'' $Z$ for $S_1'$ such that:
The prover defines a ``running sum'' $Z$ for $S_1'$ such that:
\begin{gather*}
Z^{S_1}_{n-1} = 1 \\
Z^{S_1}_{i+1} = Z^{S_1}_i \cdot [f^1_i \cdot \Big(\sum_{j=0}^{m-1} \alpha^j \cdot c^{1, j}_i + \beta \Big) + (1 - f^1_i)]
Z^{S_1}_{n-1} = \frac{1}{\sum_{j=0}^{m-1} \alpha^j \cdot c^{1, j}_{n-1} + \beta} \\
Z^{S_1}_{i+1} = Z^{S_1}_i + f^1_i \cdot \frac{1}{\sum_{j=0}^{m-1} \alpha^j \cdot c^{1, j}_i + \beta}
\end{gather*}
The second equation ``selects'' the terms of interest thanks to $f^1$ and filters out the rest.
Similarly, the prover constructs a running product $Z^{S_2}$for $S_2$. Note that $Z$ is computed ``upside down'': we start with $Z_{n-1} = 1$ and the final product is in $Z_0$.
Similarly, the prover constructs a running sum $Z^{S_2}$for $S_2$. Note that $Z$ is computed ``upside down'': we start with $Z_{n-1}$ and the final sum is in $Z_0$.
On top of the constraints to check that the running products were correctly constructed, the verifier checks that $Z^{S_1}_0 = Z^{S_2}_0$.
On top of the constraints to check that the running sums were correctly constructed, the verifier checks that $Z^{S_1}_0 = Z^{S_2}_0$.
This ensures that the columns in $S_1'$ and the columns in $S_2'$ are permutations of each other.
In other words, the CTL argument is a logUp lookup argument where $S_1'$ is the looking table, $S_2'$ is the looked table, and $S_1' = S_2'$ (all the multiplicities are 1).
For more details about logUp, see the next section.
To sum up, for each STARK $S$, the prover:
\begin{enumerate}
\item constructs a running product $P_i^l$ for each table looking into $S$ (called looking products here),
\item constructs a running product $P^S$ for $S$ (called looked product here),
\item sends the final value for each running product $P_{i, 0}^l$ and $P^S_0$ to the verifier,
\item sends a commitment to $P_i^l$ and $P^S$ to the verifier.
\item constructs a running sum $Z_i^l$ for each table looking into $S$ (called looking sums here),
\item constructs a running sum $Z^S$ for $S$ (called looked sum here),
\item sends the final value for each running sum $Z_{i, 0}^l$ and $Z^S_0$ to the verifier,
\item sends a commitment to $Z_i^l$ and $Z^S$ to the verifier.
\end{enumerate}
Then, for each STARK $S$, the verifier:
\begin{enumerate}
\item computes the product $P = \prod_i P_{i, 0}^l$,
\item checks that $P = P^S_0$,
\item checks that each $P_i^l$ and $P^S$ was correctly constructed.
\item computes the sum $Z = \sum_i Z_{i, 0}^l$,
\item checks that $Z = Z^S_0$,
\item checks that each $Z_i^l$ and $Z^S$ was correctly constructed.
\end{enumerate}
\subsection{Range-checks}
\label{rc}
In most cases, tables deal with U256 words, split into 32-bit limbs (to avoid overflowing the field). To prevent a malicious prover from cheating, it is crucial to range-check those limbs.
@ -151,4 +154,4 @@ Finally, the verifier needs to ensure that the table $t$ was also correctly comp
\item $t(1) = 0$
\item $(t(g^{i+1}) - t(g^{i})) \cdot ((t(g^{i+1}) - t(g^{i})) - 1) = 0$
\item $t(g^{n-1}) = 2^{16} - 1$
\end{enumerate}
\end{enumerate}

BIN
evm/spec/zkevm.pdf
View File

Binary file not shown.

119
evm/src/cross_table_lookup.rs
View File

@ -559,14 +559,14 @@ pub(crate) fn cross_table_lookup_data<F: RichField, const D: usize>(
log::debug!("Processing CTL for {:?}", looked_table.table);
for &challenge in &ctl_challenges.challenges {
let zs_looking = looking_tables.iter().map(|table| {
partial_products(
partial_sums(
&trace_poly_values[table.table as usize],
&table.columns,
&table.filter_column,
challenge,
)
});
let z_looked = partial_products(
let z_looked = partial_sums(
&trace_poly_values[looked_table.table as usize],
&looked_table.columns,
&looked_table.filter_column,
@ -595,40 +595,64 @@ pub(crate) fn cross_table_lookup_data<F: RichField, const D: usize>(
ctl_data_per_table
}
/// Computes the cross-table lookup partial products for one table and given column linear combinations.
/// Computes the cross-table lookup partial sums for one table and given column linear combinations.
/// `trace` represents the trace values for the given table.
/// `columns` are all the column linear combinations to evaluate.
/// `filter_column` is a column linear combination used to determine whether a row should be selected.
/// `challenge` is a cross-table lookup challenge.
/// The initial product `p` is 1.
/// The initial sum `s` is 0.
/// For each row, if the `filter_column` evaluates to 1, then the rows is selected. All the column linear combinations are evaluated at said row. All those evaluations are combined using the challenge to get a value `v`.
/// The product is updated: `p *= v`, and is pushed to the vector of partial products.
fn partial_products<F: Field>(
/// The sum is updated: `s += 1/v`, and is pushed to the vector of partial sums.
fn partial_sums<F: Field>(
trace: &[PolynomialValues<F>],
columns: &[Column<F>],
filter_column: &Option<Column<F>>,
challenge: GrandProductChallenge<F>,
) -> PolynomialValues<F> {
let mut partial_prod = F::ONE;
let mut partial_sum = F::ZERO;
let degree = trace[0].len();
let mut filters = Vec::with_capacity(degree);
let mut res = Vec::with_capacity(degree);
for i in (0..degree).rev() {
let filter = if let Some(column) = filter_column {
column.eval_table(trace, i)
if let Some(column) = filter_column {
let filter = column.eval_table(trace, i);
if filter.is_one() {
filters.push(true);
} else {
assert_eq!(filter, F::ZERO, "Non-binary filter?");
filters.push(false);
}
} else {
F::ONE
filters.push(false);
};
if filter.is_one() {
let combined = if filters[filters.len() - 1] {
let evals = columns
.iter()
.map(|c| c.eval_table(trace, i))
.collect::<Vec<_>>();
partial_prod *= challenge.combine(evals.iter());
challenge.combine(evals.iter())
} else {
assert_eq!(filter, F::ZERO, "Non-binary filter?")
// Dummy value. Cannot be zero since it will be batch-inverted.
F::ONE
};
res.push(partial_prod);
res.push(combined);
}
res = F::batch_multiplicative_inverse(&res);
if !filters[0] {
res[0] = F::ZERO;
}
for i in (1..degree) {
let mut cur_value = res[i - 1];
if filters[i] {
cur_value += res[i];
}
res[i] = cur_value;
}
res.reverse();
res.into()
}
@ -709,11 +733,11 @@ impl<'a, F: RichField + Extendable<D>, const D: usize>
}
/// Checks the cross-table lookup Z polynomials for each table:
/// - Checks that the CTL `Z` partial products are correctly updated.
/// - Checks that the final value of the CTL product is the combination of all STARKs' CTL polynomials.
/// CTL `Z` partial products are upside down: the complete product is on the first row, and
/// - Checks that the CTL `Z` partial sums are correctly updated.
/// - Checks that the final value of the CTL sum is the combination of all STARKs' CTL polynomials.
/// CTL `Z` partial sums are upside down: the complete sum is on the first row, and
/// the first term is on the last row. This allows the transition constraint to be:
/// Z(w) = Z(gw) * combine(w) where combine is called on the local row
/// `combine(w) * (Z(w) - Z(gw)) = filter` where combine is called on the local row
/// and not the next. This enables CTLs across two rows.
pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, S, const D: usize, const D2: usize>(
vars: &S::EvaluationFrame<FE, P, D2>,
@ -748,13 +772,11 @@ pub(crate) fn eval_cross_table_lookup_checks<F, FE, P, S, const D: usize, const
} else {
P::ONES
};
// If the filter evaluates to 1, then the previously computed combination is used.
let select = local_filter * combined + P::ONES - local_filter;
// Check value of `Z(g^(n-1))`
consumer.constraint_last_row(*local_z - select);
// Check `Z(w) = combination * Z(gw)`
consumer.constraint_transition(*next_z * select - *local_z);
consumer.constraint_last_row(*local_z * combined - local_filter);
// Check `Z(w) = Z(gw) * (filter / combination)`
consumer.constraint_transition((*local_z - *next_z) * combined - local_filter);
}
}
@ -831,12 +853,12 @@ impl<'a, F: Field, const D: usize> CtlCheckVarsTarget<'a, F, D> {
}
}
/// Circuit version of `eval_cross_table_lookup_checks`. Checks the cross-table lookups for each table:
/// - Checks that the CTL `Z` partial products are correctly updated.
/// - Checks that the final value of the CTL product is the combination of all STARKs' CTL polynomials.
/// CTL `Z` partial products are upside down: the complete product is on the first row, and
/// Circuit version of `eval_cross_table_lookup_checks`. Checks the cross-table lookup Z polynomials for each table:
/// - Checks that the CTL `Z` partial sums are correctly updated.
/// - Checks that the final value of the CTL sum is the combination of all STARKs' CTL polynomials.
/// CTL `Z` partial sums are upside down: the complete sum is on the first row, and
/// the first term is on the last row. This allows the transition constraint to be:
/// Z(w) = Z(gw) * combine(w) where combine is called on the local row
/// `combine(w) * (Z(w) - Z(gw)) = filter` where combine is called on the local row
/// and not the next. This enables CTLs across two rows.
pub(crate) fn eval_cross_table_lookup_checks_circuit<
S: Stark<F, D>,
@ -866,15 +888,6 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
} else {
one
};
fn select<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
filter: ExtensionTarget<D>,
x: ExtensionTarget<D>,
) -> ExtensionTarget<D> {
let one = builder.one_extension();
let tmp = builder.sub_extension(one, filter);
builder.mul_add_extension(filter, x, tmp) // filter * x + 1 - filter
}
// Compute all linear combinations on the current table, and combine them using the challenge.
let evals = columns
@ -883,14 +896,14 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
.collect::<Vec<_>>();
let combined = challenges.combine_circuit(builder, &evals);
// If the filter evaluates to 1, then the previously computed combination is used.
let select = select(builder, local_filter, combined);
// Check value of `Z(g^(n-1))`
let last_row = builder.sub_extension(*local_z, select);
let last_row = builder.mul_sub_extension(*local_z, combined, local_filter);
consumer.constraint_last_row(builder, last_row);
// Check `Z(w) = combination * Z(gw)`
let transition = builder.mul_sub_extension(*next_z, select, *local_z);
// Check `Z(w) = Z(gw) * (filter / combination)`
let z_diff = builder.sub_extension(*local_z, *next_z);
let lhs = builder.mul_extension(combined, z_diff);
let transition = builder.sub_extension(lhs, local_filter);
consumer.constraint_transition(builder, transition);
}
}
@ -899,7 +912,7 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit<
pub(crate) fn verify_cross_table_lookups<F: RichField + Extendable<D>, const D: usize>(
cross_table_lookups: &[CrossTableLookup<F>],
ctl_zs_first: [Vec<F>; NUM_TABLES],
ctl_extra_looking_products: Vec<Vec<F>>,
ctl_extra_looking_sums: Vec<Vec<F>>,
config: &StarkConfig,
) -> Result<()> {
let mut ctl_zs_openings = ctl_zs_first.iter().map(|v| v.iter()).collect::<Vec<_>>();
@ -912,20 +925,20 @@ pub(crate) fn verify_cross_table_lookups<F: RichField + Extendable<D>, const D:
) in cross_table_lookups.iter().enumerate()
{
// Get elements looking into `looked_table` that are not associated to any STARK.
let extra_product_vec = &ctl_extra_looking_products[looked_table.table as usize];
let extra_sum_vec = &ctl_extra_looking_sums[looked_table.table as usize];
for c in 0..config.num_challenges {
// Compute the combination of all looking table CTL polynomial openings.
let looking_zs_prod = looking_tables
let looking_zs_sum = looking_tables
.iter()
.map(|table| *ctl_zs_openings[table.table as usize].next().unwrap())
.product::<F>()
* extra_product_vec[c];
.sum::<F>()
+ extra_sum_vec[c];
// Get the looked table CTL polynomial opening.
let looked_z = *ctl_zs_openings[looked_table.table as usize].next().unwrap();
// Ensure that the combination of looking table openings is equal to the looked table opening.
ensure!(
looking_zs_prod == looked_z,
looking_zs_sum == looked_z,
"Cross-table lookup {:?} verification failed.",
index
);
@ -941,7 +954,7 @@ pub(crate) fn verify_cross_table_lookups_circuit<F: RichField + Extendable<D>, c
builder: &mut CircuitBuilder<F, D>,
cross_table_lookups: Vec<CrossTableLookup<F>>,
ctl_zs_first: [Vec<Target>; NUM_TABLES],
ctl_extra_looking_products: Vec<Vec<Target>>,
ctl_extra_looking_sums: Vec<Vec<Target>>,
inner_config: &StarkConfig,
) {
let mut ctl_zs_openings = ctl_zs_first.iter().map(|v| v.iter()).collect::<Vec<_>>();
@ -951,21 +964,21 @@ pub(crate) fn verify_cross_table_lookups_circuit<F: RichField + Extendable<D>, c
} in cross_table_lookups.into_iter()
{
// Get elements looking into `looked_table` that are not associated to any STARK.
let extra_product_vec = &ctl_extra_looking_products[looked_table.table as usize];
let extra_sum_vec = &ctl_extra_looking_sums[looked_table.table as usize];
for c in 0..inner_config.num_challenges {
// Compute the combination of all looking table CTL polynomial openings.
let mut looking_zs_prod = builder.mul_many(
let mut looking_zs_sum = builder.add_many(
looking_tables
.iter()
.map(|table| *ctl_zs_openings[table.table as usize].next().unwrap()),
);
looking_zs_prod = builder.mul(looking_zs_prod, extra_product_vec[c]);
looking_zs_sum = builder.add(looking_zs_sum, extra_sum_vec[c]);
// Get the looked table CTL polynomial opening.
let looked_z = *ctl_zs_openings[looked_table.table as usize].next().unwrap();
// Verify that the combination of looking table openings is equal to the looked table opening.
builder.connect(looked_z, looking_zs_prod);
builder.connect(looked_z, looking_zs_sum);
}
}
debug_assert!(ctl_zs_openings.iter_mut().all(|iter| iter.next().is_none()));

18
evm/src/fixed_recursive_verifier.rs
View File

@ -41,9 +41,9 @@ use crate::proof::{
};
use crate::prover::prove;
use crate::recursive_verifier::{
add_common_recursion_gates, add_virtual_public_values,
get_memory_extra_looking_products_circuit, recursive_stark_circuit, set_public_value_targets,
PlonkWrapperCircuit, PublicInputs, StarkWrapperCircuit,
add_common_recursion_gates, add_virtual_public_values, get_memory_extra_looking_sum_circuit,
recursive_stark_circuit, set_public_value_targets, PlonkWrapperCircuit, PublicInputs,
StarkWrapperCircuit,
};
use crate::stark::Stark;
use crate::util::h256_limbs;
@ -565,15 +565,15 @@ where
}
}
// Extra products to add to the looked last value.
// Extra sums to add to the looked last value.
// Only necessary for the Memory values.
let mut extra_looking_products =
vec![vec![builder.one(); stark_config.num_challenges]; NUM_TABLES];
let mut extra_looking_sums =
vec![vec![builder.zero(); stark_config.num_challenges]; NUM_TABLES];
// Memory
extra_looking_products[Table::Memory as usize] = (0..stark_config.num_challenges)
extra_looking_sums[Table::Memory as usize] = (0..stark_config.num_challenges)
.map(|c| {
get_memory_extra_looking_products_circuit(
get_memory_extra_looking_sum_circuit(
&mut builder,
&public_values,
ctl_challenges.challenges[c],
@ -586,7 +586,7 @@ where
&mut builder,
all_cross_table_lookups(),
pis.map(|p| p.ctl_zs_first),
extra_looking_products,
extra_looking_sums,
stark_config,
);

4
evm/src/keccak/keccak_stark.rs
View File

@ -633,7 +633,7 @@ mod tests {
use crate::config::StarkConfig;
use crate::cross_table_lookup::{
CtlData, CtlZData, GrandProductChallenge, GrandProductChallengeSet,
Column, CtlData, CtlZData, GrandProductChallenge, GrandProductChallengeSet,
};
use crate::keccak::columns::reg_output_limb;
use crate::keccak::keccak_stark::{KeccakStark, NUM_INPUTS, NUM_ROUNDS};
@ -748,7 +748,7 @@ mod tests {
gamma: F::ZERO,
},
columns: vec![],
filter_column: None,
filter_column: Some(Column::constant(F::ZERO)),
};
let ctl_data = CtlData {
zs_columns: vec![ctl_z_data.clone(); config.num_challenges],

59
evm/src/recursive_verifier.rs
View File

@ -420,16 +420,13 @@ fn verify_stark_proof_with_challenges_circuit<
);
}
/// Recursive version of `get_memory_extra_looking_products`.
pub(crate) fn get_memory_extra_looking_products_circuit<
F: RichField + Extendable<D>,
const D: usize,
>(
/// Recursive version of `get_memory_extra_looking_sum`.
pub(crate) fn get_memory_extra_looking_sum_circuit<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
public_values: &PublicValuesTarget,
challenge: GrandProductChallenge<Target>,
) -> Target {
let mut product = builder.one();
let mut sum = builder.zero();
// Add metadata writes.
let block_fields_scalars = [
@ -497,34 +494,20 @@ pub(crate) fn get_memory_extra_looking_products_circuit<
let metadata_segment = builder.constant(F::from_canonical_u32(Segment::GlobalMetadata as u32));
block_fields_scalars.map(|(field, target)| {
// Each of those fields fit in 32 bits, hence in a single Target.
product = add_data_write(
builder,
challenge,
product,
metadata_segment,
field,
&[target],
);
sum = add_data_write(builder, challenge, sum, metadata_segment, field, &[target]);
});
beneficiary_random_base_fee_cur_hash_fields.map(|(field, targets)| {
product = add_data_write(
builder,
challenge,
product,
metadata_segment,
field,
targets,
);
sum = add_data_write(builder, challenge, sum, metadata_segment, field, targets);
});
// Add block hashes writes.
let block_hashes_segment = builder.constant(F::from_canonical_u32(Segment::BlockHashes as u32));
for i in 0..256 {
product = add_data_write(
sum = add_data_write(
builder,
challenge,
product,
sum,
block_hashes_segment,
i,
&public_values.block_hashes.prev_hashes[8 * i..8 * (i + 1)],
@ -534,10 +517,10 @@ pub(crate) fn get_memory_extra_looking_products_circuit<
// Add block bloom filters writes.
let bloom_segment = builder.constant(F::from_canonical_u32(Segment::GlobalBlockBloom as u32));
for i in 0..8 {
product = add_data_write(
sum = add_data_write(
builder,
challenge,
product,
sum,
bloom_segment,
i,
&public_values.block_metadata.block_bloom[i * 8..(i + 1) * 8],
@ -573,44 +556,37 @@ pub(crate) fn get_memory_extra_looking_products_circuit<
];
trie_fields.map(|(field, targets)| {
product = add_data_write(
builder,
challenge,
product,
metadata_segment,
field,
&targets,
);
sum = add_data_write(builder, challenge, sum, metadata_segment, field, &targets);
});
// Add kernel hash and kernel length.
let kernel_hash_limbs = h256_limbs::<F>(KERNEL.code_hash);
let kernel_hash_targets: [Target; 8] = from_fn(|i| builder.constant(kernel_hash_limbs[i]));
product = add_data_write(
sum = add_data_write(
builder,
challenge,
product,
sum,
metadata_segment,
GlobalMetadata::KernelHash as usize,
&kernel_hash_targets,
);
let kernel_len_target = builder.constant(F::from_canonical_usize(KERNEL.code.len()));
product = add_data_write(
sum = add_data_write(
builder,
challenge,
product,
sum,
metadata_segment,
GlobalMetadata::KernelLen as usize,
&[kernel_len_target],
);
product
sum
}
fn add_data_write<F: RichField + Extendable<D>, const D: usize>(
builder: &mut CircuitBuilder<F, D>,
challenge: GrandProductChallenge<Target>,
running_product: Target,
running_sum: Target,
segment: Target,
idx: usize,
val: &[Target],
@ -643,7 +619,8 @@ fn add_data_write<F: RichField + Extendable<D>, const D: usize>(
builder.assert_one(row[12]);
let combined = challenge.combine_base_circuit(builder, &row);
builder.mul(running_product, combined)
let inverse = builder.inverse(combined);
builder.add(running_sum, inverse)
}
fn eval_l_0_and_l_last_circuit<F: RichField + Extendable<D>, const D: usize>(

26
evm/src/verifier.rs
View File

@ -122,13 +122,13 @@ where
let public_values = all_proof.public_values;
// Extra products to add to the looked last value.
// Extra sums to add to the looked last value.
// Only necessary for the Memory values.
let mut extra_looking_products = vec![vec![F::ONE; config.num_challenges]; NUM_TABLES];
let mut extra_looking_sums = vec![vec![F::ZERO; config.num_challenges]; NUM_TABLES];
// Memory
extra_looking_products[Table::Memory as usize] = (0..config.num_challenges)
.map(|i| get_memory_extra_looking_products(&public_values, ctl_challenges.challenges[i]))
extra_looking_sums[Table::Memory as usize] = (0..config.num_challenges)
.map(|i| get_memory_extra_looking_sum(&public_values, ctl_challenges.challenges[i]))
.collect_vec();
verify_cross_table_lookups::<F, D>(
@ -136,7 +136,7 @@ where
all_proof
.stark_proofs
.map(|p| p.proof.openings.ctl_zs_first),
extra_looking_products,
extra_looking_sums,
config,
)
}
@ -144,14 +144,14 @@ where
/// Computes the extra product to multiply to the looked value. It contains memory operations not in the CPU trace:
/// - block metadata writes,
/// - trie roots writes.
pub(crate) fn get_memory_extra_looking_products<F, const D: usize>(
pub(crate) fn get_memory_extra_looking_sum<F, const D: usize>(
public_values: &PublicValues,
challenge: GrandProductChallenge<F>,
) -> F
where
F: RichField + Extendable<D>,
{
let mut prod = F::ONE;
let mut sum = F::ZERO;
// Add metadata and tries writes.
let fields = [
@ -241,29 +241,29 @@ where
let segment = F::from_canonical_u32(Segment::GlobalMetadata as u32);
fields.map(|(field, val)| prod = add_data_write(challenge, segment, prod, field as usize, val));
fields.map(|(field, val)| sum = add_data_write(challenge, segment, sum, field as usize, val));
// Add block bloom writes.
let bloom_segment = F::from_canonical_u32(Segment::GlobalBlockBloom as u32);
for index in 0..8 {
let val = public_values.block_metadata.block_bloom[index];
prod = add_data_write(challenge, bloom_segment, prod, index, val);
sum = add_data_write(challenge, bloom_segment, sum, index, val);
}
// Add Blockhashes writes.
let block_hashes_segment = F::from_canonical_u32(Segment::BlockHashes as u32);
for index in 0..256 {
let val = h2u(public_values.block_hashes.prev_hashes[index]);
prod = add_data_write(challenge, block_hashes_segment, prod, index, val);
sum = add_data_write(challenge, block_hashes_segment, sum, index, val);
}
prod
sum
}
fn add_data_write<F, const D: usize>(
challenge: GrandProductChallenge<F>,
segment: F,
running_product: F,
running_sum: F,
index: usize,
val: U256,
) -> F
@ -280,7 +280,7 @@ where
row[j + 4] = F::from_canonical_u32((val >> (j * 32)).low_u32());
}
row[12] = F::ONE; // timestamp
running_product * challenge.combine(row.iter())
running_sum + challenge.combine(row.iter()).inverse()
}
pub(crate) fn verify_stark_proof_with_challenges<