Lenguaje de Especificación de Move

Este documento describe el lenguaje de especificación de Move (MSL), un subconjunto del lenguaje Move que soporta especificación del comportamiento de programas Move. MSL funciona junto con el Move Prover, una herramienta que puede verificar estáticamente la corrección de especificaciones MSL contra programas Move. En contraste con las pruebas tradicionales, la verificación de MSL es exhaustiva y se mantiene para todas las posibles entradas y estados globales de un módulo Move o script Move. Al mismo tiempo, esta verificación de MSL es lo suficientemente rápida y automatizada que puede ser usada en un lugar similar en el flujo de trabajo del desarrollador donde las pruebas típicamente se realizan (por ejemplo, para calificación de pull requests en integración continua).

Mientras el lenguaje de programación Move en este punto es estable, el subconjunto representado por MSL debe considerarse en evolución. Esto no tiene impacto en la estabilidad de la plataforma, ya que MSL no se ejecuta en producción; sin embargo MSL se usa para aseguramiento de calidad offline donde se mejora continuamente para objetivos en evolución.

Este documento describe solo el lenguaje; ver Usar el Move Prover para instrucciones. Se espera que el lector tenga conocimiento básico del lenguaje Move, así como principios básicos de especificaciones de pre- y post-condición. (Ver por ejemplo el Diseño por contrato). Para ejemplos de especificaciones, nos referimos a la documentación del framework de Aptos, que tiene especificaciones integradas.

Expresiones

Las expresiones en MSL son un subconjunto de expresiones de programas Move más un conjunto de construcciones adicionales, como se discute en las siguientes secciones.

Sistema de Tipos

El sistema de tipos de MSL es similar al de Move, con las siguientes diferencias:

• Hay dos tipos de codificaciones para tipos enteros: num y bv (vector de bits). Si un entero (ya sea una constante o una variable) no está involucrado en operaciones bitwise directa o indirectamente, independientemente de su tipo en Move (u8, u16, u32, u64, u128 y u256), se trata como el mismo tipo. En especificaciones, este tipo se llama num, que es un tipo entero con signo de precisión arbitraria. Cuando MSL se refiere a un nombre Move que representa un u8 o similar, será automáticamente ampliado a num. Esto permite escribir expresiones MSL como x + 1 <= MAX_U128 o x - y >= 0 sin necesidad de preocuparse por desbordamiento o subdesbordamiento. Diferente de num, bv no puede y no necesita ser usado explícitamente en especificaciones: si un entero está involucrado en operaciones bitwise como &, | o ^, será automáticamente codificado como bv en el backend. Además, un entero bv tiene una precisión fija, que es consistente con su precisión en Move (bv8, bv16, bv32, bv64, bv128 y bv256). Nota que, en general usar bv no es tan eficiente como num en el solver SMT como Z3. Consecuentemente, el Move Prover tiene algunas restricciones al usar operaciones bitwise, que se establecen en detalle abajo.
• Los tipos Move &T, &mut T, y T se consideran equivalentes para MSL. La igualdad se interpreta como igualdad de valor. No hay necesidad de preocuparse por desreferenciar una referencia del programa Move: estas se desreferencian automáticamente según sea necesario. Esta simplificación es posible porque MSL no puede modificar valores de un programa Move, y el programa no puede razonar directamente sobre igualdad de referencia (lo que elimina la necesidad de hacerlo en MSL). (Nota que también hay una restricción en expresividad que viene con esto, a saber para funciones que devuelven &mut T. Sin embargo, esto raramente se encuentra en la práctica, y hay soluciones alternativas).
• Hay el tipo adicional type, que es el tipo de todos los tipos. Solo puede usarse en cuantificadores.
• Hay el tipo adicional range, que representa un rango de enteros (y la notación n..m para denotar un valor).

Nomenclatura

La resolución de nombres en MSL funciona similar al lenguaje Move. Las declaraciones use pueden introducir alias para nombres importados. Los nombres de funciones MSL y variables deben comenzar con una letra minúscula. Los nombres de esquemas se tratan como tipos y deben comenzar con una letra mayúscula. (Los esquemas son una construcción nombrada discutida más adelante).

Las funciones Move, funciones MSL, tipos Move, y esquemas todos comparten el mismo namespace y son por lo tanto no ambiguos si se les da alias a través de una cláusula use de Move. Debido al namespace común, una función MSL no puede tener el mismo nombre que una función Move. Esto a menudo se maneja a través de la convención de prefijar funciones MSL como en spec_has_access cuando la función Move relacionada se llama has_access.

Operadores

Todos los operadores Move son soportados en MSL, excepto &, &mut, y * (desreferencia).

Además de los operadores existentes, subíndice de vector v[i], rebanado v[i..j], y construcción de rango i..j son soportados (el tipo de rangos de enteros es un nuevo tipo incorporado llamado range). Además, la implicación booleana p ==> q es soportada como una forma más intuitiva que !p || q.

Llamadas de función

En expresiones MSL, las funciones pueden llamarse como en Move. Sin embargo, el llamado debe ser una función auxiliar MSL o una función Move pura.

Las funciones Move se consideran puras si no modifican el estado global y no usan características de expresión Move que no son soportadas en expresiones MSL (como se define en este documento).

Hay una extensión. Si una definición de función Move contiene un assert directo, esto será ignorado cuando se llame desde una expresión MSL, y la función se considerará pura. Por ejemplo:

module 0x42::m {
  fun get(addr: address): &T {
    assert(exists<T>(addr), ERROR_CODE);
    borrow_global<T>(addr)
  }
}

Cuando se llama get(addr) desde una expresión MSL, el assert será ignorado y la función se comportará como si solo contuviera borrow_global<T>(addr).

Construcciones de Especificación

MSL proporciona varias construcciones de especificación que permiten expresar propiedades de programas Move:

Especificaciones de Función

Las especificaciones de función describen el comportamiento esperado de funciones Move:

spec my_function {
    // Pre-condiciones
    requires condition;

    // Post-condiciones
    ensures condition;

    // Condiciones de aborto
    aborts_if condition;
}

Invariantes

Los invariantes describen propiedades que deben mantenerse verdaderas:

spec module {
    // Invariante global
    invariant condition;
}

spec struct MyStruct {
    // Invariante de estructura
    invariant field > 0;
}

Funciones Auxiliares

Las funciones auxiliares permiten factorizar lógica común en especificaciones:

spec module {
    fun spec_is_valid(x: num): bool {
        x > 0 && x < 100
    }
}

Esquemas

Los esquemas permiten reutilizar especificaciones comunes:

spec schema ValidRange<T> {
    x: T;
    requires x > 0;
    ensures result > x;
}

Este documento cubre los conceptos básicos del lenguaje de especificación de Move. Para uso avanzado y ejemplos más detallados, consulta la documentación del framework de Aptos y los ejemplos en el repositorio de aptos-core.