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 24 additions and 26 deletions
+24 -26
  • zkevm-docs/8-arithmetic.markdown zkevm-docs/8-arithmetic.markdown +24 -26
  • No files found.
zkevm-docs/8-arithmetic.markdown
View page @ 34628e00
......@@ -74,12 +74,13 @@ operand* 用来存放算术中的参数值,如 a+b=c+overflow 指令中的 a,b
## Div_Mod
我们有a/b = d + c ==> d * b + c = a 同时约束 c 小于 b
我们有(a-d)/b = c ==> c * b + d = a 同时约束 d 小于 b
```
if tag is div, (a,b,c,d) = (push, pop2, pop1 - push \* pop2, pop1)
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
a * b + c = d
- define t0 = a0 \* b0
- define t1 = a0 \* b1 + a1 \* b0
- define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
......@@ -142,42 +143,39 @@ define
## Sdiv_Smod
这里我们还是使用 a\*b+c=d 的公式来进行核心约束,值的关注的是对有符号的数进行操作,我们需要运用到补码的知识。
这里我们还是使用 (a-c)\*b =d 的公式来进行核心约束,值的关注的是对有符号的数进行乘法操作时,我们需要运用到如下补码的知识。
1. 首先我们统一计算a,b 的补码,补码表示法将一个负整数表示为其正值的按位取反(二进制反码)加 1。正整数的补码表示与其无符号表示相同。
2. 使用 DIV 和 MOD 操作码执行无符号整数除法和取余:将转换后的 U256 数字相除或取余。由于步骤 1 中的转换,这将正确处理有符号整数除法和取余。
3. 在div 中如果我们是一正一负,需要对计算结果再进行补码计算。如果是mod 则有只要a是负数计算结果才需要进行补码计算
```
if tag is sdiv
- a = push
- b = pop2
- c = if is*pop1_neg{get_neg(pop1_abs - push_abs * pop2*abs)}else{pop1_abs - push_abs * pop2_abs}
- d = pop1
if tag is smod
- a = if is_pop2_zero{0}else if is_pop1_neg == is_pop2_neg {pop1_abs / pop2_abs}else{get_neg(pop1_abs / pop2_abs)}
- b = pop2
- c = if pop2.is_zero() { pop1 } else { push }
- d = pop1
3. 在div 中如果我们是一正一负,需要对计算结果再进行Neg计算(-x mod 2**256.)。如果是mod 则只有被除数是负数时,计算结果才需要进行Neg计算。
###核心约束说明
```
a_abs,b_abs,c_abs,d_abs
根据上述补码的知识,我们有 b_com*c_com+d_com=a_com. 其中a_com是a的补码,b_com是b的补码,c_com是c的补码,d_com是d的补码.
1. 乘法约束
细节请参考mul模块约束内容
```
关于补码的相关约束如下
2. 补码的相关约束如下
- 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部分)
- carry_hi == 1 when x < 0
```
- mul_add_words (请参考mul部分约束内容)
- abs(remainder) < abs(divisor) when divisor != 0
- mul_add_words中的carry_hi == 0
- sign(dividend) == sign(remainder) when quotient, divisor and remainder are all non-zero。 这里主要是有mod的值与被除数的符号相同
- quotient_abs_word.is_neg().expr() + divisor_abs_word.is_neg().expr() (如果被除数的补码也是负数,与余数和除数等于零,则排除约束情况) 这里说到的符号都是非补码的符号
- dividend_abs_word.is_neg().expr()
3. 范围约束
因为当前算法中使用了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()
- 2.expr()
* quotient_abs_word.is_neg().expr()
* divisor_abs_word.is_neg().expr(), 这里计算的都是div情况下的变化
* quotient_original.is_neg().expr()
* divisor__original.is_neg().expr(), 这里计算的都是div情况下的变化
5. 取余结果值约束
为了保证mul乘法的有效当b==0时,我们设置d==a.(eg余数=被除数)。但是在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号