diff --git a/specs/opcode/31BALANCE.md b/specs/opcode/31BALANCE.md new file mode 100644 index 000000000..05311532a --- /dev/null +++ b/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`. diff --git a/src/zkevm_specs/evm/execution/__init__.py b/src/zkevm_specs/evm/execution/__init__.py index 26f60ac45..c5db712b3 100644 --- a/src/zkevm_specs/evm/execution/__init__.py +++ b/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, diff --git a/src/zkevm_specs/evm/execution/balance.py b/src/zkevm_specs/evm/execution/balance.py new file mode 100644 index 000000000..6cfcb75e1 --- /dev/null +++ b/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)), + ) diff --git a/tests/evm/test_balance.py b/tests/evm/test_balance.py new file mode 100644 index 000000000..291c611e6 --- /dev/null +++ b/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, + ), + ], + )