Análisis de los principios de Binius STARKs y reflexiones sobre su optimización

1 Introducción

Una de las principales razones de la ineficiencia de STARKs es que la mayoría de los valores en los programas reales son bastante pequeños, como los índices en los bucles for, los valores booleanos, los contadores, etc. Sin embargo, para garantizar la seguridad de las pruebas basadas en árboles de Merkle, al usar la codificación de Reed-Solomon para expandir los datos, muchos valores redundantes adicionales ocuparán todo el campo, incluso si el valor original en sí es muy pequeño. Para resolver este problema, reducir el tamaño del campo se ha convertido en una estrategia clave.

El ancho de codificación de la primera generación de STARKs es de 252 bits, el ancho de codificación de la segunda generación de STARKs es de 64 bits, y el ancho de codificación de la tercera generación de STARKs es de 32 bits, pero el ancho de codificación de 32 bits aún presenta una gran cantidad de espacio desperdiciado. En comparación, el dominio binario permite operar directamente sobre los bits, codificando de manera compacta y eficiente sin ningún espacio desperdiciado, es decir, la cuarta generación de STARKs.

En comparación con los cuerpos finitos descubiertos en investigaciones recientes como Goldilocks, BabyBear y Mersenne31, el estudio de los cuerpos binarios se remonta a la década de 1980. Actualmente, los cuerpos binarios se utilizan ampliamente en criptografía, ejemplos típicos incluyen:

• Estándar de cifrado avanzado ( AES ), basado en el campo F28;

• Galois código de autenticación de mensajes ( GMAC ), basado en el campo F2128;

• Código QR, utiliza codificación Reed-Solomon basada en F28;

• Protocolo FRI original y zk-STARK, así como la función hash Grøstl que llegó a la final de SHA-3, que se basa en el campo F28, es un algoritmo de hash muy adecuado para la recursión.

Cuando se utilizan dominios más pequeños, la operación de extensión de dominio se vuelve cada vez más importante para garantizar la seguridad. El dominio binario utilizado por Binius depende completamente de la extensión de dominio para garantizar su seguridad y viabilidad práctica. La mayoría de los polinomios involucrados en los cálculos de Prover no necesitan entrar en la extensión de dominio, sino que operan únicamente en el dominio base, logrando así alta eficiencia en dominios pequeños. Sin embargo, las verificaciones de puntos aleatorios y los cálculos de FRI aún requieren profundizar en una extensión de dominio más grande para garantizar la seguridad necesaria.

Al construir un sistema de pruebas basado en el dominio binario, existen 2 problemas prácticos: al calcular la representación de la traza en STARKs, el tamaño del dominio utilizado debe ser mayor que el grado del polinomio; al comprometer el árbol de Merkle en STARKs, es necesario realizar la codificación de Reed-Solomon, y el tamaño del dominio utilizado debe ser mayor que el tamaño después de la expansión de la codificación.

Binius ha propuesto una solución innovadora que aborda estos dos problemas por separado y logra representar los mismos datos de dos maneras diferentes: primero, utilizando polinomios multivariables (específicamente polinomios multilineales) en lugar de polinomios univariables, representando toda la trayectoria de cálculo a través de sus valores en "hipercubos"; en segundo lugar, dado que la longitud de cada dimensión del hipercubo es 2, no se puede realizar una extensión estándar de Reed-Solomon como en los STARKs, pero se puede considerar el hipercubo como un cuadrado, basando la extensión de Reed-Solomon en ese cuadrado. Este método, al garantizar la seguridad, mejora enormemente la eficiencia de codificación y el rendimiento de cálculo.

2 Análisis de Principios

La mayoría de los sistemas SNARKs actualmente se construyen generalmente en dos partes:

• Prueba de Oráculo Interactivo Polinómico de Teoría de la Información (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP): PIOP, como núcleo del sistema de pruebas, transforma las relaciones computacionales de entrada en ecuaciones polinómicas verificables. Diferentes protocolos PIOP permiten al probador enviar polinomios de manera gradual a través de la interacción con el validador, de modo que el validador pueda verificar si el cálculo es correcto consultando los resultados de la evaluación de un pequeño número de polinomios. Los protocolos PIOP existentes incluyen: PLONK PIOP, Spartan PIOP y HyperPlonk PIOP, cada uno de los cuales tiene diferentes formas de manejar las expresiones polinómicas, lo que afecta el rendimiento y la eficiencia de todo el sistema SNARK.

• Esquema de Compromiso Polinómico (Polynomial Commitment Scheme, PCS): El esquema de compromiso polinómico se utiliza para demostrar si se cumple la igualdad polinómica generada por PIOP. El PCS es una herramienta criptográfica que permite al probador comprometerse a un polinomio y luego verificar el resultado de la evaluación de ese polinomio, mientras oculta otra información sobre el polinomio. Los esquemas de compromiso polinómico comunes incluyen KZG, Bulletproofs, FRI (Fast Reed-Solomon IOPP) y Brakedown, entre otros. Diferentes PCS tienen diferentes características de rendimiento, seguridad y escenarios de aplicación.

Según las necesidades específicas, elija diferentes PIOP y PCS, y combine con el campo finito o la curva elíptica adecuada, se puede construir un sistema de pruebas con diferentes atributos. Por ejemplo:

• Halo2: combina PLONK PIOP y Bulletproofs PCS, y está basado en la curva Pasta. Halo2 se diseñó con un enfoque en la escalabilidad y en la eliminación de la configuración de confianza del protocolo ZCash.

• Plonky2: utiliza la combinación de PLONK PIOP y FRI PCS, y se basa en el campo Goldilocks. Plonky2 está diseñado para lograr una recursividad eficiente. Al diseñar estos sistemas, la PIOP y el PCS seleccionados deben coincidir con el campo finito o la curva elíptica utilizados, para garantizar la corrección, el rendimiento y la seguridad del sistema. La elección de estas combinaciones no solo afecta el tamaño de la prueba SNARK y la eficiencia de verificación, sino que también determina si el sistema puede lograr transparencia sin una configuración confiable, y si puede soportar funciones extendidas como pruebas recursivas o pruebas agregadas.

Binius: HyperPlonk PIOP + Brakedown PCS + dominio binario. En concreto, Binius incluye cinco tecnologías clave para lograr su eficiencia y seguridad. Primero, la aritmética basada en torres de campos binarios constituye la base de su computación, permitiendo realizar operaciones simplificadas dentro del dominio binario. En segundo lugar, Binius ha adaptado la verificación de producto y permutación de HyperPlonk en su protocolo de prueba de Oracle interactivo (PIOP), asegurando una verificación de consistencia entre las variables y sus permutaciones de manera segura y eficiente. En tercer lugar, el protocolo introduce una nueva prueba de desplazamiento multivariable, optimizando la eficiencia en la verificación de relaciones multivariadas en pequeños dominios. Cuarto, Binius utiliza una versión mejorada de la prueba de búsqueda Lasso, que proporciona flexibilidad y una sólida seguridad al mecanismo de búsqueda. Por último, el protocolo emplea un esquema de compromiso polinómico de pequeño dominio (Small-Field PCS), lo que le permite implementar un sistema de pruebas eficiente en un dominio binario, reduciendo el costo generalmente asociado con grandes dominios.

2.1 Campo finito: aritmética basada en torres de campos binarios

Los cuerpos binarios en torre son clave para lograr cálculos verificables rápidos, principalmente debido a dos aspectos: cálculo eficiente y aritmética eficiente. Los cuerpos binarios, en esencia, admiten operaciones aritméticas altamente eficientes, lo que los convierte en una opción ideal para aplicaciones criptográficas que requieren un alto rendimiento. Además, la estructura de los cuerpos binarios admite un proceso de aritmética simplificada, es decir, las operaciones realizadas sobre el cuerpo binario se pueden representar en una forma algebraica compacta y fácil de verificar. Estas características, junto con la capacidad de aprovechar plenamente su naturaleza jerárquica a través de la estructura en torre, hacen que los cuerpos binarios sean particularmente adecuados para sistemas de prueba escalables como Binius.

En este contexto, "canónico" se refiere a la representación única y directa de un elemento en un campo binario. Por ejemplo, en el campo binario F2 más básico, cualquier cadena de k bits puede mapearse directamente a un elemento de campo binario de k bits. Esto es diferente de los campos primos, ya que un campo primo no puede proporcionar esta representación canónica dentro de un número fijo de bits. Aunque un campo primo de 32 bits puede contenerse en 32 bits, no todas las cadenas de 32 bits pueden corresponder de manera única a un elemento del campo, mientras que el campo binario ofrece esta conveniencia de mapeo uno a uno. En el campo primo Fp, los métodos de reducción comunes incluyen la reducción Barrett, la reducción Montgomery y métodos de reducción especiales para campos finitos específicos como Mersenne-31 o Goldilocks-64. En el campo binario F2k, los métodos de reducción comúnmente utilizados incluyen reducciones especiales (como las utilizadas en AES), la reducción Montgomery (como se utiliza en POLYVAL) y la reducción recursiva (como Tower). El artículo "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" señala que el campo binario no requiere llevar en las operaciones de suma y multiplicación, y que la operación de cuadrado en el campo binario es muy eficiente, ya que sigue la regla simplificada de (X + Y )2 = X2 + Y2.

Como se muestra en la figura 1, una cadena de 128 bits: esta cadena se puede interpretar de múltiples maneras en el contexto del campo binario. Puede ser vista como un elemento único en un campo binario de 128 bits, o ser descompuesta en dos elementos de campo de torre de 64 bits, cuatro elementos de campo de torre de 32 bits, 16 elementos de campo de torre de 8 bits, o 128 elementos de campo F2. Esta flexibilidad en la representación no requiere ningún costo computacional, solo una conversión de tipo de la cadena de bits, lo que es una propiedad muy interesante y útil. Al mismo tiempo, los elementos de campo pequeños pueden ser empaquetados en elementos de campo más grandes sin necesidad de un costo computacional adicional. El protocolo Binius aprovecha esta característica para mejorar la eficiencia computacional. Además, el artículo "On Efficient Inversion in Tower Fields of Characteristic Two" explora la complejidad computacional de realizar multiplicaciones, cuadrados y operaciones de inversión en un campo binario en torre de n bits (descomponible en subcampos de m bits).

2.2 PIOP: versión adaptada del producto HyperPlonk y PermutationCheck------aplicable a campos binarios

El diseño de PIOP en el protocolo Binius se basa en HyperPlonk, y utiliza una serie de mecanismos de verificación clave para validar la corrección de polinomios y conjuntos multivariados. Estas verificaciones clave incluyen:

1. GateCheck: Verifica si el testigo confidencial ω y la entrada pública x satisfacen la relación de operación del circuito C(x,ω)=0, para asegurar que el circuito funcione correctamente.

2. PermutationCheck: Verifica si los resultados de evaluación de dos polinomios multivariables f y g en el hipercubo booleano forman una relación de permutación f(x) = f(π(x)), para asegurar la consistencia en la permutación entre las variables del polinomio.

3. LookupCheck: Verifica si la evaluación del polinomio está en la tabla de búsqueda dada, es decir, f(Bµ) ⊆ T(Bµ), asegurando que ciertos valores estén dentro del rango especificado.

4. MultisetCheck: Verifica si dos conjuntos multivariables son iguales, es decir, {(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H, asegurando la consistencia entre varios conjuntos.

5. ProductCheck: Verifica si la evaluación de un polinomio racional en el hipercubo booleano es igual a un valor declarado ∏x∈Hµ f(x) = s, para asegurar la corrección del producto del polinomio.

6. ZeroCheck: Verificar si un polinomio multivariable en un hipercubo booleano es cero en un punto arbitrario ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, para asegurar la distribución de los ceros del polinomio.

7. SumCheck: Verifica si la suma de un polinomio multivariable es igual al valor declarado ∑x∈Hµ f(x) = s. Al transformar el problema de evaluación de polinomios multivariables en la evaluación de un polinomio univariante, se reduce la complejidad computacional del verificador. Además, SumCheck permite el procesamiento por lotes, introduciendo números aleatorios para construir combinaciones lineales y realizar el procesamiento por lotes de múltiples instancias de verificación de sumas.

8. BatchCheck: Basado en SumCheck, verifica la corrección de la evaluación de múltiples polinomios multivariables para mejorar la eficiencia del protocolo.

A pesar de que Binius y HyperPlonk tienen muchas similitudes en el diseño del protocolo, Binius ha mejorado en los siguientes 3 aspectos:

• Optimización de ProductCheck: en HyperPlonk, ProductCheck requiere que el denominador U sea no cero en todo el hipercubo, y el producto debe ser igual a un valor específico; Binius simplifica este proceso de verificación al especializar este valor en 1, reduciendo así la complejidad computacional.

• Manejo del problema de la división por cero: HyperPlonk no pudo manejar adecuadamente la situación de división por cero, lo que llevó a no poder afirmar que U es no cero en el hipercubo; Binius manejó correctamente este problema, incluso en el caso de que el denominador sea cero, el ProductCheck de Binius puede continuar procesando, permitiendo la generalización a cualquier valor de producto.

• Comprobación de permutación entre columnas: HyperPlonk no tiene esta función; Binius admite la comprobación de permutación entre múltiples columnas, lo que permite a Binius manejar situaciones de permutación polinómica más complejas.

Por lo tanto, Binius ha mejorado el mecanismo existente de PIOPSumCheck, aumentando la flexibilidad y eficiencia del protocolo, especialmente al manejar la verificación de polinomios multivariables más complejos, proporcionando un soporte funcional más robusto. Estas mejoras no solo abordan las limitaciones en HyperPlonk, sino que también establecen una base para futuros sistemas de prueba basados en campos binarios.

2.3 PIOP: nuevo argumento de desplazamiento multilineal ------ aplicable al hipercubo booleano

En el protocolo Binius, la construcción y manipulación de polinomios virtuales es una de las tecnologías clave, capaz de generar y operar de manera efectiva polinomios derivados de manejadores de entrada u otros polinomios virtuales. A continuación se presentan dos métodos clave:

• Empaque: Este método optimiza la operación empaquetando elementos más pequeños en posiciones adyacentes de la orden léxica en elementos más grandes. El operador Pack opera en bloques de tamaño 2κ y los combina.