Analysis of the Principles of Binius STARKs and Optimization Thoughts

1 Introduction

A major reason for the inefficiency of STARKs is that most of the values in actual programs are relatively small, such as indices in for loops, boolean values, counters, etc. However, to ensure the security of proofs based on Merkle trees, when using Reed-Solomon encoding to extend the data, many additional redundant values will occupy the entire field, even if the original values themselves are very small. To address this issue, 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 STARKs has a bit width of 64 bits, and the 3rd generation STARKs has a bit width of 32 bits, but the 32-bit encoding still has a lot of wasted space. In comparison, the binary field allows for direct bit manipulation, making the encoding compact and efficient without any wasted space, which is the 4th generation STARKs.

Compared to the finite fields discovered in recent years such as Goldilocks, BabyBear, and Mersenne31, the study of binary fields can be traced back to the 1980s. Currently, binary fields have been widely used in cryptography, with typical examples including:

• Advanced Encryption Standard ( AES ), based on F28 field;

• Galois Message Authentication Code ( GMAC ), based on the F2128 field;

• QR code, using F28-based Reed-Solomon encoding;

• The original FRI and zk-STARK protocols, as well as the Grøstl hash function that entered the final of SHA-3, which is based on the F28 field, are a type of hash algorithm that is very suitable for recursion.

When using smaller fields, the extension field operation becomes increasingly important for ensuring security. The binary field used by Binius relies entirely on extension fields to guarantee its security and practical usability. Most of the polynomials involved in Prover calculations do not need to enter the extension field and can operate under the base field, thus achieving high efficiency in smaller fields. However, random point checks and FRI calculations still need to delve into larger extension fields to ensure the required security.

When constructing a proof system based on binary fields, there are two practical issues: the size of the field used in STARKs for calculating the trace representation should be greater than the degree of the polynomial; during the Merkle tree commitment in STARKs, Reed-Solomon encoding needs to be performed, and the size of the field used should be greater than the size after the encoding expansion.

Binius proposed an innovative solution to address these two issues separately and achieves this by representing the same data in two different ways: first, using multivariable ( specifically multivariate ) polynomials instead of univariate polynomials, representing the entire computation trajectory through its values on "hypercubes" (; secondly, since the length of each dimension of the hypercube is 2, standard Reed-Solomon extensions cannot be performed like STARKs, but the hypercube can be treated as a square ), allowing for Reed-Solomon extensions based on that square. This approach greatly enhances encoding efficiency and computational performance while ensuring security.

2 Principle Analysis

The construction of most current SNARKs systems typically includes the following two parts:

• Information-Theoretic Polynomial Interactive Oracle Proof (: PIOP as the core of the proof system transforms the input computational relations into verifiable polynomial equations. Different PIOP protocols allow the prover to incrementally send polynomials through interaction with the verifier, enabling the verifier to validate the correctness of the computation by querying a small number of polynomial evaluation results. Existing PIOP protocols include: PLONK PIOP, Spartan PIOP, and HyperPlonk PIOP, each having different methods of handling polynomial expressions, thereby affecting the performance and efficiency of the entire SNARK system.

• Polynomial Commitment Scheme ): The polynomial commitment scheme is used to prove whether the polynomial equations generated by PIOP hold true. PCS is a cryptographic tool that allows the prover to commit to a polynomial and later verify the evaluation results of that polynomial, while hiding other information about the polynomial. Common polynomial commitment schemes include KZG, Bulletproofs, FRI ( Fast Reed-Solomon IOPP ), and Brakedown, among others. Different PCS have varying performances, security, and applicable scenarios.

According to specific requirements, choose different PIOP and PCS, and combine them with suitable finite fields or elliptic curves to construct proof systems with different properties. For example:

• Halo2: combines PLONK PIOP and Bulletproofs PCS, based on the Pasta curve. Halo2 is designed with a focus on scalability and the removal of trusted setup in the ZCash protocol.

• Plonky2: Combines PLONK PIOP and FRI PCS, based on the Goldilocks field. Plonky2 is designed for efficient recursion. When designing these systems, the chosen PIOP and PCS must match the finite field or elliptic curve used to ensure the correctness, performance, and security of the system. The choice of these combinations not only affects the proof size and verification efficiency of SNARKs but also determines whether the system can achieve transparency without a trusted setup and whether it can support extended features such as recursive proofs or aggregated proofs.

Binius: HyperPlonk PIOP + Brakedown PCS + binary field. Specifically, Binius includes five key technologies to achieve its efficiency and security. First, the arithmetic based on tower binary fields (towers of binary fields) forms the basis of its computation, enabling simplified operations within the binary field. Second, Binius adapts HyperPlonk product and permutation checks in its interactive Oracle proof protocol (PIOP), ensuring secure and efficient consistency checks between variables and their permutations. Third, the protocol introduces a new multilinear shift proof, optimizing the efficiency of verifying multilinear relationships over small fields. Fourth, Binius employs an improved Lasso lookup proof, providing flexibility and strong security for the lookup mechanism. Finally, the protocol utilizes a small field polynomial commitment scheme (Small-Field PCS), enabling it to achieve an efficient proof system over binary fields while reducing the overhead typically associated with large fields.

( 2.1 Finite Fields: Arithmetic Based on Towers of Binary Fields

Towering binary fields are key to achieving fast verifiable computation, mainly due to two aspects: efficient computation and efficient arithmetic. Binary fields inherently support highly efficient arithmetic operations, making them an ideal choice for performance-sensitive cryptographic applications. Additionally, the structure of binary fields supports a simplified arithmetic process, meaning that operations performed over binary fields can be represented in a compact and easily verifiable algebraic form. These features, combined with the ability to fully leverage their hierarchical characteristics through tower structures, make binary fields particularly suitable for scalable proof systems like Binius.

The term "canonical" refers to the unique and direct representation of elements in a binary field. For example, in the simplest binary field F2, any k-bit string can be directly mapped to a k-bit binary field element. This differs from prime fields, which cannot provide such canonical representation within a given bit length. Although a 32-bit prime field can contain within 32 bits, not every 32-bit string can uniquely correspond to a field element, while the binary field has this convenience of one-to-one mapping. In the prime field Fp, common reduction methods include Barrett reduction, Montgomery reduction, and special reduction methods for specific finite fields such as Mersenne-31 or Goldilocks-64. In the binary field F2k, common reduction methods include special reduction ) as used in AES (, Montgomery reduction ) as used in POLYVAL ###, and recursive reduction ( as in Tower ). The paper "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" notes that in binary fields, both addition and multiplication operations do not require carry propagation, and the squaring operation in binary fields is very efficient, as it follows the simplification rule (X + Y )2 = X2 + Y2.

As shown in Figure 1, a 128-bit string: this string can be interpreted in multiple ways within the context of binary fields. It can be viewed as a unique element in a 128-bit binary field, or parsed as two 64-bit tower field elements, four 32-bit tower field elements, 16 8-bit tower field elements, or 128 F2 field elements. This flexibility of representation does not require any computational overhead, merely a typecast of the bit string (typecast), which is a very interesting and useful property. At the same time, small field elements can be packed into larger field elements without additional computational overhead. The Binius protocol takes advantage of this feature to improve computational efficiency. In addition, the paper "On Efficient Inversion in Tower Fields of Characteristic Two" discusses the computational complexity of multiplication, squaring, and inversion operations in n-bit tower binary fields ( decomposed into m-bit subfields ).

( 2.2 PIOP: Adapted HyperPlonk Product and Permutation Check ------ Suitable for binary fields

The PIOP design in the Binius protocol draws on HyperPlonk and employs a series of core verification mechanisms to validate the correctness of polynomials and sets of multivariables. These core checks include:

1. GateCheck: Verify whether the confidential witness ω and public input x satisfy the circuit operation relation C)x,ω(=0, to ensure the circuit operates correctly.

2. PermutationCheck: Verify whether the evaluation results of two multivariable polynomials f and g on the Boolean hypercube form a permutation relation f)x### = f(π)x(), to ensure the consistency of the arrangement among polynomial variables.

3. LookupCheck: Verify whether the evaluation of the polynomial is in the given lookup table, that is, f(Bµ( ⊆ T)Bµ), ensuring that certain values are within the specified range.

4. MultisetCheck: Check if two multivariate sets are equal, that is, {(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H, ensuring consistency among multiple sets.

5. ProductCheck: Check whether the evaluation of the rational polynomial on the Boolean hypercube equals a declared value ∏x∈Hµ f(x) = s, to ensure the correctness of the polynomial product.

6. ZeroCheck: Verify whether a multivariable polynomial is zero at any point on the Boolean hypercube ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, to ensure the distribution of the polynomial's zeros.

7. SumCheck: Checks whether the sum of a multivariate polynomial equals the declared value ∑x∈Hµ f(x) = s. It reduces the computational complexity for the verifier by transforming the evaluation problem of multivariate polynomials into the evaluation of univariate polynomials. Additionally, SumCheck allows batching, enabling the construction of linear combinations through the introduction of random numbers to achieve batching of multiple sum verification instances.

8. BatchCheck: Based on SumCheck, to verify the correctness of multiple multivariable polynomial evaluations, in order to improve protocol efficiency.

Although Binius and HyperPlonk have many similarities in protocol design, Binius improves on the following three aspects:

• ProductCheck Optimization: In HyperPlonk, ProductCheck requires the denominator U to be non-zero everywhere on the hypercube, and the product must equal a specific value; Binius simplifies this check by specializing that value to 1, thereby reducing computational complexity.

• Handling of Division by Zero Issues: HyperPlonk fails to adequately address division by zero situations, leading to an inability to assert the non-zero problem of U on the hypercube; Binius correctly handles this issue, allowing ProductCheck to continue processing even when the denominator is zero, enabling generalization to arbitrary product values.

• Cross-column PermutationCheck: HyperPlonk does not have this feature; Binius supports PermutationCheck between multiple columns, which enables Binius to handle more complex polynomial arrangement situations.

Therefore, Binius has improved the existing PIOPSumCheck mechanism, enhancing the flexibility and efficiency of the protocol, especially in providing stronger functional support when dealing with more complex multivariate polynomial verifications. These improvements not only address the limitations in HyperPlonk but also lay the groundwork for future proof systems based on binary fields.

( 2.3 PIOP: New multilinear shift argument------applicable to boolean hypercube

In the Binius protocol, the construction and handling of virtual polynomials is one of the key technologies, capable of effectively generating and manipulating polynomials derived from input handles or other virtual polynomials. Here are two key methods:

• Packing: This method optimizes operations by packing smaller elements in adjacent positions in the dictionary order into larger elements. The Pack operator targets block operations of size 2κ and combines them into high-dimensional domains.