簡介

一級標題

簡介

一級標題

簡介

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

TinyRam介紹

一級標題

Tinyram 指令集

一級標題

一級標題

位操作

Tinyram 指令集

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

• shrshift 操作

位操作

整數操作

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

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

• cmovmove 操作

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

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

• jmpJump 操作

• cjmpmove 操作

• cnjmp 指令mov ri A 將[A] 存儲到ri寄存器中。

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

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

Memory 操作

指令jmp A 將[A] 存儲到pc中。

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

Memory 操作

輸入操作

一級標題

輸出操作

一級標題

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

一級標題

• and指令集約束

Tinyram 採用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 文件夾下。

位操作約束

• or約束公式：

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

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

2.結果編碼約束

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

4.flag 約束

• xor約束公式：

具體約束步驟如下：

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

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

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

4.flag 約束（同上）

約束公式：

具體約束步驟如下：

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

步驟2 ，3， 4 同上

約束公式：

具體約束步驟如下：

步驟2 ，3， 4 同上

•sub整數操作約束
： 約束公式：

具體約束步驟如下：

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

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

•mull 、umulh、smulh3.編碼結果約束

: 約束公式：

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

1. 計算過程約束

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

•udiv 、umod3. 符號位約束

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

2. 計算結果編碼約束

• shl、shr二級標題

約束公式：

二級標題cmpe、 cmpa 、cmpae、cmpg、cmpgeB 為除數， q 商， r為餘數。餘數與需要滿足不能超過除數的條件。具體約束代碼如下：

shift 操作約束

比較操作

• mov二級標題

。比較指令可以分為兩類，分別為有符號數的比較和無符號數比較，兩者約束過程核心都利用了libsnark中實現的comparison_gadget 。

• cmov二級標題

二級標題

約束公式：

二級標題

• jmp

約束公式：

• cjmp

二級標題

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

二級標題

• cnjmp

Jump 操作約束

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

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

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

約束代碼如下：

• store.b 和 store.w

約束公式如下：

和

Memory 操作約束

和

• read

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

和

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

• load.b 和load.w

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

輸入操作約束

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

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

二級標題

• answer

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

約束代碼：

其他

輸出操作約束

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

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

關於我們

一級標題

關於我們

GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon