|
|
|
# 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 src="../../image/APIs_image_1.png" alt="img" style="zoom: 33%;" />
|
|
|
|
|
|
|
|
- 电路表整体由单元（`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<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`。
|
|
|
|
|
|
|
|
```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<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();
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
### 参考资料
|
|
|
|
|
|
|
|
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)
|
|
|
|
|
