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

1 Introdução

Uma das principais razões para a baixa eficiência dos STARKs é que a maioria dos números em programas reais é pequena, mas para garantir a segurança das provas baseadas em árvores de Merkle, muitos valores de redundância adicionais ocupam todo o domínio ao usar codificação Reed-Solomon para expandir os dados, 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.

A largura de codificação dos STARKs de 1ª geração é de 252 bits, a largura de codificação dos STARKs de 2ª geração é de 64 bits, e a largura de codificação dos STARKs de 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 campo binário permite a operação direta em bits, com codificação compacta e eficiente, sem qualquer espaço desperdiçado, ou seja, os STARKs de 4ª geração.

Em comparação com as novas descobertas de 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 campo F2128;

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

• Protocólos originais FRI e zk-STARK, bem como a função de hash Grøstl, que chegou às finais 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ínios torna-se cada vez mais importante para garantir a segurança. O domínio binário utilizado pela Binius depende totalmente da extensão de domínios para assegurar a 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ínios, operando apenas no 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 de ser aprofundados em uma extensão de domínios maior, para garantir a segurança necessária.

Ao construir sistemas de prova baseados em domínios binários, existem 2 problemas práticos: ao calcular a representação de trace em STARKs, o tamanho do domínio deve ser maior do 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 do que o tamanho após a expansão da codificação.

Binius propôs uma solução inovadora que aborda essas duas questões 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 univariáveis, representando toda a trajetória de cálculo por meio de seus valores em "hipercubos"; em segundo lugar, devido ao comprimento de cada dimensão do hipercubo ser 2, não é possível realizar a extensão padrão de Reed-Solomon como nos STARKs, mas o hipercubo pode ser considerado como um quadrado, e a extensão de Reed-Solomon pode ser feita com base nesse quadrado. Este método, ao garantir a segurança, aumenta significativamente a eficiência da 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 Interativo Polinomial Baseada em Teoria da Informação (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP): O PIOP, como 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, 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 formas de lidar com 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, ao mesmo tempo em que 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 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 campo finito ou curva elíptica apropriada, para 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 combinado com FRI PCS e é baseado no domínio Goldilocks. Plonky2 foi projetado para realizar recursão eficiente. Ao projetar esses sistemas, o PIOP e o PCS escolhidos 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 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 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 campos binários constitui 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 de prova de Oracle interativo (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 na verificação de relações multilineares em pequenos domínios. Quarto, Binius utilizou uma versão aprimorada da prova de busca Lasso, proporcionando flexibilidade e forte segurança para o mecanismo de busca. Por fim, o protocolo emprega um esquema de compromisso polinomial de pequeno domínio (Small-Field PCS), permitindo a implementação de um sistema de provas eficiente no domínio binário 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 implementar 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 do domínio binário suporta um processo de aritmética simplificada, 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 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 elementos no 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 do campo primo, que não consegue fornecer essa representação canônica dentro de um número fixo de bits. Embora o campo 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 de campo, enquanto o campo binário possui essa conveniência de mapeamento um a um. No campo primo Fp, os 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 campos finitos específicos, como Mersenne-31 ou Goldilocks-64. No campo binário F2k, os métodos de redução comuns incluem reduções especiais (como usadas no AES), reduções de Montgomery (como usadas no POLYVAL) e reduções recursivas (como Tower). O artigo "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" aponta que no campo binário, tanto a adição quanto a multiplicação não requerem a introdução de transporte, e a operação de quadrado no campo binário é muito eficiente, pois segue a regra simplificada de (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 um domínio binário. Pode ser vista como um elemento único em um domínio binário de 128 bits, ou pode ser analisada como dois elementos de domínio de torre de 64 bits, quatro elementos de domínio de torre de 32 bits, dezesseis elementos de domínio de torre de 8 bits, ou 128 elementos do domínio F2. Essa flexibilidade de representação não requer sobrecarga computacional, sendo apenas uma conversão de tipo da string de bits, o que é uma propriedade muito interessante e útil. Ao mesmo tempo, elementos de domínio pequeno podem ser agrupados em elementos de domínio maiores sem necessidade de sobrecarga 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 de operações de multiplicação, quadrado e inversão em um domínio binário de torre de n bits (que pode ser decomposto em subdomínios de m bits).

2.2 PIOP: versão adaptada do HyperPlonk Product e PermutationCheck------aplicável ao domínio binário

O design do PIOP no protocolo Binius é inspirado no HyperPlonk e utiliza 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: Verifica se o testemunho secreto ω 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 das permutações entre as variáveis do polinómio.

3. LookupCheck: Verifica se a avaliação do polinómio está na tabela de consulta 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: 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 do polinómio.

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 da avaliação de polinómios multivariáveis em um problema de 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 possibilitam o processamento em lote de várias instâncias de verificação de somas.

8. BatchCheck: Baseado no SumCheck, valida 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 fez melhorias nas seguintes 3 áreas:

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

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

Assim, a Binius, através da melhoria do mecanismo existente PIOPSumCheck, aumentou a flexibilidade e a eficiência do protocolo, especialmente ao lidar com verificações de polinómios multivariados mais complexos, proporcionando 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 deslocamento multilinear ------ 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 de outros polinómios virtuais. Aqui estão dois métodos chave:

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