ADD

概述

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

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

trace示例：

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

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

Witness Core Row

core row中的表格设计如下：

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

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

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

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

/// +---+-------+-------+-------+----------+
/// |cnt| 8 col | 8 col | 8 col | not used |
/// +---+-------+-------+-------+----------+
/// | 2 | ARITH  |      |       |          |
/// | 1 | 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. lookup_value约束：lookup_stack_pop_b = stack_top0（栈顶的值需要和lookup_stack_pop_b相等）
4. lookup_value约束：lookup_stack_pop_a = stack_top1 （弹出一个值后，栈顶的值需要和lookup_stack_pop_a相等）
5. lookup_value约束：lookup_stack_push = stack_top1（存进一个值后，栈顶的元素需要和lookup_stack_push相等）
6. lookup_value约束：arithmetic_operand_b = lookup_stack_pop_b，arithmetic_operand_a = lookup_stack_pop_a，arithmetic_operand_push = lookup_stack_push（这里对三个操作数的hi,lo进行约束，需要和state lookup里的值相等）
7. 当前的OPCODE=ADD
8. arithmetic tag = ADD

参考如下代码：

fn get_constraints(
    &self,
    config: &ExecutionConfig<F, NUM_STATE_HI_COL, NUM_STATE_LO_COL>,
    meta: &mut VirtualCells<F>,
) -> Vec<(String, Expression<F>)> {
    let opcode = meta.query_advice(config.opcode, Rotation::cur());
    // Auxiliary字段约束 ...

    // Stack Value约束 ...

    let mut arithmetic_operands = vec![];
    for i in 0..3 {
        let entry = config.get_state_lookup(meta, i);
        constraints.append(&mut config.get_stack_constraints(
            meta,
            entry.clone(),
            i,
            NUM_ROW,
            if i == 0 { 0 } else { -1 }.expr(),
            i == 2,
        ));
        let (_, _, value_hi, value_lo, _, _, _, _) = extract_lookup_expression!(state, entry);
        arithmetic_operands.extend([value_hi, value_lo]);
    }
    
    let (tag, arithmetic_operands_full) =
        extract_lookup_expression!(arithmetic, config.get_arithmetic_lookup(meta));
    // iterate over three operands (0..6), since we don't need constraint on the fourth
    constraints.extend((0..6).map(|i| {
        (
            format!("operand[{}] in arithmetic = in state lookup", i),
            arithmetic_operands[i].clone() - arithmetic_operands_full[i].clone(),
        )
    }));

    // 其它约束 ...
    constraints
}

LookUp约束

cnt=2的vers[0]~vers[8]的位置用来存放操作数的信息。

来源：core

去向：arithmetic

参考代码如下：

fn gen_witness(&self, trace: &GethExecStep, current_state: &mut WitnessExecHelper) -> Witness {
    assert_eq!(trace.op, OpcodeId::ADD);
    let (stack_pop_a, a) = current_state.get_pop_stack_row_value(&trace);
    let (stack_pop_b, b) = current_state.get_pop_stack_row_value(&trace);
    let (arithmetic, result) = operation::add::gen_witness(vec![a, b]);

    let stack_push = current_state.get_push_stack_row(trace, result[0]);
    let mut core_row_2 = current_state.get_core_row_without_versatile(&trace, 2);
    core_row_2.insert_arithmetic_lookup(&arithmetic);
    let mut core_row_1 = current_state.get_core_row_without_versatile(&trace, 1);
    core_row_1.insert_state_lookups([&stack_pop_a, &stack_pop_b, &stack_push]);
    let core_row_0 = ExecutionState::ADD.into_exec_state_core_row(
        trace,
        current_state,
        NUM_STATE_HI_COL,
        NUM_STATE_LO_COL,
    );

    Witness {
        core: vec![core_row_2, core_row_1, core_row_0],
        state: vec![stack_pop_b, stack_pop_a, stack_push],
        arithmetic,
        ..Default::default()
    }
}

get_lookups

这里的lookup类型为LookupEntry::State和LookupEntry::Arithmetic。

参考代码如下:

fn get_lookups(
    &self,
    config: &ExecutionConfig<F, NUM_STATE_HI_COL, NUM_STATE_LO_COL>,
    meta: &mut ConstraintSystem<F>,
) -> Vec<(String, LookupEntry<F>)> {
    let stack_lookup_0 = query_expression(meta, |meta| config.get_state_lookup(meta, 0));
    let stack_lookup_1 = query_expression(meta, |meta| config.get_state_lookup(meta, 1));
    let stack_lookup_2 = query_expression(meta, |meta| config.get_state_lookup(meta, 2));
    let arithmetic = query_expression(meta, |meta| config.get_arithmetic_lookup(meta));
    vec![
        ("stack pop a".into(), stack_lookup_0),
        ("stack pop b".into(), stack_lookup_1),
        ("stack push".into(), stack_lookup_2),
        ("arithmetic lookup".into(), arithmetic),
    ]
}


pub(crate) fn get_arithmetic_lookup(&self, meta: &mut VirtualCells<F>) -> LookupEntry<F> {
    let (hi_0, lo_0, hi_1, lo_1, hi_2, lo_2, hi_3, lo_3, tag) = (
        meta.query_advice(self.vers[0], Rotation(-2)),
        meta.query_advice(self.vers[1], Rotation(-2)),
        meta.query_advice(self.vers[2], Rotation(-2)),
        meta.query_advice(self.vers[3], Rotation(-2)),
        meta.query_advice(self.vers[4], Rotation(-2)),
        meta.query_advice(self.vers[5], Rotation(-2)),
        meta.query_advice(self.vers[6], Rotation(-2)),
        meta.query_advice(self.vers[7], Rotation(-2)),
        meta.query_advice(self.vers[8], Rotation(-2)),
    );
    LookupEntry::Arithmetic {
        tag,
        values: [hi_0, lo_0, hi_1, lo_1, hi_2, lo_2, hi_3, lo_3],
    }
}