# Halo2电路基础 如需继续往下学习，需要掌握和了解关于电路的基础知识和Rust的基本语法。相关资料可以参考： - [PLONK Tutorials](https://learn.z2o-k7e.world/plonk-intro-cn/plonk-arithmetization.html) & [Lookup Gates @secbit](https://learn.z2o-k7e.world/plonk-intro-cn/plonk-lookup.html) - [Rust 圣经](https://course.rs/about-book.html) ### 1. Lookup Gate Lookup Gate的作用是证明一条（或多条）记录是否存在于一个公开的表中。这可能会有点像 Merkle Tree，如果我们把表格按行计算 hash，这些 hash 就可以产生一个 Merkle Root，然后通过 Merkle Path 就能证明一条记录是否存在表格中。但是这个方法（以及所有的 Vector Commitment 方案）存在以下两个缺点： 1. 证明时会暴露记录在表格中的位置。 2. 所产生的证明即 Merkle Path，可能会比较大，最坏情况是 *O*(*d*log*n*)。 为了解决这些问题，在电路中实现lookup，Halo2给出了[Halo2-lookup 方案](https://learn.z2o-k7e.world/plonk-intro-cn/plonk-lookup.html#halo2-lookup-方案)。在此我们只需要简单理解Lookup的相关概念，需要深入学习如何写一个简单的电路，可以查看参考资料。 ### 2. Circuits 电路结构 为了能够看懂core中各个电路的名词和概念，在此我们补充一些电路结构的基础知识。 > [The halo2 Book](https://zcash.github.io/halo2/concepts/proofs.html): 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](https://learn.z2o-k7e.world/halo2/chap-0/index.html#9) img - 电路表整体由单元（`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`。 ```rust #[derive(Clone)] struct MyCircuit { a: u64, b: u64, } ``` 然后，在 `configure` 方法中，我们定义电路需要的 `Advice` 列。 ```rust impl Circuit<()> for MyCircuit { type Config = (Column, Column, Column); 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`。 ```rust 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）分配到电路的列中。 ```rust 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(()) }, ) } } ``` 完整代码如下： ```rust 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, Column, Column); 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(); } ``` ### 参考资料 1. [zcash halo2 book](https://zcash.github.io/halo2/) / [github](https://github.com/zcash/halo2/blob/main/book/) 2. [zcash halo2 book 中文翻译](https://trapdoor-tech.github.io/halo2-book-chinese/) / [github](https://trapdoor-tech.github.io/halo2-book-chinese/) 3. [Halo2 基础](https://learn.z2o-k7e.world/halo2/halo2.html) 4. [R1CS约束](https://tlu.tarilabs.com/cryptography/rank-1) 5. [zkevm的设计和挑战](https://learnblockchain.cn/article/3108) 6. [以太坊相关操作码集合](https://cypherpunks-core.github.io/ethereumbook/13evm.html)