Riepilogo Tecnico: Automazione delle Dimostrazioni di Equivalenza per Bitvector e Campi Finiti in Lean

Enunciato del Problema

La verifica delle codifiche di circuiti per le Zero-Knowledge Proof (ZKP) affronta una sfida critica: dimostrare la correttezza di affermazioni senza quantificatori che utilizzano simultaneamente operazioni su bitvector (aritmetica macchina standard modulo $2^N$) e operazioni su campi finiti (aritmetica modulo un grande primo $P$). I sistemi ZKP richiedono spesso "aritmetizzazioni" che codificano la logica dei bitvector come polinomi su campi finiti. Garantire la correttezza di queste codifiche è vitale per la correttezza dei sistemi ZKP, ma la loro costruzione è soggetta a errori.

I flussi di lavoro di verifica esistenti soffrono di due limitazioni principali:

1. Verifica Manuale: L'inserimento di interi sistemi ZKP in Teoremi Interattivi (ITP) come Lean fornisce garanzie solide ma richiede un notevole sforzo umano. Poiché le ottimizzazioni ZKP evolvono rapidamente, queste dimostrazioni manuali richiedono frequentemente un significativo lavoro di rifacimento.
2. Verifica Automatica tramite SMT: La riduzione della verifica a query di Satisfiability Modulo Theories (SMT) offre una maggiore automazione ma lotta con due problemi fondamentali:
   • Conversione delle Teorie: I solver SMT mancano di supporto nativo per la conversione tra campi finiti e bitvector. I workaround come la suddivisione in bit (bit-splitting) introducono un eccesso di variabili, e i controlli di intervallo richiedono polinomi complessi che degradano le prestazioni del solver.
   • Base di Codice Fidata (TCB): I solver SMT hanno una TCB molto più ampia rispetto agli ITP, aumentando il rischio di errori non rilevati.

Metodologia

Gli autori presentano BitModEq, una nuova tattica Lean progettata per dimostrare automaticamente l'equivalenza tra le codifiche su campi finiti e la loro semantica bitvector corrispondente. L'approccio sfrutta la ricca semantica degli ITP per eseguire conversioni dirette di tipo, mantenendo al contempo l'automazione della risoluzione SMT attraverso un flusso di lavoro specializzato.

Flusso di Lavoro Principale

BitModEq opera in quattro fasi distinte (illustrate nella Figura 1 del documento):

1. Conversione da Campo Finito a Numero Naturale: Tutti i termini di tipo Campo Finito ($FP$) vengono convertiti in Numeri Naturali ($N$). Ciò comporta la spinta degli operatori di conversione (come toNat) verso l'interno attraverso le espressioni aritmetiche.
2. Analisi degli Intervalli: Le disuguaglianze sui numeri naturali generate durante la conversione vengono risolte utilizzando un algoritmo dedicato di analisi degli intervalli.
3. Conversione da Numero Naturale a Bitvector: I termini rimanenti di numero naturale vengono convertiti in bitvector ($BV_N$).
4. Bit-Blasting: Gli obiettivi finali di uguaglianza sui bitvector vengono risolti utilizzando bv_decide, una procedura decisionale di bit-blasting implementata in Lean.

Componenti Tecnici Chiave

1. Calcolo di Traduzione (Sezioni 4.2)
La tattica impiega un insieme di regole di traduzione per spostarsi tra i domini:

• $FP \to N$: Regole come distNat distribuiscono toNat su addizione e moltiplicazione. Crucialmente, la tattica distingue tra casi in cui l'overflow modulare può essere escluso (consentendo una semplice sottrazione) e casi in cui non può (richiedendo l'aggiunta del modulo $P$ seguito da un'operazione modulo). Regole come sqrBds rilevano codifiche bit (dove $x^2 = x$) e le traducono in limiti ($x \le 1$).
• $N \to BV$: Regole come distBV distribuiscono toBV sulle operazioni. A differenza della fase $FP \to N$, queste regole non richiedono l'aggiunta di un operatore modulo perché lo spazio target è naturalmente modulo $2^N$.

2. Analisi degli Intervalli (Sezione 4.3)
Le tattiche standard di Lean (ad esempio omega, linarith) spesso falliscono sulle aritmetizzazioni ZKP a causa di coefficienti grandi e dipendenze complesse tra variabili. BitModEq introduce un calcolo di analisi degli intervalli personalizzato e diretto dalla sintassi:

• Variabili Segnaposto: L'algoritmo introduce variabili segnaposto esistenziali per decomporre disuguaglianze complesse.
• Decomposizione ed Eliminazione: Le regole decompongono le disuguaglianze (ad esempio, $a + b \le w$ diventa $a \le w_1, b \le w_2, w_1+w_2 \le w$) ed eliminano i segnaposto istanziandoli con limiti derivati da ipotesi o proprietà note (ad esempio, gli elementi del campo finito sono limitati da $P-1$).
• Gestione delle Dipendenze: Regole specializzate (ineqCases, ineqXOR) eseguono un'analisi dei casi mirata su variabili che simulano bit (0 o 1) per risolvere dipendenze che i solver aritmetici standard non colgono.

3. Implementazione
La tattica è implementata in Lean 4.23.0, utilizzando mathlib per i lemmi e bv_decide per la fase finale di bit-blasting. Si affida al kernel di Lean per la verifica delle dimostrazioni, garantendo una Base di Calcolo Fidata minima.

Contributi Chiave

1. Tattica BitModEq: Una tattica Lean che traduce le operazioni su campi finiti in bitvector e risolve gli obiettivi risultanti tramite bit-blasting, mantenendo le garanzie di correttezza degli ITP.
2. Verifica Limitata di Codifiche Reali: Una verifica proof-of-concept di due sistemi ZKP reali (Jolt e CirC) che raggiunge limiti di larghezza in bit superiori rispetto alle tecniche precedenti.
3. Analisi degli Intervalli Specializzata: Una nuova tattica Lean per dimostrare obiettivi risultanti dalla traduzione, specificamente progettata per gestire le dipendenze tra variabili e i vincoli di disuguaglianza comuni nelle aritmetizzazioni ZKP.

Risultati e Valutazione

Gli autori hanno valutato BitModEq rispetto ai solver SMT all'avanguardia (in particolare cvc5 con basi di Gröbner complete e divise) su benchmark estratti da Jolt (una zkVM) e CirC (un compilatore zkVM).

• Prestazioni: BitModEq ha risolto il 19% in più di benchmark rispetto alle configurazioni SMT migliori.
  • Sui benchmark Jolt (tabelle di ricerca a 8 bit e 32 bit), BitModEq ha risolto 3 istanze in più a 8 bit e 7 istanze in più a 32 bit rispetto a cvc5 (codifica debole).
  • Sui benchmark CirC, BitModEq ha risolto più istanze per 13 delle 17 larghezze in bit testate.
• Scalabilità: Mentre cvc5 ha ottenuto prestazioni migliori su larghezze in bit più piccole, le sue prestazioni sono degradate significativamente all'aumentare delle larghezze in bit a causa dell'esplosione delle variabili derivante dalla suddivisione in bit. BitModEq si è scalato efficacemente fino a input a 32 bit.
• Efficienza: Uno studio di ablazione ha mostrato che l'analisi degli intervalli personalizzata è critica; la rimozione delle divisioni per casi ha ridotto significativamente il numero di benchmark risolti (ad esempio, da 737 a 720 su CirC, e da 24 a 21 su Jolt). Sostituire l'analisi personalizzata con tattiche Lean standard (ring_nf, linarith, ecc.) ha portato a un calo drastico delle istanze risolte (ad esempio, 434 contro 737 su CirC).
• Tempo di Esecuzione: L'analisi degli intervalli rappresenta circa il 52% del tempo di esecuzione totale, seguita dalla traduzione (23%) e dal bit-blasting (21%).
• Scoperta di Bug: Durante la valutazione di CirC, gli autori hanno identificato un bug di correttezza nell'implementazione dello shift aritmetico destro a 32 bit relativo all'overflow intero, che non era stato rilevato a larghezze in bit più piccole.

Significato e Affermazioni

Il documento afferma che BitModEq affronta le limitazioni specifiche dei flussi di lavoro di verifica ZKP attuali combinando la correttezza degli ITP con il ragionamento automatizzato. Traducendo i vincoli sui campi finiti di nuovo in bitvector, l'approccio evita i colli di bottiglia delle prestazioni della conversione delle teorie SMT e la grande TCB dei solver SMT.

Gli autori sottolineano che il loro approccio è particolarmente efficace per le aritmetizzazioni ZKP che simulano operazioni a livello di bit all'interno di un campo finito, un pattern comune nei moderni sistemi ZK. Sebbene il metodo non sia completo (potrebbe restituire "sconosciuto" per certe dipendenze complesse o operazioni specifiche del campo come gli inversi), verifica con successo codifiche reali che erano precedentemente intrattabili per gli strumenti automatici, fornendo dimostrazioni verificate dal kernel per la correttezza di questi componenti critici crittografici.