| ... | ... | @@ -313,7 +313,7 @@ cnt=1, vers[24]~vers[31]的位置用来存放去向为bytecode的LookUp, 即校 |
|
|
|
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，并不是bytecode,)
|
|
|
|
8. lookup_value约束：lookup_not_code=0 (next_pc所指向的位置为JUMPDEST，是具体的指令，即是opcode，并不是push的byte)
|
|
|
|
|
|
|
|
可参考下面示例代码：
|
|
|
|
|
| ... | ... | |
