Entrypoint for EVM circuit and specification for BEGIN_TX

setup.cfg

@@ -18,6 +18,8 @@ package_dir =
     = src
 packages = find:
 python_requires = >=3.6
+install_requires =
+    pycryptodome==3.11.0
 
 [options.packages.find]
 where = src

src/zkevm_specs/__init__.py

@@ -1,2 +1,4 @@
 from . import encoding
+from . import evm
 from . import opcode
+from . import util

src/zkevm_specs/evm/__init__.py

@@ -0,0 +1,8 @@
+from .execution import *
+from .execution_state import *
+from .main import *
+from .opcode import *
+from .precompiled import *
+from .step import *
+from .table import *
+from .typing import *

src/zkevm_specs/evm/execution/__init__.py

@@ -0,0 +1,7 @@
+from .begin_tx import *
+
+# Opcode's successful cases
+from .add import *
+from .push import *
+
+# Error cases

src/zkevm_specs/evm/execution/add.py

@@ -0,0 +1,24 @@
+from ..instruction import Instruction, Transition
+from ..opcode import Opcode
+
+
+def add(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(
+        instruction.add_word(instruction.select(is_sub, c, a), b)[0],
+        instruction.select(is_sub, a, c),
+    )
+
+    instruction.constrain_same_context_state_transition(
+        opcode,
+        rw_counter=Transition.delta(3),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(1),
+    )

src/zkevm_specs/evm/execution/begin_tx.py

@@ -0,0 +1,89 @@
+from ..instruction import Instruction, Transition
+from ..table import CallContextFieldTag, TxContextFieldTag, RW, AccountFieldTag
+from ..precompiled import PrecompiledAddress
+
+
+def begin_tx(instruction: Instruction, is_first_step: bool = False):
+    instruction.constrain_equal(instruction.curr.call_id, instruction.curr.rw_counter)
+
+    tx_id = instruction.call_context_lookup(CallContextFieldTag.TxId)
+    rw_counter_end_of_reversion = instruction.call_context_lookup(CallContextFieldTag.RWCounterEndOfReversion)
+    is_persistent = instruction.call_context_lookup(CallContextFieldTag.IsPersistent)
+
+    if is_first_step:
+        instruction.constrain_equal(instruction.curr.rw_counter, 1)
+        instruction.constrain_equal(tx_id, 1)
+
+    tx_caller_address = instruction.tx_lookup(tx_id, TxContextFieldTag.CallerAddress)
+    tx_callee_address = instruction.tx_lookup(tx_id, TxContextFieldTag.CalleeAddress)
+    tx_is_create = instruction.tx_lookup(tx_id, TxContextFieldTag.IsCreate)
+    tx_value = instruction.tx_lookup(tx_id, TxContextFieldTag.Value)
+    tx_call_data_length = instruction.tx_lookup(tx_id, TxContextFieldTag.CallDataLength)
+
+    # Verify nonce
+    tx_nonce = instruction.tx_lookup(tx_id, TxContextFieldTag.Nonce)
+    nonce, nonce_prev = instruction.account_write(tx_caller_address, AccountFieldTag.Nonce)
+    instruction.constrain_equal(tx_nonce, nonce_prev)
+    instruction.constrain_equal(nonce, nonce_prev + 1)
+
+    # TODO: Implement EIP 1559 (currently this assumes gas_fee_cap <= basefee + gas_tip_cap)
+    # Calculate gas fee
+    tx_gas = instruction.tx_lookup(tx_id, TxContextFieldTag.Gas)
+    tx_gas_fee_cap = instruction.tx_lookup(tx_id, TxContextFieldTag.GasFeeCap)
+    gas_fee, carry = instruction.mul_word_by_u64(tx_gas_fee_cap, tx_gas)
+    instruction.constrain_zero(carry)
+
+    # TODO: Use intrinsic gas (EIP 2028, 2930)
+    gas_left = tx_gas - (53000 if tx_is_create else 21000)
+    instruction.int_to_bytes(gas_left, 8)
+
+    # Prepare access list of caller and callee
+    instruction.constrain_equal(instruction.add_account_to_access_list(tx_id, tx_caller_address), 1)
+    instruction.constrain_equal(instruction.add_account_to_access_list(tx_id, tx_callee_address), 1)
+
+    # Verify transfer
+    instruction.constrain_transfer(
+        tx_caller_address,
+        tx_callee_address,
+        tx_value,
+        gas_fee=gas_fee,
+        is_persistent=is_persistent,
+        rw_counter_end_of_reversion=rw_counter_end_of_reversion,
+    )
+
+    if tx_is_create:
+        # TODO: Verify receiver address
+        # TODO: Set opcode_source to tx_id
+        raise NotImplementedError
+    elif tx_callee_address in list(PrecompiledAddress):
+        # TODO: Handle precompile
+        raise NotImplementedError
+    else:
+        code_hash, _ = instruction.account_read(tx_callee_address, AccountFieldTag.CodeHash)
+
+        # Setup next call's context
+        # Note that:
+        # - CallerCallId, ReturnDataOffset, ReturnDataLength, Result
+        #   should never be used in root call, so unnecessary to check
+        # - TxId is propagated from previous step or constraint to 1 if is_first_step
+        # - IsPersistent will be verified in the end of tx
+        for (tag, value) in [
+            (CallContextFieldTag.Depth, 1),
+            (CallContextFieldTag.CallerAddress, tx_caller_address),
+            (CallContextFieldTag.CalleeAddress, tx_callee_address),
+            (CallContextFieldTag.CallDataOffset, 0),
+            (CallContextFieldTag.CallDataLength, tx_call_data_length),
+            (CallContextFieldTag.Value, tx_value),
+            (CallContextFieldTag.IsStatic, False),
+        ]:
+            instruction.constrain_equal(instruction.call_context_lookup(tag), value)
+
+        instruction.constrain_new_context_state_transition(
+            rw_counter=Transition.delta(16),
+            call_id=Transition.persistent(),
+            is_root=Transition.to(True),
+            is_create=Transition.to(False),
+            opcode_source=Transition.to(code_hash),
+            gas_left=Transition.to(gas_left),
+            state_write_counter=Transition.to(2),
+        )

src/zkevm_specs/evm/execution/push.py

@@ -0,0 +1,26 @@
+from ..instruction import Instruction, Transition
+from ..opcode import Opcode
+
+
+def push(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+    num_pushed = opcode - Opcode.PUSH1 + 1
+    num_additional_pushed = num_pushed - 1
+
+    value = instruction.stack_push()
+    value_bytes = instruction.rlc_to_bytes(value, 32)
+    selectors = instruction.continuous_selectors(num_additional_pushed, 31)
+
+    for idx in range(32):
+        index = instruction.curr.program_counter + num_pushed - idx
+        if idx == 0 or selectors[idx - 1]:
+            instruction.constrain_equal(value_bytes[idx], instruction.opcode_lookup_at(index, False))
+        else:
+            instruction.constrain_zero(value_bytes[idx])
+
+    instruction.constrain_same_context_state_transition(
+        opcode,
+        rw_counter=Transition.delta(1),
+        program_counter=Transition.delta(1 + num_pushed),
+        stack_pointer=Transition.delta(-1),
+    )