在這個 EVM Circuits 的範例中，我們將運用多個不同的元素，如槽位(slot)、選擇器(q)、和多個變數(如op, va, vb, vc)，來驗證一個智能合約操作 (例如 8 = 3 + 5) 的正確性，而不會暴露操作的具體細節。

基本理解

• (op, va, vb, vc) = (1, 3, 5, 8): 這是一個示例，用於驗證 8 = 3 + 5，其中 “op” 代表操作，可能是 ADD、MUL、SUB 等。1、3、5、8分別代表處理的數值。
• v0..v31: 這些是解壓的操作值，它們用於在進行 byte 到 byte 檢查的情況下揭示輸入與輸出之間的關係。

表格和約束

在給定的表格範例中，"q", "a_1" 到 "a_32" 是定義的各種變數和操作。"q" 是用於開啟特定約束的選擇器，而 "a_1" 到 "a_32" 可能是用於存儲或操作數據的部分。

1. 操作碼約束: 當選擇器為 “1” 並且操作是ADD時，應適用特定的約束。這些約束涉及兩個源值的讀取、一個結果的寫入，以及檢查結果是否實際上是由兩個源值添加得到的。
2. CASE約束: 當操作碼是 ADD 並且相應的 case 條件為true時(例如:成功、out_of_gas錯誤、stack_underflow錯誤)，相應的約束應被應用。

實現細節

• 開啟約束: 使用 is_zero(op - 1) 確定只有當操作是ADD時，自定義約束才會被開啟。
• 資料查詢: 使用 bus_mapping_lookup 函數來查詢與特定操作相關的資料(例如:資料讀取和寫入)。
• 加法驗證: 進行8位加法檢查，確保每個字節與進位位一起正確添加。
• 下一槽位約束: 如 gc_next === gc + 3，確保下一個全局計數器的值符合預期。
• 地址、程式計數器和堆疊指針的約束: 類似地，應該有確保其他變數值符合預期的約束。

注意點

• 8 位範圍檢查可能在其他操作中是免費的，因為它可以與其他 boolean 表達式一起加入開關。
• 一旦確定所有值都在 8 位範圍內，只需迭代檢查每個字節是否使用進位位正確添加，使用簡單的自定義約束。
• 確保例外執行正常，例如：ErrOutOfGas 和 ErrStackUnderflow）。
• 對每個操作都要定義正確讀寫操作，確保運行正常。

範例

// switch on custom constraint only when the opcode is ADD
if is_zero(op - 1) {
    if case_success {
        // two source read
        for (gc, sp, v) in [(gc, sp, va), (gc+1, sp+1, vb)] {
            bus_mapping_lookup(
                gc,
                Stack,
                sp,
                compress(v),
                Read
            )
        }

        // one result write
        bus_mapping_lookup(
            gc+2,
            Stack,
            sp+1,
            compress(vc),
            Write
        )

        // result is indeed added by two source
        eight_bit_lookup(va[0])
        eight_bit_lookup(vb[0])
        eight_bit_lookup(vc[0])
        256 * carry[0] + vc[0] === va[0] + vb[0]

        for i in range 1..=31 {
            eight_bit_lookup(va[i])
            eight_bit_lookup(vb[i])
            eight_bit_lookup(vc[i])

            256 * carry[i] + vc[i] === va[i] + vb[i] + carry[i-1]
        }

        // gc in the next slot should increase 3
        gc_next === gc + 3

        // addr should be same
        addr_next === addr

        // pc should increase 1
        pc_next === pc + 1

        // sp should increase 1 (ADD = 2 POP + 1 PUSH)
        sp_next === sp + 1
    }

    if case_err_out_of_gas {
        // TODO:
        // - gas_left > gas_cost
        // - consume all give gas
        // - context switch to parent
        // - ...
    }

    if case_err_stack_underflow {
        // TODO:
        // - sp + 1 === 1023 + surfeit
        // - consume all give gas
        // - context switch to parent
        // - ...
    }
}

Python Circuits 實現

def add_sub(instruction: Instruction):
    opcode = instruction.opcode_lookup(True)

    is_sub, _ = instruction.pair_select(opcode, Opcode.SUB, Opcode.ADD)

    a = instruction.stack_pop()
    b = instruction.stack_pop()
    c = instruction.stack_push()

    instruction.constrain_equal_word(
        instruction.add_words([instruction.select_word(is_sub, c, a), b])[0],
        instruction.select_word(is_sub, a, c),
    )

    instruction.step_state_transition_in_same_context(
        opcode,
        rw_counter=Transition.delta(3),
        program_counter=Transition.delta(1),
        stack_pointer=Transition.delta(1),
    )

參考資料

• https://hackmd.io/@liangcc/zkvmbook/%2Fq8EhMIp_TimpPWWFXtwOVw
• https://github.com/privacy-scaling-explorations/zkevm-specs/blob/master/src/zkevm_specs/evm_circuit/execution/add_sub.py