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> {
    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+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
- 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
carry_hi == 0

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 (我们使用 a-b=c 的公式来约束有相同符号的内容)
- 比较最高u16位确定a,b符号。同时我们需要约束a_hi和b_hi等于对应的u16s_sum
- 不相等时。(a_lt - b_lt)作为不相等condition，
- 当 a_lt == 1 时 carry == 0。a_lt == 0时，carry=1.所以有约束 1-(a_lt + carry_hi)
- c_lo = u16 sum(rotation -4)
- c_hi = u16 sum(rotation -5)
- 相等时（1 -(a_lt - b_lt)）作为符号condition，与下面每一个约束相乘
- a,b 为正，统一condition （a_lt * b_lt）表示如果a_lt,b_lt都等于0,则不约束下面约束
- a_lo + carrry_lo * 2^128 = b_lo + c_lo
- a_hi + carry_hi * 2^128 - carry_lo= b_hi + c_hi
- a,b 为负，统一condition 1 - （a_lt * b_lt）表示如果a_lt,b_lt都等于1,则不约束下面约束
- b_lo + carrry_lo * 2^128 = a_lo + c_lo
- b_hi + carry_hi * 2^128 - carry_lo= a_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中的布局:

tag	cnt	operand_0_hi	operand_0_lo	operand_1_hi	operand_1_lo
Length	1	length	offset	data_size	0
Length	0	normal_length	zero_length	0	0

输入：length,offset,data_size
输出：normal_length, zero_length
计算方式：
以codecopy为例，length:为要copy的长度，offset为bytecode偏移量(即复制起始位置)，data_size为bytecode的总长度

fn length(length: u64, offset: u64, data_size: u64) -> (normal_length: u64, zero_length: u64) {
    if offset > data_size {
        return 0, length
    } else if offset + length < data_size {
        return length,0
    }else{
        return data_size-offset, offset+length-data_size
    }
}

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