到目前为止，我们一直专注于验证单个方法或方法序列的行为 —— 确保特定的函数调用或一组调用在给定特定输入的情况下，产生正确的状态更改。但是验证还有另一个更普遍的方面：不变量（invariants）。
不变量是合约状态必须始终保持为真的条件，无论调用哪个函数或以何种顺序调用。如果任何执行 —— 无论是直接执行还是通过一系列调用 —— 违反了不变量，这都标志着合约设计中存在根本缺陷，可能会暴露 bug 或漏洞。
在本文中，我们将探讨如何使用 Certora 的 CVL 内置 invariant 构造来形式化地规范和验证此类属性。
在 CVL 中定义不变量
CVL 的内置 invariant 构造是一种形式化规范机制，它允许开发者定义在智能合约整个生命周期内必须保持的普遍属性（不变量），即从构造函数执行开始，到合约未来可能达到的任何状态。
CVL 中的不变量使用 invariant 关键字定义，后跟唯一的名称（标识符）、可选参数，以及描述必须始终为真的条件的布尔表达式，如下所示：
invariant invariant_name(optional_parameter_1, optional_parameter_2, ...)
boolean_expression_in_CVL;
如果在不变量中定义的布尔表达式在合约的每个可达状态以及其参数的所有可能值下都计算为 true，则认为该不变量成立并报告为已验证（✅）。我们将在本章稍后更详细地探讨不变量的验证过程。
不变量与 Rules 的区别
CVL 中的 rule 旨在检查特定属性在定义的场景中是否为真：从某个特定状态开始，执行某些操作，然后检查结果。
rule check_balance_updates(env e) {
// 1. Starting State
address user = e.msg.sender;
uint initial_balance = balanceOf(user);
// 2. Actions
uint amount;
deposit(amount); // Call the deposit function
// 3. Outcome Check
uint final_balance = balanceOf(user);
assert final_balance == initial_balance + amount, "Deposit did not correctly update balance";
}
换句话说，它回答了这样一个问题：“这个特定的操作（或操作序列）是否会导致预期的结果？”
与专注于特定场景的 rule 不同，CVL 中的 invariant 表达了一个在合约的每个可达状态下都必须始终为真的条件，无论调用了哪些函数或以何种顺序调用。
下面是一个简单不变量的示例，该不变量声明 count 的值永远不应为负：
invariant count_cannot_be_negative()
count() >= 0;
简而言之，它回答了这样一个问题：“无论如何使用合约，这个条件是否普遍为真？”
何时使用 Invariants 与 Rules
决定在 CVL 中使用 rule 还是 invariant，取决于我们旨在验证的属性的性质。
何时使用 Rule：验证特定场景
当你的目标是验证定义上下文或特定操作序列中的行为时，请选择 rule。例如：
withdraw(amount)函数应正确地从调用者的余额中扣除amount并将其转移，但前提是balanceOf(caller) >= amount。- 验证试图超出最大供应量上限进行
mint的操作是否能正确被 revert。 - 检查管理员函数是否只能由指定的管理员地址成功调用。
本质上，rule 是你回答以下问题的首选方式：“该函数（或函数序列）在这种特定情况下是否正常工作？”
何时使用 Invariant：强制执行基本真理
当你想要验证一个在每一个可能的状态和每一种可能的函数调用序列中都必须保持为真的属性时，请选择 invariant。例如：
- 在 ERC-20 实现中，
totalSupply必须始终等于所有单个用户余额的总和。 - 在借贷协议中，假设清算正常运作，抵押品的总价值必须始终大于或等于总债务的特定百分比。
- 在代币合约中，用户的余额永远不会变成负数。
不变量为合约状态的长期完整性和安全性提供了最强有力的保证。它们回答了这样一个关键问题：“无论发生什么情况，我的合约的这个基本属性是否坚不可摧？”
验证范围：Rules 与 Invariants
当验证 rule 时，Prover 会检查断言是否在 rule 中定义的特定场景下成立 —— 基于初始状态、采取的操作和任何假设。rule 为探索自定义路径或边缘情况提供了灵活性，但它们仅沿着规范中显式构建的执行路径验证正确性。
相比之下，不变量必须成立，无论调用了哪些函数、具有什么参数或以何种顺序。Prover 必须确保在合约的每个可达状态中都保持该不变量。这是通过基于数学归纳法的两部分证明原理来实现的：
- 基本情况（Base Case）： 属性必须在合约部署后立即成立 —— 即它必须由 constructor 建立。
- 归纳步骤（Inductive Step）： 对于合约中的每个 public 或 external 函数，如果属性在调用该函数_之前_成立，那么它在函数调用之后必须仍然成立。
如果基本情况和归纳步骤均被证明，则 Prover 会将该不变量报告为已验证（✅）。
在 Certora 中编写 Invariant
为了理解 invariant 验证在实践中是如何工作的，让我们来看一下 Certora documentation 中简单的 Voting 合约：
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
/// @title A simple voting contract
contract Voting {
// `hasVoted[user]` is true if the user voted.
mapping(address => bool) public hasVoted;
uint256 public votesInFavor; // keep the count of votes in favor
uint256 public votesAgainst; // keep the count of votes against
uint256 public totalVotes; // keep the count of total votes cast
/// @notice Allows a user to vote in favor of the proposal.
function voteInFavor() external {
// Ensure the user has not already voted
require(!hasVoted[msg.sender], "You have already voted.");
hasVoted[msg.sender] = true;
votesInFavor += 1;
totalVotes += 1;
}
/// @notice Allows a user to vote against the proposal.
function voteAgainst() external {
// Ensure the user has not already voted
require(!hasVoted[msg.sender], "You have already voted.");
hasVoted[msg.sender] = true;
votesAgainst += 1;
totalVotes += 1;
}
}
上述 Voting 合约允许用户对提案投赞成票或反对票（单票）。为了防止重复投票，该合约使用了一个 hasVoted 映射来记录一个地址是否已经参与过。它通过三个独立的计数器来跟踪投票情况：votesInFavor、votesAgainst 和 totalVotes。当用户使用 voteInFavor() 或 voteAgainst() 函数进行投票时，相应的计数器会递增，并且 hasVoted 状态将被更新。
识别 Voting 合约中的关键不变量
由于我们的目标是形式化验证 Voting 合约的不变量，我们首先需要识别其关键属性。查看我们的 Voting 合约，其中一个关键不变量是总票数应始终等于赞成票和反对票的总和。
在识别出这个关键不变量之后，让我们来看看使用 Certora 对其进行形式化规范和验证的过程。
设置项目环境
要开始验证我们的不变量，我们首先需要设置项目结构和环境。为此，请按照以下说明操作：
- 创建一个名为
certora-invariants-examples的空目录，并进入该目录。 - 在项目目录中，运行以下命令为该项目创建一个 Python 虚拟环境。
virtualenv certora-env
- 运行以下命令激活你创建的 Python 虚拟环境。
source certora-env/bin/activate
- 运行以下命令在虚拟环境中安装 Certora-CLI。
pip3 install certora-cli
- 运行以下命令在虚拟环境中安装 solc-select。
pip3 install solc-select
- 在项目目录中，创建三个子目录，分别命名为
contracts、specs和confs - 在项目目录中，导航到
contracts子文件夹并创建一个名为Voting.sol的文件。然后，将上面讨论的Voting合约粘贴到该文件中。
在规范文件中定义 Invariant
项目环境准备好后，下一步是创建一个规范文件（specification file），我们将在其中定义我们的不变量。
1. 创建规范文件： 在你的项目目录中，导航到 specs 子文件夹并创建一个规范文件（例如 invariant.spec）。此文件将包含你的 CVL rules，包括你要验证的不变量。
2. 声明 Invariant： 在你的规范文件中，使用 invariant 关键字定义一个不变量。给它起一个描述性的名称，以清楚地传达该 rule 检查的内容。
invariant totalVotesMatch()
3. 将 Invariant 条件作为 CVL 表达式插入： 接下来，指定必须始终为真的条件。在 Voting 合约的例子中，我们要确保总票数始终等于赞成票和反对票的总和：
invariant totalVotesMatch()
to_mathint(totalVotes()) == votesInFavor() + votesAgainst();
注意：to_mathint 用于将 Solidity 的 uint256 转换为 Certora 的数学整数以进行安全比较。无需将其应用于等式的右侧，因为在 CVL 中，所有算术运算的结果都会自动成为 mathint 类型。
4. 添加 Methods Block： 接下来，让我们在规范的顶部添加一个包含正确条目的 Methods Block。
methods {
function totalVotes() external returns(uint256);
function votesInFavor() external returns(uint256);
function votesAgainst() external returns(uint256);
}
invariant totalVotesMatch()
to_mathint(totalVotes()) == votesInFavor() + votesAgainst();
将函数声明为 envfree：由于 getter 函数 votesInFavor()、votesAgainst() 和 totalVotes() 不依赖于执行环境（即它们不读取 msg.sender、msg.value 或任何其他全局变量），我们可以将它们声明为 envfree。
methods {
function totalVotes() external returns(uint256) envfree;
function votesAgainst() external returns(uint256) envfree;
function votesInFavor() external returns(uint256) envfree;
}
invariant totalVotesMatch()
to_mathint(totalVotes()) == votesInFavor() + votesAgainst();
运行验证
正确设置项目目录后，请按照以下步骤运行 Certora Prover 并验证你的不变量。
1. 创建配置文件： 在 confs 子文件夹中，创建一个配置文件（例如 invariant.conf）并将下面的代码粘贴到其中。
{
"files": [
"contracts/Voting.sol:Voting"
],
"verify": "Voting:specs/invariant.spec",
"msg": "Testing Invariant"
}
2. 添加 Certora Personal Access Key： 在项目目录中，创建一个 .profile、.bashrc 或 .zshenv 文件（取决于你的操作系统和 shell），并添加以下行以将你的 Certora Personal Access Key 设置为环境变量。
#certora access key
export CERTORAKEY=<add-your-certora-access-key-here>
3. 加载环境变量： 添加密钥后，通过运行下面显示的相应命令将环境变量加载到当前终端会话中。
# For bash users
source .profile
# For zsh users
source .zshenv
4. 添加 Solidity 编译器： 在运行 Prover 之前，我们需要添加正确的 Solidity 编译器。要添加并使用正确的 Solidity 编译器版本，请运行以下命令。
solc-select install 0.8.25
solc-select use 0.8.25
5. 运行 Prover： 要验证你的不变量，请从项目的根目录运行以下命令。
certoraRun confs/invariant.conf
如果 Prover 成功编译了你的智能合约和规范文件 —— 没有遇到任何语法或语义错误，它将生成一个验证报告的链接并将其打印在你的终端输出中。
要查看 验证结果，请使用浏览器打开终端中打印的链接。结果应该类似于下图：
注意： 根据你规范的复杂性和当前的 Prover 队列，作业状态从 Queued 变为 Executed 可能需要几分钟时间。这种延迟是正常的，所以请不要担心。
上面显示的验证结果确认 Prover 已成功验证了我们的不变量。这意味着，根据分析，未发现任何可能破坏该不变量的场景，这表明它在合约的整个行为中始终保持成立。
为了更好地理解不变量被“成功验证”意味着什么，让我们来看看 Prover 在幕后是如何验证不变量的。
Invariants 是如何被验证的？
当提交不变量进行验证时，Prover 会执行两项基本检查以确保其正确性，这直接对应于前面讨论的基于数学归纳法的两部分证明原理：
- 初始状态检查（Initial-state Check）： 首先，Prover 会验证该不变量在合约的 constructor 执行完毕后是否立即成立。这是我们归纳证明的基本情况（Base Case）。
- 归纳步骤（Inductive Step）： 接下来，Prover 会检查每个 public 和 external 方法在其执行过程中是否保留了该不变量。这对应于归纳步骤，确保如果属性在函数调用前成立，它在调用后继续成立。
在 Prover UI 的左侧面板中展开不变量 totalVotesMatch() 即可看到这两项检查的结果。
Initial-state check 的结果显示在 “Induction base: After the constructor” 下方，确认合约开始于不变量成立的有效状态。
Inductive step 的结果显示在 “Induction step: after external (non-view) methods” 下方。这部分证明旨在表明所有 public 和 external 函数都保留了该不变量。
那么，为什么报告只显示 “non-view”（状态改变）方法呢？
这是 Prover 的一个巧妙优化。Solidity 编译器保证 view 和 pure 函数不会改变合约的状态。逻辑如下：
- 我们假设不变量在任何函数调用之前成立（归纳假设）。
- 调用了一个 view 函数。
- 由于合约的状态保持完全相同，该不变量在调用之后必定依然成立。
因为 view 和 pure 函数永远不会改变合约的状态，所以无需在归纳步骤中再次验证它们。它们的正确性已由确认合约在有效状态启动的 induction base 检查所保证。跳过这些多余的检查有助于 Prover 节省验证资源并消除报告中不必要的混乱。
因此，归纳步骤检查的重点是那些可以改变状态的方法。
在我们的例子中，voteAgainst() 和 voteInFavor() 都在此检查下进行了分析。每个函数旁边的绿色复选标记（✅）表示，在调用这些方法时，它们不会违反不变量。这确认了合约的逻辑在所有改变状态的操作中都正确保留了该不变量。
除了这两个核心检查之外，Prover 还会运行一个名为 envFreeFuncsStaticCheck 的 rule，该 rule 验证规范中所有标记为 envfree 的函数是否真正独立于执行环境（如 msg.sender 或 msg.value）。
了解 Prover UI 中的附加检查
如果你使用的是较新版本的 Certora Prover，当你展开 Prover UI 中的不变量结果时，你可能会注意到一些额外的条目，例如 rule_not_vacuous 和 invariant_not_trivial_postcondition，如下所示：
这些额外的条目是 Prover 本身添加的自动健全性检查（sanity checks）。它们不是你编写的内容，也并不意味着正在验证额外的不变量或 rules。它们的目的是确保你的不变量是真正有意义的，而不是被简单平庸地满足（trivially satisfied）。
注意： 从 Certora Prover v8.1.0 开始，默认运行基本健全性检查（相当于设置 "rule_sanity": "basic"）。以前，默认值是 "none"。你可以使用 --rule_sanity CLI 选项或通过将 "rule_sanity": "none" 添加到配置文件中来控制此行为以禁用这些检查。有关所有可用健全性检查的详细说明，请参阅 Rule Sanity Checks documentation。
这些检查验证的内容：
rule_not_vacuous：确认不变量实际上是在现实条件下进行评估的。“空洞（vacuous）”的结果意味着该不变量仅仅因为从未满足前置条件而通过 —— 从本质上讲，它从未受到真正的测试。invariant_not_trivial_postcondition：确保不变量的条件并非无论合约状态如何都理所当然地为真（例如，一个始终计算为true的表达式）。
这些额外的检查不会改变核心的验证过程。Prover 仍然执行相同的两部分归纳证明：验证不变量在 constructor 之后是否成立（基本情况），以及每个改变状态的函数是否保留它（归纳步骤）。健全性检查仅仅提供了额外的信心，表明你的验证结果是有意义的，而不是规范错误造成的人为假象。
结论
智能合约不变量是关于合约状态的关键断言，它必须始终保持为真。形式化验证这些不变量可确保合约在所有可能的状态和方法执行中保持其预期的行为和正确性。
本文是关于 使用 Certora Prover 进行形式化验证 系列文章的一部分