Análise dos princípios dos STARKs da Binius e reflexões sobre a sua otimização

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, o uso de codificação Reed-Solomon para expandir os dados resulta em muitos valores redundantes adicionais ocupando todo o domínio, mesmo que o valor original em si seja muito pequeno. Para resolver esse problema, a redução do tamanho do domínio tornou-se uma estratégia chave.

A largura de codificação do STARKs de primeira geração é de 252 bits, a largura de codificação do STARKs de segunda geração é de 64 bits, e a largura de codificação do STARKs de terceira 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 operações diretas sobre os bits, codificando de forma compacta e eficiente, sem espaço desperdiçado, ou seja, o STARKs de quarta geração.

Em comparação com os domínios finitos descobertos em pesquisas recentes, como Goldilocks, BabyBear e Mersenne31, a pesquisa sobre domínios binários remonta à década de 1980. Atualmente, os domínios binários são amplamente utilizados em criptografia, exemplos típicos incluem:

• Padrão de Criptografia Avançada ( AES ), baseado no domínio F28;

• Galois Message Authentication Code ( GMAC ), baseado no domínio F2128;

• Código QR, usando codificação Reed-Solomon baseada em F28;

• Protocólos FRI originais e zk-STARK, bem como a função de hash Grøstl, que chegou à final do SHA-3, baseada no domínio F28, é um algoritmo de hash muito adequado para recursão.

Quando se utilizam domínios menores, a operação de extensão de domínio torna-se cada vez mais importante para garantir a segurança. O domínio binário utilizado pela Binius depende completamente da extensão de domínio para garantir sua segurança e viabilidade prática. A maioria dos polinómios envolvidos nos cálculos do Prover não necessita de entrar na extensão de domínio, mas apenas operar sob o domínio base, o que permite uma alta eficiência em domínios pequenos. No entanto, a verificação de pontos aleatórios e o cálculo FRI ainda precisam aprofundar-se em domínios de extensão maiores para garantir a segurança necessária.

Ao construir um sistema de prova baseado em domínios binários, existem 2 problemas práticos: ao calcular a representação do traço nos STARKs, o tamanho do domínio utilizado deve ser maior que o grau do polinômio; ao comprometer a árvore Merkle nos STARKs, é necessário realizar a codificação de Reed-Solomon, e o tamanho do domínio utilizado deve ser maior que o tamanho após a expansão da codificação.

A Binius propôs uma solução inovadora que lida separadamente com esses dois problemas e representa os mesmos dados de duas maneiras diferentes: primeiro, usando polinômios multivariados (especificamente polinômios multilineares) em vez de polinômios unidimensionais, representando toda a trajetória de cálculo por seus valores em "hipercubos" (hypercubes); em segundo lugar, como o comprimento de cada dimensão do hipercubo é 2, não é possível realizar uma extensão de Reed-Solomon padrão como nos STARKs, mas o hipercubo pode ser considerado um quadrado (square), baseado no qual se realiza a extensão de Reed-Solomon. Este método, ao garantir a segurança, melhora significativamente a eficiência de codificação e o desempenho computacional.

2 Análise de Princípios

Atualmente, a construção da maioria dos sistemas SNARKs geralmente inclui as seguintes duas partes:

• Prova de Oracle Interativa Polinomial Teórica da Informação (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP): O PIOP, como núcleo do sistema de prova, transforma as relações computacionais de entrada em igualdades polinomiais verificáveis. Diferentes protocolos PIOP permitem que o provador envie polinômios gradualmente através da interação com o verificador, de modo que o verificador possa validar se o cálculo está correto consultando os resultados de avaliação de um número reduzido de polinômios. Os protocolos PIOP existentes incluem: PIOP PLONK, PIOP Spartan e PIOP HyperPlonk, que diferem entre si na forma como tratam as expressões polinomiais, afetando assim o desempenho e a eficiência de todo o sistema SNARK.

• Esquema de Compromisso Polinomial (Polynomial Commitment Scheme, PCS): O esquema de compromisso polinomial é utilizado para provar se a igualdade polinomial gerada pelo PIOP é válida. O PCS é uma ferramenta criptográfica que permite ao provador comprometer-se com um determinado polinômio e, posteriormente, verificar o resultado da avaliação desse polinômio, enquanto oculta outras informações sobre o polinômio. Esquemas de compromisso polinomial comuns incluem KZG, Bulletproofs, FRI (Fast Reed-Solomon IOPP) e Brakedown, entre outros. Diferentes PCS apresentam diferentes desempenhos, níveis de segurança e cenários de aplicação.

De acordo com as necessidades específicas, escolha diferentes PIOP e PCS, e combine com um domínio finito ou curva elíptica apropriada, podendo assim construir sistemas de prova com diferentes propriedades. Por exemplo:

• Halo2: combina PLONK PIOP e Bulletproofs PCS, baseado na curva Pasta. O Halo2 foi projetado com foco na escalabilidade e na remoção da configuração confiável do protocolo ZCash.

• Plonky2: utiliza a combinação de PLONK PIOP e FRI PCS, baseada no domínio Goldilocks. Plonky2 foi projetado para alcançar recursão eficiente. Ao projetar esses sistemas, a PIOP e a PCS escolhidas devem corresponder ao campo finito ou curva elíptica utilizada, a fim de garantir a correção, desempenho e segurança do sistema. A escolha dessas combinações não apenas afeta o tamanho da prova e a eficiência de verificação do SNARK, mas também determina se o sistema pode alcançar transparência sem a necessidade de uma configuração confiável, e se pode suportar funcionalidades expandidas como provas recursivas ou provas de agregação.

Binius: HyperPlonk PIOP + Brakedown PCS + domínio binário. Especificamente, Binius inclui cinco tecnologias-chave para alcançar sua eficiência e segurança. Primeiro, a aritmética baseada em torres de campos binários constitui a base de seus cálculos, permitindo operações simplificadas dentro do campo binário. Em segundo lugar, o Binius adaptou a verificação de produtos e permutações do HyperPlonk em seu protocolo de prova de Oracle interativa (PIOP), garantindo uma verificação de consistência segura e eficiente entre variáveis e suas permutações. Em terceiro lugar, o protocolo introduziu uma nova prova de deslocamento multilinear, otimizando a eficiência da verificação de relações multilineares em pequenos campos. Quarto, o Binius utiliza uma versão aprimorada da prova de busca Lasso, proporcionando flexibilidade e segurança robusta ao mecanismo de busca. Por fim, o protocolo utiliza um esquema de compromisso de polinômios de pequenos campos (Small-Field PCS), permitindo a implementação de um sistema de provas eficiente no campo binário e reduzindo os custos geralmente associados a grandes campos.

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

Os domínios binários em torre são fundamentais para a implementação de cálculos rápidos e verificáveis, principalmente devido a dois aspectos: cálculo eficiente e aritmética eficiente. Os domínios binários suportam essencialmente operações aritméticas altamente eficientes, tornando-os uma escolha ideal para aplicações criptográficas sensíveis ao desempenho. Além disso, a estrutura dos domínios binários suporta um processo de aritmética simplificado, ou seja, as operações realizadas sobre os domínios binários podem ser expressas em uma forma algébrica compacta e fácil de verificar. Essas características, juntamente com a capacidade de aproveitar plenamente suas propriedades hierárquicas através da estrutura em torre, tornam os domínios binários particularmente adequados para sistemas de prova escaláveis como o Binius.

O termo "canonical" refere-se à representação única e direta de um elemento no domínio binário. Por exemplo, no domínio binário F2 mais básico, qualquer cadeia de k bits pode ser mapeada diretamente para um elemento de domínio binário de k bits. Isso difere do domínio primo, que não consegue fornecer essa representação canônica dentro de um número fixo de bits. Embora um domínio primo de 32 bits possa caber em 32 bits, nem toda cadeia de 32 bits pode corresponder de forma única a um elemento do domínio, enquanto o domínio binário possui essa conveniência de mapeamento um-para-um. No domínio primo Fp, os métodos de redução mais comuns incluem a redução Barrett, a redução Montgomery, e métodos de redução especiais para domínios finitos específicos, como Mersenne-31 ou Goldilocks-64. No domínio binário F2k, os métodos de redução comumente usados incluem a redução especial (como a usada no AES), a redução Montgomery (como a usada no POLYVAL) e a redução recursiva (como a Tower). O artigo "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" observa que no domínio binário, tanto a adição quanto a multiplicação não requerem o transporte, e a operação de quadrado no domínio binário é muito eficiente, pois segue a regra simplificada (X + Y )2 = X2 + Y2.

Como mostrado na Figura 1, uma string de 128 bits: esta string pode ser interpretada de várias maneiras no contexto de um domínio binário. Pode ser vista como um elemento único em um domínio binário de 128 bits, ou ser analisada como dois elementos de domínio de torre de 64 bits, quatro elementos de domínio de torre de 32 bits, 16 elementos de domínio de torre de 8 bits, ou 128 elementos do domínio F2. Essa flexibilidade de representação não requer nenhum custo computacional adicional, sendo apenas uma conversão de tipo da string de bits, o que é uma propriedade muito interessante e útil. Além disso, elementos de domínio pequenos podem ser empacotados em elementos de domínio maiores sem a necessidade de custos computacionais adicionais. O protocolo Binius tira proveito dessa característica para aumentar a eficiência computacional. Além disso, o artigo "On Efficient Inversion in Tower Fields of Characteristic Two" explora a complexidade computacional de multiplicação, elevação ao quadrado e operação de inversão em domínios binários de torre de n bits (que podem ser decompostos em subdomínios de m bits).

2.2 PIOP: versão adaptada do Produto HyperPlonk e Verificação de Permutação------aplicável ao domínio binário

O design do PIOP no protocolo Binius foi inspirado no HyperPlonk, adotando uma série de mecanismos de verificação fundamentais para validar a correção de polinómios e conjuntos multivariados. Essas verificações fundamentais incluem:

1. GateCheck: Verificar se a prova de conhecimento zero ω e a entrada pública x satisfazem a relação de operação do circuito C(x, ω)=0, para garantir que o circuito funcione corretamente.

2. PermutationCheck: Verifica se os resultados da avaliação de dois polinômios multivariáveis f e g no hipercubo booleano são uma relação de permutação f(x) = f(π(x)), para garantir a consistência da permutação entre as variáveis do polinômio.

3. LookupCheck: Verifica se a avaliação do polinômio está na tabela de pesquisa dada, ou seja, f(Bµ) ⊆ T(Bµ), garantindo que certos valores estejam dentro da faixa especificada.

4. MultisetCheck: Verifica se dois conjuntos multivariáveis são iguais, ou seja, {(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H, garantindo a consistência entre múltiplos conjuntos.

5. ProductCheck: Verifica se a avaliação de um polinómio racional no hipercubo booleano é igual a um valor declarado ∏x∈Hµ f(x) = s, para garantir a correção do produto polinómico.

6. ZeroCheck: Verificar se um polinômio multivariável em um hipercubo booleano em qualquer ponto é zero ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, para garantir a distribuição dos zeros do polinômio.

7. SumCheck: Verifica se a soma de um polinómio multivariável é igual ao valor declarado ∑x∈Hµ f(x) = s. Ao transformar o problema da avaliação de polinómios multivariáveis em avaliação de polinómios univariáveis, reduz a complexidade computacional para o verificador. Além disso, o SumCheck também permite o processamento em lote, introduzindo números aleatórios para construir combinações lineares que realizam o processamento em lote de várias instâncias de verificação de soma.

8. BatchCheck: baseado no SumCheck, verifica a correção da avaliação de múltiplos polinómios multivariados, para aumentar a eficiência do protocolo.

Embora Binius e HyperPlonk tenham muitas semelhanças no design do protocolo, Binius fez melhorias nas seguintes 3 áreas:

• ProductCheck otimizado: no HyperPlonk, o ProductCheck requer que o denominador U seja não nulo em todo o hipercubo, e o produto deve ser igual a um valor específico; Binius simplifica esse processo de verificação ao especializar esse valor para 1, reduzindo assim a complexidade computacional.

• Tratamento do problema da divisão por zero: HyperPlonk não conseguiu lidar adequadamente com a situação de divisão por zero, levando a não se poder afirmar que U é não zero no hipercubo; Binius tratou corretamente deste problema, mesmo quando o denominador é zero, o ProductCheck do Binius consegue continuar a processar, permitindo a generalização para qualquer valor de produto.

• Verificação de Permutação entre Colunas: HyperPlonk não possui esta funcionalidade; Binius suporta a Verificação de Permutação entre várias colunas, o que permite ao Binius lidar com situações de permutação polinomial mais complexas.

Assim, a Binius melhorou a flexibilidade e a eficiência do protocolo através da modificação do mecanismo existente PIOPSumCheck, especialmente ao lidar com a validação de polinómios multivariados mais complexos, proporcionando um suporte funcional mais robusto. Estas melhorias não só resolveram as limitações do HyperPlonk, mas também estabeleceram uma base para sistemas de prova futuros baseados em domínios binários.

2.3 PIOP: novo argumento de deslocamento multilinhar------aplicável ao hipercubo booleano

No protocolo Binius, a construção e o processamento de polinômios virtuais são uma das tecnologias-chave, capazes de gerar e operar eficazmente polinômios derivados de manipuladores de entrada ou outros polinômios virtuais. Aqui estão dois métodos-chave:

• Packing: Este método funciona ao combinar elementos menores em posições adjacentes na ordem do dicionário.