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的虛擬機執行過程進行約束。
AIR結構設計圖
AIR的約束分為stack和decoder兩部分：
圖2為stack的約束，初始化時分配了最上邊深度為8的stack。在執行時根據程序需要，可能會超出初始化分配的深度，那麼max_depth會根據需要遞增。但是不能超過最大深度16。否則報錯。
圖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 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的詞法和語法分析器解析後的最終指令代碼如下代碼段2:
下邊圖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裡。
Note：本文檔描述針對miden工程的main分支最新版本。目前miden的next分支對於指令進行了大量重新設計，AIR也只實現了很少一部分的約束。
stack約束條件
本節將展示主要的User操作指令的約束條件。其中的old_stack_x指的是指令執行前的stack的x位置存儲的value。 new_stack_x指的是指令執行後的stack的x位置存儲的value。 -->是將棧左邊位置的value拷貝到右邊位置。 ==是等式約束。 stack的約束相對比較簡單，就不多做解釋了。
條件指令
Choose
Constrain:
如果condition為1， x在堆棧頂部，condition為0， y在堆棧頂部
算術指令
add
Constrain:
mul
Constrain:
inv
Constrain:
neg
Constrain:
bool 指令
not
Constrain:
and
Constrain:
or
Constrain:
hash 指令
RESCR
滿足hash函數協議的限制函數hash
佔用6 registers
Constrain:
比較指令
eq
Constrain:
cmp
根據比較的兩個數的bit長度循環比較。比如
A: [0,1,0,1]
B: [0,0,1,1]
需要比較4次
Constrain:
堆棧操作指令
dup.n
Constrain:
swap
Constrain:
ROLL4
Constrain:
decoder的約束條件
本節將展示主要的Flow操作指令的約束條件。
用戶代碼執行
op_bits
對於cf_op_bits，ld_op_bits，hd_op_bits的約束。
約束1: 每bit只能為0或者1。
約束2: 當op_counter不為0時，ld_ops 和hd_ops不能同時為0。
約束3: 當cf_op_bits為hacc時。 op_counter狀態會加1。
約束4: BEGIN, LOOP, BREAK, and WRAP指令需要16對齊。
約束5: TEND and FEND指令需要16對齊。
約束6:PUSH指令需要8對齊。
hacc
hacc作為flowOps，每次執行該指令都會引起sponge的狀態改變，需要進行約束
條件判斷
t_end
作為if的true分支結束的約束，分為兩部分：
約束1: sponge狀態的約束，彈出棧頂的值等於new_sponge_0。 if的true分支的最後一步執行後的sponge等於new_sponge_1。 new_sponge_3等於0。
約束2: ctx_stack的約束。彈出棧頂的值等於new_sponge_0。棧內其他元素都往棧頂移動一個位置。
約束3: loop_stack的約束。 loop_stack的狀態不變。
f_end
作為if的false分支結束的約束，分為兩部分：
約束1: sponge狀態的約束，彈出棧頂的值等於new_sponge_0。 if的true分支的最後一步執行後的sponge等於new_sponge_2。 new_sponge_3等於0。
約束2: ctx_stack的約束。彈出棧頂的值等於new_sponge_0。棧內其他元素都往棧頂移動一個位置。
約束3: loop_stack的約束。 loop_stack的狀態不變。
關於我們
Sin7Y成立於2021年，由頂尖的區塊鏈開發者和密碼學工程師組成。我們既是項目孵化器也是區塊鏈技術研究團隊，探索EVM、Layer2、跨鏈、隱私計算、自主支付解決方案等最重要和最前沿的技術。
微信公眾號：Sin7Y
GitHub：Sin7Y
Twitter：@Sin7Y_Labs
Medium：Sin7Y
Mirror：Sin7Y
HackMD：Sin7Y
HackerNoon：Sin7Y
Email：contact@sin7y.org
APP 
