简介

ETH 在 DeFi 中广泛用于代币交换、提供流动性、质押和抵押，它需要一个兼容 ERC-20 的版本，以便协议能够通过与其他代币相同的标准化接口与它进行交互。

这就催生了 Wrapped ETH (WETH)，其原理非常简单：存入原生 ETH 会向用户的账户铸造等量的 WETH，而提取则会销毁相应的 WETH 并将原生 ETH 退还到用户的账户中。

在上一章中，我们对典型 ERC-20 合约的基本属性进行了形式化验证。由于 WETH 本身就是一个 ERC-20 代币，我们将在此不再重复那些规范，而是仅关注 WETH 特有的功能。我们将形式化验证使用了内联汇编进行 Gas 优化的 Solady WETH 实现。

待形式化验证的 WETH 属性

当用户存入 ETH 时，他们必须收到等量的 WETH。当他们提取时，他们必须能够随时将这些 WETH 兑换为等量的 ETH。

这两种行为定义了 WETH 合约在标准 ERC-20 功能之外的核心保证。为了维持这些保证，合约必须满足两个关键的不变量 (invariants)：

1. 合约持有的 ETH 必须始终大于或等于 WETH 的总供应量。 这保证了所有 WETH 持有者可以随时将他们的代币兑换为 ETH，无论兑换的顺序或时间如何。
2. WETH 的总供应量必须始终大于或等于所有 WETH 余额的总和。 这保证了合约分发的代币数量不能超过其铸造的数量。

然而，我们不会对第二个不变量进行形式化验证，因为 Solady WETH 合约继承的 ERC-20 实现并没有使用 mapping 来存储账户余额。相反，它使用为每个账户计算出的 slot 来读取和写入 storage。

因此，验证这个不变量需要使用 CVL 的“摘要 (summarization)”功能：我们需要对修改账户余额 storage 的函数进行摘要，使用 ghost mapping 映射它们，并通过该 ghost 状态来推导不变量。这个主题超出了本章的范围。有关更多信息，请参阅关于 summarization 的 Certora 文档。

我们没有验证这个不变量，而是形式化验证了另一个不变量：任何账户余额都不会超过总供应量。这看起来似乎微不足道，但当存取款规则依赖于与余额相关的前置条件时，它将在后面变得非常有用。这个不变量允许我们使用 requireInvariant 来替换那些假设，从而保证我们假设的这些前置条件确实是有效的。

存入的 ETH 等于收到的 WETH

当用户使用 deposit() 函数将 ETH 存入合约时，他们的 WETH 余额增加，而他们的 ETH 余额减少相同的数量。为了在 CVL 中形式化验证此行为，我们按以下步骤进行：

1. 设置前置条件：
   • 发送者不能是合约本身（e.msg.sender != currentContract），因为自身调用会破坏 ETH 余额的记账，而且没有任何执行路径允许此类调用。
   • 发送者的 WETH 余额加上存入金额必须不溢出（balanceOf(e.msg.sender) + e.msg.value <= max_uint256）。
2. 记录调用 deposit() 之前用户的 ETH 和 WETH 余额。
3. 以 e.msg.value 中的 ETH 金额调用 deposit()。
4. 记录调用 deposit() 之后用户的 ETH 和 WETH 余额。
5. 断言正确性条件：
   • 最终的 ETH 余额等于初始 ETH 余额减去存入金额。
   • 最终的 WETH 余额等于初始 WETH 余额加上存入金额。

以下是 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;
}

现在让我们详细拆解一下。

前置条件

第一个前置条件指示 Prover 排除调用者（msg.sender）是合约自身的情况：

Copy
require e.msg.sender != currentContract;

如果没有这个前置条件，Prover 会假设调用者可能是 currentContract，这将导致规则失败。例如，如果合约向自身存入 1 ETH，其持有的 ETH 净额不会发生变化（因为它向自身发送并接收了相同数量的金额）。然而，合约仍然会铸造 1 WETH，从而导致断言 assert ethBalanceAfter == ethBalanceBefore - e.msg.value 失败。

第二个前置条件 require balanceOf(e.msg.sender) + e.msg.value <= max_uint256 排除了在将调用者的初始 WETH 余额与 ETH 存款相加时发生溢出的可能性。

由于 require 语句是 Prover 不去验证的假设——它仅仅把它们当作已知条件——我们需要在后面的部分将其作为一个不变量进行形式化证明。一旦被证明，我们就可以使用 requireInvariant 将这个假设的前置条件替换为已验证的不变量。

记录在调用 deposit() 前后用户的 ETH 和 WETH 余额

设置好所有前置条件后，我们必须记录调用者在调用 deposit() 前后的 ETH 和 WETH 余额。这些记录的值将在断言中用于推导余额的变化：

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

断言

第一个断言检查调用者的 ETH 余额是否准确减少了随交易发送的 ETH 金额。第二个断言检查调用者的 WETH 余额是否准确增加了存入的 ETH 金额：

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

这是针对 deposit_ethDepositedEqualsWethReceived 规则已验证的 Prover run。

存入 ETH 增加 WETH 总供应量

除了改变余额之外，调用 deposit() 的另一个预期效果是 WETH 的 totalSupply 会增加。以下 CVL 规则捕获了这一行为：

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

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

变量 totalSupplyBefore 和 totalSupplyAfter 记录了在调用 deposit() 前后的总供应量数值，以在断言中验证预期的变化。

由于 deposit() 函数在内部调用了 _mint()，WETH 的总供应量增加了存入的金额，这反映在断言中：

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

请注意，此处没有 require e.msg.sender != currentContract 这一前置条件，因为该断言仅涉及供应量的增加。无论发送者是谁，供应量都会按存入的 ETH 金额（msg.value）增加。

这是针对 deposit_ethDepositIncreasesWETHTotalSupply 规则已验证的 Prover run。

验证 deposit() 中 revert 的原因

现在让我们来验证 deposit() 函数的 revert 路径。我们希望检测它发生意外 revert 或在应该 revert 时未能 revert 的情况。

为了在 CVL 中形式化验证此行为，我们按以下步骤进行：

1. 设置一个前置条件：调用者的 WETH 余额加上存入金额必须不溢出（balanceOf(caller) + ethDeposit <= max_uint256）。
2. 记录在调用 deposit() 之前的 WETH totalSupply 和调用者的 ETH 余额。
3. 使用 @withrevert 标签调用 deposit()，以允许规则观察 revert 现象。
4. 使用 lastReverted，它返回一个布尔值，指示上一次调用是否发生了 revert。
5. 断言该函数发生 revert 当且仅当（<=>）以下任一条件为真：
   • 调用前的调用者 ETH 余额小于存入金额（e.msg.value）。
   • 调用前的 WETH 总供应量加上存入金额超过了 max_uint256。

以下是 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
    );
}

让我们进一步拆解这条规则。

为了提高可读性，我们分别将 e.msg.sender 和 e.msg.value 赋值给 caller 和 ethDeposit：

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

如下所示的前置条件，也出现在了之前的规则 deposit_ethDepositedEqualsWethReceived() 中：

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

它在这里作为前置条件再次出现，而不是作为 revert 条件的一部分，这进一步强调了对其进行形式化验证的必要性。

接下来，在调用 deposit() 函数之前，我们记录 totalSupplyBefore（WETH 总供应量）和调用者的 nativeBalances 的值：

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

现在，我们使用 @withrevert 标签调用 deposit() 函数，并记录调用是否发生了 revert：

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

最后，断言使用双条件运算符（<=>）并以析取（使用 OR）方式列出所有发生 revert 的情况：

• 当调用者之前的 ETH 余额（ethBalanceBefore）小于 ETH 存入金额（e.msg.value）时，函数 revert。

  这意味着调用者没有足够的 ETH 进行存入操作。

• 当 WETH 总供应量（totalSupplyBefore）加上 ETH 存入金额将超过 max_uint256 时，函数也会 revert。

  由于每次存入都会铸造等量的 WETH，因此超过 uint256 的限制将导致溢出。

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

此处不需要前置条件 msg.sender != currentContract，因为 revert 条件涉及的是余额不足和溢出，这与调用者的身份无关。

这是针对 deposit_revert 规则已验证的 Prover run。

提取的 ETH 等于减少的 WETH

当用户从合约中提取 ETH 时，他们的 ETH 余额增加，而他们的 WETH 余额减少相同的数量。以下 CVL 规则捕获了这一行为：

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

这与 rule deposit_ethDepositedEqualsWethReceived() 的结构相同。到现在为止，这种模式应该已经很熟悉了：

• 设置前置条件
• 在调用 withdraw() 之前记录调用者的 ETH 和 WETH 余额
• 调用 withdraw()
• 记录调用之后的调用者的 ETH 和 WETH 余额

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

现在，我们直接来看断言。

在下面的断言中，我们验证 ETH 余额增加的数量和 WETH 余额减少的数量是否等同于提取的 amount：

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

前置条件 require e.msg.sender != currentContract 是必须的，因为自身调用不会导致合约的 ETH 余额发生变化（存入自身不会产生净变化），这会导致断言 assert ethBalanceAfter == ethBalanceBefore + amount 失败（产生误报）。

这是针对 withdraw_ethWithdrawnEqualsWETHReduced 规则已验证的 Prover run。

提取 ETH 减少 WETH 总供应量

当用户提取 ETH 时，相应数量的 WETH 会被销毁，这会减少总供应量。这是 withdraw() 函数的预期效果。以下 CVL 规则捕获了这一行为：

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

由于提取操作会根据提取的金额（等同于被销毁的余额）来减少总供应量，以下前置条件通过要求任何单个余额都不能超过总供应量，来确保 totalSupply 的减法不会发生下溢：

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

与之前的规则一样，这个前置条件代表了一个必须在稍后进行形式化验证的假设。

接下来，我们遵循一种熟悉的模式，记录在 withdraw 调用前后的 WETH 总供应量：

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

然后我们断言 WETH totalSupply 减少了预期的数量：

Copy
assert totalSupplyAfter == totalSupplyBefore - amount;

此处前置条件 require e.msg.sender != currentContract 是不必要的，因为供应量的减少（或供应量的变化）与调用者是谁无关。

这条规则证实了在提取期间销毁 WETH 正确地减少了总供应量。这是已验证的 Prover run。

验证 withdraw() 中 revert 的原因

withdraw_revert 规则遵循了与 deposit_revert 规则不同的模式。为了理解原因，让我们首先看看 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)
        }
    }
}

除了实现自身 revert 条件的 _burn() 函数外，withdraw() 函数还包含了用于检查 ETH 转账是否成功的汇编代码：

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

iszero 表达式在 ETH 转账失败时返回 true，这会触发 revert。否则，它返回 false，意味着 ETH 转账成功。为了验证这种汇编行为，我们使用 CVL 钩子（hook，即 CALL）来观察底层的 ETH 转账调用是否如预期那样 revert。

以下是验证所有 withdraw() revert 条件（包括底层调用失败）的 CVL 规则：

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

让我们解释一下上面的规则。

下面这一行是 persistent ghost（持久幽灵）变量的声明：

Copy
persistent ghost bool g_lowLevelCallFail;

注意：关于普通 ghost 与 persistent ghost 之间的区别，请参阅单独的“使用 Persistent Ghosts”一章。

这个 ghost 变量由 CALL 钩子负责更新。当 withdraw() 方法被调用时，具体是由向调用者转账 ETH 的底层调用来触发该钩子。如果底层调用失败（rc == 0），ghost 变量 g_lowLevelCallFail 会被设置为 true；如果调用成功（rc != 0），它会被设置为 false，如下面的 CALL 钩子所示：

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

这为 Prover 提供了一种在汇编块内部追踪 ETH 转账成功/失败的方法。

现在我们来看看规则。

像往常一样，我们在调用 withdraw() 函数之前记录余额：

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

然后我们使用 @withrevert 标签调用 withdraw() 函数，并记录调用是否发生了 revert：

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

在下面的断言中，该函数发生 revert 当且仅当（<=>）满足以下任一条件：

• 提取的 amount 超过了调用者的 WETH 余额（wethBalanceBefore）

  这意味着调用者试图提取的 ETH 超过了其 WETH 余额所允许的数量。

• 在调用的同时发送了 ETH

  这是不被允许的，因为 withdraw 不是一个 payable 函数。

• 将 ETH 转回调用者的操作失败

  此条件通过使用 g_lowLevelCallFail ghost 变量跟踪底层的 CALL 结果来判定。

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

这是针对 withdraw_revert 规则已验证的 Prover run。

不变量：ETH 总存款大于或等于 WETH 总供应量（偿付能力）

为了让用户成功使用他们的 WETH 赎回 ETH，合约持有的 ETH 必须始终大于或等于 WETH 总供应量。以下是捕获此属性的 CVL 不变量：

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

下面这行代码表达了该不变量：

Copy
nativeBalances[currentContract] >= totalSupply()

然而，这个不变量并不普遍成立。它仅在 preserved 块中定义的特定条件下才成立。下面的 preserved 块要求调用者（e.msg.sender）不等于 currentContract。

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

这个 require 条件出现在以下规则中并不是巧合：

• deposit_ethDepositedEqualsWethReceived()
• withdraw_ethWithdrawnEqualsWETHReduced()

很明显，这与 ETH 存款和 WETH 发行之间的记账有关。如果合约调用自身并存入 ETH，就不会有净 ETH 的增加，但 WETH 可能仍然会被铸造，这会导致 totalSupply 超过实际的 ETH 存款量。

下一个 preserved 块要求 msg.sender 的余额小于或等于 totalSupply()，这可以防止 withdraw 操作引发下溢：

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

这个条件在相关的规则中再次出现并不奇怪。虽然它在这里作为 withdraw() 的 preserved 条件出现，但它之前曾作为前置条件出现在 withdraw_ethWithdrawDecreasesWETHSupply 规则中。

在这两种情况中，目的都是为了防止发生与下溢相关的反例。这是一个充分的理由，说明我们应该将该条件作为一个不变量进行证明，我们将在下一节中进行这一操作。

这是针对 ethDepositsAlwaysGTEWethTotalSupply 不变量已验证的 Prover run。

不变量：任何账户余额均不超过 WETH 总供应量

这个不变量，表示为 balanceOf(address) <= totalSupply()，保证了以下几点：

• 任何账户余额永远不会超过总供应量。
• 因此，由于 totalSupply() 本身不能超过 max_uint256，单个账户的余额也不可能溢出。

在我们之前讨论的规则中，引入了以下前置条件以防止溢出：

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
    
    ...
}

在下面的 withdraw 规则中，添加了该前置条件以防止下溢：

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

在下面的 ethDepositsAlwaysGTEWethTotalSupply 不变量中，它也被用作 preserved 条件以防止下溢：

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

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

下面的不变量直接应对了这些反复出现的前置条件，它通过形式化验证证明了任何账户余额永远不会超过总供应量：

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

让我们拆解它。

下面这行代码是不变量：

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

我们使用 filtered 过滤掉了 transfer() 和 transferFrom()，因为这些函数会计算并写入存储槽，而不是使用 mapping 变量来存储账户余额。因此，要追踪账户余额，就需要使用 CVL summaries（摘要）对这些函数进行摘要处理（这个主题超出了本章的范围）。

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

过滤掉 transfer() 和 transferFrom() 是合理的，因为只有 deposit() 和 withdraw()（它们分别调用了 _mint() 和 _burn()）能够影响该不变量。transfer() 和 transferFrom() 只是转移了已经计入总供应量的代币。如果总供应量不正确，问题必定源自 deposit() 或 withdraw()，而不是来自转账。

如果 Solady WETH 使用了 mapping 变量（在设计上它故意没有这么做），那么追踪余额和定义这个不变量将是非常直接的，也就没有必要使用这些 filters 了。

尽管如此，就像前置条件和 preserved 块一样，应该谨慎使用 filters，因为它们有可能会掩盖真实的 bug。

最后，preserved 块要求 e1.msg.sender（也就是我们在不变量中检查其余额的地址）在 withdraw 函数执行期间等于调用者：

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

preserved 条件 require e1.msg.sender == e2.msg.sender 可以防止 Prover 在没有调用 withdraw() 的账户上测试该不变量。

withdraw() 函数会触发一次销毁，这会减少总供应量，同时仅减少调用者的余额。如果该不变量检查的是另一个余额未发生变化的账户，Prover 可能会在销毁操作之后观察到 balanceOf(differentAccount) > totalSupply()，从而报告一次虚假的违例。

通过要求该不变量遵循执行 withdraw() 的同一个地址，preserved 块强制该检查仅适用于余额实际减少的账户。

这是已验证的 Prover run。

使用 requireInvariant 替换前置条件

既然现在已经对 noAccountBalanceExceedsTotalSupply() 进行了形式化验证，我们可以在以下规范中，用这个不变量来替换前置条件和 preserved 条件：

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

以下是使用 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);
    }
}

这是针对这些规则和不变量已验证的 Prover run。

完整 CVL 规范与 Prover 运行

以下是本章中编写的完整规范：

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

这是本章中讨论的 WETH 规范已验证的 Prover run。

本文是使用 Certora Prover 进行形式化验证系列文章的一部分