binius_ip/
fracaddcheck.rs

1// Copyright 2025-2026 The Binius Developers
2
3//! Reduction from fractional-addition layers to a multilinear evaluation claim.
4//!
5//! Each layer represents combining siblings with the fractional-addition rule:
6//! (a0 / b0) + (a1 / b1) = (a0 * b1 + a1 * b0) / (b0 * b1).
7
8use binius_field::{Field, field::FieldOps};
9use binius_math::line::extrapolate_line;
10use binius_transcript::Error as TranscriptError;
11
12use crate::{
13	channel::IPVerifierChannel,
14	sumcheck::{self, BatchSumcheckOutput},
15};
16
17#[derive(Debug, Clone, PartialEq, Eq)]
18pub struct FracAddEvalClaim<F> {
19	/// The evaluation of the numerator and denominator multilinears.
20	pub num_eval: F,
21	pub den_eval: F,
22	/// The evaluation point.
23	pub point: Vec<F>,
24}
25
26pub fn verify<F, C>(
27	k: usize,
28	claim: FracAddEvalClaim<C::Elem>,
29	channel: &mut C,
30) -> Result<FracAddEvalClaim<C::Elem>, Error>
31where
32	F: Field,
33	C: IPVerifierChannel<F>,
34{
35	if k == 0 {
36		return Ok(claim);
37	}
38
39	let FracAddEvalClaim {
40		num_eval,
41		den_eval,
42		point,
43	} = claim;
44
45	let evals = [num_eval, den_eval];
46
47	// Reduce numerator and denominator sum claims to evaluations at a challenge point.
48	let BatchSumcheckOutput {
49		batch_coeff,
50		eval,
51		mut challenges,
52	} = sumcheck::batch_verify_mle(&point, 2, &evals, channel)?;
53
54	// Read evaluations of numerator/denominator halves at the reduced point.
55	let [num_0, num_1, den_0, den_1] = channel.recv_array()?;
56
57	// Sumcheck binds variables high-to-low; reverse to low-to-high for point evaluation.
58	challenges.reverse();
59	let reduced_eval_point = challenges;
60
61	let numerator_eval = num_0.clone() * den_1.clone() + num_1.clone() * den_0.clone();
62	let denominator_eval = den_0.clone() * den_1.clone();
63	let batched_eval = numerator_eval + denominator_eval * batch_coeff;
64
65	channel.assert_zero(batched_eval - eval)?;
66
67	// Reduce evaluations of the two halves to a single evaluation at the next point.
68	let r = channel.sample();
69	let next_num = extrapolate_line(num_0, num_1, r.clone());
70	let next_den = extrapolate_line(den_0, den_1, r.clone());
71
72	let mut next_point = reduced_eval_point;
73	next_point.push(r);
74
75	verify(
76		k - 1,
77		FracAddEvalClaim {
78			num_eval: next_num,
79			den_eval: next_den,
80			point: next_point,
81		},
82		channel,
83	)
84}
85
86/// Pads a leaf fraction — the forward map that the prover's `unpad_leaf_claim` inverts.
87///
88/// Padding a tree scales its numerator by the padding coordinates' equality weight $q$ and sends
89/// its denominator through the one-padding selector $\textsf{sel}(q, v) = 1 + (v - 1) q$. A
90/// verifier that rebuilds a padded batch's leaf claim from transparent parts applies this to each
91/// tree. The inverse direction is the prover's: only it holds claims on padded witnesses to
92/// reduce, so `unpad_leaf_claim` lives in `binius-ip-prover`.
93///
94/// The weight is a parameter rather than the padding coordinates, so a caller padding several
95/// trees computes each distinct one once.
96///
97/// # Arguments
98///
99/// * `fraction` - The unpadded leaf's numerator and denominator.
100/// * `pad_eq` - The padding coordinates' equality weight $\text{eq}(0^\nu; X_\text{pad})$, which is
101///   the all-zeros equality indicator over the lowest coordinates of the leaf point.
102pub fn pad_leaf_fraction<E: FieldOps>(fraction: (E, E), pad_eq: E) -> (E, E) {
103	let (num, den) = fraction;
104	(num * pad_eq.clone(), E::one() + (den - E::one()) * pad_eq)
105}
106
107#[derive(Debug, thiserror::Error)]
108pub enum Error {
109	#[error("sumcheck error: {0}")]
110	Sumcheck(#[source] sumcheck::Error),
111	#[error("transcript error: {0}")]
112	Transcript(#[source] TranscriptError),
113	#[error("verification error: {0}")]
114	Verification(#[from] VerificationError),
115}
116
117impl From<sumcheck::Error> for Error {
118	fn from(err: sumcheck::Error) -> Self {
119		match err {
120			sumcheck::Error::Verification(err) => VerificationError::Sumcheck(err).into(),
121			_ => Error::Sumcheck(err),
122		}
123	}
124}
125
126impl From<TranscriptError> for Error {
127	fn from(err: TranscriptError) -> Self {
128		match err {
129			TranscriptError::NotEnoughBytes => VerificationError::TranscriptIsEmpty.into(),
130			_ => Error::Transcript(err),
131		}
132	}
133}
134
135impl From<crate::channel::Error> for Error {
136	fn from(err: crate::channel::Error) -> Self {
137		match err {
138			crate::channel::Error::ProofEmpty => VerificationError::TranscriptIsEmpty.into(),
139			crate::channel::Error::InvalidAssert => VerificationError::InvalidAssert.into(),
140		}
141	}
142}
143
144#[derive(Debug, thiserror::Error)]
145pub enum VerificationError {
146	#[error("sumcheck: {0}")]
147	Sumcheck(#[from] sumcheck::VerificationError),
148	#[error("incorrect layer fraction sum evaluation: {round}")]
149	IncorrectLayerFractionSumEvaluation { round: usize },
150	#[error("incorrect round evaluation: {round}")]
151	IncorrectRoundEvaluation { round: usize },
152	#[error("transcript is empty")]
153	TranscriptIsEmpty,
154	#[error("invalid assertion: value is not zero")]
155	InvalidAssert,
156}
binius_ip/fracaddcheck.rs

binius_ip/
fracaddcheck.rs
