GitLab

简介

证据Witness是一张大表格，列数对应着zk电路里的列column，行数则依据执行轨迹而定。

Witness的列也可以按照功能拆分，拆分成Core, State, Bytecode的子表格，像子电路一样。子表格决定着子电路的列的设置，数值的填入，也间接决定着约束的设置。它也是从EVM程序的执行轨迹到zk电路逻辑的中间形式。因此，子表格的设计是整个zkEVM设计的重点。

代码里，不同子表格使用Vec<Row>来表示，例如Core子表格就是Vec<core::Row>。结构体Row是所需数值的集合，例如struct Row { pc: U256, opcode: U256};。而Witness就是将子表格集合起来的结构体：

pub struct Witness {
    pub bytecode: Vec<bytecode::Row>,
    pub copy: Vec<copy::Row>,
    pub core: Vec<core::Row>,
    pub exp: Vec<exp::Row>,
    pub public: Vec<public::Row>,
    pub state: Vec<state::Row>,
    pub arithmetic: Vec<arithmetic::Row>,
}

因为不同子表格、不同列使用的行数可能不同，然而最终的表格显示出来所有列应该使用相同的行数，所以给短的列数填充默认值，一般为0。代码里一般用Rust的Option的None表示填充的默认值。

以下举一个简单的例子。一个智能合约的执行轨迹包含4步：PUSH一个数，PUSH一个数，ADD，STOP。其字节码（易读格式）为

PUSH1 1 PUSH1 2 ADD STOP

那么可以简单的设计core, state, bytecode这三个子表格（作为示例，并非正式设计）：

Core

core子表格负责表示4步轨迹，其列可以包含pc, opcode, operand （操作数，此处最多3个，因为ADD是a+b=c），以及负责表示操作数性质的列，例如stack_pointer（操作数在栈上的高度），is_write（是从栈读，还是写入）。操作数对于不同opcode不同，空的地方视为填充默认值0。

（对上表中的stack_pointer如有不理解，可看下段的介绍。stamp也在下段介绍。）

State

state子表格负责执行轨迹涉及的所有状态读写，并保持读写的一致性，即读的值必须是上次写的值。根据此例子，读写都是栈上的，因此我们可以暂时不考虑memory，storage的读写，只考虑栈的。每一步轨迹涉及如下读写：

1. PUSH1 1: 一次写，将值1写到栈的顶，此时栈顶高度为1（我们不从0开始，从1开始）
2. PUSH1 2: 一次写，将值2写到栈的顶，此时栈顶高度为2
3. ADD: 两次读，读出栈顶2个数，读的过程中，两个数在栈中的高度分别是2、1。一次写，将2个数的和写入栈顶，此时栈顶高度为1
4. STOP: 没有读写。

由此可见，共有5次栈读写操作。对于每次操作，我们用一行来表示。（由此可见，不同子电路的一行含义不同。）每一行中，我们需要：value, stack_pointer, is_write。为了区分在同一stack_pointer的多次不同操作，我们还需要一个栈操作计数器，即这是总计第几次操作。我们可以选择从1开始计数。这一计数器命名为stamp。

如果用在同一栈高度，这是第几次操作，比较难设计。因此用总计第几次操作。

由上述原因，core子表格的每个operand要增加一列stamp，表示这个计数器的值。

综上，state表格如下：

思考：为什么需要stack pointer？只用一个is_write表示push、pop行不行？

在go/java/c++/rust代码里，栈push pop等操作会“自动”从栈顶操作。但是zk没有这么自动，它不知道栈顶是哪里，需要用变量来告诉它！

除了每个操作数的stack pointer，我们还需要知道此时栈顶到底多高，因此core子表格中应该还需要加一列，名字为stack height，记录在这一步各种操作完成之后的栈顶高度。stamp同理，需要一个stamp_at_end记录在这一步各种操作完成之后的计数器的值。

Bytecode

bytecode子表格用来放置被执行的合约的字节码。此表格较为静态，不会依据执行轨迹构建，而是依据程序字节码构建。在这个简单的例子中，我们需要两列：计数器cnt和值byte。计数器从0开始递增。byte记录一个字节的值，可以是PUSH1, ADD, STOP，也可以是例子里跟在PUSH1后的值。

为什么需要cnt？还是因为zk没有非常自动，在一行里，它不知道此行的行号是多少。如果只有byte，无法区分这个byte是字节码的第几个！

表格示例如下：

子表格间关系

子表格、子电路基本是通过lookup进行关联的。

对于core中的栈的读写，体现在电路上，是从core子电路每个操作数及其属性变量，往state子电路的对应列进行lookup。

对于core中的pc和opcode，体现在电路上，是从core中这两列，往bytecode子电路的两列进行lookup。

后续文档会详细说明。