💻 computer science

Formal Verification of Imperative First-Class Functions in Move

Este artigo apresenta uma extensão ao Move Prover que permite a verificação formal de funções imperativas de primeira classe na linguagem Move, introduzindo predicados comportamentais, rótulos de estado e uma estratégia de codificação SMT que aproveita a separação estática de memória do Move para verificação eficiente e inferência automatizada de especificações.

Autores originais: Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman

Publicado 2026-05-14

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

A Visão Geral: A Fábrica de "Contratos Inteligentes"

Imagine que a Aptos é uma fábrica de alta segurança que constrói ativos digitais (como dinheiro ou ingressos) usando uma linguagem especial chamada Move. Para garantir que esses ativos não sejam roubados ou danificados, a fábrica utiliza um inspetor robótico chamado Move Prover (MVP). Este robô lê os projetos (o código) e prova matematicamente que tudo funcionará corretamente antes mesmo da fábrica começar a operar.

Por muito tempo, este robô era excelente em verificar instruções simples. Mas, recentemente, a fábrica adicionou um novo e complicado recurso: Funções de Primeira Classe.

Pense nessas novas funções como varinhas mágicas.

Antigo método: Você precisava segurar a varinha pessoalmente para lançar um feitiço. O robô sabia exatamente qual feitiço você estava lançando.
Novo método: Você pode colocar a varinha em uma caixa, entregar a caixa a um amigo, guardar a caixa em um cofre ou passar para uma máquina que não sabe o que há dentro. A máquina apenas sabe: "Preciso acenar com uma varinha", mas não sabe qual varinha até o último segundo.

Isso é chamado de Disparo Dinâmico (Dynamic Dispatch). É poderoso, mas quebra o inspetor robótico porque ele não consegue ver o futuro para saber qual feitiço específico está sendo lançado.

O Problema: O Dilema da "Caixa Preta"

O artigo explica como os autores atualizaram o inspetor robótico (MVP) para lidar com essas varinhas mágicas sem entrar em pânico.

Anteriormente, se uma função fosse uma "caixa preta" (uma variável contendo uma função), o robô tinha que adivinhar ou verificar todas as possibilidades de uma vez, o que fazia a matemática explodir e o robô ficar lento.

Os autores introduziram duas novas ferramentas para resolver isso:

1. Predicados Comportamentais: O "Cartão de Garantia"

Em vez de olhar dentro da varinha mágica para ver como ela funciona, o robô agora olha para o Cartão de Garantia anexado à varinha.

O Antigo Método: "Preciso saber exatamente como esta varinha calculate_price funciona, até cada linha de código, antes de permitir que você a use."
O Novo Método: "Não me importo como a varinha funciona por dentro. Só preciso ler seu Cartão de Garantia. O cartão diz: 'Se você me der 5 moedas, eu devolverei 3 moedas e nunca quebrarei.'"

O artigo chama isso de Predicados Comportamentais. Eles são como um contrato que descreve:

Pré-condições: O que deve ser verdade antes de você acenar com a varinha.
Pós-condições: O que será verdade depois que você a acenar.
Condições de Aborto: Quando a varinha pode explodir (falhar).

Isso permite que o robô verifique a promessa da varinha sem precisar conhecer o segredo da receita dentro dela.

2. Rótulos de Estado: A "Câmera de Carimbo de Tempo"

Às vezes, uma sequência de eventos acontece. Imagine uma linha de montagem onde um robô pinta um carro e, em seguida, outro robô coloca as rodas.

Se você quiser provar que o carro está seguro, precisa conhecer o estado do carro após a pintura, mas antes de as rodas serem colocadas.

Os autores introduziram Rótulos de Estado. Pense neles como Câmeras de Carimbo de Tempo colocadas em pontos específicos do processo.

Câmera A (Início): O carro é apenas metal nu.
Câmera B (Meio): O carro está pintado.
Câmera C (Fim): As rodas estão instaladas.

O robô agora pode dizer: "Sei que a pintura ocorreu entre a Câmera A e a Câmera B, e as rodas foram adicionadas entre a Câmera B e a Câmera C." Isso ajuda o robô a raciocinar sobre sequências complexas de eventos sem se confundir sobre como o mundo parecia em qualquer momento dado.

Como o Robô Funciona Realmente (O "Quadro de Comutação")

O artigo descreve como o robô traduz essas ideias em matemática (lógica SMT) que um computador pode resolver.

Imagine que o robô tem um Quadro de Comutação.

Cenário A (Varinha Conhecida): Se o robô vê uma varinha específica e conhecida (por exemplo, a função product), ele aciona o interruptor para o "Modo Direto". Ele ignora o cartão de garantia e apenas verifica o código real daquela varinha específica.
Cenário B (Varinha Desconhecida): Se o robô vê uma caixa genérica (uma variável), ele aciona o interruptor para o "Modo Abstrato". Ele ignora completamente o código e confia apenas no Cartão de Garantia (os predicados comportamentais) para provar que o sistema está seguro.

Isso é eficiente porque o robô não precisa tentar abrir todas as caixas possíveis. Ele abre apenas as que conhece e, para as demais, confia no contrato.

O "Auto-Inspeção" (Inferência de Especificação)

Uma das partes mais legais do artigo é que o robô agora pode escrever seus próprios Cartões de Garantia.

Geralmente, humanos precisam escrever esses cartões manualmente, o que é tedioso. Os autores atualizaram o robô para que ele possa examinar o código, descobrir o que o Cartão de Garantia deveria dizer e escrevê-lo para você.

Entrada: Um pedaço de código bagunçado com uma varinha mágica.
Ação do Robô: "Vejo que este código verifica se uma taxa existe. Vou escrever um Cartão de Garantia que diz: 'Esta varinha explodirá se a taxa estiver faltando'."
Resultado: O robô verifica seu próprio trabalho. Se o código corresponder ao cartão, ele passa.

Isso é demonstrado no artigo com um exemplo de Fazedor de Mercado Automatizado (AMM). Este é um sistema que negocia ativos. O robô provou que, embora a regra de precificação (a varinha mágica) pudesse ser alterada pelo usuário, o sistema nunca travaria ou perderia dinheiro, desde que a nova varinha seguisse as regras escritas em seu Cartão de Garantia.

Resumo da Conquista

O artigo afirma ter resolvido uma grande dor de cabeça na verificação de contratos inteligentes:

Tornou as "Varinhas Mágicas" (funções) seguras para uso de uma maneira que permite que sejam armazenadas, passadas adiante e alteradas dinamicamente.
Criou uma nova linguagem (Predicados Comportamentais + Rótulos de Estado) que permite ao robô falar sobre essas varinhas sem precisar vê-las por dentro.
Tornou o robô mais rápido e inteligente usando uma abordagem de "Quadro de Comutação" que alterna entre olhar para o código e olhar para o contrato.
Automatizou a papelada permitindo que o robô gere os contratos necessários para você.

Em resumo, eles ensinaram o inspetor robótico a confiar na promessa de um estranho (o contrato) sem precisar conhecer os segredos do estranho, tornando a fábrica mais segura e flexível.

Resumo Técnico: Verificação Formal de Funções Imperativas de Primeira Classe em Move

Enunciado do Problema
O Move Prover (MVP) é uma ferramenta de verificação formal projetada para contratos inteligentes Move, originalmente construída sobre um estilo de especificação modular com despacho estático. Uma extensão recente à linguagem Move introduziu funções de ordem superior, permitindo que funções sejam valores de primeira classe que podem ser passados como argumentos, armazenados em estruturas de dados e persistidos em armazenamento global. Essa capacidade habilita o despacho dinâmico, mas rompe as premissas de análise estática das quais o MVP dependia. Especificamente, quando uma função é chamada dinamicamente, suas pré e pós-condições não podem ser resolvidas no local da chamada. O chamador deve raciocinar abstratamente sobre o comportamento dos argumentos de valor-função, enquanto o verificador deve reconciliar essas especificações abstratas com as funções concretas que podem alcançar o local da chamada. Soluções existentes em outras linguagens (por exemplo, Dafny, F*, Verus) ou carecem de suporte para funções imperativas de primeira classe que modificam estado ou dependem de lógica de separação, o que pode levar a codificações SMT complexas. O desafio é suportar esses recursos dinâmicos de forma eficiente, garantindo que a verificação permaneça rápida, completa para casos relevantes e livre de instabilidade de gatilhos SMT.

Metodologia
Os autores estendem o MVP e a linguagem de especificação Move para suportar funções de ordem superior através de três mecanismos primários:

Predicados Comportamentais: A linguagem de especificação é estendida com predicados que caracterizam o comportamento de valores-função ( $f$ ) em argumentos específicos ( $\bar{x}$ ) e resultados ( $\bar{y}$ ). Estes incluem:
- requires_of<f>(x): Pré-condições.
- aborts_of<f>(x): Condições de abortação.
- ensures_of<f>(x, y): Pós-condições.
  Esses predicados rastreiam implicitamente dependências de estado de leitura e leitura/escrita, permitindo que especificações se refiram abstratamente a argumentos de função sem incorporar seus corpos.
Rótulos de Estado: Para raciocinar sobre transições de estado sequenciais e estados intermediários de memória, os autores introduzem rótulos de estado (por exemplo, $S$ ). Esses rótulos nomeiam pontos específicos na execução. Predicados podem ser de estado único ( $S \mid \sim p$ ) ou de dois estados ( $S.. \mid \sim q$ ), permitindo a composição de predicados comportamentais para descrever sequências de operações (por exemplo, o estado pós de uma função tornando-se o estado pré de outra).
Codificação SMT via Discriminação de Variantes: No nível SMT, valores-função são codificados usando tipos de dados algébricos que representam todas as fontes possíveis de um valor-função (closures concretas, parâmetros de função ou campos de estrutura). Quando um valor-função é invocado:
- Se a função concreta é conhecida (por exemplo, uma closure específica), a invocação é substituída pelo efeito dessa função concreta.
- Se a função é desconhecida (por exemplo, um parâmetro ou uma closure carregada do armazenamento), a invocação é modelada usando os predicados comportamentais associados ao tipo desse valor-função.
- A codificação utiliza construções "havoc" e "assume" para modelar modificações de memória e garante que as condições de quadro sejam respeitadas, distinguindo entre os mapas de memória de estado pré e estado pós.

Contribuições Principais
O artigo detalha as seguintes contribuições específicas:

Extensões de Linguagem: A introdução de predicados comportamentais e rótulos de estado à linguagem de especificação Move, tornando as especificações de função cidadãos de primeira classe capazes de rastrear dependências de estado.
Implementação no MVP: Uma codificação baseada em Boogie que discrimina variantes de valores-função nos locais de chamada. Essa abordagem evita a necessidade de lógica de separação ao aproveitar a separação de memória estática de Move (modelo de recursos), levando a codificações SMT mais eficientes.
Inferência de Especificação: Uma extensão da ferramenta de análise de pré-condição mais fraca (WP) do MVP para lidar com código de ordem superior. Essa ferramenta deriva semi-automaticamente especificações baseadas em predicados comportamentais a partir de bytecode Move arbitrário, reduzindo a carga de anotação manual e fornecendo um pipeline de validação para os novos construtos.
Tratamento de Efeitos Colaterais Imperativos: Diferentemente de algumas ferramentas existentes (por exemplo, Dafny), essa abordagem suporta funções imperativas de primeira classe que modificam estado via referências no estilo Rust e variáveis globais.

Resultados e Validação
Os autores demonstram a abordagem usando um exemplo de Criador de Mercado Automatizado (AMM) onde uma curva de precificação é armazenada como um valor-função. O sistema verifica com sucesso:

Invariantes: Propriedades como "a função nunca aborta", "monotonicidade de saída" e "preservação de produto constante" são verificadas usando predicados comportamentais e rótulos de estado.
Verificação de Conformidade: A ferramenta de inferência de especificação deriva automaticamente condições de abortação para funções de precificação (por exemplo, detectando que uma função de precificação baseada em taxas aborta se um recurso de taxa estiver ausente), permitindo verificações de conformidade legíveis por máquina sem anotações manuais.
Suite de Testes: Uma suite de testes abrangente cobrindo chamadas diretas, recursão mútua, parâmetros de ordem superior e despacho de closures armazenadas confirma que a codificação é internamente consistente e que as especificações inferidas são suficientemente precisas para que o verificador as descarregue.

Significado
O artigo afirma que este trabalho permite a verificação rotineira e orientada à produção de contratos inteligentes Move que apresentam despacho dinâmico e funções de ordem superior. Ao preservar o modelo de custos do MVP — onde a verificação é concluída em segundos por função —, a extensão permite que desenvolvedores utilizem padrões complexos como fluxos de ativos baseados em callbacks e gerentes de ativos extensíveis com garantias formais. A abordagem distingue-se de ferramentas baseadas em lógica de separação ao utilizar a separação de memória estática inerente a Move para simplificar codificações SMT. Além disso, a integração da inferência de especificação fornece um caminho prático para verificar a conformidade de valores-função, abordando uma barreira significativa para a adoção de funções de ordem superior em contratos inteligentes críticos para segurança. O trabalho reconhece que, embora a verificação do lado da aplicação seja agora comparável à de funções de primeira ordem, a verificação do lado da conformidade (provar que uma função passada satisfaz um contrato) ainda pode exigir dicas de prova manuais ou suposições confiáveis em casos complexos.