Skip to content

GitLab

新注册的用户请输入邮箱并保存，随后登录邮箱激活账号。后续可直接使用邮箱登录！

8 arithmetic · Changes

Page history
feat: modify docs --story=1 authored by gz Xu's avatar gz Xu
Hide whitespace changes
Inline Side-by-side
Showing with 142 additions and 140 deletions
zkevm-docs/8-arithmetic.markdown
View page @ 66f9a8e9
# 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 |
| 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 |
| 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,23 +137,23 @@ 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 |
| 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 |
| 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
### 3.4 Mul
### 公式
#### 公式
在 `Mul`（乘法）子电路中，我们涉及到的公式和约束是用来确保乘法结果的正确性的。这里详细解释一下每个公式和约束：
......@@ -195,22 +197,22 @@ 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 |
| 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 |
| 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
### 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 | | | |
| 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,36 +314,36 @@ 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 | | | | |
| 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
### 公式
| 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
#### 公式
#### 核心公式：
......@@ -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,41 +439,41 @@ a + b = n * q + r （式2）
- `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  电路功能：
#### 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  电路功能：
输入参数：
......@@ -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 |
| 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 |
| 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 的约束就好。具体如下所示
......

Copyright © 2024 ChainWeaver Org. All Rights Reserved. 版权所有。

京ICP备2023035722号-3

京公网安备 11010802044225号