Skip to content

GitLab

新注册的用户请输入邮箱并保存，随后登录邮箱激活账号。后续可直接使用邮箱登录！

6 bytecode · Changes

Page history
chore: modify bytecode doc authored by maqingyuan's avatar maqingyuan
Hide whitespace changes
Inline Side-by-side
Showing with 229 additions and 234 deletions
zkevm-docs/6-bytecode.markdown
View page @ 03b2bbc6
Bytecode circuit用于约束合约的Bytecode，为其他电路提供bytecode的来源依据，其他子电路可通过Lookup约束来验证所操作bytecode码是否是合法的。
Bytecode table中存放的可能并不只是一个合约的Bytecode，不同的合约的Bytecode以`address`进行标识，Bytecode与address是唯一一一对应。
对于一个合约的Bytecode而言，`pc`是opcode或者no_code(push的byte)唯一的标识
在对Bytecode进行处理时，将Bytecode分为两类：
1. Opcode(非PUSH)：操作指令，如ADD、SUB、CODECOPY
2. Opcode(PUSH)：PUSH1~PUSH2
## Witness、Column设计
### Witness
```rust
#[derive(Clone, Debug, Default, Serialize)]
pub struct Row {
/// the contract address of the bytecodes
pub addr: Option<U256>,
/// the index that program counter points to
pub pc: Option<U256>,
/// bytecode, operation code or pushed value
pub bytecode: Option<U256>,
/// pushed value, high 128 bits (0 or non-push opcodes)
pub value_hi: Option<U256>,
/// pushed value, low 128 bits (0 or non-push opcodes)
pub value_lo: Option<U256>,
/// accumulated value, high 128 bits. accumulation will go X times for PUSHX
pub acc_hi: Option<U256>,
/// accumulated value, low 128 bits. accumulation will go X times for PUSHX
pub acc_lo: Option<U256>,
/// count for accumulation, accumulation will go X times for PUSHX
pub cnt: Option<U256>,
/// whether count is equal or larger than 16
pub is_high: Option<U256>,
}
```
- cnt:如果是非PUSH的Opcode则cnt=0， 对于PUSH指令，cnt为PUSH的byte的数量，如PUSH1 --> cnt=1, PUSH2 --> cnt=2, PUSH31 --> cnt=31, PUSH32 --> cnt=32，对于no_code则cnt的值为(0~cnt-1)
- is_high：cnt >=16 ---> 1，cnt < 16 ---> 0，主要是用于辅助计算acc的值(规定acc的值最多为16个字节)
- acc_hi：cnt >=16的Bytecode执行此计算，`acc_hi_pre * 256 + bytecode`，即计算byte的累加值
- acc_lo：cnt < 16的Bytecode执行此计算，`acc_lo_pre * 256 + bytecode`，即计算byte的累加值
- value_hi：cnt >= 16的Bytecode的最终累加值，即最终的acc_hi
- value_lo：cnt < 15的Bytecode的最终累加值，即最终的acc_lo
注：Opcode的 cnt、is_high、acc_hi、acc_lo、value_hi、value_lo值都为0
假如有如下指令：
```shell
PUSH1 0xa
PUSH18 0x02030405060708090a0b0c0d0e0f10111213
ADD
```
假如addr为0xaa，则表格如下（这里的Opcode以字符串的形式表现比较形象）：
| addr | pc | bytecode | acc_hi | acc_lo | value_hi | value_lo | cnt | is_high |
| ---- | ---- | -------- | ------ | --------------------------------- | -------- | --------------------------------- | ---- | ------- |
| 0xaa | 0 | PUSH1 | 0x0 | 0x0 | 0x0 | 0x0 | 1 | 0 |
| 0xaa | 1 | 0xa | 0x0 | 0xa | 0x0 | 0xa | 0 | 0 |
| 0xaa | 2 | PUSH17 | 0x0 | 0x0 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 18 | 1 |
| 0xaa | 3 | 0x2 | 0x2 | 0x0 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 17 | 1 |
| 0xaa | 4 | 0x3 | 0x203 | 0x0 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 16 | 1 |
| 0xaa | 5 | 0x4 | 0x203 | 0x4 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 15 | 0 |
| 0xaa | 6 | 0x5 | 0x203 | 0x405 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 14 | 0 |
| 0xaa | 7 | 0x6 | 0x203 | 0x40506 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 13 | 0 |
| 0xaa | 8 | 0x7 | 0x203 | 0x4050607 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 12 | 0 |
| 0xaa | 9 | 0x8 | 0x203 | 0x405060708 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 11 | 0 |
| 0xaa | 10 | 0x9 | 0x203 | 0x40506070809 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 10 | 0 |
| 0xaa | 11 | 0xa | 0x203 | 0x405060708090a | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 9 | 0 |
| 0xaa | 12 | 0xb | 0x203 | 0x405060708090a0b | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 8 | 0 |
| 0xaa | 13 | 0xc | 0x203 | 0x405060708090a0b0c | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 7 | 0 |
| 0xaa | 14 | 0xd | 0x203 | 0x405060708090a0b0c0d | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 6 | 0 |
| 0xaa | 15 | 0xe | 0x203 | 0x405060708090a0b0c0d0e | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 5 | 0 |
| 0xaa | 16 | 0xf | 0x203 | 0x405060708090a0b0c0d0e0f | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 4 | 0 |
| 0xaa | 17 | 0x10 | 0x203 | 0x405060708090a0b0c0d0e0f10 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 3 | 0 |
| 0xaa | 18 | 0x11 | 0x203 | 0x405060708090a0b0c0d0e0f1011 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 2 | 0 |
| 0xaa | 19 | 0x12 | 0x203 | 0x405060708090a0b0c0d0e0f101112 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 1 | 0 |
| 0xaa | 20 | 0x13 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 0 | 0 |
| 0xaa | 21 | ADD | 0x0 | 0x0 | 0x0 | 0x0 | 0 | 0 |
| 0xaa | 22 | STOP | 0x0 | 0x0 | 0x0 | 0x0 | 0 | 0 |
### Circuit Column
```rust
#[derive(Clone)]
pub struct BytecodeCircuitConfig<F> {
q_enable: Selector,
/// the contract address of the bytecodes. public input
instance_addr: Column<Instance>,
/// bytecode, operation code or pushed value. public input
instance_bytecode: Column<Instance>,
/// the contract address of the bytecodes (need to copy from public input)
addr: Column<Advice>,
/// the index that program counter points to
pc: Column<Advice>,
/// bytecode, operation code or pushed value (need to copy from public input)
bytecode: Column<Advice>,
/// pushed value, high 128 bits
value_hi: Column<Advice>,
/// pushed value, low 128 bits
value_lo: Column<Advice>,
/// accumulated value, high 128 bits. accumulation will go X times for PUSHX
acc_hi: Column<Advice>,
/// accumulated value, low 128 bits. accumulation will go X times for PUSHX
acc_lo: Column<Advice>,
/// count for accumulation, accumulation will go X times for PUSHX
cnt: Column<Advice>,
/// whether count is equal or larger than 16
is_high: Column<Advice>,
/// for chip to determine whether cnt is 0
cnt_is_zero: IsZeroWithRotationConfig<F>,
/// for chip to determine whether cnt is 15
cnt_is_15: IsZeroConfig<F>,
/// for chip to check if addr is changed from previous row
addr_unchange: IsZeroConfig<F>,
/// for chip to check if addr is zero, which means the row is padding
addr_is_zero: IsZeroWithRotationConfig<F>,
}
```
对于IsZeroConfig小工具，如果传入的值为0则返回结果为1，如果传入的值不为0则返回结果为0
- cnt_is_zero：用于判断cnt是否为0
- cnt_is_15：用于判断cnt是否为15
- addr_unchange：用于判断address是否发生了变化（Bytecode circuit table中可能是多个合约Bytecode共存的，不同的Bytecode对应不同的address），addr_cur - addr_prev，如果为0则addr没有发生变化
- addr_is_zero：Bytecode circuit table中会存在一个除了有实际意义的row之外，还存在一些为了凑行数的padding row，这些padding row所有的格子都是0
## 门约束
**cnt_prev=0约束**
cnt_prev=0的情况有三种：Opcode(非PUSH)、PUSH的最后一个byte、padding的行，
则当前行是新的Opcode或者是padding行
(padding的行由addr=0来约束，所有值都为0，Opcode的行则需要判断Bytecode不是PUSH的byte)
cnt_prev=0 ----> acc_hi_cur=0, acc_lo_cur=0
**cnt=0约束**
cnt=0的情况有三种：Opcode(非PUSH)、PUSH指令PUSH的最后一个byte、padding的row
(padding的row由addr=0来约束, Opcode(非PUSH) cnt一定为0, PUSH的最后一个byte的cnt_prev-cnt_cur=1)
cnt ==0 ----> value_hi-acc_hi=0, value_lo-acc_lo=0 (统一约束了cnt=0的value_hi和value_lo的值)
**cnt!=0约束**
cnt !=0 的情况只有一种，PUSH指令所PUSH的byte(非最后一个byte)，cnt是逐行减1的
cnt !=0 ----> `cnt_prev - cnt_cur = 1 `(约束cnt)
cnt !=0 ----> `acc_hi_prev + is_high*(acc_hi_prev*255 + bytecode) - acc_hi_cur =0`(约束acc_hi)
​ cnt !=0 && is_high=0 ----> `acc_hi_cur-acc_hi_prev=0` (cnt < 16的行，acc_hi的值是不变的)
​ cnt !=0 && is_high=1 ----> `acc_hi_prev + (acc_hi_prev*255 + bytecode) - acc_hi_cur =0=0` (即acc_hi_cur的值为`acc_pre*256+bytecoce`)
cnt !=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 !=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)
**addr约束**
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是累加的)
**todo：**
总结：
Opcode(非PUSH): cnt!=0 -----> cnt!=0的约束
Opcode(PUSH): cnt、is_high、acc_hi、acc_lo、value_hi、value_lo值都为0 (该约束缺少)
Addr=0， 所有值都为0
怎么区分Opcode是否为PUSH指令(IsZeroConfig?? 但是PUSH指令有12个，PUSH1~PUSH32)
当cnt != 0时
当前的value_lo等于Rotation(cur_cnt)的value_lo，value_hi也是同理，即value_lo和value_hi应等于最终计. 算出的value_lo、value_hi(PUSH的最后一个byte)
当cnt_prev=0时
​ padding的行由addr=0来约束，所有值都为0
​ Bytecode是Opcode而不是PUSH的byte
当cnt==0时
​ Opcode(PUSH): cnt为0
​ PUSH的最后一个byte的cnt_prev-cnt_cur=1 (怎么区分是PUSH的byte而不是Opcode)
怎么区分Opcode是否为PUSH指令(IsZeroConfig?? 但是PUSH指令有12个，PUSH1~PUSH32)
怎么区分是PUSH的byte而不是Opcode
is_code? ----> 如果是opcode===>is_code=1, 如果不是opcode===>is_code=0
is_push? ---->如果是push===>is_push=1, 如果不是is_push===>is_push=0
Tag? ----> Nil,OPCODE_NOPUSH, OPCODE_PUSH, BYTE
## Lookup约束
每一个byte都应该在fixed电路中Lookup到，即每一个字节大小都应该在0~255范围内
Bytecode circuit用于约束合约的Bytecode，为其他电路提供bytecode的来源依据，其他子电路可通过Lookup约束来验证所操作bytecode码是否是合法的。
Bytecode table中存放的可能并不只是一个合约的Bytecode，不同的合约的Bytecode以`address`进行标识，Bytecode与address是唯一一一对应。
对于一个合约的Bytecode而言，`pc`是opcode或者no_code(push的byte)唯一的标识
在对Bytecode进行处理时，将Bytecode分为两类：
1. Opcode(非PUSH)：操作指令，如ADD、SUB、CODECOPY
2. Opcode(PUSH)：PUSH1~PUSH2
## Witness、Column设计
### Witness
```rust
#[derive(Clone, Debug, Default, Serialize)]
pub struct Row {
/// the contract address of the bytecodes
pub addr: Option<U256>,
/// the index that program counter points to
pub pc: Option<U256>,
/// bytecode, operation code or pushed value
pub bytecode: Option<U256>,
/// pushed value, high 128 bits (0 or non-push opcodes)
pub value_hi: Option<U256>,
/// pushed value, low 128 bits (0 or non-push opcodes)
pub value_lo: Option<U256>,
/// accumulated value, high 128 bits. accumulation will go X times for PUSHX
pub acc_hi: Option<U256>,
/// accumulated value, low 128 bits. accumulation will go X times for PUSHX
pub acc_lo: Option<U256>,
/// count for accumulation, accumulation will go X times for PUSHX
pub cnt: Option<U256>,
/// whether count is equal or larger than 16
pub is_high: Option<U256>,
}
```
- cnt:如果是非PUSH的Opcode则cnt=0， 对于PUSH指令，cnt为PUSH的byte的数量，如PUSH1 --> cnt=1, PUSH2 --> cnt=2, PUSH31 --> cnt=31, PUSH32 --> cnt=32，对于no_code则cnt的值为(0~cnt-1)
- is_high：cnt >=16 ---> 1，cnt < 16 ---> 0，主要是用于辅助计算acc的值(规定acc的值最多为16个字节)
- acc_hi：cnt >=16的Bytecode执行此计算，`acc_hi_pre * 256 + bytecode`，即计算byte的累加值
- acc_lo：cnt < 16的Bytecode执行此计算，`acc_lo_pre * 256 + bytecode`，即计算byte的累加值
- value_hi：cnt >= 16的Bytecode的最终累加值，即最终的acc_hi
- value_lo：cnt < 15的Bytecode的最终累加值，即最终的acc_lo
注：Opcode的 cnt、is_high、acc_hi、acc_lo、value_hi、value_lo值都为0
假如有如下指令：
```shell
PUSH1 0xa
PUSH18 0x02030405060708090a0b0c0d0e0f10111213
ADD
```
假如addr为0xaa，则表格如下（这里的Opcode以字符串的形式表现比较形象）：
| addr | pc | bytecode | acc_hi | acc_lo | value_hi | value_lo | cnt | is_high |
| ---- | ---- | -------- | ------ | --------------------------------- | -------- | --------------------------------- | ---- | ------- |
| 0xaa | 0 | PUSH1 | 0x0 | 0x0 | 0x0 | 0x0 | 1 | 0 |
| 0xaa | 1 | 0xa | 0x0 | 0xa | 0x0 | 0xa | 0 | 0 |
| 0xaa | 2 | PUSH17 | 0x0 | 0x0 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 18 | 1 |
| 0xaa | 3 | 0x2 | 0x2 | 0x0 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 17 | 1 |
| 0xaa | 4 | 0x3 | 0x203 | 0x0 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 16 | 1 |
| 0xaa | 5 | 0x4 | 0x203 | 0x4 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 15 | 0 |
| 0xaa | 6 | 0x5 | 0x203 | 0x405 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 14 | 0 |
| 0xaa | 7 | 0x6 | 0x203 | 0x40506 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 13 | 0 |
| 0xaa | 8 | 0x7 | 0x203 | 0x4050607 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 12 | 0 |
| 0xaa | 9 | 0x8 | 0x203 | 0x405060708 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 11 | 0 |
| 0xaa | 10 | 0x9 | 0x203 | 0x40506070809 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 10 | 0 |
| 0xaa | 11 | 0xa | 0x203 | 0x405060708090a | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 9 | 0 |
| 0xaa | 12 | 0xb | 0x203 | 0x405060708090a0b | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 8 | 0 |
| 0xaa | 13 | 0xc | 0x203 | 0x405060708090a0b0c | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 7 | 0 |
| 0xaa | 14 | 0xd | 0x203 | 0x405060708090a0b0c0d | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 6 | 0 |
| 0xaa | 15 | 0xe | 0x203 | 0x405060708090a0b0c0d0e | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 5 | 0 |
| 0xaa | 16 | 0xf | 0x203 | 0x405060708090a0b0c0d0e0f | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 4 | 0 |
| 0xaa | 17 | 0x10 | 0x203 | 0x405060708090a0b0c0d0e0f10 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 3 | 0 |
| 0xaa | 18 | 0x11 | 0x203 | 0x405060708090a0b0c0d0e0f1011 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 2 | 0 |
| 0xaa | 19 | 0x12 | 0x203 | 0x405060708090a0b0c0d0e0f101112 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 1 | 0 |
| 0xaa | 20 | 0x13 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 0x203 | 0x405060708090a0b0c0d0e0f10111213 | 0 | 0 |
| 0xaa | 21 | ADD | 0x0 | 0x0 | 0x0 | 0x0 | 0 | 0 |
| 0xaa | 22 | STOP | 0x0 | 0x0 | 0x0 | 0x0 | 0 | 0 |
### Circuit Column
```rust
#[derive(Clone)]
pub struct BytecodeCircuitConfig<F> {
q_enable: Selector,
/// the contract address of the bytecodes. public input
instance_addr: Column<Instance>,
/// bytecode, operation code or pushed value. public input
instance_bytecode: Column<Instance>,
/// the contract address of the bytecodes (need to copy from public input)
addr: Column<Advice>,
/// the index that program counter points to
pc: Column<Advice>,
/// bytecode, operation code or pushed value (need to copy from public input)
bytecode: Column<Advice>,
/// pushed value, high 128 bits
value_hi: Column<Advice>,
/// pushed value, low 128 bits
value_lo: Column<Advice>,
/// accumulated value, high 128 bits. accumulation will go X times for PUSHX
acc_hi: Column<Advice>,
/// accumulated value, low 128 bits. accumulation will go X times for PUSHX
acc_lo: Column<Advice>,
/// count for accumulation, accumulation will go X times for PUSHX
cnt: Column<Advice>,
/// whether count is equal or larger than 16
is_high: Column<Advice>,
/// for chip to determine whether cnt is 0
cnt_is_zero: IsZeroWithRotationConfig<F>,
/// for chip to determine whether cnt is 15
cnt_is_15: IsZeroConfig<F>,
/// for chip to check if addr is changed from previous row
addr_unchange: IsZeroConfig<F>,
/// for chip to check if addr is zero, which means the row is padding
addr_is_zero: IsZeroWithRotationConfig<F>,
}
```
对于IsZeroConfig小工具，如果传入的值为0则返回结果为1，如果传入的值不为0则返回结果为0
- cnt_is_zero：用于判断cnt是否为0
- cnt_is_15：用于判断cnt是否为15
- addr_unchange：用于判断address是否发生了变化（Bytecode circuit table中可能是多个合约Bytecode共存的，不同的Bytecode对应不同的address），addr_cur - addr_prev，如果为0则addr没有发生变化
- addr_is_zero：Bytecode circuit table中会存在一个除了有实际意义的row之外，还存在一些为了凑行数的padding row，这些padding row所有的格子都是0
## 门约束
**cnt_prev=0约束**
cnt_prev=0的情况有三种：Opcode(非PUSH)、PUSH的最后一个byte、padding的行，
则当前行是新的Opcode或者是padding行
(padding的行由addr=0来约束，所有值都为0，Opcode的行则需要判断Bytecode不是PUSH的byte)
cnt_prev=0 ----> acc_hi_cur=0, acc_lo_cur=0
**cnt=0约束**
cnt=0的情况有三种：Opcode(非PUSH)、PUSH指令PUSH的最后一个byte、padding的row
(padding的row由addr=0来约束, Opcode(非PUSH) cnt一定为0, PUSH的最后一个byte的cnt_prev-cnt_cur=1)
cnt ==0 ----> value_hi-acc_hi=0, value_lo-acc_lo=0 (统一约束了cnt=0的value_hi和value_lo的值)
**cnt!=0约束**
cnt !=0 的情况只有一种，PUSH指令所PUSH的byte(非最后一个byte)，cnt是逐行减1的
cnt !=0 ----> `cnt_prev - cnt_cur = 1 `(约束cnt)
cnt !=0 ----> `acc_hi_prev + is_high*(acc_hi_prev*255 + bytecode) - acc_hi_cur =0`(约束acc_hi)
​ cnt !=0 && is_high=0 ----> `acc_hi_cur-acc_hi_prev=0` (cnt < 16的行，acc_hi的值是不变的)
​ cnt !=0 && is_high=1 ----> `acc_hi_prev + (acc_hi_prev*255 + bytecode) - acc_hi_cur =0=0` (即acc_hi_cur的值为`acc_pre*256+bytecoce`)
cnt !=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 !=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)
**addr约束**
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是累加的)
**todo：**
总结：
Opcode(非PUSH): cnt!=0 -----> cnt!=0的约束
Opcode(PUSH): cnt、is_high、acc_hi、acc_lo、value_hi、value_lo值都为0 (该约束缺少)
Addr=0， 所有值都为0
怎么区分Opcode是否为PUSH指令(IsZeroConfig?? 但是PUSH指令有12个，PUSH1~PUSH32)
当cnt != 0时
当前的value_lo等于Rotation(cur_cnt)的value_lo，value_hi也是同理，即value_lo和value_hi应等于最终计算出的value_lo、value_hi(PUSH的最后一个byte)
当cnt_prev=0时
​ padding的行由addr=0来约束，所有值都为0
​ Bytecode是Opcode而不是PUSH的byte
当cnt==0时
​ Opcode(PUSH): cnt为0
​ PUSH的最后一个byte的cnt_prev-cnt_cur=1 (怎么区分是PUSH的byte而不是Opcode)
怎么区分Opcode是否为PUSH指令(IsZeroConfig?? 但是PUSH指令有12个，PUSH1~PUSH32)
怎么区分是PUSH的byte而不是Opcode
is_code? ----> 如果是opcode===>is_code=1, 如果不是opcode===>is_code=0
is_push? ---->如果是push===>is_push=1, 如果不是is_push===>is_push=0
Tag? ----> Nil,OPCODE_NOPUSH, OPCODE_PUSH, BYTE
## Lookup约束
每一个byte都应该在fixed电路中Lookup到，即每一个字节大小都应该在0~255范围内

Copyright © 2024 ChainWeaver Org. All Rights Reserved. 版权所有。

京ICP备2023035722号-3

京公网安备 11010802044225号