布局

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 对应的约束不同

• AddWith3rdConfined (含义：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，且 a 的 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 等价于 b>c; carry_hi=0 等价于 b<=c

• Div_Mod (a*b+c=d 同时约束 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 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 8,并且约束 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
  • overflow == 0 for opcode DIV/MOD overflow = carry*hi + a1 * b3 + a2 _ b2 + a3 _ b1 + a2 _ b3 + a3 _ b2 + a3 _ b3
  • if tag is div 约束 a - a * (1.expr() - divisor_is_zero.expr()) a 是 core gadget push value
  • is tag is mod 约束 c - c * (1.expr() - divisor_is_zero.expr()) c 是 core gadget push value

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

  • 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 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)
  • （t_lo-car_lo*2^128） -（c_lo）
  • （t_hi+car_lo-car_hi*2^128）- （c_hi）

• Slt_Sgt (以下操作待写)

• 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

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

实现 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