En este capítulo, aprenderemos cómo usar las etiquetas de métodos (@withrevert y @norevert) y la variable especial lastReverted en CVL para verificar los reverts esperados en la ejecución de contratos inteligentes.
Configuración de escenarios de verificación para la función Add()
Considere el siguiente contrato Math, que tiene una función básica add() que toma dos enteros sin signo como entradas y devuelve su suma como salida.
//SPDX-License-Identifier : MIT
pragma solidity 0.8.25;
contract Math {
function add(uint256 x, uint256 y) public pure returns (uint256) {
return x + y;
}
}
La función add() se comporta de la siguiente manera:
- Cuando se proporcionan entradas válidas, debe calcular correctamente la suma de
xey, y devolver el resultado como un valoruint256. Por ejemplo,add(15, 10)devolverá 25. - Dado que el contrato utiliza la versión 0.8.0 de Solidity o posterior, la transacción hará revert si la suma excede el valor máximo de
uint256(2^256 - 1). Por ejemplo, six = 2^256 - 1ey = 1, el overflow hará que la transacción haga revert en lugar de devolver un resultado.
Verificando la especificación de la función add()
Considere la siguiente especificación para verificar la corrección de la función add() del contrato Math:
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule checkAdd() {
uint256 a;
uint256 b;
uint256 c = add(a,b);
assert a + b == c;
}
Para ver el resultado de la verificación de la especificación anterior, ejecute el Prover y abra el enlace de verificación para ver un resultado similar a la imagen a continuación.
Esto podría parecer sorprendente porque se espera que la función add() haga revert cuando la suma de x e y excede el valor máximo de uint256. Dado que el Prover explora diferentes rutas de ejecución para verificar la corrección, uno esperaría que también se encontrara con el escenario de revert. En tales casos, la declaración assert debería evaluarse como falsa, y la regla debería fallar la verificación.
Sin embargo, esto no sucedió, y nuestra regla fue verificada de todos modos por el Prover. Esto se debe a que, de forma predeterminada, el Prover ignora los casos de revert durante la verificación.
Esto plantea una pregunta importante: ¿Por qué el Prover elige ignorar los casos de revert durante la verificación?
¿Por qué el Prover ignora las rutas de revert?
La razón es que los reverts pueden ser una parte normal de la operación; por ejemplo, si alguien que no es el propietario del contrato intenta realizar una acción privilegiada. En tales casos, un revert no se considera un fallo; es el comportamiento esperado.
Al ignorar las rutas de revert, el Prover se enfoca en verificar escenarios de ejecución exitosos donde la función se completa sin errores. Sin embargo, podemos anular este comportamiento predeterminado utilizando la etiqueta de método @withrevert proporcionada por CVL.
Introducción a las etiquetas de métodos de CVL
Certora nos proporciona dos etiquetas de métodos, @norevert y @withrevert, que se pueden colocar después del nombre del método pero antes de los argumentos del método, como se muestra a continuación:
function_name@norevert();
function_name@withrevert();
Cuando usamos la etiqueta @norevert con una llamada a un método, el Prover descarta activamente cualquier ruta de ejecución que resulte en un revert. En otras palabras, function_name@norevert() se comporta de manera idéntica a function_name() .
Por otro lado, cuando usamos la etiqueta @withrevert con una llamada a un método, el Prover ya no ignora los casos de revert. En cambio, trata cualquier escenario donde ocurre un revert como una violación. Por ejemplo, considere la regla checkAdd() a continuación con la etiqueta @withrevert:
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule checkAdd() {
uint256 a;
uint256 b;
uint256 c = add@withrevert(a,b);
assert a + b == c;
}
Cuando volvemos a ejecutar el Prover con esta especificación actualizada, el resultado cambia: la regla ahora falla la verificación, como se muestra en la imagen a continuación:
Dado que usamos la etiqueta @withrevert con la llamada a la función add(), el Prover ya no ignora los casos de revert. Como resultado, si la suma de a y b excede el valor máximo de uint256, la regla trata el revert como una violación. El verificador detecta este problema y reporta un contraejemplo—uno que conduce a un overflow y un revert, causando finalmente que la aserción falle. Cuando ocurre un revert, no hay valor de retorno—c no tiene restricciones y puede tomar un valor arbitrario. Debido a esto, la aserción a + b == c no se puede cumplir.
Introducción a la Variable Especial de CVL: lastReverted
En CVL, tenemos acceso a una variable booleana especial llamada lastReverted, que se actualiza después de cada llamada a un método—incluidas aquellas realizadas sin @withrevert. Esta variable indica si la función del contrato más reciente hizo revert (lastReverted = true) o se ejecutó con éxito (lastReverted = false).
Sin embargo, de forma predeterminada, el Prover ignora cualquier ruta de ejecución que resultaría en un revert. Esto significa que cuando se llama a una función sin @withrevert—como con la llamada predeterminada o usando la etiqueta @norevert—el Prover no explora escenarios de revert, y el valor de lastReverted siempre permanecerá en false.
Para rastrear con precisión si una función hace revert, debemos instruir explícitamente al Prover para que considere las rutas de revert utilizando la etiqueta @withrevert. Cuando se llama a una función con @withrevert, el Prover ya no ignora los escenarios de revert, y si ocurre un revert, lastReverted se actualiza a true.
Ejemplo: Detectando Reverts debido a Overflow
Ahora, veamos cómo se puede usar lastReverted en reglas de verificación prácticas. Probaremos una función add(), asegurándonos de que se comporte correctamente en los casos en los que ocurre y no ocurre un overflow.
Caso 1: La función debe hacer revert en caso de Overflow
Considere la regla addShouldRevert() a continuación, que tiene como objetivo verificar que la función add() haga revert correctamente cuando ocurre un overflow.
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule addShouldRevert() {
uint256 a;
uint256 b;
require(a + b > max_uint256);
add@withrevert(a,b);
assert lastReverted; // This is the same as assert lastReverted == true;
}
La declaración require(a + b > max_uint256); en la regla addShouldRevert() asegura que las entradas a y b se elijan de tal manera que su suma exceda el valor máximo que un uint256 puede almacenar, causando un overflow. Las operaciones aritméticas de Solidity hacen revert automáticamente en casos de overflow, desencadenando un revert para la llamada a la función add(a, b).
Nota: En CVL, los valores máximos para diferentes tipos de enteros están disponibles como variables, tales como max_uint8, max_uint16, …, max_uint256, etc.
Debido a que la función se invoca usando @withrevert, el Prover no ignora este escenario de revert y lo detecta correctamente. Como resultado, lastReverted se establece en true, lo que indica que la ejecución de la función hizo revert. La aserción assert lastReverted; luego se evalúa como true, ya que lastReverted coincide con el resultado esperado. En consecuencia, la regla debería pasar, como se muestra en la imagen a continuación.
Caso 2: La función no debe hacer revert en una suma válida
De manera similar, considere la regla addShouldNotRevert(), que tiene como objetivo verificar que la función add() no haga revert cuando la suma de a y b permanezca dentro del rango válido de uint256.
methods {
function add(uint256,uint256) external returns(uint256) envfree;
}
rule addShouldNotRevert() {
uint256 a;
uint256 b;
require(a + b <= max_uint256);
add@withrevert(a,b);
assert !lastReverted;
}
En la regla anterior, la declaración require(a + b <= max_uint256); asegura que las entradas a y b se elijan de tal manera que su suma no cause un overflow. Dado que las operaciones aritméticas de Solidity solo hacen revert cuando ocurre un overflow u otro fallo explícito, la función add(a, b) se ejecuta con éxito sin hacer revert.
Dado que la función se llama con @withrevert, el Prover rastrea si ocurre un revert. Sin embargo, debido a que la suma no excede el límite de uint256, no ocurre ningún revert, y lastReverted permanece en false. La aserción assert !lastReverted; verifica esto, asegurando que la regla pase con éxito, como se muestra a continuación.
Evitando la sobreescritura de lastReverted
Dado que lastReverted se actualiza después de cada llamada a una función, las llamadas posteriores pueden sobrescribir su valor. Esto significa que si una función hace revert pero otra función se ejecuta inmediatamente después, el estado de revert original se pierde.
Para prevenir errores de verificación, siempre capture lastReverted inmediatamente después de la llamada a la función relevante, antes de realizar llamadas adicionales que podrían sobrescribir su valor.
Para ilustrar esto, consideremos un contrato aritmético simple:
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Math {
function add(uint256 x, uint256 y) public pure returns (uint256) {
return x + y;
}
function divide(uint256 x, uint256 y) public pure returns (uint256) {
return x / y;
}
}
El contrato anterior define dos funciones básicas:
add(x, y)simplemente devuelve la suma dexey.divide(x, y)realiza una división de enteros, la cual hace revert siy == 0debido a la protección incorporada de Solidity contra la división por cero.
Ahora, considere la siguiente regla diseñada para verificar cómo se comportan ambas funciones cuando reciben 0 como el segundo argumento:
methods {
function divide(uint256,uint256) external returns(uint256) envfree;
function add(uint256,uint256) external returns(uint256) envfree;
}
rule checkMath() {
uint256 a;
divide@withrevert(a,0);
bool divideCallStatus = lastReverted;
add@withrevert(a,0);
bool addCallStatus = lastReverted;
assert divideCallStatus == true;
assert addCallStatus == false;
}
Si no guardamos lastReverted inmediatamente después de llamar a divide(a, 0), la siguiente llamada a la función (add(a, 0)) lo actualizará nuevamente, borrando por completo la información sobre el fallo de la operación de división.
Esto significa que si una regla comprueba más tarde si divide(a, 0) hizo revert, podría concluir incorrectamente que la función se ejecutó con éxito—incluso aunque en realidad falló. Dicha verificación falsa puede resultar en un análisis incorrecto del contrato, llevando a vulnerabilidades de seguridad o suposiciones defectuosas en lógica crítica.
Al guardar lastReverted inmediatamente después de llamar a divide(a, 0), nos aseguramos de capturar con precisión el comportamiento de la función antes de realizar cualquier otra llamada. Esto preserva el historial de ejecución correcto, previniendo sobreescrituras no intencionadas y garantizando una verificación confiable.
Conclusión
Probar tanto los casos de éxito como los de revert es crucial para realizar la verificación formal de un método, ya que proporciona una mejor cobertura y garantiza que el método se comporte correctamente bajo todas las posibles condiciones de entrada, incluyendo casos extremos como overflows o entradas inválidas.
Este artículo es parte de una serie sobre verificación formal usando el Prover de Certora