合约测试指南：实现第一个智能合约不变性测试

学习如何使用 Solidity 实现和测试智能合约的不变性。本指南涵盖了跟踪变量、定义属性，以及使用 Echidna、Medusa 和 Foundry 进行模糊测试。

引言

不变性在告诉我们智能合约系统应该如何行为方面非常强大。

在加密行业，最著名的模因之一是来自 Uniswap 的 k = x * y 不变性公式，该公式在多个版本和分叉中保证了数万亿美元的交易。

更广泛地说，不变性是关于某个系统的声明，这些声明应该始终为真。我们还可以定义仅在某些情况下成立的声明。我们称这些为属性。所有这些都有助于我们确定系统应该如何运行。

我们可以使用文档、白皮书和 README 来为任何系统定义以下属性类型。它们描述了系统应该如何工作：

• 有效状态

• 状态转换

• 变量转换

• 高级属性

在我们之前的文章中，我们看到如何为广泛使用的 ERC4626 保管库标准定义这些属性类型中的每一个。本文中，我们将讨论如何实际将这些属性作为代码实现，以便我们可以使用模糊测试工具进行测试。

一旦我们在代码中定义了属性，我们就只差一步就可以利用数千个调用序列进行模糊测试，以模拟用户交互。这就是我们发现关键bugs的方法！

作为代码的不变性

我们将测试在之前文章中定义的以下属性：

1. 股份偿付能力 - 股份代币的 totalSupply 必须 >= 每个用户的股份。

2. 保管库余额增加 - 基础资产的保管库余额必须按铸造的股份数量成比例增加。

3. 赎回后的 totalSupply - 在赎回时，totalSupply 必须按赎回的股份数量成比例减少。

4. 每股价格 - 每股价格不应更改，除非调用 deposit / withdraw

为了简单起见，下面每个属性的实现均使用 Chimera 的标准化 断言包装器，以便它们可以与 Echidna、Medusa 和 Foundry 一起工作。

全局与内联

在深入我们的属性实现之前，我们需要定义两种属性类型：全局和内联。

全局属性是在目标函数的任何调用之后由模糊测试工具检查的，因此必须始终成立。这些是我们的教科书 不变性，因为它们定义了系统的特性，这些特性在任何调用操作的情况下都应该成立。Uniswap 的 k = x * y 公式就是一个例子，因为它在所有情况下都应该成立。

内联属性是在目标函数的处理程序内定义的。处理程序是我们用于包装对目标合约的调用的函数。因此，这些属性仅在对其中一个处理程序的调用中被检查。这使我们能够断言函数调用对状态产生了某种影响，但根据定义，它们不需要在其他函数调用中成立。这些对实现仅在某些状态改变操作中需要成立的属性非常有用。

在下面的示例中，我们将实现全局和内联属性。

设置

我们将为这个repo中提供的示例实现不变性。这是一个简单的ERC4626Tester合约。它继承了 OpenZeppelin 的实现，并增加了一些集成测试的功能。

如我们在之前的文章中所述，我们使用 Recon 构建器为我们搭建了所有相关的目标函数。然后我们使用以下 Setup 合约部署我们的测试合约：

setup 函数使用一个 MockERC20Tester 实例的基础资产部署一个新的 ERC4626Tester 合约的实例。

如果你不熟悉如何创建不变性测试的搭建，请查看这篇文章。

辅助跟踪变量

在我们开始实现不变性之前，我们需要在我们的搭建中添加一些帮助程序，以便更轻松地完成工作。

BeforeAfter 合约中的跟踪变量帮助我们跟踪目标函数处理程序中任何操作之前和之后系统的状态。

对于我们的 ERC4626 保管库，我们可以用它来跟踪股份的 totalSupply 和用户股份的总和：

我们定义的 BeforeAfter 变量通过 updateBeforeAfter 修饰符更新，我们将其添加到目标函数中。这使我们能够缓存给定函数调用之前和之后系统的状态。

ghostTotalShares 是一个幽灵变量。它跟踪系统中未定义的状态值，但可以从其他状态值推导而来。在我们的例子中，用户股份的总和。

由于我们在设置中仅使用一个参与者 (address(this)) ，因此我们不需要对多个用户的 ghostTotalShares 进行求和。我们可以假设它与参与者的股份相同，因为我们的参与者，也就是将调用我们的目标函数的地址，将是唯一一个存入保管库的人。我们将在未来的文章中解释如何使用多个参与者。

这些幽灵变量让我们能够对这些值应该是什么进行断言。

定义 Solidity 不变性

现在，所有必要的设置和帮助程序都到位，我们可以开始将我们的不变性从英语翻译成 Solidity。

1. 股份偿付能力

对于这个全局属性，股份代币的 totalSupply 必须 >= 每个用户的股份，我们可以使用我们之前设置的 BeforeAfter 变量：

这个属性访问 BeforeAfter 合约中的 ghostTotalShares 和 vaultTotalShares，并断言 ghostTotalShares <= vaultTotalShares，如果断言为假，则会将消息记录到控制台。

要将我们的不变性从英语翻译成 Solidity，我们只需读取在 BeforeAfter 变量中更新的缓存值并对其进行断言，这便将我们的书面属性转化为逻辑断言。

这个属性是一个公共函数，因此模糊测试工具将随机调用它。它也是一个全局属性，因此必须始终成立。模糊测试工具会寻找一个调用序列，使逻辑语句为假，换句话说，破坏不变性。如果这是可能的，我们将在终端中看到该调用序列，以便我们理解不变性是如何被破坏的。

Echidna 和 Medusa 模糊测试工具是“智能”的，因此它们使用缩减技术将随机调用序列减少到打破不变性所需的最小数量，从中切除任何不必要的调用。

2. 保管库余额增加

对于 基础资产的保管库余额必须按铸造的股份数量成比例增加 的属性，我们可以在我们的属性定义中使用 ERC4626 规范中的 previewMint 函数。这样我们可以检查用户为特定基础资产的存款可以获得多少股份。

在我们的属性实现中，我们使用此检查保管库在调用 mint 函数之前预期接收多少资产。然后，我们可以将此与保管库实际接收到的资产数量进行比较，如下所示：

该属性仅需在 mint 函数中检查，因此我们将其作为内联属性进行检查。

我们只需要断言保管库的余额在铸造后等于其之前的余额加上为了获得特定数量股份而需要存入的资产数量，这可以通过调用 previewMint 来获得。

3. 赎回后的 totalSupply

我们的属性声明 totalSupply 必须按赎回时销毁的股份数量成比例减少。

为验证这一点，我们通过在我们的实现中直接读取合约状态来检查股份的 totalSupply。我们使用变量 totalSupplyBefore 和 totalSupplyAfter 记录函数调用之前和之后的值。最后，我们断言 totalSupply 按照赎回的股份数量减少：

我们可以从 BeforeAfter 合约中读取 totalSupply 的值，这些值是用 vaultTotalShares 变量缓存的。

在这个属性中，我们直接调用 __before() 和 __after() 函数，因为我们需要在函数调用后读取值以进行断言。这无法通过 updateBeforeAfter 修饰符实现，因为 __after() 函数只会在处理函数执行完毕后才会被调用。

4. 每股价格

在实现属性 每股价格不应更改，除非调用 deposit / withdraw 时，我们会迅速发现 ERC4626 接口缺乏查询价格的直接函数。

然而，我们可以利用要传递以铸造 1 股的资产数量作为价格的类似物，因此我们只需在 BeforeAfter 合约中跟踪这个数量：

为了计算每股价格，我们使用 previewMint 函数，估算我们需要存入多少资产才能铸造出一股，采用保管库的基础十进制精度。

现在，我们可以调用 __before() 和 __after() 函数来更新处理程序中的这些变量，类似于我们在属性 3 中所做的。然后，我们可以读取这些值，以确定在所有感兴趣的处理程序的调用中，价格是否发生了变化。

我们只关心在 deposit、mint、redeem 和 withdraw 之外的调用导致的价格变化。因此，我们只将此属性的断言添加到以下感兴趣的目标函数中：

存款或赎回会导致每股价格发生变化。因此，我们只在 approve 和 transfer 函数中检查此属性。

我们使用等式断言包装器断言任何调用 approve 和 transfer 函数时 pricePerShare 是相同的。

下一步

现在我们有了实际的属性，我们需要测试它们。我们必须检查它们在所有条件下是否成立，通过长时间的模糊测试运行。

这就是我们构建Recon 云运行器的原因，它允许你执行可以持续数周的模糊测试作业。这允许更好地探索系统的可能状态。它为我们提供了更多信心，确保我们定义的属性在所有可达状态下成立。

经过长时间的模糊测试作业，有三种结果：属性成立，由于不正确的规范而破坏，或者由于真实的bug而破坏。

如果你的属性确实成立，则表示该系统符合规范，或者你缺少对目标函数的测试覆盖率。

在未来的文章中，我们将看到如何整理所有这些案例。这将帮助你确定设置是否需要修复。

结论

我们已经看过如何在 Recon 搭建中设置帮助程序，使我们能够以更简单的方式在 Solidity 中定义属性。这有助于简化我们的测试，使用可重用的状态跟踪变量读取状态，而无需在每个测试中重新定义。

我们实现的属性可以分为全局或内联。全局属性允许我们检查在所有函数调用后应该成立的属性，我们称这些属性为不变性。内联属性则允许我们仅在特定函数调用之后检查与系统状态相关的逻辑语句是否成立。

我们看到如何使用断言将这些属性从英语翻译为 Solidity 函数。我们通过使用 BeforeAfter 跟踪帮助程序并在必要时直接从合约读取状态值，并对其应为的值进行断言来实现这一点。

在下一篇文章中，我们将讨论确保我们的测试有效执行所需做的事情。

与此同时，当你运行上述属性时会发生什么？你会遇到有效的break或由于实现错误而导致的break吗？

• 原文链接： getrecon.substack.com/p/...
• 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～