BInius: highly efficient proofs over binary fields

https://vitalik.eth.limo/general/2024/04/29/binius.html

SNARKs rely on "arithmetization": a way of converting a statement about a program into an equation involving polynomials (or sometimes vectors and matrices)

To keep numbers within reasonable sizes, the arithmetic must be done not over regular integers, but over structures called "finite fields". Modular arithmetic is the simplest example of a finite field, but there are others.

In a real program, most of the numbers are very small: for loop indices, True/False values, array indices, counters...

If a field is large, the "extra" values that get generated during proof computation are much larger. This is a key source of inefficiency.

Plonky2 and similar protocols reduce the field size, dropping from 256 bit to 64 or 31 bit. But it's even more efficient to go all the way to binary fields.

Binary fields are a fascinating mathematical structure that have many unique properties. The tower construction is a fascinating way of producing them, that adds even more advantages.

Here are addition and multiplication tables for 4-bit binary field elements, treating bitstrings as integers in little-endian representation.

They follow weird rules: 2 + 2 = 0, 2 * 6 = 11, and a² + b² = (a+b)². But they satisfy all of the usual laws of arithmetic.

Now, we get to Binius. The core idea in Binius is treating the same data as a hypercube, and as a grid. Here's an example (using regular integers):

For the purposes of polynomial commitment, we look at the hypercube as a multilinear polynomial, and take its evaluations outside the cube. For the purposes of the proof, we take the rows of the grid, and use Reed-Solomon codes to extend them.

Just like with regular FRI, a commitment to a polynomial is a Merkle root of its Reed-Solomon extension. The Reed-Solomon code adds redundancy, which is what allows random sampling of Merkle branches to provide strong guarantees about the underlying data.

The prover takes a random linear combination of the rows, which depends on the evaluation point. The verifier Reed-Solomon extends this linear combination, and takes a linear combination of some columns. If the two computation paths give matching answers, the proof is correct.

Finally, the verifier needs to actually check the evaluation of the polynomial. They can compute this using the row combination that  the prover provided.

Full Binius takes this idea, but restricts it so that the hypercube can only contain bits. To make the whole protocol operate over bits, Binius uses two clever tricks.

Plonky2 and similar protocols reduce the field size, dropping from 256 bit to 64 or 31 bit. But it's even more efficient to go all the way to binary fields.
