Skip to main content

new

pub fn new<'alloc, A, F, P>(
    alloc: &'alloc A,
    multilinears: [FieldVec<P, A>; 2],
    eval_point: Vec<F>,
    eval_claim: F,
) -> impl MleCheckProver<F> + 'alloc
where A: Allocator, F: Field, P: PackedField<Scalar = F>,
Expand description

Creates an MleCheckProver that reduces an evaluation claim on a multilinear extension of the product of two multilinears to evaluation claims on said multilinears.

§Mathematical Definition

  • $n \in N$ - number of variables in multilinear polynomials
  • $A, B \in F[x], x = (x_1, \ldots, x_n)$ - multilinears being multiplied
  • $(\widetilde{AB})[x] = y$ - evaluation claim on the product MLE

The claim is equivalent to $P(x) = \sum_{v \in B} \widetilde{eq}(v, x) A(v) B(v) = y$, and the reduction can be achieved by sumchecking the latter degree-3 composition. The paper Gruen24, however, describes a way to partition the $\widetilde{eq}(v, x)$ into three parts in round $j \in 1, \ldots, n$ during specialization of variable $v_{n-j+1}$, with $j-1$ challenges $\alpha_i$ already sampled:

$$ \widetilde{eq}(x_{n-j+2}, \ldots, x_n; \alpha_{j-1}, \ldots, \alpha_{1}) \tag{1} $$ $$ \widetilde{eq}(x_{n-j+1}; v_{n-j+1}) \tag{2} $$ $$ \widetilde{eq}(x_1, \ldots, x_{n-j}; v_1, \ldots, v_{n-j}) \tag{3} $$

The following holds:

  • (1) is a constant that can be incrementally updated in O(1) time,
  • (2) is a linear polynomial that is easy to compute in monomial form specialized to either variable
  • (3) is a an equality indicator over the claim point suffix

These observations allow us to instead sumcheck: $$ P’(x) = \sum_{v \in B} \widetilde{eq}(x_1, \ldots, x_{n-j}; v_1, \ldots, v_{n-j}) A(v) B(v) $$

Which is simpler because:

  • $P’(x)$ is degree-2 in $j$-th variable, requiring one less evaluation point
  • Equality indicator expansion does not depend on $j$-th variable and thus doesn’t need to be interpolated

After computing the round polynomial for $P’(x)$ in monomial form, one can simply multiply by (2) and (1) in polynomial form. For more details, see the equality trackers and Gruen24 Section 3.2.

Note 1: as evident from the definition, this prover binds variables in high-to-low index order.

Note 2: evaluation points are 0 (implicit), 1 and Karatsuba infinity.