TinyRAM 命令セットとは何ですか?

序章 TinyRAM は、バイト レベルのアドレス指定可能なランダム アクセス メモリと入力テープを備えた単純な縮小命令セット コンピュータ (RISC) です。 TinyRAM には 2 つのバリアントがあります。1 つはハーバード (hv) アーキテクチャに準拠しており、もう 1 つはフォン ノイマン (vn) アーキテクチャに準拠しています (この記事では主にフォン ノイマン アーキテクチャに焦点を当てています)。 Succinct Computational Integrity and Privacy Research (SCIPR) プロジェクトは、TinyRAM プログラムの正しい実行を証明するためのメカニズムを構築しており、TinyRAM はこの設定で効率的に設計されています。これは、「十分な表現性」と「小さな命令セット」という相反する 2 つの要件の間でバランスをとっています。 高水準プログラミング言語からコンパイルされたときに、短くて効率的なアセンブリ コードをサポートするのに十分な表現力。 演算回路による簡単な検証と、SCIPR のアルゴリズムと暗号化メカニズムを使用した効率的な検証をサポートする小さな命令セット。 この記事では、TinyRAM の紹介を繰り返すのではなく、前回の記事を補足し、命令と回路の制約の紹介に焦点を当てます。 TinyRAM の基本的な紹介については、以前の記事を参照してください: tinyram简介-中文 TinyRAM レビュー-英語 TinyRAM 命令セット TinyRAM は 29 の命令をサポートし、それぞれがオペコードと最大 3 つのオペランドによって指定されます。オペランドは、レジスタの名前 (つまり、0 ～ K-1 の整数) または即値 (つまり、W ビット文字列) のいずれかです。 特に指定しない限り、各命令はフラグを個別に変更せず、デフォルトで pc を i (i % 2^W) だけインクリメントします。vnTinyRAM の場合、i=2W/8 です。 一般に、最初のオペランドは命令計算のターゲット レジスタであり、他のオペランドは命令に必要なパラメータを指定します。最後に、すべての命令の実行にはマシンの 1 サイクルが必要です。 ビット関連の操作 : 命令 は、[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 instruction は、[rj] と [A] のビットと結果を ri レジスタに格納します。同様に、結果が の場合は を 1 に設定し、それ以外の場合は 0 に設定します。 not not ri A 0^{W} flag 整数関連の操作 これらは、さまざまな符号なしおよび符号付き整数関連の操作です。各設定で、算術オーバーフローまたはエラー (0 による除算など) が発生した場合は を 1 に設定し、それ以外の場合は 0 に設定します。 flag 次の部分では、 は一連の整数 {0*,…,* $2^{W} -1 $} を表します。これらの整数は、W ビットの文字列で構成されます。 は一連の整数 {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1 を表します。これらの整数も W ビット文字列で構成されます。 U_{W} S_{W} instruction は、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} instruction は、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 instruction は、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 instruction は、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 flag [rj]_u × [A] {W u ∉ S 命令 は、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 の場合、 は整数 R の唯一のバイナリ エンコーディングであり、 により、式 が一部の Q 値に対して有効になります。また、 場合のみ、 が 1 に設定されます。 {0,…,[A]_u−1} [rj]_u = [A]_u × Q+R [A]_u = 0 の flag シフト関連の操作 命令 は、[rj] 左シフトによって得られた W ビット列を [A] u ビットだけ ri レジスタに格納します。シフト後の空白位置は 0 で埋められます。また、フラグは [rj] の MSB に設定されます。 shl shl ri rj A 命令 は、[rj] を [A] u ビット右シフトして得られた W ビット列を ri レジスタに格納します。シフト後の空白位置は 0 で埋められます。また、フラグは [rj] の LSB に設定されます。 shr shr ri rj A コンペア関連の操作 比較関連操作の各命令は、レジスタを変更しません。比較結果は に格納されます。 flag 命令 は、[ri] = [A] の場合はフラグを 1 に設定し、それ以外の場合は 0 に設定します。 cmpe cmpe ri A instruction は、 場合はフラグを 1 に設定し、それ以外の場合は 0 に設定します cmpa cmpa ri A [ri]_u > [A]_u の 命令 は、 場合、フラグを 1 に設定し、それ以外の場合は 0 に設定します。 cmpae cmpae ri A [ri]_u ≥ [A]_u の instruction は、 場合はフラグを 1 に設定し、それ以外の場合は 0 に設定します cmpg cmpg ri A [ri]_s > [A]_s の instruction は、 _S の場合はフラグを 1 に設定し、それ以外の場合は 0 に設定します cmpge cmpge ri A [ri]_S ≥ [A] 移動関連操作 命令 は [A] を ri レジスタに格納します。 mov mov ri A 命令 は、フラグ = 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 は一般的な「ベース + オフセット」アドレッシング モードをサポートしていません)。 instruction は、[ri] の LSB をメモリの [A] U 番目のバイト アドレスに格納します。 store.b store A ri 命令 は、メモリ内の [A] U 番目のバイト アドレスの内容を ri レジスタに格納します (先頭バイトに 0 を埋めます)。 load.b load ri A 命令 は、メモリ内の [A]w 番目のバイトにアラインされたワード位置に [ri] を格納します。 store.w store.w A ri 命令 は、メモリ内のワードを [A]w バイトに合わせて ri レジスタに格納しました。 load.w load.w ri A 入力関連の操作 この命令は、いずれかのテープにアクセスできる唯一の命令です。 0 番目のテープはプライマリ入力に使用され、最初のテープはユーザー補助入力に使用されました。 instruction は、[A] U テープの次の W ビット ワードを ri レジスタに格納します。より正確には、[A]u テープに残りの単語がある場合、次の単語が消費されて ri に格納され、 = 0 に設定されます。それ以外の場合 ([A]u テープに残りの入力単語がない場合)、0^W を ri に格納し、 = 1 を設定します。 read read ri A flag flag TinyRAM には 2 つの入力テープしかないため、すべて ただし、最初の 2 つは空であると見なされます。 テープ 具体的には、[A]u が 0 でも 1 でもない場合、ri に 0^W を格納し、 =1 を設定します。 flag 出力関連の操作 この命令は、プログラムが計算を終了し、他の操作が許可されていないことを意味します。 instruction は、ステート マシンを「ストール」（pc の増加なし）または「停止」（計算を停止）させ、[A]u に戻ります。ストールまたは停止の選択は定義されていません。戻り値 0 は、受け入れを示すために使用されます。 answer 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 システムのすべての変数の割り当ては、主入力と補助入力の 2 つの部分に分けることができます。主なものは私たちがしばしば「声明」と呼ぶものであり、補助的なものは「証人」です。 各 R1CS 制約システムには、複数の R1CS 制約が含まれています。各制約のベクトルの長さは固定されています (プライマリ入力サイズ + 補助入力サイズ + 1)。 TinyRAM は、libsnark コードの実装で多くのカスタム ガジェットを使用して、vm の制約、opcode の実行、およびメモリの制約を表現しています。特定のコードは、gadgetslib1/ Gadgets /cpu_checkers/tinyram フォルダーにあります。 ビット関連の制約 制約式: および a * b = c および の R1CS 制約は、パラメーター 1 とパラメーター 2 を検証し、計算結果はビットごとの乗算になります。制約の手順は次のとおりです。 計算プロセスの制約、およびコードは次のとおりです。 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")); 制約式: xor 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 制約は 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 Mull 関連のすべての制約には、次の手順が含まれます。 乗算計算の制約 計算結果コーディングの制約 計算結果のフラグ制約 制約式: 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(); 比較操作 比較操作の各命令は、どのレジスタも変更しません。比較結果は に格納されます。比較命令には 、 、 が含まれます。 と は、符号付き数値比較と符号なし数値比較の 2 つのタイプに分けることができます。どちらも、制約プロセス コアで libsnark の実現された を使用します。 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")); 残りの手順は、符号付き数値比較制約と同じです。 移動操作の制約 制約式: 移動 [A] が ri レジスタに格納されていることを確認するだけでよいため、mov 制約は比較的単純です。 mov 操作は を変更しないため、制約はフラグ値が変更されないようにする必要があります。制約コードは次のとおりです。 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 の動作はフラグ値の変更に関連しており、cmov はフラグを変更しないため、制約はフラグの値が変更されないようにする必要があります。 コードは次のとおりです。 /* 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 jmp 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 cjmp は flag = 1 の場合はフラグの条件に従ってジャンプし、それ以外の場合は 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 は一般的な「ベース + オフセット」アドレッシング モードをサポートしていません)。 と 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 これら 2 つの命令では、メモリからロードされた内容を 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 制約システムを形成します。したがって、これが、多数の TinyRAM 制約が R1CS の形で生成される根本的な原因です。 ここで、 の図を参照します。これは、ERC20 転送が TinyRAM を介してプルーフを生成するのに必要な時間を示しています。 tinyram レビュー ppt 上記の例から、vnTinyRam + zk-SNARks を使用してすべての EVM 操作を検証することは不可能であり、少数の命令の計算検証にのみ適していると結論付けることができます。 vnTinyram を使用して、EVM の部分計算タイプのオペコードを検証できます。