Análise dos princípios dos STARKs da Binius e reflexão 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, como os índices em loops for, valores booleanos, contadores, etc. No entanto, para garantir a segurança das provas baseadas em árvores de Merkle, ao expandir os dados com a codificação Reed-Solomon, muitos valores redundantes adicionais ocupam 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.

Como mostrado na Tabela 1, a largura de codificação dos STARKs de primeira geração é de 252 bits, a largura de codificação dos STARKs de segunda geração é de 64 bits, a largura de codificação dos STARKs de terceira geração é de 32 bits, mas a largura de codificação de 32 bits ainda apresenta um grande espaço desperdiçado. Em comparação, o domínio binário permite operações diretas sobre os bits, com uma codificação compacta e eficiente, sem qualquer espaço desperdiçado, ou seja, os STARKs de quarta geração.

Tabela 1: Caminhos de derivação de STARKs

| Geração | Largura de código | Sistema representativo | |------|----------|----------| | 1ª Geração | 252 bit | StarkWare STARKs | | 2ª geração | 64 bits | Plonky2 | | 3ª geração | 32 bits | BabyBear | | 4ª geração | 1 bit | Binius |

Em comparação com domínios finitos recentemente descobertos, 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 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 campo F2128;

• QR code, utilizando 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, que é 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 a sua segurança e viabilidade prática. A maioria dos polinómios envolvidos nos cálculos do Prover não precisa de entrar na extensão de domínio, mas apenas operar no domínio base, alcançando assim alta eficiência em domínios pequenos. No entanto, a verificação de pontos aleatórios e os cálculos FRI ainda precisam aprofundar-se em domínios de extensão maiores para garantir a segurança necessária.

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

Binius propôs uma solução inovadora que trata estas duas questões separadamente e representa os mesmos dados de duas maneiras diferentes: primeiro, usando um polinômio multivariável ( especificamente um polinômio multilinhar ) em vez de um polinômio univariável, representando toda a trajetória de cálculo através de seus valores em "hipercubos" (; em segundo lugar, como cada dimensão do hipercubo tem comprimento 2, não é possível realizar uma extensão padrão de Reed-Solomon como nos STARKs, mas é possível considerar o hipercubo como um quadrado ), realizando 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 de Princípios

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

• Provas de Oracle Interativo Polinomial Baseadas em Teoria da Informação (: PIOP): O PIOP, como núcleo do sistema de provas, transforma as relações computacionais de entrada em igualdades polinomiais verificáveis. Diferentes protocolos PIOP permitem que o provador envie polinômios gradualmente, interagindo com o verificador, de modo que o verificador possa validar se o cálculo está correto consultando os resultados da avaliação de um número reduzido de polinômios. Os protocolos PIOP existentes incluem: PIOP PLONK, PIOP Spartan e PIOP HyperPlonk, cada um com diferentes abordagens para o tratamento das 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 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 sobre o polinômio. Os esquemas de compromisso polinomial comuns incluem KZG, Bulletproofs, FRI(Fast Reed-Solomon IOPP) e Brakedown, entre outros. Diferentes PCS têm diferentes desempenhos, segurança e cenários de aplicação.

De acordo com as necessidades específicas, escolha diferentes PIOP e PCS, e combine com o domínio finito ou curva elíptica apropriada, podendo 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 trusted setup do protocolo ZCash.

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

Binius: HyperPlonk PIOP + Brakedown PCS + domínios binários. Especificamente, Binius inclui cinco tecnologias-chave para alcançar sua eficiência e segurança. Primeiro, a aritmética baseada em torres de domínios binários (towers of binary fields) forma a base de seus cálculos, permitindo 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 interativo de prova Oracle (PIOP), garantindo uma 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. Por fim, o protocolo utiliza um esquema de compromisso polinomial de pequenos domínios (Small-Field PCS), permitindo um sistema de prova eficiente sobre domínios binários e reduzindo a sobrecarga normalmente associada a grandes domínios.

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

Os domínios 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á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 a desempenho. Além disso, a estrutura do domínio binário suporta um processo de aritmética simplificado, ou seja, as operações realizadas sobre o domínio binário podem ser representadas de forma algébrica compacta e fácil de verificar. Essas características, juntamente com a capacidade de aproveitar plenamente suas características hierárquicas através da estrutura de torre, tornam os domínios binários especialmente adequados para sistemas de prova escaláveis como o Binius.

O termo "canônico" refere-se à representação única e direta de elementos no domínio binário. Por exemplo, no domínio binário mais básico F2, qualquer string de k bits pode ser mapeada diretamente para um elemento do domínio binário de k bits. Isso é diferente dos domínios primos, que não conseguem fornecer essa representação canônica dentro de um número fixo de bits. Embora o domínio primo de 32 bits possa ser incluído em 32 bits, nem toda string 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, métodos de redução comuns incluem a redução de Barrett, a redução de 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, métodos de redução comumente usados incluem a redução especial ), como usado no AES ###, a redução de Montgomery (, como usada no POLYVAL ), e a redução recursiva (, como na Tower ). O artigo "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" aponta que o domínio binário não necessita de transporte em operações de adição e multiplicação, e que a operação de quadrado no domínio 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 de campos binários. Pode ser vista como um elemento único no campo binário de 128 bits, ou ser interpretada como dois elementos de campo de torre de 64 bits, quatro elementos de campo de torre de 32 bits, 16 elementos de campo de torre de 8 bits, ou 128 elementos do campo F2. Essa flexibilidade de representação não requer nenhum custo computacional, apenas uma conversão de tipo da string de bits (typecast), o que é uma propriedade muito interessante e útil. Ao mesmo tempo, elementos de campo menores podem ser agrupados em elementos de campo maiores sem custo computacional adicional. O protocolo Binius aproveita essa 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 das operações de multiplicação, quadrado e inversão em campos de torre de n bits ( que podem ser decompostos em subcampos de m bits ).

Figura 1: Domínio binário em torre

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

O design do PIOP no protocolo Binius baseia-se 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 o testemunho secreto ω 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: Verificar se os resultados de avaliação dos dois polinómios multivariados f e g no hipercubo booleano constituem uma relação de permutação f(x) = f(π)x((, para garantir a consistência da disposição entre as variáveis polinomiais.

3. LookupCheck: Verificar se a avaliação do polinómio está na tabela de pesquisa dada, ou seja, f)Bµ) ⊆ T(Bµ), garantindo que certos valores estão dentro do intervalo especificado.

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 polinômios racionais no hipercubo booleano é igual a um valor declarado ∏x∈Hµ f(x) = s, a fim de garantir a correção do produto dos polinômios.

6. ZeroCheck: Verificar se um polinómio multivariável em um hipercubo booleano é zero em qualquer ponto ∏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 avaliação de polinómios univariáveis, reduz a complexidade computacional do validador. Além disso, o SumCheck também permite o processamento em lote, introduzindo números aleatórios para construir combinações lineares e realizar 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.

Apesar de Binius e HyperPlonk terem muitas semelhanças no design do protocolo, Binius faz melhorias nas seguintes 3 áreas:

• ProductCheck otimização: 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 este processo de verificação ao especializar esse valor para 1, reduzindo assim a complexidade computacional.

• Tratamento do problema da divisão por zero: o HyperPlonk não conseguiu lidar adequadamente com a situação de divisão por zero, levando à impossibilidade de afirmar que U é diferente de zero no hipercubo; o Binius tratou corretamente este problema, mesmo quando o denominador é zero, o ProductCheck do Binius pode 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, permitindo que Binius lide com situações de disposição polinomial mais complexas.

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

( 2.3 PIOP: novo argumento de mudança multilinear------aplicável