理解 Lasso (二):稀疏向量与 Tensor 结构
- 作者: Yu Guo@Secbit(郭宇): Founder of Secbit, https://github.com/sec-bit
本文我们介绍一个基于 Sumcheck 的「稀疏多项式承诺方案」 Spark,这个方案最早出自 [Spartan] 证明系统。Spark 利用了稀疏向量的结构,可以大幅提升 Prover 的效率。Lasso 是在 Spark 的基础上的进一步拓展了对稀疏向量的处理。理解 Spark 是理解 Lasso 的关键。
普通的多项式承诺方案包括两个阶段,一个是承诺(Commitment)阶段,另一个是求值证明(Evaluation Argument)阶段。对于一个 MLE 多项式 ,求值点 ,以及运算结果 ,那么多项式承诺计算如下:
在求值证明阶段,Prover 可以向 Verifier 证明多项式 在某一个指定点 的运算结果为 :
Verifier 可以验证求值证明 :
如果 是一个稀疏的多项式,意味着它在 Boolean HyperCube 上的运算结果中多数的值都为零,那么我们能否利用这个特点,来设计一个针对稀疏多项式更高效的多项式承诺方案?
下面我们演示如何构造 Spark 多项式承诺。不过请记住,Spark 仍然需要基于一个普通的多项式承诺方案。换句话说,Spark 协议是将一个稀疏的 MLE 多项式的求值证明「归约」到多个普通的 MLE 多项式的求值证明,但后者这些 MLE 多项式的大小被大幅减少。
1. 稀疏向量的编码
我们考虑一个长度为 的稀疏向量 是一个 MLE 多项式 在 Boolean HyperCube 上的取值。记住 是一个稀疏的向量,其中除了 个非零元素之外其余值都为零。
先回忆下 MLE 多项式 的定义:
其中 是 MLE Lagrange 多项式。 定义如下:
如果直接使用一个普通的 MLE 多项式承诺方案来证明多项式求值, ,由于 是一个关于 项的求和公式,那么很显然 Prover 要至少花费 的计算量来遍历每一个求和项。
如果给定一个求值点 ,那么所有的 就构成了一个长度为 的向量,记为 :
别忘记稀疏向量 中仅有 个非零元素。举个例子,比如 ,即 向量中仅有四个非零值:
那么我们可以换用一种稠密的方式来表示 :
可以看出,向量 的稠密表示是一个长度仅为 的向量,其每一个元素为非零元素位置和非零元素值的二元组。我们再把上面二元组向量中的位置值单独记为 向量,把元组中非零的 记为 向量:
那么 的稠密表示可以写成:
然后 MLE 多项式 在 点的求值等式可以改写为:
注意上面这个等式中的求和项的个数仅为 。这意味着在给定 和 的情况下,我们成功地把 的求值运算从 降到了 。接下来的问题是 Prover 如何向 Verifier 证明求值过程用到了正确的 和 ?
对于一个多项式承诺方案,求值证明的公开输入里面包括了 向量的承诺,但是上面的求和式需要用到辅助向量 , 和 。其中 向量可以通过求值点 计算得到,其中每个元素为 ,而求值点 为公开输入,因此 Verifier 可以公开计算 向量或者公开验证。但 Verifier 并不能由 向量的承诺 来直接得到 和 这两个向量的信息。因此,我们需要把 和 的承诺来替代公开输入中的 向量的承诺。
换句话说,我们采用 和 来作为稀疏向量的 的编码,并利用一个普通的多项式承诺方案来计算 和 ,并把它们作为多项式求值证明的承诺(做为公开输入)。
2. 借助 的 Sumcheck
我们需要引入一个长度为 的辅助向量 ,它的每一个元素 :
这样 在 点的求值等式等价于下面的求和等式:
其中 是一个编码了 的 MLE 多项式, 是关于 的 MLE 多项式
如果 Prover 要证明上面的求和式,首先提供 的承诺 给 Verifier, 然后通过接下来的两部分来完成证明。
第一部分证明是 Prover 利用 Sumcheck 协议,把 的求值证明规约到下面的等式
其中 为 Sumcheck 协议对 个求和项进行折叠运算后的结果,而 为 Sumcheck 运行过程中 Verifier 产生的随机折叠因子。因为 Sumcheck 过程需要 轮,所以 的长度为 。
接下来 Prover 怎么证明上面的等式呢? 在求值证明之前,Verifier 已经从公开输入中得到了 , 两个向量的承诺,分别为 与 ,那么到这一步,Prover 和 Verifier 可以再利用普通的 MLE 多项式承诺方案来完成两个 Evaluation Argument,即分别证明: 与 的正确性,因为这两个向量长度均为 ,因此 Prover 产生这两个 Evaluation Argument 的计算量为 。最后 Verifier 验证 完成第一部分的证明。
第二部分证明是 Prover 证明 向量关于 , 与 的正确性,这就需要用到前文介绍过的 Offline Memory Checking 方法:Prover 只要证明 向量中的每一个元素都是从 向量(看成是内存)中读取出来的即可。这样 Prover 总的计算量为 。
3. 使用 Memory Checking 证明 的正确性
辅助向量 的正确性证明正是 Indexed Lookup Argument:
借助 Memory Checking 协议,我们把整个 向量(公开向量)看成是一段内存,Prover 证明 向量依次读取自内存 ,读取的位置为 。Prover 可以在 的计算量内完成上面的证明。
结合前文的定义,这里 为查询向量 , 为表格向量 ,而 为位置向量 。
但还有一个问题, 的承诺 怎么产生?向量元素 ,其定义中含有一个求值阶段才出现的公开输入 ,因此不能在 的承诺阶段中出现,也无法出现在 求值证明的公开输入中,一般情况多项式承诺方案的公开输入为 。如果由 Prover 计算 的话,那么 Prover 需要额外证明承诺的正确性。
幸运的是, 向量具有一定内部的结构,虽然它的长度为 ,但在给定 的情况下,它的插值多项式 可以在 的时间内进行求值计算,于是这样一来 Prover 可以不需要提供 ,而是让 Verifier 在验证过程中自行计算 在某一点的取值。我们观察下 的定义:
容易检验,对于任意的 ,
上面等式最右边是一个 项的乘积,其中每一个因子只需要常数次的加法和乘法。接下来我们稍微修改下前文中的 Offline Memory Checking 协议,把公开输入中的 替换为 ,并且让 Verifier 自行计算 的值。
Memory Checking 协议描述
公共输入:
- ,
- ,
- ,
第一轮
Prover 计算 , ,
Prover 计算并发送计数器的承诺 ,
第二轮
Verifier 发送挑战数
Prover 计算 , ,
Prover 计算 与
Prover 和 Verifier 利用基于 Sumcheck 的 Grand Product Argument 来证明下面的等式:
Grand Product Argument 证明最后会归约到对多个 MLE 多项式的求值证明,也就是对 ,,, 的求值证明。这些证明可以归约到 与 的求值证明。注意我们前面提到过, Verifier 不需要 的承诺求值证明,他可以自行计算 在任意点的求值。因为该多项式的求值计算量仅为 ,不影响 Verifier 的简洁性(Succinctness)。
进一步,任何计算过程仅为 的 MLE 多项式,Prover 也不必要一定计算它们的承诺,只要把计算任务交给 Verifier 就好。这样 Verifier 仍然保持 SNARK 的特性,同时也提高了 Prover 的效率,省去了计算承诺和产生求值证明的工作量。前提是,这一类 MLE 多项式需要具有一种特殊的内部结构,我们后文会把它们归到一个特殊的分类:MLE-Structured Vector。
对于 Prover 而言,仍然需要在证明过程中构造 ,通过动态规划算法,这需要 的计算量。
4. 求值证明协议细节
1. 承诺阶段:
Prover 要计算下面两个承诺:
- :稀疏向量 中的非零元素向量 的承诺
- : 中的所有非零元素在 中的位置向量 的承诺
2. 求值证明阶段:
公共输入:
- 多项式的承诺
- 求值点 ,以及运算结果
第一轮:
- Prover 计算 ,作为内存模拟
- Prover 计算 , 并发送承诺 ,作为 memory 顺序读取出的内容
第二轮:Prover 与 Verifier 执行 Offline Memory Checking 协议,证明
第三轮:Prover 与 Verifier 执行 Sumcheck 协议,证明
并把上面的求和等式归约到
其中 为 Verifier 在 Sumcheck 过程中发送的挑战向量。
第四轮:Prover 发送
- ,求值证明为
- ,求值证明为
验证: Verifier 验证 与 的有效性,并验证下面的等式:
性能分析
Prover 在 Memory-checking 协议中的性能开销为 ,因为内存的大小为 ,读取序列长度为 ;在 Sumcheck 协议中为 。因此 Prover 总的计算开销为 。
这样一个稀疏多项式承诺方案其实并不理想,因为 Prover 的计算量仍然与 线性有关。我们希望能够进一步减少 Prover 的计算量,这就需要进一步探索 的内部结构。
5. 向量 二维分解
为何 的求值计算量仅为 ? 因为向量 具有一种特殊的结构——Tensor Structure,也就是它可以拆分成多个短向量的 Tensor Product。简化起见,我们试着把 按照下面的方法拆分成两部分的乘积:
这里 和 是把 的二进制位拆分成相等的两段所表示的数值。举个例子,比如 是一个十进制数,它的二进制表示为 。我们可以把它拆成高二位与低二位,分别为 和 ,那么 。我们引入一个新的「拼接记号」, 表示 的二进制位为其高位和低位两个数的二进制位的拼接,按照 Big-endian 的方式。比如 。不难验证,拼接操作满足性质: 。
按照上面的分解方法,我们可以分解 为两个值的乘积:
对于长度为 的 向量中的所有元素 ,我们可以把其中每一个元素都按照相同拆分方式进行分解:
我们进而把这 16 个元素排成一个 的矩阵,每一个单元格的值 都等于它对应的行向量元素和列向量元素的乘积。
如果把上面表格的第一行的元素组成向量,记为 ,第一列记为 :
那么 向量看成是两个长度为 的向量的 Tensor Product:
回到我们关注的向量 ,其中每一个元素 也就可以看成是两个数值的乘积 ,其中 来自于 ,另一个 来自于 。
这相当于我们把整个 向量分解到了一个二维空间中,它的值等于横坐标和纵坐标值的乘积。那么我们可以继续采用 Offline Memory Checking 的思路来证明 的正确性,这次我们需要采用二维的 Offline Memory Checking 协议。更直白点说,我们需要采用两次 Offline Memory Checking 协议来证明 的正确性,每一个 对应到两个值的乘积,它们分别读取自 和 :
于是稀疏多项式 的求值等式可以改写为:
其中
其中 为非零元素 在二维矩阵中的行列坐标。这样我们可以把求值协议中的 Offline Memory Checking 子协议调用两次,但是内存的大小被大幅缩小到了 。看下前面的例子, , 向量中仅有四个非零值:
向量 为非零向量:
这时候,我们可以采用二维坐标 来标记 在 矩阵中的位置,标记矩阵中的行和列:
我们把其中行坐标向量记为 ,列坐标向量记为 ,那么 可以表示为
经过 Sumcheck 协议之后,上述等式可以被归约到:
然后 Prover 再提供三个 MLE 多项式在 点的取值, 的求值证明。
在这个二维的求值协议中,Prover 的计算开销就从上一节的 降低到了 。
下面我们给出完整的二维稀疏多项式承诺方案。
6. 二维稀疏多项式承诺 Spark
利用上面的思路,我们把稀疏向量 重新排列成一个 的二维矩阵 。为了排版清晰,我们引入符号 :
6.1. 承诺阶段:
Prover 要计算下面两个承诺:
- :稀疏向量 中的非零元素向量 的承诺
- : 中的所有非零元素在矩阵 中的行坐标构成的向量 的承诺
- : 中的所有非零元素在矩阵 中的列坐标构成的向量 的承诺
令 ,这个三元组承诺我们用符号 表示。
6.2. 求值证明阶段:
:
公共输入:
- 多项式的承诺
- 求值点 ,这个点可以拆分为两个子向量 ,其中
- 以及运算结果
第一轮:
- Prover 计算 ,作为 内存
- Prover 计算 ,作为 内存
- Prover 计算 与 , 作为分别从内存 与 读取出的内容,并发送承诺 与
第二轮:Prover 与 Verifier 执行两次 Offline Memory Checking 协议,证明 与 的正确性:
第三轮:Prover 与 Verifier 执行 Sumcheck 协议,证明下面的等式求和
并把求和等式归约到
其中 为 Verifier 在 Sumcheck 过程中发送的挑战向量,其长度为 。
第四轮:Prover 发送
- ,求值证明为
- ,求值证明为
- ,求值证明为
验证: Verifier 验证 , 与 的有效性,并验证下面的等式:
6.3. 性能分析
8. Tensor 结构 (TODO)
如果我们可以把 分解到二维空间,那么能否分解到更高维的空间?比如 的长度为 ,那么把它排成二维矩阵,比如 ,矩阵的长宽还是较大。如果把 重新排列成一个立方体,然后同样把 拆分成三段,这样我们可以把 Offline Memory Checking 的 Prover 开销进一步降低到 ,也就是 。这个分解的灵活性来源于 的结构特性,即 一个具有 Tensor Structure 的向量可以用不同的 Tensor Product 分解方式。理论上,我们可以把 分解成 个长度为 的短向量的 Tensor Product。不过实践中,我们只需要将其分解到 即可处理超长的向量。
例如当 时, 即可以排列成一个 的二维矩阵,也可以排列成 的四维矩阵:
我们可以根据 Tensor Product 逐步来推导下:
再利用上面的计算结果来计算
其实,许多常见的向量也具备 Tensor Structure,比如 :
7. 小结
本文介绍了 Tensor Structure 的概念,利用这个结构,我们可以把稀疏向量映射到一个二维空间中进行编码,然后我们基于这个结构,可以构造一个稀疏向量的多项式承诺方案。
References
- [Spartan] Spartan: Efficient and general-purpose zkSNARKs without trusted setup by Srinath Setty.
- [Lasso] Unlocking the lookup singularity with Lasso by Srinath Setty, Justin Thaler and Riad Wahby.
- [Jolt] Jolt: SNARKs for Virtual Machines via Lookups by Arasu Arun, Srinath Setty and Justin Thaler.
- [PLONK] PLONK: Permutations over Lagrange-bases for Oecumenical Noninteractive arguments of Knowledge by Ariel Gabizon, Zachary J. Williamson and Oana Ciobotaru.
- [Plookup] plookup: A simplified polynomial protocol for lookup tables by Ariel Gabizon and Zachary J. Williamson.
- [Caulk] Caulk: Lookup Arguments in Sublinear Time by Arantxa Zapico, Vitalik Buterin,Dmitry Khovratovich, Mary Maller, Anca Nitulescu and Mark Simkin
- [Caulk+] Caulk+: Table-independent lookup arguments by Jim Posen and Assimakis A. Kattis.
- [Baloo] Baloo: Nearly Optimal Lookup Arguments by Arantxa Zapico, Ariel Gabizon, Dmitry Khovratovich, Mary Maller and Carla Ràfols.
- [CQ] cq: Cached quotients for fast lookups by Liam Eagen, Dario Fiore and Ariel Gabizon.