The Sum-check Protocol #

We define the sum-check protocol as a series of Interactive Oracle Reductions (IORs), where the underlying polynomials are represented using Mathlib's noncomputable types Polynomial and MvPolynomial. See SingleRound.lean for a single round of the protocol, and the definition of the sum-check relations.

In the future, we will have files that deal with implementations of the protocol, and we will prove that those implementations derive security from that of the abstract protocol.

Protocol Specification #

The sum-check protocol is parameterized by the following:

R: the underlying ring (for soundness, required to be finite and a domain)
n + 1 : ℕ+: the number of variables (also number of rounds)
deg : ℕ: the individual degree bound for the polynomial
D : Fin m ↪ R: the set of m evaluation points for each variable (for some m), represented as an injection Fin m ↪ R. The image of D as a finite subset of R is written as Finset.univ.map D.
oSpec : OracleSpec ι: the set of underlying oracles (e.g. random oracles) that may be needed for other reductions. However, the sum-check protocol does not use any oracles.

The sum-check relation has no witness. The statement for the i-th round, where i : Fin (n + 2), contains:

target : R, which is the target value for sum-check
challenges : Fin i → R, which is the list of challenges sent from the verifier to the prover in previous rounds

There is a single oracle statement, which is:

poly : MvPolynomial (Fin (n + 2)) R, the multivariate polynomial that is summed over

The sum-check relation for the i-th round checks that:

∑ x ∈ (univ.map D) ^ᶠ (n + 1 - i), poly ⸨challenges, x⸩ = target.

Note that the last statement (when i = n) is the output statement of the sum-check protocol.

For i = 0, ..., n, the i-th round of the sum-check protocol consists of the following:

The prover sends a univariate polynomial pᵢ ∈ R⦃≤ deg⦄[X] of degree at most deg. If the prover is honest, then we have:

pᵢ(X) = ∑ x ∈ (univ.map D) ^ᶠ (n - i), poly ⸨X ⦃i⦄, challenges, x⸩.

Here, poly ⸨X ⦃i⦄, challenges, x⸩ is the polynomial poly evaluated at the concatenation of the prior challenges challenges, the i-th variable as the new indeterminate X, and the rest of the values x ∈ (univ.map D) ^ᶠ (n - i).

In the oracle protocol, this polynomial pᵢ is turned into an oracle for which the verifier can query for evaluations at arbitrary points.

The verifier then sends the i-th challenge rᵢ sampled uniformly at random from R.
The (oracle) verifier then performs queries for the evaluations of pᵢ at all points in (univ.map D), and checks that: ∑ x in (univ.map D), pᵢ.eval x = target.

If the check fails, then the verifier outputs failure.

Otherwise, it outputs a statement for the next round as follows:
- target is updated to pᵢ.eval rᵢ
- challenges is updated to the concatenation of the previous challenges and rᵢ

Notes & TODOs #

An annoying issue is that we need to index over i : Fin (n + 2), not i : Fin (n + 1). This is because existing Fin functions works better with n + 1 which is clearly positive, and not i : Fin (n + 1) (which would imply n > 0, but this fact is not apparent).

Note that to represent sum-check as a series of IORs, we will need to implicitly constrain the degree of the polynomials via using subtypes, such as Polynomial.degreeLE and MvPolynomial.degreeOf. This is because the oracle verifier only gets oracle access to evaluating the polynomials, but does not see the polynomials in the clear.

When this is compiled to an interactive proof, the corresponding polynomial commitment schemes will enforce that the declared degree bound holds, via letting the (non-oracle) verifier perform explicit degree checks.

There are some generalizations that we could consider later:

Generalize to degs : Fin (n + 2) → ℕ and domain : Fin (n + 2) → (Fin m ↪ R), e.g. can vary the degree bound and the summation domain for each variable
Generalize the challenges to come from a suitable subset of R (e.g. subtractive sets), and not necessarily the whole domain. This is used in lattice-based protocols.
Sumcheck over modules instead of just rings. This will require extending MvPolynomial to have such a notion of evaluation, something like evalModule (x : σ → M) (p : MvPolynomial σ R) : M, where we have [Module R M].