Questions

Q1 - Storage non-existing check

Currently in State circuit it's speced here as:

if value_prev == 0 and value == 0:
    mpt_lookup(NonExistingStorageProof, key)
else:
    mpt_lookup(StorageMod, key, value_prev, value)

Where the StorageMod supports insertion and deletion as said in this mpt-proof.md.

It seems to cover all the cases here, I'm curious why do we need to check the non-existing again in EVM circuit like that described in #259?

Q2 - NonExisting should also be reversible value

If we still need the NonExisting check in EVM circuit, it seems that we need to update its value to false when we insert any non-zero value into the key (of account or storage), and need to revert it as well, otherwise a prover could do NonExisting lookup even after it's no longer non-existing, but I didn't see that mentioned in #259.

My naive thought is that we don't need to have NonExisting as account field in State circuit, we could just check in the very similar way as we check storage like:

if value_prev == 0 and value == 0 and is_other_field_also_empty:
    mpt_lookup(NonExistingAccountProof, key)
else:
    mpt_lookup({NonceMod,BalanceMod,CodeHashMod}, key, value_prev, value)

Where is_other_field_also_empty is additionally witnessed by prover, and shouldn't be manipulated to pass the MPT circuit (if it's not empty the NonExisting should not pass, if it's empty the *Mod should not pass).

Q3 - About AccountDeleteMod

In my above approach, it's not complete since using {NonceMod,BalanceMod,CodeHashMod} to delete an account is not supported, instead we need to use another API AccountDeleteMod. And since SELFDESTRUCT (which is the only one that could delete an account) could also be reverted, we might need to track another tag for it and set it order after other account field tag and storage tag, to ensure after there is no more unexpected modification after account deletion.

However, since we haven't had plan for SELFDESTRUCT, perhaps we could lower its priority and implement that when we are really sure that we are going to support SELFDESTRUCT.

Reference

• https://github.com/privacy-scaling-explorations/zkevm-specs/blob/mpt/specs/mpt/mpt-proof.md
• https://github.com/privacy-scaling-explorations/zkevm-specs/blob/master/src/zkevm_specs/state.py
• https://github.com/privacy-scaling-explorations/zkevm-specs/issues/259

Notes by Edu

• I realize that having a NonExisting tag in the State circuit (that the EVM circuit uses in lookups) is extremely problematic, as shown in Q2.
  • Tags and FieldTags in the RWTable should refer to independent data; because they are sorted and consistency-checked isolated.
    • Account-{Nonce,Balance,CodeHash} is dependent on Account-NonExisting
    • AccountStorage-Exist is dependent on AccoutnStorage-NonExisting
• For Storage, I didn't find any problem in solution from Q1, and it resolves nicely the SLOAD and SSTORE
• For Account, I think it's a good idea to apply the solution from Q2. I have some doubts.
• For Account NonExist, the affected opcodes are:
  • BALANCE
  • EXTCODEHASH
  • EXTCODECOPY
  • EXTCODESIZE
  • CALL
  • CALLCODE
  • DELEGATECALL
  • STATICCALL

These opcodes have the following behaviours when account doesn't exist:

• BALANCE: get balance = 0
• EXTCODEHASH: get code_hash = 0
• {EXTCODECOPY, EXTCODESIZE, *CALL*}: use code_hash = EMPTY_CODE_HASH

How to prove a non-existing account in the EVM circuit?

• Previously: lookup nonce, balance, code_hash; check nonce == 0 and balance == 0 and code_hash == EMPTY_CODE_HASH
• Proposal: lookup code_hash; check code_hash == 0 (this should work because an existing account can never have code_hash == 0)

---

EVM execution trace

1. Account, CodeHash, A, 0->0
2. Account, Nonce, A, 0->1
3. Account, CodeHash, A, 0->H
4. Account, CodeHash, A, H->H

Sorted in Rw Table

​​​​                           R0

2. Account, Nonce, A, 0->1, R1
3. Account, CodeHash, A, 0->0, R1
4. Account, CodeHash, A, 0->H, R1
5. Account, CodeHash, A, H->H, R2

MPT lookups:

2. Nonce, A, 0->1, R0->R1: Create account leaf
   1-4. CodeHash, A, 0->H, R1->R2: Update account leaf

(We assume no selfdestruct)

---

1. Account, Exist, A, 0->0 // Another step: EXTCODEHASH
   2. Account, CodeHash, A, 0->0 // Another step: EXTCODEHASH
2. Account, Exist, A, 0->0
3. Account, Exist, A, 0->1
4. Account, Nonce, A, 0->1
5. Account, CodeHash, A, 0->H // Code deployment
6. Account, Exist, A, 1->1 // Another step: EXTCODEHASH
7. Account, CodeHash, A, H->H // Another step: EXTCODEHASH

Sorted in Rw Table

1. Account, Exist, A, 0->0, R1
2. Account, Exist, A, 0->1, R1
3. Account, Nonce, A, 0->1, R2
4. Account, CodeHash, A, 0->H, R3
5. Account, CodeHash, A, H->H, R3

MPT lookups:

1. Exist, A, 0->1, R0->R1: Insert account leaf
2. Nonce, A, 0->1, R1->R2: Update account leaf
   4-5. CodeHash, A, 0->H, R2->R3: Update account leaf

---

1. Account, Exist, A, 0->0

MPT lookups:

1. Exists, A, 0->0, RX->RX: NonExistingAccountProof proof
   Exists, A, 0->1, RX->RY: CodeHash proof (0->0)
   Exists, A, 1->1, RY->RY: CodeHash proof (N->N) && N != 0

Address	ProofType	Key	ValuePrev	Value	RootPrev	Root
$addr	NonceMod	0	$noncePrev	$nonceCur	$rootPrev	$root
$addr	BalanceMod	0	$balancePrev	$balanceCur	$rootPrev	$root
$addr	CodeHashMod	0	$codeHashPrev	$codeHashCur	$rootPrev	$root
$addr	NonExistingAccountProof	0	0	0	$root	$root
$addr	AccountDeleteMod	0	0	0	$rootPrev	$root
$addr	StorageMod	$key	$valuePrev	$value	$rootPrev	$root
$addr	NonExistingStorageProof	$key	0	0	$root	$root

---

1. Set CodeHash in RwTable as first Account tag
2. State circuit:

if value_prev == 0 and value == 0 and key == CodeHash:
    mpt_lookup(NonExistingAccountProof, key)
else:
    mpt_lookup({NonceMod,BalanceMod,CodeHashMod}, key, value_prev, value)

---

• EXTCODEHASH A // Doesn't exist
• Create A
• EXTCODEHASH A // Exists

def extcodehash():
    code_hash = lookup(addr, codeHash)
    if code_hash == 0: # doesn't exist
        return 0
    else
        return code_hash

1. Account, CodeHash, A, 0->0
2. Account, CodeHash, A, 0->H
3. Account, Nonce , A, 0->1
4. Account, CodeHash, A, H->H

RwTable

1. Account, CodeHash, A, 0->0
2. Account, CodeHash, A, 0->H
3. Account, CodeHash, A, H->H
4. Account, Nonce , A, 0->1

MptLookups

• 1-4: CodeHashMod, A, 0->H, R0->R1 // Leaf Creation via CodeHashMod
• 3: NonceMod, A, 0->1, R1->R2 // Leaf Update via NonceMod

LeafA = 0
SSTORE LeafA = 77
SLOAD LeafA
SSTORE 0 LeafA

---

• EXTCODEHASH A // Doesn't exist

1. Account, CodeHash, A, 0->0

RwTable

1. Account, CodeHash, A, 0->0

MptLookups:

• 1: NonExistingAccountProof, A, R0->R0

---

---

Changes

Storage

• State circuit specs: no change
• Circuit: apply Q1
• SLOAD/SSTORE specs + circuit: no change

Account

• State circuit specs: apply line 150-153

• Circuits: update from specs

• specs table: remove Account-NonExisting from RwTable

• BALANCE, EXTCODEHASH, EXTCODECOPY, EXTCODESIZE, CALLCODE, DELEGATECALL, STATICCALL

  • Specs: Replace usage of NonExisting tag by lookup to CodeHash with IsZero check.
  • Circuits: Implement the same logic as specs (BALANCE was already upldated with NonExisting, needs to be changed)

• CALL

  • Do lookup to CodeHash with IsZero check.

• Circuits:

  • BALANCE
  • EXTCODEHASH
  • EXTCODECOPY (skip until https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/720)
  • EXTCODESIZE
  • CALLCODE
  • DELEGATECALL
  • STATICCALL
  • CALL