BInius: highly efficient proofs over binary fields

vitalik.eth.limo/general/2024…

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):