En el último capítulo, vimos que para realizar una verificación formal usando Certora Prover, necesitamos proporcionar al Prover los siguientes elementos clave:

1. Contrato Inteligente (archivo .sol)
2. Especificación (archivo .spec)

En este capítulo, discutiremos qué significa exactamente una especificación y cómo escribir una.

¿Qué es una Especificación?

En Certora, una especificación es un fragmento de código escrito en Certora Verification Language (CVL) que define un conjunto de reglas que el contrato bajo verificación debe cumplir o respetar.

Una especificación de Certora o archivo .spec debe tener al menos dos componentes:

1. Una o más reglas
2. Un bloque de métodos

Hay otros componentes, pero por ahora, nos centraremos en estos e introduciremos el resto a medida que los usemos.

Entendiendo las reglas

Una regla define el comportamiento esperado de “antes y después” de la llamada a una función en el contrato inteligente. Se define utilizando la palabra clave rule, seguida de su nombre, como se muestra a continuación:

Copy
rule nameOfRule{}

En CVL, una regla se escribe utilizando los siguientes tres conceptos fundamentales:

1. Requisito precondicional (opcional): Esto especifica las condiciones bajo las cuales una regla debe ser evaluada por el Prover. Se especifica utilizando la declaración require.
2. Acción: Una llamada a un método que cambia el estado del contrato.
3. Expectativa posterior a la llamada: Esta parte especifica el estado esperado del contrato después de que se ejecuta la acción. Se especifica utilizando la declaración assert.

Nota: Discutiremos las declaraciones require y assert con mucho más detalle en el próximo capítulo.

Para entender mejor los conceptos discutidos anteriormente, considere el contrato Counter a continuación.

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

contract Counter {  
    uint256 public count;  

    // Increment the count  
    function increment() public {  
        count += 1;  
    }  

    // Decrement the count  
    function decrement() public {    
        count -= 1;  
    }  

}

Ahora considere la regla a continuación que está escrita para verificar formalmente la función increment() del contrato Counter.

Copy
rule checkIncrementCall() {

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

    // Call OR Action
    increment();


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

}

En nuestra regla checkIncrementCall():

• La línea require count() == 0 define el requisito precondicional al instruir al Prover que considere esta regla solo cuando el valor inicial de count sea cero.
• La línea increment() realiza una transición de estado al invocar la función increment() en el contrato. Esto representa la acción que se está probando.
• La línea assert count() == 1 define la expectativa posterior a la llamada, que especifica el estado esperado después de la acción. Aquí, garantiza que después de llamar a increment() en un contador que inicialmente estaba configurado en cero, el valor del contador se actualice a 1.

Necesitamos combinar los tres porque:

• Sin una acción, no hay nada que probar, ya que el estado del contrato permanece sin cambios.
• Si no incluimos verificaciones de poscondición, en realidad no estamos verificando nada. Las verificaciones de aserciones (declaraciones assert) aseguran que las transiciones de estado del contrato se alineen con nuestras expectativas.
• Sin la precondición, la regla podría aplicarse a escenarios no previstos.

Es importante tener en cuenta que las precondiciones son opcionales. Deben usarse con precaución, ya que podrían excluir escenarios importantes que necesitan ser verificados.

Algunas reglas se pueden implementar sin ningún requisito precondicional****. Por ejemplo, la regla a continuación comprueba la integridad de nuestro contrato Counter al verificar que las llamadas secuenciales a increment() y decrement() dan como resultado un valor de count sin cambios.

Copy
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;
}

Sin embargo, a nuestro archivo de especificación todavía le falta el bloque de métodos. Agreguémoslo antes de enviarlo al Prover para su verificación.

El bloque de métodos y su uso

El bloque de métodos contiene una lista de métodos del contrato que las reglas llamarán durante la verificación. Puede pensar en ello como una interfaz o ABI en Solidity: le dice al Prover qué funciones existen, cómo son y cómo se pueden llamar. La versión de Certora a veces tiene un poco de sintaxis adicional en comparación con Solidity simple.

El bloque de métodos se define utilizando la palabra clave methods, como se muestra a continuación:

Copy
methods {
// Contract methods entries go here
}

Cada entrada en el bloque de métodos debe seguir la sintaxis a continuación:

• Cada entrada debe comenzar con la palabra clave function para definir el método.
• Especifique el nombre del método exactamente como aparece en el contrato.
• Enumere los parámetros de entrada entre paréntesis, separando múltiples entradas con comas. Si el método no toma ninguna entrada, deje los paréntesis vacíos.
• Agregue un modificador de visibilidad, que para nuestros propósitos debería ser external para todos los métodos. Las especificaciones más avanzadas pueden resumir funciones internas, lo cual cubriremos más adelante.
• Use la palabra clave returns seguida del tipo de retorno si el método devuelve un valor. Si no hay valor de retorno, esta parte no es necesaria.
• Agregue una etiqueta opcional como envfree (discutiremos otras etiquetas a medida que las usemos).
• Termine cada declaración de método con un punto y coma (;)

Es muy importante tener en cuenta que agregar funciones al bloque de métodos no hará que la verificación sea más rápida o más efectiva a menos que esas funciones estén marcadas como envfree, optional o tengan un resumen. Si no se cumple ninguna de estas condiciones, agregar la función no tendrá ningún impacto, y es probable que el verificador emita una advertencia al respecto en el informe.

Para mantener las cosas simples y fáciles de entender, en este capítulo solo nos centraremos en envfree. Exploraremos optional y la summarization en un capítulo aparte.

¿Cuándo usar la etiqueta envfree?

Un método en el bloque de métodos se declara envfree cuando su ejecución no depende de las variables globales de Solidity, como msg.sender, block.number o tx.origin.

Por ejemplo, considere la función add() a continuación:

Copy
function add(uint256 x, uint256 y) external returns (uint256) {
    return x + y;
}

Dado que add() opera exclusivamente en sus parámetros de entrada y no necesita acceso a ningún estado global de la blockchain como block.timestamp, msg.sender, msg.value o tx.origin para su ejecución, significa que podemos declararlo como envfree en el bloque de métodos, como se muestra a continuación:

Copy
methods {  
    add(uint256, uint256) external returns(uint256) envfree;  
}

Por el contrario, algunas funciones necesitan acceso al estado global de la blockchain para su ejecución y, por lo tanto, no pueden ser declaradas envfree. Por ejemplo, la función balance() a continuación recupera el saldo del llamador:

Copy
function balance() external view returns(uint256) {
    return balances[msg.sender];
}

Debido a que balance() depende de msg.sender, no se puede declarar envfree. A continuación se muestra cómo deberíamos definirlo en el bloque de métodos:

Copy
methods {  
    balance() external returns(uint256);  
}

Agregando el bloque de métodos a nuestro spec

Dado que nuestras reglas (checkIncrementCall y checkCounter) realizan llamadas a los métodos count(), increment() y decrement() del contrato Counter, el bloque de métodos para nuestra especificación debe enumerar estas funciones, como se muestra a continuación:

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

Ninguna de estas funciones requiere acceso a las variables globales de Solidity para su ejecución, por lo que las marcamos como envfree. Si el contrato tiene otras funciones que no se utilizan en nuestra especificación, no necesitamos incluirlas en el bloque de métodos.

Ejecutando la verificación

Para verificar las reglas discutidas anteriormente, siga las instrucciones a continuación:

• Abra una terminal y asegúrese de estar en el directorio certora-counter que creamos en el último capítulo.
• Abra el directorio certora-counter en VS Code o en cualquier otro editor de código de su elección.
• Cree dos archivos vacíos: Counter2.sol dentro del subdirectorio contracts y counter-2.spec dentro del subdirectorio specs.
• Copie y pegue el contrato inteligente a continuación en Counter2.sol .

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

contract Counter {  
    uint256 public count;  

    // Increment the count  
    function increment() public {  
        count += 1;  
    }  

    // Decrement the count  
    function decrement() public {    
        count -= 1;  
    }  

}

• Copie y pegue la especificación a continuación en counter-2.spec.

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;
}

• Active el entorno virtual de Python ejecutando el comando a continuación en su terminal:

Copy
source certora-env/bin/activate

• Cargue la clave de acceso de Certora como una variable de entorno en su terminal:

Copy
source .profile  # For Bash
# OR
source .zshenv  # For Zsh

• Configure la versión correcta del compilador de Solidity ejecutando el comando a continuación:

Copy
solc-select use 0.8.25

• Finalmente, envíe la especificación y el contrato al Prover para su verificación ejecutando el siguiente comando:

Copy
certoraRun contracts/Counter2.sol:Counter --verify Counter:specs/counter-2.spec

Entendiendo el resultado de la verificación

Si el Prover compila correctamente el código sin errores, imprimirá el enlace de los resultados de la verificación en su terminal.

Para ver los resultados de la verificación, abra el enlace impreso en su terminal usando un navegador. Los resultados deberían verse similares a la imagen a continuación:

En nuestro caso, muestra los resultados para tres reglas:

• checkCounter : Esto muestra los resultados de la verificación para la regla checkCounter de nuestro spec.
• checkIncrementCall : Esto muestra los resultados de la verificación para la regla checkIncrementCall de nuestro spec.
• envfreeFuncsStaticCheck : Cuando el bloque de métodos contiene funciones marcadas como envfree, el Prover verifica que no dependan de las variables globales de Solidity. Los resultados de esta verificación se publican como envfreeFuncsStaticCheck.

La marca de verificación verde (✅) indica que el Prover no ha encontrado ninguna violación, lo que significa que nuestras reglas se han verificado con éxito. En caso de una violación, se mostrará una marca de cruz roja (❌).

Aunque se verifiquen todas las reglas, esto no significa que todo el contrato esté libre de errores. Podría haber otras partes del código que tengan errores. También podría darse el caso de que nuestro spec no capture todas nuestras expectativas. Por ejemplo, no especificamos qué debería suceder si llamamos a decrement() cuando el contador está en 0. En los siguientes capítulos, mostraremos cómo expresar reglas más complejas que la que discutimos aquí.

Conclusión

En este capítulo, exploramos la anatomía de un archivo .spec, centrándonos en el bloque de métodos para la definición de la interfaz y el bloque de reglas para las pruebas de lógica. También vimos cómo etiquetas como envfree ayudan a refinar el proceso de verificación. En el próximo capítulo, construiremos sobre esta base analizando en detalle las declaraciones require y assert.

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