Nonces（代表“只使用一次的数字”）用于数字签名方案中以防止重放攻击。为了本文的讨论，我们假设读者已经熟悉什么是 nonces 以及它们的用法。

OpenZeppelin nonces.sol 库通过使用一个为每个地址递增的计数器来跟踪签名者的 nonces。以下是完整的库代码（为了简洁起见去除了注释）：

Copy
abstract contract Nonces {

    error InvalidAccountNonce(address account, uint256 currentNonce);

    mapping(address account => uint256) private _nonces;

    function nonces(address owner) public view virtual returns (uint256) {
        return _nonces[owner];
    }

    function _useNonce(address owner) internal virtual returns (uint256) {
        unchecked {
            return _nonces[owner]++;
        }
    }

    function _useCheckedNonce(address owner, uint256 nonce) internal virtual {
        uint256 current = _useNonce(owner);
        if (nonce != current) {
            revert InvalidAccountNonce(owner, current);
        }
    }
}

简而言之，该合约的功能如下：

• nonces(address owner) 是一个视图函数，返回 owner 的当前 nonce。
• _useNonce(address owner) 为 owner 递增 nonce 并返回递增前的 nonce 值。例如，如果 Alice 的 nonce 是 2，我们为她的账户调用 _useNonce，那么 _useNonce 会返回 2，但在函数执行后她当前的 nonce 会变成 3。
• _useCheckedNonce(address owner, uint256 nonce) 会递增 nonce，但除非 nonce 参数等于当前的 nonce，否则会发生 revert。例如，如果 Alice 的 当前 nonce 是 15，那么为 nonce 参数提供除 15 之外的任何值都会导致 revert。函数调用后，Alice 的 nonce 将变为 16。

这与我们在教程前面使用的 Counter 示例并没有太大区别，因此 Certora 为这个库编写的规则将会很容易解释。

以下是将要证明的一些属性：

• nonce 只能递增
• 递增 nonce 永远不会失败
• 递增一个 nonce 对其他 nonce 没有影响

Nonces.sol Spec

这是 Certora 为 nonces.sol 编写的 spec。

辅助函数

该 spec 包含一个辅助 CVL 函数，用于检查 nonce 不是 uint256 的最大值。在实践中，计数器不可能达到那么高：

Copy
function nonceSanity(address account) returns bool {
    return nonces(account) < max_uint256;
}

Nonce 只能递增

我们将从最简单的规则开始，因为我们在参数化规则（parametric rules）一章中看到过类似的内容：

Copy
// address account in the argument is equivalent to
// declaring it inside the function body
rule nonceOnlyIncrements(
address account)
 {
    require nonceSanity(account);

    mathint nonceBefore = nonces(account);

    env e; method f; calldataarg args;
    f(e, args);

    mathint nonceAfter = nonces(account);

    assert nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1, "nonce only increments";
}

该规则表示“所有交易要么导致 nonce 不变，要么正好增加 1。”

useNonce 规则

useNonce 规则作出了两个断言：

• 调用 useNonce() 永远不会 revert
• 递增 account A 上的 nonce 不会影响所有其他账户，即它们的 nonce 不会改变。

Copy
rule useNonce(address account) {
    require nonceSanity(account);

    address other;

    mathint nonceBefore = nonces(account);
    mathint otherNonceBefore = nonces(other);

    mathint nonceUsed = useNonce@withrevert(account);
    bool success = !lastReverted;

    mathint nonceAfter = nonces(account);
    mathint otherNonceAfter = nonces(other);

    // liveness
    assert success, "doesn't revert";

    // effect
    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
}

让我们逐个部分进行解释：

Copy
require nonceSanity(account);

这段代码确保 prover 不会去测试 nonce 为 type(uint256).max 这种（不可能的）情况。

Copy
address other;

这个 other 是我们获取对除规则参数中指定的 account 之外的“任何其他账户”的引用的方式。请注意，该规则并不要求将 account != other 作为前置条件——这会在后面处理。

Copy
mathint nonceBefore = nonces(account);
mathint otherNonceBefore = nonces(other);

这会在状态转换之前读取 account 和 other 的 nonce 值。

Copy
mathint nonceUsed = useNonce@withrevert(account);
bool success = !lastReverted;

mathint nonceAfter = nonces(account);
mathint otherNonceAfter = nonces(other);

代码 mathint nonceUsed = useNonce@withrevert(account); 是关键行，因为 nonce 在这里被递增了。我们将新的 nonce 状态记录在 nonceAfter 和 otherNonceAfter 中。

现在让我们看看断言部分：

Copy
// liveness
    assert success, "doesn't revert";

    // effect
    assert nonceAfter == nonceBefore + 1 && nonceBefore == nonceUsed, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";

回想一下，useNonce 函数会返回刚刚消耗的 nonce，因此断言为 nonceBefore == nonceUsed。

最终的断言声明没有其他 nonce 发生改变。它的逻辑可以使用逆否法则（contrapositive rule）推导出来。

根据蕴含的逆否法则，如果 A → B，那么 !B → !A。假设 A 表示 other ≠ account，B 表示 otherNonceBefore = otherNonceAfter。那么我们可以说“如果 other 不等于 account，那么 other 的 nonce 就没有改变”。因此，我们可以写出 other ≠ account 蕴含 otherNonceBefore = otherNonceAfter，或者换句话说 A → B。利用逆否法则，我们可以得出 !B → !A，等价地也就是 otherNonceBefore ≠ otherNonceAfter（发生了改变）蕴含 other = account，而这正是最后一个断言所声明的。

useCheckedNonce 规则

最后一条规则重用了前面示例中的大量逻辑，我们在此不再赘述。主要区别在于这行代码：assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";。回想一下，只有当传递给它的 nonce 等于用户的当前 nonce 时，useCheckedNonce 才会成功（不会发生 revert）。因此，双条件运算符（biconditional operator）编码的逻辑是：“如果 nonce 匹配，则保证交易成功。如果不匹配，则保证 revert。”

Copy
rule useCheckedNonce(address account, uint256 currentNonce) {
    require nonceSanity(account);

    address other;

    mathint nonceBefore = nonces(account);
    mathint otherNonceBefore = nonces(other);

    useCheckedNonce@withrevert(account, currentNonce);
    bool success = !lastReverted;

    mathint nonceAfter = nonces(account);
    mathint otherNonceAfter = nonces(other);

    //// SEE HERE ////
    // liveness
    // the to_mathint cast makes it explicit to have the same type on both sides
    assert success <=> to_mathint(currentNonce) == nonceBefore, "works iff current nonce is correct";

    // effect
    assert success => nonceAfter == nonceBefore + 1, "nonce is used";

    // no side effect
    assert otherNonceBefore != otherNonceAfter => other == account, "no other nonce is used";
}

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