This is an old version of this page. You can view the most recent version or browse the history.

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();
}