Introducción

Algunos comportamientos de los contratos (propiedades) son inherentemente condicionales, y el uso de construcciones como if/else en CVL es una forma de capturar el comportamiento condicional de manera formal.

Las declaraciones if/else en CVL funcionan de la misma manera que en otros lenguajes. Aquí proporcionaremos ejemplos de verificación formal de código con características condicionales.

Aserciones e invocaciones de métodos

Comencemos verificando formalmente una función simple que toma dos enteros sin signo (uint256) y devuelve su suma (uint256). El resultado esperado es condicional: si la suma causa un overflow, la función revierte; de lo contrario, devuelve la suma.

A continuación se muestra la implementación en Solidity de la función add():

Copy
/// Solidity

function add(uint256 x, uint256 y) external pure returns (uint256) {
    return x + y;
}

Y aquí está la especificación en CVL (sum es una palabra clave reservada desde la versión del P__rover 7.25.2, así que en su lugar usamos _sum .):

Copy
/// CVL

methods {
    function add(uint256,uint256) external returns(uint256) envfree;
}

rule add_sumWithOverflowRevert() {
    uint256 x;
    uint256 y;

    mathint _sum = x + y;
    
    if (_sum <= max_uint256) { // non-revert case
        mathint result = add@withrevert(x, y);
        assert !lastReverted;
        assert result == _sum;
    }
    else { // revert case
        add@withrevert(x, y);
        assert lastReverted; 
    }
}

Analicemos qué está sucediendo en el código de especificación anterior. En las siguientes líneas,

Copy
uint256 x;
uint256 y;

mathint _sum = x + y;

la variable _sum se declara como un mathint, un tipo sin límites de overflow, lo que le permite representar de manera precisa x + y incluso si excede max_uint256. Esto nos permite detectar un overflow al comparar _sum con max_uint256 y determinar si la función debería revertir.

Ahora en las siguientes líneas,

Copy
if (_sum <= max_uint256) {
    mathint result = add@withrevert(x, y);
    assert !lastReverted;
    assert result == _sum;
}

la operación de suma de Solidity se realiza si _sum = x + y permanece dentro de los límites de max_uint256.

La etiqueta @withrevert se agrega a una función para instruir al Prover que incluya las rutas de reversión o los argumentos que causan un revert. El assert !lastReverted significa que nunca deberíamos obtener un revert si la suma no causó un overflow.

Finalmente, el bloque else que se muestra a continuación maneja los casos de overflow esperando un revert cuando _sum excede max_uint256.

Copy
else {
    add@withrevert(x, y);
    assert lastReverted; 
}

Como se esperaba, la regla de CVL da como resultado VERIFIED:

Ejecución del Prover: link

Este ejemplo muestra que las funciones de Solidity se pueden invocar y las aserciones se pueden realizar dentro de bloques o ramas condicionales.

Asignaciones de variables en una declaración if

A continuación, verificaremos formalmente la función max optimizada para gas de la biblioteca Solady.

A continuación se muestra la implementación de la función max de Solady. Aunque puede que no sea inmediatamente obvio, devuelve el mayor entre x e y. Si x es igual a y, la función simplemente devuelve x.

Copy
/// Solidity

function max(uint256 x, uint256 y) external pure returns (uint256 z) {
    assembly {
        z := xor(x, mul(xor(x, y), gt(y, x)))
    }
}

Ten en cuenta que hemos cambiado la visibilidad de internal a external para eliminar la necesidad de un archivo harness, lo cual está fuera del alcance de este capítulo.

Explicar el funcionamiento interno de esta implementación en assembly también está fuera del alcance de este capítulo. Sin embargo, si tienes curiosidad, aquí hay un video que cubre los detalles en menos de cinco minutos: https://www.youtube.com/watch?v=4nDUQIk4oqQ.

Ahora, procedamos con la verificación formal de la función max de Solady. Tiene dos variaciones: una para enteros sin signo y otra para enteros con signo. Dado que ambas siguen el mismo concepto fundamental, nos centraremos en la variación de enteros sin signo.

Aquí hay una regla de CVL inicial para verificar la función max de Solady, pero la simplificaremos en breve:

Copy
/// CVL

rule max_returnMax() {
    uint256 x;
    uint256 y;

    if (x >= y) {
        mathint max = max@withrevert(x, y);
        assert !lastReverted;
        assert max == x;
    }
    else {
        mathint max = max@withrevert(x, y);
        assert !lastReverted;
        assert max == y;
    }
}

En la regla anterior, el bloque if verifica que cuando x > y, el valor máximo es x, o si x = y, simplemente devuelve x ya que ambos valores son idénticos. El bloque else cubre el caso restante, donde x < y, lo que hace que y sea el valor máximo. En cualquier caso, no permitimos reverts ya que la función nunca debería revertir.

Como se esperaba, esta regla da como resultado VERIFIED:

Ejecución del Prover: link

Las invocaciones a funciones y las aserciones no necesitan estar dentro del bloque if/else. Podemos mover las llamadas a las funciones fuera del bloque if y calcular los resultados esperados dentro del bloque if:

Copy
/// CVL

rule max_returnMax_modified() {
    uint256 x;
    uint256 y;

    mathint expectedMax;
    
    if (x >= y) {
        expectedMax = x;
    } else {
        expectedMax = y;
    }
    
    mathint resultMax = max@withrevert(x, y);
    assert !lastReverted;
    
    assert resultMax == expectedMax;
}

Ejecución del Prover: link

Mover las invocaciones de funciones fuera de una declaración if conduce a un código CVL más eficiente, ya que las funciones se invocan solo una vez en lugar de dentro de cada rama condicional. Es posible que el impacto aún no sea notable, pero para reglas más complejas, este enfoque puede ser beneficioso, como mostraremos en la siguiente sección.

Reducción de la complejidad del Verifier, un ejemplo con mulDivUp

mulDivUp() es una función que multiplica dos enteros sin signo, divide el producto por otro entero sin signo y redondea hacia arriba si existe un resto. Si no hay resto, devuelve el cociente tal cual. Por ejemplo, 5 / 2 es 2, pero mulDivUp(5, 2) da como resultado 3 debido al redondeo hacia arriba. En contraste, 4 / 2 es 2, y mulDivUp(4, 2) también da como resultado 2, ya que no hay resto.

Además, revierte en dos casos: cuando el divisor es cero o cuando el numerador (producto de x e y) excede max_uint256.

La implementación que usaremos es mulDivUp() de Solmate, una función eficiente en gas escrita en assembly. Hemos modificado ligeramente el código cambiando su visibilidad de internal a external para evitar usar un archivo harness.

Aquí está la función mulDivUp() de Solmate:

Copy
/// Solidity

uint256 internal constant MAX_UINT256 = 2**256 - 1;

function mulDivUp(
    uint256 x,
    uint256 y,
    uint256 denominator
) external pure returns (uint256 z) {
    assembly {
        // Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))
        if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) {
            revert(0, 0)
        }

        // If x * y modulo the denominator is strictly greater than 0,
        // 1 is added to round up the division of x * y by the denominator.
        z := add(gt(mod(mul(x, y), denominator), 0), div(mul(x, y), denominator))
    }
}

La explicación del código assembly está fuera del alcance de este capítulo, pero los comentarios describen la función de cada línea.

En las líneas a continuación,

Copy
// Equivalent to require(denominator != 0 && (y == 0 || x <= type(uint256).max / y))
if iszero(mul(denominator, iszero(mul(y, gt(x, div(MAX_UINT256, y)))))) {
    revert(0, 0)
}

se define el comportamiento del revert. Implica que el denominator no debe ser cero para prevenir la división por cero. Adicionalmente, garantiza que x * y no exceda MAX_UINT256 y desencadena un revert si lo hace.

En la línea final, se define el comportamiento del redondeo:

Copy
// If x * y modulo the denominator is strictly greater than 0,
// 1 is added to round up the division of x * y by the denominator.
z := add(gt(mod(mul(x, y), denominator), 0), div(mul(x, y), denominator))

Si el resto de x * y dividido por denominator es mayor que cero, se añade uno al resultado para redondear hacia arriba; de lo contrario, el resultado permanece sin cambios.

Ahora que sabemos qué intenta hacer la función, podemos proceder con la verificación formal.

Desarrollo de especificaciones para mulDivUp

Aquí hay una especificación inicial que captura el comportamiento de la función mulDivUp() de Solmate, y la explicación se detalla a continuación:

Copy
/// CVL

rule mulDivUp_roundOrRevert() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    if (denominator == 0) { // catches revert condition: if denominator is zero 
        mulDivUp@withrevert(x, y, denominator); 
        assert lastReverted;
    }
    else if (x * y > max_uint256) { // catches revert condition: multiplication overflows a max_uint256 value
        mulDivUp@withrevert(x, y, denominator);
        assert lastReverted;
    } 
    else { // catches all non-revert conditions
        if (x * y % denominator == 0) { // if there's no remainder after x * y and denominator division
            mathint result = mulDivUp@withrevert(x, y, denominator);
            
            assert !lastReverted;
            assert result == x * y / denominator;
        } 
        else { // if there's a remainder after x * y and denominator division
            mathint result = mulDivUp@withrevert(x, y, denominator); 
            
            assert !lastReverted;
            assert result == (x * y / denominator) + 1;
        }
    }
}

Cuando ejecutamos el Certora Prover, se verifica que el mulDivUp() de Solmate es correcto:

Ejecución del Prover: link

Observa en el código anterior que podemos usar múltiples ramas condicionales con else if, y nada nos impide usar declaraciones if/else anidadas. Sin embargo, para evitar anidar declaraciones if, lo cual dificulta la lectura de la regla, podemos reorganizar las condiciones.

Las siguientes líneas manejan las condiciones de revert:

Copy
if (denominator == 0) {
    mulDivUp@withrevert(x, y, denominator);
    assert lastReverted;
} 
else if (x * y > max_uint256) {
    mulDivUp@withrevert(x, y, denominator);
    assert lastReverted;
}

Si alguna de estas condiciones se cumple, la rama afirma (asserts) lastReverted, lo que significa que la función revierte. Aunque podríamos combinar estas dos condiciones de revert en una sola, abordaremos esto más adelante cuando discutamos la optimización del código.

Si estas dos condiciones de revert no se cumplen, la ejecución pasa a la declaración else, donde se verifica el comportamiento del redondeo. Dentro del bloque else, hay otro conjunto de declaraciones if/else que definen la especificación para el comportamiento del redondeo.

En el bloque else, como verás a continuación, la condición if verifica si el producto de x e y, al calcular el módulo con el denominator, tiene un resto de cero. En este caso, no se necesita redondear hacia arriba, por lo que el valor devuelto es x * y / denominator. Sin embargo, en la rama else, donde la operación de módulo da como resultado un resto mayor que cero, el redondeo hacia arriba se realiza agregando 1 a x * y / denominator.

Copy
else {
    if (x * y % denominator == 0) {
        mathint result = mulDivUp@withrevert(x, y, denominator);
        
        assert !lastReverted;
        assert result == x * y / denominator;
    } 
    else {
        mathint result = mulDivUp@withrevert(x, y, denominator);
        
        assert !lastReverted;
        assert result == (x * y / denominator) + 1;
    }
}

Aprendimos que if/else puede consolidar las verificaciones dentro de una sola regla en lugar de crear múltiples reglas. Sin embargo, también tiene sus desventajas. A medida que la función que se está verificando se vuelve más compleja, la especificación crece en complejidad de manera desproporcionada, lo cual discutiremos a continuación.

Explosión de rutas

El uso de if/else tiende a crear ramas condicionales, invocar funciones y realizar aserciones dentro de los propios bloques condicionales. Cuando esto sucede, el Prover prueba todos los casos en cada rama, lo que aumenta la cantidad de escenarios que deben evaluarse y, naturalmente, ralentiza la ejecución de la regla.

Regla CVL optimizada para mulDivUp

A continuación se muestra la regla optimizada, y luego explicaremos los cambios que realizamos.

Copy
/// CVL

rule mulDivUp_roundOrRevert_optimized() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mathint result = mulDivUp@withrevert(x, y, denominator);

    if (denominator == 0 || x * y > max_uint256) {
        assert lastReverted;
    } 
    else {
        if (x * y % denominator == 0) {
            assert !lastReverted;
            assert result == x * y / denominator;
        } 
        else {
            assert !lastReverted;
            assert result == (x * y / denominator) + 1;
        }
    }
}

El primer cambio que hicimos fue combinar las condiciones de revert en una sola declaración if: if (denominator == 0 || x * y > max_uint256) { … }.

Luego eliminamos todas las invocaciones a la función mulDivUp@withrevert(x, y, denominator) de las ramas y las aislamos en una sola llamada. Esto mejora la eficiencia al evitar llamadas de funciones redundantes dentro de bloques condicionales.

Benchmarks de tiempo de ejecución del Prover

A continuación se muestra la comparación del tiempo de ejecución entre el código ineficiente y el código optimizado:

Ejecución del Prover: link

Al observar el reporte del Prover anterior, el uso ineficiente de if/else puede ralentizar significativamente la ejecución de la regla. Comparando las versiones ineficiente y optimizada, el código ineficiente tarda cuatro veces más en ejecutarse que el código optimizado. Este problema solo empeora a medida que desarrollamos especificaciones para proyectos reales con contratos inteligentes complejos.

Nota_:_ Para comparar dos reglas en función de sus tiempos de ejecución, debemos ejecutarlas simultáneamente y asegurarnos de que el caché esté apagado agregando --cache none en el comando de la CLI.

Todas las condiciones deben manejarse

La construcción if/else inherentemente requiere que todas las condiciones se tengan en cuenta. El bloque if maneja casos específicos, mientras que el bloque else actúa como un comodín (catch-all) para cualquier caso que no se mencione explícitamente en el if.

Esto es tanto bueno como malo. Es bueno porque asegura que se consideren todas las condiciones, previniendo casos omitidos. Sin embargo, a veces solo estamos interesados en el resultado de una condición específica, y tener que dar cuenta de todas las condiciones puede retrasarnos y consumir mucho tiempo.

Por ejemplo, omitamos explícitamente un caso de revert: x * y > max_uint256 en esta regla, y el Prover mostrará el contraejemplo donde x * y excede max_uint256.

Copy
/// CVL

rule mulDivUp_roundOrRevert_omittedARevertCase() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mathint result = mulDivUp@withrevert(x, y, denominator);

    if (denominator == 0) { // intentionally omitted `x * y > max_uint256`
        assert lastReverted;
    } else {
        if (x * y % denominator == 0) {
            assert !lastReverted;
            assert result == x * y / denominator;
        } else {
            assert !lastReverted;
            assert result == (x * y / denominator) + 1;
        }
    }
}

Si solo estamos interesados en la condición de revert denominator == 0, no podemos considerarla exclusivamente usando una construcción if/else (técnicamente podemos, pero es una solución poco elegante y es mejor evitarla). También debemos tener en cuenta todos los demás casos de revert.

La forma idiomática de manejar esto es con el operador de implicación, que se cubrirá en el siguiente capítulo.

Operador ternario

El operador ternario es una alternativa concisa a las declaraciones if/else para lógica condicional simple. Utilizando la sintaxis condition ? expressionA : expressionB, devuelve expressionA si la condición es true; de lo contrario, devuelve expressionB.

Nuestro ejemplo anterior, la función max(), se puede traducir directamente utilizando una expresión ternaria, como se muestra a continuación:

Copy
/// CVL

rule max_returnMax_ifElse() {
    uint256 x;
    uint256 y;

    mathint expectedMax;

    if (x >= y) {
        expectedMax = x;
    } else {
        expectedMax = y;
    }
    
    mathint resultMax = max@withrevert(x, y);
    assert !lastReverted;
    
    assert resultMax == expectedMax;
}

rule max_returnMax_ternary() {
    uint256 x;
    uint256 y;

    mathint resultMax = max@withrevert(x, y);
    assert !lastReverted;
    
    uint256 expectedMax = x > y ? x : y;
    assert resultMax == expectedMax;
}

Ejecución del Prover: link

Sin embargo, en otro ejemplo, add(), también podemos usar una expresión ternaria, pero solo de forma selectiva. No podemos incluir todas las posibles rutas de ejecución, como se muestra a continuación:

Copy
/// CVL

rule add_sumWithOverflowRevert_ifElse() {
    uint256 x;
    uint256 y;

    mathint _sum = x + y;

    if (_sum <= max_uint256) {
        mathint result = add@withrevert(x, y);
        assert !lastReverted;
        assert result == _sum;
    } 
    else {
        add@withrevert(x, y);
        assert lastReverted; 
    }
}

rule add_sumWithOverflowRevert_ternary() {
    uint256 x;
    uint256 y;

    mathint _sum = x + y;
    mathint result = add@withrevert(x, y);

    assert _sum <= max_uint256 ? !lastReverted : lastReverted; // selective
}

Ejecución del Prover: link

La razón por la que no podemos tener en cuenta otras condiciones es que las expresiones de retorno en una operación ternaria deben ser del mismo tipo. Por lo tanto, hacer una aserción como esta: _sum <= max_uint256 ? _sum : lastReverted no es posible porque _sum es del tipo mathint, mientras que lastReverted es un booleano.

Por último, para mulDivUp(), tampoco podemos traducir esto directamente; tenemos que elegir las propiedades una por una y aplicar el ternario a cada una, de manera similar a lo que hicimos con add().

Resumen

• if/else es intuitivo debido a la familiaridad con otros lenguajes de programación.
• Demasiadas ramas condicionales ralentizan el Prover, pero la optimización puede mejorar la eficiencia.
• if/else requiere manejar todas las condiciones, lo que lo hace poco práctico para la verificación de casos aislados.
• El operador ternario proporciona una alternativa concisa, pero no funciona cuando los tipos de retorno difieren.

Ejercicios para el lector

1. Verifica formalmente que Solady min siempre devuelve el mínimo.
2. Verifica formalmente que Solady zeroFloorSub devuelve max(0, x - y). En otras palabras, si x es menor que y, devuelve 0. De lo contrario, devuelve x - y.

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