| ... | ... | @@ -221,43 +221,51 @@ a * b + c = d |
|
|
|
|
|
|
|
## AddMod
|
|
|
|
|
|
|
|
计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有(a+b)%n = r。我们可以将这个约束转化为(a+b) = n * q + r。为了约束简单我们可以有
|
|
|
|
a % n= a_div_n + a_remainder a = n * a_div_n + a_remainder
|
|
|
|
(a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 )
|
|
|
|
(a_remainder_plus_b + a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r
|
|
|
|
note: 其中a_remainder+b 大于256位. 我们可以有以下约束
|
|
|
|
计算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** $\Leftrightarrow$ **a = n * a_div_n + a_remainder**
|
|
|
|
2. **(a_remainder + b) = (a_remainder_plus_b +a_remainder_plus_b_overflow << 256 )**
|
|
|
|
3. **(a_remainder_plus_b + a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r**
|
|
|
|
|
|
|
|
```
|
|
|
|
/// Construct the gadget that checks a * b + c == d * 2**256 + e
|
|
|
|
/// where a, b, c, d, e are 256-bit words.
|
|
|
|
///
|
|
|
|
/// We execute a multi-limb multiplication as follows:
|
|
|
|
/// a and b is divided into 4 64-bit limbs, denoted as a0~a3 and b0~b3
|
|
|
|
/// defined t0, t1, t2, t3, t4, t5, t6:
|
|
|
|
/// t0 = a0 * b0, // 0 - 128bit
|
|
|
|
/// t1 = a0 * b1 + a1 * b0, //64 - 193bit 两数相加可能存在进位
|
|
|
|
/// t2 = a0 * b2 + a2 * b0 + a1 * b1, //128 - 258bit
|
|
|
|
/// t3 = a0 * b3 + a3 * b0 + a2 * b1 + a1 * b2, //192 - 322bit
|
|
|
|
/// t4 = a1 * b3 + a2 * b2 + a3 * b1,
|
|
|
|
/// t5 = a2 * b3 + a3 * b2,
|
|
|
|
/// t6 = a3 * b3,
|
|
|
|
|
|
|
|
/// Finally we just prove:
|
|
|
|
/// t0 + t1 * 2^64 + c_lo = e_lo + carry_0 * 2^128 // carry_0 is 65bit
|
|
|
|
/// t2 + t3 * 2^64 + c_hi + carry_0 = e_hi + carry_1 * 2^128
|
|
|
|
/// t4 + t5 * 2^64 + carry_1 = d_lo + carry_2 * 2^128
|
|
|
|
/// t6 + carry_2 = d_hi
|
|
|
|
|
|
|
|
carry_0 = (t0 + (t1 << 64) + c_lo).saturating_sub(e_lo) >> 128
|
|
|
|
carry_1 = (t2 + (t3 << 64) + c_hi + carry_0).saturating_sub(e_hi) >> 128
|
|
|
|
carry_2 = (t4 + (t5 << 64) + carry_1).saturating_sub(d_lo) >> 128
|
|
|
|
```
|
|
|
|
那么需要具体的约束如下，对于第1个等式：
|
|
|
|
- a,n,a_remainder,a_div_n 存在mul_add_words约束 a_div_n * n + a_remainder = a
|
|
|
|
- 当n!=0时候, 存在a_remainder < n 约束
|
|
|
|
|
|
|
|
对于第2个等式：
|
|
|
|
- b,a_remainder,a_remainder_plus_b 存在add_words约束 a_remainder + b = a_remainder_plus_b + a_remainder_plus_b_overflow << 256
|
|
|
|
- b_div_n,n,b_remainder,a_reduced_plus_b_overflow 存在mul_add_words约束 b_div_n * n + r = a_remainder_plus_b + a_remainder_plus_b_overflow << 256 （mul_add_512_gadget）
|
|
|
|
- a_remainder < n 约束
|
|
|
|
- r < n 约束
|
|
|
|
- n_is_zero 约束
|
|
|
|
|
|
|
|
对于第3个等式：
|
|
|
|
- b_div_n,n,b_remainder,a_reduced_plus_b_overflow 存在mul_add_words约束， b_div_n * n + r = a_remainder_plus_b + a_remainder_plus_b_overflow << 256 （mul_add_512_gadget）
|
|
|
|
|
|
|
|
- 当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 |
|
|
|
|
// +-------------+-------------+--------------------------------+--------------------------------+-----+-----------------------+
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
## MulMod
|
|
|
|
|
| ... | ... | |
