zkevm-docs/4-core.markdown

@@ -259,3 +259,210 @@ pub(crate) trait ExecutionGadget<
 /// +---+-------+-------+-------+----------+
 ```
 代码：https://git.code.tencent.com/chainmaker-zk/zkevm/blob/develop/zkevm-circuits/src/execution/add.rs
+
+
+
+# Core Execution
+
+## JUMP
+
+### 概述
+
+概述：无条件跳转，跳转到指定PC的位置，JUMP跳转的位置一定是JUMPDEST所在的位置（JUMPDEST：跳转目标标记位，JUMPDEST标记的位置可以使用JUMP进行跳转）
+
+具体操作：从栈顶弹出一个值，作为要跳转的目标PC的值
+
+trace示例：JUMP指令执行时，会从栈中获取一个值，该值即是要跳转的PC，而该PC一定指向的是JUMPDEST的位置
+
+```shell
+PUSH1 0xa
+PUSH30 0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f
+ADD
+PUSH1 0x25
+JUMP
+JUMPDEST
+PUSH1 0x29
+JUMP
+JUMPDEST
+STOP
+```
+
+### Core Row
+
+core row中的表格设计如下
+
+```shell
+/// +---+-------+-------+-------+--------------------------+
+/// |cnt| 8 col | 8 col | 8 col |             8col         |
+/// +---+-------+-------+-------+--------------------------+
+/// | 1 | STATE |       |       |  Bytecode LookUp         |
+/// | 0 | DYNA_SELECTOR   | AUX                            |
+/// +---+-------+-------+-------+--------------------------+
+```
+
+### 约束
+
+1. 当前的OPCODE=JUMP
+2. Stack Value约束（tag、state_stamp、 call_id、stack_pointer、is_write）
+3. Auxiliary字段约束（state_stamp、stack_pointer、log_stamp、read_only）
+4. next_pc=stack_top_value_lo (从栈顶获取的值作为要跳转的值，pc范围是在u64内的，只取value_lo即可)
+5. Stack_top_value_hi=0 (要对value_hi进行约束为0)
+6. lookup_value约束：lookup_pc=stack_top_value_lo (查找表操作，去向为bytecode table， 用来校验next_pc的合法性， lookup_pc一定也是stack_top_value_lo)
+7. lookup_value约束：lookup_bytecode_addr=`meta.query_advice(config.code_addr, Rotation::cur());` (JUMP指令只是用来当前合约内部的PC跳转，next_pc_bytecode_addr有一定和当前的code_addr是一致的)
+8. lookup_value约束：lookup_not_code=0 (next_pc所指向的位置上JUMPDEST，是具体的指令，并不是bytecode, 而是opcode)
+
+可参考下面示例代码：
+
+```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());
+        let pc_next = meta.query_advice(config.pc, Rotation::next());
+        let code_addr = meta.query_advice(config.code_addr, Rotation::cur());
+
+        // AUX字段约束...
+
+        // stack value约束...
+
+        // 其他约束
+        let (_, _, value_hi, value_lo, _, _, _, _) = extract_lookup_expression!(state, state_entry);
+        let (lookup_addr, expect_next_pc, _, not_code, _, _, _, _) =
+            extract_lookup_expression!(bytecode, config.get_bytecode_full_lookup(meta));
+        constraints.extend([
+            (
+                "opcode is JUMP".into(),
+                opcode - OpcodeId::JUMP.as_u8().expr(),
+            ),
+            (
+                "next pc = stack top".into(),
+                pc_next.clone() - value_lo.clone(),
+            ),
+            ("stack top value_hi = 0".into(), value_hi - 0.expr()),
+            (
+                "bytecode lookup pc = stack top value_lo".into(),
+                value_lo - expect_next_pc.clone(),
+            ),
+            (
+                "bytecode lookup addr = code addr".into(),
+                code_addr - lookup_addr,
+            ),
+            ("bytecode lookup not_code = 0".into(), not_code),
+        ]);
+        constraints
+    }
+```
+
+### LookUp
+
+cnt=1的位置vers[24]~vers[31]的位置用来存放要lookUp的信息(next_pc的合法性，是否在bytecode中存在)
+
+来源：core
+
+去向：bytecode
+
+可参考下面示例代码
+
+#### insert_bytecode_full_lookup
+
+将要lookup的值放入到core row, cnt=1，vers[24]~vers[31]的位置
+
+```rust
+fn gen_witness(&self, trace: &GethExecStep, current_state: &mut WitnessExecHelper) -> Witness {
+  //...
+  core_row_1.insert_bytecode_full_lookup(
+              next_pc.as_u64(),
+              OpcodeId::JUMPDEST,
+              core_row_1.code_addr,
+              Some(0.into()),
+          );
+  // ...
+}
+
+/// We can skip the constraint by setting code_addr to 0
+ pub fn insert_bytecode_full_lookup(
+        &mut self,
+        pc: u64,
+        opcode: OpcodeId,
+        code_addr: U256,
+        push_value: Option<U256>,
+    ) {
+        // this lookup must be in the row with this cnt
+        assert_eq!(self.cnt, 1.into());
+
+        for (cell, value) in [
+            &mut self.vers_24,
+            &mut self.vers_25,
+            &mut self.vers_26,
+            &mut self.vers_27,
+            &mut self.vers_28,
+            &mut self.vers_29,
+            &mut self.vers_30,
+            &mut self.vers_31,
+        ]
+        .into_iter()
+        .zip([
+            Some(code_addr),
+            Some(pc.into()),
+            Some(opcode.as_u8().into()),
+            Some(0.into()), // non_code must be 0
+            push_value.map(|x| (x >> 128).as_u128().into()),
+            push_value.map(|x| (x.low_u128().into())),
+            Some(opcode.data_len().into()),
+            Some((opcode.is_push() as u8).into()),
+        ]) {
+            // before inserting, these columns must be none
+            assert!(cell.is_none());
+            *cell = value;
+        }
+       //....
+    }
+```
+
+#### get_lookups
+
+从core row, cnt=1，vers[24]~vers[31]的位置位置获取值，向Bytecode进行lookup, 这里使用的lookUp类型为`BytecodeFull`
+
+```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 = query_expression(meta, |meta| config.get_state_lookup(meta, 0));
+        let bytecode_loopup = query_expression(meta, |meta| config.get_bytecode_full_lookup(meta));
+        vec![
+            ("jump_lookup_stack".into(), stack_lookup),
+            ("jump_lookup_bytecode".into(), bytecode_loopup),
+        ]
+    }
+    pub(crate) fn get_bytecode_full_lookup(&self, meta: &mut VirtualCells<F>) -> LookupEntry<F> {
+        let (addr, pc, opcode, not_code, value_hi, value_lo, cnt, is_push) = (
+            meta.query_advice(self.vers[24], Rotation::prev()),
+            meta.query_advice(self.vers[25], Rotation::prev()),
+            meta.query_advice(self.vers[26], Rotation::prev()),
+            meta.query_advice(self.vers[27], Rotation::prev()),
+            meta.query_advice(self.vers[28], Rotation::prev()),
+            meta.query_advice(self.vers[29], Rotation::prev()),
+            meta.query_advice(self.vers[30], Rotation::prev()),
+            meta.query_advice(self.vers[31], Rotation::prev()),
+        );
+        LookupEntry::BytecodeFull {
+            addr,
+            pc,
+            opcode,
+            not_code,
+            value_hi,
+            value_lo,
+            cnt,
+            is_push,
+        }
+    }
+```
+
+
+
+
+