用于处理EXP指令以及电路中的exp运算的子电路

设计

Witness、Column设计

Witness设计

#[derive(Clone, Debug, Serialize)]
pub struct Row {
    // type of row, one of zero, one, SQUARE or Bit
    pub tag: Tag,
    // base of exp
    pub base_hi: U256,
    pub base_lo: U256,
    // index of exp
    pub index_hi: U256,
    pub index_lo: U256,
    // count of index
    pub count: U256,
    // exp res
    pub power_hi: U256,
    pub power_lo: U256,
}

#[derive(Clone, Copy, Debug, Default, Serialize, EnumIter, EnumString)]
pub enum Tag {
    #[default]
    Zero,
    One,
    Square,
    Bit0, // index & 1 = 0
    Bit1, // index & 1 = 1
}

Circuit Column 设计

#[derive(Clone)]
pub struct ExpCircuitConfig<F: Field> {
    q_enable: Selector,
    /// the operation tag, zero,one,Bit,SQUARE
    pub tag: BinaryNumberConfig<Tag, LOG_NUM_EXP_TAG>,
    /// base hi , base lo
    pub base: [Column<Advice>; EXP_NUM_OPERAND],
    /// index hi, index lo
    pub index: [Column<Advice>; EXP_NUM_OPERAND],
    /// power hi, power lo
    pub power: [Column<Advice>; EXP_NUM_OPERAND],
    /// count
    pub count: Column<Advice>,
    /// IsZero chip for column count
    pub count_is_zero: IsZeroWithRotationConfig<F>,
    /// for chip to determine whether count is 128
    pub count_is_128: IsZeroConfig<F>,
    /// for chip to determine whether count is 256
    pub count_is_256: IsZeroConfig<F>,
    /// arithmetic table for lookup
    arithmetic_table: ArithmeticTable,
}

Witness生成算法设计

    pub fn from_operands(
        base: U256,
        index: U256,
    ) -> (U256, Vec<Self>, Vec<arithmetic::Row>, Vec<arithmetic::Row>) 

• 入参: base为底数,index为指数
• 返回参数: exp运算结果,exp生成witness row 数组(exp rows),使用的乘法电路运算生成的witness row(mul rows),使用的加法电路运算生成的witness row(add rows)
• 算法:

  • 生成Tag::Zero 行,将其添加到exp rows中

  • 若index == 0,则直接返回

  • 生成Tag::One 行, 将其添加到exp rows中

  • 循环对 div 做2的除法和取模运算,记商为div,余数为rem

    • 生成Tag::Bit0/Tag::Bit1 Row；其中count = (exp rows中的前一行的row)的count, is_high = (exp rows中的前一行的row)的is_high
      • 若rem == 0 , 则生成Tag::Bit0 Row,将其添加到exp rows中；其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo；power hi/lo = (exp rows中的两行前的row)的 power hi/lo
      • 若rem == 1 , 则生成Tag::Bit1 Row,将其添加到exp rows中；其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo + (exp rows中的前一行的row)的index hi/lo, 调用加法电路生成add row,将其添加到add rows中；power hi/lo = (exp rows中的两行前的row)的 power hi/lo * (exp rows中的前一行的row)的 power hi/lo,调用乘法电路生成mul row,将其添加到mul rows中
    • 若div == 0, 则中断循环
    • 否则:
      • 生成Tag::SQUARE Row,将其添加到exp rows中；其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo * 2 ,调用乘法电路生成mul row,将其添加到mul rows中；power hi/lo = (exp rows中的两行前的row)的 power hi/lo 的平方,调用乘法电路生成mul row,将其添加到mul rows中；count = (exp rows中的前一行的row)的count + 1；
        • 若count == 0 ,则is_high = 0
        • 若count == 128 ,则is_high = 1
        • 否则 is_high = (exp rows中的两行前的row)的is_high

  • 去exp rows中最后一行的power hi/lo, 将power hi << 128 + power lo作为最终的power value, return (power value,exp rows, mul rows, add rows)

门约束

Base hi/lo 约束

• 若当前行的Tag为ONE,SQUARE,BIT0,BIT1, 则base hi/lo 等于前一行的base hi/lo

Tag 约束

• 若当前行的Tag为ZERO,则前一行的Tag为ZERO or BIT1 or BIT0
• 若当前行的Tag为SQUARE,则前一行的Tag必为Bit0 or Bit1
• 若当前行的Tag为ONE,则前一行的Tag必为ZERO
• 若当前行的Tag为Bit0 or Bit1,则前一行的Tag为ONE or SQUARE

Count约束

• 若当前行的Tag为ZERO,则count为0
• 若当前行的Tag为ONE,则count为0
• 若当前行的Tag为SQUARE,则count为前一行的count+1
• 若当前行的Tag为Bit0 or Bit1,则count等于前一行的count

Index/Power约束

• 若当前行的Tag为ZERO,则index为0,power为1,则index
• 若当前行的Tag为ONE,则index为1,power为BASE(底数)
• 若当前行的Tag为Bit0,则index等于前两行index,power等于前两行的power
• 若当前行的Tag为SQUARE,且count为128,则index hi为1,index lo为0

Lookup约束

Tag为SQUARE,Index运算lookup

若Tag为SQUARE时,index 等于两行前的index * 2

Tag为SQUARE,Power运算lookup

若Tag为SQUARE时,power为两行前的power的平方

Tag为Bit1,Index运算lookup

若Tag为Bit1,index为两行前的index + 一行前的index

Tag为Bit1,Power运算lookup

若Tag为Bit1,power为两行前的power * 一行前的power