Evalcheck

Unrolling evaluation claims on virtual multilinears

Throughout the reductions site section so far, our task has been to reduce complex mathematical claims to evaluation claims. At this point, we've attained this goal: our only remaining claims are evaluation claims on multilinears.

However, one catch remains: the multilinears which these claims pertain to are, in general, virtual. Almost by definition, virtual polynomials cannot be evaluated directly; rather, they must be "unwound": in order to process an evaluation claim on a virtual multilinear, the verifier must perform some further steps. These steps will entail some mix of succinct local computation, interaction with the prover, and so on; the end result will be a further evaluation claim, this time on the polynomial or polynomials that underlie the virtual polynomial.

In certain cases, the ensuing claims will be on further polynomials that are themselves virtual; in this case, the process must be repeated.

The Polynomial DAG

As we hinted in this section's background page, Binius has a unique feature absent in prior SNARKs: instance-dependent control flow. In classical SNARKs, as the instance (i.e., problem description) varies, only basic parameters—like trace length and number of constraints (as well as of course the coefficients of these constraints)—vary; the basic sequence of steps does not. In our case, on the other hand, Binius's control flow (for both the prover and the verifier) is variable and instance-dependent.

Why? Basically, because we heavily use virtual polynomials. These polynomials are allowed to depend on other polynomials, which may themselves be virtual, and so on. In practice, we get a DAG (directed acyclic graph) of polynomials, in which each polynomial points to those upon which it depends. The terminal (or "sink") nodes in this DAG are the committed and transparent polynomials. We thus need a way for the prover and verifier to traverse this DAG "dynamically"—i.e., in a way which is sensitive to the instance at hand.

Evalcheck

In Binius, evalcheck is a generic name we've given to the problem of reducing evaluation claims on possibly virtual multilinears to evaluation claims on committed multilinears. The input to the evalcheck phase consists of a list of evaluation claims—each specifying a (generally virtual) multilinear, an evaluation point, and a claimed value. The ultimate output will be a further list of claims, now all pertaining strictly to committed multilinears.

Evalcheck works by progressively consuming evaluation claims on virtual things, and outputting claims on committed things. As we've already said, each such reduction will involve some work on the verifier's part, as well as (in general) interaction with the prover.

We've already mentioned the shift polynomial above. As another (more basic) example, let's consider linear combinations. Let's write as usual $t_0, \ldots , t_{\mu - 1}$ for the underlying multilinears and $\alpha_0, \ldots , \alpha_{\mu - 1}$ for the combination scalars; we moreover write $T \coloneqq \alpha_0 \cdot t_0 + \cdots + \alpha_{\mu - 1} \cdot t_{\mu - 1}$ for the virtual linear combination polynomial. To check the evaluation claim $T(r) \stackrel{?}= s$ , the verifer may ask the prover to nondeterministically send the claimed evaluations $s_i = t_i(r)$ , for each $i \in \{0, \ldots , \mu - 1\}$ . The verifier may locally check that $s \stackrel{?}= \sum_{i = 0}^{\mu - 1} \alpha_i \cdot s_i$ . Finally, the verifier will output the reduced claims $s_i = t_i(r)$ .

This follows the typical flow: the verifier will intake a claim about something virtual, do a bit of work, and then output reduced claims on the things underlying the virtual multilinear.

Some of our virtual polynomials require sumchecks, while others don't. The shift polynomial is the most prominent example that does require a sumcheck (that sumcheck is explained in detail in our page on that polynomial). On the other hand, the linear combination polynomial just discussed doesn't require a sumcheck, though it does require that the prover nondeterministically supply a bit of data. The tiling and merge virtual polynomial are similar.

Greedy Evalcheck

In Binius, we solve the evalcheck problem using a particular approach we call greedy evalcheck. We will describe greedy evalcheck from the verifier's point of view, though the prover is analogous.

The verifier's state

Throughout, the verifier maintains some state:

A list of evaluation claims on (generally virtual) multilinears, initialized to the initial claims list fed into evalcheck.
A list of running sumcheck claims, initialized to empty.
A list of output evaluation claims on exclusively committed multilinears, initialized to empty.

The passes

Greedy evalcheck works by processing the evaluation claims in multiple passes. The verifier has two alternate types of pass, which it alternates between.

The traversal pass. In this pass, the verifier does a depth-first traversal of the DAG, using the evaluation claims list (1. above) as "source nodes" or entrypoints. At each node, the verifier does the following thing:

If the node is not sumcheck-inducing, then run all requisite local checks.
- If applicable, then recursively kick off traversals of any of the node's descendants.
- Otherwise, we're in the base case, formed by terminal virtual polynomials.
  - If the node is transparent, the verifier just evaluates it directly and checks the claim.
  - If it's committed, the verifier appends the claim to its running output list (3. above).
Otherwise, i.e. if the node is sumcheck-inducing, then append the relevant sumcheck to the running list of outstanding sumcheck claims (2. above). Instead of traversing further, nip the traversal in the bud at this point, and return.

At the end of this pass, all nodes have been traversed, except the sumcheck-inducing nodes and their descendants. Thus these nodes form a "frontier" which halts the DAG traversal.

The sumcheck pass. In this pass, all outstanding sumchecks (2. above) get batch-verified, and the list of outstanding sumchecks is then cleared. In the process, new evaluation claims will ensue; these are accrued in a new list of evaluation claims, which overwrites and supersedes 1. above.

The algorithm

To run greedy evalcheck, the verifier simply repeatedly alternates between these two types of passes, beginning with a traversal pass on the initial input list of claims. This process is repeated until the verifier completes a traversal pass during which no new sumcheck claims ensue. At this point, the sumcheck pass becomes vacuous, and the procedure terminates. The output is the full list of output claims on committed multilinears (3. above).

Some Remarks

While the greedy evalcheck algorithm just described seems a bit tricky, we offer a heuristic justification. The point is that sumchecks need to be batch-verified; if it weren't for this fact, then a simple single-pass DAG traversal would presumably suffice just fine. As things stand, we have to instead "fence off" the DAG traversal at the sumcheck-inducing nodes—so that we can collect all available sumchecks. That is, we collect as many sumchecks as we're currently prepared to execute—and no more—before verifying them and unrolling further.

We are actively thinking about if there are more sophisticated evalcheck algorithms than the greedy one.