简介

在本章中，我们将对 Solmate 的 ERC-20 实现进行形式化验证，其中包括以下内容：

• 标准的状态变更函数：transfer()、approve()、transferFrom()
• 标准的视图函数：totalSupply()、balanceOf()、allowance()
• 扩展的内部函数：_mint()、_burn()

请注意，虽然 Solmate 的 ERC-20 实现包含一个 permit() 函数，但我们有意将其省略，因为本系列尚未涵盖如何形式化验证密码学签名。

Solmate 的 ERC-20 代币的有趣之处在于它使用了 unchecked 块来在修改总供应量和余额时节省 Gas。由于 unchecked 块会绕过 Solidity 内置的溢出检查，因此形式化验证对于从数学上证明不会发生溢出至关重要。

以下是简化的 Solmate ERC-20 实现，仅移除了 permit() 函数：

Copy
// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity >=0.8.0;

/// @notice Modern and gas efficient ERC20 + EIP-2612 implementation.
/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol)
/// @author Modified from Uniswap (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol)
/// @dev Do not manually set balances without updating totalSupply, as the sum of all user balances must not exceed it.
abstract contract ERC20 {
    /*//////////////////////////////////////////////////////////////
                                 EVENTS
    //////////////////////////////////////////////////////////////*/

    event Transfer(address indexed from, address indexed to, uint256 amount);

    event Approval(address indexed owner, address indexed spender, uint256 amount);

    /*//////////////////////////////////////////////////////////////
                            METADATA STORAGE
    //////////////////////////////////////////////////////////////*/

    string public name;

    string public symbol;

    uint8 public immutable decimals;

    /*//////////////////////////////////////////////////////////////
                              ERC20 STORAGE
    //////////////////////////////////////////////////////////////*/

    uint256 public totalSupply;

    mapping(address => uint256) public balanceOf;

    mapping(address => mapping(address => uint256)) public allowance;

    /*//////////////////////////////////////////////////////////////
                               CONSTRUCTOR
    //////////////////////////////////////////////////////////////*/

    constructor(
        string memory _name,
        string memory _symbol,
        uint8 _decimals
    ) {
        name = _name;
        symbol = _symbol;
        decimals = _decimals;
    }

    /*//////////////////////////////////////////////////////////////
                               ERC20 LOGIC
    //////////////////////////////////////////////////////////////*/

    function approve(address spender, uint256 amount) public virtual returns (bool) {
        allowance[msg.sender][spender] = amount;

        emit Approval(msg.sender, spender, amount);

        return true;
    }

    function transfer(address to, uint256 amount) public virtual returns (bool) {
        balanceOf[msg.sender] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(msg.sender, to, amount);

        return true;
    }

    function transferFrom(
        address from,
        address to,
        uint256 amount
    ) public virtual returns (bool) {
        uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.

        if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

        balanceOf[from] -= amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(from, to, amount);

        return true;
    }

    /*//////////////////////////////////////////////////////////////
                        INTERNAL MINT/BURN LOGIC
    //////////////////////////////////////////////////////////////*/

    function _mint(address to, uint256 amount) internal virtual {
        totalSupply += amount;

        // Cannot overflow because the sum of all user
        // balances can't exceed the max uint256 value.
        unchecked {
            balanceOf[to] += amount;
        }

        emit Transfer(address(0), to, amount);
    }

    function _burn(address from, uint256 amount) internal virtual {
        balanceOf[from] -= amount;

        // Cannot underflow because a user's balance
        // will never be larger than the total supply.
        unchecked {
            totalSupply -= amount;
        }

        emit Transfer(from, address(0), amount);
    }
}

上述的 ERC-20 实现是一个抽象合约，需要一个继承合约使其具体化。我们还需要通过外部函数暴露 _mint() 和 _burn()，以便 Prover 可以在验证期间调用它们。为了满足这两个要求，我们使用一个 harness 合约。

harness 合约继承自被验证的合约，通过将内部函数包装为外部函数，使得 Prover 可以访问这些内部函数。它还可以定义辅助的 view 或 pure 函数，提供状态查询和实用计算，以简化规则和不变量的逻辑。

对于本规范，harness 是一个极简合约，它继承了抽象的 ERC-20 实现，既提供了一个具体的合约，又使其内部函数（_mint() 和 _burn()）可用于验证。

以下是 harness 合约：

Copy
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.25; 

import "src/Solmate/ERC20.sol";

contract ERC20Harness is ERC20 {    
    constructor (
        string memory _name, 
        string memory _symbol, 
        uint8 _decimals
    ) ERC20(_name, _symbol, _decimals) {}
    
    /// Left without access controls; integrators are expected to implement their own.
    function mint(address _to, uint256 _amount) external {
        _mint(_to, _amount);
    }
	
    /// Left without access controls; integrators are expected to implement their own.
    function burn(address _from, uint256 _amount) external {
        _burn(_from, _amount);
    }
}

形式化验证 ERC-20 属性的循序渐进方法

在本章中，我们采取一种循序渐进的方法来形式化验证 ERC-20 合约的属性。大纲如下：

• 意图是什么？用户希望发生什么？
  • 哪些函数实现了这个意图？
    • 如果调用成功，预期的状态变更如何体现？
    • 如果调用成功，绝不能发生哪些意外的副作用或针对无关方的状态变更？
    • 如果调用回退（revert），是什么导致了回退？
• 哪些不变量必须始终成立？
• 绝不能允许哪些未经授权的操作（由函数或调用者执行）？

该过程如下图所示：

接下来，我们将按照下面编号顺序所示的每个步骤进行讲解：

1. 验证函数正确性（调用成功或回退）

transfer()

让我们从发送代币的意图开始 —— 我们验证当发送者转移代币时，接收者收到了确切的指定数量。这是通过 transfer() 函数实现的。

以下是 transfer() 函数的实现：

Copy
function transfer(address to, uint256 amount) public virtual returns (bool) {
    balanceOf[msg.sender] -= amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(msg.sender, to, amount);

    return true;
}

以下是验证发送者余额减少和接收者余额增加确切数量的 CVL 规则：

Copy
rule transfer_effectOnBalances(env e) {
    address receiver;
    uint256 amount;

    require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256; // will be replaced by an invariant
    
    mathint senderBalanceBefore = balanceOf(e.msg.sender);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transfer(e, receiver, amount);

    mathint senderBalanceAfter = balanceOf(e.msg.sender);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != e.msg.sender) {
        assert senderBalanceAfter == senderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert senderBalanceAfter == senderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

我们进一步解释一下这条规则。

前置条件限制了 Prover 赋予余额之和超过 max_uint256 限制的值，如下所示：

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

这是必要的，因为 transfer() 函数在将转账金额加到 balanceOf[address] 时使用了 unchecked 块，这会导致 Prover 将溢出视为“可能发生”并报告误报。

然而，由于这个前置条件将值限制在 max_uint256 以内，Prover 无法测试实际可能发生的溢出情况，这可能会掩盖溢出错误。因此，应该使用已验证的不变量在形式化层面上排除这种情况，我们将在“requireInvariant”部分讨论这一点。

在前置条件之后，我们继续执行以下步骤：

• 记录调用 transfer() 之前的发送者和接收者余额。
• 执行 transfer() 调用。
• 调用结束后再次记录发送者和接收者的余额。我们将在断言中使用这些值来推断发送者和接收者的余额变化。

Copy
mathint senderBalanceBefore = balanceOf(e.msg.sender);
mathint receiverBalanceBefore = balanceOf(receiver);

transfer(e, receiver, amount);

mathint senderBalanceAfter = balanceOf(e.msg.sender);
mathint receiverBalanceAfter = balanceOf(receiver);

现在是断言部分：

• 如果发送者和接收者是不同的地址，我们断言：
  • 发送者的余额减少了 amount。
  • 接收者的余额增加了 amount。
• 如果发送者与接收者是同一地址，我们断言余额保持不变：

Copy
if (receiver != e.msg.sender) {
    assert senderBalanceAfter == senderBalanceBefore - amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
} 
else {
    assert senderBalanceAfter == senderBalanceBefore;
    assert receiverBalanceAfter == receiverBalanceBefore;
}

断言确认了全额的价值转移，没有任何扣除，如这个 Prover 的运行结果所示。

transfer() 回退

我们刚刚讲解了转账成功的路径。接下来，我们将验证 transfer() 在失败条件下的回退行为。

下面的 CVL 规则在断言中涵盖了所有的回退条件。它使用双向条件运算符（<=>，当且仅当）来声明只有在列出的条件之一为真时才会发生回退。这些条件包括：

• 发送者的余额不足。
• 在调用一个非 payable 函数时发送了 ETH。

Copy
rule transfer_reverts(env e) {
    address receiver;
    uint256 amount;

    mathint senderBalance = balanceOf(e.msg.sender);

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

    assert isLastReverted <=> (
        senderBalance < amount || // sender doesn't have enough balance
        e.msg.value != 0 // sending ETH with a call to transfer (non-payable)
    );
}

对于这条规则，我们没有定义任何前置条件，所以我们直接记录转账调用之前的状态。下面这行代码捕获了转账调用之前的值：

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

在断言中，仅列出了两种导致回退的场景。第一种是发送者的余额小于要转移的金额，因为发送者不应该能够发送多于他们拥有的代币：

Copy
assert isLastReverted <=> (
    senderBalance < amount || // not enough balance
    e.msg.value != 0
);

第二种情况（e.msg.value != 0）会导致回退，因为该函数是非 payable 的。任何非零的 msg.value 都会导致其失败。这是非 payable 函数的一个回退条件，并且在 ERC-20 的形式化验证过程中会频繁出现。

该断言使用了一个双向条件运算符，以保证当且仅当发生这两种情况之一时，该函数才会回退。这意味着不应该有其他任何条件导致函数回退。这是相关的 Prover 运行结果。

transferFrom()

在这里，我们验证当一个被授权的 spender 代表 holder（代币持有者）转移代币时，接收者收到了确切的指定金额。这是通过 transferFrom() 函数完成的，如下面的 Solidity 实现所示。这次转账所引起的授权额度（allowance）变化将在后面的部分进行分析。

Copy
function transferFrom(
    address from,
    address to,
    uint256 amount
) public virtual returns (bool) {
    uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.

    if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

    balanceOf[from] -= amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }

    emit Transfer(from, to, amount);

    return true;
}

下面的规则几乎与 transfer_effectOnBalances 规则完全相同 —— 唯一的区别在于它调用的是 transferFrom()。它执行了以下操作：

• 前置条件：约束 holder 和 receiver 的余额之和在 max_uint256 以内，以防止 Prover 探索 unchecked 块中的溢出场景。
• 调用前和调用后状态：记录在调用 transferFrom() 前后两个账户的余额，以便我们在断言中验证确切的余额变化。
• 断言：
  • 如果 receiver != holder，断言他们的余额差值为 amount。
  • 如果 receiver == holder，断言余额保持不变。

Copy
rule transferFrom_effectOnBalances(env e) {
    address holder;
    address receiver;
    uint256 amount;
    
    require balanceOf(holder) + balanceOf(receiver) <= max_uint256; // will be formally verified later

    mathint holderBalanceBefore = balanceOf(holder);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transferFrom(e, holder, receiver, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != holder) {
        assert holderBalanceAfter == holderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert holderBalanceAfter == holderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

查看 Prover 运行结果。

transferFrom() 回退

transferFrom() 回退规则的模式也类似于 transfer() 规则，除了一种涉及 spender 的额外情况。如下所示，如果 spender 缺乏足够的授权额度（也就是说，如果 spenderAllowance < amount），交易就会回退：

Copy
rule transferFrom_reverts(env e) {
    address holder;
    address receiver;
    uint256 amount;

    mathint holderBalance = balanceOf(holder);
    mathint spenderAllowance = allowance(holder, e.msg.sender); 
 
 

    transferFrom@withrevert(e, holder, receiver, amount); // spender is the msg.sender
    bool isLastReverted = lastReverted;

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

所有其他回退场景都与 transfer() 规则中的场景相同。这是 Prover 运行结果。

授权额度 (allowance) 的变化

当 transferFrom() 调用成功时，holder 为 spender 批准的授权额度会发生改变。transferFrom() 的实现包含以下条件语句：

Copy
if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;

这意味着，如果当前的授权额度没有设置为最大 uint256 值，那么所花费的金额将从中扣除。如果授权额度被设置为最大值，它的行为就像是一个无限额度，并且保持不变。

这种行为在下面所示的 CVL 规则的断言部分中被捕获：

Copy
rule transferFrom_allowanceChange(env e) {
    address holder;
    address receiver;
    uint256 amount;

    mathint spenderAllowanceBefore = allowance(holder, e.msg.sender);

    transferFrom(e, holder, receiver, amount);
    mathint spenderAllowanceAfter = allowance(holder, e.msg.sender);

    if (spenderAllowanceBefore != max_uint256) {
        assert spenderAllowanceAfter == spenderAllowanceBefore - amount;
    }
    else {
        assert spenderAllowanceAfter == spenderAllowanceBefore;
    }
}

Prover 运行结果： 链接

approve()

授权额度的扣除是在 transferFrom() 函数内部进行的，但实际的授权额度设置是在 approve() 函数中完成的。以下是它的实现：

Copy
function approve(address spender, uint256 amount) public virtual returns (bool) {
    allowance[msg.sender][spender] = amount;

    emit Approval(msg.sender, spender, amount);

    return true;
}

allowance 变量是一个公共的嵌套映射（mapping）。因此，Solidity 自动生成了一个 getter 函数，这使得它可以直接在 CVL 中被调用（allowance(e.msg.sender, spender)）：

Copy
rule approve_spenderAllowance(env e) {
    address spender;
    uint256 amount;

    approve@withrevert(e, spender, amount);
    bool isReverted = lastReverted;

    mathint approvedAmountAfter = allowance(e.msg.sender, spender);

    assert !isReverted => approvedAmountAfter == amount;
    assert isReverted <=> e.msg.value != 0;
}

Prover 运行结果： 链接

为了简洁起见，上述规则将成功和回退的情况结合在了一起，使用了蕴含（implication，=>）和双向条件运算符，而不是为每种情况创建单独的规则或使用 if/else 块。

approve() 函数必须在 env e 上下文内被调用，因为它依赖于全局环境变量，例如 msg.sender 和 msg.value。具体来说，该函数使用 msg.sender 来确定是哪个地址在为 spender 设置授权额度：

Copy
function approve(address spender, uint256 amount) public virtual returns (bool) {
    allowance[msg.sender][spender] = amount; // relies on msg.sender
    ...
}

现在来看断言：

• 如果函数调用成功，则授权额度被设置为指定金额。
• 当且仅当 e.msg.value 非零时（这意味着在调用 approve 函数时发送了 ETH），该函数会回退。

Copy
assert !isReverted => approvedAmountAfter == amount;
assert isReverted <=> e.msg.value != 0;

transfer()、transferFrom() 和 approve() 在调用成功时返回 true

除了状态变更操作之外，正如 ERC-20 标准所要求的那样，transfer()、transferFrom() 和 approve() 必须在执行成功时返回 true。

下列规则使用 @withrevert 调用它们各自对应的函数以捕获它们是否回退，将结果存储在 isLastReverted 中，并断言如果调用没有发生回退，它就必须返回 true：

Copy
rule transfer_successReturnsTrue(env e) {
    address receiver;
    uint256 amount;

    bool retVal = transfer@withrevert(e, receiver, amount);
    bool isLastReverted = lastReverted;

    assert !isLastReverted => (retVal == true);
}

rule transferFrom_successReturnsTrue(env e) {
    address holder;
    address receiver;
    uint256 amount;

    bool retVal = transferFrom@withrevert(e, holder, receiver, amount);
    bool isLastReverted = lastReverted;

    assert !isLastReverted => (retVal == true);
}

rule approve_successReturnsTrue(env e) {
    address spender;
    uint256 amount;

    bool retVal = approve@withrevert(e, spender, amount);
    bool isReverted = lastReverted;
    
    assert !isReverted => (retVal == true);
}

Prover 运行结果： 链接

这些规则验证了 transfer()、transferFrom() 和 approve() 在成功调用时会返回 true。

mint()

增加总供应量是铸造（minting）的意图。与此同时，新铸造的代币被分配给接收者，从而增加了他们的余额。下面的 Solidity 实现显示了 totalSupply 和 balanceOf[to] 都增加了 amount：

Copy
function _mint(address to, uint256 amount) internal virtual {
    totalSupply += amount;

    // Cannot overflow because the sum of all user
    // balances can't exceed the max uint256 value.
    unchecked {
        balanceOf[to] += amount;
    }
    ...
}

增加 balanceOf[address] 发生在 unchecked 块内，而增加 totalSupply 发生在 unchecked 块外，受到 Solidity 编译器溢出检查的保护。

由于使用了 unchecked 块，Prover 会探索余额溢出的可能性，即使考虑到余额是与 totalSupply 同步增加的，实际上这并不会发生。为了防止误报，我们添加了前置条件 require totalSupply() >= balanceOf(receiver)。

以下是捕获了总供应量增加以及接收者对应余额增加的 CVL 规则：

Copy
rule mint_increasesTotalSupplyAndBalance() {
    address receiver;
    uint256 amount;

    require totalSupply() >= balanceOf(receiver); // will be replaced by an invariant

    mathint totalSupplyBefore = totalSupply();
    mathint receiverBalanceBefore = balanceOf(receiver);

    mint(receiver, amount);

    mathint totalSupplyAfter = totalSupply();
    mathint receiverBalanceAfter = balanceOf(receiver);

    assert totalSupplyAfter == totalSupplyBefore + amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}

Prover 运行结果： 链接

按照既定模式，我们捕获了 mint() 方法调用前后的状态：

Copy
mathint totalSupplyBefore = totalSupply();
mathint receiverBalanceBefore = balanceOf(receiver);

mint(receiver, amount);

mathint totalSupplyAfter = totalSupply();
mathint receiverBalanceAfter = balanceOf(receiver);

现在来看断言，在这里，总供应量的增加和接收者余额的相应增加均等于 amount：

Copy
assert totalSupplyAfter == totalSupplyBefore + amount;
assert receiverBalanceAfter == receiverBalanceBefore + amount;

mint() 回退

当且仅当总供应量和铸造金额之和超过 max_uint256 时，mint() 函数将回退。这代表了一种溢出场景。以下是捕获此行为的 CVL 规则：

Copy
rule mint_reverts() {
    address receiver;
    uint256 amount;

    mathint totalSupply = totalSupply();

    mint@withrevert(receiver, amount);
    bool isReverted = lastReverted;

    assert isReverted <=> totalSupply + amount > max_uint256;
}

Prover 运行结果： 链接

burn()

铸造（minting）增加了总供应量，而销毁（burning）的意图则是减少它。每一次销毁操作都会同时减少总供应量和代币拥有者的余额。

以下是实现：

Copy
function _burn(address from, uint256 amount) internal virtual {
    balanceOf[from] -= amount;

    // Cannot underflow because a user's balance
    // will never be larger than the total supply.
    unchecked {
        totalSupply -= amount;
    }

    emit Transfer(from, address(0), amount);
}

以下是捕获了总供应量减少以及代币拥有者余额对应减少的规则：

Copy
rule burn_decreasesTotalSupplyAndBalance() {
    address holder;
    uint256 amount;
			
	require totalSupply() >= balanceOf(holder); // will be replaced by an invariant
		
    mathint holderBalanceBefore = balanceOf(holder);
    mathint totalSupplyBefore = totalSupply();

    burn(holder, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint totalSupplyAfter = totalSupply();

    assert holderBalanceAfter == holderBalanceBefore - amount;
    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Prover 运行结果： 链接

在 _burn() 函数中，操作 totalSupply -= amount 是在 unchecked 块内的。因此，Prover 会探索下溢（underflow）的可能性，即使它实际上并不会发生。为了防止这种情况，我们在规则中添加了前置条件 require totalSupply() >= balanceOf(holder)。

对于其余代码，模式与 mint() 类似，只不过余额和总供应量都减少了指定的数量，这正如销毁时的预期。

burn() 回退

当且仅当 holder 的余额小于要销毁的金额时，burn() 函数将回退。这是由 Solidity 强制执行的安全检查，当 balanceOf[from] -= amount（在 unchecked 块外执行）尝试减去超过可用余额的值时就会触发回退。

以下是验证此行为的 CVL 规则：

Copy
rule burn_reverts(env e) {
	address holder;
	uint256 amount;

	mathint holderBalance = balanceOf(holder);

	burn@withrevert(holder, amount);
	bool isReverted = lastReverted;

	assert isReverted <=> holderBalance < amount;
}

Prover 运行结果： 链接

2. transfer、transferFrom、mint 和 burn 的意外副作用

在验证了函数在成功和回退场景下的正确行为之后，我们现在验证对于未参与的各方是否没有意外的副作用或状态变更。

一个函数可能会意外地导致未参与该操作的账户的存储发生变化。对于此合约，我们通过形式化验证来确保没有未参与账户的余额会被 transfer()、transferFrom()、mint() 或 burn() 修改。

每一条规则都遵循相同的模式：我们指定一个地址作为未参与的（通过 require 语句），捕获它在操作之前的余额，执行函数，然后断言该余额保持不变。这就证明了只有作为参数显式传递的账户才会受到影响：

Copy
rule noUninvolvedBalancesAreAffectedByDirectTransfer(env e) {
    address receiver;
    address other;
    uint256 amount;

    require other != receiver;
    require other != e.msg.sender;

    mathint otherBalanceBefore = balanceOf(other);
    transfer(e, receiver, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByTransferFrom(env e) {
    address holder;
    address receiver;
    address other;
    uint256 amount;

    require other != receiver;
    require other != holder;

    mathint otherBalanceBefore = balanceOf(other);
    transferFrom(e, holder, receiver, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByMint() {
    address account;
    address other;
    uint256 amount;

    require account != other;

    mathint otherBalanceBefore = balanceOf(other);
    mint(account, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

rule noUninvolvedBalancesAreAffectedByBurn() {
    address account;
    address other;
    uint256 amount;

    require account != other;

    mathint otherBalanceBefore = balanceOf(other);
    burn(account, amount);

    mathint otherBalanceAfter = balanceOf(other);
    assert otherBalanceAfter == otherBalanceBefore;
}

Prover 运行结果： 链接

3. 不变量

既然我们已经验证了成功和回退的路径，并且确保没有意外的副作用发生，我们可以继续讨论不变量 —— 这是指无论调用哪个函数，使用什么参数，或者按顺序进行多少次有效调用，都必须始终成立的条件。

余额之和必须等于总供应量

在任何情况下，所有余额的总和都不应与总供应量存在差异，因为任何背离都意味着代币在 mint() 或 burn() 之外被创建或销毁了 —— 要么给了用户比实际存在更多的代币，要么导致代币从系统中消失。下面的 CVL 规范对这个不变量进行了形式化验证：

Copy
ghost mathint g_sumOfBalances {
    init_state axiom g_sumOfBalances == 0;
}

hook Sstore balanceOf[KEY address account] uint256 newBalance (uint256 oldBalance) {
    g_sumOfBalances = g_sumOfBalances + newBalance - oldBalance;
}

hook Sload uint256 balance balanceOf[KEY address account] { 
    require g_sumOfBalances >= balance;
}

invariant totalSupplyEqualsSumOfBalances()
	to_mathint(totalSupply()) == g_sumOfBalances;

Prover 运行结果： 链接

我们进一步讨论一下。

第一个代码块声明了一个 ghost（幽灵）变量 g_sumOfBalances 为 mathint 类型，并将其初始化为零。如果没有这种初始化，Prover 会为其分配任意的初始值，这可能会导致误报违规：

Copy
ghost mathint g_sumOfBalances {
    init_state axiom g_sumOfBalances == 0;
}

接下来，这是 Sstore hook，在这里使用 ghost 变量 g_sumOfBalances 来存储和跟踪总账户余额的变化：

Copy
hook Sstore balanceOf[KEY address account] uint256 newBalance (uint256 oldBalance) {
    g_sumOfBalances = g_sumOfBalances + newBalance - oldBalance;
}

下面的 Sload hook 对余额的读取进行了约束，以防止 Prover 分配大于被跟踪的余额之和的值：

Copy
hook Sload uint256 balance balanceOf[KEY address account] { 
    require g_sumOfBalances >= balance;
}

最后，我们形式化验证总供应量等于所有余额的总和：

Copy
invariant totalSupplyEqualsSumOfBalances()
	to_mathint(totalSupply()) == g_sumOfBalances;

requireInvariant —— 以不变量作为前置条件

totalSupplyEqualsSumOfBalances 不变量不仅可作为通用的属性来使用，我们还依赖它作为已被证明的假设来代替前置条件。

除了总供应量等于所有余额之和这个明显的含义之外，不变量 totalSupply() == g_sumOfBalances 还意味着：

• 总供应量始终大于或等于任何单独的余额。
• 总供应量和余额总和都保持在 max_uint256 以内。

回顾早些时候的 transfer 和 transferFrom 规则中包含了一个前置条件，要求余额保持在 max_uint256 以内。这本可能会隐藏一个溢出错误，因为该前置条件假设并约束了余额，这可能会在无意中过滤掉该错误可能出现的状态。

因此，使用经过验证的不变量 totalSupplyEqualsSumOfBalances 作为前置条件更加安全，因为它确保了该规则是在“所有”可达状态下都成立的属性环境中执行的。

现在我们将 require 语句替换为 requireInvariant totalSupplyEqualsSumOfBalances，如下所示：

Copy
rule transfer_effectOnBalances_requireInvariant(env e) {
    address receiver;
    uint256 amount;

    // previously: `require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256`
    requireInvariant totalSupplyEqualsSumOfBalances();
    
    mathint senderBalanceBefore = balanceOf(e.msg.sender);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transfer(e, receiver, amount);

    mathint senderBalanceAfter = balanceOf(e.msg.sender);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != e.msg.sender) {
        assert senderBalanceAfter == senderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert senderBalanceAfter == senderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

rule transferFrom_effectOnBalances_requireInvariant(env e) {
    address holder;
    address receiver;
    uint256 amount;

    // previously: `require balanceOf(e.msg.sender) + balanceOf(receiver) <= max_uint256`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint holderBalanceBefore = balanceOf(holder);
    mathint receiverBalanceBefore = balanceOf(receiver);

    transferFrom(e, holder, receiver, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint receiverBalanceAfter = balanceOf(receiver);

    if (receiver != holder) {
        assert holderBalanceAfter == holderBalanceBefore - amount;
        assert receiverBalanceAfter == receiverBalanceBefore + amount;
    } 
    else {
        assert holderBalanceAfter == holderBalanceBefore;
        assert receiverBalanceAfter == receiverBalanceBefore;
    }
}

此外，burn 和 mint 规则分别包含了一个前置条件，要求总供应量分别大于或等于 holder 和 receiver 的余额。这个 require 前置条件是一个假定的约束，为了安全起见，我们将其替换为已被证明的不变量。

因为 invariant totalSupplyEqualsSumOfBalances 也暗示了总供应量大于或等于所有单独的余额，我们可以将 require 前置条件替换为 requireInvariant totalSupplyEqualsSumOfBalances：

Copy
rule mint_increasesTotalSupplyAndBalance_requireInvariant() {
    address receiver;
    uint256 amount;

    // previously: `require totalSupply() >= balanceOf(receiver)`
    requireInvariant totalSupplyEqualsSumOfBalances();

    mathint totalSupplyBefore = totalSupply();
    mathint receiverBalanceBefore = balanceOf(receiver);

    mint(receiver, amount);

    mathint totalSupplyAfter = totalSupply();
    mathint receiverBalanceAfter = balanceOf(receiver);

    assert totalSupplyAfter == totalSupplyBefore + amount;
    assert receiverBalanceAfter == receiverBalanceBefore + amount;
}


rule burn_decreasesTotalSupplyAndBalance_requireInvariant() {

    address holder;
    uint256 amount;

    // previously: `require totalSupply() >= balanceOf(holder)`
    requireInvariant totalSupplyEqualsSumOfBalances(); 

    mathint holderBalanceBefore = balanceOf(holder);
    mathint totalSupplyBefore = totalSupply();

    burn(holder, amount);

    mathint holderBalanceAfter = balanceOf(holder);
    mathint totalSupplyAfter = totalSupply();

    assert holderBalanceAfter == holderBalanceBefore - amount;
    assert totalSupplyAfter == totalSupplyBefore - amount;
}

Prover 运行结果： 链接

4. 未经授权的操作 —— 不被允许改变状态的方法和调用者

这将验证某些状态变化或操作绝不能发生在被显式允许的函数或调用者之外。

只有特定方法可以改变存储 / 状态

让我们从这条属性开始：“只有 mint() 和 burn() 可以改变总供应量。”

下面的规则是一个参数化规则（参见“参数化规则简介”一章），其中可以任意调用函数（通过 f(e, args)），但只有 mint() 和 burn() 被允许改变 totalSupply。这是由以下断言强制执行的，其中 totalSupplyAfter != totalSupplyBefore 蕴含（=>）了只有这两个函数可能会引发这种改变：

Copy
rule onlyMethodsCanChangeTotalSupply(env e, method f, calldataarg args) {
    mathint totalSupplyBefore = totalSupply();

    f(e, args);
    mathint totalSupplyAfter = totalSupply();

    assert totalSupplyAfter != totalSupplyBefore => (
        f.selector == sig:mint(address,uint256).selector ||
        f.selector == sig:burn(address,uint256).selector
    );
}

虽然这断言了允许哪些函数修改 totalSupply，但同时也意味着所有其他函数均无权执行此操作。

此类别中的其余规则如下所示，遵循相同的模式：

• 只有 mint()、burn()、transfer() 和 transferFrom() 可以改变账户余额：

  Copy
  rule onlyMethodsCanChangeAccountBalances(env e, method f, calldataarg args) {
      address account;
      mathint balanceBefore = balanceOf(account);
      
      f(e, args);
      mathint balanceAfter = balanceOf(account);
  
      assert balanceBefore != balanceAfter => (
          f.selector == sig:transfer(address,uint256).selector ||
          f.selector == sig:transferFrom(address,address,uint256).selector ||
          f.selector == sig:mint(address,uint256).selector ||
          f.selector == sig:burn(address,uint256).selector
      );
  }
  

• 只有 approve() 和 transferFrom() 可以改变授权额度：

  Copy
  rule onlyMethodsCanChangeAllowance(env e, method f, calldataarg args) {
      address holder;
      address spender;
  
      mathint allowanceBefore = allowance(holder, spender);
  
      f(e, args);
      mathint allowanceAfter = allowance(holder, spender);
  
      assert allowanceAfter != allowanceBefore => (
          f.selector == sig:approve(address,uint256).selector ||
          f.selector == sig:transferFrom(address,address,uint256).selector
      );
  }
  

现在我们已经写好了用来验证哪些方法可以修改状态的规则，接下来我们可以编写用来验证哪些调用者被允许减少 holder 余额的规则了。

只有 holders 和 spenders 可以减少 holder 的余额

另一种未授权的操作是当调用者并非 holder 也不是已被批准的 spender 时，去减少某个余额。下面的规则验证了此属性：

Copy
rule onlyHolderAndSpenderCanReduceHolderBalance(env e, method f, calldataarg args) filtered {
	// `burn()` is excluded since permission checks are left to the integrator / developer
    f -> f.selector != sig:burn(address,uint256).selector                                                   
} {
    requireInvariant totalSupplyEqualsSumOfBalances(); 

    address account;

    mathint spenderAllowanceBefore = allowance(account, e.msg.sender);
	mathint holderBalanceBefore = balanceOf(account);
    
    f(e, args);
	mathint holderBalanceAfter = balanceOf(account);

    assert (holderBalanceAfter < holderBalanceBefore) => (
        e.msg.sender == account ||
        holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)
    );
}

下面这行声明了我们在参数化调用中排除了 burn() 函数：

Copy
f -> f.selector != sig:burn(address,uint256).selector

过滤掉 burn() 的原因正如前面所提到的，它是故意不设权限检查的。如果将其包含在规则中，将会导致规则失败，因为任何调用者都可以减少一个 holder 的余额，这就破坏了该规则的设计意图。

我们已经在不变量一节中讲解过 requireInvariant 了，并且也熟悉了在先前章节中方法调用前后的状态记录，因此我们可以直接跳到断言部分。

下面的断言意味着如果 holder 的余额减少了，那必定是由于以下两个原因之一：

• e.msg.sender == account

  holder 发起了该操作，或者

• holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)

  减少的金额在被批准的授权额度限制范围之内，这也意味着调用者是一个具有非零授权额度的被批准的 spender。

Copy
assert (holderBalanceAfter < holderBalanceBefore) => (
    e.msg.sender == account ||
    holderBalanceBefore - holderBalanceAfter <= to_mathint(spenderAllowanceBefore)
);

这条特定规则是 OpenZeppelin onlyAuthorizedCanTransfer 的修改版本。变化在于，原始规则在断言中包含了 sig:burn(address,uint256).selector，而在这条 onlyHolderAndSpenderCanReduceHolderBalance 规则中，我们将其过滤（filtered）掉了。

这是本节中所有规则的 Prover 运行结果。

ERC-20 的完整 CVL 规范

这是完整的 CVL 规范和 Prover 运行结果。

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