zkevm-docs/8-arithmetic.markdown

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