zkevm-docs/8-arithmetic.markdown

+
 # 布局
 
 arithmetic 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，
@@ -69,9 +70,7 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b
 
 - Div_Mod (a\*b+c=d 同时约束 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 t0 = a0 \* b0
@@ -82,6 +81,8 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - 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
+  
+  - constraint
   - 如果是 0 行，约束 num_row is 8,并且约束 cnt 自增的有效性
   - a_lo = u16 sum(rotation cur)
   - a_hi = u16 sum(rotation -1)
@@ -94,9 +95,7 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - (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
+  - carry_hi == 0
 
 - Mul(需要 6 行对 a,b,c lookup ) 其中 operand0 是 a,operand1 是 b
 
@@ -118,9 +117,23 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - （t_lo-car_lo\*2^128） -（c_lo）
   - （t_hi+car_lo-car_hi\*2^128）- （c_hi）
 
-- Slt_Sgt (以下操作待写)
+- 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)
+  - 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_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
 
-- Sdiv_Smod（这里我们还是使用 a\*b+c=d 的公式来进行核心约束，值关注的是对有符号的数进行操作，我们需要运用到补码的知识。）
+- Sdiv_Smod（这里我们还是使用 a\*b+c=d 的公式来进行核心约束，值的关注的是对有符号的数进行操作，我们需要运用到补码的知识。）
   对有符号整数进行计算时。所有的输入值都由 core circuit 传递。我们在这里约束传递值如下
 
 ```
@@ -145,9 +158,9 @@ constraints
 ```
 
 - Addmod
-
 - Mulmod
 
+
 - Length 
   arithmetic中的布局: 
   |tag|  cnt | operand_0_hi | operand_0_lo | operand_1_hi | operand_1_lo | 
@@ -170,7 +183,7 @@ constraints
       }
   }
   ```
-
+  
 # 实现 arithmetic 子电路中 Add 例子
 
 如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示