詳解Cairo指令

Sin7y

特邀专栏作者

2022-09-28 02:44

本文約2540字，閱讀全文需要約4分鐘

本文從多個角度對Cairo指令進行了詳細解讀，涉及狀態轉換、轉換邏輯、指令校驗、指令示例等。

一級標題

一級標題"12345678")則該指令佔用2個word，並且值存在第二個word裡。每個指令的第一個word由以下元素組成：

一級標題

b. 確保執行的指令是一個有效的指令

二級標題

如果指令執行前後的狀態是一致的，那麼其狀態的更新一定是按照以下邏輯執行：

二級標題

3. 指令示例

二級標題

< left_handle_op > = < right_handle_op >

二級標題

Note2：3.1斷言相等

斷言相等指令可以用下述語法表示：

它確保了公式兩邊是相等的，否則程序的執行將會被返回。

除法和減法可以分別表示為具有不同操作數順序的乘法和加法。圖4給出了斷言相等指令的一些示例，以及每個指令對應的標誌值：

解釋

◦ next_ap = ap => ap_update = 00 = 0

◦ next_pc = pc + instruction_size => pc_update = 000 = 0

解釋

指令[fp + 1] = 5：

◦ 為assert指令=> opcode = 4

◦ op0和op1沒有add or mul => res_logic(res) = 00 = 0

◦ 存在立即數=> op1_src(op1) = 001 = 1

◦ op0_reg/ off_op0 =>inital value(1/-1) //因為這個指令用不到這些flags，所以填充默認值

二級標題

3.2 條件和非條件跳轉

# Unconditional jumps.

jmp abs

jmp rel

# Conditional jumps.

jmp rel if !

jmp 指令允許更改程序計數器pc 的值。

Cairo支持相對跳轉（其操作數代表相對當前pc的偏移）和絕對跳轉- 分別用關鍵字rel和abs表示；jmp指令或許是有條件的，比如當某個內存單元的值不為0時，觸發jmp指令。圖5給出了jmp 指令的一些示例，以及每個指令對應的標誌值：

解釋

◦ next_ap = ap => ap_update = b00 = 0

◦ next_pc = pc + res=> pc_update = b010 = 2

◦ res = op0 + op1 => res_logic(res) = b01 = 1

◦ op1: [fp - 7] => op1_src(op1) = b010 = 2

◦ op1: [fp - 7] => off_op1 = -7

◦ op0: [ap + 1] => op0_src(op0) = 0

◦ op0: [ap + 1] => off_op0 = 1

◦ dst_reg/ off_dst =>inital value(1/-1) ///因為這個指令用不到這些flags，所以填充默認值

二級標題

call ret

call rel

ret

3.3 call 和ret

call和ret指令允許實現函數堆棧。 call指令更新程序計數器(pc)和幀指針(fp)寄存器。程序計數器的更新類似於jmp 指令。之前fp 的值被寫入[ap] ，以允許ret 指令將fp 的值重置為調用之前的值；類似地，返回的pc (調用指令後面指令的地址)被寫到[ap+1] ，以允許ret 指令跳回並繼續執行調用指令後面的代碼的執行。由於寫入了兩個存儲單元，ap 向前進了2，fp 被設置為新的ap。圖6給出了call 和ret 指令的一些示例，以及每個指令對應的標誌值：

解釋

◦ next_ap = ap => ap_update = b00 = 0

◦ next_pc = res => pc_update = b001 = 1

◦ res = op1 => res_logic(res) = b00 = 0

◦ op1: [fp + 4] => op1_src(op1) = b010 = 2

◦ op1: [fp + 4] => off_op1 = 4

◦ op0_reg/ off_op0 =>解釋

◦ dst_reg/ off_dst =>inital value(0/0) ///因為這個指令用不到這些flags，所以填充默認值