Cardanoでスマートコントラクトのサポートを可能にした研究の概要
Cardano研究の詳細2 -Cardanoの革新的なEUTXOについて、そしてより効率的なスマートコントラクトを提供する仕組み
2022年 6月 23日 12 分で読めます
はじめにこちらをお読みください。
前回のブログ記事では、ステーキング、委任、報酬共有など、Cardanoの中核となる要素を支える研究について紹介しました。 今回は、拡張未使用トランザクションアウトプット(EUTXO)会計モデルを活用した、分散型アプリケーション(DApp)開発用関数型スマートコントラクトプラットフォームの確立を支える論文を概観します。
UTXO対アカウントベースモデル
ビットコインとイーサリアムは、今日数あるブロックチェーンの中でも最も人気のあるブロックチェーンです。ここでは、ユーザーの資金の分布と所有を追跡するために、2つのかなり異なる台帳会計モデルが使用されています。このモデルとは、ビットコインの未使用トランザクションアウトプット(UTXO)モデルと、イーサリアムやその他のブロックチェーンで採用されているアカウントベースモデルです。
UTXOモデルは金融活動の中核におけるセキュリティを保証します。UTXOのセマンティックモデルは、複雑な並行的かつ分散された計算環境で単純性を保ちつつも、スマートコントラクトのサポートという点ではかなり限定されています。イーサリアムは、より表現の豊かなスマートコントラクトを提供するという明確な意図のもとに、アカウントベースモデルを選択しました。
UTXOモデルのセマンティックの単純性を保ちながらスマートコントラクトの表現力を持つことを可能にできるかという課題への対応として、IOGの研究者は「The Extended UTXO Model(拡張UTXOモデル)」と「Native Custom Tokens in the Extended UTXO Model(拡張UTXOモデルにおけるネイティブカスタムトークン)」という解決策に辿り着きました。2020年に公開された両論文は、Cardanoに実装されているEUTXOモデルを詳細に説明しています。
ラムダ研究者にしてInput Output Global, Inc.のPlutusアーキテクトであるManuel Chakravartyは次のように語っています。
ビットコインによって実績が試されたUTXO台帳モデルは、安全性とスケーラビリティにとってのゴールドスタンダードです。私たちは、イーサリアムが開発したスマートコントラクトの表現レベルを得ながらも、UTXOの比類なき安全性とスケーラビリティを維持するために、拡張UTXO(EUTXO)モデルを生み出しました。単純に、双方の最良の部分を取り入れたかったのです。
「拡張UTXOモデル」の研究論文では、コントラクトのステータスを継続的に維持し、トランザクションのシーケンス全体を通じて同じコントラクトコードを使用するEUTXOの能力を提示しています。EUTXOモデルが持つもう1つの強力な特徴は、有効なトランザクションに必要な手数料が、送信前に正確に予測できることです。これは、EUTXOモデルの決定的設計で実現された固有の特徴であり、アカウントベースモデルにはありません。
Plutus
スマートコントラクトは、Cardano上で契約の実行を支える推進力です。これは自己実行型であるため、第三機関に依存しません。
ACM SIGPLAN International Conference on Functional Programming(ICFP'19:関数プログラミングの国際会議) で、Manuel Chakravartyは関数型ブロックチェーンについて語り、特にスマートコントラクトへの関数型アプローチとしてPlutusを提示しました。
「性急に動いて物事を破壊する」のは、Cardanoの構築方法ではありません。壊してしまったものを簡単に直すことはできません。したがって、Plutusは関数型プログラミングの堅牢な数学的基盤の上に構築されました。これは、スマートコントラクト用のプログラミングプラットフォームであり、スマートコントラクトを作成するためのHaskellライブラリー、HaskellからPlutus Coreオンチェーンコードへのコンパイラー、そして、開発を補助するさまざまなツールといった要素を含んでいます。
ほとんどのブロックチェーンプログラミングプラットフォームはイーサリアムのSolidityのようにカスタム言語に依存しています。PlutusはHaskellをもとに構築されています。Haskellを選択することにより、IOGの研究チームとエンジニアリングチームは、高保証ソフトウェアのための実績が確立された既存のHaskellインフラ、ライブラリー、ツールを再利用することが可能となりました。Haskellは、望ましいセキュリティレベルに達するために、非形式論理、テスト、形式手法の使用を単純化しながら、簡素で再利用可能なコードを提供します。コードの正しさにおけるもっとも厳格な論理形式としての形式手法は、高価値のスマートコントラクトにとって特に重要であり、関数型プログラミングパラダイムによって十分にサポートされています。
IOGの研究チームとエンジニアリングチームは、「The Extended UTXO Model」、「Native Custom Tokens in the Extended UTXO Model」、「Unraveling recursion: compiling an IR with recursion to System F(再帰の解明:System Fへの再帰を伴うIRのコンパイル)」、「System F in Agda, for fun and profit(楽しみと利益のための、AgdaにおけるSystem F)」などの論文に基づきPlutusを提供しています。これらの論文を組み合わせることで、Cardanoのスマートコントラクト対応台帳モデルと、いわゆるラムダ用語としてのコントラクトコードのオンチェーン表現が確立されます。「System F in Agda, for fun and profit」には厳密な数学的定義が含まれますが、これは、Agda定理証明器の助けを得てコンピューターチェックされています。
Plutusは現在Cardanoにおけるスマートコントラクト用の現役の、進化するプログラミングプラットフォームです。また、IOGの教育チームはPlutusパイオニアプログラムを開始し、CardanoエコシステムのためにPlutusを使った開発者を採用、訓練しています。プログラムの詳細は、こちらをご覧ください。
Marlowe
Plutusがスマートコントラクト用の関数型プログラミング言語である一方、Marloweは、プログラミングに関する深い知識を必要とせずに、低コストのスマートコントラクトを視覚的に構築、実行できるウェブベースのプラットフォームです。これで、プログラマー以外の人々に、金融取引のための、シンプルで最適化されたコントラクトを実行するための幅広いユースケースが開かれます。
Marloweを紹介した最初の研究論文「Marlowe: financial contracts on blockchain(マーロウ:ブロックチェーンの金融コントラクト)は、2018年に発表されました。この論文は、金融契約の実行を対象としたドメイン専用言語の設計を検討しています。Marloweの実行可能なセマンティクスをHaskellで示し、実際のMarloweの事例を挙げ、ユーザーがMarloweコントラクトのシミュレーションをブラウザーで実行できるツールを説明しています。
その後、2020年に、IOGの研究チームは論文「Efficient static analysis of Marlowe contract(Marloweコントラクトの効率的な静的解析)」を発表。ここでは、Marloweコントラクトの静的解析を最適化する取り組みの概要が提示されました。続く「Marlowe: implementing and analysing financial contracts on blockchain(Marlowe:ブロックチェーンにおける金融契約の実装と分析)」では、CardanoのMarlowe実装と、ウェブベースの開発およびシミュレーション環境であるMarlowe Playgroundを説明しています。この論文ではまた、Marloweコントラクトは実行前に徹底した分析が可能であり、それゆえ契約の当事者に強力な保証を提供することができることが示されています。
Marloweはすでに、スマートコントラクトの作成プロセスを開発、シミュレーション、テストできるブラウザーベースのサンドボックス環境Marlowe Playgroundで試用できます。IOGは現在Marloweテストネットの立ち上げを準備中であり、Marloweパイオニアプログラムを活用してMarlowe製品スイート全般に関するフィードバックとユースケースを収集する予定です。先般、Marlowe CLIツールが配信され、ユーザーはコマンドラインインターフェイスを使用してトランザクションを送信したり、Marloweコントラクトを操作したりすることが可能になりました。メインネットで展開されるようになれば、MarloweコントラクトによってDeFi機能の幅が広がります。
ここでは、CardanoのEUTXOモデルと、これがいかにCardanoにおけるスマートコントラクトの開発を促進するかについて説明しました。次回は、マルチ資産サポートを可能にする研究について論じます。ご期待ください。
続きはこちらから
最新の記事
Input | Output chief scientist receives prestigious Lovelace computing award 筆者: Fergie Miller
3 December 2024
Delivering change in Ethiopia: lessons and reflections 筆者: Staff Writer
28 November 2024
Applying formal methods at Input | Output: real-world examples 筆者: James Chapman
26 November 2024