appliedzkp的zkevm（6）EVM Circuit

1. 引言

相关定义有：

• slot：一个slot内有多行（rows），用于verify a single op
• q：为enable a slot的selector，should be 1 only in the last row in a slot。
• x_diff_inv：为Prover witness，等于inv(fixde_x-x)，其中fixed_x为baked into circuit。用于switch on op and case custom constraint by 1-(fixed_x-x)*x_diff_inv （为is_zero expression）。
• context：有： – gc: global counter – addr: address holding opcodes – pc: program counter – op: operator respect to addr and pc – sp: stack pointer 等等
• v0…v31：为decompressed operating values in word bytes from low to high (0x42 will be [0x42, 0, …, 0])
• inv：为field fq域内的倒数，若不存在则返回0。
• compress：用于压缩variadic inputs into single fq using random linear combination。

2. Layout

在evm circuit中，需在单个固定的slot中，验证包括错误场景在内的所有可能的opcodes，因此，需要Prover提供一些auxiliary values来switch on custom constraint。 evm circuit主要包含3大维度：

• operating values：即opcode的输入输出。如ADD有2个输入，1个输出。Decompression is needed when the relation between inputs and outputs requires byte to byte check。
• context：the current context evm holds，可有gc, addr, pc等等。
• op and case switch：circuit的auxiliary values可用于知悉which custom constraint of opcodes and cases to switch on. 直观来说，可要求Prover来witness the {op,case}_diff_inv for circuit to produce a is_zero boolean expression to switch the op。 这样就可表达执行一个op所能遇到的所有场景。如以ADD为例，其有1种成功场景和2种错误场景——ErrOutOfGas和ErrStackUnderflow。

3. 举例——ADD

若不限制wire number，可有wide circuit (w=32) 来将每个word放一行。对于(op, va, vb, vc) = (1, 3, 5, 8) （用于验证8 = 3 + 5），可将这些值 decompress in bus mapping into 3 v0..v31 and do custom constraint of ADD： 则有如下constraints（cur() to the last row）：

// 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
        // - ...
    }
}

注意，此处并不需要8-bit addition lookup，因为在 comparators 中已使用8-bit range lookup 来check if values are in 8-bit。因此 8-bit range check become free for other ops because we only need to add the switch boolean expression together to enable it。 一旦确认了all values are in 8-bit，仅需iteratively check every bytes are added correctly with the carry bit by simple custom constraint。

4. 举例——JUMPI

如有 (op, dest, cond) = (87, 4, cond) (to verify a jump to pc=4 when condition is non zero)。此处cond为compressed form of actual value, which is used directly by is_zero gadget to check if it’s zero or not, prover has negligible chance to compress a non zero value into 0. (is_zero gadget needs another cell to allocate inverse of cond to produce the expression, so is the inv(cond) )。 未来如有需要，可进一步优化cells cost，因为a contract可有0x6000个opcodes，因此dest可fit in two cells。

// switch on custom constraint only when the opcode is JUMPI
if is_zero(op - 87) {
    if case_success {
        // one stack read for destination
        bus_mapping_lookup(
            gc,
            Stack,
            sp,
            compress(dest),
            Read
        )

        // one stack read for condition
        bus_mapping_lookup(
            gc+1,
            Stack,
            sp+1,
            cond,
            Read
        )

        // we don't jump when condition is zero
        if is_zero(cond) {
            pc_next === pc + 1 // pc should increase by 1
        } else {
            pc_next === dest // pc should change to dest
            op_next === 91   // destination should be JUMPDEST
        }

        gc_next === gc + 1 // gc should increase by 1
        addr_next === addr // addr remains the same
        sp_next === sp + 2 // sp should increase by 2 (JUMPI = 2 POP)
    }

    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
        // - ...
    }}

    if case_err_jump_dest_invalid {
        // TODO:
        // - op_lookup(addr, dest, dest_op) && dest_op !== JUMPDEST
        // - consume all give gas
        // - context switch to parent
        // - ...
    }

    if case_err_jump_dest_out_of_range {
        // TODO:
        // - dest >= len(code)
        // - consume all give gas
        // - context switch to parent
        // - ...
    }
}

5. Q&A

参考资料

[1] https://hackmd.io/@liangcc/zkvmbook/%2Fq8EhMIp_TimpPWWFXtwOVw