geruiwang布局
arithmetic 子电路的设计包含如下几列。我们重点关注 operand与 u16列，
pub struct ArithmeticCircuitConfig<F> {
q_enable: Selector,
/// Tag for arithmetic operation type
tag: BinaryNumberConfig<Tag, LOG_NUM_ARITHMETIC_TAG>,
/// The operands in one row, splitted to 2 (high and low 128-bit)
operands: [[Column<Advice>; 2]; NUM_OPERAND],
/// The 16-bit values in one row
u16s: [Column<Advice>; NUM_U16],
/// Row counter, decremented for rows in one execution state
cnt: Column<Advice>,
/// IsZero chip for column cnt
cnt_is_zero: IsZeroWithRotationConfig<F>,
}
pub enum Tag {
#[default]
Nil,
Add,
Sub,
Mul,
DivMod,
SltSgt,
SdivSmod,
Addmod,
Mulmod,
}在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见here。
列的含义
operand* 用来存放算术中的参数值，如 a+b=c+overflow 指令中的 a,b,c,overflow。u16*用来 lookup 算术中的输出如 c_hi,c_lo 属于 u128 范围。这里我们只需要保证输出值的 lookup 就好。cnt 记录某个具体算术指令的行计数器，从正数开始递减到 0。
约束
在 arithmetic 子电路中约束可以分为两类。 通用约束
- 约束 cnt 除零行外,当前行与下一行差值为 1
不同 Tag 对应的约束不同 请注意我们这里所有的 u16 都是 little endian 小端编码
Add
公式
含义：a+b=c+overflow*2^256，且 c 的 hi lo 被约束为 8 个 16bit 之和
- 注：加法可以用这个
- 如果是 cnt=0 行，则 cnt_prev=1,cnt_prev_prev=0
- c_lo = u16 sum(rotation cur)
- c_hi = u16 sum(rotation prev)
- carry hi is bool
- carry lo is bool
- 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 都可以用这个
- c_lo = u16 sum(rotation cur)
- c_hi = u16 sum(rotation prev)
- carry hi is bool
- carry lo is bool
- a_lo + carrry_lo * 2^128 = b_lo + c_lo
- 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
if tag is div, (a,b,c,d) = (pop1,pop2,push,pop1 - push * pop2)
if tag is mod, (a,b,c,d) = (pop1 ,pop2 , if pop2 is zero{zero}else{pop1 / pop2} ,if pop2 is zero{pop1}else{push})
define
a * b + c = d
- define t0 = a0 \* b0
- define t1 = a0 \* b1 + a1 \* b0
- define t2 = a0 \* b2 + a2 \* b0 + a1 \* b1
- define t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2
- define t_lo=t0+(t1)\*2^64
- define t_hi=(t2)+(t3)\*2^64
- define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128
- define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128- 如果是 0 行，约束 num_row is 10,并且约束 cnt 自增的有效性
- b_lo = u16 sum(rotation -2) //请注意因为a是输入值，我们可以不对a_hi,a_lo进行range约束
- b_hi = u16 sum(rotation -3)
- c_lo = u16 sum(rotation -4)
- c_hi = u16 sum(rotation -5)
- d_lo = u16 sum(rotation -6)
- d_hi = u16 sum(rotation -7)
- (t_lo+c_lo-car_lo*2^128) - d_lo
- (t_hi+c_hi+car_lo-car_hi*2^128) - d_hi
- residue < divisor when divisor != 0
- 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）
- define t1 = a0 * b1 + a1 * b0 (64-193bit)
- define t2 = a0 * b2 + a2 * b0 + a1 * b1 (128 - 257bit)
- define t3 = a0 * b3 + a3 * b0 + a2 * b1 + a1 * b2 (192- 322bit)
- define t_lo=t0+(t1)*2^64
- define t_hi=(t2)+(t3)*2^64
- define carry_lo = (t0 + (t1 << 64) + c_lo).saturating_sub(d_lo) >> 128 c_lo is 0
- define carry_hi = (t2 + (t3 << 64) + c_hi + carry_lo).saturating_sub(d_hi) >> 128 c_hi is 0
- 如果是 0 行，约束 num_row is 6,并且约束 cnt 自增的有效性
- a_lo = u16 sum(rotation cur)
- a_hi = u16 sum(rotation -1)
- b_lo = u16 sum(rotation -2)
- b_hi = u16 sum(rotation -3)
- c_lo = u16 sum(rotation -4)
- c_hi = u16 sum(rotation -5)
- carry_hi == u16 sum(rotation -6) 请注意这里我们使用的是5位u16数据的和，从define部分我们可以知道carry_hi等于322 - 256 = 66bit。
- carry_lo == u16 sum(rotation -7) 请注意这里我们使用的是5位u16数据的和,从define部分我们可以知道carry_lo等于193 - 128 = 65bit。
- （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的正确性。
- a,b符号不相等时。我们有(a_lt - b_lt)作为不相等condition，
- 当 a_lt == 1,a是正数,则存在carry == 0。a_lt == 0时a是负数，carry=1.所以有约束 1-(a_lt + carry_hi)
- c_lo = u16 sum(rotation -4)
- c_hi = u16 sum(rotation -5)
- a,b符号相等时,我们有(1 -(a_lt - b_lt))作为符号condition，与下面每一个约束相乘
- a_lo + carrry_lo * 2^128 = b_lo + c_lo
- 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 的公式来进行核心约束，值的关注的是对有符号的数进行乘法操作时，我们需要运用到如下补码的知识。
- 首先我们统一计算a,b 的补码，补码表示法将一个负整数表示为其正值的按位取反（二进制反码）加 1。正整数的补码表示与其无符号表示相同。
- 使用 DIV 和 MOD 操作码执行无符号整数除法和取余：将转换后的 U256 数字相除或取余。由于步骤 1 中的转换，这将正确处理有符号整数除法和取余。
- 在div 中如果我们是一正一负，需要对计算结果再进行Neg计算(-x mod 2**256.)。如果是mod 则只有被除数是负数时，计算结果才需要进行Neg计算。
核心约束说明
根据上述补码的知识，我们有 b_com*c_com+d_com=a_com. 其中a_com是a的补码，b_com是b的补码，c_com是c的补码，d_com是d的补码.
1. 乘法约束
细节请参考mul模块约束内容
2. 补码的相关约束如下(开发时我们需要实现a,b,c,d的下述约束)
- x_abs_lo == lo when x >= 0
- x_abs_hi == hi when x >= 0
- sum == 0 when x < 0 （小于0证明存在补码,同时我们有x+x_abs = 1 <<256。x + x_abs 约束请参考add部分）
- carry_hi == 1 when x < 0
3. 范围约束
因为当前算法中使用了mul约束，所以我们需要对mul中的变量进行范围约束。同时也因为判断a,b,c,d正负符号的原因，我们需要对a_hi,b_hi,c_hi,d_hi进行范围约束。
另外因为判断补码有效性的原因，我们需要对a,b,c,d以及他们的补码值进行u128范围约束，因为a,b是输入可以忽略，只需增加对a_hi,b_hi,c_lo,d_lo进行u128范围约束。
4.符号约束
sign(dividend_original) == sign(remainder_original) when quotient, divisor and remainder original value are all non-zero。 这里主要约束mod的值与被除数的符号相同
- (1.expr() - quotient_is_zero.expr())
* (1.expr() - divisor_is_zero.expr())
* (1.expr() - remainder_is_zero.expr())
* (dividend_original.is_neg().expr() - remainder_original.is_neg().expr())
quotient_original.is_neg().expr() + divisor_original.is_neg().expr() (如果被除数的补码也是负数，与余数和除数等于零，则排除约束情况) 这里说到的符号都是非补码的符号
这里计算的都是div情况下的变化
- (
quotient_original.is_neg().expr() + divisor_original.is_neg().expr() -dividend_original.is_neg().expr()
- 2.expr()
* quotient_original.is_neg().expr()
* divisor__original.is_neg().expr()
)
*(1.expr() - quotient_is_zero.expr())
* (1.expr() - divisor_is_zero.expr())
* (1.expr() - dividend_is_signed_overflow.expr()) //**dividend_is_signed_overflow是指被除数补码是否为负数,这里需要判断的原因是剔除特殊情况**
note: 对于一个特殊的SDIV情况，当输入dividend = -(1 << 255) 和 divisor = -1时，商的结果应该是1 << 255。但是一个有符号字（signed word）只能表示从-(1 << 255)到
(1 << 255) - 1的有符号值。因此，对于这种情况，约束条件sign(dividend) == sign(divisor) ^ sign(quotient)不能应用。
5. 取余结果值约束
为了保证mul乘法的有效当b==0时，我们设置d==a.(d是余数,b是除数)。但是在eth中计算取余时有b==0时，我们设置d==0.所以在core circuit部分我们需要增加b=0时d==0
Layout
(因为a,b 都是输入不需要进行范围约束，但是因为我们需要判断a,b的符号，所以只需要对a_hi,b_hi进行范围约束。因为c,d 属于非输入值，并且我们要计算c + c_com = 1<<256。 所以我们需要对c,d进行范围约束) 其中u_16 具有8列，这里为了表现清晰，我们做了简便处理。
| 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_lt_carry_hi | b_lt_carry_hi | c_lt_carry_hi | d_lt_carry_hi | 11 | a_diff | b_diff | c_diff | d_diff | a_com_diff |
| 10 | cb_diff_lo_0 | ||||||||
| 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 | ||||||||
| 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(商q可能超过256bit)。所以为了约束简单我们可以将上式转换如下：
- 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
那么需要具体的约束大致如下，对于第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
对于第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
| 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
核心公式
基础公式：
-
a*b = r (mod n)，其中a,b,n,r为 256-bit。
公式拆分：
-
a/n = k1 余 a_remainder -
(a_remainder * b) / n = k2 余 r -
a_remainder * b + 0 = e + d * 2^256-- 看做两数加法
公式转化（除转乘）：
k1 * n + a_remainder = a-
a_remainder * b + 0 = e + d * 2^256不变 k2 * n + r = e + d * 2^256
约束
（注：以公式角度进行约束描述，未忽略上一步已经约束过的变量）
-
公式1 --
k1 * n + a_remainder = a
- 参考mul操作：
-
k1, n, a_remainderu16s范围约束 128bit； -
carry_lou16s[0-5]范围约束 65bit； -
carry_hi==0除法转换；
-
- 除转乘，有
remainder < divisor if divisor != 0，参考减法a_remainder - n = a_remainder_diff - a_remainder_carry << 256：-
a_remainder_diff范围约束； -
n != 0约束；
-
-
公式2 --
a_remainder * b + 0 = e + d * 2^256
- 参考muladd512方法：
-
a_remainder,b,e,d的u16s约束 128bit； -
a_rem_mul_b_carry的u16s[0..5]约束，乘法中的进位；
-
-
公式3 --
k2 * n + r = e + d * 2^256
- 参考muladd512方法：
-
k2, n , r, e, d的u16s范围约束128bit； -
k2n_plus_r_carry的u16s[0..5]范围约束；
-
- 除转乘，
r - n = r_diff - r_carry << 256：-
r, r_diff, n范围约束； -
n != 0约束；
-
layout
| cnt | o_0_hi | o_0_lo | o_1_hi | o_1_lo | u16s_0 |
|---|---|---|---|---|---|
| 26 | k2n_carry_0 | ||||
| 25 | k2n_carry_1 | ||||
| 24 | k2n_carry_2 | ||||
| 23 | r_lo_u16s | ||||
| 22 | r_hi_u16s | ||||
| 21 | k2_lo_u16s | ||||
| 20 | k2n_carry_2 | k2n_carry_1 | k2n_carry_0 | k2_hi_u16s | |
| 19 | r_diff_hi | r_diff_lo | r_lt_hi | r_lt_lo | r_diff_lo_u16s |
| 18 | k2_hi | k2_lo | r_diff_hi_u16s | ||
| 17 | arb_carry_0 | ||||
| 16 | arb_carry_1 | ||||
| 15 | arb_carry_2 | ||||
| 14 | d_lo_u16s | ||||
| 13 | d_hi_u16s | ||||
| 12 | e_lo_u16s | ||||
| 11 | e_hi_u16s | ||||
| 10 | arb_carry_2 | arb_carry_1 | arb_carry_0 | b_lo_u16s | |
| 9 | e_hi | e_lo | d_hi | d_lo | b_hi_u16s |
| 8 | a_remainder_diff_lo_u16s | ||||
| 7 | a_remainder_diff_hi_u16s | ||||
| 6 | a_rem_carry_lo_u16s | ||||
| 5 | a_remainder_lo_u16s | ||||
| 4 | a_remainder_diff_hi | a_remainder_diff_lo | a_rem_lt_hi | a_rem_lt_lo | a_remainder_hi_u16s |
| 3 | k1_carry_hi | k1_carry_lo | n_lo_u16s | ||
| 2 | k1_hi | k1_lo | a_remainder_hi | a_remainder_lo | n_hi_u16s |
| 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
arithmetic中的布局:
| tag | cnt | operand_0_hi | operand_0_lo | operand_1_hi | operand_1_lo | u16_0 | u16_1 | u16_2 | u16_3 | u16_4 | u16_5 | u16_6 | u16_7 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Length | 3 | 0 | 0 | 0 | 0 | length_minus_datasize-minus-offset_0 | length_minus_datasize-minus-offset_1 | length_minus_datasize-minus-offset_2 | length_minus_datasize-minus-offset_3 | datasize_minus_offset_0 | datasize_minus_offset_1 | datasize_minus_offset_2 | datasize_minus_offset_3 |
| Length | 2 | length_gt_datasize-minus-offset | datasize_gt_offset | offset_24_inv | offset_overflow | offset_lo_0 | offset_lo_1 | offset_lo_2 | offset_lo_3 | offset_lo_4 | offset_lo_5 | offset_lo_6 | offset_lo_7 |
| Length | 1 | offset_hi | offset_lo | real_length | zero_length | datasize_lo_0 | datasize_lo_1 | datasize_lo_2 | datasize_lo_3 | datasize_lo_4 | datasize_lo_5 | datasize_lo_6 | datasize_lo_7 |
| Length | 0 | length_hi | length_lo | datasize_hi | datasize_lo | length_lo_0 | length_lo_1 | length_lo_2 | length_lo_3 | length_lo_4 | length_lo_5 | length_lo_6 | length_lo_7 |
限制:
// datasize_lo_16 constraints
let expr_datasize = expr_from_u16s([datasize_lo_0,datasize_lo_1,datasize_lo_2,datasize_lo_3]);
datasize_lo = expr_from_u16s([datasize_lo_0,datasize_lo_1,datasize_lo_2,datasize_lo_3,datasize_lo_4,datasize_lo_5,datasize_lo_6,datasize_lo_7]);
// length_lo_16 constraints
let expr_length = expr_from_u16s([length_lo_0,length_lo_1,length_lo_2,length_lo_3]);
length_lo = expr_from_u16s([length_lo_0,length_lo_1,length_lo_2,length_lo_3,length_lo_4,length_lo_5,length_lo_6,length_lo_7]);
// offset_lo_16 constraints
let offset_24 = offset_hi *2^64 + expr_from_u16s([offset_lo_4,offset_lo_5,offset_lo_6,offset_7]);
let is_offset_24_zero = SimpleIsZero(offset_24,offset_24_inv,"");
offset_overflow = (1-is_offset_24_zero)
let expr_offset = expr_from_u16s([offset_lo_0,offset_lo_1,offset_lo_2,offset_lo_3]);
if offset_overflow {
expr_offset = 0xffffffffffffffff;
}else{
offset_lo = expr_offset;
}
//
let datasize_gt_offset, datasize_minus_offset = expr_datasize - expr_offset;
// datasize_minus_offset = datasize_gt_offset * 2^64 + expr_datasize - expr_offset;
if !datasize_gt_offset {
real_length = 0;
zero_length = expr_length;
}else{
let length_gt_datasize-minus-offset , length_minus_datasize-minus-offset = expr_length - datasize_minus_offset;
// length_minus_datasize-minus-offset = length_gt_datasize-minus-offset * 2^64 + expr_length - datasize_minus_offset ;
if !length_gt_datasize-minus-offset {
real_length = expr_length;
zero_length = 0;
}else {
real_length = datasize_minus_offset;
zero_length = length_minus_datasize-minus-offset
}
}
输入：length,offset,data_size
输出：real_length, zero_length
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 的约束就好。具体如下所示
pub(crate) trait OperationGadget<F: Field> {
const NAME: &'static str;
const TAG: Tag;
const NUM_ROW: usize;
fn constraints(
config: &OperationConfig<F>,
meta: &mut VirtualCells<F>,
) -> Vec<(&'static str, Expression<F>)>;
}接口实现见代码，路径 zkevm-circuits/src/arithmetic_circuit/operation