zkevm-docs/8-arithmetic.markdown

@@ -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