gzxu · 348fc1dd
Hide whitespace changes
Inline Side-by-side

Showing with 222 additions and 222 deletions

zkevm-docs/12-exp.markdown zkevm-docs/12-exp.markdown +222 -222

No files found.
--- a/zkevm-docs/12-exp.markdown
+++ b/zkevm-docs/12-exp.markdown
 # Exp
 `EXP` 指令计算一个数的指数，例如 base^index，本文处理EXP指令以及电路中exp运算的子电路。
 ## Witness、Column设计  
 ### Witness设计
 ```rust
 #[derive(Clone, Debug, Serialize)]
 pub struct Row {
    // type of row, one of zero, one, SQUARE or Bit
    pub tag: Tag,
    // base of exp
    pub base_hi: U256,
    pub base_lo: U256,
    // index of exp
    pub index_hi: U256,
    pub index_lo: U256,
    // count of index
    pub count: U256,
    // exp res
    pub power_hi: U256,
    pub power_lo: U256,
 }
 #[derive(Clone, Copy, Debug, Default, Serialize, EnumIter, EnumString)]
 pub enum Tag {
    #[default]
    Zero,
    One,
    Square,
    Bit0, // index & 1 = 0
    Bit1, // index & 1 = 1
 }
 ```
 ### Circuit Column 设计
 ```rust
 #[derive(Clone)]
 pub struct ExpCircuitConfig<F: Field> {
    q_enable: Selector,
    /// the operation tag, zero,one,Bit,SQUARE
    pub tag: BinaryNumberConfig<Tag, LOG_NUM_EXP_TAG>,
    /// base hi , base lo
    pub base: [Column<Advice>; EXP_NUM_OPERAND],
    /// index hi, index lo
    pub index: [Column<Advice>; EXP_NUM_OPERAND],
    /// power hi, power lo
    pub power: [Column<Advice>; EXP_NUM_OPERAND],
    /// count
    pub count: Column<Advice>,
    /// IsZero chip for column count
    pub count_is_zero: IsZeroWithRotationConfig<F>,
    /// for chip to determine whether count is 128
    pub count_is_128: IsZeroConfig<F>,
    /// arithmetic table for lookup
    arithmetic_table: ArithmeticTable,
 }
 ```
 ## Witness生成算法设计
 ```rust
 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);
          ...
 }
 ```
 详细代码参考`/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 约束
 - 若当前行的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`或`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
 - 若当前行的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 之和
-## Lookup约束 
+### Lookup约束 
 **Tag为SQUARE,Power运算lookup**
 - 若Tag为`SQUARE`，则`power`为两行前的`power`的平方
 **Tag为Bit1,Power运算lookup** 
 若Tag为`Bit1`，则`power`为两行前的`power`乘以前一行的`power`
\ No newline at end of file