这篇文章主要介绍了 Certora Prover 的新更新，包括 CVL 中新增的 links 块，用于更直观、类型安全地把合约存储变量绑定到目标合约；TAC dump 的可视化诊断能力增强，支持前进后退、变量联动高亮和数据流图；以及 requireInvariant 在强不变量场景下的语义改进，降低外部调用后出现误报反例的概率。同时，文章还说明了 GitHub App 的评论配置新选项 gh-review 与 gh-review-jobs，并给出升级到 8.11.3 的方式。
新的 Prover 更新
新增 CVL “links” 块
CVL 中新增的 links 块允许你在 spec 中以声明式方式直接将合约存储变量绑定到目标合约，作为 .conf 文件中 link 和 struct_link 字段的首选替代方案。它支持字段访问、数组和映射索引（使用数字字面量、to_bytesX 或合约别名）、通配符、结构体遍历，以及每个 slot 对应多个链接目标。所有路径都会根据合约的存储布局进行完整的类型检查，在编译时捕获诸如未知字段、类型不匹配以及静态数组越界索引之类的错误。
文档
示例
TAC Dump 改进
用于查看 “TAC dump” 诊断信息的 HTML 得到了一些改进：
- 增加了对浏览器后退和前进按钮的支持。
- 点击某个变量时，它的输入和输出变量也会被高亮显示，以便更容易找到它们。
- 新增了 “Dataflow” 视图。在这个视图中，可以通过变量图跟踪数据流动。
文档
“requireInvariant” 在强不变式下的语义改进
当某个规则或不变式使用带有 strong invariant 的 requireInvariant 命令时，该不变式会在规则/不变式中的任意 HAVOC 之后被重新假设。这可以减少由于（强）不变式被破坏而在外部调用后出现的错误反例。
对我们的 Github App 的更改
新的 Review Comment 功能
gh-review - 用于指示何时向 PR 添加 review comment。可选项为 always、failure 和 never。默认值为 always。gh-review-jobs - 用于指示在 GitHub review comment 中包含哪些 jobs。可选项为 all 或 failed。默认值为 all。
如果 gh-review 为 never，状态链接会指向一个摘要页面，例如这里。该链接仅适用于公开仓库；私有仓库仍会指向 Prover 作业页面。我们还在文档中新增了一个更全面的 Troubleshooting 部分。
升级到 8.11.3 版本
请确保你的软件已更新到最新版本，以获取这些更新。要升级到 v8.11.3，只需运行 pip install --upgrade certora-cli。
一如既往，你可以在我们的 Discord 服务器获得支持。我们欢迎并感谢你的反馈。
