Skip to content

GitLab

新注册的用户请输入邮箱并保存，随后登录邮箱激活账号。后续可直接使用邮箱登录！

12 exp · Changes

Page history
feat: modify docs --story=1 authored by gzxu's avatar gzxu
Hide whitespace changes
Inline Side-by-side
Showing with 222 additions and 222 deletions
zkevm-docs/12-exp.markdown
View page @ 348fc1dd
# 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约束
**Tag为SQUARE,Power运算lookup**
- 若Tag为`SQUARE`，则`power`为两行前的`power`的平方
**Tag为Bit1,Power运算lookup**
# 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约束
**Tag为SQUARE,Power运算lookup**
- 若Tag为`SQUARE`，则`power`为两行前的`power`的平方
**Tag为Bit1,Power运算lookup**
若Tag为`Bit1`，则`power`为两行前的`power`乘以前一行的`power`
\ No newline at end of file

Copyright © 2024 ChainWeaver Org. All Rights Reserved. 版权所有。

京ICP备2023035722号-3

京公网安备 11010802044225号