In the past year, there have been a number of new ZK proof systems. One that interests us the most is Binius from Irreducible (formerly known as Ulvetanna).
We pay specific attention to this proof system because our portfolio company, RISC Zero, who has been developing the RISC-V zkVM, told us that Binius will be the next generation proof system and we should keep an eye on. Eddy Lazzarin, CTO of a16zcrypto, also has put Binius "as a top priority" for their proof system, Jolt.
We want to provide a high-level explanation of the Binius protocol. There are two papers on Binius:
We will dedicate two articles for Binius. In this article, we will explain Ligero-Binius, which is simpler, as the first step for understanding Binius.
In the next article, we will discuss FRI-Binius, which is the more recent version.
Ligero-Binius can be seen as an improved version of the Ligero polynomial commitment scheme, but targeted at smaller fields, and it is crucial to first understand Ligero.
Ligero provides a way for a prover to commit a polynomial
Committing the polynomial into a single hash. Ligero starts by turning the polynomial
The matrix is being filled in the following manner.
Next, Ligero applies an error-correcting code on each row. Consider an error-correcting code that encodes
Ligero then builds a Merkle tree of this final matrix of size
Opening the polynomial at a random point
The verifier, in the Ligero protocol, sends the first
For example, the first row (on the top) will be assigned row index
The weighted sum is computed by multiplying each row of the un-encoded matrix (i.e., rows in the “blue” matrix) with the corresponding weights computed above for each row.
Remember that this sum is over the un-encoded matrix, not the encoded matrix. In the animation, we distinguish the final row that is the weighted sum by adding the letter “S” on it. The prover sends the weighted sum (as an entire row) to the verifier.
The verifier now applies the same error-correcting code over the weighted sum. Since the error-correcting code that we use is a linear code, it appears that (1) the encoded form of the weighted sum equals to (2) the weighted sum of the encoded form.
In other words, each column in the encoded form of the weighted sum (shown above as the dark green row with letter "S") should be the weighted sum of the column in the encoded matrix.
The verifier, however, needs to check if this is the case—a malicious prover may have sent the incorrect weighted sum (dark blue with letter "S"), and it is incorrect in that it is inconsistent with the cells in the encoded matrix in the commitment.
Therefore, the verifier will randomly select some columns among the
The verifier then asks the prover to open these columns in their entirety against the Merkle tree root hash. Next, the verifier computes the weighted sum for these columns and checks if they match (1) the encoded form of the weighted sum.
If the encoded form matches the Merkle trees on these columns, then the verifier is convinced that the prover is honest, and the verifier can compute
To compute this "weighted weighted" sum, we first compute the new weights, now over the
The evaluation
To see why this holds, one can firstly look at the structure of f(x), which is a multilinear extension of the boolean hypercube.
We can rewrite the term in the middle to make it more intuitive. Consider the following function.
Since the cells are all over the boolean hypercube, we know that for each cell, it is always one case or the other. This allows us to simplify
The "weighted weighted" sum is basically summing up each cell, multiplied by
This concludes our discussion of how Ligero is used to open the polynomial at a random point
Ligero has an important benefit. The proof generation overhead tends to be smaller, as each step is usually over a row or a column, rather than the entire matrix all together at once. This makes it pretty suitable for hardware acceleration, as is why Irreducible has been paying a lot of attention into building a hardware accelerator for it.
The question is how to achieve good performance of Ligero over small fields.
Previously, we have proof systems that use small fields: Plonky2 pioneers the Goldilocks field, RISC Zero uses the BabyBear field, and Stwo uses the Circle M31 field. The error-correcting code is applied over the small field, while the random point r would be over a larger field to achieve a desired security level (such as 100 bits of security). This larger field is usually an extension of the smaller field, defined by the extension degree. The error-correcting code is naturally generalized into the extension field.
Goldilocks | BabyBear | Circle M31 | |
---|---|---|---|
Prime | |||
Bits | 64 | 31 | 31 |
Code | Reed-Solomon | Reed-Solomon | Circle Reed-Solomon |
Extension degree | 2 | 4 | 4 |
For Binius, which targets at the smallest possible field
With these two answers in mind, you basically have Binius. The rest is just to use Binius in replacement of Ligero in a zero-knowledge proof system that defines the circuit in binary fields. We now explain in more detail about the extension and the error-correcting code.
Binius has two extension sequences: one for CPU with special instructions, one for other hardware devices that do not have these instructions, such as GPU and FPGA.
We start with the second one, which is simpler, called the Wiedemann construction. It starts with
One can see that these eight towers build on a previous tower (or \mathbb{F}_2) and extend from it. This construction has a benefit that it is easy to "lift" elements from the previous field to the next field, as it would be a simple copy, and it is easy to multiply field elements of different levels because of the explicit structure from the previous level to the next.
The first one, on the contrary, is designed for CPUs and leverages special instructions these CPUs provide, and it made two modifications to the Wiedemann construction.
Many CPUs have support for AES field multiplication that can handle it more efficiently. To use this instruction, Binius changes how
Here,
Another change is to note that the POLYVAL field, which is over
The introduction of the POLYVAL field does not break the sequence of extension fields, as it is usually the last extension field that we care about in the sequence (as it offers enough bits of security).
In the simple case of Binius, all the data will be encoded over
There is indeed a lot of flexibility in choosing an error-correcting code here, but Binius strives to get Reed-Solomon code, which is simple and fast to do encoding, to work for small fields.
As we previously discussed, the main limitation is that
Binius borrows an idea from the concatenated code and "packs" sixteen
This packing mechanism also changes how the "columns" are randomly selected in the Ligero protocol. Previously, each column was a
The Binius paper, updated October 2024, provides some results on the performance of the proof system on the CPU. It can be summarized as follows.
As for end-to-end performance, it has been shown that Keccak can be proven at least 2x faster than Plonky3 (the one that SP1 is built over). This is an encouraging note as our current approach before Binius, FRI-based proof systems, is close to reaching its limit, and to make ZK proof systems faster, either we need a new innovation in theory, or we find more efficient hardware acceleration—for example, a key reason that FRI is getting faster in the past few years has to do with Apple’s Metal chips and Nvidia’s new GPUs.
This is why Binius is useful: on the one hand, it shows an approach different from FRI with evidence that it can be faster in some difficult use cases that FRI has been struggling with, and on the other hand, its less reliance on the 32-bit integer processing units of CPU and GPU opens the possibility of FPGA and ASIC accelerators that can be faster than CPU or GPU.
In fact, Irreducible has released the benchmark of their in-progress ASIC design for Binius’s towers and compares it with Mersenne-31. The key metrics over the 14nm process are summarized below.
Mersenne-31 | ||
---|---|---|
Silicon Area ( |
1357 | 748 |
Critical Path ( |
2.0 | 0.7 |
Both metrics are crucial for ASIC development—the smaller the silicon area is, the more units we can put on a single chip, and the shorter the critical path is, the more likely we can run it at a high frequency and have a high processing speed on a single unit. These metrics are often inherent to a specific type of computation and their implementations have been studied for more than a few decades, meaning that the numbers here are likely the best we can do.
One can draw another conclusion from this comparison that Binius's towers would be more efficient than the BabyBear field that we are using today, as the BabyBear field would be more complicated than the Mersenne-31 field to be implemented on customized silicon.
Irreducible also unveils their ASIC design, called X-Check, in a recent talk.
In this article we explain the core idea of Ligero-Binius and show how it can be useful in constructing new proof systems that break the current barriers of efficient proof generation. We will continue working on Binius, especially using Binius in Jolt, for next-generation zkVM.
The next article will discuss FRI-Binius, the more recent version of Binius.
We would like to thank Radisav Cojbasic, Jim Posen, and Benjamin Diamond from Irreducible for reviewing this article and providing feedback.