Specs for EXTCODEHASH

specs/opcode/01ADD_03SUB.md

@@ -1,4 +1,4 @@
-# ADD and SUB op code
+# ADD and SUB opcodes
 
 ## Procedure
 

specs/opcode/02MUL.md

@@ -1,4 +1,4 @@
-# MUL op code
+# MUL opcode
 
 ## Procedure
 

specs/opcode/0bSIGNEXTEND.md

@@ -1,4 +1,4 @@
-# SIGNEXTEND op code
+# SIGNEXTEND opcode
 
 ## Procedure
 

specs/opcode/10LT_11GT.md

@@ -1,4 +1,4 @@
-# LT & GT opcode
+# LT & GT opcodes
 
 ## Procedure
 

specs/opcode/12SLT_13SGT.md

@@ -1,4 +1,4 @@
-# SLT & SGT opcode
+# SLT & SGT opcodes
 
 ## Procedure
 

specs/opcode/16AND_17OR_18XOR.md

@@ -1,4 +1,4 @@
-# AND, OR, XOR op code
+# AND, OR, XOR opcodes
 
 ## Procedure
 

specs/opcode/1aBYTE.md

@@ -1,4 +1,4 @@
-# BYTE op code
+# BYTE opcode
 
 ## Procedure
 

specs/opcode/3fEXTCODEHASH.md

@@ -0,0 +1,40 @@
+# EXTCODEHASH opcode
+
+## Procedure
+
+The `EXTCODEHASH` opcode pops `address` off the stack and pushes the code hash
+of the corresponding account onto the stack. If the corresponding account is
+empty (i.e. has nonce = 0, balance = 0 and no code), then it will push 0 onto
+the stack instead.
+
+## Constraints
+
+1. opId = 0x3f
+2. State transition:
+   - gc + 7 (1 stack read, 1 stack write, 1 call context read, 3 account reads,
+     1 transaction access list write)
+   - stack_pointer + 0 (one pop and one push)
+   - pc + 1
+   - gas:
+     - the accessed `address` is warm: WARM_STORAGE_READ_COST
+     - the accessed `address` is cold: COLD_ACCOUNT_ACCESS_COST
+3. Lookups: 7
+   - `address` is popped from the stack
+   - tx id of call context is `tx_id`
+   - `address` is added to the transaction access list if not already present
+   - nonce of account is `nonce`
+   - balance of account is `balance`
+   - code hash of account is `code_hash`
+   - if the account is (non)empty, (`code_hash`) 0 is pushed onto the stack
+4. Additional Constraints
+   - value `is_warm` matches the gas cost for this opcode
+   - `is_empty` is boolean and 1 iff the account is empty
+
+## Exceptions
+
+1. stack underflow: if the stack starts empty
+2. out of gas: remaining gas is not enough
+
+## Code
+
+Please refer to `src/zkevm_specs/evm/execution/extcodehash.py`.

specs/opcode/41COINBASE.md

@@ -1,4 +1,4 @@
-# Coinbase op code
+# COINBASE op code
 
 ## Procedure
 

specs/opcode/42TIMESTAMP.md

@@ -1,4 +1,4 @@
-# Timestamp op code
+# TIMESTAMP opcode
 
 ## Procedure
 

specs/opcode/47SELFBALANCE.md

@@ -1,4 +1,4 @@
-# Selfbalance op code
+# SELFBALANCE opcode
 
 ## Procedure
 

specs/opcode/50POP.md

@@ -1,4 +1,4 @@
-# POP op code
+# POP opcode
 
 ## Procedure
 

specs/opcode/51MLOAD_52MSTORE_53MSTORE8.md

@@ -1,4 +1,4 @@
-# MLOAD & MSTORE & MSTORE8 op code
+# MLOAD & MSTORE & MSTORE8 opcodes
 
 ## Procedure
 

specs/opcode/54SLOAD_55SSTORE.md

@@ -1,4 +1,4 @@
-# SLOAD & SSTORE op code
+# SLOAD & SSTORE opcodes
 
 ## Variables definition
 

specs/opcode/56JUMP.md

@@ -1,4 +1,4 @@
-# JUMP code
+# JUMP opcode
 
 ## Procedure
 

specs/opcode/57JUMPI.md

@@ -1,4 +1,4 @@
-# JUMPI code
+# JUMPI opcode
 
 ## Procedure
 

specs/opcode/59MSIZE.md

@@ -1,4 +1,4 @@
-# MSIZE op code
+# MSIZE opcode
 
 ## Procedure
 

specs/opcode/5BJUMPDEST.md

@@ -1,4 +1,4 @@
-# JUMPDEST op code
+# JUMPDEST opcode
 
 ## Procedure
 

specs/opcode/80DUPX.md

@@ -1,4 +1,4 @@
-# DUPX op code
+# DUPX opcode
 
 ## Procedure
 

specs/opcode/CopyToMemory.md

@@ -1,4 +1,4 @@
-# CopyToMemory
+# CopyToMemory opcode
 
 ## Circuit behaviour
 

src/zkevm_specs/evm/execution/__init__.py

@@ -27,6 +27,7 @@
 from .gasprice import *
 from .storage import *
 from .selfbalance import *
+from .extcodehash import *
 
 
 EXECUTION_STATE_IMPL: Dict[ExecutionState, Callable] = {
@@ -53,4 +54,5 @@
     ExecutionState.SSTORE: sstore,
     ExecutionState.SELFBALANCE: selfbalance,
     ExecutionState.GASPRICE: gasprice,
+    ExecutionState.EXTCODEHASH: extcodehash,
 }

src/zkevm_specs/evm/execution/extcodehash.py

@@ -0,0 +1,40 @@
+from ..instruction import Instruction, Transition
+from ..table import CallContextFieldTag, AccountFieldTag
+from ..opcode import Opcode
+from ...util.param import EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS, GAS_COST_WARM_ACCESS
+from ...util.hash import EMPTY_CODE_HASH
+from ...util import FQ
+
+
+def extcodehash(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+
+    address = instruction.rlc_to_fq_exact(instruction.stack_pop(), 20)
+
+    tx_id = instruction.call_context_lookup(CallContextFieldTag.TxId)
+    is_warm = instruction.add_account_to_access_list(tx_id, address)
+
+    nonce = instruction.account_read(address, AccountFieldTag.Nonce)
+    balance = instruction.account_read(address, AccountFieldTag.Balance)
+    code_hash = instruction.account_read(address, AccountFieldTag.CodeHash)
+
+    is_empty = (
+        instruction.is_zero(nonce)
+        * instruction.is_zero(balance)
+        * instruction.is_equal(
+            code_hash, instruction.rlc_encode(EMPTY_CODE_HASH.to_bytes(64, "little"))
+        )
+    )
+
+    instruction.constrain_equal(
+        instruction.select(is_empty, FQ(0), code_hash.value),
+        instruction.stack_push(),
+    )
+
+    instruction.step_state_transition_in_same_context(
+        opcode,
+        rw_counter=Transition.delta(7),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(0),
+        dynamic_gas_cost=instruction.select(is_warm, FQ(0), FQ(EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS)),
+    )

src/zkevm_specs/evm/instruction.py

@@ -301,7 +301,7 @@ def add_words(self, addends: Sequence[RLC]) -> Tuple[RLC, FQ]:
 
         sum_bytes = sum_lo.to_bytes(16, "little") + sum_hi.to_bytes(16, "little")
 
-        return RLC(sum_bytes, self.randomness), FQ(carry_hi)
+        return self.rlc_encode(sum_bytes), FQ(carry_hi)
 
     def sub_word(self, minuend: RLC, subtrahend: RLC) -> Tuple[RLC, FQ]:
         minuend_lo, minuend_hi = self.word_to_lo_hi(minuend)
@@ -314,7 +314,7 @@ def sub_word(self, minuend: RLC, subtrahend: RLC) -> Tuple[RLC, FQ]:
 
         diff_bytes = diff_lo.n.to_bytes(16, "little") + diff_hi.n.to_bytes(16, "little")
 
-        return RLC(diff_bytes, self.randomness), FQ(borrow_hi)
+        return self.rlc_encode(diff_bytes), FQ(borrow_hi)
 
     def mul_word_by_u64(self, multiplicand: RLC, multiplier: Expression) -> Tuple[RLC, FQ]:
         multiplicand_lo, multiplicand_hi = self.word_to_lo_hi(multiplicand)
@@ -326,7 +326,7 @@ def mul_word_by_u64(self, multiplicand: RLC, multiplier: Expression) -> Tuple[RL
 
         product_bytes = product_lo.to_bytes(16, "little") + product_hi.to_bytes(16, "little")
 
-        return RLC(product_bytes, self.randomness), FQ(quotient_hi)
+        return self.rlc_encode(product_bytes), FQ(quotient_hi)
 
     def rlc_to_fq_unchecked(self, word: RLC, n_bytes: int) -> Tuple[FQ, FQ]:
         return self.bytes_to_fq(word.le_bytes[:n_bytes]), self.is_zero(
@@ -347,6 +347,9 @@ def bytes_to_fq(self, value: bytes) -> FQ:
         assert len(value) <= MAX_N_BYTES, "Too many bytes to composite an integer in field"
         return FQ(int.from_bytes(value, "little"))
 
+    def rlc_encode(self, value: bytes) -> RLC:
+        return RLC(value, self.randomness)
+
     def range_lookup(self, value: Expression, range: int):
         self.fixed_lookup(FixedTableTag.range_table_tag(range), value)
 

tests/evm/test_extcodehash.py

@@ -0,0 +1,99 @@
+import pytest
+
+from zkevm_specs.evm import (
+    ExecutionState,
+    StepState,
+    verify_steps,
+    Tables,
+    RWTableTag,
+    RW,
+    Block,
+    Bytecode,
+    CallContextFieldTag,
+    AccountFieldTag,
+    RWDictionary,
+)
+from zkevm_specs.util import (
+    rand_address,
+    rand_range,
+    rand_word,
+    rand_fq,
+    U256,
+    U160,
+    keccak256,
+    RLC,
+    rand_bytes,
+)
+from zkevm_specs.util.param import EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS, GAS_COST_WARM_ACCESS
+from zkevm_specs.util.hash import EMPTY_CODE_HASH
+
+
+TESTING_DATA = [
+    (0x30000, 0, 0, bytes(), True),  # warm empty account
+    (0x30000, 0, 0, bytes(), False),  # cold empty account
+    (0x30000, 1, 200, bytes([10, 40]), True),  # warm non-empty account
+    (0x30000, 1, 200, bytes([10, 10]), False),  # cold non-empty account
+    (0x30000, 1, 0, bytes(), False),  # non-empty account because of nonce
+    (rand_address(), rand_word(), rand_word(), rand_bytes(100), rand_range(2) == 0),
+]
+
+
+@pytest.mark.parametrize("address, nonce, balance, code, is_warm", TESTING_DATA)
+def test_extcodehash(address: U160, nonce: U256, balance: U256, code: bytes, is_warm: bool):
+    randomness = rand_fq()
+
+    code_hash = int.from_bytes(keccak256(code), "big")
+    result = 0 if (nonce == 0 and balance == 0 and code_hash == EMPTY_CODE_HASH) else code_hash
+
+    tx_id = 1
+    call_id = 1
+
+    rw_table = set(
+        RWDictionary(0)
+        .stack_read(call_id, 1023, RLC(address, randomness))
+        .call_context_read(tx_id, CallContextFieldTag.TxId, tx_id)
+        .tx_access_list_account_write(tx_id, address, True, is_warm)
+        .account_read(address, AccountFieldTag.Nonce, RLC(nonce, randomness))
+        .account_read(address, AccountFieldTag.Balance, RLC(balance, randomness))
+        .account_read(address, AccountFieldTag.CodeHash, RLC(code_hash, randomness))
+        .stack_write(call_id, 1023, RLC(result, randomness))
+        .rws
+    )
+
+    bytecode = Bytecode().extcodehash()
+    tables = Tables(
+        block_table=Block(),
+        tx_table=set(),
+        bytecode_table=set(bytecode.table_assignments(randomness)),
+        rw_table=rw_table,
+    )
+
+    bytecode_hash = RLC(bytecode.hash(), randomness)
+    verify_steps(
+        randomness=randomness,
+        tables=tables,
+        steps=[
+            StepState(
+                execution_state=ExecutionState.EXTCODEHASH,
+                rw_counter=0,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_source=bytecode_hash,
+                program_counter=0,
+                stack_pointer=1023,
+                gas_left=GAS_COST_WARM_ACCESS + (not is_warm) * EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS,
+            ),
+            StepState(
+                execution_state=ExecutionState.STOP,
+                rw_counter=7,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_source=bytecode_hash,
+                program_counter=1,
+                stack_pointer=1023,
+                gas_left=0,
+            ),
+        ],
+    )