在上一章中，我们了解了未受约束的 ghost 变量如何导致误报（false positives）。我们还学习了如何使用 require 语句在规则（rules）中有效地约束 ghost 值。
然而，虽然 require 对规则很有效，但这种方法不能用于不变量（invariant）验证。在本章中，我们将探讨为什么 require 语句与不变量不兼容，并介绍 axioms（公理）这一正确技术，用于在不变量中安全地约束 ghost 变量的值。
理解问题
为了理解未受约束的 ghost 变量如何影响不变量验证，请查看下面的 Voting 合约。该合约允许用户使用 inFavor() 或 against() 函数对提案投赞成票（in favor）或反对票（against）。
// 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;
// keep the count of votes in favor
uint256 public votesInFavor;
// keep the count of votes against
uint256 public votesAgainst;
// @notice Allows a user to vote in favor of the proposal.
function inFavor() external {
// Ensure the user has not already voted
require(!hasVoted[msg.sender], "You have already voted.");
hasVoted[msg.sender] = true;
votesInFavor += 1;
}
/// @notice Allows a user to vote against the proposal.
function against() external {
// Ensure the user has not already voted
require(!hasVoted[msg.sender], "You have already voted.");
hasVoted[msg.sender] = true;
votesAgainst += 1;
}
}
该合约维护了三个 public 状态变量：
hasVoted用于跟踪给定用户是否已经投票。votesInFavor和votesAgainst分别用于跟踪赞成票和反对票的数量。
现在考虑下面的规范（specification），它定义了一个不变量 totalVotesSum 并引入了一个 ghost 变量 totalVotes，用于跟踪投票的总数——这是合约本身并没有记录的值。
methods
{
function votesInFavor() external returns(uint256) envfree;
function votesAgainst() external returns(uint256) envfree;
}
ghost mathint totalVotes;
hook Sstore hasVoted[KEY address voter] bool newStatus(bool oldStatus) {
totalVotes = totalVotes + 1;
}
invariant totalVotesSum()
totalVotes == votesInFavor() + votesAgainst();
以下是上述规范的详细解释：
- methods 块声明了我们想要在不变量中引用的两个 public view 函数
votesInFavor()和votesAgainst()。它们被标记为envfree，因为它们的执行不依赖于环境变量，如msg.sender、msg.value等。 - ghost 变量
totalVotes被定义用来计算已投票的用户数量。由于合约并未直接暴露这个值，我们使用 ghost 来模拟它。 - hook 被附加到
hasVoted映射的Sstore操作上。每次hasVoted映射中的值被更新时，这个 hook 就会被触发，而这只会在用户投票时发生。在 hook 中，我们将totalVotes增加 1——这实际上是在计算每一个新投票者，无论他们投的是赞成票还是反对票。 - 不变量（invariant）
totalVotesSum断言，由 ghost 跟踪的投票数（totalVotes）必须始终与从合约中获取的实际投票总数（votesInFavor+votesAgainst）相匹配。
将上述规范放入项目目录后，使用 certoraRun 命令运行验证过程。接下来，打开终端中显示的验证结果链接以查看结果，其应与下图类似。
我们可以看到 Prover 未能验证我们的不变量。让我们探讨一下为什么会发生这种情况，以及如何解决它。
理解违反（Violation）的原因
不变量检查包括两个步骤：base case（基本情况，即检查构造函数之后的初始状态）和 inductive step（归纳步骤，即检查所有后续的状态转换）。
在我们的情况下，Prover 在base case下失败了，这意味着它无法确认不变量从合约的初始状态起就是有效的。
我们的不变量在 base case 失败，因为在验证任何不变量时，Prover 必须检查合约初始状态下的不变量。然而，由于我们从未指定 totalVotes 的初始值，Prover 以对抗（adversarial）的方式为我们选择了一个初始值。在调用追踪（call trace）中，我们可以看到它选择了 -2。
这导致不变量 totalVotes == votesInFavor() + votesAgainst() 立即失败，因为 Prover 检查了 -2 == 0 + 0，结果为假。为了修复这个问题，我们需要将 ghost 的初始值设置为 0。然而，与在规则中不同，我们不能使用 require 语句来约束 ghost 的初始值。这并不意味着 require 在不变量中没有立足之地。它可以用在 preserved 块内部。
preserved 块是 CVL 中的一种特殊构造，它允许你在验证不变量时添加额外假设。我们将在单独的一章中了解更多关于 preserved 块的内容。
在探讨如何在不变量中约束 ghost 变量之前，让我们首先了解为什么在这种语境下不能使用 require。
为什么我们不能使用 require 语句？
在 CVL 中，require 语句在**规则（rule）**中被用作前置条件（precondition）。它告诉 Prover，“只检查那些满足这些特定条件的场景下的以下断言。”这有助于过滤 Prover 在评估规则时探索的执行路径或输入组合。
然而，不变量（invariant）非常不同。不变量必须在合约的每一种可能状态下（包括初始状态）都成立，而不依赖于任何前置条件。换句话说，不变量表达了关于系统的无条件真理。
在不变量内部使用 require 语句是没有意义的，因为 require 仅仅在规则执行期间限制路径——它并没有定义在验证开始之前什么是真的。相反，我们需要的是一种为 Prover 建立**初始状态假设（initial state assumptions）**的方法。
为了建立这样的初始真理——例如设置 ghost 变量的起始值——我们需要一种不同的构造：axioms（公理）。
“Axioms”简介
由于不变量不能依赖前置条件，我们需要一种方法来定义在验证开始之前，Prover 应该对系统*假设（assume）*些什么。这就是 axioms 发挥作用的地方。
在 CVL 中，axiom 允许我们声明一个 Prover 必须始终承认为真的事实或关系。axiom 并不是像 require 那样过滤状态空间，而是通过指定在其逻辑宇宙中成立的真理，来塑造（shapes） Prover 的推理过程。
简而言之：
require语句限制了 Prover 检查的内容（它过滤状态）。- axiom 定义了 Prover 所相信的内容（它建立真理）。
通过使用 axioms，我们可以精确控制 ghost 变量在不变量验证期间的行为。例如，我们可以指示 Prover 假设一个 ghost 变量在构造函数之前从某个特定值开始，或者它在所有状态下始终满足给定的条件。
在 CVL 中，用于 ghost 变量的 axiom 主要有两种类型：
- Initial State Axioms（初始状态公理）
- Global Axioms（全局公理）
什么是 “Initial State Axioms”
initial state axiom 定义了一个属性，Prover 必须假设该属性在不变量检查的 base step 中或恰好在合约构造函数执行之前成立。
换句话说，它告诉 Prover，“假设当合约首次部署时，这个条件为真。”这允许你控制 ghost 变量的初始值，并消除可能导致不变量失败的任意起始状态。
初始状态公理使用 init_state 关键字声明，后跟 axiom 关键字，然后是定义 ghost 变量初始状态的条件，如下所示：
ghost type_of_ghost name_of_ghost {
init_state axiom boolean_expression;
}
例如，下面的代码定义了一个 mathint 类型的 ghost 变量 sum_of_balances，并指定其值在合约构造函数运行之前应该为 0。
ghost mathint sum_of_balances {
init_state axiom sum_of_balances == 0;
}
这将确保 Prover 以 sum_of_balances 从零开始的假设来开始验证，从而防止在初始状态下它被视为一个任意值。
什么是 “Global Axioms”
虽然初始状态公理仅适用于合约的第一个状态，但 global axioms 定义了在整个验证过程中的每个状态下都必须成立的属性。
global axiom 允许你表达关于 ghost 变量的普遍真理——这些条件在所有可能的合约执行过程中保持一致。一旦定义，Prover 将接受这些语句为始终有效且无需重新证明的事实。
定义全局 ghost 公理的方法是，在 ghost 变量声明块中包含 axiom 关键字，随后紧跟一个应在所有程序状态中成立的条件，如下所示：
ghost type_of_ghost name_of_ghost {
axiom boolean_expression;
}
例如，下面的代码定义了一个 mathint 类型的 ghost 变量 x，并断言在整个验证过程的每个状态中，它的值始终大于零：
ghost mathint x {
axiom x > 0;
}
这意味着在验证期间，Prover 将假设条件 在所有状态下成立，从而有效地约束 ghost 变量永远不会取零或负值。
在我们的规范中使用 init_state Axiom
既然我们理解了 init_state 公理的用途，让我们将它应用到前面探讨的示例中，在那个示例中，我们的不变量失败是因为 ghost 变量 totalVotes 以一个任意值开始。
为了修复这个问题，我们需要告诉 Prover，在构造函数运行之前，totalVotes 应该紧接着从 0 开始。我们通过更新 ghost 声明以包含 init_state 公理来实现这一点，如下所示：
ghost mathint totalVotes {
init_state axiom totalVotes == 0;
}
一旦你更新了规范，包含了如上所示的 init_state 公理，重新运行 Prover 并打开验证结果。我们的新验证结果应该类似于下面的结果。
这一次，我们可以观察到 Prover 已经成功验证了我们的不变量，同时通过了 base case 和 inductive step，证实了总投票数始终等于投出的赞成票与反对票之和。
在实践中使用 Global Axiom
为了理解 global axioms 在实践中是如何工作的，请考虑下面的规范：
methods {
function votesInFavor() external returns(uint256) envfree;
function votesAgainst() external returns(uint256) envfree;
}
ghost mathint totalVotes {
axiom totalVotes >= 0;
}
hook Sstore hasVoted[KEY address voter] bool newStatus(bool oldStatus) {
totalVotes = totalVotes + 1;
}
invariant totalVotesShouldAlwaysGtInFavorVotes()
totalVotes >= votesInFavor();
上述规范断言总投票数（totalVotes）必须始终大于或等于赞成票数（votesInFavor）。在上述规范中，关键部分是 axiom totalVotes >= 0 这一行，它引入了一个 global axiom，指示 Prover 始终假设在每个程序状态下 totalVotes 都是非负数。这意味着 Prover 永远不会探索任何使得 totalVotes 变为负数的执行路径。
当你将此规范提交给 Prover 时，它成功验证了该不变量，如下面的结果所示：
如我们所知，当提交不变量进行验证时，Prover 会执行两个基本检查以确保其正确性：
- Base Case：在这一步中，Prover 首先检查不变量在合约的构造函数执行后是否立即成立。在我们的例子中，这意味着在合约的初始状态下，要验证
totalVotes >= votesInFavor()是否为真。在刚刚部署之后，votesInFavor()是 0，而 Prover 假设totalVotes可以是任何非负值。由于任何非负数都满足totalVotes >= votesInFavor()这一条件，因此 base case 成立。 - Inductive Step: 接下来，Prover 确保如果在任何函数执行之前不变量成立，那么在所有可能的转换之后它仍继续成立。在这里，每次用户投票时，
hasVoted映射会被更新，并且 hook 会将totalVotes递增。- 当用户投赞成票时，
votesInFavor和totalVotes都会增加一，从而保持了不等式成立。 - 当用户投反对票时，只有
totalVotes会增加，这依然保持了不变量。
- 当用户投赞成票时，
因为这两个条件都成立，所以 Prover 成功地验证了不变量。这证实了在全局假设 totalVotes >= 0 的情况下，totalVotes 和 votesInFavor 之间的关系在所有可能的合约状态下都保持有效。
这就是 global axiom 如何帮助 Prover 推理那些在每个程序状态下普遍为真的属性的。通过定义 axiom totalVotes >= 0，我们建立了一个在整个验证过程中始终成立的逻辑事实，而不需要在每次状态转换后重新证明它。在这种情况下，该公理捕获了一个直观的真理，即总投票数永远不可能是负数，从而允许 Prover 高效且稳健（soundly）地验证不变量。
结论
在本章中，我们演示了未受约束的 ghost 变量如何导致不变量证明在 base case 失败。由于在不变量中使用 require 进行初始化是无效的，我们介绍了 axioms 作为正确的替代方案。具体来说，init_state axiom 通过为 ghost 定义有效的起始值来解决初始化问题，而 global axioms 则表达了在所有合约状态下保持为真的属性。
本文是使用 Certora Prover 进行形式化验证系列文章的一部分