ExecutionRecord为了实现对brainfuck程序的约束,需要将每条指令运行过程中的一些信息收集起来,放到ExecutionRecord中。ExecutionRecord中会包含多种event列表,后续会被转换为trace表.一条指令会生成多个event,每条指令
为了实现对 brainfuck 程序的约束,需要将每条指令运行过程中的一些信息收集起来,放到 ExecutionRecord 中。ExecutionRecord 中会包含多种 event 列表,后续会被转换为 trace 表.
一条指令会生成多个 event,每条指令都会生成 CpuEvent,大多数指令会生成 MemoryEvent,用来对内存访问一致性进行约束。
每条指令还会生成特定类型的 event,例如
+ 和 - 指令会生成 AluEvent
[ 和 ] 指令会生成 JumpEvent
> 和 < 指令会生成 MemInstrEvent
, 和 . 指令会生成 IoEvent
以 + 指令为例,假设它是第一条指令,AluEvent 为
AluEvent {
pc: 0,
opcode: Add,
next_mv: 1,
mv: 0
}
CpuEvent 为
CpuEvent {
clk: 0,
pc: 0,
next_pc: 1,
mp: 0,
next_mp: 0,
mv: 0,
next_mv: 1,
mv_access: Some(Read(MemoryReadRecord {
value: 0,
timestamp: 1,
prev_timestamp: 0
})),
next_mv_access: Some(Write(MemoryWriteRecord {
value: 1,
timestamp: 2,
prev_value: 0,
prev_timestamp: 1
}))
}
MemoryEvent 为
MemoryEvent {
addr: 0, // 对应 mp
initial_mem_access: MemoryRecord {
timestamp: 0,
value: 0
},
final_mem_access: MemoryRecord {
timestamp: 2,
value: 1
}
}
CpuEvent 和 MemoryEvent 都会记录内存访问信息,区别是,CpuEvent 记录对某个地址的每一次内存访问,而 MemoryEvent 只记录对某个地址的初始访问和最终访问。
当程序运行结束后,ExecutionRecord 中便收集到了指令运行过程中的所有信息,可通过每个 Chip 的 generate_trace 函数转为 trace 表。trace 表的列跟踪寄存器随时间的变化情况,行代表机器在某一时间点的状态。
例如 AluEvent 可通过 AddSubChip 中的 generate_trace() 转为 trace,一个 AluEvent 对应 trace 中的一行:
/// Create a row from an event.
fn event_to_row<F: PrimeField>(
&self,
event: &AluEvent,
cols: &mut AddSubCols<F>,
blu: &mut impl ByteRecord,
) {
cols.pc = F::from_canonical_u32(event.pc);
cols.is_add = F::from_bool(matches!(event.opcode, Opcode::Add));
cols.is_sub = F::from_bool(matches!(event.opcode, Opcode::Sub));
let operand_1 = if event.opcode == Opcode::Add { event.mv } else { event.next_mv };
let operand_2 = 1;
cols.add_operation.populate(blu, operand_1, operand_2);
cols.operand_1 = F::from_canonical_u8(operand_1);
cols.operand_2 = F::from_canonical_u8(operand_2);
}
例如对于程序 ++,AluChip 的 trace 表为:
| pc | operand_1 | operand_2 | value | carry | is_add | is_sub |
|---|---|---|---|---|---|---|
| 0 | 0 | 1 | 1 | 0 | 1 | 0 |
| 1 | 1 | 1 | 2 | 0 | 1 | 0 |
其中
+ 还是 - 指令,都是 mv 加 1 或减 1+ 指令;is_sub 表示是否为 - 指令,因为 AluChip 将 + 和 - 指令合并到一个 chip 中。如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!