博士

ロボ子、今日のITニュースはLean4でZK回路の埋め込みDSL「clean」を構築する話じゃ。

ロボ子

ZK回路ですか。ゼロ知識証明に関連する技術ですね。

博士

そうじゃ、ロボ子。ZK回路はバグが多いから、形式検証が重要になってくるのじゃ。そこで、Lean4を使ってZK回路を記述し、形式的に推論できるDSLを構築するらしいぞ。

ロボ子

形式検証でバグを減らせるのは良いですね。具体的にはどうやるんですか？

博士

まず、回路言語がサポートするプリミティブを定義して、そのセマンティクスを定義するのじゃ。そして、回路に対して形式的に証明するプロパティを定義するぞ。

ロボ子

なるほど。回路は変数、制約、ルックアップ関係で構成されるんですね。

博士

そうじゃ。ゼロ知識証明システムは、証明者が制約とルックアップを満たす証拠を知っていることを検証者に納得させる必要があるからの。

ロボ子

重要な性質として、健全性と完全性があるんですね。健全性は回路が過小制約でないことを保証し、完全性は回路が過剰制約でないことを保証する、と。

博士

その通り！DSL設計では、回路定義のために4つの基本操作をサポートするぞ。Witness、Assert、Lookup、Subcircuitじゃ。

ロボ子

モナドインターフェースを使って回路を定義することで、自然な構文構造を使用できるんですね。

博士

`FormalCircuit`構造体を使って検証フレームワークを構築するらしいぞ。`β`と`α`はそれぞれ入力と出力の「形状」を定義するのじゃ。

ロボ子

`FormalCircuit`は、形式的に証明された再利用可能なガジェットをカプセル化するんですね。サブ回路の健全性と完全性の証明を再利用して、回路全体の健全性と完全性のプロパティを証明する、と。

博士

8ビット加算の例も紹介されているぞ。2つのバイトと入力キャリーを入力として受け取り、2つのバイトの合計を256で割った余りと出力キャリーを返すガジェットを実装および検証するのじゃ。

ロボ子

AIRテーブルの検証もできるんですね。Fibonacci数列を計算するトレースの例が示されている、と。

博士

そうじゃ。境界制約と再帰制約を使って、数列が正しく計算されることを保証するのじゃ。

ロボ子

今後の作業として、再利用可能な基本的な回路の豊富なライブラリを追加したり、一般的なハッシュ関数回路を定義してその正当性を証明したり、RISC-Vのサブセットに対する形式検証済みの最小VMを構築したりする計画があるんですね。

博士

GitHubで公開されているから、ロボ子もチェックしてみるのじゃ。

ロボ子

はい、博士。私も貢献できることがあれば嬉しいです。

博士

ところでロボ子、ZK回路の健全性を保つにはどうすれば良いか知ってるか？

ロボ子

うーん、難しいですね。健全な食事と適度な運動でしょうか？

博士

ぶぶー！それはロボ子の健全性じゃ！ZK回路は、形式検証をしっかり行うのじゃ！