binius_core/protocols/gkr_int_mul/generator_exponent/
verify.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
// Copyright 2024-2025 Irreducible Inc.

use std::array;

use binius_field::{ExtensionField, TowerField};
use binius_utils::bail;

use super::{
	super::error::Error, common::GeneratorExponentReductionOutput, utils::first_layer_inverse,
};
use crate::{
	fiat_shamir::CanSample,
	polynomial::MultivariatePoly,
	protocols::{
		gkr_gpa::LayerClaim,
		gkr_int_mul::generator_exponent::compositions::MultiplyOrDont,
		sumcheck::{self, zerocheck::ExtraProduct, CompositeSumClaim, SumcheckClaim},
	},
	transcript::CanRead,
	transparent::eq_ind::EqIndPartialEval,
};

/// This is the verification side of the following interactive protocol
/// Consider the multilinears a_0, a_1, ..., a_63 (here EXPONENT_BIT_WIDTH = 64)
/// At each point on the hypercube, we construct the 64-bit integer a(X) as
/// a(X) = 2^0 * a_0(X) + 2^1 * a_1(X) + 2^2 * a_2(X) ... + 2^63 * a_63(X)
///
/// The multilinear n has values at each point on the hypercube such that
///
/// g^a(X) = n(X) for all X on the hypercube
///
/// This interactive protocol reduces a claimed evaluation of n to claimed evaluations of
/// the a_i's
///
/// Input: One evaluation claim on n
///
/// Output: EXPONENT_BITS_WIDTH separate claims (at different points) on each of the a_i's
pub fn verify<FGenerator, F, Transcript, const EXPONENT_BIT_WIDTH: usize>(
	claim: &LayerClaim<F>,
	mut transcript: Transcript,
	log_size: usize,
) -> Result<GeneratorExponentReductionOutput<F, EXPONENT_BIT_WIDTH>, Error>
where
	FGenerator: TowerField,
	F: TowerField + ExtensionField<FGenerator>,
	Transcript: CanSample<F> + CanRead,
{
	let mut eval_claims_on_bit_columns: [_; EXPONENT_BIT_WIDTH] =
		array::from_fn(|_| LayerClaim::<F>::default());

	let mut eval_point = claim.eval_point.clone();
	let mut eval = claim.eval;
	for exponent_bit_number in (1..EXPONENT_BIT_WIDTH).rev() {
		let generator_power_constant =
			F::from(FGenerator::MULTIPLICATIVE_GENERATOR.pow([1 << exponent_bit_number]));

		let this_round_sumcheck_claim = SumcheckClaim::new(
			log_size,
			3,
			vec![CompositeSumClaim {
				composition: ExtraProduct {
					inner: MultiplyOrDont {
						generator_power_constant,
					},
				},
				sum: eval,
			}],
		)?;

		let sumcheck_verification_output =
			sumcheck::batch_verify(&[this_round_sumcheck_claim], &mut transcript)?;

		// Verify claims on transparent polynomials

		let sumcheck_query_point = sumcheck_verification_output.challenges;

		let eq_eval =
			EqIndPartialEval::new(log_size, sumcheck_query_point.clone())?.evaluate(&eval_point)?;

		if sumcheck_verification_output.multilinear_evals[0][2] != eq_eval {
			bail!(Error::EqEvalDoesntVerify)
		}

		eval_claims_on_bit_columns[exponent_bit_number] = LayerClaim {
			eval_point: sumcheck_query_point.clone(),
			eval: sumcheck_verification_output.multilinear_evals[0][1],
		};

		eval_point = sumcheck_query_point;
		eval = sumcheck_verification_output.multilinear_evals[0][0];
	}

	eval_claims_on_bit_columns[0] = LayerClaim {
		eval_point,
		eval: first_layer_inverse::<FGenerator, _>(eval),
	};

	Ok(GeneratorExponentReductionOutput {
		eval_claims_on_exponent_bit_columns: eval_claims_on_bit_columns,
	})
}