Introducción

ETH, ampliamente utilizado en DeFi para intercambios, provisión de liquidez, staking y garantías, necesita una versión compatible con ERC-20 para que los protocolos puedan interactuar con él a través de la misma interfaz estandarizada que se utiliza para otros tokens.

Esto dio lugar a Wrapped ETH (WETH), cuyo principio es sencillo: depositar ETH nativo acuña una cantidad equivalente de WETH en la cuenta del usuario, mientras que retirar quema el WETH correspondiente y devuelve el ETH nativo a la cuenta del usuario.

En el capítulo anterior, verificamos formalmente las propiedades esenciales de un contrato ERC-20 típico. Dado que WETH es en sí mismo un ERC-20, no repetiremos esas especificaciones aquí y nos centraremos únicamente en las funcionalidades específicas de WETH. Verificaremos formalmente la implementación de Solady WETH, que utiliza ensamblador en línea (inline assembly) para la optimización de gas.

Propiedades de WETH a verificar formalmente

Cuando un usuario deposita ETH, debe recibir una cantidad equivalente de WETH. Cuando retira, debe poder canjear ese WETH por una cantidad igual de ETH en cualquier momento.

Estos dos comportamientos definen las garantías centrales del contrato WETH más allá de las funcionalidades estándar de ERC-20. Para mantenerlas, el contrato debe satisfacer dos invariantes clave:

1. El ETH que posee el contrato debe ser siempre mayor o igual al suministro total (total supply) de WETH. Esto garantiza que todos los titulares de WETH puedan canjear sus tokens por ETH en cualquier momento, independientemente del orden o el momento del canje.
2. El suministro total de WETH debe ser siempre mayor o igual a la suma de todos los saldos de WETH. Esto garantiza que el contrato no pueda distribuir más tokens de los que ha acuñado.

Sin embargo, no verificaremos formalmente el segundo invariante porque el contrato Solady WETH hereda una implementación de ERC-20 que no utiliza un mapping para los saldos de las cuentas. En su lugar, lee y escribe en el almacenamiento (storage) utilizando un slot calculado para cada cuenta.

Por lo tanto, verificar este invariante requiere la «summarization» (resumen) de CVL: necesitaríamos resumir las funciones que modifican el almacenamiento del saldo de las cuentas, reflejarlas usando un ghost mapping, y razonar sobre el invariante a través de ese estado ghost. Este tema va más allá del alcance de este capítulo. Para más información, consulte la documentación de Certora sobre summarization.

En lugar de verificar este invariante, verificamos formalmente otro: el saldo de ninguna cuenta excede el suministro total. Puede parecer trivial, pero resulta útil más adelante cuando las reglas de depósito y retiro dependen de precondiciones relacionadas con el saldo. Este invariante nos permite reemplazar esas suposiciones usando requireInvariant, lo cual proporciona garantías de que esas precondiciones que asumimos son de hecho válidas.

El ETH depositado es igual al WETH recibido

Cuando un usuario deposita ETH en el contrato usando la función deposit(), su saldo de WETH aumenta y su saldo de ETH disminuye en la misma cantidad. Para verificar formalmente este comportamiento en CVL, procedemos de la siguiente manera:

1. Establecer las precondiciones:
   • El remitente no debe ser el propio contrato (e.msg.sender != currentContract) porque las autollamadas (self-calls) rompen la contabilidad del saldo de ETH, y ninguna ruta de ejecución permite tales llamadas.
   • El saldo de WETH del remitente más la cantidad depositada no debe desbordarse (balanceOf(e.msg.sender) + e.msg.value <= max_uint256).
2. Registrar los saldos de ETH y WETH del usuario antes de invocar deposit().
3. Invocar deposit() con la cantidad de ETH en e.msg.value.
4. Registrar los saldos de ETH y WETH del usuario después de invocar deposit().
5. Afirmar (assert) las condiciones de corrección:
   • El saldo final de ETH es igual al saldo inicial de ETH menos la cantidad depositada.
   • El saldo final de WETH es igual al saldo inicial de WETH más la cantidad depositada.

Aquí está la implementación de la regla en CVL:

Copy
rule deposit_ethDepositedEqualsWethReceived(env e) {
    require e.msg.sender != currentContract;
    require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // will be replaced by an invariant

    mathint ethBalanceBefore = nativeBalances[e.msg.sender];
    mathint wethBalanceBefore = balanceOf(e.msg.sender);
    
    deposit(e);

    mathint ethBalanceAfter = nativeBalances[e.msg.sender];
    mathint wethBalanceAfter = balanceOf(e.msg.sender);

    assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
    assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}

Ahora vamos a desglosarlo.

Precondiciones

La primera precondición instruye al Prover a excluir los casos donde el llamador (msg.sender) es el propio contrato:

Copy
require e.msg.sender != currentContract;

Sin esta precondición, el Prover asume que el llamador puede ser el currentContract, lo que hace que la regla falle. Por ejemplo, si el contrato fuera a depositar 1 ETH en sí mismo, no habría ningún cambio neto en sus tenencias de ETH (ya que se envía y recibe la misma cantidad a sí mismo). Sin embargo, el contrato seguiría acuñando 1 WETH, causando que la aserción ethBalanceAfter == ethBalanceBefore - e.msg.value (amount deposited``) falle.

La segunda precondición, require balanceOf(e.msg.sender) + e.msg.value <= max_uint256, descarta la posibilidad de un desbordamiento al sumar el saldo inicial de WETH del llamador y el depósito de ETH.

Dado que las declaraciones require son suposiciones que el Prover no verifica —simplemente las da por hecho— necesitamos probar esto formalmente como un invariante en una sección posterior. Una vez probado, podemos reemplazar esta precondición asumida con el invariante verificado usando requireInvariant.

Registrar los saldos de ETH y WETH del usuario antes y después de la llamada a deposit()

Una vez establecidas todas las precondiciones, debemos registrar los saldos de ETH y WETH del llamador antes y después de invocar deposit(). Estos valores registrados se utilizarán en las aserciones para razonar sobre los cambios de saldo:

Copy
mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender);

deposit(e);

mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);

Aserciones

La primera aserción comprueba que el saldo de ETH del llamador disminuyó exactamente en la cantidad de ETH enviada con la transacción. La segunda aserción comprueba que el saldo de WETH del llamador aumentó exactamente en la cantidad de ETH depositada:

Copy
assert ethBalanceAfter == ethBalanceBefore - e.msg.value; // ETH is deposited -- ETH balance decreases
assert wethBalanceAfter == wethBalanceBefore + e.msg.value; // WETH is received -- WETH balance increases

Aquí está la ejecución verificada del Prover para la regla deposit_ethDepositedEqualsWethReceived.

El depósito de ETH aumenta el suministro total de WETH

Además de cambiar los saldos, otro efecto esperado de una llamada a deposit() es un aumento en el totalSupply de WETH. La siguiente regla en CVL captura este comportamiento:

Copy
rule deposit_ethDepositIncreasesWETHTotalSupply(env e) {
    mathint totalSupplyBefore = totalSupply();
    
    deposit(e);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter == totalSupplyBefore + e.msg.value;
}

Las variables totalSupplyBefore y totalSupplyAfter registran los valores del suministro total antes y después de la llamada a deposit() para verificar el cambio esperado en la aserción.

Dado que la función deposit() llama internamente a _mint(), el suministro total de WETH aumenta en la cantidad depositada, tal como se refleja en la aserción:

Copy
assert totalSupplyAfter == totalSupplyBefore + e.msg.value;

Note que no hay una precondición require msg.sender != currentContract porque la aserción concierne únicamente al aumento del suministro. El suministro aumenta por la cantidad de ETH depositada (msg.value) independientemente de quién sea el remitente.

Aquí está la ejecución verificada del Prover para la regla deposit_ethDepositIncreasesWETHTotalSupply.

Verificación de las causas de reversión (revert) en deposit()

Vamos ahora a verificar la ruta de reversión (revert) de la función deposit(). Queremos detectar casos en los que se revierte inesperadamente o no se revierte cuando debería hacerlo.

Para verificar formalmente este comportamiento en CVL, procedemos de la siguiente manera:

1. Establecer una precondición de que el saldo de WETH del llamador más la cantidad depositada no debe desbordarse (balanceOf(caller) + ethDeposit <= max_uint256).
2. Registrar el totalSupply de WETH y el saldo de ETH del llamador antes de invocar deposit().
3. Invocar deposit() con la etiqueta @withrevert para permitir que la regla observe las reversiones.
4. Usar lastReverted, que devuelve un booleano indicando si la última llamada se revirtió.
5. Afirmar que la función se revierte si y solo si (<=>) se cumple alguna de las siguientes condiciones:
   • El saldo de ETH del llamador antes de la llamada es menor que la cantidad del depósito (e.msg.value).
   • El suministro total de WETH antes de la llamada más la cantidad del depósito excede max_uint256.

Aquí está la regla en CVL:

Copy
rule deposit_revert(env e) {
    address caller = e.msg.sender;
    uint256 ethDeposit = e.msg.value;

    require balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant
    
    mathint totalSupplyBefore = totalSupply();
    mathint ethBalanceBefore = nativeBalances[caller];

    deposit@withrevert(e);
    bool isLastReverted = lastReverted;
    
    assert isLastReverted <=> (
        ethBalanceBefore < ethDeposit || 
        totalSupplyBefore + ethDeposit > max_uint256
    );
}

Vamos a desglosar aún más la regla.

Para facilitar la lectura, asignamos e.msg.sender y e.msg.value a caller y ethDeposit, respectivamente:

Copy
address caller = e.msg.sender;
uint256 ethDeposit = e.msg.value;

La precondición, mostrada a continuación, también apareció en la regla anterior deposit_ethDepositedEqualsWethReceived():

Copy
require balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant

Su reaparición aquí como una precondición, en lugar de como parte de las condiciones de reversión, refuerza aún más la necesidad de verificarla formalmente.

A continuación, registramos los valores de totalSupplyBefore (suministro total de WETH) y los nativeBalances del llamador antes de invocar la función deposit():

Copy
mathint totalSupplyBefore = totalSupply();
mathint ethBalanceBefore = nativeBalances[caller];

Ahora, invocamos la función deposit() con la etiqueta @withrevert y registramos si la llamada se revirtió:

Copy
deposit@withrevert(e);
bool isLastReverted = lastReverted;

Finalmente, la aserción utiliza el operador bicondicional (<=>) y enumera todos los casos de reversión de forma disyuntiva (usando OR):

• La función se revierte cuando el saldo de ETH del llamador antes (ethBalanceBefore) es menor que el depósito de ETH (e.msg.value).

  Esto significa que el llamador no tiene suficiente ETH para hacer el depósito.

• La función también se revierte cuando el suministro total de WETH (totalSupplyBefore) más el depósito de ETH excedería max_uint256.

  Dado que cada depósito acuña una cantidad igual de WETH, superar el límite de uint256 resultaría en un desbordamiento.

Copy
assert isLastReverted <=> (
    ethBalanceBefore < ethDeposit || // the caller doesn't have enough eth to deposit
    totalSupplyBefore + ethDeposit > max_uint256 // results in overflow
);

La precondición msg.sender != currentContract es innecesaria porque las condiciones de reversión se refieren a saldo insuficiente y desbordamiento, los cuales son independientes de la identidad del llamador.

Aquí está la ejecución verificada del Prover para la regla deposit_revert.

El ETH retirado es igual al WETH reducido

Cuando un usuario retira ETH del contrato, su saldo de ETH aumenta y su saldo de WETH disminuye en la misma cantidad. La siguiente regla en CVL captura este comportamiento:

Copy
rule withdraw_ethWithdrawnEqualsWETHReduced(env e) {
    uint256 amount;

    require e.msg.sender != currentContract;

    mathint ethBalanceBefore = nativeBalances[e.msg.sender];
    mathint wethBalanceBefore = balanceOf(e.msg.sender); 

    withdraw(e,amount);

    mathint ethBalanceAfter = nativeBalances[e.msg.sender];
    mathint wethBalanceAfter = balanceOf(e.msg.sender);

    assert ethBalanceAfter == ethBalanceBefore + amount;
    assert wethBalanceAfter == wethBalanceBefore - amount;
}

Esto sigue la misma estructura que rule deposit_ethDepositedEqualsWethReceived(). A estas alturas, el patrón debería resultar familiar:

• Establecer precondiciones
• Registrar los saldos de ETH y WETH del llamador antes de invocar withdraw()
• Invocar withdraw()
• Registrar los saldos de ETH y WETH del llamador después

Copy
require e.msg.sender != currentContract;

mathint ethBalanceBefore = nativeBalances[e.msg.sender];
mathint wethBalanceBefore = balanceOf(e.msg.sender); 

withdraw(e,amount);

mathint ethBalanceAfter = nativeBalances[e.msg.sender];
mathint wethBalanceAfter = balanceOf(e.msg.sender);

Ahora, vayamos directamente a la aserción.

En las aserciones a continuación, verificamos que el saldo de ETH aumenta y el saldo de WETH disminuye en la misma amount retirada:

Copy
assert ethBalanceAfter == ethBalanceBefore + amount;
assert wethBalanceAfter == wethBalanceBefore - amount;

La precondición require msg.sender != currentContract es necesaria porque una autollamada no produciría ningún cambio en el saldo de ETH del contrato (depositarse a sí mismo no produce ningún cambio neto), lo que hace que la aserción ethBalanceAfter == ethBalanceBefore + amount falle (un falso positivo).

Aquí está la ejecución verificada del Prover para la regla withdraw_ethWithdrawnEqualsWETHReduced.

El ETH retirado disminuye el suministro total de WETH

Cuando un usuario retira ETH, la cantidad correspondiente de WETH se quema (is burned), lo que reduce el suministro total. Este es un efecto esperado de la función withdraw(). La siguiente regla en CVL captura este comportamiento:

Copy
rule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
    uint256 amount;
    
	require balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant
    mathint totalSupplyBefore = totalSupply();
    
    withdraw(e, amount);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Dado que el retiro reduce el suministro total por la cantidad retirada (que equivale al saldo quemado), la siguiente precondición asegura que la resta del totalSupply no pueda sufrir un desbordamiento negativo (underflow) al requerir que ningún saldo individual exceda el suministro total:

Copy
require balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant

Al igual que con la regla anterior, esta precondición representa una suposición que debe verificarse formalmente más adelante.

A continuación, seguimos un patrón familiar, donde registramos el suministro total de WETH antes y después de la llamada a withdraw:

Copy
mathint totalSupplyBefore = totalSupply();
    
withdraw(e, amount);
mathint totalSupplyAfter = totalSupply();

Luego afirmamos que el totalSupply de WETH se reduce en la cantidad esperada:

Copy
assert totalSupplyAfter == totalSupplyBefore - amount;

La precondición require e.msg.sender != currentContract es innecesaria aquí porque la disminución del suministro (o el cambio del suministro) es independiente de quién sea el llamador.

Esta regla confirma que la quema de WETH durante el retiro disminuye correctamente el suministro total. Aquí está la ejecución verificada del Prover.

Verificación de las causas de reversión en withdraw()

La regla withdraw_revert sigue un patrón diferente a la regla deposit_revert. Para entender por qué, primero echemos un vistazo a la función withdraw:

Copy
/// @dev Burns `amount` WETH of the caller and sends `amount` ETH to the caller.
function withdraw(uint256 amount) public virtual {
    _burn(msg.sender, amount);
    /// @solidity memory-safe-assembly
    assembly {
        // Transfer the ETH and check if it succeeded or not.
        if iszero(call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)) {
            mstore(0x00, 0xb12d13eb) // `ETHTransferFailed()`.
            revert(0x1c, 0x04)
        }
    }
}

Además de la función _burn(), que implementa sus propias condiciones de reversión, la función withdraw() incluye código en ensamblador que comprueba si la transferencia de ETH tuvo éxito:

Copy
assembly {
    // Transfer the ETH and check whether it succeeded.
    if iszero(call(gas(), caller(), amount, codesize(), 0x00, codesize(), 0x00)) {
        mstore(0x00, 0xb12d13eb) // `ETHTransferFailed()`.
        revert(0x1c, 0x04)
    }
}

La expresión iszero devuelve verdadero (true) si la transferencia de ETH falla, lo que desencadena una reversión. De lo contrario, devuelve false, lo que significa que la transferencia de ETH tuvo éxito. Para verificar este comportamiento en ensamblador, utilizamos un hook de CVL (CALL) para observar si la llamada de transferencia de ETH de bajo nivel se revierte como se espera.

Aquí está la regla en CVL que verifica todas las condiciones de reversión de withdraw(), incluyendo la falla de la llamada de bajo nivel:

Copy
persistent ghost bool g_lowLevelCallFail;


hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {    

    if (rc == 0) {
        g_lowLevelCallFail = true; 
    } else {
        g_lowLevelCallFail = false; 
    }
}

rule withdraw_revert(env e) {
    uint256 amount; // the amount of eth to claim    
    
    mathint wethBalanceBefore = balanceOf(e.msg.sender); 

    withdraw@withrevert(e, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        amount > wethBalanceBefore ||
        e.msg.value != 0 ||
        g_lowLevelCallFail
    );
}

Expliquemos la regla anterior.

La línea a continuación es la declaración de la variable persistent ghost:

Copy
persistent ghost bool g_lowLevelCallFail;

Nota: Consulte el capítulo separado “Using Persistent Ghosts” para ver la discusión sobre la diferencia entre un ghost normal y un persistent ghost.

La variable ghost es actualizada por el hook CALL. El hook se activa cuando se invoca el método withdraw(), específicamente mediante la llamada de bajo nivel que transfiere ETH al llamador. Si la llamada de bajo nivel falla (rc == 0), la variable ghost g_lowLevelCallFail se establece en true; si la llamada tiene éxito (rc != 0), se establece en false, como se muestra en el hook CALL a continuación:

Copy
hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {    
    if (rc == 0) {
        g_lowLevelCallFail = true; 
    } else {
        g_lowLevelCallFail = false; 
    }
}

Esto le da al Prover una forma de rastrear el éxito/fracaso de la transferencia de ETH dentro de los bloques de ensamblador.

Ahora vayamos a la regla.

Como de costumbre, registramos el saldo antes de llamar a la función withdraw():

Copy
mathint wethBalanceBefore = balanceOf(e.msg.sender);

Luego invocamos la función withdraw() con la etiqueta @withrevert y registramos si la llamada se revirtió:

Copy
withdraw@withrevert(e, amount);
bool isLastReverted = lastReverted;

En la aserción a continuación, la función se revertirá si y solo si (<=>) se cumple una de las siguientes condiciones:

• La amount de retiro excede el saldo de WETH del llamador (wethBalanceBefore)

  Esto significa que el llamador está intentando retirar más ETH de lo que su saldo de WETH permite.

• Se envió ETH junto con la llamada

  Esto no está permitido porque withdraw no es una función payable.

• La transferencia de ETH de vuelta al llamador falló

  Esta condición se rastrea a través del resultado de la CALL de bajo nivel usando la variable ghost g_lowLevelCallFail.

Copy
assert isLastReverted <=> (
    amount > wethBalanceBefore ||   // insufficient balance: withdrawal amount exceeds weth balance
    e.msg.value != 0 ||             // non-payable: ETH was sent to a non-payable function
    g_lowLevelCallFail              // transfer failure: low-level call ETH transfer failed
);

Aquí está la ejecución verificada del Prover para la regla withdraw_revert.

Invariante: Los depósitos totales de ETH son mayores o iguales al suministro total de WETH (solvencia)

Para que los usuarios canjeen con éxito ETH usando su WETH, el ETH mantenido por el contrato debe ser siempre mayor o igual al suministro total de WETH. Aquí está el invariante en CVL que captura esta propiedad:

Copy
invariant ethDepositsAlwaysGTEWethTotalSupply() 
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with (env e) {
        require e.msg.sender != currentContract;
    }

    preserved withdraw(uint256 amount) with (env e) {
        require balanceOf(e.msg.sender) <= totalSupply();
    }
}

La línea a continuación expresa el invariante:

Copy
nativeBalances[currentContract] >= totalSupply()

Sin embargo, este invariante no se cumple universalmente. Solo se cumple bajo condiciones específicas definidas en los bloques preserved. El bloque preserved a continuación requiere que el llamador (e.msg.sender) no sea igual al currentContract.

Copy
preserved with (env e) {
    require e.msg.sender != currentContract;
}

No es coincidencia que esta condición require aparezca en las siguientes reglas:

• deposit_ethDepositedEqualsWethReceived()
• withdraw_ethWithdrawnEqualsWETHReduced()

Está claro que esto se relaciona con la contabilidad entre los depósitos de ETH y la emisión de WETH. Si el contrato se llama a sí mismo y deposita ETH, no hay una ganancia neta de ETH, pero el WETH aún podría ser acuñado, lo que causa que el totalSupply exceda los depósitos reales de ETH.

El siguiente bloque preserved requiere que el saldo de msg.sender sea menor o igual a totalSupply(), lo que evita que la operación de retiro cause un underflow (desbordamiento negativo):

Copy
preserved withdraw(uint256 amount) with (env e) {
    require balanceOf(e.msg.sender) <= totalSupply();
}

No es de extrañar que esta condición reaparezca en una regla relacionada. Si bien aquí se muestra como una condición preserved para withdraw(), anteriormente apareció como una precondición en la regla withdraw_ethWithdrawDecreasesWETHSupply.

En ambos casos, el objetivo es evitar contraejemplos relacionados con el underflow. Esta es una fuerte razón para probar la condición como un invariante, lo cual haremos en la siguiente sección.

Aquí está la ejecución verificada del Prover para el invariante ethDepositsAlwaysGTEWethTotalSupply.

Invariante: Ningún saldo de cuenta excede el suministro total de WETH

Este invariante, expresado como balanceOf(address) <= totalSupply(), garantiza lo siguiente:

• El saldo de ninguna cuenta excede nunca el suministro total.
• Como consecuencia, dado que totalSupply() en sí no puede exceder max_uint256, los saldos de las cuentas individuales tampoco pueden desbordarse (overflow).

En las reglas anteriores que discutimos, se introdujeron las siguientes precondiciones para proteger contra el desbordamiento:

Copy
rule deposit_ethDepositedEqualsWethReceived(env e) {
    ...
    require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // precondition
    
    ...
}

Copy
rule deposit_revert(env e) {
    ...
    require balanceOf(caller) + ethDeposit <= max_uint256; // precondition
    
    ...
}

En la regla withdraw a continuación, se agregó la precondición para proteger contra el underflow:

Copy
rule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
    ...
    require balanceOf(e.msg.sender) <= totalSupply(); // precondition
    
    ...
}

En el invariante ethDepositsAlwaysGTEWethTotalSupply a continuación, también se usa como una condición preserved para proteger contra el underflow:

Copy
invariant ethDepositsAlwaysGTEWethTotalSupply() 
    nativeBalances[currentContract] >= totalSupply()
{
    ...

    preserved withdraw(uint256 amount) with (env e) {
        require balanceOf(e.msg.sender) <= totalSupply(); 
    }
}

El invariante a continuación aborda directamente estas precondiciones recurrentes al verificar formalmente que ningún saldo de cuenta excede nunca el suministro total:

Copy
invariant noAccountBalanceExceedsTotalSupply(env e1) 
    balanceOf(e1.msg.sender) <= totalSupply()
    
    filtered {
        f -> f.selector != sig:transfer(address,uint256).selector && // excludes standard ERC-20 transfer function from this invariant
			f.selector != sig:transferFrom(address,address,uint256).selector // excludes standard ERC-20 transferFrom function from this invariant
    }
    {
        preserved withdraw(uint256 amount) with (env e2) {
            require e1.msg.sender == e2.msg.sender;
        }
    }

Vamos a desglosarlo.

La línea a continuación es el invariante:

Copy
balanceOf(e1.msg.sender) <= totalSupply()

Filtramos transfer() y transferFrom() utilizando filtered porque estas funciones calculan y escriben en slots de almacenamiento, en lugar de usar una variable de mapping para los saldos de las cuentas. Por lo tanto, el seguimiento de los saldos de las cuentas requeriría resumir estas funciones utilizando resúmenes de CVL (un tema fuera del alcance de este capítulo).

Copy
filtered {
    f -> f.selector != sig:transfer(address,uint256).selector &&
        f.selector != sig:transferFrom(address,address,uint256).selector
}

Es razonable filtrar transfer() y transferFrom(), ya que solo deposit() y withdraw() (que invocan _mint() y _burn() respectivamente) pueden afectar el invariante. transfer() y transferFrom() simplemente mueven tokens que ya están contabilizados en el suministro total. Si el suministro total es incorrecto, el problema se origina en deposit() o withdraw(), no en las transferencias.

Si Solady WETH hubiera utilizado variables de mapping (lo cual no hace intencionalmente por diseño), rastrear los saldos y definir este invariante habría sido sencillo, y estos filtros no serían necesarios.

Dicho esto, al igual que las precondiciones y los bloques preserved, los filtros deben usarse con precaución, ya que pueden ocultar errores reales.

Por último, el bloque preserved requiere que e1.msg.sender (la dirección cuyo saldo estamos verificando en el invariante) sea igual al llamador durante la ejecución de la función withdraw:

Copy
{
    preserved withdraw(uint256 amount) with (env e2) {
        require e1.msg.sender == e2.msg.sender;
    }
}

La condición preserved require e1.msg.sender == e2.msg.sender evita que el Prover pruebe el invariante en una cuenta que no llama a withdraw().

La función withdraw() desencadena una quema, que reduce el suministro total mientras disminuye solo el saldo del llamador. Si el invariante verifica una cuenta diferente cuyo saldo no cambia, el Prover puede observar balanceOf(differentAccount) > totalSupply() después de la quema y reportar una falsa violación.

Al requerir que el invariante siga a la misma dirección que ejecuta withdraw(), el bloque preserved impone que la comprobación se aplique a la cuenta cuyo saldo realmente disminuye.

Aquí está la ejecución verificada del Prover.

Reemplazar las precondiciones con requireInvariant

Dado que noAccountBalanceExceedsTotalSupply() ahora está verificado formalmente, podemos reemplazar las precondiciones y las condiciones preserved con este invariante en las siguientes especificaciones:

• rule deposit_ethDepositedEqualsWethReceived()
• rule deposit_revert()
• rule withdraw_ethWithdrawDecreasesWETHSupply()
• invariant ethDepositsAlwaysGTEWethTotalSupply()

Aquí están las reglas y el invariante refactorizados usando requireInvariant:

Copy
rule deposit_ethDepositedEqualsWethReceived_withInvariant(env e) {
    require e.msg.sender != currentContract;
    requireInvariant noAccountBalanceExceedsTotalSupply(e);

    mathint ethBalanceBefore = nativeBalances[e.msg.sender];
    mathint wethBalanceBefore = balanceOf(e.msg.sender);
    
    deposit(e);

    mathint ethBalanceAfter = nativeBalances[e.msg.sender];
    mathint wethBalanceAfter = balanceOf(e.msg.sender);

    assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
    assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}

rule deposit_revert_withInvariant(env e) {
    address caller = e.msg.sender;
    uint256 ethDeposit = e.msg.value;

    requireInvariant noAccountBalanceExceedsTotalSupply(e);
    
    mathint totalSupplyBefore = totalSupply();
    mathint ethBalanceBefore = nativeBalances[caller];

    deposit@withrevert(e);
    bool isLastReverted = lastReverted;
    
    assert isLastReverted <=> (
        ethBalanceBefore < ethDeposit || 
        totalSupplyBefore + ethDeposit > max_uint256
    );
}

rule withdraw_ethWithdrawDecreasesWETHSupply_withInvariant(env e) {
    uint256 amount;
    requireInvariant noAccountBalanceExceedsTotalSupply(e);
    
    mathint totalSupplyBefore = totalSupply();
    
    withdraw(e, amount);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter == totalSupplyBefore - amount;
}

invariant ethDepositsAlwaysGTEWethTotalSupply_withInvariant() 
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with (env e) {
        require e.msg.sender != currentContract;
    }

    preserved withdraw(uint256 amount) with (env e) {
        requireInvariant noAccountBalanceExceedsTotalSupply(e);
    }
}

Y aquí está la ejecución verificada del Prover para estas reglas y el invariante.

Especificación completa en CVL y ejecución del Prover

Aquí está la especificación completa escrita en este capítulo:

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

persistent ghost bool g_lowLevelCallFail;

hook CALL(uint gas, address to, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc {    
    if (rc == 0) {
        g_lowLevelCallFail = true; 
    } else {
        g_lowLevelCallFail = false; 
    }
}

rule deposit_ethDepositedEqualsWethReceived(env e) {
    require e.msg.sender != currentContract;
    require balanceOf(e.msg.sender) + e.msg.value <= max_uint256; // will be replaced by an invariant

    mathint ethBalanceBefore = nativeBalances[e.msg.sender];
    mathint wethBalanceBefore = balanceOf(e.msg.sender);
    
    deposit(e);

    mathint ethBalanceAfter = nativeBalances[e.msg.sender];
    mathint wethBalanceAfter = balanceOf(e.msg.sender);

    assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
    assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}

rule deposit_ethDepositedEqualsWethReceived_withInvariant(env e) {
    require e.msg.sender != currentContract;
    requireInvariant noAccountBalanceExceedsTotalSupply(e);

    mathint ethBalanceBefore = nativeBalances[e.msg.sender];
    mathint wethBalanceBefore = balanceOf(e.msg.sender);
    
    deposit(e);

    mathint ethBalanceAfter = nativeBalances[e.msg.sender];
    mathint wethBalanceAfter = balanceOf(e.msg.sender);

    assert ethBalanceAfter == ethBalanceBefore - e.msg.value;
    assert wethBalanceAfter == wethBalanceBefore + e.msg.value;
}

rule deposit_ethDepositIncreasesWETHTotalSupply(env e) {
    mathint totalSupplyBefore = totalSupply();
    
    deposit(e);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter == totalSupplyBefore + e.msg.value;
}

rule deposit_revert(env e) {
    address caller = e.msg.sender;
    uint256 ethDeposit = e.msg.value;

    require balanceOf(caller) + ethDeposit <= max_uint256; // will be replaced by an invariant
    
    mathint totalSupplyBefore = totalSupply();
    mathint ethBalanceBefore = nativeBalances[caller];

    deposit@withrevert(e);
    bool isLastReverted = lastReverted;
    
    assert isLastReverted <=> (
        ethBalanceBefore < ethDeposit || 
        totalSupplyBefore + ethDeposit > max_uint256
    );
}

rule deposit_revert_withInvariant(env e) {
    address caller = e.msg.sender;
    uint256 ethDeposit = e.msg.value;

    requireInvariant noAccountBalanceExceedsTotalSupply(e);
    
    mathint totalSupplyBefore = totalSupply();
    mathint ethBalanceBefore = nativeBalances[caller];

    deposit@withrevert(e);
    bool isLastReverted = lastReverted;
    
    assert isLastReverted <=> (
        ethBalanceBefore < ethDeposit || 
        totalSupplyBefore + ethDeposit > max_uint256
    );
}

rule withdraw_ethWithdrawnEqualsWETHReduced(env e) {
    uint256 amount;

    require e.msg.sender != currentContract;

    mathint ethBalanceBefore = nativeBalances[e.msg.sender];
    mathint wethBalanceBefore = balanceOf(e.msg.sender); 

    withdraw(e,amount);

    mathint ethBalanceAfter = nativeBalances[e.msg.sender];
    mathint wethBalanceAfter = balanceOf(e.msg.sender);

    assert ethBalanceAfter == ethBalanceBefore + amount;
    assert wethBalanceAfter == wethBalanceBefore - amount;
}

rule withdraw_ethWithdrawDecreasesWETHSupply(env e) {
    uint256 amount;

    require balanceOf(e.msg.sender) <= totalSupply(); // will be replaced by an invariant
    
    mathint totalSupplyBefore = totalSupply();
    
    withdraw(e, amount);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter == totalSupplyBefore - amount;
}

rule withdraw_ethWithdrawDecreasesWETHSupply_withInvariant(env e) {
    uint256 amount;
    requireInvariant noAccountBalanceExceedsTotalSupply(e);
    
    mathint totalSupplyBefore = totalSupply();
    
    withdraw(e, amount);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter == totalSupplyBefore - amount;
}

rule withdraw_revert(env e) {
    uint256 amount; // the amount of eth to claim    
    
    mathint wethBalanceBefore = balanceOf(e.msg.sender); 

    withdraw@withrevert(e, amount);
    bool isLastReverted = lastReverted;

    assert isLastReverted <=> (
        amount > wethBalanceBefore ||
        e.msg.value != 0 ||
        g_lowLevelCallFail
    );
}

invariant ethDepositsAlwaysGTEWethTotalSupply() 
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with (env e) {
        require e.msg.sender != currentContract;
    }

    preserved withdraw(uint256 amount) with (env e) {
        require balanceOf(e.msg.sender) <= totalSupply();
    }
}

invariant ethDepositsAlwaysGTEWethTotalSupply_withInvariant() 
    nativeBalances[currentContract] >= totalSupply()
{
    preserved with (env e) {
        require e.msg.sender != currentContract;
    }

    preserved withdraw(uint256 amount) with (env e) {
        requireInvariant noAccountBalanceExceedsTotalSupply(e);
    }
}

invariant noAccountBalanceExceedsTotalSupply(env e1) 
    balanceOf(e1.msg.sender) <= totalSupply()
    
    filtered {
        f -> f.selector != sig:transfer(address,uint256).selector &&
            f.selector != sig:transferFrom(address,address,uint256).selector
    }
    {
        preserved withdraw(uint256 amount) with (env e2) {
            require e1.msg.sender == e2.msg.sender;
        }
    }

Aquí está la ejecución verificada del Prover de la especificación de WETH discutida en este capítulo.

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