# Arithmetic

## 1 布局

`arithmetic` 子电路用于执行基本的数学运算，如加法、减法、乘法、除法等。`arithmetic` 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，

```rust
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,
    Length,
    memory_expansion,
}
```

在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见[here](../code-notes/binary_number_with_real_selector)。

### 列的含义

**operand***: 存放算术操作中的输入参数，如 `a+b=c+overflow` 指令中的 `a,b,c,overflow`。

**u16***: 用于查找算术运算的输出值，特别是对大数值的低16位和高16位的处理（如 `c_hi`、`c_lo`）。通常在大数运算中，将结果拆分为多个 16-bit 部分进行处理。

**cnt**: 记录某个具体算术指令的行计数器，从正数递减到0。

## 2 约束

在设计 `arithmetic` 子电路时，约束可以分为两类：

- **通用约束**:
  - 约束 `cnt` 除零行外，当前行与下一行的差值为1。这确保了行计数器的正确递减。
- **不同 Tag 对应的约束**:
  - 不同的操作（如加法、减法、乘法等）有不同的约束规则。这些规则确保了运算的正确性和结果的准确性。

## 3 运算子电路

### 3.1 Add 

#### 公式

a + b = c + overflow * 2^256`，且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit的和。

**约束**:

- `c_lo = u16 sum(rotation cur)`：当前行的低16位和。
- `c_hi = u16 sum(rotation prev)`：前一行的高16位和。
- `carry_hi` 和 `carry_lo` 为布尔值，用于表示进位。
- `c_lo + carry_lo * 2^128 = a_lo + b_lo`。
- `c_hi + carry_hi * 2^128 = a_hi + b_hi + carry_lo`。

#### layout

| cnt | op_0_hi | op_0_lo | op_1_hi  | op_1_lo  | u16s      |
| --- | ------- | ------- | -------- | -------- | --------- |
| 1   | c_hi    | c_lo    | carry_hi | carry_lo | c_lo_u16s |
| 0   | a_hi    | a_lo    | b_hi     | b_lo     | c_hi_u16s |

### 3.2 Sub

#### 公式

 `a - b = c`，且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit的和。

**约束：**

- `c_lo = u16 sum(rotation cur)`。
- `c_hi = u16 sum(rotation prev)`。
- `carry_hi` 和 `carry_lo` 为布尔值。
- `a_lo + carry_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`

#### layout

| cnt | op_0_hi | op_0_lo | op_1_hi  | op_1_lo  | u16s      |
| --- | ------- | ------- | -------- | -------- | --------- |
| 1   | c_hi    | c_lo    | carry_hi | carry_lo | c_lo_u16s |
| 0   | a_hi    | a_lo    | b_hi     | b_lo     | c_hi_u16s |

### 3.3 Div_Mod

#### 公式

`(a - d) / b = c`，即 `c * b + d = a`，同时约束 `d < b`。

```
if tag is div, (a,b,c,d) = (pop1,pop2,push,pop1 - push * pop2) 
if tag is mod, (a,b,c,d) = (pop1 ,pop2 , if pop2 is zero{zero}else{pop1 / pop2} ,if pop2 is zero{pop1}else{push})

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)。`
- `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 - carry_lo \* 2^128) - d_lo`，确保 `c` 的低16位加上 `t_lo` 和 `carry_lo` 乘以 2^128，减去 `d_lo`，结果与 `t_lo` 相匹配。`carry_lo` 用于调整进位。
- `(t_hi + c_hi + carry_lo - carry_hi \* 2^128) - d_hi`，确保 `c` 的高16位加上 `t_hi` 和 `carry_lo`，减去 `carry_hi` 乘以 2^128，结果与 `d_hi` 相匹配。`carry_hi` 用于调整进位。
- `residue < divisor when divisor != 0`确保 `d` 在除法过程中小于 `b`（当 `b` 不为0时），表示 `d` 是正确的余数。
- `carry_hi == 0`。
- `carry_lo == u16 sum(rotation -7)`确保了 `carry_lo` 的值正确。


#### layout

| tag    | cnt | o0hi  | o0lo  | o1hi | o1lo | u16s                |
| ------ | --- | ----- | ----- | ---- | ---- | ------------------- |
| DivMod | 8   |       |       |      |      | carry_lo_u16s       |
| DivMod | 7   |       |       |      |      | u16_sum_for_diff_lo |
| DivMod | 6   | diff  | diff  | lt   | lt   | u16_sum_for_diff_hi |
| DivMod | 5   |       |       |      |      | u16_sum_for_d_lo    |
| DivMod | 4   |       |       |      |      | u16_sum_for_d_hi    |
| DivMod | 3   |       |       |      |      | u16_sum_for_c_lo    |
| DivMod | 2   | carry | carry |      |      | u16_sum_for_c_hi    |
| DivMod | 1   | c     | c     | d    | d    | u16_sum_for_b_lo    |
| DivMod | 0   | a     | a     | b    | b    | u16_sum_for_b_hi    |

### 3.4 Mul

#### 公式

在 `Mul`（乘法）子电路中，我们涉及到的公式和约束是用来确保乘法结果的正确性的。这里详细解释一下每个公式和约束：

1. **定义乘法操作**
   - **`t0 = a0 \* b0`**
     计算 `a` 和 `b` 的最低16位的乘积，这个结果的位数在0到128位之间。
   - **`t1 = a0 \* b1 + a1 \* b0`**
     计算 `a` 和 `b` 的其他16位的乘积加上最低16位的乘积，这个结果的位数在64到193位之间。
   - **`t2 = a0 \* b2 + a2 \* b0 + a1 \* b1`**
     计算 `a` 和 `b` 的更高16位的乘积加上前两步的结果，这个结果的位数在128到257位之间。
   - **`t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2`**
     计算 `a` 和 `b` 的最高16位的乘积加上前面步骤的结果，这个结果的位数在192到322位之间。
   - **`t_lo = t0 + (t1 << 64)`**
     计算乘法结果的低128位，其中 `t1` 左移64位后加到 `t0` 上。
   - **`t_hi = t2 + (t3 << 64)`**
     计算乘法结果的高128位，其中 `t3` 左移64位后加到 `t2` 上。
2. **进位计算**
   - **`carry_lo = (t0 + (t1 << 64) - c_lo) >> 128`**
     计算低128位的进位，将 `t0` 和 `t1` 左移64位后的和减去 `c_lo`，右移128位得到 `carry_lo`。
   - **`carry_hi = (t2 + (t3 << 64) + carry_lo - c_hi) >> 128`**
     计算高128位的进位，将 `t2` 和 `t3` 左移64位后的和加上 `carry_lo`，减去 `c_hi`，右移128位得到 `carry_hi`。
3. **约束**
   - **`a_lo = u16 sum(rotation cur)`**
     `a` 的低16位在当前行的位置。
   - **`a_hi = u16 sum(rotation -1)`**
     `a` 的高16位在当前行的位置。
   - **`b_lo = u16 sum(rotation -2)`**
     `b` 的低16位在当前行的位置。
   - **`b_hi = u16 sum(rotation -3)`**
     `b` 的高16位在当前行的位置。
   - **`c_lo = u16 sum(rotation -4)`**
     `c` 的低16位在当前行的位置。
   - **`c_hi = u16 sum(rotation -5)`**
     `c` 的高16位在当前行的位置。
   - **`carry_hi == u16 sum(rotation -6)`**
     这里 `carry_hi` 的值应等于322 - 256 = 66位的 `u16` 数据的和。
   - **`carry_lo == u16 sum(rotation -7)`**
     这里 `carry_lo` 的值应等于193 - 128 = 65位的 `u16` 数据的和。
   - **`(t_lo - carry_lo \* 2^128) - c_lo`**
     确保乘法结果 `t_lo` 和 `c_lo` 的差与 `carry_lo` 乘以2^128的结果相匹配。
   - **`(t_hi + carry_lo - carry_hi \* 2^128) - c_hi`**
     确保乘法结果 `t_hi` 和 `c_hi` 的差与 `carry_hi` 乘以2^128的结果相匹配。

#### layout

| cnt | op_0_hi | op_0_lo | op_1_hi  | op_1_lo  | u16s          |
| --- | ------- | ------- | -------- | -------- | ------------- |
| 7   |         |         |          |          | carry_lo_u16s |
| 6   |         |         |          |          | carry_hi_u16s |
| 5   |         |         |          |          | c_lo_u16s     |
| 4   |         |         |          |          | c_hi_u16s     |
| 3   |         |         |          |          | b_lo_u16s     |
| 2   |         |         |          |          | b_hi_u16s     |
| 1   | c_hi    | c_lo    | carry_hi | carry_lo | a_lo_u16s     |
| 0   | a_hi    | a_lo    | b_hi     | b_lo     | a_hi_u16s     |

### 3.5 SLT_SGT

#### 公式

在 `SLT_SGT`（有符号比较）子电路中，我们处理有符号数的比较，通过补码表示和无符号整数比较来实现。

**符号判断**

- **`比较a_hi,b_hi最高u16位是否小于2^15`**
  通过检查最高16位来判断 `a` 和 `b` 的符号。如果 `a_lt == 1` 则 `a` 为正数，否则为负数。`b_lt` 同理。

**符号一致性约束**

- **`a_hi 和 b_hi 等于对应的 u16s_sum`**
  确保 `a` 和 `b` 的高16位在当前行的位置。
- **`a,b 符号不相等时`**
  当 `a` 和 `b` 符号不相同时，约束 `(a_lt - b_lt)` 作为不相等条件。
- **`a_lt == 1` 和 `carry == 0`**
  如果 `a_lt == 1`（`a` 为正数），则 `carry` 应为0；如果 `a_lt == 0`（`a` 为负数），则 `carry` 应为1。因此有约束 `1 - (a_lt + carry_hi)`。
- **`c_lo = u16 sum(rotation -4)`**
  `c` 的低16位在当前行的位置。
- **`c_hi = u16 sum(rotation -5)`**
  `c` 的高16位在当前行的位置。
- **`a,b 符号相等时`**
  当 `a` 和 `b` 符号相同时，约束 `(1 - (a_lt - b_lt))` 作为符号条件，与后续约束相乘。
- **`a_lo + carry_lo \* 2^128 = b_lo + c_lo`**
  确保 `a` 的低16位加上进位与 `b` 的低16位加上 `c` 的低16位匹配。
- **`a_hi + carry_hi \* 2^128 - carry_lo = b_hi + c_hi`**
  确保 `a` 的高16位加上进位减去 `carry_lo` 与 `b` 的高16位加上 `c` 的高16位匹配。
- **`carry_hi = 1` 等价于 `a < b`**
  `carry_hi = 1` 表示 `a` 小于 `b`；`carry_hi = 0` 表示 `a` 大于或等于 `b`。

#### layout

| cnt | o0hi | o0lo | o1hi  | o1lo  | u16s0            | u16s1 | u16s2     | u16s3     |
| --- | ---- | ---- | ----- | ----- | ---------------- | ----- | --------- | --------- |
| 4   |      |      |       |       | u16_sum_for_b_hi |       |           |           |
| 3   |      |      |       |       | u16_sum_for_a_hi |       |           |           |
| 2   |      |      |       |       | a_lt             | b_lt  | a_lt_diff | b_lt_diff |
| 1   | c    | c    | carry | carry | u16_sum_for_c_lo |       |           |           |
| 0   | a    | a    | b     | b     | u16_sum_for_c_hi |       |           |           |

### 3.6 Sdiv_Smod

在 `Sdiv_Smod`（有符号除法和取余）中，我们处理有符号整数的除法和取余，以下是核心约束：

**1 补码表示**

- **计算 `a` 和 `b` 的补码**
  使用补码表示法将负整数表示为其正值的按位取反加1。正整数的补码表示与其无符号表示相同。

**2 无符号整数除法和取余**

- **使用 DIV 和 MOD 操作码**
  执行无符号整数的除法和取余，得到正确的结果因为在第一步中我们已将有符号整数转换为无符号整数。

**3 调整结果**

- **当 `a` 和 `b` 一正一负**
  需要对计算结果进行取反处理 `-x mod 2^256`。
- **当 `a` 为负数，`b` 为正数时**
  只有被除数（`a`）是负数时，结果需要进行取反处理。

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

2. 补码的相关约束如下(开发时我们需要实现a,b,c,d的下述约束)
- 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的值与被除数的符号相同
  - (1.expr() - quotient_is_zero.expr())
            * (1.expr() - divisor_is_zero.expr())
            * (1.expr() - remainder_is_zero.expr())
            * (dividend_original.is_neg().expr() - remainder_original.is_neg().expr())
            
  quotient_original.is_neg().expr() + divisor_original.is_neg().expr() (如果被除数的补码也是负数，与余数和除数等于零，则排除约束情况) 这里说到的符号都是非补码的符号
     这里计算的都是div情况下的变化
  - (
    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()
    )
    *(1.expr() - quotient_is_zero.expr())
    * (1.expr() - divisor_is_zero.expr())
    * (1.expr() - dividend_is_signed_overflow.expr()) //**dividend_is_signed_overflow是指被除数补码是否为负数,这里需要判断的原因是剔除特殊情况**
  note: 对于一个特殊的SDIV情况，当输入dividend = -(1 << 255) 和 divisor = -1时，商的结果应该是1 << 255。但是一个有符号字（signed word）只能表示从-(1 << 255)到
  (1 << 255) - 1的有符号值。因此，对于这种情况，约束条件sign(dividend) == sign(divisor) ^ sign(quotient)不能应用。
  
5. 取余结果值约束
为了保证mul乘法的有效当b==0时，我们设置d==a.(d是余数,b是除数)。但是在eth中计算取余时有b==0时，我们设置d==0.所以在core circuit部分我们需要增加b=0时d==0
  ```

####  Layout

(因为a,b 都是输入不需要进行范围约束，但是因为我们需要判断a,b的符号，所以只需要对a_hi,b_hi进行范围约束。因为c,d 属于非输入值，并且我们要计算c + c_com = 1<<256。
所以我们需要对c,d进行范围约束)
其中u_16 具有8列，这里为了表现清晰，我们做了简便处理。

| hi                     | lo             | hi             | lo             | cnt | u16_0          | u16_1  | u16_2  | u16_3  | u16_4      |
| ---------------------- | -------------- | -------------- | -------------- | --- | -------------- | ------ | ------ | ------ | ---------- |
|                        |                |                |                | 17  | d_lo_0         |        |        |        |            |
|                        |                |                |                | 16  | d_hi_0         |        |        |        |            |
|                        |                |                |                | 15  | c_lo_0         |        |        |        |            |
| a_com_lt               |                |                |                | 14  | c_hi_0         |        |        |        |            |
| c_sum_carry_hi         | c_sum_carry_lo | d_sum_carry_hi | d_sum_carry_lo | 13  | b_hi_0         |        |        |        |            |
| a_sum_carry_hi         | a_sum_carry_lo | b_sum_carry_hi | b_sum_carry_lo | 12  | a_hi_0         |        |        |        |            |
| a_lt_carry_hi          | b_lt_carry_hi  | c_lt_carry_hi  | d_lt_carry_hi  | 11  | a_diff         | b_diff | c_diff | d_diff | a_com_diff |
|                        |                |                |                | 10  | cb_diff_lo_0   |        |        |        |            |
| cb_diff_hi(cb 指c < b) | cb_diff_lo     | cb_carry_hi    |                | 9   | cb_diff_hi_0   |        |        |        |            |
| mul_carry_hi           | mul_carry_lo   |                |                | 8   | mul_carry_lo_0 |        |        |        |            |
|                        |                |                |                | 7   | d_com_lo_0     |        |        |        |            |
|                        |                |                |                | 6   | d_com_hi_0     |        |        |        |            |
|                        |                |                |                | 5   | c_com_lo_0     |        |        |        |            |
|                        |                |                |                | 4   | c_com_hi_0     |        |        |        |            |
| c_com_hi               | c_com_lo       | d_com_hi       | d_com_lo       | 3   | b_com_lo_0     |        |        |        |            |
| a_com_hi               | a_com_lo       | b_com_hi       | b_com_lo       | 2   | b_com_hi_0     |        |        |        |            |
| c_hi                   | c_lo           | d_hi           | d_lo           | 1   | a_com_lo_0     |        |        |        |            |
| a_hi                   | a_lo           | b_hi           | d_lo           | 0   | a_com_hi_0     |        |        |        |            |

### 3.7 AddMod

#### 公式

#### 核心公式：

输入a,b,n 计算：

a + b mod n = r （式1）

可以将算式转换为：
a + b   = n * q + r （式2）

其中 `q` 是商，并没有实际出现在EVM的运算中，`r` 是余数。`q` 可能会超出 256 位，`r` 必须小于 `n`。

**处理溢出**:

- 如果 `q` 超出 256 位，则需要一个额外的 1 位来处理溢出。
- 如果 `n` 为 0，`r` 必须设置为 `a + b`，因为 `n` 为 0 时，`a + b` 应直接作为结果 `r`。

**约束**:

- `r < n`
- `r` 是结果的低位部分。
- `q` 的最大值为 256 位 + 1 位 carry 位（如果有溢出）。
- `n`最大值为2256-1, `q`的最大值为2256-1，`r`的最大值为2256-2，那`么n*q+r`的最大值为：2512-2256-3。关键在于约束`q`的最大值为2256-1（q_overflow = 0 or 1）
- `r` 必须小于 `n`，否则需要调整 `q` 的溢出处理。
- 当 `n = 0` 时，`r` 设置为 `a + b`，并且 `n` 处理为 0，以避免 `r` 超过 256 位。这时候式子2不能成立，这里直接让r=0（可以避免r超过256bit），使用n=0 判断式作为selector。


#### layout

| operand0          | operand1          | operand2    | operand3    | cnt | u16s        |
| ----------------- | ----------------- | ----------- | ----------- | --- | ----------- |
|                   |                   |             |             | 11  | rn_diff_lo  |
|                   |                   |             |             | 10  | rn_diff_hi  |
|                   |                   |             |             | 9   | carry_1     |
|                   |                   |             |             | 8   | carry_0     |
|                   |                   |             |             | 7   | a_plus_b_lo |
|                   |                   |             |             | 6   | a_plus_b_hi |
| a_plus_b_lo_carry | a_plus_b_hi_carry |             |             | 5   | q_lo        |
| carry_0           | carry_1           | q_overflow  |             | 4   | q_hi        |
| q_hi              | q_lo              | a_plus_b_hi | a_plus_b_lo | 3   | n_lo        |
| rn_carry_lt_hi    | rn_carry_lt_lo    | rn_diff_hi  | rn_diff_lo  | 2   | n_hi        |
| n_hi              | n_lo              | r_hi        | r_lo        | 1   | r_lo        |
| a_hi              | a_lo              | b_hi        | b_lo        | 0   | r_hi        |


### 3.8 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`约束；

#### layout

| cnt | o_0_hi              | o_0_lo              | o_1_hi         | o_1_lo         | u16s_0                   |
| --- | ------------------- | ------------------- | -------------- | -------------- | ------------------------ |
| 26  |                     |                     |                |                | k2n_carry_0              |
| 25  |                     |                     |                |                | k2n_carry_1              |
| 24  |                     |                     |                |                | k2n_carry_2              |
| 23  |                     |                     |                |                | r_lo_u16s                |
| 22  |                     |                     |                |                | r_hi_u16s                |
| 21  |                     |                     |                |                | k2_lo_u16s               |
| 20  |                     | k2n_carry_2         | k2n_carry_1    | k2n_carry_0    | k2_hi_u16s               |
| 19  | r_diff_hi           | r_diff_lo           | r_lt_hi        | r_lt_lo        | r_diff_lo_u16s           |
| 18  | k2_hi               | k2_lo               |                |                | r_diff_hi_u16s           |
| 17  |                     |                     |                |                | arb_carry_0              |
| 16  |                     |                     |                |                | arb_carry_1              |
| 15  |                     |                     |                |                | arb_carry_2              |
| 14  |                     |                     |                |                | d_lo_u16s                |
| 13  |                     |                     |                |                | d_hi_u16s                |
| 12  |                     |                     |                |                | e_lo_u16s                |
| 11  |                     |                     |                |                | e_hi_u16s                |
| 10  |                     | arb_carry_2         | arb_carry_1    | arb_carry_0    | b_lo_u16s                |
| 9   | e_hi                | e_lo                | d_hi           | d_lo           | b_hi_u16s                |
| 8   |                     |                     |                |                | a_remainder_diff_lo_u16s |
| 7   |                     |                     |                |                | a_remainder_diff_hi_u16s |
| 6   |                     |                     |                |                | a_rem_carry_lo_u16s      |
| 5   |                     |                     |                |                | a_remainder_lo_u16s      |
| 4   | a_remainder_diff_hi | a_remainder_diff_lo | a_rem_lt_hi    | a_rem_lt_lo    | a_remainder_hi_u16s      |
| 3   | k1_carry_hi         | k1_carry_lo         |                |                | n_lo_u16s                |
| 2   | k1_hi               | k1_lo               | a_remainder_hi | a_remainder_lo | n_hi_u16s                |
| 1   | n_hi                | n_lo                | r_hi           | r_lo           | k1_lo_u16s               |
| 0   | a_hi                | a_lo                | b_hi           | b_lo           | k1_hi_u16s               |

### 3.9 Length 

#### length  电路功能：

输入参数：

- `offset`：偏移量
- `length`：长度
- `size`：总大小

返回值：

- `real_len`：实际长度
- `zero_len`：超出长度
- `overflow`：是否溢出
- `_real_len_is_zero`：实际长度是否为零
- `_zero_len_is_zero`：超出长度是否为零（待定）

约束条件：

- `offset`、`length`、`size`需要符合 `u64_overflow` 约束。

逻辑判断：

- 如果 `offset + length <= size`，返回 `(length, 0)`。

- 如果 `offset + length > size`，分为两种情况：
  - 如果 `offset < size`，返回 `(size - offset, offset + length - size)`。
  - 如果 `offset >= size`，返回 `(0, length)`。

#### arithmetic中的布局: 


| operand0     | operand1     | operand2         | operand3         | cnt | u16s(0-3) | u16s(4_7)        |
| ------------ | ------------ | ---------------- | ---------------- | --- | --------- | ---------------- |
| real_len_inv | zero_len_inv | lt_offset_size   |                  | 2   | diff      | diff_offset_size |
| real_len     | zero_len     | real_len_is_zero | zero_len_is_zero | 1   | size      | offset_bound     |
| offset       | length       | size             | overflow         | 0   | offset    | length           |

#### 约束

**operand 和 u16s 大小相等**

- `offset`, `length`, `size`
- `offset_bound = offset + length`

**约束 size 是否小于 offset_bound**

- 使用 `SimpleLtGadget::new(size, offset_bound, overflow, diff)`，`range` 设置为 2^64
- `overflow` 为布尔值

**约束 offset 是否小于 size**

- 使用 `SimpleLtGadget::new(offset, size, lt_offset_size, diff_offset_size)`，`range` 设置为 2^64
- `lt_offset_size` 为布尔值

**三种情况下 (real_len, zero_len) 的约束**

- 使用 `overflow` 和 `lt_offset_size` 作为 `selector`，公式如下：

​	`real_len = (1 - overflow) * length + overflow * lt_offset_size * (size - offset)`

​	`zero_len = overflow * lt_offset_size * (offset_bound - size) + overflow * (1 - lt_offset_size) * length`

**约束 real_len_is_zero 和 zero_len_is_zero**

- 使用 `SimpleIsZero(real_len, real_len_inv)`
- 使用 `SimpleIsZero(zero_len, zero_len_inv)`

### 3.10 memory expansion

memory expansion 电路的功能是给定offset\_bound，计算是否需要拓展内存。

offset\_bound 的代表的是访问内存段的**右区间**：

1.  访问长度length是固定的，比如 mload 指令, offset = 10，mload 一次访问 length=32，那么offset\_bound = 42.
    
2.  另外还存在另一种情况，访问内存时，给定了 offset， length 是任意值：当length 不为0，那么 offset\_bound = offset + length。当length = 0，offset\_bound = 0，所以这时候无论offset取什么值，内存都不会拓展。
    

#### 电路设计

| operand0      | operand1            | operand2       | operand3             | cnt | u16s(0-3)     | u16s(4\_7)           |
| ------------- | ------------------- | -------------- | -------------------- | --- | ------------- | -------------------- |
| r0            |                     |                |                      | 1   | diff          | r1\|r2\|r3\|r4       |
| offset\_bound | memory\_chunk\_prev | expansion\_tag | access\_memory\_size | 0   | offset\_bound | access\_memory\_size |

#### 约束设计：

:::
**约束 operand 和 u16s** 
:::

*   offset\_bound  = offset\_bound
    
*   access\_memory\_size = access\_memory\_size
    
*    SimpleBinaryNumber::new（ ++r0|r1|r2|r3|r4++ ）.value  = remainder 


:::
**约束** access_memory_size = \lfloor (offset + 31) / 32  \rfloor
:::

*   access\_memory\_size \* 32 + remainder = offset + 31
    

:::
**约束** memory_chunk_cur = Max( memory_chunk_prev， access_memory_size)
:::

*   约束 expansion\_tag 是 0 或 1
    
*   使用 SimpleLtGadget::new(memory\_chunk\_prev, access\_memory\_size, expansion\_tag, diff)，range 设置为2^64
    

#### 有length 的时候如何约束offset\_bound

添加加一个 length\_inv _(大部分电路里面已经有了)_

因为如果length= 0，offset\_bound = 0; 

否则 offset\_bound = （offset + length）

那么公式为：

**offset\_bound = (offset + length) \* length \* length\_inv**

### 3.11 U64Overflow

#### 公式

w=a_hi×2^64+a_lo

`a_hi` 和 `a_lo`：分别是 64 位的高位和低位部分。

`w`：是 `a_lo` 的前 64 位与 `a_hi` 左移 64 位的结果。

`w_inv`：`w` 的逆元素，用于处理 overflow 检测。

**约束**

- 检测 `w` 是否发生了溢出，需要使用 `w` 和 `w_inv` 的 `simple is zero` 约束来实现。

- `w` 的溢出与否通过 `w \times w_inv` 判断，若为 0，则表示没有溢出，为 1 则表示发生了溢出。

#### layout

| cnt | op_0_hi | op_0_lo | op_1_hi | op_1_lo | u16s      |
| --- | ------- | ------- | ------- | ------- | --------- |
| 0   | a_hi    | a_lo    | w       | w_inv   | a_lo_u16s |

## 4 实现 arithmetic 子电路中 Add 例子

如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示

```rust
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`