布局

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 = d + c ==> d * b + c = a 同时约束 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 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*b+c=d 的公式来进行核心约束，值的关注的是对有符号的数进行操作，我们需要运用到补码的知识。

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

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

关于补码的相关约束如下
- 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

• mul_add_words (请参考mul部分约束内容)
• abs(remainder) < abs(divisor) when divisor != 0
• mul_add_words中的carry_hi == 0
• sign(dividend) == sign(remainder) when quotient, divisor and remainder are all non-zero。 这里主要是有mod的值与被除数的符号相同
• quotient_abs_word.is_neg().expr() + divisor_abs_word.is_neg().expr() (如果被除数的补码也是负数，与余数和除数等于零，则排除约束情况) 这里说到的符号都是非补码的符号
  • dividend_abs_word.is_neg().expr()
  • 2.expr()
  • quotient_abs_word.is_neg().expr()
  • divisor_abs_word.is_neg().expr(), 这里计算的都是div情况下的变化

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