zkevm-docs/8-arithmetic.markdown

@@ -221,43 +221,51 @@ a * b + c = d
 
 ## 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 = 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位. 我们可以有以下约束 
+计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有 **(a+b)%n = r**。我们可以将这个约束转化为 **(a+b) = n * q + r**(商q可能超过256bit)。所以为了约束简单我们可以将上式转换如下：
+1.  **a % n= a_div_n + a_remainder** $\Leftrightarrow$ **a = n * a_div_n + a_remainder**
+2. **(a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 )**
+3. **(a_remainder_plus_b + a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r**
 
-```
-/// 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
-
-carry_0 = (t0 + (t1 << 64) + c_lo).saturating_sub(e_lo) >> 128
-carry_1 = (t2 + (t3 << 64) + c_hi + carry_0).saturating_sub(e_hi) >> 128
-carry_2 = (t4 + (t5 << 64) + carry_1).saturating_sub(d_lo) >> 128
-```
+那么需要具体的约束如下，对于第1个等式：
   - a,n,a_remainder,a_div_n 存在mul_add_words约束 a_div_n * n + a_remainder = a
+  - 当n!=0时候, 存在a_remainder < n 约束
+
+对于第2个等式：
   - 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 约束
-  - n_is_zero 约束
+
+对于第3个等式：
+  - 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）
+
+  - 当n!=0时候,r < n 约束
+
+### layout
+```
+// Addmod arithmetic witeness rows. (Tag::Addmod)
+// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+
+// | operand_0_hi| operand_0_lo| operand_1_hi                   | operand_1_lo                   | cnt | u16s                  |
+// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+
+// |             |             |                                |                                | 18  | rn_diff_lo            |
+// |             |             |                                |                                | 17  | rn_diff_hi            |
+// |             |             |                                |                                | 16  | carry_1               |
+// |             |             |                                |                                | 15  | carry_0               |
+// |             |             |                                |                                | 14  | b_div_n_lo            |
+// |             |             |                                |                                | 13  | b_div_n_hi            |
+// |             |             |                                |                                | 12  | r_lo                  |
+// |             |             |                                |                                | 11  | r_hi                  |
+// |             |             |                                |                                | 10  | a_remainder_plus_b_lo |
+// |             |             |                                |                                | 9   | a_remainder_plus_b_hi |
+// |             |             |                                |                                | 8   | arn_diff_lo           |
+// | b_div_n_hi  | b_div_n_lo  | a_remainder_plus_b_hi          | a_remainder_plus_b_lo          | 7   | arn_diff_hi           |
+// | rn_diff_hi  | rn_diff_lo  | carry_2                        |                                | 6   | an_carry_lo           |
+// | carry_0     | carry_1     | rn_carry_lt_hi                 | rn_carry_lt_lo                 | 5   | a_remainder_lo        |
+// | arn_diff_hi | arn_diff_lo | a_remainder_plus_b_overflow_hi | a_remainder_plus_b_overflow_lo | 4   | a_remainder_hi        |
+// | an_carry_hi | an_carry_lo | arn_carry_lt_hi                | arn_carry_lt_lo                | 3   | n_lo                  |
+// | a_div_n_hi  | a_div_n_lo  | a_remainder_hi                 | a_remainder_lo                 | 2   | n_hi                  |
+// | n_hi        | n_lo        | r_hi                           | r_lo                           | 1   | a_div_n_lo            |
+// | a_hi        | a_lo        | b_hi                           | b_lo                           | 0   | a_div_n_hi            |
+// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+
+```
+
 
 ## MulMod