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 * 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 * 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*2^{254}$ 位信息。
Lookup argument可包含 $table_size 2^{254}*\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