zkevm-docs/4-core/core-addmod.markdown

@@ -28,6 +28,15 @@ ADDMOD
 
 core row中的表格设计如下：
 
+| cnt  | ver[0-7]            | ver[8-15] | ver[16-23] | ver[24-31] | 其他 |
+| ---- | ------------------- | --------- | ---------- | ---------- | ---- |
+| 2    | ARITH               | -         | -          | -          | -    |
+| 1    | STATE (stack_pop_n) | -         | -          | -          | -    |
+| 1    | STATE (stack_pop_b) | -         | -          | -          | -    |
+| 1    | STATE (stack_pop_a) | -         | -          | -          | -    |
+| 1    | STATE (stack_push)  | -         | -          | -          | -    |
+| 0    | DYNA_SELECTOR       | AUX       | -          | -          | -    |
+
 cnt=2，vers[0]~vers[8]的位置用来存放arithmetic table lookup；
 
 cnt=1，vers[0]~vers[7]的位置用来存放栈顶弹出的值stack_pop_n；
@@ -38,36 +47,109 @@ cnt=1，vers[16]~vers[23]的位置用来存放栈顶弹出的值stack_pop_a；
 
 cnt=1，vers[24]~vers[31]的位置用来存进栈顶的值stack_push。
 
+对于 `ADDMOD` 操作，给出的算术表查找ARITH的具体值可以如下：
 
-```
-/// +---+-------+-------+-------+----------+
-/// |cnt| 8 col | 8 col | 8 col | not used |
-/// +---+-------+-------+-------+----------+
-/// | 2 | ARITH  |      |       |          |
-/// | 1 | STATE | STATE | STATE | STATE    |
-/// | 0 | DYNA_SELECTOR   | AUX            |
-/// +---+-------+-------+-------+----------+
-```
+| tag    | operand_a_hi | operand_a_lo | operand_b_hi | operand_b_lo | operand_n_hi                       | operand_n_lo                       | result_hi | result_lo |
+| ------ | ------------ | ------------ | ------------ | ------------ | ---------------------------------- | ---------------------------------- | --------- | --------- |
+| ADDMOD | 0x00         | 0x10         | 0x00         | 0x10         | 0x00                               | 0x08                               | 0x00      | 0x04      |
+| ADDMOD | 0x00         | 0x02         | 0x00         | 0x02         | 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF | 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF | 0x00      | 0x01      |
 
+各个字段的含义如下：
 
+- `tag`：表示算术操作的类型，如 `ADDMOD`。
+- `operand_a_hi`：操作数 A 的高位部分。
+- `operand_a_lo`：操作数 A 的低位部分。
+- `operand_b_hi`：操作数 B 的高位部分。
+- `operand_b_lo`：操作数 B 的低位部分。
+- `operand_n_hi`：操作数 N 的高位部分。
+- `operand_n_lo`：操作数 N 的低位部分。
+- `result_hi`：结果的高位部分。
+- `result_lo`：结果的低位部分。
 
+这些字段可以用来存储 256 位数值的高 128 位和低 128 位。
 
+在上面的示例中：
+
+- 第一个条目表示 10 + 10 = 20，20 % 8 = 4。
+- 第二个条目表示 2 + 2 = 4，4 % (2^256 - 1) = 1。
 
 ### 门约束
-1. Auxiliary字段约束（state_stamp、stack_pointer、log_stamp、read_only）
-2. Stack Value约束（tag、state_stamp、 call_id、stack_pointer、is_write）
-3. 当前的OPCODE=ADDMOD
-4. arithmetic tag = ADDMOD
-5. todo...
 
-参考如下代码：
+1. Auxiliary字段约束：
 
-```Rust
-todo!()
+   这些约束用于辅助字段，如 `state_stamp`、`stack_pointer`、`log_stamp` 和 `read_only`，确保这些字段在操作期间保持一致。
 
-```
+2. Stack Value约束：
+
+   这些约束用于栈的值，包括以下内容：
+
+   - `tag`
+
+   - `state_stamp`
+
+   - `call_id`
+
+   - `stack_pointer`
 
+   - `is_write`
 
+3. lookup_value约束：
+
+   这些约束确保算术操作数和栈操作的值一致。具体来说：
+
+   - `arithmetic_operand_n = lookup_stack_pop_n`
+   - `arithmetic_operand_b = lookup_stack_pop_b`
+   - `arithmetic_operand_a = lookup_stack_pop_a`
+   - `arithmetic_operand_push = lookup_stack_push`
+
+   这些约束对操作数的高位 (`hi`) 和低位 (`lo`) 进行约束，并确保它们与状态查找中的值相等。
+
+4. 当前的OPCODE=ADDMOD
+
+5. arithmetic tag = ADDMOD
+
+参考如下代码：
+
+```Rust
+fn get_constraints(
+    &self,
+    config: &ExecutionConfig<F, NUM_STATE_HI_COL, NUM_STATE_LO_COL>,
+    meta: &mut VirtualCells<F>,
+) -> Vec<(String, Expression<F>)> {
+    let opcode = meta.query_advice(config.opcode, Rotation::cur());
+    // Auxiliary字段约束 ...
+
+    // Stack Value约束 ...
+
+    let mut arithmetic_operands = vec![];
+    for i in 0..4 {
+        let entry = config.get_state_lookup(meta, i);
+        constraints.append(&mut config.get_stack_constraints(
+            meta,
+            entry.clone(),
+            i,
+            NUM_ROW,
+            if i == 0 { 0 } else { -1 }.expr(),
+            i == 3,
+        ));
+        let (_, _, value_hi, value_lo, _, _, _, _) = extract_lookup_expression!(state, entry);
+        arithmetic_operands.extend([value_hi, value_lo]);
+    }
+    
+    let (tag, arithmetic_operands_full) =
+        extract_lookup_expression!(arithmetic, config.get_arithmetic_lookup(meta));
+    // iterate over operands (0..8)
+    constraints.extend((0..8).map(|i| {
+        (
+            format!("operand[{}] in arithmetic = in state lookup", i),
+            arithmetic_operands[i].clone() - arithmetic_operands_full[i].clone(),
+        )
+    }));
+
+    // 其它约束 ...
+    constraints
+}
+```
 
 ### LookUp约束
 
@@ -80,6 +162,40 @@ todo!()
 参考代码如下: 
 
 ```Rust
-todo!()
-
+fn get_lookups(
+    &self,
+    config: &ExecutionConfig<F, NUM_STATE_HI_COL, NUM_STATE_LO_COL>,
+    meta: &mut ConstraintSystem<F>,
+) -> Vec<(String, LookupEntry<F>)> {
+    let stack_lookup_0 = query_expression(meta, |meta| config.get_state_lookup(meta, 0));
+    let stack_lookup_1 = query_expression(meta, |meta| config.get_state_lookup(meta, 1));
+    let stack_lookup_2 = query_expression(meta, |meta| config.get_state_lookup(meta, 2));
+    let stack_lookup_3 = query_expression(meta, |meta| config.get_state_lookup(meta, 3));
+    let arithmetic = query_expression(meta, |meta| config.get_arithmetic_lookup(meta));
+    vec![
+        ("stack pop n".into(), stack_lookup_0),
+        ("stack pop b".into(), stack_lookup_1),
+        ("stack pop a".into(), stack_lookup_2),
+        ("stack push".into(), stack_lookup_3),
+        ("arithmetic lookup".into(), arithmetic),
+    ]
+}
+
+pub(crate) fn get_arithmetic_lookup(&self, meta: &mut VirtualCells<F>) -> LookupEntry<F> {
+    let (hi_0, lo_0, hi_1, lo_1, hi_2, lo_2, hi_3, lo_3, tag) = (
+        meta.query_advice(self.vers[0], Rotation(-2)),
+        meta.query_advice(self.vers[1], Rotation(-2)),
+        meta.query_advice(self.vers[2], Rotation(-2)),
+        meta.query_advice(self.vers[3], Rotation(-2)),
+        meta.query_advice(self.vers[4], Rotation(-2)),
+        meta.query_advice(self.vers[5], Rotation(-2)),
+        meta.query_advice(self.vers[6], Rotation(-2)),
+        meta.query_advice(self.vers[7], Rotation(-2)),
+        meta.query_advice(self.vers[8], Rotation(-2)),
+    );
+    LookupEntry::Arithmetic {
+        tag,
+        values: [hi_0, lo_0, hi_1, lo_1, hi_2, lo_2, hi_3, lo_3],
+    }
+}
 ```
\ No newline at end of file