MIDEN V1 で STARK ベースの実行証明プロセスはどのように機能しますか?

Miden は、技術ベースの ZKVM 実装ソリューションです。

その基本層では、ZKP ライブラリに基づいてスタークプルーフが生成され、プルーフが検証されます。以下の図1の点線部分がMidenが実装する主な機能です。主に3つのコンポーネントで構成されています。

1. 図 1 の字句解析器および構文パーサーである、字句構文コンパイラーの 1 つのセット。これらは、Miden によって定義されたアセンブリー命令をコードブロックまたはブロックに含まれる opcode および op 値にプログラムできます。

2. 命令エグゼキュータの 1 つのセット (図 1 のエグゼキュータ)。定義されたルールに従って、ブロックに含まれるコードブロックとオペコードおよびオペ値を実行します。そして実行結果が証明を生成するための実行トレースとなります。

3. スタークプルーフの要件を満たす AIR (Abstract Inter-mediate Representation) の 1 つのセット、それが図 1 の AIR です。Miden Virtual Machine の実行プロセスに制約を加えます。

図 1. Miden プロジェクトのコンポーネント

AIR 構造設計図

AIR の制約は、スタックとデコーダーに分割されます。図 2 は、スタックの制約を示しており、初期化時に最上位の深さが 8 のスタックで配布されます。

プログラムの必要に応じて、実行中に初期分布を超える可能性がある場合、max_depth は必要に応じて増分されますが、最大深度の 16 を超えることはできません。超えると、エラーが報告されます。

図 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 を形成します!

図 3: Decoder Constraint の列

Miden VMの実行プロセス例

このセクションでは、仮想マシンの実行とスタークの実行トレースの生成を説明するために、簡単な Miden ロジックを示します。

次のコード セグメント 1 は、実行するセグメントです。その実行ロジックは、3 と 5 をスタックにプッシュすることです。次に、テープからフラグを読み取ります。

フラグが 1 か 0 かを確認します。フラグが 1 の場合は、"if.true ロジック" を実行して、スタックにプッシュされた 3 と 5 の 2 つの数字を取得し、それらを加算して 8 にし、8 をスタックにプッシュします。スタック。 0 の場合は、「else ロジック」を実行して 3 と 5 の数値を掛け合わせて 15 にし、15 をスタックにプッシュします。

 begin push.3 push.5 read if.true add else mul end end

コード セグメント 1

Miden の語彙アナライザーと構文パーサーによって解析された最終的な命令コードは、次のコード セグメント 2 に示されています。

 begin noop noop noop noop noop noop noop push(3) noop noop noop noop noop noop noop push(5) read noop noop noop noop noop noop noop noop noop noop noop noop noop, if assert add noop noop noop noop noop noop noop noop noop noop noop noop noop else not assert mul noop noop noop noop noop noop noop noop noop noop noop noop end]

コード セグメント 2

図 4 は、仮想マシンがコード セグメント 2 を実行するプロセスを示しています。

中央部分は、オペコードを実行するエグゼキュータのフローチャートです。左の点線は、コード実行で生成されたデコーダー トレースを示します。右側の一点鎖線は、コード実行で生成されたスタック トレースを示します。

図では、エグゼキュータはコードブロックに従ってブロックごとに実行を行います。この例では、span ブロックが最初に実行されます。

次に、ステップ 32 の if-else-end 構造が実行されて、スイッチ ブロックに入り、前のスパン ブロックの最後の実行によって生成されたスポンジ ハッシュが ctx_stack に押し込まれます。スイッチ ブロックが実行された後、ステップ 49 でスポンジにポップします。

図 4: オペコードを実行する VM の状態変化図

注: このドキュメントでは、2022 年 5 月 27 日時点での Miden プロジェクトのメイン ブランチの最新バージョンについて説明します。これまでのところ、Miden の次のブランチでは命令の多くの再設計が行われており、AIR ではいくつかの制約しか実装されていません。

スタックの制約条件

このセクションでは、主要なユーザー操作命令の制約条件を示します。その中で、old_stack_x は命令実行前にスタックの x 位置に格納された値を指し、new_stack_x は命令実行前のスタックの x 位置に格納された値を指します。 「–>」はスタックの左側から右側への値のコピーを表し、「==」は方程式の制約を表します。スタックの制約は比較的単純で、説明は必要ありません。

コンディション説明書

選ぶ

制約:

 new_stack_0 == (condition * x) + ((1 - condition) * y) old_stack_0 == x old_stack_1 == y old_stack_2 == condition old_stack_3 --> new_stack_1 old_stack_n. --> new_stack_n-2 aux_0 == condition.is_binary == true

条件が 1 の場合、x はスタックの一番上にあります。条件が 0 の場合、y はスタックの一番上にあります。

算数指導

追加

制約:

 old_stack_0 + old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

ムル

制約:

 old_stack_0 * old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

反対

制約:

 old_stack_0 * new_stack_0 == 1 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

否定

制約:

 old_stack_0 + new_stack_0 == 0 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

ブール命令

いいえ

制約:

 aux_0: make sure old_stack_0 is binary 1-old_stack_0 == new_stack_0 old_stack_1 --> new_stack_1 old_stack_n. --> new_stack_n

と

制約:

 aux_0: make sure old_stack_0 is binary aux_1: make sure old_stack_1 is binary old_stack_0 * old_stack_1 == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

また

制約:

 aux_0: make sure old_stack_0 is binary aux_1: make sure old_stack_1 is binary 1- (1-old_stack_0) *(1- old_stack_1) == new_stack_0 old_stack_2 --> new_stack_1 old_stack_n. --> new_stack_n-1

ハッシュ命令

RESCR

ハッシュ関数プロトコルを満たす制限関数ハッシュ
6 つのレジスタを占有します。

制約:

 hash(old_stack0，old_stack1， old_stack2， old_stack3， old_stack3， old_stack5) == （new_stack0，new_stack1， new_stack2， new_stack3， new_stack3， new_stack5） old_stack_6 --> new_stack_6 old_stack_n. --> new_stack_n

比較命令

式

制約:

 aux_0 == new_stack_0 * diff == 0 new_stack_0 == 1- (old_stack_1-old_stack_2)*old_stack_0 old_stack_0 == inv(old_stack_1-old_stack_2) old_stack_3 --> new_stack_1 old_stack_n. --> new_stack_n-2

cmp

次のように、比較する 2 つの数値のビット長サイクルに従って比較します。

A: [0,1,0,1]
B: [0,0,1,1]

比較命令は 4 回実行する必要があります。

制約:

 // layout of first 8 registers // [pow, bit_a, bit_b, not_set, gt, lt, acc_b, acc_a] // x and y bits are binary new_stack_1 == x_big_idx(lg lt flag) （type:binary) new_stack_2 == y_big_idx(lg lt flag) （type:binary) bit_gt = x_big_idx*(1-y_big_idx) bit_lt = y_big_idx*(1-x_big_idx) // comparison trackers were updated correctly new_stack_3 = not_set_idx new_stack_4(gt) == old_stack_4(gt_idx) + bit_gt * not_set_idx new_stack_5(lt) == old_stack_5(lt_idx) + bit_lt * not_set_idx // binary representation accumulators were updated correctly old_stack_0 = POW2_IDX old_stack_6 = Y_ACC_IDX old_stack_7 = X_ACC_IDX new_stack_6 == old_stack_6 + x_big_idx * old_stack_0(power_of_two); new_stack_7 == old_stack_7 + y_big_idx * old_stack_0(power_of_two); // when GT or LT register is set to 1, not_set flag is cleared not_set_check = (1-old_stack_5(lt_idx))*(1-old_stack_4(gt_idx)) not_set_check == new_stack_3(not_set_idx) // power of 2 register was updated correctly new_stack[POW2_IDX] * two == old_stack[POW2_IDX] old_stack_8 --> new_stack_8 old_stack_n --> new_stack_n

スタック操作命令

dup.n

制約:

 new_stack_0 == old_stack_0 ... new_stack_n-1 == old_stack_n-1 old_stack_0 --> new_stack_n old_stack_k --> new_stack_n+k

スワップ

制約:

 new_stack_0 == old_stack_1 new_stack_1 == old_stack_0 old_stack_2 --> new_stack_2 old_stack_n --> new_stack_n

ROLL4

制約:

 new_stack_0 == old_stack_3 new_stack_1 == old_stack_0 new_stack_2 == old_stack_1 new_stack_3 == old_stack_2 old_stack_4 --> new_stack_4 old_stack_n --> new_stack_n

デコーダコメントの制約条件

このセクションでは、メインのフロー操作命令の制約条件を示します。

ユーザーコードの実行

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 に従って整列する必要があります。
制約 5: TEND および FEND 命令は、16 に従って整列する必要があります。
制約 6: PUSH 命令は、8 に従ってアラインする必要があります。

制約:

 cf_op_bits == binary ld_op_bits == binary hd_op_bits == binary // ld_ops and hd_ops can be all 0s at the first step, but cannot be all 0s at any other step op_counter * binary_not(ld_bit_prod) * binary_not(hd_bit_prod) == 0 if op_counter != 0 (1-ld_bit_prod)*(1- hd_bit_prod) == 0 if is_hacc != true op_counter = current.op_counter // BEGIN, LOOP, BREAK, and WRAP are allowed only on one less than multiple of 16 // TEND and FEND is allowed only on multiples of 16 // PUSH is allowed only on multiples of 8

ハックコメント

Hacc は flowOps として、この命令を実行すると常にスポンジの状態変化を引き起こすため、制約を実行する必要があります。

制約:

 mds(sbox(old_sponge) + user_opcode(7bits) + op_value(push_flag=1)) == sbox(inv_mds(new_sponge))

条件判定

傾向

if の真の分岐端の制約として、次の 2 つの部分に分けられます。
制約 1: スポンジ状態の制約です。

スタックの一番上にある値は、new_sponge_0 と同じです。 if の true 分岐が最後に実行された後のスポンジは、new_sponge_1 に等しくなります。 New_sponge_3 は 0 です。

制約 2: ctx_stack の制約です。スタックの一番上にある値は、new_sponge_0 と同じです。スタック内の他の要素は、スタックの一番上に 1 つ移動します。

制約 3: loop_stack の制約です。 loop_stack の状態は変化しません。

制約:

 parent_hash = current.ctx_stack()[0] block_hash = current.op_sponge()[0] new_sponge = next.op_sponge() parent_hash == new_sponge[0] block_hash == new_sponge[1] new_sponge[3] == 0 // make parent hash was popped from context stack ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint ctx_stack_end = ctx_stack_start + ctx_stack_current.len() ctx_result = &mut result[ctx_stack_start..ctx_stack_end] ctx_stack_current_0 = ctx_stack_next_1 ctx_stack_current_1 = ctx_stack_next_2 ... ctx_stack_current_n = ctx_stack_next_n+1 // loop_stack copy copy range: ctx_stack_end to. ctx_stack_end + loop_stack_current.len() loop_stack_current_0 = loop_stack_next_0 ... loop_stack_current_n = loop_stack_next_n

f_end

if の false 分岐端の制約として、次の 2 つの部分に分けられます。
制約 1: スポンジ状態の制約です。スタックの一番上にある値は、new_sponge_0 と同じです。

if の true 分岐の最後の実行後のスポンジは、new_sponge_2 に等しくなります。 new_sponge_3 は 0 です。

制約 2: ctx_stack の制約です。スタックの一番上にある値は、new_sponge_0 と同じです。スタック内の他の要素は、スタックの一番上に 1 つ移動します。

制約 3: loop_stack の制約です。 loop_stack の状態は変更されません。

制約:

 parent_hash = current.ctx_stack()[0] block_hash = current.op_sponge()[0] new_sponge = next.op_sponge() parent_hash == new_sponge[0] block_hash == new_sponge[2] new_sponge[3] == 0 // make parent hash was popped from context stack ctx_stack_start = OP_SPONGE_WIDTH + 1 // 1 is for loop image constraint ctx_stack_end = ctx_stack_start + ctx_stack_current.len() ctx_result = &mut result[ctx_stack_start..ctx_stack_end] ctx_stack_current_0 = ctx_stack_next_1 ctx_stack_current_1 = ctx_stack_next_2 ... ctx_stack_current_n = ctx_stack_next_n+1 // loop_stack copy copy range: ctx_stack_end to. ctx_stack_end + loop_stack_current.len() loop_stack_current_0 = loop_stack_next_0 ... loop_stack_current_n = loop_stack_next_n