1,096 讀數

什么是 TinyRAM 指令集？

经过 Sin7Y2022/06/21

太長; 讀書

TinyRAM 是一种简单的精简指令集计算机 (RISC)，具有字节级可寻址随机存取存储器和输入磁带。 TinyRAM 有两种变体：一种遵循哈佛 (hv) 架构，另一种遵循冯诺依曼 (vn) 架构。 TinyRAM 支持 29 条指令，每条指令由一个操作码和最多 3 个操作数指定。

Companies Mentioned

Coin Mentioned

介绍

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。

通常，第一个操作数是指令计算的目标寄存器，其他操作数指定指令所需的参数。最后，所有指令都需要一个机器周期来执行。

位相关操作

and : 指令and ri rj A将 [rj] 和 [A] 的位和结果存储在 ri 寄存器中。同样，如果结果为0^{W} ，则将flag设置为 1，否则将其设置为 0。
or指令or ri rj A将 [rj] 和 [A] 的位和结果存储在 ri 寄存器中。同样，如果结果为0^{W} ，则将flag设置为 1，否则将其设置为 0。
xor指令xor ri rj A将 [rj] 和 [A] 的位和结果存储在 ri 寄存器中。同样，如果结果为0^{W} ，则将flag设置为 1，否则将其设置为 0。
not指令not ri A将 [rj] 和 [A] 的位和结果存储在 ri 寄存器中。同样，如果结果为0^{W} ，则将flag设置为 1，否则将其设置为 0。

整数相关操作

这些是各种无符号和有符号整数相关操作。在每个设置中，如果发生算术溢出或错误（例如除以零），则将flag设置为 1 ，否则将其设置为 0。

下面的部分， U_{W}代表一系列整数{0*,…,* $2^{W} -1 $}；这些整数由 W 位字符串组成。 S_{W}表示一系列整数 {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1。这些整数也由 W 位字符串组成。

add：指令add ri rj A将 W 位串 a_{W−1}⋯a_{0} 存入 ri。 a_{W−1}⋯a_{0} 是G = [rj]_u + [A]_u的 W 最低有效位 (LSB)。此外， flag将设置为G_{W} 。 G_{W}是 G 的最高有效位 (MSB)。
sub：指令sub ri rj A将W位串a_{W−1}⋯a_{0}存入ri。 a_{W−1}⋯a_{0} 是G = [rj]_u + 2^W - [A]_u的 W 最低有效位 (LSB)。此外， flag将被设置为1−G_{W} 。 G_{W}是 G 的最高有效位 (MSB)。
mull指令mull ri rj A将 W 位串 a_{W−1}⋯a_{0} 存储到 ri 中。 a_{W−1}⋯a_{0} 是G=[rj]_u∗[A]_u的 W 最低有效位 (LSB)。此外， flag将被设置为 1，如果
[rj]_u × [A] u ∉ U {W} ，否则设为 0。
umulh指令umulh ri rj A将 W 位串 a_{W−1}⋯a_{0} 存储到 ri 中。 a_{W−1}⋯a_{0} 是G = [rj]_u ∗ [A]_u的 W 最高有效位 (MSB)。此外，如果[rj]_u × [A] u ∉ U {W} ，则flag将设置为 1，否则将其设置为 0。
smulh指令smulh ri rj A将 W 位串 a_{W−1}⋯a_{0} 存入 ri。 a_{W−1} 是[rj] u ∗ [A]_u 的符号位，a {W−2}⋯a{0}是[rj]_u ∗ [A]_u的 W - 1 MSB。此外，如果[rj]_u × [A] u ∉ S {W } ，则flag将设置为 1，否则将其设置为 0。

udiv指令udiv ri rj A将 W 位串 a_{W−1}⋯a_{0} 存储到 ri 中。

如果[A] u = 0，则 {W−1}⋯a_{0} = 0^W 。

如果[A] u∣ ≠ 0，则{W−1}⋯a_{0}是整数 Q 的唯一二进制编码，使得对于某些整数R ∈ {0,…,[A]_u − 1} ，公式[rj]_u = [A]_u × Q + R是可行的。此外，只有当[A]_u=0时， flag才会被设置为 1。

umod指令umod ri rj A将 W 位串 a_{W−1}⋯a_{0} 存入 ri。

如果[A] u = 0，则 {W−1}⋯a_{0} = 0^W 。

若[A] u∣ ≠ 0，则a {W−1}⋯a_{0}是整数R的唯一二进制编码，其取值范围为

{0,…,[A]_u−1} ，使得公式[rj]_u = [A]_u × Q+R可用于某些 Q 值。此外，只有当[A]_u = 0时， flag才会被设置为 1。

班次相关操作

shl指令shl ri rj A将[rj] 左移[A] u 位得到的W 位串存储在ri 寄存器中。移位后的空白位置用0填充。另外，flag设置为[rj]的MSB。
shr指令shr ri rj A将[rj] 右移[A] u 位得到的W 位串存储在ri 寄存器中。移位后的空白位置用0填充。另外，flag设置为[rj]的LSB。

比较相关的操作

比较相关操作中的每条指令都不会修改任何寄存器；比较结果将存储在flag中。

cmpe指令cmpe ri A如果 [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则将 flag 设置为 1，否则将其设置为 0

移动相关操作

mov指令mov ri A将 [A] 存储到 ri 寄存器中。
如果 flag = 1， cmov指令cmov ri A会将 [A] 存储到 ri 寄存器中，否则 ri 寄存器的值不会改变。

跳跃相关

这些跳转和条件跳转指令不会修改寄存器和flag ，但会修改pc 。

跳转指令jmp A将 [A] 存储到 pc 中。
cjmp指令cjmp A将在flag = 1 时将 [A] 存储到 pc 中，否则将 pc 递增 1
cnjmp指令cnjmp A在flag = 0 时将 [A] 存储到 pc 中，否则将 pc 加 1

内存相关操作

这些是简单的内存加载操作和存储操作，其中内存的地址由立即数或寄存器的内容决定。

这些是 TinyRAM 中唯一的寻址方法。（TinyRAM 不支持常见的“base+offset”寻址模式）。

store.b指令store A ri将 [ri] 的 LSB 存储在内存中的 [A] U-th 字节地址。
load.b指令load ri A将内存中第[A]个U字节地址的内容存入ri寄存器（前面字节填充0）。
store.w指令store.w A ri将 [ri] 存储在与内存中第 [A]w-th 字节对齐的字位置。
load.w指令load.w ri A已将字存储在其内存中，并与 [A]w 字节对齐到 ri 寄存器中。

输入相关操作

该指令是唯一可以访问任一磁带的指令。第 0 个磁带用于主输入，第一个磁带用于用户辅助输入。

read指令read ri A将 [A] U 磁带上的下一个 W 位字存储到 ri 寄存器中。更准确地说，如果[A]u磁带有剩余字，则将下一个字消耗并存储在ri中，并设置flag = 0；否则（如果 [A]u 磁带上没有剩余的输入字），将 0^W 存储到 ri 并设置flag = 1。

由于 TinyRAM 只有两个输入磁带，所有磁带除了前两个被假定为空。

具体来说，如果 [A]u 不是 0 或 1，那么我们将 0^W 存储在 ri 中并设置flag =1。

输出相关操作

该指令表示程序已完成计算，不允许进行其他操作。

回答指令answer A会导致状态机“停止”（不增加pc）或“暂停”（停止计算），并返回[A]u。未定义停止或停止之间的选择。返回值 0 用于表示接受。

指令集的约束

TinyRAM已经使用R1CS约束来进行电路约束，具体形式如下：

(Ai * S) * (Bi * S) - Ci * S = 0

现在，如果我们要证明我们知道原始计算的解，我们需要证明在矩阵A、B和C中，内积值的每个行向量和解向量S都符合R1CS约束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<FieldT>( { 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<FieldT>( { 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<FieldT>( { 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<FieldT>( { 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<FieldT>( { 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<FieldT>( { 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<FieldT>( { 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<FieldT>( { 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<FieldT>( { 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<FieldT> a, b, c; a.add_term(0, 1); for (size_t i = 0; i < this->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<FieldT>(a, b, c), FMT(this->annotation_prefix, " main_constraint"));

解码结果约束和布尔约束
符号位约束

mull、umulh 和 smulh约束公式：
```
 c = a * b
```
与Mulll相关的约束都涉及以下步骤：
1. 计算乘法的约束
2. 计算结果编码的约束
3. 计算结果的标志约束
udiv 和 umod约束公式：

 B * q + r = A r <= B

“B”是除数，“q”是商，“r”是余数。余数不得超过除数。具体约束代码如下：

 /* B_inv * B = B_nonzero */ linear_combination<FieldT> 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<FieldT>(a1, b1, c1), FMT(this->annotation_prefix, " B_inv*B=B_nonzero")); /* (1-B_nonzero) * B = 0 */ linear_combination<FieldT> 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<FieldT>(a2, b2, c2), FMT(this->annotation_prefix, " (1-B_nonzero)*B=0")); /* B * q + r = A_aux = A * B_nonzero */ linear_combination<FieldT> 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<FieldT>(a3, b3, c3), FMT(this->annotation_prefix, " B*q+r=A_aux")); linear_combination<FieldT> 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<FieldT>(a4, b4, c4), FMT(this->annotation_prefix, " A_aux=A*B_nonzero")); /* q * (1-B_nonzero) = 0 */ linear_combination<FieldT> 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<FieldT>(a5, b5, c5), FMT(this->annotation_prefix, " q*B_nonzero=0")); /* A<B_gadget<FieldT>(B, r, less=B_nonzero, leq=ONE) */ r_less_B->generate_r1cs_constraints();

比较操作

比较操作中的每条指令都不会修改任何寄存器；比较结果存储在flag中。比较指令包括cmpe 、 cmpa 、 cmpae 。 cmpg和cmpge ，可以分为有符号数比较和无符号数比较两种，它们的约束过程核心都使用了comparison_gadget实现的compare_gadget。

无符号数比较约束公式：

 cmpe_flag = cmpae_flag * (1-cmpa_flag)

cmp和约束代码如下：

 comparator.generate_r1cs_constraints(); this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( {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<FieldT>( {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<FieldT>( {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<FieldT>( {ONE}, {this->arg2val.packed}, {this->result}), FMT(this->annotation_prefix, " mov_result")); this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( {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<FieldT>( {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<FieldT>( {ONE}, {this->flag}, {this->result_flag}), FMT(this->annotation_prefix, " cmov_result_flag"));

跳转操作约束

这些跳转和条件跳转指令不会修改寄存器和flag ，但会修改pc 。

跳转

pc值与Jmp操作约束中指令的执行结果一致，具体约束代码如下：

 this->pb.add_r1cs_constraint( r1cs_constraint<FieldT>( { ONE }, { pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>( this->flag, pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>( this->flag, this->pc.packed + 1 - pb_packing_sum<FieldT>(pb_variable_array<FieldT>(this->argval2.bits.begin() + this->pb.ap.subaddr_len(), this->argval2.bits.end())), this->result - pb_packing_sum<FieldT>(pb_variable_array<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_STOREW], memory_subcontents - desval->packed, 0), FMT(this->annotation_prefix, " handle_storew")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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<FieldT>(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<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_STOREB], memory_subcontents - pb_packing_sum<FieldT>( pb_variable_array<FieldT>(desval->bits.begin(), desval->bits.begin() + 8)), 0), FMT(this->annotation_prefix, " handle_storeb"));

输入操作约束

读
读操作与磁带有关，具体约束如下：

当上一盘磁带用完并且有内容要读取时，不允许再读下一盘磁带。
当上一个磁带完成并且有内容要读取时， flag设置为 1
如果现在执行read指令，则读到的内容与磁带的输入内容一致
从 type1 外部读取内容， flag设置为 1
result是否为0表示flag为0

约束代码：

 this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(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<FieldT>(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<FieldT>(opcode_indicators[tinyram_opcode_READ], 1 - arg2val->packed, read_not1), FMT(this->annotation_prefix, " read_not1")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(read_not1, 1 - instruction_flags[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " other_reads_imply_flag")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(instruction_flags[tinyram_opcode_READ], instruction_results[tinyram_opcode_READ], 0), FMT(this->annotation_prefix, " read_flag_implies_result_0"));

输出操作约束

该指令表示程序已完成计算，因此不允许进一步操作

回答

当程序的输出值被接受时，has_accepted设置为1，程序的返回值被正常接受，即当前指令为answer ，arg2值为0。

约束代码如下：

 this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(next_has_accepted, 1 - opcode_indicators[tinyram_opcode_ANSWER], 0), FMT(this->annotation_prefix, " accepting_requires_answer")); this->pb.add_r1cs_constraint(r1cs_constraint<FieldT>(next_has_accepted, arg2val->packed, 0), FMT(this->annotation_prefix, " accepting_requires_arg2val_equal_zero"));