Skip to content

GitLab

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

12 exp · Changes

Page history
feat: update docs --story=1019296 authored by chenxuanhui's avatar chenxuanhui
Hide whitespace changes
Inline Side-by-side
Showing with 136 additions and 38 deletions
zkevm-docs/12-exp.markdown
View page @ 0812eb1d
用于处理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
\ No newline at end of file
若Tag为`Bit1`，则`power`为两行前的`power`乘以前一行的`power`
\ No newline at end of file

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

京ICP备2023035722号-3

京公网安备 11010802044225号