binius_spartan_verifier/

lib.rs

// Copyright 2025 Irreducible Inc.
// Copyright 2026 The Binius Developers

//! Spartan-based proof verification for Binius64 constraint systems.
//!
//! This crate provides the [`Verifier`] struct for verifying zero-knowledge proofs
//! generated by `binius_spartan_prover`. It implements the Spartan protocol adapted
//! for Binius64's constraint system.
//!
//! # When to use this crate
//!
//! Use this crate when you have a constraint system built with `binius_spartan_frontend`
//! and need to verify a Spartan-based proof. This is an alternative to the main
//! `binius_verifier` crate.
//!
//! # Key types
//!
//! - [`Verifier`] - Main verification interface; call [`Verifier::setup`] with a constraint system,
//!   then [`Verifier::verify`] with a proof and public inputs
//! - [`IOPVerifier`] - Core IOP verification logic, independent of the compilation strategy
//! - [`Error`] - Error type returned when proof verification fails
//!
//! # Related crates
//!
//! - `binius_spartan_prover` - Proving counterpart
//! - `binius_spartan_frontend` - Constraint system builder for Spartan
//! - `binius_verifier` - Alternative verification backend

#![warn(rustdoc::missing_crate_level_docs)]

pub mod config;
pub mod constraint_system;
pub mod wiring;
pub mod wrapper;

use std::{marker::PhantomData, rc::Rc};

use binius_field::{BinaryField, Field, field::FieldOps};
use binius_hash::HashSuite;
use binius_iop::{
	basefold,
	basefold::compiler::BaseFoldVerifierCompiler,
	channel::{
		IOPVerifierChannel, OracleSpec,
		oracle_setup::{DummyElem, OracleSetupChannel},
	},
	fri::{self, MinProofSizeStrategy},
	merkle_tree::BinaryMerkleTreeScheme,
};
use binius_ip::{channel::IPVerifierChannel, mlecheck, sumcheck};
use binius_math::{multilinear::eq::eq_ind_partial_eval_scalars, univariate::evaluate_univariate};
use binius_spartan_frontend::constraint_system::{ConstraintSystem, WitnessSegment};
use binius_transcript::{VerifierTranscript, fiat_shamir::Challenger};
use binius_utils::{DeserializeBytes, checked_arithmetics::checked_log_2};
use digest::Output;

use crate::constraint_system::{BlindingInfo, ConstraintSystemPadded};

pub const SECURITY_BITS: usize = 96;

/// Output of the multiplication constraint check verification.
#[derive(Debug, Clone)]
pub struct MulcheckOutput<F> {
	/// Evaluation of operand A at the challenge point.
	pub a_eval: F,
	/// Evaluation of operand B at the challenge point.
	pub b_eval: F,
	/// Evaluation of operand C at the challenge point.
	pub c_eval: F,
	/// Evaluation of the mask polynomial at the challenge point.
	pub mask_eval: F,
	/// The challenge point from the sumcheck reduction.
	pub r_x: Vec<F>,
}

/// IOP verifier for a particular constraint system.
///
/// This struct encapsulates the constraint system, providing the core verification logic
/// independent of the specific IOP compilation strategy. Most users should use [`Verifier`]
/// instead, which wraps this with a BaseFold compiler.
#[derive(Debug, Clone)]
pub struct IOPVerifier<F: Field> {
	constraint_system: ConstraintSystemPadded<F>,
}

/// Struct for verifying instances of a particular constraint system.
///
/// The [`Self::setup`] constructor determines public parameters for proving instances of the given
/// constraint system. Then [`Self::verify`] is called one or more times with individual instances.
#[derive(Clone)]
pub struct Verifier<F, H>
where
	F: BinaryField,
	H: HashSuite,
{
	iop_verifier: IOPVerifier<F>,
	/// BaseFold ZK compiler for creating verifier channels.
	basefold_compiler: BaseFoldVerifierCompiler<F>,
	/// The verifier creates its Merkle transcript channels with the hash suite `H`.
	_hash_marker: PhantomData<H>,
}

impl<F: Field> IOPVerifier<F> {
	/// Constructs an IOP verifier for a constraint system.
	pub const fn new(constraint_system: ConstraintSystemPadded<F>) -> Self {
		Self { constraint_system }
	}

	pub const fn constraint_system(&self) -> &ConstraintSystemPadded<F> {
		&self.constraint_system
	}

	/// Returns the oracle specs for the IOP channel.
	///
	/// These describe the oracles (witness and mask) that the prover commits to.
	///
	/// The specs are derived by replaying the oracle-receiving sequence against an
	/// [`OracleSetupChannel`] (which records each `recv_oracle` without doing real verification),
	/// rather than hardcoding it. IronSpartan proofs are always zero-knowledge. The precommit
	/// oracle is received by the outer [`Verifier::verify`] before it delegates to
	/// [`Self::verify`], so it is recorded here first to match that order.
	pub fn oracle_specs(&self) -> Vec<OracleSpec>
	where
		F: BinaryField,
	{
		let cs = &self.constraint_system;
		let mut channel = OracleSetupChannel::new(true);
		// Record the precommit oracle first (`OracleSetupChannel` implements the channel trait for
		// every `F`, so the trait is named explicitly to fix `F`); the `verify` call below fixes it
		// for the rest of the sequence.
		<OracleSetupChannel as IOPVerifierChannel<F>>::recv_oracle(
			&mut channel,
			cs.log_precommit() as usize,
			true,
		)
		.expect("OracleSetupChannel::recv_oracle is infallible");
		let public = vec![DummyElem::<F>::default(); 1 << cs.log_public()];
		// Discarded: the setup channel performs no real verification; we only read back the
		// recorded oracle specs.
		let _ = self.verify((), &public, &mut channel);
		channel.into_oracle_specs()
	}

	/// Verifies a proof using an IOP channel.
	///
	/// This is the core verification logic, independent of the specific IOP compilation strategy.
	/// For most users, [`Verifier::verify`] is the simpler interface.
	///
	/// # Arguments
	///
	/// * `precommit_oracle` - Handle to the precommit oracle, received from the channel by the
	///   caller before invoking `verify`.
	/// * `public` - The public inputs to the constraint system
	/// * `channel` - The IOP verifier channel
	///
	/// # Returns
	///
	/// `Ok(())` if the proof is valid, `Err(_)` otherwise.
	pub fn verify<Channel>(
		&self,
		precommit_oracle: Channel::Oracle,
		public: &[Channel::Elem],
		channel: &mut Channel,
	) -> Result<(), Error>
	where
		F: BinaryField,
		Channel: IOPVerifierChannel<F>,
	{
		let cs = &self.constraint_system;

		// Check that the public input length is correct
		if public.len() != 1 << cs.log_public() {
			return Err(Error::IncorrectPublicInputLength {
				expected: 1 << cs.log_public(),
				actual: public.len(),
			});
		}

		// Receive the private and mask oracle commitments.
		// The private witness is witness-dependent.
		// The mask is a fresh random draw, not witness data.
		// It is still flagged witness-dependent so the protocol keeps treating it as secret.
		let private_oracle = channel.recv_oracle(cs.log_private() as usize, true)?;
		let (m_n, m_d) = cs.mask_dims();
		let mask_oracle = channel.recv_oracle(m_n + m_d, true)?;

		// Verify the multiplication constraints.
		let MulcheckOutput {
			a_eval,
			b_eval,
			c_eval,
			mask_eval,
			r_x,
		} = verify_mulcheck(cs, channel)?;

		// λ is the batching challenge for the constraint operands
		let lambda = channel.sample();

		// Batch together the constraint operand evaluation claims.
		let batched_sum = evaluate_univariate(&[a_eval, b_eval, c_eval], &lambda);

		// Compute rₓ^⊤ (M_A + λ M_B + λ² M_C) x. Shared via `Rc` so the transparent closures can
		// own it and outlive this call (the opening is deferred to the channel's `finish()`). `Rc`
		// suffices over `Arc` because the closures (`TransparentEvalFn`, no `Send` bound) and the
		// channel never cross a thread boundary.
		let r_x_tensor: Rc<[Channel::Elem]> = eq_ind_partial_eval_scalars(&r_x).into();

		// The public segment's contribution to the operand evaluations.
		let public_eval =
			wiring::evaluate_wiring_mle_public(cs.mul_constraints(), public, &lambda, &r_x_tensor);

		// Prover sends the precommit segment's contribution to the operand evaluations.
		let precommit_claim = channel.recv_one()?;

		let private_claim = batched_sum - public_eval - precommit_claim.clone();

		// Build one transparent closure per oracle relation.
		// The two wiring closures share the multiplication constraints through a single `Rc`.
		// They own this handle and are `'static`, outliving this call for the deferred opening.
		let mul_constraints: Rc<[_]> = cs.mul_constraints().into();
		let precommit_transparent = wiring::eval_transparent(
			mul_constraints.clone(),
			WitnessSegment::Precommit,
			r_x_tensor.clone(),
			lambda.clone(),
		);
		let private_transparent =
			wiring::eval_transparent(mul_constraints, WitnessSegment::Private, r_x_tensor, lambda);
		let mask_transparent = mask_transparent(cs, &r_x);

		// Verify all oracle relations
		channel.verify_oracle_relation(precommit_oracle, precommit_transparent, precommit_claim)?;
		channel.verify_oracle_relation(private_oracle, private_transparent, private_claim)?;
		channel.verify_oracle_relation(mask_oracle, mask_transparent, mask_eval)?;

		Ok(())
	}
}

impl<F, H> Verifier<F, H>
where
	F: BinaryField,
	H: HashSuite,
	Output<H::LeafHash>: DeserializeBytes,
{
	/// Constructs a verifier for a constraint system.
	///
	/// See [`Verifier`] struct documentation for details.
	pub fn setup(
		constraint_system: ConstraintSystem<F>,
		log_inv_rate: usize,
	) -> Result<Self, Error> {
		// Modify the constraint system for zero-knowledge.
		let n_test_queries = fri::calculate_n_test_queries(SECURITY_BITS, log_inv_rate);
		let blinding_info = BlindingInfo::for_fri_queries(n_test_queries);
		let constraint_system = ConstraintSystemPadded::new(constraint_system, blinding_info);

		let iop_verifier = IOPVerifier::new(constraint_system);
		let oracle_specs = iop_verifier.oracle_specs();

		let merkle_scheme = BinaryMerkleTreeScheme::<F, H>::new();

		// Create the BaseFold ZK compiler for IOP verification
		let basefold_compiler = BaseFoldVerifierCompiler::new(
			&merkle_scheme,
			oracle_specs,
			log_inv_rate,
			n_test_queries,
			&MinProofSizeStrategy,
		);

		Ok(Self {
			iop_verifier,
			basefold_compiler,
			_hash_marker: PhantomData,
		})
	}

	/// Returns a reference to the IOP verifier.
	pub const fn iop_verifier(&self) -> &IOPVerifier<F> {
		&self.iop_verifier
	}

	pub const fn constraint_system(&self) -> &ConstraintSystemPadded<F> {
		self.iop_verifier.constraint_system()
	}

	/// Returns a reference to the BaseFold ZK verifier compiler.
	pub const fn iop_compiler(&self) -> &BaseFoldVerifierCompiler<F> {
		&self.basefold_compiler
	}

	/// Verifies a proof against the constraint system.
	///
	/// # Arguments
	///
	/// * `public` - The public inputs to the constraint system
	/// * `transcript` - The verifier transcript for Fiat-Shamir
	///
	/// # Preconditions
	///
	/// * The public input length must match the constraint system's public input size
	pub fn verify<Challenger_: Challenger>(
		&self,
		public: &[F],
		transcript: &mut VerifierTranscript<Challenger_>,
	) -> Result<(), Error> {
		// Verifier observes the public input (includes it in Fiat-Shamir).
		transcript.observe().write_slice(public);

		// Create channel, receive the precommit oracle, and delegate to IOPVerifier::verify. The
		// IOP verifier only queues the oracle relations; `finish` runs the single combined opening.
		let mut channel = self
			.basefold_compiler
			.create_channel_from_transcript::<H, Challenger_, _>(transcript);
		let precommit_oracle =
			channel.recv_oracle(self.constraint_system().log_precommit() as usize, true)?;
		self.iop_verifier
			.verify(precommit_oracle, public, &mut channel)?;
		channel.finish()?;
		Ok(())
	}
}

fn verify_mulcheck<F, C>(
	cs: &ConstraintSystemPadded<F>,
	channel: &mut C,
) -> Result<MulcheckOutput<C::Elem>, Error>
where
	F: BinaryField,
	C: IPVerifierChannel<F>,
{
	let log_mul_constraints = checked_log_2(cs.mul_constraints().len());

	// Sample random evaluation point
	let r_mulcheck = channel.sample_many(log_mul_constraints);

	// Verify the zerocheck for the multiplication constraints.
	let mlecheck::VerifyZKOutput {
		eval,
		mask_eval,
		challenges: mut r_x,
	} = mlecheck::verify_zk(&r_mulcheck, 2, C::Elem::zero(), channel)?;

	// Reverse because sumcheck binds high-to-low variable indices.
	r_x.reverse();

	// Read the claimed evaluations
	let [a_eval, b_eval, c_eval] = channel.recv_array()?;

	channel.assert_zero(a_eval.clone() * b_eval.clone() - c_eval.clone() - eval)?;

	Ok(MulcheckOutput {
		a_eval,
		b_eval,
		c_eval,
		mask_eval,
		r_x,
	})
}

/// Returns a closure that evaluates the mask transparent polynomial at a given point.
fn mask_transparent<F: Field, E: FieldOps + 'static>(
	cs: &ConstraintSystemPadded<F>,
	r_x: &[E],
) -> binius_iop::channel::TransparentEvalFn<E> {
	let (_m_n, m_d) = cs.mask_dims();
	let n_vars = r_x.len();
	let mask_degree = 2; // quadratic composition
	let r_x = r_x.to_vec();

	Box::new(move |point: &[E]| {
		// Split into query_k (low-order bits) and query_j (high-order bits).
		let (query_k, query_j) = point.split_at(m_d);

		mlecheck::libra_eval(&r_x, query_j, query_k, n_vars, mask_degree)
	})
}

#[derive(Debug, thiserror::Error)]
pub enum Error {
	#[error("FRI error: {0}")]
	FRI(#[from] fri::Error),
	#[error("Sumcheck error: {0}")]
	Sumcheck(#[from] sumcheck::Error),
	#[error("BaseFold error: {0}")]
	BaseFold(#[from] basefold::Error),
	#[error("Transcript error: {0}")]
	Transcript(#[from] binius_transcript::Error),
	#[error("IOP channel error: {0}")]
	IOPChannel(#[from] binius_iop::channel::Error),
	#[error("IP channel error: {0}")]
	IPChannel(#[from] binius_ip::channel::Error),
	#[error("incorrect public inputs length: expected {expected}, got {actual}")]
	IncorrectPublicInputLength { expected: usize, actual: usize },
	#[error("incorrect reduction output of the multiplication check")]
	IncorrectMulCheckEvaluation,
}