3 Arithmetization of Correct Program Execution

首先需要将关系$\mathcal R_{TinyRAM}$转换为有限域上的关系，给定字长为$W$的TinyRAM和有限域$\mathbb F$，可以通过对字进行编码来将其映射到域中的元素，比如$a\in \{0,\dots,2^W-1\}$，可以通过累加$a$次的方式来讲字映射到域上：$a1_\mathbb F=1_\mathbb F+\cdots+1_\mathbb F$，为了避免溢出，需要令域的大小$p>2^W-2^{W-1}$

此外还需要将程序、内存和状态编码为域上的三元组，这里通过引入一个新的关系$\mathcal R^{field}_{TinyRAM}$来实现，关系由元组需要满足的一组约束条件组成，目的是确保程序的执行轨迹正确，该关系的实例为$u=(P,v,T,M)$，witness为$w$

接下来介绍witness的结构，以及正确程序执行的关系如何分解为更简单的子关系

3.1 Witness Structure

对于正确执行的程序，将TinyRAM的程序、内存和状态编码为域元素，并放入表2所示的四个表中

  • 执行表$Exe$：包含编码为域元素的TinyRAM状态，该表有$T$行（因为有$T$个执行步骤），第$t$行表示TinyRAM在第$t$步时的初始状态，每一行包含程序计数器$pc_t$，指令$inst_{pc_t}$，立即数$\mathsf A_t$，当前所有寄存器的值$\{r_{0,t},\dots,r_{K-1,t}\}$，标志位$flag_t$，第$t$行还包含内存地址$addr_t$和值$v_{addr_t}$，表示该行指令执行完毕后地址$addr_t$处保存的值为$v_{addr_t}$，此外还包含一个用于检查程序执行正确性的辅助域元素$aux_{Exe}$
  • 程序表$Prog$：包含编码为域元素的TinyRAM程序$P$，每一行描述了程序当前的指令，至多三个操作数，一个立即数，该表也有一个辅助域元素$aux_{Prog}$，该表的每一行可以用于有效计算程序并用于后续的正确性验证
  • 内存表$Mem$：包含所有可能的内存地址，初始值和辅助域元素$usd$，内存表按照$usd$的取值划分为两个部分
  • 查找表$EvenBits$：包含长度为$W$的字的编码，每个字的二进制表示中的奇数位均置0，该表包含$2^{W/2}$个域元素，哟弄个与检查某些域元素是否编码为长度为$W$的字

记元组$(Exe,Prog,Mem,EvenBits)$表示四个表，对应的关系$\mathcal R^{field}_{TinyRAM}$如下，其中三个关系$\mathcal R_{check},\mathcal R_{mem},\mathcal R_{step}$确保了witness包含编码TinyRAM正确执行的域元素

简而言之，三个关系的作用如下，具体行为后续介绍

  • $\mathcal R_{check}$：用于检查内存中的初始值对应于$Mem$表中的值，$Prog$表中包含正确编码的值，$EvenBits$表中包含正确编码的额外值，同时检查TinyRAM的初始状态正确，检查程序在第$T$步正确终止并输出0
  • $\mathcal R_{mem}$：检查内存的使用与程序执行时的指令一致，也即程序第$t$步加的内存值对应于该内存地址存放的值
  • $\mathcal R_{step}$：检查程序的每一步均正确执行

此外，还有四个相关的关系

  • 相等关系$\mathcal R_{eq}$：给定$(v_1,\dots,v_m)$的$W$比特字列表，$\mathcal R_{eq}$关系用于检查该列表是否正确编码为表$Tab$中的第$i$行
  • 查找关系$\mathcal R_{lookup}$：$\mathcal R_{lookup}$关系用于检查域元素列表$\boldsymbol w$是否包含在表$Tab$中
  • 范围关系$\mathcal R_{range}$：用于检查域元素$a$（以$W$比特表示）是否在范围$\{0,\dots,2^W-1\}$内，该关系需要两个表$a_e,a_o$，分别存储元素$a$的二进制表示的偶数比特位和奇数比特位，假设$a$为4比特长，即$a=(a_3,a_2,a_1,a_0)$，则$a_e$保存$(0,a_2,0,a_0)$，$a_o$保存$(a_3,0,a_1,0)$，此时可以通过$2a_o+a_e$恢复$a$，因此令$EvenBits$表保存所有域元素的偶数位，通过$2a_o+a_e(a_o,a_e\in EvenBits)$即可完成上述范围检查
  • 置换关系$\mathcal R_{perm}$：用于检查两个向量是否互为置换

四个关系如下图所示

‍

3.2 Checking the Correctness of Values

前面提到了$\mathcal R_{check}$的目的是检查向量$w$是否包含正确数量的域元素，且这些域元素可以被划分为适当的表，并分别检查这些表中特定值是否正确，具体而言，关系$\mathcal R_{check}$包含下列几个条件

  • $Exe$表的第一行$Exe_1$包含下列值：$time=1,pc_1=0$，$inst_{pc_1}$等于程序的第一条指令，$A_1$等于第一条指令对应的立即数，所有寄存器$r_{i,1}$、内存地址$addr_1$及其值$v_{addr_1}$​均为0
  • $Exe$表的最后一行$Exe_T$包含下列值：$time=T,pc_T=L-1,inst_{pc_T}=answer,A_T=0$​
  • $Evenbits$包含所有奇数位为0的字
  • $Prog$表包含编码程序$P$的域元素及其对应的辅助值
  • $Mem$表包含输入字列表及其辅助值$usd$

结合上述五个条件，可以将关系$\mathcal R_{check}$表述如下

3.3 Checking Memory Consistency

$\mathcal R_{mem}$关系用于检查程序执行的各个步骤之间的内存一致性，也即需要检查第$t$步从某一内存地址读取的值与最后一次写入该地址的值一致，可以分为两种情况

  • 第一次读内存地址：检查读取的值与该地址的初始值一致
  • 连续两次读取同一地址：检查读取的值不变

但是由于$Exe$表是按照执行顺序排序的，而非按照内存地址排序，因此需要考虑非连续读取内存地址时的一致性检查，本文用到的方法时在$Exe$表中加入下列辅助值

$$ aux_{Exe}=\{\tau_{link},v_{link},v_{init},usd,S,L,\dots\} $$

  • $\tau_{link}$：记录上一次访问本内存地址的时刻（首次访问该地址除外）
  • $v_{link}$：记录tau_{link}时刻后本内存地址的值
  • $v_{init}$：记录本地址的初始值，该值与$Mem$表一致
  • $usd$：若为第一次访问当前地址，则该值置0，否则置1
  • $S/L$：分别写内存时$S=1$，读内存时$L=1$，其余情况置0，这两个值也会作为辅助值保存在$aux_{Prog}$中

本文通过指定内存访问的循环（cycles）来检查内存一致性，从而确保一个循环中的连续项对应于同一内存地址的两次连续访问，简单来说就是用一个循环来考虑同一内存地址的所有操作

之后利用上述辅助值，定义关系$\mathcal R_{cycle}$，该关系检查同一地址的所有内存访问（$S+L=1$）是否连接至循环，且未涉及内存的操作（$S+L=0$）不包含在循环内，此时关系$\mathcal R_{cycle}$需要检查是否有下列四个等式成立

$$ \begin{aligned} &S_t+L_t=S_{t'}+L_{t'}\\ &t=\tau_{link_{t'}}\\ &v_{addr_t}=v_{link_{t'}}\\ &addr_t=addr_{t'} \end{aligned} $$

但是上述关系仅保证在同一内存位置上存在循环，但不保证循环中的连续项对应于连续时刻的内存访问操作，因此需要有另一方式来检查内存循环是否在时间上是有序的，可以通过检查所有的$t\in [T]$均满足$t>\tau_{link_t}$来完成，由于所有内存访问均连接至循环，因此第一次访问新的内存位置时，$\tau_{link}$会保存程序访问该地址的最后一个时刻，这一检查定义为关系$\mathcal R_{time}$

接下来还需要确保循环对应于正确的内存地址，因此还需要检查访问同一地址的所有操作都包含在同一个循环内，由于循环以时间排序，必然有$usd=0$以结束循环，因此可以通过让每个内存地址的$usd$至多有一次机会可以置0，从而确保该内存地址至多为循环的一部分，这一部分的检查定义为关系$\mathcal R_{blookup}$，该关系会检查$Exe$表中的$(addr_t,v_{init_t},usd)$三项是否包含于表$Mem$中

最后还需要检查程序从某一内存地址读取的是否与上一次写入该内存的值一致（读取新内存地址的值应当与该地址的初始值一致），这一检查定义为关系$\mathcal R_{load}$，写内存地址无需检查（隐式包含在该关系中）

之后将上述四个子关系结合起来，就得到了关系$\mathcal R_{mem}$，如下

3.4 Checking Correct Execution of Instructions

前面提到了$\mathcal R_{step}$的目的是检查程序的每个步骤都正确执行，关系需要检查执行表$Exe$中的每一行保存的字是否都在范围$\{0,\dots,2^W-1\}$内，检查标志位$flag$是否为单比特，检查程序计数器和立即数是否与指令相对应，检查指令$inst$是否正确执行等等（这里假设前面内存一致性检查通过）

和内存检查一样，命令执行检查引入两个辅助值列表，由一些临时变量$a,b,c,d$，输出向量$out$和对应的选择向量$s_a,\dots,s_d$组成

$$ \begin{aligned} aux_{Exe}&=\{\dots,a,b,c,d,out,s_a,s_b,s_c,s_d,s_{out},s_{ch},\dots\}\\ aux_{Prog}&=\{\dots,s_a,s_b,s_c,s_d,s_{out},s_{ch}\} \end{aligned} $$

临时变量用于临时保存指令的输入和输出的拷贝，比如指令需要将寄存器$j$的值与立即数$A$相加，并保存至寄存器$i$中，此时需要检查$r_{i,t+1},r_{j,t},A_t$

如果令$c=r_{i,t+1},a=r_{j,t},b=A_t$，利用临时变量可以直接在辅助值中检查$c=a+b$即可，而无需考虑不同时刻的寄存器的值

而对于四个临时变量的检查需要将对应的寄存器、立即数、内存读写从临时变量中读取或保存，此时需要用选择向量来辅助操作

由于执行表中的每一行都会包含多个变量，该行和下一行的每个变量都可能是操作数，选择向量可以表明指令选择了哪一个变量进行操作

TinyRAM包含26种不同的指令，为了确保零知识性，我们需要确保执行过程中不能泄露具体执行的指令，但是如果对每一种指令都指定一种检查的话开销很大

注意到大部分指令之间具有相似性，比如对减法的检查$c=a-b$可以通过移项转变为加法的检查$a=b+c$，从而我们可以将26种指令的检查精简为对九种指令（AND,XOR,OR,SUM,SSUM,PROD,SPROD,MOD,SHIFT）和四个标志位$FLAG_1,\dots,FLAG_4$的检查，将上述这些值包含在向量$out$种，并检查适当的子集来验证指令是否正确执行

和临时变量的选择器一样，用一个二进制向量$s_{out}$来检查$out$向量，验证其内积等式即可$s_{out}\circ out=0$

除了检查指令是否正确执行以外，还需要检查未参与指令执行的状态是否被改变，这里需要通过向量$s_{ch}$来检查，若状态在指令执行后被改变（比如写寄存器，写内存等等），则该状态对应的向量$s_{ch}$中的比特为置0，否则置1

综上，$\mathcal R_{step}$可以分解为下列几个子关系

  • $\mathcal R_{mux}$：检查$a_t,b_t,c_t,d_t$与指令$inst_t$的一致性
  • $\mathcal R_{consistent}$：检查时刻计数器正确自增，检查程序计数器在正确的范围内，检查指令及和立即数之间的一致性，检查选择器向量的正确性，检查输出向量$out_t$与指令$inst_t$的一致性，检查相邻两行寄存器的一致性
  • $\mathcal R_{ins}$：检查$a_t,b_t,c_t,d_t$在范围$\{0,\dots,2^W-1\}$内，检查输出向量$out_t$与$a_t,b_t,c_t,d_t$之间的一致性

这里说一下$\mathcal R_{ins}$，该关系确保了程序指令被正确执行，这里将输出向量$out$划分为四个部分：逻辑部分（包含三个位运算AND,XOR,OR），算术部分（SUM,PROD,SSUM,SPROD），移位部分（SHIFT）和标志位（FLAG1,...,FLAG4），四个标志位分别代表四种不同的运算类型，3.5节介绍如何处理这四个部分

另外两个关系的具体检查方式可以看原文$[1]$

3.5 A Breakdown of the Instruction Relation

这一节重点介绍一下$\mathcal R_{ins}$关系，和之前提到的一样，该关系用输出向量$out$和选择向量$s_{out}$来检查指令是否正确执行，同时为了满足零知识的性质，这里将26条指令精简为了13项

假设$\mathcal R_{consistent}$关系验证正确，此时可以将$\mathcal R_{ins}$关系分为三个子关系，分别对应于$out$中的逻辑、算术、移位部分

Logical Ops

逻辑部分的检查可以用之前划分奇偶比特位的思想完成，以按位与运算为例，记$a,b$为逻辑运算的两个输入，$c$为输出，按照之间划分奇偶比特位的方式，可以得到$a=2a_o+a_e,b=2b_o+b_e$，此时将两个输入的偶数比特位相加，可以得到

$$ \begin{aligned} a_e+b_e&=(0,a_{W-2},\dots,a_0)+(0,b_{W-2},\dots,b_0)\\ &=(a_{W-2}\wedge b_{W-2},a_{W-2}\oplus b_{W-2},\dots,a_0\wedge b_0,a_0\oplus b_0) \end{aligned} $$

此时我们可以得到$a_e+b_e$的奇数位均为按位与运算，偶数为均为按位异或，因此我们可以将$a_e+b_e$进一步的拆分为$a_e+b_e=2e_o+e_e$，同理，对$a,b$的奇数位也进行上述操作，可以得到$a_o+b_o=2o_o+o_e$

之后再按照3.1节中的方法，把上面所有的值$a_o,a_e,b_o,b_e,e_o,e_e,o_o,o_e$均保存至$EvenBits$表中即可，在需要检查时，我们可以根据表中的特定值，检查下列等式即可

$$ \begin{matrix} a=2a_o+a_e&b=2b_o+b_e \\ a_o+b_o=2o_o+o_e&a_e+b_e=2e_o+e_e \\ a\wedge b =2o_o+e_o & a\oplus b = 2o_e+e_e \end{matrix} $$

接下来以指令：$and \ reg_i \ reg_j \ A$为例，令向量$out$中的$AND=2o_o+e_o-c,XOR=2o_e+e_e-c$，同时设置选择向量，使得$a=A_t,b=r_{j,t},c=r_{i,t+1}$，根据上面的等式，当且仅当$c$为$a,b$按位与的结果时，有$AND=0$，从而表明指令执行正确，同理可以检查$XOR=0$

按位或运算可以拆分为AND和XOR的组合，也即$a\vee b=(a\wedge b)+(a\oplus b)$，此时令$OR=XOR+AND+c$并检查$OR=0$即可

按位取反可以转化为一个数与$2^W-1$的异或（需要用到$Exe$表中的辅助值$2^W-1$），按位异或还需要将标志位$FLAG_1,FLAG_2$置0

上述逻辑运算结果会影响标志位，需要确保了$FLAG_1$和$FLAG_2$有且仅有一个为1，可以用下列两个等式进行检查

$$ \begin{matrix} FLAG_1=flag_{t+1}+c& FLAG_2=(flag_{t+1}+c)\cdot a_{flag}-1 \end{matrix} $$

最后将$Exe$表中的临时变量$a,b,c,d$拆分为对应的奇数位和偶数位$a_o,a_e,\dots,d_o,d_e$，同时加入对应的$o_o,o_e,e_o,e_e$和$a_{flag}$，即可得到关于逻辑运算的子关系$\mathcal R_{logic}$​

这里原文给出了四种逻辑运算所对应的选择向量（由于逻辑运算不需要用到临时变量$d$，因此可以将$s_d$置0）

Integer Ops

验证整数运算更简单了，只需要将字映射到域，并在域上完成运算即可，但是为了防止计算溢出（尤其是乘法），需要确保映射的域足够大

首先考虑无符号数，还是以指令：$add \ reg_i \ reg_j \ A$为例，设置选择向量，使得$a=A_t,b=r_{j,t},c=r_{i,t+1}$，通过检查等式$SUM=a+b-c-w^W\cdot flag_{t+1}+d=0$来验证指令是否正确执行（$flag_{t+1}$为溢出标志位，$d$置0），减法可通过转换为加法来验证

对于TInyRAM的乘法，包含三类，如下

  • mull：低位字的有符号乘法
  • umull：高位字无符号乘法
  • umulh：高位字的无符号乘法

对于指令：$mull \ reg_i \ reg_j \ A$，令$PROD=a\cdot b-d-2^W\cdot c$，设置选择向量，使得$a=A_t,b=r_{j,t},d=r_{i,t+1}$，$c$保存乘法结果，检查$PROD=0$即可，umulh指令同理

前面提到了关系$\mathcal R_{ins}$需要检查$a_t,b_t,c_t,d_t$在范围$\{0,\dots,2^W-1\}$内，由于有符号数据采用补码形式保存，对于数据$a$，记其符号位为$\sigma_a$​

根据有符号数的特性，可以将其映射为域元素$a_\sigma=-\sigma_a\cdot 2^W+a\in \{-2^{W-1},\dots,2^{W-1}-1\}$，之后再利用奇偶比特位的方法，检查$a_o+(1-2\sigma_a)\cdot 2^{W-2}\in EvenBits$即可，此类方法需要在辅助值$aux_{Exe}$中将$a,\dots,d$拆分为$a_\sigma,\sigma_a,\dots,d_\sigma,\sigma_d$，有符号数指令的验证和无符号数类似

此外，还需要验证乘法运算的标志位$FLAG_1=FLAG_2=0$

加法和乘法的选择器向量如下图所示

​

之后是模运算，以指令：$umod \ reg_i \ reg_j \ A$为例，令$d=r_{j,t}$，$c$为模数$A_t$，$b$为$d/c$的商，$a$为余数$r_{i,t+1}$，

模运算需要考虑模数为0的情况，也即当$c=0$时，操作返回0并将$flag_{t+1}$置1（此时需要检查$FLAG_1=FLGA_2=0$），若模数非零，则验证等式为$umod=d-b\cdot c-a=0$

此外模数非零时还需要检查余数小于模数，也即检查$a<c$，这一检查可以转化为对$c-a-1$的范围检查，用奇偶比特位的思想分解为$c-a-1=2r_o+r_e$，将$r_o,r_e$加入辅助值列表并验证等式$(1-flag_{t+1})\cdot (c-a-1-2r_o-r_e)=0$

注意到模运算的验证等式会验证除法的商的正确性，可以将其用于检查除法udiv，此时交换上述$a,b$的值即可，验证等式不变，这里仍然需要考虑$c=0$的情况，返回0并将$flag_{t+1}$置1，由于交换了$a,b$的值，因此需要加一个验证等式$b\cdot flag_{t+1}=0$，而除数非零的情况需要检查$a<c$

综上，除法的验证等式可以写为$FLAG_3=b\cdot flag_{t+1}+(1-flag_{t+1})\cdot (c-a-1-2r_o-r_e)$

这里有一个变形：由于$b$和$flag_{t+1}$不会同时为1，因此可以将模运算的验证等式变形为$MOD=flag_{t+1}\cdot (b-d)+d-b\cdot c-a=0$，当$flag_{t+1}=0$时该验证等式在模运算和除法中等价，当$flag_{t+1}=1$时，有$c=0$，也即$b=a$，此时有$FLAG_3=0,b=0$，因此$a=0$，这一个变形可以让我们用一个等式来验证两个运算指令

模运算和除法对应的选择器向量如图6所示

Shift Ops

左移或右移$A$位等价于将该数与$2^A$相乘或相除，因此可以将移位指令的检查转换为上述的乘法与除法的检查，有一种更有效的检查方式，下面介绍

以左移指令：$shl \ reg_i \ reg_j \ A$为例，这里构造一个新表$Pow$，该表保存值对$(a,2^a \mod 2^W),a\in [W]$，同时在$aux_{Exe}$中保存辅助值$a_{shift},a_{power}$

然后令临时变量$a$保存移位数$A_t$，此时$a_{shift}$用于检查$A_t\in [W]$，验证等式为$\Big( a_{shift}\cdot (a_{shift}-1)=0\wedge (1-a_{shift})\cdot (W-a-2r_o-r_e)=0 \Big )$，第一个子句确保$a_{shift}$为单比特，第二个子句确保$W<a$时有$a_{shift}=1$

当$a_{shift}=0$时，$a_{power}$用于保存$2^a\mod 2^W$（否则保存0），此时可以用关系$\mathcal R_{lookup}$来，通过检查表$Pow$来检查$a,2^a\mod 2^W$之间的一致性

此时对于左移指令的检查，令临时变量$b=r_{j,t},d=r_{i,t+1}$，临时变量$c$为计算结果，并验证等式$SHIFT=a_{power}\cdot b-d-2^W\cdot c=0$（这里需要检查寄存器$r_{j,t}$的最高位的一致性，通过等式$flag_{t+1}-\sigma_b=0$检查）

然后后面这里有一段右移A位等价于左移W-A位并取高W位，这里没看懂，为什么就等价了？

根据这一点，可以令$a=W-A_t,b=r_{j,t},d=r_{i,t+1}$，并检查等式$flag_{t+1}-\rho_b=0$，这里$\rho_b$表示$b$的最低有效位（这个最低有效位又是怎么来的）

因此验证公式可以转换为$FLAG_4=flag_{t+1}-b_{flag}\cdot \sigma_b-\rho_b\cdot (1-b_{flag})$

对应的选择器向量如图7所示

​

Comparison Ops

首先考虑无符号数的情况，对于相等比较指令$compe \ r_{i,t} \ A$，操作在结果为真时会将flag置1，否则置0，可以将相等比较转换为两个数的按位异或，若结果为0则将flag置1，否则置0

对于大小比较指令$compa \ r_{i,t} \ A$，当且仅当$r_{i,t} >A$时flag置1

为了同时考虑上述两种情况，令$a=r_{i,t},c=A_t,d=0$，$b$为结果，通过等式$a-c=2^W\cdot flag_{t+1}-b$，此时若$flag_{t+1}=1$，则表明等式右侧大于0，也即$a>c$，若$flag_{t+1}=0$，由于$b\in \{0,\dots,2^W-1\}$，因此有$a\leq c$，对应的验证等式为$SUM=a-c-2^W\cdot flag_{t+1}+b$

有符号数类似，验证等式需要替换为$SSUM=a_\sigma+b-c_\sigma-2^W\cdot flag_{t+1}+d=0$（等式中$d$恒等于0，其他值与无符号数相同）

对于大于等于的情况，无符号数需要将等式替换为$a-c=2^W\cdot flag_{t+1}-b-1$，有符号数令$d=1$即可

对应的选择向量如图8所示

3.6 Selection Vectors for $\mathcal R_{mux}$ and $\mathcal R_{consistent}$

3.5节介绍了计算相关的检查，本节介绍指令集的剩余操作的检查，包括移动，跳转，内存操作，终止操作

Move and Jump Ops

mov指令将$A_t$保存至寄存器$reg_i$中，jmp指令将程序计数器$pc_{t+1}$设置为$A_t$，这两个指令的检查通过临时变量$a,b$完成，对应的选择向量如图9所示

条件move指令cmov当且仅当$flag_t=1$时才会执行，此时该指令的验证等式为$MOD=flag_{t+1}\cdot (b-d)+d-a=0$，其中$a+r_{i,t+1},b=A_t,d=r_{i,t}$

条件跳转cjmp同理，此时令$a=pc_{t+1},b=A_t,d=pc_t+1$，检查$MOD=0$即可

由于$\mathcal R_{ins}$还需要对$c$进行范围检查，这里需要假设程序的长度$L<2^W-1$

条件非跳转cnjmp当且仅当$flag_t=0$时执行，此时交换$b,d$的值并验证$MOD=0$即可

Memory Ops

内存操作通过关系$\mathcal R_{mem}$检查内存一致性，也即检查内存地址$addr_t$及其对应值$v_{addr_t}$是否正确更新，检查store和load指令时，寄存器更新为$v_{addr_t}$中的值

上述检查需要检查$v_{addr_t}$与寄存器中输入或输出的值是否一致，可以通过前面提到的按位异或的方式来检查，内存操作对应的选择向量如图10所示

Answer

程序在$T$步之后会以answer 0指令结束，不失一般性，可以假定程序跳转至最后一条指令来结束程序

answer指令的立即数为0，因此$\mathcal R_{check}$中需要检查两项

  • 程序只执行一次answer指令
  • 程序不会过早的执行answer指令

上述两点通过移除$Prog$表中的所有answer指令来完成，也即$\mathcal R_{ins}$对表中$t=1,\dots,T-1$项的检查不能是answer指令

References

$[1]$ Jonathan Bootle, Andrea Cerulli, Jens Groth, Sune K. Jakobsen, Mary Maller:Nearly Linear-Time Zero-Knowledge Proofs for Correct Program Execution. IACR Cryptol. ePrint Arch. 2018: 380 (2018)

$[2]$ Ran Canetti, Yevgeniy Dodis, Shai Halevi, Eyal Kushilevitz, Amit Sahai:Exposure-Resilient Functions and All-or-Nothing Transforms. EUROCRYPT 2000: 453-469

$[3]$ Yevgeniy Dodis:Exposure-resilient cryptography. Massachusetts Institute of Technology, Cambridge, MA, USA, 2000

‍