Miden的stark證明系統

Sin7Y ｜2022-08-16 20:49

miden是⼀個基於stark技術的zkVM實現方案。它的底層是基於winterfell這個zkp庫來生成stark證明和對證明進行驗證。本文對miden證明系統架構進行了詳細闡述。

miden 證明系統架構

miden是一個基於strark技術的zkvm實現方案。它的底層是基於winterfell這個zkp庫來生成stark證明和對證明進行驗證。下圖1中虛線部分是Miden實現的主要功能。可以看出，主要有三個組件構成。

1. 一套詞法語法編譯器,下圖1中的lexical analyzer和syntax parser。它們可以將miden定義的彙編指令編程成codeblock和block中包含的opcode和op value。

2. 一套指令的執行器，下圖1中的executor。它負責按照定義的規則執行codeblock和block中包含的opcode及op value。執行結果為用於生成證明的execution trace。

3. 一套符合stark證明要求的AIR(代數中間表示)，下圖1中的AIR。用來對miden的虛擬機執行過程進行約束。

Miden的stark證明系統

AIR結構設計圖

AIR的約束分為stack和decoder兩部分：

圖2為stack的約束，初始化時分配了最上邊深度為8的stack。在執行時根據程序需要，可能會超出初始化分配的深度，那麼max_depth會根據需要遞增。但是不能超過最大深度16。否則報錯。

Miden的stark證明系統

圖3為decoder的約束。其中的op_counter,op_sponge,cf_op_bits, ld_op_bits,hd_op_bits是固定列長度的。其中的op_sponge用於執行指令的順序和正確性的約束。 cf_op_bits約束3bit的flow_ops。 ld_op_bits,hd_op_bits分別約束了user_ops的低5bits和高2bits。 ld_op_bits和hd_op_bits組合構成一條執行的user_op,還用來作為stack每step狀態約束的selector。

Miden的stark證明系統

Miden VM執行過程實例

本節將展示一個簡單的miden邏輯來說明vm的執行過程和stark的execution trace的生成。

下邊代碼段1是要執行的代碼段：

它執行的邏輯是將3和5壓棧。之後從tape讀取flag。判斷flag是1還是0。如果是1則運行if.true分支將壓棧的兩個數3和5取出，相加得到8並重新壓入棧。如果是0則運行else分支將壓棧的兩個數3和5取出相乘得到15，再將15重新壓入棧。

Miden的stark證明系統

代碼段通過miden的詞法和語法分析器解析後的最終指令代碼如下代碼段2:

Miden的stark證明系統

下邊圖4是vm運行代碼段2的過程，中間是executor執行opcode的流程圖，左邊虛線指向的是代碼執行產生的decoder trace，右邊點劃線指向的是代碼執行產生的stack trace。

其中executor是按照code block來一塊一塊執行。在本例子裡，首先執行了一個span block。之後在第32步時執行if-else-end結構進入了swtich block塊，並將之前的span block的最後一步執行生成的sponge hash壓入ctx_stack，並在swtich block塊執行完之後，在第49步彈出到sponge裡。

Miden的stark證明系統

Note：本文檔描述針對miden工程的main分支最新版本。目前miden的next分支對於指令進行了大量重新設計，AIR也只實現了很少一部分的約束。

stack約束條件

本節將展示主要的User操作指令的約束條件。其中的old_stack_x指的是指令執行前的stack的x位置存儲的value。 new_stack_x指的是指令執行後的stack的x位置存儲的value。 -->是將棧左邊位置的value拷貝到右邊位置。 ==是等式約束。 stack的約束相對比較簡單，就不多做解釋了。