Certora 正式验证 Solana 的 P-Token 升级版等同于 SPL 代币

即使 P-Token 多释放了 98% 的计算单元，Certora 仍能证明它与 SPL Token 实现字节对字节的兼容性，没有发现任何漏洞。

已发布:
已编辑:

Solana最近部署的 P-Token 升级是该网络历史上最重大的基础设施变革之一。此次升级大大减少了令牌操作所需的计算资源，同时保持了与现有 SPL 令牌计划的兼容性。

为了验证这一说法，Solana 基金会聘请Certora进行正式验证，以证明传统 SPL 令牌实施与基于 Pinocchio 的新 P-Token 程序之间的行为等效性。研发公司Anza曾将形式验证描述为 P-Token 等价性的"最有力保证"，而 Certora 的结果则进一步验证了 P-Token 作为 Solana 最广泛使用的程序之一的 "直接 "替代品的作用。

令牌计划为何重要

SPL 代币计划是 Solana 代币经济的核心。它处理网络上绝大多数资产的造币厂创建、代币账户管理、转让、烧毁和委托。由于 Solana 上几乎所有无投票权的交易都以某种形式与代币进行交互，因此代币项目的任何改变都会对生态系统产生广泛影响。

P-Token 引入了基于 Pinocchio Rust 库的新实现。升级后，性能大幅提升，许多常见操作的计算消耗降低了约 95-98%。例如，标准令牌传输从 4,645 个计算单元降至 76 个计算单元，而transfer_checked指令则从 6,200 个计算单元降至 105 个计算单元。

这些效率的提高估计可以释放整个网络 12-13% 的区块空间，在不增加区块限制的情况下创造额外的容量。

证明 "即插即用 "替代方案的挑战

虽然性能的提升吸引了人们的目光，但兼容性仍然是如此大规模的基础设施升级的最重要要求。现有的钱包、dApp、协议和智能合约都依赖于 SPL 令牌程序的行为。任何意想不到的偏差都可能导致集成问题，或给开发者和用户带来风险。

P Token

P-Token 并非简单复制原始代码库。新的实现采用了不同的架构，包括零拷贝账户访问、优化的执行路径和附加功能。因此，开发人员不能仅仅依靠传统测试来建立兼容性。

相反，Certora 使用形式验证技术，从数学角度分析这两个程序在定义的验证范围内所有可能的输入中是否表现相同。

等效性对 P-Token 意味着什么？

Certora 的验证框架针对分析的每条指令评估了三个结果类别。

首先，两个程序都不得在执行过程中发生慌乱；也就是说，程序不得因错误、边缘情况等而崩溃或中止。
其次，如果 SPL Token 程序成功处理了一条指令并返回Ok(())，P-Token 也必须返回Ok(( ))。在这种情况下，两个程序在执行后都必须以字节对字节的相同状态留下账户数据。
第三，如果 P-Token 返回错误，SPL Token 程序必须在相同条件下返回相同错误。

Certora 的框架确保，对于每一种可能的输入账户状态和指令，程序要么成功（Ok(())），要么优雅地失败（Err(e)），但绝不会内部崩溃。P-Token 的实现被设计为 SPL 令牌功能的超集，这意味着 SPL 令牌接受的任何操作也必须被 P-Token 接受。

验证工作发现了这两个程序之间的几处刻意差异。P-Token 允许委托人自我撤销，使委托人能够撤销自己的授权，而无需令牌账户所有者签署交易。SPL 令牌要求所有者签名才能进行同样的操作。

P-Token 还扩大了对 Token-2022 多重签名授权的支持。SPL 令牌拒绝这些账户，而 P-Token 则接受它们。

第三个区别是，当畸形账户数据包含非规范COption标记时，P-Token 会进行错误处理。SPL 令牌会立即以InvalidAccountData错误拒绝此类账户。P-Token 的优化账户加载过程在产生错误之前会深入到指令逻辑中，这可能会根据执行的指令产生不同的结果。

由于这些差异是有意造成的，并已记录在案，因此 Certora 在部分验证过程中加入了一些假设，以便将分析重点放在商定的兼容性边界上。

验证如何进行

Certora 的 Prover 将源代码编译成低级中间表示后进行分析。然后，工程师使用 Certora 的 Rust 验证语言（称为 CVLR）编写正式规范。

验证线束创建了账户信息和指令数据的相同副本，使验证器能在相同条件下对两个程序进行比较。利用满意度模态理论技术，该系统同时评估了所有可能的输入，而不是依赖于有限的测试用例集。

范围包括 SPL 令牌和 P-Token 之间共享的每一条指令，不包括AmountToUiAmount和UiAmountToAmount。审查还排除了三个新的 P-Token 特定指令：批处理、unwrap_lamports 和withdraw_excess_lamports。

在整个过程中，证明者要么生成了正确性证明，要么生成了具体的反例，突出了需要审查的行为差异。

发现和结果

Certora 报告称，在验证过程中没有出现可利用的漏洞。分析证实，"无恐慌 "和"错误等价"特性在范围内的所有指令中都成立，无需额外假设。在考虑到之前发现的三个故意行为差异的情况下，错误等价特性在共享指令集中也同样成立。

最重要的是，验证表明，只要两个程序成功处理相同的输入，它们就会产生字节对字节的相同操作后账户状态。这一过程还凸显了形式验证如何能够发现传统测试可能忽略的边缘情况。

索拉纳基础设施的重要里程碑

P-Token 部署到主网后不久，验证结果就出来了，为 Solana 最重要的基础设施升级之一提供了更多信心。

通过将大量计算节省与正式验证的行为等价性相结合，该升级旨在提高网络效率，而不会干扰每天依赖代币计划的应用程序和资产。