mt logoMyToken
Market cap:
0%
FGI:
0%
Cryptocurrencies:--
Exchanges --
ETH Gas:--
EN
USD
APP
Ap Store QR Code

Scan Download

TinyRam指令集和电路约束

Collect
Share

简介

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。

一般来说,第一个操作数是指令计算的目标寄存器, 其他的操作数指定指令需要的参数,最后,所有指令都需要机器的一个周期来执行。

位操作

TinyRam指令集和电路约束

整数操作

这些是各种无符号和有符号的整数操作。在每种情况下,如果发生算术溢出或错误(如除以零),flag被设置为1,否则被设置为0。

TinyRam指令集和电路约束

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中。

TinyRam指令集和电路约束

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”寻址模式)。

TinyRam指令集和电路约束

输入 操作

该指令是唯一一个访问两个tapes 中的任意一个的指令。第0 个tape 用于 primary 输入,第1个 tape 用户 auxiliary 输入。

TinyRam指令集和电路约束

输出 操作

该指令表示程序已经完成了计算,因此不能再允许其他操作。

TinyRam指令集和电路约束

指令集约束

Tinyram 采用R1CS约束形式进行电路约束, 具体形式如下:

TinyRam指令集和电路约束

一个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 约束公式:

TinyRam指令集和电路约束

and 的R1CS 约束将参数1和参数2以及计算结果 逐bit 位 进行乘法计算验证,约束步骤如下:

1.计算过程约束,代码如下:

TinyRam指令集和电路约束

2.结果编码约束

3.计算结果非全0约束(跟指令的定义保持一直,这个过程主要是为了约束flag做准备)

TinyRam指令集和电路约束

4.flag 约束

TinyRam指令集和电路约束

• or 约束公式:

TinyRam指令集和电路约束

具体约束步骤如下:

1.计算过程约束,代码如下:

TinyRam指令集和电路约束

2.结果编码约束 (同上)

3.计算结果非全0约束(跟指令的定义保持一直,这个过程主要是为了约束flag做准备)(同上)

4.flag 约束 (同上)

• xor 约束公式:

TinyRam指令集和电路约束

具体约束步骤如下:

1.计算过程约束,代码如下:

TinyRam指令集和电路约束

步骤 2 ,3, 4 同上

• not 约束公式:

TinyRam指令集和电路约束

具体约束步骤如下:

TinyRam指令集和电路约束

步骤 2 ,3, 4 同上

整数操作约束

• add : 约束公式:

TinyRam指令集和电路约束

具体约束步骤如下:

1.计算过程约束,代码如下:

TinyRam指令集和电路约束

2.解码结果约束和boolean约束

3.编码结果约束

• sub : 约束公式:
sub 约束比add 稍微复杂一些, 采用了一个中间变量表示 a - b 的结果,同时为了保证结果计算表示为正整数和符号的形式,给结果加上了 2^w。具体约束步骤如下:

TinyRam指令集和电路约束

1. 计算过程约束

TinyRam指令集和电路约束

2. 解码结果约束和boolean约束

3. 符号位约束

• mull 、 umulh 、 smulh 约束公式:

TinyRam指令集和电路约束

mull相关的约束都涉及以下几个步骤

1. 计算乘法约束

2. 计算结果编码约束

3. 计算结果 flag约束

• udiv 、 umod 约束公式:

TinyRam指令集和电路约束

B 为除数, q 商, r为余数。 余数与需要满足不能超过除数的条件。具体约束代码如下:

TinyRam指令集和电路约束

TinyRam指令集和电路约束

shift 操作约束

• shl 、 shr 约束公式

比较操作

比较操作中的指令每一个都不会修改任何寄存器; 比较的结果存储在flag中。比较指令包含 cmpe 、 cmpa 、 cmpae 、 cmpg 、 cmpge 。比较指令可以分为两类,分别为有符号数的比较和无符号数比较,两者约束过程核心都利用了libsnark中实现的comparison_gadget 。

TinyRam指令集和电路约束

TinyRam指令集和电路约束

其他剩余过程跟有符号数比较约束相同

move 操作约束

• mov 约束公式:

mov的约束比较简单,只需要确保将 [A] 存储到 ri寄存器中,由于mov操作没有修改flag,所以约束需要确保flag的值没有产生变化。约束代码如下:

TinyRam指令集和电路约束

• cmov 约束公式:

TinyRam指令集和电路约束

cmov 的约束条件比mov复杂一些,主要mov的行为跟flag值的变化有关系,同时cmov不会修改flag, 所以约束需要确保flag的值没有变化,cmov的代码如下:

TinyRam指令集和电路约束

Jump 操作约束

这些jump和条件jump 指令都不会修改寄存器和 flag 但是会修改 pc。

• jmp

Jmp操作约束pc值与指令执行结果一致,具体约束代码如下:

TinyRam指令集和电路约束

• cjmp

cjmp 根据flag 条件进行跳转,flag = 1 进行跳转,否则 pc 自增1

约束公式如下:

TinyRam指令集和电路约束

约束代码如下:

TinyRam指令集和电路约束

• cnjmp

cnjmp 根据flag 条件进行跳转,flag = 0 进行跳转,否则 pc 自增1

约束公式如下:

TinyRam指令集和电路约束

约束代码如下:

TinyRam指令集和电路约束

Memory 操作约束

这些是简单的memory load和store操作,其中memory的地址由立即数或寄存器的内容确定。 这些是tinyram 中唯一的寻址 方式 。(tinyram 不支持常见的“base+offset”寻址模式)。

• store.b store.w

对于store.w 取整个arg1val 的值,对于store.b 操作码只会取arg1val的必要部分(例如:最后一个字节),约束代码如下:

TinyRam指令集和电路约束

• load.b 和 load.w

这两个指令我们要求从内存中加载的内容被存储在instruction_results 中,约束代码如下:

TinyRam指令集和电路约束

输入 操作约束

• read

read 操作跟 tape 有关,具体的约束规则是:

1. 上一个tape中的内容被读完,没有内容可读,不会读取下一个tape。

2. 上一个tape中的内容被读完,没有内容可读,flag 被设置为1

3. 如果当前执行的指令是read,那么read读取到的内容和tape 输入内容一致

4. 从tape1 以外的地方读取内容, flag 被设置为1

5. result 为 不为0,意味着 flag 为0

约束代码:

TinyRam指令集和电路约束

输出 操作约束

该指令表示程序已经完成了计算,因此不能再允许其他操作

• answer

当程序的输出值被接受,has_accepted 会被设置为1, 程序返回值能够被正常接受意味着当前的指令为 answner 以及 arg2 value 为0。

约束代码如下:

TinyRam指令集和电路约束

其他

当然除了上述提到的一些指令相关的约束外,tinyram还有一些pc一致性、参数编解码、内存检查等各种约束。这些约束通过R1CS系统组合起来构成一个完成的tinyram 约束系统。所以这也是R1CS形式的tinyram生成约束数量较多的根本原因。

这里引用一个 tinyram介绍ppt 的图片,展示一个ERC20 transfer 用tinyram 生成证明需要的时间消耗。

TinyRam指令集和电路约束

从上图的例子可以得出结论:使用 vnTinyram + zk-SNARKs 验证所有 EVM 操作是不可能的,只适合验证少量的指令的计算验证,可以使用vnTinyram验证 EVM的部分计算类型的opcode。

关于我们

Sin7y成立于2021年,由顶尖的区块链 开发者 组成。我们既是项目孵化器也是区块链技术研究团队,探索EVM、 Layer2 跨链 隐私计算 、自主支付解决方案等最重要和最前沿的技术。

 

Disclaimer: The copyright of this article belongs to the original author and does not represent MyToken(www.mytokencap.com)Opinions and positions; please contact us if you have questions about content