This article details my implementation of Sum-Check done in OCaml, as well as a quick introduction to what the Protocol accomplishes and how it gets used.

It assumes a high-degree of technical understanding.

The full code can be found at the Github repo.

Sum-Check is an Interactive Protocol through which a Prover proves to a Verifier that their evaluation of some multi-variate polynomial g over the hypercube is equal to some value H.

This is one example of Verifiable Computation, where one party does some work, and the other party can trust in the result of that work in Sublinear Time (Time that grows slower than linear, essentially that it's asymptotically cheaper than running the computation themself).

The particular computation that we do in this protocol is summing over the boolean hypercube (That is, adding up g evaluated at each combination of values that the v-variables could be, where each variable is a boolean random variable) which is essentially #SAT (
Sharp SAT, from complexity theory
). Similar to how SAT asks if a given Boolean formula has a satisfying assignment, #SAT asks *how many* satisfying assingments a Boolean formula has.

This is interesting on its own, and gets used to build SNARKs by first using the Fiat-Shamir Heuristic to remove the interactive aspect of the protocol (The Prover sending a random challenge to the Verifier at each round, which gets replaced by the hash of the transcript).

This implementation assumes that the Oracle check is accomplished by some other means, and it hardcodes the formula / field size for convenience.

For more details, including justification for why the results follow from the conditions, see the resources section.

Given a v-variate polynomial g defined over some finite field

Essentially,

The Verifier must check the following in order to be convinced that the given value C is correct (Equal to H):

- That C and the first partial equation agree.

- That each subsequent
is consistent with the last.${g}_{i}$

- That all
are univariate polynomials of degree 1 (or 0).${g}_{i}$ - That evaluating
at the random point$g$ is equal to the last given polynomial.$({r}_{1},...,{r}_{v})$

A propositional formula is supplied (As well as a field size). The formula is arithmetized. The sumcheck protocol then runs to completion (Or until it fails because any of the above checks failed).

For each round

The Verifier checks that they agree (

The Verifier chooses a random value

The Prover constrains the polynomial with that value.

Unless this is the last round, another round begins with the following changes:

- round = round + 1
is added to the list of random numbers${r}_{i}$ $({r}_{1},...,{r}_{i})$ - The working polynomial now has
in place of${r}_{i}$ ${x}_{i}$

If this is the last round, the Verifier checks that

If that passes, then the Verifier is convinced that

Share this article: