The Backend

This site area contains the full mathematical specification of Binius64. Our section on the shift indicators contains key mathematical ideas that will get used throughout. Our sections on the AND and MUL reductions essentially operate independently of each other, though both depend on the shift indicators. Both of those reductions target the shift reduction, which can be thought of as a common internal subroutine, the "workhorse" of Binius64. That reduction in turn outputs an evaluation claim, directly amenable to our PCS.

Throughout the entirety of this site area, we assume that the prover has begun by committing his prover data $w$ using our PCS.

Here, we break down in more detail this area's sections.

• The Shift Indicators. Binius64 natively enshrines shifted value indices into its constraint system. In order to assess the validity of prover claims that involve shifted data, we need to make shifts mathematical. In this site section, we mathematically relate the multilinear extension of shifted data to the multilinear extension of the original data. Our treatment of this problem builds on Diamond and Posen [DP25, § 4.3].
• The AND Reduction. To assess whether the constraint system's AND constraints hold over the prover's shifted witness data, we recast that question as one about the vanishing of a multivariate polynomial over $\mathbb{F}_2$. To assess that vanishing problem, we in turn use an advanced adaptation of Gruen's [Gru24, § 5.1] univariate skip protocol, which also uses ideas of Dao and Thaler [DT24a, DT24b]. Our implementation of our prover works "when possible" in the 8-bit Rijndael field; we call it the Rijndael zerocheck.
• The MUL Reduction. To assess whether our prover's MUL constraints hold, we need a way of obtaining unsigned 64-bit integer multiplication within the context of binary fields. Interestingly, we achieve multiplication by replacing it something apparently harder, exponentiation. We first note that repeated exponentiation of a fixed field element gives us multiplication "in the exponent"; our next task is to handle exponentiation, which we achieve using a GKR-like idea.
• The Shift Reduction. The shift reduction is a key internal step in Binius64. That reduction picks up where both the AND and MUL reductions leave off, namely with evaluation claims on certain oblong-multilinearizations of polynomials that depend on the prover's data. To assess those evaluation claims, we first must relate those oblong-multilinears to the prover's witness, a task during whose execution we put our shift indicators to full use. We next undertake a complex, two-stage sumcheck, which roughly evokes Spartan [Set20]'s, and describe how our prover carries out that sumcheck efficiently.
• Public Input Check. Here, we finally handle the means by which the verifier might check that the public portion of the prover's data takes on the values that it should.