ミデンの厳格な証明システム

Sin7y

特邀专栏作者

2022-10-11 16:38 (UTC+8)

この記事は約2722文字で、全文を読むには約4分かかります

この文書では、Miden プルーフシステムアーキテクチャについて詳しく説明します。

AI要約

この文書では、Miden プルーフシステムアーキテクチャについて詳しく説明します。

最初のレベルのタイトル

ミデンプルーフシステムアーキテクチャ

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:

ハッシュコマンド

RESCR

文章

6つのレジスタを占有

Constrain:

比較命令

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、クロスチェーン、プライバシーコンピューティング、自律型決済ソリューションなどの最も重要で最先端のテクノロジーを研究しています。