Skip to content

GitLab

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

8 arithmetic · Changes

Page history
feat: update mulmod authored by xiaoranlu's avatar xiaoranlu
Show whitespace changes
Inline Side-by-side
Showing with 163 additions and 110 deletions
zkevm-docs/8-arithmetic.markdown
View page @ 5fcd7611
...@@ -46,95 +46,104 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b ...@@ -46,95 +46,104 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
不同 Tag 对应的约束不同 **请注意我们这里所有的 u16 都是 little endian 小端编码** 不同 Tag 对应的约束不同 **请注意我们这里所有的 u16 都是 little endian 小端编码**
- Add (含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和) ## Add
- 注：加法可以用这个 含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和
- 如果是 cnt=0 行，则 cnt_prev=1,cnt_prev_prev=0
- c_lo = u16 sum(rotation cur) - 注：加法可以用这个
- c_hi = u16 sum(rotation prev) - 如果是 cnt=0 行，则 cnt_prev=1,cnt_prev_prev=0
- carry hi is bool - c_lo = u16 sum(rotation cur)
- carry lo is bool - c_hi = u16 sum(rotation prev)
- c lo + carry lo \* 2^128 = a lo + b lo - carry hi is bool
- c hi + carry hi \* 2^128 = a hi + b hi + carry lo - carry lo is bool
- c lo + carry lo \* 2^128 = a lo + b lo
- Sub (含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和) - c hi + carry hi \* 2^128 = a hi + b hi + carry lo
- 注：减法，LT，GT 都可以用这个 ## Sub
- c_lo = u16 sum(rotation cur)
- c_hi = u16 sum(rotation prev) 含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和
- carry hi is bool
- carry lo is bool - 注：减法，LT，GT 都可以用这个
- a_lo + carrry_lo \* 2^128 = b_lo + c_lo - c_lo = u16 sum(rotation cur)
- a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi - c_hi = u16 sum(rotation prev)
- 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b - carry hi is bool
- carry lo is bool
- Div_Mod (我们有a/b = d + c ==> d * b + c = a 同时约束 c 小于 b) - a_lo + carrry_lo \* 2^128 = b_lo + c_lo
``` - a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi
if tag is div, (a,b,c,d) = (push, pop2, pop1 - push \* pop2, pop1) - 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b
if tag is mod, (a,b,c,d) = (if pop2 is zero{0}else{pop1/pop2},pop2,if pop2 is zero{pop1}else{push},pop1)
## Div_Mod
define
- define t0 = a0 \* b0 我们有a/b = d + c ==> d * b + c = a 同时约束 c 小于 b
- define t1 = a0 \* b1 + a1 \* b0 ```
- define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1 if tag is div, (a,b,c,d) = (push, pop2, pop1 - push \* pop2, pop1)
- define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2 if tag is mod, (a,b,c,d) = (if pop2 is zero{0}else{pop1/pop2},pop2,if pop2 is zero{pop1}else{push},pop1)
- define t_lo=t0+(t1)\*2^64
- define t_hi=(t2)+(t3)\*2^64 define
- define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128 - define t0 = a0 \* b0
- define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128 - define t1 = a0 \* b1 + a1 \* b0
``` - define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
- 如果是 0 行，约束 num_row is 10,并且约束 cnt 自增的有效性 - define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2
- b_lo = u16 sum(rotation -2) //请注意因为a是输入值，我们可以不对a_hi,a_lo进行range约束 - define t_lo=t0+(t1)\*2^64
- b_hi = u16 sum(rotation -3) - define t_hi=(t2)+(t3)\*2^64
- c_lo = u16 sum(rotation -4) - define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
- c_hi = u16 sum(rotation -5) - define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128
- d_lo = u16 sum(rotation -6) ```
- d_hi = u16 sum(rotation -7) - 如果是 0 行，约束 num_row is 10,并且约束 cnt 自增的有效性
- (t_lo+c_lo-car_lo\*2^128) - d_lo - b_lo = u16 sum(rotation -2) //请注意因为a是输入值，我们可以不对a_hi,a_lo进行range约束
- (t_hi+c_hi+car_lo-car_hi\*2^128) - d_hi - b_hi = u16 sum(rotation -3)
- residue < divisor when divisor != 0 - c_lo = u16 sum(rotation -4)
- carry_hi == 0 - c_hi = u16 sum(rotation -5)
- carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。 - 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
- Mul(需要8行对 a,b,d,carry lookup,carry lookup的原因是在进行计算时carry_lo或carry需要左移128位，因为有限域的特点可能存在左移后carry_lo或carry_hi在0-128bit存在值) 其中 operand0 是 a,operand1 是 b - residue < divisor when divisor != 0
- carry_hi == 0
- define t0 = a0 \* b0 （0-128bit） - carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。
- define t1 = a0 \* b1 + a1 \* b0 (64-193bit)
- define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1 (128 - 257bit) ## Mul
- define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2 (192- 322bit)
- define t_lo=t0+(t1)\*2^64 需要8行对 a,b,d,carry lookup,carry lookup的原因是在进行计算时carry_lo或carry需要左移128位，因为有限域的特点可能存在左移后carry_lo或carry_hi在0-128bit存在值) 其中 operand0 是 a,operand1 是 b
- define t_hi=(t2)+(t3)\*2^64
- define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128 c_lo is 0 - define t0 = a0 \* b0 （0-128bit）
- define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128 c_hi is 0 - define t1 = a0 \* b1 + a1 \* b0 (64-193bit)
- 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性 - define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1 (128 - 257bit)
- a_lo = u16 sum(rotation cur) - define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2 (192- 322bit)
- a_hi = u16 sum(rotation -1) - define t_lo=t0+(t1)\*2^64
- b_lo = u16 sum(rotation -2) - define t_hi=(t2)+(t3)\*2^64
- b_hi = u16 sum(rotation -3) - define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128 c_lo is 0
- c_lo = u16 sum(rotation -4) - define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128 c_hi is 0
- c_hi = u16 sum(rotation -5) - 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性
- carry_hi == u16 sum(rotation -6) 请注意这里我们使用的是5位u16数据的和，从define部分我们可以知道carry_hi等于322 - 256 = 66bit。 - a_lo = u16 sum(rotation cur)
- carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。 - a_hi = u16 sum(rotation -1)
- （t_lo-car_lo\*2^128） -（c_lo） - b_lo = u16 sum(rotation -2)
- （t_hi+car_lo-car_hi\*2^128）-（c_hi） - b_hi = u16 sum(rotation -3)
- c_lo = u16 sum(rotation -4)
- c_hi = u16 sum(rotation -5)
- Slt_Sgt (我们使用 a-b=c - carry<<256 的公式来约束有相同符号的内容这里我们需要注意的是，当符号相等时，我们统一按照无符号整数比较大小)`` - carry_hi == u16 sum(rotation -6) 请注意这里我们使用的是5位u16数据的和，从define部分我们可以知道carry_hi等于322 - 256 = 66bit。
- 比较a_hi,b_hi最高u16位是否小于2^15确定a,b符号。如果a_lt == 1则a为正数，否则为负数。b_lt同理。 - carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。
- 同时我们需要约束a_hi和b_hi等于对应的u16s_sum。这里主要是为了约束我们用来判断符号的u16的正确性。 - （t_lo-car_lo\*2^128） -（c_lo）
- a,b符号不相等时。我们有(a_lt - b_lt)作为不相等condition， - （t_hi+car_lo-car_hi\*2^128）-（c_hi）
- 当 a_lt == 1,a是正数,则存在carry == 0。a_lt == 0时a是负数，carry=1.所以有约束 1-(a_lt + carry_hi)
- c_lo = u16 sum(rotation -4) ## SLT_SGT
- c_hi = u16 sum(rotation -5)
- a,b符号相等时,我们有(1 -(a_lt - b_lt))作为符号condition，与下面每一个约束相乘 我们使用 a-b=c - carry<<256 的公式来约束有相同符号的内容这里我们需要注意的是，当符号相等时，我们统一按照无符号整数比较大小
- a_lo + carrry_lo \* 2^128 = b_lo + c_lo - 比较a_hi,b_hi最高u16位是否小于2^15确定a,b符号。如果a_lt == 1则a为正数，否则为负数。b_lt同理。
- a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi - 同时我们需要约束a_hi和b_hi等于对应的u16s_sum。这里主要是为了约束我们用来判断符号的u16的正确性。
- 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b - 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)
- Sdiv_Smod（这里我们还是使用 a\*b+c=d 的公式来进行核心约束，值的关注的是对有符号的数进行操作，我们需要运用到补码的知识。） - 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
## Sdiv_Smod
这里我们还是使用 a\*b+c=d 的公式来进行核心约束，值的关注的是对有符号的数进行操作，我们需要运用到补码的知识。
1. 首先我们统一计算a,b 的补码，补码表示法将一个负整数表示为其正值的按位取反（二进制反码）加 1。正整数的补码表示与其无符号表示相同。 1. 首先我们统一计算a,b 的补码，补码表示法将一个负整数表示为其正值的按位取反（二进制反码）加 1。正整数的补码表示与其无符号表示相同。
2. 使用 DIV 和 MOD 操作码执行无符号整数除法和取余：将转换后的 U256 数字相除或取余。由于步骤 1 中的转换，这将正确处理有符号整数除法和取余。 2. 使用 DIV 和 MOD 操作码执行无符号整数除法和取余：将转换后的 U256 数字相除或取余。由于步骤 1 中的转换，这将正确处理有符号整数除法和取余。
3. 在div 中如果我们是一正一负，需要对计算结果再进行补码计算。如果是mod 则有只要a是负数计算结果才需要进行补码计算 3. 在div 中如果我们是一正一负，需要对计算结果再进行补码计算。如果是mod 则有只要a是负数计算结果才需要进行补码计算
...@@ -168,12 +177,14 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b ...@@ -168,12 +177,14 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
* quotient_abs_word.is_neg().expr() * quotient_abs_word.is_neg().expr()
* divisor_abs_word.is_neg().expr(), 这里计算的都是div情况下的变化 * divisor_abs_word.is_neg().expr(), 这里计算的都是div情况下的变化
## AddMod
- AddMod 计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有(a+b)%n = r。我们可以将这个约束转化为(a+b) = n * q + r。为了约束简单我们可以有 计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有(a+b)%n = r。我们可以将这个约束转化为(a+b) = n * q + r。为了约束简单我们可以有
a % n= a_div_n + a_remainder a = n * a_div_n + a_remainder a % n= a_div_n + a_remainder a = n * a_div_n + a_remainder
(a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 ) (a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 )
(a_remainder_plus_b + a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r (a_remainder_plus_b + a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r
note: 其中a_remainder+b 大于256位. 我们可以有以下约束 note: 其中a_remainder+b 大于256位. 我们可以有以下约束
``` ```
/// Construct the gadget that checks a * b + c == d * 2**256 + e /// Construct the gadget that checks a * b + c == d * 2**256 + e
/// where a, b, c, d, e are 256-bit words. /// where a, b, c, d, e are 256-bit words.
...@@ -202,23 +213,65 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b ...@@ -202,23 +213,65 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
- r < n 约束 - r < n 约束
- n_is_zero 约束 - n_is_zero 约束
## MulMod
- MulMod 计算mulMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有a*b%n = r。我们可以将这个约束转化为a*b = n * q + r。为了约束简单我们可以有 ### 核心公式
a % n= a_div_n + a_remainder -> a = n * a_div_n + a_remainder
a_remainder * b =product & n= b_div_n + r **基础公式**：
product是512bit,我们将它分为两个256bit的数，product_hi,product_lo。我们可以有以下约束
- a,n,a_remainder,a_div_n 存在mul_words约束 - `a*b = r (mod n)`，其中 ` a,b,n,r` 为 256-bit。
- b,a_remainder,product_hi,product_lo 存在mul_add_words约束,请注意这里b*a_remainder的结果等于port是512bit.我们最后有product_hi * 2^256 + product_lo = b * a_remainder
- product_hi,product_lo,n,b_div_n,r 存在mul_add_words约束,同样需要注意这里n * b_div_n + r 的结果等于product是512bit.我们最后有product_hi * 2^256 + product_lo = n * b_div_n + r **公式拆分：**
- a_remainder < n 约束
- r < n 约束 - `a/n = k1 余 a_remainder`
- n_is_zero 约束
- `(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`约束；
## Length
- Length arithmetic中的布局:
arithmetic中的布局:
| tag | cnt | operand_0_hi | operand_0_lo | operand_1_hi | operand_1_lo | u16_0 | u16_1 | u16_2 | u16_3 | u16_4 | u16_5 | u16_6 | u16_7 | | tag | cnt | operand_0_hi | operand_0_lo | operand_1_hi | operand_1_lo | u16_0 | u16_1 | u16_2 | u16_3 | u16_4 | u16_5 | u16_6 | u16_7 |
......

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

京ICP备2023035722号-3

京公网安备 11010802044225号