Solanaが最近導入したP-Tokenのアップグレードは、ネットワークの歴史上最も重要なインフラ変更の1つです。このアップグレードは、既存のSPLトークンプログラムとの互換性を維持しながら、トークン操作に必要な計算リソースを劇的に削減します。
この主張を検証するため、Solana Foundationは Certoraと契約し、従来のSPL Token実装と新しいPinocchioベースのP-Tokenプログラムとの動作の等価性を証明する正式な検証を実施しました。研究開発会社のAnzaは以前、形式的検証をP-Tokenの同等性を「最強に保証するもの」と説明しており、Certoraの結果は、P-TokenがSolanaの最も広く使用されているプログラムの1つに「ドロップイン」して置き換える役割を果たすことをさらに証明するものです。
トークン・プログラムが重要な理由
SPLトークン・プログラムは、Solanaのトークンエコノミーの中心に位置しています。このプログラムは、ネットワーク上の資産の大部分について、ミントの作成、トークンのアカウント管理、転送、バーン、委任を処理します。Solana上のほぼすべての非投票トランザクションが何らかの形でトークンと相互作用するため、トークンプログラムに変更があれば、エコシステムに広範な影響を及ぼします。
P-Tokenは、Pinocchio Rustライブラリをベースに構築された新しい実装を導入しています。このアップグレードによりパフォーマンスが大幅に改善され、多くの一般的な操作で計算量が約95～98%削減されます。例えば、標準的なトークン転送は4,645コンピュート・ユニットからわずか76コンピュート・ユニットに減少し、transfer_checked命令は6,200コンピュート・ユニットから105コンピュート・ユニットに減少します。
このような効率化により、ネットワーク全体で推定12～13％のブロックスペースが解放され、ブロック制限を増やすことなく容量を増やすことができます。
ドロップイン」代替の証明という課題
性能の向上が注目される一方で、この規模のインフラのアップグレードには互換性が最も重要な要件であることに変わりはない。既存のウォレット、dApps、プロトコル、スマートコントラクトは、SPLトークン・プログラムの動作に依存しています。予期せぬ逸脱は、統合の問題を引き起こしたり、開発者やユーザーにリスクをもたらす可能性があります。
P-Tokenは単にオリジナルのコードベースをコピーしているわけではありません。新しい実装では、ゼロコピー・アカウント・アクセス、最適化された実行パス、追加機能など、異なるアーキテクチャを採用しています。その結果、開発者は互換性を確立するために従来のテストだけに頼ることはできませんでした。
その代わりに、Certora は形式的な検証技法を使用して、定義された検証範囲内で可能なすべての入力に対して、2 つのプログラムが同じ動作をするかどうかを数学的に分析しました。
P-Token にとっての同等性とは?
Certora の検証フレームワークは、解析された各命令について 3 つの結果カテゴリを評価しました。
-
第一に、どちらのプログラムも実行中にパニックを起こしてはなりません。つまり、バグやエッジケースなどによってプログラムがクラッシュしたりアボートしたりしてはなりません。
-
第二に、SPL Token プログラムが命令の処理に成功しOk(())を返した場合、P-Token もOk(())を返さなければなりません。このような場合、両プログラムは実行後、アカウントデータをバイト単位で同じ状態にしなければならない。
-
第三に、P-Token がエラーを返した場合、SPL Token プログラムも同じ条件で同じエラーを返さなければなりません。
Certora のフレームワークは、可能性のあるすべての入力アカウント状態と命令に対して、プログラムが成功（Ok() ）するか、優雅に失敗（Err(e)）するかのいずれかを保証しますが、内部的にクラッシュすることはありません。P-Token の実装は、SPL Token 機能のスーパーセットとして設計されています。つまり、SPL Token で受け入れられる操作はすべて、P-Token でも受け入れられなければなりません。
検証作業により、2つのプログラム間の意図的な違いがいくつか確認された。P-Token は、委任者の自己撤回を可能にし、トークンのアカウント所有者がトランザクションに署名する必要なく、委任者が自身の権限を撤回することを可能にします。SPL トークンでは、同じ操作に所有者の署名が必要です。
P-Token はまた、Token-2022 マルチシグ権限のサポートを拡張します。SPL Token がこれらのアカウントを拒否するのに対し、P-Token はこれを受け入れる。
3つ目の違いは、不正なアカウント・データに非正規のCOptionタグが含まれる場合のエラー処理である。SPL Tokenは、InvalidAccountDataエラーでこのようなアカウントを即座に拒否します。P-Token の最適化されたアカウント・ロード・プロセスは、エラーを生成する前に命令ロジックのより深い部分まで到達します。
これらの違いは意図的に文書化されたものであるため、Certora は検証プロセスの一部に仮定を組み込み、合意された互換性の境界に焦点を当てた分析を行いました。
検証の仕組み
Certora のプローバは、コンパイル後のソースコードを低レベルの中間表現に解析します。その後、エンジニアはCVLRとして知られるCertora Verification Language for Rustを使って正式な仕様を記述します。
検証ハーネスは、アカウント情報と命令データの同一のコピーを作成し、プローバーが両方のプログラムを同じ条件で比較できるようにした。充足可能性モジュロ理論（Satisfiability Modulo Theories）のテクニックを使用し、システムは限られたテストケースのコレクションに依存するのではなく、すべての可能な入力を同時に評価しました。
対象範囲には、AmountToUiAmountとUiAmountToAmount を除く、SPL Token と P-Token 間で共有されるすべての命令が含まれた。また、バッチ、unwrap_lamports、withdraw_excess_lamports の 3 つの新しい P-Token 固有の命令もレビューから除外された。
このプロセスを通じて、証明者は正しさの証明を生成するか、レビューが必要な動作の違いを強調する具体的な反例を生成した。
発見と結果
Certoraは、検証作業中に悪用可能な脆弱性は現れなかったと報告した。解析の結果、No PanicsおよびEquivalence on Okプロパティが、追加の仮定を必要とすることなく、スコープ内のすべての命令で成立することが確認されました。また、Equivalence on Error プロパティは、以前に特定された3つの意図的な動作の違いを考慮した場合、共有命令セット全体にわたって保持されます。
最も重要な点は、検証の結果、両プログラムが同じ入力の処理に成功した場合は常に、動作後のアカウント状態がバイト単位で同一であることが実証されたことである。また、このプロセスでは、従来のテストでは見逃されがちなエッジケースを、フォーマルな検証によっていかに発見できるかが浮き彫りになった。
ソラナ・インフラの重要なマイルストーン
検証結果は、P-Tokenのメインネットへのデプロイ直後に到着し、Solanaの最も重要なインフラ・アップグレードの1つにさらなる信頼性をもたらしました。
このアップグレードは、大幅な計算量の削減と正式に検証された動作の等価性を組み合わせることで、トークン・プログラムに日々依存しているアプリケーションや資産を中断させることなく、ネットワーク効率の向上を目指しています。
SolanaFloorの続きを読む
SolanaがついにネイティブOnchainサブスクリプションを取得、給与計算、AIエージェント予算、定期課金をアンロック
元米大統領候補アンドリュー・ヤンのNoble MobileがHelium Mobileを買収 - $HNTはどうなる？
SpaceXの$2T IPOはCryptoにどう影響するか？
