|
|
|
## 简介
|
|
|
|
|
|
|
|
证据Witness是一张大表格，列数对应着zk电路里的列column，行数则依据执行轨迹而定。
|
|
|
|
|
|
|
|
Witness的列也可以按照功能拆分，拆分成Core, State, Bytecode的子表格，像子电路一样。子表格决定着子电路的列的设置，数值的填入，也间接决定着约束的设置。它也是从EVM程序的执行轨迹到zk电路逻辑的中间形式。因此，子表格的设计是整个zkEVM设计的重点。
|
|
|
|
|
|
|
|
代码里，不同子表格使用`Vec<Row>`来表示，例如Core子表格就是`Vec<core::Row>`。结构体Row是所需数值的集合，例如`struct Row { pc: U256, opcode: U256};`。而Witness就是将子表格集合起来的结构体：
|
|
|
|
```rust
|
|
|
|
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的读写，只考虑栈的。每一步轨迹涉及如下读写：
|
|
|
|
|
|
|
|
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表格如下：
|
|
|
|
|
|
|
|
| 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` 相同，则条件为真。我们用二进制变量表示条件：
|
|
|
|
|
|
|
|
```azure
|
|
|
|
condition = (is_write_X = 0) * (stack_pointer_X = stack_pointer_{X-1})
|
|
|
|
```
|
|
|
|
|
|
|
|
写成表达式，需要将“行X若是读操作，上一行X-1如果和行X的stack pointer相同”写成一个二进制变量作为条件（`condition`），则约束表达式是：
|
|
|
|
```azure
|
|
|
|
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。
|
|
|
|
|
|
|
|
## 简介
|
|
|
|
|
|
|
|
证据Witness是一张大表格，列数对应着zk电路里的列column，行数则依据执行轨迹而定。
|
|
|
|
|
|
|
|
Witness的列也可以按照功能拆分，拆分成Core, State, Bytecode的子表格，像子电路一样。子表格决定着子电路的列的设置，数值的填入，也间接决定着约束的设置。它也是从EVM程序的执行轨迹到zk电路逻辑的中间形式。因此，子表格的设计是整个zkEVM设计的重点。
|
|
|
|
|
|
|
|
代码里，不同子表格使用`Vec<Row>`来表示，例如Core子表格就是`Vec<core::Row>`。结构体Row是所需数值的集合，例如`struct Row { pc: U256, opcode: U256};`。而Witness就是将子表格集合起来的结构体：
|
|
|
|
```rust
|
|
|
|
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的读写，只考虑栈的。每一步轨迹涉及如下读写：
|
|
|
|
|
|
|
|
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表格如下：
|
|
|
|
|
|
|
|
| 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` 相同，则条件为真。我们用二进制变量表示条件：
|
|
|
|
|
|
|
|
```azure
|
|
|
|
condition = (is_write_X = 0) * (stack_pointer_X = stack_pointer_{X-1})
|
|
|
|
```
|
|
|
|
|
|
|
|
写成表达式，需要将“行X若是读操作，上一行X-1如果和行X的stack pointer相同”写成一个二进制变量作为条件（`condition`），则约束表达式是：
|
|
|
|
```azure
|
|
|
|
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。 |
|
|
\ No newline at end of file |
