3 witness

Witness

简介

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

Witness的列也可以按照功能拆分，拆分成Core, State, Bytecode的子表格，像子电路一样。子表格决定着子电路的列的设置，数值的填入，也间接决定着约束的设置。

代码里，不同子表格使用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。

pc	opcode	operand	stack pointer	is_write	stamp	operand	stack pointer	is_write	stamp	operand	stack pointer	is_write	stamp
0	PUSH1	1	1	1	1
2	PUSH1	2	2	1	2
4	ADD	2	2	0	3	1	1	0	4	3	1	1	5
5	STOP

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

State

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

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

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

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

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

综上，state表格如下：

stamp	value	stack pointer	is_write
1	1	1	1
2	2	2	1
3	2	2	0
4	1	1	0
5	3	1	1

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

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

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

保证读写一致性的约束，在此文档中略讲如下，详见state文档。将state子表格以行为单位进行排序，按照先stack pointer，再stamp的顺序进行升序排序。

上个示例中排序后的表格如下图所示：

stamp	value	stack pointer	is_write
1	1	1	1
4	1	1	0
5	3	1	1
2	2	2	1
3	2	2	0

a. 检查第 2 行和第 1 行：

第 2 行是读取操作（is_write = 0），和第1行的stack_pointer 相同。
约束条件：value_X = value_{X-1}，即 1 = 1，满足约束。

b. 检查第 5 行和第 4 行：

第 5 行是读取操作（is_write = 0），和第4行的stack_pointer 相同。
约束条件：value_X = value_{X-1}，即 2 = 2，满足约束。

通过排序和施加约束，我们确保了读取的值总是等于前一次写入的值，保证了读写操作的一致性。

这样，一行X若是读操作（is_write=0），它的上一行X-1如果和行X的stack pointer相同，则行X-1必然是相同位置的上一次操作，因此行X的value必须要等于行X-1的value。

条件可以用布尔代数表示。如果行 X 是读操作（is_write = 0）且 stack_pointer 相同，则条件为真。我们用二进制变量表示条件：

condition = (is_write_X = 0) * (stack_pointer_X = stack_pointer_{X-1})

写成表达式，需要将“行X若是读操作，上一行X-1如果和行X的stack pointer相同”写成一个二进制变量作为条件（condition），则约束表达式是：

condition * (value_X - value_{X-1}) = 0

详细的如何写成condition，以及如何约束排序，详见state文档。

Bytecode

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

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

表格示例如下：

cnt	byte
0	0x60 (PUSH1)
1	0x01
2	0x60 (PUSH1)
3	0x02
4	0x01 (ADD)
5	0x00 (STOP)

子表格间关系

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

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

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

后续文档会详细说明。例如，此文档略去了PUSH1后边跟的数的lookup。