zkevm-docs/12-exp.markdown

-用于处理EXP指令以及电路中的exp运算的子电路
+`EXP` 指令计算一个数的指数，例如 base^index，本文处理EXP指令以及电路中exp运算的子电路。
 
 # 设计
 
@@ -7,7 +7,6 @@
 ### Witness设计
 
 ```rust
-
 #[derive(Clone, Debug, Serialize)]
 pub struct Row {
     // type of row, one of zero, one, SQUARE or Bit
@@ -34,13 +33,11 @@ pub enum Tag {
     Bit0, // index & 1 = 0
     Bit1, // index & 1 = 1
 }
-
-```  
+```
 
 ### Circuit Column 设计
 
 ```rust
-
 #[derive(Clone)]
 pub struct ExpCircuitConfig<F: Field> {
     q_enable: Selector,
@@ -61,52 +58,151 @@ pub struct ExpCircuitConfig<F: Field> {
     /// arithmetic table for lookup
     arithmetic_table: ArithmeticTable,
 }
-
 ```
 
 ## Witness生成算法设计
 
 ```rust
-    pub fn from_operands(
-        base: U256,
-        index: U256,
-    ) -> (U256, Vec<Self>, Vec<arithmetic::Row>) 
-
+pub fn from_operands(
+    base: U256,
+    index: U256,
+) -> (U256, Vec<Self>, Vec<arithmetic::Row>) {
+  let base_hi = base >> 128;
+  			...
+        exp_rows.push(zero_row);
+        if index.is_zero() {
+            return (power_value, exp_rows, mul_row);
+        }
+        let one_row = Self {
+          ...
+        };
+        exp_rows.push(one_row);
+        let mut div = index.clone();
+        let mut rem = U256::zero();
+        loop {
+            // first generate bit0/1  row
+            (div, rem) = div.div_mod(U256::from(2));
+            // then generate bit0/1
+            let pre_pre_id = exp_rows.len() - 2;
+            let pre_id = exp_rows.len() - 1;
+            let (bit_index_hi, bit_index_lo, bit_val) = if rem.is_zero() {
+                (
+                    exp_rows[pre_pre_id].index_hi,
+                    exp_rows[pre_pre_id].index_lo,
+                    (exp_rows[pre_pre_id].power_hi << 128).add(exp_rows[pre_pre_id].power_lo),
+                )
+            } else {
+                let pre_pre_index_hi = exp_rows[pre_pre_id].index_hi;
+                let pre_pre_index_lo = exp_rows[pre_pre_id].index_lo;
+                let pre_index_hi = exp_rows[pre_id].index_hi;
+                let pre_index_lo = exp_rows[pre_id].index_lo;
+                let pre_pre_val =
+                    (exp_rows[pre_pre_id].power_hi << 128).add(exp_rows[pre_pre_id].power_lo);
+                let pre_val = (exp_rows[pre_id].power_hi << 128).add(exp_rows[pre_id].power_lo);
+                let (pre_pre_val_mul_pre_val_rows, pre_pre_val_mul_pre_val_result) =
+                    operation::mul::gen_witness(vec![pre_pre_val, pre_val]);
+                mul_row.extend(pre_pre_val_mul_pre_val_rows);
+                (
+                    pre_pre_index_hi.add(pre_index_hi),
+                    pre_pre_index_lo.add(pre_index_lo),
+                    pre_pre_val_mul_pre_val_result[0],
+                )
+            };
+            let bit_row = Self {
+  					...
+            if div.is_zero() {
+                break;
+            }
+          let pre_pre_id = exp_rows.len() - 2;
+            let pre_id = exp_rows.len() - 1;
+            let pre_count = exp_rows[pre_id].count;
+            // use arithmetic mul
+            // pre_pre_power * pre_pre_power
+            let pre_pre_val =
+                (exp_rows[pre_pre_id].power_hi << 128).add(exp_rows[pre_pre_id].power_lo);
+            let count = pre_count.add(U256::one());
+            let (index_hi, index_lo) = if count.eq(&U256::from(128)) {
+                (U256::one(), U256::zero())
+            } else {
+                (
+                    exp_rows[pre_pre_id].index_hi.mul(2),
+                    exp_rows[pre_pre_id].index_lo.mul(2),
+                )
+            };
+            // pre_pre_power * pre_pre_power
+            let (val_mul_val_rows, val_mul_val_result) =
+                operation::mul::gen_witness(vec![pre_pre_val, pre_pre_val]);
+            mul_row.extend(val_mul_val_rows);
+            // first generate square
+            let square_row = Self {
+                tag: Tag::Square,
+                base_hi,
+                base_lo,
+                index_hi: index_hi,
+                index_lo: index_lo,
+                count,
+                // is_high,
+                power_hi: val_mul_val_result[0] >> 128,
+                power_lo: val_mul_val_result[0].low_u128().into(),
+            };
+            exp_rows.push(square_row);
+          ...
+}
 ```
-- 入参: base为底数,index为指数
-- 返回参数: exp运算结果,exp生成witness row 数组(exp rows),使用的乘法电路运算生成的witness row(mul rows)
-- 算法: 
-    - 生成Tag::Zero 行,将其添加到exp rows中 
-    - 若index == 0,则直接返回
-    - 生成Tag::One 行, 将其添加到exp rows中
-    - 循环对 div 做2的除法和取模运算,记商为div,余数为rem
-        - 生成Tag::Bit0/Tag::Bit1 Row；其中count = (exp rows中的前一行的row)的count
-            - 若rem == 0 , 则生成Tag::Bit0 Row,将其添加到exp rows中；其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo；power hi/lo =  (exp rows中的两行前的row)的 power hi/lo
-            - 若rem == 1 , 则生成Tag::Bit1 Row,将其添加到exp rows中；其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo + (exp rows中的前一行的row)的index hi/lo；power hi/lo = (exp rows中的两行前的row)的 power hi/lo * (exp rows中的前一行的row)的 power hi/lo,调用乘法电路生成mul row,将其添加到mul rows中
-        - 若div == 0, 则中断循环
-        - 否则: 
-            - 生成Tag::SQUARE Row,将其添加到exp rows中；count = (exp rows中的前一行的row)的count + 1；若count = 128,则index hi = 1; index lo = 0; 若count <> 128,则index hi/lo = (exp rows中的两行前的row)的 index hi/lo * 2 ；power hi/lo = (exp rows中的两行前的row)的 power hi/lo 的平方,调用乘法电路生成mul row,将其添加到mul rows中；
-    - 去exp rows中最后一行的power hi/lo, 将power hi << 128 + power lo作为最终的power value, return (power value,exp rows, mul rows)
+详细代码参考`/zkevm/zkevm-circuits/src/witness/exp.rs`
+
+**入参**:
+
+- `base`: 底数
+- `index`: 指数
+
+**返回参数**:
+
+- `exp`运算结果
+- `exp`生成的witness row数组（`exp rows`）
+- 使用乘法电路运算生成的witness row（`mul rows`）
+
+**算法**:
+
+- 生成`Tag::Zero `行,将其添加到`exp rows`中 
+- 若`index == 0`,则直接返回
+- 生成`Tag::One` 行, 将其添加到`exp rows`中
+- 循环对` div` 做2的除法和取模运算,记商为`div`,余数为`rem`
+  - 生成`Tag::Bit0/Tag::Bit1 Row`；其中count = (exp rows中的前一行的row)的count
+    - 若`rem == 0` , 则生成`Tag::Bit0 Row`,将其添加到`exp rows`中；其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo；power hi/lo =  (exp rows中的两行前的row)的 `power hi/lo`
+    - 若`rem == 1` , 则生成`Tag::Bit1 Row`,将其添加到`exp rows`中；其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo + (exp rows中的前一行的row)的index hi/lo；power hi/lo = (exp rows中的两行前的row)的 power hi/lo * (exp rows中的前一行的row)的 power hi/lo,调用乘法电路生成mul row,将其添加到`mul rows`中
+  - 若`div == 0`, 则中断循环
+  - 否则: 
+    - 生成`Tag::SQUARE Row`,将其添加到`exp rows`中；count = (exp rows中的前一行的row)的count + 1；若`count = 128`,`则index hi = 1`; `index lo = 0`; 若`count <> 128`,则index hi/lo = (exp rows中的两行前的row)的 index hi/lo * 2 ；power hi/lo = (exp rows中的两行前的row)的 power hi/lo 的平方,调用乘法电路生成`mul row`,将其添加到`mul rows`中；
+- 去`exp rows`中最后一行的`power hi/lo`, 将`power hi << 128 + power lo`作为最终的`power value`, `return (power value,exp rows, mul rows)`
 
 ## 门约束  
 
 ### Base hi/lo 约束
-- 若当前行的Tag为ONE,SQUARE,BIT0,BIT1, 则base hi/lo 等于前一行的base hi/lo
+- 若当前行的Tag为`ONE`、`SQUARE`、`BIT0`、`BIT1`，则`base hi/lo`等于前一行的`base hi/lo`
 
 ### Tag 约束
-- 若当前行的Tag为ZERO,则前一行的Tag为ZERO or BIT1 or BIT0
-- 若当前行的Tag为SQUARE,则前一行的Tag必为Bit0 or Bit1
-- 若当前行的Tag为ONE,则前一行的Tag必为ZERO
-- 若当前行的Tag为Bit0 or Bit1,则前一行的Tag为ONE or SQUARE
+- 若当前行的Tag为`ZERO`，则前一行的Tag为`ZERO`、`BIT1`或`BIT0`
+- 若当前行的Tag为`SQUARE`，则前一行的Tag必为`Bit0`或`Bit1`
+- 若当前行的Tag为`ONE`，则前一行的Tag必为`ZERO`
+- 若当前行的Tag为`Bit0`或`Bit1`，则前一行的Tag为`ONE`或`SQUARE`
 
 ### Count约束
-- 若当前行的Tag为ZERO,则count为0
-- 若当前行的Tag为ONE,则count为0
-- 若当前行的Tag为SQUARE,则count为前一行的count+1
-- 若当前行的Tag为Bit0 or Bit1,则count等于前一行的count
 
+- 若当前行的Tag为`ZERO`，则`count`为0
+- 若当前行的Tag为`ONE`，则`count`为0
+- 若当前行的Tag为`SQUARE`，则`count`为前一行的`count + 1`
+- 若当前行的Tag为`Bit0`或`Bit1`，则`count`等于前一行的`count`
 
 ### Index/Power约束
+
+- 若当前行的Tag为`ZERO`，则`index`为0，`power`为1
+- 若当前行的Tag为`ONE`，则`index`为1，`power`为`BASE`（底数）
+- 若当前行的Tag为`Bit0`，则`index`等于前两行的`index`，`power`等于前两行的`power`
+- 若当前行的Tag为`SQUARE`，且`count`为128，则`index hi`为1，`index lo`为0
+- 若当前行的Tag为`SQUARE`，且`count`不等于128，则`index hi/lo`等于两行前的`index hi/lo`乘以2
+- 若当前行的Tag为`Bit1`，则`index hi/lo`等于两行前的`index hi/lo`与前一行的`index hi/lo`之和
+
 - 若当前行的Tag为ZERO,则index为0,power为1,则index
 - 若当前行的Tag为ONE,则index为1,power为BASE(底数)
 - 若当前行的Tag为Bit0,则index等于前两行index,power等于前两行的power
@@ -116,8 +212,10 @@ pub struct ExpCircuitConfig<F: Field> {
 
 ## Lookup约束 
 
-### Tag为SQUARE,Power运算lookup
-若Tag为SQUARE时,power为两行前的power的平方
+**Tag为SQUARE,Power运算lookup**
+
+- 若Tag为`SQUARE`，则`power`为两行前的`power`的平方
+
+**Tag为Bit1,Power运算lookup** 
 
-### Tag为Bit1,Power运算lookup 
-若Tag为Bit1,power为两行前的power * 一行前的power 
+若Tag为`Bit1`，则`power`为两行前的`power`乘以前一行的`power`
\ No newline at end of file
\ No newline at end of file