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

-# ADD
-本节和接下来的章节主要介绍 EVM中各个指令的具体操作、约束条件和 witness 表示，以及如何在电路设计中实现和验证相关指令。
+# ADD 指令
+本节和接下来的章节主要介绍 EVM 中各个指令的具体操作、约束条件和 witness 表示，以及如何在电路设计中实现和验证相关指令。
 ### 概述
 
 概述：加法指令，对栈中的两个值进行加法计算（256位）。
@@ -11,8 +11,8 @@ trace示例：
 ```code
 // Example 1 
 // Result 20 //0x14
-PUSH1 10 //0x10
-PUSH1 10 //0x10
+PUSH1 10 //0x0A
+PUSH1 10 //0x0A
 ADD
 
 // Example 2
@@ -41,6 +41,8 @@ ADD
 
 - 栈内容：`[result]`
 
+> 注：SUB指令、MUL指令、DIV指令、MOD指令与ADD指令相似，因此实现在同一代码文件中，参考 `zkevm-circuits/src/execution/add_sub_mul_div_mod.rs` 。
+
 ### Witness Core Row
 
 core row中的表格设计如下：
@@ -51,7 +53,7 @@ core row中的表格设计如下：
 | 1    | STATE (stack_pop_a) | STATE (stack_pop_b) | STATE (stack_push) | -    |
 | 0    | DYNA_SELECTOR       | AUX                 | -                  | -    |
 
-cnt=2，vers[0]~vers[8]的位置用来存放arithmetic table lookup；
+cnt=2，vers[0]~vers[8]的位置用来存放arithmetic table lookup，目的是将具体的算数约束放在arithmetic子电路中，将core子电路与具体的算数约束解耦；
 
 cnt=1，vers[0]~vers[7]的位置用来存放栈顶弹出的值stack_pop_a；
 
@@ -59,41 +61,17 @@ cnt=1，vers[8]~vers[15]的位置用来存放栈顶弹出的值stack_pop_b；
 
 cnt=1，vers[16]~vers[23]的位置用来存进栈顶的值stack_push。
 
-`DYNA_SELECTOR` 和 `AUX` 部分可能存储动态选择器和辅助信息，但在这个具体表格中未被使用。
-
-其中，对于 `ADD` 操作，给出的算术表查找ARITH的具体值可以如下：
-
-| tag  | operand_a_hi | operand_a_lo | operand_b_hi | operand_b_lo | result_hi | result_lo | unused_hi | unused_lo |
-| ---- | ------------ | ------------ | ------------ | ------------ | --------- | --------- | --------- | --------- |
-| ADD  | 0x00         | 0x10         | 0x00         | 0x10         | 0x00      | 0x20      | 0x00      | 0x00      |
-| ADD  | 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF | 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF | 0x00         | 0x01         | 0x00      | 0x00      | 0x00      | 0x00      |
-
-
-各个字段的含义如下：
-
-- `tag`：表示算术操作的类型，如 `ADD`、`SUB` 等。
-- `operand_a_hi`：操作数 A 的高位部分。
-- `operand_a_lo`：操作数 A 的低位部分。
-- `operand_b_hi`：操作数 B 的高位部分。
-- `operand_b_lo`：操作数 B 的低位部分。
-- `result_hi`：结果的高位部分。
-- `result_lo`：结果的低位部分。
--  `unused `: 没有使用的部分
-
-这些字段可以用来存储 256 位数值的高 128 位和低 128 位。
-
-在上面的示例中：
-
-- 第一个条目表示 10 + 10 = 20。
-- 第二个条目表示最大值加 1，结果回到 0（因为是模 2^256 运算）。
-
 ### 门约束
 
 1. Auxiliary字段约束：
 
    这些约束用于辅助字段，如 `state_stamp`、`stack_pointer`、`log_stamp` 和 `read_only`，确保这些字段在操作期间保持一致。
 
-2. Stack Value约束：
+2. Core专有的单功能列约束：
+
+   约束单功能列如`pc`、`code_addr`等，确保下一个状态其值正确。
+
+3. Stack Value约束：
 
    这些约束用于栈的值，包括以下内容：
 
@@ -103,7 +81,9 @@ cnt=1，vers[16]~vers[23]的位置用来存进栈顶的值stack_push。
    - `stack_pointer`
    - `is_write`
 
-3. lookup_value约束：
+   同时提取出栈中的值，即`lookup_stack_pop_a`, `lookup_stack_pop_b`, `lookup_stack_push`。
+
+4. lookup_value约束：
 
    这些约束确保算术操作数和栈操作的值一致。具体来说：
 
@@ -113,58 +93,16 @@ cnt=1，vers[16]~vers[23]的位置用来存进栈顶的值stack_push。
 
    这些约束对操作数的高位 (`hi`) 和低位 (`lo`) 进行约束，并确保它们与状态查找中的值相等。
 
-4. 当前的OPCODE=ADD
-
-5. arithmetic tag = ADD
+5. 当前的 OPCODE = ADD
 
-参考如下代码：
-
-```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..3 {
-        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 == 2,
-        ));
-        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 three operands (0..6), since we don't need constraint on the fourth
-    constraints.extend((0..6).map(|i| {
-        (
-            format!("operand[{}] in arithmetic = in state lookup", i),
-            arithmetic_operands[i].clone() - arithmetic_operands_full[i].clone(),
-        )
-    }));
-
-    // 其它约束 ...
-    constraints
-}
-```
+6. 用于 arithmetic table lookup 的 arithmetic tag = ADD
 
 ### LookUp约束
 
 
 #### get_lookups
 
+TODO：使用md的 - ，列出四个Lookup都是啥。然后把这段其他的，包括参考代码，删了。
 
 这里的四个lookup, 类型为LookupEntry::State和LookupEntry::Arithmetic, 具体可以参考Witness Core Row部分的说明。