Introducción

El operador de implicación se utiliza frecuentemente como sustituto de la declaración if, ya que es más limpio.

Consideremos el siguiente ejemplo: una función mod(x, y) que toma dos enteros sin signo como parámetros y devuelve x módulo y. La operación módulo calcula el resto de dividir x por y.

La implementación en Solidity de esta función es la siguiente:

Copy
/// Solidity

function mod(uint256 x, uint256 y) external pure returns (uint256) {
    return x % y;
}

Supongamos que queremos verificar formalmente la propiedad: “si x < y, entonces el módulo debe ser igual a x.” El uso de una declaración if para expresar esto en CVL causa un error de compilación, ya que la declaración final en una regla debe ser un assert o un satisfy:

Copy
/// this rule will not compile
rule mod_ifXLessThanY_resultIsX_usingIf() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);

    if (x < y) {
        assert result == x;
    }
}

Copy
ERROR
: Failed to run Certora Prover locally. Please check the errors below for problems in the specifications (.spec files) or the prover_args defined in the .conf file.

CRITICAL
: [main] ERROR ALWAYS - Found errors in certora/specs/ImplicationOperator.spec:

CRITICAL
: [main] ERROR ALWAYS - Error in spec file (ImplicationOperator.spec:15:5): last statement of the rule mod_ifXLessThanY_resultIsX_usingIf is not an assert or satisfy command (but must be)

Para resolver esto, una solución alternativa es añadir una aserción trivial al final:

Copy
if (P) { 
	assert Q; 
}
assert true;

Copy
rule mod_ifXLessThanY_resultIsX_usingIf() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);

    if (x < y) {
    assert result == x;
    }
    assert true; // trivially TRUE
}

Sin embargo, esta solución introduce una aserción sin sentido que satura la especificación. Otra solución alternativa es utilizar una declaración if-else, donde la rama else ejecuta aserciones significativas:

Copy
if (P) { 
	assert Q; 
} else {
	assert (something_else);
}

Copy
rule mod_ifXLessThanY_resultIsX_usingIfElse() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);

    if (x < y) {
    assert result == x;
    } else {
    assert result != x;
    }
}

Sin embargo, originalmente no estábamos interesados en afirmar que: “si x >= y, entonces result != x.” En muchos casos, como el que se muestra arriba, no estamos interesados en crear una aserción para cada rama posible.

Implicación (=>) en CVL

Para manejar esto de manera elegante, utilizamos el operador de implicación (=>). Con la implicación, podemos expresar condiciones de manera sucinta evitando la complejidad del flujo de control de las declaraciones if-else.

Por lo tanto, en lugar de escribir if (P) assert Q (que no compila), podemos utilizar de manera equivalente assert P => Q:

Copy
rule mod_ifXLessThanY_thenResultIsX() {
    uint256 x;
    uint256 y;

    mathint result = mod(x, y);
    assert x < y => result == x;
}

Ejecución del Prover: link

La forma P => Q se lee como “Si P, entonces Q”, o simplemente, “P implica Q”. Ten en cuenta que Q => P no es necesariamente equivalente, como veremos en la siguiente sección.

P Implica Q P => Q

Tomemos otro ejemplo: la función max optimizada para gas de Solady. Como se discutió en el capítulo anterior, esta devuelve la mayor de dos entradas, x e y, tomando x por defecto si son iguales.

A continuación se muestra la implementación, y al igual que en el capítulo anterior, hemos cambiado la visibilidad de internal a external para evitar la necesidad de crear un arnés (harnessing) (lo cual está fuera del alcance de este capítulo):

Copy
/// Solidity

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

Vamos a verificar ahora formalmente la siguiente propiedad: “si x es mayor que y, el valor de retorno de max(x, y) debe ser x.” Podemos expresar esto en CVL como:

Copy
rule max_ifXGreaterThanY_resultX() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x > y => result == x;
}

En esta regla, la condición (x > y) y el resultado esperado (result == x) forman la implicación P => Q. Como era de esperar, la propiedad está VERIFICADA.

Ejecución del Prover: link

Nota: La verificación de la función max aún no está completa. Lo cubriremos en la siguiente sección.

P => Q no es equivalente a Q => P

Ahora consideremos la implicación inversa: “si el valor de retorno de max(x, y) es x, entonces x > y” o result == x => x > y. Esto puede parecer válido al principio; sin embargo, cuando x == y, la función sigue devolviendo x. Esto contradice la aserción de que x > y, haciendo que la implicación sea falsa en ese caso.

Aquí está la regla que falla:

Copy
rule max_ifResultIsX_thenXGreaterThanY() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result == x => x > y;
}

Contraejemplo

Cuando se viola una regla, el Prover muestra un contraejemplo. En este caso, result == x no solo ocurre cuando x > y — también ocurre cuando x == y. El contraejemplo muestra específicamente x = 3 e y = 3:

Para solucionar esto, necesitamos revisar la condición para incluir todos los casos en los que result == x es válido: tanto cuando x > y como cuando x == y.

Aquí está la regla revisada, donde || es el operador OR:

Copy
rule max_ifResultIsX_thenXGreaterOrEqualToY() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result == x => x > y || x == y;
}

o, de manera más simple:

Copy
rule max_ifResultIsX_thenXGreaterOrEqualToY_simplified() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result == x => x >= y;
}

Y ahora está VERIFICADA:

Ejecución del Prover: link

Ahora, para completar la verificación, también verificaremos la propiedad de que max(x, y) devuelve y cuando y es mayor o igual a x. Aquí está la regla:

Copy
rule max_ifResultIsY_thenYGreaterOrEqualToX() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result == y => y >= x;
}

Como se esperaba, está VERIFICADA:

Ejecución del Prover: link

P => Q es equivalente a !Q => !P

Reescribir una implicación P => Q en su forma contrapositiva !Q => !P sugiere una forma alternativa de pensar sobre una especificación.

Revisemos nuestra regla anterior con la aserción: x > y => result == x:

Copy
rule max_ifXGreaterThanY_resultX() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x > y => result == x;
}

En su forma original, esta regla se ocupa de lo que ocurre cuando x es mayor que y, que es que el valor de retorno de max(x, y) es x.

En la forma contrapositiva, assert !(result == x) => !(x > y), en cambio nos preocupamos por lo que sucede si el valor de retorno de max(x, y) no es x. En ese caso, esperamos que x no sea mayor que y (o simplemente, x <= y):

Copy
rule max_ifResultNotX_thenXNotGreaterThanY() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert result != x => x <= y;
}

Ejecución del Prover: link

Ambas formas expresan la misma verdad lógica, pero desde diferentes perspectivas.

Para entender mejor esto, usemos una analogía común:

• “Si llovió, el suelo está mojado,” o
• hasRained => isGroundWet

Su contrapositiva es:

• “Si el suelo no está mojado, entonces definitivamente no llovió,” o
• !isGroundWet => !hasRained

Sin embargo, el hecho de que no haya llovido no garantiza que el suelo no esté mojado. Alguien podría haber derramado agua sobre él. Por lo tanto, !hasRained => !isGroundWet no es lógicamente válido.

Verdad Vacua y Tautología en la Implicación

Ahora que entendemos cómo funciona la implicación, también debemos ser cautelosos al escribir estas declaraciones. Podríamos escribir sin saberlo implicaciones con garantías falsas, un tema que exploraremos a continuación.

Cuando P es siempre FALSE, P => Q es TRUE independientemente de Q (vacuo)

Una implicación se vuelve vacuamente verdadera cuando la condición (P) es inalcanzable (siempre falsa), lo que significa que no hay un estado posible donde P se cumpla. En tales casos, toda la declaración P => Q se considera automáticamente verdadera, independientemente de cuál sea el resultado (Q).

Esto sucede porque si P nunca puede ser verdadera, entonces no hay ninguna instancia en la que la implicación pueda ser violada. Por lo tanto, no existe contraejemplo.

Usemos este ejemplo: “si x < 0, entonces result == y.” Dado que x es un uint256, nunca puede ser negativo. Eso hace que x < 0 sea un estado inalcanzable. Sin importar lo que afirmemos en el lado derecho (Q), la implicación siempre se verificará.

Aquí está la regla vacua en CVL:

Copy
rule max_unreachableCondition_vacuouslyTrue() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x < 0 => result == y;
}

Esta regla está VERIFICADA, pero no porque x < 0 lleve a result == y. Se verifica solo porque x < 0 es inalcanzable en cualquier ruta de ejecución válida, haciendo que la implicación sea vacuamente verdadera. Confirma que no existe ningún contraejemplo porque la condición nunca puede ocurrir:

Ejecución del Prover: link

Dado que la condición (P) nunca puede ocurrir, el resultado (Q) puede ser cualquier cosa — incluso algo sin sentido como 1 == 2, como se muestra a continuación:

Copy
rule max_unreachableCondition_vacuouslyTrueObvious() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x < 0 => 1 == 2;
}

Ejecución del Prover: link

Cuando Q es siempre TRUE_,_ P => Q es TRUE independientemente de P (tautología)

Una implicación se vuelve tautológicamente verdadera cuando el resultado (Q) es siempre verdadero, independientemente de la condición (P). En tales casos, toda la declaración P => Q se considera automáticamente verdadera, incluso si la condición es irrelevante o engañosa.

Esto sucede porque si Q es siempre verdadera, el resultado está garantizado; por lo tanto, la implicación nunca puede ser falsa.

Usemos este ejemplo: “si x > y, entonces result >= 0.”

A primera vista, esto parece implicar que x > y garantiza un resultado no negativo. Pero result es un uint256, que siempre es mayor o igual a cero por su tipo. Así que la expresión result >= 0 es siempre verdadera.

Aquí está la regla tautológica en CVL:

Copy
rule max_outcomeIsAlwaysTrue_tautology() {
    uint256 x;
    uint256 y;

    mathint result = max(x, y);
    assert x > y => result >= 0;
}

Esta regla está VERIFICADA, no porque x > y lleve a result >= 0, sino porque result >= 0 es siempre verdadera por su tipo, haciendo que la implicación sea tautológicamente verdadera:

Ejecución del Prover: link

Verificando Formalmente mulDivUp() de Solmate

Ahora que conocemos los fundamentos, vamos a verificar formalmente mulDivUp() de Solmate utilizando el operador de implicación. Como su nombre indica, esta función multiplica dos enteros sin signo, divide el resultado por otro entero sin signo y redondea hacia arriba si hay un resto. Si no hay resto, simplemente devuelve el cociente.

Las propiedades que verificaremos formalmente se dividen en dos categorías: comportamiento de redondeo y comportamiento de reversión (revert). Pero antes de hacer eso, haremos un pequeño ajuste al código original de mulDivUp().

La función mulDivUp() de Solmate tiene una visibilidad internal, y la cambiaremos a external por conveniencia. De lo contrario, sería necesario configurar un contrato de arnés (harnessing), lo cual está fuera del alcance de este capítulo y puede introducir una carga mental innecesaria en este punto.

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

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 en assembly está fuera del alcance de este capítulo. Sin embargo, los comentarios nos ayudan a entender qué hace el código.

Estas 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)
}

como sugiere el comentario, representan una declaración require que impone las siguientes condiciones:

• denominator != 0, lo cual previene la división por cero, ya que la división por cero no está permitida.
• y == 0 || x <= type(uint256).max / y, lo que significa:
  • Si y == 0, la condición se cumple porque x * y naturalmente se evalúa a 0. En este caso, no es necesario realizar una comprobación de desbordamiento (overflow).
  • De lo contrario, si y != 0, x debe ser menor o igual a type(uint256).max / y asegurándose de que x * y no exceda type(uint256).max, previniendo el desbordamiento.

Ahora concluimos que las propiedades a verificar formalmente son las siguientes:

• Si denominator == 0, entonces la función revierte.
• Si x * y > MAX_UINT256, entonces la función revierte.

En la siguiente línea,

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))

como sugiere el comentario, la función maneja el redondeo de la siguiente manera:

• Si x * y % denominator > 0, se suma 1 a x * y / denominator para compensar el truncamiento de Solidity en la división de enteros. Dado que Solidity redondea hacia abajo, sumar 1 efectivamente redondea el valor hacia arriba.
• Si x * y % denominator == 0, no se necesita un ajuste de redondeo, y el resultado se devuelve tal cual.

Ahora concluimos que las propiedades a verificar formalmente son las siguientes:

• Si x * y % denominator > 0, entonces el resultado es x * y / denominator + 1.
• Si x * y % denominator == 0, entonces el resultado es x * y / denominator.

Dado que ahora entendemos cómo funciona la función y qué propiedades verificar formalmente, podemos proceder a escribir las reglas. Empecemos con las reglas para el comportamiento de redondeo.

Comportamiento de Redondeo

A continuación se muestra la especificación de la regla en CVL para la propiedad del comportamiento de redondeo.

La aserción de la regla mulDivUp_roundUp() establece que cuando el producto de x e y se divide por el denominator y tiene un resto, el resultado se incrementa en 1.

De manera similar, la aserción en la regla mulDivUp_noRoundUp() establece que cuando el producto de x e y se divide por el denominator y no tiene resto, el resultado se devuelve tal cual.

Como se esperaba, estas reglas están VERIFICADAS:

Copy
rule mulDivUp_roundUp() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mathint result = mulDivUp(x, y, denominator);
    assert ((x * y) % denominator > 0) => (result == (x * y / denominator) + 1); 
}

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

    mathint result = mulDivUp(x, y, denominator);
    assert ((x * y) % denominator == 0) => (result == x * y / denominator);
}

Ejecución del Prover: link

Ahora, pasemos a la siguiente categoría de propiedades para esta función: comportamiento de reversión (revert).

Comportamiento de Reversión (Revert)

Como se discutió anteriormente, hay dos casos en los que mulDivUp() revierte:

• Si denominator == 0
• Si x * y > MAX_UINT256

Al verificar formalmente los reverts, debemos incluir la etiqueta @withrevert al invocar las funciones. Por defecto, el Prover solo ejecuta las rutas que no revierten, lo que significa que todos los argumentos pasados a mulDivUp(x, y, denominator) no revierten. Sin embargo, añadir @withrevert a la función indica al Prover que también considere los argumentos que causan un revert. Esto nos permite tener en cuenta los casos de reversión en nuestras declaraciones de implicación.

A continuación se muestra la especificación de la regla en CVL:

Copy
rule mulDivUp_ifDenominatorIsZero_revert() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert (denominator == 0) => isReverted;
}

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

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert (x * y > max_uint256) => isReverted;
}

Como se esperaba, estas reglas están VERIFICADAS:

Ejecución del Prover: link

Hay un enfoque aún más interesante para esto. Hasta ahora, hemos usado la construcción P => Q, lo que significa que la condición (P) resulta en el resultado (Q). Pero si lo invertimos a Q => P, significa que el resultado (Q) se deriva de las condiciones (P); por lo tanto, debemos considerar todos los casos posibles de P que conducen a Q.

A continuación se muestra la implementación donde, en la primera regla, omitimos intencionalmente un caso de revert, mientras que, en la segunda regla, tomamos en cuenta todos los casos. Como resultado, la primera regla resulta en una VIOLATION (violación), mientras que la segunda regla está VERIFICADA:

Copy
rule mulDivUp_allRevertCases_violated() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert isReverted => (denominator == 0);
}

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

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert isReverted => (denominator == 0 || x * y > max_uint256);
}

Ejecución del Prover: link

En la siguiente subsección, verificaremos formalmente las rutas que no revierten (non-reverts), un paso opcional ya que hemos cubierto todos los casos de revert. Sin embargo, aún lo haremos ya que puede tener casos de uso futuros.

Comportamiento de No Reversión (Opcional)

Si podemos verificar formalmente las rutas que revierten, también podemos verificar las que no revierten. Para hacerlo, necesitamos replantear las declaraciones como:

• denominator != 0
• x * y <= MAX_UINT256

y combinarlas como se muestra en la implementación de la regla de CVL a continuación:

Copy
rule mulDivUp_noRevert() {
    uint256 x;
    uint256 y;
    uint256 denominator;

    mulDivUp@withrevert(x, y, denominator);
    bool isReverted = lastReverted;

    assert ((denominator != 0) && (x * y <= max_uint256)) => !isReverted;
}

Como se esperaba, la regla está VERIFICADA:

Ejecución del Prover: link

Resumen

• Una declaración de implicación consiste en una condición P, un resultado Q y el operador de implicación (=>).
• El operador de implicación define una relación condicional unidireccional, lo que significa que P => Q no implica Q => P.
• P => Q y su contrapositiva !Q => !P son lógicamente equivalentes pero ofrecen diferentes perspectivas, desplazando el enfoque de cuándo se cumple la condición a cuándo no.
• Para que una implicación sea significativa (ni vacua ni tautológica), Q (el resultado) debe depender de que P (la condición) sea verdadera.
• Una verdad vacua ocurre cuando P es inalcanzable (siempre falsa), haciendo que P => Q sea verdadera independientemente de Q debido a la falta de contraejemplos.
• Una tautología ocurre cuando Q es siempre verdadera, haciendo que P => Q sea verdadera independientemente de P.
• Las verdades vacuas y las tautologías crean una falsa sensación de seguridad en la verificación formal.

Ejercicios para el lector

1. Verifica formalmente que min de Solady siempre devuelve el mínimo.
2. Verifica formalmente que zeroFloorSub de Solady 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 utilizando el Certora Prover