This is an old version of this page. You can view the most recent version or browse the history.

8 arithmetic

布局

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

pub struct ArithmeticCircuitConfig<F> {
    // TODO use table to let core lookup
    q_enable: Selector,
    // arithmetic table for lookup starts
    tag: BinaryNumberConfig<Tag, 3>, //todo not use 3
    cnt: Column<Advice>,
    operand0_hi: Column<Advice>,
    operand0_lo: Column<Advice>,
    operand1_hi: Column<Advice>,
    operand1_lo: Column<Advice>,
    operand2_hi: Column<Advice>,
    operand2_lo: Column<Advice>,
    operand3_hi: Column<Advice>,
    operand3_lo: Column<Advice>,
    // arithmetic table for lookup ends
    u16_0: Column<Advice>,
    u16_1: Column<Advice>,
    u16_2: Column<Advice>,
    u16_3: Column<Advice>,
    u16_4: Column<Advice>,
    u16_5: Column<Advice>,
    u16_6: Column<Advice>,
    u16_7: Column<Advice>,
    cnt_is_zero: IsZeroWithRotationConfig<F>,
}

pub enum Tag {
    #[default]
    Nil,
    Add,
    Addmod,
    Mul,
    Mulmod,
    Lt,
    Gt,
    Slt,
    Sgt,
    Sub,
    DivMod,
}

在这里 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
AddWith1stConfined (含义：a+b=c+overflow*2^256，且a的hi lo被约束为8个16bit之和) (可以使用 select struct)
- 注：减法，LT，GT都可以用这个
- a_lo = u16 sum(rotation cur)
- a_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
- 注意：carry_hi=1 等价于 b>c; carry_hi=0 等价于 b<=c
Div_Mod (a*b+c=d 同时约束 c 小于 b)

  - define t_lo=operand3_0*operand1_0+(operand3_0*operand1_1+operand3_1*operand1_0)*2^64
  - define t_hi=(operand3_0*operand1_2+operand3_1*operand1_1+operand3_2*operand1_0)+(operand3_0*operand1_3+operand3_1*operand1_2+operand3_2*operand1_1+operand3_3*operand1_0)*2^64
  - 如果是 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+operand2_3+operand2_2*2^64-car_lo*2^128) - (operand0_3+operand0_2\*2^64)
  - (t_hi+operand2_0+operand2_1*2^64+car_lo-car_hi*2^128) - (operand0_1+operand0_0\*2^64)
  - 约束 c lt d

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

  - define t_lo=operand0_0*operand1_0+(operand0_0*operand1_1+operand0_1*operand1_0)*2^64
  - define t_hi=(operand0_0*operand1_2+operand0_1*operand1_1+operand0_2*operand1_0)+(operand0_0*operand1_3+operand0_1*operand1_2+operand0_2*operand1_1+operand0_3*operand1_0)*2^64
  - 如果是 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） -（operand2_3+operand2_2*2^64）
  - （t_hi+car_lo-car_hi*2^128）- （operand2_1+operand2_0*2^64）

Slt_Sgt (以下操作待写)
Sdiv_Smod
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