zkevm-docs/5-state.markdown

-TODO
+# 布局
+如下几列。注意，和LookupEntry的State基本一致。
+```rust
+pub struct StateCircuitConfig<F> {
+    q_enable: Selector,
+    /// Type of value, one of stack, memory, storage, call context, call data or return data
+    /// A `BinaryNumberConfig` can return the indicator by method `value_equals`
+    tag: BinaryNumberConfig<Tag, LOG_NUM_STATE_TAG>,
+    /// Stamp that increments for each state operation, unique for each row
+    stamp: Column<Advice>,
+    /// High 128-bit value of the row
+    value_hi: Column<Advice>,
+    /// Low 128-bit value of the row
+    value_lo: Column<Advice>,
+    /// Call id (other types) or contract address (storage type only)
+    call_id_contract_addr: Column<Advice>,
+    /// High 128-bit of the key (storage type only)
+    pointer_hi: Column<Advice>,
+    /// Low 128-bit of the key (storage type only) or call context tag
+    /// Or stack pointer or memory address or data index (call data and return data)
+    pointer_lo: Column<Advice>,
+    /// Whether it is write or read, binary value
+    is_write: Column<Advice>,
+    _marker: PhantomData<F>,
+}
+```
+其中，tag我们没有简单的使用一个advice列，而是用了一个电路小工具名叫“BinaryNumberConfig/BinaryNumberChip”。它既可以表示一个tag，也可以当做动态选择器，用于启用约束。例如，我们想tag的值为stack(1)时启动约束1，为memory(0)时启动约束2。那么，示例代码如下
+```rust
+let condition_1 = tag.value_equals(1);
+let condition_2 = tag.value_equals(0);
+vec![condition_1 * constraint_1, condition_2 * constraint_2]
+```
 
-排序：在当做电路的输入之前，需要将这个table排序。按元组排序：先按tag，再按callid, pointer hi, pointer, stamp的顺序排序。
+# 约束
 
+为了保证读写一致性，我们需要排序，按照如下顺序排序的：先按tag，再按callid, pointer hi, pointer lo, stamp的顺序排序。
 
-验证排序的方式：将元组编码为16bit的limbs，假设有L个。（可以bit更大但是那样比较难做range proof）。上下两行的limbs作差，有L个diff。第一个非零的diff，index记为first_diff_limb。要求diff[first_diff_limb]==0即可。
+在开发的代码中，例如Rust语言，排序十分简单。难的是在电路中增加约束保证整个Witness的行是符合排序规则的。参考scroll的电路，我们使用如下方法。
 
+## 约束排序的方式
 
-具体做法：用binary表示first_diff_limb. 需要用log_2 L个变量。再定义变量limb_diff表示diff[first_diff_limb]。再定义inv表示前者的逆。				
-约束1：建立一个expr数组v，是diff的累计RLC：[diff[0], diff[0]+r diff[1], diff[0]+r diff[1]+r' diff[2]...]。约束first_diff_limb.equal(i) * v[i] == 0。即，前first_diff_limb是否都为0。注：equal是binary表示的一种工具。				
+将tag, callid, pointer hi, pointer lo, stamp元组编码为16-bit的limbs，假设有L个limbs。（可以bit更大但是那样比较难做range proof）。上下两行的limbs作差，有L个diff。第一个非零的diff，index记为first_diff_limb。要求diff[first_diff_limb]==0即可。
+
+具体做法：
+- 用BinaryNumberChip表示变量first_diff_limb。需要用log_2(L)个变量。
+- 再定义变量limb_diff表示diff[first_diff_limb]。
+- 再定义inv表示前者的逆。				
+- 约束1：建立一个expr数组v，是diff的累计RLC：[diff[0], diff[0]+r diff[1], diff[0]+r diff[1]+r' diff[2]...]。约束first_diff_limb.value_equals(i) * v[i] == 0。即，前first_diff_limb是否都为0。注：value_equals(x)方法是BinaryNumberChip中用来判断值是否等于x的，若等于输出1，否则输出0。				
 注：也许可以把RLC改成^2				
-约束2：first_diff_limb.equal(i) * diff[i] - limb_diff。即，limb_diff值是否正确				
-约束3：limb_diff存在inv. 1-limb_diff * inv == 0。即它非零				
-约束4：limb_diff in range u16
\ No newline at end of file
+- 约束2：first_diff_limb.value_equals(i) * diff[i] - limb_diff。即，limb_diff值是否按照定义等于diff[first_diff_limb]。				
+- 约束3：limb_diff存在inv。 1-limb_diff * inv == 0。即它非零。
+- 约束4：limb_diff in range u16，即[0,2^16-1]。因为两个limb如果都属于u16，大的limb（下一行的）减小的limb（上一行的）的diff必然也是u16。反之，小的limb减大的limb的diff必然不是u16。
+
+## 不同state类型的约束
+
+stack的约束：TODO
+
+memory的约束：TODO。。。
\ No newline at end of file