布局

arithmetic 子电路的设计包含如下几列。我们重点关注 operand与 u16列，

pub struct ArithmeticCircuitConfig<F> {
    q_enable: Selector,
    /// Tag for arithmetic operation type
    tag: BinaryNumberConfig<Tag, LOG_NUM_ARITHMETIC_TAG>,
    /// The operands in one row, splitted to 2 (high and low 128-bit)
    operands: [[Column<Advice>; 2]; NUM_OPERAND],
    /// The 16-bit values in one row
    u16s: [Column<Advice>; NUM_U16],
    /// Row counter, decremented for rows in one execution state
    cnt: Column<Advice>,
    /// IsZero chip for column cnt
    cnt_is_zero: IsZeroWithRotationConfig<F>,
}

pub enum Tag {
    #[default]
    Nil,
    Add,
    Sub,
    Mul,
    DivMod,
    SltSgt,
    SdivSmod,
    Addmod,
    Mulmod,
}

在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见here。

列的含义

operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b,c,overflow。u16*用来 lookup 算术中的输出如 c_hi,c_lo 属于 u128 范围。这里我们只需要保证输出值的 lookup 就好。cnt 记录某个具体算术指令的行计数器，从正数开始递减到 0。

约束

在 arithmetic 子电路中约束可以分为两类。 通用约束

• 约束 cnt 除零行外,当前行与下一行差值为 1

不同 Tag 对应的约束不同 请注意我们这里所有的 u16 都是 little endian 小端编码

• Add (含义：a+b=c+overflow*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和)

  • 注：加法可以用这个
  • 如果是 cnt=0 行，则 cnt_prev=1,cnt_prev_prev=0
  • c_lo = u16 sum(rotation cur)
  • c_hi = u16 sum(rotation prev)
  • carry hi is bool
  • carry lo is bool
  • c lo + carry lo * 2^128 = a lo + b lo
  • c hi + carry hi * 2^128 = a hi + b hi + carry lo

• Sub (含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和)

  • 注：减法，LT，GT 都可以用这个
  • c_lo = u16 sum(rotation cur)
  • c_hi = u16 sum(rotation prev)
  • carry hi is bool
  • carry lo is bool
  • a_lo + carrry_lo * 2^128 = b_lo + c_lo
  • a_hi + carry_hi * 2^128 - carry_lo= b_hi + c_hi
  • 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b

• Div_Mod (我们有a/b = d + c ==> d * b + c = a 同时约束 c 小于 b)

  if tag is div, (a,b,c,d) = (push, pop2, pop1 - push \* pop2, pop1)
  if tag is mod, (a,b,c,d) = (if pop2 is zero{0}else{pop1/pop2},pop2,if pop2 is zero{pop1}else{push},pop1)
  
  define
  - define t0 = a0 \* b0
  - define t1 = a0 \* b1 + a1 \* b0
  - define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
  - define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2
  - define t_lo=t0+(t1)\*2^64
  - define t_hi=(t2)+(t3)\*2^64
  - define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
  - define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128

  • 如果是 0 行，约束 num_row is 10,并且约束 cnt 自增的有效性
  • a_lo = u16 sum(rotation cur)
  • a_hi = u16 sum(rotation -1)
  • b_lo = u16 sum(rotation -2)
  • b_hi = u16 sum(rotation -3)
  • c_lo = u16 sum(rotation -4)
  • c_hi = u16 sum(rotation -5)
  • d_lo = u16 sum(rotation -6)
  • d_hi = u16 sum(rotation -7)
  • (t_lo+c_lo-car_lo*2^128) - d_lo
  • (t_hi+c_hi+car_lo-car_hi*2^128) - d_hi
  • residue < divisor when divisor != 0
  • carry_hi == 0
  • carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。

• Mul(需要 6 行对 a,b,c lookup ) 其中 operand0 是 a,operand1 是 b

  • define t0 = a0 * b0 （0-128bit）
  • define t1 = a0 * b1 + a1 * b0 (64-193bit)
  • define t2 = a0 * b2 + a2 * b0 + a1 * b1 (128 - 257bit)
  • define t3 = a0 * b3 + a3 * b0 + a2 * b1 + a1 * b2 (192- 322bit)
  • define t_lo=t0+(t1)*2^64
  • define t_hi=(t2)+(t3)*2^64
  • define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
  • define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128
  • 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性
  • a_lo = u16 sum(rotation cur)
  • a_hi = u16 sum(rotation -1)
  • b_lo = u16 sum(rotation -2)
  • b_hi = u16 sum(rotation -3)
  • c_lo = u16 sum(rotation -4)
  • c_hi = u16 sum(rotation -5)
  • carry_hi == u16 sum(rotation -6) 请注意这里我们使用的是5位u16数据的和，从define部分我们可以知道carry_hi等于322 - 256 = 66bit。
  • carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。
  • （t_lo-car_lo*2^128） -（c_lo）
  • （t_hi+car_lo-car_hi*2^128）-（c_hi）

• Slt_Sgt (我们使用 a-b=c - carry<<256 的公式来约束有相同符号的内容这里我们需要注意的是，当符号相等时，我们统一按照无符号整数比较大小)``

  • 比较a_hi,b_hi最高u16位是否小于2^15确定a,b符号。如果a_lt == 1则a为正数，否则为负数。b_lt同理。
  • 同时我们需要约束a_hi和b_hi等于对应的u16s_sum。这里主要是为了约束我们用来判断符号的u16的正确性。
  • a,b符号不相等时。我们有(a_lt - b_lt)作为不相等condition，
  • 当 a_lt == 1,a是正数,则存在carry == 0。a_lt == 0时a是负数，carry=1.所以有约束 1-(a_lt + carry_hi)
  • c_lo = u16 sum(rotation -4)
  • c_hi = u16 sum(rotation -5)
  • a,b符号相等时,我们有(1 -(a_lt - b_lt))作为符号condition，与下面每一个约束相乘
  • a_lo + carrry_lo * 2^128 = b_lo + c_lo
  • a_hi + carry_hi * 2^128 - carry_lo= b_hi + c_hi
  • 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b

• Sdiv_Smod（这里我们还是使用 a*b+c=d 的公式来进行核心约束，值的关注的是对有符号的数进行操作，我们需要运用到补码的知识。） 对有符号整数进行计算时。所有的输入值都由 core circuit 传递。我们在这里约束传递值如下

  if tag is sdiv
  - a = push
  - b = pop2
  - c = if is*pop1_neg{get_neg(pop1_abs - push_abs * pop2*abs)}else{pop1_abs - push_abs * pop2_abs}
  - d = pop1
    if tag is smod
  - a = if is_pop2_zero{0}else if is_pop1_neg == is_pop2_neg {pop1_abs / pop2_abs}else{get_neg(pop1_abs / pop2_abs)}
  - b = pop2
  - c = if pop2.is_zero() { pop1 } else { push }
  - d = pop1

  • a_abs,b_abs,c_abs,d_abs
  • mul_add_words
  • c lt b
  • d is_signed_overflow
  • a,b,c is zero

• Addmod

• Mulmod

• Length arithmetic中的布局:

限制:

    // datasize_lo_16 constraints 
    let expr_datasize = expr_from_u16s([datasize_lo_0,datasize_lo_1,datasize_lo_2,datasize_lo_3]);
    datasize_lo = expr_from_u16s([datasize_lo_0,datasize_lo_1,datasize_lo_2,datasize_lo_3,datasize_lo_4,datasize_lo_5,datasize_lo_6,datasize_lo_7]);
    // length_lo_16 constraints 
    let expr_length = expr_from_u16s([length_lo_0,length_lo_1,length_lo_2,length_lo_3]);
    length_lo = expr_from_u16s([length_lo_0,length_lo_1,length_lo_2,length_lo_3,length_lo_4,length_lo_5,length_lo_6,length_lo_7]);
    // offset_lo_16 constraints 
    let offset_24 = offset_hi *2^64 + expr_from_u16s([offset_lo_4,offset_lo_5,offset_lo_6,offset_7]);
    let is_offset_24_zero = SimpleIsZero(offset_24,offset_24_inv,"");
    offset_overflow = (1-is_offset_24_zero)
    let expr_offset = expr_from_u16s([offset_lo_0,offset_lo_1,offset_lo_2,offset_lo_3]);
    if offset_overflow {
        expr_offset = 0xffffffffffffffff;
    }else{
        offset_lo = expr_offset;
    } 
    // 
    let datasize_gt_offset, datasize_minus_offset = expr_datasize - expr_offset;
    // datasize_minus_offset = datasize_gt_offset * 2^64 + expr_datasize - expr_offset;
    if !datasize_gt_offset {
        real_length = 0;
        zero_length = expr_length;
    }else{
    let length_gt_datasize-minus-offset , length_minus_datasize-minus-offset  = expr_length - datasize_minus_offset;
    // length_minus_datasize-minus-offset = length_gt_datasize-minus-offset * 2^64 + expr_length - datasize_minus_offset ;
    if !length_gt_datasize-minus-offset {
        real_length = expr_length;
        zero_length = 0;
    }else {
        real_length = datasize_minus_offset;
        zero_length = length_minus_datasize-minus-offset
    }
}
      

输入：length,offset,data_size
输出：real_length, zero_length

实现 arithmetic 子电路中 Add 例子

如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示

pub(crate) trait OperationGadget<F: Field> {
    const NAME: &'static str;
    const TAG: Tag;
    const NUM_ROW: usize;

    fn constraints(
        config: &OperationConfig<F>,
        meta: &mut VirtualCells<F>,
    ) -> Vec<(&'static str, Expression<F>)>;
}

接口实现见代码，路径 zkevm-circuits/src/arithmetic_circuit/operation