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 ineficiência dos STARKs é que a maioria dos valores em programas reais é bastante pequena, como índices em loops for, valores booleanos, contadores, etc. No entanto, 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 que ocupam todo o domínio, mesmo que o valor original em si seja muito pequeno. Para resolver esse problema, reduzir o tamanho do domínio tornou-se uma estratégia chave.

Como mostrado na Tabela 1, a largura de codificação da 1ª geração de STARKs é de 252 bits, a largura de codificação da 2ª geração de STARKs é de 64 bits, e a largura de codificação da 3ª geração de STARKs é 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 operação direta nos bits, com codificação compacta e eficiente, sem qualquer espaço desperdiçado, ou seja, a 4ª geração de STARKs.

Tabela 1: Caminho de Derivação STARKs

| Álgebra | Largura de codificação | Sistema representativo | |------|----------|----------| | 1ª geração | 252bit | StarkWare |
| 2ª geração | 64bit | Plonky2 | | 3ª Geração | 32bit | Polygon zkEVM | | 4ª geração | 1bit | Binius |

Comparado com as descobertas mais recentes sobre campos finitos, como Goldilocks, BabyBear e Mersenne31, a pesquisa sobre campos binários remonta à década de 1980. Atualmente, os campos binários são amplamente utilizados na 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;

• QR Code, utilizando codificação Reed-Solomon baseada em F28;

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

Quando se utiliza um domínio menor, 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 a 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 de domínio, operando apenas no domínio base, permitindo assim uma alta eficiência em domínios pequenos. No entanto, a verificação de pontos aleatórios e o cálculo de FRI ainda precisam aprofundar-se em uma extensão de domínio maior para garantir a segurança necessária.

Ao construir um sistema de provas com base em campos binários, existem 2 problemas práticos: ao calcular a representação de trace nos STARKs, o tamanho do campo 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 campo utilizado deve ser maior que o tamanho após a expansão da codificação.

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

2 Análise dos Princípios

A construção da maioria dos sistemas SNARKs atualmente geralmente inclui as seguintes duas partes:

• Prova de Oráculo Interativa Polinomial de Teoria da Informação (: PIOP): PIOP, como o núcleo do sistema de prova, transforma a relação de cálculo 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, permitindo que o verificador valide 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: PLONK PIOP, Spartan PIOP e HyperPlonk PIOP, cada um com diferentes maneiras de lidar com expressões polinomiais, impactando 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 uma equação polinomial gerada por 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 do polinômio. Os esquemas de compromisso polinomial comuns incluem KZG, Bulletproofs, FRI ( Fast Reed-Solomon IOPP ) e Brakedown, entre outros. Diferentes PCS possuem diferentes desempenhos, segurança e cenários de aplicação.

De acordo com as necessidades específicas, escolha diferentes PIOP e PCS e combine-os com um campo finito ou curva elíptica apropriados, podendo assim construir sistemas de prova com diferentes atributos. Por exemplo:

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

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

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 domínio binário (towers of binary fields) constitui a base de seus cálculos, permitindo a realização de operações simplificadas dentro do domínio binário. Em segundo lugar, Binius adaptou a verificação de produto e permutação do HyperPlonk em seu protocolo de prova Oracle interativo (PIOP), garantindo a verificação de consistência segura e eficiente entre variáveis e suas permutações. Terceiro, o protocolo introduziu uma nova prova de deslocamento multilinear, otimizando a eficiência da verificação de relações multilineares em pequenos domínios. Quarto, Binius adotou uma versão aprimorada da prova de busca Lasso, proporcionando flexibilidade e forte segurança ao mecanismo de busca. Finalmente, o protocolo utilizou um esquema de compromisso polinomial de pequeno domínio (Small-Field PCS), permitindo que ele implemente um sistema de prova eficiente no domínio binário e reduza as despesas geralmente associadas a grandes domínios.

( 2.1 Domínios finitos: aritmética baseada em torres de campos binários

Os campos binários em torre são a chave para a implementação de cálculos rápidos e verificáveis, principalmente devido a dois aspectos: cálculos eficientes e aritmética eficiente. Os campos 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 do campo binário apoia um processo aritmético simplificado, onde as operações realizadas no campo binário podem ser representadas em uma forma algébrica compacta e fácil de verificar. Essas características, juntamente com a capacidade de tirar pleno proveito de suas propriedades hierárquicas através da estrutura em torre, tornam os campos binários particularmente adequados para sistemas de prova escaláveis como o Binius.

O termo "canonical" refere-se à representação única e direta de elementos em um campo binário. Por exemplo, no campo binário mais básico F2, qualquer string de k bits pode ser mapeada diretamente para um elemento de campo binário de k bits. Isso é diferente dos campos primos, que não conseguem fornecer essa representação canônica dentro de uma quantidade fixa de bits. Embora um campo primo de 32 bits possa ser contido em 32 bits, nem toda string de 32 bits pode corresponder unicamente a um elemento de campo, enquanto o campo binário tem essa conveniência de mapeamento um-para-um. Nos campos primos Fp, métodos comuns de redução incluem a redução Barrett, a redução Montgomery e métodos de redução especiais para campos finitos específicos como Mersenne-31 ou Goldilocks-64. No campo binário F2k, métodos de redução comumente usados incluem a redução especial ), como usada no AES ###, a redução Montgomery (, como 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" aponta que, em operações de adição e multiplicação no campo binário, não há necessidade de levar em conta o transporte, e a operação de quadrado no campo binário é muito eficiente, pois segue a regra simplificada (X + Y )2 = X2 + Y 2.

Como mostrado na Figura 1, uma string de 128 bits: esta string pode ser interpretada de várias maneiras no contexto do domínio binário. Pode ser vista como um elemento único no domínio binário de 128 bits, ou ser analisada como dois elementos do domínio torre de 64 bits, quatro elementos do domínio torre de 32 bits, 16 elementos do domínio torre de 8 bits, ou 128 elementos do domínio F2. Essa flexibilidade de representação não requer nenhum custo computacional, apenas uma conversão de tipo da string de bits (typecast), que é uma propriedade muito interessante e útil. Ao mesmo tempo, elementos de pequeno domínio podem ser empacotados em elementos de domínio maior sem necessidade de custo computacional adicional. O protocolo Binius se aproveita 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 para a multiplicação, quadrado e operações de inversão em um domínio binário de torre de n bits ( que pode ser decomposto em um subdomínio de m bits ).

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

O design do PIOP no protocolo Binius foi inspirado no HyperPlonk e utiliza uma série de mecanismos de verificação essenciais para validar a correção de polinômios e conjuntos multivariados. Esses verificadores essenciais incluem:

1. GateCheck: Verificar se a testemunha secreta ω e a entrada pública x satisfazem a relação de cálculo do circuito C)x, ω###=0, para garantir o funcionamento correto do circuito.

2. PermutationCheck: Verifica se os resultados da avaliação dos 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 busca 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 vários conjuntos.

5. ProductCheck: Verificar 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 polinomial.

6. ZeroCheck: Verificar se um polinómio multivariável em um hipercubo booleano é zero em um ponto arbitrário ∏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 de avaliação de polinómios multivariáveis em uma avaliação de polinómios univariáveis, reduz a complexidade computacional para a parte de verificação. Além disso, o SumCheck também permite o processamento em lote, introduzindo números aleatórios para construir combinações lineares que possibilitam o processamento em lote de múltiplas instâncias de verificação de somas.

8. BatchCheck: Baseado em SumCheck, valida a correção da avaliação de múltiplos polinómios multivariáveis, para melhorar a eficiência do protocolo.

Apesar de Binius e HyperPlonk terem 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 que o produto seja 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 de divisão por zero: HyperPlonk não conseguiu lidar adequadamente com a situação de divisão por zero, resultando na impossibilidade de afirmar que U é diferente de zero no hipercubo; Binius tratou corretamente este problema, permitindo que o ProductCheck do Binius continuasse a processar mesmo quando o denominador é zero, permitindo a generalização para qualquer valor de produto.

• Verificação de Permutação em várias colunas: HyperPlonk não possui esta funcionalidade; Binius suporta a verificação de permutação entre várias colunas, permitindo que o Binius lide com situações de disposição polinomial mais complexas.

Assim, a Binius melhorou o mecanismo existente PIOPSumCheck, aumentando a flexibilidade e eficiência do protocolo, especialmente ao lidar com a validação de polinômios multivariáveis mais complexos, oferecendo um suporte funcional mais robusto. Essas melhorias não apenas resolveram as limitações do HyperPlonk, mas também estabeleceram as bases para futuros sistemas de prova baseados em campos binários.

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

No protocolo Binius, virtual