binius_core/protocols/sumcheck/
verify_zerocheck.rs

1// Copyright 2024-2025 Irreducible Inc.
2
3use binius_field::{TowerField, util::inner_product_unchecked};
4use binius_math::{BinarySubspace, CompositionPoly, EvaluationDomain};
5use binius_utils::{bail, checked_arithmetics::log2_ceil_usize, sorting::is_sorted_ascending};
6use tracing::instrument;
7
8use super::{
9	BatchSumcheckOutput,
10	eq_ind::{self, ClaimsSortingOrder},
11	error::{Error, VerificationError},
12	front_loaded,
13	zerocheck::{self, BatchZerocheckOutput, ZerocheckClaim, univariatizing_reduction_claim},
14};
15use crate::{
16	fiat_shamir::{CanSample, Challenger},
17	transcript::VerifierTranscript,
18};
19
20/// Univariatized domain size.
21///
22/// Note that composition over univariatized multilinears has degree $d (2^n - 1)$ and
23/// can be uniquely determined by its evaluations on $d (2^n - 1) + 1$ points. We however
24/// deliberately round this number up to $d 2^n$ to be able to use additive NTT interpolation
25/// techniques on round evaluations.
26pub const fn domain_size(composition_degree: usize, skip_rounds: usize) -> usize {
27	composition_degree << skip_rounds
28}
29
30/// For zerocheck, we know that a honest prover would evaluate to zero on the skipped domain.
31pub const fn extrapolated_scalars_count(composition_degree: usize, skip_rounds: usize) -> usize {
32	composition_degree.saturating_sub(1) << skip_rounds
33}
34
35/// Verify a batched zerocheck protocol execution.
36///
37/// Zerocheck protocol consists of three reductions, executed one after another:
38///  * Small field univariate round over `skip_rounds` low indexed variables, reducing to MLE
39///    evaluation claims on univariatized low indexed projections. This round sums over the same
40///    number of variables in each claim, thus the batching is trivial. For more details on the
41///    inner workings of this round, see
42///    [zerocheck_univariate_evals](`super::prove::univariate::zerocheck_univariate_evals`).
43///  * Front-loaded batching of large-field high-to-low eq-ind sumchecks, resulting in evaluation
44///    claims on a "rectangular" univariatized domain. Note that this arrangement of rounds creates
45///    "jagged" evaluation claims, which may comprise both the challenge from univariate round (at
46///    prefix) as well as all multilinear round challenges (at suffix), with a "gap" in between.
47///  * Single "wide" but "short" batched regular sumcheck of bivariate products between high indexed
48///    projections of the original multilinears (at multilinear round challenges) and Lagrange basis
49///    evaluation at univariate round challenge. This results in multilinear evaluation claims that
50///    EvalCheck can handle. For more details on this reduction, see
51///    [univariatizing_reduction_claim](`super::zerocheck::univariatizing_reduction_claim`).
52#[instrument(skip_all, level = "debug")]
53pub fn batch_verify<F, Composition, Challenger_>(
54	claims: &[ZerocheckClaim<F, Composition>],
55	skip_rounds: usize,
56	transcript: &mut VerifierTranscript<Challenger_>,
57) -> Result<BatchZerocheckOutput<F>, Error>
58where
59	F: TowerField,
60	Composition: CompositionPoly<F> + Clone,
61	Challenger_: Challenger,
62{
63	// Check that the claims are in non-descending order by n_vars
64	if !is_sorted_ascending(claims.iter().map(|claim| claim.n_vars())) {
65		bail!(Error::ClaimsOutOfOrder);
66	}
67
68	let max_n_vars = claims.last().map(|claim| claim.n_vars()).unwrap_or(0);
69
70	if max_n_vars < skip_rounds {
71		bail!(VerificationError::IncorrectSkippedRoundsCount);
72	}
73
74	// Sample challenges for the multilinear eq-ind sumcheck
75	let eq_ind_challenges = transcript.sample_vec(max_n_vars - skip_rounds);
76
77	// Determine univariate round domain size
78	let max_domain_size = claims
79		.iter()
80		.map(|claim| domain_size(claim.max_individual_degree(), skip_rounds))
81		.max()
82		.unwrap_or(0);
83	let zeros_prefix_len = (1 << skip_rounds).min(max_domain_size);
84
85	// Sample batching coefficients
86	let mut batch_coeffs = Vec::with_capacity(claims.len());
87	for _claim in claims {
88		let next_batch_coeff = transcript.sample();
89		batch_coeffs.push(next_batch_coeff);
90	}
91
92	// Read univariate round polynomial for the first `skip_rounds` univariatized rounds
93	// in Lagrange basis, sample univariate round challenge, evaluate round polynomial at challenge
94	let round_evals = transcript
95		.message()
96		.read_scalar_slice(max_domain_size - zeros_prefix_len)?;
97	let univariate_challenge = transcript.sample();
98
99	// REVIEW: consider using novel basis for the univariate round representation
100	//         (instead of Lagrange)
101	let max_dim = log2_ceil_usize(max_domain_size);
102	let subspace = BinarySubspace::<F::Canonical>::with_dim(max_dim)?.isomorphic::<F>();
103	let evaluation_domain = EvaluationDomain::from_points(
104		subspace.iter().take(max_domain_size).collect::<Vec<_>>(),
105		false,
106	)?;
107
108	let lagrange_coeffs = evaluation_domain.lagrange_evals(univariate_challenge);
109	let sum = inner_product_unchecked::<F, F>(
110		round_evals,
111		lagrange_coeffs[zeros_prefix_len..].iter().copied(),
112	);
113
114	// Front-loaded batching of high-to-low eq-ind sumchecks
115	let eq_ind_sumcheck_claims = zerocheck::reduce_to_eq_ind_sumchecks(skip_rounds, claims)?;
116	let sumcheck_claims = eq_ind::reduce_to_regular_sumchecks(&eq_ind_sumcheck_claims)?;
117
118	let batch_sumcheck_verifier =
119		front_loaded::BatchVerifier::new_prebatched(batch_coeffs, sum, &sumcheck_claims)?;
120
121	let mut sumcheck_output = batch_sumcheck_verifier.run(transcript)?;
122
123	// Reverse challenges since folding high-to-low
124	sumcheck_output.challenges.reverse();
125
126	let eq_ind_output = eq_ind::verify_sumcheck_outputs(
127		ClaimsSortingOrder::AscendingVars,
128		&eq_ind_sumcheck_claims,
129		&eq_ind_challenges,
130		sumcheck_output,
131	)?;
132
133	// Univariatizing reduction sumcheck
134	let reduction_claim =
135		univariatizing_reduction_claim(skip_rounds, &eq_ind_output.multilinear_evals)?;
136
137	let univariatize_verifier =
138		front_loaded::BatchVerifier::new(&[reduction_claim.clone()], transcript)?;
139	let mut reduction_sumcheck_output = univariatize_verifier.run(transcript)?;
140
141	// Reverse challenges since folding high-to-low
142	reduction_sumcheck_output.challenges.reverse();
143
144	let BatchSumcheckOutput {
145		challenges: skipped_challenges,
146		multilinear_evals: mut concat_multilinear_evals,
147	} = zerocheck::verify_reduction_sumcheck_output(
148		&reduction_claim,
149		skip_rounds,
150		univariate_challenge,
151		reduction_sumcheck_output,
152	)?;
153
154	let concat_multilinear_evals = concat_multilinear_evals
155		.pop()
156		.expect("multilinear_evals.len() == 1");
157
158	// Fin
159	let output = BatchZerocheckOutput {
160		skipped_challenges,
161		unskipped_challenges: eq_ind_output.challenges,
162		concat_multilinear_evals,
163	};
164
165	Ok(output)
166}
binius_core/protocols/sumcheck/verify_zerocheck.rs

binius_core/protocols/sumcheck/
verify_zerocheck.rs
