zkevm-docs/8-arithmetic.markdown

@@ -60,9 +60,9 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
 
 不同 Tag 对应的约束不同
 
-- Add（在表中使用两行）
-
-  - 如果是 0 行，则 cnt_prev=1,cnt_prev_prev=0
+- 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)
   - c_hi = u16 sum(rotation prev)
   - carry hi is bool
@@ -70,19 +70,18 @@ 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
 
-- Sub_Lt_Gt (a+b=c+overflow\*2^256) (可以使用 select struct)
-
-  - 如果是 0 行，则 cnt_prev=1,cnt_prev_prev=0
+- AddWith1stConfined (含义：a+b=c+overflow\*2^256，且a的hi lo被约束为8个16bit之和) (可以使用 select struct)
+  - 注：减法，LT，GT都可以用这个
+  - a_lo = u16 sum(rotation cur)
+  - a_hi = u16 sum(rotation prev)
   - carry hi is bool
   - carry lo is bool
   - c lo + carry lo \* 2^128 = a lo + b lo
   - c hi + carry hi \* 2^128 = a hi + b hi + carry lo
-  - if tag is sub 有 c_lo = u16 sum(rotation cur),c_hi = u16 sum(rotation prev) and carry_hi iszero
-  - if tag is lt 则有 carry_hi iszero
-  - if tag is gt 则有 carry_hi 1
+  - 注意：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
   - 如果是 0 行，约束 num_row is 8,并且约束 cnt 自增的有效性
@@ -97,9 +96,9 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - (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
-
+```
 - 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
   - 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性
@@ -111,8 +110,8 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - 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）
-
-- Slt_Sgt
+```
+- Slt_Sgt (以下操作待写)
 - Sdiv_Smod
 - Addmod
 - Mulmod
@@ -132,55 +131,6 @@ pub(crate) trait OperationGadget<F: Field> {
         meta: &mut VirtualCells<F>,
     ) -> Vec<(&'static str, Expression<F>)>;
 }
-
-impl<F: Field> OperationGadget<F> for AddGadget<F> {
-    const NAME: &'static str = "Arithmetic Circuit Add";
-    const TAG: Tag = Tag::Add;
-    const NUM_ROW: usize = 2;
-
-    fn constraints(
-        config: &OperationConfig<F>,
-        meta: &mut VirtualCells<F>,
-    ) -> Vec<(&'static str, Expression<F>)> {
-        let mut constraints = vec![];
-        let a_hi = meta.query_advice(config.operand0_hi, Rotation::cur());
-        ...
-        let carry_lo = meta.query_advice(config.operand3_lo, Rotation::cur());
-        let u16_0_for_c_lo = meta.query_advice(config.u16_0, Rotation::cur());
-        ...
-        let u16_7_for_c_lo = meta.query_advice(config.u16_7, Rotation::cur());
-        let u16_sum_for_c_lo = expr_from_u16s(&[
-            u16_0_for_c_lo,
-            ...
-            u16_7_for_c_lo,
-        ]);
-        let u16_0_for_c_hi = meta.query_advice(config.u16_0, Rotation::prev());
-        ...
-        let u16_7_for_c_hi = meta.query_advice(config.u16_7, Rotation::prev());
-        let u16_sum_for_c_hi = expr_from_u16s(&[
-            u16_0_for_c_hi,
-            ...
-            u16_7_for_c_hi,
-        ]);
-        constraints.push(("c lo = u16 sum", c_lo.clone() - u16_sum_for_c_lo));
-        constraints.push(("c hi = u16 sum", c_hi.clone() - u16_sum_for_c_hi));
-        constraints.push((
-            "carry hi is bool",
-            carry_hi.clone() * (1.expr() - carry_hi.clone()),
-        ));
-        constraints.push((
-            "carry lo is bool",
-            carry_lo.clone() * (1.expr() - carry_lo.clone()),
-        ));
-        constraints.push((
-            "c lo + carry lo * 2^128 = a lo + b lo",
-            c_lo + carry_lo.clone() * pow_of_two::<F>(128) - a_lo - b_lo,
-        ));
-        constraints.push((
-            "c hi + carry hi * 2^128 = a hi + b hi + carry lo",
-            c_hi + carry_hi * pow_of_two::<F>(128) - a_hi - b_hi - carry_lo,
-        ));
-        constraints
-    }
-}
 ```
+
+接口实现见代码，路径 `zkevm-circuits/src/arithmetic_circuit/operation`