|
|
|
## 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
|
|
|
|
```
|
|
|
|
|
|
|
|
### Witness Core Row
|
|
|
|
|
|
|
|
core row中的表格设计如下:
|
|
|
|
|
|
|
|
cnt=1 vers[0]~vers[7]的位置用来存放栈顶弹出的值，即next_pc
|
|
|
|
|
|
|
|
cnt=1, vers[24]~vers[31]的位置用来存放去向为bytecode的LookUp, 即校验next_pc在bytecode中是否存在
|
|
|
|
|
|
|
|
```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，是具体的指令，即是opcode，并不是push的byte)
|
|
|
|
|
|
|
|
可参考下面示例代码：
|
|
|
|
|
|
|
|
```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的合法性，即校验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类型为`LookupEntry::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,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
``` |
|
|
\ No newline at end of file |
