zkevm-docs/8-arithmetic.markdown

@@ -68,10 +68,11 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi
   - 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b
 
-- Div_Mod (a\*b+c=d 同时约束 c 小于 b)
+- Div_Mod (我们有a/b = d + c ==> d * b + c = a 同时约束 c 小于 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
   - define t0 = a0 \* b0
   - define t1 = a0 \* b1 + a1 \* b0
@@ -82,7 +83,7 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - 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
   ```
-  - 如果是 0 行，约束 num_row is 8,并且约束 cnt 自增的有效性
+  - 如果是 0 行，约束 num_row is 10,并且约束 cnt 自增的有效性
   - a_lo = u16 sum(rotation cur)
   - a_hi = u16 sum(rotation -1)
   - b_lo = u16 sum(rotation -2)
@@ -95,15 +96,16 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - (t_hi+c_hi+car_lo-car_hi\*2^128) - d_hi
   - residue < divisor when divisor != 0
   - carry_hi == 0
+  - carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。
 
   
 
 - Mul(需要 6 行对 a,b,c lookup ) 其中 operand0 是 a,operand1 是 b
-
-  - define t0 = a0 \* b0
-  - define t1 = a0 \* b1 + a1 \* b0
-  - define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
-  - define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2
+  
+  - define t0 = a0 \* b0 （0-128bit）
+  - define t1 = a0 \* b1 + a1 \* b0 (64-193bit)
+  - define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1 (128 - 257bit)
+  - 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
@@ -115,23 +117,22 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - b_hi = u16 sum(rotation -3)
   - c_lo = u16 sum(rotation -4)
   - c_hi = u16 sum(rotation -5)
+  - carry_hi == u16 sum(rotation -6) 请注意这里我们使用的是5位u16数据的和，从define部分我们可以知道carry_hi等于322 - 256 = 66bit。
+  - carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。
   - （t_lo-car_lo\*2^128） -（c_lo）
-  - （t_hi+car_lo-car_hi\*2^128）- （c_hi）
+  - （t_hi+car_lo-car_hi\*2^128）-（c_hi）
 
 
-- Slt_Sgt (我们使用 a-b=c 的公式来约束有相同符号的内容)
-  - 比较最高u16位确定a,b符号。同时我们需要约束a_hi和b_hi等于对应的u16s_sum 
-  - 不相等时。(a_lt - b_lt)作为不相等condition，
-  - 当 a_lt == 1 时 carry == 0。a_lt == 0时，carry=1.所以有约束 1-(a_lt +  carry_hi)
+- Slt_Sgt (我们使用 a-b=c - carry<<256 的公式来约束有相同符号的内容这里我们需要注意的是，当符号相等时，我们统一按照无符号整数比较大小)``
+  - 比较a_hi,b_hi最高u16位是否小于2^15确定a,b符号。如果a_lt == 1则a为正数，否则为负数。b_lt同理。
+  - 同时我们需要约束a_hi和b_hi等于对应的u16s_sum。这里主要是为了约束我们用来判断符号的u16的正确性。 
+  - a,b符号不相等时。我们有(a_lt - b_lt)作为不相等condition，
+  - 当 a_lt == 1,a是正数,则存在carry == 0。a_lt == 0时a是负数，carry=1.所以有约束 1-(a_lt +  carry_hi)
   - c_lo = u16 sum(rotation -4)
   - c_hi = u16 sum(rotation -5)
-  - 相等时（1 -(a_lt - b_lt)）作为符号condition，与下面每一个约束相乘
-  - a,b 为正，统一condition （a_lt *  b_lt）表示如果a_lt,b_lt都等于0,则不约束下面约束
+  - a,b符号相等时,我们有(1 -(a_lt - b_lt))作为符号condition，与下面每一个约束相乘
   - a_lo + carrry_lo \* 2^128 = b_lo + c_lo
   - a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi
-  - a,b 为负，统一condition 1 - （a_lt *  b_lt）表示如果a_lt,b_lt都等于1,则不约束下面约束
-  - b_lo + carrry_lo \* 2^128 = a_lo + c_lo 
-  - b_hi + carry_hi \* 2^128 - carry_lo= a_hi + c_hi 
   - 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b