Consisntency between State circuit account updates and MPT

[ed255]

Related to #354 and #259

The current design involves encoding non-existing accounts in the State Circuit as account with code_hash = 0.
Notice that the update proofs that the MPT circuit supports require that the leaf exists after the update (so they can be used as account field update proof or account creation proof with an initial account field value).
Using code_hash = 0 means that we can end up with a StateCircuit "merged" update of code_hash 0 -> 0. This is interpreted as account didn't exist before and doesn't exist afterwards, so the StateCircuit maps it to an AccountNonExisting proof of the MPT.

Nevertheless I found out that this is not enough. Even if we follow these rules:

• 1. Before writing/reading a field of a possibly non-existing account, read it's code_hash
• 2a. If we are reading, skip lookup and use default value
• 2b. If we are writing, first create the account by setting code_hash = EMPTY_HASH

We may encounter a Rw trace that is incompatible with the MPT proof types with the current State Circuit implementation, and this comes from the fact that a revert will delete an account.

Imagine the following scenario with account creation that is reverted:

Rw chronological trace:

• [...]
• rwc=1 WRITE Account.CodeHash address=A 0->EMPTY_HASH
• rwc=2 WRITE Account.Nonce address=A 0->1
• [...]
• rwc=3 WRITE Account.Nonce address=A 1->0 (revert rw)
• rwc=4 WRITE Account.CodeHash address=A EMPTY_HASH->0 (revert rw)
• [...]

RwTable:

• rwc=1 WRITE Account.CodeHash address=A 0->EMPTY_HASH
• rwc=4 WRITE Account.CodeHash address=A EMPTY_HASH->0 (revert rw)
• rwc=2 WRITE Account.Nonce address=A 0->1
• rwc=3 WRITE Account.Nonce address=A 1->0 (revert rw)

State - MPT updates:

• Account.CodeHash address=A 0->0
• Account.Nonce address=A 0->0

We end up with a Nonce update from 0->0 for an account that doesn't exist. The State Circuit currently doesn't support this scenario.
Here are the list of special cases we can encounter:

• A. Account.CodeHash 0->0
  • This is already supported
  • Can only happen when account didn't exist before, and doesn't exist after. This is because code_hash=0 never happens naturally, and use use it to encode account non-existence.
• B. Account.Nonce 0->0
  • This is currently not supported,
  • This can be a non-existing proof or a read existing proof, because nonce=0 doesn't tell us anything about account existence (for example, after a transfer to a non-existing account, the account is created with positive balance but nonce is still 0).
• C. Account.Balance 0->0
  • This is currently not supported.
  • This can be a non-existing proof or a read existing proof, because balance=0 doesn't tell us anything about account existence.

Thoughts and possible solutions.

• We need a way to map Account.Nonce 0->0 and Account.Balance 0->0 to non-existing proofs conditionally.
• I think this condition could be a "free" witness value.
• Assume that we always follow the rule in the EVM Circuit to read code_hash before doing anything with a possibly non-existing account, and create accounts by setting code_hash != 0 as the first account write lookup.
  • If we sort Account.CodeHash in RwTable before Account.Nonce, Account.Balance, AccountStorage, we know that the StateTrie Root at after all Account.CodeHash updates has a leaf for each account that will exist by the end of the block.
  • If we find Account.Nonce 0->0 or Account.Balance 0->0 we don't care if the account exists or not, only that one of these is true: either the account exists, or it has the account field value at 0. The reason why we don't care, is because in the EVM Circuit we previously performed a CodeHash read to determine account existence and proceeded with constraints using that information.