zkevm-docs/8-arithmetic.markdown

@@ -100,7 +100,7 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 
   
 
-- Mul(需要8行对 a,b,c,carry lookup,carry lookup的原因是在进行计算时carry_lo或carry需要左移128位，因为有限域的特点可能存在左移后carry_lo或carry_hi在0-128bit存在值) 其中 operand0 是 a,operand1 是 b
+- Mul(需要8行对 a,b,d,carry lookup,carry lookup的原因是在进行计算时carry_lo或carry需要左移128位，因为有限域的特点可能存在左移后carry_lo或carry_hi在0-128bit存在值) 其中 operand0 是 a,operand1 是 b
   
   - define t0 = a0 \* b0 （0-128bit）
   - define t1 = a0 \* b1 + a1 \* b0 (64-193bit)
@@ -108,8 +108,8 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2 (192- 322bit)
   - define t_lo=t0+(t1)\*2^64
   - define t_hi=(t2)+(t3)\*2^64
-  - define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
-  - define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128
+  - define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128   c_lo is 0
+  - define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128 c_hi is 0
   - 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性
   - a_lo = u16 sum(rotation cur)
   - a_hi = u16 sum(rotation -1)
@@ -137,7 +137,9 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 
 
 - Sdiv_Smod（这里我们还是使用 a\*b+c=d 的公式来进行核心约束，值的关注的是对有符号的数进行操作，我们需要运用到补码的知识。）
-  对有符号整数进行计算时。所有的输入值都由 core circuit 传递。我们在这里约束传递值如下
+1. 首先我们统一计算a,b 的补码，补码表示法将一个负整数表示为其正值的按位取反（二进制反码）加 1。正整数的补码表示与其无符号表示相同。
+2. 使用 DIV 和 MOD 操作码执行无符号整数除法和取余：将转换后的 U256 数字相除或取余。由于步骤 1 中的转换，这将正确处理有符号整数除法和取余。
+3. 在div 中如果我们是一正一负，需要对计算结果再进行补码计算。如果是mod 则有只要a是负数计算结果才需要进行补码计算
   ```
   if tag is sdiv
   - a = push
@@ -151,14 +153,45 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - d = pop1
   ```
   - a_abs,b_abs,c_abs,d_abs
-  - mul_add_words
-  - c lt b
-  - d is_signed_overflow
-  - a,b,c is zero
-
-
-- Addmod
-- Mulmod
+  ``
+  关于补码的相关约束如下
+  - 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()
+    - 2.expr()
+    * quotient_abs_word.is_neg().expr()
+    * divisor_abs_word.is_neg().expr(),
+
+
+- AddMod 计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有(a+b)%n = r。我们可以将这个约束转化为(a+b) = n * q + r。为了约束简单我们可以有
+  a % n= a_div_n + a_remainder
+  (a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r
+   其中a_remainder+b 大于256位，我们可以有以下约束 
+  - a,n,a_remainder,a_div_n 存在mul_add_words约束 a_div_n * n + a_remainder = a
+  - b,a_remainder,a_remainder_plus_b 存在add_words约束 a_remainder + b = a_remainder_plus_b
+  - b_div_n,n,b_remainder,a_reduced_plus_b_overflow 存在mul_add_words约束 b_div_n * n + r = a_remainder_plus_b + a_remainder_plus_b_overflow << 256 （mul_add_512_gadget）
+  - a_remainder < n 约束
+  - r < n 约束
+  - n_is_zero 约束
+
+
+- MulMod 计算mulMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有a*b%n = r。我们可以将这个约束转化为a*b = n * q + r。为了约束简单我们可以有
+  a % n= a_div_n + a_remainder
+  a_remainder * b =pordut & n= b_div_n + r
+  pordut是512bit,我们将它分为两个256bit的数，pordut_hi,pordut_lo。我们可以有以下约束
+  - a,n,a_remainder,a_div_n 存在mul_add_words约束
+  - b,a_remainder,pordut_hi,pordut_lo 存在mul_add_words约束,请注意这里b*a_remainder的结果等于pordut是512bit
+  - pordut_hi,pordut_lo,n,b_div_n,r 存在mul_add_words约束,同样需要注意这里n * b_div_n + r 的结果等于pordut是512bit
+  - r < n 约束
+  - n_is_zero 约束
   
 
 - Length