Concordance：利用 LLM 安全地简化复杂智能合约

随着 Web3 领域日趋成熟，智能合约开发者也变得越来越老练，编写经过高度优化的代码，通常使用 Solidity 中提供的底层汇编语言。虽然这种方法意味着更快（且更便宜）的智能合约执行，但这些精妙的编码技术使得 审计和代码审查更加困难。

这就是为什么我们很高兴地宣布发布一款名为 Concordance 的全新开源工具，它可以帮助人们更好地理解极其复杂的代码。Concordance 使用 LLM 自动简化复杂的智能合约实现，而不 改变代码在链上的可观察行为。由于 我们的等价性检查器 Concord，我们能够保证行为不会改变。

Concordance 概述

为了解释我们编写 Concordance 的原因以及它如何发挥作用，让我们首先看一个来自 Solady 库的示例函数：

function safeTransferFrom(
   address token,
   address from,
   address to,
   uint256 amount
) internal {
   assembly {
       let m := mload(0x40)
       mstore(0x60, amount)
       mstore(0x40, to)
       mstore(0x2c, shl(96, from))
       mstore(0x0c, 0x23b872dd000000000000000000000000)
       let success := call(gas(), token, 0, 0x1c, 0x64, 0x00, 0x20)
       if iszero(and(eq(mload(0x00), 1), success)) {
           if iszero(
               lt(
                   or(iszero(extcodesize(token)), returndatasize()),
                   success
               )
           ) {
               mstore(0x00, 0x7939f424)
               revert(0x1c, 0x04)
           }
       }
       mstore(0x60, 0)
       mstore(0x40, m)
   }
}

名称表明这正在执行“安全”的 `transferFrom` 操作，但其执行方式并不立即清楚，并且 revert 条件几乎难以理解。在 Web3 应用程序中，除了 Solady 库之外，找到像这样的手动优化代码非常常见。审计或简单地审查像此示例这样经过高度优化的代码极其困难且容易出错。

如果我们能够审查一个 等效 但 更简单 的版本 呢？

Concordance 将迭代地简化我们的 Solady 示例为：

function safeTransferFrom(
   address token,
   address from,
   address to,
   uint256 amount
) internal {
   (bool success, bytes memory returndata) = token.call(
       abi.encodeWithSelector(0x23b872dd, from, to, amount)
   );

   // Check if the call succeeded AND returned exactly 1 (true)
   // 检查调用是否成功并且返回了 1 (true)
   bool returnsOne = success && returndata.length >= 32 &&
                       uint256(bytes32(returndata)) == 1;

   if (!returnsOne) {
       // When success = 0: always revert
       // 当 success = 0 时：总是 revert
       // When success = 1: revert if (token.code.length == 0 OR returndata.length > 0)
       // 当 success = 1 时：如果 (token.code.length == 0 OR returndata.length > 0) 则 revert
       if (!success) {
           revert TransferFromFailed();
       } else {
           // success = 1 case
           // success = 1 的情况
           if (token.code.length == 0 || returndata.length > 0) {
               revert TransferFromFailed();
           }
       }
   }
}

在此，构建对 `token` 调用的汇编代码已替换为使用 Solidity 的内置 ABI 编码 API。revert 逻辑也得到了显著澄清。我们现在可以看到，在以下情况下，该函数会 revert：

1. transferFrom 函数调用 revert，或
2. 该函数返回一个非空缓冲区，该缓冲区未正确编码布尔值“true”，或
3. 该函数返回一个空缓冲区，并且该 token 没有代码

该实现在 safeTransferFrom 的所有可能参数以及被调用 token 的所有可能行为（例如，token revert、返回格式错误的缓冲区或是一个 EOA 等）上都表现相同。

工作原理

请注意，Concordance“迭代地”得出此结果。 Concordance 首先使用 LLM 来为提供的代码 提出 等效的重写。在我们的示例中，这是 Solady safeTransferFrom。但是，正如我们刚刚讨论的那样，原始函数非常复杂，因此 LLM 的此初始提议可能在行为上存在一些细微的差异。为了确保重写是等效的，Concordance 始终使用一个名为 Concord 的“等价性检查器”将 LLM 的提议与原始代码进行比较。

此等价性检查器将产生一个数学证明，证明这两段代码在所有可能的输入上都表现相同，或者产生一个行为发散的示例输入。在后一种情况下，由 Concord 发现的此示例会反馈到 LLM 中，并带有纠正建议重写的说明。此循环会迭代进行，直到等价性检查器 Concord 判断建议的重写与原始代码等效。

通过使用 Concord 来检查 LLM 的提议，返回给用户的重写必然在每种 可观察 的方式上都与原始代码等效。因此，Concord 是 Concordance 赖以生存的基础。

等价性检查

Concord 是我们的通用等价性检查器的名称，该工具可以自动（且详尽地）检查两个智能合约是否等效。在讨论我们使用 Concord 原型发现的 Vyper 编译器错误 时，我们之前曾提到过此工具。在那篇博文中，我们没有深入探讨两个程序等效意味着什么，但我们将在本文中对此进行说明。

我们说过，生成的代码在每个 可观察 的方面都是等效的。这种区别很重要：如果我们坚持认为以太坊虚拟机 (EVM) 的内存和堆栈在运行两个不同的程序时始终看起来完全相同，那么这将为进行上述重写所需的任何更改留出很小的空间。相反，我们坚持认为代码的可观察副作用必须相同。这些副作用是：

1. 存储更改
2. 生成日志事件
3. Revert/返回当前 EVM 帧
4. 外部调用（包括价值转移）

与这些副作用相关联的数据（revert 的原因、发出的日志的主题）在两个程序之间也必须相同。更技术地说，两个等效的实现 A 和 B 将满足以下属性：

• 对于任何输入，如果 A 以原因 R revert，则 B 也必须在同一输入上以原因 R revert
• 对于任何输入，如果 A 返回缓冲区 R，则 B 也必须返回缓冲区 R

如果两个实现都 revert，则它们执行的任何副作用都将被回滚。但是，当实现返回时，我们坚持认为它们对状态的影响是相同的。特别是，如果 A 和 B 返回时没有异常，那么它们必须对相同的地址进行相同的外部调用序列，具有相同的以太币价值和 calldata。 它们还必须发出相同的日志，具有相同的主题和数据，并且每个存储槽中的值必须相等。

Gas 消耗 不是 我们对等价性的定义的一部分。 事实上，除非两个 EVM 执行以完全相同的数据执行完全相同的操作码，否则 Gas 消耗等效的可能性极小。 此外，在简化代码时，简化的版本很可能会使用更多的 Gas - 这是为撤消优化所做的必要权衡。

有了这个粗略的等价性定义，一个自然的问题出现了：我们如何才能确保以上内容适用于所有可能输入的两个实现 A 和 B？ 正如我们在 Vyper 博客文章中提到的，Concord 构建在 Certora Prover 使用的符号推理之上，这使其能够有效地推理无限状态空间，覆盖所有可能的输入。

Concord 如何在 Certora Prover 的框架内实现这一点本身就是几篇博文的主题。 然而，为了给出一个快速概述：Concord 检测 它正在比较的两个实现，以将执行的任何路径上遇到的所有副作用记录到两个不同的向量中。 在象征性地执行两个实现之后，我们断言这两个向量是等效的； 如果它们不等效，则两个实现之间存在一些行为差异。Concord 分析向量以提供对不同行为的人类可读的解释：正是这个解释 Concordance 返回给 LLM。 可以在我们关于 Concord 的技术报告 此处 中找到对该技术的更详细的解释，以及围绕定义等价性的更长的讨论。

Concordance 重新审视

重申一下，Concord 是一种独立的工具，可用于检查两个智能合约实现之间的差异。 为了更好地了解 Concordance 如何在其基础上构建，让我们检查 LLM 和 Concord 之间的一个交互轮，该交互由 Concordance 调解。

LLM 首先为 Solady safeTransferFrom 提出以下重写：

function safeTransferFrom(
   address token,
   address from,
   address to,
   uint256 amount
) internal {
   (bool success, bytes memory returndata) = token.call(
       abi.encodeWithSelector(0x23b872dd, from, to, amount)
   );

   // Check if the call succeeded and returned true (1)
   // 检查调用是否成功并返回 true (1)
   if (success && returndata.length >= 32 && abi.decode(returndata, (bool))) {
       return;
   }

   // Allow calls to contracts that don't return values (non-standard tokens)
   // 允许调用不返回值 (非标准 token) 的合约
   if (success && token.code.length > 0 && returndata.length == 0) {
       return;
   }

   // All other cases should revert with TransferFromFailed error using same pattern as original
   // 所有其他情况都应使用与原始模式相同的 TransferFromFailed 错误进行 revert
   assembly {
       mstore(0x00, 0x7939f424) // TransferFromFailed()
       revert(0x1c, 0x04)
   }
}

这非常接近了，但 Concord 发现了一个反例：

There were 1 call(s) prior to this event:
在此事件之前有 1 个调用：
   External call to 0xffffffffffffffffffffffffffffffffffffffff with eth: 0
   对 0xffffffffffffffffffffffffffffffffffffffff 的外部调用，eth: 0
    The calldata buffer was:
    Calldata 缓冲区为：
23b872dd00000000000000000000000000000000000000000000ffffffffffffffffffffffffffffffffffffffff00000000000000000000000000000000
     The callee codesize was chosen as: 1
     被调用者的代码大小选择为：1
     The call result was:
     调用结果为：
         A successful return
         成功返回
         With a buffer of length: 4294967295
         缓冲区长度：4294967295
         The returned buffer model is:
         返回的缓冲区模型为：
             0000000000000000000000000000000000000000000000000000000000000002... missing 4294967263 more bytes
             0000000000000000000000000000000000000000000000000000000000000002... 缺少 4294967263 个字节
The methods performed different actions.
这些方法执行了不同的操作。
In SafeTransferFromHarness.safeTransferFromExternal(address,address,address,uint256):
在 SafeTransferFromHarness.safeTransferFromExternal(address,address,address,uint256) 中：
    ! The call reverted
    ! 调用 revert
    Event Context:
    事件上下文：
        No additional context information
        没有其他上下文信息
    The raw buffer used in the event was:
    事件中使用的原始缓冲区为：
        7939f424
In SafeTransferFromRewriteHarness.safeTransferFromExternal(address,address,address,uint256):
在 SafeTransferFromRewriteHarness.safeTransferFromExternal(address,address,address,uint256) 中：
    ! The call reverted
    ! 调用 revert
    Event Context:
    事件上下文：
        No additional context information
        没有其他上下文信息
    The raw buffer used in the event was:
    事件中使用的原始缓冲区为：
        ! Empty
        ! 空

在此处解释底层结果，我们可以看到 Concord 正在考虑一种情况，即被调用的 `safeTransferFrom` 函数返回一个巨大的 4294967295 字节缓冲区。原始代码使用 7939f424 (AKA TransferFromFailed()) revert，而建议的重写使用一个空缓冲区 revert。巨大的缓冲区大小并不是导致行为分歧的原因。相反，请注意此缓冲区中的第一个字是 0x0…02。这不是布尔值的有效编码，因此在建议的重写中对 `abi.decode` 的调用将使用一个空缓冲区 revert。上述反例将发回给 Claude 以进行完善，并且最终会收敛到正确的重写。

安装 Concordance

Concordance 是一个 Python 脚本，包含在开源 Certora 存储库中。你可以在 此处 找到描述如何安装依赖项并运行该工具的 README。 如前所述，Concordance 是一个你可以立即尝试的开源工具，尽管我们强调它仍处于 pre-alpha 开发阶段。 当然，如果你自己尝试使用，我们欢迎你提供任何反馈。

总结

随着 LLM 变得越来越强大，我们可以将它们应用于越来越复杂的软件工程任务。但是，正如被广泛记录的那样，LLM 并非完美，并且可能会犯一些细微（有时并非那么细微）的错误。通过使用形式验证工具作为 LLM 的防护栏，我们可以从 AI 的自动化和易用性中受益，同时仍然获得形式验证的万无一失的保证。我们还在探索同一种思路中的其他可能性，希望很快能够分享。敬请关注！

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