如何在不被 REKT 的情况下优化你的Gas消耗

Certora 等价检查器的使用指南

作者：Netanel Rubin-Blaier

编辑：Thomas Adams, Uri Kirstein, Yura Sherman.

介绍：去中心化金融的三难困境

越来越多的人达成共识，去中心化金融（DeFi）世界面临的一个关键障碍是智能合约的安全性问题。

确实，当新闻周期被欺诈和损失的故事主导时，更广泛的主流接受仍然是一个遥不可及的前景，更不用说与当前的金融服务和投资银行巨头如Visa、J.P. Morgan和Goldman-Sachs的真正竞争了。

与许多“区块链外部”人士所说的相反，这个问题不仅仅是由于过度宣传的项目带来了不可理喻的截止日期或是有着“牛仔编码”文化的初创公司造成的。

这些被广泛宣传的因素在某些情况下确实存在，并且它们肯定没有帮助，但将所有责任仅仅归咎于这些因素是完全没有道理的，任何“区块链内部”的人都可以告诉你。

实际上，情况要恶劣得多。

这是因为开发一个 DeFi 产品是一个具有欺骗性深度的工程问题——虽然写一个在 Solidity 中（大部分）可以实现你想要功能的智能合约容易，但要做到这一点得当却很难。就像 Vitalik Buterin 的著名区块链三难困境一样，智能合约开发的过程也受到三个分离且时常相互冲突的目标的指导：

• 最小化Gas消耗。 就像高频交易一样，看似“微不足道”的优化可能对Gas成本及其可用性产生深远的影响。在用尽通常的“技巧包”后，提升各个操作的Gas成本通常需要用汇编语言而不是 Solidity（或 Viper）编写，或者寻找聪明的技巧来计算非线性和计算密集型函数的近似值。
• 最大化安全性。 与硬件一样，智能合约是根据设计不可变的，这意味着在开发过程中引入的任何错误都是永久存在的。确实，可升级的合约存在，可以绕过不可变性。然而，它们的存在带来了另一个权衡：用户永远无法确定自己交互的合约不会改变，而每次升级都会有引入新错误的风险。加上 DeFi 协议所处理的大量资金和 EOA 地址与现实世界身份之间固有的解耦（以及“代码即法律”哲学），这些现实可以使代码中的任何漏洞都变得极其危险和代价高昂。特别是，这意味着必须非常小心四舍五入错误、边缘情况和数学设计问题。

• 最小化上市时间。 这是任何软件项目中的紧迫问题，但在去中心化金融这个竞争极其激烈和高度波动的领域更是如此。不幸的是，即使一个人在Gas优化和安全方面同时取得了目标，很明显每一步施加的额外检查将显著减慢开发过程。

开发周期中的形式验证

Certora 正在开发一种名为等价检查器的新产品，以帮助开发人员达到更好的平衡，而无需在这三项要求之一上妥协。与专注于测试和安全的 Certora Prover 不同，这种轻量级的形式验证工具允许 DeFi 程序员比较同一数学公式的不同版本，这些公式可以用：

1. 低级（Yul 或汇编）
2. 高级（Solidity）
3. 纯逻辑（编码于Certora 验证语言，简称 CVL）

并证明它们是等价的（稍后将详细说明）。它旨在作为项目整个生命周期中的快速开发工具，帮助提升安全性、开发时间和Gas消耗。

本文其余部分展示了该新工具在一个具体案例中的工作流程。我们将介绍等价检查器的不同模式，并演示它如何能够在实时代码中立即检测出一个著名的旧错误和一个新的、以前未发现的错误（备注：读者应注意这是一个低严重性的错误，选择它是出于教学目的。在本博客的后续部分中，我们将揭示并分析一个更复杂的案例，其中通过等价检查器检测到一个高严重性的错误——敬请期待更多内容！）

但首先，

“功能等价性”究竟是什么意思？

如果一个 Solidity/Yul 函数不读取或修改状态（尽管它们可以在发生错误时回滚潜在的状态更改），我们称它为纯函数。它可以有多个输入和输出值。例如，以下函数是纯的：

    function safeAdd(uint a, uint b) public pure returns (uint c) {
        c = a + b;
        require(c >= a);
    }

我们说两个纯函数 f(…) 和 g(…) 是等价的，如果：

1. 它们具有相同的输入/输出变量。
2. [假设第1点成立：] 对于给定的输入值元组 -

(a) f 仅在 g 也回退时回退。

(b) [假设 f 和 g 不回退：] f 和 g 的返回值是相同的。

当然，这一定义可以扩展到适合 EVM 字节码的适当片段，并在以太坊的黄皮书的形式中加以细化。（纯函数与逻辑公式之间的等价性是类似的，但稍微更微妙，第二个例子将在下面解释得更清楚）。

现在我们已经恰当地定义了等价性，是时候开始我们认真讨论了。

背景：实现定点除法

Ethereum 虚拟机（EVM）仅原生支持两种数据类型：256 位单元和 8 位字节。此外，大多数 EVM 操作码一次处理单元大小的数据块，包括所有的数学操作。因此，在以太坊中，实际上只有两种数字数据类型：

• 有符号 256 位整数。
• 无符号 256 位整数。

这让人失望，因为几乎任何类型的金融应用都需要实现某种支持小数算术的功能。实现这一目标的方式有几种，但在 DeFi 应用中（远远）最流行的是定点数。这些基本上是分子和被定义为某个预定义常数的简单分数，通常是 2 的幂（“二进制”）或 10（“十进制”）。在十进制情况下，标准选择的分母是 10¹⁸（称为“wad”）或 10²⁷（称为“ray”）。因此，现有 Solidity 定点库通常将一个 wad 表示为一个 256 位整数。这对于加法和减法来说是相当简单的，但在进行乘法或除法时，必须重新缩放结果以获得正确的答案。

例如，

1.5 * 2.7 == 4.05
// 正常整数算术添加数量级：
150 * 270 == 40500
// Wad 算术不添加数量级：
wadMul(1.5 ether, 2.7 ether) == 4.05 ether

考虑以下测试用例。我们想要编写一个名为 wadDiv 的函数，该函数将两个 wad 相除，四舍五入 大于或等于五 到最近的 wad。这些类型的算术函数在 DeFi 中非常常见。它们有助于考虑整数算术与实际小数算术之间的差异。

第一步：测试代码

作为第一步，我们考虑如下在 Solidity 中编写的 wadDiv 的参考实现：

uint256 internal constant WAD = 1e18;
function wadDivSol(uint256 a, uint256 b) public pure returns (uint256 c)
{
  c = (a * WAD + (b/2)) / b;
  return c;
}

在尝试优化它时，我们尝试了一些汇编并创建了以下临时 Yul 版本：

function wadDivAsm(uint256 a, uint256 b) public pure returns (uint256 c)
{
  assembly
  {
    if iszero(iszero(gt(a, div(sub(not(0), div(b, 2)), WAD))))
    { revert(0, 0) }
    c := div(add(mul(a, WAD), div(b, 2)), b)
  }
}

确实，我们看到Gas成本大幅降低：Solidity 版本执行计算大约需要 ~860 Gas，而汇编版本仅需 ~140 Gas。

问题。 这是否可行（即这两个函数是等价的）？

与其苦思冥想出答案，等价检查器的通用规则模板会立即生成以下两个规则，用 CVL（Certora 验证语言）编写，并提交给 Prover 进行形式验证。

几乎立即，证明者检测到了两个回退条件之间的差异：

并产生了以下反例：

（为什么？因为在 Yul 中的除零返回零而不是回退！见链接的 推特线程 以获得详细讨论）

第二步：测试逻辑

假设我们已经修复了错误，并编写了新的 Yul 版本：

function wadDivAsmNew(uint256 a, uint256 b) public pure returns (uint256 c)
{
  assembly
  {
    if or(iszero(b), iszero(iszero(gt(a, div(sub(not(0), div(b, 2)), WAD)))))
    { revert(0, 0) }
    c := div(add(mul(a, WAD), div(b, 2)), b)
  }
}

问题。 我们完成了吗？

好消息： 运行等价检查器现在表明它与 Solidity 版本相同！

坏消息： 别急……因为我们原来的 Solidity 版本是错误的。

要看到这一点，我们需要在不同的配置中运行等价检查器。在上一段中，我们解释了如何使用等价检查器比较代码（wadDivAsmOld）与代码（wadDivSol / wadDivAsmNew）的比较。

现在我们需要比较一段代码（wadDivSol），它在 EVM 上进行某种数学计算，和两个编码其行为的数学函数：

• wadDiv_ShouldRevert — 编码所需的回退条件，即一个布尔值函数，接受与 wadDivSol 相同的输入参数，仅在 EVM 执行 wadDivSol 时应导致回退时返回 true。在我们的案例中，我们希望 wadDivSol 仅在分母为零或结果大于 2²⁵⁶-1（可以存储在 uint256 中的最大整数）时回退，导致整数溢出。
• wadDiv_ComputeInMathint — 接受与 wadDivSol 相同的输入参数并编码输出的公式，该输出是在整数上计算得出的。

用 CVL 编写的这两个函数的规范是 -

在这种情况下，等价性测试的内容是检查以下两个规则是否为真 -

它们意味着什么？

• 哦，第一个规则正是它看起来的那样。它表示 wadDiv_ShouldRevert 当且仅当 wadDivSol 回退时才回退。
• 第二个规则则更微妙。它说明在相同的输入下，wadDivSol 和 wadDiv_ComputeInMathint 返回相同的 uint256 值，前提是 wadDivSol 没有回退（注意第二个规则中没有 @withrevert 修饰符）。

运行 Prover 得到一个反例：

实际上，在将这些值转换为十进制后，我们得到：

X (作为 WAD) = 1766847064778384331350144565521302847.177628462396921805
Y (作为 WAD) = 0.000000000000000003
=> X/Y (作为 WAD) = 588949021592794777116714855173767615725876154132307268.333333333333333333

该结果仍然在范围内并可以通过 uint256 类型表示。因此，我们发现我们编写的 Solidity 版本的回退“过于急切”，即我们选择实现计算的方式导致回退的发生，即使在不应当发生回退的情况下。

结论：

等价检查器是一个灵活、易于使用的命令行工具，允许用户比较两段代码，或将实现与规范进行功能等价比较。它的目的是加速代码开发并提高Gas效率，而不损害安全性。目前原型版本支持 Yul、Solidity 和 CVL。预计将在 2023 年第二季度发布。

未来计划版本可能支持 Solidity/Yul 与 Vyper（甚至 Cairo）之间的比较。

我希望你喜欢本教程并探讨该工具的能力。我们非常希望从开发人员和用户那里获得反馈和改进建议 —— 如果你有任何问题或建议，请在下方评论。

最后，正如我们之前提到的，这篇博客只是一个系列的第一部分——敬请期待更多内容！

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