Halo2 学习笔记——设计之Proving system之Lookup argument
Posted mutourend
tags:
篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了Halo2 学习笔记——设计之Proving system之Lookup argument相关的知识，希望对你有一定的参考价值。
1. 引言
Halo2中使用了lookup结束，支持lookups in arbitrary sets，且比Plookup更简单。
Halo2中，采用不同语言来描述PLONK概念：
- 1）将类似PLONK argument都想象成table，每一列对应a “wire”，将table中的entries称为“cells”。
- 2）将“selector polynomials”称为“fixed columns”，当a cell in a fixed column is being used to control whether a particular constraint is enable in that row时，则使用a “selector constraint”。
- 3）将仅由Prover掌握的其他polynomials统称为“advice columns”。
- 4）将“gate”称为rule，如：
A ( X ) ⋅ q A ( X ) + B ( X ) ⋅ q B ( X ) + A ( X ) ⋅ B ( X ) ⋅ q M ( X ) + C ( X ) ⋅ q C ( X ) = 0 A(X) \\cdot q_A(X) + B(X) \\cdot q_B(X) + A(X) \\cdot B(X) \\cdot q_M(X) + C(X) \\cdot q_C(X) = 0 A(X)⋅qA(X)+B(X)⋅qB(X)+A(X)⋅B(X)⋅qM(X)+C(X)⋅qC(X)=0 - 5）将 Z ( X ) Z(X) Z(X)多项式（the grand product argument polynomial for the permutation argument）称为"permutation product" column。
2. 不具有zero knowledge属性的subset argument
为了便于解释，接下来将介绍已忽略zero knowledge的简化版argument。
将lookups称为a “subset argument” over a table with
2
k
2^k
2k rows（从
0
0
0开始编号），具有columns
A
A
A 和
S
S
S。
subset argument的目的是：
- enforce A A A中的每个cell 等于 S S S中的某个cell。即意味着，允许 A A A中的多个cell 等于 S S S中的同一cell，而 S S S中的某个cell 可不等于 A A A中的任意cell。
注意：
- S S S可以是fixed，也可以不是。支持look up values in fixed tables 或 variable tables。若为variable tables，其中包含advice columns。
-
A
A
A和
S
S
S中可以具有重复的元素，即
A
A
A中的sets size 和（或）
S
S
S中的sets size 可不为
2
k
2^k
2k，可将
S
S
S以重复值扩展，将
A
A
A以
S
S
S中具有的ummy值扩展。
- 可增加“lookup selector”来控制 A A A column中的哪些元素将参与lookups。若a lookup is not selected，将需要修改下面permutation rule中的 A ( X ) A(X) A(X)，将其中的 A A A替换为 S 0 S_0 S0。
令 ℓ i \\ell_i ℓi为Lagrange basis polynomial，其evaluates to 1 1 1 at row i i i，and 0 0 0 otherwise。
总体流程为：
- 1）Prover已知
A
A
A和
S
S
S的permutation columns：
A
′
,
S
′
A',S'
A′,S′。
相应的permutation argument rule with product column Z Z Z为：
Z ( ω X ) ⋅ ( A ′ ( X ) + β ) ⋅ ( S ′ ( X ) + γ ) − Z ( X ) ⋅ ( A ( X ) + β ) ⋅ ( S ( X ) + γ ) = 0 Z(\\omega X) \\cdot (A'(X) + \\beta) \\cdot (S'(X) + \\gamma) - Z(X) \\cdot (A(X) + \\beta) \\cdot (S(X) + \\gamma) = 0 Z(ωX)⋅(A′(X)+β)⋅(S′(X)+γ)−Z(X)⋅(A(X)+β)⋅(S(X)+γ)=0
ℓ 0 ( X ) ⋅ ( 1 − Z ( X ) ) = 0 \\ell_0(X) \\cdot (1 - Z(X)) = 0 ℓ0(X)⋅(1−Z(X))=0
即，假设分子不为零，对于所有的 i ∈ [ 0 , 2 k ) i\\in[0, 2^k) i∈[0,2k)有：
Z i + 1 = Z i ⋅ ( A i + β ) ⋅ ( S i + γ ) ( A i ′ + β ) ⋅ ( S i ′ + γ ) Z_{i+1} = Z_i \\cdot \\frac{(A_i + \\beta) \\cdot (S_i + \\gamma)}{(A'_i + \\beta) \\cdot (S'_i + \\gamma)} Zi+1=Zi⋅(Ai′+β)⋅(Si′+γ)(Ai+β)⋅(Si+γ)
Z 2 k = Z 0 = 1 Z_{2^k} = Z_0 = 1 Z2k=Z0=1
以上，即为a version of the permutation argument，可证明 A ′ , S ′ A',S' A′,S′为permutation of A , S A,S A,S，但是无法确定准确的permutations。 β , γ \\beta,\\gamma β,γ为独立的challenges，可将2个permutation argument合并为1个，而不用担心会相互干扰。
这些permutations的主要目的是允许Prover对 A ′ , S ′ A',S' A′,S′进行排列：
- 1）将 A ′ A' A′ column中的所有cells 排列为 like-valued cells为vertically adjacent to each other。可借助某种sorting排序算法来实现，最终要求like-valued cells在 A ′ A' A′ column的consecutive rows，且 A ′ A' A′为a permutation of A A A。
- 2）The first row in a sequence of like values in
A
′
A'
A′ is the row that has the
corresponding value in S ′ . S'. S′. Apart from this constraint, S ′ S' S′ is any arbitrary
permutation of S . S. S.
可使用如下rule来enforce 要么 A i ′ = S i ′ A_i'=S_i' Ai′=Si′ 要么 A i ′ = A i − 1 ′ A_i'=A_{i-1}' Ai′=Ai−1′以上是关于Halo2 学习笔记——设计之Proving system之Lookup argument的主要内容，如果未能解决你的问题，请参考以下文章
Halo2 学习笔记——设计之Proving system之Permutation argument
Halo2 学习笔记——设计之Proving system之Lookup argument
Halo2 学习笔记——设计之Proving system之Circuit commitments
Halo2 学习笔记——设计之Proving system之Vanishing argument