ExecutionRecord
为了实现对 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 转 Trace
当程序运行结束后,ExecutionRecord 中便收集到了指令运行过程中的所有信息,可通过每个 Chip 的 generate_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);
}
没有评论