简介
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、跨链、隐私计算、自主支付解决方案等最重要和最前沿的技术。
微信公众号：Sin7Y
GitHub | Twitter | Telegram | Medium| Mirror | HackMD | HackerNoon
