| ... | ... | @@ -192,6 +192,29 @@ a * b + c = d |
|
|
|
|
|
|
|
```
|
|
|
|
|
|
|
|
### Layout
|
|
|
|
|
|
|
|
| hi | lo | hi | lo | cnt | u16_0 | u16_1 | u16_2 | u16_3 | u16_4 |
|
|
|
|
| ---------------------- | -------------- | -------------- | -------------- | ---- | ------------------------------------------------------------ | ------ | ------ | ------ | ------ |
|
|
|
|
| | | | | 17 | d_lo_0 | | | | |
|
|
|
|
| | | | | 16 | d_hi_0 | | | | |
|
|
|
|
| | | | | 15 | c_lo_0 | | | | |
|
|
|
|
| a_com_lt | | | | 14 | c_hi_0 | | | | |
|
|
|
|
| c_sum_carry_hi | c_sum_carry_lo | d_sum_carry_hi | d_sum_carry_lo | 13 | b_hi_0 | | | | |
|
|
|
|
| a_sum_carry_hi | a_sum_carry_lo | b_sum_carry_hi | b_sum_carry_lo | 12 | a_hi_0 (因为a,b 都是输入，我们不用约束它们，这里hi主要是给lt使用) | | | | |
|
|
|
|
| a_lt_carry_hi | b_lt_carry_hi | c_lt_carry_hi | d_lt_carry_hi | 11 | a_diff | | | | |
|
|
|
|
| | | | | 10 | cb_diff_lo_0(c,d 约束因为c,d 非输入值。并且我们要计算c + c_com = 1<<256) | | | | |
|
|
|
|
| cb_diff_hi(cb 指c < b) | cb_diff_lo | cb_carry_hi | | 9 | cb_diff_hi_0 | | | | |
|
|
|
|
| mul_carry_hi | mul_carry_lo | | | 8 | mul_carry_lo_0 | | | | |
|
|
|
|
| | | | | 7 | d_com_lo_0 | | | | |
|
|
|
|
| | | | | 6 | d_com_hi_0 | a_diff | a_diff | a_diff | a_diff |
|
|
|
|
| | | | | 5 | c_com_lo_0 | | | | |
|
|
|
|
| | | | | 4 | c_com_hi_0 | | | | |
|
|
|
|
| c_com_hi | c_com_lo | d_com_hi | d_com_lo | 3 | b_com_lo_0 | | | | |
|
|
|
|
| a_com_hi | a_com_lo | b_com_hi | b_com_lo | 2 | b_com_hi_0 | | | | |
|
|
|
|
| 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
|
|
|
|
|
|
|
|
计算addMod操作码我们等于验证a,b,n,r 其中n是mod值，r是余数。我们有(a+b)%n = r。我们可以将这个约束转化为(a+b) = n * q + r。为了约束简单我们可以有
|
| ... | ... | |
