En el capítulo anterior, vimos cómo las variables ghost sin restricciones pueden dar lugar a falsos positivos. También aprendimos cómo se puede utilizar una declaración require para restringir eficazmente los valores ghost dentro de las reglas.

Sin embargo, aunque require funciona bien para las reglas, este enfoque no se puede utilizar para la verificación de invariantes. En este capítulo, exploraremos por qué la declaración require es incompatible con los invariantes y presentaremos los axiomas (axioms) como la técnica adecuada para restringir de manera segura los valores de las variables ghost en los invariantes.

Comprendiendo el Problema

Para entender cómo una variable ghost sin restricciones puede afectar la verificación de invariantes, considera el contrato Voting que se muestra a continuación. Este contrato permite a los usuarios votar a favor o en contra de una propuesta utilizando las funciones inFavor() o against().

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

/// @title A simple voting contract
contract Voting {

    // `hasVoted[user]` is true if the user voted.
    mapping(address => bool) public hasVoted;

    // keep the count of votes in favor
    uint256 public votesInFavor;

    // keep the count of votes against
    uint256 public votesAgainst; 


    // @notice Allows a user to vote in favor of the proposal.
    function inFavor() external {
        // Ensure the user has not already voted
        require(!hasVoted[msg.sender], "You have already voted.");
        hasVoted[msg.sender] = true;

        votesInFavor += 1;
    }

    /// @notice Allows a user to vote against the proposal.
    function against() external {
        // Ensure the user has not already voted
        require(!hasVoted[msg.sender], "You have already voted.");
        hasVoted[msg.sender] = true;

        votesAgainst += 1;
  }
}

Este contrato mantiene tres variables de estado públicas:

• hasVoted rastrea si un usuario determinado ya ha votado.
• votesInFavor y votesAgainst llevan la cuenta del número de votos a favor y en contra, respectivamente.

Ahora considera la especificación a continuación, que define un invariante totalVotesSum e introduce una variable ghost totalVotes que rastrea el número total de votos emitidos — un valor que el contrato en sí no registra.

Copy
methods 
{
    function votesInFavor() external returns(uint256) envfree;
    function votesAgainst() external returns(uint256) envfree;
}

ghost mathint totalVotes;


hook Sstore hasVoted[KEY address voter] bool newStatus(bool oldStatus) {
    totalVotes = totalVotes + 1;
}

invariant totalVotesSum()
    totalVotes == votesInFavor() + votesAgainst();

A continuación se detalla la explicación de la especificación anterior:

• El bloque methods declara las dos funciones de vista públicas, votesInFavor() y votesAgainst(), a las que queremos hacer referencia en el invariante. Están marcadas como envfree porque su ejecución no depende de variables de entorno como msg.sender, msg.value, etc.
• La variable ghost totalVotes se define para contar el número de usuarios que han votado. Dado que el contrato no expone este valor directamente, lo simulamos usando un ghost.
• El hook se adjunta a la operación Sstore del mapping hasVoted. Este hook se activa cada vez que se actualiza un valor en el mapping hasVoted, lo que solo ocurre cuando un usuario emite un voto. En el hook, incrementamos totalVotes en 1, contando efectivamente cada nuevo votante independientemente de si votó a favor o en contra.
• El invariante totalVotesSum afirma que el número de votos rastreados por el ghost (totalVotes) siempre debe coincidir con la suma real de votos recuperados del contrato (votesInFavor + votesAgainst).

Una vez que coloques la especificación anterior en el directorio de tu proyecto, ejecuta el proceso de verificación utilizando el comando certoraRun. A continuación, abre el enlace del resultado de verificación que se muestra en tu terminal para ver el resultado, el cual debería verse similar a la imagen de abajo.

Podemos ver que el Prover no ha logrado verificar nuestro invariante. Exploremos por qué ocurrió esto y cómo podemos solucionarlo.

Comprendiendo la Causa de la Violación

Una comprobación de invariante implica dos pasos: el caso base (comprobar el estado inicial después del constructor) y el paso inductivo (comprobar todas las transiciones de estado subsiguientes).

En nuestra situación, el Prover falla en el caso base, lo que significa que no puede confirmar que el invariante sea válido directamente desde el estado inicial del contrato.

Nuestro invariante falla en el caso base porque, al verificar cualquier invariante, el Prover debe comprobar el invariante en el estado inicial del contrato. Sin embargo, dado que nunca especificamos un valor inicial para totalVotes, el Prover eligió uno de forma adversarial por nosotros. En el rastro de la llamada (call trace), podemos ver que eligió -2.

Esto hace que el invariante totalVotes == votesInFavor() + votesAgainst() falle inmediatamente, ya que el Prover comprueba si -2 == 0 + 0, lo cual es falso. Para solucionar esto, necesitamos establecer el valor inicial del ghost en 0. Sin embargo, a diferencia de en las reglas, no podemos usar una declaración require para restringir el valor inicial del ghost. Esto no significa que require no tenga lugar en los invariantes. Puede ser utilizado dentro de un bloque preserved.

Un bloque preserved es una construcción especial en CVL que te permite añadir suposiciones adicionales mientras verificas un invariante. Aprenderemos más sobre los bloques preserved en un capítulo separado.

Antes de explorar cómo restringir variables ghost dentro de invariantes, primero entendamos por qué no se puede usar require en este contexto.

¿Por qué no podemos usar la declaración require?

En CVL, una declaración require se usa dentro de una regla para actuar como una precondición. Le dice al Prover: “Solo comprueba las siguientes aserciones para escenarios donde se cumplan estas condiciones específicas.” Esto ayuda a filtrar las rutas de ejecución o las combinaciones de entrada que el Prover explora al evaluar la regla.

Sin embargo, un invariante es muy diferente. Un invariante debe cumplirse en todo estado posible del contrato, incluido el inicial, sin depender de ninguna precondición. En otras palabras, los invariantes expresan verdades incondicionales sobre el sistema.

Usar una declaración require dentro de un invariante no tiene sentido, porque require solo limita las rutas durante la ejecución de la regla, no define qué es cierto antes de que comience la verificación. Lo que necesitamos en su lugar es una forma de establecer las suposiciones del estado inicial para el Prover.

Para establecer tales verdades iniciales — como configurar el valor de inicio de una variable ghost — necesitamos una construcción diferente: los axiomas.

Introducción a los “Axiomas”

Dado que los invariantes no pueden depender de precondiciones, necesitamos una manera de definir qué debería asumir el Prover sobre el sistema antes de que comience la verificación. Aquí es donde entran los axiomas.

En CVL, un axioma nos permite declarar un hecho o relación que el Prover siempre debe aceptar como verdadero. En lugar de filtrar el espacio de estados como hace require, un axioma da forma al razonamiento del Prover especificando las verdades que se mantienen en su universo lógico.

En términos sencillos:

• Una declaración require limita lo que el Prover comprueba (filtra estados).
• Un axioma define lo que el Prover cree (establece verdades).

Al usar axiomas, podemos controlar con precisión cómo se comportan las variables ghost durante la verificación de invariantes. Por ejemplo, podemos instruir al Prover para que asuma que una variable ghost comienza con cierto valor antes del constructor, o que siempre satisface una condición dada en todos los estados.

Existen dos tipos principales de axiomas utilizados para las variables ghost en CVL:

1. Axiomas de Estado Inicial
2. Axiomas Globales

¿Qué son los “Axiomas de Estado Inicial”?

Un axioma de estado inicial define una propiedad que el prover debe asumir que se cumple en el paso base de la comprobación del invariante o justo antes de que se ejecute el constructor del contrato.

En otras palabras, le dice al Prover: “asume que esta condición es verdadera cuando el contrato se despliega por primera vez.” Esto te permite controlar los valores iniciales de las variables ghost y eliminar los estados de inicio arbitrarios que de otra manera pueden causar fallos en el invariante.

El axioma de estado inicial se declara usando la palabra clave init_state, seguida de la palabra clave axiom, y luego la condición que define el estado inicial de la variable ghost, como se muestra a continuación:

Copy
ghost type_of_ghost name_of_ghost {
    init_state axiom boolean_expression;
}

Por ejemplo, el código a continuación define una variable ghost sum_of_balances de tipo mathint y especifica que su valor debe ser 0 antes de que se ejecute el constructor del contrato.

Copy
ghost mathint sum_of_balances {
    init_state axiom sum_of_balances == 0;
}

Esto asegurará que el Prover comience la verificación con la suposición de que sum_of_balances inicia en cero, evitando que sea tratado como un valor arbitrario en el estado inicial.

¿Qué son los “Axiomas Globales”?

Mientras que los axiomas de estado inicial se aplican solo al primer estado del contrato, los axiomas globales definen propiedades que deben cumplirse en todos los estados a lo largo de la verificación.

Un axioma global te permite expresar verdades universales sobre las variables ghost — condiciones que se mantienen consistentes a través de todas las posibles ejecuciones del contrato. Una vez definidos, el Prover acepta estas declaraciones como hechos que siempre son válidos y nunca necesitan ser probados nuevamente.

Un axioma ghost global se define incluyendo la palabra clave axiom dentro del bloque de declaración de la variable ghost, seguido de una condición que debe cumplirse en todos los estados del programa, como se muestra a continuación:

Copy
ghost type_of_ghost name_of_ghost {    
  axiom boolean_expression;
}

Por ejemplo, el código a continuación define una variable ghost x de tipo mathint y afirma que su valor siempre es mayor que cero en cada estado durante el proceso de verificación:

Copy
ghost mathint x {    
  axiom x > 0;
}

Esto significa que, durante la verificación, el Prover asumirá que la condición $x > 0$ se cumple en todos los estados, restringiendo efectivamente a la variable ghost para que nunca tome valores cero o negativos.

Usando el Axioma init_state en nuestra Especificación

Ahora que entendemos el propósito de un axioma init_state, apliquémoslo al ejemplo que exploramos anteriormente, donde nuestro invariante falló porque la variable ghost totalVotes comenzó con un valor arbitrario.

Para solucionar esto, necesitamos decirle al Prover que totalVotes debería comenzar en 0 inmediatamente antes de que se ejecute el constructor. Hacemos esto actualizando la declaración del ghost para incluir un axioma init_state, como se muestra a continuación:

Copy
ghost mathint totalVotes {    
  init_state axiom totalVotes == 0;
}

Una vez que hayas actualizado la especificación para incluir el axioma init_state como se muestra arriba, vuelve a ejecutar el Prover y abre el resultado de la verificación. Nuestro nuevo resultado de verificación debería verse similar al resultado a continuación.

Esta vez, podemos observar que el Prover ha verificado con éxito nuestro invariante al pasar tanto el caso base como el paso inductivo, confirmando que el número total de votos siempre es igual a la suma de los votos emitidos a favor y los votos emitidos en contra.

Usando un Axioma Global en la Práctica

Para entender cómo funcionan los axiomas globales en la práctica, considera la especificación a continuación:

Copy
methods {
    function votesInFavor() external returns(uint256) envfree;
    function votesAgainst() external returns(uint256) envfree;
}

ghost mathint totalVotes {
    axiom totalVotes >= 0;
}

hook Sstore hasVoted[KEY address voter] bool newStatus(bool oldStatus) {
    totalVotes = totalVotes + 1;
}

invariant totalVotesShouldAlwaysGtInFavorVotes()
    totalVotes >= votesInFavor();

La especificación anterior afirma que el número total de votos (totalVotes) debe ser siempre mayor o igual que el número de votos a favor (votesInFavor). En la especificación anterior, la parte clave es la línea axiom totalVotes >= 0, la cual introduce un axioma global que instruye al Prover a asumir siempre que totalVotes es no negativo en cada estado del programa. Esto significa que el Prover nunca explorará ninguna ruta de ejecución en la que totalVotes se vuelva negativo.

Cuando envías esta especificación al Prover, verifica con éxito el invariante, como se muestra en el resultado a continuación:

Como sabemos, cuando se envía un invariante para su verificación, el Prover realiza dos comprobaciones esenciales para asegurar su correctitud:

1. Caso Base: En este paso, el Prover comprueba primero si el invariante se cumple inmediatamente después de que se ejecute el constructor del contrato. En nuestro ejemplo, esto significa verificar que totalVotes >= votesInFavor() sea verdadero en el estado inicial del contrato. Inmediatamente después del despliegue, votesInFavor() es 0, mientras que el Prover asume que totalVotes puede ser cualquier valor no negativo. Dado que cualquier número no negativo satisface la condición totalVotes >= votesInFavor(), el caso base se cumple.
2. Paso Inductivo: A continuación, el Prover asegura que si el invariante se cumple antes de la ejecución de cualquier función, seguirá cumpliéndose después de todas las posibles transiciones. Aquí, cada vez que un usuario emite un voto, el mapping hasVoted se actualiza y el hook incrementa totalVotes.
   • Cuando un usuario vota a favor, tanto votesInFavor como totalVotes aumentan en uno, preservando la desigualdad.
   • Cuando un usuario vota en contra, solo aumenta totalVotes, lo cual sigue manteniendo el invariante.

Dado que ambas condiciones se cumplen, el Prover verifica con éxito el invariante. Esto confirma que, bajo la suposición global totalVotes >= 0, la relación entre totalVotes y votesInFavor sigue siendo válida a través de todos los posibles estados del contrato.

Así es como un axioma global ayuda al Prover a razonar sobre propiedades que son universalmente verdaderas en cada estado del programa. Al definir axiom totalVotes >= 0, establecemos un hecho lógico que se mantiene a lo largo de toda la verificación, sin necesidad de probarlo nuevamente después de cada transición de estado. En este caso, el axioma captura una verdad intuitiva de que el número total de votos nunca puede ser negativo, y permite al Prover verificar el invariante de manera eficiente y sólida.

Conclusión

En este capítulo, demostramos cómo las variables ghost sin restricciones pueden causar que las pruebas de invariantes fallen en el caso base. Dado que usar require para la inicialización no es válido dentro de los invariantes, presentamos los axiomas como la alternativa correcta. Específicamente, el axioma init_state resuelve el problema de inicialización al definir valores de inicio válidos para los ghosts, mientras que los axiomas globales expresan propiedades que permanecen como verdaderas a lo largo de todos los estados del contrato.

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