ADD 指令

本节和接下来的章节主要介绍 EVM 中各个指令的具体操作、约束条件和 witness 表示，以及如何在电路设计中实现和验证相关指令。

详细设计

概述

概述：加法指令，对栈中的两个值进行加法计算（256位）。

具体操作：从栈顶弹出两个值a和b，进行整数加法（mod 2^256），将结果存进栈。

trace示例：

// Example 1 
// Result 20 //0x14
PUSH1 10 //0x0A
PUSH1 10 //0x0A
ADD

// Example 2
// Result 0x0
PUSH32 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
PUSH1 1 //0x01
ADD

由于在evm中ADD指令会自动从栈中弹出两个操作数并将结果推入栈中，所以在trace中没有显式的POP操作。

示例具体操作流程如下：

初始状态：

• 栈内容：[a, b]
• 其中，a 和 b 是256位整数，a 在栈顶，b 在栈顶下方。

操作步骤：

• 弹出值：从栈中弹出两个值 a 和 b。此时栈变为空。
• 计算：执行加法操作：result = (a + b) % 2^256。这个操作确保结果始终保持在256位整数范围内。
• 推入结果：将计算得到的结果 result 推入栈中。

最终状态：

• 栈内容：[result]

注：SUB指令、MUL指令、DIV指令、MOD指令与ADD指令相似，因此实现在同一代码文件中，参考 zkevm-circuits/src/execution/add_sub_mul_div_mod.rs 。

Witness Core Row

core row中的表格设计如下：

cnt	ver[0-7]	ver[8-15]	ver[16-23]	其他
2	ARITH	-	-	-
1	STATE (stack_pop_a)	STATE (stack_pop_b)	STATE (stack_push)	-
0	DYNA_SELECTOR	AUX	-	-

cnt=2，vers[0]~vers[8]的位置用来存放arithmetic table lookup，目的是将具体的算数约束放在arithmetic子电路中，将core子电路与具体的算数约束解耦；

cnt=1，vers[0]~vers[7]的位置用来存放栈顶弹出的值stack_pop_a；

cnt=1，vers[8]~vers[15]的位置用来存放栈顶弹出的值stack_pop_b；

cnt=1，vers[16]~vers[23]的位置用来存进栈顶的值stack_push。

门约束

1. Auxiliary字段约束：

   这些约束用于辅助字段，如 state_stamp、stack_pointer、log_stamp 和 read_only，确保这些字段在操作期间保持一致。

2. Core专有的单功能列约束：

   约束单功能列如pc、code_addr等，确保下一个状态其值正确。

3. Stack Value约束：

   这些约束用于栈的值，包括以下内容：

   • tag
   • state_stamp
   • call_id
   • stack_pointer
   • is_write

   同时提取出栈中的值，即lookup_stack_pop_a, lookup_stack_pop_b, lookup_stack_push。

4. lookup_value约束：

   这些约束确保算术操作数和栈操作的值一致。具体来说：

   • arithmetic_operand_a = lookup_stack_pop_a
   • arithmetic_operand_b = lookup_stack_pop_b
   • arithmetic_operand_push = lookup_stack_push

   这些约束对操作数的高位 (hi) 和低位 (lo) 进行约束，并确保它们与状态查找中的值相等。

5. 当前的 OPCODE = ADD

6. 用于 arithmetic table lookup 的 arithmetic tag = ADD

LookUp约束

这里的四个lookup, 其中3个为类型为LookupEntry::State，其余为 LookupEntry::Arithmetic, 具体可以参考：

• 5-state
• 8-arithmetic