Spec for opcode BALANCE

specs/opcode/31BALANCE.md

@@ -0,0 +1,51 @@
+# BALANCE opcode
+
+## Procedure
+
+The `BALANCE` opcode gets balance of the given account.
+
+## EVM behaviour
+
+The `BALANCE` opcode pops `address` (20 bytes of data) off the stack and pushes
+the balance of the corresponding account onto the stack. If the given account
+doesn't exist (by checking non existing flag), then it will push 0 onto the
+stack instead.
+
+## Circuit behaviour
+
+1. Construct call context table in rw table.
+2. Do bus-mapping lookup for stack read, call context read and account read
+   operations.
+3. Do bus-mapping lookup for transaction access list write and stack write
+   operations.
+
+## Constraints
+
+1. opId = 0x31
+2. State transition:
+   - gc + 7 (1 stack read, 1 stack write, 3 call context reads, 1 account reads,
+     1 transaction access list write)
+   - stack_pointer + 0 (one pop and one push)
+   - pc + 1
+   - gas:
+     - the accessed `address` is warm: GAS_COST_WARM_ACCESS
+     - the accessed `address` is cold: GAS_COST_ACCOUNT_COLD_ACCESS
+3. Lookups: 7 busmapping lookups
+   - `address` is at top of the stack.
+   - 3 reads from call context for `tx_id`, `rw_counter_end_of_reversion`, and
+     `is_persistent`.
+   - `address` is added to the transaction access list if not already present.
+   - If witness value `exists == 1`, lookup account `balance`. Otherwise lookup
+     account non-existing proof.
+   - The BALANCE result is at the new top of the stack.
+4. Additional Constraints
+   - value `is_warm` matches the gas cost for this opcode.
+
+## 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/balance.py`.

src/zkevm_specs/evm/execution/__init__.py

@@ -11,6 +11,7 @@
 from .addmod import *
 from .address import *
 from .mulmod import *
+from .balance import *
 from .block_ctx import *
 from .blockhash import *
 from .call_staticcall import *
@@ -57,6 +58,7 @@
     ExecutionState.MUL: mul_div_mod,
     ExecutionState.NOT: not_opcode,
     ExecutionState.ORIGIN: origin,
+    ExecutionState.BALANCE: balance,
     ExecutionState.CALLER: caller,
     ExecutionState.CALLVALUE: callvalue,
     ExecutionState.CALLDATACOPY: calldatacopy,

src/zkevm_specs/evm/execution/balance.py

@@ -0,0 +1,34 @@
+from ...util import EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS, FQ, N_BYTES_ACCOUNT_ADDRESS, RLC
+from ..instruction import Instruction, Transition
+from ..opcode import Opcode
+from ..table import AccountFieldTag, CallContextFieldTag
+
+
+def balance(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+    instruction.constrain_equal(opcode, Opcode.BALANCE)
+
+    address = instruction.rlc_to_fq(instruction.stack_pop(), N_BYTES_ACCOUNT_ADDRESS)
+
+    tx_id = instruction.call_context_lookup(CallContextFieldTag.TxId)
+    is_warm = instruction.add_account_to_access_list(tx_id, address, instruction.reversion_info())
+
+    # Load account `exists` value from auxilary witness data.
+    exists = instruction.curr.aux_data
+
+    if exists == 0:  # 1 - exists == 1
+        instruction.account_read(address, AccountFieldTag.NonExisting)
+
+    balance = instruction.account_read(address, AccountFieldTag.Balance) if exists == 1 else RLC(0)
+    instruction.constrain_equal(
+        instruction.select(exists, balance.expr(), FQ(0)),
+        instruction.stack_push(),
+    )
+
+    instruction.step_state_transition_in_same_context(
+        opcode,
+        rw_counter=Transition.delta(7),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.same(),
+        dynamic_gas_cost=instruction.select(is_warm, FQ(0), FQ(EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS)),
+    )

tests/evm/test_balance.py

@@ -0,0 +1,124 @@
+import pytest
+
+from zkevm_specs.evm import (
+    AccountFieldTag,
+    Block,
+    Bytecode,
+    CallContextFieldTag,
+    ExecutionState,
+    RWDictionary,
+    StepState,
+    Tables,
+    verify_steps,
+)
+from zkevm_specs.util import (
+    EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS,
+    GAS_COST_WARM_ACCESS,
+    RLC,
+    U160,
+    U256,
+    rand_address,
+    rand_bytes,
+    rand_fq,
+    rand_range,
+    rand_word,
+)
+
+TESTING_DATA = [
+    (0x30000, 0, 0, True, True),
+    (0x30000, 0, 0, False, True),
+    (0x30000, 200, 1, True, True),
+    (0x30000, 200, 1, False, True),
+    (
+        rand_address(),
+        rand_word(),
+        rand_range(2),
+        rand_range(2) == 0,
+        True,  # persistent call
+    ),
+    (
+        rand_address(),
+        rand_word(),
+        rand_range(2),
+        rand_range(2) == 0,
+        False,  # reverted call
+    ),
+]
+
+
+@pytest.mark.parametrize("address, balance, exists, is_warm, is_persistent", TESTING_DATA)
+def test_balance(address: U160, balance: U256, exists: int, is_warm: bool, is_persistent: bool):
+    randomness = rand_fq()
+
+    result = balance if exists == 1 else 0
+
+    tx_id = 1
+    call_id = 1
+
+    # 9 + 1 reversible operation (the account access list write)
+    rw_counter_end_of_reversion = 0 if is_persistent else 10
+    reversible_write_counter = 0
+
+    rw_dictionary = (
+        RWDictionary(1)
+        .stack_read(call_id, 1023, RLC(address, randomness))
+        .call_context_read(tx_id, CallContextFieldTag.TxId, tx_id)
+        .call_context_read(
+            tx_id, CallContextFieldTag.RwCounterEndOfReversion, rw_counter_end_of_reversion
+        )
+        .call_context_read(tx_id, CallContextFieldTag.IsPersistent, is_persistent)
+        .tx_access_list_account_write(
+            tx_id,
+            address,
+            True,
+            is_warm,
+            rw_counter_of_reversion=rw_counter_end_of_reversion - reversible_write_counter,
+        )
+    )
+    if exists == 1:
+        rw_dictionary.account_read(address, AccountFieldTag.Balance, RLC(balance, randomness))
+    else:
+        rw_dictionary.account_read(
+            address, AccountFieldTag.NonExisting, RLC(1 - exists, randomness)
+        )
+
+    rw_table = set(rw_dictionary.stack_write(call_id, 1023, RLC(result, randomness)).rws)
+
+    bytecode = Bytecode().balance()
+    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.BALANCE,
+                rw_counter=1,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_hash=bytecode_hash,
+                program_counter=0,
+                stack_pointer=1023,
+                gas_left=GAS_COST_WARM_ACCESS + (not is_warm) * EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS,
+                aux_data=exists,
+            ),
+            StepState(
+                execution_state=ExecutionState.STOP if is_persistent else ExecutionState.REVERT,
+                rw_counter=8,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_hash=bytecode_hash,
+                program_counter=1,
+                stack_pointer=1023,
+                gas_left=0,
+            ),
+        ],
+    )