zkevm-docs/8-arithmetic.markdown

@@ -4,28 +4,16 @@ arithmetic 子电路的设计包含如下几列。我们重点关注 operand*与
 
 ```rust
 pub struct ArithmeticCircuitConfig<F> {
-    // TODO use table to let core lookup
     q_enable: Selector,
-    // arithmetic table for lookup starts
-    tag: BinaryNumberConfig<Tag, 3>, //todo not use 3
+    /// Tag for arithmetic operation type
+    tag: BinaryNumberConfig<Tag, LOG_NUM_ARITHMETIC_TAG>,
+    /// The operands in one row, splitted to 2 (high and low 128-bit)
+    operands: [[Column<Advice>; 2]; NUM_OPERAND],
+    /// The 16-bit values in one row
+    u16s: [Column<Advice>; NUM_U16],
+    /// Row counter, decremented for rows in one execution state
     cnt: Column<Advice>,
-    operand0_hi: Column<Advice>,
-    operand0_lo: Column<Advice>,
-    operand1_hi: Column<Advice>,
-    operand1_lo: Column<Advice>,
-    operand2_hi: Column<Advice>,
-    operand2_lo: Column<Advice>,
-    operand3_hi: Column<Advice>,
-    operand3_lo: Column<Advice>,
-    // arithmetic table for lookup ends
-    u16_0: Column<Advice>,
-    u16_1: Column<Advice>,
-    u16_2: Column<Advice>,
-    u16_3: Column<Advice>,
-    u16_4: Column<Advice>,
-    u16_5: Column<Advice>,
-    u16_6: Column<Advice>,
-    u16_7: Column<Advice>,
+    /// IsZero chip for column cnt
     cnt_is_zero: IsZeroWithRotationConfig<F>,
 }
 
@@ -33,15 +21,13 @@ pub enum Tag {
     #[default]
     Nil,
     Add,
-    Addmod,
-    Mul,
-    Mulmod,
-    Lt,
-    Gt,
-    Slt,
-    Sgt,
     Sub,
+    Mul,
     DivMod,
+    SltSgt,
+    SdivSmod,
+    Addmod,
+    Mulmod,
 }
 ```
 
@@ -71,15 +57,15 @@ 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 之和)
+- Sub (含义：a-b=c，且 a 的 hi lo 被约束为 8 个 16bit 之和)
 
   - 注：减法，LT，GT 都可以用这个
-  - a_lo = u16 sum(rotation cur)
-  - a_hi = u16 sum(rotation prev)
+  - c_lo = u16 sum(rotation cur)
+  - c_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
+  - a_lo + carrry_lo \* 2^128 = b_lo + c_lo
+  - a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi
   - 注意：carry_hi=1 等价于 b>c; carry_hi=0 等价于 b<=c
 
 - Div_Mod (a\*b+c=d 同时约束 c 小于 b)
@@ -133,7 +119,31 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b
   - （t_hi+car_lo-car_hi\*2^128）- （c_hi）
 
 - Slt_Sgt (以下操作待写)
-- Sdiv_Smod
+
+- Sdiv_Smod（这里我们还是使用 a\*b+c=d 的公式来进行核心约束，值关注的是对有符号的数进行操作，我们需要运用到补码的知识。）
+  对有符号整数进行计算时。所有的输入值都由 core circuit 传递。我们在这里约束传递值如下
+
+```
+  if tag is sdiv
+  - a = push
+  - b = pop2
+  - c = if is*pop1_neg{get_neg(pop1_abs - push_abs * pop2*abs)}else{pop1_abs - push_abs * pop2_abs}
+  - d = pop1
+    if tag is smod
+  - a = if is_pop2_zero{0}else if is_pop1_neg == is_pop2_neg {pop1_abs / pop2_abs}else{get_neg(pop1_abs / pop2_abs)}
+  - b = pop2
+  - c = if pop2.is_zero() { pop1 } else { push }
+  - d = pop1
+
+constraints
+  - a_abs,b_abs,c_abs,d_abs
+  - mul_add_words
+  - c lt b
+  - d is_signed_overflow
+  - a,b,c is zero
+
+```
+
 - Addmod
 - Mulmod