zkevm-docs/8-arithmetic.markdown

-# 布局
+# 1 布局
 
-arithmetic 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，
+`arithmetic` 子电路用于执行基本的数学运算，如加法、减法、乘法、除法等。`arithmetic` 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，
 
 ```rust
 pub struct ArithmeticCircuitConfig<F> {
@@ -37,31 +37,36 @@ pub enum Tag {
 
 ## 列的含义
 
-operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b,c,overflow。u16*用来 lookup 算术中的输出如 c_hi,c_lo 属于 u128 范围。这里我们只需要保证输出值的 lookup 就好。cnt 记录某个具体算术指令的行计数器，从正数开始递减到 0。
+**operand***: 存放算术操作中的输入参数，如 `a+b=c+overflow` 指令中的 `a,b,c,overflow`。
 
-# 约束
+**u16***: 用于查找算术运算的输出值，特别是对大数值的低16位和高16位的处理（如 `c_hi`、`c_lo`）。通常在大数运算中，将结果拆分为多个 16-bit 部分进行处理。
 
-在 arithmetic 子电路中约束可以分为两类。
-通用约束
+**cnt**: 记录某个具体算术指令的行计数器，从正数递减到0。
 
-- 约束 cnt 除零行外,当前行与下一行差值为 1
+# 2 约束
 
-不同 Tag 对应的约束不同 **请注意我们这里所有的 u16 都是 little endian 小端编码**
+在设计 `arithmetic` 子电路时，约束可以分为两类：
 
-## Add 
+- **通用约束**:
+  - 约束 `cnt` 除零行外，当前行与下一行的差值为1。这确保了行计数器的正确递减。
+- **不同 Tag 对应的约束**:
+  - 不同的操作（如加法、减法、乘法等）有不同的约束规则。这些规则确保了运算的正确性和结果的准确性。
+
+# 3 运算子电路
+
+## 3.1 Add 
 
 ### 公式
 
-含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和
+a + b = c + overflow * 2^256`，且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit的和。
+
+**约束**:
 
-- 注：加法可以用这个
-- 如果是 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
+- `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
 
@@ -74,16 +79,17 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 
 ### 公式
 
-含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和
+ `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`。
 
-- 注：减法，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
+- 注意：`carry_hi=1 `等价于 `a<b; carry_hi=0 `等价于` a>=b`
 
 ### layout
 
@@ -96,9 +102,9 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 
 ### 公式
 
-我们有(a-d)/b = c ==> c * b + d = a 同时约束 d 小于 b
-```
+`(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})
 
@@ -113,18 +119,21 @@ a * b + c = d
 - 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。
+**约束**:
+
+- 如果是 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
 
@@ -144,27 +153,47 @@ a * b + c = d
 
 ### 公式
 
-需要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) >> 128
-- define carry_hi = (t2 + (t3 << 64) + carry_lo - c_hi) >> 128
-- 如果是 0 行，约束 num_row, 并且约束 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）
+在 `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
 
@@ -183,17 +212,33 @@ a * b + c = d
 
 ### 公式
 
-我们使用 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
+在 `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
 
@@ -207,11 +252,24 @@ a * b + c = d
 
 ## Sdiv_Smod
 
-这里我们还是使用 (a-c)\*b =d 的公式来进行核心约束，值的关注的是对有符号的数进行乘法操作时，我们需要运用到如下补码的知识。
+在 `Sdiv_Smod`（有符号除法和取余）中，我们处理有符号整数的除法和取余，以下是核心约束：
+
+**1 补码表示**
+
+- **计算 `a` 和 `b` 的补码**
+  使用补码表示法将负整数表示为其正值的按位取反加1。正整数的补码表示与其无符号表示相同。
 
-1. 首先我们统一计算a,b 的补码，补码表示法将一个负整数表示为其正值的按位取反（二进制反码）加 1。正整数的补码表示与其无符号表示相同。
-2. 使用 DIV 和 MOD 操作码执行无符号整数除法和取余：将转换后的 U256 数字相除或取余。由于步骤 1 中的转换，这将正确处理有符号整数除法和取余。
-3. 在div 中如果我们是一正一负，需要对计算结果再进行Neg计算(-x mod 2**256.)。如果是mod 则只有被除数是负数时，计算结果才需要进行Neg计算。
+**2 无符号整数除法和取余**
+
+- **使用 DIV 和 MOD 操作码**
+  执行无符号整数的除法和取余，得到正确的结果因为在第一步中我们已将有符号整数转换为无符号整数。
+
+**3 调整结果**
+
+- **当 `a` 和 `b` 一正一负**
+  需要对计算结果进行取反处理 `-x mod 2^256`。
+- **当 `a` 为负数，`b` 为正数时**
+  只有被除数（`a`）是负数时，结果需要进行取反处理。
 
 ### 核心约束说明
   ```
@@ -252,7 +310,6 @@ a * b + c = d
   
 5. 取余结果值约束
 为了保证mul乘法的有效当b==0时，我们设置d==a.(d是余数,b是除数)。但是在eth中计算取余时有b==0时，我们设置d==0.所以在core circuit部分我们需要增加b=0时d==0
-
   ```
 
 ### Layout
@@ -286,21 +343,30 @@ a * b + c = d
 
 ### 公式
 
-输入a,b,n 计算：
+#### 核心公式：
 
-$$a + b  n = r （式1）$$
+输入a,b,n 计算：
 
+a + b mod n = r （式1）
 
 可以将算式转换为：
 a + b   = n * q + r （式2）
 
-这里的q是商，并没有实际出现在EVM的运算中。
-q溢出256bit：
-其中q 可能为257bit，比如当a=b=2^256, n = 1 时。我们可以将q设计为256位+1bit carry位。
-考虑n*q+r溢出512bit：
-n最大值为2256-1, q的最大值为2256-1，r的最大值为2256-2，那么n*q+r的最大值为：2512-2256-3。关键在于约束q的最大值为2256-1（q_overflow = 0 or 1）。
-除数为0：
-考虑n=0，EVM的设计里r = 0，但是实际的程序计算出来的 r = a + b。这时候式子2不能成立，这里直接让r=0（可以避免r超过256bit），使用n=0 判断式作为selector。
+其中 `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
@@ -356,16 +422,12 @@ n最大值为2256-1, q的最大值为2256-1，r的最大值为2256-2，那么n*q
   - `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方法：
@@ -419,7 +481,7 @@ n最大值为2256-1, q的最大值为2256-1，r的最大值为2256-2，那么n*q
     
 *   判断 offset + length > size
     
-*   三种情况_(不用管length是否为0)_，需要返回    **return (real\_len, zero\_len)**：                   
+*   三种情况_(不管length是否为0)_，需要返回    **return (real\_len, zero\_len)**：                   
     
 
 1.  offset + length <= size，                    **return (length,  0)**
@@ -462,8 +524,7 @@ n最大值为2256-1, q的最大值为2256-1，r的最大值为2256-2，那么n*q
     2.  lt\_offset\_size is bool
         
 
-4.  **三种情况下 (real\_len, zero\_len) 的约束：**
-                
+4.  **三种情况下 (real\_len, zero\_len) 的约束：**            
 
 **参考上文，使用overflow 和  lt\_offset\_size 作为 selector，那么公式为：**
 
@@ -512,7 +573,7 @@ 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
@@ -546,13 +607,19 @@ offset\_bound 的代表的是访问内存段的**右区间**：
 
 ### 公式
 
-一行：
+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` 约束来实现。
 
-- operand: a_hi a_lo w w_inv
-- u16s: a_lo 分拆成8个u_16
-- 约束：w=a_lo的前64位 + a_hi<<64
-- w和w_inv的simple is zero约束
-在core里可以使用4个数[a_hi a_lo w w_inv]进行lookup，再加一个Tag = U64Overflow。使用w*w_inv表示0/1，是否u64 overflow。
+- `w` 的溢出与否通过 `w \times w_inv` 判断，若为 0，则表示没有溢出，为 1 则表示发生了溢出。
 
 ### layout