|
|
|
专门处理 AND OR XOR BYTE 这些按位运算的指令的子电路。在此电路内，位数长的整数被拆成字节，以字节为单位进行逻辑运算。
|
|
|
|
|
|
|
|
## 设计
|
|
|
|
|
|
|
|
### Witness、Column设计
|
|
|
|
|
|
|
|
见代码
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub struct Row {
|
|
|
|
/// The operation tag, one of AND, OR, XOR
|
|
|
|
pub tag: Tag,
|
|
|
|
/// The byte value of operand 0
|
|
|
|
pub byte_0: U256,
|
|
|
|
/// The byte value of operand 1
|
|
|
|
pub byte_1: U256,
|
|
|
|
/// The byte value of operand 2
|
|
|
|
pub byte_2: U256,
|
|
|
|
/// The accumulation of bytes in one operation of operand 0
|
|
|
|
pub acc_0: U256,
|
|
|
|
/// The accumulation of bytes in one operation of operand 1
|
|
|
|
pub acc_1: U256,
|
|
|
|
/// The accumulation of bytes in one operation of operand 2
|
|
|
|
pub acc_2: U256,
|
|
|
|
/// The sum of bytes in one operation of operand 2, used to compute byte opcode
|
|
|
|
pub sum_2: U256,
|
|
|
|
/// The counter for one operation
|
|
|
|
pub cnt: U256,
|
|
|
|
}
|
|
|
|
|
|
|
|
pub enum Tag {
|
|
|
|
#[default]
|
|
|
|
Nil
|
|
|
|
And,
|
|
|
|
Or,
|
|
|
|
Xor,
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
### 布局
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub struct BitwiseCircuitConfig<F: Field> {
|
|
|
|
q_enable: Selector,
|
|
|
|
/// The operation tag, one of AND, OR, XOR
|
|
|
|
pub tag: BinaryNumberConfig<crate::witness::copy::Tag, NUM_BITWISE_TAG>,
|
|
|
|
/// The byte value of operand 0
|
|
|
|
pub byte_0: Column<Advice>,
|
|
|
|
/// The byte value of operand 1
|
|
|
|
pub byte_1: Column<Advice>,
|
|
|
|
/// The byte value of operand 2
|
|
|
|
pub byte_2: Column<Advice>,
|
|
|
|
/// The accumulation of bytes in one operation of operand 0
|
|
|
|
pub acc_0: Column<Advice>,
|
|
|
|
/// The accumulation of bytes in one operation of operand 1
|
|
|
|
pub acc_1: Column<Advice>,
|
|
|
|
/// The accumulation of bytes in one operation of operand 2
|
|
|
|
pub acc_2: Column<Advice>,
|
|
|
|
/// The sum of bytes in one operation of operand 2, used to compute byte opcode
|
|
|
|
pub sum_2: Column<Advice>,
|
|
|
|
/// The counter for one operation
|
|
|
|
pub cnt: Column<Advice>,
|
|
|
|
/// IsZero chip for column cnt
|
|
|
|
pub cnt_is_zero: IsZeroWithRotationConfig<F>,
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
### 列的含义
|
|
|
|
|
|
|
|
`BitwiseCircuit`主要用于对两个长度最长的整数进行AND、OR、XOR运算，每一个整数都会被拆成一个一个字节，实际运算时分别对相应位置的byte进行运算。
|
|
|
|
|
|
|
|
`byte_0`和`byte_1`分别是两个数值的某一个位置上的byte，`byte_2`为`byte_0`和`byte_1`的运算结果，`acc_0`、`acc_1`、`acc_2`分别是`byte_0`、`byte_1`、`byte_2`的累加值，即`acc=byte+acc_pre*256`，`sum_2`为`byte_2`的累加和，即`sum=byte+sum_pre`。
|
|
|
|
|
|
|
|
例如：0xabcdef AND 0xaabbcc
|
|
|
|
|
|
|
|
| tag | byte_0 | byte_1 | byte_2 | acc_0 | acc_1 | acc_2 | sum_2 | cnt |
|
|
|
|
| ---- | ------ | ------ | ------ | -------- | -------- | -------- | ----- | ---- |
|
|
|
|
| And | 0xab | 0xaa | 0xaa | 0xab | 0xaa | 0xaa | 0xaa | 0 |
|
|
|
|
| And | 0xcd | 0xbb | 0x89 | 0xabcd | 0xaabb | 0xaa89 | 0x133 | 1 |
|
|
|
|
| And | 0xef | 0xcc | 0xcc | 0xabcdef | 0xaabbcc | 0xaa89cc | 0x1ff | 2 |
|
|
|
|
|
|
|
|
### 门约束
|
|
|
|
|
|
|
|
电路中的行数不可能是16的整数倍，因为存在一些填充值(如begin_padding)，电路自动padding的行使用Tag::Nil进行约束，Tag为Nil的行的值都为默认值，即为0
|
|
|
|
|
|
|
|
- tag_is_not_nil，cnt=0 ---> acc_0=byte_0、acc_1=byte_1、acc_2=byte_2、sum_2=byte_2 ，`cnt=0-->pre_cnt=15（暂未使用）`
|
|
|
|
- tag_is_not_nil，cnt != 0 ---> `acc_0=byte_0+acc_0_pre*256`，`acc_1=byte_1+acc_1_pre*256`，`acc_2=acc_2_pre*256`, `sum_2=byte_2+sum2_pre`，`cnt=cnt_pre+1`，`tag=tag_pre`
|
|
|
|
- tag_is_not_nil，next_cnt=0 --> cnt=15
|
|
|
|
|
|
|
|
- tag_is_nil ---> byte_0=0, byte_1=0, byte_2=0, acc_0=0, acc_1=0, acc_2=0, sum_2=0, cnt=0
|
|
|
|
|
|
|
|
next_cnt=0--->cnt=15 (同时也验证了，只要cnt=15则next_cnt=0)
|
|
|
|
|
|
|
|
### LookUp约束
|
|
|
|
|
|
|
|
使用lookup对`<tag、byte_0、byte1、byte_2>`进行证明，来源：bitwise，去向：fixed (fxed子电路中有对256位的数值的and、or、xor的计算的枚举)
|
|
|
|
|
|
|
|
注：只对Tag不为Nil的行进行LookUp
|
|
|
|
|
|
|
|
专门处理 AND OR XOR BYTE 这些按位运算的指令的子电路。在此电路内，位数长的整数被拆成字节，以字节为单位进行逻辑运算。
|
|
|
|
|
|
|
|
## 设计
|
|
|
|
|
|
|
|
### Witness、Column设计
|
|
|
|
|
|
|
|
见代码
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub struct Row {
|
|
|
|
/// The operation tag, one of AND, OR, XOR
|
|
|
|
pub tag: Tag,
|
|
|
|
/// The byte value of operand 0
|
|
|
|
pub byte_0: U256,
|
|
|
|
/// The byte value of operand 1
|
|
|
|
pub byte_1: U256,
|
|
|
|
/// The byte value of operand 2
|
|
|
|
pub byte_2: U256,
|
|
|
|
/// The accumulation of bytes in one operation of operand 0
|
|
|
|
pub acc_0: U256,
|
|
|
|
/// The accumulation of bytes in one operation of operand 1
|
|
|
|
pub acc_1: U256,
|
|
|
|
/// The accumulation of bytes in one operation of operand 2
|
|
|
|
pub acc_2: U256,
|
|
|
|
/// The sum of bytes in one operation of operand 2, used to compute byte opcode
|
|
|
|
pub sum_2: U256,
|
|
|
|
/// The counter for one operation
|
|
|
|
pub cnt: U256,
|
|
|
|
}
|
|
|
|
|
|
|
|
pub enum Tag {
|
|
|
|
#[default]
|
|
|
|
Nil
|
|
|
|
And,
|
|
|
|
Or,
|
|
|
|
Xor,
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
### 布局
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub struct BitwiseCircuitConfig<F: Field> {
|
|
|
|
q_enable: Selector,
|
|
|
|
/// The operation tag, one of AND, OR, XOR
|
|
|
|
pub tag: BinaryNumberConfig<crate::witness::copy::Tag, NUM_BITWISE_TAG>,
|
|
|
|
/// The byte value of operand 0
|
|
|
|
pub byte_0: Column<Advice>,
|
|
|
|
/// The byte value of operand 1
|
|
|
|
pub byte_1: Column<Advice>,
|
|
|
|
/// The byte value of operand 2
|
|
|
|
pub byte_2: Column<Advice>,
|
|
|
|
/// The accumulation of bytes in one operation of operand 0
|
|
|
|
pub acc_0: Column<Advice>,
|
|
|
|
/// The accumulation of bytes in one operation of operand 1
|
|
|
|
pub acc_1: Column<Advice>,
|
|
|
|
/// The accumulation of bytes in one operation of operand 2
|
|
|
|
pub acc_2: Column<Advice>,
|
|
|
|
/// The sum of bytes in one operation of operand 2, used to compute byte opcode
|
|
|
|
pub sum_2: Column<Advice>,
|
|
|
|
/// The counter for one operation
|
|
|
|
pub cnt: Column<Advice>,
|
|
|
|
/// IsZero chip for column cnt
|
|
|
|
pub cnt_is_zero: IsZeroWithRotationConfig<F>,
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
### 列的含义
|
|
|
|
|
|
|
|
`BitwiseCircuit`主要用于对两个长度最长的整数进行AND、OR、XOR运算，每一个整数都会被拆成一个一个字节，实际运算时分别对相应位置的byte进行运算。
|
|
|
|
|
|
|
|
`byte_0`和`byte_1`分别是两个数值的某一个位置上的byte，`byte_2`为`byte_0`和`byte_1`的运算结果，`acc_0`、`acc_1`、`acc_2`分别是`byte_0`、`byte_1`、`byte_2`的累加值，即`acc=byte+acc_pre*256`，`sum_2`为`byte_2`的累加和，即`sum=byte+sum_pre`。
|
|
|
|
|
|
|
|
例如：0xabcdef AND 0xaabbcc
|
|
|
|
|
|
|
|
| tag | byte_0 | byte_1 | byte_2 | acc_0 | acc_1 | acc_2 | sum_2 | cnt |
|
|
|
|
| ---- | ------ | ------ | ------ | -------- | -------- | -------- | ----- | ---- |
|
|
|
|
| And | 0xab | 0xaa | 0xaa | 0xab | 0xaa | 0xaa | 0xaa | 0 |
|
|
|
|
| And | 0xcd | 0xbb | 0x89 | 0xabcd | 0xaabb | 0xaa89 | 0x133 | 1 |
|
|
|
|
| And | 0xef | 0xcc | 0xcc | 0xabcdef | 0xaabbcc | 0xaa89cc | 0x1ff | 2 |
|
|
|
|
|
|
|
|
### 门约束
|
|
|
|
|
|
|
|
电路中的行数不可能是16的整数倍，因为存在一些填充值(如begin_padding)，电路自动padding的行使用Tag::Nil进行约束，Tag为Nil的行的值都为默认值，即为0
|
|
|
|
|
|
|
|
- tag_is_not_nil，cnt=0 ---> acc_0=byte_0、acc_1=byte_1、acc_2=byte_2、sum_2=byte_2 ，`cnt=0-->pre_cnt=15（暂未使用）`
|
|
|
|
- tag_is_not_nil，cnt != 0 ---> `acc_0=byte_0+acc_0_pre*256`，`acc_1=byte_1+acc_1_pre*256`，`acc_2=acc_2_pre*256`, `sum_2=byte_2+sum2_pre`，`cnt=cnt_pre+1`，`tag=tag_pre`
|
|
|
|
- tag_is_not_nil，next_cnt=0 --> cnt=15
|
|
|
|
|
|
|
|
- tag_is_nil ---> byte_0=0, byte_1=0, byte_2=0, acc_0=0, acc_1=0, acc_2=0, sum_2=0, cnt=0
|
|
|
|
|
|
|
|
next_cnt=0--->cnt=15 (同时也验证了，只要cnt=15则next_cnt=0)
|
|
|
|
|
|
|
|
### LookUp约束
|
|
|
|
|
|
|
|
使用lookup对`<tag、byte_0、byte1、byte_2>`进行证明，来源：bitwise，去向：fixed (fxed子电路中有对256位的数值的and、or、xor的计算的枚举)
|
|
|
|
|
|
|
|
注：只对Tag不为Nil的行进行LookUp
|
|
|
|
|
