Constraint Systems

In Binius64, we use a constraint system language that's R1CS-like, but adapts that system to make it work natively with 64-bit unsigned integers. This lets us write down constraint systems that efficiently represent computations that act on machine words.

Our constraint system language enriches R1CS in various ways. First, it operates natively on 64-bit words, as opposed to on "field elements". Further, it has shifts—logical-left, logical-right, and arithmetic-right—natively built in. Finally, instead of supporting the "field multiplication" nonlinearity (which is generally hard to exploit efficiently), we support bitwise AND and unsigned 64-bit multiplication nonlinearities.

We give further details in this site section.

• Introduction. We explain in informal terms how we adopt and enrich R1CS. In short, instead of operating on subset sums of our witness, our constraint system operates on XORS-of-shifts.
• Shifted Value Indices. A shifted value index is basically a datum that specifies that a certain component of the prover's witness should be shifted by a certain amount, in a certain direction. They form a key building block of our constraint system; we explain them here.
• AND Constraints. AND constraints demand that certain 64-bit words derived from the prover's witness be the bitwise AND of other such words. Here, we specify what exactly AND constraints mean in our system, and what it means for them to be fulfilled.
• MUL Constraints. Multiplication constraints demand that certain pairs of 64-bit words derived from the prover's witness, when multiplied as unsigned integers, yield double-width products made up of other witness-derived words. Here, we explain everything.