maqingyuan · 838c18d0
Hide whitespace changes
Inline Side-by-side

Showing with 185 additions and 190 deletions

zkevm-docs/8-arithmetic.markdown zkevm-docs/8-arithmetic.markdown +185 -190

No files found.
--- a/zkevm-docs/8-arithmetic.markdown
+++ b/zkevm-docs/8-arithmetic.markdown
 # 布局
 arithmetic 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，
 ```rust
 pub struct ArithmeticCircuitConfig<F> {
    q_enable: Selector,
    /// 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>,
    /// IsZero chip for column cnt
    cnt_is_zero: IsZeroWithRotationConfig<F>,
 }
 pub enum Tag {
    #[default]
    Nil,
    Add,
    Sub,
    Mul,
    DivMod,
    SltSgt,
    SdivSmod,
    Addmod,
    Mulmod,
 }
 ```
 在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见[here](../code-notes/binary_number_with_real_selector.rs的内容和用法.markdown)。
 ## 列的含义
 operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b,c,overflow。u16*用来 lookup 算术中的输出如 c_hi,c_lo 属于 u128 范围。这里我们只需要保证输出值的 lookup 就好。cnt 记录某个具体算术指令的行计数器，从正数开始递减到 0。
 # 约束
 在 arithmetic 子电路中约束可以分为两类。
 通用约束
 - 约束 cnt 除零行外,当前行与下一行差值为 1
 不同 Tag 对应的约束不同 **请注意我们这里所有的 u16 都是 little endian 小端编码**
 - Add (含义：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
  - 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
 - Sub (含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和)
  - 注：减法，LT，GT 都可以用这个
  - c_lo = u16 sum(rotation cur)
  - c_hi = u16 sum(rotation prev)
  - carry hi is bool
  - carry lo is bool
  - 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 等价于 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
  - 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)
  - b_lo = u16 sum(rotation -2)
  - b_hi = u16 sum(rotation -3)
  - c_lo = u16 sum(rotation -4)
  - c_hi = u16 sum(rotation -5)
  - d_lo = u16 sum(rotation -6)
  - d_hi = u16 sum(rotation -7)
  - (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 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)
  - b_lo = u16 sum(rotation -2)
  - b_hi = u16 sum(rotation -3)
  - c_lo = u16 sum(rotation -4)
  - c_hi = u16 sum(rotation -5)
  - （t_lo-car_lo\*2^128） -（c_lo）
  - （t_hi+car_lo-car_hi\*2^128）- （c_hi）
 - Slt_Sgt (以下操作待写)
 - 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
 - Normallength
+  输入：length,offset,data_size
-  输入：length,offset,data_size
+  输出：normal_length, zero_length
+  计算方式：
-  输出：normal_length, zero_length
+      以codecopy为例，length:为要copy的长度，offset为bytecode偏移量(即复制起始位置)，data_size为bytecode的总长度
+  ```rust
-  计算方式：
+  fn normal_length(length: u64, offset: u64, data_size: u64) -> (normal_length: u64, zero_length: u64) {
+      if offset > data_size {
-  以codecopy为例，length:为要copy的长度，offset为bytecode偏移量(即复制起始位置)，data_size为bytecode的总长度
+          return 0, length
+      } else if offset + length < data_size {
-  ```rust
+          return length,0
-  fn normal_length(length: u64, offset: u64, data_size: u64) -> (normal_length: u64, zero_length: u64) {
+      }else{
-      if offset > data_size {
+          return data_size-offset, offset+length-data_size
-          return 0, length
+      }
-      } else if offset + length < data_size {
+  }
-          return length,0
+  ```
-      }else{
-          return data_size-offset, offset+length-data_size
+# 实现 arithmetic 子电路中 Add 例子
-      }
-  }
+如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示
-  ```
+```rust
-# 实现 arithmetic 子电路中 Add 例子
+pub(crate) trait OperationGadget<F: Field> {
+    const NAME: &'static str;
-如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示
+    const TAG: Tag;
+    const NUM_ROW: usize;
-```rust
-pub(crate) trait OperationGadget<F: Field> {
+    fn constraints(
-    const NAME: &'static str;
+        config: &OperationConfig<F>,
-    const TAG: Tag;
+        meta: &mut VirtualCells<F>,
-    const NUM_ROW: usize;
+    ) -> Vec<(&'static str, Expression<F>)>;
+}
-    fn constraints(
+```
-        config: &OperationConfig<F>,
-        meta: &mut VirtualCells<F>,
+接口实现见代码，路径 `zkevm-circuits/src/arithmetic_circuit/operation`
-    ) -> Vec<(&'static str, Expression<F>)>;
-}
-```
-接口实现见代码，路径 `zkevm-circuits/src/arithmetic_circuit/operation`