Halo2 学习笔记——设计之Proving system之Permutation argument

Posted 2021-10-14 mutourend

1. 引言

由于Halo2 circuit中的gate是operate “locally”（on cells in the current row or defined relative rows），因此，通常需要从 任意cell中复制a value 到 gate所在当前行中。通常以equality argument的方式来实现，用于约束source cell和destination cell中的值相同。

Halo2中通过构建a permutation来实现equality constraints，并在proof中使用a permutation argument来完成相应约束。

所谓permutation：
为a one-to-one and onto mapping of a set onto itself。

可将a permutation唯一分解为cycles组合（up to ordering of cycles, and rotation of each cycle）。

有时，也会用cycle notation来表示permutation。令$(abc)$表示a cycle，其中$a$ maps to $b$，$b$ maps to $c$，$c$ maps to $a$，可将此扩展为任意size的cycle。
将两个或多个cycles写在一起，表示相应的permutation组合。如$(ab)(cd)$表示a permutation：
$a$ maps to $b$，$b$ maps to $a$，$c$ maps to $d$，以及$d$ maps to $c$。

2. 构建permutation

2.1 目标

想要构建a permutation，其中，a equality-constraint set中的每个subset of variables可形成a cycle。
如，假设具有定义了如下equality constraints的circuit：

• $a\equiv b$
• $a\equiv c$
• $d\equiv e$

从而具有equality-constraint sets { a , b , c } \\{a,b,c\\} {a,b,c}和 { d , e } \\{d,e\\} {d,e}。即想构建permutation：
$(abc)(de)$
其中定义了mapping of $[a,b,c,d,e]$ to $[b,c,a,e,d]$。

2.2 算法

为了跟踪the set of cycles，需使用 disjoint set data structure，这种方式比较简单也易于实现，尽管不是最优的方案。

将current state 表示为：

• 1）一个数组 $\mathsf{m}\mathsf{a}\mathsf{p}\mathsf{p}\mathsf{i}\mathsf{n}\mathsf{g}$ 来表示permutation 本身。
• 2）一个辅助数组 $\mathsf{a}\mathsf{u}\mathsf{x}$ 来跟踪每个cycle的distinguished element。
• 3）另一个数组 $\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}$ 来跟踪每个cycle的size。

对于cycle $C$中的每个元素$c$，有$\mathsf{a}\mathsf{u}\mathsf{x}(x)$指向该元素$c\in C$。这可支持快速判断2个element $x,y$是否在同一cycle——check $\mathsf{a}\mathsf{u}\mathsf{x}(x)=\mathsf{a}\mathsf{u}\mathsf{x}(y)$是否成立。
同理，$\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(x))$ 为包含$x$的cycle size。（仅适于$\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(x))$，而不是$\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(x)$。）

以identity permutation为例：
对于所有的$x$，有 $\mathsf{m}\mathsf{a}\mathsf{p}\mathsf{p}\mathsf{i}\mathsf{n}\mathsf{g}(x)=x,\mathsf{a}\mathsf{u}\mathsf{x}(x)=x,\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(x)=1$。

为了增加an equality constraint $left\equiv right$：

• 1）check $left$ 和 $right$ 是否在同一cycle，即判断$\mathsf{a}\mathsf{u}\mathsf{x}(left)=\mathsf{a}\mathsf{u}\mathsf{x}(right)$是否成立，若成立，则直接返回。
• 2）若不成立，则$left$ 和 $right$分属不同的cycle。将 $left$ 标记为larger cycle, $right$ 标记为smaller cycle。若$\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(left))<\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(right))$，则将$left$ 和 $right$ 两者交换。
• 3）设置 $\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(left))=\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(left))+\mathsf{s}\mathsf{i}\mathsf{z}\mathsf{e}\mathsf{s}(\mathsf{a}\mathsf{u}\mathsf{x}(right))$。
• 4）跟随 $right$ （smaller）cycle的mapping around步骤，对于每一个元素$x$，设置$\mathsf{a}\mathsf{u}\mathsf{x}(x)=\mathsf{a}\mathsf{u}\mathsf{x}(left)$。
• 5）通过交换 $\mathsf{m}\mathsf{a}\mathsf{p}\mathsf{p}\mathsf{i}\mathsf{n}\mathsf{g}(left)$和$\mathsf{m}\mathsf{a}\mathsf{p}\mathsf{p}\mathsf{i}\mathsf{n}\mathsf{g}(right)$，将smaller cycle 拼接成 larger cycle。

比如，已知2个disjoint cycles $(ABCD)$ 和 $(EFGH)$：

A +---> B
^       +
|       |
+       v
D <---+ C       E +---> F
                ^       +
                |       |
                +       v
                H <---+ G

在增加constraint $B\equiv E$ 后，以上算法生成的cycle为：

A +---> B +-------------+
^                       |
|                       |
+                       v
D <---+ C <---+ E       F
                ^       +
                |       |
                +       v
                H <---+ G

若不在第1）步中验证$left$和$right$是否在同一cycle，则将end up undoing an equality constraint。以如下constraints为例：

• $a\equiv b$
• $b\equiv c$
• $c\equiv d$
• $b\equiv d$

若只使用上述算法中的步骤5）来add an equality constraint，则最终构造的cycle为$(ab)(cd)$，而不是正确的cycle $(abcd)$。

3. Argument specification

如需check a permutation of cells in $m$ columns，可使用Lagrange basis polynomial $v_0,\dots ,v_{m-1}$ 来表示。

可将$m$ columns中的每个cell 以a unique element of ${\mathbb{F}}^{\times }$来标记。

假设有permutation：
以上是关于Halo2 学习笔记——设计之Proving system之Permutation argument的主要内容，如果未能解决你的问题，请参考以下文章

Halo2 学习笔记——设计之Proving system之Permutation argument

Halo2 学习笔记——设计之Proving system之Lookup argument

Halo2 学习笔记——设计之Proving system之Circuit commitments

Halo2 学习笔记——设计之Proving system之Vanishing argument

Halo2 学习笔记——设计之Proving system之Multipoint opening argument

Halo2学习笔记——设计之Protocol Description