通过 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$

表示如果 $mvi = 0$ 则 $pc{i+1} -$ 目标指令指针 = 0，进行跳转；否则 $pc_{i+1} - pc_i - 1 = 0$，跳过当前指令 [

] 指令约束

$(pc_{i+1} - dst)mvi + (pc{i+1} - pc_i - 1) \cdot iszero = 0$

表示如果 $mvi \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$

更多细节可见：https://aping-dev.com/index.php/archives/811/

repo：https://github.com/felicityin/zkvm-brainfuck.git