TinyRam 命令セットと回路制約
導入
最初のレベルのタイトル
導入
Tinyram は、バイトアドレス指定可能なランダム アクセス メモリと入力テープを備えたシンプルな RISC ランダム アクセス マシンです。 TinyRAM には 2 つのバリアントがあります。1 つはハーバード アーキテクチャに準拠し、もう 1 つはフォン ノイマン アーキテクチャに準拠しています (この記事では主にフォン ノイマン アーキテクチャについて説明します)。
Concise Computational Integrity and Privacy Research (SCIPR) プロジェクトは、TinyRAM プログラムの正しい実行を証明するメカニズムを構築し、TinyRAM はこの場合に効率的になるように設計されました。 「十分な表現力」と「十分なシンプルさ」という相反するもののバランスをとります。
• 高級プログラミング言語からコンパイルした場合に、短く効率的なアセンブリ コードをサポートする十分な表現力。TinyRam の紹介
TinyRam の紹介
最初のレベルのタイトル
Tinyram 命令セット
Tinyram には合計 29 個の命令があり、各命令は 1 つのオペコードと最大 3 つのオペランドで構成されます。オペランドには、レジスタの名前 (0 から K-1 までの整数) または即値 (W ビットの文字列) を指定できます。特に指定がない限り、命令はフラグを個別に変更しません。 vnTinyram i= 2W/8 の場合、各命令はデフォルトで pc を i (i % 2^W) ずつ増加させます。
一般に、最初のオペランドは命令計算のターゲット レジスタであり、他のオペランドは命令に必要なパラメータを指定し、最後にすべての命令の実行にはマシンの 1 サイクルが必要です。
ビット操作
整数演算
• shlこれらは、さまざまな符号なし整数演算と符号付き整数演算です。いずれの場合も、算術オーバーフローまたはエラー (ゼロ除算など) が発生した場合は flag が 1 に設定され、それ以外の場合は 0 に設定されます。
• shrシフト操作
命令 shl ri rj A は、[rj] を [A]u ビットだけ左シフトすることによって得られた W ビット列を ri レジスタに格納します。シフト後の空の位置は 0 で埋められます。さらに、[rj] の最上位ビットに flag が設定されます。
命令 shr ri rj A は、[rj] を [A]u ビット右シフトして得られた W ビット列を ri レジスタに格納します。シフト後の空の位置は 0 で埋められます。また、[rj]の最下位ビットにはflagが設定されます。
比較演算
• mov比較演算の各命令はレジスタを変更せず、比較結果は flag に格納されます。
• cmov移動操作
命令 mov ri A は、[A] を ri レジスタに格納します。
命令 cmov ri A flag = 1 の場合、[A] を ri レジスタに格納します。それ以外の場合、ri レジスタの値は変更されません。
• jmpジャンプ操作
• cjmpこれらのジャンプ命令と条件付きジャンプ命令はレジスタやフラグを変更しませんが、pc を変更します。
• cnjmp jmp A 命令は [A] を PC に格納します。
cjmp A命令は、flag = 1の条件で[A]をpcに格納し、それ以外の場合はpcを1インクリメントします。
cnjmp A命令は、flag = 0の条件で[A]をpcに格納し、それ以外の場合はpcを1インクリメントします。
メモリ操作
これらは単純なメモリのロードおよびストア操作であり、メモリのアドレスは即値またはレジスタの内容によって決定されます。これらは tinyram の唯一のアドレッシング モードです。 (tinyram は一般的な「ベース + オフセット」アドレッシング モードをサポートしていません)。
入力操作
出力動作
この命令は、プログラムが計算を終了したため、それ以上の操作が許可されないことを示します。
最初のレベルのタイトル
命令セットの制約
Tinyram は回路制約に R1CS 制約形式を使用します。具体的な形式は次のとおりです。
R1CS 制約には、a、b、および c の 3 つの線形組み合わせ表現を含めることができます。R1CS システム内のすべての変数の割り当ては、主入力と補助入力の 2 つの部分に分割できます。プライマリは、私たちがよく「ステートメント」と呼ぶものです。補助語は「証人」です。
R1CS 制約システムには複数の R1CS 制約が含まれます。各制約のベクトル長は固定されています (主入力サイズ + 補助入力サイズ + 1)。
• andTinyram は、libsnark のコード実装で多くのカスタム ガジェットを使用して、vm の制約と、オペコードの実行とメモリの制約を表現します。特定のコードは gadgetslib1/gadgets/cpu_checkers/tinyram フォルダーにあります。
ビット操作の制約
制約式:
R1CS 制約は、パラメータ 1 とパラメータ 2 および乗算計算の計算結果を 1 ビットずつ検証します。制約の手順は次のとおりです。
1. 計算プロセスの制約。コードは次のとおりです。
2. 結果のエンコーディングの制約
• or3. 計算結果はすべて 0 制約ではありません (命令の定義との一貫性を保ち、このプロセスは主に制約フラグを準備するためのものです)
4.フラグ制約
制約式:
具体的な制約の手順は次のとおりです。
1. 計算プロセスの制約。コードは次のとおりです。
2. 結果コーディングの制約 (上記と同じ)
• xor3. 計算結果がすべて0制約ではない（命令の定義との整合性を保ち、この処理は主に制約フラグを準備するためのものです）（同上）
4.フラグ制約（上記と同じ）
制約式:
具体的な制約の手順は次のとおりです。
•not1. 計算プロセスの制約。コードは次のとおりです。
ステップ 2、3、4 上記と同じ
制約式:
具体的な制約の手順は次のとおりです。
•addステップ 2、3、4 上記と同じ
整数操作の制約
: 制約式:
具体的な制約の手順は次のとおりです。
1. 計算プロセスの制約。コードは次のとおりです。
•sub2. 結果制約とブール制約のデコード
3. コーディング結果の制約
: 制約式:
sub 制約は add よりも少し複雑です。a - b の結果を表すために中間変数が使用されます。同時に、結果の計算が次の形式で表現されるように、2^w が結果に加算されます。正の整数と記号。具体的な制約の手順は次のとおりです。
1. 計算プロセスの制約
•mull 、umulh、smulh2. 結果制約とブール制約のデコード
3. 符号ビットの制約
制約式:
Mull 関連の制約には次の手順が含まれます
1. 乗算制約を計算する
•udiv 、umod2. 計算結果のコーディング制約
制約式:
B は約数、q は商、r は余りです。剰余の合計は、除数を超えてはいけないという条件を満たす必要があります。具体的な制約コードは次のとおりです。
• shl、shr副題
シフト演算の制約
制約式cmpe、 cmpa 、cmpae、cmpg、cmpge比較演算
。比較命令は符号付き数値の比較と符号なし数値の比較の 2 つに分類でき、どちらの制約処理の中核も libsnark に実装された Compare_gadget を使用します。
残りの手順は、符号付き比較制約の場合と同じです。
• mov副題
移動操作の制約
• cmov制約式:
制約式:
cmov の制約は mov の制約よりも複雑です。mov の主な動作はフラグ値の変更に関連しています。同時に、cmov はフラグを変更しないため、制約はフラグの値が変更されることを保証する必要があります。 cmov のコードは次のとおりです。
副題
• jmp
ジャンプ操作の制約
• cjmp
これらのジャンプ命令と条件付きジャンプ命令はレジスタやフラグを変更しませんが、pc を変更します。
Jmp 演算は、pc 値が命令の実行結果と一致するように制約します。具体的な制約コードは次のとおりです。
cjmp はフラグの条件に従ってジャンプします。フラグ = 1 でジャンプします。それ以外の場合は、pc が 1 ずつインクリメントされます。
• cnjmp
制約式は次のとおりです。
制約コードは次のとおりです。
cnjmp はフラグの条件に従ってジャンプします。フラグ = 0 でジャンプします。それ以外の場合は、pc が 1 ずつインクリメントされます。
制約式は次のとおりです。
メモリ操作の制約
• store.b そして store.w
これらは単純なメモリのロードおよびストア操作であり、メモリのアドレスは即値またはレジスタの内容によって決定されます。これらは tinyram の唯一のアドレッシング モードです。 (tinyram は一般的な「ベース + オフセット」アドレッシング モードをサポートしていません)。
そして
store.w の場合、arg1val 全体の値が取得され、store.b の場合、オペコードは arg1val の必要な部分 (例: 最後のバイト) のみを取得します。制約コードは次のとおりです。
•load.bとload.w
• read
これら 2 つの命令について、メモリからロードする必要があるコンテンツは、instruction_results に保存されます。制約コードは次のとおりです。
入力操作上の制約
読み取り操作はテープに関連しており、具体的な制約ルールは次のとおりです。
1. 前のテープの内容は読み取られていますが、読み取る内容はなく、次のテープは読み取られません。
2. 前のテープのコンテンツは読み取られていますが、読み取るコンテンツはなく、フラグは 1 に設定されます。
3. 現在実行されている命令が読み取られた場合、read によって読み取られた内容はテープの入力内容と一致します。
5. 結果は 0 ではありません。これはフラグが 0 であることを意味します。
制約コード:
副題
• answer
出力操作の制約
プログラムの出力値が受け入れられると、 has_accepted は 1 に設定され、プログラムの戻り値が正常に受け入れられることは、現在の命令が応答であり、arg2 の値が 0 であることを意味します。
他の
制約コードは次のとおりです。
上図の例から、vnTinyram + zk-SNARKs を使用してすべての EVM 動作を検証することは不可能であり、少数の命令の計算検証の検証にのみ適していると結論付けることができます。 EVM の一部の計算タイプのオペコードを確認します。
私たちについて
最初のレベルのタイトル
私たちについて
GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon
