En el capítulo anterior, aprendimos el lado teórico de la verificación formal, incluyendo qué es y cómo funciona. En este módulo, iremos más allá de la teoría y aprenderemos lo siguiente:

• Cómo configurar un proyecto para trabajar con Certora Prover.
• Cómo obtener y usar una clave de acceso de Certora.
• Cómo realizar una verificación formal usando el Certora Prover.

Empecemos configurando el entorno del proyecto para Certora Prover.

Instalando las Herramientas y Requisitos Previos Esenciales

Antes de configurar el directorio del proyecto, asegúrate de que tu máquina local tenga instalados los siguientes requisitos previos:

• Java Development Kit(JDK) 21 o más reciente

• Python 3.9 o más reciente

Puedes comprobar si tu máquina tiene ambos instalados simplemente ejecutando el comando python3 --version y java --version en tu terminal.

💡 Para los usuarios de Windows, recomendamos encarecidamente utilizar el Subsistema de Windows para Linux (WSL) para una mejor experiencia.

Configurando Nuestro Directorio del Proyecto

Una vez que los requisitos previos estén instalados, crea un directorio vacío llamado certora-counter, navega hacia él y sigue las instrucciones a continuación para configurar correctamente el directorio de tu proyecto.

1. En tu máquina local, instala virtualenv ejecutando el siguiente comando. Esta herramienta nos permitirá crear un entorno virtual de Python, lo cual es esencial para gestionar las dependencias dentro del directorio de tu proyecto.

Copy
pip3 install virtualenv

2. Una vez que tengamos instalado virtualenv, crea un entorno virtual de Python para nuestro proyecto ejecutando el siguiente comando en tu terminal.

Copy
virtualenv certora-env

3. A continuación, activa el entorno virtual de Python que creaste ejecutando el siguiente comando en tu terminal.

Copy
source certora-env/bin/activate

4. A continuación, ejecuta el siguiente comando en tu terminal para instalar el Prover.

Copy
pip3 install certora-cli

5. A continuación, instala solc-select en tu entorno virtual utilizando el siguiente comando. Esto nos permitirá cambiar convenientemente la versión del compilador de Solidity que estamos utilizando.

Copy
pip3 install solc-select

Añadiendo la Clave de Acceso Personal de Certora

Para ejecutar el Prover, necesitas configurar una clave de acceso como variable de sistema. Para obtener tu acceso personal, regístrate en el sitio web de Certora. Una vez que te registres, recibirás un correo electrónico de Certora que contendrá la clave de acceso y una contraseña inicial para tu cuenta de Certora.

Para añadir la clave de acceso como variable de sistema, sigue las siguientes instrucciones:

Para Usuarios de Linux

1. Abre una terminal y asegúrate de estar en el directorio del proyecto.
2. Crea y abre el archivo .profile utilizando el comando nano .profile.
3. Para añadir la clave de acceso como variable de entorno, añade el siguiente texto en él.

Copy
#certora access key
export CERTORAKEY=<your-certora-access-key>

4. Para guardar los cambios, presiona CTRL + O y luego presiona Enter.
5. Para salir, presiona CTRL + X.
6. Para cargar los cambios recientes que hicimos en el archivo .profile, ejecuta el siguiente comando en tu terminal.

Copy
source .profile

Para Usuarios de Mac Usando zsh

1. Abre una terminal y asegúrate de estar en el directorio certora-counter.
2. Crea un archivo con el nombre .zshenv ejecutando el comando nano .zshenv en tu terminal.
3. Abre el archivo .zshenv en tu editor de texto favorito.
4. Para añadir la clave de acceso como variable de entorno, añade el siguiente texto en él.

Copy
#certora access key
export CERTORAKEY=<your-certora-access-key>

5. Para guardar los cambios, presiona CTRL + O y luego presiona Enter.
6. Para salir, presiona CTRL + X.
7. Para aplicar la variable de entorno que acabamos de crear, ejecuta el siguiente comando en tu terminal.

Copy
source .zshenv

Ten en cuenta que cada vez que abras una nueva terminal, asegúrate de ejecutar el comando source .zshenv o source .profile para cargar las variables de entorno; de lo contrario, obtendrás el mensaje de error The environment variable CERTORAKEY does not contain a Certora key por parte del Prover.

Añadiendo un Contrato en el Directorio del Proyecto

En el directorio certora-counter, añade una subcarpeta llamada contracts. Una vez hecho esto, crea un archivo llamado Counter.sol en ella, y añade el contrato a continuación.

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

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

El contrato anterior es un contrato inteligente simple que tiene solo una variable de estado pública llamada count, cuyo valor puede ser incrementado por la función externa increment().

Configurando el LSP de Certora Verification Language

Si utilizas el editor VS Code de Microsoft o una bifurcación de este, te recomendamos instalar el Certora Verification Language LSP para mejorar tu experiencia de desarrollo con verificación de sintaxis, resaltado de sintaxis y autocompletado de código siguiendo las instrucciones a continuación:

1. Abre VS Code en tu máquina.
2. Abre el Marketplace de Extensiones haciendo clic en el icono de Extensiones en la barra lateral.
3. Busca “Certora Verification Language LSP” en la barra de búsqueda de Extensiones.
4. Haz clic en “Instalar” en la extensión publicada por Certora.
5. Reinicia VS Code para activar completamente la extensión y aplicar todos los cambios.

Escribiendo Tu Primera Especificación

En el directorio certora-counter, añade una subcarpeta llamada specs. Una vez hecho esto, crea un archivo llamado counter.spec en ella y añade el siguiente código.

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


rule checkCounter() {

    // Pre-Call State
    uint256 precallCount = count();

    // Method Call
    increment();

    // Post-call state
    uint256 postcallCount = count();

    // Assert that the post-call count is exactly one more than the pre-call count
    assert postcallCount == precallCount + 1;

}

Por ahora, no te preocupes por el código. Lo desglosaremos y explicaremos cada parte en detalle en el próximo capítulo.

Añadiendo el Compilador de Solidity

Antes de ejecutar el Prover, necesitamos añadir el compilador de Solidity correcto. Para añadir y usar la versión correcta del compilador de Solidity para nuestro proyecto, ejecuta los dos comandos a continuación en tu terminal.

Copy
solc-select install 0.8.25
solc-select use 0.8.25

Ejecutando la Verificación

Una vez que tenemos un contrato y una especificación, podemos enviarlos al Certora Prover para el proceso de verificación ejecutando el comando certoraRun. Este comando requiere la ruta al contrato de Solidity y el archivo .spec asociado, como se muestra a continuación, para ejecutarse con éxito.

Copy
certoraRun contractFilePath:contractName --verify contractName:specFilePath

Para verificar nuestra especificación, asegúrate de estar en el directorio certora-counter, y luego ejecuta el siguiente comando en tu terminal.

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

Una vez que ejecutes el comando anterior, deberías ver una salida como la siguiente.

Para ver el resultado de la verificación, abre el enlace de verificación impreso en tu terminal. El resultado debería verse similar a la imagen a continuación.

Sin embargo, para un proyecto grande, usar el comando certoraRun con muchos argumentos directamente en la terminal puede volverse engorroso. Por lo tanto, se recomienda usar un archivo de configuración.

Usando un Archivo de Configuración para Simplificar el Comando certoraRun

En Certora, un archivo de configuración es un archivo JSON5 simple escrito con una extensión .conf que requiere al menos dos parámetros clave junto con otras opciones de configuración:

• files: Una ruta a nuestro contrato, junto con el nombre del contrato.
• verify: Una ruta al archivo de especificación.

Para usar el archivo de configuración, crea una subcarpeta llamada confs en el directorio de tu proyecto. Luego, crea un archivo llamado counter.conf dentro de la carpeta confs y añade el siguiente contenido.

Copy
{
    "files": [
        "contracts/Counter.sol:Counter"
    ],
    "verify": "Counter:specs/counter.spec",
}

Una vez que tengamos el archivo de configuración ubicado correctamente, podemos realizar el proceso de verificación simplemente ejecutando el comando certoraRun y referenciando la ruta al archivo de configuración, como se muestra a continuación:

Copy
certoraRun confs/counter.conf

Si el comando se ejecuta con éxito, deberías ver una salida como la siguiente, que contiene un enlace al resultado de la verificación.

Abre el enlace de verificación impreso en tu terminal para ver el resultado de la verificación. El resultado debería verse similar a la imagen a continuación.

Por ahora, solo comprende que la marca de verificación verde (✅) indica que el Prover ha verificado con éxito las condiciones especificadas en el archivo de especificaciones (counter.spec). Esto significa que el contrato se ha comportado como se esperaba basándose en las afirmaciones y la lógica descritas en la especificación.

Conclusión

¡Felicidades! Has configurado con éxito tu entorno de desarrollo y ejecutado tu primera prueba de verificación formal. Sin embargo, hasta ahora, hemos tratado el archivo de especificación (.spec) como una ‘caja negra’. Lo ejecutamos, pero no miramos en su interior. En el próximo capítulo, abriremos esa caja y analizaremos la anatomía de una especificación de Certora. Desglosaremos sus dos componentes esenciales, los Rule Blocks y los Methods Blocks, y aprenderemos a definir las precondiciones, acciones y postcondiciones necesarias para verificar tu primer contrato inteligente.

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