binius_core/protocols/evalcheck/

verify.rs

// Copyright 2024-2025 Irreducible Inc.

use std::mem;

use binius_field::{util::inner_product_unchecked, TowerField};
use getset::{Getters, MutGetters};
use itertools::chain;
use tracing::instrument;

use super::{
	deserialize_evalcheck_proof,
	error::{Error, VerificationError},
	evalcheck::{EvalcheckHint, EvalcheckMultilinearClaim},
	subclaims::{
		add_bivariate_sumcheck_to_constraints, add_composite_sumcheck_to_constraints,
		composite_mlecheck_meta, packed_sumcheck_meta, shifted_sumcheck_meta,
	},
	EvalPoint,
};
use crate::{
	fiat_shamir::Challenger,
	oracle::{
		ConstraintSet, ConstraintSetBuilder, Error as OracleError, MultilinearOracleSet,
		MultilinearPolyVariant, OracleId,
	},
	polynomial::MultivariatePoly,
	transcript::VerifierTranscript,
	transparent::select_row::SelectRow,
};

/// A mutable verifier state.
///
/// Can be persisted across [`EvalcheckVerifier::verify`] invocations. Accumulates
/// `new_sumchecks` bivariate sumcheck constraints, as well as holds mutable references to
/// the trace (to which new oracles & multilinears may be added during verification)
#[derive(Getters, MutGetters)]
pub struct EvalcheckVerifier<'a, F>
where
	F: TowerField,
{
	/// Mutable reference to the oracle set which is modified to create new claims arising from sumchecks
	pub(crate) oracles: &'a mut MultilinearOracleSet<F>,

	/// The committed evaluation claims in this round
	#[getset(get = "pub", get_mut = "pub")]
	committed_eval_claims: Vec<EvalcheckMultilinearClaim<F>>,

	/// The new sumcheck constraints in this round
	new_sumcheck_constraints: Vec<ConstraintSetBuilder<F>>,

	/// The list of claims that have been verified in this round
	round_claims: Vec<EvalcheckMultilinearClaim<F>>,
}

impl<'a, F: TowerField> EvalcheckVerifier<'a, F> {
	/// Create a new verifier state from a mutable reference to the oracle set
	/// (it needs to be mutable because `new_sumcheck` reduction may add new
	/// oracles & multilinears)
	pub const fn new(oracles: &'a mut MultilinearOracleSet<F>) -> Self {
		Self {
			oracles,
			committed_eval_claims: Vec::new(),
			new_sumcheck_constraints: Vec::new(),
			round_claims: Vec::new(),
		}
	}

	/// A helper method to move out sumcheck constraints
	pub fn take_new_sumcheck_constraints(&mut self) -> Result<Vec<ConstraintSet<F>>, OracleError> {
		self.new_sumcheck_constraints
			.iter_mut()
			.map(|builder| mem::take(builder).build_one(self.oracles))
			.filter(|constraint| !matches!(constraint, Err(OracleError::EmptyConstraintSet)))
			.collect()
	}

	/// Verify an evalcheck claim.
	///
	/// For each claim, we verify the proof by recursively verifying the subclaims in a DFS manner deduplicating previously verified claims
	/// See [`EvalcheckProver::prove`](`super::prove::EvalcheckProver::prove`) docs for more details.
	#[instrument(skip_all, name = "EvalcheckVerifierState::verify", level = "debug")]
	pub fn verify<Challenger_: Challenger>(
		&mut self,
		evalcheck_claims: impl IntoIterator<Item = EvalcheckMultilinearClaim<F>>,
		transcript: &mut VerifierTranscript<Challenger_>,
	) -> Result<(), Error> {
		self.round_claims.clear();
		for claim in evalcheck_claims {
			self.verify_multilinear(claim, transcript)?;
		}
		Ok(())
	}

	fn verify_multilinear<Challenger_: Challenger>(
		&mut self,
		evalcheck_claim: EvalcheckMultilinearClaim<F>,
		transcript: &mut VerifierTranscript<Challenger_>,
	) -> Result<(), Error> {
		let evalcheck_proof = deserialize_evalcheck_proof(&mut transcript.message())?;

		// If the proof is a duplicate claim, we need to check if the claim is already in the round
		// claims, which have been verified.
		if let EvalcheckHint::DuplicateClaim(index) = evalcheck_proof {
			if let Some(expected_claim) = self.round_claims.get(index as usize) {
				if *expected_claim == evalcheck_claim {
					return Ok(());
				}
			}
			return Err(VerificationError::DuplicateClaimMismatch.into());
		}

		self.verify_multilinear_skip_duplicate_check(evalcheck_claim, transcript)
	}

	fn verify_multilinear_skip_duplicate_check<Challenger_: Challenger>(
		&mut self,
		evalcheck_claim: EvalcheckMultilinearClaim<F>,
		transcript: &mut VerifierTranscript<Challenger_>,
	) -> Result<(), Error> {
		self.round_claims.push(evalcheck_claim.clone());

		let EvalcheckMultilinearClaim {
			id,
			eval_point,
			eval,
		} = evalcheck_claim;

		let multilinear = self.oracles.oracle(id);
		let multilinear_label = multilinear.label();
		match multilinear.variant {
			MultilinearPolyVariant::Transparent(inner) => {
				let actual_eval = inner.poly().evaluate(&eval_point)?;
				if actual_eval != eval {
					return Err(VerificationError::IncorrectEvaluation(multilinear_label).into());
				}
			}

			MultilinearPolyVariant::Committed => {
				self.committed_eval_claims.push(EvalcheckMultilinearClaim {
					id,
					eval_point,
					eval,
				});
			}

			MultilinearPolyVariant::Repeating { id, log_count } => {
				let n_vars = eval_point.len() - log_count;
				self.verify_multilinear(
					EvalcheckMultilinearClaim {
						id,
						eval_point: eval_point.slice(0..n_vars),
						eval,
					},
					transcript,
				)?;
			}

			MultilinearPolyVariant::Projected(projected) => {
				let new_eval_point = {
					let (lo, hi) = eval_point.split_at(projected.start_index());
					chain!(lo, projected.values(), hi)
						.copied()
						.collect::<Vec<_>>()
				};

				self.verify_multilinear(
					EvalcheckMultilinearClaim {
						id: projected.id(),
						eval_point: new_eval_point.into(),
						eval,
					},
					transcript,
				)?;
			}

			MultilinearPolyVariant::Shifted(shifted) => {
				let meta = shifted_sumcheck_meta(self.oracles, &shifted, &eval_point)?;
				add_bivariate_sumcheck_to_constraints(
					&meta,
					&mut self.new_sumcheck_constraints,
					shifted.block_size(),
					eval,
				)
			}

			MultilinearPolyVariant::Packed(packed) => {
				let meta = packed_sumcheck_meta(self.oracles, &packed, &eval_point)?;
				add_bivariate_sumcheck_to_constraints(
					&meta,
					&mut self.new_sumcheck_constraints,
					packed.log_degree(),
					eval,
				)
			}

			MultilinearPolyVariant::LinearCombination(linear_combination) => {
				let evals = linear_combination
					.polys()
					.map(|sub_oracle_id| {
						self.verify_multilinear_subclaim(
							sub_oracle_id,
							eval_point.clone(),
							transcript,
						)
					})
					.collect::<Result<Vec<_>, _>>()?;

				// Verify the evaluation of the linear combination over the claimed evaluations
				let actual_eval = linear_combination.offset()
					+ inner_product_unchecked::<F, F>(evals, linear_combination.coefficients());

				if actual_eval != eval {
					return Err(VerificationError::IncorrectEvaluation(multilinear_label).into());
				}
			}
			MultilinearPolyVariant::ZeroPadded(padded) => {
				let subclaim_eval_point = chain!(
					&eval_point[..padded.start_index()],
					&eval_point[padded.start_index() + padded.n_pad_vars()..],
				)
				.copied()
				.collect::<Vec<_>>();

				let zs =
					&eval_point[padded.start_index()..padded.start_index() + padded.n_pad_vars()];
				let select_row = SelectRow::new(zs.len(), padded.nonzero_index())?;
				let select_row_term = select_row
					.evaluate(zs)
					.expect("select_row is constructor with zs.len() variables");

				let inner_eval = eval * select_row_term.invert_or_zero();

				self.verify_multilinear(
					EvalcheckMultilinearClaim {
						id: padded.id(),
						eval_point: subclaim_eval_point.into(),
						eval: inner_eval,
					},
					transcript,
				)?;
			}
			MultilinearPolyVariant::Composite(composition) => {
				let meta = composite_mlecheck_meta(self.oracles, &eval_point)?;
				add_composite_sumcheck_to_constraints(
					meta,
					&mut self.new_sumcheck_constraints,
					&composition,
					eval,
				)
			}
		}

		Ok(())
	}

	fn verify_multilinear_subclaim<Challenger_: Challenger>(
		&mut self,
		oracle_id: OracleId,
		eval_point: EvalPoint<F>,
		transcript: &mut VerifierTranscript<Challenger_>,
	) -> Result<F, Error> {
		// If the subproof is a duplicate claim, we need to check that the claim is already in the
		// round claims and return the evaluation. Otherwise, we verify the subclaim recursively.
		let subproof = deserialize_evalcheck_proof(&mut transcript.message())?;
		match subproof {
			EvalcheckHint::DuplicateClaim(index) => {
				let index = index as usize;
				if self.round_claims[index].id != oracle_id
					|| self.round_claims[index].eval_point != eval_point
				{
					return Err(VerificationError::DuplicateClaimMismatch.into());
				}

				Ok(self.round_claims[index].eval)
			}
			EvalcheckHint::NewClaim => {
				let eval = transcript.message().read_scalar()?;
				let subclaim = EvalcheckMultilinearClaim {
					id: oracle_id,
					eval_point,
					eval,
				};
				self.verify_multilinear_skip_duplicate_check(subclaim, transcript)?;
				Ok(eval)
			}
		}
	}
}