布局

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

• Add（在表中使用两行）

  • 如果是 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_Lt_Gt (a+b=c+overflow*2^256) (可以使用 select struct)

  • 如果是 0 行，则 cnt_prev=1,cnt_prev_prev=0
  • 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
  • if tag is sub 有 c_lo = u16 sum(rotation cur),c_hi = u16 sum(rotation prev) and carry_hi iszero
  • if tag is lt 则有 carry_hi iszero
  • if tag is gt 则有 carry_hi 1

• Div_Mod

• Mul

• Slt_Sgt

• Sdiv_Smod

• Addmod

• Mulmod

实现 arithmetic 子电路中 Add 例子

如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget，然后在 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>)>;
}

impl<F: Field> OperationGadget<F> for AddGadget<F> {
    const NAME: &'static str = "Arithmetic Circuit Add";
    const TAG: Tag = Tag::Add;
    const NUM_ROW: usize = 2;

    fn constraints(
        config: &OperationConfig<F>,
        meta: &mut VirtualCells<F>,
    ) -> Vec<(&'static str, Expression<F>)> {
        let mut constraints = vec![];
        let a_hi = meta.query_advice(config.operand0_hi, Rotation::cur());
        ...
        let carry_lo = meta.query_advice(config.operand3_lo, Rotation::cur());
        let u16_0_for_c_lo = meta.query_advice(config.u16_0, Rotation::cur());
        ...
        let u16_7_for_c_lo = meta.query_advice(config.u16_7, Rotation::cur());
        let u16_sum_for_c_lo = expr_from_u16s(&[
            u16_0_for_c_lo,
            ...
            u16_7_for_c_lo,
        ]);
        let u16_0_for_c_hi = meta.query_advice(config.u16_0, Rotation::prev());
        ...
        let u16_7_for_c_hi = meta.query_advice(config.u16_7, Rotation::prev());
        let u16_sum_for_c_hi = expr_from_u16s(&[
            u16_0_for_c_hi,
            ...
            u16_7_for_c_hi,
        ]);
        constraints.push(("c lo = u16 sum", c_lo.clone() - u16_sum_for_c_lo));
        constraints.push(("c hi = u16 sum", c_hi.clone() - u16_sum_for_c_hi));
        constraints.push((
            "carry hi is bool",
            carry_hi.clone() * (1.expr() - carry_hi.clone()),
        ));
        constraints.push((
            "carry lo is bool",
            carry_lo.clone() * (1.expr() - carry_lo.clone()),
        ));
        constraints.push((
            "c lo + carry lo * 2^128 = a lo + b lo",
            c_lo + carry_lo.clone() * pow_of_two::<F>(128) - a_lo - b_lo,
        ));
        constraints.push((
            "c hi + carry hi * 2^128 = a hi + b hi + carry lo",
            c_hi + carry_hi * pow_of_two::<F>(128) - a_hi - b_hi - carry_lo,
        ));
        constraints
    }
}