zkevm-docs/3-witness.markdown

@@ -69,11 +69,45 @@ state子表格负责执行轨迹涉及的所有状态读写，并保持读写的
 >
 > 除了每个操作数的stack pointer，我们还需要知道此时栈顶到底多高，因此core子表格中应该还需要加一列，名字为stack height，记录在这一步各种操作完成之后的栈顶高度。stamp同理，需要一个stamp_at_end记录在这一步各种操作完成之后的计数器的值。
 
-保证读写一致性的约束，在此文档中略讲如下，详见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文档。
+保证读写一致性的约束，在此文档中略讲如下，详见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` 相同，则条件为真。我们用二进制变量表示条件：
+
+$$
+\text{condition} = (\text{is\_write}_X = 0) \times (\text{stack\_pointer}_X = \text{stack\_pointer}_{X-1})
+$$
+
+
+写成表达式，需要将“行X若是读操作，上一行X-1如果和行X的stack pointer相同”写成一个二进制变量作为条件（`condition`），则约束表达式是：
+
+$$
+\text{condition} \times (value_X - value_{X-1}) = 0
+$$
+详细的如何写成`condition`，以及如何约束排序，详见state文档。
 ### Bytecode
 
 bytecode子表格用来放置被执行的合约的字节码。此表格较为静态，不会依据执行轨迹构建，而是依据程序字节码构建。在这个简单的例子中，我们需要两列：计数器cnt和值byte。计数器从0开始递增。byte记录一个字节的值，可以是PUSH1, ADD, STOP，也可以是例子里跟在PUSH1后的值。