作者: 白菜
标签: Sumcheck, IPA, GKR, Hyrax, VSM, Spice, Spark, Spartan
时间: 2023-10-06

Table of Content

• Table of Content
• Motivation
• Introduction
• VSM in Spice
  • Takeaways
• Memory Check for Spark
  • Problem
  • Resolution
    • Initialization
    • Operation
    • Verification
  • Arithmetic
  • Circuit
    • for $$\begin{gathered} widetildeH\_ \\ gamma\_1, \\ gamma2(Initrow) \end{gathered}$$ evaluation
    • for $$\begin{gathered} widetildeH\_ \\ gamma\_1, \\ gamma2(WSrow) \end{gathered}$$ evaluation
    • for $$\begin{gathered} widetildeH\_ \\ gamma\_1, \\ gamma2(Auditrow) \end{gathered}$$ evaluation
    • for $$\begin{gathered} widetildeH\_ \\ gamma\_1, \\ gamma2(RSrow) \end{gathered}$$ evaluation
• Spark Overview
  • Target of Spark
  • Technic in Spark
• Spartan Protolcol Overview
  • Round One
  • Round Two
  • Round Three
• One more thing
• Thanks
• References

Motivation

缘于folding，缘于NOVA，缘于Setty，了解到了Spartan，但当时并不认识它，所以才有了本篇及前两篇前置[3] 和[7]…… 

关于Spartan，在ZK领域可能时间上相对也有点儿远了，暂且不考虑它在某些方面的争议，它的一些思想其实已经影响到其它比较热门的方向了，比如当下的热点Lasso & Jolt，所以它的研究意义仍然很大，尤其是其中的Spark。

Introduction

本文是Spartan [4] research的终结篇，将重点囊括Spark 和 Spice [1]，前两篇[3] 和 [7] 是本篇的预备部分，如果对Sumcheck 不熟悉，也可以参考一下[6]。

Spark 是Spartan 整个协议的core part，Memory Check是Spark 的core part，而VSM又是Memory Check或者Spice的core part。本篇文章将从内向外延伸，读者尽管从感兴趣的地方切入即可。

VSM in Spice

VSM，全称Verifiable State Machine，这个概念源自Spice[1]。

它的一个intuitive 的理解就是：把任何一个storage 对象当作一个State Machine，在这个State Machine上的任何operation 导致其state 的transition 都可以生成相应的proof 给verifier 验证。这就是所谓的Verifiable State Machine。

以单个Query或者read operation为例，我们看看Spice 中的VSM 长什么样子：

关于Spice的其它细节这里不展开，大家可以参考原始资料Spice [1]。

Takeaways

• Spice 有两个drawback 或者特性：其一，批量验证，也就是n 个operation之后一起验证，成本会平摊到每个operation上，所以成本会很低，但会有时间上的delay；其二，如果验证不通过，是无法判断哪个operation 出的问题

• Storage 作为三方一个独立存在的个体，state 通常以key-value-timestamp的格式出现，它相比传统的key-value 的Storage 的区别就是加了一个可以表征State Machine的非常关键元素Timestamp

• Prover 自身维护两个set state $RS$ 和 $WS$，发送一个query/read operation 会更新本地的这两个set state $RS$ 和 $WS$，并update Storage的state $Audit$ ，发送一个write operation 会更新本地的state $WS$，并update Storage 的state $Audit$

• Verifier 拿着更新前的state $Init$，和更新后的state $Audit$，以及operaton 过程产生的中间state 或者proof $RS/WS$，进行最后的验证，验证通过说明返回的结果没有问题

Memory Check for Spark

Spark 中Memory Check 的核心思想源自Spice[1]，Spice 支持读、写操作的验证，而Spark 中只需要具备lookup 功能的验证，所以可以简单理解为read-only 版本的Spice。

验证query/lookup 的结果对与不对，上一节我们提到过，这里我们就以Spartan为背景，举个实例detail一下它的执行过程，可以回答大家可能比较关心的两个问题：1. memory check 究竟解决的是什么问题？2. 为什么它可以work？

Problem

假定有这么两个query 向量： $$\begin{gathered} add{r}_{row}=[0,0,1,1,1,2,3,3] \\ add{r}_{col}=[0,2,0,1,3,2,0,2] \end{gathered}$$

另外，假定： $$(r_x,r_y)=((2,3),(3,4))$$

以及相应的两个Storage 对象，或者叫lookup table $me{m}_{row}、me{m}_{col}$： $$\begin{array}{cccc}i& me{m}_{row}=\widetilde{eq}(i,r_x)& j& me{m}_{col}=\widetilde{eq}(j,r_y)\\ 0& (1-2)\cdot (1-3)=2& 0& (1-3)\cdot (1-4)=2\\ 1& (1-2)\cdot 3=2& 1& (1-3)\cdot 4=2\\ 2& 2\cdot (1-3)=1& 2& 3\cdot (1-4)=1\\ 3& 2\cdot 3=1& 3& 3\cdot 4=2\end{array}$$

query 的过程：给定$ro{w}_{addr}/co{l}_{addr}$ 向量中的某个元素值，返回相应table 中evaluation值。比如请求$add{r}_{row}[5]=2$，返回$\widetilde{eq}(2,r_x)=1$。

为了简化，以下实例我们均以query $add{r}_{row}=[0,0,1,1,1,2,3,3]$ 为例。如何证明它的返回结果 $e_{row}=[2,2,2,2,2,1,1,1]$ 是正确的呢？这里我们detail 一下上一节中VSM 的逻辑。

Resolution

Initialization

lookup table $me{m}_{row}$ 最开始的State： $$Ini{t}_{row}=[(0,2,0),(1,2,0),(2,1,0),(3,1,0)]$$

Operation

批量query $add{r}_{row}=[0,0,1,1,1,2,3,3]$ 之后，$me{m}_{row}$ 的State 变成了： $$Audi{t}_{row}=[(0,2,2),(1,2,3),(2,1,1),(3,1,2)]$$

批量query $add{r}_{row}=[0,0,1,1,1,2,3,3]$ 之后，prover 这边维护的两个中间State 或者proof 为： $$\begin{gathered} R{S}_{row}=[(0,2,0),(0,2,1),(1,2,0),(1,2,1),(1,2,2),(2,1,0),(3,1,0),(3,1,1)] \\ W{S}_{row}=[(0,2,1),(0,2,2),(1,2,1),(1,2,2),(1,2,3),(2,1,1),(3,1,1),(3,1,2)] \end{gathered}$$

Verification

批量query 之前，verifier 请求拿到$me{m}_{row}$ 的初始State $Ini{t}_{row}$；批量query $add{r}_{row}=[0,0,1,1,1,2,3,3]$ 之后，verifier 请求得到$me{m}_{row}$ 的最新State $Audi{t}_{row}$，再结合prover 传递过来的proof $R{S}_{row}/W{S}_{row}$ 进行最后的验证： $$Ini{t}_{row}\cup W{S}_{row}\stackrel{?}{=}Audi{t}_{row}\cup R{S}_{row}$$

接下来的问题是，如何把上面的计算过程算术化？

Arithmetic

$$Ini{t}_{row}\cup W{S}_{row}\stackrel{?}{=}Audi{t}_{row}\cup R{S}_{row}$$

这个等式本质是要判定两个set 是否相等？也就是说是一个permutaion的问题，自然就会联想到plonk 里lookup contrain用到的grand-product 的逻辑，也就是说： $$\begin{gathered} [(0,2,0),(1,2,0),(2,1,0),(3,1,0)]\cup [(0,2,1),(0,2,2),(1,2,1),(1,2,2),(1,2,3),(2,1,1),(3,1,1),(3,1,2)] \\ \stackrel{?}{=} \\ [(0,2,2),(1,2,3),(2,1,1),(3,1,2)]\cup [(0,2,0),(0,2,1),(1,2,0),(1,2,1),(1,2,2),(2,1,0),(3,1,0),(3,1,1)] \end{gathered}$$

演变成了： $$\begin{gathered} (0,2,0)\cdot (1,2,0)\cdot (2,1,0)\cdot (3,1,0)\cdot (0,2,1)\cdot (0,2,2)\cdot (1,2,1)\cdot (1,2,2)\cdot (1,2,3)\cdot (2,1,1)\cdot (3,1,1)\cdot (3,1,2) \\ \stackrel{?}{=} \\ (0,2,2)\cdot (1,2,3)\cdot (2,1,1)\cdot (3,1,2)\cdot (0,2,0)\cdot (0,2,1)\cdot (1,2,0)\cdot (1,2,1)\cdot (1,2,2)\cdot (2,1,0)\cdot (3,1,0)\cdot (3,1,1) \end{gathered}$$

很显明三元组的元素是无法直接相乘的，引入两个challenge factor ${\gamma }_1、{\gamma }_2$把三元组的元素合成一个field： $$H_{{\gamma }_1,{\gamma }_2}(a,v,t)=(a\cdot {\gamma }_1^2+v\cdot {\gamma }_1+t)-{\gamma }_2$$

因此上面的等式就变成了： $$\begin{gathered} H_{{\gamma }_1,{\gamma }_2}(0,2,0)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,0)\cdot H_{{\gamma }_1,{\gamma }_2}(2,1,0)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,0)\cdot H_{{\gamma }_1,{\gamma }_2}(0,2,1)\cdot H_{{\gamma }_1,{\gamma }_2}(0,2,2)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,1)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,2)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,3)\cdot H_{{\gamma }_1,{\gamma }_2}(2,1,1)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,1)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,2) \\ \stackrel{?}{=} \\ {H}_{{\gamma }_1,{\gamma }_2}(0,2,2)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,3)\cdot H_{{\gamma }_1,{\gamma }_2}(2,1,1)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,2)\cdot H_{{\gamma }_1,{\gamma }_2}(0,2,0)\cdot H_{{\gamma }_1,{\gamma }_2}(0,2,1)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,0)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,1)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,2)\cdot H_{{\gamma }_1,{\gamma }_2}(2,1,0)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,0)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,1) \end{gathered}$$

接下来的问题是，如何把上面的算术逻辑放在电路里，以便通过某个或者某几个协议来完成它的验证？

Circuit

我们把上面的等式grand-product 拆分成四个部分： $$\begin{array}{rl}{H}_{{\gamma }_1,{\gamma }_2}(Ini{t}_{row})& =H_{{\gamma }_1,{\gamma }_2}(0,2,0)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,0)\cdot H_{{\gamma }_1,{\gamma }_2}(2,1,0)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,0)\\ & \\ H_{{\gamma }_1,{\gamma }_2}(W{S}_{row})& =H_{{\gamma }_1,{\gamma }_2}(0,2,1)\cdot H_{{\gamma }_1,{\gamma }_2}(0,2,2)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,1)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,2)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,3)\cdot H_{{\gamma }_1,{\gamma }_2}(2,1,1)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,1)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,2)\\ & \\ H_{{\gamma }_1,{\gamma }_2}(Audi{t}_{row})& =H_{{\gamma }_1,{\gamma }_2}(0,2,2)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,3)\cdot H_{{\gamma }_1,{\gamma }_2}(2,1,1)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,2)\\ & \\ H_{{\gamma }_1,{\gamma }_2}(R{S}_{row})& =H_{{\gamma }_1,{\gamma }_2}(0,2,0)\cdot H_{{\gamma }_1,{\gamma }_2}(0,2,1)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,0)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,1)\cdot H_{{\gamma }_1,{\gamma }_2}(1,2,2)\cdot H_{{\gamma }_1,{\gamma }_2}(2,1,0)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,0)\cdot H_{{\gamma }_1,{\gamma }_2}(3,1,1)\end{array}$$

假定这四组向量都是witness，用GKR-like layered circuit 来把这四个grand-product 的计算trace 给描述出来，通过Hyrax [2] 协议来完成grand-product 的验证，最后验证四个grand-product 的结果是否满足等式即可： $$H_{{\gamma }_1,{\gamma }_2}(Ini{t}_{row})\cdot H_{{\gamma }_1,{\gamma }_2}(W{S}_{row})\stackrel{?}{=}{H}_{{\gamma }_1,{\gamma }_2}(Audi{t}_{row})\cdot H_{{\gamma }_1,{\gamma }_2}(R{S}_{row})$$

我们用图直观感受一下这四个电路长什么样子？

Circuit for $Ini{t}_{row}$:

Circuit for $W{S}_{row}$:

Circuit for $Audi{t}_{row}$:

Circuit for $R{S}_{row}$:

熟悉Hyrax 协议的应该知道，Hyrax协议是由多个Sumcheck 协议与一个IPA协议组成 [3]。Hyrax 的最后需要计算tree 的叶子节点，也就是witness向量，的MLE 多项式在某个opening $r$ 上的evaluation，它是通过一个IPA协议来完成的。

也就是说，在这里我们分别需要通过IPA协议完成四个evaluation 的验证： $$\begin{array}{r}\begin{array}{ll}\widetilde{H_{{\gamma }_1,{\gamma }_2}(Ini{t}_{row}}(r))& \stackrel{?}{=}{v}_{Init}\\ & \\ \widetilde{H_{{\gamma }_1,{\gamma }_2}(W{S}_{row}}(r))& \stackrel{?}{=}{v}_{WS}\\ & \\ \widetilde{H_{{\gamma }_1,{\gamma }_2}(Audi{t}_{row}}(r))& \stackrel{?}{=}{v}_{Audit}\\ & \\ \widetilde{H_{{\gamma }_1,{\gamma }_2}(R{S}_{row}}(r))& \stackrel{?}{=}{v}_{RS}\end{array}\}\end{array}$$

等式右边的四个evaluation值是通过Sumcheck 协议reduce 后拿到的。

$H_{{\gamma }_1,{\gamma }_2}(a,v,t)$ 是由相应的三元组$a、v、t$，即$addr、val、ts$ 组成。所以上面的四个evaluation 需要进行再次拆解。

for $\widetilde{H_{{\gamma }_1,{\gamma }_2}(Ini{t}_{row})}$ evaluation

$$\begin{array}{rl}\widetilde{add{r}_{Init}(r_{addr})}& \stackrel{?}{=}{v}_{Init}.v_{addr}\\ \widetilde{me{m}_{Init}(r_{mem})}& \stackrel{?}{=}{v}_{Init}.v_{mem}\\ \widetilde{t{s}_{Init}(r_{ts})}& \stackrel{?}{=}{v}_{Init}.v_{ts}\end{array}$$

三个dense 向量或者witness 为：

$$\begin{array}{ccc}addr& mem& t{s}_{init}\\ 0& 2& 0\\ 1& 2& 0\\ 2& 1& 0\\ 3& 1& 0\end{array}$$

用3个IPA协议去验证以上三个MLE 的evaluation值是否合法。

for $\widetilde{H_{{\gamma }_1,{\gamma }_2}(W{S}_{row})}$ evaluation

$$\begin{array}{rl}\widetilde{add{r}_{WS}(r_{addr})}& \stackrel{?}{=}{v}_{WS}.v_{addr}\\ \widetilde{e_{WS}(r_e)}& \stackrel{?}{=}{v}_{WS}.v_e\\ \widetilde{t{s}_{WS}(r_{ts})}& \stackrel{?}{=}{v}_{WS}.v_{ts}\end{array}$$

三个dense 向量或者witness 为： $$\begin{array}{ccc}add{r}_{WS}& e_{WS}& t{s}_{WS}\\ 0& 2& 1\\ 0& 2& 2\\ 1& 2& 1\\ 1& 2& 2\\ 1& 2& 3\\ 2& 1& 1\\ 3& 1& 1\\ 3& 1& 2\end{array}$$

用3个IPA协议去验证以上三个MLE 的evaluation值是否合法。

for $\widetilde{H_{{\gamma }_1,{\gamma }_2}(Audi{t}_{row})}$ evaluation

$$\begin{array}{rl}\widetilde{add{r}_{Audit}(r_{addr})}& \stackrel{?}{=}{v}_{Audit}.v_{addr}\\ \widetilde{me{m}_{Audit}(r_{mem})}& \stackrel{?}{=}{v}_{Audit}.v_{mem}\\ \widetilde{t{s}_{Audit}(r_{ts})}& \stackrel{?}{=}{v}_{Audit}.v_{ts}\end{array}$$

三个dense 向量或者witness 为：

$$\begin{array}{ccc}addr& mem& t{s}_{init}\\ 0& 2& 2\\ 1& 2& 3\\ 2& 1& 1\\ 3& 1& 2\end{array}$$

用3个IPA协议去验证以上三个MLE 的evaluation值是否合法。

for $\widetilde{H_{{\gamma }_1,{\gamma }_2}(R{S}_{row})}$ evaluation

$$\begin{array}{rl}\widetilde{add{r}_{RS}(r_{addr})}& \stackrel{?}{=}{v}_{RS}.v_{addr}\\ \widetilde{e_{RS}(r_e)}& \stackrel{?}{=}{v}_{RS}.v_e\\ \widetilde{t{s}_{RS}(r_{ts})}& \stackrel{?}{=}{v}_{RS}.v_{ts}\end{array}$$

三个dense 向量或者witness 为： $$\begin{array}{ccc}add{r}_{WS}& e_{WS}& t{s}_{WS}\\ 0& 2& 0\\ 0& 2& 1\\ 1& 2& 0\\ 1& 2& 1\\ 1& 2& 2\\ 2& 1& 0\\ 3& 1& 0\\ 3& 1& 1\end{array}$$

用3个IPA协议去验证以上三个MLE 的evaluation值是否合法。

到此为止，Spark 中memory check 的逻辑就完整了！关于Spark 的应用在Brakedown [5]中也有应用，感兴趣的话也可以参考一下。

最后我们再revisit 一下之前提到的两个问题：

接下来我们就可以非常轻松的review 一下Spark 了。

Spark Overview

Target of Spark

以$O(n)$ 的时间复杂度完成Sparse Matrix Polynomial 的evaluation。

比如，有一个Sparse Matrix: $$M=\left[\begin{array}{c}1,0,2,0\\ 2,4,0,3\\ 0,0,1,0\\ 3,0,4,0\end{array}\right]$$

其中涉及到的常量： $$\begin{array}{rl}& m=4\\ & n=8\\ & s=\log m=2\\ & u=2s=4\end{array}$$

$m$ 代表矩阵的行数/列数，$n$ 代表矩阵中non-zero 元素的个数，$u$ 代表matrix dense MLE中的变量个数。

上面这个matrix 的dense MLE 可以表示为： $$\tilde{M}(r_x,r_y)=\sum _{x\in \{0,1{\}}^s,y\in \{0,1{\}}^s}M(x,y)\cdot \widetilde{eq}(x,r_x)\cdot \widetilde{eq}(y,r_y)$$

因为是dense 的表达，所以默认$M(x,y)$是按顺序遍历的，一共有$m^2\cdot 2s=m^2\cdot 2\log m$ 次乘法运算，即时间复杂度为$O(m^2\cdot \log m)$，成本随着$m$ 的增大，会呈现asymptotic 式的增长。在Spartan中，$m$ 又代表R1CS 的gate 数量，这种特征就会体现得更明显。

Spark 把sparse matrix 的evaluation代理给prover，并通过memory check 的消除这种asymptotic，把它的时间复杂度控制在$O(n)$，跟R1CS 的gate 数量无关了，仅仅跟Sparse 的呈度有关。因此，matrix 越稀疏，它的优势就体现得越明显。即 $n\ll m^2$

Technic in Spark

首先，Spark不再用矩阵表达了，而是换作三个向量来表达： $$\begin{array}{rl}add{r}_{row}& =[0,0,1,1,1,2,3,3]\\ add{r}_{col}& =[0,2,0,1,3,2,0,2]\\ val& =[1,2,2,4,3,1,3,4]\end{array}$$

其次，Spark 改变了MLE evaluation 的多项式： $$\begin{array}{rl}\tilde{M}(r_x,r_y)& =\sum _{x=0}^{x<n}val(x)\cdot \widetilde{eq}(add{r}_{row}(x),r_x)\cdot \widetilde{eq}(add{r}_{col}(x),r_y)\end{array}$$

假定$(r_x,r_y)=((2,3),(3,4))$，通过时间复杂度为$O(m)$ 的计算，可以拿到两个类似lookup table的东西$me{m}_{row}、me{m}_{col}$： $$\begin{array}{cccc}i& me{m}_{row}=\widetilde{eq}(i,r_x)& j& me{m}_{col}=\widetilde{eq}(j,r_y)\\ 0& (1-2)\cdot (1-3)=2& 0& (1-3)\cdot (1-4)=2\\ 1& (1-2)\cdot 3=2& 1& (1-3)\cdot 4=2\\ 2& 2\cdot (1-3)=1& 2& 3\cdot (1-4)=1\\ 3& 2\cdot 3=1& 3& 3\cdot 4=2\end{array}$$

通过查表的方式，我们很容易拿到$e_{row}(x)=\widetilde{eq}(add{r}_{row}(x),r_x)$ 和 $e_{row}(x)=\widetilde{eq}(add{r}_{col}(x),r_x)$ 的取值： $$\begin{array}{ccccc}x& val(x)& e_{row}(x)& e_{col}(x)& M(x)\\ 000& 1& 2& 2& 4\\ 001& 2& 2& 1& 4\\ 010& 2& 2& 2& 3\\ 011& 4& 2& 2& 1\\ 100& 3& 2& 2& 2\\ 101& 1& 1& 1& 1\\ 110& 3& 1& 2& 1\\ 111& 4& 1& 1& 4\end{array}$$

因此我们可以得到sparase matrix 在$(r_x,r_y)=((2,3),(3,4))$ 上的evaluation值 $\tilde{M}(r_x,r_y)=0$。接下来prover 要做的就是生成相应的proof ： $$\begin{array}{rl}\tilde{M}(r_x,r_y)& =\sum _{x=0}^{x<n}val(x)\cdot \widetilde{eq}(add{r}_{row}(x),r_x)\cdot \widetilde{eq}(add{r}_{col}(x),r_y)\\ \Downarrow & \\ M(r)& =\sum _{x\in \{0,1{\}}^{\log n}}[val(x)\cdot \prod _{i=1}^{i<\log n}(x_i\cdot r_i+(1-x_i)\cdot (1-r_i))]\\ & \cdot [e_{row}(x)\cdot \prod _{j=1}^{j<\log n}(x_j\cdot r_j+(1-x_j)\cdot (1-r_j))]\\ & \cdot [e_{col}(x)\cdot \prod _{k=1}^{k<\log n}(x_k\cdot r_k+(1-x_k)\cdot (1-r_k))]\\ & \stackrel{?}{=}0\end{array}$$

本质是要证明三个多项式乘积的sum 等于0，这是一个标准的degree为3的Sumcheck。Sumcheck 的last round 需要验证： $$\widetilde{val}(r^{\prime })\cdot \widetilde{e_{row}}(r^{\prime })\cdot \widetilde{e_{col}}(r^{\prime })\stackrel{?}{=}{v}_{last}$$

其中$v_{last}$ Sumcheck 最后reduced 得到的claim，左边的三个term，其中$\widetilde{val}(r^{\prime })\stackrel{?}{=}{v}_{val}$ 可以轻易地通过一个IPA 协议证明得到；但是，$\widetilde{e_{row}}(r^{\prime })、\widetilde{e_{col}}(r^{\prime })$ 呢？也直接可以通过IPA 协议证明吗？

不行！细心地会发现上面的表中$e_{row}(x)、e_{col}(x)$ 并不是跟$val(x)$ 一样以determined dense vector 或者 determined witness的形式出现在verifier 面前的，对于verifier 来说，它只知道有： $$\begin{array}{rl}add{r}_{row}& =[0,0,1,1,1,2,3,3]\\ add{r}_{col}& =[0,2,0,1,3,2,0,2]\\ val& =[1,2,2,4,3,1,3,4]\end{array}$$ 这三样determined 的东西，$e_{row}(x)、e_{col}(x)$ 是prover 基于$add{r}_{row}、add{r}_{col}$通过查表 $me{m}_{row}$ 和 $me{m}_{col}$拿到的，对于verifier来说叫做non-determined witness，也是一种中间过程变量。因此还需要一个验证查表过程的电路，来保证它们的来历合规合法！

剩下的就是memory check的show time，上节已经detail 了它的整个过程，这里就不再赘述。

到此为止，Spark是如何更高效地解决Sparse Matrix evaluation 问题的就已经解释清楚了。文章的最后我们就可以非常轻松地revisit一下 Spartan 的整个协议了。

Spartan Protolcol Overview

假定，有这么一个业务计算： $$f(x)=x^3+3,x\in {\mathbb{F}}_{11}$$

setup 阶段构造R1CS Instance： $$\begin{gathered} A=\left[\begin{array}{ccccc}1& 0& 0& 0& 0\\ 0& 1& 0& 0& 0\\ 0& 0& 1& 0& 3\end{array}\right] \\ B=\left[\begin{array}{ccccc}1& 0& 0& 0& 0\\ 1& 0& 0& 0& 0\\ 0& 0& 0& 0& 1\end{array}\right] \\ C=\left[\begin{array}{ccccc}0& 1& 0& 0& 0\\ 0& 0& 1& 0& 0\\ 0& 0& 0& 1& 0\end{array}\right] \end{gathered}$$

这是非常典型的sparse matrix，可以充分发挥Spark的优势！

prover 填充向量$z$: $$z=\left[\begin{array}{c}2\\ 4\\ 8\\ 0\\ 1\end{array}\right]$$

令： $$\begin{array}{rl}\tilde{}{v}_A(x)& =\sum _{y\in \{0,1{\}}^s}\tilde{A}(x,y)\cdot \tilde{z}(y)\\ & =[(1-x_1)(1-x_2)\ast A_0\cdot z+(1-x_1)x_2\ast A_1\cdot z+x_1(1-x_2)\ast A_2\cdot z+x_1{x}_2\ast A_3\cdot z]\\ & \\ v_B(x)& =\sum _{y\in \{0,1{\}}^s}\tilde{B}(x,y)\cdot \tilde{z}(y)\\ & =[(1-x_1)(1-x_2)\ast B_0\cdot z+(1-x_1)x_2\ast B1\cdot z+x_1(1-x_2)\ast B_2\cdot z+x_1{x}_2\ast B_3\cdot z]\\ & \\ v_C(x)& =\sum _{y\in \{0,1{\}}^s}\tilde{C}(x,y)\cdot \tilde{z}(y)\\ & =[(1-x_1)(1-x_2)\ast C_0\cdot z+(1-x_1)x_2\ast C_1\cdot z+x_1(1-x_2)\ast C_2\cdot z+x_1{x}_2\ast C_3\cdot z]\end{array}$$

其中$A_0$ 代表矩阵$A$ 的第0行，同理$A_1$、$A_2$ … $B_0$…

还有： $$\tilde{F}(x)=v_A(x)\cdot v_B(x)-v_C(x)$$

prover 需要证明： $$\tilde{F}(x)=0,\forall x\in \{0,1{\}}^s$$

令： $$\begin{array}{rl}Q(\tau )& =\sum _{x\in \{0,1{\}}^s}\tilde{F}(x)\cdot \widetilde{\text{eq}}(x,\tau ),\forall \tau \in {\mathbb{F}}^s\\ & =\sum _{x\in \{0,1{\}}^s}\tilde{F}(x)\cdot \prod _{i=0}^s[x_i{r}_{{\tau }_i}+(1-x_i)(1-r_{{\tau }_i})]\end{array}$$

实例中，$s=2$: $$Q(\tau )=\tilde{F}(00)\cdot [(1-{\tau }_0)(1-{\tau }_1)]+\tilde{F}(01)\cdot [(1-{\tau }_0){\tau }_1]+\tilde{F}(10)\cdot [{\tau }_0(1-{\tau }_1)]+\tilde{F}(11)\cdot [{\tau }_0{\tau }_1]$$

假设：

$$Q(\tau )=0,\forall \tau \in {\mathbb{F}}^s$$

上面红色部分等于0的概率就非常低，因为$\tau$ 的domain是整个field，等于0或者1的概率自然就非常小几乎可以忽略，那么我们就可以推出：

$$\tilde{F}(x)=0,\forall x\in \{0,1{\}}^s$$

Round One

verifier 随机给定一个challenge factor $r_{\tau }\in {\mathbb{F}}^s$，prover 只需要证明：

$$\begin{array}{rl}Q(r_{\tau })& =\sum _{x\in \{0,1{\}}^s}\tilde{F}(x)\cdot \widetilde{\text{eq}}(x,r_{\tau })\\ & =\sum _{x\in \{0,1{\}}^s}\tilde{F}(x)\cdot \prod _{i=0}^s[x_i{r}_{{\tau }_i}+(1-x_i)(1-r_{{\tau }_i})]\\ & \stackrel{?}{=}0\end{array}$$

这是典型的degree 为3的Sumcheck（三个MLE polynomial的乘法），Sumcheck 的最后reduce 成： $$（\widetilde{v_A}(r_x)\cdot \widetilde{v_B}(r_x)-\widetilde{v_C}(r_x))\cdot \widetilde{eq}(r_x,r_{\tau })\stackrel{?}{=}{v}_x$$

其中$\widetilde{eq}(r_x,r_{\tau })$ verifier 可以自行计算，但$\widetilde{v_A}(r_x)、\widetilde{v_B}(r_x)、\widetilde{v_C}(r_x)$ 隐藏着witness信息，需要prover 计算完成之后发送$v_A、v_B、v_C$给verifier，verifier 完成上述等式验证。

Round Two

接着prover 需要证明： $$\begin{array}{rl}\tilde{}{v}_A(r_x)& =\sum _{y\in \{0,1{\}}^s}\tilde{A}(r_x,y)\cdot \tilde{z}(y)\\ & =\sum _{y\in \{0,1{\}}^s}[(1-r_x^1)(1-r_x^2)\cdot {\tilde{A}}_0(y)\cdot \tilde{z}(y)]+[(1-r_x^1)r_x^2\cdot {\tilde{A}}_1(y)\cdot \tilde{z}(y)]+[r_x^1(1-r_x^2)\cdot {\tilde{A}}_2(y)\cdot \tilde{z}(y)]++[r_x^1{r}_x^2\cdot {\tilde{A}}_3(y)\cdot \tilde{z}(y)]\\ & =\sum _{y\in \{0,1{\}}^s}[(1-r_x^1)(1-r_x^2)]\cdot [A((0,0),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[(1-r_x^1)r_x^2]\cdot [A((0,1),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[r_x^1(1-r_x^2)]\cdot [A((1,0),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[r_x^1{r}_x^2]\cdot [A((1,1),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & \stackrel{?}{=}{v}_A\\ & \\ v_B(x)& =\sum _{y\in \{0,1{\}}^s}\tilde{B}(r_x,y)\cdot \tilde{z}(y)\\ & =\sum _{y\in \{0,1{\}}^s}[(1-r_x^1)(1-r_x^2)\cdot {\tilde{B}}_0(y)\cdot \tilde{z}(y)]+[(1-r_x^1)r_x^2\cdot {\tilde{B}}_1(y)\cdot \tilde{z}(y)]+[r_x^1(1-r_x^2)\cdot {\tilde{B}}_2(y)\cdot \tilde{z}(y)]++[r_x^1{r}_x^2\cdot {\tilde{B}}_3(y)\cdot \tilde{z}(y)]\\ & =\sum _{y\in \{0,1{\}}^s}[(1-r_x^1)(1-r_x^2)]\cdot [B((0,0),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[(1-r_x^1)r_x^2]\cdot [B((0,1),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[r_x^1(1-r_x^2)]\cdot [B((1,0),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[r_x^1{r}_x^2]\cdot [B((1,1),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & \stackrel{?}{=}{v}_B\\ & \\ v_C(x)& =\sum _{y\in \{0,1{\}}^s}\tilde{C}(r_x,y)\cdot \tilde{z}(y)\\ & =\sum _{y\in \{0,1{\}}^s}[(1-r_x^1)(1-r_x^2)\cdot {\tilde{C}}_0(y)\cdot \tilde{z}(y)]+[(1-r_x^1)r_x^2\cdot {\tilde{C}}_1(y)\cdot \tilde{z}(y)]+[r_x^1(1-r_x^2)\cdot {\tilde{C}}_2(y)\cdot \tilde{z}(y)]++[r_x^1{r}_x^2\cdot {\tilde{C}}_3(y)\cdot \tilde{z}(y)]\\ & =\sum _{y\in \{0,1{\}}^s}[(1-r_x^1)(1-r_x^2)]\cdot [C((0,0),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[(1-r_x^1)r_x^2]\cdot [C((0,1),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[r_x^1(1-r_x^2)]\cdot [C((1,0),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & +[r_x^1{r}_x^2]\cdot [C((1,1),y)\cdot \widetilde{eq}(y,r^{\prime })]\cdot [z(y)\cdot \widetilde{eq}(y,r^{\prime })]\\ & \stackrel{?}{=}{v}_C\end{array}$$