Introducción

En el capítulo anterior, aprendimos sobre las reglas paramétricas, las cuales nos permiten verificar formalmente propiedades que se espera que se mantengan independientemente de la función que se llame. Esto es particularmente útil para verificar invariantes universales. Pero, ¿qué sucede si el comportamiento deseado no es universal y, en cambio, depende de la función específica que se esté llamando? Por ejemplo, considere los siguientes escenarios:

• El owner de cualquier contrato debería permanecer igual, excepto cuando el propietario llama a changeOwner o renounceOwnership.
• El suministro total de un token ERC-20 debe permanecer igual, excepto cuando los tokens son acuñados o quemados.

¿Cómo manejamos estos casos en los que una propiedad generalmente se mantiene pero tiene excepciones conocidas basadas en la función? ¿O qué sucede si simplemente desea excluir por completo ciertos métodos administrativos de las comprobaciones generales de invariantes?

En este capítulo, aprenderemos cómo utilizar las propiedades de métodos para aplicar aserciones específicas de funciones en reglas paramétricas. También veremos cómo excluir ciertas funciones de la verificación cuando esas reglas no sean aplicables.

¿Qué son las propiedades de métodos?

El siguiente código muestra una regla paramétrica: una que se aplica a todas las funciones.

Copy
rule someParametricRule() {  
    env e;
      
    method f;  
    calldataarg args;  
    f(e, args);  

    assert property_1;  
}

Ya sea que necesite aplicar aserciones específicas de una función o excluir ciertas funciones de la regla, necesita una forma de distinguir una función de otra. Aquí es donde entran en juego las propiedades de métodos.

En CVL, las propiedades de métodos son atributos accesibles en la variable method (como f) utilizando una sintaxis similar a la de los campos (por ejemplo, f.propertyName). Estas propiedades proporcionan información sobre la función a la que f hace referencia en tiempo de ejecución, permitiendo que la lógica de su regla se adapte en función del método específico que se esté invocando.

Las propiedades de métodos disponibles incluyen:

• f.selector : Devuelve el selector de función de 4 bytes (un hash de la firma de la función, por ejemplo, 0xa9059cbb) que puede usarse para identificar funciones específicas por su nombre (por ejemplo, f.selector == sig:transfer(address,uint256).selector) para aplicar aserciones específicas de la función en una regla paramétrica.
• f.isPure : Devuelve true si la función f está declarada con la palabra clave pure en Solidity. Esto puede ser útil para excluir funciones puramente computacionales de reglas que solo tienen sentido para la lógica que modifica el estado.
• f.isView : Devuelve true si la función f está declarada con la palabra clave view. Esto se puede utilizar para omitir funciones de solo lectura al escribir reglas relacionadas con cambios de estado. Exploraremos los beneficios de esto en una sección posterior.
• f.isFallback : Devuelve true si f representa una función fallback() o receive(). Esto es útil cuando necesita escribir reglas que rijan el comportamiento de respaldo (fallback), como requisitos payable o el manejo especial para llamadas de bajo nivel.
• f.numberOfArguments : Devuelve el número de argumentos que espera la función f.
• f.contract : Devuelve el contrato en el que está definida la función. Esto es útil cuando se están verificando múltiples contratos a la vez o cuando se trata con herencia, como cuando dos contratos tienen funciones con el mismo nombre y argumentos. Esto es algo que exploraremos en capítulos posteriores, ya que nuestros ejemplos actuales involucran solo un único contrato.

De todas estas, las propiedades de métodos más utilizadas son f.selector, f.isView y f.isPure. Estas cubren los casos de uso más típicos, como identificar una función específica (usando el selector) u omitir funciones de solo lectura y computacionales (isView e isPure) al escribir reglas enfocadas en cambios de estado. Para mantener un enfoque práctico, nos centraremos en estas propiedades en los próximos ejemplos y mostraremos cómo ayudan a escribir reglas paramétricas más precisas y eficientes.

Aplicación de aserciones dependientes de funciones en una regla paramétrica

Para entender cómo se pueden usar las propiedades de métodos para aplicar aserciones dependientes de funciones dentro de una regla paramétrica, considere la implementación ERC-20 RareToken que se muestra a continuación, la cual incluye las funcionalidades mint y burn:

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

contract RareToken {
    uint256 public totalSupply;
    address public owner;
    
    mapping(address => uint256) public balanceOf;
    mapping(address => mapping(address => uint256)) public allowance;

    event Transfer(address indexed from, address indexed to, uint256 value);
    event Approval(address indexed owner, address indexed spender, uint256 value);

    modifier onlyOwner() {
        require(msg.sender == owner, "Unauthorized");
        _;
    }

    constructor(uint256 _initialSupply) {
        owner = msg.sender;
        if (_initialSupply > 0) {
            _mint(msg.sender, _initialSupply);
        }
    }

    function transfer(address to, uint256 amount) public virtual returns (bool) {
        _transfer(msg.sender, to, amount);
        return true;
    }

    function approve(address spender, uint256 amount) public virtual returns (bool) {
        _approve(msg.sender, spender, amount);
        return true;
    }

    function transferFrom(address from, address to, uint256 amount) public virtual returns (bool) {
        address spender = msg.sender;
        uint256 currentAllowance = allowance[from][spender];
        require(currentAllowance >= amount, "Allowance exceeded");
        
        if (currentAllowance != type(uint256).max) {
            _approve(from, spender, currentAllowance - amount);
        }
        
        _transfer(from, to, amount);
        return true;
    }

    function mint(address account, uint256 amount) public onlyOwner {
        _mint(account, amount);
    }

    function burn(uint256 amount) public virtual {
        _burn(msg.sender, amount);
    }

    function _transfer(address from, address to, uint256 amount) internal virtual {
        require(from != address(0), "Invalid sender");
        require(to != address(0), "Invalid recipient");
        
        uint256 fromBalance = balanceOf[from];
        require(fromBalance >= amount, "Insufficient balance");
        
        balanceOf[from] = fromBalance - amount;
        balanceOf[to] += amount;
        emit Transfer(from, to, amount);
    }

    function _mint(address account, uint256 amount) internal virtual {
        require(account != address(0), "Invalid recipient");
        
        totalSupply += amount;
        balanceOf[account] += amount;
        emit Transfer(address(0), account, amount);
    }

    function _burn(address account, uint256 amount) internal virtual {
        require(account != address(0), "Invalid burner");
        
        uint256 accountBalance = balanceOf[account];
        require(accountBalance >= amount, "Burn exceeds balance");
        
        balanceOf[account] = accountBalance - amount;
        totalSupply -= amount;
        emit Transfer(account, address(0), amount);
    }

    function _approve(address ownerAccount, address spender, uint256 amount) internal virtual {
        require(ownerAccount != address(0), "Invalid owner");
        require(spender != address(0), "Invalid spender");
        
        allowance[ownerAccount][spender] = amount;
        emit Approval(ownerAccount, spender, amount);
    }
}

Dado que la implementación ERC-20 anterior incluye mint() y burn(), se espera que el valor de totalSupply cambie durante las llamadas a esas funciones, a diferencia de la implementación ERC-20 que utilizamos en el último capítulo, donde a ninguna función se le permitía alterar el suministro.

Ahora, supongamos que queremos escribir una regla paramétrica para el contrato RareToken que exija el siguiente comportamiento:

• Cuando se llama a la función mint(), el totalSupply no debe disminuir (puede aumentar o permanecer igual si la cantidad es cero).
• Cuando se llama a la función burn(), el totalSupply no debe aumentar (puede disminuir o permanecer igual si la cantidad es cero).
• Para cualquier otra función (como transfer, approve, transferFrom), el totalSupply debe permanecer inalterado.

Para definir una regla paramétrica que aplique el comportamiento anterior, la regla debe asegurar lo siguiente:

1. La regla primero debe registrar el valor inicial de la variable totalSupply antes de la ejecución de cualquier función para establecer un punto de referencia para la comparación de estado.
2. Para evaluar el impacto de múltiples funciones sobre el estado de totalSupply, la regla debe emplear un marco paramétrico que ejecute cada función objetivo una por una.
3. Después de que cada función complete su ejecución, la regla debe registrar el valor actualizado de totalSupply para rastrear las modificaciones de estado.
4. Finalmente, la regla debe aplicar tres aserciones críticas basadas en la función ejecutada.

La siguiente regla, totalSupplyIntegrityCheck, implementa todos estos pasos. Captura el totalSupply antes y después de la ejecución de cada función, invoca cualquier método utilizando una configuración paramétrica y luego aplica el comportamiento esperado dependiendo de qué función haya sido llamada:

Copy
rule totalSupplyIntegrityCheck() {

    env e;

    // Step 1: Record initial state
    mathint supplyBefore = totalSupply(e);

    // Step 2: Execute an arbitrary function
    method f;
    calldataarg args;
    f(e, args);

    // Step 3: Record updated state
    mathint supplyAfter = totalSupply(e);

    // Step 4: Function-specific assertions
    if (f.selector == sig:mint(address,uint256).selector) {
        assert supplyAfter >= supplyBefore, "Total supply should not decrease after mint()";
    } 
    else if (f.selector == sig:burn(uint256).selector) {
        assert supplyAfter <= supplyBefore, "Total supply should not increase after burn()";
    } 
    else {
        assert supplyAfter == supplyBefore, "Total supply must remain unchanged for other function calls";
    }
}

En la regla anterior, accedimos al selector de función de una función arbitraria (f) utilizando f.selector, y derivamos el selector de función de una función conocida utilizando la notación sig:functionName(...).selector. Luego lo usamos para comparar si la función ejecutada f corresponde a una función nombrada específica como mint() o burn() para aplicar aserciones específicas de funciones dentro de nuestra regla paramétrica.

La regla anterior simplemente aplica el siguiente comportamiento:

1. Si se ejecuta la función mint() (identificada por f.selector == sig:mint(address,uint256).selector), el valor de totalSupply no debe disminuir en comparación con su valor inicial.
2. Si se ejecuta la función burn() (identificada por f.selector == sig:burn(uint256).selector), el valor de totalSupply no debe aumentar en comparación con su valor inicial.
3. Para todas las demás llamadas de función, la regla exige que el valor de totalSupply deba permanecer inalterado, garantizando que ninguna función no deseada modifique la variable totalSupply.

Para ver los resultados de nuestra regla paramétrica, configure el entorno de Certora Prover colocando el contrato RareToken y su especificación en el directorio apropiado. Luego, ejecute el proceso de verificación. Si el contrato cumple con las condiciones de la regla, el probador (prover) confirmará una verificación exitosa sin violaciones detectadas, como se muestra en los resultados a continuación.

Los resultados de la verificación confirman que la regla totalSupplyIntegrityCheck se ejecutó correctamente y que las nueve comprobaciones pasaron sin ninguna violación detectada. Esto valida que el comportamiento de mint(), burn() y otras funciones en el contrato RareToken es consistente con las expectativas de la regla: totalSupply aumenta después de mint(), disminuye después de burn() y permanece inalterado para todas las demás funciones.

La regla anterior utiliza exitosamente lógica condicional basada en f.selector para aplicar las aserciones correctas después de ejecutar cada función f. Esto asegura que cada función compatible con los parámetros de la regla sea comprobada frente a la expectativa adecuada basada en su identidad.

Optimización de reglas paramétricas con bloques filtered

Cuando revisamos el informe de verificación, notamos que Certora Prover ha aplicado nuestras comprobaciones de aserción a todas las funciones en el contrato, incluidas las de solo lectura como totalSupply(), balanceOf() y owner(). Estas funciones están marcadas como view en Solidity, lo que significa que solo leen del estado de la cadena de bloques y no modifican nada. Por esta razón, ejecutar reglas de cambio de estado en estas funciones no tiene mucho sentido y no nos ayuda a detectar errores significativos.

Aunque verificarlas no es técnicamente incorrecto, causa un trabajo computacional adicional y ralentiza el proceso. Es por eso que es importante excluir funciones que no impactan el estado del contrato cuando no son relevantes para la regla que se está probando. Aquí es donde el bloque filtered resulta útil.

El bloque de filtro nos permite incluir o excluir selectivamente métodos de ser analizados por una regla paramétrica basándose en propiedades de métodos como isView, isPure, etc.

Uso del bloque filtered para excluir funciones View

Para comprender el funcionamiento del bloque de filtro, considere la especificación a continuación que incluye una regla que contiene un bloque de filtro.

Copy
rule totalSupplyIntegrityCheck(env e, method f, calldataarg args) filtered {
    f -> !f.isView
} {

    // Step 1: Record initial state
    mathint supplyBefore = totalSupply(e);

    // Step 2: Execute an arbitrary function
    f(e, args);

    // Step 3: Record updated state
    mathint supplyAfter = totalSupply(e);

    // Step 4: Function-specific assertions
    if (f.selector == sig:mint(address,uint256).selector) {
        assert supplyAfter >= supplyBefore, "Total supply should not decrease after mint()";
    } 
    else if (f.selector == sig:burn(uint256).selector) {
        assert supplyAfter <= supplyBefore, "Total supply should not increase after burn()";
    } 
    else {
        assert supplyAfter == supplyBefore, "Total supply must remain unchanged for other function calls";
    }
}

En la regla anterior, la línea f -> !f.isView dentro del bloque de filtro filtered {} actúa como un filtro que le dice al Prover: “Ejecuta esta regla solo en funciones donde f.isView sea falso”. En otras palabras, excluye de la verificación a todas las funciones marcadas como view.

Si volvemos a ejecutar el Prover con la especificación anterior, podemos ver que las funciones view como totalSupply(), balanceOf()** y** owner() ya no están incluidas en la verificación de esta regla, como se muestra en la imagen a continuación:

Usar un bloque de filtro dentro de una regla paramétrica nos ayuda a lograr dos cosas:

1. Reduce la sobrecarga computacional al omitir funciones irrelevantes de las que se garantiza que no cambiarán el estado del contrato.
2. Simplifica la salida de verificación, permitiéndonos enfocarnos únicamente en los resultados de las funciones que cambian el estado.

Conclusión

Así es como podemos utilizar las propiedades de métodos para aplicar aserciones específicas de funciones, así como excluir funciones irrelevantes de la verificación mediante el uso de bloques filtered.

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