Halo2简单示例

Halo2简介

[[Halo2]]是使用[[Rust]]语言开发，基于[[PLANK算法]]的，一款开源交互式([[STARKs]])，[[零知识证明(ZKP)]]的[[证明系统]]。

GitHub仓库地址：halo2

不同于普通的开发框架，Halo2中的功能开发称为电路(Circuit)开发，电路开发使用表格来设计并记录运算，并包含一系列的约束来验证运算结果并生成证明。

PLANK算术化

PLANK算术化的基本特点：

• 使用表格设计并记录运算，可以自定义使用多少列以及列的类型，列数越多成本越高
• 有限域(行数有限) ，一般是2的幂，如2^32
• 3种不同的列
      - Advice：隐私值(证明者计算过程整参数)
      - Fixed：公开常量(固定值)
      - Selector：选择器，用于决定是否在该行启用某种约束；
      - Instance：公开输入/输出
• 约束单元格之间关系：处完成计算外，还应包含包含多个规则约束来验证计算过程并生成证明
      - 自定义门约束(Custom Gate)：使用等于零的多项式来描述单元格关系，如 s_mul * a * b - r = 0。
      - 查找表约束(Lookup args) ：单元格值为，已知值Lookup列表中的一项
      - 固定值约束(Constance)：单元格值为固定值(常量)。

基础概念

• 芯片Chip：芯片一般用于实现单一指令(操作)。除具体的计算外，芯片还应实现加载隐私值(输入)、加载常量(输入)、公开结果(输出)等方法。
  • 芯片指令特性Chip Instructions
• 电路Circuit：由开发者开发的，包含一组功能的应用程序(证明系统)，证明者可以完成指定的计算，生成证明(Proof)，以供验证者验证。
  • 电路可以包含子电路SubCircuit、装置Gadgets(组合指令)、芯片Chip(单一操作)等。
  • 电路的配置和装置Gadget、芯片Chip相似，包含要使用的列数即类型，约束列表等。

简单示例

示例：证明计算 \(3a^2b^2=c\)
电路及芯片设计

实现乘法芯片

要实现该多项式计算，(假设)我们需要实现一个带有乘法功能的芯片FieldChip，当然，在零知识证明系统中，除了实现乘法计算外，还需要包含输入(加载私密值、加载常量)和输出(公开计算结果)等功能。

芯片指令特性

芯片指令特性是芯片要实现的抽象接口，例如，乘法芯片FieldChip要实现的特性如下：

trail NumbericInstructions<F: Field>: Chip<F> {
	type Num; // 定义数字类型
	// 加载证明者私密值
	fn load_private(&self, layouter: impl Layouter<F>, value: Value<F>) -> Result<Self::Num, Error>;
	// 加载常量，如3
	fn load_constant(&self, layouter: impl Layouter<F>, constant: F) -> Result<Self::Num, Error>;
	// 计算乘法
	fn mul(&self, layouter: impl Layouter<F>, a: Self::Num, b: Self::Num) -> Result<Self::Num, Error>;
	// 公开计算结果
	fn expose_public(&self, layouter: impl Layouter<F>, num: Self::Num, row: usize) -> Result<(), Error>;
}

芯片配置声明

芯片配置本质上是声明使用的列数量、列类型以及约束列表(单元格相互关系)，一般芯片还包含一个选择器Selector类，用于在某些行启用/关闭某些约束。
为节省成本，我们把相乘的结果直接放到下一行第一个，这样可以省一列，列配置如下：

芯片配置代码如下

struct FiledConfig {
	advice: [Column<Advice>; 2], // 存计算过程中的 a 和 b
	instance: Column<Instance>,  // 验证者-输入输出
	s_mul: Selector,  // 选择器-该行是否启用乘法约束
}

芯片功能实现

实现Halo2基本芯片特性

// 芯片结构声明
struct FiledChip<F: Field> {
	config: FiledConfig,
}

// 实现Halo2基本功能 config & loaded
impl<F: Field> Chip<F> for FiledChip<F>{
	type Config = FieldConfig:
	type Loaded = ();

	fn config(&self) -> &Self.Config { &self.config }
	fn loaded(&self) -. &Self::Loaded { &() }
}

实现芯片配置及约束

impl <F: Field> FieldChip<F> {
	// 构造方法
	fn construct(config: <Self as Chip<F>>::Config) -> Self { Self {config} }
	// 配置及创建约束
	fn configure(meta: &mut ConstraintSystem<F>, 
	            advice, instance: Column<Instance>, constant: Column<Fixed>) 
				-> <Self as Chip<F>>::Config {  
		meta.enable_equlity(instance);  // 启用相等检查
		meta.enable_constant(constant); // 启用常量检查
		for column in &advice { meta.enable_equlity(*column); }  // 启用相等检查
		
		let s_mul = meta.selector();  // 初始化选择器
		// 创建自定义门约束
		meta.create_gate("mul", |meta| {
		    let s_mul = meta.query_selector(s_mul);  // 获取选择器列数据
			let a = meta.query_advice(advice(0), Rotation::cur());  // 获取当前行-advice第1列数据
			let b = meta.query_advice(advice(1), Rotation::cur());  // 获取当前行-advice第2列数据
			let r = meta.query_advice(advice(1), Rotation::next()); // 获取下一行-advice第1列数据
			// 闭包-返回约束列表
		    vec![
			    s_mul * (a * b - r),
			]
		});
		
		FiledConfig { advice, instance, s_mul } // 返回芯片配置
	}
	
}

约束系统ConstraintSystem(即参数meta)常用方法

• enable_equlity()：启用相等检查
• enable_constant()：启用常量检查
• selector()：创建选择器
• query_advice: 查询Advice列对应单元格，本行(cur)或下一行(next)的值。

实现芯片指令特性

// 定义FieldChip所需要的数字类型
struct Number<F: Field> (AssignedCell<F, F>);

impl <F: Field> NumbericInstructions<F> for FieldChip<F> {
	type Num = Number<F>;
	// 加载私密数据-证明者在表中填数
	fn load_private(&self, layouter: impl Layouter<F>, value: Value<F>) -> Result<Self::Num, Error> {
		let config = self.config();
		layouter.assign_region(name: || "加载私密数据", 
							   assignment: |mut region| {
								   region.assign_advice(anotation: || "私密输入"
														column: config.advice[0], 
														offset: 0
														to: || value).map(op: Number)
							   })
	}
	// 加载常量数据
	fn load_constant(&self, layouter: impl Layouter<F>, constant: F) -> Result<Self::Num, Error> {
		let config = self.config();
		layouter.assign_region(name: || "加载常量数据", 
							   assignment: |mut region| {
								   region.assign_advice(anotation: || "常量值"
														column: config.advice[0], 
														offset: 0
														to: || constant).map(op: Number)
							   })
	}
	// 乘法计算
	fn mul(&self, layouter: impl Layouter<F>, a: Self::Num, b: Self::Num) -> Result<Self::Num, Error> {
		let config = self.config();
		layouter.assign_region(name: || "乘法", 
							   assignment: |mut region| {
								    config.s_mul.enable(&mut region, offset: 0)?;  // 启用s_mul选择器-出错则panic!
								    // 拷贝参数a的值到 advice第1列
								    a.0.copy_advice(|| "a", &mut region, config.advice[0], offset: 0)?;
								    // 拷贝参数b的值到 advice第2列
								    b.0.copy_advice(|| "b", &mut region, config.advice[1], offset: 0)?;
									// 计算 a * b
								    let r = a.0.value().copied() * b.0.value();
								
								    region.assign_advice(anotation: || "r"
														column: config.advice[0], 
														offset: 1 // 下一行
														to: || r).map(op: Number)
							   })
	
	}
	// 暴露(输出)结果
	fn expose_public(&self, layouter: impl Layouter<F>, num: Self::Num, row: usize) -> Result<(), Error> {
		let config = self.config();  
		
		layouter.constrain_instance(num.0.cell(), config.instance, row)
	}
}

.map(): Option内置方法，类似于match，用于处理多条件分支。

布局器Layouter、布局区域Region、及已分配值AssignedCell常用方法

• layouter.assign_region(name, assignment): 分配区域
• layouter.constrain_instance(cell, column, row): 约束instance输出列
• region.assign_advice(anotation, column, offset, to)：给Advice列单元格分配值
• assigned_cell.copy_advice(anotation, column, offset)：复制单元格值到advice列

构建电路

由于该示例比较简单，电路的配置和芯片的配置一样。

电路声明

struct MyCircuit<F: Field> {
	constant: F
	a: Value<F>,
	b: Value<F>
}

实现电路特性

impl<F: Field> Circuit<F> for MyCircuit<F> {
	type Config = FieldConfig;
	type FloorPlanner = SimleFloorPlanner;

	fn without_withnesses(&self) -> Self { Self::default() }
	// 电路配置-从meta约束系统取出数据, 生成Filed芯片配置
	fn configure(meta: &mut ConstaintSystem<F>) -> Self::Config {
		// 配置advice, instance 及 constant列
		let advice = [meta.advice_column(), meth,advice_column()]; // advice用两列
		let instance = meta.instance_column();
		let constant = meta.fixed_column();  // 常量是fied_column()

		FieldChip::config(meta, advice, instance, constant)  // 返回Field芯片配置
	}
	// 合成电路(电路运行入口)-实现多项式 a^2 * b^2 = c
	fn synthesize(&self, config: Self::Config, mut layouter: impl Layouter<F>) -> Result<(), Error> {
		let field_chip = FieldChip::<F>::construct(config) // 调用构造方法-生成Field芯片对象
		// 1.加载隐私数据
		//  1.1 从芯片中加载(填写到表)私密数据 a和b - 证明者在表格中填写a和b的值
		let a = field_chip.load_private(layouter.namespace(||"加载a", self.a));
		let b = field_chip.load_private(layouter.namespace(||"加载b", self.b));
		//  1.2 加载(填写到表)常量Field
		let constant = filed_chip.load_constant(layouter.namespace(||"加载常量Field"), self.constant)?;
		// 2. 乘法运算：使用芯片计算 a^2 * b^2 * 3 = c 可以转化成 (a*b)^2 * 3 = c，步骤更少, 成本更低
		let ab = field_chip.mul(layouter.namespace(|| "a*b"), a, b)?; // 计算 a*b
		let ab_ab = field_chip.mul(layouter.namespace(|| "ab*ab"), ab.clone(), ab)?;
		let c = fild_chip.mul(layouter.namespace(|| "constant * ab_ab"), constant, ab_ab)?;
		// 3. 暴露结果作为公开的电路输入值
		filed_chip.expose_public(layouter.namespace(||"暴露c"), c, 0)
	}
}

测试电路

use halo2_proofs::dev::MockProver;  
use halo2curves::pasta::Fp;

fn main(){
	// 测试 3 * a^2 * b^2 = c, a=4, b=5, c=1200
	let constant = Fp::from(3);
	let a = Fp::from(4);
	let b = Fp::from(5);

	// 使用私密数据-实例化电路对象
	let circuit = MyCircuit { cosntant, a: Value::known(a), b: Value::known};

	let k = 4; // 电路运行行数限制 2^k=16 行
	// 场景1: c=1200 成功
	let mut public_inputs = vec![Fp::from(1200)]; // 验证者-输入c=1200
	let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()].unwrap();)  // 生成模拟证明者
	assert_eq!(prover.verify(), Ok(()));  // 断言证明者可以验证成功
	// 场景2: c=1201 失败
	let mut public_inputs = vec![Fp::from(1201)]; // 验证者-输入c=1200
	let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()].unwrap();)  // 生成模拟证明者
	assert!(prover.verify().is_err());  // 断言证明者可以验证成功

完整代码：simple-example.rs

参考

• The halo2 Book
• halo2 - The halo2 Book 翻译
• Github-halo2 简单示例
• Halo2原理详解
• Zero Knowledge Proof — A Guide to Halo2 Source Code | by Trapdoor-Tech | Medium

本栏目推荐文章
• AntDesignBlazor示例——暗黑模式
• net8实现MediatR小示例C#
• YAML示例：nginx使用configmap配置并开启镜像
• C# MemCached学习笔记（三）-MemCached使用示例 (4个月前)
• YAML示例：创建单幅本nginx容器到指定节点及其service
• 线程安全问题的例子以及解决方案示例代码
• 【LeetCode 2989. 班级表现】T-SQL 动态sql编程示例
• DM7_SQL语言使用手册_第 2 章 手册中的示例说明
• 测试驱动的Spring Boot应用程序开发数据层示例
• 手册中的示例说明

示例 Halo2 Halo示例halo2 halo halo2 插件halo2 halo 11 表单 数据halo2 halo 模板halo2 halo 11 电路 技巧 中学halo2 版本halo halo1 halo2 halo2 halo halo moon-halo