zkevm-docs/8-arithmetic.markdown

@@ -76,8 +76,9 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 
 我们有(a-d)/b = c ==> c * b + d = a 同时约束 d 小于 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)
+
+if tag is div, (a,b,c,d) = (pop1,pop2,push,pop1 - push * pop2) (push, pop2, pop1 - push \* pop2, pop1)
+if tag is mod, (a,b,c,d) = (pop1 ,pop2 , if pop2 is zero{zero}else{pop1 / pop2} ,if pop2 is zero{zero}else{push})
 
 define
 a * b + c = d
@@ -219,6 +220,10 @@ a % n= a_div_n + a_remainder a = n * a_div_n + a_remainder
 ///   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
 ```
   - 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 + a_remainder_plus_b_overflow << 256