到目前为止，我们要么编写 规则 (rule) 来验证特定行为，要么编写 不变量 (invariant) 来验证在合约整个生命周期中必须始终成立的属性。然而，在验证新属性时，我们通常希望假设我们已经证明过的其他属性继续保持成立。
例如，在验证代币转账的规则时，我们可能希望假设总供应量仍然等于所有余额的总和——这是一个已经由单独的不变量证明过的属性。使用已证明的不变量作为假设，可以防止规则因为不切实际的合约状态（即违反了我们已证明永远不会发生之属性的状态）而验证失败。
这就是 CVL 的 requireInvariant 语句发挥作用的地方。requireInvariant 语句允许我们采用已经证明过的不变量，并在验证新规则或不变量时将其用作假设。
在本章中，我们将探讨什么是 requireInvariant，为什么它很有用，以及在 CVL 中编写规则和不变量时如何有效地应用它。
理解 requireInvariant 语句
requireInvariant 语句是一个 CVL 构造，它允许我们将已证明的不变量作为附加条件注入到规则或另一个不变量中。
requireInvariant 是如何工作的
当规则或另一个不变量中包含 requireInvariant 语句时，Prover 会在验证过程中自动假设所引用的不变量已经为真。因此，它只会探索满足此条件的那些合约状态。
在规则和不变量中使用 requireInvariant
要在 规则 中使用 requireInvariant，只需在规则的开头通过名称引用该不变量即可：
rule ruleName(env e, ...) {
requireInvariant invariantName();
// rule logic here
}
当在 不变量（而不是规则）内部使用 requireInvariant 时，语法会有所不同。该语句会被放置在一个 preserved 块中，如下所示：
invariant invariantName()
conditionExpression;
{
preserved with (env e) {
requireInvariant otherInvariantName();
}
}
现在我们已经了解了 requireInvariant 语句的用途以及它如何帮助我们重用已证明的不变量，接下来让我们看看它在实践中是如何工作的。
回顾 totalSupplyEqSumOfBalances() 不变量
在处理 ERC20 代币时，最基本的安全检查之一是确保 所有余额的总和始终等于代币的总供应量。这个通常被称为 代币完整性 (token integrity) 的不变量，保证了代币不会被无意中创建或销毁，并且所有个人余额的总和等于总供应量。
在名为 “使用 Ghosts 和 Hooks 验证不变量” 的章节中，我们使用以下规范，形式化验证了 Transmission11的 Solmate 库中 ERC20 实现的这一关键安全属性：
methods {
function totalSupply() external returns(uint256) envfree;
}
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sload uint256 balance balanceOf[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount) {
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
让我们看看如何将已证明的 totalSupplyEqSumOfBalances() 不变量作为假设用在另一个规则或不变量中。
在规则中应用 requireInvariant
假设我们想定义一个规则 checkTransferSuccess()，以验证我们 ERC20 合约中 transfer() 函数的正确性。具体来说，我们希望确保一次成功的转账能够正确更新发送方和接收方的余额，同时保持总供应量不变。
为了表达这样一个规则，我们遵循以下步骤：
- 理解
transfer()函数的预期行为。 - 编写一个 CVL 规则来验证此行为。
- 运行验证并观察结果。
正如我们将看到的，最初的验证会失败——这不是因为合约中存在错误，而是因为 Prover 探索了不切实际的状态。这将引导我们引入 requireInvariant 作为解决方案。
让我们将这些步骤付诸实践。
理解 transfer() 函数的预期行为
为了定义 transfer() 成功调用的规范，我们首先来看一下 Solmate 的 ERC20 合约中该函数的实现：
function transfer(address to, uint256 amount) public virtual returns (bool) {
balanceOf[msg.sender] -= amount;
unchecked {
balanceOf[to] += amount;
}
emit Transfer(msg.sender, to, amount);
return true;
}
从上面的代码中，我们可以看到 transfer() 函数将指定数量的代币（amount）从发送方的账户转移到接收方的账户（to）。该函数遵循以下逻辑：
- 如果发送方有足够的代币： 发送方的余额减少
amount，接收方的余额增加相同的数量。 - 如果发送方没有足够的代币： 操作将由于算术下溢而自动回滚，并且不会发生任何状态更改。
在 CVL 中表达我们的 transfer() 调用预期
既然我们已经清楚地了解了 transfer() 函数的预期行为，我们可以按照以下步骤将其转化为 CVL 代码：
- 打开规范文件： 在你的 Certora 项目目录中，导航到 specs 子目录并打开我们为验证
totalSupplyEqSumOfBalances()不变量而创建的erc20.spec文件。该文件应包含以下规范：
methods {
function totalSupply() external returns(uint256) envfree;
}
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sload uint256 balance balanceOf[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount) {
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
- 添加一个规则： 通过添加一个名为
checkTransferCall()的新规则块来扩展erc20.spec文件。
rule checkTransferSuccess() {
// we’ll fill this step by step
}
- 包含环境参数： 由于我们的
transfer()调用需要访问交易环境（如msg.sender和其他 EVM 上下文变量），我们将该环境作为env e类型的参数传入。
rule checkTransferSuccess(env e) {
// we’ll fill this step by step
}
- 声明输入：
transfer()函数需要两个输入：一个接收方****地址和要转账的代币数量。我们在规则中将它们声明为局部变量。
rule checkTransferSuccess(env e){
// NEWLY ADDED //
address to;
uint256 amount;
}
- 向环境添加最小约束： 并非每种输入组合都代表有效的验证场景。例如，我们不希望调用者（
msg.sender）是合约本身，并且我们不希望允许发送方和接收方是同一个账户的转账。我们添加require语句来排除这些无效场景。
rule checkTransferSuccess(env e){
address to;
uint256 amount;
// NEWLY ADDED //
require e.msg.sender != currentContract;
require e.msg.sender != to;
}
- 捕获调用前状态： 在进行
transfer()调用之前，我们记录发送方的余额、接收方的余额以及总供应量。这些值将作为我们在调用后验证状态更改的基准线。
rule checkTransferSuccess(env e){
address to;
uint256 amount;
require e.msg.sender != currentContract;
require e.msg.sender != to;
// NEWLY ADDED //
mathint precallSenderBalance = balanceOf(e.msg.sender);
mathint precallReceiverBalance = balanceOf(to);
mathint precallTotalSupply = totalSupply();
}
- 调用
transfer()函数： 我们现在使用环境e，连同接收方地址to和转账数量amount，来调用transfer()函数。
rule checkTransferSuccess(env e){
address to;
uint256 amount;
require e.msg.sender != currentContract;
require e.msg.sender != to;
mathint precallSenderBalance = balanceOf(e.msg.sender);
mathint precallReceiverBalance = balanceOf(to);
mathint precallTotalSupply = totalSupply();
// NEWLY ADDED //
transfer(e,to,amount);
}
注意：我们在调用 transfer() 时没有使用 @withrevert 修饰符——这意味着规则只验证转账成功执行的情况。如果转账发生回滚（例如由于余额不足），Prover 会直接从验证中排除该路径。
- 捕获调用后状态：在转账执行后，我们再次捕获发送方的余额、接收方的余额以及总供应量，以便我们将它们与我们的预期进行比较。
rule checkTransferSuccess(env e) {
address to;
uint256 amount;
require e.msg.sender != currentContract;
require e.msg.sender != to;
mathint precallSenderBalance = balanceOf(e.msg.sender);
mathint precallReceiverBalance = balanceOf(to);
mathint precallTotalSupply = totalSupply();
transfer@withrevert(e,to,amount);
bool transferCallStatus = lastReverted;
// NEWLY ADDED //
mathint postcallSenderBalance = balanceOf(e.msg.sender);
mathint postcallReceiverBalance = balanceOf(to);
mathint postcallTotalSupply = totalSupply();
}
- 断言结果的正确性： 接下来，我们将预期编码为断言：
- 发送方的余额应准确减少
amount。 - 接收方的余额应准确增加
amount。 - 总供应量应保持不变（转账只是移动代币，并没有创建或销毁代币）。
rule checkTransferSuccess(env e){
address to;
uint256 amount;
require e.msg.sender != currentContract;
require e.msg.sender != to;
mathint precallSenderBalance = balanceOf(e.msg.sender);
mathint precallReceiverBalance = balanceOf(to);
mathint precallTotalSupply = totalSupply();
transfer(e, to, amount);
mathint postcallSenderBalance = balanceOf(e.msg.sender);
mathint postcallReceiverBalance = balanceOf(to);
mathint postcallTotalSupply = totalSupply();
// NEWLY ADDED //
assert postcallSenderBalance == precallSenderBalance - amount;
assert postcallReceiverBalance == precallReceiverBalance + amount;
assert precallTotalSupply == postcallTotalSupply;
}
- 更新 methods 块： 以前，我们的 methods 块仅包含
totalSupply()函数，因为它是规范中唯一被显式调用的函数。现在，我们还需要包含balanceOf()函数，因为我们的规则引用了它来读取账户余额。
methods {
function totalSupply() external returns(uint256) envfree;
function balanceOf(address) external returns(uint256) envfree; // Add this
}
与 totalSupply() 类似，balanceOf() 函数不依赖于交易环境（例如，它不使用 msg.sender 或 msg.value）。因此，我们将其声明为 envfree。
注意： 如果你想知道为什么我们能使用 balanceOf() 函数，尽管它没有出现在合约源码中，答案在于 Solidity 处理 public 状态变量 的方式。当你声明一个如 mapping(address => uint256) public balanceOf; 的变量时，编译器会自动生成一个带有以下签名的 getter 函数：
function balanceOf(address) external view returns (uint256);
这个 getter 是编译后合约接口的一部分，即使它没有显式地写在源代码中。
可选地，我们还可以在 methods 块中包含 transfer() 函数的签名。然而，这样做并不会提高验证性能，因为该函数不是 envfree 的。
methods {
function totalSupply() external returns(uint256) envfree;
function balanceOf(address) external returns(uint256) envfree;
function transfer(address,uint256) external returns(bool);
}
运行初步验证
现在我们的规则 checkTransferSuccess() 已经完成，让我们运行 Prover 看看它是否能通过验证。
要运行验证，请遵循以下说明：
- 确保你的
.conf文件与以下配置匹配：
{
"files": [
"contracts/ERC20.sol:ERC20"
],
"verify": "ERC20:specs/erc20.spec",
"optimistic_loop": true,
"msg": "Testing erc20 functionality"
}
- 接下来，在你的终端中执行以下命令：
certoraRun confs/erc20.conf
这会将你的规范和合约发送给 Certora Prover 进行验证。
- 一旦 Prover 完成运行（可能需要几分钟的时间），它会在终端中输出验证报告的唯一链接。在浏览器中打开该链接，你将看到类似于下图的结果：
结果表明 checkTransferSuccess() 未通过 验证。
理解失败原因
为了理解规则为何失败，让我们检查一下调用跟踪。在 Global State #1 下的 Storage State（存储状态）部分中，我们可以看到 Prover 选择的初始值：
Prover 从具有以下值的状态开始：
Storage State (ERC20):
balanceOf[0x2712]=0x7(7 个代币)balanceOf[0x25fc]=2^256 - 5(一个天文数字)totalSupply=0x6(仅 5 个代币)sumOfBalances=2^256 + 8( Ghost State)
注意每个值右侧的 HAVOC 标签。这表明这些值是由 Prover 任意选取的。
这种不一致性非常明显：一个账户持有 2^256 - 5 个代币，而总供应量却只有 6。另一个账户持有 7 个代币——比总供应量还多出一个。同时，ghost 变量 sumOfBalances 被设置为 2^256 + 8，这与单个账户余额或总供应量没有任何关系。
发生这种情况是因为，Prover 在验证新规则时并不会自动假设我们先前已证明的不变量 totalSupplyEqSumOfBalances() 是成立的。每个规则都从一个全新的符号化状态开始，除非我们显式地约束它们，否则存储变量和 ghost 都会被分配任意值。结果就是，Prover 探索了在真实的 ERC-20 执行中永远不可能发生的状态——在这些状态下，余额、ghost 和总供应量之间的记账关系已经完全崩坏。
当 transfer() 在这些不切实际的条件下执行时，我们关于余额变化的断言就会失败，哪怕合约逻辑本身是正确的。
使用 requireInvariant 修复失败
为了排除这种不一致的状态，我们需要告诉 Prover，只有在假设 totalSupplyEqSumOfBalances() 已经成立的情况下，才应该检查 checkTransferCall()。
我们可以通过在规则的最开始处插入以下代码行来做到这一点：
requireInvariant totalSupplyEqSumOfBalances();
这行代码告诉 Prover 从我们之前的不变量已经为真的状态开始验证。简单来说，Prover 将只在总供应量已经等于所有余额总和的情况下检查该规则。
以下是添加了 requireInvariant 的完整规则：
// Our Rule
rule checkTransferSuccess(env e){
requireInvariant totalSupplyEqSumOfBalances();
address to;
uint256 amount;
require e.msg.sender != currentContract;
require e.msg.sender != to;
mathint precallSenderBalance = balanceOf(e.msg.sender);
mathint precallReceiverBalance = balanceOf(to);
mathint precallTotalSupply = totalSupply();
transfer(e,to,amount);
mathint postcallSenderBalance = balanceOf(e.msg.sender);
mathint postcallReceiverBalance = balanceOf(to);
mathint postcallTotalSupply = totalSupply();
assert postcallSenderBalance == precallSenderBalance - amount;
assert postcallReceiverBalance == precallReceiverBalance + amount;
assert precallTotalSupply == postcallTotalSupply;
}
重新运行验证
现在，让我们在加入 requireInvariant 语句后再次运行 Prover：
certoraRun confs/erc20.conf
打开验证链接以查看结果：
我们的验证结果清楚地表明 Prover 已经成功验证了该规则。这意味着 transfer() 函数能够正确地更新余额并保持总供应量不变量。
上面讨论的例子清楚地表明，添加 requireInvariant 可确保 Prover 只考虑那些遵循已证明的全局属性的、切合实际的合约状态。在下一节中，我们将看到如何在另一个不变量定义中使用 requireInvariant。
在不变量中使用 requireInvariant
为了了解如何在 CVL 的不变量构造内部使用 requireInvariant，让我们在我们的 erc20.spec 文件中定义另一个名为 indBalanceCap() 的不变量（就在 totalSupplyEqSumOfBalances() 不变量的正下方）。
///..
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
// Our new Invariant
invariant indBalanceCap(address a)
to_mathint(balanceOf(a)) <= to_mathint(totalSupply());
//.....
这个新的不变量编码了一个基本的 ERC-20 安全属性：任何账户的余额都不应超过总供应量。
验证我们的新不变量
现在让我们运行 Prover，然后打开 Prover 提供的验证链接，你将看到类似于下图的结果：
上面的结果显示我们的不变量 indBalanceCap() 未通过验证过程。
对 Prover 报告的进一步分析表明，该不变量未通过归纳检查。具体来说，Prover 识别出 transfer() 和 transferFrom() 函数调用违反了该不变量，如下图所示：
为了理解违规的原因，让我们分析一下 transfer() 的调用跟踪。（注意： transferFrom() 因为相同的原因失败，因此分析 transfer() 就涵盖了这两种情况）
理解违规原因
让我们从 Prover 报告的 Storage State（存储状态）部分开始分析。这部分显示了合约的存储变量在验证初始点的实际值。
在存储状态中，我们可以看到各个账户余额如下：
balanceOf[0x2711] = 0x5（账户0x2711持有 5 个代币）balanceOf[0x2713] = 0x4（账户0x2713持有 4 个代币）
同时代币的 totalSupply 仅记录为 0x4（即 4 个代币）。
既然我们已经证明了 totalSupplyEqSumOfBalances() 不变量，像这样的状态就不应该在合约的实际执行过程中发生。该不变量声明，在每一个有效状态下，总供应量必须始终等于所有余额的总和。但在上面的追踪中，余额总和为 9，而总供应量仅为 4。这种不匹配表明，Prover 从一个在我们的 ERC-20 实现中实际上不可达的状态开始了验证。
发生这种情况是因为，Prover 在开始验证新属性时_并不_会自动假设之前证明过的不变量应该成立。除非我们显式地将其与先前的结果联系起来，否则每个新规则或不变量都从一个全新的符号化状态开始。结果，Prover 可能会选择一个违反我们之前证明过的不变量的初始配置，即便这种配置在实际的合约执行期间是不可能出现的。
使用 requireInvariant 语句修复失败
为了排除这种不一致的状态，我们需要告诉 Prover，只有在假设 totalSupplyEqSumOfBalances() 已经成立的情况下，才应该检查 indBalanceCap()。
为了强制执行这一点，我们使用 requireInvariant 显式导入该不变量，如下所示：
invariant indBalanceCap(address a)
to_mathint(balanceOf(a)) <= to_mathint(totalSupply())
{
preserved with (env e) {
// Require that our earlier invariant holds
requireInvariant totalSupplyEqSumOfBalances();
}
}
这样一来，Prover 就会从一个已经满足我们之前证明的代币守恒规则的世界开始，从而防止搜索空间漂移到不可能出现的 ERC-20 状态中。
验证增强后的不变量
现在，如果我们重新运行 Prover：
certoraRun confs/erc20.conf
并打开验证链接，我们将看到类似于下图的结果：
正如预期的那样，我们可以看到 indBalanceCap() 现在已成功通过验证。由于 Prover 被限制在已满足 totalSupplyEqSumOfBalances() 的状态范围内，它不再遇到导致早先失败的那些不可能的配置。
require 对比 requireInvariant：相同的过滤， 不同的保证
有趣的是，如果我们使用常规的 require 语句代替 requireInvariant，indBalanceCap() 不变量也同样会通过验证，如下所示：
发生这种情况是因为，在一个 preserved 块中，require 和 requireInvariant 具有相同的操作目的：它们过滤归纳步骤的预状态。实际上，这两个语句都在指示 Prover：
“只探索从满足此条件的状态开始的转换。”
出于这个原因，以下两行代码对搜索空间施加了_相同的功能性限制_：
requireInvariant totalSupplyEqSumOfBalances();
和
require to_mathint(totalSupply()) == sumOfBalances;
两者都防止了 Prover 考虑我们之前观察到的不一致的初始状态，从而允许 indBalanceCap() 不变量通过验证。
为什么 requireInvariant 仍然是更好的选择
尽管这两种形式对搜索空间的限制相似，但它们在所产生的规范的可靠性和原则性方面存在差异。
requireInvariant 更安全，因为它导入了一个 Prover 在所有可达状态下都已经确定为真的属性。而普通的 require 则完全依赖规范编写者来陈述一个正确的条件。例如：
require to_mathint(totalSupply()) == sumOfBalances;
这会强制 Prover 接受这个等式，而不去检查它是否真实存在。如果该条件哪怕有轻微的不正确或不完整，Prover 也可能会默默忽略真正的反例，给出一个具有误导性的成功验证。
因此，关键区别很简单：
require强制执行我们编写的条件。requireInvariant强制执行一个已被证明为普遍为真的条件。
正因为如此，requireInvariant 提供了一种更安全、更具原则性的方式来重用假设，而普通的 require 如果条件不正确或不完整，可能会无意中隐藏真实的违规行为。
结论
这就是我们如何使用 requireInvariant 使我们的规范更加强大、更具模块化且更高效的方法。
- 在 规则 中，它允许我们重用已证明的不变量作为先决条件，确保每条执行路径都在切合实际的条件下受到检查。
- 在 不变量 中，它允许我们通过假设早期的属性来证明新的属性，避免了因不一致的状态而产生无意义的反例。
关键原则简单而强大：首先证明全局不变量，然后在验证特定行为或额外不变量时将它们重用为构建块。
本文是关于 使用 Certora Prover 进行形式化验证 系列文章的一部分