En el capítulo anterior, aprendimos que una especificación es una pieza de código escrita en CVL que describe el comportamiento esperado de un contrato inteligente. Una especificación consta principalmente de:

• Reglas
• El Bloque de Métodos

Los cuerpos de estas reglas y el Bloque de Métodos están compuestos por sentencias de CVL.

En este capítulo, aprenderemos sobre las sentencias de CVL.

Introducción a las sentencias de CVL

Según la documentación oficial de Certora , “Las sentencias describen los pasos que simula el Prover al evaluar una regla.” En otras palabras, las sentencias definen las condiciones y acciones que guían cómo el Certora Prover evalúa un contrato inteligente frente a una regla.

CVL ofrece una amplia gama de sentencias para escribir reglas, pero por ahora nos centraremos en las siguientes:

• require – Se utiliza para especificar una condición que debe cumplirse antes de ejecutar la regla.
• assert – Se utiliza para especificar una condición que debe cumplirse en todas las rutas de ejecución para que una regla se evalúe como verificada.
• satisfy – Se utiliza para afirmar que existe al menos una ruta de ejecución válida.

¿Qué significa “Ruta de Ejecución”?

Al verificar un contrato inteligente, el Prover explora diferentes estados y transiciones posibles para comprobar que la regla se cumple bajo todos los escenarios. Una ruta de ejecución se refiere a una secuencia específica de llamadas a funciones y cambios de estado por los que pasa el contrato durante la verificación.

Entendiendo el uso de assert

La sentencia assert en CVL se utiliza para verificar una condición que debe ser verdadera durante la ejecución del contrato. Toda regla debe concluir con una sentencia assert o satisfy.

Si una regla no termina con una sentencia assert o satisfy, el Prover no puede determinar qué condición se debe comprobar, lo que genera un error. Por ejemplo, considere ejecutar la siguiente especificación del capítulo anterior con las sentencias assert comentadas:

Copy
methods {
    function count() external returns(uint256) envfree;
    function increment() external envfree;
    function decrement() external envfree;
}


rule checkIncrementCall() {

    //Precall Requirement
    require count() == 0;

    // Call OR Action
    increment();


    // Post-call Expectation
    //assert count() == 1;

}
rule checkCounter() {

    //Retrieval of Pre-call value
    uint256 precallCountValue = count();

    // Call
    increment();
    decrement();

    //Retrieval of Post-call value
    uint256  postcallCountValue = count();

    //Post-call Expectation
    //assert postcallCountValue == precallCountValue;
}

Dado que ninguna de las reglas anteriores incluye una sentencia assert al final, el Prover no puede determinar qué propiedad verificar. Esto da como resultado el error “last statement of the rule …… is not an assert or satisfy command (but must be)”, como se muestra a continuación.

La sentencia assert contiene el estado esperado del contrato en forma de expresión, junto con una cadena de mensaje opcional que describe la expresión, como se muestra a continuación:

Copy
assert Expression, "An Optional Message String";
//OR
assert Expression;

Durante la verificación, una regla pasa si todas las rutas de ejecución satisfacen las condiciones expresadas en sus sentencias assert. Sin embargo, si alguna sentencia assert se evalúa como falsa en cualquier ruta de ejecución, la regla se considera violada.

Definiendo puntos de referencia de validación para el contrato Counter

Para comprender mejor cómo funciona la sentencia assert, revisemos nuestro ejemplo anterior Counter y exploremos su funcionalidad con más detalle.

Copy
//SPDX-License-Identifier: MIT
pragma solidity 0.8.24;
contract Counter {

    uint256 public count;
    
    function increment() external {
        count++;
    }
}

Se puede considerar que el contrato anterior funciona correctamente si satisface las siguientes condiciones durante las pruebas:

1. Una vez desplegado el contrato, la variable count debe inicializarse correctamente.
2. Cuando se llama a increment(), el valor de count debe aumentar en 1.

Transformando expectativas en comprobaciones de aserción

Ahora, supongamos que queremos verificar formalmente nuestras expectativas para el contrato Counter. Para hacer esto, definimos una regla llamada checkCountValidity(), que asegura que la variable count comience en cero y se incremente correctamente con cada llamada a la función.

Copy
rule checkCountValidity(.......)

Así es como funciona la regla, paso a paso:

1. Capturar el estado inicial: Primero recuperamos el valor actual de count usando el getter count() y lo almacenamos en una variable llamada PrecallCountValue. Esto nos da un punto de referencia antes de que ocurra cualquier modificación.

Copy
rule checkCountValidity() {

    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();
}

2. Realizar los incrementos: Luego llamamos a la función increment() tres veces para aumentar el contador.

Copy
rule checkCountValidity() {

    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    // Call to increment()
    increment();
    increment();
    increment();
}

3. Recuperar el estado actualizado: Después de ejecutar las llamadas a increment(), obtenemos el nuevo valor de count y lo almacenamos en PostcallCountValue. Esto nos permite comparar el estado antes y después de las ejecuciones de la función.

Copy
rule checkCountValidity() {

    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    // Call to increment()
    increment();
    increment();
    increment();

    // Grabbing the state of count after the increment() calls
    uint256 PostcallCountValue = count();

}

4. Validar el estado inicial: Para garantizar la exactitud, usamos una sentencia assert para verificar que count era inicialmente 0, confirmando que el contrato comienza desde un estado conocido y esperado.

Copy
rule checkCountValidity() {

    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    // Call to increment()
    increment();
    increment();
    increment();

    // Grabbing the state of count after the increment() calls
    uint256 PostcallCountValue = count();

    // Assertions 
    assert PrecallCountValue == 0;
}

5. Verificar el comportamiento del incremento: Finalmente, afirmamos que count ha aumentado exactamente en 3, confirmando que cada llamada a increment() agregó con éxito 1 al valor.

Copy
rule checkCountValidity() {
    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    // Call to increment()
    increment();
    increment();
    increment();

    // Grabbing the state of count after the increment() calls
    uint256 PostcallCountValue = count();

    // Assertions
    assert PrecallCountValue == 0;
    assert PostcallCountValue == PrecallCountValue + 3;
}

Podemos ver cómo usamos las sentencias assert para hacer cumplir nuestras expectativas sobre el comportamiento del contrato.

¿Cuál es el resultado esperado?

A primera vista, se podría esperar que checkCountValidity pase la verificación porque:

1. Inicialización por defecto: El contrato Counter no inicializa explícitamente la variable de estado count, por lo que Solidity la establece automáticamente en 0. Como resultado, cuando la regla recupera el valor inicial usando count(), debería devolver 0, haciendo que la aserción PrecallCountValue == 0 sea válida para cualquier ruta de ejecución.
2. Comportamiento de incremento: Cada llamada a increment() aumenta la variable count en 1. Dado que la regla llama a increment() tres veces, el valor final esperado de count debería ser PrecallCountValue + 3. Por lo tanto, se espera que la aserción PostcallCountValue == PrecallCountValue + 3 se cumpla como verdadera para cualquier ruta de ejecución.

Ejecutando la verificación

Sin embargo, al ejecutar el proceso de verificación, encontrará un resultado inesperado como se muestra a continuación.

En el resultado anterior, podemos ver claramente que el Prover falló al verificar la regla checkCountValidity(). Esto sugiere que al menos una de las siguientes condiciones se evaluó como falsa, resultando en una violación de la regla:

• assert PrecallCountValue == 0
• assert PostcallCountValue == PrecallCountValue + 3

En caso de una violación, el Prover genera un informe detallado describiendo la violación, incluyendo información sobre qué aserción falló, los valores relevantes de las variables y los pasos de ejecución que llevaron al fallo.

Interpretando los fallos de verificación mediante contraejemplos

Para entender la violación, el Certora Prover proporciona contraejemplos. En términos simples, un contraejemplo es una ruta de ejecución específica donde la verificación de una regla falla.

Para ver el contraejemplo de nuestra regla violada, haga clic en el nombre de la regla violada (checkCountValidity) en la página del informe para obtener una vista similar a la siguiente.

Al hacerlo, se muestran los valores de los parámetros y variables de la regla (en el lado derecho), y una traza de llamada (en el centro), como se muestra a continuación.

Al investigar una violación, la traza de llamada es extremadamente útil ya que proporciona información detallada sobre las variables de estado al comienzo de la ejecución de la regla y también rastrea las actualizaciones de esas variables a lo largo de la ejecución, como se muestra a continuación:

En el contraejemplo proporcionado por el Certora Prover, podemos ver claramente que nuestra regla falló la verificación porque la regla esperaba que count comenzara en 0, pero en su lugar comenzó en 10, lo que causó que assert PrecallCountValue == 0 fallara.

Esto plantea una pregunta importante: ¿Por qué count se establece en 10 en lugar del 0 esperado por defecto? Para entender esto, necesitamos comprender cómo Solidity y CVL manejan las variables no inicializadas de manera diferente.

¿Por qué el valor de count se establece en 10 en lugar de 0?

Como sabemos, si un contrato inteligente de Solidity no inicializa explícitamente una variable de estado, se le asigna automáticamente un valor por defecto basado en su tipo. Por ejemplo:

• Para uint256, el valor por defecto es 0 .
• Para bool, el valor por defecto es false .
• Para address, el valor por defecto es la dirección cero.

A diferencia de Solidity, CVL no asigna automáticamente valores por defecto a las variables. En su lugar, las variables no inicializadas en CVL permanecen sin restricciones (unconstrained), lo que significa que pueden tomar cualquier valor posible dentro de su rango definido durante la verificación. Esto se relaciona con un concepto crucial: las reglas de CVL no inician la verificación desde el estado de despliegue inicial específico del contrato (como suele asumir la ejecución en Solidity), sino desde un estado arbitrario. Esta es una diferencia clave y un aspecto fundamental de la verificación formal.

Debido a este comportamiento, el valor inicial de count se estableció en 10 durante la verificación, lo que provocó que la regla fallara, ya que esperábamos que count comenzara en 0.

Entendiendo el uso de require

Como se observó anteriormente, el Prover asigna valores arbitrarios a las variables de estado durante el proceso de verificación, lo que puede dar lugar a valores iniciales inesperados y provocar el fallo de las aserciones si la regla asume los valores por defecto de Solidity.

En tales casos, es posible que queramos definir explícitamente restricciones sobre las variables de estado en nuestra configuración de verificación, asegurando que comiencen con los valores esperados antes de ejecutar la regla. Aquí es donde la sentencia require en CVL resulta útil.

La sentencia require en CVL se utiliza para especificar precondiciones para una regla, asegurando que se cumplan ciertas condiciones antes de que la regla se considere válida.

Cuando se incluye una sentencia require en una regla, actúa como un filtro que le dice al Prover que ignore cualquier ruta de ejecución donde la condición especificada no se cumpla. Esto significa que el Prover solo considerará escenarios en los que la expresión require se evalúe como verdadera, excluyendo efectivamente a todas las demás del análisis.

Por ejemplo, podemos usar la sentencia require en nuestra regla checkCountValidity para restringir el valor inicial de count a cero, como se muestra a continuación:

Copy
rule checkCountValidity() {

    // We just added this 
    
require count() == 0;


    // Grabbing the initial state of the count variable
    uint256 PrecallCountValue = count();

    //Call to increment()
    increment();
    increment();
    increment();

    //Grabbing the state of count after the increment() calls
    uint256 PostcallCountValue = count();

    // Asserting that the initial value of count is 0
    assert PrecallCountValue == 0;
    assert PostcallCountValue == PrecallCountValue + 3;

}

Si vuelve a ejecutar el Prover con el cambio anterior y abre el enlace de verificación impreso en su terminal, obtendrá una regla verificada, como se muestra a continuación.

Esta vez, podemos ver que el Prover ha verificado con éxito nuestra regla. Esto se debe a que, con la restricción require, el prover ignorará cualquier ruta de ejecución donde el valor inicial de count no sea cero.

Por defecto, el Prover no proporciona una traza de llamada para una regla verificada porque puede haber un número extremadamente grande de trazas de ejecución válidas que satisfagan las condiciones de la regla. Dado que una regla verificada confirma que no existen contraejemplos, generar y mostrar todas las trazas válidas posibles sería innecesario y poco práctico.

Entendiendo el uso de satisfy

Como se mencionó anteriormente, el Prover no genera una traza de llamada cuando una regla se verifica con éxito. Sin embargo, CVL ofrece la sentencia satisfy, la cual le permite producir una traza de ejecución que cumpla con todas las condiciones impuestas por las sentencias require y assert. Esto es especialmente útil cuando se desea confirmar si un escenario específico puede ocurrir dentro de la lógica del contrato.

Por ejemplo, podemos escribir una regla que use la sentencia satisfy para verificar:

• Que exista al menos una ruta de ejecución donde un usuario pueda retirar completamente su liquidez después de depositar y acuñar tokens LP.
• Que exista al menos una ruta de ejecución donde la posición de un prestatario sea liquidada si el valor de su colateral cae por debajo de un umbral especificado.

Cuando una regla incluye la sentencia satisfy, el Prover comprueba si al menos una ruta de ejecución válida satisface la condición. Aunque puede haber múltiples de estas rutas, solo se genera una traza satisfactoria (si se encuentra). Basándose en el resultado, la regla se clasifica de la siguiente manera:

• Regla Verificada: El Prover informa la regla como verificada si al menos una ejecución válida satisface la sentencia satisfy.
• Regla Violada: El Prover informa la regla como violada si ninguna ruta de ejecución satisface la sentencia satisfy.

Usando satisfy en una regla

Para entender cómo funciona la sentencia satisfy, considere la siguiente especificación que tiene una regla searchValidExecution() que termina con una sentencia satisfy.

Copy
methods {
    function count() external returns(uint256) envfree;
    function increment() external  envfree;
}

rule searchValidExecution {

    increment();
    increment();
    increment();

    satisfy count() == 8;
}

Dado que la regla searchValidExecution termina con una sentencia satisfy, instruye al Prover a explorar posibles rutas de ejecución y determinar si existe una secuencia de tres llamadas a increment() que daría como resultado que count() alcance un valor de 8. Si encuentra una ruta de este tipo, el Prover reporta la regla como verificada. De lo contrario, la reporta como violada.

Para comprobar si la regla searchValidExecution se cumple, ejecute el Prover y abra el enlace de verificación en un navegador para ver el resultado.

Los resultados anteriores muestran que el Certora Prover ha verificado con éxito la regla. Esto significa que encontró al menos una ruta de ejecución que satisface la sentencia satisfy. Específicamente, el Prover identificó un estado donde count() alcanza 8 después de tres llamadas sucesivas a increment().

Este resultado se alinea con las expectativas porque, idealmente, el valor de count() puede llegar a 8 después de tres llamadas sucesivas a increment() si el valor inicial es 5 (asumiendo que cada llamada aumenta el contador en 1). Dado que la regla busca una ruta de ejecución válida, el Prover confirmó su existencia, lo que condujo a una verificación exitosa.

Usando el Prover para resolver y verificar sistemas de ecuaciones lineales

Dado que el Prover evalúa solo una única ruta de ejecución al procesar una regla que contiene una sentencia satisfy, funciona como un solucionador (solver), determinando los valores de entrada que satisfacen las restricciones dadas. Para demostrar esta capacidad, usemos satisfy para encontrar una solución a un sistema de ecuaciones.

Por ejemplo, considere las siguientes ecuaciones:

• $2x + 3y = 22$
• $4x - y = 2$

Ahora, supongamos que queremos encontrar valores enteros de $x$ y $y$ que satisfagan ambas ecuaciones. Para lograr esto, primero debemos definir una función de Solidity que codifique el sistema de ecuaciones**:**

Copy
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

contract Math {

    function eqn(uint256 x, uint256 y) external pure returns (bool) {
        return (2 * x + 3 * y == 22) && (4 * x - y == 2);
    }

}

Una vez que definimos la función de Solidity, podemos crear una regla para instruir al Prover a que busque valores válidos de $x$ y $y$ que satisfagan las restricciones como se muestra a continuación:

Copy
methods {

    function eqn(uint256, uint256) external returns (bool) envfree;
}

rule checkEqn() {

    uint256 x; 
    uint256 y;

    satisfy eqn(x, y) == true;
}

Alternativamente, las variables pueden definirse directamente en la declaración de la regla en lugar de declararse dentro del cuerpo de la regla, como se muestra a continuación:

Copy
rule checkEqn(uint256 x, uint256 y) {
    satisfy eqn(x, y) == true;
}

Cuando se ejecuta la regla, el Prover intenta encontrar valores para $x$ y $y$ que hagan que la función devuelva verdadero. En este caso, la solución entera correcta es $x = 2$ y $y = 6$.

Además, si las ecuaciones se modifican de una manera que las hace inconsistentes —como al definir líneas paralelas— el Prover detectará que no existe solución. Considere el sistema modificado:

• $2x + 3y = 22$
• $4x + 6y = 50$

Dado que la segunda ecuación es solo un múltiplo de la primera ecuación pero con una constante diferente, el sistema no tiene soluciones porque las dos líneas ahora son paralelas y nunca se cruzan. La función equivalente en Solidity es:

Copy
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

contract Math {

    function eqn(uint256 x, uint256 y) external pure returns (bool) {
        return (2 * x + 3 * y == 22) && (4 * x + 6 * y == 50);
    }

}

Cuando volvemos a ejecutar la regla checkEqn() en esta función modificada, el resultado de la verificación indica que el Prover identifica correctamente la ausencia de una solución válida.

Los resultados anteriores resaltan la capacidad del Prover no solo para encontrar soluciones válidas cuando existen, sino también para detectar y confirmar cuando un conjunto de restricciones es inherentemente insatisfactible, como en el caso de ecuaciones inconsistentes o paralelas.

Consideraciones clave al usar sentencias satisfy

Hay algunos matices importantes a tener en cuenta al usar la sentencia satisfy en cualquier regla:

• Si una regla contiene múltiples sentencias satisfy, el Prover la informará como verificada solo si todas las sentencias satisfy ejecutadas se cumplen para al menos una ruta de ejecución; de lo contrario, la regla se considerará violada (en el modo por defecto del Prover) como se muestra a continuación:

• Una sentencia satisfy en una rama condicional que no se ejecuta no necesita cumplirse, ya que nunca se alcanza durante la verificación. El Prover verifica cada ruta de ejecución de forma independiente y reporta los resultados de las rutas ejecutadas, como se muestra a continuación.

Diferencia entre assert y satisfy

A primera vista, las sentencias assert y satisfy pueden parecer similares en funcionalidad, ya que ambas se utilizan para validar condiciones dentro de una regla. Sin embargo, sus propósitos y usos son bastante diferentes, como se muestra a continuación:

Conclusión

En este capítulo, examinamos cómo las sentencias de CVL guían al Certora Prover durante la verificación. Aprendimos cómo assert hace cumplir propiedades en todas las rutas de ejecución, cómo require restringe los estados que el Prover considera y cómo satisfy demuestra la existencia de rutas de ejecución válidas. Entender estas sentencias y cómo el Prover razona sobre estados arbitrarios es esencial para escribir reglas de CVL correctas y efectivas.

Este artículo es parte de una serie sobre verificación formal usando Certora Prover