Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
zkevm-circuits
zkevm-circuits
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 0
    • Issues 0
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 0
    • Merge Requests 0
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Packages & Registries
    • Packages & Registries
    • Package Registry
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar

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

  • zkp
  • zkevm-circuitszkevm-circuits
  • Wiki
    • Zkevm docs
  • 8 arithmetic

8 arithmetic · Changes

Page history
feat: update core docs --story=1019296 authored Aug 02, 2024 by chenxuanhui's avatar chenxuanhui
Show whitespace changes
Inline Side-by-side
Showing with 52 additions and 58 deletions
+52 -58
  • zkevm-docs/8-arithmetic.markdown zkevm-docs/8-arithmetic.markdown +52 -58
  • No files found.
zkevm-docs/8-arithmetic.markdown
View page @ ff06ac1b
...@@ -75,7 +75,7 @@ a + b = c + overflow * 2^256`,且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit ...@@ -75,7 +75,7 @@ a + b = c + overflow * 2^256`,且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit
| 1 | c_hi | c_lo | carry_hi | carry_lo | c_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 | | 0 | a_hi | a_lo | b_hi | b_lo | c_hi_u16s |
## Sub ## 3.2 Sub
### 公式 ### 公式
...@@ -98,7 +98,7 @@ a + b = c + overflow * 2^256`,且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit ...@@ -98,7 +98,7 @@ a + b = c + overflow * 2^256`,且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit
| 1 | c_hi | c_lo | carry_hi | carry_lo | c_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 | | 0 | a_hi | a_lo | b_hi | b_lo | c_hi_u16s |
## Div_Mod ## 3.3 Div_Mod
### 公式 ### 公式
...@@ -149,7 +149,7 @@ a * b + c = d ...@@ -149,7 +149,7 @@ a * b + c = d
| DivMod | 1 | c | c | d | d | u16_sum_for_b_lo | | DivMod | 1 | c | c | d | d | u16_sum_for_b_lo |
| DivMod | 0 | a | a | b | b | u16_sum_for_b_hi | | DivMod | 0 | a | a | b | b | u16_sum_for_b_hi |
## Mul ## 3.4 Mul
### 公式 ### 公式
...@@ -208,7 +208,7 @@ a * b + c = d ...@@ -208,7 +208,7 @@ a * b + c = d
| 1 | c_hi | c_lo | carry_hi | carry_lo | a_lo_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 | | 0 | a_hi | a_lo | b_hi | b_lo | a_hi_u16s |
## SLT_SGT ## 3.5 SLT_SGT
### 公式 ### 公式
...@@ -250,7 +250,7 @@ a * b + c = d ...@@ -250,7 +250,7 @@ a * b + c = d
| 1 | c | c | carry | carry | u16_sum_for_c_lo | | | | | 1 | c | c | carry | carry | u16_sum_for_c_lo | | | |
| 0 | a | a | b | b | u16_sum_for_c_hi | | | | | 0 | a | a | b | b | u16_sum_for_c_hi | | | |
## Sdiv_Smod ## 3.6 Sdiv_Smod
在 `Sdiv_Smod`(有符号除法和取余)中,我们处理有符号整数的除法和取余,以下是核心约束: 在 `Sdiv_Smod`(有符号除法和取余)中,我们处理有符号整数的除法和取余,以下是核心约束:
...@@ -339,7 +339,7 @@ a * b + c = d ...@@ -339,7 +339,7 @@ a * b + c = d
| c_hi | c_lo | d_hi | d_lo | 1 | a_com_lo_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 | | | | | | a_hi | a_lo | b_hi | d_lo | 0 | a_com_hi_0 | | | | |
## AddMod ## 3.7 AddMod
### 公式 ### 公式
...@@ -387,7 +387,7 @@ a + b = n * q + r (式2) ...@@ -387,7 +387,7 @@ a + b = n * q + r (式2)
| a_hi | a_lo | b_hi | b_lo | 0 | r_hi | | a_hi | a_lo | b_hi | b_lo | 0 | r_hi |
## MulMod ## 3.8 MulMod
### 核心公式 ### 核心公式
...@@ -469,28 +469,35 @@ a + b = n * q + r (式2) ...@@ -469,28 +469,35 @@ a + b = n * q + r (式2)
| 1 | n_hi | n_lo | r_hi | r_lo | k1_lo_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 | | 0 | a_hi | a_lo | b_hi | b_lo | k1_hi_u16s |
## Length ## 3.9 Length
### length  电路功能: ### length  电路功能:
输入 offset, length, size 输入参数:
返回 real\_len, zero\_len, overflow, _real\_len\_is\_zero, zero\_len\_is\_zero(?待定)_ - `offset`:偏移量
- `length`:长度
- `size`:总大小
* offset,length,size,需要 u64\_overflow 约束 返回值:
* 判断 offset + length > size - `real_len`:实际长度
- `zero_len`:超出长度
- `overflow`:是否溢出
- `_real_len_is_zero`:实际长度是否为零
- `_zero_len_is_zero`:超出长度是否为零(待定)
* 三种情况_(不管length是否为0)_,需要返回    **return (real\_len, zero\_len)**:                    约束条件:
- `offset`、`length`、`size`需要符合 `u64_overflow` 约束。
1. offset + length <= size,                    **return (length,  0)** 逻辑判断:
2. offset + length > size,分为两种情况: - 如果 `offset + length <= size`,返回 `(length, 0)`。
1. offset < size ,                            **return (size - offset, offset + length - size)** - 如果 `offset + length > size`,分为两种情况:
- 如果 `offset < size`,返回 `(size - offset, offset + length - size)`。
2. offset >= size,                             **return (0, length).** - 如果 `offset >= size`,返回 `(0, length)`。
### arithmetic中的布局: ### arithmetic中的布局:
...@@ -503,48 +510,35 @@ a + b = n * q + r (式2) ...@@ -503,48 +510,35 @@ a + b = n * q + r (式2)
### 约束 ### 约束
1. **operand 和 u16s 大小相等** **operand 和 u16s 大小相等**
1. offset, size, length
2. offset\_bound = offset + length
2. **约束 size 是否小于 offset\_bound**
1. 使用 SimpleLtGadget::new(size, offset\_bound, overflow, diff),range 设置为2^64
2. overflow is bool
3. **约束 offset 是否小于 size**
1. 使用 SimpleLtGadget::new(offset, size, lt\_offset\_size, diff\_offset\_size),range 设置为2^64
2. lt\_offset\_size is bool
4. **三种情况下 (real\_len, zero\_len) 的约束:** - `offset`, `length`, `size`
- `offset_bound = offset + length`
**参考上文,使用overflow 和  lt\_offset\_size 作为 selector,那么公式为:** **约束 size 是否小于 offset_bound**
1. real\_len = (1-overflow) \* length  - 使用 `SimpleLtGadget::new(size, offset_bound, overflow, diff)`,`range` 设置为 2^64
- `overflow` 为布尔值
**约束 offset 是否小于 size**
+ overflow \*  lt\_offset\_size \* (size - offset) - 使用 `SimpleLtGadget::new(offset, size, lt_offset_size, diff_offset_size)`,`range` 设置为 2^64
- `lt_offset_size` 为布尔值
2. zero\_len = overflow \* lt\_offset\_size \* (offset\_bound - size) **三种情况下 (real_len, zero_len) 的约束**
- 使用 `overflow` 和 `lt_offset_size` 作为 `selector`,公式如下:
+ overflow \* (1 - lt\_offset\_size) \* length ​ `real_len = (1 - overflow) * length + overflow * lt_offset_size * (size - offset)`
5. **约束 real\_len\_is\_zero, zero\_len\_is\_zero** ​ `zero_len = overflow * lt_offset_size * (offset_bound - size) + overflow * (1 - lt_offset_size) * length`
1. SimpleIsZero(real\_len,real\_len\_inv) **约束 real_len_is_zero 和 zero_len_is_zero**
2. SimpleIsZero(zero\_len,zero\_len\_inv) - 使用 `SimpleIsZero(real_len, real_len_inv)`
- 使用 `SimpleIsZero(zero_len, zero_len_inv)`
## memory expansion ## 3.10 memory expansion
memory expansion 电路的功能是给定offset\_bound,计算是否需要拓展内存。 memory expansion 电路的功能是给定offset\_bound,计算是否需要拓展内存。
...@@ -603,7 +597,7 @@ offset\_bound 的代表的是访问内存段的**右区间**: ...@@ -603,7 +597,7 @@ offset\_bound 的代表的是访问内存段的**右区间**:
**offset\_bound = (offset + length) \* length \* length\_inv** **offset\_bound = (offset + length) \* length \* length\_inv**
## U64Overflow ## 3.11 U64Overflow
### 公式 ### 公式
...@@ -627,7 +621,7 @@ w=a_hi×2^64+a_lo ...@@ -627,7 +621,7 @@ w=a_hi×2^64+a_lo
| ---- | ------- | ------- | ------- | ------- | --------- | | ---- | ------- | ------- | ------- | ------- | --------- |
| 0 | a_hi | a_lo | w | w_inv | a_lo_u16s | | 0 | a_hi | a_lo | w | w_inv | a_lo_u16s |
# 实现 arithmetic 子电路中 Add 例子 # 4 实现 arithmetic 子电路中 Add 例子
如果我们希望为某一个 tag 实现它的约束,我们需要实现 OperationGadget trait,然后在 config 方法中实现相应 tag 的约束就好。具体如下所示 如果我们希望为某一个 tag 实现它的约束,我们需要实现 OperationGadget trait,然后在 config 方法中实现相应 tag 的约束就好。具体如下所示
......
Clone repository
  • basics
    • evm
    • halo2
  • code notes
    • binary_number_with_real_selector
    • how to use macro
    • simple_lt
    • simple_lt_word
  • Home
  • image
  • zkevm docs
    • 1 introduction
    • 10 public
    • 11 fixed
    • 12 exp
    • 13 keccak
    • 14 comparisons
    • 15 differences
View All Pages

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

京ICP备2023035722号-3

京公网安备 11010802044225号