implement insufficient balance state

specs/error_state/ErrorInsufficientBalance.md

@@ -0,0 +1,19 @@
+# ErrorInsufficientBalance state
+
+## Procedure
+### EVM behavior
+this type of error only occurs when executing op code is  `Call` `CallCode` ,`Create` or `Create2`.
+For `Call` `CallCode`, it will pop 7 stack elements , and the third is transfer `value` within the call.
+when caller's balance <  `value`, then go to `ErrorInsufficientBalance` state. for this kind of error, the failed
+call result was pushed into stack, continue to execute next step.
+
+### circuit behavior
+1.  pop 7 stack elements, even though the other six elements not closely relevant to this error
+state constraints, but in order to be accordance with evm trace, also need to handle them here for stack pointer
+transition, which impact next step's stack status.
+
+2. lookup current callee address and its balance, then ensure balance <  `value`
+
+## Code
+
+Please refer to `src/zkevm_specs/evm/execution/error_insufficient_balance.py`.

src/zkevm_specs/evm/execution/__init__.py

@@ -46,10 +46,13 @@
 from .stop import stop
 from .return_ import *
 from .extcodecopy import *
+
+# Opcode's error cases
 from .oog_constant import *
 from .oog_call import *
 from .error_stack import *
 from .error_Invalid_jump import *
+from .error_insufficient_balance import *
 
 
 EXECUTION_STATE_IMPL: Dict[ExecutionState, Callable] = {
@@ -99,4 +102,5 @@
     ExecutionState.ErrorInvalidJump: invalid_jump,
     ExecutionState.ErrorOutOfGasCALL: oog_call,
     ExecutionState.ErrorStack: stack_error,
+    ExecutionState.ErrorInsufficientBalance: insufficient_balance,
 }

src/zkevm_specs/evm/execution/error_insufficient_balance.py

@@ -0,0 +1,40 @@
+from ...util import FQ
+from ..instruction import Instruction, Transition
+from ..table import CallContextFieldTag, AccountFieldTag
+from ..opcode import Opcode
+
+
+def insufficient_balance(instruction: Instruction):
+    opcode = instruction.opcode_lookup(True)
+    # TODO: add Create / Create2 in the future
+    instruction.constrain_in(opcode, [FQ(Opcode.CALL), FQ(Opcode.CALLCODE)])
+    # TODO: for create/create2 have different stack from Call, will handle it in the future
+    # Lookup values from stack
+    instruction.stack_pop()
+    instruction.stack_pop()
+    value_rlc = instruction.stack_pop()
+    instruction.stack_pop()
+    instruction.stack_pop()
+    instruction.stack_pop()
+    instruction.stack_pop()
+    is_success_rlc = instruction.stack_push()
+    # if is_success_rlc value is zero then decode RLC should also be zero
+    instruction.constrain_zero(is_success_rlc)
+
+    value = instruction.rlc_to_fq(value_rlc, 31)
+    current_address = instruction.call_context_lookup(CallContextFieldTag.CalleeAddress)
+    caller_balance_rlc = instruction.account_read(current_address, AccountFieldTag.Balance)
+    caller_balance = instruction.rlc_to_fq(caller_balance_rlc, 31)
+    # compare value and balance
+    insufficient_balance, _ = instruction.compare(caller_balance, value, 31)
+
+    instruction.constrain_equal(insufficient_balance, FQ(1))
+
+    # Do step state transition
+    instruction.constrain_step_state_transition(
+        call_id=Transition.same(),
+        rw_counter=Transition.delta(10),
+        program_counter=Transition.delta(1),
+        stack_pointer=Transition.delta(6),
+        # TODO: handle gas_left
+    )

src/zkevm_specs/evm/execution/extcodehash.py

@@ -13,7 +13,7 @@ def extcodehash(instruction: Instruction):
     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.
+    # Load account `exists` value from auxillary witness data.
     exists = instruction.curr.aux_data
 
     if exists == 0:

src/zkevm_specs/evm/instruction.py

@@ -504,7 +504,6 @@ def add_words(self, addends: Sequence[RLC]) -> Tuple[RLC, FQ]:
 
         carry_lo, sum_lo = divmod(self.sum(addends_lo).n, 1 << 128)
         carry_hi, sum_hi = divmod((self.sum(addends_hi) + carry_lo).n, 1 << 128)
-
         sum_bytes = sum_lo.to_bytes(16, "little") + sum_hi.to_bytes(16, "little")
 
         return self.rlc_encode(sum_bytes), FQ(carry_hi)

tests/evm/test_insufficient_balance.py

@@ -0,0 +1,96 @@
+import pytest
+
+from zkevm_specs.evm import (
+    ExecutionState,
+    StepState,
+    Opcode,
+    verify_steps,
+    Tables,
+    Block,
+    Bytecode,
+    RWDictionary,
+    CallContextFieldTag,
+    AccountFieldTag,
+)
+from zkevm_specs.util import rand_fq, RLC
+from itertools import chain
+from collections import namedtuple
+
+
+TESTING_DATA = (
+    # balance | transfer value
+    (200, 250),
+    (1, 2),
+)
+
+
+@pytest.mark.parametrize("balance, transfer_value", TESTING_DATA)
+def test_insufficient_balance(balance: int, transfer_value: int):
+    randomness = rand_fq()
+
+    block = Block()
+    bytecode = Bytecode().call(0, 0xFC, transfer_value, 0, 0, 0, 0).stop()
+    bytecode_hash = RLC(bytecode.hash(), randomness)
+
+    tables = Tables(
+        block_table=set(block.table_assignments(randomness)),
+        tx_table=set(),
+        bytecode_table=set(bytecode.table_assignments(randomness)),
+        rw_table=set(
+            RWDictionary(9)
+            .stack_read(1, 1010, RLC(10000, randomness))  # gas
+            .stack_read(1, 1011, RLC(0xFC, randomness))  # address
+            .stack_read(1, 1012, RLC(transfer_value, randomness))  # value
+            .stack_read(1, 1013, RLC(0, randomness))
+            .stack_read(1, 1014, RLC(10, randomness))
+            .stack_read(1, 1015, RLC(0, randomness))
+            .stack_read(1, 1016, RLC(0, randomness))
+            .stack_write(1, 1016, RLC(0, randomness))
+            .call_context_read(1, CallContextFieldTag.CalleeAddress, 0xFE)
+            .account_read(0xFE, AccountFieldTag.Balance, RLC(balance, randomness))
+            .rws
+        ),
+    )
+
+    verify_steps(
+        randomness=randomness,
+        tables=tables,
+        steps=[
+            StepState(
+                execution_state=ExecutionState.ErrorInsufficientBalance,
+                rw_counter=9,
+                call_id=1,
+                is_root=True,
+                is_create=False,
+                code_hash=bytecode_hash,
+                program_counter=231,
+                stack_pointer=1010,
+                gas_left=8,
+            ),
+            StepState(
+                execution_state=ExecutionState.STOP,
+                program_counter=232,
+                rw_counter=19,
+                call_id=1,
+                stack_pointer=1016,
+                gas_left=0,
+            ),
+        ],
+    )
+
+
+CallContext = namedtuple(
+    "CallContext",
+    [
+        "is_root",
+        "is_create",
+        "program_counter",
+        "stack_pointer",
+        "gas_left",
+        "memory_size",
+        "reversible_write_counter",
+    ],
+    defaults=[True, False, 232, 1023, 10, 0, 0],
+)
+
+TESTING_DATA_NOT_ROOT = ((CallContext(), 100, 101),)