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

@@ -4,7 +4,7 @@
 
 概述：无条件跳转，跳转到指定PC的位置，JUMP跳转的位置一定是JUMPDEST所在的位置（JUMPDEST：跳转目标标记位，JUMPDEST标记的位置可以使用JUMP进行跳转）
 
-具体操作：从栈顶弹出一个值，作为要跳转的目标PC的值
+具体操作：从栈顶弹出一个值，作为要跳转的目标PC的值。
 
 trace示例：JUMP指令执行时，会从栈中获取一个值，该值即是要跳转的PC，而该PC一定指向的是JUMPDEST的位置
 
@@ -21,6 +21,74 @@ JUMPDEST
 STOP
 ```
 
+在这个例子中，栈的情况和具体的执行流程如下：
+
+```tex
+Initial State:
+PC = 0
+Stack = []
+
+Step 1:
+PC = 0
+Instruction = PUSH1 0xa
+Stack = [0xa]
+Description = 将 0xa 推入栈
+
+Step 2:
+PC = 2
+Instruction = PUSH30 0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f
+Stack = [0xa, 0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f]
+Description = 将 30 字节的值推入栈
+
+Step 3:
+PC = 33
+Instruction = ADD
+Stack = [0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e29]
+Description = 弹出两个值进行加法操作，并将结果推入栈
+
+Step 4:
+PC = 34
+Instruction = PUSH1 0x25
+Stack = [0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e29, 0x25]
+Description = 将 0x25 推入栈
+
+Step 5:
+PC = 36
+Instruction = JUMP
+Stack = [0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e29]
+Description = 跳转到栈顶值 0x25 对应的 PC，0x25对应10进制为37
+
+Step 6:
+PC = 37
+Instruction = JUMPDEST
+Stack = [0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e29]
+Description = 标记一个有效跳转目标
+
+Step 7:
+PC = 38
+Instruction = PUSH1 0x29
+Stack = [0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e29, 0x29]
+Description = 将 0x29 推入栈中
+
+Step 8:
+PC = 40
+Instruction = JUMP
+Stack = [0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e29]
+Description = 跳转到栈顶值 0x29 对应的 PC，0x29对应十进制为41
+
+Step 9:
+PC = 41
+Instruction = JUMPDEST
+Stack = [0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e29]
+Description = 标记另一个有效跳转目标
+
+Step 10:
+PC = 42
+Instruction = STOP
+Stack = [0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e29]
+Description = 停止执行。
+```
+
 ### Witness Core Row
 
 Witness Core Row用于记录每个操作的中间状态，包括操作码（opcode）、程序计数器（PC）、代码地址（code_addr）和栈值（value_lo 和 value_hi）等。其中JUMP的core row中的表格设计如下:
@@ -40,16 +108,57 @@ cnt=1, vers[24]~vers[31]的位置用来存放去向为bytecode的LookUp, 即校
 
 ### 门约束
 
-门约束用于确保每一步操作符合预期，包括栈操作和跳转验证。以下是详细的门约束设计：
+设计 EVM 的 `JUMP` 指令门约束时，主要确保程序的控制流合法且安全。`JUMP` 指令的作用是将程序计数器（PC）跳转到栈顶的某个地址，这个地址必须是一个有效的 `JUMPDEST` 指令。大致的设计流程如下：
+
+1. **操作和要求**
+   - **操作**：从栈顶弹出一个值，作为目标 PC（程序计数器）值。
+   - **要求**：目标 PC 值必须是有效的 `JUMPDEST` 位置。
+2. **定义输入和输出**
+   - **输入**：栈顶的一个值 `next_pc`。
+   - **输出**：程序计数器跳转到 `next_pc`。
+3. **定义门约束**
+   - **合法性约束**：`next_pc` 必须是一个有效的 `JUMPDEST`。
+   - **跳转约束**：程序计数器必须正确地跳转到 `next_pc`。
+
+**详细的门约束设计如下：**
+
+**1. 当前的 OPCODE = JUMP**
+
+确保当前指令是 `JUMP` 操作。
+
+**2. Stack Value 约束**
+
+- **字段**：tag、state_stamp、call_id、stack_pointer、is_write
+- 约束：确保栈中的值符合 `JUMP` 指令的操作要求。
+
+**3. Auxiliary 字段约束**
+
+- **字段**：state_stamp、stack_pointer、log_stamp、read_only
+- 约束：辅助字段需要保持一致性和正确性，以支持 `JUMP` 指令的执行。
+
+**4. next_pc = stack_top_value_lo**
+
+- **描述**：从栈顶获取的值作为要跳转的目标 PC 值。
+- **范围**：`next_pc` 的范围在 `u64` 内，只取 `value_lo` 即可。
+
+**5. stack_top_value_hi = 0**
+
+- **约束**：对 `stack_top_value_hi` 进行约束，确保其为 `0`。
+- **描述**：确保高位部分为 `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**
 
-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，是具体的指令，即是opcode，并不是push的byte)
+- **描述**：`next_pc` 所指向的位置为 `JUMPDEST`，是具体的指令，即为 `opcode`，并不是 `push` 的字节。
 
 可参考下面示例代码：