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]
    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

门约束

• cnt=0 ---> acc_0=byte_0、acc_1=byte_1、acc_2=byte_2、sum_2=byte_2
• 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，tag=tag_pre

LookUp约束

使用lookup对byte_2进行范围证明(小于256的范围)，来源：bitwise，去向：fixed