Binius STARKs Analysis and Optimization

1. Introduction

One of the main reasons for the inefficiency of STARKs is that most values in actual programs are relatively small. However, to ensure the security of proofs based on Merkle trees, using Reed-Solomon encoding to expand the data results in many additional redundant values occupying the entire field. Reducing the size of the field has become a key strategy.

The encoding bit width of the 1st generation STARKs is 252 bits, the 2nd generation is 64 bits, and the 3rd generation is 32 bits, but the 32-bit encoding bit width still has a lot of wasted space. The binary domain allows for direct bit manipulation, making the encoding compact and efficient without any wasted space, which could be the 4th generation STARKs.

Binius uses arithmetic based on tower binary fields, an improved version of HyperPlonk for product and permutation checking, and techniques such as small field polynomial commitments to enhance efficiency from various perspectives.

2. Principle Analysis

Binius consists of five key technologies:

1. Arithmetic based on tower binary fields
2. Modified HyperPlonk Product and Permutation Check
3. New Multilinear Shift Proof
4. Improved Lasso search proof
5. Small Domain Polynomial Commitment Scheme

2.1 Arithmetic Based on Tower Binary Fields

Tower binary fields support efficient arithmetic operations and simplified arithmetic processes. Binary field elements can be directly mapped to k-bit strings, providing the convenience of a one-to-one mapping.

2.2 Adapted Version HyperPlonk Product Sum and Permutation Check

Binius draws on the core verification mechanisms of HyperPlonk, including GateCheck, PermutationCheck, LookupCheck, etc., and has made improvements in the following aspects:

• ProductCheck Optimization
• Handling of Division by Zero
• Cross-column Permutation Check

2.3 New Multilinear Shift Argument

Binius introduces two key methods, Packing and Shift operators, to construct and manipulate virtual polynomials.

2.4 Adaptation of Lasso Search Argument

Binius adapted Lasso for operations in the binary domain and introduced a multiplicative version of the Lasso protocol.

2.5 Polynomial Commitment

Binius provides two binary field-based Brakedown polynomial commitment schemes, primarily using small field polynomial commitments with extended field evaluation, small field universal construction, and block-level encoding with Reed-Solomon coding techniques.

3. Optimizing Thinking

3.1 GKR-based PIOP

The binary field multiplication algorithm based on GKR transforms "check whether 2 32-bit integers A and B satisfy A·B =? C" into "check whether (gA)B =? gC is valid", significantly reducing the commitment overhead with the help of the GKR protocol.

3.2 ZeroCheck PIOP optimization

By adjusting the workload distribution between the prover and the verifier, various optimization schemes have been proposed:

• Reduce the data transmission of the proving party
• Reduce the number of evaluation points for the proving party
• Algebraic Interpolation Optimization

3.3 Sumcheck PIOP optimization

Ingonyama proposed an improved scheme for the small domain-based Sumcheck protocol, focusing on the selection of the switching round t.

3.4 PCS Optimization: FRI-Binius

FRI-Binius has implemented the FRI folding mechanism in the binary domain, bringing four aspects of innovation:

• Flattened Polynomial
• Subspace Disappearance Polynomial
• Algebra Base Packing
• Ring Exchange SumCheck

4. Summary

Binius is a collaborative design solution that uses "hardware, software, and FPGA-accelerated Sumcheck protocol" to prove quickly with very low memory usage. The commitment bottleneck of the Prover has been almost completely removed in Binius, and the new bottleneck lies in the Sumcheck protocol, which can be efficiently addressed with dedicated hardware.

The FRI-Binius scheme is a variant of FRI that eliminates embedding overhead from the proof layer without causing a spike in costs for the aggregate proof layer. Currently, multiple teams are developing Binius-related technologies, including recursive layers, zkVM, and more.