AutoProver 与人工编写的 Aave v4 规范

我们把 AutoProver 指向 Aave v4 Hub，没有把我们已有的任何工作交给它，而是让它自己编写规范。它给出了 Hub 的偿付能力不变量：一份份额的价值永远不低于一个资产。这与我们手动编写的 P-06 是同一个属性，能在无人辅助的情况下得出这一点并非易事。

它还投入了相当大的努力来证明这条性质。如果你只是把该不变量直接交给 Prover，它是通不过的；AutoProver 做了我们本来也会做的那些工作，才让它通过。

这次运行没有产出的是 P-06 的另一半：份额价格永远不会下降。这两者听起来像是同一个属性，但捕获的是不同的 bug。下限（floor）捕获了我们在 Hub 上报告的一个问题；单调性捕获了另一个问题，而 AutoProver 证明的任何内容都无法捕获后一个问题。

AutoProver 会交给你大量真实且可检查的规则，其中也包括一些重要的规则。然而，它还不是一个能够完全洞悉你意图的完美预言机。你仍然需要确保与协议安全最相关的那些属性得到了验证。

我们双方都编写了偿付能力

以下是 AutoProver 在其生成的规范文件中写下的内容：

/// 属性 20 的核心（归纳）形式：在存储的分类账上衡量时，
/// 新增份额的价格永远不会低于每份一个资产。由于该语句为
/// `addedShares + realizedFees <= liquidity + swept + owed`，
/// 它也因此意味着 `totalAddedAssets` 永远不会下溢。
invariant added_shares_do_not_exceed_total_added_assets(uint256 assetId)
    currentContract._assets[assetId].addedShares
        <= totalAddedAssetsStored(assetId)

Certora 将这条规则记为 P-06，totalAssetsVsShares：“新增资产的总和大于或等于新增份额的总和。” 偿付能力是每个借贷协议都应该具备的属性；任何做过借贷协议的人都知道要去找它，而 Hub 的分类账会告诉你这些条件必须是什么。任何对 Hub.sol 的认真工作，都必须对偿付能力进行推理。

AutoProver 并不是简单地看到这条属性并照原样转写。它自己提出了这个不变量，并自动围绕它构建起了证明。

其他属性也是如此。它编写了五个不变量，说明每个资产级总数等于其各 Spoke 行之和；这些不变量共同构成了我们手动推导出的 P-05。它编写了这五个不变量所依赖的四个字段约束：已列出资产的 drawn index 永远不会低于 RAY，流动性费用不超过 100%，资产 id 当且仅当小于资产数量时才被列出，premium offset 永远不会高于 premium shares。这些属性共同构成了我们的 P-04。它还证明了 Hub 的代币余额足以覆盖每种资产记录的流动性，即我们的 solvency_external。

更有趣的不只是它发现了相同的属性，还有它发现了相同的依赖图。它的偿付能力证明中那五条 requireInvariant 行，正是我们的字段完整性组。它推断出偿付能力边界依赖于这四个事实；而要学到这些，通常需要看着证明失败，经历大量迭代、工作和时间。AutoProver 将这一迭代过程自动化，节省了我们的时间，让我们能够对协议正确性进行更高层次的思考。

它能完成困难的证明

一个看似简单直观的属性，背后可能有着复杂的证明依据。

如果按原样交给它，addedShares <= totalAddedAssets 是无法通过验证的。该查询必须同时推理利息增长指数以及操作自身的份额算术，最终在 add、remove、draw 和 restore 上失败。AutoProver 对此做了三件事：

它拆分了证明。 每个会变更状态的 Hub 入口点都是 accrue(); op()，因此转换被分解成两步。假设资产已经计息，开头的 accrue() 便被消去，只给 Prover 留下操作。计息部分于是成为它自己的规则 accrual_preserves_added_shares_bound。第三条规则再把结果从存储的分类账提升到 getAddedAssets 实际返回的数字。三个入口点完全不调用 accrue()，因此它们有自己的 preserved 块。

它检查了自己的规则是否真的证明了什么。 这条提升规则以 !lastReverted 为前提，而这正是那种在调用总是回滚时会空真通过的形态。规范文件说明了这一点，并说明了真正的证明依据所在：

“下面的提升规则以 !lastReverted 为前提，因此已计息索引处的无下溢内容由 accrual_preserves_added_shares_bound 承载；该规则的右侧是纯 mathint 算术，因此不可能被空真满足。”

它绕开了汇编。 四个 SharesMath 辅助函数在 CVL 中被精确重写，用两侧的乘法约束来固定每个商，而不是执行除法，从而绕开 OpenZeppelin 的 512 位 Math.mulDiv 汇编，并把份额价格论证所需的乘积事实直接交给求解器。它自己的注释是：“这最终让 eliminateDeficit 得到了验证。”

所以，它不是那种只能表述简单性质的工具。它完成了那种我们通常预期要由自己来做的证明工作。下一节要讲的，是一个 AutoProver 识别出来并试图证明、但在可用预算内未能完成的属性。

它未能完成的规则

P-06 有两个部分：AutoProver 证明了其中的基础部分；另一个是 supplyExchangeRateIsMonotonic——份额价格永远不会下降。AutoProver 也识别并形式化了这个属性，但证明在完成之前就超出了可用预算。AutoProver 明确陈述了该属性：

“对于每个已列出资产，供应份额价格 (totalAddedAssets() + SharesMath.VIRTUAL_ASSETS) / (asset.addedShares + SharesMath.VIRTUAL_SHARES) 永远不会因任何外部可调用函数而下降：add、remove、draw、restore、reportDeficit、eliminateDeficit、refreshPremium、transferShares、payFeeShares、mintFeeShares、sweep、reclaim、addSpoke/updateSpokeConfig/updateAssetConfig/setInterestRateData 或计息过程。”

这个属性很重要。我们在 Hub 上报告的两个利率相关发现都违反了单调性，而其中只有一个同时违反了基础部分。

M-02 同时破坏了这两个属性。totalAddedAssets 过去在两个地方分别独立向上取整，而 reportDeficit 会在它们之间转移价值，因此转移后的总数可能比之前更小。这会使得价格低于 1，所以基础的偿付能力属性能够捕获它。AutoProver 已证明的那个不变量本来也能捕获这个问题。

M-01 则只破坏了单调性。getFeeShares() 当时是这样计算费用的：

uint256 feesAmount = indexDelta
  .rayMulDown(asset.baseDrawnShares + asset.premiumDrawnShares)
  .percentMulDown(liquidityFee);

它在合并后的 base 和 premium drawn shares 上向下取整，而 totalDebt 是对两者分别计算的。两条路径在取整上不一致，因此计息可能会削减股东的价值。它从未把价格压到 1 以下，只是在费用路径上让价格朝错误方向稍稍移动了一点。基础的偿付能力属性对此视而不见。

这就是两个部分之间的差距，而且这绝非一个微小的技术细节。一个协议可以轻松地让每份份额的价值保持在 1 个资产以上，同时在单笔交易中从持有者身上悄悄泄漏价值。基础的偿付能力是合理性检查，单调性才是真正的验证。

编写这条规则本身并不难：读取利率，调用方法，再次读取利率，断言它没有下降。困难之处在于决定这就是那条绝不能向下移动的利率，并注意到费用路径与债务路径在取整上并不一致。这个决定来自追问协议对用户负有什么义务，而这一点在源代码中并没有被明明白白地写出来。AutoProver 自动得出了这个（正确的）决定，但由于我们的 beta 版存在技术限制，最终没能完成证明。

覆盖不是任务

这次运行返回了 104 条规则。其中大多数真实、可检查，但并不特别引人注目：注册表条目格式良好，未列出的槽位为空，配置 setter 写入它们声称要写入的字段。这些都是值得知道的内容。虽然它们并不是你会围绕其构建一个验证委托的那类属性，但检查它们仍然很有用。

在审计或形式化验证委托之前，先证明你系统中的这些基本正确性属性是很有用的。这样，验证委托就能专注于确保没有遗漏任何关键属性。

一次验证委托的目的不是生成规则列表，而是精确识别出那些为了使协议及其用户在经济上安全而必须成立的不变量，然后把它们证明出来。在 Hub 上，这意味着要判断出供应利率必须是单调的而不仅仅是有界的；在触及同一数量的每一条路径上，取整都必须保持一致；并且不能允许两次添加同一个 spoke 而悄悄把一个活跃头寸清零。这三个判断带来了三个发现。

在哪些情况下 AutoProver 是正确的选择

如果一个协议完全没有做形式化验证，那么这是很有力的第一步，我们会对任何人都这么说。你能在几小时内获得关于实际代码的大量经机器检查的属性，无需自己做任何规范工作，并且无论你当前处于哪个 commit 都适用。你不必成为形式化验证专家，也能立刻得到一套不错的验证套件。此外，它也是日后继续扩展的合理基础，无论你是想扩大覆盖范围，还是想构建更多代码。

如果你需要的是关于你的协议可能以哪些特定方式亏损的保证，那么生成的规范只是一个起点，而不是全部答案。专业的验证委托仍然需要识别最重要的属性、找出缺失了什么，并把它们证明出来。先运行 AutoProver，会让这一委托更短、更顺畅、更聚焦。在 Hub 上，研究人员介入之前，它就已经完成了大量工作。我们不必从空白规范开始，而是可以基于一大批经机器检查的属性展开工作，其中包括偿付能力不变量及其所依赖的支撑规则。

让它指向你自己的代码。 AutoProver 就在 Certora 平台 上。判断它是否好用的有效方式，是把它用在你熟悉的合约上：阅读它生成的规范，看看你最关心的属性是否在里面。我们正在持续改进 AutoProver，让它覆盖更难、更有影响力的属性。来和我们谈谈，我们会找到帮助你安全交付的最佳方式。

• 原文链接： certora.com/blog/autopro...
• 鸿途知科网 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～