Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 84 additions & 16 deletions crypto/stark/src/constraints/zerofier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -115,10 +115,16 @@ pub fn zerofier_evaluations_on_extended_domain<F: IsFFTField>(
.collect()
}

/// Evaluation of the constraint's zerofier at some point `z`, which may be in
/// a field extension.
pub fn evaluate_zerofier<F, E>(
meta: &ConstraintMeta,
/// The end-exemptions correction `∏(z − rᵢ)` at `z`, where `rᵢ` are the roots for a
/// constraint skipping its last `end_exemptions` rows (`1` when there are none).
///
/// This is the only per-constraint-varying factor of the transition zerofier at
/// `z`: the full inverse zerofier is `1/(zᴺ − 1)` × this. Exposed separately so a
/// caller evaluating many constraints at the same `z` computes `1/(zᴺ − 1)` once
/// and this once per distinct `end_exemptions`, rather than a fresh `zᴺ` power and
/// extension inversion per constraint (see the verifier's OOD zerofier sum).
pub fn end_exemptions_correction<F, E>(
end_exemptions: usize,
z: &FieldElement<E>,
trace_primitive_root: &FieldElement<F>,
trace_length: usize,
Expand All @@ -127,16 +133,78 @@ where
F: IsSubFieldOf<E>,
E: IsField,
{
let roots = end_exemptions_roots(meta, trace_primitive_root, trace_length);
// Factor `z - rᵢ` written as `-(rᵢ - z)`: the field ops only go
// subfield − superfield, and `rᵢ ∈ F`, `z ∈ E`.
let end_exemptions_eval = roots.iter().fold(FieldElement::<E>::one(), |acc, root| {
acc * -(root.clone() - z.clone())
});

// 1/(z^N − 1), times the end-exemptions correction.
(-FieldElement::<F>::one() + z.pow(trace_length))
.inv()
.unwrap()
* &end_exemptions_eval
if end_exemptions == 0 {
return FieldElement::<E>::one();
}
// Roots are gᴺ⁻¹, g²⁽ᴺ⁻¹⁾, … (walking backward from the last row by
// g⁻¹ = gᴺ⁻¹). Written `-(rᵢ - z)` so the field ops only go subfield −
// superfield (`rᵢ ∈ F`, `z ∈ E`), matching `end_exemptions_roots`.
let decrement = trace_primitive_root.pow(trace_length - 1);
let mut current = decrement.clone();
let mut acc = FieldElement::<E>::one();
for _ in 0..end_exemptions {
acc *= -(current.clone() - z.clone());
current = &current * &decrement;
}
acc
}

#[cfg(test)]
mod tests {
use super::*;
use math::field::extensions_goldilocks::Degree3GoldilocksExtensionField;
use math::field::goldilocks::GoldilocksField;

type F = GoldilocksField;
type E = Degree3GoldilocksExtensionField;

/// The exempt-row product `∏(z − gⁱ)` over the last `end_exemptions` rows
/// (indices `N−e .. N−1`), derived directly from `gⁱ` — the value
/// [`end_exemptions_correction`] must equal. Independent of its backward
/// `g⁻¹` walk, so a mismatch catches an error in that root derivation.
fn exempt_product(
end_exemptions: usize,
z: &FieldElement<E>,
g: &FieldElement<F>,
n: usize,
) -> FieldElement<E> {
let mut acc = FieldElement::<E>::one();
for i in (n - end_exemptions)..n {
// `-(gⁱ − z) = z − gⁱ`, keeping the ops subfield − superfield to
// match the production body.
acc *= -(g.pow(i) - *z);
}
acc
}

#[test]
fn correction_matches_direct_exempt_product_over_cubic_extension() {
let n = 16usize;
let g = F::get_primitive_root_of_unity(n.trailing_zeros() as u64).unwrap();
// A point off the trace domain, genuinely inside the cubic extension.
let z = FieldElement::<E>::new([
FieldElement::<F>::from(7u64),
FieldElement::<F>::from(3u64),
FieldElement::<F>::from(1u64),
]);

// 0 → one() (no exemptions); 1..=3 exercise the multi-group fold the
// verifier drives, one distinct `end_exemptions` per group.
for end_exemptions in 0..=3usize {
let got = end_exemptions_correction::<F, E>(end_exemptions, &z, &g, n);
let want = exempt_product(end_exemptions, &z, &g, n);
assert_eq!(got, want, "mismatch for end_exemptions = {end_exemptions}");
}
}

#[test]
fn correction_with_no_exemptions_is_one() {
let n = 8usize;
let g = F::get_primitive_root_of_unity(n.trailing_zeros() as u64).unwrap();
let z = FieldElement::<E>::from(5u64);
assert_eq!(
end_exemptions_correction::<F, E>(0, &z, &g, n),
FieldElement::<E>::one()
);
}
}
174 changes: 110 additions & 64 deletions crypto/stark/src/verifier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -328,25 +328,49 @@ pub trait IsStarkVerifier<
let transition_ood_frame_evaluations =
air.compute_transition(&transition_evaluation_context);

let mut denominators =
vec![FieldElement::<FieldExtension>::zero(); air.num_transition_constraints()];
air.constraints_meta().iter().for_each(|m| {
denominators[m.constraint_idx] = crate::constraints::zerofier::evaluate_zerofier(
m,
&challenges.z,
&domain.trace_primitive_root,
trace_length,
);
});
// Every transition constraint's zerofier at z is 1/(zᴺ − 1) times an
// end-exemptions correction ∏(z − rᵢ) that depends only on the
// constraint's `end_exemptions`. 1/(zᴺ − 1) is shared by all of them, so
// compute it once, group the constraints by `end_exemptions` (a tiny set —
// almost always just {0}), accumulate Σ βᵢ·evalᵢ per group, then factor the
// shared inverse and each group's correction out of the sum. Replaces the
// previous per-constraint zᴺ power + extension inversion.
let inv_zerofier_denominator =
match (-FieldElement::<Field>::one() + challenges.z.pow(trace_length)).inv() {
Ok(inv) => inv,
// z lands on the trace domain (zᴺ = 1); an honest off-domain z never
// does. Reject rather than divide by zero.
Err(_) => return false,
};

let transition_c_i_evaluations_sum = itertools::izip!(
transition_ood_frame_evaluations,
&challenges.transition_coeffs,
denominators
)
.fold(FieldElement::zero(), |acc, (eval, beta, denominator)| {
acc + beta * eval * &denominator
});
// Σ βᵢ·evalᵢ bucketed by end_exemptions. `constraints_meta` has one entry per
// active transition constraint; a constraint absent from it contributed a
// zero denominator before and is likewise skipped here.
let mut grouped_numerator_sums: Vec<(usize, FieldElement<FieldExtension>)> = Vec::new();
for m in air.constraints_meta() {
let term = &challenges.transition_coeffs[m.constraint_idx]
* &transition_ood_frame_evaluations[m.constraint_idx];
match grouped_numerator_sums
.iter_mut()
.find(|(exemptions, _)| *exemptions == m.end_exemptions)
{
Some((_, acc)) => *acc += term,
None => grouped_numerator_sums.push((m.end_exemptions, term)),
}
}

let transition_c_i_evaluations_sum = grouped_numerator_sums.into_iter().fold(
FieldElement::zero(),
|acc, (end_exemptions, numerator_sum)| {
let correction = crate::constraints::zerofier::end_exemptions_correction(
end_exemptions,
&challenges.z,
&domain.trace_primitive_root,
trace_length,
);
acc + correction * numerator_sum
},
) * inv_zerofier_denominator;

let composition_poly_ood_evaluation =
&boundary_quotient_ood_evaluation + transition_c_i_evaluations_sum;
Expand Down Expand Up @@ -839,12 +863,6 @@ pub trait IsStarkVerifier<
return None;
}

let mut deep_poly_evaluations = Vec::with_capacity(num_queries);
let mut deep_poly_evaluations_sym = Vec::with_capacity(num_queries);

// Build the base-field LDE evaluations as concatenated slice (precomputed + main)
// without lifting to the extension field. The helper now subtracts directly via
// the F: IsSubFieldOf<E> Sub impl, so we avoid a per-query base->extension lift.
let primitive_root = &Field::get_primitive_root_of_unity(domain.root_order as u64)
.expect("verifier domain root_order is a valid power of two");

Expand All @@ -856,8 +874,48 @@ pub trait IsStarkVerifier<
step_size,
)?;

for (i, iota) in challenges.iotas.iter().enumerate() {
// Each query's DEEP terms divide by (evaluation_point − z·gᵏ) for the OOD
// rows and by (evaluation_point − z^parts) for the composition part. Those
// z·gᵏ row points and z^parts are query-independent, so build them once and
// collect every query point's denominators (primary + symmetric) into ONE
// vector for a single whole-proof batch inverse — instead of a per-query-pair
// inversion (2·num_queries field inversions). One field inversion per proof.
let ood_height = ood_full.height;
let mut z_row_points = Vec::with_capacity(ood_height);
let mut current_z = challenges.z.clone();
for _ in 0..ood_height {
z_row_points.push(current_z.clone());
current_z = primitive_root * &current_z;
}
// z^parts, already computed once in `compute_query_invariant_deep_terms`.
let z_pow_parts = &query_invariant_terms.z_pow;

// Layout per query point: `ood_height` trace denominators then 1 composition
// denominator; points ordered [q0 primary, q0 sym, q1 primary, q1 sym, …].
let stride = ood_height + 1;
let mut denominators = Vec::with_capacity(2 * num_queries * stride);
for iota in challenges.iotas.iter() {
for is_sym in [false, true] {
let evaluation_point =
Self::query_challenge_to_evaluation_point(*iota, is_sym, domain);
for z_row_point in &z_row_points {
denominators.push(&evaluation_point - z_row_point);
}
denominators.push(&evaluation_point - z_pow_parts);
}
}
// One inversion for the whole proof's DEEP denominators. Fails closed if any
// evaluation point lands on an OOD point (malformed proof) — same rejection
// the previous per-pair inversions gave.
FieldElement::inplace_batch_inverse(&mut denominators).ok()?;

let mut deep_poly_evaluations = Vec::with_capacity(num_queries);
let mut deep_poly_evaluations_sym = Vec::with_capacity(num_queries);

for (i, _iota) in challenges.iotas.iter().enumerate() {
let opening = proof.deep_poly_opening(i);
let primary_base = 2 * i * stride;
let sym_base = primary_base + stride;

// Base-field portion as two borrowed slices in commit order —
// precomputed columns FIRST, then main trace columns. The callee
Expand Down Expand Up @@ -885,14 +943,8 @@ pub trait IsStarkVerifier<
.map(|a| a.evaluations_sym())
.unwrap_or(&[]);

let evaluation_point = Self::query_challenge_to_evaluation_point(*iota, false, domain);
let evaluation_point_sym =
Self::query_challenge_to_evaluation_point(*iota, true, domain);
let (evaluation, evaluation_sym) =
Self::reconstruct_deep_composition_poly_evaluation_pair(
&evaluation_point,
&evaluation_point_sym,
primitive_root,
challenges,
&query_invariant_terms,
next_row_cols,
Expand All @@ -905,6 +957,10 @@ pub trait IsStarkVerifier<
lde_main_sym,
lde_aux_sym,
opening.composition_poly().evaluations_sym(),
&denominators[primary_base..primary_base + ood_height],
&denominators[primary_base + ood_height],
&denominators[sym_base..sym_base + ood_height],
&denominators[sym_base + ood_height],
)?;
deep_poly_evaluations.push(evaluation);
deep_poly_evaluations_sym.push(evaluation_sym);
Expand All @@ -917,15 +973,13 @@ pub trait IsStarkVerifier<
/// trace term `coeff*(base-ood)*denom` as `denom*(coeff*base - coeff*ood)`
/// isolates `coeff*ood` (identical for both points, hoisted into
/// `query_invariant_terms`) from `coeff*base` (per-point), so both points
/// share the OOD walk and a single batch-inverse for their denominators.
/// g·z pruning restricts next rows (`row_idx >= step_size`) to the
/// transition-window columns `next_row_cols` — all other next-row
/// coefficients are zero, so those terms vanish from both sums.
/// share the OOD walk. Denominators are pre-inverted by the caller in one
/// whole-proof batch inverse and passed in as slices. g·z pruning restricts
/// next rows (`row_idx >= step_size`) to the transition-window columns
/// `next_row_cols` — all other next-row coefficients are zero, so those terms
/// vanish from both sums.
#[allow(clippy::too_many_arguments)]
fn reconstruct_deep_composition_poly_evaluation_pair<'b>(
evaluation_point: &FieldElement<Field>,
evaluation_point_sym: &FieldElement<Field>,
primitive_root: &FieldElement<Field>,
challenges: &Challenges<FieldExtension>,
query_invariant_terms: &QueryInvariantDeepTerms<FieldExtension>,
next_row_cols: &[usize],
Expand All @@ -938,6 +992,13 @@ pub trait IsStarkVerifier<
lde_trace_main_evaluations_sym: &'b [FieldElement<Field>],
lde_trace_aux_evaluations_sym: &[FieldElement<FieldExtension>],
lde_composition_poly_parts_evaluation_sym: &[FieldElement<FieldExtension>],
// Pre-inverted 1/(evaluation_point − z·gᵏ) per OOD row and
// 1/(evaluation_point − z^parts) for the composition part, primary then
// symmetric — all from the caller's single whole-proof batch inverse.
inv_denoms_trace: &[FieldElement<FieldExtension>],
inv_denom_composition: &FieldElement<FieldExtension>,
inv_denoms_trace_sym: &[FieldElement<FieldExtension>],
inv_denom_composition_sym: &FieldElement<FieldExtension>,
) -> Option<(FieldElement<FieldExtension>, FieldElement<FieldExtension>)> {
let ood_evaluations_table_height = query_invariant_terms.ood_row_sum.len();
let ood_evaluations_table_width = query_invariant_terms.ood_width;
Expand Down Expand Up @@ -977,23 +1038,12 @@ pub trait IsStarkVerifier<
{
return None;
}

// Build both denominator sets (regular, then symmetric) and invert
// them together in a single batch.
let mut denoms = Vec::with_capacity(2 * ood_evaluations_table_height);
let mut current_z = challenges.z.clone();
for _ in 0..ood_evaluations_table_height {
denoms.push(evaluation_point - &current_z);
current_z = primitive_root * &current_z;
}
let mut current_z = challenges.z.clone();
for _ in 0..ood_evaluations_table_height {
denoms.push(evaluation_point_sym - &current_z);
current_z = primitive_root * &current_z;
// The caller passes one pre-inverted trace denominator per OOD row.
if inv_denoms_trace.len() != ood_evaluations_table_height
|| inv_denoms_trace_sym.len() != ood_evaluations_table_height
{
return None;
}
// A malformed proof can land an OOD evaluation point on the LDE coset, reject.
FieldElement::inplace_batch_inverse(&mut denoms).ok()?;
let (denoms_trace, denoms_trace_sym) = denoms.split_at(ood_evaluations_table_height);

let mut trace_term = FieldElement::<FieldExtension>::zero();
let mut trace_term_sym = FieldElement::<FieldExtension>::zero();
Expand Down Expand Up @@ -1032,8 +1082,8 @@ pub trait IsStarkVerifier<
}
}
}
trace_term += &denoms_trace[row_idx] * &(&base_row_sum - ood_row_sum);
trace_term_sym += &denoms_trace_sym[row_idx] * &(&base_row_sum_sym - ood_row_sum);
trace_term += &inv_denoms_trace[row_idx] * &(&base_row_sum - ood_row_sum);
trace_term_sym += &inv_denoms_trace_sym[row_idx] * &(&base_row_sum_sym - ood_row_sum);
}

let number_of_parts = query_invariant_terms.number_of_parts;
Expand All @@ -1044,12 +1094,6 @@ pub trait IsStarkVerifier<
{
return None;
}
let z_pow = &query_invariant_terms.z_pow;

// A malformed proof can make evaluation_point == z_pow, reject.
let mut denom_composition_pair = [evaluation_point - z_pow, evaluation_point_sym - z_pow];
FieldElement::inplace_batch_inverse(&mut denom_composition_pair).ok()?;
let [denom_composition, denom_composition_sym] = denom_composition_pair;

let mut h_sum = FieldElement::<FieldExtension>::zero();
let mut h_sum_sym = FieldElement::<FieldExtension>::zero();
Expand All @@ -1060,8 +1104,10 @@ pub trait IsStarkVerifier<
h_sum += h_i_upsilon * gamma;
h_sum_sym += h_i_upsilon_sym * gamma;
}
let h_terms = (&h_sum - &query_invariant_terms.h_sum_zpow) * denom_composition;
let h_terms_sym = (&h_sum_sym - &query_invariant_terms.h_sum_zpow) * denom_composition_sym;
let h_diff = &h_sum - &query_invariant_terms.h_sum_zpow;
let h_diff_sym = &h_sum_sym - &query_invariant_terms.h_sum_zpow;
let h_terms = &h_diff * inv_denom_composition;
let h_terms_sym = &h_diff_sym * inv_denom_composition_sym;

Some((trace_term + h_terms, trace_term_sym + h_terms_sym))
}
Expand Down
Loading