zkevm-docs/8-arithmetic.markdown

@@ -60,7 +60,8 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 
 不同 Tag 对应的约束不同
 
-- AddWith3rdConfined (含义：a+b=c+overflow\*2^256，且c的hi lo被约束为8个16bit之和)
+- AddWith3rdConfined (含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和)
+
   - 注：加法可以用这个
   - 如果是 cnt=0 行，则 cnt_prev=1,cnt_prev_prev=0
   - c_lo = u16 sum(rotation cur)
@@ -70,8 +71,9 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - c lo + carry lo \* 2^128 = a lo + b lo
   - c hi + carry hi \* 2^128 = a hi + b hi + carry lo
 
-- AddWith1stConfined (含义：a+b=c+overflow\*2^256，且a的hi lo被约束为8个16bit之和) (可以使用 select struct)
-  - 注：减法，LT，GT都可以用这个
+- AddWith1stConfined (含义：a+b=c+overflow\*2^256，且 a 的 hi lo 被约束为 8 个 16bit 之和)
+
+  - 注：减法，LT，GT 都可以用这个
   - a_lo = u16 sum(rotation cur)
   - a_hi = u16 sum(rotation prev)
   - carry hi is bool
@@ -81,9 +83,19 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - 注意：carry_hi=1 等价于 b>c; carry_hi=0 等价于 b<=c
 
 - Div_Mod (a\*b+c=d 同时约束 c 小于 b)
-```
-  - define t_lo=operand3_0*operand1_0+(operand3_0*operand1_1+operand3_1*operand1_0)*2^64
-  - define t_hi=(operand3_0*operand1_2+operand3_1*operand1_1+operand3_2*operand1_0)+(operand3_0*operand1_3+operand3_1*operand1_2+operand3_2*operand1_1+operand3_3*operand1_0)*2^64
+
+  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 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 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
   - 如果是 0 行，约束 num_row is 8,并且约束 cnt 自增的有效性
   - a_lo = u16 sum(rotation cur)
   - a_hi = u16 sum(rotation -1)
@@ -93,14 +105,23 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - c_hi = u16 sum(rotation -5)
   - d_lo = u16 sum(rotation -6)
   - d_hi = u16 sum(rotation -7)
-  - (t_lo+operand2_3+operand2_2*2^64-car_lo*2^128) - (operand0_3+operand0_2\*2^64)
-  - (t_hi+operand2_0+operand2_1*2^64+car_lo-car_hi*2^128) - (operand0_1+operand0_0\*2^64)
-  - 约束 c lt d
-```
+  - (t_lo+c_lo-car_lo\*2^128) - d_lo
+  - (t_hi+c_hi+car_lo-car_hi\*2^128) - d_hi
+  - residue < divisor when divisor != 0
+  - overflow == 0 for opcode DIV/MOD overflow = carry*hi + a1 * b3 + a2 _ b2 + a3 _ b1 + a2 _ b3 + a3 _ b2 + a3 \_ b3
+  - if tag is div 约束 a - a \* (1.expr() - divisor_is_zero.expr()) a 是 core gadget push value
+  - is tag is mod 约束 c - c \* (1.expr() - divisor_is_zero.expr()) c 是 core gadget push value
+
 - Mul(需要 6 行对 a,b,c lookup ) 其中 operand0 是 a,operand1 是 b
-```
-  - define t_lo=operand0_0*operand1_0+(operand0_0*operand1_1+operand0_1*operand1_0)*2^64
-  - define t_hi=(operand0_0*operand1_2+operand0_1*operand1_1+operand0_2*operand1_0)+(operand0_0*operand1_3+operand0_1*operand1_2+operand0_2*operand1_1+operand0_3*operand1_0)*2^64
+
+  - 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 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
   - 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性
   - a_lo = u16 sum(rotation cur)
   - a_hi = u16 sum(rotation -1)
@@ -108,9 +129,9 @@ 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)
-  - （t_lo-car_lo*2^128） -（operand2_3+operand2_2*2^64）
-  - （t_hi+car_lo-car_hi*2^128）- （operand2_1+operand2_0*2^64）
-```
+  - （t_lo-car_lo\*2^128） -（c_lo）
+  - （t_hi+car_lo-car_hi\*2^128）- （c_hi）
+
 - Slt_Sgt (以下操作待写)
 - Sdiv_Smod
 - Addmod