| title | author | date | css | header-includes | |||
|---|---|---|---|---|---|---|---|
ゼロ知識証明を知りたい人のためのzkVM作成入門 |
ClankPan |
2025-03-12 |
|
|
このオンラインブックは執筆中です。完成版ではありません。フィードバック はこちらからお願いいたします。2025年6月の完成を目指しています。現在は推敲と校正前ですので、誤字脱字や文章におかしな部分がありますが、ご容赦ください
本書では、アセンブリ言語にコンパイルされたプログラムの実行を証明する仮想マシン、つまりzkVMを作成を通して、ゼロ知識証明について学びます。
zkVMにはパラダイムがありますが、その中でも比較的理解しやすいものを選びました。本書だけではzkVMの全てを知ることはできませんが、ここで得られた知識はゼロ知識証明の世界に飛び込む読者の足がかりになるはずです。一見、難しそうに見える数式やコードが出てきますが、全てステップ・バイ・ステップで説明していきます。分からないと感じたらぜひ前の章に戻ってみてください。
この本では、理論と実装のパートが分かれています。もし、理論の途中でわからなくなってしまったら、再度上から読み直して、理解できるところまで実装してみてください。手を動かしてみると、より理解が深まりその先へと進めると思います。また、この時代はChatGPTのようなLLMに質問することも理解の手助けになると思いますので、ぜひ活用してみてください。
この本の読者は数学やプログラムが得意である必要はなく、むしろパズルの解き方を頭の中や紙の上で時間をかけて理解できれば十分です。なぜなら、私たちは新しい研究をするのではなく、すでに答えがある問いに対して、その解き方を理解できれば十分だからです。
また、本書の理解には必要ないが重要な概念や補足、こぼれ話はコラムとしてまとめていきますので、身構えず気楽に読み進めてください。
ゼロ知識証明を知るのに、なぜzkVMを題材に選んだのでしょうか?これは、近年のゼロ知識証明の研究が、どのようにzkVMを作るかという方向で活発化しているからです。そもそもVMとはVirtual Machineのことで、仮想機械、つまりプログラム上でCPUなどのハードウェアをシミュレートし、さらにその上でプログラムを動かすという階層高構造になる仕組みのことです。ゼロ知識証明では複雑な計算を証明したいわけですが、基本的には証明のプロトコルによって書き方が異なります。
計算そのものをどう分かりやすく表現するかが問題になりますが、これにはいくつか方法があります。一つは専用の言語を作ってその言語でプログラムを直接書くことです。しかし、プログラマは既存のプログラムを専用言語でいちいち書き直したくないですし、ツールによって言語を使い分けることも認知的なコストが高くなりがちです。
一般的なプログラミング言語を専用言語に変換する、といった方法もありますが、プログラミング言語もバージョンによって書き方が微妙に異なりますし、全てに対して専用のコンパイラを用意するのもコストに見合うかわかりません。
そこで、既存のどのプログラミング言語からもコンパイルできて、変更が滅多に行われない言語、つまりアセンブリ言語そのものを証明してしまおう、ということです。アセンブリ言語で書かれた計算を証明するには、CPUそのもの挙動をゼロ知識証明のフォーマットで一度だけ定義し、どんなプログラムに対しても同じゼロ知識証明の回路を使い回せばいいのです。すると、プログラマも普段の業務と同じように好きな言語でプログラムを書き、自然とその計算が証明されるわけです。
zkVMはあくまでも「やりたいこと」であって、実際にどのような実装かを指す言葉ではありません。実装にはいくつかのパラダイムがあります。一つはプログラムの実行を一つの大きな証明回路にして、一度に証明しまう方式です。もう一つはプログラムの実行を小さなステップに分けて証明回路を繰り返し適用することで再帰的に証明する方式です。
前者をモノリシック(Monorithic)方式といい、後者をリカーシブ(Recursive)方式といいます。Monorithicで代表的なものはJolt/Lasso方式ですが、入門には難しすぎるので、比較的わかりやすいRecursiveのNova方式を本書では採用します。さらに、Novaの中でもわかりやすく今後の発展の基本となりそうなHyperNovaをベースに解説していきます。とくに、HyperNovaで使われる技術はJoltでも使われるものが多く、学ぶと他にも応用が効きます。
::::{.note} コラム: ゼロ知識証明の回路
ゼロ知識証明の中でもSNARKという分野では、計算をひとまとまりにした単位を回路と呼びます。面白いことにzkVMは、CPUを二進数のANDやORの論理回路から、有限体のADDやMULの証明回路で書き直していく作業になります。ある意味でzkVMは、論理演算を使わない別の世界のコンピューターをいえるかもしれません。
::::
::::{.note} コラム: Novaの一族
Novaは高速なRecursive方式として、2021年ごろに登場しました。その後も改良が登場しましたが、それらの名前はオリジナルのNova(新星爆発)にちなんで付けられていきました。
最初に登場したのがSuperNova(超新星爆発)です。その後すぐにHyperNova(極超新星爆発)が提案され、さらにその後すぐに二つを組み合わせたSuperHyperNovaなんていうのも提案されかけました。
爆発のインフレーションはすぐに終わりましたが、現在でもNeutronNova(中性子新星爆発?)のような〇〇Novaという名称や、Nebula(星雲)や ProtoStar(原始星)など宇宙にちなんだ名前が付けられています。
あなたのzkVMにも宇宙や星に関連する名前をつけてみるのも面白いかもしれません。
::::
ClankPan (@ClankPan)。NovaNet という zkVM 開発企業で働いており、仕事としては直接ゼロ知識証明に携わってはいないものの、個人的に勉強しながら業界の動向を追っています。
まだ黎明期にある zkVM は、ゼロ知識証明の中でも特に注目されるトピックですが、網羅的に学べる日本語の解説はほとんどありません。そこで、私自身の勉強の過程で得た知見をまとめようと思い、この書籍の執筆を始めました。
書籍のフォーマットは私の尊敬する植山類さんの「低レイヤを知りたい人のためのCコンパイラ作成入門」のフォーマットをお借りしました。
この書籍が、zkVM やゼロ知識証明に興味を持った日本の皆さんの学習に少しでも役立てば幸いです。
また、本書の内容を題材とした勉強会や講演のご依頼なども歓迎します。興味のある方はお気軽にお声がけください。皆さんと学びを共有しながら、zkVM やゼロ知識証明の面白さをより多くの方にお伝えできれば幸いです。
ゼロ知識証明というのは、その名の通り、「自分が持っている情報を明かさず、持っていることだけを証明する」技術の総称です。自分が隠したい情報を秘匿することが主な内容ですが、最近は計算量を圧縮することができる特性が注目されています。
たとえば、ブロックチェーン上で何かを計算させると、その計算量に応じてとにかく支払うコストが莫大にかかります。そこで、少しでも計算量と通信を減らしたいという動機が生まれ、この技術に注目と投資が集まるようになりました。これが近年急速にゼロ知識証明の研究が進んでいる理由です。
::::{.note} コラム: SNARK
情報を秘匿しなくてもいいから計算が正しいことを証明したい、という需要があります。これを他のゼロ知識証明と区別するため、SNARK(スナーク)と名付けられました。
サイズの証明が短く (succinct) 、やり取りが一度きり (non-interactive) という意味です。さらに、ゼロ知識性がある場合はzkSNARKとZero Knowledgeの頭文字であるzkを先頭につけます。
::::
計算量を圧縮できるとはどういうことでしょうか。これは、問題を解く計算量と答えを検証する計算量が対等ではない、というありふれた問題として考えることができます。
たとえば、ソートを例に考えてみましょう。数字を順列に並び替える計算は、数列が順列であることを確かめるよりも多くの計算を必要とします。並び替え単純な方法は、最初の数字が右の数字よりも小さいかを比較して、大きければ入れ替える、という計算を全ての数字が満たすまで繰り返していきます。
一方で、数字が全て小さい順に並んでいるのを確かめるだけなら、左から順に数字を比較していくだけなので、数字の個数分の計算だけで済みます。つまり、100個の数字があるとすれば、ソートにはざっくり660回程度の計算が必要になりますが、確かめるには100回程度だけです。
このように、解く計算量よりも検証する計算の方が小さい、といった問題はありふれています。もし仮に、プログラムなどの計算をソートの解を求めることに置き換えることができるのなら、プログラムの計算が正しいかは、解が順列であるかを確かめるだけです。
ソートはあくまでも例えなので実際の証明には使いませんが、大きく分けて
- 計算をとある問題の解を求めることへ変換して証明、
- その問題の解が正しいか検証してもらう、
の二つに分けることができます。
ソートの例の代わりに、シュワルツ・ジッペルの補題(Schwartz-Zippel lemma)とSumcheck(合計チェック)いうものを使います。この二つによって、証明者が出した解を、検証者がより少ない計算で検証することができます。
ではいったい、どんな計算を減らすことができるのでしょうか? それは、式の合計を求める計算です。
シュワルツ・ジッペルの補題とサムチェックを使うことで、証明者は式の合計がとある値になることを伝え、検証がそれが成り立つかを簡単に確かめることができるのです。
まずは、多項式が何かについておさらいしていきましょう。多項式とはその名の通り、項(係数
シュワルツ・ジッペルの補題は、「 二つの多項式の変数をランダムな値で評価したときに同じ結果になれば、二つが同じ多項式であると見なせる 」といった定理です。中学や高校の数学の授業で、「二つの式が交わる点を求めよ」という問題を解いたことはないでしょうか? 2つのグラフは、ほとんどの場所で重ならず、一点か二点だけでしか交わりません。
2つの多項式をグラフにプロットしたときに、交わる点は全体の中では驚くほど少ないということです。なので、全く異なる多項式が、完全にランダムな点で交わる確率は極僅かになります。この確率は適切に設定すれば実用上無視できる確率になります。どれくらいかというと、地球上のすべての砂粒の中から、私がまいた砂の1粒を1回で選び出す確率よりも低くなります。
シュワルツ・ジッペルの補題は、ゼロ知識証明の中でも頻出なので、ぜひ押さえておきましょう。
証明者が特定の範囲では常に0になる多項式を見つけることができれば、検証者はその範囲の全ての値の合計も0であることを確かめれば良いのです。これにはサムチェックを使います。では、シュワルツ・ジッペルの補題はどこで出てくるかとういうと、サムチェックの中に出てきます。この辺りは後ほど解説しますので、身構えず読み進めてみてください。
::::{.note} コラム: 計算量を表すオーダー
これを、オーダー(
ソートには最速でも
このように、大きな
::::{.note} コラム: 式を評価?
多項式に限らず、式の変数に値で代入して結果を求めることを「評価」するといいます。この単語は英語由来のevaluationを直訳したものなので、日本語にすると少し不思議な感じがします。evaluationには値付けという意味があるので、式の値を求める述語としては少し納得できます。
どちらにしろ、数学の世界では評価という単語が使われていますので、計算する、くらいの意味として覚えておいてください。
::::
証明したい計算、つまりプログラム、を多項式の形で表現できれば、どうやら証明できそうなことが分かってきました。ここからは、計算をどう多項式に変換していくかについて考えていきます。プログラムを含めた色々な種類の計算のフォーマットの全てから直接多項式に変換する方法を考えるのは、非常にコストが高い作業になります。そこで、このような問題を解決するのによく用いられる手法が中間表現です。多様なフォーマットから変換しやすく、目的にフォーマットにも変換しやすい表現を中間に挟むことで、開発のコストを下げるという考え方です。
まずは、このような計算の記述方法についてみていきましょう。
プログラムを多項式に変換していく前ステップとして、まずは計算を次のような制約式の連なりで表現していきます。
ルールは、 それぞれの項の中にはいくら足し算を入れもていいですが、掛け算は1つの制約式につき一回だけですので、もう一度掛け算が必要な場合は次の式で行います。
たとえば、フィボナッチ数列なら次のようになります。aとbを足した結果がcとなり、次の行ではbとcが足されdとなっています。変数が同じなら、
変数に値を入れてみると、次のようになるはずです。この
この表現方法でプログラムのすべてを書き出すのは少々骨が折れる作業ですが、全くできないという程でもありません。また、変換するツールなどもあるので、それらを使えば好きなプログラムをこの形式に直すこともできます。先ほど説明した専用言語やコンパイラのことです。
浮動小数点数やビット演算などの表現が難しいものは、別の技術を使ってカバーします。
::::{.note} コラム: ルックアップ
ビット演算などの論理演算を、このような代数演算的な表現に落とし込むのはとても大変です。たとえば、変数が
このようにして、1つの変数に1つのビットを割り当てていくことができますが、32bitを表現するだけで30以上の制約式が必要となってしまいます。
このように、コンピュータ上で行われる全ての式を代数的な表現に置き換えることは証明コストの面から難しいため、通常は別の方法が使われます。それがルックアップです。
ビット演算などの計算に対して、あらかじめ答えが記録された表を作っておき、表に対して正しい入出力が行われたかだけを制約します。
::::
::::{.note} コラム: 中間表現 IR
中間表現のことを一般に IR(Intermediate Representation)といいます。この用語はプログラミング言語の世界でよく使われるもので、様々なな言語から多様なCPUに対して言語を変換する際によく考えらます。特に、CPUの命令セットよって機械語が大きく異なるので、IRは必須です。もしIRがなければ、この世には「言語の種類
一番有名なIRは、LLVMでしょう。LLVMは抽象的な命令セットで、ここから多くのアーキテクチャ向けに変換することが可能です。多くのプログラミング言語のコンパイラは、このLLVMのIR向けに言語を翻訳することで、多くのCPUへの対応をサポートしているのです。
現実の世界でも、英語がこのような役割を持つことがあります。
執筆中: 英語、機械翻訳の中間言語
::::
さて、プログラムを単純な形で表現することができましたので、次は証明できる形へ変換していきます。特に、$a,b,c,d,v,w,x,..$ などの変数は、文字的に同じ変数と見なしているだけで、それらが同じであるかを制約するものは何もありません。
変数を束縛して、同じ変数をそれぞれの制約式で使われたものと同じであることを式として表現するには、行列の積を使います。行列の積を使えば綺麗に変数の束縛を表せるのですが、残念ながら私たちが使う証明には行列を使うことができません。そのため、行列の積をさらに多項式に変換してあげる必要があるのです。
このような変数の使い回しを式で表現するには、行列の掛け算を使います。まずは、行列について少し触れます。
行列と聞くと数学の難しい概念を想像してしまうかもしれません。しかし、実際には数字を縦と横に並べただけの表です。たとえば、これは、「2行
- 行 (row): 横方向のまとまり
- 列 (column): 縦方向のまとまり
上の例なら、1行目が
::::{.note} コラム: マトリックス
執筆中: 映画, NVidia, 機械学習
行列は見た目が複雑で数字がたくさん並んでいるので、難しいように見えますが、やることは至ってシンプルです。
ではなぜ行列というものが存在するかというと、
::::
行列をただの表として捉えることもできますが、便利な演算のルールが用意されています。
この行列の積を使って、
行列の積を使う理由は、「どの変数とどの変数を足し合わせるのか」を表現したいからでした。制約式の中では、
行列の掛け算をうまく利用すると、変数同士の足し算をうまく表現することができます。どの変数とどの変数を足し合わせるのか、これを先ほどのフィボナッチの例で見てみましょう。変数
まずは、計算に使われた変数
1番目と2番目が
これを拡張して、要素が
フィボナッチ数列の制約式のうち、$\alpha$ のすべての項の集合になっていることがわかります。
最終的に、行列の式で表すと、次のようになります。
行列を使うことで、どの変数をどう使うかを表現することができました。この表現方法はR1CS(Rank-1 Constrain System)と呼ばれます。
::::{.note} コラム: 中間表現の中間表現 CCS
執筆中: R1CS以外の中間表現, AIR, CCS
::::
::::{.note} コラム: 似て非なる、行列の式と行列式
一般的には「行列方程式 (matrix equation)」または「行列演算式 (matrix expression)」と呼びます。
「行列式 (determinant)」 は、行列から 1つのスカラー値(数)を計算する別の概念で、縦棒 |..| で書かれます。
*執筆中: *
::::
ここまでで、プログラムを制約式で表現し、さらに変数の束縛を行列の積で表現することができました。しかし、私たちが使う証明の方法では、行列の式を直接証明することができません。
そこで、行列の積で表現した変数の束縛を変えずに、行列の積そのものを多項式で表現します。
まずは、行列の積のルールについておさらいしましょう。二つの行列をかけるには、左の行列の「行(縦)」と右の行列の「列(横)」の要素をかけて足します。
行列の積の規則は複雑ですが、中身は掛け算の足し算のみですので、適切に分解してあげれば難しいことはありません。行列の
行列
式の意味は、「
証明で使えるような多項式に行列の積を変換する方向性が見えてきました。いくつか馴染みのない記号($\sum$ や
行列の式を多項式に変換するのは、証明に適した形にしたいからでした。ここまでをいったん整理してみましょう。フィボナッチ数列の制約式は、次のような式でした。
また、これを行列で表すとこうなります。行列を使う理由は、変数の束縛を表現できるからでした。
この式は、行列
では、$0$ 行目が実際にどうなるか一緒に式を展開してみましょう。
ここまでの、合計する記号
この式はつまり、
お気づきかもしれませんが、
ここまでは、
最終的な証明には、全てが多項式でなければならないので、記号
-
$A[i,j]$ : 「要素を取り出す記号」 -
$A(x,y)$ : 「要素を取り出す多項式」
使い方は、3番目の要素を取り出したければ、3つ目の変数のみを
しかし、これでは変数の数が多い上に、2つ以上を選択してその合計値を取ってくることが出来てしまします。そこで、$Z$ の
3は二進数では
用意するのは、2つの二進数が一致すれば
3bitはここに書くのは長いので2bitにしますが、展開するとこのようになります。ビットが違う項はゼロになるので、一つでもゼロになれば掛け算によって結果もゼロになります。
ということで
これを定義にしてみましょう。 少し複雑なので順を追って説明していきます。
例えば、このようになります。
::::{.note} コラム: 多重線形拡張 MLE
執筆中 ::::
定義した多項式を一つにまとめます。
$$ \begin{aligned} G(X) &= \sum_{y\in {0,1}^{\log N}} \tilde{A}(X, y) \cdot \tilde{Z}(y) \cdot \sum_{y\in {0,1}^{\log N}} \tilde{B}(X, y) \cdot \tilde{Z}(y)
- \sum_{y\in {0,1}^{\log N}} \tilde{C}(X, y) \cdot \tilde{Z}(y) \ \ &X \in {0,1}^{\log M} \end{aligned} $$
この
行列の行数
全て
しかし、例えば、$G((0,0)) = 1, G((0,1)) = -1$ だとすると、お互いを打ち消してしまい、合計として
そこで、$G$ にランダムな係数をかけて、打消し合う可能性を小さくするという発想が考えられます。
だだし、これでは変数がなく、多項式ではなくなってしまうので、次のようにしてあげることで、多項式のままにすることができます。
$$
\tilde{Q}(\beta) = \sum_{y\in {0,1}^{\log M}} G(y) \cdot eq(y, \beta) = 0
$$
式を見ると、$G$ にかかるランダムな係数が、$eq(y, \beta)$ によって変化していくことがわかります。ランダムな値
例えば、$\beta = (11, 22)$ ならば、次のように展開できます。
そこで、$Q(\beta)$ から合計する前の項を取り出し、
検証者に直接
ここで使えるのが、sumcheck protocol です。検証者が全パターンを試すよりも少ないコストで、全てのパターンが
いよいよ登場しました、Sumcheck Protocol です。 仕組みを言葉で表現するならば、「変数が1つの多項式に分解し、それぞれが同じ多変数多項式がベースであることをランダムな点で検証してもらう。」です。
多変数多項式とは、
単純に考えると、3変数多項式なら、$f$ の中の3つの変数の評価を8パターンで試すので、$3 \times 2^3 = 24$ の計算が必要になります。
一方で、3変数多項式を3つの1変数多項式に分解すると、変数を評価は同じく8パターンですが、式中の変数は1つだけなので、
Sumcheck Protocol では1つの式ごとに3回の評価が必要なだけなので、
このように、検証者の評価の回数を減らしつつ、適切に元の多変数多項式が分けられているのかを証明するのがこの Sumcheck Protocolの肝なのです。
さらに、サムチェック・プロトコルを使った証明の中にもいくつかのステップがあります。これら三つの証明を組み合わせることで、全体の証明がなされます。今回はサムチェックを使っていますが、このような構成はよくあるので、ぜひ覚えておきましょう。
::::{.note} コラム: プロトコル
執筆中: 馴染みのない用語 protocol
::::
ではまず、多変数から1変数への変換方法を考えます。ここでは
検証者は、$g(X)$ が全てのパターンで
なので検証者は、本当に
しかし、$g_1(x)$ の内部の
二つが同じ値になるなら、$g_1$ の内部で使われている多項式
ここまでは
と検証しいき、$G((r_1, r_2,.., r_n)) = g_n(r_n)$ となることを確かめます。
1変数多項式とシュワルツ・ジッペルの補題によって、少ない計算回数によって合計が計算できることが分かりました。しかし、多項式コミットメントを使うと、これよりもまだ検証者の計算を減らすことができます。今の状態では、検証者は証明者から
目指すところは、多項式
まずは、式変形した結果をお見せします。この式の意味は、「$P(x) - b = 0$ という式は
この法則は、因数定理といいます。要は、「$f(a) = 0$ ならば、
では、実際に計算してみましょう。下の
左辺(
::::{.note} コラム: 因数定理
執筆中: 根と因数
::::
しかし、ここで起きる問題は、証明者が事前に
さて、ここから一気に複雑になりますので、頑張ってついてきてください。
まずは、次のような性質を持つ
これを利用すると、先ほど例に出した
ここで、$h(x)$ に重要な性質を追加します。それは、$h(s)$ の結果
よって、 $h_{s^0},..,h_{s^3}$ を渡された証明者は
検証者は、証明者に
では、この式が成り立つか展開して確かめてみましょう。
もし証明者が
このような性質を持つ
この
ここまでで、知られて良い乱数
乱数
ただし、乱数の生成のタイミングには注意が必要です。なぜなら、乱数を本来必要とする前に乱数が何であるかを知られてしまうと、任意の結果となる多項式をいくらでも作れてしまうからです。シュワルツ・ジッペルの補題は、多項式が乱数よりも前に存在することを前提としています。
では、どのように多項式よりも後に乱数を生成させるかというと、多項式のパラメーターやコミットメントをハッシュしたもの乱数としてしまう方法です。事前にハッシュがどのような値になるかを予測して多項式を決めることはできませんので、あとは、検証者が同じコミットメントなどをハッシュに入力して同じ乱数が生成されるかを確認すればいいだけです。
ハッシュ関数はコンピュータサイエンスにおいて広く利用される技術です。その実装は多岐にわたりますが、一般に次のような特性を持ちます。
- 出力から入力を逆算することが困難
- ある入力と同じ出力となる異なる入力を見つけることは困難
- 同じ出力となる異なる入力を見つけることは困難
これらの特性は、厳密には「逆像困難性」「第二原像困難性」「衝突耐性」と呼ばれています。しかしここでは、「事前に予測できない乱数として利用するという観点からは十分な性質であり、実際に使用する際はこのような特性を備えたハッシュ関数を選ぶ必要がある」として覚えておいてください。
::::{.note} コラム: 誕生日攻撃
執筆中: 第二原像困難性と衝突耐性の違い、
::::
::::{.note} コラム: 楕円軌道
執筆中: 惑星の軌道、ニュートンとケプラー
::::
::::{.note} コラム: 楕円曲線暗号
執筆中
::::
フィボナッチ数列はご存知の通り、再帰のプログラムで書くことができます。つまり、計算を続けようと思えばいくらでも続けることができるはずですが、"計算の変換" で示した方法では、固定の回数しか表すことができませんでした。この章では、いかに繰り返しを含む計算を証明するかを解説していきます。特に、プログラムにはループはよく含まれ、CPUの動作も繰り返しですので、この挙動はzkVMの作る上で欠かせません。
このままだと、再帰が含まれる計算は、繰り返した回数だけ証明が増えて行ってしまします。これでは、Succient(簡潔)ではありません。
繰り返しを含む計算を証明する方法として、まず考えられるのが、検証の計算を証明してしまうという方法です。この方法では、前の計算が正しかったことを検証し、その結果を今回の証明で入力として使います。そして、今回の計算結果とその証明は、次の再帰証明で使われるというわけです。最終的に、検証者は一番最後の証明だけを検証すれば、その証明には前の証明が正しいことが含まれているわけですから、一度の検証だけで済みます。
このようにしていけば、フィボナッチのような繰り返しを好きな回数だけ計算した結果を証明できるわけですが、繰り返しのたびに証明・検証を行うことは、非常に大きなオーバーヘッドとなります。
そこで考えられたのが、証明を最後まで遅延させることで証明・検証のオーバーヘッドを避けるFoldoing-Scheme(畳み込み)です。
TODO: 再帰と畳み込みの明確な違いの説明
ここからは、どのように計算を折りたたんでいくかを考えていきます。HyperNovaの根幹は、「多項式に変換した2つの計算を1つの多項式に折りたたむ」ことにあります。
では、どのように畳み込むかというと、サムチェックを行いたい二つの多項式を一つにしてサムチェックを行い、その時に内部に現れる多項式をさらに次のサムチェックへ送り出します。
そもそも、制約が満たされているかは、$Q(X)$ を全てのパターンの
$$ \left{ \begin{aligned} Q(X) &= G(X) \cdot eq(\beta, X), \[0.8em] G(X) &= \sum_{y\in {0,1}^{\log N}} \tilde{A}(X, y) \cdot \tilde{Z}(y) \cdot \sum_{y\in {0,1}^{\log N}} \tilde{B}(X, y) \cdot \tilde{Z}(y)
- \sum_{y\in {0,1}^{\log N}} \tilde{C}(X, y) \cdot \tilde{Z}(y) \end{aligned} \right. $$
サムチェックを行う過程で、検証者は
これは大きなコストなので、内側のサムを直接計算する代わりに証明者から与えられた値を使い、外側のサムを検証した後に、内側のサムをサムチェックで検証することが基本的なアイディアです。
InnerSum)、外側の合計(OuterSum)に分けることができます。
-
InnerSum:$v_i = \sum_{y\in B_y} \tilde{M_i}(r, y) \cdot \tilde{Z}(y)$ -
OuterSum:$(v_1 \cdot v_2 - v_3) \cdot eq(\beta, r)$
InnerSum には制約が満たされているかの多項式の計算が全て含まれているので重いですが、OuterSumには
HyperNovaでは、この InnerSum を折りたたみ、一番最後までサムチェックを遅延させることで、再帰証明よりも高速な再帰を行うことができます。
次の図は、畳み込みの全体の見取り図です。証明したい InnerSumを結合して、その証明で使われた新たなInnerSumを次の
では、流れを順番に追っていきましょう。
Incoming Sumは、実際に証明したい制約を表す多項式です。これの合計がゼロであれば、制約式が満たされていることになります。
$$ \begin{aligned} Q(x) &= G(x) \cdot eq(\beta, x), \[0.8em] G(x) &= \sum_{y\in B_y} \tilde{M_1}(x, y) \cdot \tilde{Z_1}(y) \cdot \sum_{y\in B_y} \tilde{M_2}(x, y) \cdot \tilde{Z_1}(y)
- \sum_{y\in B_y} \tilde{M_3}(x, y) \cdot \tilde{Z_1}(y) \end{aligned} $$
Inner Sumは、前回のサムチェックで証明を後回しにした多項式の合計、$v_1, v_2, v_3$ です。
まず、$v_i$ は次のように計算されます。これが前回のサムチェックで使われた訳です。注意して見て欲しいのが、ランダム
つまり、次が成り立つことを確認していきましょう。
左辺から展開していきましょう。
右辺も展開するとこのようになります。