GitLab

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

设计

Witness、Column设计

见代码

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

布局

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

门约束

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