Riepilogo Tecnico: Combinazione dell'Inferenza di Specifiche Meccaniche e Agentiche per Move

Enunciato del Problema

La verifica formale degli smart contract Move utilizzando Move Prover (MVP) affronta un collo di bottiglia pratico significativo: l'alto costo della scrittura manuale delle specifiche. Sebbene gli sviluppatori mirino a verificare proprietà di alto livello (ad esempio, invarianti dello stato globale, conservazione dei fondi o aborti condizionali), il processo di verifica richiede pre-condizioni e post-condizioni esplicite e di basso livello per ogni funzione di supporto. La scrittura di queste specifiche è meccanica, tediosa e spesso domina il costo dell'utilizzo di un verificatore, ostacolando una più ampia adozione. Sebbene MVP possa incorporare i corpi delle funzioni per verificare le chiamate non specificate, questo approccio non scala per la verifica modulare.

Metodologia

Il documento presenta un nuovo strumento che combina l'analisi meccanica della pre-condizione più debole (WP) con la codifica agenziale (specificamente tramite Claude Code) per inferire specifiche per il bytecode Move. Il sistema opera attraverso un flusso di lavoro collaborativo in cui Move Prover funge da oracolo sia per i segnali meccanici che per quelli generati dall'IA.

1. Componente Meccanica: Analisi della Pre-condizione più Debole (WP)

La base meccanica si affida a un'analisi WP standard eseguita sul bytecode Move. Le caratteristiche tecniche chiave includono:

• Eliminazione dei Riferimenti: Prima dell'analisi, la pipeline di trasformazione di Move Prover elimina i riferimenti in stile Rust (&T, &mut T) riscrivendo il bytecode in una forma intermedia priva di riferimenti. I riferimenti condivisi vengono incorporati (inlined) e i riferimenti mutabili vengono convertiti in parametri in/out. Ciò permette di applicare direttamente il ragionamento classico di stile Dijkstra.
• Strumentazione delle Specifiche: Il bytecode viene strumentato con istruzioni assume e assert derivate dalle specifiche utente esistenti. Le chiamate vengono strumentate utilizzando predicati comportamentali (ad esempio, result_of, aborts_of) per astrarre i contratti delle funzioni chiamate.
• Output: Il motore WP deriva meccanicamente le condizioni di aborto, le clausole modifies e le post-condizioni di tipo conseguenza. Tuttavia, fatica con gli invarianti di ciclo, che generalmente non sono derivabili dai soli corpi dei cicli; senza questi, le specifiche inferite diventano vuote.

2. Componente Agente: Inferenza Guidata dall'IA

Un agente di codifica IA (Claude Code), integrato tramite un servizio Model Context Protocol (MCP), affronta i limiti del motore WP:

• Invarianti di Ciclo: L'agente utilizza il riconoscimento di pattern per proporre invarianti induttivi (ad esempio, monotonia, conservazione delle somme, prefissi ordinati) che il motore WP non può derivare.
• Idiomi di Alto Livello: L'agente genera specifiche di alto livello (ad esempio, monotonia, invarianti strutturali) in idiomi familiari agli sviluppatori umani.
• Semplificazione: L'agente affina le specifiche verbose, semanticamente corrette ma spesso ingombranti generate dal motore WP, in forme più compatte e leggibili.
• Suggerimenti di Prova: Quando la verifica va in timeout (ad esempio, a causa di aritmetica non lineare), l'agente genera lemmi e suggerimenti di prova per guidare il verificatore.

3. Il Flusso di Lavoro

Il processo è fornito come plugin Claude Code che utilizza "abilità" (istruzioni Markdown), hook in fase di modifica e un server MCP. Il flusso di lavoro segue una sequenza di task fissa:

1. Sintesi degli Invarianti di Ciclo: L'agente identifica i cicli privi di invarianti e li propone.
2. Inferenza delle Pre-condizioni più Deboli: L'agente chiama MVP tramite MCP per generare le specifiche di base meccaniche.
3. Semplificazione: L'agente riscrive le specifiche combinate per leggibilità e concisione.
4. Verifica e Affinamento: Viene eseguita una esecuzione di verifica a tutto campo. Se vengono trovati errori logici, l'agente li corregge. Se si verificano timeout, l'agente introduce lemmi o suggerimenti di prova.
5. Iterazione: I contro-esempi dal verificatore vengono inviati all'agente per l'affinamento. L'utente può intervenire in qualsiasi punto.

Contributi Chiave

Il documento identifica tre contributi principali:

1. Architettura di Inferenza Ibrida: A conoscenza degli autori, questo è il primo sistema di inferenza di specifiche basato su LLM a combinare una base meccanica solida (WP) con un componente agenziale. Il motore WP gestisce la derivazione meccanica (aborti, modifiche, post-condizioni), mentre l'IA gestisce le parti "più deboli" del WP (invarianti di ciclo e idiomi di alto livello).
2. Integrazione Interattiva dell'Agente di Codifica: A differenza dei precedenti strumenti di inferenza che operano come script autonomi, questo sistema è integrato come plugin in un agente di codifica interattivo (Claude Code). Ciò permette un ciclo collaborativo in cui l'utente può monitorare, sovrascrivere o contribuire al processo di inferenza.
3. Eliminazione dei Riferimenti per WP: Il documento dettaglia l'applicazione dell'eliminazione dei riferimenti (precedentemente utilizzata in Aeneas per Rust) al bytecode Move per abilitare l'analisi WP classica. Questa combinazione di forme intermedie prive di riferimenti con l'inferenza WP non è stata precedentemente descritta.

Risultati e Valutazione

Lo strumento è stato applicato a un corpus di codice Move canonico, includendo:

• Funzioni di ordine superiore: Nello specifico, una funzione di ricerca vettoriale che utilizza predicati.
• Aritmetica: Una funzione di esponenziazione che coinvolge aritmetica non lineare e controlli di overflow.
• Algoritmi dipendenti dallo stato: Una funzione che modifica lo storage globale su più indirizzi.

Osservazioni:

• L'approccio ibrido ha generato con successo specifiche per scenari complessi che coinvolgono cicli, dispatch dinamico e stato globale.
• Nell'esempio di esponenziazione, il motore WP ha fornito la condizione di correttezza, mentre l'agente ha introdotto con successo un lemma di monotonia per risolvere un timeout di verifica.
• L'agente ha riscritto frequentemente le specifiche generate da WP in forme più compatte, anche dopo la propria semplificazione dei termini del motore WP.
• Il sistema gestisce le condizioni "vuote" facendo sì che l'agente le scarti durante la fase di semplificazione.

Significato e Affermazioni

Il documento inquadra questo lavoro come lavoro iniziale e un documento sugli strumenti con risultati preliminari. Gli autori fanno affermazioni modeste riguardo al significato:

• Punti di Forza Complementari: Il sistema sfrutta l'affidabilità della deduzione meccanica per il boilerplate e le capacità di riconoscimento di pattern degli LLM per il ragionamento induttivo. La base WP impedisce all'agente di suggerire specifiche "completamente errate", mentre l'agente colma le lacune dove WP fallisce.
• Innovazione nel Flusso di Lavoro: L'integrazione della verifica in un ciclo di codifica conversazionale tramite abilità e MCP rappresenta un passaggio dagli strumenti di analisi statica a flussi di lavoro dinamici e collaborativi.
• Direzione Futura: Gli autori riconoscono che la definizione di "abilità" (istruzioni) è un'area in evoluzione. Prevedono di applicare lo strumento retrospettivamente all'Aptos Framework e a un motore di trading perpetuo complesso per valutare la scalabilità e i costi dei token rispetto alle specifiche scritte a mano. Notano esplicitamente che l'efficacia dell'approccio ibrido rispetto all'inferenza pura LLM richiede ulteriori studi sistematici.

Il documento conclude che questa metodologia dimostra una via percorribile per ridurre il costo del boilerplate della verifica formale in Move, abilitando una collaborazione tra IA, deduzione meccanica e sviluppatori umani.