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。

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

位操作

整数操作

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

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

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

输入 操作

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

输出 操作

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

指令集约束

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 文件夹下。

位操作约束

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

关于我们

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