GitLab

专门处理 AND OR BYTE 这些按位运算的指令的子电路。在此电路内，位数长的整数被拆成字节，以字节为单位进行逻辑运算。

设计

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,
}

pub enum Tag {
    #[default]
    Nil,
    And,
    Or,
}

布局

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运算，每一个整数都会被拆成一个一个字节，实际运算时分别对相应位置的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

门约束

电路中的行数不可能是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_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是所求的数值