ビットコイン・コヴナンツの解放：高度なスマートコントラクトのための形式的モデル

1. 序論

ビットコインの未使用トランザクション出力（UTXO）モデルは、並行通貨移転においては優雅である一方、共有可能な可変状態を欠いているため、複雑で状態を持つスマートコントラクトの実装には重大な制限がある。コヴナンツは、ビットコインスクリプトを拡張するために提案された重要な言語的プリミティブとして登場し、トランザクションが将来の償還トランザクションのスクリプトに制約を課すことを可能にする。本論文は、2013年頃の登場以来、主に低水準で実装に焦点を当てた観点から記述されてきたコヴナンツに関する形式的・抽象的なモデルのギャップに取り組む。形式的基盤を提供することで、この研究は契約特性に関する推論を簡素化し、ビットコインの現在の能力を超えた高度なユースケースの仕様化を可能にし、より高水準のプログラミング抽象化の設計を促進することを目指している。

2. 純粋なビットコインモデル

本論文は、中核的なビットコイントランザクションモデルの形式化を採用する。UTXOモデルでは、ブロックチェーンの状態は未使用トランザクション出力の集合によって定義される。各出力は、価値（ビットコインの量）と、それを使用するために必要な条件を指定するscriptPubKey（ロックスクリプト）を含む。使用トランザクションはscriptSig（アンロックスクリプト）を提供し、消費したいUTXOを参照する。検証には、連結されたスクリプトの実行が含まれる。決定的に重要なのは、標準的なビットコインスクリプトは限定的であることだ：署名検証と基本的な算術・論理を超えて、使用トランザクションの構造を内省したり制約したりすることができず、多段階プロトコルを強制する契約の作成を妨げている。

3. コヴナンツの形式的モデル

中核的な貢献は、提案されているコヴナンツのオペコード（OP_CHECKTEMPLATEVERIFYなど）を抽象化した形式的モデルである。

4. 複雑なビットコイン契約の仕様化

形式的モデルを適用して、純粋なビットコインでは表現不可能または煩雑な契約を仕様化する。

5. 高水準言語プリミティブ

本論文では、コヴナンツが高水準契約言語のコンパイルターゲットとしてどのように機能し得るかについて議論する。「時間T後に引き出す」、「相手方が署名した場合のみ使用する」、「状態をAからBに遷移させる」などのプリミティブは、特定のコヴナンツ制約に直接マッピングでき、ビットコイン契約開発者のための抽象化レベルを引き上げる。

6. 核心的洞察とアナリストの視点

核心的洞察： Bartolettiらは、単なる別のコヴナンツオペコードを提案しているのではなく、巧妙なハックをビットコインの正当で分析可能なプログラミングパラダイムに変える、欠けていた形式的理論を提供している。これは、アドホックなスクリプティングを超えて、UTXOブロックチェーン上での複雑で安全な契約の体系的なエンジニアリングを可能にする鍵である。

論理的流れ： 議論は説得力を持って単純である：1) ビットコインのUTXOモデルは状態を欠き、契約を制限する。2) 修正案として提案されたコヴナンツは形式的に十分に理解されていない。3) したがって、我々は形式的モデルを構築する。4) このモデルを用いて、価値ある複雑なユースケース（ヴォールト、チャネル、DeFi）を表現できることを実証する。5) この形式化は、自然に高水準言語設計を可能にする。これは、精密に実行された典型的な「理論が実践を可能にする」パイプラインである。

強みと欠点： 主要な強みは、暗号学/プログラミング言語理論とビットコインエンジニアリングの間のギャップを埋めることである。このギャップは、イーサリアムのアカウントベースモデルで高価なバグを引き起こしてきた。形式的意味論は特性検証を可能にし、大きな利点である。暗黙的に認められている欠点は、ビットコインの政治経済学である。本論文が指摘するように、ビットコインの「極めて慎重なアプローチ」は、その形式的優雅さに関わらず、コヴナンツのような新しいオペコードの導入を非常に困難な課題にしている。ネイティブなコヴナンツなしでのライトニングのようなレイヤー2の成功も、必要性と利便性に関する疑問を提起する。さらに、このモデルの安全性は、制約されたフィールド（スクリプトハッシュなど）が十分であるという仮定に依存している。他のオペコードとの予期せぬ相互作用効果が残る可能性がある。

実践的洞察： 研究者にとって、この論文は青写真である：形式的メソッドを用いてブロックチェーンアップグレードのリスクを低減し、明確化する。開発者にとっては、コヴナンツが存在すると仮定して（LiquidやStacksで見られるように）、今すぐ契約フレームワークの設計を始める。ビットコインプロトコル開発者にとって、この論文はBIP 119（OP_CTV）や類似の提案を主張するために必要な厳密な基盤を提供する。それは機能要求をエンジニアリング仕様に変換する。最大の要点：ビットコインスマートコントラクトの未来は、イーサリアムを模倣することではなく、独自のUTXO+コヴナンツパラダイムを活用して、新しく、潜在的により安全でスケーラブルな分散型アプリケーションのクラスを作り出すことにある。

7. 技術的詳細と形式化

形式的モデルは、トランザクション、スクリプト、および検証を文脈的に定義する。重要な技術的詳細は、コヴナンツ制約の表現である。$\texttt{tx}$ をトランザクションを表すとする。コヴナンツは関数として見ることができる：

$\text{Covenant}_{\text{cond}} : \texttt{tx}_{\text{current}} \times \texttt{tx}_{\text{next}} \times \sigma \rightarrow \{\text{True}, \text{False}\}$

ここで $\sigma$ は検証コンテキスト（ブロック高など）を表す。述語 $\text{cond}$ は、$\texttt{tx}_{\text{next}}$ フィールドに対するチェックの論理積であり得る：

$\text{cond} \equiv (\texttt{hashOutputs}(\texttt{tx}_{\text{next}}) = H) \land (\texttt{nLockTime}(\texttt{tx}_{\text{next}}) > T) \land ...$

これは、使用トランザクションの指定された部分のハッシュを比較のためにスタックにプッシュするOP_CHECKTEMPLATEVERIFYのような提案と一致する。再帰的特性は、$\texttt{tx}_{\text{next}}$ の出力が、それ自体がコヴナンツ $\text{Covenant}_{\text{cond}'}$ を強制するスクリプト $S'$ を含むことを保証することで形式化される。

8. 分析フレームワークと事例ケース

事例：単純なヴォールト契約
目標： 二つの方法で使用できるUTXOを作成する：1) 即時に、ただし特定の「コールドストレージ」アドレスのみに。2) 任意のアドレスに、ただし30日の遅延の後（盗難のキャンセルを可能にする）。
形式的モデルを用いたフレームワークの適用：
1. 初期ロックスクリプト（scriptPubKey）： コヴナンツ条件 $C_1$ を含む。
2. コヴナンツ $C_1(T_{vault}, T_{spend})$： Trueと評価されなければならない。以下をチェックする：
    a) パスA（即時）： $\texttt{hashOutputs}(T_{spend}) = H_{cold}$ // 出力は事前にコミットされたコールドストレージアドレスにハッシュされなければならない。
    b) パスB（遅延）： $\texttt{nLockTime}(T_{spend}) \geq \text{currentBlock} + 4320$ (30日をブロック数で) AND $\texttt{hashOutputs}(T_{spend})$ は任意でよい。
3. 検証： ヴォールトUTXOを $T_{spend}$ で使用する際、ビットコインノードはスクリプトを実行する。ヴォールト所有者からの署名が必要であり、かつ $C_1$ がトランザクションペアに対して成立することを検証する。
この事例は、形式的モデルの述語 $C(T_x, T_{next})$ が、次のトランザクションのフィールドに対する具体的なチェックで具体化され、基本ビットコインでは不可能なセキュリティ特性（盗難回復）を可能にする方法を示している。

9. 将来の応用と方向性

この形式化は、いくつかの将来の方向性を開く：

• 検証済みコンパイラ： 高水準言語（SimplicityやMiniscript拡張など）からコヴナンツ埋め込みビットコインスクリプトへのコンパイラを構築し、正しさの形式的証明を伴う。
• クロスチェーンコヴナンツ： 他のブロックチェーンやオラクルからのイベントを条件とするコヴナンツを、SPVのような暗号学的証明を用いて探索する。「ブリッジ」に関する初期の研究やロールアップに関する最近の研究で示唆されているように。
• プライバシー保護コヴナンツ： コヴナンツチェックをゼロ知識証明（例：Taproot/Schnorr署名の使用）と統合し、契約ロジックを隠蔽しながらもそれを強制する。Arkのようなプロジェクトで探求されている方向性。
• 形式的セキュリティ分析： このモデルを用いて、提案されたコヴナンツ構築のセキュリティを、経済的・暗号学的攻撃に対して体系的に分析する。IEEE Symposium on Security and Privacy コミュニティによるイーサリアムのスマートコントラクトに関する研究と同様に。
• レイヤー2プロトコルの簡素化： ライトニングネットワークやサイドチェーン（Liquid）のようなプロトコルを、ネイティブなコヴナンツを活用してより効率的で信頼最小化されたものに再設計し、複雑な監視塔や連合の必要性を減らす。

10. 参考文献

1. M. Bartoletti, S. Lande, R. Zunino. Bitcoin covenants unchained. arXiv:2006.03918v2 [cs.PL]. 2020.
2. S. Nakamoto. Bitcoin: A Peer-to-Peer Electronic Cash System. 2008.
3. J. Poon, T. Dryja. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. 2016.
4. M. Moser, I. Eyal, E. G. Sirer. Bitcoin Covenants. Financial Cryptography 2016 Workshops.
5. Bitcoin Improvement Proposal 119 (BIP 119). OP_CHECKTEMPLATEVERIFY.
6. G. Wood. Ethereum: A Secure Decentralised Generalised Transaction Ledger. Ethereum Yellow Paper. 2014.
7. A. Miller, et al. Hashed Timelock Contracts (HTLCs). 2017.
8. R. O'Connor. Simplicity: A New Language for Blockchains. Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security.
9. Blockstream. Liquid Network. https://blockstream.com/liquid/
10. IEEE Symposium on Security and Privacy. Multiple papers on smart contract security analysis. Various years.