Add spec for CREATE(2)

specs/opcode/F0CREATE_F5CREATE2.md

@@ -0,0 +1,97 @@
+# CREATE and CREATE2 opcodes
+
+## Procedure
+
+### EVM behavior
+
+The `CREATE` and `CREATE2` opcodes create a new call context at a new address.
+They transfer the specified amount of ether from the caller address to the new address and then execute the specified initialization code.
+The bytecode of the new address will be updated to be the return bytes of this initialization code.
+
+The following values are popped from the stack:
+1. `value` - The amount of ether to transfer from the caller to the new address.
+2. `offset` - The memory offset in the caller's memory where the initialization code starts.
+3. `size` - The length of the initialization code, in bytes.
+4. `salt` - Only for `CREATE2`: salt for the hash that will determine the new address.
+
+If the initialization call is successful, the new address will be pushed to the stack.
+If not, 0 will be pushed instead.
+
+The gadget does several things in the caller's call context:
+1. Expands memory
+2. Add `new_address` to the access list
+3. Calculate gas cost for this step.
+4. Uses EIP150 to calculate how much gas will remain in the caller's context.
+
+The memory size is calculated as follows:
+
+```
+calc_memory_size(offset, length) := 0 if length == 0 else ceil((offset + length) / 32)
+```
+
+`new_address` is calculated as follows:
+
+```
+new_address := keccak256([0xff] + caller_address + salt + keccak256(initialization_bytecode)) if op_id == CREATE2 else rlp([caller_address, caller_address.nonce])
+```
+
+The memory expansion gas cost is:
+
+```
+MEMORY_EXPANSION_QUAD_DENOMINATOR := 512
+MEMORY_EXPANSION_LINEAR_COEFF := 3
+calc_memory_cost(memory_size) := MEMORY_EXPANSION_LINEAR_COEFF * memory_size + floor(memory_size * memory_size / MEMORY_EXPANSION_QUAD_DENOMINATOR)
+```
+
+The gas cost charged for the additional `memory_size` is:
+
+```
+next.memory_size := max(
+    curr.memory_size,
+    memory_size(offset, length),
+)
+memory_expansion_gas_cost := calc_memory_cost(next.memory_size) - memory_cost(curr.memory_size)
+```
+
+The `gas_cost` for the step is:
+
+```
+GAS_COST_CREATE := 32000
+KECCAK_WORD_GAS_COST : 6
+
+keccak_gas_cost = KECCAK_WORD_GAS_COST * size if op_id == CREATE2 else 0
+gas_cost = (
+    GAS_COST_CREATE
+    + memory_expansion_gas_cost
+    + keccak_gas_cost
+)
+```
+
+The `callee_gas_left` for new context by rule in EIP150 is calculated like this:
+
+```
+gas_available := curr.gas_left - gas_cost
+callee_gas_left := min(gas_available - floor(gas_available / 64), gas)
+```
+
+In the initialization call context, it does:
+
+1. Transfer `value` from the caller address to the new address
+2. Executes the initialization bytecode
+3. Update the bytecode of the new address to be the `return_data` of execution
+
+### Circuit behavior
+
+The circuit takes the starting `rw_counter` as next call's `call_id` to make sure each call has a unique `call_id`.
+
+It pops 3 words for `CREATE` and 4 words for `CREATE2` from the stack.
+In both cases, it then pushes 1 word to the stack.
+
+It then checks that `callee.is_persistent = caller.is_persistent and caller.is_success`.
+If the caller is not persistent, we need to propagate the `rw_counter_end_of_reversion` to make sure every state update in the new call has a corresponding reversion.
+
+It stores the current call context by writing the current values `rw_table` and checks that the new call context is setup correctly by reading to `rw_table`, and then does a step state transition to the call and begins the execution o the initialization bytecode.
+
+## Code
+
+Please refer to `src/zkevm_specs/evm/execution/create.py`.

src/zkevm_specs/copy_circuit.py

@@ -42,7 +42,7 @@ def verify_row(cs: ConstraintSystem, rows: Sequence[CopyCircuitRow]):
         cs.constrain_equal(rows[0].addr + 1, rows[2].addr)
         cs.constrain_equal(rows[0].src_addr_end, rows[2].src_addr_end)
 
-    # contrain the transition for `rw_counter` and `rwc_inc_left`
+    # constrain the transition for `rw_counter` and `rwc_inc_left`
     rw_diff = (1 - rows[0].is_pad) * (rows[0].is_memory + rows[0].is_tx_log)
     with cs.condition(1 - rows[0].is_last) as cs:
         # not last row

src/zkevm_specs/evm_circuit/execution/__init__.py

@@ -52,6 +52,7 @@
 from .sdiv_smod import sdiv_smod
 from .sha3 import sha3
 from .shl_shr import shl_shr
+from .create import create
 from .signextend import *
 from .stop import stop
 from .return_revert import *
@@ -113,6 +114,8 @@
     ExecutionState.SAR: sar,
     ExecutionState.SDIV_SMOD: sdiv_smod,
     ExecutionState.SHL_SHR: shl_shr,
+    ExecutionState.CREATE: create,
+    ExecutionState.CREATE2: create,
     ExecutionState.STOP: stop,
     ExecutionState.RETURN: return_revert,
     ExecutionState.ErrorInvalidJump: invalid_jump,

src/zkevm_specs/evm_circuit/execution/create.py

@@ -0,0 +1,200 @@
+from zkevm_specs.evm_circuit.opcode import Opcode
+from zkevm_specs.util.arithmetic import FQ, Word, WordOrValue
+from zkevm_specs.util.hash import EMPTY_CODE_HASH
+from zkevm_specs.util.param import (
+    GAS_COST_COPY_SHA3,
+    GAS_COST_CREATE,
+    N_BYTES_ACCOUNT_ADDRESS,
+    N_BYTES_GAS,
+    N_BYTES_MEMORY_ADDRESS,
+    N_BYTES_MEMORY_SIZE,
+    N_BYTES_U64,
+)
+from ...util import (
+    CALL_CREATE_DEPTH,
+)
+from ..instruction import Instruction, Transition
+from ..table import RW, CallContextFieldTag, AccountFieldTag, CopyDataTypeTag
+
+
+def create(instruction: Instruction):
+    # check opcode is CREATE or CREATE2
+    opcode = instruction.opcode_lookup(True)
+    is_create, is_create2 = instruction.pair_select(opcode, Opcode.CREATE, Opcode.CREATE2)
+    instruction.responsible_opcode_lookup(opcode)
+
+    # set the caller_id to the current rw_counter
+    callee_call_id = instruction.curr.rw_counter
+
+    # Stack parameters and result
+    value_word = instruction.stack_pop()
+    offset_word = instruction.stack_pop()
+    size_word = instruction.stack_pop()
+    salt_word = instruction.stack_pop() if is_create2 == FQ(1) else Word(0)
+    return_contract_address_word = instruction.stack_push()
+
+    offset = instruction.word_to_fq(offset_word, N_BYTES_MEMORY_ADDRESS)  # src_addr
+    size = instruction.word_to_fq(size_word, N_BYTES_MEMORY_ADDRESS)
+
+    depth = instruction.call_context_lookup(CallContextFieldTag.Depth)
+    tx_id = instruction.call_context_lookup(CallContextFieldTag.TxId)
+    caller_address = instruction.call_context_lookup(CallContextFieldTag.CallerAddress)
+    nonce, nonce_prev = instruction.account_write(caller_address, AccountFieldTag.Nonce)
+    is_success = instruction.call_context_lookup(CallContextFieldTag.IsSuccess)
+    is_static = instruction.call_context_lookup(CallContextFieldTag.IsStatic)
+    reversion_info = instruction.reversion_info()
+
+    # calculate contract address
+    contract_address = (
+        instruction.generate_contract_address(caller_address, nonce)
+        if is_create == 1
+        else instruction.generate_CREAET2_contract_address(
+            caller_address, salt_word, instruction.next.code_hash
+        )
+    )
+
+    # verify the equality of input `size` and length of calldata
+    code_size = instruction.bytecode_length(instruction.next.code_hash)
+    instruction.constrain_equal(code_size, size)
+
+    # verify return contract address
+    instruction.constrain_equal(
+        instruction.word_to_fq(return_contract_address_word, N_BYTES_ACCOUNT_ADDRESS),
+        is_success * contract_address,
+    )
+
+    # Verify depth is less than 1024
+    instruction.range_lookup(depth, CALL_CREATE_DEPTH)
+
+    # ErrNonceUintOverflow constraint
+    (is_not_overflow, _) = instruction.compare(nonce, nonce_prev, N_BYTES_U64)
+    instruction.is_zero(is_not_overflow)
+
+    # add contract address to access list
+    instruction.add_account_to_access_list(tx_id, contract_address)
+
+    # ErrContractAddressCollision constraint
+    # code_hash_prev could be either 0 or EMPTY_CODE_HASH
+    # code_hash should be EMPTY_CODE_HASH to make sure the account is created properly
+    code_hash, code_hash_prev = instruction.account_write_word(
+        contract_address, AccountFieldTag.CodeHash
+    )
+    instruction.constrain_in_word(
+        code_hash_prev,
+        [Word(0), Word(EMPTY_CODE_HASH)],
+    )
+    instruction.constrain_equal_word(code_hash, Word(EMPTY_CODE_HASH))
+
+    # Propagate is_persistent
+    callee_reversion_info = instruction.reversion_info(call_id=callee_call_id)
+    instruction.constrain_equal(
+        callee_reversion_info.is_persistent,
+        reversion_info.is_persistent * is_success.expr(),
+    )
+
+    # can't be a STATICCALL
+    instruction.is_zero(is_static)
+
+    # transfer value from caller to contract address
+    instruction.transfer(caller_address, contract_address, value_word, callee_reversion_info)
+
+    # gas cost of memory expansion
+    (
+        next_memory_size,
+        memory_expansion_gas_cost,
+    ) = instruction.memory_expansion(
+        offset,
+        size,
+    )
+
+    # CREATE = GAS_COST_CREATE + memory expansion + GAS_COST_CODE_DEPOSIT * len(byte_code)
+    # CREATE2 = gas cost of CREATE + GAS_COST_COPY_SHA3 * memory_size
+    # byte_code is only available in `return_revert`,
+    # so the last part (GAS_COST_CODE_DEPOSIT * len(byte_code)) won't be calculated here
+    gas_left = instruction.curr.gas_left
+    gas_cost = GAS_COST_CREATE + memory_expansion_gas_cost
+    if is_create2 == 1:
+        memory_size, _ = instruction.constant_divmod(size + FQ(31), FQ(32), N_BYTES_MEMORY_SIZE)
+        gas_cost += GAS_COST_COPY_SHA3 * memory_size
+    gas_available = gas_left - gas_cost
+
+    # Apply EIP 150
+    one_64th_gas, _ = instruction.constant_divmod(gas_available, FQ(64), N_BYTES_GAS)
+    all_but_one_64th_gas = gas_available - one_64th_gas
+    is_u64_gas = instruction.is_zero(
+        instruction.sum(WordOrValue(gas_left).to_le_bytes()[N_BYTES_GAS:])
+    )
+    callee_gas_left = instruction.select(
+        is_u64_gas,
+        instruction.min(all_but_one_64th_gas, gas_left, N_BYTES_GAS),
+        all_but_one_64th_gas,
+    )
+
+    # copy init_code from memory to bytecode
+    copy_rwc_inc, _ = instruction.copy_lookup(
+        instruction.curr.call_id,  # src_id
+        CopyDataTypeTag.Memory,  # src_type
+        instruction.next.code_hash,  # dst_id
+        CopyDataTypeTag.Bytecode,  # dst_type
+        offset,  # src_addr
+        offset + size,  # src_addr_boundary
+        FQ(0),  # dst_addr
+        size,  # length
+        instruction.curr.rw_counter + instruction.rw_counter_offset,
+    )
+    instruction.rw_counter_offset += int(copy_rwc_inc)
+
+    # CREATE:  3 pops and 1 push, stack delta = 2
+    # CREATE2: 4 pops and 1 push, stack delta = 3
+    stack_pointer_delta = 2 + is_create2
+    # Save caller's call state
+    for field_tag, expected_value in [
+        (CallContextFieldTag.ProgramCounter, instruction.curr.program_counter + 1),
+        (
+            CallContextFieldTag.StackPointer,
+            instruction.curr.stack_pointer + stack_pointer_delta,
+        ),
+        (CallContextFieldTag.GasLeft, gas_left - gas_cost - callee_gas_left),
+        (CallContextFieldTag.MemorySize, next_memory_size),
+        (
+            CallContextFieldTag.ReversibleWriteCounter,
+            instruction.curr.reversible_write_counter + 1,
+        ),
+    ]:
+        instruction.constrain_equal(
+            instruction.call_context_lookup(field_tag, RW.Write),
+            expected_value,
+        )
+
+    # Setup next call's context.
+    for field_tag, expected_value in [
+        (CallContextFieldTag.CallerId, instruction.curr.call_id),
+        (CallContextFieldTag.TxId, tx_id),
+        (CallContextFieldTag.Depth, depth + 1),
+        (CallContextFieldTag.CallerAddress, caller_address),
+        (CallContextFieldTag.CalleeAddress, contract_address),
+        (CallContextFieldTag.IsSuccess, is_success),
+        (CallContextFieldTag.IsStatic, FQ(False)),
+        (CallContextFieldTag.IsRoot, FQ(False)),
+        (CallContextFieldTag.IsCreate, FQ(True)),
+    ]:
+        instruction.constrain_equal(
+            instruction.call_context_lookup(field_tag, call_id=callee_call_id),
+            expected_value,
+        )
+    instruction.constrain_equal_word(
+        instruction.call_context_lookup_word(CallContextFieldTag.CodeHash, call_id=callee_call_id),
+        code_hash,
+    )
+
+    instruction.step_state_transition_to_new_context(
+        rw_counter=Transition.delta(instruction.rw_counter_offset),
+        call_id=Transition.to(callee_call_id),
+        is_root=Transition.to(False),
+        is_create=Transition.to(True),
+        code_hash=Transition.to_word(instruction.next.code_hash),
+        gas_left=Transition.to(callee_gas_left),
+        # `transfer` includes two balance updates
+        reversible_write_counter=Transition.to(2),
+        log_id=Transition.same(),
+    )