zkevm-docs/8-arithmetic.markdown

@@ -84,9 +84,7 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128
   ```
   - 如果是 0 行，约束 num_row is 10,并且约束 cnt 自增的有效性
-  - a_lo = u16 sum(rotation cur)
-  - a_hi = u16 sum(rotation -1)
-  - b_lo = u16 sum(rotation -2)
+  - b_lo = u16 sum(rotation -2) //请注意因为a是输入值，我们可以不对a_hi,a_lo进行range约束
   - b_hi = u16 sum(rotation -3)
   - c_lo = u16 sum(rotation -4)
   - c_hi = u16 sum(rotation -5)
@@ -153,30 +151,52 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - d = pop1
   ```
   - a_abs,b_abs,c_abs,d_abs
-  ``
+  ```
   关于补码的相关约束如下
   - x_abs_lo == lo when x >= 0
-  - x_abs_hi == hi 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()
+  - 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(),
+    * divisor_abs_word.is_neg().expr(),  这里计算的都是div情况下的变化
 
 
 - 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_div_n + a_remainder a = n * a_div_n + a_remainder
+  (a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 )
+  (a_remainder_plus_b + a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r
+   note: 其中a_remainder+b 大于256位. 我们可以有以下约束 
+```
+/// Construct the gadget that checks a * b + c == d * 2**256 + e
+/// where a, b, c, d, e are 256-bit words.
+///
+/// We execute a multi-limb multiplication as follows:
+/// a and b is divided into 4 64-bit limbs, denoted as a0~a3 and b0~b3
+/// defined t0, t1, t2, t3, t4, t5, t6:
+///   t0 = a0 * b0, // 0 - 128bit
+///   t1 = a0 * b1 + a1 * b0, //64 - 193bit 两数相加可能存在进位
+///   t2 = a0 * b2 + a2 * b0 + a1 * b1, //128 - 258bit
+///   t3 = a0 * b3 + a3 * b0 + a2 * b1 + a1 * b2, //192 - 322bit
+///   t4 = a1 * b3 + a2 * b2 + a3 * b1,
+///   t5 = a2 * b3 + a3 * b2,
+///   t6 = a3 * b3,
+
+/// Finally we just prove: 
+///   t0 + t1 * 2^64 + c_lo = e_lo + carry_0 * 2^128 // carry_0 is 65bit
+///   t2 + t3 * 2^64 + c_hi + carry_0 = e_hi + carry_1 * 2^128
+///   t4 + t5 * 2^64 + carry_1 = d_lo + carry_2 * 2^128
+///   t6 + carry_2 = d_hi
+```
   - 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,a_remainder,a_remainder_plus_b 存在add_words约束 a_remainder + b = a_remainder_plus_b + a_remainder_plus_b_overflow << 256
   - 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 约束
@@ -184,16 +204,19 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 
 
 - 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
+  a % n= a_div_n + a_remainder  -> a = n * a_div_n + a_remainder
+  a_remainder * b =product & n= b_div_n + r
+  product是512bit,我们将它分为两个256bit的数，product_hi,product_lo。我们可以有以下约束
+  - a,n,a_remainder,a_div_n 存在mul_words约束
+  - b,a_remainder,product_hi,product_lo 存在mul_add_words约束,请注意这里b*a_remainder的结果等于port是512bit.我们最后有product_hi * 2^256 + product_lo = b * a_remainder
+  - product_hi,product_lo,n,b_div_n,r 存在mul_add_words约束,同样需要注意这里n * b_div_n + r 的结果等于product是512bit.我们最后有product_hi * 2^256 + product_lo = n * b_div_n + r
+  - a_remainder < n 约束
   - r < n 约束
   - n_is_zero 约束
   
 
+
+
 - Length 
   arithmetic中的布局: