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 的 stringW−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