... | ... | @@ -75,7 +75,7 @@ a + b = c + overflow * 2^256`,且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit |
|
|
| 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
|
|
|
## 3.2 Sub
|
|
|
|
|
|
### 公式
|
|
|
|
... | ... | @@ -98,7 +98,7 @@ a + b = c + overflow * 2^256`,且 `c` 的 `hi` 和 `lo` 被约束为8个16-bit |
|
|
| 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
|
|
|
## 3.3 Div_Mod
|
|
|
|
|
|
### 公式
|
|
|
|
... | ... | @@ -149,7 +149,7 @@ a * b + c = d |
|
|
| DivMod | 1 | c | c | d | d | u16_sum_for_b_lo |
|
|
|
| DivMod | 0 | a | a | b | b | u16_sum_for_b_hi |
|
|
|
|
|
|
## Mul
|
|
|
## 3.4 Mul
|
|
|
|
|
|
### 公式
|
|
|
|
... | ... | @@ -208,7 +208,7 @@ a * b + c = d |
|
|
| 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
|
|
|
## 3.5 SLT_SGT
|
|
|
|
|
|
### 公式
|
|
|
|
... | ... | @@ -250,7 +250,7 @@ a * b + c = d |
|
|
| 1 | c | c | carry | carry | u16_sum_for_c_lo | | | |
|
|
|
| 0 | a | a | b | b | u16_sum_for_c_hi | | | |
|
|
|
|
|
|
## Sdiv_Smod
|
|
|
## 3.6 Sdiv_Smod
|
|
|
|
|
|
在 `Sdiv_Smod`(有符号除法和取余)中,我们处理有符号整数的除法和取余,以下是核心约束:
|
|
|
|
... | ... | @@ -339,7 +339,7 @@ a * b + c = d |
|
|
| c_hi | c_lo | d_hi | d_lo | 1 | a_com_lo_0 | | | | |
|
|
|
| a_hi | a_lo | b_hi | d_lo | 0 | a_com_hi_0 | | | | |
|
|
|
|
|
|
## AddMod
|
|
|
## 3.7 AddMod
|
|
|
|
|
|
### 公式
|
|
|
|
... | ... | @@ -387,7 +387,7 @@ a + b = n * q + r (式2) |
|
|
| a_hi | a_lo | b_hi | b_lo | 0 | r_hi |
|
|
|
|
|
|
|
|
|
## MulMod
|
|
|
## 3.8 MulMod
|
|
|
|
|
|
### 核心公式
|
|
|
|
... | ... | @@ -469,28 +469,35 @@ a + b = n * q + r (式2) |
|
|
| 1 | n_hi | n_lo | r_hi | r_lo | k1_lo_u16s |
|
|
|
| 0 | a_hi | a_lo | b_hi | b_lo | k1_hi_u16s |
|
|
|
|
|
|
## Length
|
|
|
## 3.9 Length
|
|
|
|
|
|
### length 电路功能:
|
|
|
|
|
|
输入 offset, length, size
|
|
|
输入参数:
|
|
|
|
|
|
返回 real\_len, zero\_len, overflow, _real\_len\_is\_zero, zero\_len\_is\_zero(?待定)_
|
|
|
- `offset`:偏移量
|
|
|
- `length`:长度
|
|
|
- `size`:总大小
|
|
|
|
|
|
* offset,length,size,需要 u64\_overflow 约束
|
|
|
返回值:
|
|
|
|
|
|
* 判断 offset + length > size
|
|
|
- `real_len`:实际长度
|
|
|
- `zero_len`:超出长度
|
|
|
- `overflow`:是否溢出
|
|
|
- `_real_len_is_zero`:实际长度是否为零
|
|
|
- `_zero_len_is_zero`:超出长度是否为零(待定)
|
|
|
|
|
|
* 三种情况_(不管length是否为0)_,需要返回 **return (real\_len, zero\_len)**:
|
|
|
约束条件:
|
|
|
|
|
|
- `offset`、`length`、`size`需要符合 `u64_overflow` 约束。
|
|
|
|
|
|
1. offset + length <= size, **return (length, 0)**
|
|
|
逻辑判断:
|
|
|
|
|
|
2. offset + length > size,分为两种情况:
|
|
|
- 如果 `offset + length <= size`,返回 `(length, 0)`。
|
|
|
|
|
|
1. offset < size , **return (size - offset, offset + length - size)**
|
|
|
|
|
|
2. offset >= size, **return (0, length).**
|
|
|
- 如果 `offset + length > size`,分为两种情况:
|
|
|
- 如果 `offset < size`,返回 `(size - offset, offset + length - size)`。
|
|
|
- 如果 `offset >= size`,返回 `(0, length)`。
|
|
|
|
|
|
### arithmetic中的布局:
|
|
|
|
... | ... | @@ -503,48 +510,35 @@ a + b = n * q + r (式2) |
|
|
|
|
|
### 约束
|
|
|
|
|
|
1. **operand 和 u16s 大小相等**
|
|
|
|
|
|
1. offset, size, length
|
|
|
|
|
|
2. offset\_bound = offset + length
|
|
|
|
|
|
|
|
|
2. **约束 size 是否小于 offset\_bound**
|
|
|
|
|
|
1. 使用 SimpleLtGadget::new(size, offset\_bound, overflow, diff),range 设置为2^64
|
|
|
|
|
|
2. overflow is bool
|
|
|
|
|
|
|
|
|
3. **约束 offset 是否小于 size**
|
|
|
|
|
|
1. 使用 SimpleLtGadget::new(offset, size, lt\_offset\_size, diff\_offset\_size),range 设置为2^64
|
|
|
|
|
|
2. lt\_offset\_size is bool
|
|
|
|
|
|
**operand 和 u16s 大小相等**
|
|
|
|
|
|
4. **三种情况下 (real\_len, zero\_len) 的约束:**
|
|
|
- `offset`, `length`, `size`
|
|
|
- `offset_bound = offset + length`
|
|
|
|
|
|
**参考上文,使用overflow 和 lt\_offset\_size 作为 selector,那么公式为:**
|
|
|
**约束 size 是否小于 offset_bound**
|
|
|
|
|
|
1. real\_len = (1-overflow) \* length
|
|
|
- 使用 `SimpleLtGadget::new(size, offset_bound, overflow, diff)`,`range` 设置为 2^64
|
|
|
- `overflow` 为布尔值
|
|
|
|
|
|
**约束 offset 是否小于 size**
|
|
|
|
|
|
+ overflow \* lt\_offset\_size \* (size - offset)
|
|
|
- 使用 `SimpleLtGadget::new(offset, size, lt_offset_size, diff_offset_size)`,`range` 设置为 2^64
|
|
|
- `lt_offset_size` 为布尔值
|
|
|
|
|
|
2. zero\_len = overflow \* lt\_offset\_size \* (offset\_bound - size)
|
|
|
**三种情况下 (real_len, zero_len) 的约束**
|
|
|
|
|
|
- 使用 `overflow` 和 `lt_offset_size` 作为 `selector`,公式如下:
|
|
|
|
|
|
+ overflow \* (1 - lt\_offset\_size) \* length
|
|
|
`real_len = (1 - overflow) * length + overflow * lt_offset_size * (size - offset)`
|
|
|
|
|
|
5. **约束 real\_len\_is\_zero, zero\_len\_is\_zero**
|
|
|
`zero_len = overflow * lt_offset_size * (offset_bound - size) + overflow * (1 - lt_offset_size) * length`
|
|
|
|
|
|
1. SimpleIsZero(real\_len,real\_len\_inv)
|
|
|
**约束 real_len_is_zero 和 zero_len_is_zero**
|
|
|
|
|
|
2. SimpleIsZero(zero\_len,zero\_len\_inv)
|
|
|
- 使用 `SimpleIsZero(real_len, real_len_inv)`
|
|
|
- 使用 `SimpleIsZero(zero_len, zero_len_inv)`
|
|
|
|
|
|
## memory expansion
|
|
|
## 3.10 memory expansion
|
|
|
|
|
|
memory expansion 电路的功能是给定offset\_bound,计算是否需要拓展内存。
|
|
|
|
... | ... | @@ -603,7 +597,7 @@ offset\_bound 的代表的是访问内存段的**右区间**: |
|
|
|
|
|
**offset\_bound = (offset + length) \* length \* length\_inv**
|
|
|
|
|
|
## U64Overflow
|
|
|
## 3.11 U64Overflow
|
|
|
|
|
|
### 公式
|
|
|
|
... | ... | @@ -627,7 +621,7 @@ w=a_hi×2^64+a_lo |
|
|
| ---- | ------- | ------- | ------- | ------- | --------- |
|
|
|
| 0 | a_hi | a_lo | w | w_inv | a_lo_u16s |
|
|
|
|
|
|
# 实现 arithmetic 子电路中 Add 例子
|
|
|
# 4 实现 arithmetic 子电路中 Add 例子
|
|
|
|
|
|
如果我们希望为某一个 tag 实现它的约束,我们需要实现 OperationGadget trait,然后在 config 方法中实现相应 tag 的约束就好。具体如下所示
|
|
|
|
... | ... | |