Introducción

El operador bicondicional nos permite afirmar relaciones si y solo si (if-and-only-if) entre valores booleanos. La implicación (P => Q) establece que si se satisface la condición P, entonces se observa Q. El bicondicional añade el requisito inverso: si se observa Q, entonces la condición P también debe satisfacerse. En otras palabras, P <=> Q es equivalente a afirmar tanto P => Q como Q => P.

NOTA: Se asume que el lector ya ha leído el capítulo “Operador de implicación”, ya que sienta las bases para este capítulo.

Función setX()

Comencemos con una función setter básica. Toma una entrada uint256 y actualiza la variable de almacenamiento x, pero solo si el nuevo valor es estrictamente mayor que el actual. Esta restricción se aplica mediante una declaración require, que revierte la transacción si no se cumple la condición:

Copy
/// Solidity

uint256 public x;

function setX(uint256 _x) external {
    require(_x > x, "x must be greater than the previous value");
    x = _x;
}

Para verificar formalmente esta función utilizando el operador de implicación, podemos expresar la relación entre el éxito de la transacción y el cambio de estado resultante como dos declaraciones de aserción de implicación:

Copy
rule setX_usingImplication() {
    uint256 _x;
    
    mathint xBefore = x();
    
    setX@withrevert(_x);
    bool success = !lastReverted;
    
    mathint xAfter = x();

    assert success => xAfter > xBefore; // If the call succeeds, then x increased (P => Q)
    assert xAfter > xBefore => success; // If x increased, then the call must have succeeded (Q => P)
}

Ejecución del Prover: link

Aunque es lógicamente correcto, escribir dos implicaciones unidireccionales (P => Q y Q => P) es innecesariamente verboso.

Bicondicional (<=>) en CVL

La intención aquí es expresar una regla precisa: “la transacción tiene éxito si y solo si el valor de entrada es mayor que el valor actual de x”.

Esto se puede escribir de forma más limpia como:

Copy
rule setX_TxSucceeds_iff_XIncreases() {
    uint256 _x;
    
    mathint xBefore = x();
    
    setX@withrevert(_x);
    bool success = !lastReverted;
    
    mathint xAfter = x();
    assert success <=> xAfter > xBefore;
}

Esta única declaración de aserción bicondicional es más concisa y expresa directamente la relación bidireccional entre el éxito de la llamada y el cambio en el estado x (incremento). En otras palabras, la función solo tiene éxito si x aumenta, y x solo aumenta si la llamada tiene éxito.

Como era de esperar, esta regla se verifica:

Ejecución del Prover: link

Implícitamente, también podemos razonar que: si la llamada falló, entonces x no aumentó:

Copy
assert !success <=> !(xAfter > xBefore);

o

Copy
assert !success <=> xAfter <= xBefore;

Esto ya está implícito en el bicondicional y no necesita escribirse por separado.

Verificación formal de mulDivUp() de Solmate

En el capítulo anterior (Operador de implicación), discutimos el comportamiento de la función mulDivUp() de Solmate, sus comprobaciones de desbordamiento (overflow) y su lógica de redondeo. Aquí hay un breve resumen:

• Revierte si denominator == 0 (división por cero) o si x * y > MAX_UINT256 (desbordamiento).
• mulDivUp(x, y, denominator) multiplica x e y, divide el resultado entre denominator, y redondea hacia arriba si hay un resto; de lo contrario, devuelve el cociente exacto.

Ahora vamos a verificar formalmente estos comportamientos utilizando el operador bicondicional.

Comportamiento de reversión

Comencemos con el comportamiento de reversión. Empezamos escribiendo la condición de reversión más simple, denominator == 0, y luego avanzamos hasta tener una regla completa.

Esto fallará, como sabemos, porque no captura todos los escenarios de reversión, pero sirve como un buen punto de partida:

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

    mulDivUp@withrevert(x, y, denominator);
    assert denominator == 0 <=> lastReverted;
}

La regla falla debido a un contraejemplo donde el producto de x e y excede max_uint256. Necesitamos incluir eso como una condición de reversión adicional:

Aquí está la regla CVL corregida:

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

    mulDivUp@withrevert(x, y, denominator);
    assert denominator == 0 || x * y > max_uint256 <=> lastReverted;
}

Ejecución del Prover: link

Ten en cuenta que el bicondicional es reversible (a diferencia de la implicación), por lo que podemos reescribir la aserción de esta manera:

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

    mulDivUp@withrevert(x, y, denominator);
    assert lastReverted <=> denominator == 0 || x * y > max_uint256;
}

Ejecución del Prover: link

Además, dado que un bicondicional es una implicación bidireccional combinada (P => Q y Q => P), ambos están unidos lógicamente; por lo tanto, las expresiones razonadas a través de <=> son inseparables.

Comportamiento de redondeo

La regla a continuación especifica el comportamiento de redondeo de la función mulDivUp(). Afirma que la función devuelve un valor redondeado hacia arriba si y solo si hay un resto presente. El operador bicondicional garantiza que el resto es la única condición que desencadena el redondeo hacia arriba y que ninguna otra condición puede afectar el valor de retorno:

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

Ejecución del Prover: link

La regla a continuación cubre el “otro” caso. Afirma que la función devuelve el cociente exacto si y solo si no hay resto. El operador bicondicional garantiza que la única razón para devolver un resultado sin redondear es la ausencia de un resto:

Copy
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

Cuándo usar el bicondicional en lugar de la implicación

Excluir la incertidumbre

La regla anterior, como vimos en el capítulo previo, se puede escribir utilizando => porque la propiedad que se está verificando da la casualidad de tener solo una condición que conduce al resultado. En tales casos, => se puede reemplazar con <=>. Este reemplazo es preferible porque <=> establece que nada más que la condición especificada puede causar el resultado. El operador de implicación no proporciona esta garantía, por lo que en casos como estos, es mejor usar el bicondicional para hacer explícita esa garantía.

En el ejemplo anterior (función max), tuvimos en cuenta todas las condiciones de reversión porque estábamos verificando la corrección de la función en su conjunto. Sin embargo, al tratar con una función que llama a varias funciones internas, cada una causando potencialmente diferentes condiciones de reversión, usar una implicación puede ser más práctico. Este enfoque se centra únicamente en la(s) condición(es) necesaria(s) para la reversión, sin tratar exhaustivamente cada posible escenario de fallo.

Verificar la dependencia mutua

La dependencia mutua ocurre cuando dos variables son interdependientes, lo que significa que un cambio en una desencadena un cambio correspondiente en la otra, y viceversa.

Tomemos como ejemplo un pool AMM WETH/USDC: Durante los swaps, el balance de WETH aumenta si y solo si el balance de USDC disminuye, y viceversa. Esto crea una dependencia bidireccional donde el balance de un token debe ajustarse en respuesta a los cambios en el otro, lo que indica que ningún balance puede cambiar de forma independiente.

Resumen

• El bicondicional (<=>) garantiza explícitamente la implicación en ambas direcciones. Si se satisface la condición P, se cumple Q, y si se cumple Q, la condición P también debe satisfacerse.
• El operador de implicación (=>) funciona cuando una o más condiciones conducen a un resultado, pero no garantiza que el resultado solo pueda ser causado por esa condición.
• Usar el bicondicional puede ser poco práctico cuando hay muchas condiciones potenciales que resultan en el desenlace.

Ejercicios para el lector

1. Verifica formalmente que Solady min siempre devuelve el min.
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 utilizando el Certora Prover