|
|
|
# 布局
|
|
|
|
|
|
|
|
arithmetic 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub struct ArithmeticCircuitConfig<F> {
|
|
|
|
q_enable: Selector,
|
|
|
|
/// Tag for arithmetic operation type
|
|
|
|
tag: BinaryNumberConfig<Tag, LOG_NUM_ARITHMETIC_TAG>,
|
|
|
|
/// The operands in one row, splitted to 2 (high and low 128-bit)
|
|
|
|
operands: [[Column<Advice>; 2]; NUM_OPERAND],
|
|
|
|
/// The 16-bit values in one row
|
|
|
|
u16s: [Column<Advice>; NUM_U16],
|
|
|
|
/// Row counter, decremented for rows in one execution state
|
|
|
|
cnt: Column<Advice>,
|
|
|
|
/// IsZero chip for column cnt
|
|
|
|
cnt_is_zero: IsZeroWithRotationConfig<F>,
|
|
|
|
}
|
|
|
|
|
|
|
|
pub enum Tag {
|
|
|
|
#[default]
|
|
|
|
Nil,
|
|
|
|
Add,
|
|
|
|
Sub,
|
|
|
|
Mul,
|
|
|
|
DivMod,
|
|
|
|
SltSgt,
|
|
|
|
SdivSmod,
|
|
|
|
Addmod,
|
|
|
|
Mulmod,
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见[here](../code-notes/binary_number_with_real_selector.rs的内容和用法.markdown)。
|
|
|
|
|
|
|
|
## 列的含义
|
|
|
|
|
|
|
|
operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b,c,overflow。u16*用来 lookup 算术中的输出如 c_hi,c_lo 属于 u128 范围。这里我们只需要保证输出值的 lookup 就好。cnt 记录某个具体算术指令的行计数器，从正数开始递减到 0。
|
|
|
|
|
|
|
|
# 约束
|
|
|
|
|
|
|
|
在 arithmetic 子电路中约束可以分为两类。
|
|
|
|
通用约束
|
|
|
|
|
|
|
|
- 约束 cnt 除零行外,当前行与下一行差值为 1
|
|
|
|
|
|
|
|
不同 Tag 对应的约束不同 **请注意我们这里所有的 u16 都是 little endian 小端编码**
|
|
|
|
|
|
|
|
- Add (含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和)
|
|
|
|
|
|
|
|
- 注：加法可以用这个
|
|
|
|
- 如果是 cnt=0 行，则 cnt_prev=1,cnt_prev_prev=0
|
|
|
|
- c_lo = u16 sum(rotation cur)
|
|
|
|
- c_hi = u16 sum(rotation prev)
|
|
|
|
- carry hi is bool
|
|
|
|
- carry lo is bool
|
|
|
|
- c lo + carry lo \* 2^128 = a lo + b lo
|
|
|
|
- c hi + carry hi \* 2^128 = a hi + b hi + carry lo
|
|
|
|
|
|
|
|
- Sub (含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和)
|
|
|
|
|
|
|
|
- 注：减法，LT，GT 都可以用这个
|
|
|
|
- c_lo = u16 sum(rotation cur)
|
|
|
|
- c_hi = u16 sum(rotation prev)
|
|
|
|
- carry hi is bool
|
|
|
|
- carry lo is bool
|
|
|
|
- a_lo + carrry_lo \* 2^128 = b_lo + c_lo
|
|
|
|
- a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi
|
|
|
|
- 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b
|
|
|
|
|
|
|
|
- Div_Mod (a\*b+c=d 同时约束 c 小于 b)
|
|
|
|
|
|
|
|
if tag is div, (a,b,c,d) = (push, pop2, pop1 - push \* pop2, pop1)
|
|
|
|
|
|
|
|
if tag is mod, (a,b,c,d) = (if pop2 is zero{0}else{pop1/pop2},pop2,if pop2 is zero{pop1}else{push},pop1)
|
|
|
|
|
|
|
|
- define t0 = a0 \* b0
|
|
|
|
- define t1 = a0 \* b1 + a1 \* b0
|
|
|
|
- define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
|
|
|
|
- define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2
|
|
|
|
- define t_lo=t0+(t1)\*2^64
|
|
|
|
- define t_hi=(t2)+(t3)\*2^64
|
|
|
|
- define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
|
|
|
|
- define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128
|
|
|
|
- 如果是 0 行，约束 num_row is 8,并且约束 cnt 自增的有效性
|
|
|
|
- a_lo = u16 sum(rotation cur)
|
|
|
|
- a_hi = u16 sum(rotation -1)
|
|
|
|
- b_lo = u16 sum(rotation -2)
|
|
|
|
- b_hi = u16 sum(rotation -3)
|
|
|
|
- c_lo = u16 sum(rotation -4)
|
|
|
|
- c_hi = u16 sum(rotation -5)
|
|
|
|
- d_lo = u16 sum(rotation -6)
|
|
|
|
- d_hi = u16 sum(rotation -7)
|
|
|
|
- (t_lo+c_lo-car_lo\*2^128) - d_lo
|
|
|
|
- (t_hi+c_hi+car_lo-car_hi\*2^128) - d_hi
|
|
|
|
- residue < divisor when divisor != 0
|
|
|
|
- overflow == 0 for opcode DIV/MOD overflow = carry*hi + a1 * b3 + a2 _ b2 + a3 _ b1 + a2 _ b3 + a3 _ b2 + a3 \_ b3
|
|
|
|
- if tag is div 约束 a - a \* (1.expr() - divisor_is_zero.expr()) a 是 core gadget push value
|
|
|
|
- is tag is mod 约束 c - c \* (1.expr() - divisor_is_zero.expr()) c 是 core gadget push value
|
|
|
|
|
|
|
|
- Mul(需要 6 行对 a,b,c lookup ) 其中 operand0 是 a,operand1 是 b
|
|
|
|
|
|
|
|
- define t0 = a0 \* b0
|
|
|
|
- define t1 = a0 \* b1 + a1 \* b0
|
|
|
|
- define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
|
|
|
|
- define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2
|
|
|
|
- define t_lo=t0+(t1)\*2^64
|
|
|
|
- define t_hi=(t2)+(t3)\*2^64
|
|
|
|
- define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
|
|
|
|
- define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128
|
|
|
|
- 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性
|
|
|
|
- a_lo = u16 sum(rotation cur)
|
|
|
|
- a_hi = u16 sum(rotation -1)
|
|
|
|
- b_lo = u16 sum(rotation -2)
|
|
|
|
- b_hi = u16 sum(rotation -3)
|
|
|
|
- c_lo = u16 sum(rotation -4)
|
|
|
|
- c_hi = u16 sum(rotation -5)
|
|
|
|
- （t_lo-car_lo\*2^128） -（c_lo）
|
|
|
|
- （t_hi+car_lo-car_hi\*2^128）- （c_hi）
|
|
|
|
|
|
|
|
- Slt_Sgt (以下操作待写)
|
|
|
|
|
|
|
|
- Sdiv_Smod（这里我们还是使用 a\*b+c=d 的公式来进行核心约束，值关注的是对有符号的数进行操作，我们需要运用到补码的知识。）
|
|
|
|
对有符号整数进行计算时。所有的输入值都由 core circuit 传递。我们在这里约束传递值如下
|
|
|
|
|
|
|
|
```
|
|
|
|
if tag is sdiv
|
|
|
|
- a = push
|
|
|
|
- b = pop2
|
|
|
|
- c = if is*pop1_neg{get_neg(pop1_abs - push_abs * pop2*abs)}else{pop1_abs - push_abs * pop2_abs}
|
|
|
|
- d = pop1
|
|
|
|
if tag is smod
|
|
|
|
- a = if is_pop2_zero{0}else if is_pop1_neg == is_pop2_neg {pop1_abs / pop2_abs}else{get_neg(pop1_abs / pop2_abs)}
|
|
|
|
- b = pop2
|
|
|
|
- c = if pop2.is_zero() { pop1 } else { push }
|
|
|
|
- d = pop1
|
|
|
|
|
|
|
|
constraints
|
|
|
|
- a_abs,b_abs,c_abs,d_abs
|
|
|
|
- mul_add_words
|
|
|
|
- c lt b
|
|
|
|
- d is_signed_overflow
|
|
|
|
- a,b,c is zero
|
|
|
|
|
|
|
|
```
|
|
|
|
|
|
|
|
- Addmod
|
|
|
|
|
|
|
|
- Mulmod
|
|
|
|
|
|
|
|
- Normallength
|
|
|
|
|
|
|
|
输入：length,offset,data_size
|
|
|
|
|
|
|
|
输出：normal_length, zero_length
|
|
|
|
|
|
|
|
计算方式：
|
|
|
|
|
|
|
|
以codecopy为例，length:为要copy的长度，offset为bytecode偏移量(即复制起始位置)，data_size为bytecode的总长度
|
|
|
|
|
|
|
|
```rust
|
|
|
|
fn normal_length(length: u64, offset: u64, data_size: u64) -> (normal_length: u64, zero_length: u64) {
|
|
|
|
if offset > data_size {
|
|
|
|
return 0, length
|
|
|
|
} else if offset + length < data_size {
|
|
|
|
return length,0
|
|
|
|
}else{
|
|
|
|
return data_size-offset, offset+length-data_size
|
|
|
|
}
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
# 实现 arithmetic 子电路中 Add 例子
|
|
|
|
|
|
|
|
如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub(crate) trait OperationGadget<F: Field> {
|
|
|
|
const NAME: &'static str;
|
|
|
|
const TAG: Tag;
|
|
|
|
const NUM_ROW: usize;
|
|
|
|
|
|
|
|
fn constraints(
|
|
|
|
config: &OperationConfig<F>,
|
|
|
|
meta: &mut VirtualCells<F>,
|
|
|
|
) -> Vec<(&'static str, Expression<F>)>;
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
接口实现见代码，路径 `zkevm-circuits/src/arithmetic_circuit/operation` |
|
|
|
# 布局
|
|
|
|
|
|
|
|
arithmetic 子电路的设计包含如下几列。我们重点关注 operand*与 u16*列，
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub struct ArithmeticCircuitConfig<F> {
|
|
|
|
q_enable: Selector,
|
|
|
|
/// Tag for arithmetic operation type
|
|
|
|
tag: BinaryNumberConfig<Tag, LOG_NUM_ARITHMETIC_TAG>,
|
|
|
|
/// The operands in one row, splitted to 2 (high and low 128-bit)
|
|
|
|
operands: [[Column<Advice>; 2]; NUM_OPERAND],
|
|
|
|
/// The 16-bit values in one row
|
|
|
|
u16s: [Column<Advice>; NUM_U16],
|
|
|
|
/// Row counter, decremented for rows in one execution state
|
|
|
|
cnt: Column<Advice>,
|
|
|
|
/// IsZero chip for column cnt
|
|
|
|
cnt_is_zero: IsZeroWithRotationConfig<F>,
|
|
|
|
}
|
|
|
|
|
|
|
|
pub enum Tag {
|
|
|
|
#[default]
|
|
|
|
Nil,
|
|
|
|
Add,
|
|
|
|
Sub,
|
|
|
|
Mul,
|
|
|
|
DivMod,
|
|
|
|
SltSgt,
|
|
|
|
SdivSmod,
|
|
|
|
Addmod,
|
|
|
|
Mulmod,
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见[here](../code-notes/binary_number_with_real_selector.rs的内容和用法.markdown)。
|
|
|
|
|
|
|
|
## 列的含义
|
|
|
|
|
|
|
|
operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b,c,overflow。u16*用来 lookup 算术中的输出如 c_hi,c_lo 属于 u128 范围。这里我们只需要保证输出值的 lookup 就好。cnt 记录某个具体算术指令的行计数器，从正数开始递减到 0。
|
|
|
|
|
|
|
|
# 约束
|
|
|
|
|
|
|
|
在 arithmetic 子电路中约束可以分为两类。
|
|
|
|
通用约束
|
|
|
|
|
|
|
|
- 约束 cnt 除零行外,当前行与下一行差值为 1
|
|
|
|
|
|
|
|
不同 Tag 对应的约束不同 **请注意我们这里所有的 u16 都是 little endian 小端编码**
|
|
|
|
|
|
|
|
- Add (含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和)
|
|
|
|
|
|
|
|
- 注：加法可以用这个
|
|
|
|
- 如果是 cnt=0 行，则 cnt_prev=1,cnt_prev_prev=0
|
|
|
|
- c_lo = u16 sum(rotation cur)
|
|
|
|
- c_hi = u16 sum(rotation prev)
|
|
|
|
- carry hi is bool
|
|
|
|
- carry lo is bool
|
|
|
|
- c lo + carry lo \* 2^128 = a lo + b lo
|
|
|
|
- c hi + carry hi \* 2^128 = a hi + b hi + carry lo
|
|
|
|
|
|
|
|
- Sub (含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和)
|
|
|
|
|
|
|
|
- 注：减法，LT，GT 都可以用这个
|
|
|
|
- c_lo = u16 sum(rotation cur)
|
|
|
|
- c_hi = u16 sum(rotation prev)
|
|
|
|
- carry hi is bool
|
|
|
|
- carry lo is bool
|
|
|
|
- a_lo + carrry_lo \* 2^128 = b_lo + c_lo
|
|
|
|
- a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi
|
|
|
|
- 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b
|
|
|
|
|
|
|
|
- Div_Mod (a\*b+c=d 同时约束 c 小于 b)
|
|
|
|
|
|
|
|
if tag is div, (a,b,c,d) = (push, pop2, pop1 - push \* pop2, pop1)
|
|
|
|
|
|
|
|
if tag is mod, (a,b,c,d) = (if pop2 is zero{0}else{pop1/pop2},pop2,if pop2 is zero{pop1}else{push},pop1)
|
|
|
|
|
|
|
|
- define t0 = a0 \* b0
|
|
|
|
- define t1 = a0 \* b1 + a1 \* b0
|
|
|
|
- define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
|
|
|
|
- define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2
|
|
|
|
- define t_lo=t0+(t1)\*2^64
|
|
|
|
- define t_hi=(t2)+(t3)\*2^64
|
|
|
|
- define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
|
|
|
|
- define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128
|
|
|
|
- 如果是 0 行，约束 num_row is 8,并且约束 cnt 自增的有效性
|
|
|
|
- a_lo = u16 sum(rotation cur)
|
|
|
|
- a_hi = u16 sum(rotation -1)
|
|
|
|
- b_lo = u16 sum(rotation -2)
|
|
|
|
- b_hi = u16 sum(rotation -3)
|
|
|
|
- c_lo = u16 sum(rotation -4)
|
|
|
|
- c_hi = u16 sum(rotation -5)
|
|
|
|
- d_lo = u16 sum(rotation -6)
|
|
|
|
- d_hi = u16 sum(rotation -7)
|
|
|
|
- (t_lo+c_lo-car_lo\*2^128) - d_lo
|
|
|
|
- (t_hi+c_hi+car_lo-car_hi\*2^128) - d_hi
|
|
|
|
- residue < divisor when divisor != 0
|
|
|
|
- overflow == 0 for opcode DIV/MOD overflow = carry*hi + a1 * b3 + a2 _ b2 + a3 _ b1 + a2 _ b3 + a3 _ b2 + a3 \_ b3
|
|
|
|
- if tag is div 约束 a - a \* (1.expr() - divisor_is_zero.expr()) a 是 core gadget push value
|
|
|
|
- is tag is mod 约束 c - c \* (1.expr() - divisor_is_zero.expr()) c 是 core gadget push value
|
|
|
|
|
|
|
|
- Mul(需要 6 行对 a,b,c lookup ) 其中 operand0 是 a,operand1 是 b
|
|
|
|
|
|
|
|
- define t0 = a0 \* b0
|
|
|
|
- define t1 = a0 \* b1 + a1 \* b0
|
|
|
|
- define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
|
|
|
|
- define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2
|
|
|
|
- define t_lo=t0+(t1)\*2^64
|
|
|
|
- define t_hi=(t2)+(t3)\*2^64
|
|
|
|
- define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
|
|
|
|
- define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128
|
|
|
|
- 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性
|
|
|
|
- a_lo = u16 sum(rotation cur)
|
|
|
|
- a_hi = u16 sum(rotation -1)
|
|
|
|
- b_lo = u16 sum(rotation -2)
|
|
|
|
- b_hi = u16 sum(rotation -3)
|
|
|
|
- c_lo = u16 sum(rotation -4)
|
|
|
|
- c_hi = u16 sum(rotation -5)
|
|
|
|
- （t_lo-car_lo\*2^128） -（c_lo）
|
|
|
|
- （t_hi+car_lo-car_hi\*2^128）- （c_hi）
|
|
|
|
|
|
|
|
- Slt_Sgt (以下操作待写)
|
|
|
|
|
|
|
|
- Sdiv_Smod（这里我们还是使用 a\*b+c=d 的公式来进行核心约束，值关注的是对有符号的数进行操作，我们需要运用到补码的知识。）
|
|
|
|
对有符号整数进行计算时。所有的输入值都由 core circuit 传递。我们在这里约束传递值如下
|
|
|
|
|
|
|
|
```
|
|
|
|
if tag is sdiv
|
|
|
|
- a = push
|
|
|
|
- b = pop2
|
|
|
|
- c = if is*pop1_neg{get_neg(pop1_abs - push_abs * pop2*abs)}else{pop1_abs - push_abs * pop2_abs}
|
|
|
|
- d = pop1
|
|
|
|
if tag is smod
|
|
|
|
- a = if is_pop2_zero{0}else if is_pop1_neg == is_pop2_neg {pop1_abs / pop2_abs}else{get_neg(pop1_abs / pop2_abs)}
|
|
|
|
- b = pop2
|
|
|
|
- c = if pop2.is_zero() { pop1 } else { push }
|
|
|
|
- d = pop1
|
|
|
|
|
|
|
|
constraints
|
|
|
|
- a_abs,b_abs,c_abs,d_abs
|
|
|
|
- mul_add_words
|
|
|
|
- c lt b
|
|
|
|
- d is_signed_overflow
|
|
|
|
- a,b,c is zero
|
|
|
|
|
|
|
|
```
|
|
|
|
|
|
|
|
- Addmod
|
|
|
|
|
|
|
|
- Mulmod
|
|
|
|
|
|
|
|
- Normallength
|
|
|
|
输入：length,offset,data_size
|
|
|
|
输出：normal_length, zero_length
|
|
|
|
计算方式：
|
|
|
|
以codecopy为例，length:为要copy的长度，offset为bytecode偏移量(即复制起始位置)，data_size为bytecode的总长度
|
|
|
|
```rust
|
|
|
|
fn normal_length(length: u64, offset: u64, data_size: u64) -> (normal_length: u64, zero_length: u64) {
|
|
|
|
if offset > data_size {
|
|
|
|
return 0, length
|
|
|
|
} else if offset + length < data_size {
|
|
|
|
return length,0
|
|
|
|
}else{
|
|
|
|
return data_size-offset, offset+length-data_size
|
|
|
|
}
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
# 实现 arithmetic 子电路中 Add 例子
|
|
|
|
|
|
|
|
如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示
|
|
|
|
|
|
|
|
```rust
|
|
|
|
pub(crate) trait OperationGadget<F: Field> {
|
|
|
|
const NAME: &'static str;
|
|
|
|
const TAG: Tag;
|
|
|
|
const NUM_ROW: usize;
|
|
|
|
|
|
|
|
fn constraints(
|
|
|
|
config: &OperationConfig<F>,
|
|
|
|
meta: &mut VirtualCells<F>,
|
|
|
|
) -> Vec<(&'static str, Expression<F>)>;
|
|
|
|
}
|
|
|
|
```
|
|
|
|
|
|
|
|
接口实现见代码，路径 `zkevm-circuits/src/arithmetic_circuit/operation` |
