Quando a cobertura de linha mente

Esta nota foi escrita para ser lida duas vezes. As duas primeiras seções não pressupõem nenhum contato prévio com sistemas de restrições e constroem o mecanismo do zero. O resto é escrito para quem constrói e audita esses circuitos, e vai direto ao código exato, à álgebra do exploit e a uma validação projetada para não se autolisonjear.

O que um sistema de restrições realmente checa

Uma prova zero knowledge de uma computação repousa sobre uma única ideia. Em vez de reexecutar o trabalho, um verificador checa que uma tabela preenchida, chamada de trace, obedece a um conjunto fixo de regras algébricas. Cada linha é um passo da computação e cada coluna é um registrador ou valor intermediário. Formalmente a trace é $T\in {\mathbb{F}}^{n\times w}$, uma matriz de $n$ linhas e $w$ colunas sobre um corpo finito.

Cada regra é um polinômio que deve avaliar para zero. Uma regra que age sobre uma única linha pede que algum polinômio $C$ se anule em toda linha:

Uma regra que amarra um passo ao seguinte age sobre um par de linhas adjacentes, $C({\mathbf{t}}_i,{\mathbf{t}}_{i+1})=0$. O prover envia uma trace e o verificador checa que toda regra se anula. Se todas se anulam, o verificador se convence de que a computação foi realizada corretamente.

Soundness é a propriedade que torna isso confiável. As regras precisam fixar a trace, de modo que, para uma dada entrada pública, não exista trace válida além da honesta. Quando as regras são fracas demais, uma trace diferente satisfaz todas elas e o sistema fica sub-restringido.

Um prover que quer trapacear preenche essa outra trace, toda regra ainda se anula e o resultado é uma prova válida de uma afirmação falsa. Sub-restrição não é uma preocupação teórica. É a classe de bug de soundness dominante em sistemas zero knowledge de produção, e já movimentou dinheiro de verdade.

O que importa aqui é a condicionalidade. A maioria das regras se aplica só às vezes. Uma regra de fronteira se aplica só na primeira linha, uma regra de transição se aplica entre linhas consecutivas mas não na virada cíclica do final, uma regra de instrução se aplica só nas linhas onde uma flag de opcode específica está ligada. O framework não escreve um if. Ele multiplica a regra por um polinômio seletor $s$ que é um onde a regra deve se aplicar e zero no resto, e então pede que o produto se anule:

Tudo decorre dessa única equação. Onde $s=1$ a linha precisa satisfazer $C$. Onde $s=0$ o produto é zero não importa o que $C$ seja, então nessas linhas a restrição não impõe nada. Ela é inerte.

O ponto cego

Um circuito é código, e as equipes o testam como código. O reflexo usual é a cobertura de linha: rodar os testes, confirmar que toda linha da definição da restrição executou, tratar verde como seguro.

A cobertura de linha responde a uma pergunta diferente da que soundness precisa. Ela pergunta se a instrução de asserção rodou, e rodou. O avaliador percorre toda linha da trace e chama a restrição em cada uma, então a linha é coberta em todas elas, até nas linhas onde o seletor é zero e a restrição não impõe nada. A instrução executou enquanto a restrição ficou sem teste.

No topo está o que uma ferramenta de cobertura reporta, cem por cento: a asserção rodou nas oito linhas. A faixa abaixo é o que de fato aconteceu, a restrição imposta em três delas. Uma ferramenta de linha não consegue separar um guarda ligado corretamente de um quebrado, porque ambos rodam a mesma linha o mesmo número de vezes. O visto verde mede execução e reporta como segurança.

Isto não é um canto raro. Restrições condicionais são a forma padrão nesses sistemas, o que é quase todas elas.

O bug que isso esconde

Uma família de bugs vive na lacuna, e é simples de enunciar: uma restrição correta acoplada ao seletor errado. Ela roda, mostra verde e falha em restringir as linhas que importam.

Tome um acumulador. A exponenciação por quadrados repetidos constrói um valor corrente onde cada passo eleva o anterior ao quadrado e multiplica por um fator dependente de bit:

onde o valor na última linha, $a_{n-1}$, é o resultado alegado $r$. A recorrência precisa valer em toda linha após a primeira, já que a linha zero não tem predecessora. Guardada corretamente, com um seletor que é um em toda parte exceto na primeira linha, ela é imposta nas linhas $1$ até $n-1$ e alcança a última linha, então o resultado fica amarrado à computação.

Guardada com o seletor errado, um que é zero na última linha em vez da primeira, ela é imposta nas linhas $0$ até $n-2$ e nunca toca a linha de saída. Uma trace honesta parece boa, porque uma trace honesta satisfaz a recorrência em toda parte de qualquer jeito. O resultado agora está livre.

Um prover define $a_{n-1}$ para qualquer valor escolhido, toda linha imposta ainda vale, a regra de fronteira que amarra a coluna de saída à alegação pública é satisfeita por construção e o verificador aceita uma prova de um expoente falso. Este é um achado real de uma auditoria publicada de uma máquina virtual zero knowledge de produção, e todo o defeito é um único seletor errado.

Uma métrica que mede imposição, não execução

O resto desta nota é para quem trabalha nesses sistemas.

A correção não é uma ferramenta de cobertura de linha melhor, mas uma medição diferente. Para cada sítio de restrição, sobre uma trace válida, registre onde o guarda esteve de fato ativo em vez de se a instrução rodou. Chame esse registro de perfil de ativação:

struct ConstraintCov {
    active_rows: usize,             // guarda não nulo
    inactive_rows: usize,          // guarda zero
    min_active_row: Option<usize>, // primeira linha alcançada
    max_active_row: Option<usize>, // última linha alcançada
    // ... mais active_zero / active_nonzero
}

Um ponto de design não era óbvio de antemão. Um booleano, "esta restrição esteve ativa alguma vez", não pega os bugs reais. No acumulador acima o guarda quebrado está ativo em sete das oito linhas e o correto também está ativo em sete das oito linhas, então ambos reportam "ativa alguma vez". O sinal não é quantas linhas, mas quais linhas: o guarda correto alcança a última linha e o quebrado não. O perfil de ativação carrega essa distinção e o booleano a descarta.

A instrumentação é pequena, e esse é o ponto. Num builder no estilo Plonky3 a multiplicação do guarda vive em exatamente um lugar, o builder filtrado que dobra uma condição numa asserção:

// FilteredAirBuilder::assert_zero
fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
    self.inner.assert_zero(self.condition() * x.into());
}

Toda restrição guardada no sistema inteiro passa por essa única multiplicação. Então um único hook ali, alimentado pelo avaliador de trace concreta, enxerga todas elas:

fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
    // Reporta o guarda antes de ele ser dobrado no termo. Após a
    // multiplicação, o guarda e a expressão restringida são indistinguíveis.
    self.inner.aircov_note_guard(&self.condition);
    self.inner.assert_zero(self.condition() * x.into());
}

Esse recorder fica atrás de uma feature flag e permanece inerte a menos que uma sessão esteja aberta, então builds comuns não pagam nada. A métrica é lida a partir de uma trace válida: rode as restrições pelo avaliador, e em vez de passa ou falha a saída é o conjunto de linhas em que cada guarda esteve vivo.

O exploit, no perfil de ativação

O bug do acumulador agora é visível antes de alguém rodar o exploit. Alterne o guarda abaixo e observe a última linha, a que carrega o resultado.

Sob o guarda correto a recorrência alcança a linha de saída, então um resultado errado não pode passar. O guarda quebrado deixa a linha de saída sem restrição, que é exatamente a liberdade que a falsificação usa. Dois perfis, um seletor diferente, mesmo código e mesmas linhas executadas. O bug enviado tinha esta cara:

// Impõe a recorrência de acumulação.
builder
    .when(local.is_real)
    .when_not(local.is_last)   // guarda enviado; a correção é is_first
    .assert_eq(local.accum, local.prev_accum_squared_times_multiplier);

A cobertura de linha dessa asserção é cem por cento sob qualquer teste honesto, porque a asserção roda em toda linha. O perfil de ativação é o único sinal barato que a separa da versão correta numa trace válida, sem que ninguém precise pensar na falsificação primeiro.

Validação, construída para não se autolisonjear

Há uma objeção óbvia. Os campos de posição de linha foram adicionados enquanto se olhava para um bug de guarda de linha, então validar a métrica sobre esse mesmo bug não prova nada, porque uma métrica sempre pega o caso em torno do qual foi moldada.

Para separar previsão de ajuste, a métrica foi congelada por escrito e as previsões foram registradas de antemão. O critério foi fixado antes de qualquer bug reservado ser construído: o AIRCov distingue um bug quando o perfil congelado por sítio, computado sobre uma trace válida, difere entre o circuito correto e o quebrado em pelo menos um sítio compartilhado. Quatro classes de bug foram então reconstruídas como circuitos mínimos escritos à mão, cada uma uma reconstrução fiel de um padrão documentado em vez de um bug pego na natureza, e cada uma confirmada genuinamente explorável, ou seja, uma trace forjada que o circuito quebrado aceita e o correto rejeita.

As quatro previsões se sustentaram. Olhe a linha do seletor errado, que carrega o peso. É um mecanismo diferente do bug de guarda de linha em torno do qual a métrica foi moldada, então uma captura ali é evidência de que o perfil generaliza para um bug que não foi projetado ao seu redor, em vez de evidência de que memorizou um caso. Os três erros foram previstos de antemão e marcam a fronteira honesta do método.

Uma ressalva mora dentro do critério. Ele pergunta se o perfil difere entre o circuito correto e o quebrado, o que pressupõe uma referência sabidamente correta para comparar. Uma auditoria real não tem tal referência. Essa ausência é o problema inteiro. Em produção a métrica emite um único perfil e um revisor o julga por conta própria, onde uma recorrência que nunca alcança a linha de saída se lê como errada sem nenhuma irmã com que comparar. O quatro de quatro é medido sob esse oráculo mais favorável. O sinal em produção é a leitura mais fraca da mesma impressão digital, e é por isso que o enquadramento final a chama de impressão digital de um revisor e não de um veredito.

Congele a métrica, escreva as previsões primeiro, depois reconstrua os bugs. Resultados que só valem depois de ajustados são uma medição de retrospecto.

O que ela não consegue pegar

Essa fronteira é nítida, e enunciá-la com clareza é o ponto de uma métrica que vale a pena confiar.

O AIRCov pega bugs de guarda e de seletor cujo perfil de ativação difere numa trace válida. Três coisas permanecem fora de alcance:

• Restrições faltantes. Sem sítio, não há nada a medir. Uma métrica sobre as restrições que existem não consegue ver a que não existe.
• Bugs de expressão estreita. Uma regra que checa um limb de uma palavra onde deveria checar todos tem o mesmo sítio, o mesmo guarda e o mesmo perfil de ativação da versão correta. Não há diferença a detectar, porque a diferença mora dentro da expressão em vez de em quando ela dispara.
• Bugs de guarda invisíveis em traces válidas. Uma condição extra espúria que dados honestos por acaso satisfazem não deixa marca na cobertura medida sobre traces válidas. Este é um limite de qualquer cobertura sobre trace válida, o AIRCov incluído, não uma lacuna que uma métrica mais afiada feche.

Então este é um instrumento para uma classe, com uma borda caracterizada. Ele traz à tona uma impressão digital, uma recorrência que nunca alcança a linha de saída, uma restrição que dispara nas linhas que sua irmã pula, que um revisor ou uma regra a jusante então interpreta. Ele não profere um veredito.

Na pilha real, e onde isto se situa

Nada do acima depende de um brinquedo. A instrumentação roda na pilha de produção. O SP1 atual avalia seus chips através de uma reexportação da crate p3-air publicada, então o mesmo hook de uma linha, vendorizado nessa crate e aplicado como patch, flui pelo builder de restrições real. A cobertura foi coletada num chip que vai no SP1, rodado pelo seu próprio avaliador. O exploit foi rodado num chip construído com os traits reais e o builder de restrições do SP1 que carrega a mesma classe de seletor errado, embora não um dos chips de produção pré-existentes, como as unidades aritméticas. Nesse caminho vivo o defeito é ao mesmo tempo explorável, com uma trace forjada aceita com zero linhas em falha, invisível à cobertura de linha, medido em cem por cento na restrição que o carrega e visível no perfil de ativação. Injetar padrões documentados nos próprios chips de produção é o trabalho restante.

Uma palavra sobre trabalho anterior. Um fuzzer metamórfico para máquinas virtuais zero knowledge já encontra bugs de soundness e de completude, já usa feedback leve de cobertura de instrução e nomeia a cobertura sob medida para restrições como trabalho futuro. Ele é ao mesmo tempo o baseline e evidência independente de que a direção vale a pena trilhar. Os trabalhos diferem. Aquela linha de trabalho gera testes e encontra bugs, enquanto o AIRCov mede se uma suíte de testes já em mãos é adequada, para uma classe de bug, com a fronteira desenhada. Nenhuma reivindicação é feita de ser o primeiro em teste de mutação neste espaço. O que se reivindica é mais estreito: uma métrica de adequação baseada em perfil de ativação por posição de linha, com evidência reservada pré-registrada de que ela separa uma classe de bug real que a cobertura de linha não consegue ver.

Os forks instrumentados e todo teste acima são públicos, do caso de viabilidade, passando pelo exploit de prova forjada e pelo achado de auditoria reconstruído, até a validação congelada pré-registrada, então os números aqui podem ser reexecutados em vez de aceitos na fé.

Reproduza

Dois forks carregam a instrumentação e os testes.

• Fork do Plonky3: o recorder, o hook de guarda de uma linha e os quatro testes, viabilidade, o exploit de prova forjada, o achado de auditoria reconstruído e a validação congelada pré-registrada. Detalhes no seu AIRCOV.md.
• Fork do SP1: o mesmo hook na pilha de produção, ligado através de uma cópia vendorizada de p3-air e do próprio builder de restrições do SP1, com a cobertura rodada num chip real. Detalhes no seu AIRCOV.md.