🐙

コードによるHalo2(ZKP)入門

2024/03/09に公開

cryptography

zkp

halo2

tech

はじめに

ZKPの学習には数学がつきもので、それも楽しいんだけれど数学のバックグラウンドがない自分にとっては、それはそれで結構ハードで...
そこで、とにかく手を動かしてHalo2を触った感を得るのに素敵な記事があったので、かみ砕きつつ紹介していきたい。(なお私もZKPビギナーなので積極的に指摘いただけたら嬉しい。)

参考記事
https://hackmd.io/oLh70KETSqOK0NJ0vapocw#Endeavor-into-Halo2
ZKPについて詳細な説明は今回省くが、こちらの記事がとてもわかりやすいです。
https://dev.to/spalladino/a-beginners-intro-to-coding-zero-knowledge-proofs-c56
一旦細かいことはいいから動かしてみたいという方は5. テストしてみるからどうぞ

Halo2とは

Plonkという証明システムを用いたzkSNARKの1つです。Plonkについてはこれまた理解するのに骨が折れますが(数学が必須)、以前に記事を書いたので参考程度にどうぞ。

PLONKは比較的新しいzkSNARKの証明システムです。Groth16のようなこれまでのzkSNARKはcircuitごとにセットアップを行っていましたが、PLONKでは一度開始すればすべてのcircuitで再利用でき、他のcircuitを用いたりして再帰的な証明が可能であるこというところが大きな特徴です。

Halo2の部品

Halo2の全体感を抑えるのに良い図です。
Halo2 API & Building a Basic Fibonacci Circuit
Halo2における演算や計算の表現は、行と列を持つ行列として構成され、各セルは特定の計算の初期値、中間値、または出力値を持ちます。これらの値には制約が適用され、証明の正確性を保証するために必要なものです。
と言われてもよくわからないので、それぞれについてみていきます。

Columns(縦列)

advice columns(上記図)
証明者のprivate input（witness）を含む。これらの値はゼロ知識証明の構築において、秘密情報として扱われ、検証者には知られない。
instance columns(上記図)
証明者と検証者の両方に公開されている入力を含む。
fixed columns(上記図)
全ての証明で使用される固定された定数を含む。これらは回路の設計時に定義され、証明プロセス全体で変わることはない。
selector columns(上記図)
特定の制約を選択的に有効化するために使用される。これにより、計算の特定の部分(制約)を動的にオンまたはオフにすることができる。

制約とは

制約とは、ZKPにおいて特定の計算が正しいことを保証するための数学的条件やルールのことを指します。証明者が正しい計算を行ったこと、及びその計算結果が特定の条件を満たしていることを検証者が検証できるように設計されています。なので、そもそも制約が通らないということは正しく証明できなかったとも言えるのでZKPに置いて根幹をなす要素です。

Rows(横行)

行列の行数は通常2のべき乗で、有限体Fのサイズによって制限される。制約はすべての行に適用されるが、selector columnsで定義されたselectorによって有効/無効にすることができる。

有限体Fのサイズによって制限される理由

まず、有限体とは

有限体Fは、有限数の要素を含む数の集まりで、加算、減算、乗算、除算（0でない元(集まりの要素)に対して）の演算ができて、これらの演算に関して閉じている(演算の結果が要素にのいずれかになる)。有限体Fのサイズ（または位数）は、その中に存在する要素の数を意味し、通常∣F∣ と表される。

行数の制限の理由

多項式補間

ZKPでは、計算の正確性を証明するために多項式補間がよく使用される。特定の点の集合から一意の多項式を構築するプロセスです。例えば、1次関数y=ax + bだったら2つの点が分かればが式が定まります。2次関数だと3点分かればy=ax^2 + bx + cが定まります。この点集合の大きさは多項式の次数に影響を与え、次数は∣F∣−1 以下でなければなりません（有限体の性質による）。

有限体のサイズと多項式の次数

有限体F上で定義される多項式は、その体の要素を係数として使用します。多項式の次数が∣F∣ に近づくと、補間に使用できる点の数に自然な制限が生じます。なぜなら、有限体Fには∣F∣ 個のユニークな要素しかなく、それ以上のユニークな点で多項式を定義しようとすると、体のサイズを超えることになり、数学的に不可能になるからです。

行数と多項式の関係

ZKPにおいて、行列の行数は計算を表現するために使用される多項式の次数に対応します。行数が2のべき乗である理由は、FFT（高速フーリエ変換）アルゴリズムを使用することが多いためであり、FFTは2のべき乗サイズの入力で最も効率的に動作するそうです。有限体のサイズ∣F∣ によって行数が制限されるのは、上記の多項式補間の制約によるものです。

Cells

行列のセルは、セルの値はpubloc inputとwitness値に対応し、計算トレースと呼ばれます。つまりそれぞれのセルに、初期値が定まっていたり、計算していく過程で値が入っていったり、出力値として使われたりします。
ただ、列や行を増やすと証明のサイズが大きくなり、証明の生成や検証にかかる時間が長くなってしまいます。そのために、演算化を最適化する必要があり、最適化する方法の1つにレイアウターを使用する方法がありますが、後で説明します。
次の表はフィボナッチ数列の計算回路の表現です。各行は計算ステップを表し、a0とa1はフィボナッチ数列の2つ前の項目であり、a2は制約a2 = a0 + a1を満たすようにa0とa1を加算（a0 + a1）して計算されます。
Halo2 API & Building a Basic Fibonacci Circuit

a0, a1, a2は、advice column（制約のwitness）です。
各行で、制約を適用するためにselector columnsが有効(1)になっています。
0行目のa0とa1はフィボナッチ数列の最初の2項目です。

Gate

ゲートは、簡単にいうと演算が行われる制約がセットとなったものです。大きく2種類あります。

標準ゲート
乗算や除算などの一般的な算術演算。
カスタムゲート
よりカスタム可能で、回路内の特殊な演算をサポートできる。例を以下のフィボナッチ回路に示します（selectorが有効な場合、ゲートはすべての行に適用されます）。
Halo2 API & Building a Basic Fibonacci Circuit

Copy constraint

コピー制約（equality constraintとも呼ばれる）は、行列の2つのセルが同じ値を含むことを強制します。Halo2のコピー制約はPLONKのpermutation引数で表現されます。コピー制約の例を以下に示します。

0行目のa1 と 1行目のa0が等しい
0行目のa2 と 1行目のa1が等しい
ということを表現しています。

Lookup table

ルックアップテーブルは、あらかじめ計算された値の集合を格納するデータ構造で、特定の入力に対する出力値を取得(検索)するために使用されます。乗算や加算では簡単に表現できない、複雑な計算を効率的に扱うことができます。これはPlonk証明システムだから可能になっているものです。
(今回の例では扱いません)

ルックアップテーブルの使用例

ビットの検証
ある変数が0または1の値のみを取る（すなわち、1ビットの情報を持つ）ことを証明したい場合、0と1の値を持つルックアップテーブルを用いて、その変数の値がテーブル内の値と一致することを検証できます。
有効な範囲の検証
変数が特定の範囲内の値を持つことを証明するには、その範囲内のすべての有効な値を含むルックアップテーブルを使用し、変数の値がテーブル内に存在することを検証できます。
複雑な関数の計算
ある関数の出力値が入力値に対応することを証明したい場合、関数の入出力のペアをルックアップテーブルに格納し、特定の入力に対する出力値がテーブル内の値と一致するかどうかを検証できます。

こちらが参考になると思います。

Chip

チップは、回路実装の監査性、効率性、モジュール性を向上させることを目的として、特定の機能の事前実装を提供する、より高度なAPIです。関数のようなものと考えて良いかと思います。Halo2でチップを使って実装できる機能の例としては、暗号ハッシュ関数、スカラー乗算、ペアリング・チェックなどがあります。

Gadget

ガジェットは、チップの低レベル実装を抽象化しつつ、チップの機能にアクセスするためのより高レベルのインターフェース/APIです。チップを包み込んだコンポーネントのようなものと考えてよいかと思います。楕円曲線演算、シンセミラハッシュ関数、その他の機能をHalo2回路に実装するのに便利です。

Halo2で回路を書く方法

Halo2の部品を一通り抑えたので実際に書いていきましょう！
今まで見てきたフィボナッチ数列の回路を例にして、SNARK 証明を生成する Halo2 回路の実装方法を見ていきます。
コード

下記のステップで進めます。

Chipの設定
ゲートのレイアウト、セルとセル値の割り当て
回路の構築
テストのための関数を準備
テストしてみる
他にバグが起こる可能性を試してみる

1. Chipの設定

column（advice、instance、selectorなど）、コピー制約を定義して、カスタムゲートとルックアップテーブルを作成することから始めます。これを行うためのHalo2のConstraintSystemのAPIがあります。

advice_column
advice columnを作成する
instance_column
instance columnを作成する
enable_equality
指定されたカラムでの値の等価性をチェック(コピー制約)するための制約を有効にする命令。
create_gate
制約を含む新しいゲートを作成する

fibonacci.rs

// Config構造体を定義。これは、回路の構成を保持します。
#[derive(Clone, Debug, Copy)]
struct Config {
    elem_1: Column<Advice>,     // 最初のフィボナッチ数を格納するadvice column
    elem_2: Column<Advice>,     // 2番目のフィボナッチ数を格納するadvice column
    elem_3: Column<Advice>,     // 計算される数を格納するadvice column
    q_fib: Selector,            // 計算の適用を制御するselector
    instance: Column<Instance>, // public inputを格納するinstance column
}
impl Config {
    // Configのconfigureメソッドを定義。これは、回路の設定を行う
    fn configure<F: Field>(cs: &mut ConstraintSystem<F>) -> Self { // 可変のConstraintSystem参照を引数として受け取る
        // advice columnを作成し、それぞれに等価性の制約を有効にする
        let elem_1 = cs.advice_column();
        cs.enable_equality(elem_1);
        let elem_2 = cs.advice_column();
        cs.enable_equality(elem_2);
        let elem_3 = cs.advice_column();
        cs.enable_equality(elem_3);
        // instance columnを作成し、等価性の制約を有効にする
        let instance = cs.instance_column();
        cs.enable_equality(instance);
        // 計算の適用を制御するselectorを作成
        let q_fib = cs.selector();
        // フィボナッチ数列の計算を表すゲート（制約）を作成
        cs.create_gate("fibonacci", |virtual_cells| {
            // セレクタと各advice columnの現在の値を問い合わせる
            let q_fib = virtual_cells.query_selector(q_fib);
            let elem_1 = virtual_cells.query_advice(elem_1, Rotation::cur());
            let elem_2 = virtual_cells.query_advice(elem_2, Rotation::cur());
            let elem_3 = virtual_cells.query_advice(elem_3, Rotation::cur());
            // フィボナッチ数列の特定の性質を検証する制約を定義します。
            // elem_1 + elem_2 - elem_3 が0となるようにする　-> elem_3 = elem_1 + elem_2 を保証する
            vec![q_fib * (elem_1 + elem_2 - elem_3)]
        });
        // Config構造体のインスタンスを返す
        Self {
            elem_1,
            elem_2,
            elem_3,
            q_fib,
            instance,
        }
    }

let elem_1 = virtual_cells.query_advice(elem_1, Rotation::cur())について
- virtual_cellsは、現在のゲートの仮想的なセルを操作するためのオブジェクト
- query_adviceメソッドは、指定されたアドバイスカラムから値を取得するために使用される
- elem_1（メソッド呼び出しの第一引数）は、値を取得したいアドバイスカラムを指定する
- Rotation::cur()は、現在の計算ステップの値を問い合わせる(curはcurrentの略)

2. ゲートのレイアウト、セルとセル値の割り当て

このステップでは、チップのゲートの領域を割り当て、ゲートのセルを埋め、チップ機能を実装します。コードに移る前に必要な用語について理解します。

レイアウターとは？
どこにゲートを配置するかを決めてくれるものです。以前の説明で、てきとうにゲート割り当てると行列の列と行が大きくなり、証明が重くなってしまいます。それを最適化してくれるツールがlayouterというわけです。
リージョンとは？
リージョンは、レイアウターがグローバルにレイアウトを最適化し、ゲートのローカル位置（offset）を推論するために使用します。リージョンは、リージョン内の相対offset（位置）を保持するゲートの割り当てブロックです。
offsetとは？
下記のコードで示しているように、基本offsetは0で設定されます。layouter.assign_regionによって新しいRegionが開始されると、そのRegion内での操作（値の割り当てなど）にはこのoffsetが使用されます。offset = 0は、新しいRegion内での操作が最初の位置から始まることを意味します。

2-1: フィボナッチ回路の最初の行を割り当てる

fibonacci.rs

fn init<F: Field>(
        &self,
        mut layouter: impl Layouter<F>, // Layouter: 回路のレイアウトを管理するオブジェクト。複数の領域(Region)に分けて計算を配置する
        elem_1: Value<F>, // 最初のフィボナッチ数
        elem_2: Value<F>, // 二番目のフィボナッチ数
    ) -> Result<
        (
            AssignedCell<F, F>, // このメソッドからは、2番目と3番目のフィボナッチ数を表すAssignedCellを返す
            AssignedCell<F, F>, 
        ),
        Error,
    > {
        layouter.assign_region(
            || "init Fibonacci", // assign_regionメソッドは、与えられたクロージャ内で回路の一部を構成する。ここでは「init Fibonacci」という名前の領域を作成している。
            |mut region| { // Region: 回路の一部を構成するためのオブジェクト。ここで実際の値の割り当てが行われる
                let offset = 0; // offset: 現在の領域内での行の位置を指定する。0スタート
                // q_fib Selectorをこの領域で有効化 -> 計算が適用される
                self.q_fib.enable(&mut region, offset)?;

                // elem_1（最初のフィボナッチ数）をAdvice列に割り当てる。Advice列は、計算に使用される値をもつ
                region.assign_advice(|| "elem_1", self.elem_1, offset, || elem_1)?;

                // elem_2（二番目のフィボナッチ数）を同様にAdvice列に割り当てる
                let elem_2 = region.assign_advice(|| "elem_2", self.elem_2, offset, || elem_2)?;

                // elem_1 + elem_2の結果（次のフィボナッチ数）を計算し、elem_3としてAdvice列に割り当てる
                let elem_3 = elem_1 + elem_2.value_field().evaluate();
                let elem_3 = region.assign_advice(|| "elem_3", self.elem_3, offset, || elem_3)?;
                // 計算結果を含むAssignedCellを返す
                Ok((elem_2, elem_3))
            },
        )
    }

q_fibの有効化
selectorを有効にします。これにより、計算が適用される。
elem_1とelem_2の割り当て
最初の2つのフィボナッチ数を割り当てる
elem_3の計算と割り当て
最初の2数の和（elem_1 + elem_2）を計算し、次の要素（elem_3）として割り当てます。

Rustの話「region.assign_advice(|| "elem_1", self.elem_1, offset, || elem_1)?の書き方」

クロージャとスコープ

region.assign_advice(|| "elem_1", self.elem_1, offset, || elem_1)?
の部分では、elem_1の値を割り当てますが、このelem_1は関数の引数として渡されたelem_1の値を参照しています。ここでの|| elem_1は、クロージャ（匿名関数）の中で使われており、そのクロージャが呼び出される際に、外側のスコープから引数elem_1の値を捕捉して使用します。この操作は、elem_1の外側の値には影響を与えず、単にその値を使用してassign_adviceメソッドに渡すだけです。

let elem_2 = region.assign_advice(|| "elem_2", self.elem_2, offset, || elem_2)?
の場合も同様に、関数の引数として渡されたelem_2の値をクロージャが捕捉していますが、ここで重要なのはassign_adviceメソッドの呼び出し結果（AssignedCell<F, F>型）を新たにelem_2という名前の変数に束縛しているところです。このelem_2（AssignedCell<F, F>型）は、引数として渡されたelem_2（Value<F>型）とは異なる変数になります。Rustでは、このように同じ名前の変数を新たに定義することで、新しいスコープでのみ有効な新しい束縛を作成できます（シャドーイング）。

// elem_2の値を割り当て、AssignedCellを得る
let elem_2 = region.assign_advice(|| "elem_2", self.elem_2, offset, || elem_2)?;
// ^ このelem_2は新しいスコープでの新しい束縛（シャドーイングされたelem_2）

スコープとシャドーイング

関数の引数としてのelem_2
このelem_2は関数initのスコープ全体で有効です。この変数はValue<F>型で、初期のフィボナッチ数の一つを表します。
assign_advice内でのelem_2
region.assign_advice(...)を呼び出す際に、このメソッドの戻り値を新しいlet elem_2に束縛します。この操作により、元のelem_2（関数の引数として渡されたもの）を新しいAssignedCell<F, F>型のelem_2でシャドーイングします。この新しいelem_2は、assign_regionクロージャのスコープ内でのみ有効で、割り当てられたセルを参照します。

2-2 次の行を割り当てる

これがfor文でどんどん呼ばれていくイメージ。

fibonacci.rs

fn assign<F: Field>(
        &self,
        mut layouter: impl Layouter<F>,
        elem_2: &AssignedCell<F, F>, // 前の行でのelem_2、次の行の計算でelem_1として使用
        elem_3: &AssignedCell<F, F>, // 前の行でのelem_3、次の行の計算でelem_2として使用
    ) -> Result<
        (
            AssignedCell<F, F>, // 新しいelem_2、つまり更新された値
            AssignedCell<F, F>, // 新しいelem_3、計算された新しいフィボナッチ数
        ),
        Error,
    > {
        layouter.assign_region(
            || "next row", // 次のフィボナッチ数を計算する新しい領域
            |mut region| {
                let offset = 0; // 新しい領域の開始点、ここでは常に0から開始

                // q_fib Selectorを有効化し、フィボナッチ計算がこの領域に適用されるようにする
                self.q_fib.enable(&mut region, offset)?;

                // 前の行のelem_2を現在の行のelem_1としてコピー
                let elem_1 = elem_2.copy_advice(
                    || "copy elem_2 into current elem_1",
                    &mut region,
                    self.elem_1,
                    offset,
                )?;

                // 前の行のelem_3を現在の行のelem_2としてコピー
                let elem_2 = elem_3.copy_advice(
                    || "copy elem_3 into current elem_2",
                    &mut region,
                    self.elem_2,
                    offset,
                )?;
                
                // 新しいフィボナッチ数（elem_1 + elem_2）を計算し、elem_3として割り当て
                let elem_3 = elem_1.value_field().evaluate() + elem_2.value_field().evaluate();
                let elem_3 = region.assign_advice(
                    || "elem_3", // 新しく計算されたフィボナッチ数をelem_3に割り当て
                    self.elem_3,
                    offset,
                    || elem_3,
                )?;

                Ok((elem_2, elem_3)) // 新しいelem_2とelem_3の値を返す
            },
        )
    }

AssignedCell.copy_advice
セルの値を与えられたアドバイスセルにコピーし、並べ替え引数を用いてそれらが等しくなるように制約する。

2-3 出力（フィボナッチ数列の最後の項目）がinstance値と等しくなるように制約する

fibonacci.rs

     // 特定のフィボナッチ数を公開するメソッド
    fn expose_public<F: Field>(
        &self,
        mut layouter: impl Layouter<F>, // Layouterオブジェクト。回路のレイアウトを管理
        cell: &AssignedCell<F, F>, // 公開したいフィボナッチ数。
        row: usize, // 公開する行番号。
    ) -> Result<(), Error> {
        // Instance列に割り当てることで、特定のフィボナッチ数をパブリックに公開する
        layouter.constrain_instance(cell.cell(), self.instance, row)
    }

Layouter.constrain_instance
セルの値がインスタンス値と等しくなるように制約する
layouter.constrain_instance(cell.cell(), self.instance, row)
この行は、実際にパブリック入力を回路に公開する処理を行う。
- cell.cell()は、公開したい値が格納されているAssignedCellから実際のセル（位置情報を含む）を取得
- self.instanceは、この値が格納されるインスタンス列を指定
- rowは、この値をどの行に配置するかを指定

具体的な例

最終的なFibonacci数がelem_3カラムの第10行に計算されたとする

この値をパブリックに公開したい場合、cellはその計算結果が格納されたAssignedCellを表す
layouter.constrain_instance(cell.cell(), self.instance, row)を使用して、この値を特定のインスタンス列（例えば、公開入力を受け取るために予約された列）の指定された行（例えば、第0行）に公開する
これによって、回路の外部（例えば、検証者）は、第0行のインスタンス列を見ることで、計算が正しく行われたことを確認できる

3. 回路の構築

回路を構築していきます。2つの関数を準備します。コード記載後ほど説明します。

configure関数
synthesize関数

fibonacci.rs

// デフォルト値で初期化できるようにMyCircuit構造体にderiveマクロを適用
#[derive(Default)]

// MyCircuit構造体を定義。FはFieldトレイトを実装する型パラメータ
struct MyCircuit<F: Field> {
    elem_1: Value<F>, // 最初のフィボナッチ数
    elem_2: Value<F>, // 二番目のフィボナッチ数
}

// Fieldトレイトを実装する任意の型Fに対してCircuitトレイトを実装
impl<F: Field> Circuit<F> for MyCircuit<F> {
    type Config = Config; // 回路の設定をConfig型として指定
    type FloorPlanner = SimpleFloorPlanner; // 回路のレイアウト計画にSimpleFloorPlannerを使用

    // ウィットネス（証明に必要な秘密情報）を持たない新しいインスタンスを返す
    fn without_witnesses(&self) -> Self {
        Self::default() // デフォルト値で構造体を初期化
    }

    // 回路の構造を設定するためのメソッド。ConstraintSystemを介して回路を構成
    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        Self::Config::configure(meta) // Config構造体のconfigureメソッドを呼び出し
    }

    // 実際の計算を行い、回路にウィットネスを配置するメソッド
    fn synthesize(
        &self,
        config: Self::Config, // configureメソッドから得られた回路の設定
        mut layouter: impl Layouter<F>, // 回路のレイアウトを管理するLayouter
    ) -> Result<(), Error> {
        // 初期のフィボナッチ数（elem_1とelem_2）を設定
        let (mut elem_2, mut elem_3) =
            config.init(layouter.namespace(|| "init"), self.elem_1, self.elem_2)?;

        // フィボナッチ数列の次の数を計算し、回路に配置。繰り返しで数列を構築
        for _i in 3..11 { // 3から10までの数でループ
            let (_, new_elem_3) =
                config.assign(layouter.namespace(|| "next row"), &elem_2, &elem_3)?;

            // 更新された値を次の計算のためにセット
            elem_2 = elem_3;
            elem_3 = new_elem_3;
        }

        // 最終的なフィボナッチ数を公開情報として設定
        config.expose_public(layouter, &elem_3, 0)?;
        Ok(())
    }
}

configure 関数

configure関数は、回路の構造を設定するために使用されます。この関数内で、使用されるカラム（Advice列やInstance列など）、セレクタ、およびその他の回路の構成要素を定義します。具体的には、以下のような作業を行います。

Advice列の定義: 回路で使用する変数や計算結果を格納する列を定義します。
セレクタの定義: 特定の計算が行われるべきタイミングを制御するためにセレクタを定義します。
Instance列の定義: 外部からの入力を受け取るための列を定義します。これは、証明を検証する際に公開される情報を含みます。

synthesize 関数

synthesize関数は、具体的な計算を行い、その結果を回路内のセルに割り当てるために使用されます。この関数では、初期値、中間値、最終結果を計算し、それらを回路の適切な位置に配置します。

初期値の設定: config.initを用いて、フィボナッチ数列の最初の2つの数を設定します。
フィボナッチ数の計算: forループ内でconfig.assignを用いて、フィボナッチ数列の次の数を繰り返し計算し、それらを回路に割り当てます。
公開情報の設定: 最終的なフィボナッチ数を外部からアクセス可能な形で公開するためにconfig.expose_publicを呼び出します。

4. テストのための関数を準備

fibonacci.rs

// フィボナッチ数列のテスト関数を定義
#[test]
fn test_fib() {
    // MyCircuit構造体のインスタンスを作成。最初の2つのフィボナッチ数を1として初期化
    let circuit = MyCircuit {
        elem_1: Value::known(Fp::one()), // 最初のフィボナッチ数を1で初期化
        elem_2: Value::known(Fp::one()), // 二番目のフィボナッチ数も1で初期化
    };

    // テストケースで使用する公開入力を設定。ここではフィボナッチ数列の10番目の数である55を使用
    let instance = Fp::from(55);
    // 公開入力をベクタとして用意
    let mut public_input = vec![instance];

    // MockProverを使って、回路の検証を実行。k=5のZK-STARKを想定
    let prover = MockProver::run(5, &circuit, vec![public_input]).unwrap();

    // MockProverを用いて回路が正しく構成されているか検証
    prover.assert_satisfied();
}

`MockProver::run`は検証するツール

MockProver::runは回路をデバッグし、制約が満たされていることを検証するツールです。
MockProver::run(k: u32, circuit: &ConcreteCircuit, instance: Vec<Vec>)は、「多項式の最大次数である数k（行数を決める：2^k）」、「検証対象のcircuit」、「回路内のすべてのゲートのインスタンス値（パブリック入力）」を受け取ります。

検証

Prover.assert_satisfied()は、制約が満たされているかどうかを検証します。制約が満たされていない場合(制約が誤りの場合)、MockProverは正確な制約とともにエラーを出力します。

5. テストしてみる

まずはcloneしてきます

git clone https://github.com/Mameta29/halo2_fibonacci.git

プロジェクトに移動 & 依存パッケージインストール

cd halo2_fibonacci
cargo build

テスト実行

cargo test

成功実行結果

うまくパスできたことがわかります。それではフィボナッチ数列の項目を一つ増やすか減らしてみましょう。下記の部分を10ではない数字にしてみてください。

失敗実行結果(10を11に変更しました。)

6. 他にバグが起こる可能性を試してみる

制約を満たさない時のエラー

インスタンス値の変更
let instance = Fp::from(55)の55を別の値にしてみる
セルの代入の変更
フィボナッチ回路で、let elem_3 =elem_1.value_field().evaluate() +elem_2.value_field().evaluate() を let elem_3 = elem_1.value_field().evaluate() + elem_1.value_field().evaluate()のように加算する値を変更してみる
セル行の変更
config.expose_public(layouter, &elem_3, 0)? をconfig.expose_public(layouter, &elem_3, 1)?に変更してみる

逆に制約の欠落によるエラーを出力しない

MockProver::runは（特定の制約が欠落していても）正常にパスし、回路にバグを生じさせます。

インスタンス（パブリック入力）の値に関する制約が欠けている
config.expose_public(layouter, &elem_3, 0)を削除して、フィボナッチ回路のセルの初期値（elem_1）を2に変更してみる。

まとめ

Halo2についてまだまだわかっていないことは多いですが、一度手を動かしたり図を見ながら理解することで大枠は捉えることができるようになりました。
今度は自分で実際に1からコーディングして紹介できたらいいなと思います。

はじめに

Halo2とは

Halo2の部品

Columns(縦列)

制約とは

Rows(横行)

まず、有限体とは

行数の制限の理由

多項式補間

有限体のサイズと多項式の次数

行数と多項式の関係

Cells

Gate

Copy constraint

Lookup table

ルックアップテーブルの使用例

Chip

Gadget

Halo2で回路を書く方法

1. Chipの設定

2. ゲートのレイアウト、セルとセル値の割り当て

2-1: フィボナッチ回路の最初の行を割り当てる

クロージャとスコープ

スコープとシャドーイング

2-2 次の行を割り当てる

2-3 出力（フィボナッチ数列の最後の項目）がinstance値と等しくなるように制約する

具体的な例

3. 回路の構築

configure 関数

synthesize 関数

4. テストのための関数を準備

MockProver::runは検証するツール

検証

5. テストしてみる

6. 他にバグが起こる可能性を試してみる

制約を満たさない時のエラー

逆に制約の欠落によるエラーを出力しない

まとめ

Discussion

`MockProver::run`は検証するツール