Skip to content

GitLab

新注册的用户请输入邮箱并保存，随后登录邮箱激活账号。后续可直接使用邮箱登录！

Last edited by geruiwang
Page history
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 指令。大致的设计流程如下：

  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

  • 描述：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

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

 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,
        }
    }

Copyright © 2024 ChainWeaver Org. All Rights Reserved. 版权所有。

京ICP备2023035722号-3

京公网安备 11010802044225号