geruiwang1 布局
arithmetic 子电路用于执行基本的数学运算，如加法、减法、乘法、除法等。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,
Length,
memory_expansion,
}在这里 tag 我们使用了一个电路小工具“BinaryNumberConfig/BinaryNumberChip”。关于 BinaryNumberChip，详见here。
列的含义
operand*: 存放算术操作中的输入参数，如 a+b=c+overflow 指令中的 a,b,c,overflow。
u16*: 用于查找算术运算的输出值，特别是对大数值的低16位和高16位的处理（如 c_hi、c_lo）。通常在大数运算中，将结果拆分为多个 16-bit 部分进行处理。
cnt: 记录某个具体算术指令的行计数器，从正数递减到0。
2 约束
在设计 arithmetic 子电路时，约束可以分为两类：
-
通用约束:
- 约束
cnt除零行外，当前行与下一行的差值为1。这确保了行计数器的正确递减。
- 约束
-
不同 Tag 对应的约束:
- 不同的操作（如加法、减法、乘法等）有不同的约束规则。这些规则确保了运算的正确性和结果的准确性。
3 运算子电路
3.1 Add
公式
a + b = c + overflow * 2^256，且 c的hi和lo` 被约束为8个16-bit的和。
约束:
-
c_lo = u16 sum(rotation cur)：当前行的低16位和。 -
c_hi = u16 sum(rotation prev)：前一行的高16位和。 -
carry_hi和carry_lo为布尔值，用于表示进位。 -
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个16-bit的和。
约束：
-
c_lo = u16 sum(rotation cur)。 -
c_hi = u16 sum(rotation prev)。 -
carry_hi和carry_lo为布尔值。 -
a_lo + carry_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)。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 - carry_lo \* 2^128) - d_lo，确保c的低16位加上t_lo和carry_lo乘以 2^128，减去d_lo，结果与t_lo相匹配。carry_lo用于调整进位。 -
(t_hi + c_hi + carry_lo - carry_hi \* 2^128) - d_hi，确保c的高16位加上t_hi和carry_lo，减去carry_hi乘以 2^128，结果与d_hi相匹配。carry_hi用于调整进位。 -
residue < divisor when divisor != 0确保d在除法过程中小于b（当b不为0时），表示d是正确的余数。 -
carry_hi == 0。 -
carry_lo == u16 sum(rotation -7)确保了carry_lo的值正确。
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
公式
在 Mul（乘法）子电路中，我们涉及到的公式和约束是用来确保乘法结果的正确性的。这里详细解释一下每个公式和约束：
-
定义乘法操作
-
t0 = a0 \* b0计算a和b的最低16位的乘积，这个结果的位数在0到128位之间。 -
t1 = a0 \* b1 + a1 \* b0计算a和b的其他16位的乘积加上最低16位的乘积，这个结果的位数在64到193位之间。 -
t2 = a0 \* b2 + a2 \* b0 + a1 \* b1计算a和b的更高16位的乘积加上前两步的结果，这个结果的位数在128到257位之间。 -
t3 = a0 \* b3 + a3 \* b0 + a2 \* b1 + a1 \* b2计算a和b的最高16位的乘积加上前面步骤的结果，这个结果的位数在192到322位之间。 -
t_lo = t0 + (t1 << 64)计算乘法结果的低128位，其中t1左移64位后加到t0上。 -
t_hi = t2 + (t3 << 64)计算乘法结果的高128位，其中t3左移64位后加到t2上。
-
-
进位计算
-
carry_lo = (t0 + (t1 << 64) - c_lo) >> 128计算低128位的进位，将t0和t1左移64位后的和减去c_lo，右移128位得到carry_lo。 -
carry_hi = (t2 + (t3 << 64) + carry_lo - c_hi) >> 128计算高128位的进位，将t2和t3左移64位后的和加上carry_lo，减去c_hi，右移128位得到carry_hi。
-
-
约束
-
a_lo = u16 sum(rotation cur)a的低16位在当前行的位置。 -
a_hi = u16 sum(rotation -1)a的高16位在当前行的位置。 -
b_lo = u16 sum(rotation -2)b的低16位在当前行的位置。 -
b_hi = u16 sum(rotation -3)b的高16位在当前行的位置。 -
c_lo = u16 sum(rotation -4)c的低16位在当前行的位置。 -
c_hi = u16 sum(rotation -5)c的高16位在当前行的位置。 -
carry_hi == u16 sum(rotation -6)这里carry_hi的值应等于322 - 256 = 66位的u16数据的和。 -
carry_lo == u16 sum(rotation -7)这里carry_lo的值应等于193 - 128 = 65位的u16数据的和。 -
(t_lo - carry_lo \* 2^128) - c_lo确保乘法结果t_lo和c_lo的差与carry_lo乘以2^128的结果相匹配。 -
(t_hi + carry_lo - carry_hi \* 2^128) - c_hi确保乘法结果t_hi和c_hi的差与carry_hi乘以2^128的结果相匹配。
-
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
公式
在 SLT_SGT（有符号比较）子电路中，我们处理有符号数的比较，通过补码表示和无符号整数比较来实现。
符号判断
-
比较a_hi,b_hi最高u16位是否小于2^15通过检查最高16位来判断a和b的符号。如果a_lt == 1则a为正数，否则为负数。b_lt同理。
符号一致性约束
-
a_hi 和 b_hi 等于对应的 u16s_sum确保a和b的高16位在当前行的位置。 -
a,b 符号不相等时当a和b符号不相同时，约束(a_lt - b_lt)作为不相等条件。 -
a_lt == 1和carry == 0如果a_lt == 1（a为正数），则carry应为0；如果a_lt == 0（a为负数），则carry应为1。因此有约束1 - (a_lt + carry_hi)。 -
c_lo = u16 sum(rotation -4)c的低16位在当前行的位置。 -
c_hi = u16 sum(rotation -5)c的高16位在当前行的位置。 -
a,b 符号相等时当a和b符号相同时，约束(1 - (a_lt - b_lt))作为符号条件，与后续约束相乘。 -
a_lo + carry_lo \* 2^128 = b_lo + c_lo确保a的低16位加上进位与b的低16位加上c的低16位匹配。 -
a_hi + carry_hi \* 2^128 - carry_lo = b_hi + c_hi确保a的高16位加上进位减去carry_lo与b的高16位加上c的高16位匹配。 -
carry_hi = 1等价于a < bcarry_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
在 Sdiv_Smod（有符号除法和取余）中，我们处理有符号整数的除法和取余，以下是核心约束：
1 补码表示
-
计算
a和b的补码 使用补码表示法将负整数表示为其正值的按位取反加1。正整数的补码表示与其无符号表示相同。
2 无符号整数除法和取余
- 使用 DIV 和 MOD 操作码 执行无符号整数的除法和取余，得到正确的结果因为在第一步中我们已将有符号整数转换为无符号整数。
3 调整结果
-
当
a和b一正一负 需要对计算结果进行取反处理-x mod 2^256。 -
当
a为负数，b为正数时 只有被除数（a）是负数时，结果需要进行取反处理。
核心约束说明
根据上述补码的知识，我们有 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==0Layout
(因为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
公式
核心公式：
输入a,b,n 计算：
a + b mod n = r （式1）
可以将算式转换为： a + b = n * q + r （式2）
其中 q 是商，并没有实际出现在EVM的运算中，r 是余数。q 可能会超出 256 位，r 必须小于 n。
处理溢出:
- 如果
q超出 256 位，则需要一个额外的 1 位来处理溢出。 - 如果
n为 0，r必须设置为a + b，因为n为 0 时，a + b应直接作为结果r。
约束:
r < n-
r是结果的低位部分。 -
q的最大值为 256 位 + 1 位 carry 位（如果有溢出）。 -
n最大值为2256-1,q的最大值为2256-1，r的最大值为2256-2，那么n*q+r的最大值为：2512-2256-3。关键在于约束q的最大值为2256-1（q_overflow = 0 or 1） -
r必须小于n，否则需要调整q的溢出处理。 - 当
n = 0时，r设置为a + b，并且n处理为 0，以避免r超过 256 位。这时候式子2不能成立，这里直接让r=0（可以避免r超过256bit），使用n=0 判断式作为selector。
layout
| 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
核心公式
基础公式：
-
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
length 电路功能：
输入 offset, length, size
返回 real_len, zero_len, overflow, real_len_is_zero, zero_len_is_zero(？待定)
-
offset，length，size，需要 u64_overflow 约束
-
判断 offset + length > size
-
三种情况_(不管length是否为0)_，需要返回 return (real_len, zero_len)：
-
offset + length <= size， return (length, 0)
-
offset + length > size，分为两种情况：
-
offset < size ， return (size - offset, offset + length - size)
-
offset >= size, return (0, length).
-
arithmetic中的布局:
| operand0 | operand1 | operand2 | operand3 | cnt | u16s(0-3) | u16s(4_7) |
|---|---|---|---|---|---|---|
| real_len_inv | zero_len_inv | lt_offset_size | 2 | diff | diff_offset_size | |
| real_len | zero_len | real_len_is_zero | zero_len_is_zero | 1 | size | offset_bound |
| offset | length | size | overflow | 0 | offset | length |
约束
-
operand 和 u16s 大小相等
-
offset, size, length
-
offset_bound = offset + length
-
-
约束 size 是否小于 offset_bound
-
使用 SimpleLtGadget::new(size, offset_bound, overflow, diff)，range 设置为2^64
-
overflow is bool
-
-
约束 offset 是否小于 size
-
使用 SimpleLtGadget::new(offset, size, lt_offset_size, diff_offset_size)，range 设置为2^64
-
lt_offset_size is bool
-
-
三种情况下 (real_len, zero_len) 的约束：
参考上文，使用overflow 和 lt_offset_size 作为 selector，那么公式为：
- real_len = (1-overflow) * length
+ overflow * lt_offset_size * (size - offset)
- zero_len = overflow * lt_offset_size * (offset_bound - size)
+ overflow * (1 - lt_offset_size) * length
-
约束 real_len_is_zero, zero_len_is_zero
-
SimpleIsZero（real_len，real_len_inv）
-
SimpleIsZero（zero_len，zero_len_inv）
-
memory expansion
memory expansion 电路的功能是给定offset_bound，计算是否需要拓展内存。
offset_bound 的代表的是访问内存段的右区间：
-
访问长度length是固定的，比如 mload 指令, offset = 10，mload 一次访问 length=32，那么offset_bound = 42.
-
另外还存在另一种情况，访问内存时，给定了 offset， length 是任意值：当length 不为0，那么 offset_bound = offset + length。当length = 0，offset_bound = 0，所以这时候无论offset取什么值，内存都不会拓展。
电路设计
| operand0 | operand1 | operand2 | operand3 | cnt | u16s(0-3) | u16s(4_7) |
|---|---|---|---|---|---|---|
| r0 | 1 | diff | r1|r2|r3|r4 | |||
| offset_bound | memory_chunk_prev | expansion_tag | access_memory_size | 0 | offset_bound | access_memory_size |
约束设计：
::: 约束 operand 和 u16s :::
-
offset_bound = offset_bound
-
access_memory_size = access_memory_size
-
SimpleBinaryNumber::new（ ++r0|r1|r2|r3|r4++ ）.value = remainder
::: 约束 access_memory_size = \lfloor (offset + 31) / 32 \rfloor :::
- access_memory_size * 32 + remainder = offset + 31
::: 约束 memory_chunk_cur = Max( memory_chunk_prev， access_memory_size) :::
-
约束 expansion_tag 是 0 或 1
-
使用 SimpleLtGadget::new(memory_chunk_prev, access_memory_size, expansion_tag, diff)，range 设置为2^64
有length 的时候如何约束offset_bound
添加加一个 length_inv (大部分电路里面已经有了)
因为如果length= 0，offset_bound = 0;
否则 offset_bound = （offset + length）
那么公式为：
offset_bound = (offset + length) * length * length_inv
U64Overflow
公式
w=a_hi×2^64+a_lo
a_hi 和 a_lo：分别是 64 位的高位和低位部分。
w：是 a_lo 的前 64 位与 a_hi 左移 64 位的结果。
w_inv：w 的逆元素，用于处理 overflow 检测。
约束
-
检测
w是否发生了溢出，需要使用w和w_inv的simple is zero约束来实现。 -
w的溢出与否通过w \times w_inv判断，若为 0，则表示没有溢出，为 1 则表示发生了溢出。
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