布局

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-d)/b = c ==> c * b + d = a 同时约束 d 小于 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
a * b + c = d
- 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 自增的有效性
• b_lo = u16 sum(rotation -2) //请注意因为a是输入值，我们可以不对a_hi,a_lo进行range约束
• 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

需要8行对 a,b,d,carry lookup,carry lookup的原因是在进行计算时carry_lo或carry需要左移128位，因为有限域的特点可能存在左移后carry_lo或carry_hi在0-128bit存在值) 其中 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 c_lo is 0
• define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128 c_hi is 0
• 如果是 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-c)*b =d 的公式来进行核心约束，值的关注的是对有符号的数进行乘法操作时，我们需要运用到如下补码的知识。

1. 首先我们统一计算a,b 的补码，补码表示法将一个负整数表示为其正值的按位取反（二进制反码）加 1。正整数的补码表示与其无符号表示相同。
2. 使用 DIV 和 MOD 操作码执行无符号整数除法和取余：将转换后的 U256 数字相除或取余。由于步骤 1 中的转换，这将正确处理有符号整数除法和取余。
3. 在div 中如果我们是一正一负，需要对计算结果再进行Neg计算(-x mod 2**256.)。如果是mod 则只有被除数是负数时，计算结果才需要进行Neg计算。

###核心约束说明

根据上述补码的知识，我们有 b_com*c_com+d_com=a_com. 其中a_com是a的补码，b_com是b的补码，c_com是c的补码，d_com是d的补码.
1. 乘法约束
细节请参考mul模块约束内容

2. 补码的相关约束如下
- x_abs_lo == lo when x >= 0
- x_abs_hi == hi when x >= 0
- sum == 0 when x < 0 （小于0证明存在补码,同时我们有x+x_abs = 1 <<256。x + x_abs 约束请参考add部分）
- carry_hi == 1 when x < 0

3. 范围约束
因为当前算法中使用了mul约束，所以我们需要对mul中的变量进行范围约束。同时也因为判断a,b,c,d正负符号的原因，我们需要对a_hi,b_hi,c_hi,d_hi进行范围约束。
另外因为判断补码有效性的原因，我们需要对a,b,c,d以及他们的补码值进行u128范围约束，因为a,b是输入可以忽略，只需增加对a_hi,b_hi,c_lo,d_lo进行u128范围约束。

4.符号为约束
- sign(dividend_original) == sign(remainder_original) when quotient, divisor and remainder original value are all non-zero。 这里主要约束mod的值与被除数的符号相同
- quotient_original.is_neg().expr() + divisor_original.is_neg().expr() (如果被除数的补码也是负数，与余数和除数等于零，则排除约束情况) 这里说到的符号都是非补码的符号
  - dividend_original.is_neg().expr()
  - 2.expr()
  * quotient_original.is_neg().expr()
  * divisor__original.is_neg().expr(),  这里计算的都是div情况下的变化

5. 取余结果值约束
为了保证mul乘法的有效当b==0时，我们设置d==a.(eg余数=被除数)。但是在eth中计算取余时有b==0时，我们设置d==0.所以在core circuit部分我们需要增加b=0时，d==0

AddMod

计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有(a+b)%n = r。我们可以将这个约束转化为(a+b) = n * q + r。为了约束简单我们可以有 a % n= a_div_n + a_remainder a = n * a_div_n + a_remainder (a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 ) (a_remainder_plus_b + a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r note: 其中a_remainder+b 大于256位. 我们可以有以下约束

/// Construct the gadget that checks a * b + c == d * 2**256 + e
/// where a, b, c, d, e are 256-bit words.
///
/// We execute a multi-limb multiplication as follows:
/// a and b is divided into 4 64-bit limbs, denoted as a0~a3 and b0~b3
/// defined t0, t1, t2, t3, t4, t5, t6:
///   t0 = a0 * b0, // 0 - 128bit
///   t1 = a0 * b1 + a1 * b0, //64 - 193bit 两数相加可能存在进位
///   t2 = a0 * b2 + a2 * b0 + a1 * b1, //128 - 258bit
///   t3 = a0 * b3 + a3 * b0 + a2 * b1 + a1 * b2, //192 - 322bit
///   t4 = a1 * b3 + a2 * b2 + a3 * b1,
///   t5 = a2 * b3 + a3 * b2,
///   t6 = a3 * b3,

/// Finally we just prove: 
///   t0 + t1 * 2^64 + c_lo = e_lo + carry_0 * 2^128 // carry_0 is 65bit
///   t2 + t3 * 2^64 + c_hi + carry_0 = e_hi + carry_1 * 2^128
///   t4 + t5 * 2^64 + carry_1 = d_lo + carry_2 * 2^128
///   t6 + carry_2 = d_hi

• a,n,a_remainder,a_div_n 存在mul_add_words约束 a_div_n * n + a_remainder = a
• b,a_remainder,a_remainder_plus_b 存在add_words约束 a_remainder + b = a_remainder_plus_b + a_remainder_plus_b_overflow << 256
• b_div_n,n,b_remainder,a_reduced_plus_b_overflow 存在mul_add_words约束 b_div_n * n + r = a_remainder_plus_b + a_remainder_plus_b_overflow << 256 （mul_add_512_gadget）
• a_remainder < n 约束
• r < n 约束
• n_is_zero 约束

MulMod

核心公式

基础公式：

• a*b = r (mod n)，其中 a,b,n,r 为 256-bit。

公式拆分：

• a/n = k1 余 a_remainder

• (a_remainder * b) / n = k2 余 r

• a_remainder * b + 0 = e + d * 2^256 -- 看做两数加法

公式转化（除转乘）：

• k1 * n + a_remainder = a
• a_remainder * b + 0 = e + d * 2^256 不变
• k2 * n + r = e + d * 2^256

约束

（注：以公式角度进行约束描述，未忽略上一步已经约束过的变量）

1. 公式1 -- k1 * n + a_remainder = a

• 参考mul操作：
  • k1, n, a_remainder u16s范围约束 128bit；
  • carry_lo u16s[0-5]范围约束 65bit；
  • carry_hi==0 除法转换；
• 除转乘，有 remainder < divisor if divisor != 0，参考减法a_remainder - n = a_remainder_diff - a_remainder_carry << 256：
  • a_remainder_diff范围约束；
  • n != 0约束；

2. 公式2 -- a_remainder * b + 0 = e + d * 2^256

• 参考muladd512方法：
  • a_remainder,b,e,d的u16s约束 128bit；
  • a_rem_mul_b_carry的u16s[0..5]约束，乘法中的进位；

3. 公式3 -- k2 * n + r = e + d * 2^256

• 参考muladd512方法：
  • k2, n , r, e, d的u16s范围约束128bit；
  • k2n_plus_r_carry的u16s[0..5]范围约束；
• 除转乘，r - n = r_diff - r_carry << 256：
  • r, r_diff, n范围约束；
  • n != 0约束；

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