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

首先我们统一计算a,b 的补码，补码表示法将一个负整数表示为其正值的按位取反（二进制反码）加 1。正整数的补码表示与其无符号表示相同。
使用 DIV 和 MOD 操作码执行无符号整数除法和取余：将转换后的 U256 数字相除或取余。由于步骤 1 中的转换，这将正确处理有符号整数除法和取余。
在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 计算mulMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有ab%n = r。我们可以将这个约束转化为ab = n * q + r。为了约束简单我们可以有 a % n= a_div_n + a_remainder -> a = n * a_div_n + a_remainder a_remainder * b =product & n= b_div_n + r product是512bit,我们将它分为两个256bit的数，product_hi,product_lo。我们可以有以下约束
- a,n,a_remainder,a_div_n 存在mul_words约束
- b,a_remainder,product_hi,product_lo 存在mul_add_words约束,请注意这里b*a_remainder的结果等于port是512bit.我们最后有product_hi * 2^256 + product_lo = b * a_remainder
- product_hi,product_lo,n,b_div_n,r 存在mul_add_words约束,同样需要注意这里n * b_div_n + r 的结果等于product是512bit.我们最后有product_hi * 2^256 + product_lo = n * b_div_n + r
- a_remainder < n 约束
- r < n 约束
- n_is_zero 约束
Length arithmetic中的布局:

tag	cnt	operand_0_hi	operand_0_lo	operand_1_hi	operand_1_lo	u16_0	u16_1	u16_2	u16_3	u16_4	u16_5	u16_6	u16_7
Length	3	0	0	0	0	length_minus_datasize-minus-offset_0	length_minus_datasize-minus-offset_1	length_minus_datasize-minus-offset_2	length_minus_datasize-minus-offset_3	datasize_minus_offset_0	datasize_minus_offset_1	datasize_minus_offset_2	datasize_minus_offset_3
Length	2	length_gt_datasize-minus-offset	datasize_gt_offset	offset_24_inv	offset_overflow	offset_lo_0	offset_lo_1	offset_lo_2	offset_lo_3	offset_lo_4	offset_lo_5	offset_lo_6	offset_lo_7
Length	1	offset_hi	offset_lo	real_length	zero_length	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	0	length_hi	length_lo	datasize_hi	datasize_lo	length_lo_0	length_lo_1	length_lo_2	length_lo_3	length_lo_4	length_lo_5	length_lo_6	length_lo_7

限制:

    // 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