zkevm-docs/8-arithmetic.markdown

-# 1 布局
+# Arithmetic
+
+## 1 布局
 
 `arithmetic` 子电路用于执行基本的数学运算，如加法、减法、乘法、除法等。`arithmetic` 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，
 
@@ -35,7 +37,7 @@ pub enum Tag {
 
 在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见[here](../code-notes/binary_number_with_real_selector.rs的内容和用法.markdown)。
 
-## 列的含义
+### 列的含义
 
 **operand***: 存放算术操作中的输入参数，如 `a+b=c+overflow` 指令中的 `a,b,c,overflow`。
 
@@ -43,7 +45,7 @@ pub enum Tag {
 
 **cnt**: 记录某个具体算术指令的行计数器，从正数递减到0。
 
-# 2 约束
+## 2 约束
 
 在设计 `arithmetic` 子电路时，约束可以分为两类：
 
@@ -52,11 +54,11 @@ pub enum Tag {
 - **不同 Tag 对应的约束**:
   - 不同的操作（如加法、减法、乘法等）有不同的约束规则。这些规则确保了运算的正确性和结果的准确性。
 
-# 3 运算子电路
+## 3 运算子电路
 
-## 3.1 Add 
+### 3.1 Add 
 
-### 公式
+#### 公式
 
 a + b = c + overflow * 2^256`，且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit的和。
 
@@ -68,16 +70,16 @@ a + b = c + overflow * 2^256`，且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit
 - `c_lo + carry_lo * 2^128 = a_lo + b_lo`。
 - `c_hi + carry_hi * 2^128 = a_hi + b_hi + carry_lo`。
 
-### layout
+#### 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
+### 3.2 Sub
 
-### 公式
+#### 公式
 
  `a - b = c`，且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit的和。
 
@@ -91,16 +93,16 @@ a + b = c + overflow * 2^256`，且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit
 
 - 注意：`carry_hi=1 `等价于 `a<b; carry_hi=0 `等价于` a>=b`
 
-### layout
+#### 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
+### 3.3 Div_Mod
 
-### 公式
+#### 公式
 
 `(a - d) / b = c`，即 `c * b + d = a`，同时约束 `d < b`。
 
@@ -135,10 +137,10 @@ a * b + c = d
 - `carry_lo == u16 sum(rotation -7)`确保了 `carry_lo` 的值正确。
 
 
-### layout
+#### 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 |
@@ -149,9 +151,9 @@ a * b + c = d
 | 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
+### 3.4 Mul
 
-### 公式
+#### 公式
 
 在 `Mul`（乘法）子电路中，我们涉及到的公式和约束是用来确保乘法结果的正确性的。这里详细解释一下每个公式和约束：
 
@@ -195,10 +197,10 @@ a * b + c = d
    - **`(t_hi + carry_lo - carry_hi \* 2^128) - c_hi`**
      确保乘法结果 `t_hi` 和 `c_hi` 的差与 `carry_hi` 乘以2^128的结果相匹配。
 
-### layout
+#### 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     |
@@ -208,9 +210,9 @@ a * b + c = d
 | 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
+### 3.5 SLT_SGT
 
-### 公式
+#### 公式
 
 在 `SLT_SGT`（有符号比较）子电路中，我们处理有符号数的比较，通过补码表示和无符号整数比较来实现。
 
@@ -240,17 +242,17 @@ a * b + c = d
 - **`carry_hi = 1` 等价于 `a < b`**
   `carry_hi = 1` 表示 `a` 小于 `b`；`carry_hi = 0` 表示 `a` 大于或等于 `b`。
 
-### layout
+#### 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
+### 3.6 Sdiv_Smod
 
 在 `Sdiv_Smod`（有符号除法和取余）中，我们处理有符号整数的除法和取余，以下是核心约束：
 
@@ -271,7 +273,7 @@ a * b + c = d
 - **当 `a` 为负数，`b` 为正数时**
   只有被除数（`a`）是负数时，结果需要进行取反处理。
 
-### 核心约束说明
+#### 核心约束说明
   ```
 根据上述补码的知识，我们有 b_com*c_com+d_com=a_com. 其中a_com是a的补码，b_com是b的补码，c_com是c的补码，d_com是d的补码.
 1. 乘法约束
@@ -312,14 +314,14 @@ a * b + c = d
 为了保证mul乘法的有效当b==0时，我们设置d==a.(d是余数,b是除数)。但是在eth中计算取余时有b==0时，我们设置d==0.所以在core circuit部分我们需要增加b=0时d==0
   ```
 
-###  Layout
+####  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         |        |        |        |            |
@@ -339,9 +341,9 @@ a * b + c = d
 | 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
+### 3.7 AddMod
 
-### 公式
+#### 公式
 
 #### 核心公式：
 
@@ -369,10 +371,10 @@ a + b   = n * q + r （式2）
 - 当 `n = 0` 时，`r` 设置为 `a + b`，并且 `n` 处理为 0，以避免 `r` 超过 256 位。这时候式子2不能成立，这里直接让r=0（可以避免r超过256bit），使用n=0 判断式作为selector。
 
 
-### layout
+#### layout
 
 | operand0          | operand1          | operand2    | operand3    | cnt | u16s        |
-|-------------------|-------------------|-------------|-------------|-----|-------------|
+| ----------------- | ----------------- | ----------- | ----------- | --- | ----------- |
 |                   |                   |             |             | 11  | rn_diff_lo  |
 |                   |                   |             |             | 10  | rn_diff_hi  |
 |                   |                   |             |             | 9   | carry_1     |
@@ -387,9 +389,9 @@ a + b   = n * q + r （式2）
 | a_hi              | a_lo              | b_hi        | b_lo        | 0   | r_hi        |
 
 
-## 3.8 MulMod
+### 3.8 MulMod
 
-### 核心公式
+#### 核心公式
 
 **基础公式**：
 
@@ -408,7 +410,7 @@ a + b   = n * q + r （式2）
 - `a_remainder * b + 0 = e + d * 2^256 ` 不变
 - `k2 * n + r = e + d * 2^256` 
 
-### 约束
+#### 约束
 
 （注：以公式角度进行约束描述，未忽略上一步已经约束过的变量）
 
@@ -437,10 +439,10 @@ a + b   = n * q + r （式2）
   - `r, r_diff, n`范围约束；
   - `n != 0`约束；
 
-### layout
+#### 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              |
@@ -469,9 +471,9 @@ a + b   = n * q + r （式2）
 | 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 
+### 3.9 Length 
 
-### length  电路功能：
+#### length  电路功能：
 
 输入参数：
 
@@ -499,16 +501,16 @@ a + b   = n * q + r （式2）
   - 如果 `offset < size`，返回 `(size - offset, offset + length - size)`。
   - 如果 `offset >= size`，返回 `(0, length)`。
 
-### arithmetic中的布局: 
+#### 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 大小相等**
 
@@ -538,7 +540,7 @@ a + b   = n * q + r （式2）
 - 使用 `SimpleIsZero(real_len, real_len_inv)`
 - 使用 `SimpleIsZero(zero_len, zero_len_inv)`
 
-## 3.10 memory expansion
+### 3.10 memory expansion
 
 memory expansion 电路的功能是给定offset\_bound，计算是否需要拓展内存。
 
@@ -549,14 +551,14 @@ offset\_bound 的代表的是访问内存段的**右区间**：
 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** 
@@ -585,7 +587,7 @@ offset\_bound 的代表的是访问内存段的**右区间**：
 *   使用 SimpleLtGadget::new(memory\_chunk\_prev, access\_memory\_size, expansion\_tag, diff)，range 设置为2^64
     
 
-### 有length 的时候如何约束offset\_bound
+#### 有length 的时候如何约束offset\_bound
 
 添加加一个 length\_inv _(大部分电路里面已经有了)_
 
@@ -597,9 +599,9 @@ offset\_bound 的代表的是访问内存段的**右区间**：
 
 **offset\_bound = (offset + length) \* length \* length\_inv**
 
-## 3.11 U64Overflow
+### 3.11 U64Overflow
 
-### 公式
+#### 公式
 
 w=a_hi×2^64+a_lo
 
@@ -615,13 +617,13 @@ w=a_hi×2^64+a_lo
 
 - `w` 的溢出与否通过 `w \times w_inv` 判断，若为 0，则表示没有溢出，为 1 则表示发生了溢出。
 
-### layout
+#### 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 例子
+## 4 实现 arithmetic 子电路中 Add 例子
 
 如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示