Sin7Y 团队全面解读——如何使用 Halo2 开发电路
source link: https://learnblockchain.cn/article/3031
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
使用 Halo2 开发电路
Halo2 是 ECC 公司在 Halo 的基础上，使用 Plonk 对 Halo 进行升级改造，充分利用了 Plonk 的特性，比如 custom gate，Plonkup 等，使得用 Halo2 开发零知识证明电路更加高效和方便。关于 Halo2 的原理详情，请参见我们之前的文章 Halo2 原理详解。
Halo2 广泛使用在目前众多的 zkEVM 的方案中，我们在这篇文章中，以一个简单的例子为例，来介绍如何进行 Halo2 的电路开发。
Halo2 电路系统
在开始讲解例子之前，先说说 Halo2 的证明系统。Halo2 电路是由表（matrix/table）定义，一般使用 matrix 的行（rows），列（columns），单元格（cells）来表示各种特殊不同的意义。
一个电路取决于如下的配置：
- 有限域 F，单元格元素都是 F 域元素；
- 和另一个 ZKP 电路系统 bellman 不同，Halo2 的电路系统用 advice 列代表 witness，instance 列代表 public input，fixed 列代表电路中固定的部分，Plonk 中引用出来的 lookup table 就是在 fixed 列中，selector 列是 fixed 列的辅助字段，用于确定在什么条件下激活门；
- 一部分可用于相等性约束的列；
- 一个多项式阶上限；
- 一系列多项式约束，这些都是在有限域 F 上的多变量多项式，每行的结果都必须是 0。多项式约束中的变量可以是当前行的某一列的单元格，或者相对于当前行的某一列的某一单元格；
- 一系列在输入表达式（如上述所述的多变量多项式）和 table 列上定义的查找表，这个就是 Plonk 里的 plonkup；
- 一系列用于指定两个单元格有相同值的相等性约束，熟悉 Plonk 的同学知道，这其实就是拷贝约束；
关于 Halo2 的电路系统，参见下图：
- a 代表的黄色的列，是 advice column
- i 代表的红色的列，是 instance column
- f 代表的蓝色的列，是 fixed column
- s 代表的紫色的列，是 selector column
对于不同的 proof，advice 和 instance column 不同，这个好理解，因为每次生成不同的 proof，witness 和 public input 基本上不同；而 fixed 和 selector column 都是和电路有关，跟输入无关。
Halo2 提供的工具
Mock Prover
用于调试电路的工具，可以在单元测试中，将电路中的每个约束都测试一遍。对 Halo2 的电路开发非常重要，我们在电路开发过程中，需要经常使用halo2::dev::MockProver来调试代码。如果某个约束不满足，则run报错，否则正常返回。
- 电路可视化工具
circuit_layout 可以用图表的形式展示电路的不同部分，如上面讲到的 advice/fixed/instance。
- 电路消耗检测工具
cost-model工具可以用来计算电路生成的 proof 大小，verify 花费的时间等。
Halo2 电路开发示例
如下，要开发一个电路， a, b 作为 private input，c 作为 public input，来证明得到：
1. 定义 instructions
因为电路可用于任意场景的证明描述，比如小的判断大小，大的一个程序执行的正确性。在这儿电路需要证明上述等式，就需要定义上述场景的电路，在这儿是乘法。以 a 的平方为例，其可以看成是 a 乘以 a。最外面则是 a 的平方乘以 b 的平方。
并且我们电路处理的是两个数字的相乘，所以这个 instructions 输入和输出都是 Num。该接口如下：
trait NumericInstructions<F: FieldExt>: Chip<F> {
/// Variable representing a number.
type Num;
/// Loads a number into the circuit as a private input.
fn load_private(&self, layouter: impl Layouter<F>, a: Option<F>) -> Result<Self::Num, Error>;
/// Loads a number into the circuit as a fixed constant.
fn load_constant(&self, layouter: impl Layouter<F>, constant: F) -> Result<Self::Num, Error>;
/// Returns `c = a * b`.
fn mul(
&self,
layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error>;
/// Exposes a number as a public input to the circuit.
fn expose_public(
&self,
layouter: impl Layouter<F>,
num: Self::Num,
row: usize,
) -> Result<(), Error>;
}
其中，Num 用于适配这个接口中处理的类型，load_private用于载入 witness，load_constant 用于载入常量，mul 用于计算两数相乘，expose_public用于设置 instance。
2. 定义 chip 实现
使用 Halo2 进行电路开发，大多数时候，不需要自己定义 instructions 和 chip，这些模块实现特别功能，属于基础设施，一般用 Halo2 提供的就足够了。但如果需要使用复杂的，而 Halo2 没有提供的，则需要自己实现，比如实现一个新兴的密码学算法。
如果要开发自定义 chip，则需要对 Halo2 的 chip trait 进行实现。
/// The chip that will implement our instructions! Chips store their own
/// config, as well as type markers if necessary.
struct FieldChip<F: FieldExt> {
config: FieldConfig,
_marker: PhantomData<F>,
}
impl<F: FieldExt> Chip<F> for FieldChip<F> {
type Config = FieldConfig;
type Loaded = ();
fn config(&self) -> &Self::Config {
&self.config
}
fn loaded(&self) -> &Self::Loaded {
&()
}
}
其中，config 函数返回自定义 chip 的配置，loaded 函数返回自定义 chip 的载入数据，此处不需要返回。
3. 配置 chip
一个 chip 的关键，都在其 config 中。如下，我们自定义的 chip 需要两个 advice 列，一个 instance 列，一个 selector 列，以及一个 constant。
truct FieldConfig {
/// For this chip, we will use two advice columns to implement our instructions.
/// These are also the columns through which we communicate with other parts of
/// the circuit.
advice: [Column<Advice>; 2],
/// This is the public input (instance) column.
instance: Column<Instance>,
// We need a selector to enable the multiplication gate, so that we aren't placing
// any constraints on cells where `NumericInstructions::mul` is not being used.
// This is important when building larger circuits, where columns are used by
// multiple sets of instructions.
s_mul: Selector,
/// The fixed column used to load constants.
constant: Column<Fixed>,
}
impl<F: FieldExt> FieldChip<F> {
fn construct(config: <Self as Chip<F>>::Config) -> Self {
Self {
config,
_marker: PhantomData,
}
}
fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
instance: Column<Instance>,
constant: Column<Fixed>,
) -> <Self as Chip<F>>::Config {
meta.enable_equality(instance.into());
meta.enable_constant(constant);
for column in &advice {
meta.enable_equality((*column).into());
}
let s_mul = meta.selector();
// Define our multiplication gate!
meta.create_gate("mul", |meta| {
// To implement multiplication, we need three advice cells and a selector
// cell. We arrange them like so:
//
// | a0 | a1 | s_mul |
// |-----|-----|-------|
// | lhs | rhs | s_mul |
// | out | | |
//
// Gates may refer to any relative offsets we want, but each distinct
// offset adds a cost to the proof. The most common offsets are 0 (the
// current row), 1 (the next row), and -1 (the previous row), for which
// `Rotation` has specific constructors.
let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
let out = meta.query_advice(advice[0], Rotation::next());
let s_mul = meta.query_selector(s_mul);
// Finally, we return the polynomial expressions that constrain this gate.
// For our multiplication gate, we only need a single polynomial constraint.
//
// The polynomial expressions returned from `create_gate` will be
// constrained by the proving system to equal zero. Our expression
// has the following properties:
// - When s_mul = 0, any value is allowed in lhs, rhs, and out.
// - When s_mul != 0, this constrains lhs * rhs = out.
vec![s_mul * (lhs * rhs - out)]
});
FieldConfig {
advice,
instance,
s_mul,
constant,
}
}
}
其中，最关键的函数 configure，enable_equality 用于进行传入参数的相等性检查，在create_gate 函数中，两个 adive（a，b）在同一行的不同列，而相乘的结果 advice 和 a 在同一列下一行，最后函数返回多项式约束：如果s_mul不为 0，则激活检查乘法约束，要结果是 0，则lhs * rhs - out须为 0，则lhs * rhs = out；如果s_mul 为 0，则没有激活检查乘法约束，后面任何数值都可以，我们不关心。
4. 实现 chip 接口
我们之前定义的 instructions 接口需要实现，我们定义 Number 的实现，是对有限域元素的封装。
#[derive(Clone)]
struct Number<F: FieldExt> {
cell: Cell,
value: Option<F>,
}
impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
type Num = Number<F>;
fn load_private(
&self,
mut layouter: impl Layouter<F>,
value: Option<F>,
) -> Result<Self::Num, Error> {
let config = self.config();
let mut num = None;
layouter.assign_region(
|| "load private",
|mut region| {
let cell = region.assign_advice(
|| "private input",
config.advice[0],
0,
|| value.ok_or(Error::SynthesisError),
)?;
num = Some(Number { cell, value });
Ok(())
},
)?;
Ok(num.unwrap())
}
fn load_constant(
&self,
mut layouter: impl Layouter<F>,
constant: F,
) -> Result<Self::Num, Error> {
let config = self.config();
let mut num = None;
layouter.assign_region(
|| "load constant",
|mut region| {
let cell = region.assign_advice_from_constant(
|| "constant value",
config.advice[0],
0,
constant,
)?;
num = Some(Number {
cell,
value: Some(constant),
});
Ok(())
},
)?;
Ok(num.unwrap())
}
fn mul(
&self,
mut layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error> {
let config = self.config();
let mut out = None;
layouter.assign_region(
|| "mul",
|mut region: Region<'_, F>| {
// We only want to use a single multiplication gate in this region,
// so we enable it at region offset 0; this means it will constrain
// cells at offsets 0 and 1.
config.s_mul.enable(&mut region, 0)?;
// The inputs we've been given could be located anywhere in the circuit,
// but we can only rely on relative offsets inside this region. So we
// assign new cells inside the region and constrain them to have the
// same values as the inputs.
let lhs = region.assign_advice(
|| "lhs",
config.advice[0],
0,
|| a.value.ok_or(Error::SynthesisError),
)?;
let rhs = region.assign_advice(
|| "rhs",
config.advice[1],
0,
|| b.value.ok_or(Error::SynthesisError),
)?;
region.constrain_equal(a.cell, lhs)?;
region.constrain_equal(b.cell, rhs)?;
// Now we can assign the multiplication result into the output position.
let value = a.value.and_then(|a| b.value.map(|b| a * b));
let cell = region.assign_advice(
|| "lhs * rhs",
config.advice[0],
1,
|| value.ok_or(Error::SynthesisError),
)?;
// Finally, we return a variable representing the output,
// to be used in another part of the circuit.
out = Some(Number { cell, value });
Ok(())
},
)?;
Ok(out.unwrap())
}
fn expose_public(
&self,
mut layouter: impl Layouter<F>,
num: Self::Num,
row: usize,
) -> Result<(), Error> {
let config = self.config();
layouter.constrain_instance(num.cell, config.instance, row)
}
}
其中，最关键的函数 mul 中，从 config 里取出两个 cell，检查和输入的 a，b 是否相等，再返回 a * b。需要注意的是，cell 的位置，除了 row 和 column，还可以通过相对位置 offset 来确定，一般 offset 就三种，0 代表当前位置，1 代表下一个位置，-1 代表上一个位置。
5. 构造电路
circuit trait 是开发电路的入口，我们需要定义自己的 circuit 结构，接入 witness 输入。
#[derive(Default)]
struct MyCircuit<F: FieldExt> {
constant: F,
a: Option<F>,
b: Option<F>,
}
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
// Since we are using a single chip for everything, we can just reuse its config.
type Config = FieldConfig;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
Self::default()
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// We create the two advice columns that FieldChip uses for I/O.
let advice = [meta.advice_column(), meta.advice_column()];
// We also need an instance column to store public inputs.
let instance = meta.instance_column();
// Create a fixed column to load constants.
let constant = meta.fixed_column();
FieldChip::configure(meta, advice, instance, constant)
}
fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let field_chip = FieldChip::<F>::construct(config);
// Load our private values into the circuit.
let a = field_chip.load_private(layouter.namespace(|| "load a"), self.a)?;
let b = field_chip.load_private(layouter.namespace(|| "load b"), self.b)?;
// Load the constant factor into the circuit.
let constant =
field_chip.load_constant(layouter.namespace(|| "load constant"), self.constant)?;
// We only have access to plain multiplication.
// We could implement our circuit as:
// asq = a*a
// bsq = b*b
// absq = asq*bsq
// c = constant*asq*bsq
//
// but it's more efficient to implement it as:
// ab = a*b
// absq = ab^2
// c = constant*absq
let ab = field_chip.mul(layouter.namespace(|| "a * b"), a, b)?;
let absq = field_chip.mul(layouter.namespace(|| "ab * ab"), ab.clone(), ab)?;
let c = field_chip.mul(layouter.namespace(|| "constant * absq"), constant, absq)?;
// Expose the result as a public input to the circuit.
field_chip.expose_public(layouter.namespace(|| "expose c"), c, 0)
}
}
之前定义的接口，在这儿都用到了。configure 创建 advice/instance/constant 的存储 column。synthesize 是使用自定义 chip，来获取输入 witness 和 constant，最后计算结果，并返回 public input。
其实对一般电路开发来说，只需要实现 circuit trait 就能满足绝大多数的场景，一些常见的功能 chip，Halo2 都已经实现了。
6. 测试电路
我们在工具章节中说到的 MockProver 和 CircuitLayout 可以派上用场了。
fn main() {
use halo2::{dev::MockProver, pasta::Fp};
// ANCHOR: test-circuit
// The number of rows in our circuit cannot exceed 2^k. Since our example
// circuit is very small, we can pick a very small value here.
let k = 4;
// Prepare the private and public inputs to the circuit!
let constant = Fp::from(7);
let a = Fp::from(2);
let b = Fp::from(3);
let c = constant * a.square() * b.square();
// Instantiate the circuit with the private inputs.
let circuit = MyCircuit {
constant,
a: Some(a),
b: Some(b),
};
// Arrange the public input. We expose the multiplication result in row 0
// of the instance column, so we position it there in our public inputs.
let mut public_inputs = vec![c];
// Given the correct public input, our circuit will verify.
let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
assert_eq!(prover.verify(), Ok(()));
// // If we try some other public input, the proof will fail!
public_inputs[0] += Fp::one();
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
assert!(prover.verify().is_err());
// ANCHOR_END: test-circuit
}
使用 MockProver 可以检查约束，查看其 verify 函数可知，检查了 selector，gate，lookup，permutation 几种约束。而使用下述代码，则可以输出电路 layout，展示电路的不同部分，感兴趣的自己去尝试，看看这个简单例子的电路可视化 layout 是什么样子的。
let root = BitMapBackend::new("simple-circuit-layout.png", (1024, 768)).into_drawing_area();
root.fill(&WHITE).unwrap();
let root = root
.titled("Simple Example Circuit Layout", ("sans-serif", 60))
.unwrap();
CircuitLayout::default().render(5, &circuit, &root).unwrap();
这个例子中，circuit，chip，instructions trait 以及其实现之间的关系如下图所示：
我们在本文中，介绍了 Halo2 电路开发的基本流程，希望对读者有所帮助。Halo2 电路设计和 bellman 方案颇为不同，有自己 row/column/cell/chip/region 等的新奇设计。Halo2 中的门，更多的使用了 Plonk 的门设计，和 R1CS 的门不同。在我们写这篇文章时，AZtec 团队又发布了 Plonk 的最新升级算法——Fflonk，新算法提升 verify 效率，节省 verify 时间，ECC 团队是否会将 Fflonk 结合到 Halo2 中，我们拭目以待。而关于 Fflonk 的原理分析，敬请期待我们后面的文章。
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK