Título original encaminhado 'Vitalik explica Binius em detalhe: um sistema de prova eficiente baseado em campos binários'

Esta publicação destina-se principalmente a leitores que estejam mais ou menos familiarizados com a criptografia da era de 2019, especialmente SNARKs e STARKs. Se não estiver, recomendo que leia esses artigos primeiro. Um agradecimento especial a Justin Drake, Jim Posen, Benjamin Diamond e Radi Cojbasic pela colaboração e revisão.

Nos últimos dois anos, os STARKs tornaram-se uma tecnologia crucial e insubstituível para fazer de forma eficiente provas criptográficas fáceis de verificar de declarações muito complicadas (por exemplo, provar que um bloco Ethereum é válido). Uma das razões-chave é o tamanho pequeno do campo: enquanto os SNARKs baseados em curvas elípticas exigem que você trabalhe com inteiros de 256 bits para ser seguro o suficiente, os STARKs permitem que você use tamanhos de campo muito menores, que são mais eficientes: primeiro o campo Goldilocks (inteiros de 64 bits) e depois Mersenne31 e BabyBear (ambos de 31 bits). Graças a esses ganhos de eficiência, o Plonky2, que usa o Goldilocks, é centenas de vezes mais rápido na comprovação de muitos tipos de cálculos do que seus antecessores.

Uma pergunta natural a fazer é: podemos levar esta tendência à sua conclusão lógica, construindo sistemas de prova que funcionem ainda mais rapidamente operando diretamente sobre zeros e uns? É exatamente isso que o Binius está a tentar fazer, usando uma série de truques matemáticos que o tornam muito diferente dos SNARKs e STARKs de há três anos. Este artigo explora as razões pelas quais os campos pequenos tornam a geração de provas mais eficiente, por que os campos binários são singularmente poderosos e os truques que o Binius usa para fazer com que as provas sobre campos binários funcionem de forma tão eficaz.

Binius. Até ao final deste post, deverá ser capaz de compreender cada parte deste diagrama.

Recap: campos finitos

Uma das tarefas-chave de um sistema de prova criptográfica é operar sobre grandes quantidades de dados, mantendo os números pequenos. Se puder comprimir uma declaração sobre um grande programa num equação matemática envolvendo poucos números, mas esses números forem tão grandes quanto o programa original, não terá ganhado nada.

Para fazer aritmética complicada mantendo os números pequenos, os criptógrafos geralmente usam aritmética modular. Escolhemos um certo número primo 'módulo' p. O operador % significa 'pegar o resto de': 15 % 7=1, 53 % 10=3, etc (note que a resposta é sempre não negativa, então, por exemplo, −1 % 10=9).

Provavelmente já viu aritmética modular, no contexto de adição e subtração de tempo (por exemplo, que horas são quatro horas após as 9:00?). Mas aqui, não apenas adicionamos e subtraímos módulo de algum número, também multiplicamos, dividimos e tomamos exponenciais.

Nós redefinimos:

As regras acima são todas autoconsistentes. Por exemplo, se p=7, então:

5+3=1 (because 8%7=1)

1-3=5 (porque -2%7=5)

2*5=3

3/5=2

Um termo mais geral para este tipo de estrutura é um campo finito. Um campo finito é uma estrutura matemática que obedece às leis usuais da aritmética, mas onde há um número limitado de valores possíveis, e assim cada valor pode ser representado em um tamanho fixo.

Aritmética modular (ou campos primos) é o tipo mais comum de campo finito, mas também existe outro tipo: campos de extensão. Você provavelmente já viu um campo de extensão antes: os números complexos. Nós “imaginamos” um novo elemento, que rotulamos como 𝑖, e declaramos que satisfaz 𝑖2=−1. Você pode então tomar qualquer combinação de números regulares e 𝑖, e fazer matemática com isso: (3𝑖+2)∗(2𝑖+4)= 6𝑖2+12𝑖+4𝑖+8=16𝑖+2. Podemos de forma semelhante fazer extensões de campos primos. Conforme começamos a trabalhar com campos menores, as extensões de campos primos tornam-se cada vez mais importantes para preservar a segurança, e os campos binários (que a Binius utiliza) dependem inteiramente de extensões para ter utilidade prática.

Recap: aritmetização

A maneira como SNARKs e STARKs provam coisas sobre programas de computador é através da aritmetização: converte-se uma declaração sobre um programa que se pretende provar numa equação matemática envolvendo polinómios. Uma solução válida para a equação corresponde a uma execução válida do programa.

Para dar um exemplo simples, suponha que eu tenha calculado o 100º número de Fibonacci e queira provar para você qual é. Eu crio um polinómio 𝐹 que codifica os números de Fibonacci: assim 𝐹(0)=𝐹(1)=1, 𝐹(2)=2, 𝐹(3)=3, 𝐹(4)=5, e assim por diante por 100 passos. A condição que eu preciso provar é que 𝐹(𝑥+2)=𝐹(𝑥)+𝐹(𝑥+1) ao longo do intervalo 𝑥={0,1…98}. Posso convencer você disso dando-lhe o quociente:

onde Z(x) = (x-0) (x-1)…(x-98). . Se eu puder provar que existe F e H que satisfazem esta equação, então F deve satisfazer F(x+2)-F(x+1)-F(x) no intervalo. Se eu verificar adicionalmente que F é satisfeito, F(0)=F(1)=1, então F(100) deve ser realmente o 100º número de Fibonacci.

Se quiser provar algo mais complicado, então substitua a relação “simples” 𝐹(𝑥+2)=𝐹(𝑥)+𝐹(𝑥+1) por uma equação mais complicada, que basicamente diz “𝐹(𝑥+1) é a saída de inicializar uma máquina virtual com o estado 𝐹(𝑥) e executar um passo computacional”. Também pode substituir o número 100 por um número maior, por exemplo, 100000000, para acomodar mais passos.

Todos os SNARKs e STARKs são baseados nesta ideia de usar uma equação simples sobre polinômios (ou às vezes vetores e matrizes) para representar um grande número de relações entre valores individuais. Nem todos envolvem a verificação da equivalência entre passos computacionais adjacentes da mesma forma que acima: o PLONK não o faz, por exemplo, e o R1CS também não. Mas muitos dos mais eficientes o fazem, pois a imposição da mesma verificação (ou das mesmas poucas verificações) muitas vezes torna mais fácil minimizar a sobrecarga.

Plonky2: de SNARKs de 256 bits e STARKs para 64 bits… apenas STARKs

Há cinco anos, um resumo razoável dos diferentes tipos de prova de conhecimento zero era o seguinte. Existem dois tipos de provas: (baseadas em curvas elípticas) SNARKs e (baseadas em hash) STARKs. Tecnicamente, STARKs são um tipo de SNARK, mas na prática é comum usar "SNARK" para se referir apenas à variedade baseada em curvas elípticas e "STARK" para se referir às construções baseadas em hash. SNARKs são pequenos, e assim você pode verificá-los muito rapidamente e ajustá-los facilmente à cadeia. STARKs são grandes, mas não requerem configurações confiáveis, e são resistentes a ataques quânticos.

STARKs funcionam tratando os dados como um polinómio, calculando avaliações desse polinómio em vários pontos e usando a raiz de Merkle desses dados estendidos como o "compromisso polinomial"

Um ponto chave da história aqui é que as SNARKs baseadas em curvas elípticas vieram a ser amplamente utilizadas primeiro: demorou até aproximadamente 2018 para que as STARKs se tornassem suficientemente eficientes para serem usadas, graças a FRI, e nessa altura a Zcash já estava em funcionamento há mais de um ano. As SNARKs baseadas em curvas elípticas têm uma limitação chave: se você quiser usar SNARKs baseadas em curvas elípticas, então a aritmética nestas equações deve ser feita com inteiros módulo o número de pontos na curva elíptica. Este é um número grande, geralmente próximo de 2256: por exemplo, para a curva bn128, é 21888242871839275222246405745257275088548364400416034343698204186575808495617. Mas o cálculo real está usando números pequenos: se você pensar sobre um programa “real” na sua linguagem favorita, a maior parte do que está a ser trabalhada são contadores, índices em loops, posições no programa, bits individuais representando Verdadeiro ou Falso, e outras coisas que quase sempre terão apenas alguns dígitos de comprimento.

Mesmo que os seus dados “originais” sejam compostos por números “pequenos”, o processo de comprovação requer o cálculo de quocientes, extensões, combinações lineares aleatórias e outras transformações dos dados, o que leva a um número igual ou maior de objetos que, em média, são tão grandes quanto o tamanho total do seu campo. Isso cria uma ineficiência-chave: para provar um cálculo sobre n valores pequenos, é necessário fazer ainda mais cálculos sobre n valores muito maiores. A princípio, os STARKs herdaram o hábito de usar campos de 256 bits dos SNARKs e, portanto, sofreram da mesma ineficiência.

Uma extensão de Reed-Solomon de algumas avaliações polinomiais. Embora os valores originais sejam pequenos, os valores extras todos explodem para o tamanho total do campo (neste caso, 2 elevado à potência 31 -1)

Em 2022, Plonky2 foi lançado. A principal inovação do Plonky2 foi fazer aritmética módulo um primo menor: 2⁶⁴−2³²+1=18446744069414584321. Agora, cada adição ou multiplicação pode sempre ser feita em apenas algumas instruções em uma CPU, e a hash de todos os dados juntos é 4x mais rápida do que antes. Mas isso vem com uma pegadinha: este método é exclusivo do STARK. Se você tentar usar um SNARK, com uma curva elíptica de tamanho tão pequeno, a curva elíptica se torna insegura.

Para continuar a ser seguro, Plonky2 também precisava de introduzir campos de extensão. Uma técnica chave na verificação de equações aritméticas é o “amostragem num ponto aleatório”: se quiser verificar se 𝐻(𝑥)∗𝑍(𝑥) realmente é igual a 𝐹(𝑥+2)−𝐹(𝑥+1)−𝐹(𝑥), pode escolher alguma coordenada aleatória 𝑟, fornecer provas de abertura de compromisso de polinómio provando 𝐻(𝑟), 𝑍(𝑟), 𝐹(𝑟), 𝐹(𝑟+1) e 𝐹(𝑟+2), e depois verificar se 𝐻(𝑟)∗𝑍(𝑟) é igual a 𝐹(𝑟+2)−𝐹(𝑟+1)−𝐹(𝑟). Se o atacante conseguir adivinhar a coordenada antecipadamente, o atacante pode enganar o sistema de prova - daí a necessidade de ser aleatório. Mas isso também significa que a coordenada deve ser amostrada de um conjunto suficientemente grande para que o atacante não a consiga adivinhar por acaso. Se o módulo estiver perto de 2²⁵⁶, este é claramente o caso. Mas com um módulo de 2⁶⁴−2³²+1, ainda não estamos lá, e se baixarmos para 2³¹−1, definitivamente não é o caso. Tentar falsificar uma prova duas mil milhões de vezes até que se tenha sorte está absolutamente dentro do alcance das capacidades de um atacante.

Para parar isto, amostramos 𝑟 de um campo de extensão. Por exemplo, você pode definir 𝑦 onde 𝑦³=5, e fazer combinações de 1, 𝑦 e 𝑦². Isto aumenta o número total de coordenadas para cerca de 2⁹³. A maioria dos polinómios calculados pelo provador não entram neste campo de extensão; eles apenas usam inteiros módulo 2³¹−1 e assim ainda obtém todas as eficiências de usar o campo pequeno. Mas a verificação do ponto aleatório e o cálculo do FRI mergulham neste campo maior, a fim de obter a segurança necessária.

Dos pequenos primos ao binário

Os computadores realizam cálculos representando números maiores como sequências de zeros e uns e construindo 'circuitos' com base nesses bits para calcular coisas como adição e multiplicação. Os computadores são especialmente otimizados para fazer cálculos com inteiros de 16 bits, 32 bits e 64 bits. Módulos como 2⁶⁴−2³²+1 e 2³¹−1 são escolhidos não apenas porque se encaixam dentro desses limites, mas também porque se alinham bem com esses limites: você pode fazer multiplicação módulo 2⁶⁴−2³²+1 fazendo multiplicação regular de 32 bits e deslocando e copiando as saídas bitwise em alguns lugares; este artigo explica bem alguns dos truques.

O que seria ainda melhor, no entanto, seria fazer cálculos em binário diretamente. E se a adição pudesse ser apenas XOR, sem a necessidade de se preocupar com o 'transporte' do overflow de adicionar 1 + 1 em uma posição de bit para a próxima posição de bit? E se a multiplicação pudesse ser mais paralelizável da mesma forma? E todas essas vantagens viriam além de poder representar valores Verdadeiro/Falso com apenas um bit.

Capturar diretamente essas vantagens de fazer computação binária é exatamente o que Binius está tentando fazer. Uma tabela da apresentação do zkSummit da equipe Binius mostra os ganhos de eficiência:

Apesar de terem aproximadamente o mesmo “tamanho”, uma operação de campo binário de 32 bits consome 5 vezes menos recursos computacionais do que uma operação sobre o campo Mersenne de 31 bits.

De polinómios univariados a hipercubos

Suponhamos que estamos convencidos por este raciocínio e queremos fazer tudo sobre bits (zeros e uns). Como nos comprometemos realmente com um polinómio que representa um bilião de bits?

Aqui, enfrentamos dois problemas práticos:

1. Para que um polinómio represente muitos valores, esses valores precisam de ser acessíveis nas avaliações do polinómio: no nosso exemplo de Fibonacci acima, 𝐹(0), 𝐹(1) … 𝐹(100), e numa computação maior, os índices iriam até aos milhões. E o campo que usamos precisa de conter números até esse tamanho.

2. Provar qualquer coisa sobre um valor ao qual estamos a comprometer-nos numa árvore de Merkle (como todos os STARKs fazem) requer codificá-lo de Reed-Solomon: estendendo 𝑛 valores em, por exemplo, 8𝑛 valores, usando a redundância para impedir um provador malicioso de fazer batota ao falsificar um valor no meio do cálculo. Isto também requer ter um campo suficientemente grande: para estender um milhão de valores para 8 milhões, é necessário ter 8 milhões de pontos diferentes nos quais avaliar o polinómio.

Uma ideia-chave em Binius é resolver esses dois problemas separadamente, e fazê-lo representando os mesmos dados de duas maneiras diferentes. Primeiro, o polinômio em si. SNARKs baseados em curvas elípticas, STARKs da era 2019, Plonky2 e outros sistemas geralmente lidam com polinômios sobre uma variável: F(x). Binius, por outro lado, inspira-se no protocolo espartano e trabalha com polinômios multivariados: F(x1,x2... xk). Na verdade, representamos todo o traço computacional no "hipercubo" de avaliações onde cada xi é 0 ou 1. Por exemplo, se quiséssemos representar uma sequência de números de Fibonacci, e ainda estivéssemos usando um campo grande o suficiente para representá-los, poderíamos visualizar os primeiros dezesseis deles como sendo algo assim:

Ou seja, 𝐹(0,0,0,0) seria 1, 𝐹(1,0,0,0) também seria 1, 𝐹(0,1,0,0) seria 2, e assim por diante, até chegarmos a 𝐹(1,1,1,1)=987. Dado um hipercubo de avaliações, há exatamente um polinómio multilinear (grau 1 em cada variável) que produz essas avaliações. Assim, podemos pensar nesse conjunto de avaliações como representando o polinómio; nunca precisamos realmente incomodar-nos em calcular os coeficientes.

Este exemplo é, naturalmente, apenas para ilustração: na prática, o objetivo de ir para um hipercubo é permitir-nos trabalhar com bits individuais. A forma “Binius-native” de contar números de Fibonacci seria usar um cubo de dimensão superior, utilizando cada conjunto de, por exemplo, 16 bits para armazenar um número. Isso requer alguma engenhosidade para implementar a adição de inteiros em cima dos bits, mas com o Binius não é muito difícil.

Agora, chegamos à codificação de apagamento. A maneira como os STARKs funcionam é: você pega 𝑛 valores, estende-os com Reed-Solomon para um maior número de valores (geralmente 8𝑛, normalmente entre 2𝑛 e 32𝑛), e depois seleciona aleatoriamente alguns ramos de Merkle da extensão e realiza algum tipo de verificação neles. Um hipercubo tem comprimento 2 em cada dimensão. Portanto, não é prático estendê-lo diretamente: não há espaço suficiente para amostrar ramos de Merkle a partir de 16 valores. Então, o que fazemos em vez disso? Fingimos que o hipercubo é um quadrado!

Simple Binius - um exemplo

Ver aquipara uma implementação em Python deste protocolo.

Vamos passar por um exemplo, usando inteiros regulares como nosso campo para conveniência (em uma implementação real, isso será elementos de campo binário). Primeiro, pegamos o hipercubo ao qual queremos nos comprometer e o codificamos como um quadrado:

Agora, estendemos o Reed-Solomon para o quadrado. Ou seja, tratamos cada linha como sendo um polinómio de grau 3 avaliado em x = {0, 1, 2, 3}, e avaliamos o mesmo polinómio em x = {4, 5, 6, 7}:

Repare que os números aumentam rapidamente! É por isso que, numa implementação real, usamos sempre um campo finito para isso, em vez de inteiros regulares: se usássemos inteiros módulo 11, por exemplo, a extensão da primeira linha seria apenas [3, 10, 0, 6].

Se quiser brincar com a extensão e verificar os números por si próprio, pode usar meu código de extensão Reed-Solomon simples aqui.

A seguir, tratamos esta extensão como colunas e fazemos uma árvore de Merkle das colunas. A raiz da árvore de Merkle é o nosso compromisso.

Agora, vamos supor que o provador queira provar uma avaliação desse polinômio em algum momento r={r0,r1,r2,r3}. Há uma nuance em Binius que o torna um pouco mais fraco do que outros esquemas de compromisso polinomial: o provador não deve saber, ou ser capaz de adivinhar, s, até depois de se comprometer com a raiz de Merkle (em outras palavras, r deve ser um valor pseudoaleatório que depende da raiz de Merkle). Isso torna o esquema inútil para "pesquisa de banco de dados" (por exemplo. "ok você me deu a raiz Merkle, agora me prove P(0,0,1,0)!"). Mas os protocolos reais de prova de conhecimento zero que usamos geralmente não precisam de "pesquisa de banco de dados"; eles simplesmente precisam verificar o polinômio em um ponto de avaliação aleatório. Portanto, esta restrição é aceitável para os nossos propósitos.

Suponhamos que escolhemos 𝑟={1,2,3,4} (o polinómio, neste ponto, avalia-se em −137; pode confirmarcom este código). Agora, entramos no processo de realmente fazer a prova. Dividimos 𝑟 em duas partes: a primeira parte {1,2} representando uma combinação linear de colunas dentro de uma linha, e a segunda parte {3,4} representando uma combinação linear de linhas. Calculamos um “produto tensorial”, tanto para a parte da coluna:

E para a parte da fila:

O que isto significa é: uma lista de todos os possíveis produtos de um valor de cada conjunto. No caso da linha, obtemos:

[(1-r2)(1-r3), (1-r3), (1-r2)r3, r2*r3]

Use r={1,2,3,4} (então r2=3 e r3=4):

[(1-3)(1-4), 3(1-4),(1-3)4,34] = [6, -9 -8 -12]

Agora, calculamos uma nova “linha” 𝑡′, ao tomar esta combinação linear das linhas existentes. Ou seja, tomamos:

Você pode ver o que está acontecendo aqui como uma avaliação parcial. Se multiplicássemos o produto tensorial completo ⨂𝑖=03(1−𝑟𝑖,𝑟𝑖) pelo vetor completo de todos os valores, obteríamos a avaliação 𝑃(1,2,3,4)=−137. Aqui estamos multiplicando um produto tensorial parcial que usa apenas metade das coordenadas de avaliação, e estamos reduzindo uma grade de 𝑁 valores para uma linha de 𝑁 valores. Se você der esta linha a outra pessoa, ela pode usar o produto tensorial da outra metade das coordenadas de avaliação para completar o restante do cálculo.

O provador fornece ao verificador esta nova linha, 𝑡′, bem como as provas de Merkle de algumas colunas amostradas aleatoriamente. Isto é 𝑂(𝑁) dados. No nosso exemplo ilustrativo, o provador fornecerá apenas a última coluna; na vida real, o provador precisaria fornecer algumas dezenas de colunas para alcançar segurança adequada.

Agora, tiramos proveito da linearidade dos códigos de Reed-Solomon. A propriedade-chave que usamos é: fazer uma combinação linear de uma extensão de Reed-Solomon dá o mesmo resultado que uma extensão de Reed-Solomon de uma combinação linear. Esse tipo de “independência de ordem” frequentemente acontece quando você tem duas operações que são ambas lineares.

O verificador faz exatamente isso. Eles calculam a extensão de 𝑡′ e calculam a mesma combinação linear de colunas que o provador calculou anteriormente (mas apenas para as colunas fornecidas pelo provador) e verificam se esses dois procedimentos dão a mesma resposta.

Neste caso, ao estender 𝑡′ e calcular a mesma combinação linear ([6,−9,−8,12]) da coluna, ambos dão a mesma resposta: −10746. Isso prova que a raiz de Merkle foi construída "de boa fé" (ou pelo menos "suficientemente próxima"), e corresponde a 𝑡′: pelo menos a grande maioria das colunas são compatíveis entre si e com 𝑡′.

Mas o verificador ainda precisa verificar mais uma coisa: verificar realmente a avaliação do polinómio em {𝑟0..𝑟3}. Até agora, nenhum dos passos do verificador dependia realmente do valor que o provador afirmou. Aqui está como fazemos essa verificação. Tomamos o produto tensorial daquilo a que chamamos a parte "coluna" do ponto de avaliação:

No nosso exemplo, onde r={1,2,3,4} então metade da coluna selecionada é {1,2}), isto é igual a:

Então agora tomamos esta combinação linear de 𝑡′:

Que é exatamente igual à resposta que se obtém ao avaliar o polinômio diretamente.

O acima está muito próximo de uma descrição completa do protocolo Binius "simples". Isso já tem algumas vantagens interessantes: por exemplo, porque os dados são divididos em linhas e colunas, você só precisa de um campo com metade do tamanho. Mas isso está longe de perceber todos os benefícios de fazer cálculos em binário. Para isso, precisaremos do protocolo Binius completo. Mas primeiro, vamos obter uma compreensão mais profunda dos campos binários.

Campo binário

O campo mais pequeno possível é a aritmética módulo 2, que é tão pequena que podemos escrever as suas tabelas de adição e multiplicação:

Podemos fazer campos binários maiores através de extensões: se começarmos com 𝐹2 (inteiros módulo 2) e depois definirmos 𝑥 onde 𝑥2=𝑥+1, obtemos a seguinte tabela de adição e multiplicação:

Acontece que podemos expandir o campo binário para tamanhos arbitrariamente grandes repetindo esta construção. Ao contrário dos números complexos sobre os reais, onde você pode adicionar um novo elemento 𝑖, mas não pode adicionar mais nenhum (os quatérnions existem, mas são matematicamente estranhos, por exemplo, 𝑎𝑏≠𝑏𝑎), com campos finitos você pode continuar adicionando novas extensões para sempre. Especificamente, definimos os elementos da seguinte forma:

E assim por diante. Isso é frequentemente chamado de construção da torre, porque cada extensão sucessiva pode ser vista como adicionando uma nova camada a uma torre. Esta não é a única maneira de construir campos binários de tamanho arbitrário, mas tem algumas vantagens únicas das quais o Binius tira proveito.

Podemos representar esses números como uma lista de bits, por exemplo, 1100101010001111. O primeiro bit representa múltiplos de 1, o segundo bit representa múltiplos de 𝑥0, em seguida, bits subsequentes representam múltiplos de: 𝑥1, 𝑥1∗𝑥0, 𝑥2, 𝑥2∗𝑥0 e assim por diante. Esta codificação é boa porque você pode decompor isso:

Esta é uma notação relativamente incomum, mas gosto de representar elementos de campo binário como inteiros, considerando a representação de bits em que os bits mais significativos estão à direita. Ou seja, 1=1, 𝑥₀=01=2, 1+𝑥₀=11=3, 1+𝑥₀+𝑥₂=11001000=19 e assim por diante. 1100101010001111 é, nesta representação, 61779.

A adição num campo binário é apenas XOR (assim como a subtração, aliás); note que isto significa que x+x=0 para qualquer x. Para multiplicar dois elementos x*y, existe um algoritmo recursivo muito simples: dividir cada número ao meio:

Em seguida, divida a multiplicação:

A última peça é a única um pouco complicada, porque tem que aplicar a regra de redução e substituir 𝑅𝑥∗𝑅𝑦∗𝑥𝑘2 por 𝑅𝑥∗𝑅𝑦∗(𝑥𝑘−1∗𝑥𝑘+1). Existem maneiras mais eficientes de fazer multiplicação, análogas ao algoritmo de Karatsuba e às transformadas rápidas de Fourier, mas deixarei como exercício para o leitor interessado descobrir isso.

A divisão em campos binários é feita combinando multiplicação e inversão. A maneira "simples, mas lenta" de fazer a inversão é uma aplicação do pequeno teorema de Fermat generalizado. Também existe um algoritmo de inversão mais complicado, mas mais eficiente, que você pode encontrar aquiPode usaro código aquipara brincar com a adição, multiplicação e divisão de campo binário por si mesmo.

Esquerda: tabela de adição para elementos de campo binário de quatro bits (ou seja, elementos compostos apenas por combinações de 1, 𝑥₀，𝑥₁ e 𝑥₀𝑥₁.

Certo: tabela de multiplicação para elementos do campo binário de quatro bits.

A coisa bonita sobre este tipo de campo binário é que combina algumas das melhores partes dos inteiros "regulares" e da aritmética modular. Como os inteiros regulares, os elementos do campo binário são ilimitados: você pode continuar estendendo o quanto quiser. Mas, como a aritmética modular, se você fizer operações com valores dentro de um limite de tamanho, todas as suas respostas também permanecem dentro do mesmo limite. Por exemplo, se você tomar potências sucessivas de 42, você obtém:

Após 255 passos, estás de volta aos 42²⁵⁵= 1. Tal como os inteiros positivos e a aritmética modular, eles seguem as leis matemáticas habituais: ab=ba, a(b+c)=a b+a*c, há até algumas leis novas estranhas.

Finalmente, os campos binários tornam fácil lidar com bits: se fizer matemática com números que cabem 2^kbits, então toda a sua saída também caberá em 2 k bits. Isso evita constrangimentos. No EIP-4844 do Ethereum, cada "bloco" de um blob deve ser um módulo digital 52435875175126190479447740508185965837690552500527637822603658699938581184513, então codificar os dados binários requer descartar algum espaço e fazer uma verificação adicional para garantir que cada elemento armazene um valor inferior a 2²⁴⁸. Isto também significa que as operações de campo binário são super rápidas em computadores - tanto CPUs quanto designs teoricamente ótimos de FPGA e ASIC.

O que tudo isto significa é que podemos fazer algo semelhante à codificação de Reed-Solomon que fizemos acima, de uma forma que evita completamente a “explosão” de inteiros, como vimos no nosso exemplo, e de uma forma muito “explodindo”. Forma “nativa”, o tipo de computação que os computadores são bons. O atributo “split” dos campos binários - como fazemos isso 1100101010001111=11001010+10001111*x₃e depois dividi-lo de acordo com as nossas necessidades também é crucial para alcançar muita flexibilidade.

Full Binius

Ver aquipara uma implementação em Python deste protocolo.

Agora, podemos chegar ao “Binius completo”, que ajusta o “Binius simples” para (i) funcionar sobre campos binários e (ii) nos permitir comprometer-nos com bits individuais. Este protocolo é complicado de entender, porque continua a voltar atrás e para a frente entre diferentes maneiras de olhar para uma matriz de bits; certamente demorou-me mais tempo a entender do que o habitual para entender um protocolo criptográfico. Mas uma vez que entenda os campos binários, a boa notícia é que não há “matemática mais difícil” de que o Binius dependa. Isto não são emparelhamentos de curvas elípticas, onde há buracos de coelho cada vez mais profundos de geometria algébrica para explorar; aqui, os campos binários são tudo o que precisa.

Vamos olhar novamente para o diagrama completo:

Neste momento, já deve estar familiarizado com a maioria dos componentes. A ideia de "aplanar" um hipercubo numa grelha, a ideia de calcular uma combinação de linhas e uma combinação de colunas como produtos tensoriais do ponto de avaliação, e a ideia de verificar a equivalência entre "Reed-Solomon estendendo e depois calculando a combinação de linhas", e "calculando a combinação de linhas e depois estendendo Reed-Solomon", estavam todos no simples Binius.

Quais são as novidades no “Binius completo”? Basicamente três coisas:

• Os valores individuais no hipercubo e no quadrado têm de ser bits (0 ou 1)
• O processo de extensão estende bits em mais bits, agrupando bits em colunas e fingindo temporariamente que são elementos de campo maiores
• Após o passo de combinação de linhas, há um passo de "decomposição em bits" elemento a elemento, que converte a extensão de volta em bits

Vamos passar por ambos por sua vez. Primeiro, o novo procedimento de extensão. Um código Reed-Solomon tem a limitação fundamental de que, se estiver a estender 𝑛 valores para 𝑘∗𝑛 valores, precisa de trabalhar num campo que tenha 𝑘∗𝑛 valores diferentes que possa usar como coordenadas. Com 𝐹₂ (aka, bits), você não pode fazer isso. E então o que fazemos é, "embalamos" F adjacente₂em elementos maiores. No exemplo aqui, estamos empacotando dois bits de cada vez em elementos em {0,1,2,3}, porque a nossa extensão só tem quatro pontos de avaliação e isso é suficiente para nós. Num prova “real”, provavelmente empacotaríamos 16 bits de uma vez. Em seguida, fazemos o código Reed-Solomon sobre esses valores empacotados e desempacotamo-los novamente em bits.

Agora, a combinação da linha. Para tornar as verificações de “avaliar num ponto aleatório” criptograficamente seguras, precisamos que esse ponto seja amostrado a partir de um espaço bastante grande, muito maior do que o hipercubo em si. Assim, enquanto os pontos dentro do hipercubo são bits, as avaliações fora do hipercubo serão muito maiores. No nosso exemplo acima, a “combinação da linha” acaba sendo [11,4,6,1].

Isto apresenta um problema: sabemos como combinar pares de bits num valor maior e depois fazer uma extensão de Reed-Solomon sobre isso, mas como fazemos o mesmo com pares de valores muito maiores?

O truque em Binius é fazê-lo bit a bit: olhamos para os bits individuais de cada valor (por exemplo, para o que rotulamos como "11", isso é [1,1,0,1]), e depois estendemos linha a linha. Ou seja, realizamos o procedimento de extensão na linha 1 de cada elemento, depois na linha 𝑥0, depois no "𝑥"₁"linha, depois no 𝑥₀∗𝑥₁linha e assim por diante (bem, no nosso exemplo simplificado, paramos aí, mas numa implementação real iríamos até 128 linhas (sendo a última a 𝑥₆∗ …∗ 𝑥₀))

Recapitulando:

• Nós pegamos os bits no hipercubo e convertemo-los numa grelha
• Então, tratamos grupos adjacentes de bits em cada linha como elementos de campo maiores e realizamos operações aritméticas neles para estender as linhas de Reed-Solomon
• Em seguida, pegamos uma combinação de linha de cada coluna de bits e obtemos uma coluna de bits (para quadrados maiores que 4x4, muito menores) para cada linha como saída
• Em seguida, olhamos para a saída como uma matriz e tratamos os bits como linhas novamente

Por que é que isto funciona? Na matemática “normal”, a capacidade de (muitas vezes) realizar operações lineares em qualquer ordem e obter o mesmo resultado pára de funcionar se começar a dividir um número por dígitos. Por exemplo, se começar com o número 345 e o multiplicar por 8 e depois por 3, obterá 8280, e se fizer essas duas operações ao contrário, também obterá 8280. Mas se inserir uma operação de “divisão por dígito” entre os dois passos, isso falha: se fizer 8x e depois 3x, obterá:

Mas se você fizer 3x, e depois 8x, você obtém:

Mas num campo binário construído com uma estrutura de torre, esta abordagem funciona. A razão reside na sua separabilidade: se multiplicar um valor grande por um valor pequeno, o que acontece em cada segmento fica em cada segmento. Se multiplicarmos 1100101010001111 por 11, isto é o mesmo que a primeira fatorização de 1100101010001111, que é

E depois multiplicando cada componente separadamente por 11.

Colocando tudo junto

Geralmente, os sistemas de prova do conhecimento zero funcionam fazendo afirmações sobre polinómios que representam simultaneamente afirmações sobre as avaliações subjacentes: tal como vimos no exemplo de Fibonacci, 𝐹(𝑋+2)−𝐹(𝑋+1)−𝐹(𝑋)=𝑍(𝑋)∗𝐻(𝑋) verifica simultaneamente todos os passos do cálculo de Fibonacci. Verificamos afirmações sobre polinómios provando avaliações num ponto aleatório. Esta verificação num ponto aleatório serve para verificar o polinómio inteiro: se a equação polinomial não corresponder, a probabilidade de coincidir num coordenada aleatória específica é mínima.

Na prática, uma fonte importante de ineficiência vem do facto de que, nos programas reais, a maioria dos números com que trabalhamos são pequenos: índices em loops for, valores Verdadeiro/Falso, contadores e coisas semelhantes. Mas quando “estendemos” os dados usando a codificação Reed-Solomon para lhes dar a redundância necessária para tornar seguras as verificações baseadas em prova de Merkle, a maioria dos valores “extras” acaba por ocupar o tamanho completo de um campo, mesmo que os valores originais sejam pequenos.

Para contornar isso, queremos tornar o campo o mais pequeno possível. O Plonky2 fez-nos passar de números de 256 bits para números de 64 bits, e depois o Plonky3 foi ainda mais longe, para 31 bits. Mas mesmo assim, isso é subótimo. Com campos binários, podemos trabalhar com bits individuais. Isso torna a codificação 'densa': se os seus dados subjacentes reais têm n bits, então a sua codificação terá n bits, e a extensão terá 8 * n bits, sem qualquer sobrecarga extra.

Agora, vamos olhar para o diagrama pela terceira vez:

Em Binius, comprometemo-nos com um polinómio multilinear: um hipercubo 𝑃(x₀,x₁,…x_k) , onde as avaliações individuais 𝑃(0,0…0), 𝑃(0,0…1) até 𝑃(1,1,…1) estão a manter os dados que nos interessam. Para provar uma avaliação num ponto, nós “re-interpretamos” os mesmos dados como um quadrado. Em seguida, estendemos cada linha, usando codificação Reed-Solomon sobre grupos de bits, para dar aos dados a redundância necessária para que as consultas aleatórias de ramos de Merkle sejam seguras. Depois calculamos uma combinação linear aleatória de linhas, com coeficientes projetados de forma que a nova linha combinada realmente contenha a avaliação que nos interessa. Tanto esta nova linha criada (que é re-interpretada como 128 linhas de bits), como algumas colunas selecionadas aleatoriamente com ramos de Merkle, são passadas para o verificador.

O verificador então faz uma 'combinação de linha da extensão' (ou melhor, algumas colunas da extensão), e uma 'extensão da combinação de linha', e verifica que as duas coincidem. Em seguida, eles calculam uma combinação de coluna e verificam se retorna o valor que o provador está alegando. E aí está o nosso sistema de prova (ou melhor, o esquema de compromisso polinomial, que é o principal bloco de construção de um sistema de prova).

O que é que nós não cobrimos?

• Algoritmos eficientes para estender as linhas, que são necessárias para realmente tornar a eficiência computacional do verificador. Usamos transformadas rápidas de Fourier sobre campos binários, descritas aqui(embora a implementação exata seja diferente, porque este post usa uma construção menos eficiente não baseada em extensão recursiva).
• Aritmetização. Os polinómios univariados são convenientes porque pode fazer coisas como F(X+2)-F(X+1)-F(X) = Z(X)*H(X) para relacionar passos adjacentes no cálculo. Num hipercubo, 'o próximo passo' é muito menos interpretável do que 'X+1'. Poderia fazer X+k, potências de k, mas esse comportamento de saltar sacrificaria muitas das principais vantagens do Binius. A solução é apresentada no Papel Binius (Ver Secção 4.3), mas isto é um buraco de coelho profundo em si mesmo.
• Como realizar com segurança verificações de valor específico. O exemplo de Fibonacci requer a verificação das condições de limite da chave: F(0)=F(1)=1 e o valor de F(100). Mas com Binius “bruto”, é inseguro verificar em pontos de avaliação pré-conhecidos. Existem maneiras bastante simples de converter uma verificação de avaliação conhecida em uma verificação de avaliação desconhecida, usando o que são chamados de protocolos de verificação de soma; mas não entrámos nesse assunto aqui.
• Protocolos de pesquisa, outra tecnologia que tem ganho uso recentemente como forma de criar sistemas de prova ultraeficientes. Binius pode ser combinado com protocolos de pesquisa para muitas aplicações.
• Ultrapassando o tempo de verificação da raiz quadrada. A raiz quadrada é cara: uma prova de Binius de bits tem cerca de 11 MB de comprimento. Pode remediar isso usando outro sistema de prova para fazer uma "prova de uma prova de Binius", ganhando assim tanto a eficiência do Binius na comprovação da declaração principal quanto um tamanho de prova pequeno. Outra opção é o protocolo FRI-Binius muito mais complicado, que cria uma prova de tamanho polilogarítmico (como FRI regular).
• Como o Binius afeta o que conta como 'SNARK-friendly'. O resumo básico é que, se você usar o Binius, não precisa mais se preocupar muito em tornar a computação 'aritmética-friendly': hashes 'regulares' não são mais eficientes do que hashes aritméticos tradicionais, multiplicação módulo ou módulo já não é mais uma grande dor de cabeça comparada à multiplicação módulo , e assim por diante. Mas este é um tópico complicado; muitas coisas mudam quando tudo é feito em binário.

Espero muitas mais melhorias nas técnicas de prova baseadas em campos binários nos próximos meses.

Aviso legal：

1. Este artigo é republicado de [GatePanews]. Encaminhar o Título Original 'Vitalik详解Binius：基于二进制字段的高效证明系统'. Todos os direitos autorais pertencem ao autor original [Vitalik Buterin*]. Se houver objeções a esta reimpressão, entre em contato com o Gate Learnequipa e eles tratarão disso prontamente.
2. Responsabilidade de Isenção: As opiniões expressas neste artigo são exclusivamente do autor e não constituem qualquer conselho de investimento.
3. As traduções do artigo para outros idiomas são feitas pela equipe Gate Learn. A menos que seja mencionado, copiar, distribuir ou plagiar os artigos traduzidos é proibido.