Resumo Técnico: Automação de Provas de Equivalência de Vetores de Bits e Campos Finitos em Lean

Declaração do Problema

A verificação de codificações de circuitos de Prova de Conhecimento Zero (ZKP) enfrenta um desafio crítico: provar a correção de afirmações livres de quantificadores que utilizam simultaneamente operações de vetor de bits (aritmética de máquina padrão módulo $2^N$) e operações de campo finito (aritmética módulo um primo grande $P$). Sistemas ZKP frequentemente requerem "aritmetizações" que codificam lógica de vetores de bits como polinômios de campo finito. Garantir que essas codificações sejam corretas é vital para a solidez dos sistemas ZKP, contudo, construí-las é propenso a erros.

Os fluxos de trabalho de verificação existentes sofrem de duas limitações primárias:

1. Verificação Manual: Incorporar sistemas ZKP inteiros em Provedores de Teoremas Interativos (ITPs) como Lean fornece garantias fortes, mas exige esforço humano substancial. À medida que as otimizações de ZKP evoluem rapidamente, essas provas manuais frequentemente exigem retrabalho significativo.
2. Verificação Automática via SMT: Reduzir a verificação a consultas de Satisfatibilidade Modulo Teorias (SMT) oferece maior automação, mas luta com dois problemas fundamentais:
   • Conversão de Teoria: Solucionadores SMT carecem de suporte nativo para conversão entre campos finitos e vetores de bits. Soluções alternativas como divisão de bits introduzem variáveis excessivas, e verificações de intervalo requerem polinômios complexos que degradam o desempenho do solucionador.
   • Base de Código Confiável (TCB): Solucionadores SMT possuem uma TCB muito maior do que ITPs, aumentando o risco de bugs não detectados.

Metodologia

Os autores apresentam BitModEq, uma tática Lean inovadora projetada para provar automaticamente a equivalência entre codificações de campo finito e suas semânticas de vetor de bits correspondentes. A abordagem aproveita a semântica rica dos ITPs para realizar conversões de tipos diretas, mantendo a automação da resolução SMT através de um fluxo de trabalho especializado.

Fluxo de Trabalho Principal

BitModEq opera em quatro fases distintas (ilustradas na Figura 1 do artigo):

1. Conversão de Campo Finto para Número Natural: Todos os termos de ordem Campo Finito ($FP$) são convertidos para Números Naturais ($N$). Isso envolve empurrar operadores de conversão (como toNat) para dentro através de expressões aritméticas.
2. Análise de Intervalo: Desigualdades sobre números naturais geradas durante a conversão são resolvidas usando um algoritmo dedicado de análise de intervalo.
3. Conversão de Número Natural para Vetor de Bits: Os termos de número natural restantes são convertidos para vetores de bits ($BV_N$).
4. Explosão de Bits (Bit-Blasting): As metas finais de igualdade de vetores de bits são resolvidas usando bv_decide, um procedimento de decisão de explosão de bits implementado em Lean.

Componentes Técnicos Principais

1. Cálculo de Tradução (Seções 4.2)
A tática emprega um conjunto de regras de tradução para mover entre domínios:

• $FP \to N$: Regras como distNat distribuem toNat sobre adição e multiplicação. Crucialmente, a tática distingue entre casos onde o envolvimento modular pode ser descartado (permitindo subtração simples) e casos onde não pode (requerendo a adição do módulo $P$ seguido de uma operação de módulo). Regras como sqrBds detectam codificações de bits (onde $x^2 = x$) e as traduzem para limites ($x \le 1$).
• $N \to BV$: Regras como distBV distribuem toBV sobre operações. Diferentemente da etapa $FP \to N$, essas regras não requerem a adição de um operador de módulo porque o espaço alvo é naturalmente módulo $2^N$.

2. Análise de Intervalo (Seção 4.3)
Táticas Lean padrão (por exemplo, omega, linarith) frequentemente falham em aritmetizações de ZKP devido a grandes coeficientes e dependências complexas de variáveis. BitModEq introduz um cálculo de análise de intervalo personalizado e dirigido pela sintaxe:

• Variáveis Placeholder: O algoritmo introduz variáveis placeholder existenciais para decompor desigualdades complexas.
• Decomposição e Eliminação: Regras decompoem desigualdades (por exemplo, $a + b \le w$ torna-se $a \le w_1, b \le w_2, w_1+w_2 \le w$) e eliminam placeholders instanciando-os com limites derivados de hipóteses ou propriedades conhecidas (por exemplo, elementos de campo finito são limitados por $P-1$).
• Tratamento de Dependências: Regras especializadas (ineqCases, ineqXOR) realizam análise de casos direcionada em variáveis simulando bits (0 ou 1) para resolver dependências que solucionadores aritméticos padrão perdem.

3. Implementação
A tática é implementada em Lean 4.23.0, utilizando mathlib para lemas e bv_decide para a etapa final de explosão de bits. Ela depende do kernel do Lean para verificação de provas, garantindo uma Base de Computação Confiável mínima.

Contribuições Principais

1. Tática BitModEq: Uma tática Lean que traduz operações de campo finito para vetores de bits e resolve as metas resultantes via explosão de bits, mantendo as garantias de correção dos ITPs.
2. Verificação Limitada de Codificações do Mundo Real: Uma verificação de conceito de dois sistemas ZKP do mundo real (Jolt e CirC) que alcança limites de largura de bits mais altos do que técnicas anteriores.
3. Análise de Intervalo Especializada: Uma nova tática Lean para provar metas resultantes da tradução, especificamente projetada para lidar com as dependências de variáveis e restrições de desigualdade comuns em aritmetizações de ZKP.

Resultados e Avaliação

Os autores avaliaram BitModEq contra solucionadores SMT de última geração (especificamente cvc5 com bases de Gröbner completas e divididas) em benchmarks extraídos de Jolt (uma zkVM) e CirC (um compilador de zkVM).

• Desempenho: BitModEq resolveu 19% mais benchmarks do que as configurações SMT de melhor desempenho.
  • Em benchmarks Jolt (tabelas de pesquisa de 8 bits e 32 bits), BitModEq resolveu 3 instâncias de 8 bits e 7 instâncias de 32 bits a mais do que o cvc5 (codificação fraca).
  • Em benchmarks CirC, BitModEq resolveu mais instâncias para 13 dos 17 larguras de bits testados.
• Escalabilidade: Embora o cvc5 tenha se saído melhor em larguras de bits menores, seu desempenho degradou significativamente à medida que as larguras de bits aumentaram devido à explosão de variáveis da divisão de bits. BitModEq escalou efetivamente até entradas de 32 bits.
• Eficiência: Um estudo de ablação mostrou que a análise de intervalo personalizada é crítica; remover divisões de casos reduziu significativamente o número de benchmarks resolvidos (por exemplo, de 737 para 720 no CirC, e de 24 para 21 no Jolt). Substituir a análise personalizada por táticas Lean padrão (ring_nf, linarith, etc.) resultou em uma queda drástica nas instâncias resolvidas (por exemplo, 434 vs 737 no CirC).
• Tempo de Execução: A análise de intervalo representa aproximadamente 52% do tempo de execução total, seguida pela tradução (23%) e explosão de bits (21%).
• Descoberta de Bugs: Durante a avaliação do CirC, os autores identificaram um bug de solidez na implementação de deslocamento à direita aritmético de 32 bits relacionado a estouro de inteiro, que não foi detectado em larguras de bits menores.

Significado e Alegações

O artigo afirma que BitModEq aborda as limitações específicas dos fluxos de trabalho atuais de verificação de ZKP combinando a solidez dos ITPs com raciocínio automatizado. Ao traduzir restrições de campo finito de volta para vetores de bits, a abordagem evita os gargalos de desempenho da conversão de teoria SMT e a grande TCB dos solucionadores SMT.

Os autores enfatizam que sua abordagem é particularmente eficaz para aritmetizações de ZKP que simulam operações em nível de bit dentro de um campo finito, um padrão comum em sistemas ZK modernos. Embora o método não seja completo (pode retornar "desconhecido" para certas dependências complexas ou operações específicas de campo como inversos), ele verifica com sucesso codificações do mundo real que anteriormente eram intratáveis para ferramentas automáticas, fornecendo provas verificadas pelo kernel para a correção desses componentes criptográficos críticos.