A menudo resulta necesario inspeccionar los cambios en ubicaciones de almacenamiento específicas para demostrar que se cumple una propiedad o invariante, especialmente cuando el almacenamiento no es accesible externamente o cuando los valores de interés no son calculados o expuestos explícitamente por el contrato.

Por ejemplo, supongamos que queremos verificar que, en una implementación ERC-20, el valor de totalSupply siempre es igual a la suma de todos los balances de las cuentas individuales. A primera vista, esto parece sencillo: podríamos hacer assert totalSupply() == sumOfBalances().

Sin embargo, la dificultad radica en que el contrato en realidad nunca mantiene esta suma acumulativa; solo almacena el balance de cada cuenta en un mapping. A diferencia de totalSupply, que se almacena explícitamente y se puede consultar directamente, la “suma de balances” no existe en el estado del contrato. En cambio, esta información se distribuye en múltiples slots de almacenamiento, lo que hace imposible verificar la relación sin observar cómo se accede a esos slots y cómo se actualizan. El desafío se vuelve aún mayor cuando algunas de estas variables son privadas.

Para abordar este desafío, CVL proporciona hooks y variables ghost. Los hooks nos permiten observar eventos de bajo nivel, como lecturas y escrituras en el almacenamiento, mientras que las variables ghost nos permiten capturar, agregar y compartir esas observaciones para que puedan ser referenciadas en otras partes de la especificación. Juntos, cierran la brecha entre el comportamiento interno del contrato y las reglas de verificación de alto nivel, permitiéndonos razonar sobre propiedades que dependen de cambios de estado ocultos o implícitos.

En este capítulo, aprenderá cómo funcionan los hooks, los diferentes tipos disponibles y las limitaciones asociadas a ellos. También le presentaremos las variables ghost, una característica principal de CVL que permite la comunicación entre los hooks y las reglas, permitiéndole verificar propiedades de corrección complejas que de otro modo estarían ocultas en el almacenamiento interno del contrato.

Entendiendo “la Necesidad”

Para comprender mejor los problemas de los que estamos hablando, considere el siguiente contrato inteligente que mantiene una variable privada count y un owner establecido en el momento del despliegue. Tanto increment() como resetCounter() están protegidos por el modificador onlyOwner: increment() incrementa la variable privada count en uno y resetCounter() la restablece a cero, y solo la dirección owner almacenada en el contrato puede llamar a cualquiera de estas funciones.

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


contract Counter {

    // State variables
    address private owner;
    uint256 private count;



    /// @notice Initializes the contract and sets the deployer as the owner
    constructor() {
        owner = msg.sender;
    }


    /// @notice Restricts function calls to the contract owner only
    modifier onlyOwner() {
        require(msg.sender == owner, "Counter: caller is not the owner");
        _;
    }

    // External functions

    /// @notice Increments the counter by 1
    /// @dev Only callable by the owner
    function increment() external onlyOwner {
        count++;
    }

    /// @notice Resets the counter to 0
    /// @dev Only callable by the owner
    function resetCounter() external onlyOwner {
        count = 0;
    }
}

Ahora supongamos que queremos verificar formalmente las siguientes propiedades:

1. El owner nunca debe cambiar una vez que se establece en el constructor.
2. Una llamada a increment() debería aumentar el count exactamente en uno.

A primera vista, ambas propiedades parecen sencillas. Sin embargo, expresarlas en forma de reglas de CVL presenta algunos desafíos. El problema de expresar la primera propiedad como una regla de CVL es que la variable owner está marcada como private y el contrato no proporciona un getter para exponer su valor. Sin poder acceder a él desde una regla, no podemos afirmar que permanezca inalterado una vez establecido en el constructor.

La segunda propiedad introduce un desafío diferente. Aunque podemos llamar a increment() dentro de una regla, la variable count es privada y el contrato no proporciona ningún getter para leer su valor. Esto significa que la regla no puede ver directamente qué le sucede a count cuando se ejecuta la función.

Dado que las reglas solo pueden observar las entradas y salidas de las funciones, no los cambios en el almacenamiento interno, no tienen forma de capturar los valores antiguos y nuevos de count cuando se actualiza. Sin esa visibilidad, el Prover no puede confirmar que cada llamada a increment() realmente aumenta el contador en uno.

En pocas palabras, el problema no es que las propiedades sean difíciles de enunciar, sino que dependen del comportamiento de almacenamiento de bajo nivel y requieren una observación directa de cómo se actualiza el almacenamiento durante la ejecución. Las reglas estándar de CVL se limitan a interactuar con el contrato a través de su interfaz pública, por lo que no pueden capturar estos cambios internos. Para verificar propiedades como la inmutabilidad del owner o los incrementos exactos del contador, necesitamos herramientas que nos permitan echar un vistazo dentro del contrato, monitorear sus operaciones de almacenamiento y llevar esas observaciones a nuestras especificaciones.

Aquí es donde entran en juego los hooks.

¿Qué son los Hooks?

En CVL, los hooks son bloques de código que se ejecutan automáticamente durante el proceso de verificación siempre que un contrato inteligente realiza operaciones de bajo nivel en la EVM, como leer o escribir en el almacenamiento, ejecutar un opcode o modificar datos transitorios.

Un hook se define utilizando la palabra clave hook, y cada hook de CVL especifica lo siguiente:

1. La operación que escucha (por ejemplo, SLOAD, SSTORE o un opcode específico de la EVM).
2. Un bloque de código CVL que se ejecuta cuando se detecta esa operación, proporcionando acceso a los datos relevantes de ese evento.

Tipos de Hooks

CVL proporciona 3 tipos diferentes de hooks, categorizados por el tipo de operación que monitorean. Esos 3 tipos son:

1. Hooks de Almacenamiento
2. Hooks de Opcode
3. Hooks de Almacenamiento Transitorio

Para este capítulo en particular, nos centraremos en los Hooks de Almacenamiento, ya que son los de aplicación más amplia y forman la base para comprender cómo funcionan los hooks en CVL. Los otros tipos de hooks son igualmente útiles en contextos específicos y los cubriremos en capítulos posteriores.

¿Qué son los Hooks de Almacenamiento?

Los hooks de almacenamiento son un tipo específico de hook en CVL que se activan cada vez que se accede a la variable de almacenamiento de un contrato, ya sea para lectura o escritura. En otras palabras, se activan cuando la EVM realiza una operación de lectura (SLOAD) o escritura (SSTORE) en un slot de almacenamiento monitoreado, lo que nos permite:

• Capturar el valor que se está leyendo o escribiendo.
• Imponer condiciones cada vez que se accede a una variable o se modifica.
• Rastrear cómo evoluciona el estado del contrato a lo largo de diferentes ejecuciones.

Existen dos tipos principales de hooks de almacenamiento en CVL:

1. Los Load Hooks
2. Los Store Hooks

1. Los Load Hooks

Un load hook se activa cuando ocurre una operación de lectura (SLOAD) en una variable de almacenamiento monitoreada y le permite capturar el valor que se está leyendo.

Se define utilizando las palabras clave hook Sload, seguidas del tipo y un nombre para una variable de CVL que contendrá el valor cargado y, por último, el nombre de la variable de almacenamiento del contrato que se está monitoreando.

Copy
hook Sload address contractOwner owner { ... }

El hook anterior se ejecutará siempre que el contrato bajo verificación acceda a su variable de almacenamiento owner, de tipo address, para una operación de lectura. Luego, el valor se almacenará en contractOwner, una variable de CVL.

2. Los Store Hooks

Los store hooks se ejecutan antes de que se lleve a cabo cualquier operación de escritura en cualquier variable de almacenamiento específica.

Los store hooks también se definen utilizando la palabra clave hook, seguida de la palabra clave Sstore. Después de eso, especifica el nombre de la variable de almacenamiento del contrato que se está monitoreando, junto con el tipo y el nombre de la variable de CVL que contendrá el valor que está a punto de escribirse en esa ubicación de almacenamiento.

Copy
hook Sstore owner address newOwner{...}

Opcionalmente, el patrón también puede incluir el tipo y el nombre de una variable para almacenar el valor anterior que se está sobrescribiendo.

Copy
hook Sstore owner address newOwner (address oldOwner) {...}

Antes de aplicar hooks para verificar las propiedades del contrato Counter, hay una limitación importante que se debe comprender: las variables declaradas dentro de los hooks son locales al bloque del hook y no son directamente visibles para las reglas.

Entendiendo las Limitaciones de los Hooks

Un hook no solo nos permite monitorear una variable de almacenamiento específica, sino que también proporciona acceso a su valor al almacenarlo en una variable de CVL para su uso. Sin embargo, una limitación es que las variables de CVL definidas dentro de los hooks tienen un alcance local al hook, lo que significa que no se puede acceder a ellas directamente desde las reglas.

Para comprender esta limitación, considere la siguiente especificación que tiene como objetivo demostrar que el owner del contrato Counter nunca cambia después de establecerse por primera vez en el constructor:

Copy
hook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;


}

En la especificación anterior, el hook Sload hace que la variable privada owner sea observable siempre que se lea, almacenando su valor en contractOwner. En la regla, la especificación guarda este valor observado como prevOwner, realiza una llamada simbólica a cualquier función del contrato con entradas arbitrarias y luego observa owner de nuevo como currentOwner. Por último, afirma que prevOwner == currentOwner, lo que significa que en todas las llamadas posibles, el owner debe seguir siendo consistente.

Sin embargo, al ejecutar el Certora Prover, experimentará el siguiente error:

El error anterior simplemente resalta el hecho de que la regla checkOwnerConsistency() no puede acceder ni utilizar contractOwner declarado dentro de nuestro load hook.

Esto podría plantear la pregunta: si los hooks están diseñados para capturar y almacenar datos, ¿por qué no podemos usar esos datos en nuestras reglas directamente?

La respuesta radica en el alcance de las variables definidas dentro de los hooks.

La Limitación de Alcance de los Hooks

Cuando define una variable dentro de un hook, su alcance es local solo a ese hook. Es como definir una variable dentro de una función: se puede usar dentro de ese bloque, pero no es visible fuera de él. Por eso contractOwner es perfectamente válido dentro del hook, pero completamente desconocido para la regla checkOwnerConsistency().

Esto significa que las reglas de CVL y los hooks no comparten variables; operan en alcances separados.

Entonces, ¿cómo podemos usar la información extraída en un hook para escribir reglas útiles?

La respuesta son las variables ghost.

Solucionando la Limitación de Alcance con Ghost

Aunque no podemos acceder directamente a las variables de los hooks dentro de las reglas, podemos definir variables especiales llamadas variables ghost (o simplemente ghosts) para comunicar información entre los hooks y las reglas.

Un ghost se declara utilizando la palabra clave ghost seguida de su tipo y nombre, como se muestra a continuación.

Copy
ghost bool hasVoted;
ghost uint x;
ghost mathint numVoted;
ghost mapping(address => mathint) balances;

Una variable ghost puede ser de cualquier tipo compatible con CVL o un mapping. En el caso de un mapping, sus claves deben ser tipos compatibles con CVL y sus valores pueden ser tipos de CVL u otros mappings.

Verificando la Consistencia del Owner en el Contrato Counter

Para hacer que la regla checkOwnerConsistency() funcione según lo previsto, el valor observado dentro del hook debe estar disponible en el alcance de la regla. Podemos lograr esto almacenando el valor observado en una variable ghost. Los pasos para lograr esto se describen a continuación:

1. Declarar un ghost para almacenar el valor observado de owner: En el nivel superior de nuestra especificación, introduzca una variable ghost llamada ghostOwner. Este ghost servirá como contenedor para el valor del slot owner del contrato siempre que se lea.

Copy

/// Top-level ghost variable to mirror the contract's `owner` slot
ghost address ghostOwner;

hook Sload address contractOwner owner {}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;

}

Al declarar variables ghost, es importante ponerles el prefijo ghost o ghost_ (por ejemplo, ghostOwner, ghost_owner) para distinguirlas claramente de las variables de almacenamiento de Solidity y las variables de CVL locales de los hooks.

En esta etapa, la variable ghost ghostOwner ha sido declarada pero aún no está sincronizada con el almacenamiento del contrato.

2. Sincronizar el ghost dentro del hook: A continuación, modifique el hook Sload de modo que cada vez que el contrato realice una lectura en el slot de almacenamiento owner, el hook capture el valor y lo escriba en el ghost.

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    //assign captured value to ghost
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

     
    address prevOwner = contractOwner;

     //parametric call
     method f;
     calldataarg args;
     f(e,args);

     address currentOwner = contractOwner;

     assert prevOwner == currentOwner;


}

Esto crea un puente desde el almacenamiento privado del contrato hacia el hook, y desde el hook hacia una variable ghost que persiste más allá del alcance local del hook. Cada vez que el contrato lee owner, el ghost ghostOwner se sincroniza con ese valor de almacenamiento.

3. Usar el ghost dentro de la regla: Por último, actualice la regla checkOwnerConsistency() para que, en lugar de usar la variable local del hook contractOwner, haga referencia al ghost ghostOwner.

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

rule checkOwnerConsistency(env e) {

    //Take a snapshot of the ghost before the call
    address prevOwner = ghostOwner;

    //parametric call
    method f;
    calldataarg args;
    f(e,args);
     
    //Take another snapshot after the call
    address currentOwner = ghostOwner;

     
    assert prevOwner == currentOwner;
}

Una vez que haya actualizado su especificación de acuerdo con las instrucciones proporcionadas anteriormente, vuelva a ejecutar el Certora Prover utilizando el comando certoraRun. Esta vez el Prover compilará nuestra regla sin ningún error e imprimirá el resultado de la verificación en su terminal. El resultado será similar a la imagen a continuación:

Después de ver el resultado anterior, es posible que se sorprenda y se pregunte por qué nuestra regla aún falló a pesar de que el contrato Counter nunca actualiza explícitamente a su owner. La razón no radica en el código de Solidity, sino en cómo el Prover interpreta los ghosts y cómo se ejecutan los hooks durante la ejecución de verificación.

Sincronizando los Ghosts con el Almacenamiento

Las variables ghost no están vinculadas automáticamente al almacenamiento del contrato. Al inicio de la ejecución, el Prover les asigna valores con havoc — marcadores de posición arbitrarios que pueden cambiar a través de las trazas a menos que se inicialicen explícitamente. En nuestro caso, el ghost ghostOwner solo se actualiza cuando se lee el slot owner (vía Sload). Si no ocurre ninguna lectura antes de que la regla compare prevOwner y currentOwner, el ghost permanece sin inicializar, manteniendo un valor arbitrario no relacionado con el almacenamiento real.

Esto es lo que sucedió en realidad: el slot de almacenamiento para owner contenía una dirección (p. ej., 0x2712 o 0x2711), pero el ghost ghostOwner contenía un valor completamente diferente (p. ej., 0x401).

Dado que el ghost nunca se alineó con el almacenamiento, nuestra regla terminó comparando dos valores sin sentido, y el Prover, de manera bastante correcta, informó de un fallo.

Podemos ver que el problema principal es que las variables ghost no reflejan automáticamente el almacenamiento del contrato. Para solucionar esto, debemos asegurarnos de que el ghost se actualice explícitamente a través de un hook antes de que se use en una regla. En la práctica, esto significa obligar al contrato a realizar una lectura del slot de almacenamiento relevante para que el hook Sload pueda activarse y sincronizar el ghost con el valor real en el almacenamiento.

Para lograr esto, simplemente hacemos una llamada inicial que haga que el contrato lea el slot owner, lo que a su vez dispara el hook Sload y actualiza nuestro ghost. En nuestro caso, haremos esto llamando a resetCounter(e) al inicio de la regla. Debido a que resetCounter(e) está protegido por el modificador onlyOwner, la EVM debe leer el slot de almacenamiento del owner para verificar la condición del modificador. Esta lectura dispara automáticamente el hook, asegurando que ghostOwner se actualice antes de que lo capturemos en prevOwner.

A continuación se muestra la especificación actualizada mostrando la regla modificada en su totalidad:

Copy
ghost address ghostOwner;

hook Sload address contractOwner owner {
    ghostOwner = contractOwner;
}

// Updated rule: now includes an initial sync call
rule checkOwnerConsistency(env e) {

    // NEW: Force an SLOAD of `owner` so the hook fires and syncs `ghostOwner`
    resetCounter(e);
    
    /// Take the first snapshot after synchronization
    address prevOwner = ghostOwner;
    
    //parametric call
    method f;
    calldataarg args;
    f(e, args);

    // Take another snapshot after the call
    address currentOwner = ghostOwner;

    // The owner must not change across any call
    assert prevOwner == currentOwner;
}

La primera línea dentro de la regla (resetCounter(e);) es la adición clave.

Con el ghost ahora debidamente sincronizado, la comparación entre prevOwner y currentOwner adquiere sentido, permitiendo que el Prover verifique correctamente la consistencia de la variable owner.

Analicemos paso a paso lo que sucedió aquí:

1. Llamada de sincronización inicial (resetCounter(e))
   • La regla comienza llamando a resetCounter(e).
   • Para verificar el modificador onlyOwner, el contrato debe leer el slot owner (SLOAD).
   • Esa lectura dispara el hook Sload, que escribe el valor observado en el ghost ghostOwner.
   • Como resultado, ghostOwner ahora está sincronizado con el valor real de almacenamiento antes de que tomemos cualquier instantánea.
2. Primera instantánea (prevOwner)
   • Justo después de la sincronización, la regla ejecuta address prevOwner = ghostOwner;.
   • Debido al Paso 1, prevOwner es el owner real tal como está almacenado en el contrato.
3. Llamada arbitraria (method f; calldataarg args; f(e, args);)
   • El Prover ahora explora una llamada externa arbitraria con entradas simbólicas.
   • En este contrato, eso significa increment(...) o resetCounter(...) con argumentos arbitrarios.
   • Ambas funciones están protegidas por onlyOwner y no escriben en owner.
   • Durante esta llamada, cualquier lectura adicional de owner (debido a onlyOwner) volverá a disparar el hook Sload, pero solo escribirá el mismo valor en el ghost.
4. Segunda instantánea (currentOwner)
   • Después de que la llamada arbitraria retorna, la regla ejecuta address currentOwner = ghostOwner;.
   • Dado que el contrato nunca muta owner, y el hook solo refleja las lecturas, currentOwner es igual al mismo valor respaldado por el almacenamiento capturado anteriormente.
5. Aserción
   • La regla verifica assert prevOwner == currentOwner;.
   • Dado que el contrato nunca modifica a owner después del despliegue, no hay una ruta de código donde estas dos instantáneas puedan diferir.
   • Por lo tanto, en todas las ejecuciones exploradas, prevOwner y currentOwner siempre permanecen iguales.
   • Como resultado, el Prover no encuentra ningún contraejemplo y reporta la regla como verificada.

Con la propiedad del owner verificada, pasemos ahora a la segunda propiedad que identificamos anteriormente.

Verificando la Llamada a Increment() en el Contrato Counter

La segunda propiedad que queremos probar es que una llamada a increment() debería aumentar el count exactamente en uno. Debido a que count es privado, las reglas por sí solas no pueden observar la escritura de almacenamiento real realizada por count++. Para demostrar esta propiedad, adjuntamos un store hook al slot de count, capturamos los valores antes y después de la escritura, los persistimos en ghosts y, por último, afirmamos la relación aritmética en una regla.

Aquí es cómo se ve la especificación completa:

Copy
methods {
    function increment() external;
}


ghost mathint ghost_prevCount;

ghost mathint ghost_currentCount;

hook Sstore count uint256 postcallValue (uint256 precallValue) {
    ghost_prevCount = precallValue;
    ghost_currentCount = postcallValue;
}

rule checkCounter() {

    env e;

    //call to increment
    increment(e);

    assert ghost_currentCount == ghost_prevCount + 1; 
}

En la especificación anterior, el hook observa las actualizaciones del slot de almacenamiento count cada vez que se llama a la función increment(). El valor antiguo (precallValue) se almacena en una variable ghost (ghost_prevCount), mientras que el nuevo valor (postcallValue) se almacena en otra (ghost_currentCount). Esto le permite a la regla verificar si el contador ha aumentado exactamente en uno, como se espera, después de una llamada a la función increment().

Cuando ejecutamos el Prover en la especificación anterior, veremos que la regla ha sido verificada, como se muestra en la imagen a continuación:

Analicemos paso a paso lo que sucede aquí:

1. Antes de la llamada: La variable privada count del contrato tiene algún valor inicial (digamos X).
2. Durante la llamada a increment():
   • La EVM ejecuta la declaración count++, que se traduce en una lectura seguida de una escritura en el slot de almacenamiento count.
   • Justo antes de que ocurra la escritura, se activa el hook Sstore.
   • El hook captura el valor que estaba a punto de ser sobrescrito (precallValue) y el nuevo valor que se está escribiendo (postcallValue).
   • Estos se almacenan en las variables ghost ghost_prevCount y ghost_currentCount.
3. La comprobación de la regla:
   • Una vez que se completa la llamada a la función, la regla afirma que ghost_currentCount == ghost_prevCount + 1.
   • Dado que ghost_currentCount = X + 1 y ghost_prevCount = X, la aserción es verdadera.

Por lo tanto, obtuvimos un resultado verificado por parte del Prover. En otras palabras, cualquier llamada a increment() aumenta el contador exactamente en uno, y el Prover pudo verificar formalmente esta propiedad sin encontrar ningún contraejemplo.

Las Variables Ghost como Extensión del Almacenamiento

Podemos ver que los hooks se utilizan para observar y recopilar datos al detectar operaciones específicas de lectura o escritura en el almacenamiento del contrato. Sin embargo, dado que las variables declaradas dentro de los hooks son locales al hook, sus valores desaparecen una vez que el hook termina de ejecutarse. Para retener y reutilizar esta información a través de la especificación, CVL introduce las variables ghost: almacenamiento persistente a nivel de especificación que refleja o extiende el estado real del contrato. Debido a esto, las variables ghost pueden ser vistas y tratadas como una extensión del almacenamiento del contrato.

De hecho, el Certora Prover trata las variables ghost de manera muy similar al almacenamiento regular:

• Cualquier actualización de un ghost se revierte automáticamente si la transacción en curso se revierte más tarde, al igual que el almacenamiento.
• Al comienzo de una ejecución de verificación, los ghosts (al igual que otras variables de CVL) representan valores arbitrarios (havoced) a menos que se establezcan explícitamente en la especificación, reflejando la visión simbólica que el Prover tiene del almacenamiento.

Exploraremos estos comportamientos con mayor detalle en un capítulo posterior, donde también aprenderemos a inicializar explícitamente las variables ghost para evitar havocs involuntarios y garantizar resultados de verificación más predecibles.

Conclusión

Los hooks de Certora proporcionan una poderosa observabilidad de las operaciones de almacenamiento y de la EVM. Sin embargo, sus variables están limitadas al alcance local de cada hook. Las variables ghost resuelven este problema al capturar datos de los hooks y hacerlos accesibles para las reglas, lo que permite un razonamiento efectivo y exhaustivo sobre el estado interno de un contrato durante la verificación.

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