| ... | ... | @@ -670,6 +670,150 @@ fn gen_witness(&self, trace: &GethExecStep, current_state: &mut WitnessExecHelpe |
|
|
|
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约束
|
| ... | ... | |
