Certora验证器8.1.0版本发布，包含新功能和重大变更

此版本中的重大更改

重要提示：此版本引入了重大更改，可能需要更新你的规范、配置或工作流程。请在升级前查看以下更改。

最低 Java 版本提高到 19

更改内容：

Certora Prover 现在需要 Java 运行时环境（JRE）19 或更高版本。

影响：

如果你使用旧版本的 JRE（18 或以下），Prover 将无法启动。

所需操作：

在运行新版本之前，请将你的 Java 安装更新到 19 或更高版本。

Java 安装说明

最低 Python 版本提高到 3.9

更改内容：

Python 3.8 已经达到生命周期结束（end-of-life），certora-cli 将不再明确支持此版本。

影响：

如果你使用 Python 3.8，则在使用较新版本的 certora-cli 时可能会遇到兼容性问题或安装错误。

所需操作：

将你的 Python 安装升级到 3.9 或更高版本。

Python 安装说明

默认情况下现在运行健全性检查（包括不变量基本情况）

更改内容：

Prover 现在默认运行基本的健全性检查，包括对空虚性和简单条件的检查。此更改等效于在早期版本中设置 “rule_sanity”: “basic”。

作为此更新的一部分，我们修复了一个错误：现在可以正确执行不变量基本情况的空虚性检查。以前，此检查会被悄悄跳过。

影响：

作业的运行时间可能会稍长一些，并且某些先前通过的规则现在可能会由于未能通过健全性检查而失败。这确保了规则有意义，而不是琐碎或空洞地满足。

所需操作：

如果你遇到新的违规情况，请查看你的规则并检查 Rule Notification 选项卡。我们在文档中更详细地解释了健全性检查失败。

文档

requireInvariant 的新语义

更改内容：

requireInvariant 的语义已更新，以解决一个不健全的问题。以前，它被视为 require(<invariant expression>) 的快捷方式，这可能会错误地假设不变量在任意点都成立，即使无法保证这一点。

在此版本中，requireInvariant 仅在规则启动之前假定不变量为真，而其真实性已得到证明。

影响：

此更改使不变量假设默认情况下是可靠的。如果你的规范依赖于旧的行为，你现在可能会看到新的失败或结果变化。

所需操作：

查看 requireInvariant 的用法，并确保它仅出现在规则开始之前不变量应该成立的位置。

文档

示例

Solana 和 Soroban 验证必须使用专用命令

更改内容：

不再支持使用 certoraRun 运行 Solana 和 Soroban 作业。这些目标现在需要其专用的 CLI 入口点：

• 对 Solana 作业使用 certoraSolanaProver
• 对 Soroban 作业使用 certoraSorobanProver

影响：

尝试使用 certoraRun 运行 Solana 或 Soroban 合约现在会导致错误。

所需操作：

更新你的工作流程和脚本，以使用适用于 Solana 或 Soroban 验证的相应命令。

默认报告链接现在是私有的

更改内容：

默认情况下，所有新生成的验证报告链接现在都是私有的，这意味着只有你可以访问它们。在持续集成（CI）运行中，报告链接将继续默认公开，以避免破坏现有工作流程。

验证报告 UI 已更新，在“共享链接”按钮旁边有一个下拉菜单。此菜单允许你：

• 复制私有或公共链接
• （可选）在复制链接时保留当前的报告视图状态（例如，打开的选项卡、滚动位置、高亮显示的行）

新的 url_visibility 选项允许你在运行作业时控制链接类型，可以通过命令行或在配置文件中进行控制。

影响：

如果你的当前工作流程依赖于公共链接，你现在需要显式设置 url_visibility public 以保留旧的行为。

所需操作：

如果你的用例需要公共链接，请更新你的配置或 CLI 命令。

文档

CVL 函数的回滚处理

更改内容：

CVL 函数现在支持显式回滚行为：

• 在 CVL 函数中使用 revert 关键字来模拟失败场景。
• CVL 函数现在可以使用 @withrevert 后缀调用，以推理成功和恢复情况。

影响：

以前，Prover 不会推理 CVL 函数回滚，即使它用于总结使用 @withrevert 调用的 Solidity 函数。这导致了不正确的验证结果，因为 CVL 摘要中可能的回滚被静默忽略。

通过此更新，Prover 会检查 CVL 函数是否可能回滚，并且先前通过的规则现在可能会由于缺少回滚建模而失败。

所需操作：

如果使用 @withrevert 调用 Solidity 函数并使用 CVL 函数对其进行总结，请确保 CVL 函数正确地考虑了成功和失败路径。根据需要使用 revert 关键字来准确捕获回滚条件。

文档

示例

已删除已弃用的 CLI 选项

更改内容：

以前打印警告的几个 CLI 选项不再受支持。这些选项已逐步淘汰，并且在大多数情况下，已由较新的替代方案取代。如果你在升级后遇到错误，请检查你的配置文件或脚本中是否存在不受支持的标志，并相应地替换它们。

你可以在文档中找到支持的 CLI 选项的完整列表。

文档

adaptiveSolverConfig false 替换为 backendStrategy singlerace

更改内容：

Prover 不再接受 -adaptiveSolverConfig false 选项作为 prover_arg。它已被一个新选项替换：-backendStrategy singlerace。

影响：

使用旧选项现在会导致错误。

所需操作：

更新你的配置文件 prover_args 以使用 -backendStrategy singlerace 代替。

新的 Prover 更新

CVL 规范格式化程序

现在有一个新的命令行工具可用于格式化 CVL 规范文件。你可以从终端运行它：

certoraCVLFormatter <SPEC_FILE> --overwrite

这将自动重新格式化你的 CVL 代码，以实现一致性和可读性。

该格式化程序也可作为 VSCode 扩展 使用。

文档

重定向摘要

你现在可以通过将调用重定向到自定义 Solidity 函数来总结采用存储参数的内部函数。这解锁了以前无法实现表达式摘要的新用例。

文档

示例

瞬态存储Hook

CVL 现在支持瞬态存储字段上的Hook，从而可以精确地推理读取（TLOAD）和写入（TSTORE）。你可以为这些操作码定义具有命名存储变量的Hook，并像常规存储字段一样直接在 CVL 中访问相应的字段。

注意：仅当禁用存储拆分时才支持 ALLTSTORE 和 ALLTLOAD Hook，这与常规存储Hook行为一致。

文档

示例

Foundry Remappings 支持

你现在可以在编译合约时使用 Foundry 的内置重映射解析。Prover 会自动运行 forge remappings 以收集在你的 foundry.toml 及其依赖项中定义的所有包映射。当未明确提供 packages 时，此功能处于活动状态，从而可以简化设置并更好地兼容基于 Foundry 的项目。

文档

示例

升级到 8.1.0 版本

通过确保你的软件是最新的版本来访问这些更新。要升级到 v8.1.0，只需运行 pip install --upgrade certora-cli。

与往常一样，我们欢迎并感谢你的反馈。

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