The Reductions

In this section, we describe Binius's cryptographic reductions. These reductions are designed to simplify and process mathematical claims—about the vanishing of polynomials, or the equality of multisets, for example—and to reduce them to simpler ones. Ultimately, we want to reduce everything to evaluation claims, amenable to treatment at the hands of our polynomial commitment scheme.

Thus, our cryptographic reductions represent a sort of "conveyor belt" or "middleware", that sits between our frontend and our polynomial commitment scheme. They occupy a critical intermediate territory in Binius, and represent a significant source of cryptographic and engineering complexity.

In prime-field SNARKs based on the DEEP-ALI paradigm—like Plonky3 and Stwo—the need for reductions like ours doesn't quite exist. Those schemes essentially support just tables, and not channels; most importantly, they don't support virtual polynomials.

In Binius, we must enrich this model, for various reasons. First, we rely heavily on virtual polynomials, polynomials which "sit on top of"—and modify—underlying committed polynomials. Virtual polynomials may be compositions or concatenations, say, of raw polynomials; they may also modify their underlying polynomials in more-complex ways—by shifting or packing them, for example.

Secondly, our frontend uses the M3 paradigm. If we just had tables—like the AIR and PLONKish arithmetizations schemes do—then we would just need a zerocheck protocol. As it stands, however, we have channel-balancing too to deal with, and must devise a way to check the equality of multisets. (These multisets are themselves often heavily virtual, as we've noted already.)

Putting these facts together, we see that Binius needs a much-richer landscape of intermediate cryptographic reductions than other SNARKs do. We explain these thoroughly throughout the following subsections.

Section Directory

This section contains the following subsections:

• Background. Here, we explain prior works, and how ours differs from them.
• Virtual polynomials. Binius makes extensive use of virtual polynomials, polynomials which depend algebraically on committed polynomials. Departing from previous works, we allow even virtual polynomials whose evaluation schemes are interactive, in that they reduce to their underlying polynomials' evaluation schemes only with the aid of an interactive protocol (e.g., a sumcheck). This notion proves critical in Binius, as we explain in that page.
• Zerocheck. The zerocheck protocol is designed to process vanishing claims, like those associated with table constraints in M3. This step intakes a zerocheck claim—that is, a claim whereby a certain composition of multilinears vanishes identically over the cube—and reduces that claim to a set of evaluation claims, themselves pertaining to the various polynomials (both raw and virtual) underlying the initial composition. In this setting, we use sophisticated techniques tailored to the case of small-field polynomials.
• Multiset check. Here, we discuss how to process multiset equality claims, a key sort of claim associated with the balancing of channels.
• GKR-based grand product. Grand-product claims pertain to the products of the respective values taken by polynomials over the cube. These arise as internal reduction targets of our multiset protocol.
• Evalcheck. Our evalcheck protocol is designed to replace evaluation claims on virtual multilinears by evaluation claims on concrete ones.