1,087 測定値

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

に Sin7Y2022/06/21

長すぎる; 読むには

TinyRAM は、バイトレベルのアドレス指定可能なランダムアクセスメモリと入力テープを備えた単純な縮小命令セットコンピュータ (RISC) です。 TinyRAM には 2 つのバリアントがあります。1 つは Harvard (hv) アーキテクチャに準拠し、もう 1 つは von Neumann (vn) アーキテクチャに準拠しています。 TinyRAM は 29 の命令をサポートし、それぞれがオペコードと最大 3 つのオペランドで指定されます。

Companies Mentioned

Coin Mentioned

序章

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 サイクルが必要です。

ビット関連の操作

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 instruction not ri Aは、[rj] と [A] のビットと結果を ri レジスタに格納します。同様に、結果が0^{W}の場合はflagを 1 に設定し、それ以外の場合は 0 に設定します。

整数関連の操作

これらは、さまざまな符号なしおよび符号付き整数関連の操作です。各設定で、算術オーバーフローまたはエラー (0 による除算など) が発生した場合はflagを 1 に設定し、それ以外の場合は 0 に設定します。

次の部分では、 U_{W}は一連の整数 {0*,…,* $2^{W} -1 $} を表します。これらの整数は、W ビットの文字列で構成されます。 S_{W}は一連の整数 {−2^(W−1),… 0, 1, $2 ^ $} {} W - 1-1 を表します。これらの整数も W ビット文字列で構成されます。

add: instruction 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: instruction 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 instruction 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 instruction 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 です。また、 flagは[rj]_u × [A] u ∉ S {W } の場合は 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 の場合、 {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] 左シフトによって得られた W ビット列を [A] u ビットだけ ri レジスタに格納します。シフト後の空白位置は 0 で埋められます。また、フラグは [rj] の MSB に設定されます。
shr命令shr ri rj Aは、[rj] を [A] u ビット右シフトして得られた W ビット列を ri レジスタに格納します。シフト後の空白位置は 0 で埋められます。また、フラグは [rj] の LSB に設定されます。

コンペア関連の操作

比較関連操作の各命令は、レジスタを変更しません。比較結果はflagに格納されます。

cmpe命令cmpe ri Aは、[ri] = [A] の場合はフラグを 1 に設定し、それ以外の場合は 0 に設定します。
cmpa instruction cmpa ri Aは、 [ri]_u > [A]_u の場合はフラグを 1 に設定し、それ以外の場合は 0 に設定します
cmpae命令cmpae ri Aは、 [ri]_u ≥ [A]_u の場合、フラグを 1 に設定し、それ以外の場合は 0 に設定します。
cmpg instruction cmpg ri Aは、 [ri]_s > [A]_s の場合はフラグを 1 に設定し、それ以外の場合は 0 に設定します
cmpge instruction cmpge ri Aは、 [ri]_S ≥ [A] _S の場合はフラグを 1 に設定し、それ以外の場合は 0 に設定します

移動関連操作

mov命令mov ri Aは [A] を ri レジスタに格納します。
cmov命令cmov ri Aは、フラグ = 1 の場合、[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 は一般的な「ベース + オフセット」アドレッシングモードをサポートしていません)。

store.b instruction store A riは、[ri] の LSB をメモリの [A] U 番目のバイトアドレスに格納します。
load.b命令load ri Aは、メモリ内の [A] U 番目のバイトアドレスの内容を ri レジスタに格納します (先頭バイトに 0 を埋めます)。
store.w命令store.w A riは、メモリ内の [A]w 番目のバイトにアラインされたワード位置に [ri] を格納します。
load.w命令load.w ri Aは、メモリ内のワードを [A]w バイトに合わせて ri レジスタに格納しました。

入力関連の操作

この命令は、いずれかのテープにアクセスできる唯一の命令です。 0 番目のテープはプライマリ入力に使用され、最初のテープはユーザー補助入力に使用されました。

read instruction read ri Aは、[A] U テープの次の W ビットワードを ri レジスタに格納します。より正確には、[A]u テープに残りの単語がある場合、次の単語が消費されて ri に格納され、 flag = 0 に設定されます。それ以外の場合 ([A]u テープに残りの入力単語がない場合)、0^W を ri に格納し、 flag = 1 を設定します。

TinyRAM には 2 つの入力テープしかないため、すべてテープただし、最初の 2 つは空であると見なされます。

具体的には、[A]u が 0 でも 1 でもない場合、ri に 0^W を格納し、 flag =1 を設定します。

出力関連の操作

この命令は、プログラムが計算を終了し、他の操作が許可されていないことを意味します。

answer instruction 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 システムのすべての変数の割り当ては、主入力と補助入力の 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<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"));

xor制約式:

 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 制約は 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
```
Mull 関連のすべての制約には、次の手順が含まれます。
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は、符号付き数値比較と符号なし数値比較の 2 つのタイプに分けることができます。どちらも、制約プロセスコアで libsnark の実現されたcomparison_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"));

残りの手順は、符号付き数値比較制約と同じです。

移動操作の制約

移動制約式:

[A] が ri レジスタに格納されていることを確認するだけでよいため、mov 制約は比較的単純です。 mov 操作は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 の動作はフラグ値の変更に関連しており、cmov はフラグを変更しないため、制約はフラグの値が変更されないようにする必要があります。コードは次のとおりです。

 /* 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を変更します。

jmp

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

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<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 は一般的な「ベース + オフセット」アドレッシングモードをサポートしていません)。

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

これら 2 つの命令では、メモリからロードされた内容を 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"));

他の

もちろん、上記の命令関連の制約に加えて、TinyRAM には PC の一貫性、パラメータコーデック、メモリチェックなどに関する制約もあります。これらの制約は R1CS システムを介して結合され、完全な TinyRAM 制約システムを形成します。したがって、これが、多数の TinyRAM 制約が R1CS の形で生成される根本的な原因です。

ここで、 tinyram レビュー pptの図を参照します。これは、ERC20 転送が TinyRAM を介してプルーフを生成するのに必要な時間を示しています。