Background

In classical, DEEP-ALI-based SNARKs like Plonky3 and Stwo, all instances more-or-less have the same shape. We need to pick a field. We need to fix a trace width and a maximal trace height. Finally, we need to write down our AIR instance, which more-or-less looks like crafting a bunch of constraint polynomials (fixed once and for all). This is the extent of the instance-specific parameters which the parties must write down. On a per-statement basis, the prover's job basically looks like filling in a big trace table, and then cranking the handle.

This means that even across AIR instances, the provers' and verifiers' respective jobs more-or-less continue to look the same (they have the same control flow). As instances differ, the only thing that changes is the trace shape, as well as the quantity of and the definitions of the constraint polynomials. On the other hand, the rough sequence of operations of steps remains fixed.

Binius departs radically from this story. In Binius, as we look across various M3 instances, all manner of things vary. For one, our table and flushing rules both vary, so as to incorporate instance-specific virtual columns (in general). These virtual columns may depend in arbitrarily complex ways—i.e., as the instance demands—on their committed counterparts, and even on each other. In general, we get a DAG (directed acyclic graph) of virtual polynomials, where each edge links some "outer polynomial" to an "inner polynomial" it depends on (terminating with committed or transparent polynomials).

In order to evaluate such a virtual polynomial, therefore, we must undergo some sequence of unwinding steps. Moreover, as the instance varies, the shape of this DAG will vary; so too, therefore, will the control flow that the prover and the verifier must go through in order to traverse it. Binius contains complex and subtle logic designed to allow both parties simultaneously and cooperatively to traverse this DAG. Both parties must do so, of course, in a way that is sensitive to the definitions of the various virtual polynomials involved. Since the dependencies between our virtual polynomials often themselves involve sums, sumchecks ensue. Binius must take responsibility for scheduling, orchestrating, and batching all of the resulting sumchecks—in such a manner that the prover and verifier can coordinate.

Constraints and Channels

One further factor makes our prover and verifier algorithms complex and instance-dependent. While the vanishing claims that arise from the constraint-satisfaction of tables are fairly familiar, we moreover have channel-balancing claims to deal with. As we've explained, these latter claims amount to multiset equality checks. In Binius, we thus need to generally evaluate not just vanishing claims but moreover multiset checks.

We explain our zerocheck techniques thoroughly here. In a separate page, we moreover explain our multiset-check. As we explain in that latter page, we resolve multiset equality claims by reducing them to grand-product claims on multilinears that are themselves virtual: these latter multilinears are certain "fingerprinted" combinations (i.e., of the multilinears that make up the tuple being multiset-checked). These latter things, too, are virtual polynomials in the same sense, and are treated as such in Binius.