... | @@ -130,38 +130,44 @@ pub struct BytecodeCircuitConfig<F> { |
... | @@ -130,38 +130,44 @@ pub struct BytecodeCircuitConfig<F> { |
|
|
|
|
|
## 门约束
|
|
## 门约束
|
|
|
|
|
|
**cnt_prev=0约束**
|
|
addr = 0 ----> Padding row(所有值都为0)
|
|
|
|
|
|
cnt_prev=0的情况有三种:Opcode(非PUSH)、PUSH的最后一个byte、padding的行,
|
|
cnt_prev=0 && cnt_cur !=0 ----> OPCODE(PUSH)
|
|
|
|
|
|
则当前行是新的Opcode或者是padding行
|
|
cnt_prev=0 && cnt_cur =0 && addr != 0 ---> OPCODE(非PUSH)
|
|
|
|
|
|
(padding的行由addr=0来约束,所有值都为0,Opcode的行则需要判断Bytecode不是PUSH的byte)
|
|
cnt_prev != 0 && cnt_cur != 0 ------> PUSH的byte(非push的最后一个字节)
|
|
|
|
|
|
cnt_prev=0 ----> acc_hi_cur=0, acc_lo_cur=0
|
|
cnt_prev != 0 && cnt_cur == 0 -------> PUSH的最后一个字节
|
|
|
|
|
|
|
|
cnt=0的情况有三种:Opcode(非PUSH)、PUSH指令PUSH的最后一个byte、padding的row
|
|
|
|
|
|
|
|
**pc约束**
|
|
|
|
|
|
**cnt=0约束**
|
|
addr change ----> pc=0 (addr发生变化,说明是一个新的合约,pc应该从0开始)
|
|
|
|
|
|
cnt=0的情况有三种:Opcode(非PUSH)、PUSH指令PUSH的最后一个byte、padding的row
|
|
addr unchange && addr != 0 ----> pc_cur - pc_prev = 1 (同一个合约中pc是累加的)
|
|
|
|
|
|
(padding的row由addr=0来约束, Opcode(非PUSH) cnt一定为0, PUSH的最后一个byte的cnt_prev-cnt_cur=1)
|
|
**Padding row**
|
|
|
|
|
|
cnt ==0 ----> value_hi-acc_hi=0, value_lo-acc_lo=0 (统一约束了cnt=0的value_hi和value_lo的值)
|
|
cnt、addr、pc、bytecode、value_hi、value_lo、acc_hi、acc_lo、is_high都为0
|
|
|
|
|
|
|
|
**Opcode(非PUSH)**
|
|
|
|
|
|
|
|
cnt、value_hi、value_lo、acc_hi、acc_lo、is_high都为0
|
|
|
|
|
|
**cnt!=0约束**
|
|
**Opcode(PUSH)**
|
|
|
|
|
|
cnt !=0 的情况只有一种,PUSH指令所PUSH的byte(非最后一个byte),cnt是逐行减1的
|
|
cnt !=0, acc_hi=0,acc_lo=0
|
|
|
|
|
|
cnt !=0 ----> `cnt_prev - cnt_cur = 1 `(约束cnt)
|
|
当前的value_lo等于Rotation(cur_cnt)的value_lo,value_hi同理,即value_lo和value_hi应等于最终计算出的value_lo、value_hi(PUSH的最后一个byte)
|
|
|
|
|
|
**cnt_prev != 0**
|
|
**cnt_prev != 0**
|
|
|
|
|
|
cnt_prev != 0说明当前行为PUSH指令PUSH的byte
|
|
cnt_prev != 0说明当前行为PUSH指令PUSH的byte
|
|
|
|
|
|
|
|
cnt_prev !=0 ----> `cnt_prev - cnt_cur = 1 `(PUSH指令的cnt是递减的)
|
|
|
|
|
|
cnt_prev !=0 -----> `is_high_prev - is_heigh_cur - cnt_is_15 = 0` (用于约束cnt=15和cat=16的分界线的cnt, 当cnt=15时, cnt_is_15=1,因为cnt>=16时is_high=1, cnt<16时is_high=0, 所以cnt_is_16_is_high - cnt_is_15_is_high =1)
|
|
cnt_prev !=0 -----> `is_high_prev - is_heigh_cur - cnt_is_15 = 0` (用于约束cnt=15和cat=16的分界线的cnt, 当cnt=15时, cnt_is_15=1,因为cnt>=16时is_high=1, cnt<16时is_high=0, 所以cnt_is_16_is_high - cnt_is_15_is_high =1)
|
|
|
|
|
|
cnt_prev !=0 ----> `acc_hi_prev + is_high*(acc_hi_prev*255 + bytecode) - acc_hi_cur =0`(约束acc_hi)
|
|
cnt_prev !=0 ----> `acc_hi_prev + is_high*(acc_hi_prev*255 + bytecode) - acc_hi_cur =0`(约束acc_hi)
|
... | @@ -172,32 +178,11 @@ cnt_prev !=0 ----> `acc_hi_prev + is_high*(acc_hi_prev*255 + bytecode) - acc_hi_ |
... | @@ -172,32 +178,11 @@ cnt_prev !=0 ----> `acc_hi_prev + is_high*(acc_hi_prev*255 + bytecode) - acc_hi_ |
|
|
|
|
|
cnt_prev !=0 ----> `acc_lo_cur - acc_lo_prev - (1-is_high) *(acc_lo_prev*255 + bytecode)=0` (约束acc_lo,当cnt < 16, 即high=0时,acc_lo_cur=acc_lo_prev*256 + bytecode)
|
|
cnt_prev !=0 ----> `acc_lo_cur - acc_lo_prev - (1-is_high) *(acc_lo_prev*255 + bytecode)=0` (约束acc_lo,当cnt < 16, 即high=0时,acc_lo_cur=acc_lo_prev*256 + bytecode)
|
|
|
|
|
|
|
|
当前的value_lo等于Rotation(cur_cnt)的value_lo,value_hi同理,即value_lo和value_hi应等于最终计算出的value_lo、value_hi(PUSH的最后一个byte)
|
|
|
|
|
|
|
|
**PUSH的最后一个byte:**
|
|
|
|
|
|
**addr约束**
|
|
cnt_prev!=0, cnt=0,value_hi=acc_hi, value_lo=acc_lo
|
|
|
|
|
|
addr = 0 ---> addr=0, pc=0, bytecode=0, value_hi=0, value_lo=0, acc=hi=0, acc_lo=0, cnt=0, is_high=0 (padding的行所有的值都是0)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
**pc约束**
|
|
|
|
|
|
|
|
addr change ----> pc=0 (addr发生变化,说明是一个新的合约,pc应该从0开始)
|
|
|
|
|
|
|
|
addr unchange && addr != 0 ----> pc_cur - pc_prev = 1 (同一个合约中pc是累加的)
|
|
|
|
|
|
|
|
|
|
|
|
**区分Opcode(非PUSH)、Opcode(PUSH)、Push的Byte**:
|
|
|
|
|
|
|
|
cnt_prev=0 && cnt_cur !=0 ----> OPCODE(PUSH)
|
|
|
|
|
|
|
|
cnt_prev=0 && cnt_cur =0 && addr != 0 ---> OPCODE(非PUSH)
|
|
|
|
|
|
|
|
addr = 0 ----> Padding row
|
|
|
|
|
|
|
|
cnt_prev != 0 && cnt_cur != 0 ------> PUSH的byte(非push的最后一个字节)
|
|
|
|
|
|
|
|
cnt_prev != 0 && cnt_cur == 0 -------> PUSH的最后一个字节
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
... | | ... | |