Implement CTL bundling (#1439)

* Implement CTL bundling

* Cleanup

* Clippy

* Preallocate memory

* Apply comments and remove unnecessary functions.

* Start removing clones

* Set columns and filters inside if condition.

* Remove extra CTL helper columns

* Add circuit version, with cleanup and fixes

* Remove some overhead

* Use refs

* Pacify clippy

---------

Co-authored-by: Robin Salen <salenrobin@gmail.com>

evm/src/all_stark.rs

@@ -1,5 +1,6 @@
 use std::iter;
 
+use itertools::Itertools;
 use plonky2::field::extension::Extendable;
 use plonky2::field::types::Field;
 use plonky2::hash::hash_types::RichField;

evm/src/cpu/memio.rs

@@ -204,7 +204,7 @@ fn eval_packed_store<P: PackedField>(
 }
 
 /// Circuit version of `eval_packed_store`.
-/// /// Evaluates constraints for MSTORE_GENERAL.
+/// Evaluates constraints for MSTORE_GENERAL.
 fn eval_ext_circuit_store<F: RichField + Extendable<D>, const D: usize>(
     builder: &mut plonky2::plonk::circuit_builder::CircuitBuilder<F, D>,
     lv: &CpuColumnsView<ExtensionTarget<D>>,

evm/src/keccak/keccak_stark.rs

@@ -740,13 +740,14 @@ mod tests {
 
         // Fake CTL data.
         let ctl_z_data = CtlZData {
+            helper_columns: vec![PolynomialValues::zero(degree)],
             z: PolynomialValues::zero(degree),
             challenge: GrandProductChallenge {
                 beta: F::ZERO,
                 gamma: F::ZERO,
             },
             columns: vec![],
-            filter: Some(Filter::new_simple(Column::constant(F::ZERO))),
+            filter: vec![Some(Filter::new_simple(Column::constant(F::ZERO)))],
         };
         let ctl_data = CtlData {
             zs_columns: vec![ctl_z_data.clone(); config.num_challenges],

evm/src/lookup.rs

@@ -12,7 +12,10 @@ use plonky2::plonk::circuit_builder::CircuitBuilder;
 use plonky2_util::ceil_div_usize;
 
 use crate::constraint_consumer::{ConstraintConsumer, RecursiveConstraintConsumer};
-use crate::cross_table_lookup::{Column, Filter};
+use crate::cross_table_lookup::{
+    eval_helper_columns, eval_helper_columns_circuit, get_helper_cols, Column, Filter,
+    GrandProductChallenge,
+};
 use crate::evaluation_frame::StarkEvaluationFrame;
 use crate::stark::Stark;
 
@@ -64,48 +67,38 @@ pub(crate) fn lookup_helper_columns<F: Field>(
     let num_helper_columns = lookup.num_helper_columns(constraint_degree);
     let mut helper_columns: Vec<PolynomialValues<F>> = Vec::with_capacity(num_helper_columns);
 
+    let looking_cols = lookup
+        .columns
+        .iter()
+        .map(|col| vec![col.clone()])
+        .collect::<Vec<Vec<Column<F>>>>();
+
+    let grand_challenge = GrandProductChallenge {
+        beta: F::ONE,
+        gamma: challenge,
+    };
+
+    let columns_filters = looking_cols
+        .iter()
+        .zip(lookup.filter_columns.iter())
+        .map(|(col, filter)| (&col[..], filter))
+        .collect::<Vec<_>>();
     // For each batch of `constraint_degree-1` columns `fi`, compute `sum 1/(f_i+challenge)` and
     // add it to the helper columns.
-    // TODO: This does one batch inversion per column. It would also be possible to do one batch inversion
-    // for every group of columns, but that would require building a big vector of all the columns concatenated.
-    // Not sure which approach is better.
     // Note: these are the h_k(x) polynomials in the paper, with a few differences:
     //       * Here, the first ratio m_0(x)/phi_0(x) is not included with the columns batched up to create the
     //         h_k polynomials; instead there's a separate helper column for it (see below).
     //       * Here, we use 1 instead of -1 as the numerator (and subtract later).
     //       * Here, for now, the batch size (l) is always constraint_degree - 1 = 2.
-    for (i, mut col_inds) in (&lookup.columns.iter().chunks(constraint_degree - 1))
-        .into_iter()
-        .enumerate()
-    {
-        let first = col_inds.next().unwrap();
-
-        let mut column = first.eval_all_rows(trace_poly_values);
-        let length = column.len();
-
-        for x in column.iter_mut() {
-            *x = challenge + *x;
-        }
-        let mut acc = F::batch_multiplicative_inverse(&column);
-        if let Some(filter) = &lookup.filter_columns[0] {
-            batch_multiply_inplace(&mut acc, &filter.eval_all_rows(trace_poly_values));
-        }
-
-        for (j, ind) in col_inds.enumerate() {
-            let mut column = ind.eval_all_rows(trace_poly_values);
-            for x in column.iter_mut() {
-                *x = challenge + *x;
-            }
-            column = F::batch_multiplicative_inverse(&column);
-            let filter_idx = (constraint_degree - 1) * i + j + 1;
-            if let Some(filter) = &lookup.filter_columns[filter_idx] {
-                batch_multiply_inplace(&mut column, &filter.eval_all_rows(trace_poly_values));
-            }
-            batch_add_inplace(&mut acc, &column);
-        }
-
-        helper_columns.push(acc.into());
-    }
+    //       * Here, there are filters for the columns, to only select some rows
+    //         in a given column.
+    let mut helper_columns = get_helper_cols(
+        trace_poly_values,
+        trace_poly_values[0].len(),
+        &columns_filters,
+        grand_challenge,
+        constraint_degree,
+    );
 
     // Add `1/(table+challenge)` to the helper columns.
     // This is 1/phi_0(x) = 1/(x + t(x)) from the paper.
@@ -168,38 +161,30 @@ pub(crate) fn eval_packed_lookups_generic<F, FE, P, S, const D: usize, const D2:
     for lookup in lookups {
         let num_helper_columns = lookup.num_helper_columns(degree);
         for &challenge in &lookup_vars.challenges {
-            let challenge = FE::from_basefield(challenge);
+            let grand_challenge = GrandProductChallenge {
+                beta: F::ONE,
+                gamma: challenge,
+            };
+            let lookup_columns = lookup
+                .columns
+                .iter()
+                .map(|col| vec![col.eval_with_next(local_values, next_values)])
+                .collect::<Vec<Vec<P>>>();
+
             // For each chunk, check that `h_i (x+f_2i) (x+f_{2i+1}) = (x+f_2i) * filter_{2i+1} + (x+f_{2i+1}) * filter_2i` if the chunk has length 2
             // or if it has length 1, check that `h_i * (x+f_2i) = filter_2i`, where x is the challenge
-            for (j, chunk) in lookup.columns.chunks(degree - 1).enumerate() {
-                let mut x = lookup_vars.local_values[start + j];
-                let mut y = P::ZEROS;
-                let col_values = chunk
-                    .iter()
-                    .map(|col| col.eval_with_next(local_values, next_values));
-                let filters = lookup.filter_columns
-                    [(degree - 1) * j..(degree - 1) * j + chunk.len()]
-                    .iter()
-                    .map(|maybe_filter| {
-                        if let Some(filter) = maybe_filter {
-                            filter.eval_filter(local_values, next_values)
-                        } else {
-                            P::ONES
-                        }
-                    })
-                    .rev()
-                    .collect::<Vec<_>>();
-                let last_filter_value = filters[0];
-                for (val, f) in col_values.zip_eq(filters) {
-                    x *= val + challenge;
-                    y += (val + challenge) * f;
-                }
-                match chunk.len() {
-                    2 => yield_constr.constraint(x - y),
-                    1 => yield_constr.constraint(x - last_filter_value),
-                    _ => todo!("Allow other constraint degrees."),
-                }
-            }
+            eval_helper_columns(
+                &lookup.filter_columns,
+                &lookup_columns,
+                local_values,
+                next_values,
+                &lookup_vars.local_values[start..start + num_helper_columns - 1],
+                degree,
+                &grand_challenge,
+                yield_constr,
+            );
+
+            let challenge = FE::from_basefield(challenge);
 
             // Check the `Z` polynomial.
             let z = lookup_vars.local_values[start + num_helper_columns - 1];
@@ -245,45 +230,30 @@ pub(crate) fn eval_ext_lookups_circuit<
     let mut start = 0;
     for lookup in lookups {
         let num_helper_columns = lookup.num_helper_columns(degree);
+        let col_values = lookup
+            .columns
+            .iter()
+            .map(|col| vec![col.eval_with_next_circuit(builder, local_values, next_values)])
+            .collect::<Vec<_>>();
+
         for &challenge in &lookup_vars.challenges {
+            let grand_challenge = GrandProductChallenge {
+                beta: builder.one(),
+                gamma: challenge,
+            };
+
+            eval_helper_columns_circuit(
+                builder,
+                &lookup.filter_columns,
+                &col_values,
+                local_values,
+                next_values,
+                &lookup_vars.local_values[start..start + num_helper_columns - 1],
+                degree,
+                &grand_challenge,
+                yield_constr,
+            );
             let challenge = builder.convert_to_ext(challenge);
-            for (j, chunk) in lookup.columns.chunks(degree - 1).enumerate() {
-                let mut x = lookup_vars.local_values[start + j];
-                let mut y = builder.zero_extension();
-                let col_values = chunk
-                    .iter()
-                    .map(|k| k.eval_with_next_circuit(builder, local_values, next_values))
-                    .collect::<Vec<_>>();
-                let filters = lookup.filter_columns
-                    [(degree - 1) * j..(degree - 1) * j + chunk.len()]
-                    .iter()
-                    .map(|maybe_filter| {
-                        if let Some(filter) = maybe_filter {
-                            filter.eval_filter_circuit(builder, local_values, next_values)
-                        } else {
-                            one
-                        }
-                    })
-                    .rev()
-                    .collect::<Vec<_>>();
-                let last_filter_value = filters[0];
-                for (&val, f) in col_values.iter().zip_eq(filters) {
-                    let tmp = builder.add_extension(val, challenge);
-                    x = builder.mul_extension(x, tmp);
-                    y = builder.mul_add_extension(f, tmp, y);
-                }
-                match chunk.len() {
-                    2 => {
-                        let tmp = builder.sub_extension(x, y);
-                        yield_constr.constraint(builder, tmp)
-                    }
-                    1 => {
-                        let tmp = builder.sub_extension(x, last_filter_value);
-                        yield_constr.constraint(builder, tmp)
-                    }
-                    _ => todo!("Allow other constraint degrees."),
-                }
-            }
 
             let z = lookup_vars.local_values[start + num_helper_columns - 1];
             let next_z = lookup_vars.next_values[start + num_helper_columns - 1];

evm/src/proof.rs

@@ -974,7 +974,10 @@ impl<F: RichField + Extendable<D>, const D: usize> StarkOpeningSet<F, D> {
         auxiliary_polys_commitment: &PolynomialBatch<F, C, D>,
         quotient_commitment: &PolynomialBatch<F, C, D>,
         num_lookup_columns: usize,
+        num_ctl_polys: &[usize],
     ) -> Self {
+        let total_num_helper_cols: usize = num_ctl_polys.iter().sum();
+
         // Batch evaluates polynomials on the LDE, at a point `z`.
         let eval_commitment = |z: F::Extension, c: &PolynomialBatch<F, C, D>| {
             c.polynomials
@@ -989,6 +992,9 @@ impl<F: RichField + Extendable<D>, const D: usize> StarkOpeningSet<F, D> {
                 .map(|p| p.eval(z))
                 .collect::<Vec<_>>()
         };
+
+        let auxiliary_first = eval_commitment_base(F::ONE, auxiliary_polys_commitment);
+        let ctl_zs_first = auxiliary_first[num_lookup_columns + total_num_helper_cols..].to_vec();
         // `g * zeta`.
         let zeta_next = zeta.scalar_mul(g);
         Self {
@@ -996,9 +1002,7 @@ impl<F: RichField + Extendable<D>, const D: usize> StarkOpeningSet<F, D> {
             next_values: eval_commitment(zeta_next, trace_commitment),
             auxiliary_polys: eval_commitment(zeta, auxiliary_polys_commitment),
             auxiliary_polys_next: eval_commitment(zeta_next, auxiliary_polys_commitment),
-            ctl_zs_first: eval_commitment_base(F::ONE, auxiliary_polys_commitment)
-                [num_lookup_columns..]
-                .to_vec(),
+            ctl_zs_first,
             quotient_polys: eval_commitment(zeta, quotient_commitment),
         }
     }
@@ -1051,7 +1055,7 @@ pub(crate) struct StarkOpeningSetTarget<const D: usize> {
     pub auxiliary_polys: Vec<ExtensionTarget<D>>,
     /// `ExtensionTarget`s for the opening of lookups and cross-table lookups `Z` polynomials at `g * zeta`.
     pub auxiliary_polys_next: Vec<ExtensionTarget<D>>,
-    /// /// `ExtensionTarget`s for the opening of lookups and cross-table lookups `Z` polynomials at 1.
+    /// `ExtensionTarget`s for the opening of lookups and cross-table lookups `Z` polynomials at 1.
     pub ctl_zs_first: Vec<Target>,
     /// `ExtensionTarget`s for the opening of quotient polynomials at `zeta`.
     pub quotient_polys: Vec<ExtensionTarget<D>>,

evm/src/prover.rs

@@ -135,6 +135,7 @@ where
             &trace_poly_values,
             &all_stark.cross_table_lookups,
             &ctl_challenges,
+            all_stark.arithmetic_stark.constraint_degree()
         )
     );
 
@@ -375,9 +376,14 @@ where
     // We add CTLs to the permutation arguments so that we can batch commit to
     // all auxiliary polynomials.
     let auxiliary_polys = match lookup_helper_columns {
-        None => ctl_data.z_polys(),
+        None => {
+            let mut ctl_polys = ctl_data.ctl_helper_polys();
+            ctl_polys.extend(ctl_data.ctl_z_polys());
+            ctl_polys
+        }
         Some(mut lookup_columns) => {
-            lookup_columns.extend(ctl_data.z_polys());
+            lookup_columns.extend(ctl_data.ctl_helper_polys());
+            lookup_columns.extend(ctl_data.ctl_z_polys());
             lookup_columns
         }
     };
@@ -402,6 +408,8 @@ where
 
     let alphas = challenger.get_n_challenges(config.num_challenges);
 
+    let num_ctl_polys = ctl_data.num_ctl_helper_polys();
+
     #[cfg(test)]
     {
         check_constraints(
@@ -414,6 +422,7 @@ where
             alphas.clone(),
             degree_bits,
             num_lookup_columns,
+            &num_ctl_polys,
         );
     }
 
@@ -432,6 +441,7 @@ where
             alphas,
             degree_bits,
             num_lookup_columns,
+            &num_ctl_polys,
             config,
         )
     );
@@ -486,6 +496,7 @@ where
         &auxiliary_polys_commitment,
         &quotient_commitment,
         stark.num_lookup_helper_columns(config),
+        &num_ctl_polys,
     );
     // Get the FRI openings and observe them.
     challenger.observe_openings(&openings.to_fri_openings());
@@ -502,7 +513,7 @@ where
         timing,
         "compute openings proof",
         PolynomialBatch::prove_openings(
-            &stark.fri_instance(zeta, g, ctl_data.len(), config),
+            &stark.fri_instance(zeta, g, num_ctl_polys.iter().sum(), num_ctl_polys, config),
             &initial_merkle_trees,
             challenger,
             &fri_params,
@@ -535,6 +546,7 @@ fn compute_quotient_polys<'a, F, P, C, S, const D: usize>(
     alphas: Vec<F>,
     degree_bits: usize,
     num_lookup_columns: usize,
+    num_ctl_columns: &[usize],
     config: &StarkConfig,
 ) -> Vec<PolynomialCoeffs<F>>
 where
@@ -545,6 +557,7 @@ where
 {
     let degree = 1 << degree_bits;
     let rate_bits = config.fri_config.rate_bits;
+    let total_num_helper_cols: usize = num_ctl_columns.iter().sum();
 
     let quotient_degree_bits = log2_ceil(stark.quotient_degree_factor());
     assert!(
@@ -616,18 +629,35 @@ where
             // - for each CTL:
             //     - the filter `Column`
             //     - the `Column`s that form the looking/looked table.
+
+            let mut start_index = 0;
             let ctl_vars = ctl_data
                 .zs_columns
                 .iter()
                 .enumerate()
-                .map(|(i, zs_columns)| CtlCheckVars::<F, F, P, 1> {
-                    local_z: auxiliary_polys_commitment.get_lde_values_packed(i_start, step)
-                        [num_lookup_columns + i],
-                    next_z: auxiliary_polys_commitment.get_lde_values_packed(i_next_start, step)
-                        [num_lookup_columns + i],
-                    challenges: zs_columns.challenge,
-                    columns: &zs_columns.columns,
-                    filter: &zs_columns.filter,
+                .map(|(i, zs_columns)| {
+                    let num_ctl_helper_cols = num_ctl_columns[i];
+                    let helper_columns = auxiliary_polys_commitment
+                        .get_lde_values_packed(i_start, step)[num_lookup_columns
+                        + start_index
+                        ..num_lookup_columns + start_index + num_ctl_helper_cols]
+                        .to_vec();
+
+                    let ctl_vars = CtlCheckVars::<F, F, P, 1> {
+                        helper_columns,
+                        local_z: auxiliary_polys_commitment.get_lde_values_packed(i_start, step)
+                            [num_lookup_columns + total_num_helper_cols + i],
+                        next_z: auxiliary_polys_commitment
+                            .get_lde_values_packed(i_next_start, step)
+                            [num_lookup_columns + total_num_helper_cols + i],
+                        challenges: zs_columns.challenge,
+                        columns: zs_columns.columns.clone(),
+                        filter: zs_columns.filter.clone(),
+                    };
+
+                    start_index += num_ctl_helper_cols;
+
+                    ctl_vars
                 })
                 .collect::<Vec<_>>();
 
@@ -691,6 +721,7 @@ fn check_constraints<'a, F, C, S, const D: usize>(
     alphas: Vec<F>,
     degree_bits: usize,
     num_lookup_columns: usize,
+    num_ctl_helper_cols: &[usize],
 ) where
     F: RichField + Extendable<D>,
     C: GenericConfig<D, F = F>,
@@ -699,6 +730,8 @@ fn check_constraints<'a, F, C, S, const D: usize>(
     let degree = 1 << degree_bits;
     let rate_bits = 0; // Set this to higher value to check constraint degree.
 
+    let total_num_helper_cols: usize = num_ctl_helper_cols.iter().sum();
+
     let size = degree << rate_bits;
     let step = 1 << rate_bits;
 
@@ -754,18 +787,34 @@ fn check_constraints<'a, F, C, S, const D: usize>(
             });
 
             // Get the local and next row evaluations for the current STARK's CTL Z polynomials.
+            let mut start_index = 0;
             let ctl_vars = ctl_data
                 .zs_columns
                 .iter()
                 .enumerate()
-                .map(|(iii, zs_columns)| CtlCheckVars::<F, F, F, 1> {
-                    local_z: auxiliary_subgroup_evals[i][num_lookup_columns + iii],
-                    next_z: auxiliary_subgroup_evals[i_next][num_lookup_columns + iii],
-                    challenges: zs_columns.challenge,
-                    columns: &zs_columns.columns,
-                    filter: &zs_columns.filter,
+                .map(|(iii, zs_columns)| {
+                    let num_helper_cols = num_ctl_helper_cols[iii];
+                    let helper_columns = auxiliary_subgroup_evals[i][num_lookup_columns
+                        + start_index
+                        ..num_lookup_columns + start_index + num_helper_cols]
+                        .to_vec();
+                    let ctl_vars = CtlCheckVars::<F, F, F, 1> {
+                        helper_columns,
+                        local_z: auxiliary_subgroup_evals[i]
+                            [num_lookup_columns + total_num_helper_cols + iii],
+                        next_z: auxiliary_subgroup_evals[i_next]
+                            [num_lookup_columns + total_num_helper_cols + iii],
+                        challenges: zs_columns.challenge,
+                        columns: zs_columns.columns.clone(),
+                        filter: zs_columns.filter.clone(),
+                    };
+
+                    start_index += num_helper_cols;
+
+                    ctl_vars
                 })
                 .collect::<Vec<_>>();
+
             // Evaluate the polynomial combining all constraints, including those associated
             // to the permutation and CTL arguments.
             eval_vanishing_poly::<F, F, F, S, D, 1>(

evm/src/recursive_verifier.rs

@@ -229,10 +229,24 @@ where
     let zero_target = builder.zero();
 
     let num_lookup_columns = stark.num_lookup_helper_columns(inner_config);
-    let num_ctl_zs =
-        CrossTableLookup::num_ctl_zs(cross_table_lookups, table, inner_config.num_challenges);
-    let proof_target =
-        add_virtual_stark_proof(&mut builder, stark, inner_config, degree_bits, num_ctl_zs);
+    let (total_num_helpers, num_ctl_zs, num_helpers_by_ctl) =
+        CrossTableLookup::num_ctl_helpers_zs_all(
+            cross_table_lookups,
+            table,
+            inner_config.num_challenges,
+            stark.constraint_degree(),
+        );
+    let num_ctl_helper_zs = num_ctl_zs + total_num_helpers;
+
+    let proof_target = add_virtual_stark_proof(
+        &mut builder,
+        stark,
+        inner_config,
+        degree_bits,
+        num_ctl_helper_zs,
+        num_ctl_zs,
+    );
+
     builder.register_public_inputs(
         &proof_target
             .trace_cap
@@ -257,6 +271,8 @@ where
         cross_table_lookups,
         &ctl_challenges_target,
         num_lookup_columns,
+        total_num_helpers,
+        &num_helpers_by_ctl,
     );
 
     let init_challenger_state_target =
@@ -330,6 +346,12 @@ fn verify_stark_proof_with_challenges_circuit<
     let zero = builder.zero();
     let one = builder.one_extension();
 
+    let num_ctl_polys = ctl_vars
+        .iter()
+        .map(|ctl| ctl.helper_columns.len())
+        .sum::<usize>();
+    let num_ctl_z_polys = ctl_vars.len();
+
     let StarkOpeningSetTarget {
         local_values,
         next_values,
@@ -407,6 +429,7 @@ fn verify_stark_proof_with_challenges_circuit<
         builder,
         challenges.stark_zeta,
         F::primitive_root_of_unity(degree_bits),
+        num_ctl_polys,
         ctl_zs_first.len(),
         inner_config,
     );
@@ -759,6 +782,7 @@ pub(crate) fn add_virtual_stark_proof<
     stark: &S,
     config: &StarkConfig,
     degree_bits: usize,
+    num_ctl_helper_zs: usize,
     num_ctl_zs: usize,
 ) -> StarkProofTarget<D> {
     let fri_params = config.fri_params(degree_bits);
@@ -766,7 +790,7 @@ pub(crate) fn add_virtual_stark_proof<
 
     let num_leaves_per_oracle = vec![
         S::COLUMNS,
-        stark.num_lookup_helper_columns(config) + num_ctl_zs,
+        stark.num_lookup_helper_columns(config) + num_ctl_helper_zs,
         stark.quotient_degree_factor() * config.num_challenges,
     ];
 
@@ -776,7 +800,13 @@ pub(crate) fn add_virtual_stark_proof<
         trace_cap: builder.add_virtual_cap(cap_height),
         auxiliary_polys_cap,
         quotient_polys_cap: builder.add_virtual_cap(cap_height),
-        openings: add_virtual_stark_opening_set::<F, S, D>(builder, stark, num_ctl_zs, config),
+        openings: add_virtual_stark_opening_set::<F, S, D>(
+            builder,
+            stark,
+            num_ctl_helper_zs,
+            num_ctl_zs,
+            config,
+        ),
         opening_proof: builder.add_virtual_fri_proof(&num_leaves_per_oracle, &fri_params),
     }
 }
@@ -784,6 +814,7 @@ pub(crate) fn add_virtual_stark_proof<
 fn add_virtual_stark_opening_set<F: RichField + Extendable<D>, S: Stark<F, D>, const D: usize>(
     builder: &mut CircuitBuilder<F, D>,
     stark: &S,
+    num_ctl_helper_zs: usize,
     num_ctl_zs: usize,
     config: &StarkConfig,
 ) -> StarkOpeningSetTarget<D> {
@@ -791,10 +822,12 @@ fn add_virtual_stark_opening_set<F: RichField + Extendable<D>, S: Stark<F, D>, c
     StarkOpeningSetTarget {
         local_values: builder.add_virtual_extension_targets(S::COLUMNS),
         next_values: builder.add_virtual_extension_targets(S::COLUMNS),
-        auxiliary_polys: builder
-            .add_virtual_extension_targets(stark.num_lookup_helper_columns(config) + num_ctl_zs),
-        auxiliary_polys_next: builder
-            .add_virtual_extension_targets(stark.num_lookup_helper_columns(config) + num_ctl_zs),
+        auxiliary_polys: builder.add_virtual_extension_targets(
+            stark.num_lookup_helper_columns(config) + num_ctl_helper_zs,
+        ),
+        auxiliary_polys_next: builder.add_virtual_extension_targets(
+            stark.num_lookup_helper_columns(config) + num_ctl_helper_zs,
+        ),
         ctl_zs_first: builder.add_virtual_targets(num_ctl_zs),
         quotient_polys: builder
             .add_virtual_extension_targets(stark.quotient_degree_factor() * num_challenges),

evm/src/stark.rs

@@ -92,7 +92,8 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
         &self,
         zeta: F::Extension,
         g: F,
-        num_ctl_zs: usize,
+        num_ctl_helpers: usize,
+        num_ctl_zs: Vec<usize>,
         config: &StarkConfig,
     ) -> FriInstanceInfo<F, D> {
         let trace_oracle = FriOracleInfo {
@@ -102,7 +103,7 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
         let trace_info = FriPolynomialInfo::from_range(TRACE_ORACLE_INDEX, 0..Self::COLUMNS);
 
         let num_lookup_columns = self.num_lookup_helper_columns(config);
-        let num_auxiliary_polys = num_lookup_columns + num_ctl_zs;
+        let num_auxiliary_polys = num_lookup_columns + num_ctl_helpers + num_ctl_zs.len();
         let auxiliary_oracle = FriOracleInfo {
             num_polys: num_auxiliary_polys,
             blinding: false,
@@ -110,9 +111,10 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
         let auxiliary_polys_info =
             FriPolynomialInfo::from_range(AUXILIARY_ORACLE_INDEX, 0..num_auxiliary_polys);
 
+        let mut start_index = num_lookup_columns;
         let ctl_zs_info = FriPolynomialInfo::from_range(
             AUXILIARY_ORACLE_INDEX,
-            num_lookup_columns..num_lookup_columns + num_ctl_zs,
+            num_lookup_columns + num_ctl_helpers..num_auxiliary_polys,
         );
 
         let num_quotient_polys = self.num_quotient_polys(config);
@@ -152,6 +154,7 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
         builder: &mut CircuitBuilder<F, D>,
         zeta: ExtensionTarget<D>,
         g: F,
+        num_ctl_helper_polys: usize,
         num_ctl_zs: usize,
         inner_config: &StarkConfig,
     ) -> FriInstanceInfoTarget<D> {
@@ -162,7 +165,7 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
         let trace_info = FriPolynomialInfo::from_range(TRACE_ORACLE_INDEX, 0..Self::COLUMNS);
 
         let num_lookup_columns = self.num_lookup_helper_columns(inner_config);
-        let num_auxiliary_polys = num_lookup_columns + num_ctl_zs;
+        let num_auxiliary_polys = num_lookup_columns + num_ctl_helper_polys + num_ctl_zs;
         let auxiliary_oracle = FriOracleInfo {
             num_polys: num_auxiliary_polys,
             blinding: false,
@@ -172,7 +175,8 @@ pub trait Stark<F: RichField + Extendable<D>, const D: usize>: Sync {
 
         let ctl_zs_info = FriPolynomialInfo::from_range(
             AUXILIARY_ORACLE_INDEX,
-            num_lookup_columns..num_lookup_columns + num_ctl_zs,
+            num_lookup_columns + num_ctl_helper_polys
+                ..num_lookup_columns + num_ctl_helper_polys + num_ctl_zs,
         );
 
         let num_quotient_polys = self.num_quotient_polys(inner_config);

evm/src/vanishing_poly.rs

@@ -42,7 +42,12 @@ pub(crate) fn eval_vanishing_poly<F, FE, P, S, const D: usize, const D2: usize>(
         );
     }
     // Evaluate the STARK constraints related to the cross-table lookups.
-    eval_cross_table_lookup_checks::<F, FE, P, S, D, D2>(vars, ctl_vars, consumer);
+    eval_cross_table_lookup_checks::<F, FE, P, S, D, D2>(
+        vars,
+        ctl_vars,
+        consumer,
+        stark.constraint_degree(),
+    );
 }
 
 /// Circuit version of `eval_vanishing_poly`.
@@ -66,5 +71,11 @@ pub(crate) fn eval_vanishing_poly_circuit<F, S, const D: usize>(
         eval_ext_lookups_circuit::<F, S, D>(builder, stark, vars, lookup_vars, consumer);
     }
     // Evaluate all of the STARK's constraints related to the cross-table lookups.
-    eval_cross_table_lookup_checks_circuit::<S, F, D>(builder, vars, ctl_vars, consumer);
+    eval_cross_table_lookup_checks_circuit::<S, F, D>(
+        builder,
+        vars,
+        ctl_vars,
+        consumer,
+        stark.constraint_degree(),
+    );
 }

evm/src/verifier.rs

@@ -16,7 +16,8 @@ use crate::constraint_consumer::ConstraintConsumer;
 use crate::cpu::kernel::aggregator::KERNEL;
 use crate::cpu::kernel::constants::global_metadata::GlobalMetadata;
 use crate::cross_table_lookup::{
-    verify_cross_table_lookups, CtlCheckVars, GrandProductChallenge, GrandProductChallengeSet,
+    num_ctl_helper_columns_by_table, verify_cross_table_lookups, CtlCheckVars,
+    GrandProductChallenge, GrandProductChallengeSet,
 };
 use crate::evaluation_frame::StarkEvaluationFrame;
 use crate::lookup::LookupCheckVars;
@@ -56,11 +57,17 @@ where
         cross_table_lookups,
     } = all_stark;
 
+    let num_ctl_helper_cols = num_ctl_helper_columns_by_table(
+        cross_table_lookups,
+        all_stark.arithmetic_stark.constraint_degree(),
+    );
+
     let ctl_vars_per_table = CtlCheckVars::from_proofs(
         &all_proof.stark_proofs,
         cross_table_lookups,
         &ctl_challenges,
         &num_lookup_columns,
+        &num_ctl_helper_cols,
     );
 
     verify_stark_proof_with_challenges(
@@ -300,7 +307,12 @@ pub(crate) fn verify_stark_proof_with_challenges<
     config: &StarkConfig,
 ) -> Result<()> {
     log::debug!("Checking proof: {}", type_name::<S>());
-    validate_proof_shape(stark, proof, config, ctl_vars.len())?;
+    let num_ctl_polys = ctl_vars
+        .iter()
+        .map(|ctl| ctl.helper_columns.len())
+        .sum::<usize>();
+    let num_ctl_z_polys = ctl_vars.len();
+    validate_proof_shape(stark, proof, config, num_ctl_polys, num_ctl_z_polys)?;
     let StarkOpeningSet {
         local_values,
         next_values,
@@ -374,11 +386,16 @@ pub(crate) fn verify_stark_proof_with_challenges<
         proof.quotient_polys_cap.clone(),
     ];
 
+    let num_ctl_zs = ctl_vars
+        .iter()
+        .map(|ctl| ctl.helper_columns.len())
+        .collect::<Vec<_>>();
     verify_fri_proof::<F, C, D>(
         &stark.fri_instance(
             challenges.stark_zeta,
             F::primitive_root_of_unity(degree_bits),
-            ctl_zs_first.len(),
+            num_ctl_polys,
+            num_ctl_zs,
             config,
         ),
         &proof.openings.to_fri_openings(),
@@ -395,6 +412,7 @@ fn validate_proof_shape<F, C, S, const D: usize>(
     stark: &S,
     proof: &StarkProof<F, C, D>,
     config: &StarkConfig,
+    num_ctl_helpers: usize,
     num_ctl_zs: usize,
 ) -> anyhow::Result<()>
 where
@@ -424,7 +442,8 @@ where
     let degree_bits = proof.recover_degree_bits(config);
     let fri_params = config.fri_params(degree_bits);
     let cap_height = fri_params.config.cap_height;
-    let num_auxiliary = num_ctl_zs + stark.num_lookup_helper_columns(config);
+
+    let num_auxiliary = num_ctl_helpers + stark.num_lookup_helper_columns(config) + num_ctl_zs;
 
     ensure!(trace_cap.height() == cap_height);
     ensure!(auxiliary_polys_cap.height() == cap_height);