Análise dos Princípios e Reflexões de Otimização sobre Binius STARKs

1. Introdução

Uma das principais razões para a baixa eficiência dos STARKs é que a maioria dos valores nos programas reais é bastante pequena, mas para garantir a segurança das provas baseadas em árvores de Merkle, a codificação de Reed-Solomon expande os dados, resultando em muitos valores redundantes adicionais que ocupam todo o domínio. Para resolver esse problema, a redução do tamanho do domínio tornou-se uma estratégia chave.

A largura de codificação dos STARKs da 1ª geração é de 252 bits, a da 2ª geração é de 64 bits e a da 3ª geração é de 32 bits, mas a largura de codificação de 32 bits ainda apresenta uma grande quantidade de espaço desperdiçado. Em comparação, o domínio binário permite a manipulação direta de bits, com codificação compacta e eficiente sem espaço desperdiçado, ou seja, os STARKs da 4ª geração.

O domínio binário utilizado pela Binius depende completamente da extensão do domínio para garantir sua segurança e viabilidade prática. A maioria dos polinômios envolvidos nos cálculos do Prover não precisa entrar na extensão do domínio, operando apenas no domínio base, permitindo assim uma alta eficiência em um pequeno domínio. No entanto, a verificação de pontos aleatórios e os cálculos FRI ainda precisam aprofundar-se em uma extensão de domínio maior para garantir a segurança necessária.

Binius apresentou uma solução inovadora: primeiro, usando polinômios multivariáveis (especificamente polinômios multilineares) em vez de polinômios univariáveis, representando toda a trajetória de cálculo através de seus valores em "hipercubos" (hypercubes); em segundo lugar, dado que o comprimento de cada dimensão do hipercubo é 2, não é possível fazer a extensão padrão de Reed-Solomon como nos STARKs, mas pode-se considerar o hipercubo como um quadrado (square) e realizar a extensão de Reed-Solomon com base nesse quadrado.

2. Análise do Princípio

Binius inclui cinco tecnologias-chave:

1. Arithmetização baseada em domínios binários em torre
2. Verificação de produtos e permutações da versão adaptada do HyperPlonk
3. Nova prova de deslocamento multilinear
4. Versão Melhorada da Prova de Busca Lasso
5. Esquema de compromisso de polinômios de pequeno domínio

2.1 Domínios Finitos: Arithmetização baseada em torres de campos binários

Vantagens do domínio binário em torre:

• Cálculo eficiente: o domínio binário suporta essencialmente operações aritméticas altamente eficientes
• Arithmetização eficiente: a estrutura do campo binário suporta um processo de aritmização simplificado
• Representação normalizada: os elementos no domínio binário têm uma representação única e direta.

Vantagens do domínio binário:

• As operações de adição e multiplicação não requerem o transporte.
• A operação quadrática é muito eficiente, seguindo a regra de simplificação (X + Y)^2 = X^2 + Y^2
• Representa flexibilidade: uma string de 128 bits pode ser vista como um elemento único no domínio binário de 128 bits ou interpretada como uma combinação de vários elementos de domínio.

2.2 PIOP: Versão adaptada do Produto HyperPlonk e Verificação de Permutação

Mecanismo de verificação central do Binius PIOP:

• GateCheck
• PermutationCheck
• LookupCheck
• MultisetCheck
• ProductCheck
• ZeroCheck
• SumCheck
• BatchCheck

Melhorias da Binius no HyperPlonk:

• Otimização do ProductCheck
• Tratamento do problema da divisão por zero
• Suporte a PermutationCheck entre colunas

2.3 PIOP: novo argumento de deslocamento multilinear

Método chave:

• Packing: Otimização de operações através do empacotamento de elementos adjacentes
• Operador de deslocamento: reordenar elementos dentro do bloco

2.4 PIOP: versão adaptada do argumento de pesquisa Lasso

Composição do protocolo Lasso:

• Abstração de polinômios virtuais de grande tabela
• Pesquisa de tabela pequena
• Verificação de múltiplos conjuntos

Adaptação do Binius para o Lasso:

• Introdução da versão multiplicativa do protocolo Lasso
• Requer que a parte comprovante se comprometa com um vetor de contagem de leituras que seja sempre não zero.

2.5 PCS: versão adaptada Brakedown PCS

Ideia central: packing

Duas propostas de compromisso polinomial Brakedown baseadas em domínios binários:

1. Instanciar código concatenado
2. Utilizando a tecnologia de codificação em nível de bloco, suporta o uso independente de códigos de Reed-Solomon.

Principais tecnologias:

• Compromissos de polinómios de pequeno domínio e avaliação de domínio alargado
• Construção de pequeno domínio
• Codificação em bloco e códigos de Reed-Solomon

3. Otimização do Pensamento

Quatro pontos-chave de otimização:

3.1 PIOP baseado em GKR: multiplicação de campo binário baseada em GKR

Vantagens em comparação com a solução de pesquisa Binius:

• Apenas um compromisso auxiliar
• Reduzir os custos de Sumchecks

3.2 ZeroCheck PIOP otimização: balanço de custos entre Prover e Verifier

Método de otimização:

• Reduzir a transmissão de dados do provedor de prova
• Reduzir o número de pontos de avaliação da parte comprovadora
• Otimização de interpolação algébrica

3.3 Sumcheck PIOP otimização: protocolo Sumcheck baseado em pequenos domínios

Pontos-chave:

• Impacto da mudança de rodadas e fator de melhoria
• O impacto do tamanho do domínio na performance
• Benefícios da otimização do algoritmo de Karatsuba
• Aumento da eficiência da memória

3.4 PCS otimização: FRI-Binius reduz o tamanho da prova Binius

FRI-Binius quatro inovações:

• Polinômio achatado
• Polinômio de desaparecimento do subespaço
• Embalagem de base algébrica
• Troca de Anéis SumCheck

FRI-Binius PCS processo:

• Fase de Compromisso
• Fase de Avaliação

4. Resumo

Proposta de valor da Binius:

• Pode usar o menor domínio de potência de dois para testemunhas.
• Proposta de design colaborativo, baixa taxa de utilização de memória para prova rápida
• Remoção básica do gargalo de compromisso do Prover
• O novo gargalo está no protocolo Sumcheck, que pode ser resolvido de forma eficiente com hardware dedicado.

FRI-Binius方案:

• Eliminar o custo de incorporação da camada de prova de domínio
• Não irá causar um aumento explosivo nos custos da camada de prova de agregação

Progresso atual:

• A equipe Irreducible desenvolve uma camada recursiva, em colaboração com a Polygon, para construir um zkVM baseado em Binius.
• JoltzkVM mudou de Lasso para Binius
• A equipe Ingonyama implementou a versão FPGA do Binius