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

-TODO
\ No newline at end of file
+
+# ADD
+
+### 概述
+
+概述：加法指令，对栈中的两个值进行加法计算（256位）。
+
+具体操作：从栈顶弹出两个值a和b，进行整数加法（mod 2^256），将结果存进栈。
+
+trace示例：
+
+```code
+// Example 1 
+// Result 0x14
+PUSH1 10
+PUSH1 10
+ADD
+
+// Example 2
+// Result 0x0
+PUSH32 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
+PUSH1 1
+ADD
+```
+
+### Witness Core Row
+
+core row中的表格设计如下：
+
+cnt=2，vers[0]~vers[8]的位置用来存放arithmetic table lookup；
+
+cnt=1，vers[0]~vers[7]的位置用来存放栈顶弹出的值stack_pop_b；
+
+cnt=1，vers[8]~vers[15]的位置用来存放栈顶弹出的值stack_pop_a；
+
+cnt=1，vers[16]~vers[23]的位置用来存进栈顶的值stack_push。
+
+
+```
+/// +---+-------+-------+-------+----------+
+/// |cnt| 8 col | 8 col | 8 col | not used |
+/// +---+-------+-------+-------+----------+
+/// | 2 | ARITH  |      |       |          |
+/// | 1 | STATE | STATE | STATE |          |
+/// | 0 | DYNA_SELECTOR   | AUX            |
+/// +---+-------+-------+-------+----------+
+```
+
+
+#### 解释
+
+
+
+### 门约束
+1. Auxiliary字段约束（state_stamp、stack_pointer、log_stamp、read_only）
+2. Stack Value约束（tag、state_stamp、 call_id、stack_pointer、is_write）
+3. lookup_value约束：lookup_stack_pop_b = stack_top0（栈顶的值需要和lookup_stack_pop_b相等）
+4. lookup_value约束：lookup_stack_pop_a = stack_top1 （弹出一个值后，栈顶的值需要和lookup_stack_pop_a相等）
+5. lookup_value约束：lookup_stack_push = stack_top1（存进一个值后，栈顶的元素需要和lookup_stack_push相等）
+6. lookup_value约束：arithmetic_operand_b = lookup_stack_pop_b，arithmetic_operand_a = lookup_stack_pop_a，arithmetic_operand_push = lookup_stack_push（这里对三个操作数的hi,lo进行约束，需要和state lookup里的值相等）
+7. 当前的OPCODE=ADD
+8. arithmetic tag = 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
+}
+```
+
+
+
+### LookUp约束
+
+cnt=2的vers[0]~vers[8]的位置用来存放操作数的信息。
+
+来源：core
+
+去向：arithmetic
+
+参考代码如下：
+
+
+```Rust
+fn gen_witness(&self, trace: &GethExecStep, current_state: &mut WitnessExecHelper) -> Witness {
+    assert_eq!(trace.op, OpcodeId::ADD);
+    let (stack_pop_a, a) = current_state.get_pop_stack_row_value(&trace);
+    let (stack_pop_b, b) = current_state.get_pop_stack_row_value(&trace);
+    let (arithmetic, result) = operation::add::gen_witness(vec![a, b]);
+
+    let stack_push = current_state.get_push_stack_row(trace, result[0]);
+    let mut core_row_2 = current_state.get_core_row_without_versatile(&trace, 2);
+    core_row_2.insert_arithmetic_lookup(&arithmetic);
+    let mut core_row_1 = current_state.get_core_row_without_versatile(&trace, 1);
+    core_row_1.insert_state_lookups([&stack_pop_a, &stack_pop_b, &stack_push]);
+    let core_row_0 = ExecutionState::ADD.into_exec_state_core_row(
+        trace,
+        current_state,
+        NUM_STATE_HI_COL,
+        NUM_STATE_LO_COL,
+    );
+
+    Witness {
+        core: vec![core_row_2, core_row_1, core_row_0],
+        state: vec![stack_pop_b, stack_pop_a, stack_push],
+        arithmetic,
+        ..Default::default()
+    }
+}
+```
+
+
+#### get_lookups
+
+这里的lookup类型为LookupEntry::State和LookupEntry::Arithmetic。
+
+参考代码如下: 
+
+```Rust
+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 arithmetic = query_expression(meta, |meta| config.get_arithmetic_lookup(meta));
+    vec![
+        ("stack pop a".into(), stack_lookup_0),
+        ("stack pop b".into(), stack_lookup_1),
+        ("stack push".into(), stack_lookup_2),
+        ("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