私たちは今月頭にブロックチェーン言語であるSimplicityのソースコードをリリースしました。
Simplicityはブロックチェーンで高度なスマートコントラクトを書くときに直面する問題に対して私たちが出した答えです。Simplicity以前のブロックチェーン・プログラミング言語は表現力と信頼性とのトレードオフを余儀無くされました。エンジニアは複雑で信頼性の低いものを作るか、簡単で信頼性の高いものを作るかの選択肢しかありませんでした。今回、Simplicityの登場によって高度なスマートコントラクトをデザインし、またその結果も確信できるようになりました。
SimplicityはBlockstreamのElementプラットフォームと互換性を持つように作られました。Elements
上で独立的なブロックチェーンやサイドチェーンを開発中のエンジニアがSimplicityの機能を自由に利用できるようになります。Elementsの実装例としてのLiquidネットワークもSimplicityをサポートすることによって、低信頼エスクローサービスや金庫アプリケーション、また、多様な複雑なスマートコントラクトをデザインすることができるようになります。
今回のリリースに含まれる機能は以下で確認できます。
- Coqに正式に明記されたSimplicity言語の表示的意味論と拡張機能
- Coqに正式に明記されたるSimplicity言語の操作的意味論
- Haskellで書かれたSimplicity言語のインタプリタ、型チェッカーとシリアライズ
- Simplicity言語の式の例、SHA256やEC-Schnorr署名検証などの暗号処理も含む
- Simplicity言語のテクニカルレポート
Simplicityを使う理由
ブロックチェーンには従来のプログラミング言語では適切に対処できない独特な問題があります。
- 全ての環境で利用者全員が計算の結果に同意しなければならない。
- スマートコントラクトの利用者は全てのインプットに対する結果であるアウトプットの全てを事前に知っていなければならない。
- 全ての利用者は過度のメモリーと計算時間を費やすDoS(denial of service)攻撃から安全でなければならない。
- スマートコントラクトの利用者はプログラムの実行に必要なコストを全てのインプットに対して事前に理解できなければならない。
イーサリアムのEVMのようにブロックチェーンの為にデザインされた従来のプログラミング言語も上で記述した問題に直面しています。つい最近には、全てのインプルメンテーションが計算の結果に同意しなかった為、EVMのアップグレードがテスティングの際に失敗した例もありました。スマートコントラクトのロジックのエラーや、リソースのリミットを超えたことによって資金が盗難されたり、回収不能になった例は幾つもありました。
一方で、ビットコインのスクリプト言語は一般的にはデジタル署名の確認、タイムロック、ハッシュロックのコンビネーションに限定されています。ライトニング・ネットワークのような素晴らしいプロトコルが限定された機能の上で作られましたが、ビットコインのスクリプト言語は高度なスマートコントラクトをデザインするには表現性に限りがあります。
Simplicityは高度な計算の為の柔軟性と表現性を提供する一方で、安全性、セキュリティとスマートコントラクトの費用を検証できる言語を目指しています。
Simplicityとは何か？
Simplicityは低レベルのプログラミング言語でありブロックチェーンを基盤とするスマートコントラクトのマシーンモデルです。簡単なセマンティクスを持つよう一からデザインされており、形式手法によるスタティック解析と推論が可能です。Simplicity言語はCoq proof assistantでのインプルメンテーションで定義されています。
言語のコアはTシャツに納まるほど非常に簡単ですが、言語の簡単さが開発の簡単さには直接的に繋がるわけではありません。その理由としては以下をご覧ください。
- ブロックチェーンは従来のプログラミングモデルとは根本的に違います。ブロックチェーンの役割は計算結果を検証することであり、計算自体が主ではありません。微細な違いと思いがちですが、チューリング完全性を持たなくても任意コードの実行の際、検証が可能である為大きな違いでもあります。
- スマートコントラクトはその特性としてディプロイされた後は変更不可能であり、間違いを修正することはできません。Simplicityはこの問題に対して利用者がスマートコントラクトの正確性の正式証明を基に検証できるようしています。
- Simplicityは直接実行するには非常に低レベルの言語です。JavaやPythonよりアセンブラ言語に似ているでしょう。究極的には高レベル言語でコントラクトを書き、Simplicityでコンパイルすることになるでしょう。
最新情報
以前、Simplicityに関してブログ記事で紹介したのですが、それから単なる試験的言語リサーチから正式的な言語スペックを持ち合わすように努力してきました。
Coq proof assistantにてSimplicity言語を再実装しました。
- 署名データ、アサーション、移譲などの拡張機能を含めSimplicity言語の表示的意味論の確立
- 自由カテゴリーに基づく“the Bit Machine”と称する抽象機械の正式的仕様によってSimplicityコア言語の操作的意味論の確立
- Tagless final styleから作られたHaskellの実装例からSimplicity表現の評価、実行、タイプ検証が可能
- モデュラー方式のSimplicity言語の拡張機能は使用しない時には、その効果を無視可能
- libsecp256k1の再実装版を含めSimplicityで書かれた暗号化プリミティブを保有
- Simplicity言語の非公式的数学的仕様について説明されているテクニカルレポートを提供。CoqやHaskellで開発の為のガイドを提供。
Simplicityの開発は今も進められていますが、エンジニア自らがSimplicity言語を使い色んなことを試す段階に入ったと思います。Simplicityの開発はオープンソースとし、メーリングリストを始めました。
これからの課題
これからも様々な領域でSimplicityの開発が進められる予定です。
私たちが集中している領域は以下の通りです。
- C インタプリタの完了
- 様々な暗号化機能の為にjetsのライブラリを実装
- Verifiable Cを使いC インタプリタとjetsが正確であることを証明
- Elementsブロックチェーンプラットフォームへの統合
他の領域としては:
- Simplicityコードのオプティマイザー開発。
- Simplicity生成の為にIvyのような高レベルのスマートコントラクト・プラットフォームの開発、または、適合。
- Simplicityの暗号化プリミティブの機能的正確性と暗号化プロトコルの正式的正確性の結合を通じて完全に検証可能なスマートコントラクトの開発
私たちと一緒にプロジェクトに参加しませんか。