什么是 TinyRAM 指令集？

介绍 TinyRAM 是一种简单的精简指令集计算机 (RISC)，具有字节级可寻址随机存取存储器和输入磁带。 TinyRAM 有两种变体：一种遵循哈佛（hv）架构，另一种遵循冯诺依曼（vn）架构（在本文中，我们主要关注冯诺依曼架构）。 简洁的计算完整性和隐私研究 (SCIPR) 项目构建了用于证明 TinyRAM 程序正确执行的机制，而 TinyRAM 旨在提高此设置的效率。它在两个相反的要求——“足够的可表达性”和“小指令集”之间取得了平衡： 从高级编程语言编译时具有足够的可表达性以支持简短、高效的汇编代码， 小型指令集，支持通过算术电路进行简单验证，并使用 SCIPR 的算法和密码机制进行有效验证。 在本文中，我们将补充上一篇文章而不是重复TinyRAM介绍，然后重点介绍指令和电路约束。 关于TinyRAM的基本介绍，请参考我们之前的文章： tinyram简介-中文 TinyRAM Review-English TinyRAM 指令集 TinyRAM 支持 29 条指令，每条指令由一个操作码和最多 3 个操作数指定。操作数可以是寄存器的名称（即，从 0 到 K-1 的整数）或立即数（即，W 位字符串）。 除非另有说明，否则每条指令不会单独修改标志位，默认情况下将 pc 递增 i (i % 2^W)，对于 vnTinyRAM，i=2W/8。 通常，第一个操作数是指令计算的目标寄存器，其他操作数指定指令所需的参数。最后，所有指令都需要一个机器周期来执行。 位相关操作 : 指令 将 [rj] 和 [A] 的位和结果存储在 ri 寄存器中。同样，如果结果为 ，则将 设置为 1，否则将其设置为 0。 and and ri rj A 0^{W} flag 指令 将 [rj] 和 [A] 的位和结果存储在 ri 寄存器中。同样，如果结果为 ，则将 设置为 1，否则将其设置为 0。 or or ri rj A 0^{W} flag 指令 将 [rj] 和 [A] 的位和结果存储在 ri 寄存器中。同样，如果结果为 ，则将 设置为 1，否则将其设置为 0。 xor xor ri rj A 0^{W} flag 指令 将 [rj] 和 [A] 的位和结果存储在 ri 寄存器中。同样，如果结果为 ，则将 设置为 1，否则将其设置为 0。 not not ri A 0^{W} flag 整数相关操作 这些是各种无符号和有符号整数相关操作。在每个设置中，如果发生算术溢出或错误（例如除以零），则将 设置为 1 ，否则将其设置为 0。 flag 下面的部分， 代表一系列整数{0*,…,* $2^{W} -1 $}；这些整数由 W 位字符串组成。 表示一系列整数 {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1。这些整数也由 W 位字符串组成。 U_{W} S_{W} 指令 将 W 位串 a_{W−1}⋯a_{0} 存入 ri。 a_{W−1}⋯a_{0} 是 的 W 最低有效位 (LSB)。此外， 将设置为 。 是 G 的最高有效位 (MSB)。 add： add ri rj A G = [rj]_u + [A]_u flag G_{W} G_{W} 指令 将W位串a_{W−1}⋯a_{0}存入ri。 a_{W−1}⋯a_{0} 是 的 W 最低有效位 (LSB)。此外， 将被设置为 。 是 G 的最高有效位 (MSB)。 sub： sub ri rj A G = [rj]_u + 2^W - [A]_u flag 1−G_{W} G_{W} 指令 将 W 位串 a_{W−1}⋯a_{0} 存储到 ri 中。 a_{W−1}⋯a_{0} 是 的 W 最低有效位 (LSB)。此外， 将被设置为 1，如果 mull mull ri rj A G=[rj]_u∗[A]_u flag ，否则设为 0。 [rj]_u × [A] {W} u ∉ U 指令 将 W 位串 a_{W−1}⋯a_{0} 存储到 ri 中。 a_{W−1}⋯a_{0} 是 的 W 最高有效位 (MSB)。此外，如果 ，则 将设置为 1，否则将其设置为 0。 umulh umulh ri rj A G = [rj]_u ∗ [A]_u [rj]_u × [A] {W} u ∉ U flag 指令 将 W 位串 a_{W−1}⋯a_{0} 存入 ri。 a_{W−1} 是 是 的 W - 1 MSB。此外，如果 } ，则 将设置为 1，否则将其设置为 0。 smulh smulh ri rj A [rj] {W−2}⋯a{0} u ∗ [A]_u 的符号位，a [rj]_u ∗ [A]_u [rj]_u × [A] {W u ∉ S flag 指令 将 W 位串 a_{W−1}⋯a_{0} 存储到 ri 中。 udiv udiv ri rj A 如果 。 [A] 则 {W−1}⋯a_{0} = 0^W u = 0， 如果 是整数 Q 的唯一二进制编码，使得对于某些整数 ，公式 是可行的。此外，只有当 时， 才会被设置为 1。 [A] {W−1}⋯a_{0} u∣ ≠ 0，则 R ∈ {0,…,[A]_u − 1} [rj]_u = [A]_u × Q + R [A]_u=0 flag 指令 将 W 位串 a_{W−1}⋯a_{0} 存入 ri。 umod umod ri rj A 如果 。 [A] 则 {W−1}⋯a_{0} = 0^W u = 0， 若 其取值范围为 [A] {W−1}⋯a_{0} u∣ ≠ 0，则a 是整数R的唯一二进制编码， ，使得公式 可用于某些 Q 值。此外，只有当 时， 才会被设置为 1。 {0,…,[A]_u−1} [rj]_u = [A]_u × Q+R [A]_u = 0 flag 班次相关操作 指令 将[rj] 左移[A] u 位得到的W 位串存储在ri 寄存器中。移位后的空白位置用0填充。另外，flag设置为[rj]的MSB。 shl shl ri rj A 指令 将[rj] 右移[A] u 位得到的W 位串存储在ri 寄存器中。移位后的空白位置用0填充。另外，flag设置为[rj]的LSB。 shr shr ri rj A 比较相关的操作 比较相关操作中的每条指令都不会修改任何寄存器；比较结果将存储在 中。 flag 指令 如果 [ri] = [A] 则将 flag 设置为 1，否则将其设置为 0 cmpe cmpe ri A 指令 如果 则将 flag 设置为 1，否则将其设置为 0 cmpa cmpa ri A [ri]_u > [A]_u 指令 如果 则将 flag 设置为 1，否则将其设置为 0 cmpae cmpae ri A [ri]_u ≥ [A]_u 指令 如果 则将 flag 设置为 1，否则将其设置为 0 cmpg cmpg ri A [ri]_s > [A]_s 指令 如果 则将 flag 设置为 1，否则将其设置为 0 cmpge cmpge ri A [ri]_S ≥ [A]_S 移动相关操作 指令 将 [A] 存储到 ri 寄存器中。 mov mov ri A 如果 flag = 1， 指令 会将 [A] 存储到 ri 寄存器中，否则 ri 寄存器的值不会改变。 cmov cmov ri A 跳跃相关 这些跳转和条件跳转指令不会修改寄存器和 ，但会修改 。 flag pc 指令 将 [A] 存储到 pc 中。 跳转 jmp A 指令 将在 = 1 时将 [A] 存储到 pc 中，否则将 pc 递增 1 cjmp cjmp A flag 指令 在 = 0 时将 [A] 存储到 pc 中，否则将 pc 加 1 cnjmp cnjmp A flag 内存相关操作 这些是简单的内存加载操作和存储操作，其中内存的地址由立即数或寄存器的内容决定。 这些是 TinyRAM 中唯一的寻址方法。 （TinyRAM 不支持常见的“base+offset”寻址模式）。 指令 将 [ri] 的 LSB 存储在内存中的 [A] U-th 字节地址。 store.b store A ri 指令 将内存中第[A]个U字节地址的内容存入ri寄存器（前面字节填充0）。 load.b load ri A 指令 将 [ri] 存储在与内存中第 [A]w-th 字节对齐的字位置。 store.w store.w A ri 指令 已将字存储在其内存中，并与 [A]w 字节对齐到 ri 寄存器中。 load.w load.w ri A 输入相关操作 该指令是唯一可以访问任一磁带的指令。第 0 个磁带用于主输入，第一个磁带用于用户辅助输入。 指令 将 [A] U 磁带上的下一个 W 位字存储到 ri 寄存器中。更准确地说，如果[A]u磁带有剩余字，则将下一个字消耗并存储在ri中，并设置 = 0；否则（如果 [A]u 磁带上没有剩余的输入字），将 0^W 存储到 ri 并设置 = 1。 read read ri A flag flag 由于 TinyRAM 只有两个输入磁带，所有 除了前两个被假定为空。 磁带 具体来说，如果 [A]u 不是 0 或 1，那么我们将 0^W 存储在 ri 中并设置 =1。 flag 输出相关操作 该指令表示程序已完成计算，不允许进行其他操作。 指令 会导致状态机“停止”（不增加pc）或“暂停”（停止计算），并返回[A]u。未定义停止或停止之间的选择。返回值 0 用于表示接受。 回答 answer A 指令集的约束 TinyRAM已经使用R1CS约束来进行电路约束，具体形式如下： (Ai * S) * (Bi * S) - Ci * S = 0 现在，如果我们要证明我们知道原始计算的解，我们需要证明在矩阵A、B和C中，内积值的每个行向量和解向量 都符合R1CS约束 表示矩阵中的行向量）。 S A_i，B_i , C_i 每个 R1CS 约束可以由 linear_combination a、b 或 c 表示。 R1CS系统中所有变量的赋值可以分为两部分：主输入和辅助输入。主要的就是我们常说的“陈述”，辅助就是“见证”。 每个 R1CS 约束系统包含多个 R1CS 约束。每个约束的向量长度是固定的（主输入大小 + 辅助输入大小 + 1）。 TinyRAM 在 libsnark 代码实现中使用了很多自定义小工具来表达 vm 约束以及操作码执行和内存约束。具体代码在gadgetslib1/Gadgets/cpu_checkers/tinyram文件夹中。 位相关约束 约束公式： 和 a * b = c 参数1和参数2的R1CS约束和验证，计算结果是逐位相乘。约束步骤如下： 计算过程约束，代码如下： this->pb.add_r1cs_constraint( r1cs_constraint ( { this->arg1val.bits[i] }, { this->arg2val.bits[i] }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i)); 结果编码约束 计算结果不都是零约束（与指令定义一致，过程主要是准备约束标志） /* the gadgets below are Fp specific: I * X = R (1-R) * X = 0 if X = 0 then R = 0 if X != 0 then R = 1 and I = X^{-1} */ 标志约束 /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); 约束公式： 或 (1 - a) * (1 - b) = (1 - c) 具体约束步骤如下： 计算过程约束，代码如下： this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE, this->arg1val.bits[i] * (-1) }, { ONE, this->arg2val.bits[i] * (-1) }, { ONE, this->res_word[i] * (-1) }), FMT(this->annotation_prefix, " res_word_%zu", i)); 结果编码约束 计算结果不都是零约束（与指令定义一致，这个过程主要是为约束标志做准备） 标志约束 /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); 约束公式： 异或 c = a ^ b c = a + b - 2*a*b, (2*b)*a = a+b - c 具体约束步骤如下： 计算过程约束，代码如下： this->pb.add_r1cs_constraint( r1cs_constraint ( { this->arg1val.bits[i] * 2}, { this->arg2val.bits[i] }, { this->arg1val.bits[i], this->arg2val.bits[i], this->res_word[i] * (-1) }), FMT(this->annotation_prefix, " res_word_%zu", i)); 结果编码约束 计算结果不都是零约束（与指令定义一致，这个过程主要是为约束标志做准备） 标志约束 /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); 约束公式： 非 1 * （1 - b） = c 具体约束步骤如下： this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->arg2val.bits[i] * (-1) }, { this->res_word[i] }), FMT(this->annotation_prefix, " res_word_%zu", i)); 结果编码约束 计算结果不都是零约束（与指令定义一致，这个过程主要是为约束标志做准备） 标志约束 /* result_flag = 1 - not_all_zeros = result is 0^w */ this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { ONE, this->not_all_zeros_result * (-1) }, { this->result_flag }), FMT(this->annotation_prefix, " result_flag")); 整数相关的操作约束 约束公式： 加： 1 * （a + b） = c 具体约束步骤如下： 计算过程约束，代码如下： this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { this->arg1val.packed, this->arg2val.packed }, { this->addition_result }), FMT(this->annotation_prefix, " addition_result")); 解码结果约束和布尔约束 编码结果约束 约束公式： sub： sub 约束比 add 稍微复杂一些，中间变量代表 ab 结果，加上 2^w 保证结果计算为正整数和符号。具体约束步骤如下： intermediate_result = 2^w + a -b 计算过程约束： /* intermediate_result = 2^w + (arg1val - arg2val) */ FieldT twoi = FieldT::one(); linear_combination a, b, c; a.add_term(0, 1); for (size_t i = 0; i pb.ap.w; ++i) { twoi = twoi + twoi; } b.add_term(0, twoi); b.add_term(this->arg1val.packed, 1); b.add_term(this->arg2val.packed, -1); c.add_term(intermediate_result, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a, b, c), FMT(this->annotation_prefix, " main_constraint")); 解码结果约束和布尔约束 符号位约束 约束公式： mull、umulh 和 smulh c = a * b 与Mulll相关的约束都涉及以下步骤： 计算乘法的约束 计算结果编码的约束 计算结果的标志约束 约束公式： udiv 和 umod B * q + r = A r a1, b1, c1; a1.add_term(B_inv, 1); b1.add_term(this->arg2val.packed, 1); c1.add_term(B_nonzero, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a1, b1, c1), FMT(this->annotation_prefix, " B_inv*B=B_nonzero")); /* (1-B_nonzero) * B = 0 */ linear_combination a2, b2, c2; a2.add_term(ONE, 1); a2.add_term(B_nonzero, -1); b2.add_term(this->arg2val.packed, 1); c2.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint (a2, b2, c2), FMT(this->annotation_prefix, " (1-B_nonzero)*B=0")); /* B * q + r = A_aux = A * B_nonzero */ linear_combination a3, b3, c3; a3.add_term(this->arg2val.packed, 1); b3.add_term(udiv_result, 1); c3.add_term(A_aux, 1); c3.add_term(umod_result, -; this->pb.add_r1cs_constraint(r1cs_constraint (a3, b3, c3), FMT(this->annotation_prefix, " B*q+r=A_aux")); linear_combination a4, b4, c4; a4.add_term(this->arg1val.packed, 1); b4.add_term(B_nonzero, 1); c4.add_term(A_aux, 1); this->pb.add_r1cs_constraint(r1cs_constraint (a4, b4, c4), FMT(this->annotation_prefix, " A_aux=A*B_nonzero")); /* q * (1-B_nonzero) = 0 */ linear_combination a5, b5, c5; a5.add_term(udiv_result, 1); b5.add_term(ONE, 1); b5.add_term(B_nonzero, -1); c5.add_term(ONE, 0); this->pb.add_r1cs_constraint(r1cs_constraint (a5, b5, c5), FMT(this->annotation_prefix, " q*B_nonzero=0")); /* A (B, r, less=B_nonzero, leq=ONE) */ r_less_B->generate_r1cs_constraints(); 比较操作 比较操作中的每条指令都不会修改任何寄存器；比较结果存储在 中。比较指令包括 、 、 。 和 ，可以分为有符号数比较和无符号数比较两种，它们的约束过程核心都使用了 实现的compare_gadget。 flag cmpe cmpa cmpae cmpg cmpge comparison_gadget 无符号数比较约束公式： cmpe_flag = cmpae_flag * (1-cmpa_flag) cmp和约束代码如下： comparator.generate_r1cs_constraints(); this->pb.add_r1cs_constraint( r1cs_constraint ( {cmpae_result_flag}, {ONE, cmpa_result_flag * (-1)}, {cmpe_result_flag}), FMT(this->annotation_prefix, " cmpa_result_flag")); 有符号数比较约束公式： 无符号数约束比有符号数比较约束更复杂，因为符号位约束处理更多。 符号位约束如下： /* negate sign bits */ this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {ONE, this->arg1val.bits[this->pb.ap.w - 1] * (-1)}, {negated_arg1val_sign}), FMT(this->annotation_prefix, " negated_arg1val_sign")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {ONE, this->arg2val.bits[this->pb.ap.w - 1] * (-1)}, {negated_arg2val_sign}), FMT(this->annotation_prefix, " negated_arg2val_sign")); 其余步骤与有符号数比较约束相同。 移动操作约束 约束公式： mov mov 约束比较简单，因为它只需要保证 [A] 存储在 ri 寄存器中。 mov 操作不会修改 ，所以约束需要保证 flag 值不改变。约束代码如下： flag this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->arg2val.packed}, {this->result}), FMT(this->annotation_prefix, " mov_result")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " mov_result_flag")); 约束公式： cmov flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval cmov的约束条件比mov复杂，因为mov的行为与flag值的变化有关，cmov不会修改flag，所以约束需要保证flag的值不变，并且 代码如下： /* flag1 * arg2val + (1-flag1) * desval = result flag1 * (arg2val - desval) = result - desval */ this->pb.add_r1cs_constraint( r1cs_constraint ( {this->flag}, {this->arg2val.packed, this->desval.packed * (-1)}, {this->result, this->desval.packed * (-1)}), FMT(this->annotation_prefix, " cmov_result")); this->pb.add_r1cs_constraint( r1cs_constraint ( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " cmov_result_flag")); 跳转操作约束 这些跳转和条件跳转指令不会修改寄存器和 ，但会修改 。 flag pc 跳转 pc值与Jmp操作约束中指令的执行结果一致，具体约束代码如下： this->pb.add_r1cs_constraint( r1cs_constraint ( { ONE }, { pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())) }, { this->result }), FMT(this->annotation_prefix, " jmp_result")); cjmp 当 flag = 1 时 cjmp 将根据标志条件跳转，否则将 pc 加 1。 约束公式如下： flag1 * argval2 + (1-flag1) * (pc1 + 1) = cjmp_result flag1 * (argval2 - pc1 - 1) = cjmp_result - pc1 - 1 约束代码如下： this->pb.add_r1cs_constraint( r1cs_constraint ( this->flag, pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())) - this->pc.packed - 1, this->result - this->pc.packed - 1), FMT(this->annotation_prefix, " cjmp_result")); cnjmp cnjmp 会根据标志条件跳转。如果 flag = 0，则 PC 跳转，否则，将 pc 递增 1。 约束公式如下： flag1 * (pc1 + 1) + (1-flag1) * argval2 = cnjmp_result flag1 * (pc1 + 1 - argval2) = cnjmp_result - argval2 约束代码如下： this->pb.add_r1cs_constraint( r1cs_constraint ( this->flag, this->pc.packed + 1 - pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())), this->result - pb_packing_sum (pb_variable_array (this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end()))), FMT(this->annotation_prefix, " cnjmp_result")); 内存操作约束 这些是简单的内存加载和存储操作，其中内存地址由立即数或寄存器的内容确定。 这些是 TinyRAM 中唯一的寻址方法。 （TinyRAM 不支持常见的“base+offset”寻址模式）。 和 store.b store.w 对于 store.w，取 arg1val 的所有值，对于 store.b 操作码，只取 arg1val 的必要部分（例如，最后一个字节），约束代码如下： this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_STOREW], memory_subcontents - desval->packed, 0), FMT(this->annotation_prefix, " handle_storew")); this->pb.add_r1cs_constraint(r1cs_constraint (1 - (opcode_indicators[tinyram_opcode_STOREB] + opcode_indicators[tinyram_opcode_STOREW]), ls_prev_val_as_doubleword_variable->packed - ls_next_val_as_doubleword_variable->packed, 0), FMT(this->annotation_prefix, " non_store_instructions_dont_change_memory")); 和 load.b load.w 对于这两条指令，我们要求将从内存中加载的内容存放在instruction_results中，约束代码如下： this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_LOADB], memory_subcontents - instruction_results[tinyram_opcode_LOADB], 0), FMT(this->annotation_prefix, " handle_loadb")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_LOADW], memory_subcontents - instruction_results[tinyram_opcode_LOADW], 0), FMT(this->annotation_prefix, " handle_loadw")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_STOREB], memory_subcontents - pb_packing_sum ( pb_variable_array (desval->bits.begin(), desval->bits.begin() + 8)), 0), FMT(this->annotation_prefix, " handle_storeb")); 输入操作约束 读 读操作与磁带有关，具体约束如下： 当上一盘磁带用完并且有内容要读取时，不允许再读下一盘磁带。 当上一个磁带完成并且有内容要读取时， 设置为 1 flag 如果现在执行 指令，则读到的内容与磁带的输入内容一致 read 从 type1 外部读取内容， 设置为 1 flag 是否为0表示 为0 result flag 约束代码： this->pb.add_r1cs_constraint(r1cs_constraint (prev_tape1_exhausted, 1 - next_tape1_exhausted, 0), FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_next_tape1_exhausted")); this->pb.add_r1cs_constraint(r1cs_constraint (prev_tape1_exhausted, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " prev_tape1_exhausted_implies_flag")); this->pb.add_r1cs_constraint(r1cs_constraint (opcode_indicators[tinyram_opcode_READ], 1 - arg2val->packed, read_not1), FMT(this->annotation_prefix, " read_not1")); this->pb.add_r1cs_constraint(r1cs_constraint (read_not1, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " other_reads_imply_flag")); this->pb.add_r1cs_constraint(r1cs_constraint (instruction_flags[tinyram_opcode_READ], instruction_results[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " read_flag_implies_result_0")); 输出操作约束 该指令表示程序已完成计算，因此不允许进一步操作 回答 当程序的输出值被接受时，has_accepted设置为1，程序的返回值被正常接受，即当前指令为 ，arg2值为0。 answer 约束代码如下： this->pb.add_r1cs_constraint(r1cs_constraint (next_has_accepted, 1 - opcode_indicators[tinyram_opcode_ANSWER], 0), FMT(this->annotation_prefix, " accepting_requires_answer")); this->pb.add_r1cs_constraint(r1cs_constraint (next_has_accepted, arg2val->packed, 0), FMT(this->annotation_prefix, " accepting_requires_arg2val_equal_zero")); 其他 当然，除了上面提到的一些指令相关的约束外，TinyRAM还对pc一致性、参数编解码、内存检查等有一些约束，这些约束通过R1CS系统组合起来，形成一个完整的TinyRAM约束系统。因此，这就是为什么会以 R1CS 的形式生成大量 TinyRAM 约束的根本原因。 这里我们参考一张 的图，展示了一个 ERC20 转账通过 TinyRAM 生成证明所需的时间。 tinyram review ppt 从上面的例子可以得出结论：vnTinyRam + zk-SNARks 无法验证所有的 EVM 操作，只适合少量指令的计算验证。 vnTinyram 可用于验证 EVM 的部分计算类型的操作码。