Jun Zhang on Warpcast

Jun Zhang pfp

BInius: highly efficient proofs over binary fields https://vitalik.eth.limo/general/2024/04/29/binius.html

1 reply

0 recast

1 reaction

Jun Zhang pfp

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

1 reply

0 recast

0 reaction

Jun Zhang pfp

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.

1 reply

0 recast

0 reaction

Jun Zhang pfp

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.

1 reply

0 recast

0 reaction

Jun Zhang pfp

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.

1 reply

0 recast

0 reaction

Jun Zhang pfp

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.

1 reply

0 recast

0 reaction

Jun Zhang pfp

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.

1 reply

0 recast

0 reaction

Jun Zhang pfp

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

1 reply

0 recast

0 reaction

Jun Zhang pfp

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.

1 reply

0 recast

0 reaction

Jun Zhang pfp

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.

1 reply

0 recast

0 reaction

Jun Zhang pfp

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.

1 reply

0 recast

0 reaction