ADDMOD

概述

概述：加法取模指令，对栈中的两个值进行加法取模计算（此操作的所有中间计算不受2^256模的限制。）。

具体操作：从栈顶弹出三个值a,b和n，对a，b进行整数加法再对n取模，将结果存进栈。

trace示例：

// Example 1
// Result 4
PUSH1 8
PUSH1 10
PUSH1 10
ADDMOD

// Example 2
// Result 1
PUSH1 2
PUSH1 2
PUSH32 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
ADDMOD

Witness Core Row

core row中的表格设计如下：

cnt=2，vers[0]~vers[8]的位置用来存放arithmetic table lookup；

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

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

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

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

/// +---+-------+-------+-------+----------+
/// |cnt| 8 col | 8 col | 8 col | not used |
/// +---+-------+-------+-------+----------+
/// | 2 | ARITH  |      |       |          |
/// | 1 | STATE | STATE | STATE | STATE    |
/// | 0 | DYNA_SELECTOR   | AUX            |
/// +---+-------+-------+-------+----------+

门约束

1. Auxiliary字段约束（state_stamp、stack_pointer、log_stamp、read_only）
2. Stack Value约束（tag、state_stamp、 call_id、stack_pointer、is_write）
3. 当前的OPCODE=ADDMOD
4. arithmetic tag = ADDMOD
5. todo...

参考如下代码：

LookUp约束

get_lookups

这里的四个lookup, 类型为LookupEntry::State和LookupEntry::Arithmetic, 具体可以参考Witness Core Row部分的说明。

参考代码如下: