Overview

Abstract

Binius64 is a simple SNARK designed to efficiently prove statements about 64-bit words. At a very high level, Binius64's power comes from its new constraint system language, which adapts SuperSpartan's [STW23]. We enrich that framework using what we call shifted value indices, data that combine value references with logical and arithmetic shifts. Our design yields constraint systems that are 64-fold smaller than those based on bits alone can deliver; on the other hand, we also fully exploit binary field arithmetic.

Our constraint system acts natively on on 64-bit words. To prove bitwise-AND constraints on these words, we devise an advanced univariate skip variant, building on ideas of Gruen [Gru24, § 5.1] and Hu et al. [Hu+25]. We also support constraints about the products—as unsigned, 64-bit integers—of prover words; to handle these, we use a GKR-based technique. We handle shifts by arithmetizing them, adapting an idea of Diamond and Posen [DP25, § 4.3]. We use the small-field multilinear polynomial commitment scheme of Diamond and Posen [DP24].

Our protocol targets modern 64-bit CPUs with SIMD instructions, making it practical for real-world applications that require zero-knowledge proofs.

Introduction

Modern cryptographic proof systems face a fundamental trade-off between expressiveness and efficiency. While general-purpose SNARKs can handle arbitrary computations, they often incur significant overheads when applied to programs that operate naturally on machine words. Traditional arithmetization frameworks such as R1CS express computations with arithmetic constraints over finite fields, but expressing standard CPU operations typically requires inefficient techniques like binary decomposition and sophisticated lookups arguments. Binius64 addresses this gap with a specialized protocol that exploits the natural alignment between binary field arithmetic and 64-bit word operations to achieve practical proving performance.

The original Binius framework [DP25] pioneered the use of binary tower fields for efficient polynomial commitments. However, its reliance on AIR tables and multi-field arithmetization introduced complexity that hindered both implementation and analysis. Binius64 takes a different approach: we design a constraint system specifically for 64-bit word operations, drawing inspiration from the customizable constraint systems of SuperSpartan [STW23].

Our key technical contribution is the concept of shifted value indices, objects that unify value references with bitwise shift operations. This innovation lets us apply our AND and multiplication constraints directly on shifts of the prover's raw witness data, without demanding that these shifted data be separately committed or constrained. By operating at the word level, as opposed to the bit level, we achieve a 64-fold reduction in the number of constraints compared to naive binary approaches, while maintaining the efficiency benefits of binary field arithmetic.

Beyond efficiency, Binius64 is designed with simplicity as a primary goal. We target modern 64-bit CPUs with SIMD instructions, particularly ARM64 processors with NEON extensions, enabling practical deployment on commodity hardware.

Why Not Binary Spartan?

A natural starting point for a multilinear SNARK over binary fields would be to adapt Spartan [Set20] to work over $\mathbb{F}_2$. That approach seems attractive: the witness would be a single multilinear polynomial over $\mathbb{F}_2$, making the efficient FRI-Binius commitment scheme available; nonlinear constraints could be verified using binary-optimized sumcheck protocols.

However, this approach suffers from a critical efficiency bottleneck in the wiring check. The R1CS matrices $A$, $B$, and $C$ would contain $O(n)$ entries for $n$ witness bits. During the proving protocol, computing partially evaluated matrices would require $O(n)$ multiplications between elements of a large extension field and $\mathbb{F}_2$, resulting in $O(\lambda \cdot n)$ bit operations, where $\lambda \approx 128$ is the security parameter. Additionally, proving the sparse matrix openings would incur another $O(\lambda n)$ factor.

Binius64 addresses this bottleneck using word-level parallelism. By operating on 64-bit words rather than individual bits, we reduce the number of constraint matrix entries by up to 64-fold. Even though the word size is a constant (namely 64), if we model it as proportional to the security parameter (i.e., as $O(\lambda)$), then our approach reduces the number of constraint matrix entries from $O(\lambda n)$ to $O(n)$. Though the asymptotic prover complexity remains $O(\lambda n)$ for the shift reduction protocol, this representation significantly impacts concrete proving costs.

Constraint System

The Binius64 constraint builds on R1CS and CCS [STW23], with several adaptations to efficiently model natural CPU operations. Witness values are represented as 64-bit words rather than finite field elements. Linear relations over words are expressed using bitwise XOR, while the fundamental non-linear constraint encodes bitwise AND. Operands can also incorporate shifts directly on witness words, with native support for logical-left, logical-right, and arithmetic-right shifts. In addition, the system introduces a second non-linear constraint for 64-bit unsigned integer multiplication, avoiding the high cost of emulating this operation using only bitwise constraints.

The diagram below depicts how the AND and MUL constraints apply to the XOR-accumulations of shifted value indices:

On the very left, we have the prover's data, a long array, written vertically. On the right, we have a number of cells, each defined to be an XOR-of-shifts of the prover's data—i.e., an XOR of shifted value indices. On the top right, we demand that various triples $(a[x], b[x], c[x])$ of cells constructed in this way satisfy the AND relationship $a[x] \mathbin{\&} b[x] \stackrel{?}= c[x]$. Lower down, we do a similar thing, now for multiplication constraints. Here, we demand that various quadruples $(p[x], q[x], \text{lo}[x], \text{hi}[x])$ satisfy $p[x] \cdot q[x] \stackrel{?}= 2^{64} \cdot \text{hi}[x] + \text{lo}[x]$ (all products here take place over the integers).

At the bottom, we describe how the unsigned addition of 64-bit integers can be carried out using ANDs and shifts. In short, provided that the prover nondeterministically supplies the 64-bit carry-out word cout, the constraint system can define cin ≔ cout << 1. The single AND constraint

(x ⊕ cin) & (y ⊕ cin) == (cout ⊕ cin)

exactly captures the relationship whereby, bitwise, cout is 1 precisely when at least 2 among the three relevant bits of x, y and cin are 1. Provided that this relationship is enforced, the gadget can return the XOR-of-shifts

z ≔ x ⊕ y ⊕ cin,

or in other words the unsigned addition of x and y.

Protocol Overview

The interactive protocol argues constraint satisfaction through a sequence of interactive reductions that ultimately reduce all checks to a single witness evaluation. The protocol proceeds in several phases:

• Oracle Commitment. The prover sends the witness polynomial commitment to the verifier.
• AND Constraint Reduction. The prover and verifier use the Rijndael zerocheck to reduce AND constraints to evaluation claims on shifted witness values.
• MUL Constraint Reduction. The prover and verifier use the integer multiplication GKR protocol to reduce multiplication constraints to evaluation claims on shifted witness values.
• Shift Reduction. A sumcheck protocol reduces evaluation claims on shifted values (from both MUL and AND constraints) to evaluation claims on the original witness.
• Public Input Check. A final sumcheck verifies that the witness correctly encodes the public constants and input/output values.
• Oracle Opening. The verifier queries the witness polynomial at a single point to complete verification.

This is summarized in the diagram below: