约束不变量中的幽灵变量

RareSkills
发布于 2026-02-14 13:45
阅读 11

本文深入探讨了 Certora 形式化验证中，如何在不变量（invariants）内正确约束幽灵变量（ghost variables）。文章指出 require 语句不适用于不变量，并详细介绍了使用 init_state axiom 来设置幽灵变量的初始值，以及使用 global axiom 来定义在所有状态下都成立的属性，以解决验证失败的问题。

Certora 的形式化验证

## 在不变量中约束幽灵变量

[模块 2：不变量、存储Hook、幽灵变量和形式化验证代币不变量、存储Hook、幽灵变量和形式化验证代币](https://rareskills.io/tutorials/certora-book)

上次更新于 2026 年 2 月 13 日

在上一章中，我们了解了不受约束的幽灵变量如何导致假阳性。我们还学习了如何使用 `require` 语句有效地约束规则中的幽灵值。

然而，尽管 `require` 对于规则运作良好，但这种方法不能用于不变量验证。在本章中，我们将探讨为什么 `require` 语句与不变量不兼容，并介绍 **公理（axioms）** 作为在不变量中安全约束幽灵变量值的正确技术。

## 理解问题

为了理解不受约束的幽灵变量如何影响 **不变量验证**，请考虑下面所示的 `Voting` 合约。此合约允许用户使用 `inFavor()` 或 `against()` 函数对提案进行 **赞成** 或 **反对** 投票。

```solidity
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

/// @title 一个简单的投票合约
contract Voting {

// `hasVoted[user]` 为 true 表示用户已投票。
    mapping(address => bool) public hasVoted;

// 统计赞成票数
    uint256 public votesInFavor;

// 统计反对票数
    uint256 public votesAgainst;

// @notice 允许用户投票赞成提案。
    function inFavor() external {
        // 确保用户尚未投票
        require(!hasVoted[msg.sender], "You have already voted.");
        hasVoted[msg.sender] = true;

votesInFavor += 1;
    }

/// @notice 允许用户投票反对提案。
    function against() external {
        // 确保用户尚未投票
        require(!hasVoted[msg.sender], "You have already voted.");
        hasVoted[msg.sender] = true;

votesAgainst += 1;
  }
}
```

此合约维护三个公共状态变量：

-   `hasVoted` 跟踪给定用户是否已投票。
-   `votesInFavor` 和 `votesAgainst` 分别记录赞成票数和反对票数。

现在考虑下面的规范，它定义了一个不变量 `totalVotesSum` 并引入了一个幽灵变量 `totalVotes`，用于跟踪已投出的总票数——合约本身并未记录这个值。

```solidity
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 块** 声明了我们希望在不变量中引用的两个公共视图函数 `votesInFavor()` 和 `votesAgainst()`。它们被标记为 `envfree`，因为它们的执行不依赖于 `msg.sender`、`msg.value` 等环境变量。
-   **幽灵变量** `totalVotes` 定义用于计算已投票用户数量。由于合约不直接暴露此值，我们使用幽灵变量来模拟它。
-   **hook** 附加到 `hasVoted` 映射的 `Sstore` 操作上。每当 `hasVoted` 映射中的值更新时（这只在用户投票时发生），此 hook 就会触发。在 hook 中，我们将 `totalVotes` 增加 1——有效地计算每个新投票者，无论他们是投赞成票还是反对票。
-   **不变量** `totalVotesSum` 断言由幽灵变量跟踪的票数 (`totalVotes`) 必须始终与从合约中检索到的实际票数之和 (`votesInFavor` + `votesAgainst`) 相匹配。

将上述规范放置到你的项目目录中后，使用 `certoraRun` 命令运行验证过程。接下来，打开终端中显示的验证结果链接以查看结果，结果应如下图所示。

![image](https://img.learnblockchain.cn/2026/02/28/fcad1789622c8628-image1.png)

我们可以看到 Prover 未能验证我们的不变量。让我们探讨一下为什么会发生这种情况以及如何解决它。

## 理解违规原因

不变量检查包括两个步骤：**基本情况**（检查构造函数后的初始状态）和 **归纳步骤**（检查所有后续状态转换）。

在我们的情况下，Prover 在 **基本情况** 下失败，这意味着它无法确认不变量从合约的初始状态开始就是有效的。

![image](https://img.learnblockchain.cn/2026/02/28/b190f84d86ef03ae-image2.png)

我们的不变量在 **基本情况** 下失败，因为在验证任何不变量时，Prover 必须检查合约初始状态下的不变量。然而，由于我们从未为 `totalVotes` 指定初始值，Prover 对我们来说对抗性地选择了一个值。在调用跟踪中，我们可以看到它选择了 `-2`。

![image](https://img.learnblockchain.cn/2026/02/28/6d5f18b065f5d2c1-image3.png)

这导致不变量 `$totalVotes == votesInFavor() + votesAgainst()$` 立即失败，因为 Prover 检查 `$-2 == 0 + 0$` 是否为真，而这是假的。为了解决这个问题，我们需要将幽灵变量的初始值设置为 `0`。然而，与规则不同，我们不能使用 `require` 语句来约束幽灵变量的初始值。这并不意味着 `require` 在不变量中没有用武之地。它可以在 `preserved` 块内使用。

`preserved` 块是 CVL 中的一种特殊构造，它允许你在验证不变量时添加 **额外假设**。我们将在单独的章节中学习更多关于 `preserved` 块的内容。

在我们探讨如何在不变量中约束幽灵变量之前，让我们首先了解 **为什么不能使用 require 语句**。

## 为什么我们不能使用 require 语句？

在 CVL 中，`require` 语句在 **规则** 中用作 **前置条件**。它告诉 Prover：“**只在这些特定条件成立的情况下检查以下断言。**” 这有助于过滤 Prover 在评估规则时探索的执行路径或输入组合。

然而，**不变量** 非常不同。不变量必须在合约的 **每个可能状态** 下都成立，包括初始状态，而不依赖于任何前置条件。换句话说，不变量表达了系统 **无条件的真理**。

在不变量内部使用 `require` 语句没有意义，因为 `require` 只限制 **规则执行期间** 的路径——它不定义 **验证开始前** 什么为真。我们需要的是一种建立 Prover **初始状态假设** 的方法。

为了建立这样的初始真理——例如设置幽灵变量的起始值——我们需要一种不同的构造：**公理（axioms）**。

## “公理”介绍

由于不变量不能依赖于前置条件，我们需要一种方法来定义 Prover 在验证开始前应该 **假设** 什么。这就是 **公理（axioms）** 的作用。

在 CVL 中，**公理** 允许我们声明 Prover 必须始终接受为真的事实或关系。公理不像 `require` 那样过滤状态空间，而是通过指定其逻辑宇宙中成立的真理来 **塑造** Prover 的推理。

简单来说：

-   `require` 语句 **限制 Prover 检查的内容**（它过滤状态）。
-   公理 **定义 Prover 相信的内容**（它建立真理）。

通过使用公理，我们可以精确控制幽灵变量在不变量验证期间的行为。例如，我们可以指示 Prover 假设一个幽灵变量在构造函数之前以某个特定值开始，或者它始终满足所有状态下的给定条件。

用于 CVL 中幽灵变量的公理主要有两种类型：

1.  **初始状态公理（Initial State Axioms）**
2.  **全局公理（Global Axioms）**

## 什么是“初始状态公理”

**初始状态公理** 定义了 Prover 必须假定在不变量检查的基本步骤中或在合约的构造函数执行之前成立的属性。

换句话说，它告诉 Prover：“**当合约首次部署时，假设此条件为真。**” 这允许你控制幽灵变量的初始值，并消除否则可能导致不变量失败的任意起始状态。

初始状态公理使用 `init_state` 关键字声明，后跟 `axiom` 关键字，然后是定义幽灵变量初始状态的布尔表达式，如下所示：

```solidity
ghost type_of_ghost name_of_ghost {
    init_state axiom boolean_expression;
}
```

例如，以下代码定义了一个 `mathint` 类型的幽灵变量 `sum_of_balances`，并指定其值在合约构造函数 **运行之前** 应为 0。

```solidity
ghost mathint sum_of_balances {
    init_state axiom sum_of_balances == 0;
}
```

这将确保 Prover 在验证开始时假设 `sum_of_balances` 以零开始，从而防止其在初始状态被视为任意值。

## 什么是“全局公理”

虽然初始状态公理仅适用于合约的第一个状态，但 **全局公理** 定义了在整个验证过程中 **每个状态** 都必须成立的属性。

全局公理允许你表达关于幽灵变量的普遍真理——在所有可能的合约执行中保持一致的条件。一旦定义，Prover 将这些语句视为始终有效且无需重新证明的事实。

全局幽灵公理通过在幽灵变量声明块内包含 `axiom` 关键字来定义，后跟在所有程序状态中都应成立的条件，如下所示：

```solidity
ghost type_of_ghost name_of_ghost {
  axiom boolean_expression;
}
```

例如，以下代码定义了一个 `mathint` 类型的幽灵变量 `x`，并断言其值在整个验证过程中在每个状态下始终大于零：

```solidity
ghost mathint x {
  axiom x > 0;
}
```

这意味着在验证期间，Prover 将假设条件 `$x > 0$` 在所有状态下都成立，有效地约束幽灵变量永远不会取零或负值。

## 在我们的规范中使用 `init_state` 公理

现在我们了解了 `init_state` 公理的目的，让我们将其应用于我们之前探讨的示例，在该示例中，我们的不变量因为幽灵变量 `totalVotes` 以任意值开始而失败。

为了解决这个问题，我们需要告诉 Prover，`totalVotes` 应该在构造函数运行之前立即从 0 开始。我们通过更新幽灵变量声明以包含 `init_state` 公理来实现这一点，如下所示：

```solidity
ghost mathint totalVotes {
  init_state axiom totalVotes == 0;
}
```

更新规范以包含 `init_state` 公理后，重新运行 Prover 并打开验证结果。我们的新验证结果应与下图所示的结果类似。

![image](https://img.learnblockchain.cn/2026/02/28/a374275e269f7ca6-image4.png)

这一次，我们可以观察到 Prover 已成功验证了我们的不变量，通过了 **基本情况** 和 **归纳步骤**，确认总票数始终等于赞成票数和反对票数之和。

![image](https://img.learnblockchain.cn/2026/02/28/b004267a9f02fc40-image5.png)

## 实际应用全局公理

为了理解全局公理在实践中如何工作，请考虑以下规范：

```solidity
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`，它引入了一个全局公理，指示 Prover **始终假设** `totalVotes` 在每个程序状态中都是非负的。这意味着 Prover 永远不会探索 `totalVotes` 变为负值的任何执行路径。

当你将此规范提交给 Prover 时，它会成功验证不变量，结果如下所示：

![image](https://cdn.rareskills.io/github-images/435535b171c3cd1-image6.png)

如我们所知，当提交不变量进行验证时，Prover 执行两项基本检查以确保其正确性：

1.  **基本情况**：在此步骤中，Prover 首先检查不变量是否在合约的构造函数执行后立即成立。在我们的示例中，这意味着验证 `$totalVotes \ge votesInFavor()$` 在合约的初始状态下是否为真。部署后，`votesInFavor()` 为 0，而 Prover 假设 `totalVotes` 可以是任何非负值。由于任何非负数都满足条件 `$totalVotes \ge votesInFavor()$`，因此基本情况成立。
2.  **归纳步骤**：接下来，Prover 确保如果不变量在任何函数执行之前成立，那么在所有可能的转换之后它仍然成立。在这里，每次用户投票时，`hasVoted` 映射都会更新，并且 hook 会增加 `totalVotes`。
    -   当用户投 **赞成票** 时，`votesInFavor` 和 `totalVotes` 都增加 1，保持了不等式。
    -   当用户投 **反对票** 时，只有 `totalVotes` 增加，这仍然保持了不变量。

由于两个条件都成立，Prover 成功验证了不变量。这证实了在全局假设 `$totalVotes \ge 0$` 下，`totalVotes` 和 `votesInFavor` 之间的关系在所有可能的合约状态下都保持有效。

这就是 **全局公理** 如何帮助 Prover 推理在每个程序状态中普遍为真的属性。通过定义 `axiom totalVotes >= 0`，我们建立了一个在整个验证过程中都成立的逻辑事实，而无需在每次状态转换后重新证明它。在这种情况下，公理捕捉了一个直观的真理，即总票数永远不能为负，并允许 Prover 高效且可靠地验证不变量。

## 结论

在本章中，我们演示了不受约束的幽灵变量如何导致不变量证明在基本情况下失败。由于在不变量中使用 `require` 进行初始化是无效的，我们引入了 **公理（axioms）** 作为正确的替代方案。具体来说，`init_state` **公理** 通过定义幽灵变量的有效起始值解决了初始化问题，而 **全局公理** 则表达了在所有合约状态下都保持为真的属性。

_本文是关于 [使用 Certora Prover 进行形式化验证](https://rareskills.io/tutorials/certora-book) 系列文章的一部分。_

>- 原文链接： [rareskills.io/post/certo...](https://rareskills.io/post/certora-constraining-ghosts-in-invariants)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

Certora 的形式化验证

在不变量中约束幽灵变量

模块 2：不变量、存储Hook、幽灵变量和形式化验证代币不变量、存储Hook、幽灵变量和形式化验证代币

上次更新于 2026 年 2 月 13 日

在上一章中，我们了解了不受约束的幽灵变量如何导致假阳性。我们还学习了如何使用 require 语句有效地约束规则中的幽灵值。

然而，尽管 require 对于规则运作良好，但这种方法不能用于不变量验证。在本章中，我们将探讨为什么 require 语句与不变量不兼容，并介绍 公理（axioms） 作为在不变量中安全约束幽灵变量值的正确技术。

理解问题

为了理解不受约束的幽灵变量如何影响 不变量验证，请考虑下面所示的 Voting 合约。此合约允许用户使用 inFavor() 或 against() 函数对提案进行赞成或反对投票。

// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;

/// @title 一个简单的投票合约
contract Voting {

    // `hasVoted[user]` 为 true 表示用户已投票。
    mapping(address => bool) public hasVoted;

    // 统计赞成票数
    uint256 public votesInFavor;

    // 统计反对票数
    uint256 public votesAgainst;

    // @notice 允许用户投票赞成提案。
    function inFavor() external {
        // 确保用户尚未投票
        require(!hasVoted[msg.sender], "You have already voted.");
        hasVoted[msg.sender] = true;

        votesInFavor += 1;
    }

    /// @notice 允许用户投票反对提案。
    function against() external {
        // 确保用户尚未投票
        require(!hasVoted[msg.sender], "You have already voted.");
        hasVoted[msg.sender] = true;

        votesAgainst += 1;
  }
}

此合约维护三个公共状态变量：

hasVoted 跟踪给定用户是否已投票。
votesInFavor 和 votesAgainst 分别记录赞成票数和反对票数。

现在考虑下面的规范，它定义了一个不变量 totalVotesSum 并引入了一个幽灵变量 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 块 声明了我们希望在不变量中引用的两个公共视图函数 votesInFavor() 和 votesAgainst()。它们被标记为 envfree，因为它们的执行不依赖于 msg.sender、msg.value 等环境变量。
幽灵变量 totalVotes 定义用于计算已投票用户数量。由于合约不直接暴露此值，我们使用幽灵变量来模拟它。
hook 附加到 hasVoted 映射的 Sstore 操作上。每当 hasVoted 映射中的值更新时（这只在用户投票时发生），此 hook 就会触发。在 hook 中，我们将 totalVotes 增加 1——有效地计算每个新投票者，无论他们是投赞成票还是反对票。
不变量 totalVotesSum 断言由幽灵变量跟踪的票数 (totalVotes) 必须始终与从合约中检索到的实际票数之和 (votesInFavor + votesAgainst) 相匹配。

将上述规范放置到你的项目目录中后，使用 certoraRun 命令运行验证过程。接下来，打开终端中显示的验证结果链接以查看结果，结果应如下图所示。

我们可以看到 Prover 未能验证我们的不变量。让我们探讨一下为什么会发生这种情况以及如何解决它。

理解违规原因

不变量检查包括两个步骤：基本情况（检查构造函数后的初始状态）和 归纳步骤（检查所有后续状态转换）。

在我们的情况下，Prover 在 基本情况 下失败，这意味着它无法确认不变量从合约的初始状态开始就是有效的。

我们的不变量在 基本情况 下失败，因为在验证任何不变量时，Prover 必须检查合约初始状态下的不变量。然而，由于我们从未为 totalVotes 指定初始值，Prover 对我们来说对抗性地选择了一个值。在调用跟踪中，我们可以看到它选择了 -2。

这导致不变量 $totalVotes == votesInFavor() + votesAgainst()$ 立即失败，因为 Prover 检查 $-2 == 0 + 0$ 是否为真，而这是假的。为了解决这个问题，我们需要将幽灵变量的初始值设置为 0。然而，与规则不同，我们不能使用 require 语句来约束幽灵变量的初始值。这并不意味着 require 在不变量中没有用武之地。它可以在 preserved 块内使用。

preserved 块是 CVL 中的一种特殊构造，它允许你在验证不变量时添加 额外假设。我们将在单独的章节中学习更多关于 preserved 块的内容。

在我们探讨如何在不变量中约束幽灵变量之前，让我们首先了解 为什么不能使用 require 语句。

为什么我们不能使用 require 语句？

在 CVL 中，require 语句在规则中用作 前置条件。它告诉 Prover：“只在这些特定条件成立的情况下检查以下断言。” 这有助于过滤 Prover 在评估规则时探索的执行路径或输入组合。

然而，不变量 非常不同。不变量必须在合约的 每个可能状态 下都成立，包括初始状态，而不依赖于任何前置条件。换句话说，不变量表达了系统 无条件的真理。

在不变量内部使用 require 语句没有意义，因为 require 只限制 规则执行期间 的路径——它不定义 验证开始前 什么为真。我们需要的是一种建立 Prover 初始状态假设 的方法。

为了建立这样的初始真理——例如设置幽灵变量的起始值——我们需要一种不同的构造：公理（axioms）。

“公理”介绍

由于不变量不能依赖于前置条件，我们需要一种方法来定义 Prover 在验证开始前应该假设什么。这就是 公理（axioms） 的作用。

在 CVL 中，公理允许我们声明 Prover 必须始终接受为真的事实或关系。公理不像 require 那样过滤状态空间，而是通过指定其逻辑宇宙中成立的真理来塑造 Prover 的推理。

简单来说：

require 语句 限制 Prover 检查的内容（它过滤状态）。
公理 定义 Prover 相信的内容（它建立真理）。

用于 CVL 中幽灵变量的公理主要有两种类型：

初始状态公理（Initial State Axioms）
全局公理（Global Axioms）

什么是“初始状态公理”

初始状态公理 定义了 Prover 必须假定在不变量检查的基本步骤中或在合约的构造函数执行之前成立的属性。

换句话说，它告诉 Prover：“当合约首次部署时，假设此条件为真。” 这允许你控制幽灵变量的初始值，并消除否则可能导致不变量失败的任意起始状态。

初始状态公理使用 init_state 关键字声明，后跟 axiom 关键字，然后是定义幽灵变量初始状态的布尔表达式，如下所示：

ghost type_of_ghost name_of_ghost {
    init_state axiom boolean_expression;
}

例如，以下代码定义了一个 mathint 类型的幽灵变量 sum_of_balances，并指定其值在合约构造函数 运行之前 应为 0。

ghost mathint sum_of_balances {
    init_state axiom sum_of_balances == 0;
}

这将确保 Prover 在验证开始时假设 sum_of_balances 以零开始，从而防止其在初始状态被视为任意值。

什么是“全局公理”

虽然初始状态公理仅适用于合约的第一个状态，但 全局公理 定义了在整个验证过程中 每个状态 都必须成立的属性。

全局幽灵公理通过在幽灵变量声明块内包含 axiom 关键字来定义，后跟在所有程序状态中都应成立的条件，如下所示：

ghost type_of_ghost name_of_ghost {
  axiom boolean_expression;
}

例如，以下代码定义了一个 mathint 类型的幽灵变量 x，并断言其值在整个验证过程中在每个状态下始终大于零：

ghost mathint x {
  axiom x > 0;
}

这意味着在验证期间，Prover 将假设条件 $x > 0$ 在所有状态下都成立，有效地约束幽灵变量永远不会取零或负值。

在我们的规范中使用 `init_state` 公理

现在我们了解了 init_state 公理的目的，让我们将其应用于我们之前探讨的示例，在该示例中，我们的不变量因为幽灵变量 totalVotes 以任意值开始而失败。

为了解决这个问题，我们需要告诉 Prover，totalVotes 应该在构造函数运行之前立即从 0 开始。我们通过更新幽灵变量声明以包含 init_state 公理来实现这一点，如下所示：

ghost mathint totalVotes {
  init_state axiom totalVotes == 0;
}

更新规范以包含 init_state 公理后，重新运行 Prover 并打开验证结果。我们的新验证结果应与下图所示的结果类似。

这一次，我们可以观察到 Prover 已成功验证了我们的不变量，通过了 基本情况 和 归纳步骤，确认总票数始终等于赞成票数和反对票数之和。

实际应用全局公理

为了理解全局公理在实践中如何工作，请考虑以下规范：

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，它引入了一个全局公理，指示 Prover 始终假设 totalVotes 在每个程序状态中都是非负的。这意味着 Prover 永远不会探索 totalVotes 变为负值的任何执行路径。

当你将此规范提交给 Prover 时，它会成功验证不变量，结果如下所示：

如我们所知，当提交不变量进行验证时，Prover 执行两项基本检查以确保其正确性：

基本情况：在此步骤中，Prover 首先检查不变量是否在合约的构造函数执行后立即成立。在我们的示例中，这意味着验证 $totalVotes \ge votesInFavor()$ 在合约的初始状态下是否为真。部署后，votesInFavor() 为 0，而 Prover 假设 totalVotes 可以是任何非负值。由于任何非负数都满足条件 $totalVotes \ge votesInFavor()$ ，因此基本情况成立。
归纳步骤：接下来，Prover 确保如果不变量在任何函数执行之前成立，那么在所有可能的转换之后它仍然成立。在这里，每次用户投票时，hasVoted 映射都会更新，并且 hook 会增加 totalVotes。
- 当用户投 赞成票 时，votesInFavor 和 totalVotes 都增加 1，保持了不等式。
- 当用户投 反对票 时，只有 totalVotes 增加，这仍然保持了不变量。

由于两个条件都成立，Prover 成功验证了不变量。这证实了在全局假设 $totalVotes \ge 0$ 下，totalVotes 和 votesInFavor 之间的关系在所有可能的合约状态下都保持有效。

这就是 全局公理 如何帮助 Prover 推理在每个程序状态中普遍为真的属性。通过定义 axiom totalVotes >= 0，我们建立了一个在整个验证过程中都成立的逻辑事实，而无需在每次状态转换后重新证明它。在这种情况下，公理捕捉了一个直观的真理，即总票数永远不能为负，并允许 Prover 高效且可靠地验证不变量。

结论

在本章中，我们演示了不受约束的幽灵变量如何导致不变量证明在基本情况下失败。由于在不变量中使用 require 进行初始化是无效的，我们引入了 公理（axioms） 作为正确的替代方案。具体来说，init_state 公理通过定义幽灵变量的有效起始值解决了初始化问题，而 全局公理 则表达了在所有合约状态下都保持为真的属性。

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

原文链接： rareskills.io/post/certo...

登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

本文参与登链社区写作激励计划，好文好收益，欢迎正在阅读的你也加入。

约束不变量中的幽灵变量

在不变量中约束幽灵变量

理解问题

理解违规原因

为什么我们不能使用 require 语句？

“公理”介绍

什么是“初始状态公理”

什么是“全局公理”

在我们的规范中使用 `init_state` 公理

实际应用全局公理

结论

0 条评论

文章目录

约束不变量中的幽灵变量

在不变量中约束幽灵变量

理解问题

理解违规原因

为什么我们不能使用 require 语句？

“公理”介绍

什么是“初始状态公理”

什么是“全局公理”

在我们的规范中使用 init_state 公理

实际应用全局公理

结论

0 条评论

文章目录

在我们的规范中使用 `init_state` 公理