Hasta ahora, hemos escrito una regla para verificar comportamientos específicos o un invariante para verificar propiedades que siempre deben cumplirse durante la vida útil del contrato. Sin embargo, al verificar nuevas propiedades, a menudo queremos asumir que otras propiedades que ya hemos probado se siguen cumpliendo.

Por ejemplo, al verificar una regla para la transferencia de tokens, es posible que queramos asumir que el suministro total sigue siendo igual a la suma de todos los saldos, una propiedad ya probada por un invariante separado. El uso de invariantes probados como suposiciones evita que las reglas fallen debido a estados de contrato poco realistas (estados que violan propiedades que ya hemos probado que nunca pueden ocurrir).

Aquí es donde entra en juego la declaración requireInvariant de CVL. La declaración requireInvariant nos permite tomar un invariante que ya hemos probado y usarlo como suposición al verificar nuevas reglas o invariantes.

En este capítulo, exploraremos qué es requireInvariant, por qué es útil y cómo aplicarlo de manera efectiva al escribir reglas e invariantes en CVL.

Comprendiendo la declaración requireInvariant

La declaración requireInvariant es una construcción de CVL que nos permite inyectar un invariante probado como una condición adicional en una regla u otro invariante.

Cómo funciona requireInvariant

Cuando se incluye una declaración requireInvariant en una regla u otro invariante, el Prover asume automáticamente que el invariante referenciado ya es verdadero durante la verificación. Como resultado, explora solo aquellos estados del contrato que satisfacen esta condición.

Uso de requireInvariant en Reglas e Invariantes

Para usar requireInvariant en una regla, simplemente haz referencia al invariante por su nombre al principio de la regla:

Copy
rule ruleName(env e, ...) {

    requireInvariant invariantName();

    // rule logic here
}

Al usar requireInvariant dentro de un invariante (en lugar de una regla), la sintaxis es diferente. La declaración se coloca dentro de un bloque preserved, como se muestra a continuación:

Copy
invariant invariantName()
    conditionExpression;

{
    preserved with (env e) {
        requireInvariant otherInvariantName();
    }
}

Ahora que entendemos el propósito de la declaración requireInvariant y cómo nos ayuda a reutilizar invariantes probados, veamos cómo funciona en la práctica.

Revisando el invariante totalSupplyEqSumOfBalances()

Al trabajar con tokens ERC20, una de las comprobaciones de seguridad más fundamentales es garantizar que la suma de todos los saldos sea siempre igual al suministro total de tokens. Este invariante, a menudo denominado integridad del token, garantiza que los tokens no puedan crearse o destruirse involuntariamente y que la suma de todos los saldos individuales sea igual al suministro total.

En el capítulo titulado “Verificando un Invariante Usando Ghosts y Hooks”, verificamos formalmente esta propiedad de seguridad crítica de la implementación de ERC20 de Transmission11 y su biblioteca Solmate usando la siguiente especificación:

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

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}


invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

Veamos cómo podemos usar el invariante probado totalSupplyEqSumOfBalances() como suposición en otra regla o invariante.

Aplicando requireInvariant en Reglas

Supongamos que queremos definir una regla checkTransferSuccess() para verificar la exactitud de la función transfer() en nuestro contrato ERC20. Específicamente, queremos asegurarnos de que una transferencia exitosa actualice correctamente los saldos del remitente y del destinatario mientras deja intacto el suministro total.

Para expresar tal regla, seguimos estos pasos:

1. Comprender el comportamiento esperado de la función transfer().
2. Escribir una regla en CVL para verificar este comportamiento.
3. Ejecutar la verificación y observar el resultado.

Como veremos, la verificación inicial fallará; no por un error en el contrato, sino porque el Prover explora estados poco realistas. Esto nos llevará a introducir requireInvariant como la solución.

Pongamos estos pasos en práctica.

Comprendiendo la expectativa de la función transfer()

Para definir la especificación para la llamada exitosa de transfer(), primero examinemos la implementación de la función del contrato ERC20 de Solmate:

Copy
function transfer(address to, uint256 amount) public virtual returns (bool) {

    balanceOf[msg.sender] -= amount;

    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(msg.sender, to, amount);

    return true;
}

A partir del código anterior, podemos ver que la función transfer() mueve un número específico de tokens (amount) de la cuenta del remitente a la cuenta del destinatario (to). La función sigue esta lógica:

• Si el remitente tiene suficientes tokens: el saldo del remitente disminuye en amount, y el saldo del destinatario aumenta en la misma cantidad.
• Si el remitente no tiene suficientes tokens: la operación se revierte automáticamente debido a un desbordamiento aritmético negativo (underflow), y no ocurren cambios de estado.

Expresando nuestra expectativa de la llamada a transfer() en CVL

Ahora que tenemos una comprensión clara del comportamiento esperado de la función transfer(), podemos traducirlo a código CVL siguiendo estos pasos:

1. Abrir el archivo de especificación: Dentro del directorio de tu proyecto de Certora, navega al subdirectorio specs y abre el archivo erc20.spec que creamos para verificar el invariante totalSupplyEqSumOfBalances(). El archivo debería contener la siguiente especificación:

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

ghost mathint sumOfBalances {
    init_state axiom sumOfBalances == 0;
}

hook Sload uint256 balance balanceOf[KEY address addr] {
    require sumOfBalances >= to_mathint(balance);
}

hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount)  {
    sumOfBalances = sumOfBalances - oldAmount + newAmount;
}

invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

2. Añadir una regla: Extiende el archivo erc20.spec añadiendo un nuevo bloque de regla llamado checkTransferCall().

Copy
rule checkTransferSuccess() {
    // we’ll fill this step by step
}

3. Incluir el argumento del entorno: Dado que nuestra llamada a transfer() necesita acceso al entorno de la transacción (como msg.sender y otras variables de contexto de la EVM), pasamos este entorno como un argumento de tipo env e.

Copy
rule checkTransferSuccess(env e) {
    // we’ll fill this step by step
}

4. Declarar las entradas: La función transfer() requiere dos entradas: una dirección de destinatario y una cantidad de tokens a transferir. Declaramos estas como variables locales en nuestra regla.

Copy
rule checkTransferSuccess(env e){

    // NEWLY ADDED //
    address to;
    uint256 amount;
    
}

5. Añadir restricciones mínimas al entorno: No todas las combinaciones de entrada representan un escenario válido para la verificación. Por ejemplo, no queremos que el llamador (msg.sender) sea el propio contrato, y no queremos permitir transferencias donde el remitente y el destinatario sean la misma cuenta. Añadimos declaraciones require para excluir estos escenarios inválidos.

Copy
rule checkTransferSuccess(env e){

    address to;
    uint256 amount;
    
    // NEWLY ADDED //
    require e.msg.sender != currentContract;
    require e.msg.sender != to;
}

6. Capturar el estado previo a la llamada: Antes de realizar la llamada a transfer(), registramos el saldo del remitente, el saldo del destinatario y el suministro total. Estos valores sirven como línea base contra la cual verificamos los cambios después de la llamada.

Copy
rule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;
    
    // NEWLY ADDED //
    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();
}

7. Invocar la función transfer(): Ahora invocamos la función transfer() usando el entorno e, junto con la dirección del destinatario to y la cantidad de transferencia amount.

Copy
rule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();
    
    // NEWLY ADDED //
    transfer(e,to,amount);
    
}

Nota: Llamamos a transfer() sin el modificador @withrevert; esto significa que la regla solo verifica las ejecuciones donde la transferencia tiene éxito. Si la transferencia se revirtiera (por ejemplo, debido a un saldo insuficiente), el Prover simplemente excluye esa ruta de la verificación.

8. Capturar el estado posterior a la llamada: Después de que se ejecuta la transferencia, una vez más capturamos el saldo del remitente, el saldo del destinatario y el suministro total para poder compararlos con nuestras expectativas.

Copy
rule checkTransferSuccess(env e) {

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;


    mathint precallSenderBalance = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer@withrevert(e,to,amount);
    bool transferCallStatus = lastReverted;

    // NEWLY ADDED //
    mathint postcallSenderBalance = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();
    
}

9. Asegurar la exactitud de los resultados: A continuación, codificamos nuestras expectativas como aserciones:

• El saldo del remitente debería disminuir exactamente en amount.
• El saldo del destinatario debería aumentar exactamente en amount.
• El suministro total debe permanecer sin cambios (las transferencias mueven tokens, no los crean ni los destruyen).

Copy
rule checkTransferSuccess(env e){

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer(e, to, amount);

    mathint postcallSenderBalance   = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();
    
    // NEWLY ADDED //
    assert postcallSenderBalance == precallSenderBalance - amount;
    assert postcallReceiverBalance == precallReceiverBalance + amount;
    assert precallTotalSupply == postcallTotalSupply;
}

10. Actualizar el bloque de métodos: Anteriormente, nuestro bloque methods contenía solo la función totalSupply(), ya que era la única invocada explícitamente en la especificación. Ahora, también necesitamos incluir la función balanceOf(), ya que nuestra regla hace referencia a ella para leer los saldos de las cuentas.

Copy
methods {
    function totalSupply() external returns(uint256) envfree;
    function balanceOf(address) external returns(uint256) envfree; // Add this
}

Al igual que totalSupply(), la función balanceOf() no depende del entorno de la transacción (por ejemplo, no utiliza msg.sender ni msg.value). Por lo tanto, la declaramos como envfree.

Nota: Si te preguntas cómo estamos usando la función balanceOf() aunque no aparece en el código fuente del contrato, la respuesta radica en cómo Solidity maneja las variables de estado públicas. Cuando declaras una variable como mapping(address => uint256) public balanceOf;, el compilador genera automáticamente una función getter con la firma:

Copy
function balanceOf(address) external view returns (uint256);

Este getter es parte de la interfaz del contrato compilado, incluso si no está escrito explícitamente en el código fuente.

Opcionalmente, también podemos incluir la firma de la función transfer() en el bloque de métodos. Sin embargo, hacerlo no mejorará el rendimiento de la verificación, ya que esta función no es envfree.

Copy
methods {
    function totalSupply() external returns(uint256) envfree;
    function balanceOf(address) external returns(uint256) envfree;
    function transfer(address,uint256) external returns(bool);
}

Ejecutando la Verificación Inicial

Ahora que nuestra regla checkTransferSuccess() está completa, ejecutemos el Prover para ver si pasa la verificación.

Para ejecutar la verificación, sigue las instrucciones a continuación:

1. Asegúrate de que tu archivo .conf coincida con la configuración a continuación:

Copy
{
    "files": [
        "contracts/ERC20.sol:ERC20"
    ],
    "verify": "ERC20:specs/erc20.spec",
    "optimistic_loop": true,
    "msg": "Testing erc20 functionality"
}

2. A continuación, ejecuta el siguiente comando en tu terminal:

Copy
certoraRun confs/erc20.conf

Esto enviará tu especificación y contrato al Certora Prover para su verificación.

3. Una vez que el Prover finalice la ejecución (lo que puede tardar unos minutos), mostrará un enlace único al informe de verificación en tu terminal. Abre el enlace en tu navegador para ver un resultado similar a la imagen a continuación:

El resultado muestra que checkTransferSuccess() ha fallado la verificación.

Comprendiendo el fallo

Para entender por qué falló la regla, examinemos la traza de la llamada. En la sección Storage State bajo Global State #1, podemos ver los valores iniciales que eligió el Prover:

El Prover comenzó desde un estado con los siguientes valores:

Storage State (ERC20):

• balanceOf[0x2712] = 0x7 (7 tokens)
• balanceOf[0x25fc] = 2^256 - 5 (un valor astronómicamente grande)
• totalSupply = 0x6 (solo 5 tokens)
• sumOfBalances = 2^256 + 8 ( Ghost State)

Nota las etiquetas HAVOC en el lado derecho de cada valor. Esto indica que estos valores fueron elegidos arbitrariamente por el Prover.

La inconsistencia es sorprendente: una cuenta posee 2^256 - 5 tokens, pero el suministro total es solo de 6. Otra cuenta tiene 7 tokens, uno más que el suministro total. Mientras tanto, la variable ghost sumOfBalances está establecida en 2^256 + 8, lo que no tiene relación ni con los saldos individuales ni con el suministro total.

Esto sucede porque el Prover no asume automáticamente que nuestro invariante previamente probado totalSupplyEqSumOfBalances() se cumpla al verificar una nueva regla. Cada regla comienza desde un estado simbólico nuevo donde a las variables de almacenamiento y a los ghosts se les asignan valores arbitrarios, a menos que los restrinjamos explícitamente. Como resultado, el Prover explora estados que nunca podrían ocurrir en una ejecución real de ERC-20; estados donde la relación contable entre los saldos, el ghost y el suministro total está completamente rota.

Cuando se ejecuta transfer() bajo estas condiciones poco realistas, nuestras aserciones sobre los cambios de saldo fallan, aunque la lógica del contrato sea correcta.

Solucionando el Fallo con requireInvariant

Para descartar tales estados inconsistentes, debemos decirle al Prover que checkTransferCall() solo debe verificarse bajo la suposición de que totalSupplyEqSumOfBalances() ya se cumple.

Hacemos esto insertando la siguiente línea al principio de la regla:

Copy
requireInvariant totalSupplyEqSumOfBalances();

Esta línea le dice al Prover que comience la verificación desde un estado donde nuestro invariante anterior ya es verdadero. En términos simples, el Prover solo comprobará la regla en situaciones donde el suministro total ya sea igual a la suma de todos los saldos.

Aquí está la regla completa con requireInvariant añadido:

Copy
// Our Rule
rule checkTransferSuccess(env e){
   
   requireInvariant totalSupplyEqSumOfBalances();

    address to;
    uint256 amount;

    require e.msg.sender != currentContract;
    require e.msg.sender != to;

    mathint precallSenderBalance   = balanceOf(e.msg.sender);
    mathint precallReceiverBalance = balanceOf(to);
    mathint precallTotalSupply = totalSupply();

    transfer(e,to,amount);

    mathint postcallSenderBalance   = balanceOf(e.msg.sender);
    mathint postcallReceiverBalance = balanceOf(to);
    mathint postcallTotalSupply = totalSupply();
    
    
    assert postcallSenderBalance == precallSenderBalance - amount;
    assert postcallReceiverBalance == precallReceiverBalance + amount;
    assert precallTotalSupply == postcallTotalSupply;
 
}

Re-ejecutando la Verificación

Ahora ejecutemos el Prover de nuevo con la declaración requireInvariant en su lugar:

Copy
certoraRun confs/erc20.conf

Abre el enlace de verificación para ver el resultado:

Nuestro resultado de verificación muestra claramente que el Prover ha verificado la regla. Eso significa que la función transfer() actualiza correctamente los saldos y preserva el invariante del suministro total.

El ejemplo discutido anteriormente deja en claro que añadir requireInvariant garantiza que el Prover solo considere estados de contrato realistas que respeten las propiedades globales ya probadas. En la siguiente sección, veremos cómo usar requireInvariant dentro de otra definición de invariante.

Uso de requireInvariant en Invariantes

Para entender cómo se puede utilizar requireInvariant dentro de la construcción de invariante de CVL, definamos otro invariante llamado indBalanceCap() dentro de nuestro archivo erc20.spec (justo debajo del invariante totalSupplyEqSumOfBalances()).

Copy
///..
invariant totalSupplyEqSumOfBalances()
    to_mathint(totalSupply()) == sumOfBalances;

// Our new Invariant
invariant indBalanceCap(address a)
    to_mathint(balanceOf(a)) <= to_mathint(totalSupply());
//.....

Este nuevo invariante codifica una propiedad de seguridad fundamental de ERC-20: el saldo de ninguna cuenta debería exceder nunca el suministro total.

Verificando Nuestro Nuevo Invariante

Ahora ejecutemos el Prover, y luego abramos el enlace de verificación proporcionado por el Prover para ver un resultado similar a la imagen a continuación:

El resultado anterior muestra que nuestro invariante indBalanceCap() ha fallado el proceso de verificación.

Un análisis más detallado del informe del Prover muestra que el invariante falló la comprobación de inducción. Específicamente, el Prover identificó violaciones del invariante a través de las llamadas a las funciones transfer() y transferFrom(), como se muestra en la imagen a continuación:

Para entender la causa de la violación, analicemos la traza de la llamada a transfer(). (Nota: transferFrom() falla por la misma razón, así que analizar transfer() cubre ambos casos)

Comprendiendo la Violación

Comencemos nuestro análisis con la sección Storage State del informe del Prover. Esta sección muestra los valores reales de las variables de almacenamiento del contrato en el punto inicial de la verificación.

En el Storage State, podemos ver que los saldos de las cuentas individuales son los siguientes:

• balanceOf[0x2711] = 0x5 (la cuenta 0x2711 posee 5 tokens)
• balanceOf[0x2713] = 0x4 (la cuenta 0x2713 posee 4 tokens)

mientras que el totalSupply del token se registra como solo 0x4 (es decir, 4 tokens).

Dado que ya probamos el invariante totalSupplyEqSumOfBalances(), un estado como este nunca debería ocurrir durante una ejecución real del contrato. Ese invariante dice que en todo estado válido, el suministro total debe ser siempre igual a la suma de todos los saldos. Pero en la traza anterior, los saldos suman 9 mientras que el suministro total es solo 4. Esta discrepancia muestra que el Prover comenzó desde un estado que en realidad no es alcanzable en nuestra implementación de ERC-20.

Esto sucede porque el Prover no asume automáticamente que los invariantes probados previamente deban cumplirse cuando comienza a verificar una nueva propiedad. Cada nueva regla o invariante comienza desde un estado simbólico nuevo a menos que lo conectemos explícitamente a resultados anteriores. Como resultado, el Prover puede elegir una configuración inicial que viole el invariante que probamos antes, incluso si tal configuración es imposible durante la ejecución real del contrato.

Solucionando el fallo con la declaración requireInvariant

Para descartar tales estados inconsistentes, debemos decirle al Prover que indBalanceCap() solo debe verificarse bajo la suposición de que totalSupplyEqSumOfBalances() ya se cumple.

Para forzar esto, importamos explícitamente ese invariante usando requireInvariant, como se muestra a continuación:

Copy
invariant indBalanceCap(address a)
    to_mathint(balanceOf(a)) <= to_mathint(totalSupply())
{
    preserved with (env e) {
        // Require that our earlier invariant holds
        requireInvariant totalSupplyEqSumOfBalances();
    }
}

De esta manera, el Prover comienza desde un mundo que ya satisface la regla de conservación de tokens que probamos previamente y evita que el espacio de búsqueda se desvíe hacia estados imposibles de ERC-20.

Verificando el Invariante Fortalecido

Ahora, si volvemos a ejecutar el Prover con:

Copy
certoraRun confs/erc20.conf

y abrimos el enlace de verificación, veremos un resultado similar a la imagen a continuación:

Podemos ver, como se esperaba, que indBalanceCap() ahora se verifica con éxito. Dado que el Prover fue restringido a estados que ya satisfacen totalSupplyEqSumOfBalances(), ya no encontró las configuraciones imposibles que causaron el fallo anterior.

require vs requireInvariant: Mismo Filtro, Diferente Garantía

Curiosamente, el invariante indBalanceCap() también pasaría la verificación si usáramos una declaración require regular en lugar de requireInvariant, como se muestra a continuación:

Esto sucede porque, dentro de un bloque preserved, tanto require como requireInvariant cumplen el mismo propósito operativo: filtran el estado previo del paso de inducción. En efecto, ambas declaraciones instruyen al Prover:

“Solo explora las transiciones que comienzan desde estados que satisfacen esta condición.”

Por esta razón, las siguientes dos líneas imponen la misma restricción funcional en el espacio de búsqueda:

Copy
requireInvariant totalSupplyEqSumOfBalances();

y

Copy
require to_mathint(totalSupply()) == sumOfBalances;

Ambas evitan que el Prover considere el estado inicial inconsistente que observamos anteriormente, permitiendo que el invariante indBalanceCap() pase.

Por qué requireInvariant sigue siendo preferible

Aunque ambas formas restringen el espacio de búsqueda de manera similar, difieren en cuán confiable y fundamentada resulta la especificación.

Un requireInvariant es más seguro porque importa una propiedad que el Prover ya ha establecido como verdadera en todos los estados alcanzables. Un require simple confía enteramente en que el autor de la especificación declare una condición correcta. Por ejemplo:

Copy
require to_mathint(totalSupply()) == sumOfBalances;

obliga al Prover a aceptar esta igualdad sin comprobar si es realmente verdadera. Si la condición es aunque sea ligeramente incorrecta o incompleta, el Prover podría ignorar silenciosamente contraejemplos reales, dando una verificación engañosamente exitosa.

Por lo tanto, la diferencia clave es simple:

• require aplica la condición que escribimos.
• requireInvariant aplica una condición que ya se ha demostrado que es universalmente verdadera.

Debido a esto, requireInvariant ofrece una forma más segura y fundamentada de reutilizar suposiciones, mientras que un require simple puede ocultar involuntariamente violaciones genuinas si la condición es incorrecta o incompleta.

Conclusión

Así es como podemos usar requireInvariant para hacer que nuestras especificaciones sean más fuertes, más modulares y más eficientes.

• En las reglas, nos permite reutilizar invariantes probados como prerrequisitos, asegurando que cada ruta de ejecución se compruebe bajo condiciones realistas.
• En los invariantes, nos permite probar nuevas propiedades asumiendo las anteriores, evitando contraejemplos sin sentido que provienen de estados inconsistentes.

El principio clave es simple pero poderoso: prueba los invariantes globales primero, luego reutilízalos como bloques de construcción al verificar comportamientos específicos o invariantes adicionales.

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