Lookup Singularity

1. 引言

Lookup Singularity概念 由Barry WhiteHat在2022年11月在zkResearch论坛 Lookup Singularity中首次提出：

• 其主要目的是：让SNARK前端生成仅需做lookup的电路。
• Barry预测这样有很多好处，特别是对于可审计性 以及 形式化验证：
  • 更易于审计单个lookup argument和各种lookup tables，不再需要数千行的硬编码电路。
• 承认现有的lookup argument方案具有性能瓶颈 但 预测将得到改进：
  • 强调可能需要支持巨大table，如size为$2^{128}$的table。
• Lasso/Jolt可能可实现该愿景？

多年来，ZKP的核心元素为check：

• $A\ast B+D==C$

在构建整个电路过程中，重复运用该check。将这种表示的电路称为R1CS。

但是，对于某些任务，R1CS昂贵得令人望而却步，为此，引入了lookup arguments的大量使用。当前，很多ZKP使用lookup argument ＋ R1CS变种多项式承诺 来构建电路。

仅使用R1CS来构建电路存在一些障碍。为此，人们创建了一些hand tuned circuits，在这些hand tuned circuits中，同时包含了多项式约束和lookup arguments。这些hand tuned circuits是特定的，并不是很容易扩展。

1.1 多项式约束

多项式约束是复杂的。电路实现人员构建大量多项式方程式，整个电路定义为由多项式方程式组成的系统。
对这个“由多项式方程式组成的系统” 的solution，构成了a valid proof。很难对方程组的结果进行推理。目前的形式化验证工具无法求解素数域中的多项式方程。

1.2 Lookup argument

lookup argument为set membership check。lookup argument：

• 首次用于做高效的big integer arithmetic。
• 目前还用作VM的控制流
• 做某些不是snark-friendly的运算
• 并不是对所有运算都是更高效的
• 每个lookup会引入一定的prover开销
• 目前控制使用lookup argument的次数 的原因在于，其对Prover来说是昂贵的。

2. 为何Lookup arguments很好？

2.1 语言

当前的snark friendly语言对于新程序员来说是难学的。其使用了不同于之前范式的素数域和多项式约束。而仅使用lookup arguments的语言可能会更简单。当前的语言擅长做snarks定向计算，但当用于传统计算时要昂贵很多。

而仅有lookup的语言，将：

• 既擅长做snarks定向计算
• 也擅长做传统计算

2.2 安全审查

审计人员不再需要取对一组多项式方程式求解。lookup arguments推理起来要简单得多。

如：某电路具有一个ANDgate，有2个输入bit 变量，输出为这2个输入的AND运算结果。

多项式方案为：

(x)(x-1) = 0 
y(y-1) = 0 
x*y = out
return(out)

Lookup方案为：

out = get x,y from AND table
return(out)

其中AND lookup table为：

由此可知，Lookup方案要简单得多。因此，对于仅有lookup的电路，要更容易找出bug。

2.3 形式化验证

形式化验证工具需对一组多项式方程式求解。现有的形式化验证工具不擅长求解素数域中的多项式方程——这样会引入大量额外工作。

而仅使用lookup argument的话，则可使用现有的形式化验证工具，同时可能可探索一些其它方案。

lookup argument限制了电路中任意point的有限变量集合，使得可能的变量集合由$2^{254}$ 限制为了 $2$或$2^{16}$。这样甚至可支持做state space enumeration 来确认 “电路是正确的”。

2.4 信息论对比

为高效将程序描述为电路，需构建一个电路来将“某输入”映射为“正确的输出”。可将“电路”看成是“每个prover time second编码的信息”。这似乎是对比“实现电路的不同方式”的一种好角度。

多项式约束具有有限的degree：

• 因为degree会影响Prover time。
• degree会限制可编码的信息。

如degree为5的多项式可将5个输入值 映射为 5个输出值。除非增加degree，否则无法在该多项式中包含更多的值。

很多情况下，这样是ok的，因为是使用多项式约束的structure来做计算。因此，乘法运算对应为多项式运算$A\ast B==C$，而XOR运算不是，需要编码为keys to values。

Lookup argument可包含更多的信息。之前已限制lookup table size为$2^{28}$个元素。但近期研究成果表明，circuit size仅受限于可灵活完成的最大trusted setup——会限制table_size。
Baloo: Nearly Optimal Lookup Arguments中指出：

• 单个多项式约束中可包含约$5\ast 2^{254}$位信息。
• Lookup argument可包含$2^{254}\ast \text{table\_size}$

当使用多项式约束的structure时，多项式约束是很有用的。但随着更大尺寸的table变得可行，这种优势将消失。

3. 结论

若可仅使用lookup argument来高效定义电路，则将由更简单的工具和电路。
这样，lookup argument 将总是比 多项式约束 效率更高。

未来将关注构建以lookup为中心的ZKP工具。

4. 展望

未来工作：

• 比较现有电路的效率
• 构建仅有lookup的语言示例
• 对不同lookup argument效率做对比，并预测改进空间。
• 寻找lookup argument优于（和劣于）多项式约束的实例：
  • 寻找lookup argument 和 多项式约束 的worst case。
  • 对现有电路进行benchmark，比对效率：
    • lookup argument
    • lookup + polynomial constraints

参考资料

[1] Lookup Singularity
[2] The lookup singularity - how zero-knowledge proofs can be made simpler and easier to review.

Justin Thaler系列博客

• SNARK Design
• Rollup项目的SNARK景观
• SNARK原理示例
• SNARK性能及安全——Prover篇
• SNARK性能及安全——Verifier篇
• sum-check protocol in zkproof
• sum-check protocol深入研究
• Lasso、Jolt 以及 Lookup Singularity——Part 1
• Lasso、Jolt 以及 Lookup Singularity——Part 2

lookup系列博客

• PLOOKUP
• PLOOKUP代码解析
• Efficient polynomial commitment schemes for multiple points and polynomials学习笔记
• PLONK + PLOOKUP
• PlonKup: Reconciling PlonK with plookup
• PLONK: permutations over lagrange-bases for oecumenical noninteractive arguments of knowledge 学习笔记
• Plonk代码解析
• RapidUp: Multi-Domain Permutation Protocol for Lookup Tables学习笔记
• Lookup argument总览
• Halo2 学习笔记——设计之Proving system之Lookup argument（1）
• 多变量lookup argument
• cq：fast lookup argument
• Lookup Argument性能优化——Caulk
• 2023年 ZK Hack以及ZK Summit 亮点记
• Research Day 2023：Succinct ZKP最新进展
• Lasso、Jolt 以及 Lookup Singularity——Part 1
• Lasso、Jolt 以及 Lookup Singularity——Part 2