The sumcheck protocol with a final evaluation check

The index is a polynomial P in n variables over a finite field F with every individual degree at most d. A claim (r, c) at round i consists of the challenges r : Fin i → F of the earlier rounds and a value c. It states that the sum of P over the Boolean hypercube in the coordinates i, …, n - 1, with the coordinates below i fixed to r, is c (Sumcheck.rel P i). At round 0 this is the sumcheck claim ∑_{b ∈ {0,1}ⁿ} P b = c, and at round n it is the evaluation claim P r = c.

This is the protocol of Lund, Fortnow, Karloff and Nisan [LFKN92] as a composition of one-round reductions, with each challenge uniform on the field. Each round needs i < n: past the last variable the honest round polynomial is constant, and the round is neither complete nor round-by-round sound. The TQBF protocol in Complexity.Computability.Complexity.Classes.IP.TQBF.Protocol is a separate, unchanged development.

Main definitions

• Sumcheck.Claim F i: the claims of round i, a point of F^i and a value.
• Sumcheck.partialSum P r: the sum of P over the Boolean hypercube in the coordinates from i on, with the coordinates below i fixed to r : Fin i → F.
• Sumcheck.round d P i reduces rel P i to rel P (i + 1) in one prover message (a univariate polynomial) and one uniform challenge z, and appends z to the point.
• Sumcheck.finalCheck P reduces rel P n to acceptance by evaluating P without interaction.
• Sumcheck.proof d P is round 0, …, round (n - 1), by Reduction.iterate, followed by finalCheck.

Main results

• Sumcheck.round_complete, Sumcheck.round_rbrSound: each round is perfectly complete and round-by-round sound with error d / |F|.
• Sumcheck.finalCheck_complete, Sumcheck.finalCheck_rbrSound: the final check is perfectly complete and round-by-round sound without error.
• Sumcheck.proof_complete, Sumcheck.proof_sound: the end-to-end theorems, corollaries of the component theorems through the composition theorems. The soundness error n * (d / |F|) is the sum of the per-round errors, and no step of the composed protocol is reasoned about directly.

References

• C. Lund, L. Fortnow, H. Karloff, N. Nisan, Algebraic methods for interactive proof systems

@[reducible, inline]

abbrev Cslib.Interactive.Sumcheck.Claim (F : Type) (i : ℕ) : Type

A claim of round i: the challenges of the rounds before i and the claimed value.

def Cslib.Interactive.Sumcheck.point {F : Type} [Field F] {n i : ℕ} (r : Fin i → F) (b : Fin (n - i) → Bool) : Fin n → F

The point of F^n equal to r on the first i coordinates and to the Boolean point b on the others.

noncomputable def Cslib.Interactive.Sumcheck.partialSum {F : Type} [Field F] {n : ℕ} (P : MvPolynomial (Fin n) F) {i : ℕ} (r : Fin i → F) : F

The sum of P over the Boolean hypercube in the coordinates from i on, with the coordinates below i fixed to r.

def Cslib.Interactive.Sumcheck.rel {F : Type} [Field F] {n : ℕ} (P : MvPolynomial (Fin n) F) (i : ℕ) : Claim F i → Unit → Prop

The relation of round i: the claimed value is the partial sum. There is no witness.

noncomputable def Cslib.Interactive.Sumcheck.roundPoly {F : Type} [Field F] {n : ℕ} (P : MvPolynomial (Fin n) F) {i : ℕ} (r : Fin i → F) : Polynomial F

The honest message of round i: the partial sum as a polynomial in coordinate i.

@[reducible, inline]

abbrev Cslib.Interactive.Sumcheck.roundSpec (F : Type) [Semiring F] : Spec

One round: the prover sends a polynomial, read in full; the verifier sends a field element.

@[reducible, inline]

abbrev Cslib.Interactive.Sumcheck.accepts {F : Type} [Field F] (d : ℕ) (c : F) (g : Polynomial F) : Prop

The verifier's test of a round polynomial g against the claimed value c.

noncomputable def Cslib.Interactive.Sumcheck.round {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) (P : MvPolynomial (Fin n) F) (i : ℕ) : Reduction OracleSpec.empty OracleSpec.empty (roundSpec F) (Claim F i) Unit (Claim F (i + 1)) Unit

Round i of sumcheck: on the claim (r, c) and the challenge z, the new claim is (Fin.snoc r z, g.eval z) for the prover's polynomial g.

noncomputable def Cslib.Interactive.Sumcheck.finalCheck {F : Type} [Field F] [DecidableEq F] {n : ℕ} (P : MvPolynomial (Fin n) F) : Reduction OracleSpec.empty OracleSpec.empty [] (Claim F n) Unit Unit Unit

The final check: evaluate P at the claimed point, without interaction.

noncomputable def Cslib.Interactive.Sumcheck.proof {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) (P : MvPolynomial (Fin n) F) : Reduction OracleSpec.empty OracleSpec.empty (iterSpec (fun (x : ℕ) => roundSpec F) n ++ []) (Claim F 0) Unit Unit Unit

Sumcheck followed by the final check: a proof system for the claim ∑_{b ∈ {0,1}ⁿ} P b = c (rel P 0).

The round polynomial

theorem Cslib.Interactive.Sumcheck.partialSum_self {F : Type} [Field F] {n : ℕ} (P : MvPolynomial (Fin n) F) (r : Fin n → F) : partialSum P r = (MvPolynomial.eval r) P

At round n all coordinates are fixed: the partial sum is the evaluation.

Component theorems (milestone 2)

theorem Cslib.Interactive.Sumcheck.round_complete {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) (P : MvPolynomial (Fin n) F) (hP : ∀ (j : Fin n), MvPolynomial.degreeOf j P ≤ d) {i : ℕ} (hi : i < n) : Reduction.Complete World.plain (round d P i) (rel P i) (rel P (i + 1)) 0

Each round is perfectly complete.

theorem Cslib.Interactive.Sumcheck.round_rbrSound {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) (P : MvPolynomial (Fin n) F) (hP : ∀ (j : Fin n), MvPolynomial.degreeOf j P ≤ d) {i : ℕ} (hi : i < n) : (round d P i).verifier.RbrSound (language (rel P i)) (language (rel P (i + 1))) (↑d / ↑(Fintype.card F), ())

Each round is round-by-round sound with error d / |F| (Schwartz–Zippel for one variable).

theorem Cslib.Interactive.Sumcheck.finalCheck_complete {F : Type} [Field F] [DecidableEq F] {n : ℕ} (P : MvPolynomial (Fin n) F) : Reduction.Complete World.plain (finalCheck P) (rel P n) Accept 0

The final check is perfectly complete.

theorem Cslib.Interactive.Sumcheck.finalCheck_rbrSound {F : Type} [Field F] [DecidableEq F] {n : ℕ} (P : MvPolynomial (Fin n) F) : (finalCheck P).verifier.RbrSound (language (rel P n)) Set.univ ()

The final check is round-by-round sound without error.

End-to-end theorems, by composition

theorem Cslib.Interactive.Sumcheck.proof_complete {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) (P : MvPolynomial (Fin n) F) (hP : ∀ (j : Fin n), MvPolynomial.degreeOf j P ≤ d) : Reduction.Complete World.plain (proof d P) (rel P 0) Accept 0

Completeness of sumcheck with the final check.

theorem Cslib.Interactive.Sumcheck.proof_sound {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (d : ℕ) (P : MvPolynomial (Fin n) F) (hP : ∀ (j : Fin n), MvPolynomial.degreeOf j P ≤ d) : Verifier.Sound World.plain (proof d P).verifier (language (rel P 0)) Set.univ (↑n * (↑d / ↑(Fintype.card F)))

Soundness of sumcheck with the final check: a false claim is accepted with probability at most n * (d / |F|).