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 表。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 表为：

其中

• operand_1 是 mv
• operand_2 永远都是 1，因为无论是 + 还是 - 指令，都是 mv 加 1 或减 1
• carry 表示是否进位
• value 表示计算结果
• is_add 表示是否为 + 指令；is_sub 表示是否为 - 指令，因为 AluChip 将 + 和 - 指令合并到一个 chip 中。

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