Polkadot パレット Balances を形式検証に備える

目次

• はじめに
• 方法論の定義
• 方法論の実行
• 再現手順ガイド
  • Fungible トレイト仕様のテキスト記述：トレイト実装に関与する公開関数
• balances_contract の逆アセンブリ結果の分析と検証見通し
  • 1. 構造的観察
  • 2. 本アーキテクチャ特有の検証課題
  • 3. 残高操作の検証戦略
  • 4. 注釈付きコードにおける具体的検証課題
• 段階的検証のロードマップ
  • 基盤フェーズ（インフラの公理化）
  • ビジネスロジック・フェーズ（機能的正当性）
  • 統合フェーズ
  • 期待される成果と限界
  • 契約インフラ推論の適用可能性：Polkadot ランタイム全体との比較
• 結論

はじめに

暗号金融の業界では、デプロイ前に見逃されたバグが壊滅的な金銭的損害を引き起こし得ます。特に、第三者の開発者が任意のコントラクトをチェーン上にアップロード・実行できるシステムでは、二つの異なる脅威クラスが生まれます。第一に、チューリング完全な計算のために多数のユーザーへ隔離環境を提供する必要が、共有インフラに対する広大な攻撃面を必然的に形成します。第二に、たとえコントラクト開発者に悪意がなくても、ビジネスロジックの実装におけるアルゴリズム上の誤りや、インフラプリミティブの誤用により、コントラクトに資産を預けたユーザーが第三者から金銭的な被害を受け得ます。プラットフォーム開発者がこのような状況に直接の責任を負うわけではありませんが、コントラクト作成のために提供するツールとインターフェイスが、信頼できるアルゴリズムをどれだけ容易に実装できるかに大きく影響するのは明らかです。

バグのコストが深刻な既存の工学分野――たとえば故障が致命的となる用途（医療、化学/原子力産業、航空、軍事応用など）のマイコンプログラミング――では、典型的なプログラマが親しむパラダイムでは到達できない信頼性を実現するために、形式検証が広く用いられています。残念ながら、この経験を比較的若い暗号金融の領域へ直接移植することは、いくつかの客観的事情により困難です。一見すると、中心的問題は巨大な「道具立ての隔たり」にあるように見えるかもしれません――「信頼性の高い」ソフトウェア産業は、数十年にわたって閉じたエコシステムで最適化された高度に専門化されたソリューションを普遍的に採用している一方で、暗号金融の世界は巨大なオープンソース基盤に依存しており、つい最近まで急進的な信頼性ソリューションを切実に必要としてはいませんでした。

しかし私たちは、問題はさらに根深く、道具立てよりも方法論的だと確信しています。産業実務では「信頼性の高い」ソフトウェアを作るためのワークフローがまったく異なる形で組織されており、ダイナミックな暗号金融産業の文脈では想像しにくいからです。たとえば、ブロックチェーン開発者に対して、技術フロンティアを巡る絶え間ない競争の渦中で、新しいコンセプトの迅速なプロトタイピングではなく、設計するシステムの主要コンポーネントについての詳細な数学的仕様の作成から開発を始めることを期待することはできません――スタートアップには、そのような徹底したアプローチのための時間もスキルもないのが普通です。状況はそこからさらに悪化します――自らのアイデアを実装するためのツールを選ぶ際に、論理の機械化が成熟していてプログラム振る舞いに関する形式的命題の証明が可能な言語やフレームワークに自らを制限し、強力で便利なオープン技術の大多数へのアクセスを断つことに同意するチームは稀です。

このような、もっともな産業の現状の帰結として、プログラム性質の論理的検証によって究極的な信頼性保証を得ることは、この分野の専門家の基準から見ても真に非標準的な課題になります。pallet_balances サブシステムを形式仕様に備える作業は、この問題の鮮やかな実例となりました。以下では、この作業の中で私たちが直面した具体的な事柄、この経験が今後の研究の見通し評価にどのように影響するか、そして継続する場合にどのような選択を迫られるかを説明します。

方法論の定義

Polkadot の主要な開発言語は Rust であるため、まず形式検証の方法論空間における Rust の位置づけに触れる必要があります。産業で広く使われる他の多くの高級言語と同様に、Rust にはソースコードレベルの意味論の形式記述が存在しません。そのため、アルゴリズムの性質を定式化・証明できるような高レベルの論理機械化の登場は期待し難いのが現実です。したがって、アルゴリズム仕様のためには、実装から完全に抽象化して形式化した擬似コード（例えば $TLA^+$ のようなスタイル）で振る舞いを記述するか、あるいは逆に 1 段階下ってコンパイル結果として得られるアセンブリの振る舞いを記述するかのいずれかが必要になります。

前者の道は、意味のある適用のためにはワークフローの抜本的な見直しを要します。というのも、複雑なシステムを擬似コードの記述で十分に近似できるのは、そのような記述がプロジェクト文書の中心要素であり、最初の 1 行の実コードが書かれる前に完成している場合に限られるからです。この場合、そのように形式指定され、性質が証明されたリファレンスを、対象プラットフォームで実行可能なコードへ翻訳するプログラマは、実際の命令が仕様の局所的で明確に定義されたルールに従うことだけを保証すればよく、グローバルな信頼性は証明済みの擬似コード・リファレンスによって確保されます。すでに活発に開発が進んでいるプロジェクトに対して、事後的にこのような形式記述を再構築しようとするのはほとんど意味がありません。というのも、既に実装されたアルゴリズムの擬似コード版が、重要でない実装詳細だけでなく、その中に含まれている非局所的なエラーまでも抽象化してしまっていないことを真に検証することは不可能だからです。

後者の道は、理論的には革命なしにプラスの効果をもたらし得ます。ここでの仕様化・検証の対象は、実際に実行されるアセンブリコードであり、一般的なプラットフォームに対しては意味論の厳密な形式記述が存在するからです――例えば WebAssembly と RISC-V については、それぞれ Rocq や Lean で論理機械化が活発に進んでいます。しかし実際には、この戦略は相当な労力を要する複数の問題を孕んでいます。Polkadot のオンチェーン・ランタイムの内部構造に向き合った私たちの経験が示すように、十分に複雑な Rust プロジェクトをモノリシックな塊（blob）にコンパイルすると、その個別サブシステムを形式記述のために切り出すことが事実上不可能になります。私たちは、モジュールのビジネスロジックを含むアセンブリ関数だけを取り出して精査しようと試みました。しかしこれらの試みは、FRAME のマクロや Rust コンパイラ内部が自動生成する非自明なインフラが行単位でコードと入り組んでいるために、ことごとく頓挫しました。

このような状況では、性質の形式化対象として引く境界をどう定めようとも、その内側には pallet_balances の本質である中核的ビジネスロジックとは直接関係のないコードが主要コードの 2 倍以上の分量で入り込むことになります。さらに悪いことに、モノリシックなアーキテクチャのモジュール内部に引いた境界では、仕様の定式化の段階でさえ、内部構造のいかなる詳細からも抽象化することが実質的に不可能です。逆アセンブルした Polkadot ランタイムのリスティングに含まれる命令数が文字通り数百万行規模であり、その大半があらゆるモジュール関数に浸透する単一のインフラであることを踏まえると、pallet_balances のビジネスロジックの性質を周辺文脈から切り離して形式検証するには、それ以外に道がないと考えられます。

方法論の実行

選んだ道の中心的障害がランタイムのモノリシックなアーキテクチャであると判明したため、私たちはこれを回避する目的で、pallet_balances の機能を Ink! プラットフォームへ移植することにしました。これにより、スマートコントラクトの隔離メカニズムを用いて、対象モジュールとその実行環境の間に自然な境界を引けるようになります。パレットとコントラクト環境の間の大局的には重要でない差異を考慮しつつ、十分に機械的な再実装を行った結果、balances_contract と呼ぶ新しい成果物を得ました。これは Rust で約 1000 行強の小さなモジュールで、「fungible conformance」スイートの全テストに合格し、cargo-contract ビルドシステムでコンパイルして逆アセンブル約 1.6 万行の比較的コンパクトな Wasm モジュールとなります。

この隔離手法は、モジュールが付随インフラで膨らむという問題を完全には解消しません（balances_contract の逆アセンブルリストのうち、会計特性に関係するコードは最大 20–25%にとどまります）。それでも、実行環境との明確に画定され文書化された境界が得られることは疑いようのない利点です。モノリシックなランタイム内部に引いた境界とは異なり、コントラクトのインターフェイスは、FRAME インフラや Rust コンパイラ内部の複合的要因の副産物ではなく、意味のある工学的設計の産物です――したがって、その仕様は実質的に単純であるだけでなく、後続の結果再利用の観点からも（おそらく）より有用であることが強く期待できます。モノリシック・ランタイムの内部構造のいかなる側面の形式化であれ、それが Polkadot の信頼性（検証産業における「信頼性」の意味で）に実際に資するには、ランタイム全体の大域仕様の文脈に組み込まれる必要がありますが、これは現時点では非常に遠い展望に見えます。対して、独立モジュールとして隔離されたコントラクト様のモジュールの検証は、他のパレットやコントラクト、そして機能に関わらず同じインフラ要素を含むクリティカルなアルゴリズムの検証に、リファレンスとして利用できます。いったん、たとえば SCALE コーデック、コールディスパッチャ、ベクタアロケータの性質を証明してしまえば、具体的証明をより普遍的な戦術に一般化し、自らの実装の信頼性を真に確保したい利用者に対して、この種の問題を事前に解決することが可能になります。

再現手順ガイド

.wasm へのコントラクトのコンパイルは、以下の環境で cargo contract build --verifiable ツールチェーンにより行いました。

Operating System: Kubuntu 25.04
Kernel Version: 6.14.0-33-generic (64-bit)
Processors: 16 × AMD Ryzen 7 7840HS w/ Radeon 780M Graphics
Memory: 14.8 GiB of RAM
Source record of build json:
    "hash": "0x7130f80848d2f90872da6be9fdf595c4c222b6980eabe050fae953da53f90ea0",
    "language": "ink! 5.1.1",
    "compiler": "rustc 1.84.0",
    "build_info": {
      "build_mode": "Release",
      "cargo_contract_version": "5.0.3",
      "rust_toolchain": "stable-x86_64-unknown-linux-gnu",
      "wasm_opt_settings": {
        "keep_debug_symbols": false,
        "optimization_passes": "Z"
      }
    }

バイナリは wasm2wat バージョン 1.0.36 で逆アセンブルし、手動で注釈を付しました。注釈付きモジュールがビルド成果物とビット完全一致であることは、アセンブリ出力の比較によって確認しました。

~/Git/pallet-balances-formal-verification/balances_contract$ wat2wasm balances_contract.wat 
~/Git/pallet-balances-formal-verification/balances_contract$ cmp balances_contract.wasm target/ink/polkadot_balances_contract_formal_verification.wasm 

いくつかビルド再現性の問題に遭遇しました。別のマシンでは cargo contract build --verifiable が意味的には同一だがビット完全ではない（モジュール内の関数順序の差異によりインデックスが異なる）成果物を生成することがありました。ただし、そのような小さな差異は、形式手法適用の予備的分析には有意な影響を与えません。

WASM binary compilation artifact

Fungible トレイト仕様のテキスト記述：トレイト実装に関与する公開関数

pallet_balances のトレイトメソッドを WebAssembly 実装へ写像した完全な記述は、文書「Mapping Pallet Balances Trait Methods to WebAssembly Implementation」を参照してください。

balances_contract の逆アセンブリ結果の分析と検証見通し

注釈付きの balances_contract の WebAssembly 表現は、より取り回し可能な構造を示しつつも、形式検証に向けたいくつかの課題を依然として提示します。以下に、主要な側面と、それが仕様化・検証作業に与える含意を整理します。

1. 構造的観察

逆アセンブルした Wasm モジュールは、明確な三層構造を示します。

インフラ層（コードの約 30%）

• メモリ管理プリミティブ（memcpy, memmove, memset, memcmp）
• SCALE コーデック処理（Rust 型のバイト表現へのエンコード/デコード）
• パニックハンドラやエラー報告機構
• アロケーションプリミティブ（alloc, vec_reserve など）

ホストインターフェイス層（約 40%）

• seal_get_storage, seal_set_storage, seal_clear_storage をラップするストレージ操作
• seal_deposit_event によるイベント発行
• 呼出人識別や価値移転の取り扱い
• ストレージキー用の暗号プリミティブ（BLAKE2-256）

ビジネスロジック層（約 30%）

• メッセージディスパッチャ（dispatch_call, dispatch_deploy）
• 残高操作（transfer, mint, burn_from）
• アカウント状態管理
• ロック/アンロック機構
• アカウントデータを返すクエリメソッド

2. 本アーキテクチャ特有の検証課題

課題 2.1：SCALE コーデックの正当性

SCALE コーデックは、すべてのコントラクト状態とメッセージの直列化形式であり、コード全体に遍在します。encode_u128, encode_compact_u32 といった主要関数やそのデコード版は、あらゆるストレージ操作に現れます。残高操作を検証するには、以下の保証が必要です。

• エンコードの決定性と単射性：∀x, y: encode(x) = encode(y) → x = y
• デコードがエンコードの左逆：∀x: decode(encode(x)) = Some(x)
• エンコードが値域制約を保存：∀x: 0 ≤ x < 2^128 → length(encode(x)) = 16

現実の実装では、非整列（unaligned）メモリロードからの多バイト値再構成のために、複雑なビットシフト処理（巨大なセレクタディスパッチ内に顕著）が用いられています。これを検証するには、次を扱う必要があります。

• バイトレベルのメモリレイアウト
• エンディアン性の保証（u128 はリトルエンディアン）
• ビット演算中のオーバーフローの挙動

推奨アプローチ：残高不変条件に取り組む前に、使用される SCALE コーデックのサブセット（Compact<u32>, u32, u128, AccountId, Vec<T>, Option<T>）の独立仕様を確立します。これは、Wasm メモリ領域と抽象的な Rust 値の双方向関係として形式化し、往復性を証明できます。

課題 2.2：ストレージキー生成の非単射性

AccountId → AccountData の写像は、BLAKE2-256 ハッシュによるストレージキー導出を用います。

storage_key = BLAKE2-256(mapping_prefix || account_id)

BLAKE2-256 はランダム入力に対する強い衝突耐性を持ちますが、本用途で写像が単射であることを検証するには以下が必要です。

• 暗号学的ハッシュの衝突耐性を公理として仮定する
• mapping_prefix が他のストレージ名前空間と重複しないことを示す
• 32 バイトの AccountId エンコードが正規的であることを保証する

ハッシュ関数自体はコントラクト Wasm ではなくホスト環境（seal_hash_blake2_256）で実装されます。したがって、仕様ではホスト関数の振る舞いを公理化する必要があります。

推奨アプローチ：ストレージを、Storage: (Prefix × Key) ⇀ Value の抽象的 KV ストアとしてモデル化し、異なる (prefix, AccountId) ペアに対するキーの衝突なしを仮定します。BLAKE2-256 の実際の耐性は証明不要で、前提条件として与えます。

課題 2.3：メッセージディスパッチの複雑さ

dispatch_call 関数は 1000 行超で、深い入れ子のブロックによるセレクタマッチを実装しています。このロジックは多段のカスケードです。

1. セレクタ 0 バイト目での第 1 段ディスパッチ（9 ケースの br_table）
2. 特定のバイト範囲の第 2 段サブテーブル（例：0xC8–0xD0, 0xF3–0xFA）
3. 残りのセレクタに対する 4 バイト完全一致

これは意味論的必然ではなくコンパイラ最適化に起因します。検証上は以下が必要です。

• ディスパッチの完全性：有効な 4 バイトセレクタはちょうど 1 つのハンドラに対応
• 無効セレクタは拒否される（パニックではなくエラーを返す）
• 各メッセージ型のパラメータデコードの正しさ

推奨アプローチ：ディスパッチ機構を、dispatch: (u32, &[u8]) → Result<MessageHandler> という部分関数に抽象化します。サポートする 35 のセレクタすべてについて、当該関数が正しいハンドラを返し、正しくデコードすることを証明します。入れ子ブロックの構造自体は、仕様では抽象化します。

3. 残高操作の検証戦略

中核となる残高操作には、形式仕様に適したパターンが見られます。

パターン 3.1：オーバーフロー処理を伴う検査付き算術

すべての残高更新は明示的なオーバーフローチェックを用います（例：deposit_into_account）。

local.get 0          ;; account.free (low 64)
local.get 2          ;; amount (low 64)
i64.add
local.tee 11         ;; new_free (low 64)
local.get 7
i64.lt_u             ;; Check for carry

このパターンは次のように仕様化できます。

checked_add(a: u128, b: u128) → Result<u128> where
  a + b < 2^128 → Ok(a + b)
  a + b ≥ 2^128 → Err(Overflow)

パターン 3.2：保全モード（Preservation）の遵守

transfer_with_checks は保全モードの複雑なロジックを実装します：

if preservation = Preserve then
  new_balance ≥ existential_deposit ∨ new_balance = 0

検証では次を確認します。

• Expendable：最終残高は任意（0 を含む）で可
• Preserve：最終残高は ED 以上または0
• Protect：最終残高は厳密に ED 以上（ダスト不可）

パターン 3.3：出金時のロック尊重

transfer_with_checks は凍結残高を尊重します：

usable_balance = account.free - account.frozen
withdraw_amount ≤ usable_balance

これは、すべての出金パス（転送・バーン等）で満たされる必要があります。

4. 注釈付きコードにおける具体的検証課題

課題 4.1：ディスパッチにおける複雑な制御フロー

ディスパッチ関数は68 の入れ子ブロックと35 以上のケースを持つ br_table を含みます。意味論的には単純な switch 文に等価ですが、正しさを示すには以下が必要です。

• 到達可能なすべての分岐でパラメータが正しくデコードされること
• バイトシフト再構成（例：非整列 i64 ロードからの u128 再構成）が値を保つこと
• アラインメント違反による未定義挙動がないこと（Wasm は非整列ロードを許容するが、正しさは再構成ロジックに依存）

例（セレクタマッチ・ハンドラ 4：mint）：

local.get 1
i64.load offset=27 align=1     ;; Load 8 bytes at offset 27 (unaligned)
local.tee 11
i64.const 56
i64.shl                         ;; Shift left 56 bits
local.get 1
i64.load offset=19 align=1     ;; Load 8 bytes at offset 19
local.tee 10
i64.const 8
i64.shr_u                       ;; Shift right 8 bits
i64.or                          ;; Combine to reconstruct u128 low 64 bits
local.set 12                    ;; Store as amount_low

これは、2 つの重なり合う非整列 i64 ロードからリトルエンディアンの u128 を再構成します。エンコードされた値が保たれることを検証するには、次を示す必要があります。

∀ bytes[0..16]: u128::from_le_bytes(bytes) = 
  (bytes[11..19] as u64) << 56 | (bytes[19..27] as u64) >> 8

課題 4.2：ロック集約の正確性

set_lock は既存のロック ID をベクタから探索し、更新または追加します。最大ロック量は次で再計算されます。

;; 疑似仕様:
∀ account: account.frozen = max { lock.amount | lock ∈ locks(account) }

これを検証するには：

1. ベクタ探索が一致する lock.id を正しく特定すること
2. max 計算がすべてのロックを走査すること
3. ベクタ操作中にロックが失われないこと

ベクタ拡張ロジック（vec_reserve）は既存要素を完全に保持する必要があります。

課題 4.3：ダスト処理の健全性（check_deposit_feasibility 関数）

ダスト回収（ED 未満の残高を dust_trap へ移す）では、総発行量を維持しなければなりません。

Pre:  total_issuance = Σ(account.free) + Σ(account.reserved)
Post: total_issuance' = Σ(account'.free) + Σ(account'.reserved)
      ∨ (dust_trap.is_none() ∧ total_issuance' = total_issuance - dust_removed)

現行実装（複数関数に散在）は複数の経路でダストを扱います。検証では次が必要です。

• すべての経路で総発行量が正しく更新されること
• 二重計上や取りこぼしがないこと
• DustLost イベントが、ダストがバーンされた場合にのみ発行されること

段階的検証のロードマップ

この複雑性を踏まえ、コントラクト全体の一括検証ではなく、段階的形式化を提案します。現実的には、以下の 3 フェーズで取り組みます。

基盤フェーズ（インフラの公理化）

Step 1: コーデック検証

• SCALE エンコード/デコードの往復性を以下の型で証明：

  • u32, u64, u128
  • Compact<u32>
  • AccountId（32 バイト配列）
  • Option<T>, Result<T, E>

• 目標：各型に対して ∀x: T. decode(encode(x)) = Some(x) を証明

Step 2: ストレージ抽象化

• ストレージを部分写像 Storage: (Prefix × Key) ⇀ Value としてモデル化
• ストレージ操作が次を満たすことを証明：
  • Set-Get 往復：storage_set(k, v); storage_get(k) = Some(v)
  • キーの独立性：k₁ ≠ k₂ → storage_set(k₁, v₁) は storage_get(k₂) に影響しない
• BLAKE2 のハッシュは抽象化（衝突なしを仮定）

ビジネスロジック・フェーズ（機能的正当性）

Step 3: コアの残高不変条件

• mint, burn_from, transfer について次を証明：

  • 総量保存（ダスト会計を含む）
  • 非負性
  • オーバーフローフリー（前提条件の下で検査付き算術が成功）

• 不変述語 I(state) を定義：

  I(state) ≜ 
    total_issuance = Σ(account.free) + Σ(account.reserved) - dust_lost ∧
    ∀ account: account.free ≥ 0 ∧
    ∀ account: account.free > 0 → account.free ≥ ED ∨ in_dust_handling(account)
  

• ∀ msg: {I(state)} handle(msg) {I(state')} を証明

Step 4: ロック機構の検証

• ロック不変条件：∀ account: frozen = max(locks.map(_.amount))
• set_lock と remove_lock がこの不変条件を維持することを証明
• usable_balance = free - frozen が引出し時に常に尊重されることを検証

統合フェーズ

Step 5: エンドツーエンドのメッセージ安全性

• ディスパッチ関数の正しさを証明：
  • 35 のセレクタすべてでパラメータを正しくデコード
  • 無効セレクタは Err を返す（パニックしない）
• すべての有効入力でパニックが起きないこと
• Wasm 実行と高レベル仕様の間の精緻化関係を確立

期待される成果と限界

想定期間：各フェーズ 2 か月、合計 6 か月

達成可能なこと：

• 高い確度での総量保存、非負性、前提条件下のオーバーフローフリー
• ディスパッチ正当性の証明：すべての有効入力が正しいハンドラへ到達
• 形式検証済み SCALE サブセット：他の Ink! コントラクトで再利用可能
• ロック機構の健全性：凍結残高がロックベクタから正しく計算される

スコープ外（公理化のため）：

• ホスト関数のバグ：seal_get_storage などが仕様通りに振る舞うことを仮定。Substrate 実装側のバグは捕捉しない
• 暗号学的仮定：BLAKE2 の衝突耐性は仮定であり、証明は行わない

契約インフラ推論の適用可能性：Polkadot ランタイム全体との比較

balances_contract とモノリシックなランタイムの pallet_balances の検証比較：

結論

balances_contract は、モノリシックなランタイムの pallet_balances に比べ、形式検証の対象として格段に扱いやすいことが分かりました。主な理由は次の通りです。

1. 明確なインターフェイス境界（メッセージセレクタ、ホスト関数 ABI）
2. 管理可能なコード規模（約 1.6 万行、そのうち約 4 千行がビジネスロジック）
3. ランタイム複雑性からの隔離（ホスト関数で Substrate 内部を抽象化）

とはいえ、いくつかの課題は残ります。

• SCALE コーデックの検証には、バイトレベルのメモリレイアウトの推論が必要
• ロック機構の正確性は、ベクタ操作の正当性の証明に依存
• 保全モードのロジックは、複数の条件が相互作用するために複雑

まずインフラの公理化から始め、コアの残高不変条件へ進み、最後にエンドツーエンドのメッセージ安全性を証明するという段階的アプローチが、志と実現可能性の最良のバランスを提供します。

このブログ記事の議論に参加してください: