虛擬境界28：EVM Circuits 範例 - JUMPI - iT 邦幫忙::一起幫忙解決難題，拯救 IT 人的一天

2023 iThome 鐵人賽

DAY 28

Web 3

以 Python 進入以太坊虛擬機 (EVM) 的幻想境界系列第 28 篇

虛擬境界28：EVM Circuits 範例 - JUMPI

15th鐵人賽

kidneyweakx

2023-10-13 10:08:52

454 瀏覽

分享至

在 Ethereum 虛擬機(EVM) 中，JUMPI 是一個條件跳躍指令。它從堆疊(Stack)中彈出兩個元素：目的地(dest)和條件(cond)。如果 cond 不是 0，則程序計數器(pc) 被設置為 dest，代碼跳轉到 dest 位置並開始執行；如果 cond 是 0，則繼續執行下一個指令。在跳轉目的地，JUMPDEST 操作碼通常會被用來標記一個有效的跳轉位置。

電路介紹

1. 表格和變數

(op, dest, cond) = (87, 4, cond): 這是一個操作的示例，其中 87 是 JUMPI 操作的操作碼，4 是跳躍的目的地，cond 是壓縮形式的條件值。
表格中的 q, a_1 到 a_32 表示的是約束和操作的不同變數和狀態。

2. 約束和查詢

條件約束: 只有當操作碼是 JUMPI (op - 87 為 0) 時，自定義約束才被激活。
讀取操作: 使用 bus_mapping_lookup 函數讀取堆疊中的 dest 和 cond 值。
跳躍約束: pc_next 的值取決於 cond 是否為 0，並可能設置為 dest 或 pc + 1。

3. 案例約束

這部分定義了在不同的執行情況（例如成功、out_of_gas錯誤、stack_underflow錯誤、無效或超出範圍的跳轉目的地）下應該應用的約束和操作。

實作要點

正常操作：當操作碼是JUMPI並且操作成功時，進行兩個讀取操作（一個用於目的地，另一個用於條件）。如果條件為非0，程式計數器跳到指定的目的地，否則增加1。堆疊指針增加2，因為兩個值已從堆疊中彈出。
異常操作：在不同的錯誤情況下（例如：out of gas、stack underflow、無效或超出範圍的跳轉目的地），需要定義不同的約束和操作。具體情況下的操作未在提供的代碼段中詳細定義（用TODO標記），但它們通常會包括檢查某些條件（例如：gas用量、堆疊大小和跳轉目的地的有效性）並可能進行一些清理或回滾操作。

備註

JUMPI 指令確實涉及到複雜的檢查和條件分支，並且在處理合約時需要仔細處理和驗證，以確保跳轉的合法性和安全性。
確保在實現這些約束時處理所有可能的邊界情況和錯誤情況，以避免任何潛在的安全問題。

範例

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

Python

def jumpi(instruction: Instruction):
    opcode = instruction.opcode_lookup(True)
    instruction.constrain_equal(opcode, Opcode.JUMPI)

    # Do not check 'dest' is within MaxCodeSize(24576) range in successful case
    # as byte code lookup can ensure it.
    dest_word = instruction.stack_pop()
    instruction.constrain_zero(dest_word.hi.expr())
    dest = dest_word.lo.expr()

    cond = instruction.stack_pop()

    # check `cond` is zero or not
    if instruction.is_zero_word(cond):
        pc_diff = FQ(1)
    else:
        pc_diff = dest - instruction.curr.program_counter
        # assert Opcode.JUMPDEST == instruction.opcode_lookup_at(dest_value, True)
        instruction.constrain_equal(Opcode.JUMPDEST, instruction.opcode_lookup_at(dest, True))

    instruction.step_state_transition_in_same_context(
        opcode,
        rw_counter=Transition.delta(2),
        program_counter=Transition.delta(pc_diff),
        stack_pointer=Transition.delta(2),
    )