Bitwise
专门处理 AND OR 这些按位运算的指令的子电路。在此电路内,位数长的整数被拆成字节,以字节为单位进行逻辑运算。
设计
Witness、Column设计
见代码
pub struct Row {
/// The operation tag, one of AND, OR
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,
/// Operand 2 most significant byte index
pub index: U256,
}
pub enum Tag {
#[default]
Nil,
And,
Or,
}
布局
pub struct BitwiseCircuitConfig<F: Field> {
q_enable: Selector,
/// The operation tag, one of AND, OR
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>,
/// Index of the most significant byte
pub index: Column<Advice>,
/// IsZero chip for column cnt
pub cnt_is_zero: IsZeroWithRotationConfig<F>,
/// acc_2 is zero flag
pub acc_2_is_zero: IsZeroWithRotationConfig<F>,
}
列的含义
BitwiseCircuit
主要用于对两个长度最长的整数进行AND、OR运算,每一个整数都会被拆成一个一个字节,实际运算时分别对相应位置的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
。
index
用于表示最高有效字节数,在cnt==0
时,如果acc_2
为0,index = 0
,否则index = 16
;对于cnt != 0
的行,当acc_2
从0值变为非0值时,index = 16-cnt
,否则index = prev_index
。
例如:0xabcdef AND 0xaabbcc
tag | byte_0 | byte_1 | byte_2 | acc_0 | acc_1 | acc_2 | sum_2 | cnt | index |
---|---|---|---|---|---|---|---|---|---|
And | 0xab | 0xaa | 0xaa | 0xab | 0xaa | 0xaa | 0xaa | 0 | 16 |
And | 0xcd | 0xbb | 0x89 | 0xabcd | 0xaabb | 0xaa89 | 0x133 | 1 | 16 |
And | 0xef | 0xcc | 0xcc | 0xabcdef | 0xaabbcc | 0xaa89cc | 0x1ff | 2 | 16 |
门约束
电路中的行数不可能是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
-
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_not_nil, cnt == 0 ==> index = 16 or 0
-
tag_is_not_nil, cnt != 0 ==> index = index_prev or index = 16 - cnt
-
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
LookUp约束
使用lookup对<tag、byte_0、byte1、byte_2>
进行证明,来源:bitwise,去向:fixed (fxed子电路中有对256位的数值的and、or 的计算的枚举)
注:只对Tag不为Nil的行进行LookUp
ACC计算
应该使用u128.to_be_bytes,即大端序来计算,例如:0x123456789a计算acc
---->内存地址增长方向:低地址--------------------->高地址
---->u128.to_be_bytes()
---->小端序[u8;16]: 低位字节在低位地址,高位字节在高位地址
----> [154,120,86,52,18, 0, 0...0, 0]
----> 即[0x9a,0x78,0x56,0x34,0x12, 0, 0...0, 0]
---->遍历[u8;16], acc = cur_byte + acc_pre
---->0x9a785634120000000000000000000000
---->内存地址增长方向:低地址--------------------->高地址
---->u128.to_be_bytes()
---->大端序[u8;16]:高位字节在低位地址,低字节在高位地址
---->[0, 0...18,52,86,120,154]
---->即[0, 0...0x12,0x34,0x56,0x78,0x9a]
---->遍历[u8;16], acc = cur_byte + acc_pre
----> 0x0000000000000000000000123456789a
即u128的大端序的[u8;16]计算acc是所求的数值