最初のレベルのタイトル
ミデンプルーフシステムアーキテクチャ
miden は、strark テクノロジーに基づいた zkvm 実装です。その最下層は、Winterfell の zkp ライブラリに基づいており、明確な証明を生成し、証明を検証します。以下の図 1 の点線は、Miden によって実装される主な機能です。主に 3 つのコンポーネントがあることがわかります。
1. 以下の図 1 の字句文法コンパイラ、字句アナライザ、および構文パーサのセット。これらは、miden によって定義されたアセンブリ命令を、コードブロックとブロックに含まれるオペコードとオペ値にプログラムできます。
3. 厳密な証明の要件を満たす一連の AIR (代数中間表現)、以下の図 1 の AIR。これは、miden の仮想マシンの実行プロセスを制約するために使用されます。
最初のレベルのタイトル
AIR構造設計
AIR の制約は、スタックとデコーダーの 2 つの部分に分かれています。
図 3 は、デコーダの制約を示しています。このうち、op_counter、op_sponge、cf_op_bits、ld_op_bits、hd_op_bits は固定カラム長です。このうち、op_sponge は、命令の実行順序と正確性を制約するために使用されます。 cf_op_bits は 3 ビットの flow_ops を制約します。 ld_op_bits、hd_op_bits はそれぞれ user_ops の下位 5 ビットと上位 2 ビットを制約します。 ld_op_bits と hd_op_bits の組み合わせは、実行される user_op を構成し、スタックの各ステップ状態制約のセレクターとしても使用されます。
最初のレベルのタイトル
Miden VM 実行プロセス インスタンス
このセクションでは、vm の実行プロセスと stark の実行トレースの生成を説明するための単純な miden ロジックを示します。
以下のコード セグメント 1 は、実行されるコード セグメントです。
実行されるロジックは、3 と 5 をスタックにプッシュすることです。次に、テープからフラグを読み取ります。フラグが 1 か 0 かを判断します。 1 の場合は、if.true ブランチを実行して、スタックにプッシュされた 2 つの数値 3 と 5 を取り出し、それらを加算して 8 を取得し、スタックにプッシュし直します。 0 の場合は、else 分岐を実行して、スタックにプッシュされた 2 つの数値 3 と 5 を取り出し、それらを乗算して 15 を取得し、15 をスタックに戻します。
コード セグメントが miden の字句および文法アナライザーによって解析された後の最終的な命令コードは次のとおりです。コード セグメント 2:
以下の図 4 は、コード セグメント 2 を実行する vm のプロセスを示しています。中央は、オペコードを実行するエグゼキュータのフローチャートです。左側の点線は、コードの実行によって生成されたデコーダ トレースを指し、右側の点線は、コードの実行によって生成されるスタック トレース。
このうちエグゼキュータはコードブロックに従って一つずつ実行されます。この例では、最初にスパンブロックが実行されます。次に、ステップ 32 で if-else-end 構造を実行して swtich ブロックに入り、前の Span ブロックの最後のステップで生成されたスポンジ ハッシュを ctx_stack にプッシュし、swtich ブロックが実行された後、ステップ 49 でポップします。スポンジ。
注: このドキュメントでは、miden プロジェクトのメイン ブランチの最新バージョンについて説明します。現在、miden の次のブランチでは多くの命令が再設計されており、AIR は制約のごく一部のみを実装しています。
スタック制約
条件付き命令
Choose
Constrain:
文章
文章
add
Constrain:
mul
Constrain:
inv
Constrain:
neg
Constrain:
ブールディレクティブ
not
Constrain:
and
Constrain:
or
Constrain:
ハッシュコマンド
RESCR
文章
6つのレジスタを占有
Constrain:
比較命令
eq
Constrain:
cmp
文章
A: [0,1,0,1]
B: [0,0,1,1]
4回比較する必要がある
Constrain:
文章
dup.n
Constrain:
swap
Constrain:
ROLL4
Constrain:
最初のレベルのタイトル
デコーダの制約
ユーザーコードの実行
op_bits
文章
cf_op_bits、ld_op_bits、hd_op_bits の制約。
制約 1: 各ビットは 0 または 1 のみにすることができます。
制約 2: op_counter が 0 でない場合、ld_ops と hd_ops を同時に 0 にすることはできません。
制約 3: cf_op_bits が hacc の場合。 op_counter ステータスは 1 ずつ増加します。
制約 4: BEGIN、LOOP、BREAK、および WRAP 命令には 16 個のアライメントが必要
制約 6: PUSH 命令には 8 つのアライメントが必要です
hacc
hacc は flowOps として使用されます。この命令を実行するたびにスポンジの状態が変化するため、これを制約する必要があります。
条件判断
t_end
文章
if の true 分岐の終わりである制約は 2 つの部分に分かれています。
制約 1: スポンジ状態の制約。ポップアップ スタックの最上位の値は new_sponge_0 に等しくなります。 if の true 分岐の最後のステップの実行後のスポンジは、new_sponge_1 と等しくなります。 new_sponge_3 は 0 に等しい。
制約 3:loop_stack の制約。 Loop_stack の状態は変化しません。
f_end
文章
if の false 分岐の最後の制約として、次の 2 つの部分に分かれています。
制約 1: スポンジ状態の制約。ポップアップ スタックの最上位の値は new_sponge_0 に等しくなります。 if の true 分岐の最後のステップの実行後のスポンジは、new_sponge_2 と等しくなります。 new_sponge_3 は 0 に等しい。
Sin7y は 2021 年に設立され、トップのブロックチェーン開発者で構成されています。私たちはプロジェクト インキュベーターであると同時にブロックチェーン テクノロジー研究チームでもあり、EVM、レイヤー 2、クロスチェーン、プライバシー コンピューティング、自律型決済ソリューションなどの最も重要で最先端のテクノロジーを研究しています。
私たちについて
Sin7y は 2021 年に設立され、トップのブロックチェーン開発者で構成されています。私たちはプロジェクト インキュベーターであると同時にブロックチェーン テクノロジー研究チームでもあり、EVM、レイヤー 2、クロスチェーン、プライバシー コンピューティング、自律型決済ソリューションなどの最も重要で最先端のテクノロジーを研究しています。
WeChat 公開アカウント: Sin7Y
GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon
IOS
Android