Spec for opcode BALANCE

specs/opcode/30ADDRESS.md

@@ -0,0 +1,37 @@
+# ADDRESS opcode
+
+## Procedure
+
+The `ADDRESS` opcode gets the address of currently executing account.
+
+## EVM behaviour
+
+The `ADDRESS` opcode loads the callee address (20 bytes of data) from call
+context, then pushes this address to the stack.
+
+## Circuit behaviour
+
+1. Construct call context table in rw table
+2. Do busmapping lookup for call context callee read operation
+3. Do busmapping lookup for stack write operation
+
+## Constraints
+
+1. opId = 0x30
+2. State transition:
+   - gc + 2 (1 stack write, 1 call context read)
+   - stack_pointer - 1
+   - pc + 1
+   - gas - 2
+3. Lookups: 2
+   - `address` is in the rw table {call context, call ID, callee}
+   - `address` is on top of stack
+
+## Exceptions
+
+1. stack overflow: stack is full, stack pointer = 0
+2. out of gas: remaining gas is not enough
+
+## Code
+
+Please refer to `src/zkevm_specs/evm/execution/address.py`.

specs/opcode/31BALANCE.md

@@ -0,0 +1,49 @@
+# 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, 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
+   - `address` is popped from 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.
+   - `balance` is read from the given account. Set to 0 if it doesn't exist.
+   - the `balance` result is pushed onto 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/copy_circuit.py

@@ -50,12 +50,13 @@ def verify_row(cs: ConstraintSystem, rows: Sequence[CopyCircuitRow]):
         cs.constrain_equal(rows[0].rwc_inc_left - rw_diff, rows[1].rwc_inc_left)
         # rlc_acc is the same over all rows
         cs.constrain_equal(rows[0].rlc_acc, rows[1].rlc_acc)
+    # rwc_inc_left == rw_diff for last row in the copy slot
     with cs.condition(rows[0].is_last) as cs:
-        # rwc_inc_left == rw_diff for last row in the copy slot
         cs.constrain_equal(rows[0].rwc_inc_left, rw_diff)
-        # for RlcAcc type, value == rlc_acc at the last row
-        with cs.condition(rows[0].is_rlc_acc) as cs:
-            cs.constrain_equal(rows[0].rlc_acc, rows[0].value)
+
+    # for RlcAcc type, value == rlc_acc at the last row
+    with cs.condition(rows[0].is_last * rows[0].is_rlc_acc) as cs:
+        cs.constrain_equal(rows[0].rlc_acc, rows[0].value)
 
 
 def verify_step(cs: ConstraintSystem, rows: Sequence[CopyCircuitRow], r: FQ):
@@ -64,28 +65,28 @@ def verify_step(cs: ConstraintSystem, rows: Sequence[CopyCircuitRow], r: FQ):
         cs.constrain_zero(rows[1].is_last * (1 - rows[0].bytes_left))
         # bytes_left == bytes_left_next + 1 for non-last step
         cs.constrain_zero((1 - rows[1].is_last) * (rows[0].bytes_left - rows[2].bytes_left - 1))
-
-        # write value == read value if not rlc accumulator
-        with cs.condition(1 - rows[1].is_rlc_acc):
-            cs.constrain_equal(rows[0].value, rows[1].value)
-        # read value == write value for the first step (always)
-        with cs.condition(rows[0].is_first):
-            cs.constrain_equal(rows[0].value, rows[1].value)
-
         # value == 0 when is_pad == 1 for read
         cs.constrain_zero(rows[0].is_pad * rows[0].value)
         # is_pad == 1 - (src_addr < src_addr_end) for read row
-        cs.constrain_equal(
-            1 - lt(rows[0].addr, rows[0].src_addr_end, N_BYTES_MEMORY_ADDRESS), rows[0].is_pad
-        )
+        # We skip tx_log because:
+        # 1. It can only ever be a write row, so q_step == 0 and the constraint will be satisfied.
+        # 2. Since `lt(..)` will still be computed, it's excepted to throw an exception since
+        #    dst addr is a very large number: addr += (int(TxLogFieldTag.Data) << 32) + (log_id << 48)
+        if rows[0].is_tx_log == FQ.zero():
+            cs.constrain_equal(
+                1 - lt(rows[0].addr, rows[0].src_addr_end, N_BYTES_MEMORY_ADDRESS), rows[0].is_pad
+            )
         # is_pad == 0 for write row
         cs.constrain_zero(rows[1].is_pad)
-
-    with cs.condition(1 - rows[0].q_step):
-        with cs.condition(1 - rows[0].is_last):
-            # next_write_value == (write_value * r) + next_read_value if rlc accumulator
-            with cs.condition(rows[0].is_rlc_acc):
-                cs.constrain_equal(rows[2].value, rows[0].value * r + rows[1].value)
+    # write value == read value if not rlc accumulator
+    with cs.condition(rows[0].q_step * (1 - rows[1].is_rlc_acc)):
+        cs.constrain_equal(rows[0].value, rows[1].value)
+    # read value == write value for the first step (always)
+    with cs.condition(rows[0].q_step * rows[0].is_first):
+        cs.constrain_equal(rows[0].value, rows[1].value)
+    # next_write_value == (write_value * r) + next_read_value if rlc accumulator
+    with cs.condition((1 - rows[0].q_step) * (1 - rows[0].is_last) * rows[0].is_rlc_acc):
+        cs.constrain_equal(rows[2].value, rows[0].value * r + rows[1].value)
 
 
 def verify_copy_table(copy_circuit: CopyCircuit, tables: Tables, r: FQ):

src/zkevm_specs/evm/execution/__init__.py

@@ -9,7 +9,9 @@
 # Opcode's successful cases
 from .add_sub import *
 from .addmod import *
+from .address import *
 from .mulmod import *
+from .balance import *
 from .block_ctx import *
 from .call import *
 from .calldatasize import *
@@ -47,10 +49,12 @@
     ExecutionState.EndBlock: end_block,
     ExecutionState.ADD: add_sub,
     ExecutionState.ADDMOD: addmod,
+    ExecutionState.ADDRESS: address,
     ExecutionState.MULMOD: mulmod,
     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/address.py

@@ -0,0 +1,24 @@
+from ...util import N_BYTES_ACCOUNT_ADDRESS
+from ..instruction import Instruction, Transition
+from ..table import CallContextFieldTag
+from ..opcode import Opcode
+
+
+def address(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+    instruction.constrain_equal(opcode, Opcode.ADDRESS)
+
+    # Get callee address from call context and compare with stack top after push.
+    instruction.constrain_equal(
+        instruction.call_context_lookup(CallContextFieldTag.CalleeAddress),
+        # NOTE: We can replace this with N_BYTES_WORD if we reuse the 32 byte RLC constraint in
+        # all places. See: https://github.com/privacy-scaling-explorations/zkevm-specs/issues/101
+        instruction.rlc_to_fq(instruction.stack_push(), N_BYTES_ACCOUNT_ADDRESS),
+    )
+
+    instruction.step_state_transition_in_same_context(
+        opcode,
+        rw_counter=Transition.delta(2),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(-1),
+    )

src/zkevm_specs/evm/execution/balance.py

@@ -0,0 +1,25 @@
+from ...util import EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS, FQ, N_BYTES_ACCOUNT_ADDRESS
+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())
+
+    balance = instruction.account_read(address, AccountFieldTag.Balance)
+    instruction.constrain_equal(instruction.stack_push(), balance)
+
+    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)),
+    )

src/zkevm_specs/evm/execution/sha3.py

@@ -16,19 +16,22 @@ def sha3(instruction: Instruction):
     # convert RLC encoded stack elements to FQ.
     memory_offset, length = instruction.memory_offset_and_length(offset, size)
 
-    copy_rwc_inc, rlc_acc = instruction.copy_lookup(
-        instruction.curr.call_id,
-        CopyDataTypeTag.Memory,
-        instruction.curr.call_id,
-        CopyDataTypeTag.RlcAcc,
-        memory_offset,
-        memory_offset + length,
-        FQ.zero(),
-        length,
-        instruction.curr.rw_counter + instruction.rw_counter_offset,
-    )
-    keccak256_rlc_acc = instruction.keccak_lookup(length, rlc_acc)
+    if instruction.is_zero(length) == FQ.zero():
+        copy_rwc_inc, rlc_acc = instruction.copy_lookup(
+            instruction.curr.call_id,
+            CopyDataTypeTag.Memory,
+            instruction.curr.call_id,
+            CopyDataTypeTag.RlcAcc,
+            memory_offset,
+            memory_offset + length,
+            FQ.zero(),
+            length,
+            instruction.curr.rw_counter + instruction.rw_counter_offset,
+        )
+    else:
+        copy_rwc_inc, rlc_acc = FQ.zero(), FQ.zero()
 
+    keccak256_rlc_acc = instruction.keccak_lookup(length, rlc_acc)
     instruction.constrain_equal(
         keccak256_rlc_acc,
         sha3_value.expr(),

src/zkevm_specs/evm/typing.py

@@ -690,9 +690,11 @@ class CopyCircuit:
     rows: List[CopyCircuitRow]
     pad_rows: List[CopyCircuitRow]
 
-    def __init__(self) -> None:
+    def __init__(self, pad_rows: Optional[List[CopyCircuitRow]] = None) -> None:
         self.rows = []
-        self.pad_rows = [CopyCircuitRow(FQ(1), *[FQ(0)] * 18), CopyCircuitRow(*[FQ(0)] * 19)]
+        self.pad_rows = []
+        if pad_rows is not None:
+            self.pad_rows = pad_rows
 
     def table(self) -> Sequence[CopyCircuitRow]:
         return self.rows + self.pad_rows
@@ -805,7 +807,7 @@ def _append_row(
         if is_memory:
             if is_write:
                 rw_dict.memory_write(id, addr, value)
-            else:
+            elif is_pad is False:
                 rw_dict.memory_read(id, addr, value)
         elif is_tx_log:
             assert is_write

src/zkevm_specs/util/constraint_system.py

@@ -17,7 +17,9 @@ def __init__(self, cond: Optional[Expression] = None):
     def __enter__(self):
         return self
 
-    def __exit__(self, type, value, traceback):
+    def __exit__(self, e_type, e_value, traceback):
+        if e_type is not None:
+            raise e_value
         self.cond = None
         return self
 

tests/evm/test_address.py

@@ -0,0 +1,70 @@
+import pytest
+
+from zkevm_specs.evm import (
+    Bytecode,
+    CallContextFieldTag,
+    ExecutionState,
+    RWDictionary,
+    StepState,
+    Tables,
+    verify_steps,
+)
+from zkevm_specs.util import RLC, U160, rand_address, rand_fq
+
+
+TESTING_DATA = (
+    0x00,
+    0x10,
+    0x030201,
+    0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF,
+    rand_address(),
+)
+
+
+@pytest.mark.parametrize("address", TESTING_DATA)
+def test_address(address: U160):
+    randomness = rand_fq()
+
+    bytecode = Bytecode().address()
+    bytecode_hash = RLC(bytecode.hash(), randomness)
+
+    tables = Tables(
+        block_table=set(),
+        tx_table=set(),
+        bytecode_table=set(bytecode.table_assignments(randomness)),
+        rw_table=set(
+            RWDictionary(9)
+            .call_context_read(1, CallContextFieldTag.CalleeAddress, address)
+            .stack_write(1, 1023, RLC(address, randomness))
+            .rws
+        ),
+    )
+
+    verify_steps(
+        randomness=randomness,
+        tables=tables,
+        steps=[
+            StepState(
+                execution_state=ExecutionState.ADDRESS,
+                rw_counter=9,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_hash=bytecode_hash,
+                program_counter=0,
+                stack_pointer=1024,
+                gas_left=2,
+            ),
+            StepState(
+                execution_state=ExecutionState.STOP,
+                rw_counter=11,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_hash=bytecode_hash,
+                program_counter=1,
+                stack_pointer=1023,
+                gas_left=0,
+            ),
+        ],
+    )