Skip to content

GitLab

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

8 arithmetic · Changes

Page history
feat: supplyment arithmetic layout authored by xiaoranlu's avatar xiaoranlu
Show whitespace changes
Inline Side-by-side
Showing with 94 additions and 28 deletions
zkevm-docs/8-arithmetic.markdown
View page @ 05e8943c
...@@ -48,6 +48,8 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b ...@@ -48,6 +48,8 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
## Add ## Add
### 公式
含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和 含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和
- 注：加法可以用这个 - 注：加法可以用这个
...@@ -59,8 +61,17 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b ...@@ -59,8 +61,17 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
- c lo + carry lo \* 2^128 = a lo + b lo - c lo + carry lo \* 2^128 = a lo + b lo
- c hi + carry hi \* 2^128 = a hi + b hi + carry 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 |
## Sub ## Sub
### 公式
含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和 含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和
- 注：减法，LT，GT 都可以用这个 - 注：减法，LT，GT 都可以用这个
...@@ -72,8 +83,17 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b ...@@ -72,8 +83,17 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
- a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi - 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
| 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 |
## Div_Mod ## Div_Mod
### 公式
我们有(a-d)/b = c ==> c * b + d = a 同时约束 d 小于 b 我们有(a-d)/b = c ==> c * b + d = a 同时约束 d 小于 b
``` ```
...@@ -104,8 +124,24 @@ a * b + c = d ...@@ -104,8 +124,24 @@ a * b + c = d
- carry_hi == 0 - carry_hi == 0
- carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。 - carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。
### 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 |
## Mul ## Mul
### 公式
需要8行对 a,b,d,carry lookup,carry lookup的原因是在进行计算时carry_lo或carry需要左移128位，因为有限域的特点可能存在左移后carry_lo或carry_hi在0-128bit存在值) 其中 operand0 是 a,operand1 是 b 需要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 t0 = a0 \* b0 （0-128bit）
...@@ -128,8 +164,23 @@ a * b + c = d ...@@ -128,8 +164,23 @@ a * b + c = d
- （t_lo-car_lo\*2^128） -（c_lo） - （t_lo-car_lo\*2^128） -（c_lo）
- （t_hi+car_lo-car_hi\*2^128）-（c_hi） - （t_hi+car_lo-car_hi\*2^128）-（c_hi）
### 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 |
## SLT_SGT ## SLT_SGT
### 公式
我们使用 a-b=c - carry<<256 的公式来约束有相同符号的内容这里我们需要注意的是，当符号相等时，我们统一按照无符号整数比较大小 我们使用 a-b=c - carry<<256 的公式来约束有相同符号的内容这里我们需要注意的是，当符号相等时，我们统一按照无符号整数比较大小
- 比较a_hi,b_hi最高u16位是否小于2^15确定a,b符号。如果a_lt == 1则a为正数，否则为负数。b_lt同理。 - 比较a_hi,b_hi最高u16位是否小于2^15确定a,b符号。如果a_lt == 1则a为正数，否则为负数。b_lt同理。
- 同时我们需要约束a_hi和b_hi等于对应的u16s_sum。这里主要是为了约束我们用来判断符号的u16的正确性。 - 同时我们需要约束a_hi和b_hi等于对应的u16s_sum。这里主要是为了约束我们用来判断符号的u16的正确性。
...@@ -142,6 +193,16 @@ a * b + c = d ...@@ -142,6 +193,16 @@ a * b + c = d
- a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi - 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
| 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 | | | |
## Sdiv_Smod ## Sdiv_Smod
这里我们还是使用 (a-c)\*b =d 的公式来进行核心约束，值的关注的是对有符号的数进行乘法操作时，我们需要运用到如下补码的知识。 这里我们还是使用 (a-c)\*b =d 的公式来进行核心约束，值的关注的是对有符号的数进行乘法操作时，我们需要运用到如下补码的知识。
...@@ -221,6 +282,8 @@ a * b + c = d ...@@ -221,6 +282,8 @@ a * b + c = d
## AddMod ## AddMod
### 公式
计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有 **(a+b)%n = r**。我们可以将这个约束转化为 **(a+b) = n * q + r**(商q可能超过256bit)。所以为了约束简单我们可以将上式转换如下： 计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有 **(a+b)%n = r**。我们可以将这个约束转化为 **(a+b) = n * q + r**(商q可能超过256bit)。所以为了约束简单我们可以将上式转换如下：
1. **a % n= a_div_n + a_remainder** 1. **a % n= a_div_n + a_remainder**
2. **(a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 )** 2. **(a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 )**
...@@ -239,32 +302,28 @@ a * b + c = d ...@@ -239,32 +302,28 @@ a * b + c = d
- 当n!=0时, 存在r < n 约束 - 当n!=0时, 存在r < n 约束
### layout ### layout
```
// Addmod arithmetic witeness rows. (Tag::Addmod) | operand_0_hi | operand_0_lo | operand_1_hi | operand_1_lo | cnt | u16s |
// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+ | ------------ | ------------ | ------------------------------ | ------------------------------ | ---- | --------------------- |
// | operand_0_hi| operand_0_lo| operand_1_hi | operand_1_lo | cnt | u16s | | | | | | 18 | rn_diff_lo |
// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+ | | | | | 17 | rn_diff_hi |
// | | | | | 18 | rn_diff_lo | | | | | | 16 | carry_1 |
// | | | | | 17 | rn_diff_hi | | | | | | 15 | carry_0 |
// | | | | | 16 | carry_1 | | | | | | 14 | b_div_n_lo |
// | | | | | 15 | carry_0 | | | | | | 13 | b_div_n_hi |
// | | | | | 14 | b_div_n_lo | | | | | | 12 | r_lo |
// | | | | | 13 | b_div_n_hi | | | | | | 11 | r_hi |
// | | | | | 12 | r_lo | | | | | | 10 | a_remainder_plus_b_lo |
// | | | | | 11 | r_hi | | | | | | 9 | a_remainder_plus_b_hi |
// | | | | | 10 | a_remainder_plus_b_lo | | | | | | 8 | arn_diff_lo |
// | | | | | 9 | a_remainder_plus_b_hi | | b_div_n_hi | b_div_n_lo | a_remainder_plus_b_hi | a_remainder_plus_b_lo | 7 | arn_diff_hi |
// | | | | | 8 | arn_diff_lo | | rn_diff_hi | rn_diff_lo | carry_2 | | 6 | an_carry_lo |
// | b_div_n_hi | b_div_n_lo | a_remainder_plus_b_hi | a_remainder_plus_b_lo | 7 | arn_diff_hi | | carry_0 | carry_1 | rn_carry_lt_hi | rn_carry_lt_lo | 5 | a_remainder_lo |
// | rn_diff_hi | rn_diff_lo | carry_2 | | 6 | an_carry_lo | | arn_diff_hi | arn_diff_lo | a_remainder_plus_b_overflow_hi | a_remainder_plus_b_overflow_lo | 4 | a_remainder_hi |
// | carry_0 | carry_1 | rn_carry_lt_hi | rn_carry_lt_lo | 5 | a_remainder_lo | | an_carry_hi | an_carry_lo | arn_carry_lt_hi | arn_carry_lt_lo | 3 | n_lo |
// | arn_diff_hi | arn_diff_lo | a_remainder_plus_b_overflow_hi | a_remainder_plus_b_overflow_lo | 4 | a_remainder_hi | | a_div_n_hi | a_div_n_lo | a_remainder_hi | a_remainder_lo | 2 | n_hi |
// | an_carry_hi | an_carry_lo | arn_carry_lt_hi | arn_carry_lt_lo | 3 | n_lo | | n_hi | n_lo | r_hi | r_lo | 1 | a_div_n_lo |
// | a_div_n_hi | a_div_n_lo | a_remainder_hi | a_remainder_lo | 2 | n_hi | | a_hi | a_lo | b_hi | b_lo | 0 | a_div_n_hi |
// | n_hi | n_lo | r_hi | r_lo | 1 | a_div_n_lo |
// | a_hi | a_lo | b_hi | b_lo | 0 | a_div_n_hi |
// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+
```
## MulMod ## MulMod
...@@ -321,8 +380,6 @@ a * b + c = d ...@@ -321,8 +380,6 @@ a * b + c = d
- `r, r_diff, n`范围约束； - `r, r_diff, n`范围约束；
- `n != 0`约束； - `n != 0`约束；
### layout ### layout
| cnt | o_0_hi | o_0_lo | o_1_hi | o_1_lo | u16s_0 | | cnt | o_0_hi | o_0_lo | o_1_hi | o_1_lo | u16s_0 |
...@@ -409,13 +466,22 @@ arithmetic中的布局: ...@@ -409,13 +466,22 @@ arithmetic中的布局:
## U64Overflow ## U64Overflow
### 公式
一行： 一行：
- operand: a_hi a_lo w w_inv - operand: a_hi a_lo w w_inv
- u16s: a_lo 分拆成8个u_16 - u16s: a_lo 分拆成8个u_16
- 约束：w=a_lo的前64位 + a_hi<<64 - 约束：w=a_lo的前64位 + a_hi<<64
- w和w_inv的simple is zero约束 - 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。 在core里可以使用4个数[a_hi a_lo w w_inv]进行lookup，再加一个Tag = U64Overflow。使用w*w_inv表示0/1，是否u64 overflow。
### 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 |
# 实现 arithmetic 子电路中 Add 例子 # 实现 arithmetic 子电路中 Add 例子
如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示 如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示
......

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

京ICP备2023035722号-3

京公网安备 11010802044225号