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

1. Introducción

Una de las principales razones de la baja eficiencia de STARKs es que la mayoría de los valores en los programas reales son relativamente pequeños. Sin embargo, para garantizar la seguridad de las pruebas basadas en árboles de Merkle, al expandir los datos utilizando codificación de Reed-Solomon, muchos valores redundantes adicionales ocupan todo el campo. Reducir el tamaño del campo se ha convertido en una estrategia clave.

La primera generación de codificación STARKs tiene un ancho de 252 bits, la segunda generación tiene 64 bits y la tercera generación tiene 32 bits, pero el ancho de codificación de 32 bits todavía presenta un gran desperdicio de espacio. En comparación, el campo binario permite operaciones directas a nivel de bits, la codificación es compacta y eficiente sin ningún desperdicio de espacio, es decir, la cuarta generación de STARKs.

Binius utiliza un dominio binario, y depende completamente de la extensión del 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 del dominio, sino que solo operan en el dominio base, logrando así una alta eficiencia en un dominio pequeño. Sin embargo, las verificaciones de puntos aleatorios y los cálculos de FRI aún deben profundizar en un dominio de extensión más grande para asegurar la seguridad necesaria.

Binius ha propuesto una solución innovadora: primero, utilizando un polinomio multivariable (específicamente un polinomio multilineal) en lugar de un polinomio univariable, para representar toda la trayectoria de cálculo a través de sus valores en el "hipercubo"; en segundo lugar, considerando el hipercubo como cuadrado, se realiza una expansión de Reed-Solomon basada en ese cuadrado. Este método, al asegurar la seguridad, mejora enormemente la eficiencia de codificación y el rendimiento computacional.

2. Análisis de principios

Binius incluye cinco tecnologías clave:

1. Arithmetización basada en el dominio binario en torre
2. Versión adaptada de la verificación de productos y permutaciones de HyperPlonk
3. Nueva prueba de desplazamiento multilineal
4. Versión mejorada del teorema de búsqueda de Lasso
5. Esquema de compromiso de polinomios de pequeño dominio

2.1 Campos finitos: aritmética basada en torres de campos binarios

El dominio binario en torre admite operaciones aritméticas altamente eficientes y un proceso de aritmética simplificado. Los elementos del dominio binario tienen una representación única y directa, lo que permite convertir y empaquetar de manera flexible entre dominios de diferentes tamaños.

2.2 PIOP: versión adaptada de HyperPlonk Product y PermutationCheck

Binius ha adoptado una serie de mecanismos de verificación fundamentales, incluidos GateCheck, PermutationCheck, LookupCheck, MultisetCheck, ProductCheck, ZeroCheck, SumCheck y BatchCheck.

En comparación con HyperPlonk, Binius ha mejorado en los siguientes aspectos:

• Optimización de ProductCheck
• Manejo del problema de división por cero
• Comprobación de Permutación de Filas

2.3 PIOP: nuevo argumento de desplazamiento multilineal

Binius utiliza dos métodos clave, Packing y el operador de desplazamiento, para manejar polinomios virtuales.

2.4 PIOP: versión adaptada del argumento de búsqueda Lasso

El protocolo Lasso se compone de tres componentes:

• Abstracción de polinomios virtuales de gran tabla
• Búsqueda de la tabla pequeña
• Verificación de múltiples conjuntos

Binius ha introducido una versión multiplicativa del protocolo Lasso, que requiere que la parte que prueba y la parte que verifica realicen la operación de "conteo de memoria" del protocolo de forma conjunta, no mediante un simple incremento de 1, sino mediante el incremento utilizando generadores de multiplicación en el campo binario.

2.5 PCS: versión adaptada Brakedown PCS

Binius compromiso polinómico utiliza principalmente:

• Compromisos de polinomios sobre pequeños dominios y evaluación en dominios extendidos
• Construcción de pequeño dominio
• Codificación a nivel de bloque y tecnología de códigos de Reed-Solomon

3. Optimización del pensamiento

3.1 PIOP basado en GKR: multiplicación de dominio binario basada en GKR

El algoritmo de multiplicación entera basado en GKR, transforma "verificar si 2 enteros de 32 bits A y B satisfacen A·B =? C" en "verificar si (gA)B =? gC es cierto", reduciendo significativamente el costo de compromiso gracias al protocolo GKR.

3.2 ZeroCheck PIOP optimización: balance de costos de cálculo entre Prover y Verifier

• Reducir la transmisión de datos del probador.
• Reducir la cantidad de puntos de evaluación del comprobante.
• Optimización de interpolación algebraica

3.3 Optimización de PIOP de Sumcheck: Protocolo de Sumcheck basado en pequeños dominios

• Efecto y factor de mejora del cambio de ronda
• El impacto del tamaño del dominio en el rendimiento
• Beneficios de la optimización del algoritmo de Karatsuba
• Mejora de la eficiencia de la memoria

3.4 PCS Optimización: FRI-Binius reduce el tamaño de la prueba de Binius

FRI-Binius ha implementado el mecanismo de plegado FRI en el dominio binario, lo que trae cuatro innovaciones:

• Polinomio plano
• Polinomio de desaparición de subespacio
• Paquete de base algebraica
• Intercambio de suma de anillos

4. Resumen

Binius ha eliminado prácticamente por completo el cuello de botella de compromiso de Prover, el nuevo cuello de botella radica en el protocolo Sumcheck. El esquema FRI-Binius es una variante de FRI, que puede eliminar el costo de incrustación en la capa de prueba de dominio. Actualmente, el equipo de Irreducible está desarrollando su capa recursiva y colaborando con el equipo de Polygon para construir un zkVM basado en Binius; JoltzkVM está pasando de Lasso a Binius; el equipo de Ingonyama está implementando una versión FPGA de Binius.