执行轨迹(Execution trace 或者 trace)

执行轨迹是由执行某个计算时,一组机器状态序列构成。说得直白点,就是为了执行某个程序C,申请了W个寄存器,执行了N个步骤,那么执行轨迹可以用一张大小为表来描述。

以斐波那契数列计算为例,可参考ZKHack Mini2 Can you turn up the heat?

fn fib(start: (Felt, Felt), n: usize) -> Felt {
    let mut t0 = start.0;
    let mut t1 = start.1;

    for _ in 0..(n - 1) {
        t1 = t0 + t1;
        core::mem::swap(&mut t0, &mut t1);
    }
    t1
}

可以看到这里使用了2个寄存器,s0s1分别存放每一个中间状态下的数据。模拟n = 10的时候,生成的执行轨迹是一个数组,包含了5对中间状态数据(state[0],state[1])。这里的执行轨迹是由prover定义并生成的,源码如下:

	pub fn build_trace(start: (Felt, Felt), n: usize) -> TraceTable<Felt> {
        
        let mut trace = TraceTable::new(2, n / 2);
        trace.fill(
            |state| {
                state[0] = start.0;
                state[1] = start.1;
            },
            |_, state| {
                state[0] += state[1];
                state[1] += state[0];
            },
        );

        trace
    }

执行轨迹中的数据如下图所示。

image-20220314160016374

这样定义出来的执行轨迹只有2列,状态转换的具体约束条件如下:

		result[0] = next_state[0] - (current_state[0] + current_state[1]);
    result[1] = next_state[1] - (current_state[1] + next_state[0]);

也就是说,每一次状态转换必须满足这2个约束:

  1. s_{0, i+1} = s_{0, i} + s_{1, i}
  2. s_{1, i+1} = s_{1, i} + s_{0, i+1}

相应的约束多项式的度最大为1。因此,创建AIR时,定义状态转换的约束多项式的度为1。

		let degrees = vec![
            TransitionConstraintDegree::new(1),
            TransitionConstraintDegree::new(1),
        ];

此外,AIR中还需要对输入、输出进行约束,参考如下:

		vec![
            Assertion::single(0, 0, self.start.0),       // input contraint
            Assertion::single(1, 0, self.start.1),       // input contraint
            Assertion::single(0, last_step, self.end),   // output contraint
        ]

至此,我们就构建了执行轨迹,并根据执行轨迹构建了对应的约束。

实际上,构建一个合理执行轨迹,并据此设计无懈可击的约束系统是学习并使用ZK-Stark非常重要的一步。如果感兴趣,可以参考**ZKHack Mini1: There’s something in the AIR ** ,帮助更深入地理解AIR。