binius_ip/
batch_eval.rs

1// Copyright 2026 The Binius Developers
2
3//! Reducing many evaluation claims on one multilinear to a single claim.
4
5use binius_field::{Field, field::FieldOps};
6use binius_math::multilinear::eq::eq_ind;
7
8use crate::{
9	MultilinearEvalClaim,
10	channel::IPVerifierChannel,
11	sumcheck::{Error, batch_verify},
12};
13
14/// Reduces evaluation claims on one multilinear at several points to one claim at one point.
15///
16/// Every claim names the same multilinear.
17/// So what comes back names it too, at a point none of them chose.
18///
19/// ```text
20///     k claims at k points  ->  one claim at one point
21/// ```
22///
23/// The claim that comes out has the same shape as the ones that went in.
24/// So a caller may reduce again.
25///
26/// That is what lets an aggregation node carry one claim, however many it received.
27///
28/// # The reduction
29///
30/// An evaluation is a sum over the multilinear's own index space.
31/// Its weight is an equality indicator at the point.
32///
33/// Batching the claims weights that sum by a combination of indicators.
34/// That is a plain degree-two sumcheck.
35///
36/// So this is the batched sumcheck plus one reconstruction, and not a protocol of its own.
37///
38/// A single value comes off the channel: the multilinear's evaluation at the reduced point.
39/// Every claim shares it, since every claim is about the same multilinear.
40/// The verifier derives each indicator itself.
41///
42/// # Soundness
43///
44/// Suppose any claim given here is false.
45/// Then the claim returned is false too, except with negligible probability.
46///
47/// For `k` claims over `n` variables that bound is about `(k - 1 + 3n) / |F|`.
48///
49/// Three terms make it up:
50///
51/// - the batching challenge,
52/// - the sumcheck itself, at degree two,
53/// - the chance the combined indicator vanishes where the sumcheck lands.
54///
55/// # Errors
56///
57/// Returns an error if the sumcheck fails, or if the reconstruction does not hold.
58///
59/// The reconstruction is asserted over the channel rather than compared.
60/// So it becomes a constraint on a channel that carries wires.
61/// That is what lets this run inside a circuit.
62///
63/// # Panics
64///
65/// Panics if no claim is given, or if the claims do not all span the same number of variables.
66pub fn verify<F, C>(
67	claims: impl IntoIterator<Item = MultilinearEvalClaim<C::Elem>>,
68	channel: &mut C,
69) -> Result<MultilinearEvalClaim<C::Elem>, Error>
70where
71	F: Field,
72	C: IPVerifierChannel<F>,
73{
74	let claims = claims.into_iter().collect::<Vec<_>>();
75	let n_vars = claims
76		.first()
77		.expect("precondition: at least one claim")
78		.point
79		.len();
80	assert!(
81		claims.iter().all(|claim| claim.point.len() == n_vars),
82		"precondition: every claim must span the same variables"
83	);
84
85	// One sumcheck over the multilinear's index space, at degree two.
86	// Sampling the batching challenge is part of it.
87	let evals = claims
88		.iter()
89		.map(|claim| claim.eval.clone())
90		.collect::<Vec<_>>();
91	let output = batch_verify::<F, C>(n_vars, 2, &evals, channel)?;
92
93	// The multilinear's evaluation is the one thing the verifier cannot derive.
94	let eval = channel.recv_one()?;
95
96	// The rounds bind the highest variable first, so the point reads back in reverse.
97	let mut point = output.challenges;
98	point.reverse();
99
100	// The weight the sumcheck ran against, rebuilt at the point it landed on.
101	//
102	//     weight = sum_j batch^j * eq(point_j, point)
103	let mut weight = C::Elem::zero();
104	let mut batch_power = C::Elem::one();
105	for claim in &claims {
106		weight += eq_ind(&claim.point, &point) * &batch_power;
107		batch_power *= &output.batch_coeff;
108	}
109
110	// The reduced claim is the product of the two factors the sumcheck ran over.
111	channel.assert_zero(eval.clone() * &weight - output.eval)?;
112
113	Ok(MultilinearEvalClaim { eval, point })
114}
binius_ip/batch_eval.rs

binius_ip/
batch_eval.rs
