在上一章中，我们介绍了如何在 CVL 中推理依赖环境的函数，重点关注了非 payable 上下文中的 msg.sender。在那些例子中，访问控制依赖于调用者的地址。我们还解释了如何处理由意外的非零 msg.value 引起的回退（reverts）。

在本章中，我们将介绍如何：

• 为预期有非零支付的函数（即标记为 payable 的函数）编写规则
• 如何对账户余额进行断言
• 如何获取当前合约的余额，类似于 Solidity 中的 address(this).balance

e.msg.sender 与 e.msg.value (payable)

考虑一个白名单合约，用户通过调用标记为 payable 的 register() 函数进行注册，并发送至少 0.05 ETH。注册后，调用者的地址（msg.sender）将通过在 whitelisted 映射中将其值设置为 true，从而被标记为已加入白名单：

Copy
/// Solidity

contract PayableWhitelist {
    mapping(address => bool) public whitelisted;

    function register() external payable {
        require(msg.value >= 0.05 ether, "whitelist fee is 0.05 eth");
        require(!whitelisted[msg.sender], "already whitelisted");

        whitelisted[msg.sender] = true;
    }

    function isWhitelisted(address _account) external view returns (bool) {
        return whitelisted[_account];
    }
}

我们将形式化验证以下属性：“当且仅当调用者支付至少 0.05 ETH 时，他们才能成功调用 register()”。为了验证这一点，我们编写以下 CVL 规则：

Copy
rule register_payEthToWhitelist(env e) {
    require !isWhitelisted(e.msg.sender);
    register@withrevert(e);
    assert !lastReverted <=> e.msg.value >= 5 * 10^16;
}

注意：在 CVL 中，指数运算使用 ^__，而在 Solidity 中使用 **__。

正如我们所知，由于我们使用的是双条件运算符（biconditional operator），我们必须通过前置条件排除其他引发回退的情况。我们添加 require(!isWhitelisted(e.msg.sender)) 作为前置条件，以要求 msg.sender 最初未被加入白名单（从而排除其已在白名单中的情况）。

现在，来看双条件断言：

assert !lastReverted <=> e.msg.value >= 5 * 10^16。

由于我们排除了发送者已被加入白名单的情况（require !isWhitelisted(e.msg.sender)），我们预期该规则将通过验证（VERIFIED），这意味着只有当 e.msg.value >= 5 * 10^16 时，函数才不会回退。

然而，正如形式化验证中常见的情况一样，一个狡猾的反例（counterexample）出现了，导致了违规（violation）。那就是发送者的 ETH 余额少于打算发送的金额，即余额不足：

可以通过在前置条件中添加 require(nativeBalances[e.msg.sender] >= e.msg.value) 来解决这个问题，从而排除余额不足导致回退的情况。

CVL 中的 nativeBalances

nativeBalances[address] 是 CVL 中的一个内置函数，用于获取指定地址当前的 ETH 余额。在下方，我们要求发送者的 nativeBalances 至少与 msg.value 一样大：

Copy
rule register_payEthToWhitelist(env e) {
    require !isWhitelisted(e.msg.sender);
    require nativeBalances[e.msg.sender] >= e.msg.value;

    register@withrevert(e);

    assert !lastReverted <=> e.msg.value >= 5 * 10^16;
}

现在，该规则已通过验证（VERIFIED）：

Prover 运行结果：link

验证白名单状态

既然我们已经验证了“当且仅当调用者支付至少 0.05 ETH 时，他们才能成功调用 register()”，现在让我们进一步扩展规则的作用域，断言调用者在成功调用后其状态为 isWhitelisted。

以下是更新后要进行形式化验证的属性：“当且仅当调用者发送至少 0.05 ETH 并被加入白名单时，交易才会成功。”为了实现这一点，我们可以复用之前的规则，并添加一个额外的断言：isWhitelisted。

以下是更新后的 CVL 规则：

Copy
rule register_payEthToWhitelist_modified(env e) {
    require !isWhitelisted(e.msg.sender);
    require nativeBalances[e.msg.sender] >= e.msg.value;

    register@withrevert(e);

    assert !lastReverted <=> e.msg.value >= 5 * 10^16 && isWhitelisted(e.msg.sender);
}

上述规则意味着，当且仅当发送者发送至少 0.05 ETH（e.msg.value >= 5 * 10^16）并且被加入白名单（isWhitelisted(e.msg.sender)）时，交易才不会回退（!lastReverted）。

换句话说，如果 !lastReverted 为 true（交易成功），那么充足的 ETH 和加入白名单这两个条件都必须成立。

以下是 Prover 的报告，且已通过验证（VERIFIED）：

Prover 运行结果：link

使用 => 替代 <=> 来放宽前置条件

另一种方法是使用蕴含运算符（implication operator）。如果你的目标仅仅是检查当发送了不正确的 msg.value 时函数是否会回退，那么以下规则就足够了。这条规则并不排除其他引发回退的原因，比如发送者没有足够的余额。它只是表明如果发送的 ether 少于 0.05，那么它必定会回退。

Copy
rule register_payEthToWhitelist_implication(env e) {
    register@withrevert(e);
    assert e.msg.value < 5 * 10^16 => lastReverted;
}

如果我们使用这条规则，可以看到它通过了验证（VERIFIED）：

Prover 运行结果：link

验证 ETH 余额转账 与自转账边缘情况

假设我们想要形式化验证余额的更新，即 msg.sender 的余额减少了 msg.value，而合约的余额增加了相同的数量。

下面是 CVL 规则，将在下一节中进行解释：

Copy
rule register_nativeBalances(env e) {
    mathint balanceBefore = nativeBalances[currentContract];
    register(e);

    mathint balanceAfter = nativeBalances[currentContract];
    assert balanceAfter == balanceBefore + e.msg.value;
}

currentContract

在上述规则中，我们获取了 currentContract 的初始 ETH 余额（balanceBefore）和最终余额（balanceAfter）。currentContract 是一个内置变量，指的是当前正在被验证的合约。将该变量传递给 nativeBalances[currentContract] 即可获取该合约的余额。在这两次获取余额的调用之间，触发了 register() 函数，因此我们预期余额将增加与 msg.value 相等的金额。

一个出乎意料的反例会导致此规则失败。Prover 会生成一个 msg.sender == currentContract 的反例。Prover 会探索所有可能的场景，包括合约调用自身的场景。

这表明合约将 ETH 发送给了自己，而不是从外部发送者那里接收新的 ETH。结果，余额并没有像预期那样实际增加（因为向自己发送 ETH 不会改变总余额），从而导致断言 balanceAfter == balanceBefore + e.msg.value 失败。

为了解决这个问题，由于 msg.sender 不应该是合约本身（currentContract），我们需要在验证 ETH 余额变化时通过添加前置条件来过滤掉自转账（self-transfers）：require(e.msg.sender != currentContract)。

然而，这里有一个注意事项：在实际项目中，要确保合约不能调用自己的函数，因为某些情况仍可能导致自调用（self-calls）。如果没有进行适当的检查，这可能会掩盖一个 Bug。

以下是修正后的规则和 Prover 报告。正如预期的那样，此规则通过了验证（VERIFIED）：

Copy
rule register_nativeBalances(env e) {
    mathint balanceBefore = nativeBalances[currentContract];

    require e.msg.sender != currentContract;
    register(e);

    mathint balanceAfter = nativeBalances[currentContract];
    assert balanceAfter == balanceBefore + e.msg.value;
}

Prover 运行结果：link

使用 <=> 和 || 验证所有回退情况

假设我们想要验证每一个可能导致回退的原因都被明确说明。我们可以将断言表达为双条件运算（<=>），并使用析取（使用 OR 或 ||）列出所有的回退情况。

下面的规则指出，可能导致回退的原因只有以下几种：

• 发送者已被加入白名单
• 发送者的余额不足
• 发送者没有转入足够的资金

如果 register() 因为任何其他原因发生回退，我们将得到一个断言违规（assert violation）。

规则如下：

Copy
rule register_allRevertCases(env e) {
    bool wasWhitelisted = isWhitelisted(e.msg.sender);
    mathint balanceBefore = nativeBalances[e.msg.sender];

    register@withrevert(e);

    assert lastReverted <=> (
        wasWhitelisted ||              // sender already whitelisted
        balanceBefore < e.msg.value || // sender's balance insufficient
        e.msg.value < 5 * 10^16        // sender's transfer amount insufficient 
    );
}

正如预期的那样，该规则通过了验证（VERIFIED）：

Prover 运行结果：link

总结

• 在 CVL 中，环境变量 e.msg.value 用于表达和验证一个 payable 函数应该是成功还是回退，通常是通过断言一个最小的或确切的所需金额。
• nativeBalances[address] 是一个内置函数，用于获取指定地址的当前 ETH 余额，并且可以通过检查余额变化来验证转账。
• currentContract 是一个内置变量，指的是当前正在被验证的合约。
• Prover 会将自调用包含在测试用例中，因此在我们的示例中，我们通过添加 require(e.msg.sender != currentContract) 来排除它们以避免产生虚假反例；但请谨慎，因为自调用可能是合理存在的，并可能在现实世界的合约中揭示真实的 Bug。

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