| ... | ... | @@ -48,6 +48,8 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b |
|
|
|
|
|
|
|
## Add
|
|
|
|
|
|
|
|
### 公式
|
|
|
|
|
|
|
|
含义：a+b=c+overflow\*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和
|
|
|
|
|
|
|
|
- 注：加法可以用这个
|
| ... | ... | @@ -59,8 +61,17 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b |
|
|
|
- c lo + carry lo \* 2^128 = a lo + b lo
|
|
|
|
- c hi + carry hi \* 2^128 = a hi + b hi + carry lo
|
|
|
|
|
|
|
|
### layout
|
|
|
|
|
|
|
|
| cnt | op_0_hi | op_0_lo | op_1_hi | op_1_lo | u16s |
|
|
|
|
| ---- | ------- | ------- | -------- | -------- | --------- |
|
|
|
|
| 1 | c_hi | c_lo | carry_hi | carry_lo | c_lo_u16s |
|
|
|
|
| 0 | a_hi | a_lo | b_hi | b_lo | c_hi_u16s |
|
|
|
|
|
|
|
|
## Sub
|
|
|
|
|
|
|
|
### 公式
|
|
|
|
|
|
|
|
含义：a-b=c，且 c 的 hi lo 被约束为 8 个 16bit 之和
|
|
|
|
|
|
|
|
- 注：减法，LT，GT 都可以用这个
|
| ... | ... | @@ -72,8 +83,17 @@ operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b |
|
|
|
- a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi
|
|
|
|
- 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b
|
|
|
|
|
|
|
|
### layout
|
|
|
|
|
|
|
|
| cnt | op_0_hi | op_0_lo | op_1_hi | op_1_lo | u16s |
|
|
|
|
| ---- | ------- | ------- | -------- | -------- | --------- |
|
|
|
|
| 1 | c_hi | c_lo | carry_hi | carry_lo | c_lo_u16s |
|
|
|
|
| 0 | a_hi | a_lo | b_hi | b_lo | c_hi_u16s |
|
|
|
|
|
|
|
|
## Div_Mod
|
|
|
|
|
|
|
|
### 公式
|
|
|
|
|
|
|
|
我们有(a-d)/b = c ==> c * b + d = a 同时约束 d 小于 b
|
|
|
|
```
|
|
|
|
|
| ... | ... | @@ -104,8 +124,24 @@ a * b + c = d |
|
|
|
- carry_hi == 0
|
|
|
|
- carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。
|
|
|
|
|
|
|
|
### layout
|
|
|
|
|
|
|
|
| tag | cnt | o0hi | o0lo | o1hi | o1lo | u16s |
|
|
|
|
| ------ | ---- | ----- | ----- | ---- | ---- | ------------------- |
|
|
|
|
| DivMod | 8 | | | | | carry_lo_u16s |
|
|
|
|
| DivMod | 7 | | | | | u16_sum_for_diff_lo |
|
|
|
|
| DivMod | 6 | diff | diff | lt | lt | u16_sum_for_diff_hi |
|
|
|
|
| DivMod | 5 | | | | | u16_sum_for_d_lo |
|
|
|
|
| DivMod | 4 | | | | | u16_sum_for_d_hi |
|
|
|
|
| DivMod | 3 | | | | | u16_sum_for_c_lo |
|
|
|
|
| DivMod | 2 | carry | carry | | | u16_sum_for_c_hi |
|
|
|
|
| DivMod | 1 | c | c | d | d | u16_sum_for_b_lo |
|
|
|
|
| DivMod | 0 | a | a | b | b | u16_sum_for_b_hi |
|
|
|
|
|
|
|
|
## Mul
|
|
|
|
|
|
|
|
### 公式
|
|
|
|
|
|
|
|
需要8行对 a,b,d,carry lookup,carry lookup的原因是在进行计算时carry_lo或carry需要左移128位，因为有限域的特点可能存在左移后carry_lo或carry_hi在0-128bit存在值) 其中 operand0 是 a,operand1 是 b
|
|
|
|
|
|
|
|
- define t0 = a0 \* b0 （0-128bit）
|
| ... | ... | @@ -128,8 +164,23 @@ a * b + c = d |
|
|
|
- （t_lo-car_lo\*2^128） -（c_lo）
|
|
|
|
- （t_hi+car_lo-car_hi\*2^128）-（c_hi）
|
|
|
|
|
|
|
|
### layout
|
|
|
|
|
|
|
|
| cnt | op_0_hi | op_0_lo | op_1_hi | op_1_lo | u16s |
|
|
|
|
| ---- | ------- | ------- | -------- | -------- | ------------- |
|
|
|
|
| 7 | | | | | carry_lo_u16s |
|
|
|
|
| 6 | | | | | carry_hi_u16s |
|
|
|
|
| 5 | | | | | c_lo_u16s |
|
|
|
|
| 4 | | | | | c_hi_u16s |
|
|
|
|
| 3 | | | | | b_lo_u16s |
|
|
|
|
| 2 | | | | | b_hi_u16s |
|
|
|
|
| 1 | c_hi | c_lo | carry_hi | carry_lo | a_lo_u16s |
|
|
|
|
| 0 | a_hi | a_lo | b_hi | b_lo | a_hi_u16s |
|
|
|
|
|
|
|
|
## SLT_SGT
|
|
|
|
|
|
|
|
### 公式
|
|
|
|
|
|
|
|
我们使用 a-b=c - carry<<256 的公式来约束有相同符号的内容这里我们需要注意的是，当符号相等时，我们统一按照无符号整数比较大小
|
|
|
|
- 比较a_hi,b_hi最高u16位是否小于2^15确定a,b符号。如果a_lt == 1则a为正数，否则为负数。b_lt同理。
|
|
|
|
- 同时我们需要约束a_hi和b_hi等于对应的u16s_sum。这里主要是为了约束我们用来判断符号的u16的正确性。
|
| ... | ... | @@ -142,6 +193,16 @@ a * b + c = d |
|
|
|
- a_hi + carry_hi \* 2^128 - carry_lo= b_hi + c_hi
|
|
|
|
- 注意：carry_hi=1 等价于 a<b; carry_hi=0 等价于 a>=b
|
|
|
|
|
|
|
|
### layout
|
|
|
|
|
|
|
|
| cnt | o0hi | o0lo | o1hi | o1lo | u16s0 | u16s1 | u16s2 | u16s3 |
|
|
|
|
| ---- | ---- | ---- | ----- | ----- | ---------------- | ----- | --------- | --------- |
|
|
|
|
| 4 | | | | | u16_sum_for_b_hi | | | |
|
|
|
|
| 3 | | | | | u16_sum_for_a_hi | | | |
|
|
|
|
| 2 | | | | | a_lt | b_lt | a_lt_diff | b_lt_diff |
|
|
|
|
| 1 | c | c | carry | carry | u16_sum_for_c_lo | | | |
|
|
|
|
| 0 | a | a | b | b | u16_sum_for_c_hi | | | |
|
|
|
|
|
|
|
|
## Sdiv_Smod
|
|
|
|
|
|
|
|
这里我们还是使用 (a-c)\*b =d 的公式来进行核心约束，值的关注的是对有符号的数进行乘法操作时，我们需要运用到如下补码的知识。
|
| ... | ... | @@ -221,6 +282,8 @@ a * b + c = d |
|
|
|
|
|
|
|
## AddMod
|
|
|
|
|
|
|
|
### 公式
|
|
|
|
|
|
|
|
计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有 **(a+b)%n = r**。我们可以将这个约束转化为 **(a+b) = n * q + r**(商q可能超过256bit)。所以为了约束简单我们可以将上式转换如下：
|
|
|
|
1. **a % n= a_div_n + a_remainder**
|
|
|
|
2. **(a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 )**
|
| ... | ... | @@ -239,32 +302,28 @@ a * b + c = d |
|
|
|
- 当n!=0时, 存在r < n 约束
|
|
|
|
|
|
|
|
### layout
|
|
|
|
```
|
|
|
|
// Addmod arithmetic witeness rows. (Tag::Addmod)
|
|
|
|
// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+
|
|
|
|
// | operand_0_hi| operand_0_lo| operand_1_hi | operand_1_lo | cnt | u16s |
|
|
|
|
// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+
|
|
|
|
// | | | | | 18 | rn_diff_lo |
|
|
|
|
// | | | | | 17 | rn_diff_hi |
|
|
|
|
// | | | | | 16 | carry_1 |
|
|
|
|
// | | | | | 15 | carry_0 |
|
|
|
|
// | | | | | 14 | b_div_n_lo |
|
|
|
|
// | | | | | 13 | b_div_n_hi |
|
|
|
|
// | | | | | 12 | r_lo |
|
|
|
|
// | | | | | 11 | r_hi |
|
|
|
|
// | | | | | 10 | a_remainder_plus_b_lo |
|
|
|
|
// | | | | | 9 | a_remainder_plus_b_hi |
|
|
|
|
// | | | | | 8 | arn_diff_lo |
|
|
|
|
// | b_div_n_hi | b_div_n_lo | a_remainder_plus_b_hi | a_remainder_plus_b_lo | 7 | arn_diff_hi |
|
|
|
|
// | rn_diff_hi | rn_diff_lo | carry_2 | | 6 | an_carry_lo |
|
|
|
|
// | carry_0 | carry_1 | rn_carry_lt_hi | rn_carry_lt_lo | 5 | a_remainder_lo |
|
|
|
|
// | arn_diff_hi | arn_diff_lo | a_remainder_plus_b_overflow_hi | a_remainder_plus_b_overflow_lo | 4 | a_remainder_hi |
|
|
|
|
// | an_carry_hi | an_carry_lo | arn_carry_lt_hi | arn_carry_lt_lo | 3 | n_lo |
|
|
|
|
// | a_div_n_hi | a_div_n_lo | a_remainder_hi | a_remainder_lo | 2 | n_hi |
|
|
|
|
// | n_hi | n_lo | r_hi | r_lo | 1 | a_div_n_lo |
|
|
|
|
// | a_hi | a_lo | b_hi | b_lo | 0 | a_div_n_hi |
|
|
|
|
// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+
|
|
|
|
```
|
|
|
|
|
|
|
|
| operand_0_hi | operand_0_lo | operand_1_hi | operand_1_lo | cnt | u16s |
|
|
|
|
| ------------ | ------------ | ------------------------------ | ------------------------------ | ---- | --------------------- |
|
|
|
|
| | | | | 18 | rn_diff_lo |
|
|
|
|
| | | | | 17 | rn_diff_hi |
|
|
|
|
| | | | | 16 | carry_1 |
|
|
|
|
| | | | | 15 | carry_0 |
|
|
|
|
| | | | | 14 | b_div_n_lo |
|
|
|
|
| | | | | 13 | b_div_n_hi |
|
|
|
|
| | | | | 12 | r_lo |
|
|
|
|
| | | | | 11 | r_hi |
|
|
|
|
| | | | | 10 | a_remainder_plus_b_lo |
|
|
|
|
| | | | | 9 | a_remainder_plus_b_hi |
|
|
|
|
| | | | | 8 | arn_diff_lo |
|
|
|
|
| b_div_n_hi | b_div_n_lo | a_remainder_plus_b_hi | a_remainder_plus_b_lo | 7 | arn_diff_hi |
|
|
|
|
| rn_diff_hi | rn_diff_lo | carry_2 | | 6 | an_carry_lo |
|
|
|
|
| carry_0 | carry_1 | rn_carry_lt_hi | rn_carry_lt_lo | 5 | a_remainder_lo |
|
|
|
|
| arn_diff_hi | arn_diff_lo | a_remainder_plus_b_overflow_hi | a_remainder_plus_b_overflow_lo | 4 | a_remainder_hi |
|
|
|
|
| an_carry_hi | an_carry_lo | arn_carry_lt_hi | arn_carry_lt_lo | 3 | n_lo |
|
|
|
|
| a_div_n_hi | a_div_n_lo | a_remainder_hi | a_remainder_lo | 2 | n_hi |
|
|
|
|
| n_hi | n_lo | r_hi | r_lo | 1 | a_div_n_lo |
|
|
|
|
| a_hi | a_lo | b_hi | b_lo | 0 | a_div_n_hi |
|
|
|
|
|
|
|
|
|
|
|
|
## MulMod
|
| ... | ... | @@ -321,8 +380,6 @@ a * b + c = d |
|
|
|
- `r, r_diff, n`范围约束；
|
|
|
|
- `n != 0`约束；
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
### layout
|
|
|
|
|
|
|
|
| cnt | o_0_hi | o_0_lo | o_1_hi | o_1_lo | u16s_0 |
|
| ... | ... | @@ -409,13 +466,22 @@ arithmetic中的布局: |
|
|
|
|
|
|
|
## U64Overflow
|
|
|
|
|
|
|
|
### 公式
|
|
|
|
|
|
|
|
一行：
|
|
|
|
|
|
|
|
- operand: a_hi a_lo w w_inv
|
|
|
|
- u16s: a_lo 分拆成8个u_16
|
|
|
|
- 约束：w=a_lo的前64位 + a_hi<<64
|
|
|
|
- w和w_inv的simple is zero约束
|
|
|
|
在core里可以使用4个数[a_hi a_lo w w_inv]进行lookup，再加一个Tag = U64Overflow。使用w*w_inv表示0/1，是否u64 overflow。
|
|
|
|
|
|
|
|
### layout
|
|
|
|
|
|
|
|
| cnt | op_0_hi | op_0_lo | op_1_hi | op_1_lo | u16s |
|
|
|
|
| ---- | ------- | ------- | ------- | ------- | --------- |
|
|
|
|
| 0 | a_hi | a_lo | w | w_inv | a_lo_u16s |
|
|
|
|
|
|
|
|
# 实现 arithmetic 子电路中 Add 例子
|
|
|
|
|
|
|
|
如果我们希望为某一个 tag 实现它的约束，我们需要实现 OperationGadget trait，然后在 config 方法中实现相应 tag 的约束就好。具体如下所示
|
| ... | ... | |
