526互联

翻译-我从Halo2电路开发中学到的一些小技巧

发布时间 2023-11-14 10:46:45作者: 韩志超

角色

flowchart LR 证明者-->|输入/输出/证明|验证者

?‍♂️证明者：提供 输入 / 输出 / 证明
?‍? 验证者：我不重新运行计算，但我确信输出计算正确

  1. 准备(开发)阶段
  • ?‍?开发者：定义常量
  • ?‍?开发者：发送密钥给 ?‍♂️证明者 及 ?‍?验证者
  1. 验证阶段
  • ?‍♂️证明者：填写计算过程
  • ?‍♂️证明者：生成证明
  • ?‍?验证者：验证证明

痛苦之处-电路开发和普通开发的不同

  • ?‍?普通开发：使用变量、分支、循环、函数来设计逻辑
  • ?‍?电路开发：使用表格，描述单元格之间的相互关系来定义约束
    • 算术化
    • 计算过程

游戏规则

有限域算术中的运算

  • 小于p的证书
  • 例如p=3
  • 则 2 + 2 = 1 (mod 3)
  • p通常是一个非常大的数，例如254bits

使用表格布局运算过程

![[Pasted image 20231110183106.png]]

  • 单元格：可以填写字段元素
  • 列：额外的列会增加 额外的证明/验证花费
  • 行：想用多少用多少，一般限制在2^18行以内。

列的类型

  • Advice： 引导(输入)列，用于?‍♂️证明者，在证明阶段填写隐私数据，仅?‍♂️证明者可见。
  • Fixed：常量列，?‍?开发者在开发阶段设置的固定值(常量)，?‍?验证者可见
  • Instance：实例(输出)列，用于?‍♂️证明者，在证明阶段填写的公开数据，?‍?验证者可见
  1. 开发阶段
  • ?‍?开发者设置Fixed固定列
  1. 证明阶段
  • ?‍♂️证明者填写计算过程
    • 填写 Advice列
    • 填写 Instance列
    • 生成证明
  1. 验证阶段
  • 验证Fixed列、Instance列(结果)和证明

约束：单元格中的那些值是有效的？

自定义门约束：在多项式中定义约束

![[Pasted image 20231110184701.png]]

  • 在门约束中定义的表达式中包含的Selctor选择器是一个Fixed列，例如0或1，来在该行禁用或启用
    该门约束。
  • 在门约束中，我们可以引用前面或后面的单元格，甚至20行以后的单元格，但是带来kzg opening的消耗。

一切都是多项式。

自定义门约束示例-斐波那契数列

示例代码：fibonacci.rs

可以使用4列
![[Pasted image 20231113142303.png]]

也可以使用3列
![[Pasted image 20231113142323.png]]

复制约束 / 相等检查

  • 复制约束绑定两个单元格，以便其分配的值必须是相同。
  • 最便宜的约束。尽可能多地使 。
  • 单元格位置在准备阶段已确定好，在证明解读不可更改。

规则：证明者可能是邪恶的

技巧

限制选项

限制单元格值的选项

  • 想要：单元格的值只能是 1，2， 3
  • 门表达式：(x-1)*(x-2)*(x-3) = 0

转化If-else

def foo(a: int, b: int, happy: bool):
	if happy:
		return a + b
	else:
		return a * b

门表达式：`happy * (a+b) + (1-happy) * (a*b) - output = 0`

转化For循环

def foo(n: int):
	r = 0
	for _ in range(n):
		r += 5
	return r

计算过程

![[Pasted image 20231113144656.png]]

  • 我们没有无限的行来存放n，因此我们必须限制n的最大可能值，例如5
  • 复制单元格
    • r0 == counst0: 已知的r初始值放到常量Fixed列里
    • r5 === out1： int/out列第一个为函数(验证者)输入，第二个为函数(验证者)输出，即最大行结果和输出值相等。

尝试添加一个证明者可见的Selector选择列

![[Pasted image 20231113145524.png]]

s：选择器列(Advice列)-仅证明者可见
r：步骤结果(Advice列)-仅证明者可见
in/out：输入/输出(Instance列)-验证者可见，仅使用两行

  • 门约束表达式：s * (r_next -r - 5) * (1-s)(r_next - r) = 0

即：
- if选择器为1时：r下一行结果 = r当前行+5
- else选择其为0时：下一行结果 = 当前行结果

但是这种有漏洞-如果selector=0的行不连续，例如：
![[Pasted image 20231113150216.png]]

状态转换技巧

stateDiagram-v2 direction LR [*] --> Add [*] --> Pad Add --> Add Add --> Pad Pad --> Pad Pad --> [*]

Add: 运算+5
Pad: 填充最终结果

门约束表达式：

  • s *(r_next-r-5)*(1-s)(r_next-r)=0

选择器s应是布尔类型

  • s * (1-s) == 0

如果当前选择器为0，则下一行选择器也必须为0

  • (1-s) s_next = 0

最后的点睛之笔：添加输入检查

![[Pasted image 20231113151325.png]]

  • 输入in连续整数或后续不变：s (in_next -in -1) + (1-s)(in_next-in)=0
  • 下一行结果为当前行+5或连续不变： s *(r_next-r-5)*(1-s)(r_next-r)=0
  • 选择器s应是布尔类型: s * (1-s) == 0
  • 如果当前选择器为0，则下一行选择器也必须为0: (1-s) s_next = 0

我们为什么要做这一切？

![[Pasted image 20231113152127.png]]

  • 在CPU中，我们有一组指令，这些指令需要可变的时间，在每个周期中，我们运行一条指令。
  • 当我们有一个if/else时，执行只遵循一条路径
  • 在算术电路中，我们没有循环！我们必须“展平”所有可能的执行路径，并同时“运行”它们，并通过乘以 0 来丢弃我们不需要的路径。

拿走不谢

  • 电路开发人员面临的挑战
    • 使用“计算跟踪”而不是执行：需要展平路径
    • 使用字段元素算术而不是位和字节：需要处理数学和方程式。
    • 使用验证思维：需要防止证明者作弊
  • 技巧
    • if-else 约束布尔值和 约束 s*(true path) +(1-s)*(false path)
    • 复杂循环：识别状态转换和设计约束。