diff --git a/evm/src/cross_table_lookup.rs b/evm/src/cross_table_lookup.rs index a9b90428..315bf42f 100644 --- a/evm/src/cross_table_lookup.rs +++ b/evm/src/cross_table_lookup.rs @@ -25,6 +25,7 @@ use crate::vars::{StarkEvaluationTargets, StarkEvaluationVars}; #[derive(Clone, Debug)] pub struct Column { linear_combination: Vec<(usize, F)>, + next_row_linear_combination: Vec<(usize, F)>, constant: F, } @@ -32,6 +33,7 @@ impl Column { pub fn single(c: usize) -> Self { Self { linear_combination: vec![(c, F::ONE)], + next_row_linear_combination: vec![], constant: F::ZERO, } } @@ -42,9 +44,24 @@ impl Column { cs.into_iter().map(|c| Self::single(*c.borrow())) } + pub fn single_next_row(c: usize) -> Self { + Self { + linear_combination: vec![], + next_row_linear_combination: vec![(c, F::ONE)], + constant: F::ZERO, + } + } + + pub fn singles_next_row>>( + cs: I, + ) -> impl Iterator { + cs.into_iter().map(|c| Self::single_next_row(*c.borrow())) + } + pub fn constant(constant: F) -> Self { Self { linear_combination: vec![], + next_row_linear_combination: vec![], constant, } } @@ -70,6 +87,34 @@ impl Column { ); Self { linear_combination: v, + next_row_linear_combination: vec![], + constant, + } + } + + pub fn linear_combination_and_next_row_with_constant>( + iter: I, + next_row_iter: I, + constant: F, + ) -> Self { + let v = iter.into_iter().collect::>(); + let next_row_v = next_row_iter.into_iter().collect::>(); + + assert!(!v.is_empty() || !next_row_v.is_empty()); + debug_assert_eq!( + v.iter().map(|(c, _)| c).unique().count(), + v.len(), + "Duplicate columns." + ); + debug_assert_eq!( + next_row_v.iter().map(|(c, _)| c).unique().count(), + next_row_v.len(), + "Duplicate columns." + ); + + Self { + linear_combination: v, + next_row_linear_combination: next_row_v, constant, } } @@ -106,13 +151,43 @@ impl Column { + FE::from_basefield(self.constant) } + pub fn eval_with_next(&self, v: &[P], next_v: &[P]) -> P + where + FE: FieldExtension, + P: PackedField, + { + self.linear_combination + .iter() + .map(|&(c, f)| v[c] * FE::from_basefield(f)) + .sum::

() + + self + .next_row_linear_combination + .iter() + .map(|&(c, f)| next_v[c] * FE::from_basefield(f)) + .sum::

() + + FE::from_basefield(self.constant) + } + /// Evaluate on an row of a table given in column-major form. pub fn eval_table(&self, table: &[PolynomialValues], row: usize) -> F { - self.linear_combination + let mut res = self + .linear_combination .iter() .map(|&(c, f)| table[c].values[row] * f) .sum::() - + self.constant + + self.constant; + + // If we access the next row at the last row, for sanity, we consider the next row's values to be 0. + // If CTLs are correctly written, the filter should be 0 in that case anyway. + if !self.next_row_linear_combination.is_empty() && row < table.len() - 1 { + res += self + .next_row_linear_combination + .iter() + .map(|&(c, f)| table[c].values[row + 1] * f) + .sum::(); + } + + res } pub fn eval_circuit( @@ -136,6 +211,36 @@ impl Column { let constant = builder.constant_extension(F::Extension::from_basefield(self.constant)); builder.inner_product_extension(F::ONE, constant, pairs) } + + pub fn eval_with_next_circuit( + &self, + builder: &mut CircuitBuilder, + v: &[ExtensionTarget], + next_v: &[ExtensionTarget], + ) -> ExtensionTarget + where + F: RichField + Extendable, + { + let mut pairs = self + .linear_combination + .iter() + .map(|&(c, f)| { + ( + v[c], + builder.constant_extension(F::Extension::from_basefield(f)), + ) + }) + .collect::>(); + let next_row_pairs = self.next_row_linear_combination.iter().map(|&(c, f)| { + ( + next_v[c], + builder.constant_extension(F::Extension::from_basefield(f)), + ) + }); + pairs.extend(next_row_pairs); + let constant = builder.constant_extension(F::Extension::from_basefield(self.constant)); + builder.inner_product_extension(F::ONE, constant, pairs) + } } #[derive(Clone, Debug)] @@ -276,7 +381,7 @@ fn partial_products( let mut partial_prod = F::ONE; let degree = trace[0].len(); let mut res = Vec::with_capacity(degree); - for i in 0..degree { + for i in (0..degree).rev() { let filter = if let Some(column) = filter_column { column.eval_table(trace, i) } else { @@ -293,6 +398,7 @@ fn partial_products( }; res.push(partial_prod); } + res.reverse(); res.into() } @@ -362,6 +468,10 @@ impl<'a, F: RichField + Extendable, const D: usize> } } +/// CTL Z partial products are upside down: the complete product 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 +/// and not the next. This enables CTLs across two rows. pub(crate) fn eval_cross_table_lookup_checks( vars: StarkEvaluationVars, ctl_vars: &[CtlCheckVars], @@ -380,27 +490,23 @@ pub(crate) fn eval_cross_table_lookup_checks P { - let evals = columns.iter().map(|c| c.eval(v)).collect::>(); - challenges.combine(evals.iter()) - }; - let filter = |v: &[P]| -> P { - if let Some(column) = filter_column { - column.eval(v) - } else { - P::ONES - } - }; - let local_filter = filter(vars.local_values); - let next_filter = filter(vars.next_values); - let select = |filter, x| filter * x + P::ONES - filter; - // Check value of `Z(1)` - consumer.constraint_first_row(*local_z - select(local_filter, combine(vars.local_values))); - // Check `Z(gw) = combination * Z(w)` - consumer.constraint_transition( - *local_z * select(next_filter, combine(vars.next_values)) - *next_z, - ); + let evals = columns + .iter() + .map(|c| c.eval_with_next(vars.local_values, vars.next_values)) + .collect::>(); + let combined = challenges.combine(evals.iter()); + let local_filter = if let Some(column) = filter_column { + column.eval(vars.local_values) + } else { + P::ONES + }; + 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); } } @@ -493,11 +599,6 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit< } else { one }; - let next_filter = if let Some(column) = filter_column { - column.eval_circuit(builder, vars.next_values) - } else { - one - }; fn select, const D: usize>( builder: &mut CircuitBuilder, filter: ExtensionTarget, @@ -508,34 +609,30 @@ pub(crate) fn eval_cross_table_lookup_checks_circuit< builder.mul_add_extension(filter, x, tmp) // filter * x + 1 - filter } - // Check value of `Z(1)` - let local_columns_eval = columns + let evals = columns .iter() - .map(|c| c.eval_circuit(builder, vars.local_values)) + .map(|c| c.eval_with_next_circuit(builder, vars.local_values, vars.next_values)) .collect::>(); - let combined_local = challenges.combine_circuit(builder, &local_columns_eval); - let selected_local = select(builder, local_filter, combined_local); - let first_row = builder.sub_extension(*local_z, selected_local); - consumer.constraint_first_row(builder, first_row); - // Check `Z(gw) = combination * Z(w)` - let next_columns_eval = columns - .iter() - .map(|c| c.eval_circuit(builder, vars.next_values)) - .collect::>(); - let combined_next = challenges.combine_circuit(builder, &next_columns_eval); - let selected_next = select(builder, next_filter, combined_next); - let transition = builder.mul_sub_extension(*local_z, selected_next, *next_z); + + let combined = challenges.combine_circuit(builder, &evals); + let select = select(builder, local_filter, combined); + + // Check value of `Z(g^(n-1))` + let last_row = builder.sub_extension(*local_z, select); + consumer.constraint_last_row(builder, last_row); + // Check `Z(w) = combination * Z(gw)` + let transition = builder.mul_sub_extension(*next_z, select, *local_z); consumer.constraint_transition(builder, transition); } } pub(crate) fn verify_cross_table_lookups, const D: usize>( cross_table_lookups: &[CrossTableLookup], - ctl_zs_lasts: [Vec; NUM_TABLES], + ctl_zs_first: [Vec; NUM_TABLES], ctl_extra_looking_products: Vec>, config: &StarkConfig, ) -> Result<()> { - let mut ctl_zs_openings = ctl_zs_lasts.iter().map(|v| v.iter()).collect::>(); + let mut ctl_zs_openings = ctl_zs_first.iter().map(|v| v.iter()).collect::>(); for ( index, CrossTableLookup { @@ -568,11 +665,11 @@ pub(crate) fn verify_cross_table_lookups, const D: pub(crate) fn verify_cross_table_lookups_circuit, const D: usize>( builder: &mut CircuitBuilder, cross_table_lookups: Vec>, - ctl_zs_lasts: [Vec; NUM_TABLES], + ctl_zs_first: [Vec; NUM_TABLES], ctl_extra_looking_products: Vec>, inner_config: &StarkConfig, ) { - let mut ctl_zs_openings = ctl_zs_lasts.iter().map(|v| v.iter()).collect::>(); + let mut ctl_zs_openings = ctl_zs_first.iter().map(|v| v.iter()).collect::>(); for CrossTableLookup { looking_tables, looked_table, diff --git a/evm/src/fixed_recursive_verifier.rs b/evm/src/fixed_recursive_verifier.rs index 5c0f1f80..855fa47c 100644 --- a/evm/src/fixed_recursive_verifier.rs +++ b/evm/src/fixed_recursive_verifier.rs @@ -526,7 +526,7 @@ where verify_cross_table_lookups_circuit::( &mut builder, all_cross_table_lookups(), - pis.map(|p| p.ctl_zs_last), + pis.map(|p| p.ctl_zs_first), extra_looking_products, stark_config, ); diff --git a/evm/src/proof.rs b/evm/src/proof.rs index 14f22b67..76f3af32 100644 --- a/evm/src/proof.rs +++ b/evm/src/proof.rs @@ -623,7 +623,7 @@ impl, C: GenericConfig, const D: usize> S } pub fn num_ctl_zs(&self) -> usize { - self.openings.ctl_zs_last.len() + self.openings.ctl_zs_first.len() } } @@ -704,8 +704,8 @@ pub struct StarkOpeningSet, const D: usize> { pub permutation_ctl_zs: Vec, /// Openings of permutations and cross-table lookups `Z` polynomials at `g * zeta`. pub permutation_ctl_zs_next: Vec, - /// Openings of cross-table lookups `Z` polynomials at `g^-1`. - pub ctl_zs_last: Vec, + /// Openings of cross-table lookups `Z` polynomials at `1`. + pub ctl_zs_first: Vec, /// Openings of quotient polynomials at `zeta`. pub quotient_polys: Vec, } @@ -717,7 +717,6 @@ impl, const D: usize> StarkOpeningSet { trace_commitment: &PolynomialBatch, permutation_ctl_zs_commitment: &PolynomialBatch, quotient_commitment: &PolynomialBatch, - degree_bits: usize, num_permutation_zs: usize, ) -> Self { let eval_commitment = |z: F::Extension, c: &PolynomialBatch| { @@ -738,10 +737,8 @@ impl, const D: usize> StarkOpeningSet { next_values: eval_commitment(zeta_next, trace_commitment), permutation_ctl_zs: eval_commitment(zeta, permutation_ctl_zs_commitment), permutation_ctl_zs_next: eval_commitment(zeta_next, permutation_ctl_zs_commitment), - ctl_zs_last: eval_commitment_base( - F::primitive_root_of_unity(degree_bits).inverse(), - permutation_ctl_zs_commitment, - )[num_permutation_zs..] + ctl_zs_first: eval_commitment_base(F::ONE, permutation_ctl_zs_commitment) + [num_permutation_zs..] .to_vec(), quotient_polys: eval_commitment(zeta, quotient_commitment), } @@ -765,10 +762,10 @@ impl, const D: usize> StarkOpeningSet { .copied() .collect_vec(), }; - debug_assert!(!self.ctl_zs_last.is_empty()); - let ctl_last_batch = FriOpeningBatch { + debug_assert!(!self.ctl_zs_first.is_empty()); + let ctl_first_batch = FriOpeningBatch { values: self - .ctl_zs_last + .ctl_zs_first .iter() .copied() .map(F::Extension::from_basefield) @@ -776,7 +773,7 @@ impl, const D: usize> StarkOpeningSet { }; FriOpenings { - batches: vec![zeta_batch, zeta_next_batch, ctl_last_batch], + batches: vec![zeta_batch, zeta_next_batch, ctl_first_batch], } } } @@ -787,7 +784,7 @@ pub struct StarkOpeningSetTarget { pub next_values: Vec>, pub permutation_ctl_zs: Vec>, pub permutation_ctl_zs_next: Vec>, - pub ctl_zs_last: Vec, + pub ctl_zs_first: Vec, pub quotient_polys: Vec>, } @@ -797,7 +794,7 @@ impl StarkOpeningSetTarget { buffer.write_target_ext_vec(&self.next_values)?; buffer.write_target_ext_vec(&self.permutation_ctl_zs)?; buffer.write_target_ext_vec(&self.permutation_ctl_zs_next)?; - buffer.write_target_vec(&self.ctl_zs_last)?; + buffer.write_target_vec(&self.ctl_zs_first)?; buffer.write_target_ext_vec(&self.quotient_polys)?; Ok(()) } @@ -807,7 +804,7 @@ impl StarkOpeningSetTarget { let next_values = buffer.read_target_ext_vec::()?; let permutation_ctl_zs = buffer.read_target_ext_vec::()?; let permutation_ctl_zs_next = buffer.read_target_ext_vec::()?; - let ctl_zs_last = buffer.read_target_vec()?; + let ctl_zs_first = buffer.read_target_vec()?; let quotient_polys = buffer.read_target_ext_vec::()?; Ok(Self { @@ -815,7 +812,7 @@ impl StarkOpeningSetTarget { next_values, permutation_ctl_zs, permutation_ctl_zs_next, - ctl_zs_last, + ctl_zs_first, quotient_polys, }) } @@ -838,10 +835,10 @@ impl StarkOpeningSetTarget { .copied() .collect_vec(), }; - debug_assert!(!self.ctl_zs_last.is_empty()); - let ctl_last_batch = FriOpeningBatchTarget { + debug_assert!(!self.ctl_zs_first.is_empty()); + let ctl_first_batch = FriOpeningBatchTarget { values: self - .ctl_zs_last + .ctl_zs_first .iter() .copied() .map(|t| t.to_ext_target(zero)) @@ -849,7 +846,7 @@ impl StarkOpeningSetTarget { }; FriOpeningsTarget { - batches: vec![zeta_batch, zeta_next_batch, ctl_last_batch], + batches: vec![zeta_batch, zeta_next_batch, ctl_first_batch], } } } diff --git a/evm/src/prover.rs b/evm/src/prover.rs index 8f587823..0426da8e 100644 --- a/evm/src/prover.rs +++ b/evm/src/prover.rs @@ -453,7 +453,6 @@ where trace_commitment, &permutation_ctl_zs_commitment, "ient_commitment, - degree_bits, stark.num_permutation_batches(config), ); challenger.observe_openings(&openings.to_fri_openings()); @@ -468,7 +467,7 @@ where timing, "compute openings proof", PolynomialBatch::prove_openings( - &stark.fri_instance(zeta, g, degree_bits, ctl_data.len(), config), + &stark.fri_instance(zeta, g, ctl_data.len(), config), &initial_merkle_trees, challenger, &fri_params, diff --git a/evm/src/recursive_verifier.rs b/evm/src/recursive_verifier.rs index e669f4ab..8a9661bf 100644 --- a/evm/src/recursive_verifier.rs +++ b/evm/src/recursive_verifier.rs @@ -59,7 +59,7 @@ pub struct RecursiveAllProof< pub(crate) struct PublicInputs> { pub(crate) trace_cap: Vec>, - pub(crate) ctl_zs_last: Vec, + pub(crate) ctl_zs_first: Vec, pub(crate) ctl_challenges: GrandProductChallengeSet, pub(crate) challenger_state_before: P, pub(crate) challenger_state_after: P, @@ -85,11 +85,11 @@ impl> Public }; let challenger_state_before = P::new(&mut iter); let challenger_state_after = P::new(&mut iter); - let ctl_zs_last: Vec<_> = iter.collect(); + let ctl_zs_first: Vec<_> = iter.collect(); Self { trace_cap, - ctl_zs_last, + ctl_zs_first, ctl_challenges, challenger_state_before, challenger_state_after, @@ -150,7 +150,7 @@ impl, C: GenericConfig, const D: usize> // Verify the CTL checks. verify_cross_table_lookups::( &cross_table_lookups, - pis.map(|p| p.ctl_zs_last), + pis.map(|p| p.ctl_zs_first), extra_looking_products, inner_config, )?; @@ -350,7 +350,7 @@ where let challenger_state = challenger.compact(&mut builder); builder.register_public_inputs(challenger_state.as_ref()); - builder.register_public_inputs(&proof_target.openings.ctl_zs_last); + builder.register_public_inputs(&proof_target.openings.ctl_zs_first); verify_stark_proof_with_challenges_circuit::( &mut builder, @@ -414,7 +414,7 @@ fn verify_stark_proof_with_challenges_circuit< next_values, permutation_ctl_zs, permutation_ctl_zs_next, - ctl_zs_last, + ctl_zs_first, quotient_polys, } = &proof.openings; let vars = StarkEvaluationTargets { @@ -484,8 +484,7 @@ fn verify_stark_proof_with_challenges_circuit< builder, challenges.stark_zeta, F::primitive_root_of_unity(degree_bits), - degree_bits, - ctl_zs_last.len(), + ctl_zs_first.len(), inner_config, ); builder.verify_fri_proof::( @@ -869,7 +868,7 @@ fn add_virtual_stark_opening_set, S: Stark, c .add_virtual_extension_targets(stark.num_permutation_batches(config) + num_ctl_zs), permutation_ctl_zs_next: builder .add_virtual_extension_targets(stark.num_permutation_batches(config) + num_ctl_zs), - ctl_zs_last: builder.add_virtual_targets(num_ctl_zs), + ctl_zs_first: builder.add_virtual_targets(num_ctl_zs), quotient_polys: builder .add_virtual_extension_targets(stark.quotient_degree_factor() * num_challenges), } diff --git a/evm/src/stark.rs b/evm/src/stark.rs index 72cee0ad..73b51ada 100644 --- a/evm/src/stark.rs +++ b/evm/src/stark.rs @@ -84,7 +84,6 @@ pub trait Stark, const D: usize>: Sync { &self, zeta: F::Extension, g: F, - degree_bits: usize, num_ctl_zs: usize, config: &StarkConfig, ) -> FriInstanceInfo { @@ -131,13 +130,13 @@ pub trait Stark, const D: usize>: Sync { point: zeta.scalar_mul(g), polynomials: [trace_info, permutation_ctl_zs_info].concat(), }; - let ctl_last_batch = FriBatchInfo { - point: F::Extension::primitive_root_of_unity(degree_bits).inverse(), + let ctl_first_batch = FriBatchInfo { + point: F::Extension::ONE, polynomials: ctl_zs_info, }; FriInstanceInfo { oracles: vec![trace_oracle, permutation_ctl_oracle, quotient_oracle], - batches: vec![zeta_batch, zeta_next_batch, ctl_last_batch], + batches: vec![zeta_batch, zeta_next_batch, ctl_first_batch], } } @@ -147,7 +146,6 @@ pub trait Stark, const D: usize>: Sync { builder: &mut CircuitBuilder, zeta: ExtensionTarget, g: F, - degree_bits: usize, num_ctl_zs: usize, inner_config: &StarkConfig, ) -> FriInstanceInfoTarget { @@ -195,14 +193,13 @@ pub trait Stark, const D: usize>: Sync { point: zeta_next, polynomials: [trace_info, permutation_ctl_zs_info].concat(), }; - let ctl_last_batch = FriBatchInfoTarget { - point: builder - .constant_extension(F::Extension::primitive_root_of_unity(degree_bits).inverse()), + let ctl_first_batch = FriBatchInfoTarget { + point: builder.one_extension(), polynomials: ctl_zs_info, }; FriInstanceInfoTarget { oracles: vec![trace_oracle, permutation_ctl_oracle, quotient_oracle], - batches: vec![zeta_batch, zeta_next_batch, ctl_last_batch], + batches: vec![zeta_batch, zeta_next_batch, ctl_first_batch], } } diff --git a/evm/src/verifier.rs b/evm/src/verifier.rs index 1aa9db97..7a0f2d3e 100644 --- a/evm/src/verifier.rs +++ b/evm/src/verifier.rs @@ -135,7 +135,9 @@ where verify_cross_table_lookups::( cross_table_lookups, - all_proof.stark_proofs.map(|p| p.proof.openings.ctl_zs_last), + all_proof + .stark_proofs + .map(|p| p.proof.openings.ctl_zs_first), extra_looking_products, config, ) @@ -308,7 +310,7 @@ where next_values, permutation_ctl_zs, permutation_ctl_zs_next, - ctl_zs_last, + ctl_zs_first, quotient_polys, } = &proof.openings; let vars = StarkEvaluationVars { @@ -374,8 +376,7 @@ where &stark.fri_instance( challenges.stark_zeta, F::primitive_root_of_unity(degree_bits), - degree_bits, - ctl_zs_last.len(), + ctl_zs_first.len(), config, ), &proof.openings.to_fri_openings(), @@ -415,7 +416,7 @@ where next_values, permutation_ctl_zs, permutation_ctl_zs_next, - ctl_zs_last, + ctl_zs_first, quotient_polys, } = openings; @@ -432,7 +433,7 @@ where ensure!(next_values.len() == S::COLUMNS); ensure!(permutation_ctl_zs.len() == num_zs); ensure!(permutation_ctl_zs_next.len() == num_zs); - ensure!(ctl_zs_last.len() == num_ctl_zs); + ensure!(ctl_zs_first.len() == num_ctl_zs); ensure!(quotient_polys.len() == stark.num_quotient_polys(config)); Ok(())