This is an old version of this page. You can view the most recent version or browse the history.

core jump

JUMP指令

概述

概述：无条件跳转，跳转到指定PC的位置，JUMP跳转的位置一定是JUMPDEST所在的位置（JUMPDEST：跳转目标标记位，JUMPDEST标记的位置可以使用JUMP进行跳转）

具体操作：从栈顶弹出一个值，作为要跳转的目标PC的值。

trace示例：JUMP指令执行时，会从栈中获取一个值，该值即是要跳转的PC，而该PC一定指向的是JUMPDEST的位置

PUSH1 0xa
PUSH30 0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f
ADD
PUSH1 0x25
JUMP
JUMPDEST
PUSH1 0x29
JUMP
JUMPDEST
STOP

在这个例子中，栈的情况和具体的执行流程如下：

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中的表格设计如下:

cnt=1 vers[0]~vers[7]的位置用来存放栈顶弹出的值，即next_pc

cnt=1, vers[24]~vers[31]的位置用来存放去向为bytecode的LookUp, 即校验next_pc在bytecode中是否存在

/// +---+-------+-------+-------+--------------------------+
/// |cnt| 8 col | 8 col | 8 col |             8col         |
/// +---+-------+-------+-------+--------------------------+
/// | 1 | STATE |       |       |  Bytecode LookUp         |
/// | 0 | DYNA_SELECTOR   | AUX                            |
/// +---+-------+-------+-------+--------------------------+

门约束

设计 EVM 的 JUMP 指令门约束时，主要确保程序的控制流合法且安全。JUMP 指令的作用是将程序计数器（PC）跳转到栈顶的某个地址，这个地址必须是一个有效的 JUMPDEST 指令。大致的设计流程如下：

操作和要求
- 操作：从栈顶弹出一个值，作为目标 PC（程序计数器）值。
- 要求：目标 PC 值必须是有效的 JUMPDEST 位置。
定义输入和输出
- 输入：栈顶的一个值 next_pc。
- 输出：程序计数器跳转到 next_pc。
定义门约束
- 合法性约束：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

描述：next_pc 所指向的位置为 JUMPDEST，是具体的指令，即为 opcode，并不是 push 的字节。

可参考下面示例代码：

 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约束

LookUp约束用于验证跳转目标PC是一个有效的JUMPDEST指令位置。以下是详细的LookUp约束设计：

cnt=1的位置vers[24]~vers[31]的位置用来存放要lookUp的信息(next_pc的合法性，即校验next_pc在bytecode中是否存在)

其中，vers[24]~vers[31]的Witness Core Row 表结构如下：

| cnt | vers[24]  | vers[25] | vers[26] | vers[27] | vers[28] | vers[29] | vers[30] | vers[31] |
| --- | --------- | -------- | -------- | -------- | -------- | -------- | -------- | -------- |
| 1   | code_addr | pc       | opcode   | not_code | value_hi | value_lo | -        | is_push  |

来源：core

去向：bytecode

可参考下面示例代码

insert_bytecode_full_lookup

将要lookup的值放入到core row, cnt=1，vers[24]~vers[31]的位置

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

除了state lookup 外，

5-state.markdown

需要从core row, cnt=1，vers[24]~vers[31]的位置获取值，去向为Bytecode进行lookup, 这里使用的LookUp类型为LookupEntry::BytecodeFull

6-bytecode