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

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。令 ( a   b   c ) (a\ b\ c) (a b c)表示a cycle，其中 a a a maps to b b b， b b b maps to c c c， c c c maps to a a a，可将此扩展为任意size的cycle。 将两个或多个cycles写在一起，表示相应的permutation组合。如 ( a   b )   ( c   d ) (a\ b)\ (c\ d) (a b) (c d)表示a permutation： a a a maps to b b b， b b b maps to a a a， c c c maps to d d d，以及 d d d maps to c c c。

2. 构建permutation 2.1 目标

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

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

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

2.2 算法

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

将current state 表示为：

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

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

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

为了增加an equality constraint l e f t ≡ r i g h t \mathit{left} \equiv \mathit{right} left≡right：

• 1）check l e f t \mathit{left} left 和 r i g h t \mathit{right} right 是否在同一cycle，即判断 a u x ( l e f t ) = a u x ( r i g h t ) \mathsf{aux}(left)=\mathsf{aux}(right) aux(left)=aux(right)是否成立，若成立，则直接返回。
• 2）若不成立，则 l e f t \mathit{left} left 和 r i g h t \mathit{right} right分属不同的cycle。将 l e f t \mathit{left} left 标记为larger cycle, r i g h t \mathit{right} right 标记为smaller cycle。若 s i z e s ( a u x ( l e f t ) ) < s i z e s ( a u x ( r i g h t ) ) \mathsf{sizes}(\mathsf{aux}(\mathit{left})) < \mathsf{sizes}(\mathsf{aux}(\mathit{right})) sizes(aux(left)) B ^ + | | + v D F ^ + | | + v H B +-------------+ ^ | | | + v D