Introducción

En capítulos anteriores, utilizamos variables fantasma (a través de los hooks de Sstore) para registrar valores de almacenamiento y cantidades que no se rastreaban explícitamente en los contratos inteligentes — por ejemplo, la suma de todos los balances. Permiten observar y razonar sobre los cambios en el estado o las relaciones entre las variables de estado a lo largo del tiempo durante la verificación.

Sin embargo, durante la ejecución de las reglas después de invocar un método del contrato, las variables fantasma pueden:

• sufrir havoc cuando el Prover encuentra una llamada externa no resuelta, o
• revertirse a su estado anterior (restablecerse) cuando la llamada se revierte (revert).

Los fantasmas sufren havoc durante una llamada externa no resuelta porque el Prover no puede ver la implementación del contrato llamado. Dado que el contrato externo podría potencialmente volver a llamar al llamador (call back) y modificar el almacenamiento, el Prover no puede descartar que las variables fantasma puedan ser actualizadas a través de sus hooks. Para manejar esta incertidumbre, el Prover asigna valores no deterministas a las variables fantasma.

Cuando una llamada se revierte, los fantasmas no se vuelven no deterministas. En su lugar, se revierten (restablecen) al valor que tenían antes de que comenzara la llamada. Según la documentación de Certora, “Los fantasmas pueden verse como una extensión del estado de los contratos bajo verificación. Esto significa que en caso de que una llamada se revierta, los valores del fantasma se revertirán a su estado previo”.

Estos son los comportamientos predeterminados de los fantasmas: sufren havoc en llamadas no resueltas y se restablecen cuando la llamada a un método se revierte. Sin embargo, existe un tipo de fantasma de propósito especial llamado persistent ghost (fantasma persistente), que mantiene su valor (no sufre havoc) tanto en llamadas externas no resueltas como en reversiones.

En este capítulo, demostraremos cómo funcionan los persistent ghosts, cómo se diferencian de los fantasmas regulares, cuándo usarlos y cuándo no.

Declarando un persistent ghost

Un persistent ghost se declara con la palabra clave persistent, como se muestra a continuación:

Copy
persistent ghost bool g_flag;
persistent ghost uint256 g_count;

Por legibilidad, utilizamos el prefijo g_ para todas las variables fantasma en este artículo, aunque pueden nombrarse libremente.

Para inicializar los persistent ghosts con valores específicos, agregue init_state axiom dentro de la declaración del fantasma:

Copy
persistent ghost bool g_flag {
    init_state axiom g_flag == false;
}

persistent ghost uint256 g_count {
    init_state axiom g_count == 0;
}

Nota: Aunque los persistent ghosts no sufren havoc durante las llamadas a métodos no resueltos, sí sufren havoc en el estado previo a la llamada para las reglas y en el caso base para los invariantes; lo mismo ocurre con los fantasmas regulares. Por lo tanto, aún deben restringirse adecuadamente como una precondición (a través de sentencias require) en las reglas e inicializarse utilizando init_state axiom para los casos base de los invariantes.

El comportamiento de los persistent ghosts vs. los fantasmas regulares

El siguiente diagrama muestra cómo un persistent ghost conserva su valor a través de llamadas revertidas y llamadas externas no resueltas. Durante la ejecución de la regla, cuando un hook asigna un valor a ghostVar, ese valor nunca se revierte (restablece) ni sufre havoc, por lo que su estado final siempre refleja el último valor asignado por el hook:

En contraste con los persistent ghosts, los fantasmas regulares sufren havoc en llamadas externas no resueltas y se restablecen en reversiones:

Nota: Tanto los persistent ghosts como los fantasmas regulares mantienen sus valores solo dentro de la ejecución de una única regla y no se transfieren entre reglas. La diferencia es que los persistent ghosts sobreviven a llamadas no resueltas o revertidas dentro de esa ejecución, mientras que los fantasmas regulares no lo hacen.

Rastreando reverts con persistent ghosts

Esta sección demuestra cómo los persistent ghosts permiten rastrear reversiones de una manera que los fantasmas regulares no pueden. Explica por qué los fantasmas regulares fallan en este caso de uso y muestra cómo los persistent ghosts resuelven el problema.

El fantasma regular se restablece cuando una llamada a un método se revierte

Cuando un método se revierte, el estado de los fantasmas regulares también se revierte. Este comportamiento se alinea con la forma en que las variables de almacenamiento se revierten a sus valores anteriores durante una llamada fallida.

Para ilustrar este comportamiento, consideremos este contrato, SimpleVault, donde los usuarios pueden depositar y retirar ETH:

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

contract SimpleVault {
    mapping(address => uint256) public balanceOf;

    /// deposit ETH into the vault
    function deposit() external payable {
        balanceOf[msg.sender] += msg.value;
    }

    /// withdraw ETH from the vault
    function withdraw(uint256 amount) external {
        require(balanceOf[msg.sender] >= amount, "Insufficient balance");
        balanceOf[msg.sender] -= amount;

        (bool success, ) = msg.sender.call{value: amount}("");
        require(success, "ETH transfer failed");
    }
}

El objetivo es verificar que withdraw() se revierte en exactamente estos casos:

• la cantidad de retiro excede el balance depositado (amount > balanceBefore)
• se envía un msg.value distinto de cero a esta función no pagadera (e.msg.value != 0)
• la transferencia de ETH falla, o la llamada de bajo nivel devolvió false

Esta sección se enfoca específicamente en el tercer caso: rastrear las fallas de transferencia de ETH.

La siguiente regla implementa un patrón de aserción del capítulo sobre “Account Balances”. Utiliza el operador bicondicional (<=>) y enumera todas las condiciones de reversión esperadas de forma disyuntiva (||). Esto toma en cuenta todos los posibles reverts del método si y solo si ocurre una de estas condiciones:

Copy
ghost bool g_lowLevelCallSuccess; // regular ghost

rule withdraw_revert(env e) {
    uint256 amount;
   
 	require g_lowLevelCallSuccess; // by requiring it to be true initially, you can detect when it becomes false during execution

    mathint balanceBefore = balanceOf(e.msg.sender);

    withdraw@withrevert(e, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

Para rastrear el resultado de la transferencia de ETH, usamos un hook CALL; una característica de CVL que monitorea la instrucción EVM CALL de bajo nivel y captura su código de retorno. Asignamos este código de retorno a g_lowLevelCallSuccess (0 para fallo, 1 para éxito):

Copy
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

Aquí está la especificación completa:

Copy
methods {
    function balanceOf(address) external returns uint256 envfree;
}

ghost bool g_lowLevelCallSuccess;

hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

rule withdraw_revert(env e) {
    uint256 amount;
    require g_lowLevelCallSuccess;

    mathint balanceBefore = balanceOf(e.msg.sender);

    withdraw@withrevert(e, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

Usando fantasmas regulares, la verificación falla:

Ver la ejecución fallida del Prover: link

Examinemos por qué ocurrió el fallo.

Restablecimiento del valor del fantasma regular — traza de la llamada

La verificación falla porque g_lowLevelCallSuccess es un fantasma regular que se restablece en un revert. El hook CALL captura el fallo (returnCode == 0), pero cuando withdraw se revierte, el fantasma se restablece y pierde este valor.

Como se muestra en la imagen a continuación, g_lowLevelCallSuccess es true antes de que se invoque el método withdraw() (estado previo a la llamada):

Cuando la llamada de transferencia de ETH de bajo nivel falla, el hook CALL captura la llamada fallida (valor de retorno de 0), lo que establece g_lowLevelCallSuccess en false:

Cuando el opcode CALL (capturado por el hook CALL de CVL) devuelve cero, significa que la transferencia de ETH falla. Dentro de la regla, el fantasma se restablece a su estado previo a la llamada cuando la invocación withdraw@withrevert(e, amount) se revierte. La imagen a continuación muestra el fantasma volviendo a true a pesar de la transferencia fallida:

Arreglando la especificación con un persistent ghost

Para recapitular lo que observamos en la traza de la llamada con un fantasma regular, la ejecución se desarrolla de la siguiente manera:

1. El fantasma g_lowLevelCallSuccess se inicializa en true (a través de la sentencia require).
2. La función withdraw se ejecuta y desencadena un CALL de bajo nivel que falla.
3. El hook CALL detecta el fallo (returnCode == 0) y establece g_lowLevelCallSuccess en false.
4. La función withdraw se revierte porque require(success) falla cuando success es false.
5. El revert causa que el fantasma se restablezca a su estado previo a la llamada de true.

El problema raíz es claro: el revert en el paso 5 restablece el fantasma de nuevo a true, borrando el valor false que registraba el fallo de la transferencia en el paso 3.

Para arreglar esto, declare el fantasma como persistent para que el valor booleano asignado por el hook CALL sobreviva al revert y permanezca accesible en la regla:

Copy
methods {
    function balanceOf(address) external returns uint256 envfree;
}

persistent ghost bool g_lowLevelCallSuccess;

hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint returnCode {
    if (returnCode == 0) {
        g_lowLevelCallSuccess = false;
    } else {
        g_lowLevelCallSuccess = true;
    }
}

rule withdraw_revert(env e) {
    uint256 amount;
    require g_lowLevelCallSuccess;

    mathint balanceBefore = balanceOf(e.msg.sender);

    withdraw@withrevert(e, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        amount > balanceBefore ||   // insufficient balance: withdrawal amount exceeds user balance
        e.msg.value != 0 ||         // non-payable: ETH was sent to this non-payable function
        !g_lowLevelCallSuccess      // transfer failure: low-level call ETH transfer failed
    );
}

Como era de esperar, la regla se verifica:

Ejecución del Prover: link

Con el persistent ghost, rastreamos con éxito el fallo de la transferencia de ETH en la llamada de bajo nivel a través del revert, algo imposible con un fantasma regular. Este ejemplo muestra un caso de uso adecuado para los persistent ghosts: capturar información de estado que de otro modo se perdería durante las reversiones.

Cuándo NO usar persistent ghosts

Habiendo visto un caso de uso adecuado para los persistent ghosts, es igualmente importante entender cuándo no deben usarse.

La facilidad de agregar la palabra clave persistent a un fantasma regular lo hace propenso a un mal uso. Use persistent ghosts intencionalmente cuando necesite observar lo que sucede en ejecuciones revertidas o no resueltas — no como una solución temporal (workaround) cuando las reglas o invariantes no se verifican.

Para demostrar el problema de su mal uso, consideremos una bóveda (vault) similar que acepta tokens ERC-20 en lugar de ETH. Su mapping de balances es privado, por lo que se necesita una variable fantasma para reflejar los balances internos ya que no hay una función getter desde la cual leer:

Copy
/// minimal ERC20 interface
interface IERC20 {
    function transfer(address to, uint256 amount) external returns (bool);
	...
}

contract SimpleVault20 {
    IERC20 public immutable token;
    mapping(address => uint256) private balanceOf;
    
    constructor(address _token) {
        token = IERC20(_token);
    }
    
    function deposit(uint256 amount) external {
        require(amount > 0, "Zero deposit");
        
        balanceOf[msg.sender] += amount;
        require(token.transferFrom(msg.sender, address(this), amount), "transferFrom failed");
    }
    
    ...
}

Escribamos las especificaciones para la función deposit(). Para el fantasma y los hooks:

• declarar el fantasma como un fantasma regular
• implementar el hook Sstore para rastrear los cambios en los balances por cuenta de depositante
• implementar el hook Sload para sincronizar las lecturas del almacenamiento y del fantasma

Copy
ghost mapping(address => mathint) g_balanceOf;

hook Sstore balanceOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_balanceOf[account] = g_balanceOf[account] + newVal - oldVal;
}

hook Sload uint256 balance balanceOf[KEY address account] {
    require g_balanceOf[account] == balance;
}

En cuanto a la regla, verificamos que depositar una cantidad (depositAmount) la acredite correctamente al balance del remitente en la bóveda:

Copy
rule deposit(env e) {
    uint256 depositAmount;

    require currentContract != e.msg.sender;
    require g_balanceOf[e.msg.sender] == 0;
    
    deposit(e, depositAmount);
    assert g_balanceOf[e.msg.sender] == depositAmount;
}

Ejecutemos la verificación. Dado que la función de depósito llama a una implementación desconocida de ERC-20 (lo que causará havoc), esperamos que falle:

Ejecución del Prover: link

Por qué falló la verificación

La causa raíz se encuentra en la siguiente línea del contrato SimpleVault20, donde llama a una implementación desconocida de ERC-20:

Copy
contract SimpleVault20 {
    ...
    function deposit(uint256 amount) external {
        require(amount > 0, "Zero deposit");
        
        balanceOf[msg.sender] += amount;
        
        // `token` is an unknown ERC-20 implementation
        require(token.transferFrom(msg.sender, address(this), amount), "transferFrom failed");
    }
    ...
}

En la imagen a continuación, vemos que el Prover asignó el valor 0xa (o 10) a depositAmount, que luego se pasó a través del hook Sstore a la variable de mapping del fantasma g_balanceOf[address]:*

Luego, el fantasma sufrió havoc durante la llamada a un contrato externo porque su implementación era desconocida:

Al ver el error de havoc, uno podría verse tentado a agregar la palabra clave persistent para suprimirlo. Aunque esto hace que la verificación pase, oculta el verdadero problema: no sabemos cómo está implementado el contrato externo ERC-20:

Ejecución del Prover: link

El Prover verifica con una suposición incorrecta

El Prover muestra la regla como verificada, pero esto se basa en una suposición incorrecta. Al usar un fantasma persistent, la especificación asume que la implementación ERC-20 nunca se revierte ni modifica el almacenamiento del contrato que la llama. Por lo tanto, acredita la cantidad 0xa (o 10) a msg.sender a pesar de que la transferencia podría fallar en realidad:

Esto demuestra por qué el uso de un fantasma persistent en este caso es engañoso: elude la incertidumbre del comportamiento del contrato externo, ocultando errores potenciales en lugar de revelarlos.

La implementación real del token debe estar vinculada a la bóveda

La solución adecuada NO es usar un persistent ghost. En cambio, debemos “vincular” (link) una implementación de ERC-20 conocida a la escena — ya sea el propio ERC20 del protocolo, WETH, DAI, o cualquier token ERC-20 cuyo código esté disponible.

La vinculación (linking) indica al Prover que use la implementación real del contrato incluida en la escena de verificación para las llamadas externas, en lugar de tratar esas llamadas como un comportamiento de havoc.

Para SimpleVault20, la dirección del token es inmutable, lo que significa que el ERC-20 a utilizar se conoce en el momento de la implementación y no cambiará a lo largo de la vida del contrato. Por lo tanto, podemos usar link para “enlazarlo” a una implementación de ERC-20 agregando el contrato ERC-20 a la escena y configurándolo en la especificación. Esto permite al Prover verificar el contrato SimpleVault20 frente a la implementación real del token. De lo contrario, sin la vinculación, el Prover no puede verificar con precisión la interacción de la bóveda con el token, lo que lleva a falsos positivos como se demostró anteriormente.

Para más detalles sobre link, consulte la documentación de Certora: [1, 2]

Resumen

• Los persistent ghosts sobreviven al havoc y a las reversiones (reverts), mientras que los fantasmas regulares sufren havoc durante las llamadas externas a contratos desconocidos y se restablecen durante las reversiones.
• Las llamadas externas a contratos desconocidos causan havoc porque el Prover no puede ver la implementación del receptor de la llamada (callee), por lo que modela todos los posibles valores de retorno y efectos de almacenamiento.
• Un uso adecuado de los persistent ghosts es capturar información de los hooks de CVL — como los códigos de retorno de CALL — que deben sobrevivir a través de rutas de ejecución fallidas, como rastrear transferencias de ETH de bajo nivel que han fallado.
• Agregar la palabra clave persistent como una solución rápida para pasar reglas fallidas crea una falsa sensación de éxito en la verificación al ignorar los efectos de las implementaciones de contratos desconocidos o llamadas no resueltas.

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