A Rust-to-Lean Verification Pipeline with AI Provers: An Experience Report

Riepilogo Tecnico: Una Pipeline di Verifica da Rust a Lean con Prover AI

Enunciato del Problema
Il codice crittografico di produzione, in particolare all'interno di stack di macchine virtuali a conoscenza zero (zkVM) come quelli utilizzati in Ethereum, tollera quasi zero errori. I metodi di verifica tradizionali—revisione del codice, fuzzing e test basati su proprietà—presentano limitazioni strutturali: si basano sull'anticipazione di specifici pattern di bug o sull'esplorazione di budget di input finiti, spesso mancando divergenze semantiche silenziose. Sebbene la verifica formale offra prove verificate dalla macchina per tutti gli input, il suo costo storico è stato proibitivo, richiedendo anni di sforzo per accoppiare implementazione e prova in sistemi come seL4 o CompCert. Inoltre, gli strumenti esistenti di verifica per Rust (ad esempio Verus, Prusti, Kani) mirano spesso a frammenti specifici del linguaggio o si affidano a solver SMT senza collegare Rust di produzione alle specifiche matematiche astratte richieste per i protocolli crittografici.

Metodologia
Gli autori propongono e implementano una pipeline di verifica neurosimbolica che integra tre componenti distinti per colmare il divario tra codice Rust di produzione e prove verificate dalla macchina in Lean 4:

1. Estrazione Simbolica: La pipeline eleva codice Rust sicuro in Lean 4 funzionale puro utilizzando strumenti di estrazione.
   • Aeneas/Charon: Traduce Rust sicuro tramite una rappresentazione intermedia tipizzata (LLBC) in Lean 4, trattando le garanzie del borrow-checker come input semantici e avvolgendo le operazioni in un monade Result.
   • Hax: Uno strumento guidato da annotazioni che traduce Rust (tramite THIR) in Lean 4, F⋆ o Rocq.
2. Specifiche Formali: Il codice estratto viene verificato rispetto a target matematici astratti forniti da librerie specializzate:
   • ArkLib: Formalizza argomenti non interattivi di conoscenza compatti (SNARKs) e Riduzioni di Oracolo Interattive (IORs), inclusi protocolli come FRI, Sum-Check e WHIR.
   • CompPoly: Fornisce teoria dei polinomi computazionali e dei campi finiti.
3. Prover AI: La pipeline impiega agenti AI (Aristotle e Aleph) per chiudere gli obblighi di prova generati durante la verifica. Questi agenti decompongono gli obiettivi, generano lemma candidati e costruiscono prove. Crucialmente, il kernel Lean ricontrolla ogni prova, garantendo che l'output AI non comprometta la correttezza.

Il flusso di lavoro procede in quattro fasi: (1) Estrazione da Rust a Lean 4; (2) Definizione delle specifiche (o scritta a mano o tramite equivalenza di libreria); (3) Costruzione della prova (manuale, assistita da AI o ibrida); e (4) Ricontrollo del kernel.

Contributi Chiave
Il documento apporta quattro contributi principali:

• Integrazione della Pipeline: Documenta la prima integrazione riuscita di strumenti di estrazione da Rust a Lean, librerie crittografiche formali e prover AI in un singolo flusso di lavoro end-to-end.
• Applicazione a Primitive Crittografiche: La pipeline è stata applicata a otto target critici per il consenso all'interno del Progetto di Verifica zkEVM della Ethereum Foundation, specificamente in Plonky3 (folding FRI, aritmetica di campo Mersenne31/KoalaBear, valutazione di Horner, pianificazione dei round) e RISC Zero (verifica dell'inclusione Merkle).
• Analisi Empirica dei Prover AI: Gli autori forniscono un resoconto a livello di lemma delle prestazioni dell'AI. Segnalano che i prover AI (in particolare Aleph) hanno chiuso con successo due teoremi non banali di tipo bound nella funzione compute_log_arity_for_round di Plonky3. Queste prove hanno coinvolto la decomposizione di legami monadici e la gestione di bound condizionali, producendo lemma di aiuto riutilizzabili.
• Documentazione del Divario Ingegneristico: Il documento identifica specifici punti di attrito, tra cui la deriva degli strumenti della toolchain Lean 4 tra diversi strumenti, i limiti di estrazione in Aeneas/Hax (ad esempio, problemi con trait generici, crate esterne e cicli while) e la mancanza di lemma nelle librerie standard. Propone tre soluzioni alternative: fix a monte, estrazione di modelli semantici e tooling stratificato per codice non sicuro.

Risultati

• Verifica Riuscita: La pipeline ha verificato con successo che le implementazioni in Rust delle primitive crittografiche sono equivalenti alle loro specifiche matematiche in ArkLib e CompPoly.
• Prestazioni AI: Nell'esempio in esecuzione (compute_log_arity_for_round), Aleph ha chiuso automaticamente due teoremi precedentemente irrisolti (arity_respects_max_bound e arity_respects_target_distance) generando prove strutturate con lemma di aiuto.
• Limitazioni Osservate: I prover AI hanno funzionato bene su lemma strutturali di controllo del flusso, aritmetica lineare con condizioni secondarie lievi e semplificazione boilerplate. Tuttavia, hanno faticato con identità algebriche specifiche del dominio che richiedevano una selezione specifica di lemma Mathlib4, invarianti di ciclo in funzioni ricorsive e obblighi che richiedevano l'assiomatizzazione di interfacce esterne. Queste aree sono rimaste compiti manuali.
• Disponibilità degli Artefatti: Tutto il codice, le specifiche e le prove sono pubblici, inclusi i repository per le verifiche basate su Aeneas e quelle basate su Hax.

Significato e Affermazioni
Il documento afferma di documentare il primo tentativo di combinare questi tre filoni tecnologici (estrazione, librerie formali, prover AI) per Rust crittografico reale. Il suo significato risiede nel dimostrare una pipeline funzionante in cui:

1. La correttezza è preservata: L'output AI è rigorosamente validato dal kernel Lean.
2. La produttività è potenziata: L'AI agisce come moltiplicatore per obblighi strutturali e aritmetici, sebbene gli ingegneri umani rimangano essenziali per la progettazione delle specifiche, la scoperta di invarianti e la selezione di astrazioni matematiche.
3. Le barriere sono abbassate: L'approccio offre una strada verso una verifica formale più efficace dei sistemi di produzione, superando il modello di "anni-persona" di verifica strettamente accoppiata osservato nei sistemi pionieristici precedenti.

Gli autori rimangono modesti, notando che, sebbene l'AI abbia chiuso lemma specifici non banali, la forma fondamentale dello sforzo di verifica (specificazione e astrazione) rimane un compito di ingegneria umana. Posizionano questo lavoro come un passo verso l'abbassamento delle barriere all'adozione e la facilitazione di un'integrazione AI più efficace nelle pipeline di verifica formale.