... | @@ -241,7 +241,7 @@ pub(crate) trait ExecutionGadget< |
... | @@ -241,7 +241,7 @@ pub(crate) trait ExecutionGadget< |
|
## 分配数值
|
|
## 分配数值
|
|
因为证据Witness的表格设计和子电路的列的设计基本呈对应关系,分配数值的代码被大大简化。我们只需将表格每一行的数值分配给子电路的相应列的相应行(offset)即可。Witness生成则由每个执行工具的gen_witness方法负责,详见其代码。
|
|
因为证据Witness的表格设计和子电路的列的设计基本呈对应关系,分配数值的代码被大大简化。我们只需将表格每一行的数值分配给子电路的相应列的相应行(offset)即可。Witness生成则由每个执行工具的gen_witness方法负责,详见其代码。
|
|
|
|
|
|
# 例子
|
|
## 例子
|
|
形象展示:
|
|
形象展示:
|
|
```rust
|
|
```rust
|
|
/// Add Execution State layout is as follows
|
|
/// Add Execution State layout is as follows
|
... | @@ -260,680 +260,4 @@ pub(crate) trait ExecutionGadget< |
... | @@ -260,680 +260,4 @@ pub(crate) trait ExecutionGadget< |
|
```
|
|
```
|
|
代码:https://git.code.tencent.com/chainmaker-zk/zkevm/blob/develop/zkevm-circuits/src/execution/add.rs
|
|
代码:https://git.code.tencent.com/chainmaker-zk/zkevm/blob/develop/zkevm-circuits/src/execution/add.rs
|
|
|
|
|
|
|
|
# 执行状态的转换流程 |
|
|
|
\ No newline at end of file |
|
# Core Execution
|
|
|
|
|
|
|
|
## 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,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
## EXTCODECOPY
|
|
|
|
|
|
|
|
### 概述
|
|
|
|
|
|
|
|
#### CODECOPY
|
|
|
|
|
|
|
|
概述:该操作通常用于在智能合约中实现一些动态代码加载或代码复制的逻辑,将合约中字节码复制到Memory中,即将合约代码复制到内存的操作。
|
|
|
|
|
|
|
|
具体操作:从栈顶弹出三个值,分别为:destOffset、offset、length,根据当前三个值进行操作:`memory[destOffset:destOffset+length] = address(this).code[offset:offset+length]`,即从code中以offset的位置开始,复制长度为length的字节码到Memory以destOffset为起始的位置(都是以字节为单位进行操作)
|
|
|
|
|
|
|
|
trace示例:CODECOPY指令执行时,会从栈顶弹出三个值:destOffset、offset、length,然后根据这三个值进行合约代码的复制
|
|
|
|
|
|
|
|
```shell
|
|
|
|
PUSH1 0xa
|
|
|
|
PUSH30 0x02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f
|
|
|
|
ADD
|
|
|
|
PUSH1 0x1E
|
|
|
|
PUSH1 0x03
|
|
|
|
PUSH1 0x00
|
|
|
|
CODECOPY
|
|
|
|
STOP
|
|
|
|
```
|
|
|
|
|
|
|
|
此操作会从合约代码第3个字节开始复制,长度为30,复制到Memory以00起始的位置,即将`02030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f` 复制到Memory中
|
|
|
|
|
|
|
|
#### EXTCODECOPY
|
|
|
|
|
|
|
|
概述: 该操作类似CODECOPY,区别之处在于,可以通过参数指定合约源码地址栈顶。从栈顶第一个弹出的address来指定合约的源码地址,首先找到code=find_code_by(address),余下操作同CODECOPY
|
|
|
|
|
|
|
|
### Witness Core Row
|
|
|
|
|
|
|
|
core row的表格设计如下:
|
|
|
|
|
|
|
|
cnt=2, vers[0]~vers[8] 为正常copy row进行LookUp的值
|
|
|
|
|
|
|
|
cnt=2, vers[8]~vers[17] 为padding copy row进行LookUp的值
|
|
|
|
|
|
|
|
```shell
|
|
|
|
/// +---+-------+-------+-------+----------+
|
|
|
|
/// |cnt| 8 col | 8 col | 8 col | 8 col |
|
|
|
|
/// +---+-------+-------+-------+----------+
|
|
|
|
/// | 2 | COPY(9) | ZEROCOPY(9)|
|
|
|
|
/// | 1 | STATE | STATE | STATE | STATE |
|
|
|
|
/// | 0 | DYNA_SELECTOR | AUX |
|
|
|
|
/// +---+-------+-------+-------+----------+
|
|
|
|
```
|
|
|
|
|
|
|
|
#### 解释
|
|
|
|
|
|
|
|
在进行copy时,offset即是要复制的合约的代码的起始位置start,复制长度为length,复制的结束位置end: start+length,但是在进行copy的时候可能存在边界问题,如下:
|
|
|
|
|
|
|
|
1)offset<=len(code), copy_len > 0, offset+copy_len <= len(code), 无需进行0填充
|
|
|
|
|
|
|
|
2)offset<=len(code), copy_len == 0, offset+copy_len <= len(code), 无需0填充, 也无需拷贝,即code[start:start],为空
|
|
|
|
|
|
|
|
3)offset<=len(code), copy_len>0, offset_copy_len > len(code),需要进行0填充,填充长度为 copy_len - (len(code)-offset) --> offset+copy_len - len(code)
|
|
|
|
|
|
|
|
4)offset>len(code), copy_len>=0, offset+copy_len > len(code), 需要进行0填充,填充长度为offset+copy_len-len(code)
|
|
|
|
|
|
|
|
此外当 offset > u64时,会对offset进行特殊处理为u64的最大值
|
|
|
|
|
|
|
|
对于Padding的值也会被放到Memory中,Padding的值,Src部分都是默认值,dst部分正常填充(对Copy子电路来说,Padding部分,因为ByteCode中并不存在Padding的值,所以不存在来源,但是Padding的值也会被放入到Memory中,所以存在去向,所以Padding部分的LookUp无来源,但是有去向为State)。
|
|
|
|
|
|
|
|
不过padding中的dst部分在进行赋值时需要注意:dst_pointer和dst_stamp,因为在Copy子电路中,memory_addr=dst_pointer+cnt,memory_stamp=dst_stamp+cnt,而Padding和正常的Copy是分成两部分的(Padding在Copy子电路中的Type为Zero),即Padding在Copy子电路中的cnt也是从0开始计数的。
|
|
|
|
|
|
|
|
举例如下:
|
|
|
|
|
|
|
|
> 合约代码长度:len(code)=5
|
|
|
|
> 进行CodeCopy操作:
|
|
|
|
> offset: 0
|
|
|
|
> copy_len: 8
|
|
|
|
> destOffset: 0
|
|
|
|
> 进行CodeCopy, 因为offset+copy_len > len(code) 所以需要填充0,填充长度为offset+copy_len - len(code) = 3, 所以整体CopyRow的生成就分成了两部分:正常的CopyRow5行,PaddingCopyRow3行。
|
|
|
|
> 加入在生成Copy时的stamp为1记为OriginalStamp
|
|
|
|
> 则NoPaddingCopyRow的Stamp都为1(OriginalStamp),dest_pointer为destOffset+{0..4}, cnt为0~4
|
|
|
|
> 则PaddingCopyRow的Stamp为6(OriginalStamp+len(code)), dest_pointer为destOffset+len(code)+{0..2}, cnt为0~2
|
|
|
|
> 因为是分为两部分的,所以stamp、dest_pointer不是相同的
|
|
|
|
|
|
|
|
代码如下:
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub fn get_code_copy_rows_new(
|
|
|
|
&mut self,
|
|
|
|
address: U256,
|
|
|
|
dst: U256,
|
|
|
|
src: U256,
|
|
|
|
len: U256,
|
|
|
|
) -> (Vec<copy::Row>, Vec<state::Row>, u64, u64, u64) {
|
|
|
|
//...
|
|
|
|
|
|
|
|
// NoPaddingCopyRow赋值
|
|
|
|
let codecopy_stamp = self.state_stamp;
|
|
|
|
if code_copy_length > 0 {
|
|
|
|
for i in 0..code_copy_length {
|
|
|
|
let code = self.bytecode.get(&address).unwrap();
|
|
|
|
let byte = code.get((src_offset + i) as usize).unwrap().value;
|
|
|
|
copy_rows.push(copy::Row {
|
|
|
|
byte: byte.into(),
|
|
|
|
src_type: copy::Type::Bytecode,
|
|
|
|
src_id: address,
|
|
|
|
src_pointer: src_offset.into(),
|
|
|
|
src_stamp: None,
|
|
|
|
dst_type: copy::Type::Memory,
|
|
|
|
dst_id: self.call_id.into(),
|
|
|
|
dst_pointer: dst_offset.into(),
|
|
|
|
dst_stamp: codecopy_stamp.into(),
|
|
|
|
cnt: i.into(),
|
|
|
|
len: code_copy_length.into(),
|
|
|
|
});
|
|
|
|
state_rows.push(self.get_memory_write_row((dst_offset + i) as usize, byte));
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
// PaddingCopyRow赋值
|
|
|
|
let codecopy_padding_stamp = self.state_stamp;
|
|
|
|
if padding_length > 0 {
|
|
|
|
for i in 0..padding_length {
|
|
|
|
state_rows.push(
|
|
|
|
self.get_memory_write_row(
|
|
|
|
(dst_offset + code_copy_length + i) as usize,
|
|
|
|
0 as u8,
|
|
|
|
),
|
|
|
|
);
|
|
|
|
copy_rows.push(copy::Row {
|
|
|
|
byte: 0.into(),
|
|
|
|
src_type: copy::Type::default(),
|
|
|
|
src_id: 0.into(),
|
|
|
|
src_pointer: 0.into(),
|
|
|
|
src_stamp: None,
|
|
|
|
dst_type: copy::Type::Memory,
|
|
|
|
dst_id: self.call_id.into(),
|
|
|
|
dst_pointer: (dst_offset + code_copy_length).into(),
|
|
|
|
dst_stamp: codecopy_padding_stamp.into(),
|
|
|
|
cnt: i.into(),
|
|
|
|
len: U256::from(padding_length),
|
|
|
|
})
|
|
|
|
}
|
|
|
|
}
|
|
|
|
// ...
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
此外还需要注意**copy_len为0**的特殊值,当copy_len为0时,NoPaddingCopyRow行数等于0, PaddingCopyRow行数等于0,则CoreRow cnt=2的值会存放两个全是默认值的CopyRow(即全为0的值)放在vers[0]~vers[17],当NoPaddingCopyRow行数大于0,PaddingCopyRow行数等于0时,vers[8]~vers[17]会存放全是默认值当CopyRow(即全为0的值)
|
|
|
|
|
|
|
|
并且行数为0的情况并不会放到State和Copy子电路的表中,因为copy_len为0,理应该不做任何操作,代码示例如下:
|
|
|
|
|
|
|
|
```rust
|
|
|
|
fn gen_witness(&self, trace: &GethExecStep, current_state: &mut WitnessExecHelper) -> Witness {
|
|
|
|
let (stack_pop_0, address) = current_state.get_pop_stack_row_value(&trace);
|
|
|
|
assert!(address.leading_zeros() >= ADDRESS_ZERO_COUNT);
|
|
|
|
//let address_code = current_state.bytecode.get(&address).unwrap();
|
|
|
|
// ...
|
|
|
|
let (copy_rows, mem_rows, input_length, padding_length, code_copy_length) =
|
|
|
|
current_state.get_code_copy_rows_new(address, mem_offset, code_offset, size);
|
|
|
|
|
|
|
|
let mut default_copy_row = ¤t_state.get_none_copy_row();
|
|
|
|
if input_length > 0 && code_copy_length > 0 {
|
|
|
|
default_copy_row = ©_rows[0];
|
|
|
|
}
|
|
|
|
let mut default_padding_row = ¤t_state.get_none_padding_copy_row();
|
|
|
|
if input_length > 0 && padding_length > 0 {
|
|
|
|
default_padding_row = ©_rows[code_copy_length as usize]
|
|
|
|
}
|
|
|
|
|
|
|
|
// ...
|
|
|
|
if input_length > 0 {
|
|
|
|
Witness {
|
|
|
|
copy: copy_rows,
|
|
|
|
core: vec![core_row_2, core_row_1, core_row_0],
|
|
|
|
state: state_vec,
|
|
|
|
..Default::default()
|
|
|
|
}
|
|
|
|
} else {
|
|
|
|
Witness {
|
|
|
|
core: vec![core_row_2, core_row_1, core_row_0],
|
|
|
|
state: state_vec,
|
|
|
|
..Default::default()
|
|
|
|
}
|
|
|
|
}
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
### 门约束
|
|
|
|
|
|
|
|
1. 当前的OPCODE一致
|
|
|
|
1. Stack Value约束(tag,state_stamp,call_id,stack_pointer,is_write)
|
|
|
|
1. Auxiliary字段约束(state_stamp,stack_pointer,log_stamp,read_only),值得注意的是state_stamp的约束需要考虑copy的长度为0的情况
|
|
|
|
1. next_pc=stack_top_value_lo (从栈顶获取的值作为要跳转的值,pc范围是在u64内的,只取value_lo即可)
|
|
|
|
1. lookup_value约束: copy_lookup_len *(copy_lookup_src_type - Bytecode) ,当代码拷贝真实发生时候,src_type必然为Bytecode
|
|
|
|
1. lookup_value约束: copy_lookup_len *(copy_lookup_dst_type - Memory), 当代码拷贝真实发生时候,dst_type必然为Memory
|
|
|
|
1. lookup_value约束: copy_lookup_len *(copy_lookup_dst_id - call_id) ,当代码拷贝真实发生时候,dst_id必然为call_id
|
|
|
|
1. lookup_value约束: copy_lookup_len *(copy_lookup_dst_stamp - copy_code_stamp_start -1) ,当代码拷贝真实发生时候,拷贝代码行开始处必然在最后一个出栈元素的下一行
|
|
|
|
1. lookup_value约束: copy_lookup_len *(copy_lookup_src_id - address ),当代码拷贝真实发生时候,src_id必然为代码块的代码address
|
|
|
|
1. lookup_value约束: copy_lookup_len *(copy_lookup_dst_pointer - mem_offset ), 当代码拷贝真实发生的时候,dst_pointer必然为内存偏移量
|
|
|
|
1. lookup_value约束: copy_lookup_len *(copy_lookup_src_pointer - code_offset), 当代码拷贝真实发生的时候,src_pointer必然为代码偏移量
|
|
|
|
1. lookup_value约束: copy_lookup_len + copy_padding_lookup_len - length, 代码拷贝长度 + padding的长度必然等于参数指定的拷贝长度
|
|
|
|
1. lookup_value约束: copy_padding_lookup_src_type - Zero ,padding的src_type 为 Zero类型(也即default()类型)
|
|
|
|
1. lookup_value约束: copy_padding_lookup_len* (copy_padding_lookup_dst_type - Memory) ,当真实有padding数据时候,dst_type应该为Memory
|
|
|
|
1. lookup_value约束: copy_padding_lookup_src_id - 0 , padding的src_id为默认值0
|
|
|
|
1. lookup_value约束: copy_padding_lookup_src_pointer - 0 , padding的src_pointer为默认值0
|
|
|
|
1. lookup_value约束: copy_padding_lookup_len* (copy_padding_lookup_dst_pointer - copy_lookup_dst_pointer - copy_lookup_len ), 当真实有padding数据的时候, padding的dst_pointer 与 copy的dst_pointer相差拷贝的代码长度(copy_lookup_len)
|
|
|
|
1. lookup_value约束: copy_padding_lookup_len* (copy_padding_lookup_dst_stamp - copy_code_stamp_start - copy_lookup_len - 1), 当真实有padding数据的时候,padding的dst_stamp与栈中最后一个元素所处的stamp相差真实拷贝的代码长度+1
|
|
|
|
可参考如下示例代码:
|
|
|
|
```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_cur = meta.query_advice(config.pc, Rotation::cur());
|
|
|
|
let call_id = meta.query_advice(config.call_id, Rotation::cur());
|
|
|
|
let pc_next = meta.query_advice(config.pc, Rotation::next());
|
|
|
|
let (
|
|
|
|
copy_lookup_src_type,
|
|
|
|
copy_lookup_src_id,
|
|
|
|
copy_lookup_src_pointer,
|
|
|
|
_,
|
|
|
|
copy_lookup_dst_type,
|
|
|
|
copy_lookup_dst_id,
|
|
|
|
copy_lookup_dst_pointer,
|
|
|
|
copy_lookup_dst_stamp,
|
|
|
|
copy_lookup_len,
|
|
|
|
) = extract_lookup_expression!(copy, config.get_copy_lookup(meta));
|
|
|
|
|
|
|
|
let (
|
|
|
|
copy_padding_lookup_src_type,
|
|
|
|
copy_padding_lookup_src_id,
|
|
|
|
copy_padding_lookup_src_pointer,
|
|
|
|
_,
|
|
|
|
copy_padding_lookup_dst_type,
|
|
|
|
copy_padding_lookup_dst_id,
|
|
|
|
copy_padding_lookup_dst_pointer,
|
|
|
|
copy_padding_lookup_dst_stamp,
|
|
|
|
copy_padding_lookup_len,
|
|
|
|
) = extract_lookup_expression!(copy, config.get_copy_padding_lookup(meta));
|
|
|
|
|
|
|
|
let delta = AuxiliaryDelta {
|
|
|
|
state_stamp: STATE_STAMP_DELTA.expr()
|
|
|
|
+ copy_lookup_len.clone()
|
|
|
|
+ copy_padding_lookup_len.clone(),
|
|
|
|
stack_pointer: STACK_POINTER_DELTA.expr(),
|
|
|
|
..Default::default()
|
|
|
|
};
|
|
|
|
// auxiliary constraints ...
|
|
|
|
|
|
|
|
// stack constraints ...
|
|
|
|
|
|
|
|
|
|
|
|
// copy lookup constraints
|
|
|
|
constraints.extend([
|
|
|
|
(
|
|
|
|
"etxcodecopy src_type".into(),
|
|
|
|
copy_lookup_len.clone()
|
|
|
|
* (copy_lookup_src_type.clone() - (copy::Type::Bytecode as u8).expr()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy dst_type".into(),
|
|
|
|
copy_lookup_len.clone()
|
|
|
|
* (copy_lookup_dst_type.clone() - (copy::Type::Memory as u8).expr()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy dst_id".into(),
|
|
|
|
copy_lookup_len.clone() * (copy_lookup_dst_id.clone() - call_id.clone()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy dst_stamp".into(),
|
|
|
|
copy_lookup_len.clone()
|
|
|
|
* (copy_lookup_dst_stamp.clone() - copy_code_stamp_start.clone() - 1.expr()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy src_id".into(),
|
|
|
|
copy_lookup_len.clone()
|
|
|
|
* (copy_lookup_src_id
|
|
|
|
- copy_operands[0][0].clone() * pow_of_two::<F>(128)
|
|
|
|
- copy_operands[0][1].clone()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy dst_pointer value_hi = 0".into(),
|
|
|
|
copy_operands[1][0].clone() - 0.expr(),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy dst_pointer".into(),
|
|
|
|
copy_lookup_len.clone()
|
|
|
|
* (copy_lookup_dst_pointer.clone() - copy_operands[1][1].clone()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy src_pointer value_hi = 0".into(),
|
|
|
|
copy_operands[2][0].clone() - 0.expr(),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy src_pointer".into(),
|
|
|
|
copy_lookup_len.clone()
|
|
|
|
* (copy_lookup_src_pointer.clone() - copy_operands[2][1].clone()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy len value_hi = 0".into(),
|
|
|
|
copy_operands[3][0].clone() - 0.expr(),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy len".into(),
|
|
|
|
copy_lookup_len.clone() + copy_padding_lookup_len.clone()
|
|
|
|
- copy_operands[3][1].clone(),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy padding src_type".into(),
|
|
|
|
copy_padding_lookup_src_type.clone() - (copy::Type::default() as u8).expr(),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy padding dst_type".into(),
|
|
|
|
copy_padding_lookup_len.clone()
|
|
|
|
* (copy_padding_lookup_dst_type.clone() - (copy::Type::Memory as u8).expr()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy padding src_id".into(),
|
|
|
|
copy_padding_lookup_src_id.clone() - 0.expr(),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy padding src_pointer".into(),
|
|
|
|
copy_padding_lookup_src_pointer.clone() - 0.expr(),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy padding dst_id".into(),
|
|
|
|
copy_padding_lookup_len.clone()
|
|
|
|
* (copy_padding_lookup_dst_id.clone() - call_id.clone()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy padding dst_pointer".into(),
|
|
|
|
copy_padding_lookup_len.clone()
|
|
|
|
* (copy_padding_lookup_dst_pointer.clone()
|
|
|
|
- copy_lookup_dst_pointer.clone()
|
|
|
|
- copy_lookup_len.clone()),
|
|
|
|
),
|
|
|
|
(
|
|
|
|
"extcodecopy padding copy_padding_lookup_dst_stamp".into(),
|
|
|
|
copy_padding_lookup_len.clone()
|
|
|
|
* (copy_padding_lookup_dst_stamp.clone()
|
|
|
|
- copy_code_stamp_start.clone()
|
|
|
|
- copy_lookup_len.clone()
|
|
|
|
- 1.expr()),
|
|
|
|
),
|
|
|
|
]);
|
|
|
|
// pc & opcode constrains ...
|
|
|
|
constraints
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
### LookUp约束
|
|
|
|
|
|
|
|
LookUp约束被放在cnt=2的CopyRow,被分为两个种约束:NoPaddingCopy的约束和PaddingCopy约束,各占9列: vers[0]~vers[8], vers[9]~vers[17]
|
|
|
|
|
|
|
|
参考Witness Code Row中的解释部分,当offset+copy_len > len(code)时,需要填充0,填充长度为offset+copy_len-len(code)。
|
|
|
|
|
|
|
|
来源:Core
|
|
|
|
|
|
|
|
去向:Copy
|
|
|
|
|
|
|
|
特别注意:当copy_len为0或者padding_len为0时,为0的CopyRow(都是默认值,全为零值)也是需要进行LookUp的(LookUp Copy中全为默认值行)
|
|
|
|
|
|
|
|
可参考代码如下:
|
|
|
|
|
|
|
|
#### insert_copy_lookup
|
|
|
|
|
|
|
|
在copy row cnt=2的位置分别NoPaddingCopyRow(vers[0]~vers[8])和PaddingCopyRow(vers[9]~vers[17])要lookUp的值
|
|
|
|
|
|
|
|
```rust
|
|
|
|
fn gen_witness(&self, trace: &GethExecStep, current_state: &mut WitnessExecHelper) -> Witness {
|
|
|
|
// ...
|
|
|
|
|
|
|
|
// 生成copy_rows
|
|
|
|
let (copy_rows, mem_rows, input_length, padding_length, code_copy_length) =
|
|
|
|
current_state.get_code_copy_rows_new(address, mem_offset, code_offset, size);
|
|
|
|
|
|
|
|
// default_copy_row:全为默认值的CopyRow
|
|
|
|
let mut default_copy_row = ¤t_state.get_none_copy_row();
|
|
|
|
if input_length > 0 && code_copy_length > 0 {
|
|
|
|
default_copy_row = ©_rows[0];
|
|
|
|
}
|
|
|
|
// default_padding_row:全为默认值的CopyRow
|
|
|
|
let mut default_padding_row = ¤t_state.get_none_copy_row();
|
|
|
|
if input_length > 0 && padding_length > 0 {
|
|
|
|
default_padding_row = ©_rows[code_copy_length as usize]
|
|
|
|
}
|
|
|
|
|
|
|
|
core_row_2.insert_copy_lookup_new(
|
|
|
|
default_copy_row,
|
|
|
|
default_padding_row,
|
|
|
|
code_copy_length,
|
|
|
|
padding_length,
|
|
|
|
);
|
|
|
|
// ...
|
|
|
|
}
|
|
|
|
|
|
|
|
pub fn insert_copy_lookup_new(
|
|
|
|
&mut self,
|
|
|
|
copy: ©::Row,
|
|
|
|
padding_copy: ©::Row,
|
|
|
|
copy_length: u64,
|
|
|
|
padding_length: u64,
|
|
|
|
) {
|
|
|
|
//
|
|
|
|
assert_eq!(self.cnt, 2.into());
|
|
|
|
for (cell, value) in [
|
|
|
|
// code copy
|
|
|
|
(&mut self.vers_0, Some((copy.src_type as u8).into())),
|
|
|
|
(&mut self.vers_1, Some(copy.src_id)),
|
|
|
|
(&mut self.vers_2, Some(copy.src_pointer)),
|
|
|
|
(&mut self.vers_3, copy.src_stamp),
|
|
|
|
(&mut self.vers_4, Some((copy.dst_type as u8).into())),
|
|
|
|
(&mut self.vers_5, Some(copy.dst_id)),
|
|
|
|
(&mut self.vers_6, Some(copy.dst_pointer)),
|
|
|
|
(&mut self.vers_7, Some(copy.dst_stamp)),
|
|
|
|
(&mut self.vers_8, Some(copy.len)),
|
|
|
|
// padding copy
|
|
|
|
(&mut self.vers_9, Some((padding_copy.src_type as u8).into())),
|
|
|
|
(&mut self.vers_10, Some(padding_copy.src_id)),
|
|
|
|
(&mut self.vers_11, Some(padding_copy.src_pointer)),
|
|
|
|
(&mut self.vers_12, padding_copy.src_stamp),
|
|
|
|
(
|
|
|
|
&mut self.vers_13,
|
|
|
|
Some((padding_copy.dst_type as u8).into()),
|
|
|
|
),
|
|
|
|
(&mut self.vers_14, Some(padding_copy.dst_id)),
|
|
|
|
(&mut self.vers_15, Some(padding_copy.dst_pointer)),
|
|
|
|
(&mut self.vers_16, Some(padding_copy.dst_stamp)),
|
|
|
|
(&mut self.vers_17, Some(padding_copy.len)),
|
|
|
|
// (&mut self.vers_18, Some(U256::from(copy_length))),
|
|
|
|
// (&mut self.vers_19, Some(U256::from(padding_length))),
|
|
|
|
//
|
|
|
|
] {
|
|
|
|
// before inserting, these columns must be none
|
|
|
|
assert!(cell.is_none());
|
|
|
|
*cell = value;
|
|
|
|
}
|
|
|
|
// ....
|
|
|
|
}
|
|
|
|
|
|
|
|
```
|
|
|
|
|
|
|
|
#### get_lookups
|
|
|
|
|
|
|
|
从copy row cnt=2的位置分别去NoPaddingCopyRow: vers[0]~vers[8],PaddingCopyRow: vers[9]~vers[17]
|
|
|
|
|
|
|
|
```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_0 = query_expression(meta, |meta| config.get_state_lookup(meta, 0));
|
|
|
|
let stack_lookup_1 = query_expression(meta, |meta| config.get_state_lookup(meta, 1));
|
|
|
|
let stack_lookup_2 = query_expression(meta, |meta| config.get_state_lookup(meta, 2));
|
|
|
|
let stack_lookup_3 = query_expression(meta, |meta| config.get_state_lookup(meta, 3));
|
|
|
|
let copy_lookup = query_expression(meta, |meta| config.get_copy_lookup(meta));
|
|
|
|
let padding_copy_lookup =
|
|
|
|
query_expression(meta, |meta| config.get_copy_padding_lookup(meta));
|
|
|
|
|
|
|
|
vec![
|
|
|
|
("stack pop account address".into(), stack_lookup_0),
|
|
|
|
("stack pop mem offset".into(), stack_lookup_1),
|
|
|
|
("stack pop code offset".into(), stack_lookup_2),
|
|
|
|
("stack pop length".into(), stack_lookup_3),
|
|
|
|
("copy look up".into(), copy_lookup),
|
|
|
|
("padding look up".into(), padding_copy_lookup),
|
|
|
|
]
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|