feat: update account non-existence handling

specs/evm-proof.md

@@ -42,3 +42,48 @@ We call the list of random read-write access records `BusMapping` because it act
 The repeated chip has 2 main states, one is call initialization, another is bytecode execution.
 
 **TODO**
+
+## Account non-existence
+
+The following opcodes contain special cases for non-existing accounts:
+- BALANCE
+- EXTCODEHASH
+- EXTCODECOPY
+- EXTCODESIZE
+- CALL
+- CALLCODE
+- DELEGATECALL
+- STATICCALL
+
+The rest of the opcodes only deal with accounts that are known to exist (by previous conditions).
+
+We encode the state of existence of an account with its value of the
+`code_hash` in the `rw_table` (managed by the State Circuit): `code_hash = 0`
+means that the account doesn't exist, and `code_hash != 0` means that the
+account exists.  We can guarantee this fact with the following properties:
+- Every time an account is created, the `code_hash` is set from zero to a
+  non-zero value.
+    - By the read consistency guaranteed by the State Circuit, we know that if a
+      `code_hash` is non-zero, the account must exist (because it has been created
+      previously)
+- A `code_hash` read with value 0 is translated to a non-existence account
+  proof in the MPT (via the state circuit).
+    - From this we know that if a `code_hash` is read as zero, the account
+      doesn't exist.
+- There are no other valid transitions of `code_hash`.  In summary, the valid
+  transitions are: `0->0`, and `0->H` (where H != 0).  Note that we're not
+  considering account destruction for now.
+
+Since only `code_hash` encodes account existence, we must be careful to never
+read (lookup) another account property unless we have checked that the account
+exists.  This is because the RwTable in the State Circuit has all the entries
+sorted by [Tag, FieldTag], so `CodeHash`, `Nonce` and `Balance` are treated
+independently, which means that a lookup to `Nonce` or `Balance` could suceed
+on a non-existing account if the account is created afterwards.  For this
+reason we must guarantee that:
+- A `Nonce` and `Balance` lookup to an account must only be performed if we
+  have previously verified that the account exists by reading its `CodeHash`
+  and checking it to be non-zero.  This check can be done in the same step (for
+  opcodes that can deal with non-existing accounts), or in a previous step (as
+  a precondition, for opcodes that work with the caller account).
+

specs/opcode/31BALANCE.md

@@ -23,20 +23,20 @@ stack instead.
 
 1. opId = 0x31
 2. State transition:
-   - gc + 7 (1 stack read, 1 stack write, 3 call context reads, 1 account reads,
+   - gc + 7 (1 stack read, 1 stack write, 3 call context reads, 1/2 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
+3. Lookups: 7/8 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.
+   - 1 account `code_hash` lookup to determine account existence.
+   - If account exists, lookup account `balance`.
    - The BALANCE result is at the new top of the stack.
 4. Additional Constraints
    - value `is_warm` matches the gas cost for this opcode.

specs/opcode/3bEXTCODESIZE.md

@@ -8,8 +8,8 @@ The `EXTCODESIZE` opcode gets code size of the given account.
 
 The `EXTCODESIZE` opcode pops `address` (20 bytes of data) off the stack and
 pushes the code size 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.
+account doesn't exist (by checking that `code_hash == 0`), then it will push 0
+onto the stack instead.
 
 ## Circuit behaviour
 
@@ -35,8 +35,8 @@ the stack instead.
    - 3 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 `code_hash`, then get
-     `code_size`. Otherwise only lookup the account non-existing proof.
+   - Lookup account `code_hash`, then get `code_size` if `code_hash != 0`, 
+     otherwise skip the `code_size` lookup.
    - The EXTCODESIZE result is at the new top of the stack.
 4. Additional Constraints
    - value `is_warm` matches the gas cost for this opcode.

specs/opcode/3cEXTCODECOPY.md

@@ -25,8 +25,8 @@ The `EXTCODECOPY` circuit constrains the values popped from stack, call context/
    - `memory_offset` is at the second position of the stack
    - `code_offset` is at the third position of the stack
    - `size` is at the fourth position of the stack
-   - `code_hash` from the address if witness value `exists == 1`. Otherwise only lookup the account non-existing proof.
-   - `code_size` from the bytecode table
+   - `code_hash` from the address (will be 0 when the account doesn't exist).
+   - `code_size` from the bytecode table if account exists (`code_hash != 0`)
    - `tx_id`, `rw_counter_end_of_reversion`, `is_persistent` from call context
    - `address` is added to the transaction access list if not already present
 

specs/opcode/3fEXTCODEHASH.md

@@ -4,8 +4,9 @@
 
 The `EXTCODEHASH` opcode pops `address` off the stack and pushes the code hash
 of the corresponding account onto the stack. If the corresponding account
-doesn't exist (by checking non existing flag), then it will push 0 onto the
-stack instead.
+doesn't exist then it will push 0 onto the stack instead.  Since we use
+`code_hash = 0` to encode non-existing accounts, we can use the lookup result
+directly.
 
 ## Constraints
 
@@ -23,8 +24,7 @@ stack instead.
    - 3 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 `code_hash`. Otherwise
-     lookup account non-existing proof.
+   - lookup account `code_hash`.
    - The EXTCODEHASH result is at the new top of the stack.
 4. Additional Constraints
    - value `is_warm` matches the gas cost for this opcode.

specs/tables.md

@@ -79,7 +79,6 @@ NOTE: `kN` means `keyN`
 | $counter | $isWrite    | Account                    |             | $address           | Nonce                      |                     | $value    | $committedValue  | $root |
 | $counter | $isWrite    | Account                    |             | $address           | Balance                    |                     | $value    | $committedValue  | $root |
 | $counter | $isWrite    | Account                    |             | $address           | CodeHash                   |                     | $value    | $committedValue  | $root |
-| $counter | $isWrite    | Account                    |             | $address           | NonExisting                |                     | 0         | 0                | $root |
 | $counter | true        | AccountDestructed          |             | $address           |                            |                     | $value    | 0                | $root |
 |          |             |                            |             |                    |                            |                     |           |                  |                 |
 |          |             | *CallContext constant*     |             |                    | *CallContextFieldTag* (ro) |                     |           |                  |                 |

src/zkevm_specs/evm/execution/balance.py

@@ -13,11 +13,10 @@ def balance(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.
-    exists = instruction.curr.aux_data
-
-    if exists == 0:
-        instruction.account_read(address, AccountFieldTag.NonExisting)
+    # Check account existence with code_hash != 0
+    exists = FQ(1) - instruction.is_zero(
+        instruction.account_read(address, AccountFieldTag.CodeHash)
+    )
 
     balance = instruction.account_read(address, AccountFieldTag.Balance) if exists == 1 else RLC(0)
 
@@ -28,7 +27,7 @@ def balance(instruction: Instruction):
 
     instruction.step_state_transition_in_same_context(
         opcode,
-        rw_counter=Transition.delta(7),
+        rw_counter=Transition.delta(7 + exists.n),
         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/callop.py

@@ -128,17 +128,15 @@ def callop(instruction: Instruction):
         )
         instruction.constrain_zero(1 - value_lt_caller_balance - value_eq_caller_balance)
 
-    # Load callee account `exists` value from auxilary witness data.
-    callee_exists = instruction.curr.aux_data
+    callee_code_hash = instruction.account_read(code_address, AccountFieldTag.CodeHash)
+    # Check calle account existence with code_hash != 0
+    callee_exists = FQ(1) - instruction.is_zero(callee_code_hash)
 
     if callee_exists == 1:
-        # Get callee code hash.
-        callee_code_hash = instruction.account_read(code_address, AccountFieldTag.CodeHash)
         is_empty_code_hash = instruction.is_equal(
             callee_code_hash, instruction.rlc_encode(EMPTY_CODE_HASH, 32)
         )
     else:  # callee_exists == 0
-        instruction.account_read(code_address, AccountFieldTag.NonExisting)
         is_empty_code_hash = FQ(1)
 
     # Verify gas cost.

src/zkevm_specs/evm/execution/extcodecopy.py

@@ -19,14 +19,12 @@ def extcodecopy(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.
-    exists = instruction.curr.aux_data
+    code_hash = instruction.account_read(address, AccountFieldTag.CodeHash)
+    # Check account existence with code_hash != 0
+    exists = FQ(1) - instruction.is_zero(code_hash)
     if exists == 1:
-        code_hash = instruction.account_read(address, AccountFieldTag.CodeHash)
         code_size = instruction.bytecode_length(code_hash.expr())
     else:
-        instruction.account_read(address, AccountFieldTag.NonExisting)
-        code_hash = RLC(0)
         code_size = RLC(0)
 
     next_memory_size, memory_expansion_gas_cost = instruction.memory_expansion_dynamic_length(

src/zkevm_specs/evm/execution/extcodehash.py

@@ -1,4 +1,4 @@
-from ...util import EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS, FQ, N_BYTES_ACCOUNT_ADDRESS, RLC
+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
@@ -13,18 +13,11 @@ 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.
-    exists = instruction.curr.aux_data
-
-    if exists == 0:
-        instruction.account_read(address, AccountFieldTag.NonExisting)
-
-    code_hash = (
-        instruction.account_read(address, AccountFieldTag.CodeHash) if exists == 1 else RLC(0)
-    )
+    # We already define code_hash to be 0 when the account doesn't exist.
+    code_hash = instruction.account_read(address, AccountFieldTag.CodeHash)
 
     instruction.constrain_equal(
-        instruction.select(exists, code_hash.expr(), FQ(0)),
+        code_hash.expr(),
         instruction.stack_push(),
     )
 

src/zkevm_specs/evm/execution/extcodesize.py

@@ -19,14 +19,13 @@ def extcodesize(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.
-    exists = instruction.curr.aux_data
+    code_hash = instruction.account_read(address, AccountFieldTag.CodeHash)
+    # Check account existence with code_hash != 0
+    exists = FQ(1) - instruction.is_zero(code_hash)
 
     if exists == 1:
-        code_hash = instruction.account_read(address, AccountFieldTag.CodeHash)
         code_size = instruction.bytecode_length(code_hash)
     else:  # exists == 0
-        instruction.account_read(address, AccountFieldTag.NonExisting)
         code_size = RLC(0)
 
     instruction.constrain_equal(

src/zkevm_specs/evm/main.py

@@ -22,7 +22,7 @@ def verify_steps(
     if end_with_last_step:
         steps.append(DUMMY_STEP_STATE)
 
-    ok = True
+    exception = None
     for idx, (curr, next) in enumerate(zip(steps, steps[1:])):
         try:
             verify_step(
@@ -36,8 +36,13 @@ def verify_steps(
                 )
             )
         except AssertionError as e:
-            ok = False
-    assert ok == success
+            exception = e
+    if success:
+        if exception:
+            raise exception
+        assert exception is None
+    else:
+        assert exception is not None
 
 
 def verify_step(instruction: Instruction):

src/zkevm_specs/state.py

@@ -257,6 +257,8 @@ def check_storage(row: Row, row_prev: Row, row_next: Row, tables: Tables):
     # 4.0. Unused keys are 0
     assert row.field_tag() == 0
 
+    # value = 0 means the leaf doesn't exist. 0->0 transition requires a
+    # non-existing proof.
     is_non_exist = FQ(row.value.expr() == FQ(0)) * FQ(row.committed_value.expr() == FQ(0))
 
     # 4.1. MPT lookup for last access to (address, storage_key)
@@ -304,11 +306,20 @@ def check_account(row: Row, row_prev: Row, row_next: Row, tables: Tables):
     assert row.id() == 0
     assert row.storage_key() == 0
 
+    # We use code_hash = 0 as non-existing account state.  code_hash: 0->0
+    # transition requires a non-existing proof.
+    is_non_exist = (
+        FQ(row.value.expr() == FQ(0))
+        * FQ(row.committed_value.expr() == FQ(0))
+        * FQ(field_tag == FQ(AccountFieldTag.CodeHash))
+    )
+
     # 6.2. MPT storage lookup for last access to (address, field_tag)
     if not all_keys_eq(row, row_next):
         tables.mpt_lookup(
             get_addr(row),
-            FQ(proof_type),
+            is_non_exist * FQ(MPTProofType.NonExistingAccountProof)
+            + (1 - is_non_exist) * FQ(proof_type),
             row.storage_key(),
             row.value,
             row.committed_value,

tests/evm/test_balance.py

@@ -14,43 +14,44 @@
 from zkevm_specs.util import (
     EXTRA_GAS_COST_ACCOUNT_COLD_ACCESS,
     GAS_COST_WARM_ACCESS,
+    FQ,
+    EMPTY_CODE_HASH,
     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),
+    (0x30000, 0, False, True, True),
+    (0x30000, 0, False, False, True),
+    (0x30000, 200, True, True, True),
+    (0x30000, 200, True, False, True),
     (
         rand_address(),
         rand_word(),
-        rand_range(2),
+        rand_range(2) == 0,
         rand_range(2) == 0,
         True,  # persistent call
     ),
     (
         rand_address(),
         rand_word(),
-        rand_range(2),
+        rand_range(2) == 0,
         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):
+def test_balance(address: U160, balance: U256, exists: bool, is_warm: bool, is_persistent: bool):
     randomness = rand_fq()
 
-    result = balance if exists == 1 else 0
+    result = balance if exists else 0
 
     tx_id = 1
     call_id = 1
@@ -75,12 +76,11 @@ def test_balance(address: U160, balance: U256, exists: int, is_warm: bool, is_pe
             rw_counter_of_reversion=rw_counter_end_of_reversion - reversible_write_counter,
         )
     )
-    if exists == 1:
+    rw_dictionary.account_read(
+        address, AccountFieldTag.CodeHash, RLC(EMPTY_CODE_HASH if exists else 0, randomness)
+    )
+    if exists:
         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)
 
@@ -107,11 +107,10 @@ def test_balance(address: U160, balance: U256, exists: int, is_warm: bool, is_pe
                 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,
+                rw_counter=8 + (1 if exists else 0),
                 call_id=1,
                 is_root=True,
                 is_create=False,