GhaSShee


Quadratic Arithmetic Programs


This is the Japanese translation of https://vitalik.ca/general/2016/12/10/qap.html . 最近の zk-SNARks の技術の背後には、興味深い話がたくさんある。 とりわけ、これらの話は、暗号学の知識でいうと、変換が潰れていて可逆性のないような、複雑度に依存しており、 多くの人が、ますます、その高度な数学への険しい道のりへと果敢にも挑戦している。 zk-SNARKs は、実際に把握するのは、かなり挑戦的な課題ではある。 とくに、複雑な各部分を理解した上で、全体像を想像するのは困難と言えるかもしれない。 しかしながら、これら背後にある原理を細かく断片にまで分解してひとつひとつ眺めていくと、随分シンプルなものだということがわかるはずだ。 ![](/image/vb/qap01.png) この投稿の目的は、zk-SNARKs の導入が目的ではない。 この投稿は、次の二つの前提を必要とします。 1. zk-SNARKs がどういうものであり、どのような目的で使われるのか。 2. 多項式計算のような基礎的な数学の知識( $ P, Q $ を多項式とすると、$ P(x) + Q(x) = (P + Q)(x) $ はとても自然で自明だと感じられるくらいのレベルで十分である) この投稿では、zk-SNARKs の背後にある技術のパイプラインにおける前半部分を、zk-SNARKs 研究者の Eran Tromer 氏が描くイメージに沿って説明をする。 まず、この前半部分の説明を行うにあたり、さらに2つのステップに分解する。 最初に、zk-SNARKs は、どのような計算問題に対しても、直接適用できるわけではない。 むしろ、計算問題を zk-SNARKs が適用できる「正しい形式」に変換しなければならない。 その形式は、「二次算術プログラム Quadratic Arithmetic Program 」 と呼ばれており、QAP と呼ぶことにする。 計算を表す関数を、この形式に変形することは、それ自体自明なことではない。 関数のコードを、QAPの形式に変換するプロセスに伴って、もう一つ別のプロセスが次のような役割をする。 もし、コードが入力を持てば、それに対応する QAP の「解答」(しばしば、QAP の witness と呼ばれる。)をひとつ作るのである。 そのあと、さらに、別の公正な意味で多種多様なプロセスがあり、実際に witness に対する『ゼロ知識証明』を作成する。 別のプロセスが、つまり、検証者は、誰かにより手渡された証明を検証するのであるが、それは本稿では説明しない。 ここでは、簡単な例をあげよう。 この例では、あなたは、ある三次方程式 $ x^3 + x + 5 = 35 $ の解を知っている (その解を $ x = 3 $ としよう) ということを証明したい。 この問題設定は、結果としてでてくる QAP は、それほどでかい規模のものでないが、すべてのカラクリが十分に可視化できるくらいには十分非自明な例である。 われわれの取り扱う関数を定義すると次のようになる。 ~~~python def qeval(x): y = x**3 return x + y + 5 ~~~ ここで、我々がコードを記述するのに使うプログラミング言語は、とてもシンプルなものであり、 加減乗除 $ + , - , * , / $ や、$ x^7 $ のような定数乗数(つまり、$ x^y $ はサポートしていない。) 、そして、代入演算 $ x := a $ をサポートしているが、 剰余計算 module (%) や、比較演算子 $ \le $ などはサポートしていない。 (というのは、暗号理論の基礎となっている数体系である、有限巡回群の中で、大小比較などができてしまえば、 二分探索や中国剰余定理を使って、暗号が破られてしまうからである。) この言語は理論的に、ループを持たない有限ステップの計算を行う文には、十分強力である。 この言語に対して、例えば、$ 13 = 2^3 + 2^2 + 1 $ のような 『bit 分割』を提供することで、比較演算や、剰余計算を与えて言語拡張することが可能で、 これら bit 分割の正しさを証明したり、(CPUなどの)二進数回路の設定における数学をすることを可能とする。 有限体上の計算では、 等さ $ == $ の検証は、可能であり、実際簡単であるが、この投稿では、そのあたりについては触れない。 この言語に、if else 文のような条件式をサポートするように拡張したいが、次のように考えることが可能である。 例えば、`if x < 5 : y = 7 else : y = 9` は、$ y = 7 * (x \lt 5) + 9 * ( x \ge 5 ) $ と解釈すればよいのである。 しかし、注意しないといけないのは、この変換だと、条件式が真のときの計算と偽のときの計算の双方を必ず計算しなければいけないので、 普通の条件式とはことなり、複数分岐をするオーバーヘッドは大きい。 さて、今から、このプロセスを逐一実行していきましょう。 もし、これを自分の環境で実行したいという方のために、教材用の簡単なコンパイラをつくりましたので https://github.com/ethereum/research/tree/master/zksnark を参照してください。 (あくまで教材用であり、実際の zk-SNARKs に適用する準備まではしていません。) # Flattening 第一のステップは、『平坦化 flattening』と呼ばれるプロセスです。 先ほど示した、複雑な文や式を含むようなプログラムコードを、次の二つの形式からなる文の列に変換します。 ~~~ x = y x = y (op) z ~~~ ここで、op は加減乗除 ` + , - , * , / ` を著しており、 $ y $ , $ z $ は、変数や定数あるいは部分式などをとることができます。 (BNF形式でかくと以下となります) ~~~BNF stmt ::= l = r | l = r op r l ::= v (variable) r ::= v (variable) | n (number) op ::= + | - | * | / ~~~ 上にあげた二つの文は、回路における(ニ値)論理ゲートのようなものだと捉えることができます。 最初にあげたプログラムコードを、今説明した文の列に変換します。 ~~~ sym_1 = x * x y = sym_1 * x sym_2 = y + x ~out = sym_2 + 5 ~~~ 元のプログラムコードと、この(3番値)コード列が等価であるということは、簡単にわかると思います。 # Gates to R1CS さて、このゲート形式(3番地コード)を 『一次元制約システム Rank-1 Constraint System』( R1CS )へと変換しましょう。 ある一つの RICS とは、三つのベクトル $(a,b,c)$ を一単位とし、その単位が集まってできたグループのことを指します。 R1CS に対する『解 solution』とは、ひとつのベクトル $ s $ を指し、 この解は、$s \cdot a \times s \cdot b - s \cdot c = 0$ という等式を満たさなければなりません。 ここで、$ . $ は、ベクトル内積です。 簡単な言葉で言えば、ふたつのベクトルを『zip』するともいいます。 つまり、ベクトル内の同じポジションの要素同志は掛け合わせる演算です。 つまりは、3番目の内積 $s \cdot c$ は最初の二つの結果の積に等しくなります。 例えば、次の図は、$s$ が、R1CS を満たしている図です。 ![](/image/vb/qap02.png) この解 $ s $ は、 ただ一つの制約条件を満たすように選ぶことができるばかりでなく、 各論理ゲート(3番地コード)に対応する複数の制約を満たすようにとることが可能です。 ひとつの論理ゲート(3番地コード)を、二項演算子 $+ , - , * , /$ に何をとるかで場合分けをし、 RICS $(a,b,c)$ の三つ組に変換する標準的な方法があります。 ベクトルの長さというのは、システムにおける、変数の総数に一致します。 ただしこれら変数には、定数を表す、ダミー変数 `~one` が1番目の変数として含まれます。 また、入力変数や出力変数や、媒体変数などもすべてふくまれます。 ベクトルは一般的に『疎 sparse』なものであり、論理演算の入出力変数に相応するベクトルのスロットを数で埋めるようなものです。 最初に、ここで使う、変数のマッピングを用意しましょう。 ~~~ '~one', 'x', '~out', 'sym_1', 'y', 'sym_2' ~~~ 『解』ベクトルは、これらのすべての変数に対する、順序通りの代入を満たすようなものとなります。 例でこのことを見ていきましょう。 最初の論理ゲート `sym_1 = x * x` は以下に変換されます。 ~~~ a = [0, 1, 0, 0, 0, 0] b = [0, 1, 0, 0, 0, 0] c = [0, 0, 0, 1, 0, 0] ~~~ もし『解』ベクトル $ s $ の2番目に $ 3 $ を 4番目に $ 9 $ をもっていれば、内積演算により、解としての制約 $ 3 * 3 = 9 $ を満たすことがわかります。 また例えば、2番目に $ -3 $ をもっていたとしても同様に解を満たすことになります。 実際、『解』ベクトルの2番目に $ 7 $ 、4番目に $49$ を持っていたとしても同じことが言えます。 いま行った、最初の解検査は、最初の論理ゲート(3番地コード)を通過するかだけを検証しています。 二つ目の論理ゲート `y = sym_1 * x` に移りましょう。 ~~~ a = [0, 0, 0, 1, 0, 0] b = [0, 1, 0, 0, 0, 0] c = [0, 0, 0, 0, 1, 0] ~~~ ここでは、一つ目のゲートと同じようにして `sym_1 * x = y`であるかを検査しています。 三つ目の論理ゲート `sym_2 = y + x` に移りましょう。 ~~~ a = [0, 1, 0, 0, 1, 0] b = [1, 0, 0, 0, 0, 0] c = [0, 0, 0, 0, 0, 1] ~~~ ここでは、パターンが少しちがいます。 先ほどまでの論理ゲートが『乗算』 $*$ を取り扱っていたのと異なり、『加算』$+$ を符号化したいので、ベクトル $ b $ を単に、定数 $1$ ととることで、 ` (x + y) * 1 = sym_2 ` といった検査を表すことが可能となります。 最後に、四つ目の論理ゲート `~out = sym_2 + 5` を見ていきましょう。 ~~~ a = [5, 0, 0, 0, 0, 1] b = [1, 0, 0, 0, 0, 0] c = [0, 0, 1, 0, 0, 0] ~~~ この内積は、6番目の要素に、一番面の要素を $1$ を $5$ 回を足し、ます。 (つまりは、$ 5 $ を加算するの演算をしています。) そして、3つ目の要素である、`~out` と等しいかどうかを検査しています。 これまでの4つの制約からなる、R1CS が構成されました。 この RICS に対する『解』あるいは witness は、これらすべての変数に対し、代入される次のベクトルです。 ~~~ [1, 3, 35, 9, 27, 30] ~~~ この解は、最初の入力となる、変数代入 $ x = 3 $ から初めて、平坦化された3番値コードの列を順に計算し、その結果を順次変数に入れていくことにより、簡単に得ることができます。 これらをひとつの R1CS として表示すると、 ~~~ A [0, 1, 0, 0, 0, 0] [0, 0, 0, 1, 0, 0] [0, 1, 0, 0, 1, 0] [5, 0, 0, 0, 0, 1] B [0, 1, 0, 0, 0, 0] [0, 1, 0, 0, 0, 0] [1, 0, 0, 0, 0, 0] [1, 0, 0, 0, 0, 0] C [0, 0, 0, 1, 0, 0] [0, 0, 0, 0, 1, 0] [0, 0, 0, 0, 0, 1] [0, 0, 1, 0, 0, 0] ~~~ となります。 # R1CS to QAP つぎのステップは、この R1CS を 『QAP 形式』に変換することです。 この『QAP形式』は、ベクトル内積の代わりに、多項式を利用するということ以外は、同じ理屈で実装されます。 次のように行います。 長さ6の3ベクトルの4つ組を、(4-1)次多項式3つを一組とした、6組に変換します。 ここで、多項式 $P$ において、座標 $x$ において表される値 $P(x)$ はひとつの制約をあらわしています。 つまり、$ x = 1 $ で多項式を評価すると、1番目の変数に関する制約を表す縦ベクトルを得、 $ x = 2 $ で多項式を評価すると、2番目の変数に関する制約を表す縦ベクトルを得る、といった具合です。 この変換に『ラグランジュ補間 Lagrange interpolation』と呼ばれる手法を用います。 ラグランジュ補間が、解くことのできる問題とは、次のようなものです。 座標の組 $(x,y)$ である点の集合から、それらの点をすべて通るような多項式をつくるような方法のこと指します。 我々は、次のようにこの点集合から多項式をつくるという問題を分割して考えます。 各座標 $x$ に対し、次のような多項式を一つ与えます。 座標 $x$ に対しては、$y$ 座標をもつものの、他のすべての点に関して、$y$ 座標の値が $0$ となるような多項式です。 そして、最終的にこれらの多項式をすべて足し合わせます。 ひとつ例を見てみましょう。 $ (1,3) (2,2) (3,4) $ の3点を通る多項式が我々が得たい曲線だとしましょう。 まず、我々がつくるのは、$ (1,3) (2,0) (3,0) $ を通る多項式です。 これは、$y=0$ をもつ2点を通る次の多項式を少し変形すればよいのです。 $$ (x - 2)(x - 3) $$ ![](/image/vb/qap03.png) $x=1$ における高さを修正するために、 $\frac{3}{(1 - 2)(1 - 3)}$ を掛け、再スケールすればよいわけです。 $$ (x - 2)(x - 3) \times \frac{3}{(1 - 2)(1 - 3)} $$ つまりは、 $$ 1.5 x^2 - 7.5 x + 9 $$ ![](/image/vb/qap04.png) を得ます。 他の2点についても同様にします。 つまりは、上の例では、 $x=1$ を固定していましたが、$x=2$ と $x=3$ をそれぞれどうように固定し、 さらに二つの多項式を、同じ手順により作ることができます。 こうして得た三つの多項式を全て足し合わせると、 $$ 1.5 x^2 - 5.5 x + 7 $$ ![](/image/vb/qap05.png) を得ます。 まさにこれは我々の欲していた座標を通るグラフそのものです。 今示したアルゴリズムは $O(n^3)$ の計算量を要するものです。 $n$ 個の各点で、多項式を掛け合わせるのに、 $O(n^2)$ の計算量を要します。 少し頭を使えば、$O(n^2)$ へまで減らすことができ、より頭をひねり、Fast Fourier Transform を使えば、もっと速くすることが可能です。 というのは、これは、数千の論理ゲート(3番地コード)を持つような zk-SNARKs の最適化にとっては、とても重要な課題であるのです。 さて、われわれが得た R1CS に対してラグランジュ補間を適用してみましょう。 まず、すべての $a$ ベクトルから、最初の要素をとり出し、 ラグランジュ補間を適用して多項式$P$ を作ります。ここで、$i$ における多項式の値 $P(i)$ は、$i$ 番目の $a$ ベクトルの最初の要素となります。 この手順をすべての $b$ ベクトルと $c$ ベクトルの最初の値の各集合に対しても同じことして多項式を二つつくります。 そして、また $a$ ベクトルに戻り、今度は2番目の値を抜き出して同様のことをし、3番目、と同様にくり返します。 こうして得られる多項式 polynomial の結果だけをお見せしましょう ~~~ A polynomials [-5.0, 9.166, -5.0, 0.833] [8.0, -11.333, 5.0, -0.666] [0.0, 0.0, 0.0, 0.0] [-6.0, 9.5, -4.0, 0.5] [4.0, -7.0, 3.5, -0.5] [-1.0, 1.833, -1.0, 0.166] B polynomials [3.0, -5.166, 2.5, -0.333] [-2.0, 5.166, -2.5, 0.333] [0.0, 0.0, 0.0, 0.0] [0.0, 0.0, 0.0, 0.0] [0.0, 0.0, 0.0, 0.0] [0.0, 0.0, 0.0, 0.0] C polynomials [0.0, 0.0, 0.0, 0.0] [0.0, 0.0, 0.0, 0.0] [-1.0, 1.833, -1.0, 0.166] [4.0, -4.333, 1.5, -0.166] [-6.0, 9.5, -4.0, 0.5] [4.0, -7.0, 3.5, -0.5] ~~~ これは、多項式の係数を次数のひくいものから昇順であわらしています。 例えば、一番上の多項式は、実際は、 $$ 0.833 x^3 -5.0 x^2 + 9.166 x - 5.0 $$ を表現しています。 この多項式の集合(に後で説明する『Z多項式』をひとつ加えたもの)は、 ひとつの QAP を構成し、ひとつのプログラムを表しています。 今まで行った全構成は、zk-SNARKs を使って検証をするようなすべての『関数』に対して、一度行うだけで良いということには注意しておくべきでしょう。 一度 QAP パラメータを生成すれば、再利用することが可能なのです。 これらの全ての多項式を $x=1$ で評価してみましょう。 $x=1$ を代入するわけですから、単に係数を全て足し合わせるだけで良いわけです。( $1^k = 1$ となります。) ~~~ A results at x=1 0 1 0 0 0 0 B results at x=1 0 1 0 0 0 0 C results at x=1 0 0 0 1 0 0 ~~~ これは、まさに最初の論理ゲート(3番値コード)に対して、我々が作成したベクトルの集合そのものです。 # Checking the QAP さてこの一風変わった変形の要点とはなんであろうか。 その答えとは、個々の R1CS での制約をそれぞれ検査する代わりに、 多項式上で内積検査をすることで、制約条件を同時に検査することができる、ということである。 ![](/image/vb/qap06.png) 多項式上で、の内積検査と、多項式上の一連の加算や乗算の列であるので、 結果もまた、多項式となる。 もし、結果となる多項式上で、全ての論理ゲートを表す各 $x$ 座標で評価された値が、$ 0 $ に等しいならば、 検査はすべてパスしたということを意味する。 もし、ひとつでも $0$ でない値がでてきたならば、論理ゲート(3番値コード)に入る値と出てきた値が不一致だ、ということになる。 (つまりは、3番値コードが $ y = x * sym_1 $ で、変数として、 $x=2$ 、 $sym_1=2$ 、 $y=5$ が与えられている状況などである) 結果としてでてくる多項式が、零定数多項式である必要はない。 実際そのようになるような場合はほとんどない。 どの論理ゲート(3番地コード)とも関連しない $x$ 座標においては、どのような値を取っていても良いわけである。 正しさの検証をするのに、実は、結果としてえられたこの多項式を直接評価しなくても良いのである。 その代わりに、$ (x-1)(x-2)(x-3)(x-4) $ という別の多項式で割ると、余りがでないことを確認すれば良いのである。 今割るのに使用したものを『Z多項式』と呼ぶことにする。Z多項式は論理ゲートの数により、 $ (x-1)(x-2)(x-3)(x-4)... $ となり、 論理ゲートの数だけ多項式の値が、$ 0 $ となる点をもつような『最小多項式』であるという。 代数学の基本的事項として、 これら全ての点で、零をとるような多項式というのは、上の最小多項式を含んでいるということが知られている。 各値で評価すると零になること、と最小多項式で割り切れることの二つの命題が同値であることから、 我々がすべきことを、もっと簡単にすることができます。 さて、実際に多項式に対して、内積検査を行ってみましょう。 最初に、途中式となる三つの多項式を得ます。 ~~~ A . s = [43.0, -73.333, 38.5, -5.166] B . s = [-3.0, 10.333, -5.0, 0.666] C . s = [-41.0, 71.666, -24.5, 2.833] ~~~ さてこれらを $A \cdot s \times B \cdot s - C \cdot s$ により計算すると、 ~~~ t = [-88.0, 592.666, -1063.777, 805.833, -294.777, 51.5, -3.444] ~~~ となります。再小多項式は、 ~~~ Z = [24, -50, 35, -10, 1] ~~~ であり、この $Z$ で $t$ を除してやると、 ~~~ h = t / Z = [-3.666, 17.055, -3.444] ~~~ この商 $h$ が、余り無しで、得られます。 余りがないということは、割る前の多項式 $t = A \cdot s \times B \cdot s - C \cdot s$ において $x=1,2,3,4$ を代入した値すべてが $0$ となるということです。 つまりは検証が成功し、我々は、QAP の解を持っていることになるのです。 もし、検査を失敗させたいならば、例えば、解の最後の値を、30 でなく 31 とすると、 x=3 での値が -1 となり検査が失敗するような多項式 $t$ が得られます。 あるいは、最小多項式Zで割ると、余り `[-5.0, 8.833, -4.5, 0.666]` が出てしまい、検査失敗となります。 実際の zk-SNARKs の世界では、これらの加減乗除は、実数上で行われるのではなく、 有限体の上での演算となります。代数的法則を満たすような、少し風変わりな演算が定義され、その演算を実際は行っています。