geruiwangJUMP
概述
概述：无条件跳转，跳转到指定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
STOPWitness Core Row
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 |
/// +---+-------+-------+-------+--------------------------+门约束
- 当前的OPCODE=JUMP
- Stack Value约束（tag、state_stamp、 call_id、stack_pointer、is_write）
- Auxiliary字段约束（state_stamp、stack_pointer、log_stamp、read_only）
- next_pc=stack_top_value_lo (从栈顶获取的值作为要跳转的值，pc范围是在u64内的，只取value_lo即可)
- stack_top_value_hi=0 (要对value_hi进行约束为0)
- lookup_value约束：lookup_pc=stack_top_value_lo (查找表操作，去向为bytecode table， 用来校验next_pc的合法性， lookup_pc一定也是stack_top_value_lo)
- lookup_value约束：lookup_bytecode_addr=
meta.query_advice(config.code_addr, Rotation::cur());(JUMP指令只是用来当前合约内部的PC跳转，next_pc_bytecode_addr有一定和当前的code_addr是一致的) - lookup_value约束：lookup_not_code=0 (next_pc所指向的位置为JUMPDEST，是具体的指令，即是opcode，并不是push的byte)
可参考下面示例代码：
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的合法性，即校验next_pc在bytecode中是否存在)
来源：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,
}
}