zkevm-docs/3-witness.markdown

@@ -19,13 +19,14 @@ pub struct Witness {
 
 因为不同子表格、不同列使用的行数可能不同，然而最终的表格显示出来所有列应该使用相同的行数，所以给短的列数填充默认值，一般为0。代码里一般用Rust的Option的None表示填充的默认值。
 
-以下举一个简单的例子。一个智能合约的执行轨迹包含4步：PUSH一个数，PUSH一个数，ADD，STOP。其字节码（易读格式）为
+## 例子
+以下举一个简单的例子，**并不是我们目前的设计，只是为了好理解**。一个智能合约的执行轨迹包含4步：PUSH一个数，PUSH一个数，ADD，STOP。其字节码（易读格式）为
 
 > PUSH1 1 PUSH1 2 ADD STOP
 
 那么可以简单的设计core, state, bytecode这三个子表格（作为示例，并非正式设计）：
 
-## Core
+### 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 |
@@ -37,7 +38,7 @@ core子表格负责表示4步轨迹，其列可以包含pc, opcode, operand （
 
 （对上表中的stack_pointer如有不理解，可看下段的介绍。stamp也在下段介绍。）
 
-## State
+### State
 state子表格负责执行轨迹涉及的所有状态读写，并保持读写的一致性，即读的值必须是上次写的值。根据此例子，读写都是栈上的，因此我们可以暂时不考虑memory，storage的读写，只考虑栈的。每一步轨迹涉及如下读写：
 
 1. PUSH1 1: 一次写，将值1写到栈的顶，此时栈顶高度为1（我们不从0开始，从1开始）
@@ -68,7 +69,12 @@ state子表格负责执行轨迹涉及的所有状态读写，并保持读写的
 >
 > 除了每个操作数的stack pointer，我们还需要知道此时栈顶到底多高，因此core子表格中应该还需要加一列，名字为stack height，记录在这一步各种操作完成之后的栈顶高度。stamp同理，需要一个stamp_at_end记录在这一步各种操作完成之后的计数器的值。
 
-## Bytecode
+保证读写一致性的约束，在此文档中略讲如下，详见state文档。将state子表格以行为单位进行排序，按照先stack pointer，再stamp的顺序进行升序排序。这样，一行X若是读操作（is_write=0），它的上一行X-1如果和行X的stack pointer相同，则行X-1必然是相同位置的上一次操作，因此行X的value必须要等于行X-1的value。写成表达式，需要将“行X若是读操作，上一行X-1如果和行X的stack pointer相同”写成一个二进制变量作为条件（`condition`），则约束表达式是：
+```
+condition * (value-value_prev)
+```
+如何写成`condition`，以及如何约束排序，详见state文档。
+### Bytecode
 
 bytecode子表格用来放置被执行的合约的字节码。此表格较为静态，不会依据执行轨迹构建，而是依据程序字节码构建。在这个简单的例子中，我们需要两列：计数器cnt和值byte。计数器从0开始递增。byte记录一个字节的值，可以是PUSH1, ADD, STOP，也可以是例子里跟在PUSH1后的值。
 
@@ -85,7 +91,7 @@ bytecode子表格用来放置被执行的合约的字节码。此表格较为静
 | 4   | 0x01 (ADD)   |
 | 5   | 0x00 (STOP)  |
 
-## 子表格间关系
+### 子表格间关系
 
 子表格、子电路基本是通过lookup进行关联的。