通过 chip 的 eval() 函数对 trace 表的列添加约束。本文列出每个 chip 的核心约束。
列出如下变量/寄存器
clk：每条指令运行的时间戳pc：指令指针，指向当前指令ci：当前指令，pc指向的指令mp：内存指针，执行一个内存单元mv：内存值，mp所指内存单元的值
CpuChip
cpu 表的约束如下
- $clk_{i+1} - clk_i - 2 = 0$，因为 clk 代表时间戳，一条指令可能涉及 2 次内存访问，如
+指令涉及一次读内存和一次写内存，需要用不同的时间戳进行区分，所以 clk 每次递增 2 - 对于非跳转指令，有 $pc_{i+1} - pc_{i} - 1 = 0$
- cpu 表中出现的指令 $ci_i$ 必须和 program 表中的一致，通过 lookup 协议实现
- 内存访问一致性：通过 read write 操作之间的 lookup 协议实现
- 对每条指令进行约束，不过 CpuChip 本身不做该项工作，而是通过 lookup 协议由各个指令的 chip 实现
lookup 细节见：https://aping-dev.com/index.php/archives/811
Instruction
每条指令都应该进行约束，将指令分为四种类型，对应四种 chip，分别为 AluChip, JumpChip, IoChip 和 MemoryInstructionsChip
AluChip
AluChip 对 + 和 - 指令进行约束。
+ 指令约束：$mv_{i+1} - mv_i - 1 = 0$
- 指令约束：$mv_{i} - mv_{i+1} - 1 = 0$
JumpChip
JumpChip 对 [ 和 ] 指令进行约束。
引入如下变量
inv：如果mv为 0，则值为 0，否则为mv的乘法逆元iszero：1 - mv * inv的结果，当mv为 0 时，它取值为 1，否则为 0
[ 指令约束
$(pc_{i+1} - dst) \cdot iszero + (pc_{i+1} - pc_i - 1)mv_i = 0$
表示如果 $mv_i = 0$ 则 $pc_{i+1} -$ 目标指令指针 = 0，进行跳转；否则 $pc_{i+1} - pc_i - 1 = 0$，跳过当前指令 [
] 指令约束
$(pc_{i+1} - dst)mv_i + (pc_{i+1} - pc_i - 1) \cdot iszero = 0$
表示如果 $mv_i \ne 0$ 则 $pc_{i+1} -$ 目标指令指针 = 0，进行跳转；否则 $pc_{i+1} - pc_i - 1 = 0$ ，跳过当前指令 ]
IoChip
IoChip 对 , 和 . 指令进行约束。
通过 lookup 协议确保和 cpu 表中出现的 I/O 指令保持一致。
MemoryInstructionsChip
MemoryInstructionsChip 对 > 和 < 指令进行约束。
> 指令约束：$mp_{i+1} - mp_i - 1 = 0$
< 指令约束：$mp_{i} - mp_{i+1} - 1 = 0$
MemoryChip
MemoryChip 用于对内存访问一致性进行约束。
MemoryChip 只记录对某个地址的初始化和最终状态的读写操作 $init, final$，而 CpuChip 记录对某个地址的所有读写操作 $read, write$，内存访问一致性需满足该约束：$read \cup final = write \cup init$
没有评论