## Questions
### Q1 - Storage non-existing check
Currently in State circuit it's speced [here](https://github.com/privacy-scaling-explorations/zkevm-specs/blob/4c7a2fe6db6047f07cc75d14c8258f8b5ad82c2b/src/zkevm_specs/state.py#L264-L273) as:
```python3
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](https://github.com/privacy-scaling-explorations/zkevm-specs/blob/mpt/specs/mpt/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](https://github.com/privacy-scaling-explorations/zkevm-specs/issues/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](https://github.com/privacy-scaling-explorations/zkevm-specs/issues/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:
```python
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
1. Account, CodeHash, A, 0->0, R1
3. Account, CodeHash, A, 0->H, R1
4. 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~~
3. Account, Exist, A, 0->0
4. Account, Exist, A, 0->1
5. Account, Nonce, A, 0->1
6. Account, CodeHash, A, 0->H // Code deployment
7. Account, Exist, A, 1->1 // Another step: EXTCODEHASH
8. 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
3. 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:
```python
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
```python
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
4. Account, CodeHash, A, H->H
3. 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
- [x] State circuit specs: no change
- [x] Circuit: apply Q1
- [x] SLOAD/SSTORE specs + circuit: no change
## Account
- [x] State circuit specs: apply line 150-153
- [x] Circuits: update from specs
- [x] 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:
- [x] BALANCE
- [x] EXTCODEHASH
- [ ] EXTCODECOPY (skip until https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/720)
- [x] EXTCODESIZE
- [x] CALLCODE
- [x] DELEGATECALL
- [x] STATICCALL
- [x] CALL