halo2

Halo2电路基础

如需继续往下学习，需要掌握和了解关于电路的基础知识和Rust的基本语法。相关资料可以参考：

1. Lookup Gate

Lookup Gate的作用是证明一条（或多条）记录是否存在于一个公开的表中。这可能会有点像 Merkle Tree，如果我们把表格按行计算 hash，这些 hash 就可以产生一个 Merkle Root，然后通过 Merkle Path 就能证明一条记录是否存在表格中。但是这个方法（以及所有的 Vector Commitment 方案）存在以下两个缺点：

证明时会暴露记录在表格中的位置。
所产生的证明即 Merkle Path，可能会比较大，最坏情况是 O(dlogn)。

为了解决这些问题，在电路中实现lookup，Halo2给出了Halo2-lookup 方案。在此我们只需要简单理解Lookup的相关概念，需要深入学习如何写一个简单的电路，可以查看参考资料。

2. Circuits 电路结构

为了能够看懂core中各个电路的名词和概念，在此我们补充一些电路结构的基础知识。

The halo2 Book: The language that we use to express circuits for a particular proof system is called an arithmetization. Usually, an arithmetization will define circuits in terms of polynomial constraints on variables over a field. 2

电路表整体由单元（cell）、列（Column）和行（Row）组成。
相邻的cell、row 和 colum 的任意组合可以构成 region。
列又可以分为三种类型：advice，instance 和 selector。
- advice columns:包含了 private input & 电路运行中所需的中间变量，即witness,这部分只有prover知道
- instance columns：包含了 Prover/Verifier 之间共享的输入，通常用于公共输入 (public inputs)
- selector columns/fixed columns：包含在 key generation 阶段设置的 preprocessed values，可以视为是电路结构固定的一部分，也是可以被 pre-compute 的。比如查找表 Lookup table column。

Tips: 同一行可以支持若干种不同的约束, 比如三元三次, 或者三元二次, 可以通过 selector 来选择具体需要满足哪个约束。比如有 3 个 custom gate, 可以只满足其中一个就 OK , 或者满足其中的 2 个，非常灵活

3. 一个简单的示例

下面我们演示如何使用 Halo2 来实现一个基本的加法电路。实现电路一般按照以下三个流程进行：

1). 确定电路配置

首先，确定电路需要的列数和类型。在我们的加法电路例子中，我们需要三列 Advice 列来存储输入 a、输入 b 和输出 sum。

我们定义一个结构来存储电路的输入 a 和 b。

#[derive(Clone)]
struct MyCircuit {
    a: u64,
    b: u64,
}

然后，在 configure 方法中，我们定义电路需要的 Advice 列。

impl Circuit<()> for MyCircuit {
    type Config = (Column<Advice>, Column<Advice>, Column<Advice>);
    type FloorPlanner = SimpleFloorPlanner;

    fn configure(meta: &mut ConstraintSystem<()>) -> Self::Config {
        let col_a = meta.advice_column();
        let col_b = meta.advice_column();
        let col_sum = meta.advice_column();

        meta.enable_equality(col_a);
        meta.enable_equality(col_b);
        meta.enable_equality(col_sum);

        (col_a, col_b, col_sum)
    }
}

2). 确定电路需要的门

接下来，确定电路需要的门。门可以是标准的乘法门、加法门，或者是自定义门。如果需要特定功能，可以添加 lookup 表。

在我们的例子中，只需要一个简单的加法约束，即 sum = a + b。

在 configure 方法中，我们还需要定义电路的约束。这包括定义一个加法门，确保 sum = a + b。

impl Circuit<()> for MyCircuit {
    fn configure(meta: &mut ConstraintSystem<()>) -> Self::Config {
        // ... 省略前面的代码

        meta.create_gate("Addition", |meta| {
            let a = meta.query_advice(col_a, Rotation::cur());
            let b = meta.query_advice(col_b, Rotation::cur());
            let sum = meta.query_advice(col_sum, Rotation::cur());

            vec![sum - (a + b)]
        });

        (col_a, col_b, col_sum)
    }
}

3). 填充 witness

最后，根据电路所需的输入输出，填充 witness。witness 是电路计算过程中实际使用的值。假设我们电路的输入值 a 和 b 分别是 3 和 4，那么电路的 witness 就是：

a = 3
b = 4
sum = a + b = 7

电路的 witness 可以用一个表格来表示，表格的每一行代表一个电路的列，每一列代表一个电路的行。对于这个简单的电路，我们只需要一个行来表示计算过程。

	Column `a`	Column `b`	Column `sum`
Row 0	3	4	7

在我们的例子中，我们将 a、b 和 sum 分配到对应的列中。

在 synthesize 方法中，我们使用 Layouter 将实际的值（witness）分配到电路的列中。

impl Circuit<()> for MyCircuit {
    fn synthesize(&self, config: Self::Config, mut layouter: impl Layouter<()>) -> Result<(), Error> {
        let (col_a, col_b, col_sum) = config;

        layouter.assign_region(
            || "Assign values",
            |mut region| {
                region.assign_advice(|| "a", col_a, 0, || Ok(self.a.into()))?;
                region.assign_advice(|| "b", col_b, 0, || Ok(self.b.into()))?;
                region.assign_advice(|| "sum", col_sum, 0, || Ok((self.a + self.b).into()))?;
                Ok(())
            },
        )
    }
}

完整代码如下：

use halo2::circuit::{Layouter, SimpleFloorPlanner};
use halo2::plonk::{Advice, Circuit, Column, ConstraintSystem, Error};
use halo2::poly::Rotation;

#[derive(Clone)]
struct MyCircuit {
    a: u64,
    b: u64,
}

impl Circuit<()> for MyCircuit {
    type Config = (Column<Advice>, Column<Advice>, Column<Advice>);
    type FloorPlanner = SimpleFloorPlanner;

    fn configure(meta: &mut ConstraintSystem<()>) -> Self::Config {
        let col_a = meta.advice_column();
        let col_b = meta.advice_column();
        let col_sum = meta.advice_column();

        meta.enable_equality(col_a);
        meta.enable_equality(col_b);
        meta.enable_equality(col_sum);

        meta.create_gate("Addition", |meta| {
            let a = meta.query_advice(col_a, Rotation::cur());
            let b = meta.query_advice(col_b, Rotation::cur());
            let sum = meta.query_advice(col_sum, Rotation::cur());
            vec![sum - (a + b)]
        });
        (col_a, col_b, col_sum)
    }

    fn synthesize(&self, config: Self::Config, mut layouter: impl Layouter<()>) -> Result<(), Error> {
        let (col_a, col_b, col_sum) = config;

        layouter.assign_region(
            || "Assign values",
            |mut region| {
                region.assign_advice(|| "a", col_a, 0, || Ok(self.a.into()))?;
                region.assign_advice(|| "b", col_b, 0, || Ok(self.b.into()))?;
                region.assign_advice(|| "sum", col_sum, 0, || Ok((self.a + self.b).into()))?;
                Ok(())
            },
        )
    }
}

fn main() {
    let circuit = MyCircuit { a: 3, b: 4 };

    let prover = halo2::dev::MockProver::run(4, &circuit, vec![]).unwrap();
    prover.assert_satisfied();
}