TinyRam 指令集和電路約束

簡介

Tinyram是一個簡單的RISC隨機存取機器，具有字節尋址的random-access memory 和input tapes。 TinyRAM有兩個變體：一個遵循哈佛架構，一個遵循馮諾依曼架構(本文我們主要討論馮諾依曼架構)。

簡明計算完整性和隱私研究（SCIPR）項目構建了證明TinyRAM程序正確執行的機制，而TinyRAM的設計是為了在這種情況下提高效率。它在“擁有足夠表達能力”和“足夠簡約”這兩個對立面之間取得平衡：

• 當從高級編程語⾔編譯時，有足夠的表達能力來支持簡短高效的彙編代碼。
• 小指令集，指令通過運算電路簡單驗證，利用SCIPR 的算法和密碼機制實現高效驗證。

本文對於tinyram不再進行重複介紹，會對上一篇文章進行補充，然後重點是指令介紹和電路約束介紹。 tinyram 基礎介紹可以參考我們團隊上一篇文章： TinyRam介紹-中文

Tinyram 指令集

Tinyram 總共有29個指令，每條指令都由一個操作碼和最多三個操作數組成。一個操作數可以是一個寄存器的名稱（一個介於0和K-1之間的整數), 也可以是一個立即數（W 位的字符串）。除非特別說明，否則指令不會單獨修改flag。每條指令默認將pc增加i (i % 2^W), 對於vnTinyram 來說i= 2W/8。

一般來說，第一個操作數是指令計算的目標寄存器， 其他的操作數指定指令需要的參數，最後，所有指令都需要機器的一個週期來執行。

位操作

• and ：指令and ri rj A 將[rj] 和[A] 的按位與結果存儲在ri寄存器中。此外，如果結果是 ，那麼將flag 設置為1，否則將flag 設置為0。
• or ： 指令or ri rj A 將[rj] 和[A] 的按位與結果存儲在ri寄存器中。如果結果是 ，那麼將flag 設置為1，否則將flag 設置為0。
• xor ：指令xor ri rj A 將[rj]和[A]的按位異或結果存儲在ri寄存器中。如果結果是 ，那麼將flag 設置為1，否則將flag 設置為0。
• not ：指令not ri A 將[A]的取反結果存儲在ri寄存器中。如果結果是 ，那麼將flag 設置為1，否則將flag 設置為0。

整數操作

這些是各種無符號和有符號的整數操作。在每種情況下，如果發生算術溢出或錯誤（如除以零），flag被設置為1，否則被設置為0。

在後⽂中， 代表⼀系列整數{0, . . . , }; 這些整數是可以由W-bit 的strings 組成的。 代表⼀系列整數{ , ...0, 1, }。這些整數也是由W-bit的strings組成的。

• add：指令add ri rj A將W-bit 的string 存儲到ri中。 是的W個最低有效位（LSB），此外flag將會被設置為 。 是G的最高有效位（MSB）。
• sub:指令sub ri rj A將W-bit 的string 存儲到ri中。 是的W個最低有效位（LSB）。此外flag將會被設置為 。 是G的最高有效位(MSB)。
• mull指令mull ri rj A將W-bit 的string 存儲到ri中。 是的W個最低有效位（LSB）。此外如果 ， flag將會被設置為1， 否則flag被設置為0。
• umulh指令umulh ri rj A將W-bit 的string 存儲到ri中。 是的W個最高有效位（MSB）。此外如果 ， flag將會被設置為1， 否則flag被設置為0。
• smulh指令smulh ri rj A將W-bit 的string W−1⋯a0"> 存儲到ri 中。 是的符號位， 是的W - 1個最高有效位。此外如果 ， flag將會被設置為1，否則flag被設置為0。
• udiv指令udiv ri rj A將W-bit 的string 存儲到ri中。

如果 , 。

如果 ，那麼是一個唯一整數Q 的二進制編碼形式，使得對於某些整數 ，式子成立。此外只有當的時候flag才會被設置為1。

• umod指令umod ri rj A將W-bit 的string 存儲到ri中。

如果 , 。

如果 ，那麼是一個唯一整數R 的二進制編碼形式, R的取值範圍為 ,使得式子成立對於某些Q取值來說。此外，只有當的時候flag才會被設置為1。

shift 操作

• shl指令shl ri rj A將[rj] 左移位[A]u bit 得到的W 位string 存儲在ri 寄存器中。移位後的空白位置被填充為0。此外flag被設置為[rj] 的最高有效位。
• shr指令shr ri rj A將[rj] 右移位[A]u bit 得到的W 位string 存儲在ri 寄存器中。移位後的空白位置被填充為0。此外flag被設置為[rj] 的最低有效位。

比較操作

比較操作中的指令每一個都不會修改任何寄存器； 比較的結果存儲在flag中。

• cmpe指令cmpe ri A 如果[ri]=[A] ，該指令將flag 設置為1，否則設置為0
• cmpa指令cmpa ri A 如果 ，該指令將flag 設置為1，否則設置為0
• cmpae指令cmpae ri A 如果 ，該指令將flag 設置為1，否則設置為0
• cmpg指令cmpg ri A 如果 ，該指令將flag 設置為1，否則設置為0
• cmpge指令cmpge ri A 如果 ，該指令將flag 設置為1，否則設置為0

move 操作

• mov指令mov ri A將[A] 存儲到ri寄存器中
• cmov指令cmov ri A如果flag = 1， 將[A] 存儲到ri寄存器中。否則ri 寄存器的值不會改變。

Jump 操作

這些jump和條件jump 指令都不會修改寄存器和flag 但是會修改pc。

• jmp指令jmp A將[A] 存儲到pc中。
• cjmp指令cjmp A在flag = 1 的條件下將[A] 存儲到pc中, 否則pc 自增1。
• cnjmp指令cnjmp A在flag = 0 的條件下將[A] 存儲到pc中, 否則pc 自增1。

Memory 操作

這些是簡單的memory load和store操作，其中memory的地址由立即數或寄存器的內容確定。這些是tinyram 中唯一的尋址方式。 （tinyram 不支持常見的“base+offset”尋址模式）。

• store.b指令store A ri將[ri] 的最低有效字節存儲在memory 的第[A]u-th 字節地址。
• load.b指令load ri A將memory中[A]u-th 字節地址的內容存儲到ri 寄存器中（前面有0填充）
• store.w指令store.w A ri將[ri] 存儲在memory中與第[A]w-th 字節對齊的word處
• load.w指令load.w ri A將內存中與第[A]w 字節對齊的word存儲到ri 寄存器中。

輸入操作

該指令是唯一一個訪問兩個tapes 中的任意一個的指令。第0個tape 用於primary 輸入，第1個tape 用戶auxiliary 輸入。

• read指令read ri A 將第[A]u 個tape上的下一個W-bit word存儲在ri 寄存器中。更多的準確地說，如果第[A]u 個tape有剩餘的word，則消耗下一個word，將其存儲在ri 中，並設置flag = 0； 否則（如果在第[A]u 個tape上沒有剩餘的輸入字）將存儲ri 中, 並設置flag = 1

因為TinyRAM只有兩個輸入tape，所以除了前兩個tape外，所有的tape都被假定為是空的。具體來說，如果[A]u不是0或1，那麼我們在ri中存儲 ，並設置flag=1。

輸出操作

該指令表示程序已經完成了計算，因此不能再允許其他操作。

• answer指令answer A導致狀態機stall（即不增加pc）或halt（即計算停止）,返回值[A]u。 stall或halt之間的選擇是未定義的。返回值0 用於表示程序接受。

指令集約束

Tinyram 採用R1CS約束形式進行電路約束， 具體形式如下：

此時，如果我們想證明我們知道原始計算的一個解，那麼就需要證明A，B，C矩陣中的每個行向量與解向量S的內積之後的值是符合R1CS約束的表示矩陣中的行向量)。

一個R1CS約束，可以有a，b, c 三個linear_combination表示，一個R1CS系統中的所有變量的賦值，可以分為兩個部分：primary input 和auxilary input。 Primary 就是我們經常說的“statement”。 auxiliary 就是“witness”。

一個R1CS 約束系統包含多個R1CS 約束。每個約束的向量長度是固定的（primary Input size + auxiliary input size + 1）。

Tinyram 在libsnark 的代碼實現中大量使用了一些定制gadgtes 來表述vm的約束以及opcode 執行和memory的約束。具體代碼在gadgetslib1/gadgets/cpu_checkers/tinyram 文件夾下。

位操作約束

• and約束公式：

and 的R1CS 約束將參數1和參數2以及計算結果逐bit 位進行乘法計算驗證，約束步驟如下：

1.計算過程約束，代碼如下：

2.結果編碼約束

3.計算結果非全0約束（跟指令的定義保持一直，這個過程主要是為了約束flag做準備）

4.flag 約束

• or約束公式：

具體約束步驟如下：

1.計算過程約束，代碼如下：

2.結果編碼約束（同上）

3.計算結果非全0約束（跟指令的定義保持一直，這個過程主要是為了約束flag做準備）（同上）

4.flag 約束（同上）

• xor約束公式：

具體約束步驟如下：

1.計算過程約束，代碼如下：

步驟2 ，3， 4 同上

• not約束公式：

具體約束步驟如下：

步驟2 ，3， 4 同上

整數操作約束

• add ： 約束公式：

具體約束步驟如下：

1.計算過程約束，代碼如下：

2.解碼結果約束和boolean約束

3.編碼結果約束

• sub : 約束公式：

sub 約束比add 稍微複雜一些， 採用了一個中間變量表示a - b 的結果，同時為了保證結果計算表示為正整數和符號的形式，給結果加上了2^w。具體約束步驟如下：

1. 計算過程約束

2. 解碼結果約束和boolean約束

3. 符號位約束

• mull 、umulh、smulh約束公式：

mull相關的約束都涉及以下幾個步驟

1. 計算乘法約束

2. 計算結果編碼約束

3. 計算結果flag約束

• udiv 、umod約束公式：

B 為除數， q 商， r為餘數。餘數與需要滿足不能超過除數的條件。具體約束代碼如下：

shift 操作約束

• shl、shr約束公式

比較操作

比較操作中的指令每一個都不會修改任何寄存器； 比較的結果存儲在flag中。比較指令包含cmpe、 cmpa 、cmpae、cmpg、cmpge 。比較指令可以分為兩類，分別為有符號數的比較和無符號數比較，兩者約束過程核心都利用了libsnark中實現的comparison_gadget 。

其他剩餘過程跟有符號數比較約束相同

move 操作約束

• mov約束公式：

mov的約束比較簡單，只需要確保將[A] 存儲到ri寄存器中，由於mov操作沒有修改flag，所以約束需要確保flag的值沒有產生變化。約束代碼如下：

• cmov約束公式：

cmov 的約束條件比mov複雜一些，主要mov的行為跟flag值的變化有關係，同時cmov不會修改flag， 所以約束需要確保flag的值沒有變化，cmov的代碼如下：

Jump 操作約束

這些jump和條件jump 指令都不會修改寄存器和flag 但是會修改pc。

• jmp

Jmp操作約束pc 值與指令執行結果一致，具體約束代碼如下：

• cjmp

cjmp 根據flag條件進行跳轉，flag = 1進行跳轉，否則pc 自增1

約束公式如下：

約束代碼如下：

• cnjmp

cnjmp 根據flag 條件進行跳轉，flag = 0 進行跳轉，否則pc 自增1

約束公式如下：

約束代碼如下：

Memory 操作約束

這些是簡單的memory load和store操作，其中memory的地址由立即數或寄存器的內容確定。這些是tinyram 中唯一的尋址方式。 （tinyram 不支持常見的“base+offset”尋址模式）。

• store.b和store.w

對於store.w 取整個arg1val 的值，對於store.b 操作碼只會取arg1val的必要部分（例如:最後一個字節），約束代碼如下:

• load.b和load.w

這兩個指令我們要求從內存中加載的內容被存儲在instruction_results 中，約束代碼如下：

輸入操作約束

• read

read 操作跟tape 有關，具體的約束規則是：

1. 上一個tape中的內容被讀完，沒有內容可讀，不會讀取下一個tape。

2. 上一個tape中的內容被讀完，沒有內容可讀，flag 被設置為1

3. 如果當前執行的指令是read,那麼read讀取到的內容和tape 輸入內容一致

4. 從tape1 以外的地方讀取內容， flag 被設置為1

5. result 為不為0，意味著flag 為0

約束代碼：

輸出操作約束

該指令表示程序已經完成了計算，因此不能再允許其他操作

• answer

當程序的輸出值被接受，has_accepted 會被設置為1， 程序返回值能夠被正常接受意味著當前的指令為answner 以及arg2 value 為0。

約束代碼如下：

其他

當然除了上述提到的一些指令相關的約束外，tinyram還有一些pc一致性、參數編解碼、內存檢查等各種約束。這些約束通過R1CS系統組合起來構成一個完成的tinyram 約束系統。所以這也是R1CS形式的tinyram生成約束數量較多的根本原因。

這裡引用一個tinyram介紹ppt的圖片，展示一個ERC20 transfer 用tinyram 生成證明需要的時間消耗。

從上圖的例子可以得出結論：使用vnTinyram + zk-SNARKs 驗證所有EVM 操作是不可能的，只適合驗證少量的指令的計算驗證，可以使用vnTinyram驗證EVM的部分計算類型的opcode。

引用

tinyram介紹ppt：https://docs.google.com/presentation/d/1lbyLmXhCry61fxWm8LLxPKhCYV67RcZaK3WL20Hb-t8/edit#slide=id.g5b38da04a0_0_21

關於我們

Sin7Y成立於2021年，由頂尖的區塊鏈開發者和密碼學工程師組成。我們既是項目孵化器也是區塊鏈技術研究團隊，探索EVM、Layer2、跨鏈、隱私計算、自主支付解決方案等最重要和最前沿的技術。

微信公眾號：Sin7Y

GitHub：Sin7Y

Twitter：@Sin7Y_Labs

Medium：Sin7Y

Mirror：Sin7Y

HackMD：Sin7Y

HackerNoon：Sin7Y

Email：contact@sin7y.org