MPT: Initial Specification Scoping

[aguzmant103]

• Document and define clearly what our circuit is build upon. In our case, it is Geth specification.
• Explore all Geth edge cases if they can really happen.
• Describe all the theoretical edge cases and estimate probability that they will happen. If the probability is negligible (2^-128), we don't need to implement them.
• Add this as an appendix to the specification.
• Add the proof types the MPT circuit must support. Related to MPT table API for proof of non-existance #249

[aguzmant103]

Assignig this to @ed255 and @adria0 as support

[ed255]

Notes on the geth implementation:
source: https://github.com/ethereum/go-ethereum/blob/master/trie/trie.go (and other files in the trie package)
comment by Miha: some special cases are due to hexToCompact in https://github.com/ethereum/go-ethereum/blob/master/trie/encoding.go . This is how the key (the remaining nibbles that are not used in the branches above the leaf) is stored in the leaf

[aguzmant103]

In review by Miha

[ed255]

Document: https://hackmd.io/nI_STO5HQ4G-ugKnQEzctg?view

[aguzmant103]

The initial scoping didn't discover new use cases. However there are two open topics to address in the specification scoping doc:

• When the extension node is replaced with another extension node. (already mentioned in the document) @adria0 will add this.
• 16 limit in Geth and 17th element possibility: it seems this is never used. @miha-stopar will ask an internal developer of Geth if this use case is possible?

[adria0]

@miha-stopar, could you describe an example about the extension node is replaced with another extension node, please? I'm not able to find out how this happens.

[miha-stopar]

Imagine you have an extension node at n1 n2 n3 n4 (where each of these is a nibble). Let's say this extension node has the following nibbles as the extension: n5 n6 n7. So at position n1 n2 n3 n4 n5 n6 n7 there is some branch.

Now we want to add a leaf at position n1 n2 n3 n4 n5 m1 where m1 != n6. The adding algorithm walks through the trie, but it bumps into an extension node where it should put this leaf. So a new extension node is added at position n1 n2 n3 n4 which only has one nibble: n5. So at n1 n2 n3 n4 n5 we have a branch now. In this brach, at position m we have a leaf, while at position n6 we have another extension node with one extension nibble: n7. At this position (n7) we have the branch from the original extension node.

Does this help?

[miha-stopar]

Imagine you have an extension node at n1 n2 n3 n4 (where each of these is a nibble). Let's say this extension node has the following nibbles as the extension: n5 n6 n7. So at position n1 n2 n3 n4 n5 n6 n7 there is some branch.

Now we want to add a leaf at position n1 n2 n3 n4 n5 m1 where m1 != n6. The adding algorithm walks through the trie, but it bumps into an extension node where it should put this leaf. So a new extension node is added at position n1 n2 n3 n4 which only has one nibble: n5. So at n1 n2 n3 n4 n5 we have a branch now. In this brach, at position m we have a leaf, while at position n6 we have another extension node with one extension nibble: n7. At this position (n7) we have the branch from the original extension node.

Does this help?

Aha, now I see a related case is covered by Insert when branching occurs in E in the scoping document. There are multiple variations though. Sorry for confusion!

[miha-stopar]

Imagine you have an extension node at n1 n2 n3 n4 (where each of these is a nibble). Let's say this extension node has the following nibbles as the extension: n5 n6 n7. So at position n1 n2 n3 n4 n5 n6 n7 there is some branch.
Now we want to add a leaf at position n1 n2 n3 n4 n5 m1 where m1 != n6. The adding algorithm walks through the trie, but it bumps into an extension node where it should put this leaf. So a new extension node is added at position n1 n2 n3 n4 which only has one nibble: n5. So at n1 n2 n3 n4 n5 we have a branch now. In this brach, at position m we have a leaf, while at position n6 we have another extension node with one extension nibble: n7. At this position (n7) we have the branch from the original extension node.
Does this help?

Aha, now I see a related case is covered by Insert when branching occurs in E in the scoping document. There are multiple variations though. Sorry for confusion!

Ah, probably this case was added after my comments?

[adria0]

Sorry for answering so late @miha-stopar, yes, I added after your comments, could you check if correct?

[aguzmant103]

Next steps: Edu or Adria to check the changes and confirm the additions are sufficient. Afterwards we can close this issue.

[adria0]

Checked https://github.com/privacy-scaling-explorations/zkevm-specs/blob/5cda455650b27d25dc9e3472c387f4b3e1942c3d/specs/mpt/scope.md

There is the For cases when additional extension node need to be inserted, the implementation is not ready yet. comment, but IMO we can move forward with the MPT spec review.

Waiting for @ed255 comments, if there's something else to address.

[miha-stopar]

There is the For cases when additional extension node need to be inserted, the implementation is not ready yet. comment, but IMO we can move forward with the MPT spec review.

Yes, this is not ready yet, it is being implemented in privacy-scaling-explorations/zkevm-circuits#914.

[ed255]

I have reviewed https://github.com/privacy-scaling-explorations/zkevm-specs/blob/5cda455650b27d25dc9e3472c387f4b3e1942c3d/specs/mpt/scope.md

I see that the hackmd contains 4 cases in Insert when branching occurs in L that are not in the scope.md; I would like to understand if they are covered by other cases that are equivalent, or they are missing?

I've also checked https://github.com/privacy-scaling-explorations/zkevm-specs/blob/5cda455650b27d25dc9e3472c387f4b3e1942c3d/specs/mpt/mpt-proof.md which covers the use cases that the MPT circuit supports. This is the list from the specs:

• Storage modification
• Nonce modification
• Balance modification
• Codehash proof
• Account delete modification
• Non existing account proof
• Non existing storage proof

My question is:

• Does Storage modification also support Storage leaf creation and storage leaf deletion?
• Does Nonce modification also support Account leaf creation with Nonce value and the rest of fields to default?
• Does Balance modification also support Account leaf creation with Balance value and the rest of fields to default?

If the answer to these questions is yes, could you please extend the mpt-proof.md document to explain that these proof types also support the above transitions?

The rest looks very good! Thanks a lot @miha-stopar !

[miha-stopar]

Thank you for reviewing @ed255 !

The answer is yes, I added a sentence to mpt-proof.md here.

For example, a test for implicit account creation with nonce modification is generated here.