一級標題
一級標題
一級標題
Miden 證明系統架構
3. 一套符合stark證明要求的AIR(代數中間表示)，下圖1中的AIR。用來對miden的虛擬機執行過程進行約束。
一級標題
一級標題
一級標題
圖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裡。
hash 指令
Choose
Constrain:
正文
正文
add
Constrain:
mul
Constrain:
inv
Constrain:
neg
Constrain:
bool 指令
not
Constrain:
and
Constrain:
or
Constrain:
hash 指令
RESCR
正文
正文
Constrain:
比較指令
eq
Constrain:
cmp
正文
A: [0,1,0,1]
B: [0,0,1,1]
正文
Constrain:
正文
dup.n
Constrain:
swap
Constrain:
ROLL4
Constrain:
一級標題
一級標題
用戶代碼執行
op_bits
正文
正文
正文
對於cf_op_bits，ld_op_bits，hd_op_bits的約束。
約束1: 每bit只能為0或者1。
約束2: 當op_counter不為0時，ld_ops 和hd_ops不能同時為0。
約束4: BEGIN, LOOP, BREAK, and WRAP指令需要16對齊
hacc
正文
條件判斷
t_end
正文
正文
正文
約束3: loop_stack的約束。 loop_stack的狀態不變。
f_end
正文
正文
正文
Sin7y成立於2021年，由頂尖的區塊鏈開發者組成。我們既是項目孵化器也是區塊鏈技術研究團隊，探索EVM、Layer2、跨鏈、隱私計算、自主支付解決方案等最重要和最前沿的技術。
關於我們
Sin7y成立於2021年，由頂尖的區塊鏈開發者組成。我們既是項目孵化器也是區塊鏈技術研究團隊，探索EVM、Layer2、跨鏈、隱私計算、自主支付解決方案等最重要和最前沿的技術。
微信公眾號：Sin7Y
GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon
