| ... | ... | @@ -286,46 +286,39 @@ a * b + c = d |
|
|
|
|
|
|
|
### 公式
|
|
|
|
|
|
|
|
计算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 )**
|
|
|
|
3. **(a_remainder_plus_b + a_remainder_plus_b_overflow << 256 ) % n= b_div_n + r**
|
|
|
|
输入a,b,n 计算：
|
|
|
|
|
|
|
|
那么需要具体的约束大致如下，对于第1个等式：
|
|
|
|
- a,n,a_remainder,a_div_n 存在mul_add_words约束 a_div_n * n + a_remainder = a
|
|
|
|
- 当n!=0时候, 存在a_remainder < n 约束
|
|
|
|
$$a + b n = r （式1）$$
|
|
|
|
|
|
|
|
对于第2个等式：
|
|
|
|
- b,a_remainder,a_remainder_plus_b 存在add_words约束 a_remainder + b = a_remainder_plus_b + a_remainder_plus_b_overflow << 256
|
|
|
|
|
|
|
|
对于第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）
|
|
|
|
可以将算式转换为：
|
|
|
|
a + b = n * q + r （式2）
|
|
|
|
|
|
|
|
这里的q是商，并没有实际出现在EVM的运算中。
|
|
|
|
q溢出256bit：
|
|
|
|
其中q 可能为257bit，比如当a=b=2^256, n = 1 时。我们可以将q设计为256位+1bit carry位。
|
|
|
|
考虑n*q+r溢出512bit：
|
|
|
|
n最大值为2256-1, q的最大值为2256-1，r的最大值为2256-2，那么n*q+r的最大值为：2512-2256-3。关键在于约束q的最大值为2256-1（q_overflow = 0 or 1）。
|
|
|
|
除数为0：
|
|
|
|
考虑n=0，EVM的设计里r = 0，但是实际的程序计算出来的 r = a + b。这时候式子2不能成立，这里直接让r=0（可以避免r超过256bit），使用n=0 判断式作为selector。
|
|
|
|
|
|
|
|
- 当n!=0时, 存在r < n 约束
|
|
|
|
|
|
|
|
### layout
|
|
|
|
|
|
|
|
| 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 |
|
|
|
|
| operand0 | operand1 | operand2 | operand3 | cnt | u16s |
|
|
|
|
|-------------------|-------------------|-------------|-------------|-----|-------------|
|
|
|
|
| | | | | 11 | rn_diff_lo |
|
|
|
|
| | | | | 10 | rn_diff_hi |
|
|
|
|
| | | | | 9 | carry_1 |
|
|
|
|
| | | | | 8 | carry_0 |
|
|
|
|
| | | | | 7 | a_plus_b_lo |
|
|
|
|
| | | | | 6 | a_plus_b_hi |
|
|
|
|
| a_plus_b_lo_carry | a_plus_b_hi_carry | | | 5 | q_lo |
|
|
|
|
| carry_0 | carry_1 | q_overflow | | 4 | q_hi |
|
|
|
|
| q_hi | q_lo | a_plus_b_hi | a_plus_b_lo | 3 | n_lo |
|
|
|
|
| rn_carry_lt_hi | rn_carry_lt_lo | rn_diff_hi | rn_diff_lo | 2 | n_hi |
|
|
|
|
| n_hi | n_lo | r_hi | r_lo | 1 | r_lo |
|
|
|
|
| a_hi | a_lo | b_hi | b_lo | 0 | r_hi |
|
|
|
|
|
|
|
|
|
|
|
|
## MulMod
|
| ... | ... | |
