💻 computer science

Formal Verification of Imperative First-Class Functions in Move

Este artículo presenta una extensión al Move Prover que habilita la verificación formal de funciones imperativas de primera clase en el lenguaje Move mediante la introducción de predicados de comportamiento, etiquetas de estado y una estrategia de codificación SMT que aprovecha la separación estática de memoria de Move para una verificación eficiente y la inferencia automatizada de especificaciones.

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

Publicado 2026-05-14

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

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

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

El Panorama General: La Fábrica de "Contratos Inteligentes"

Imagina que Aptos es una fábrica de alta seguridad que construye activos digitales (como dinero o entradas) utilizando un lenguaje especial llamado Move. Para asegurarse de que estos activos no sean robados ni dañados, la fábrica utiliza un inspector robot llamado Move Prover (MVP). Este robot lee los planos (el código) y demuestra matemáticamente que todo funcionará correctamente antes de que la fábrica se ponga en marcha.

Durante mucho tiempo, este robot fue excelente para verificar instrucciones simples. Pero recientemente, la fábrica añadió una nueva y complicada característica: Funciones de Primera Clase.

Piensa en estas nuevas funciones como varitas mágicas.

Antiguo método: Tenías que sostener la varita tú mismo para lanzar un hechizo. El robot sabía exactamente qué hechizo estabas lanzando.
Nuevo método: Puedes poner la varita en una caja, entregar la caja a un amigo, guardar la caja en una bóveda o pasarla a una máquina que no sabe qué hay dentro. La máquina solo sabe: "Necesito agitar una varita", pero no sabe cuál varita hasta el último segundo.

Esto se llama Despacho Dinámico. Es poderoso, pero rompe al inspector robot porque no puede ver el futuro para saber qué hechizo específico se está lanzando.

El Problema: El Dilema de la "Caja Negra"

El documento explica cómo los autores actualizaron al inspector robot (MVP) para manejar estas varitas mágicas sin entrar en pánico.

Anteriormente, si una función era una "caja negra" (una variable que contiene una función), el robot tenía que adivinar o verificar cada posibilidad individualmente a la vez, lo que hacía que las matemáticas explotaran y el robot se volviera lento.

Los autores introdujeron dos nuevas herramientas para resolver esto:

1. Predicados Comportamentales: La "Tarjeta de Garantía"

En lugar de mirar dentro de la varita mágica para ver cómo funciona, el robot ahora mira la Tarjeta de Garantía adjunta a la varita.

El Antiguo Método: "Necesito saber exactamente cómo funciona esta varita calculate_price, hasta cada línea de código, antes de permitirte usarla".
El Nuevo Método: "No me importa cómo funciona la varita por dentro. Solo necesito leer su Tarjeta de Garantía. La tarjeta dice: 'Si me das 5 monedas, te devolveré 3 monedas, y nunca me romperé'".

El documento llama a esto Predicados Comportamentales. Son como un contrato que describe:

Precondiciones: Lo que debe ser cierto antes de que agites la varita.
Postcondiciones: Lo que será cierto después de que la agites.
Condiciones de aborto: Cuándo la varita podría explotar (fallar).

Esto permite al robot verificar la promesa de la varita sin necesidad de conocer la receta secreta que hay dentro.

2. Etiquetas de Estado: La "Cámara de Marca de Tiempo"

A veces, ocurre una secuencia de eventos. Imagina una línea de montaje donde un robot pinta un coche y luego otro robot le pone las ruedas.

Si quieres probar que el coche es seguro, necesitas conocer el estado del coche después de pintarlo pero antes de ponerle las ruedas.

Los autores introdujeron Etiquetas de Estado. Piensa en estas como Cámaras de Marca de Tiempo colocadas en puntos específicos del proceso.

Cámara A (Inicio): El coche es metal desnudo.
Cámara B (Medio): El coche está pintado.
Cámara C (Fin): Las ruedas están puestas.

El robot ahora puede decir: "Sé que la pintura ocurrió entre la Cámara A y la Cámara B, y que las ruedas se añadieron entre la Cámara B y la Cámara C". Esto ayuda al robot a razonar sobre secuencias complejas de eventos sin confundirse sobre cómo se veía el mundo en cualquier momento dado.

Cómo Funciona Realmente el Robot (El "Tablero de Conmutación")

El documento describe cómo el robot traduce estas ideas a matemáticas (lógica SMT) que una computadora puede resolver.

Imagina que el robot tiene un Tablero de Conmutación.

Escenario A (Varita Conocida): Si el robot ve una varita específica y conocida (por ejemplo, la función product), cambia el interruptor a "Modo Directo". Ignora la tarjeta de garantía y simplemente verifica el código real de esa varita específica.
Escenario B (Varita Desconocida): Si el robot ve una caja genérica (una variable), cambia el interruptor a "Modo Abstracto". Ignora el código por completo y confía únicamente en la Tarjeta de Garantía (los predicados comportamentales) para probar que el sistema es seguro.

Esto es eficiente porque el robot no tiene que intentar abrir cada caja posible. Solo abre las que conoce, y para el resto, confía en el contrato.

El "Auto-Inspector" (Inferencia de Especificaciones)

Una de las partes más geniales del documento es que el robot ahora puede escribir sus propias Tarjetas de Garantía.

Por lo general, los humanos tienen que escribir estas tarjetas manualmente, lo cual es tedioso. Los autores actualizaron al robot para que pueda mirar el código, averiguar qué debería decir la Tarjeta de Garantía y escribirla por ti.

Entrada: Un pedazo de código desordenado con una varita mágica.
Acción del Robot: "Veo que este código verifica si existe una tarifa. Escribiré una Tarjeta de Garantía que diga: 'Esta varita explotará si falta la tarifa'".
Resultado: El robot verifica su propio trabajo. Si el código coincide con la tarjeta, aprueba.

Esto se demuestra en el documento con un ejemplo de Creador de Mercado Automatizado (AMM). Este es un sistema que comercia activos. El robot demostró que, aunque la regla de precios (la varita mágica) podría ser cambiada por el usuario, el sistema nunca se bloquearía ni perdería dinero, siempre que la nueva varita siguiera las reglas escritas en su Tarjeta de Garantía.

Resumen del Logro

El documento afirma haber resuelto un gran dolor de cabeza en la verificación de contratos inteligentes:

Hizo que las "Varitas Mágicas" (funciones) fueran seguras de usar de una manera que permite almacenarlas, pasarlas y cambiarlas dinámicamente.
Creó un nuevo lenguaje (Predicados Comportamentales + Etiquetas de Estado) que permite al robot hablar de estas varitas sin necesidad de ver dentro de ellas.
Hizo al robot más rápido e inteligente utilizando un enfoque de "Tablero de Conmutación" que cambia entre mirar el código y mirar el contrato.
Automatizó la documentación permitiendo que el robot genere los contratos necesarios por ti.

En resumen, enseñaron al inspector robot a confiar en la promesa de un extraño (el contrato) sin necesidad de conocer los secretos del extraño, haciendo la fábrica más segura y flexible.

Resumen Técnico: Verificación Formal de Funciones Imperativas de Primera Clase en Move

Enunciado del Problema
El Move Prover (MVP) es una herramienta de verificación formal diseñada para contratos inteligentes en Move, construida originalmente sobre un estilo de especificación modular con despacho estático. Una extensión reciente del lenguaje Move introdujo funciones de orden superior, permitiendo que las funciones sean valores de primera clase que pueden pasarse como argumentos, almacenarse en estructuras de datos y persistir en almacenamiento global. Esta capacidad habilita el despacho dinámico, pero rompe las suposiciones de análisis estático en las que MVP confiaba. Específicamente, cuando una función se llama dinámicamente, sus precondiciones y postcondiciones no pueden resolverse en el sitio de la llamada. El llamador debe razonar abstractamente sobre el comportamiento de los argumentos de valor-función, mientras que el verificador debe conciliar estas especificaciones abstractas con las funciones concretas que pueden llegar al sitio de la llamada. Las soluciones existentes en otros lenguajes (por ejemplo, Dafny, F*, Verus) carecen de soporte para funciones imperativas de primera clase que modifican el estado o dependen de lógica de separación, lo que puede conducir a codificaciones SMT complejas. El desafío consiste en admitir estas características dinámicas de manera eficiente, asegurando que la verificación permanezca rápida, completa para los casos relevantes y libre de inestabilidad de los disparadores (triggers) del SMT.

Metodología
Los autores extienden MVP y el lenguaje de especificación de Move para admitir funciones de orden superior mediante tres mecanismos principales:

Predicados de Comportamiento: El lenguaje de especificación se extiende con predicados que caracterizan el comportamiento de los valores de función ( $f$ ) sobre argumentos específicos ( $\bar{x}$ ) y resultados ( $\bar{y}$ ). Estos incluyen:
- requires_of<f>(x): Precondiciones.
- aborts_of<f>(x): Condiciones de aborto.
- ensures_of<f>(x, y): Postcondiciones.
  Estos predicados rastrean implícitamente las dependencias de estado de lectura y lectura/escritura, permitiendo que las especificaciones hagan referencia abstracta a los argumentos de la función sin insertar sus cuerpos.
Etiquetas de Estado: Para razonar sobre transiciones de estado secuenciales y estados intermedios de memoria, los autores introducen etiquetas de estado (por ejemplo, $S$ ). Estas etiquetas nombran puntos específicos en la ejecución. Los predicados pueden ser de un solo estado ( $S \mid \sim p$ ) o de dos estados ( $S.. \mid \sim q$ ), lo que permite la composición de predicados de comportamiento para describir secuencias de operaciones (por ejemplo, que el estado posterior de una función se convierta en el estado previo de otra).
Codificación SMT mediante Discriminación de Variantes: A nivel de SMT, los valores de función se codifican utilizando tipos de datos algebraicos que representan todas las fuentes posibles de un valor de función (cierres concretos, parámetros de función o campos de estructura). Cuando se invoca un valor de función:
- Si la función concreta es conocida (por ejemplo, un cierre específico), la invocación se reemplaza por el efecto de esa función concreta.
- Si la función es desconocida (por ejemplo, un parámetro o un cierre cargado desde el almacenamiento), la invocación se modela utilizando los predicados de comportamiento asociados con el tipo de ese valor de función.
- La codificación utiliza construcciones de "havoc" (caos) y "assume" (asumir) para modelar las modificaciones de memoria y asegura que se respeten las condiciones de marco, distinguiendo entre los mapas de memoria del estado previo y del estado posterior.

Contribuciones Clave
El documento detalla las siguientes contribuciones específicas:

Extensiones del Lenguaje: La introducción de predicados de comportamiento y etiquetas de estado en el lenguaje de especificación de Move, convirtiendo las especificaciones de funciones en ciudadanos de primera clase capaces de rastrear dependencias de estado.
Implementación en MVP: Una codificación basada en Boogie que discrimina sobre las variantes de valores de función en los sitios de llamada. Este enfoque evita la necesidad de lógica de separación aprovechando la separación estática de memoria de Move (modelo de recursos), lo que conduce a codificaciones SMT más eficientes.
Inferencia de Especificaciones: Una extensión de la herramienta de análisis de precondición más débil (WP) de MVP para manejar código de orden superior. Esta herramienta deriva semi-automáticamente especificaciones basadas en predicados de comportamiento a partir de bytecode de Move arbitrario, reduciendo la carga de anotación manual y proporcionando un flujo de trabajo de validación para las nuevas construcciones.
Manejo de Efectos Secundarios Imperativos: A diferencia de algunas herramientas existentes (por ejemplo, Dafny), este enfoque admite funciones imperativas de primera clase que modifican el estado mediante referencias al estilo de Rust y variables globales.

Resultados y Validación
Los autores demuestran el enfoque utilizando un ejemplo de Creador de Mercado Automatizado (AMM) donde una curva de precios se almacena como un valor de función. El sistema verifica con éxito:

Invariantes: Propiedades como "la función nunca aborta", "monotonía de salida" y "preservación del producto constante" se verifican utilizando predicados de comportamiento y etiquetas de estado.
Verificación de Cumplimiento: La herramienta de inferencia de especificaciones deriva automáticamente condiciones de aborto para funciones de precios (por ejemplo, detectando que una función de precios basada en tarifas aborta si falta un recurso de tarifa), lo que permite verificaciones de cumplimiento legibles por máquina sin anotaciones manuales.
Conjunto de Pruebas: Un conjunto de pruebas exhaustivo que cubre llamadas directas, recursión mutua, parámetros de orden superior y despacho de cierres almacenados confirma que la codificación es internamente consistente y que las especificaciones inferidas son lo suficientemente precisas para que el verificador las descargue.

Significado
El documento afirma que este trabajo permite la verificación rutinaria y orientada a la producción de contratos inteligentes de Move que presentan despacho dinámico y funciones de orden superior. Al preservar el modelo de costos de MVP, donde la verificación se completa en segundos por función, la extensión permite a los desarrolladores utilizar patrones complejos como flujos de activos basados en callbacks y gestores de activos extensibles con garantías formales. El enfoque se distingue de las herramientas basadas en lógica de separación al utilizar la separación estática de memoria inherente a Move para simplificar las codificaciones SMT. Además, la integración de la inferencia de especificaciones proporciona una vía práctica para verificar el cumplimiento de los valores de función, abordando una barrera significativa para la adopción de funciones de orden superior en contratos inteligentes críticos para la seguridad. El trabajo reconoce que, si bien la verificación del lado de la aplicación ahora es comparable a la de funciones de primer orden, la verificación del lado del cumplimiento (demostrar que una función pasada satisface un contrato) puede requerir aún indicaciones de prueba manuales o suposiciones confiables en casos complejos.