简介

在“Storage Hook 和 Ghost 简介”一章中，我们介绍了在简单存储变量中使用的 Storage Hook 和 Ghost。我们展示了 Hook 能够跟踪那些无法通过 public 或 external 方法直接访问的存储变量。我们还演示了，当某些数量没有被显式存储，但在规范推理中又是必需的时，结合 Hook 和 Ghost 变量可以用来计算并持久化这些值。

如果这些变量是 public 或可以从外部访问的，它们的值就可以在 CVL 中直接调用并被轻松读取，从而允许根据需要计算任何派生量。

然而，映射（Mapping）是不同的。它们是不可枚举的——要访问一个值，必须已经知道它的键（key），而且没有内置的方法可以从映射中检索出“所有键”或“所有值”。

这种限制给验证带来了巨大挑战：许多重要的合约属性需要对映射的所有条目进行推理。由于我们无法直接枚举或检查所有键，我们需要一种机制来跟踪映射发生时的变化。

在本章中，我们将 Sstore Hook 的使用范围扩展到整数、地址和布尔值之外，并将其应用于存储映射——由于许多合约严重依赖映射，这在规范中是一种常见模式。

映射的 Sstore Hook 语法

在继续进行代码演示之前，我们先来学习一下映射的 Sstore Hook 的代码语法与模式。

Sstore hook — 捕获新值和旧值

以下是用于捕获存储映射新值和旧值的 Sstore Hook 语法：

Copy
hook Sstore balances[KEY address user] uint256 newVal (uint256 oldVal) {
    // Implement hook logic for the balances mapping where:
		// - KEY is `user`
		// - old (previous) value is `oldVal`
		// - new (current) value is `newVal`
}

每当写入映射值时，旧值和新值都可以被捕获。

例如，要验证用户的余额增加不超过 10，我们会计算新旧余额之间的差值，并将结果赋给 Ghost 变量 g_balanceDelta：

Copy
ghost mathint g_balanceDelta;


hook Sstore balances[KEY address user] uint256 newVal (uint256 oldVal) {
    g_balanceDelta = newVal - oldVal;
}

Hook 会计算差值（newVal - oldVal）并将其存储在 Ghost 变量 g_balanceDelta 中，该变量表示在这次存储更新期间用户余额变化了多少。

然后，g_balanceDelta 的值即可用于验证变化限制。例如：

Copy
rule deltaNotMoreThan10() {
    ...
    assert g_balanceDelta <= 10;
}

Sstore hook — 仅捕获新值

我们可以选择仅捕获新值而省略旧值，因为后者是可选的：

Copy
hook Sstore balances[KEY address user] uint256 newVal {
	// implement hook logic
}

这主要用于简单地设置存储，且在验证逻辑中不需要计算差值（变化量）的情况。

例如，如果我们想要推理证明用户的余额不超过 2000，我们只需要捕获 newVal 并将其赋给 Ghost 变量即可：

Copy
ghost mathint g_balance;


hook Sstore balances[KEY address user] uint256 newVal {
	g_balance = newVal;
}

然后，g_balance 的值即可用于验证余额是否保持在定义的限制范围内。例如：

Copy
rule balanceDoesNotExceed2000() {
	...
	assert g_balance <= 2000;
}

如果没有 Sstore Hook，跟踪映射中的所有键和值是不可能的

为了理解为什么在验证涉及映射的属性时需要使用 Hook，让我们从一个简单的合约 PointSystem 开始，它的功能如下：

• 为特定用户增加积分并增加总积分。
• 在映射 pointsOf[address] 中保存每个用户的记录。
• 在变量 totalPoints 中跟踪总体总数。

Copy
contract PointSystem {
    mapping (address => uint256) public pointsOf;
    uint256 public totalPoints;

    function addPoints(address _user, uint256 _amount) external {
        pointsOf[_user] += _amount;
        totalPoints += _amount;
    }
}

现在，让我们验证这个属性：“各个用户的积分总和等于总积分。”

如果不使用 Sstore Hook，一种方法是处理有限数量的用户（例如，两个用户）。我们直接从映射 pointsOf 读取他们的余额，将他们的积分相加，并断言这个总和等于 totalPoints。

下面的规则演示了这种方法，其中 totalPoints 和所有的 pointsOf 值都从零开始：

Copy
rule sumOfUserPointsEqualsTotalPoints() {
    address account1; address account2; 
    uint256 amount1; uint256 amount2;   

    require account1 != account2;
    require pointsOf(account1) == 0 && pointsOf(account2) == 0; // points per user starts at zero
    require totalPoints() == 0; // total starts at zero

    addPoints(account1, amount1);
    addPoints(account2, amount2);

    assert to_mathint(totalPoints()) == pointsOf(account1) + pointsOf(account2);
}

在这次 Prover 运行中，我们看到该属性得到了验证：

Prover 运行结果：link

通过仅使用两个用户断言相等性（即使通过声明额外的账户变量手动添加了更多用户），该属性也被局限于那一部分账户子集中。这并不是我们想要验证的确切属性，因为映射中可能还存在许多其他用户，而他们的积分被排除在检查之外。

现在，让我们改进这个规则。通过移除前提条件 require pointsOf(account1) == 0 && pointsOf(account2) == 0 以及 require totalPoints() == 0，让 totalPoints 和用户积分（pointsOf[address]）从任意值（而不是零）开始。

然后，我们在 addPoints() 方法调用前后分别记录 totalPoints 和 pointsOf[address] 的值。这样做允许我们计算由该调用引起的差值，并确定每个变量发生了多少变化。

最后，我们断言总积分（totalPointsAfter）等于初始总积分（totalPointsBefore）加上 account1 和 account2 积分变化的综合。这种调整使得无论初始状态如何，规则都能正常工作：

Copy
rule sumOfUserPointsEqualsTotalPoints_modified() {
    address account1; address account2;
    uint256 amount1; uint256 amount2;

    require account1 != account2;

    // Capture the state BEFORE the method call
    mathint totalPointsBefore = totalPoints();
    mathint pointsOfAccount1Before = pointsOf(account1);
    mathint pointsOfAccount2Before = pointsOf(account2);

    // Method call
    addPoints(account1, amount1);
    addPoints(account2, amount2);

    // Capture the state AFTER the method call
    mathint totalPointsAfter = totalPoints();
    mathint pointsOfAccount1After = pointsOf(account1);
    mathint pointsOfAccount2After = pointsOf(account2);

    // Calculate how much each account's points changed
    mathint deltaPointsOfAccount1 = pointsOfAccount1After - pointsOfAccount1Before;
    mathint deltaPointsOfAccount2 = pointsOfAccount2After - pointsOfAccount2Before;

    // Assertion: The total points equal the initial total plus the changes in the points of account1 and account2
    assert totalPointsAfter == totalPointsBefore + deltaPointsOfAccount1 + deltaPointsOfAccount2;
}

Prover 运行结果：link

即使有了这种规则上的改进，它也没有准确地反映该属性，因为它只考虑了两个特定用户而忽略了映射中的所有其他用户。它仅仅证明了用户的某个子集与总数是一致的。

如果没有 Sstore Hook，哪怕映射可以从外部访问，跟踪所有用户的积分也是不可能的。

使用 Sstore Hook 来枚举存储映射值

每次合约向 pointsOf[address] 写入数据时，Sstore Hook 都会捕获新值和旧值，这使得它能够计算差值（变化量）并将其赋给 Ghost 变量。我们不需要直接（从合约）查询映射以获取所有可能的键，而是维护一个 Ghost 变量追踪器，在每次发生存储写入时将其记录下来。

让我们来实现 Sstore Hook 的逻辑。如前所述，我们捕获旧值和新值，计算差值（变化量）并将其添加到一个 Ghost 变量中以记录总积分。我们将这个 Ghost 变量声明为 g_sumOfUserPoints：

Copy
ghost mathint g_sumOfUserPoints;

hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}

既然各个用户积分的总和在 Ghost 变量 g_sumOfUserPoints 中变得可量化了，下一步就是在规则或不变式（invariant）中使用它，以检查此追踪器是否始终等于合约的存储变量 totalPoints。

规则与不变式中的 Ghost

Ghost 既可用于规则中，也可用于不变式中。在以下示例中，我们将验证 totalPoints（存储变量）等于 g_sumOfUserPoints（Ghost 变量），后者的值是在 Sstore Hook 中追踪和计算出来的。

将验证 totalPoints() 等于 g_sumOfUserPoints 作为一个规则

下面是参数化形式的规则，其中 f(e, args) 允许 Prover 验证带有任意参数的所有合约函数的规则。对于以下规则，我们要求 totalPoints 和 g_sumOfUserPoints 从零开始：

Copy
rule sumOfUserPointsEqualsTotalPoints(env e, method f, calldataarg args) {
    require totalPoints() == 0 && g_sumOfUserPoints == 0;

    f(e, args);
    assert totalPoints() == g_sumOfUserPoints;
}

Prover 运行结果：link

或者，我们可以允许 totalPoints 和 g_sumOfUserPoints 从任意值开始，只要它们从相同的值开始即可：

Copy
rule sumOfUserPointsEqualsTotalPoints_alt(env e, method f, calldataarg args) {
    require totalPoints() == g_sumOfUserPoints; // starts at any value, as long as they start at the same value
																						    
    f(e, args);
    assert totalPoints() == g_sumOfUserPoints;
}

Prover 运行结果（已验证）：link

将验证 totalPoints() 等于 g_sumOfUserPoints 作为一个不变式

为了以归纳的方式（基本情况和归纳步骤）验证同一属性，我们将其写为一个 CVL 不变式（invariant）。Ghost 被初始化为零，并且在这里应用了上一条规则中相同的 Sstore Hook：

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

hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}

invariant sumOfUserPointsEqualsTotalPoints_inv() 
    totalPoints() == g_sumOfUserPoints;

Prover 运行结果（已验证）：link

当在 CVL 不变式中使用 Ghost 时，必须使用 init_state axiom 初始化它们以设置正确的起始值——在本例中，g_sumOfUserPoints 为零。

由于每个用户的积分都从零开始，因此所有用户积分的总和（g_sumOfUserPoints）也从零开始。这很重要，因为作为归纳过程的一部分，不变式会检查该属性在基本情况（就在构造函数之后）是否成立。

当我们之前作为规则来验证这个属性时，我们测试了两者都从零开始的情况，以及从非零（但相等）值开始的情况。而作为不变式时，我们只测试两者都从零开始的情况。

原因是，不变式必须在构造函数（基本情况）之后立即开始测试，此时未初始化的存储变量默认值为零。这意味着不变式只有在构造函数显式设置了非零值的情况下，才能从非零值开始。然而，规则可以假设任意起始状态——可以是零或非零。

总结

• 在证明涉及不断变化的值的属性时，对于映射使用 Sstore Hook 是不可避免的。它通过监视存储槽位并为映射键捕获新旧值，解决了枚举难题。
• 如果没有 Sstore Hook，属性就只能针对手动查询的一组有限的键进行证明，而无法直接监视存储。
• 在规则中，Ghost 变量的初始值使用 require 语句进行约束。
• 在不变式中，Ghost 变量使用 init_state 公理（axiom）进行初始化。

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