Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
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: add sdiv_smod doc authored 1 year ago by liuxingxing1's avatar liuxingxing1
Show whitespace changes
Inline Side-by-side
Showing with 23 additions and 9 deletions
+23 -9
  • zkevm-docs/8-arithmetic.markdown zkevm-docs/8-arithmetic.markdown +23 -9
  • No files found.
zkevm-docs/8-arithmetic.markdown
View page @ 21fd5ac5
......@@ -149,13 +149,13 @@ a * b + c = d
2. 使用 DIV 和 MOD 操作码执行无符号整数除法和取余:将转换后的 U256 数字相除或取余。由于步骤 1 中的转换,这将正确处理有符号整数除法和取余。
3. 在div 中如果我们是一正一负,需要对计算结果再进行Neg计算(-x mod 2**256.)。如果是mod 则只有被除数是负数时,计算结果才需要进行Neg计算。
###核心约束说明
### 核心约束说明
```
根据上述补码的知识,我们有 b_com*c_com+d_com=a_com. 其中a_com是a的补码,b_com是b的补码,c_com是c的补码,d_com是d的补码.
1. 乘法约束
细节请参考mul模块约束内容
2. 补码的相关约束如下
2. 补码的相关约束如下(开发时我们需要实现a,b,c,d的下述约束)
- x_abs_lo == lo when x >= 0
- x_abs_hi == hi when x >= 0
- sum == 0 when x < 0 (小于0证明存在补码,同时我们有x+x_abs = 1 <<256。x + x_abs 约束请参考add部分)
......@@ -165,16 +165,30 @@ a * b + c = d
因为当前算法中使用了mul约束,所以我们需要对mul中的变量进行范围约束。同时也因为判断a,b,c,d正负符号的原因,我们需要对a_hi,b_hi,c_hi,d_hi进行范围约束。
另外因为判断补码有效性的原因,我们需要对a,b,c,d以及他们的补码值进行u128范围约束,因为a,b是输入可以忽略,只需增加对a_hi,b_hi,c_lo,d_lo进行u128范围约束。
4.符号为约束
- sign(dividend_original) == sign(remainder_original) when quotient, divisor and remainder original value are all non-zero。 这里主要约束mod的值与被除数的符号相同
- quotient_original.is_neg().expr() + divisor_original.is_neg().expr() (如果被除数的补码也是负数,与余数和除数等于零,则排除约束情况) 这里说到的符号都是非补码的符号
- dividend_original.is_neg().expr()
4.符号约束
sign(dividend_original) == sign(remainder_original) when quotient, divisor and remainder original value are all non-zero。 这里主要约束mod的值与被除数的符号相同
- (1.expr() - quotient_is_zero.expr())
* (1.expr() - divisor_is_zero.expr())
* (1.expr() - remainder_is_zero.expr())
* (dividend_original.is_neg().expr() - remainder_original.is_neg().expr())
quotient_original.is_neg().expr() + divisor_original.is_neg().expr() (如果被除数的补码也是负数,与余数和除数等于零,则排除约束情况) 这里说到的符号都是非补码的符号
这里计算的都是div情况下的变化
- (
quotient_original.is_neg().expr() + divisor_original.is_neg().expr() -dividend_original.is_neg().expr()
- 2.expr()
* quotient_original.is_neg().expr()
* divisor__original.is_neg().expr(), 这里计算的都是div情况下的变化
* divisor__original.is_neg().expr()
)
*(1.expr() - quotient_is_zero.expr())
* (1.expr() - divisor_is_zero.expr())
* (1.expr() - dividend_is_signed_overflow.expr()) //**dividend_is_signed_overflow是指被除数补码是否为负数,这里需要判断的原因是剔除特殊情况**
note: 对于一个特殊的SDIV情况,当输入dividend = -(1 << 255) 和 divisor = -1时,商的结果应该是1 << 255。但是一个有符号字(signed word)只能表示从-(1 << 255)到
(1 << 255) - 1的有符号值。因此,对于这种情况,约束条件sign(dividend) == sign(divisor) ^ sign(quotient)不能应用。
5. 取余结果值约束
为了保证mul乘法的有效当b==0时,我们设置d==a.(eg余数=被除数)。但是在eth中计算取余时有b==0时,我们设置d==0.所以在core circuit部分我们需要增加b=0时,d==0
为了保证mul乘法的有效当b==0时,我们设置d==a.(d是余数,b是除数)。但是在eth中计算取余时有b==0时,我们设置d==0.所以在core circuit部分我们需要增加b=0时d==0
```
## AddMod
......
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号