geruiwangExp
EXP 指令计算一个数的指数，例如 base^index，本文处理EXP指令以及电路中exp运算的子电路。
Witness、Column设计
Witness设计
#[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 设计
#[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生成算法设计
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-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