Scilla
WIP
概要
Zilliqa向けのスマートコントラクト言語
coqを使って形式的検証を行う
参考
Scillaの概要と背景、スマートコントラクト、Coqによる証明までまとまったスライド まだ開発途中
(2018年9月現在、ここ数ヶ月のアップデートがあまりない?)
型チェック機能がない
現状はScillaを直接インタプリタが実行しているが、将来的には、
EVM風のバイトコードまたはLLVMにコンパイルされる
Scillaを中間言語として、高級な言語で開発する
形式的検証をデプロイ時に義務付ける(かも)とブログに書いてあった
設計思想
Separation between computation and communication
コントラクトを一つのオートマトンと見立て、その内部の計算(ステートの書き換えや関数実行)と、他のコントラクトとのコミュニケーション(message)を分ける
Separation between effectful and pure computations.
pureな式とステートの操作を分ける
形式証明しやすくする
Separation between invocation and continuation.
継続渡しスタイル
プログラムの制御を、「継続」(まだ評価されていないプログラムの残りの部分)を用いて明示的に表すプログラミングスタイル
外部の(コントラクトの)関数のコールは最後の命令になる
transitionの最後でcontinuationを呼ぶ
リエントラント攻撃を防げる
特徴
チューリング完全ではない
ループの代わりに再帰
決定的
スマートコントラクトのモデル
決定性オートマトン
オートマトン同士が通信
https://gyazo.com/cd9ab268d6006d15a573467743d0353b
ScillaからCoqにトランスパイルし、Coqにより形式的検証を行う
現状はマニュアルだが、いずれ自動でやれるようになる
参考