IsabelleによるCBC CasperのSafetyの証明をしました

日記です。

リポジトリ: LayerXcom/cbc-casper-proof

概要

(私は LayerX の人ではないですが)LayerX 社の人と色々あって CBC Casper というブロックチェーンのプロトコルの検証作業を行いました。(主に定理証明士としてのお手伝い)

半年くらいかかったけどやりたかった証明についにたどり着いたよという話。

CBC Casper って何

わからん。(無知)

何かブロックチェーンのプロトコルの名前らしい。Ethereum 財団が目をつけてるらしい。いわゆるビットコインとは違ってブロックを頑張ってマシンをぶん回してマイニングしたりしないらしい(ビットコインは PoW で CBC Casper は PoS)。

詳しいことは詳しい人に聞いたほうがいいよ(真理)。

cf: CBC Casper と形式的検証

Isabelle で検証って何するの

ブロックチェーンはコンセンサス(分散合意)アルゴリズムの一種で、みんなで合意を取りましょうみたいなやつ。コンセンサスアルゴリズムで言われる正当性というのは主に次の 2 つ。

  1. Safety: 1 つの round でたかだか 1 つの値にしか合意しないこと
  2. Liveness: 必ず 1 つの値にいずれは合意できること(一生合意できないみたいな状態に陥らないこと)

実際のステートメントでは色々条件はあるがそういうのは一旦おいておいて、CBC Casper に対しては Safety は示されていて(論文があり) Liveness はまだ示されていないみたいなステータスだったはず。定理証明はどちらもされていないので、今回は簡単な(というか参考になる論文がすでにある)Safety の方を示した。

実際の証明について

証明は基本的に論文に沿って進めた: https://github.com/cbc-casper/cbc-casper-paper

ただし Safety Oracle の証明について、論文では clique というタイプのグラフについての性質を示すことで証明を行っているが、今回はこれを inspector(finality detector)というやつに一般化して証明を行った。

完走した感想

ドメイン知識がないこともあってめっちゃ大変だったというのが正直なところ。アタリマエであるが、論文に書いてない行間を埋める作業や誤植・足りない仮定を追加するなどの作業はちゃんと理論側の理解がないとやはりつらい。

一方で、今回は「理論側は別の人・定理証明は私」という分担を行ったが、そういう感じでもこういう証明の仕事を行うことは不可能ではないなという手応えを感じることが出来たのも良かった気がする。

証明がめっちゃ汚いのとまだ一般化する余地がそれなりに残っているので(あと Liveness の証明という大仕事も手付かずだし…)、気が向いたらまた続きをやりたいと思います。

Isabelle について

今回の証明を通して得た、Isabelle についての学び

  • 定理はなるべく HOL より Pure logic の形で述べるほうが良い: apply (rule THM) って出来るの偉大だなと思った
  • context を必要に応じて使おう: 以後〜を仮定する、みたいなのが意外とある
  • sledgehammer は definition が苦手: definition を入れると展開した後の探索が必要な分 sledgehammer の賢さが目に見えて下がってしまう。definition でラップする場合はちゃんと補題もラップしたやつを用意しておいてあげないといろいろ大変
  • Isabelle のタクティクスよくわからない: sledgehammer にばっかり頼っているので未だに rule と simp くらいしかわからない…。どっかでちゃんと勉強したいですね(どこで？)

終わりに

私は定理証明士としての貢献ができてそれなりに満足したので、もしこれを見て興味が沸いたつよつよ定理証明士は私の代わりに残りの作業をやってほしい。