Binius

Binius is a new STARK (a proof system like a SNARK) that works natively over binary fields.

Older SNARKS like Groth16 and PLONK are widely used in practice (here at 0xPARC, our ZK infrastructure rests on Groth16), but they are very costly because they work over large fields. Since Binius works over binary fields, it offers big reductions in prover overhead.

Overview of a SNARK / STARK

A proof system (SNARK or STARK) lets a prover convince a verifier of the truth of some statement, like:

• “I have a message, with a valid digital signature from Utility Inc., that contains the text “Balance due: $0”.

A SNARK or STARK starts with witnesses to the truth of the statement. In our example, the witnesses might include:

• The full text of the message.
• The string “Balance due: $0”.
• A character index that shows where to find “Balance due: $0” in the full message.
• Utility Inc’s public signature-verification key.
• A computation trace showing that the digital signature verifies correctly.

Most SNARKs and STARKs have a feature called “zero-knowledge”: the prover can choose which witnesses to make public and which to keep private. In our example, the string “Balance due: $0” and the signature-verification key would be public witnesses: the verifier needs to see them for the proof to have meaning. All other witnesses would be private, so the verifier would not learn anything else about the text of the message.

To product a cryptographic proof, a SNARK/STARK will pass through three steps.

• Arithmetization: The prover encodes the witnesses in a specific mathematical form, for example as elements of a finite field. The prover also transforms the statement to be proven into a mathematical statement about the witness values – for example, it might become a system of quadratic equations.
• Commitment: The prover produces some sort of commitment to the witnesses. In practice, the prover will commit to some sort of polynomial that encodes the full list of witnesses; later on, the prover will be able to “open” the commitment by evaluating the polynomial at any point.
• Proof: By opening the polynomial commitment at a small number of carefully selected points, the prover can convince the verifier that the statement is true for the full list of witnesses.

(The difference between a SNARK and a STARK isn’t important to us here, but in case you’re wondering: A SNARK requires a “trusted setup.” In trusted setup, a trusted third party does some randomized math to generate some “public parameters”, and then they forget the random numbers they used to make the parameters. The third party has to be trusted to delete those secret random numbers – if they don’t, they will have a secret back door that they could use to create false proofs. A STARK doesn’t rely on trusted setup, so it is safe against this sort of security vulnerability.)

Overview of Binius

Now that we’ve explained the three pieces of a STARK, we can come back and show how Binius works.

• Arithmetization. Binius encodes the witness as a sequence of bits. We can think of bits as elements of the two-element field $\mathbb{F}_2$. Or, alternatively, we can pack $2^k$ bits together to get an element of the field $\mathbb{F}_{2^{2^k}}$ (yes, that really is a double exponential!).

  In fact, this idea of packing and unpacking bits is what unlocks the efficiency gains in Binius. When you need a large field for security, you pack 256 bits together and work in a 256-bit field. But in most steps of the calculation, security is not a concern, so you unpack the values and just work directly with bits.

  Binius offers support for several different constraints on the witnesses. The most important are:

  • Polynomial constraints: Assert that some witnesses satisfy a low-degree polynomial equations.
  • Equality constraints: Assert that two witnesses are equal to each other, or that one witness is equal to a public constant.
  • Lookup constraints: Assert that one witness can be found in a “lookup table” of permissible values. (This is very important because some mathematical functions are most effectively implemented by lookup tables.)

• Commitment. Binius uses a commitment scheme for multilinear polynomials, called Brakedown. We explain it in a separate post.

• Proof. The proof uses a suite of advanced protocols, most developed over the past few years. Highlights include the classic sumcheck protocol and a new (2023) lookup system called Lasso.

  For full details, check out the original paper.