... | ... | @@ -10,7 +10,7 @@ |
|
|
|
|
|
#[derive(Clone, Debug, Serialize)]
|
|
|
pub struct Row {
|
|
|
// type of row, one of zero, one, base2 or arbitrary
|
|
|
// type of row, one of zero, one, SQUARE or Bit
|
|
|
pub tag: Tag,
|
|
|
// base of exp
|
|
|
pub base_hi: U256,
|
... | ... | @@ -20,8 +20,6 @@ pub struct Row { |
|
|
pub index_lo: U256,
|
|
|
// count of index
|
|
|
pub count: U256,
|
|
|
// whether count is equal or large than 2**128
|
|
|
pub is_high: U256,
|
|
|
// exp res
|
|
|
pub power_hi: U256,
|
|
|
pub power_lo: U256,
|
... | ... | @@ -32,9 +30,9 @@ pub enum Tag { |
|
|
#[default]
|
|
|
Zero,
|
|
|
One,
|
|
|
Base2,
|
|
|
Arbitrary0, // index & 1 = 0
|
|
|
Arbitrary1, // index & 1 = 1
|
|
|
Square,
|
|
|
Bit0, // index & 1 = 0
|
|
|
Bit1, // index & 1 = 1
|
|
|
}
|
|
|
|
|
|
```
|
... | ... | @@ -46,7 +44,7 @@ pub enum Tag { |
|
|
#[derive(Clone)]
|
|
|
pub struct ExpCircuitConfig<F: Field> {
|
|
|
q_enable: Selector,
|
|
|
/// the operation tag, zero,one,arbitrary,base2
|
|
|
/// 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],
|
... | ... | @@ -56,8 +54,6 @@ pub struct ExpCircuitConfig<F: Field> { |
|
|
pub power: [Column<Advice>; EXP_NUM_OPERAND],
|
|
|
/// count
|
|
|
pub count: Column<Advice>,
|
|
|
/// is_high
|
|
|
pub is_high: Column<Advice>,
|
|
|
/// IsZero chip for column count
|
|
|
pub count_is_zero: IsZeroWithRotationConfig<F>,
|
|
|
/// for chip to determine whether count is 128
|
... | ... | @@ -85,55 +81,52 @@ pub struct ExpCircuitConfig<F: Field> { |
|
|
- 生成Tag::Zero 行,将其添加到exp rows中
|
|
|
- 若index == 0,则直接返回
|
|
|
- 生成Tag::One 行, 将其添加到exp rows中
|
|
|
- 计算index对2的除法和取模运算,记商为div,余数为rem
|
|
|
- 如果rem == 0, 则生成 Tag::Arbitrary0 Row,将其添加到exp rows中;其中 index hi/lo = (Tag::Zero row )的index hi/lo ;power hi/lo = (Tag::Zero row)的power hi/lo;
|
|
|
- 如果rem == 1, 则生成 Tag::Arbitrary1 Row,将其添加到exp rows中;其中 index hi/lo = (Tag::Zero row 与 Tag::One row)的index hi/lo 之和,调用加法电路生成add row,将其添加到add rows中;power hi/lo = (Tag::Zero row 与 Tag::One row)的 power hi/lo之积,调用乘法电路生成mul row ,将其添加到mul rows中;
|
|
|
- 若div == 0,则直接返回
|
|
|
- 循环对 div 做2的除法和取模运算,记商为div,余数为rem
|
|
|
- 若div == 0 且 rem == 0, 则中断循环
|
|
|
- 生成Tag::Bit0/Tag::Bit1 Row;其中count = (exp rows中的前一行的row)的count, is_high = (exp rows中的前一行的row)的is_high
|
|
|
- 若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, 调用加法电路生成add row,将其添加到add rows中;power hi/lo = (exp rows中的两行前的row)的 power hi/lo * (exp rows中的前一行的row)的 power hi/lo,调用乘法电路生成mul row,将其添加到mul rows中
|
|
|
- 若div == 0, 则中断循环
|
|
|
- 否则:
|
|
|
- 生成Tag::Base2 Row,将其添加到exp rows中;其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo * 2 ,调用乘法电路生成mul row,将其添加到mul rows中;power hi/lo = (exp rows中的两行前的row)的 power hi/lo 的平方,调用乘法电路生成mul row,将其添加到mul rows中;count = (exp rows中的前一行的row)的count + 1;
|
|
|
- 生成Tag::SQUARE Row,将其添加到exp rows中;其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo * 2 ,调用乘法电路生成mul row,将其添加到mul rows中;power hi/lo = (exp rows中的两行前的row)的 power hi/lo 的平方,调用乘法电路生成mul row,将其添加到mul rows中;count = (exp rows中的前一行的row)的count + 1;
|
|
|
- 若count == 0 ,则is_high = 0
|
|
|
- 若count == 128 ,则is_high = 1
|
|
|
- 否则 is_high = (exp rows中的两行前的row)的is_high
|
|
|
- 生成Tag::Arbitrary0/Tag::Arbitrary1 Row;其中count = (exp rows中的前一行的row)的count, is_high = (exp rows中的前一行的row)的is_high
|
|
|
- 若rem == 0 , 则生成Tag::Arbitrary0 Row,将其添加到exp rows中;其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo;power hi/lo = (exp rows中的两行前的row)的 power hi/lo
|
|
|
- 若rem == 1 , 则生成Tag::Arbitrary1 Row,将其添加到exp rows中;其中index hi/lo = (exp rows中的两行前的row)的 index hi/lo + (exp rows中的前一行的row)的index hi/lo, 调用加法电路生成add row,将其添加到add rows中;power hi/lo = (exp rows中的两行前的row)的 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, add rows)
|
|
|
|
|
|
## 门约束
|
|
|
|
|
|
### Base hi/lo 约束
|
|
|
- 若当前行的Tag为ONE,SQUARE,BIT0,BIT1, 则base hi/lo 等于前一行的base hi/lo
|
|
|
|
|
|
### Tag 约束
|
|
|
- 若当前行的Tag为ZERO,则前一行的Tag也为ZERO
|
|
|
- 若当前行的Tag为BASE2,则前一行的Tag必为ARBITRARY0 or ARBITRARY1
|
|
|
- 若当前行的Tag为ARBITRARY0 or ARBITRARY1,则前一行的Tag为ONE or BASE2
|
|
|
- 若当前行的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
|
|
|
|
|
|
### Count约束
|
|
|
- 若当前行的Tag为ZERO,则count为0
|
|
|
- 若当前行的Tag为BASE2,则count为前一行的count+1
|
|
|
- 若当前行的Tag为ARBITRARY0 or ARBITRARY1,则count等于前一行的count
|
|
|
- count不等于256
|
|
|
- 若当前行的Tag为ONE,则count为0
|
|
|
- 若当前行的Tag为SQUARE,则count为前一行的count+1
|
|
|
- 若当前行的Tag为Bit0 or Bit1,则count等于前一行的count
|
|
|
|
|
|
### Is_high约束
|
|
|
- 若当前行的count为0,则is_high为0
|
|
|
- 若当前行的count为128,则is_high为1
|
|
|
- 若当前行的count不为0和128,则is_high等于前一行的is_high
|
|
|
|
|
|
### Index/Power约束
|
|
|
- 若当前行的Tag为ZERO,则index为0,power为1,则index
|
|
|
- 若当前行的Tag为ONE,则index为1,power为BASE(底数)
|
|
|
- 若当前行的Tag为ARBITRARY0,则index等于前两行index,power等于前两行的power
|
|
|
- 若当前行的Tag为BASE2,且count为128,则index hi为1,index lo为0
|
|
|
- 若当前行的Tag为Bit0,则index等于前两行index,power等于前两行的power
|
|
|
- 若当前行的Tag为SQUARE,且count为128,则index hi为1,index lo为0
|
|
|
|
|
|
## Lookup约束
|
|
|
|
|
|
### Tag为BASE2,Index运算lookup
|
|
|
若Tag为BASE2时,index 等于两行前的index * 2,若count为128时,则index hi为1,index为0
|
|
|
### Tag为SQUARE,Index运算lookup
|
|
|
若Tag为SQUARE时,index 等于两行前的index * 2
|
|
|
|
|
|
### Tag为BASE2,Power运算lookup
|
|
|
若Tag为BASE2时,power为两行前的power的平方
|
|
|
### Tag为SQUARE,Power运算lookup
|
|
|
若Tag为SQUARE时,power为两行前的power的平方
|
|
|
|
|
|
### Tag为ARBITRARY1,Index运算lookup
|
|
|
若Tag为ARBITRARY1,index为两行前的index + 一行前的index
|
|
|
### Tag为ARBITRARY1,Power运算lookup
|
|
|
若Tag为ARBITRARY1,power为两行前的power * 一行前的power |
|
|
\ No newline at end of file |
|
|
### Tag为Bit1,Index运算lookup
|
|
|
若Tag为Bit1,index为两行前的index + 一行前的index
|
|
|
### Tag为Bit1,Power运算lookup
|
|
|
若Tag为Bit1,power为两行前的power * 一行前的power |
|
|
\ No newline at end of file |