Skip to content

fix: minor typos in the docs #112

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: v0.7
Choose a base branch
from
Open

fix: minor typos in the docs #112

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
435e4e1
fix typos mpt-proof.md
tudorpintea999 Nov 2, 2023
acd213e
Merge branch 'scroll-tech:v0.7' into fix-typos
tudorpintea999 Dec 5, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 21 additions & 21 deletions spec/mpt-proof.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,23 +31,23 @@ The MPT table is constructed following this [zkTrie spec].
Each row of the MPT table reflects an

- `MPTUpdate`
- `key`: `AccountStorage` or `Account`, each one has its onw data fields
- `key`: `AccountStorage` or `Account`, each one has its own data fields
- `old_value` and `new_value`, change in value
- `old_root` and `new_root`, change in trie root

Columns `address` and `storage_key` indicate the location where changes in account or storage happen.

## The purpose of MPT circuit and its witness generation inside [zkevm-circuits]
## The purpose of the MPT circuit and its witness generation inside [zkevm-circuits]

MPT circuit aims at proving the correctedness of the MPT table described above. This means its constraint system enforces a unique structure of the MPT (zkTrie) as described.
MPT circuit aims at proving the correctness of the MPT table described above. This means its constraint system enforces a unique structure of the MPT (zkTrie) as described.

When the MPT is changed due to account or storage updates, MPT circuit must prove this update leads to the correct root change. We [encode](https://github.com/scroll-tech/zkevm-circuits/blob/c656b971d894102c41c30000a40e07f8e0520627/zkevm-circuits/src/witness/mpt.rs#L77) one step of `MPTUpdate` into an `SMTTrace` that carries [old_path, new_path] on the trie for account/storage. Here SMT stands for <i>Sparse Merkle Trie</i> (this confirmed by repo author @noel2004).
When the MPT is changed due to account or storage updates, the MPT circuit must prove this update leads to the correct root change. We [encode](https://github.com/scroll-tech/zkevm-circuits/blob/c656b971d894102c41c30000a40e07f8e0520627/zkevm-circuits/src/witness/mpt.rs#L77) one step of `MPTUpdate` into an `SMTTrace` that carries [old_path, new_path] on the trie for account/storage. Here SMT stands for <i>Sparse Merkle Trie</i> (this confirmed by repo author @noel2004).

Both paths are from root to leaf, encoding the change of path in that step. This construction is done inside the [zkTrie] of the zkevm-circuits.

<i>Note: Refactor logic (for account as example) is [handle_new_state](https://github.com/scroll-tech/zkevm-circuits/blob/7e821a9386e6c9aad85ef40e669986305e04dc77/zktrie/src/state/witness.rs#L258) (update the trie according to `MPTProofType` category) -> [trace_account_update](https://github.com/scroll-tech/zkevm-circuits/blob/7e821a9386e6c9aad85ef40e669986305e04dc77/zktrie/src/state/witness.rs#L182) (provide old and new paths in the trie based on the update) -> [decode_proof_for_mpt_path](https://github.com/scroll-tech/zkevm-circuits/blob/7e821a9386e6c9aad85ef40e669986305e04dc77/zktrie/src/state/witness.rs#L398) (determine the path, which must start from root and end at either a leafnode or an empty node in the old/new trie based on the given key).</i>
<i>Note: Refactor logic (for account as an example) is [handle_new_state](https://github.com/scroll-tech/zkevm-circuits/blob/7e821a9386e6c9aad85ef40e669986305e04dc77/zktrie/src/state/witness.rs#L258) (update the trie according to `MPTProofType` category) -> [trace_account_update](https://github.com/scroll-tech/zkevm-circuits/blob/7e821a9386e6c9aad85ef40e669986305e04dc77/zktrie/src/state/witness.rs#L182) (provide old and new paths in the trie based on the update) -> [decode_proof_for_mpt_path](https://github.com/scroll-tech/zkevm-circuits/blob/7e821a9386e6c9aad85ef40e669986305e04dc77/zktrie/src/state/witness.rs#L398) (determine the path, which must start from root and end at either a leafnode or an empty node in the old/new trie based on the given key).</i>

<i>Note: In [zkTrie] the update is constructed according to `MPTProofType`, and for `MPTProofType::AccountDoesNotExist` and `MPTProofType::StorageDoesNotExist` the convention here is that the provided account/storage is empty both <b>before and after</b> the update. The proof of non-existence of account before writing into or after deletion from the existing mpt, will be included as separate constraints that correspond to different types of non-existence proof (we call them type 1 and type 2 non-existence, see below).</i>
<i>Note: In [zkTrie] the update is constructed according to `MPTProofType`, and for `MPTProofType::AccountDoesNotExist` and `MPTProofType::StorageDoesNotExist` the convention here is that the provided account/storage is empty both <b>before and after</b> the update. The proof of non-existence of the account before writing into or after deletion from the existing mpt, will be included as separate constraints that correspond to different types of non-existence proof (we call them type 1 and type 2 non-existence, see below).</i>

`SMTTrace` consists of the following hierarchy of notions:

Expand All @@ -73,7 +73,7 @@ Both paths are from root to leaf, encoding the change of path in that step. This
- Either account update can be `None`, if the `SMTTrace` is for an update to an account that previously doesn't exist, or the update for `MPTProofType::AccountDoesNotExist`.
- `state_path`: `Option<[Option<SMTPath>; 2]>`. SMTPath's for **storage** trie. There are 5 possibilities for `None`/`Some(...)` here:
1. `None`: the update doesn't touch the account's storage. I.e. the proof type matches `MPTProofType::{NonceChanged, BalanceChanged, CodeHashExists, PoseidonCodeHashExists, CodeSizeExists, AccountDoesNotExist}`
2. `[None, None]` the storage slot for the update starts and ends with value 0. Either the proof type is `MPTProofType::StorageDoesNotExist` or it is `MPTProofType::StorageChanged` and the new and old values are both 0.
2. `[None, None]` the storage slot for the update starts and ends with the value 0. Either the proof type is `MPTProofType::StorageDoesNotExist` or it is `MPTProofType::StorageChanged` and the new and old values are both 0.
3. `[Some(...), Some(...)]`: the proof type is `MPTProofType::StorageChanged` and the new and old values are non-zero.
4. `[None, Some(...)]`: the proof type is `MPTProofType::StorageChanged` and the old value is 0 and the new value is non-zero.
5. `[Some(...), None]`: the proof type is `MPTProofType::StorageChanged` and the old value is non-zero and the new value is non-zero.
Expand Down Expand Up @@ -170,17 +170,17 @@ Circuit configures constraints for each [`MPTProofType`](https://github.com/scro

|old_hash|new_hash|old_value|new_value|proof_type|address|storage_key_rlc|segment_type|path_type|depth|key|other_key|other_key_hash|other_leaf_data_hash|direction|sibling|upper_128_bits|
|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|-|
|node's open hash|node's close hash|node's open value|node's close value|MPTProofType|||Start, AccountTrie, AccountLeaf0, AccountLeaf1, AccountLeaf2, AccountLeaf3, AccountLeaf4, StorageTrie, StorageLeaf0, StorageLeaf1|Common, ExtensionOld, ExtensionNew|depth increase from root to leaf, from current row to next row|provided key|match provided key with existing mpt path key, until reaching leafnode, obtain resulting key. For type 1 non-existence proof, this key is different from provided key, for type 2 non-existence proof, this key is same as provided key|hash(1, other_key) if other_key matches provided key, else is 0|hash of the leaf/empty node pointed by other key|direction must match key|sibling node's hash|most significant 128 bits of address or storage key|
|node's open hash|node's close hash|node's open value|node's close value|MPTProofType|||Start, AccountTrie, AccountLeaf0, AccountLeaf1, AccountLeaf2, AccountLeaf3, AccountLeaf4, StorageTrie, StorageLeaf0, StorageLeaf1|Common, ExtensionOld, ExtensionNew|depth increase from root to leaf, from current row to next row|provided key|match provided key with existing mpt path key, until reaching leafnode, obtain resulting key. For type 1 non-existence proof, this key is different from provided key, for type 2 non-existence proof, this key is the same as provided key|hash(1, other_key) if other_key matches provided key, else is 0|hash of the leaf/empty node pointed by other key|direction must match key|sibling node's hash|most significant 128 bits of address or storage key|

Each circuit row represents the mpt update (from old to new) of a path from root to leaf, at a certain depth (depth of root is 0). So each row represents only one node (virtual node in case it does not exist). The row offset order `previous --> current --> next` indicates an increase of depth towards leafnode.

The configuration changes to the MPT is characterized by the following two columns:
The configuration changes to the MPT are characterized by the following two columns:

(1) `PathType`: This characterizes topological structural change. It includes `PathType::Start`, `PathType::Common`, `PathType::ExtensionOld` and `PathType::ExtensionNew`;

(2) `SegmentType`: This characterizes data field (which form the trie's leafnode hash) change. It includes `SegmentType::Start`, `SegmentType::AccountTrie`, `SegmentType::AccountLeaf0`-`SegmentType::AccountLeaf4`, `SegmentType::StorageTrie`, `SegmentType::StorageLeaf0`-`SegmentType::StorageLeaf1`.
(2) `SegmentType`: This characterizes data field (which forms the trie's leafnode hash) change. It includes `SegmentType::Start`, `SegmentType::AccountTrie`, `SegmentType::AccountLeaf0`-`SegmentType::AccountLeaf4`, `SegmentType::StorageTrie`, `SegmentType::StorageLeaf0`-`SegmentType::StorageLeaf1`.

In both of the above two column witnesses, `Start` is used as boundary marker between updates. This means each circuit row with a `Start` indicates a new MPT update.
In both of the above two-column witnesses, `Start` is used as a boundary marker between updates. This means each circuit row with a `Start` indicates a new MPT update.


### Topological structure changes to the trie, their corresponding mpt operations and account/storage types
Expand All @@ -190,7 +190,7 @@ Operations to the trie can be classified as
(1) <i>modify</i>: an account/storage slot is being changed. The account/storage under this operation is named <b>type 0</b>, i.e., type 0 account/storage are in the MPT. This means that they're non-emtpy, i.e. at least one of their fields is non-zero. Figure below:
![PathType_Common_modify](https://i.imgur.com/jPtyZia.jpg)

(2) <i>insert to/delete from append</i>: an account/storage slot is inserted to the MPT as append, i.e. it forms a new leafnode that previously does not exist even as empty nodes (<i>insert to append</i>), or it is deleted from an appended leaf, i.e., after deletion there will be no node (including empty node) left (<i>delete from append</i>). The account/storage under this operation is named <b>type 1</b>, i.e., type 1 account/storage are empty. Where they could be in the MPT, there is instead a leaf node that maps to another non-empty account/storage. Figure below (for insert case, and delete case just swap old and new):
(2) <i>insert to/delete from append</i>: an account/storage slot is inserted to the MPT as append, i.e. it forms a new leafnode that previously does not exist even as empty nodes (<i>insert to append</i>), or it is deleted from an appended leaf, i.e., after deletion there will be no node (including empty node) left (<i>delete from append</i>). The account/storage under this operation is named <b>type 1</b>, i.e., type 1 account/storage is empty. Where they could be in the MPT, there is instead a leaf node that maps to another non-empty account/storage. Figure below (for insert case, and delete case just swap old and new):
![PathType_ExtensionNew_append](https://i.imgur.com/n45hYz3.jpg)
Notice that the zkTrie adds only one bit of common prefix at each level of its depth. It also applies the optimization that replaces subtrees consisting of exactly one leaf with a single leaf node to reduce the tree height. This means that when inserting/deleting new account as append, it may happen that an extension happens with some intermediate nodes that provide key prefix bits, either for the old path or for the new path. It is constrained that at all the new siblings added are empty nodes.

Expand All @@ -201,19 +201,19 @@ Notice that the zkTrie adds only one bit of common prefix at each level of its d

#### PathType::Common

`PathType::Common` refers to the sitation that the old and new path share the same toplogical configuration.
`PathType::Common` refers to the situation that the old and new path share the same topological configuration.

This can correspond to the toloplgical configuration change on the whole path in the modify operation, or the common path (not extended one) of the insert to/delete from append, or the insert to/delete from fill operations.
This can correspond to the topological configuration change on the whole path in the modify operation, or the common path (not extended one) of the insert to/delete from append, or the insert to/delete from fill operations.

#### PathType::ExtensionNew

`PathType::ExtensionNew` refers to the sitation that the new path extends the old path in its toplogical configuration.
`PathType::ExtensionNew` refers to the situation that the new path extends the old path in its topological configuration.

This can correspond to the extended part of the path in insert to append, insert to fill operations.

#### PathType::ExtensionOld

`PathType::ExtensionOld` refers to the sitation that the old path extends the new path in its toplogical configuration.
`PathType::ExtensionOld` refers to the situation that the old path extends the new path in its topological configuration.

This can correspond to the extended part of the path in delete from append, delete from fill operations.

Expand All @@ -224,7 +224,7 @@ Each circuit row will be assigned a PathType at witness generation. Along a path
#### <i>Discussion: Can we come up with a simpler way of looking at all the PathTypes?</i>
<i>In fact, if we do not compress subtrees with empty nodes as in the [zkTrie spec], then we can combine the two subcases in account addition case (or account deletion case). Here the previous figure for `PathType::ExtensionNew` in account addition case becomes the following
![PathTypeDiscussion_FullTrieCase](https://i.imgur.com/0D6BYhb.jpg)
However, using the empty-node compression in the current [zkTrie spec] will result in extension and we have to work with various PathTypes. This is a trade-off, though from the above agument based on whether old path hits a leaf or an empty node, we know that we exhausted all path types.</i>
However, using the empty-node compression in the current [zkTrie spec] will result in an extension and we have to work with various PathTypes. This is a trade-off, though, from the above argument based on whether the old path hits a leaf or an empty node, we know that we exhausted all path types.</i>



Expand All @@ -234,11 +234,11 @@ These cases of non-existence proofs do <b>not</b> really correspond to `MPTProof

There are 2 cases to constrain based on the path directed by the provided non-existing key (coming from hash of account address):

- <b>Type 1 non-existence proof</b> (insert to append/delete from append): the path ended at a leaf node. Illustration figure shown below:
- <b>Type 1 non-existence proof</b> (insert to append/delete from append): the path ended at a leaf node. The illustration figure shown below:
![AccountNotExist_Leaf](https://i.imgur.com/SyExuBC.png)
In this case, due to our construction of the old and new paths of `SMTTrace`, the old path (when inserting)/new path (when deleting) must be directed to this leaf node. The prefix key provided by the old/new path must end at a bit position <i>before</i> the last bit of the leaf key that is to be proved non-exist. So we constrain that the non-existing account/storage must have its key that is not equal to the key at this leaf node. Circuit columns `other_key`, `other_key_hash`, `other_leafnode_hash` and an IsEqualGadget `key_equals_other_key` are used to provide witness to these constraints and to constrain.

- <b>Type 2 non-existence proof</b> (insert to fill/delete from fill): the path ended at an empty node. Illustration figure shown below:
- <b>Type 2 non-existence proof</b> (insert to fill/delete from fill): the path ended at an empty node. The illustration figure shown below:
![AccounNotExist_Empty](https://i.imgur.com/FLxg11Q.png)
In this case, due to our construction of the old and new paths of `SMTTrace`, the old path (when inserting)/new path (when deleting) must be directed to this empty node. So we constrain the emptiness of these nodes. Circuit provides two IsZeroGadgets `old_hash_is_zero` and`new_hash_is_zero` to constrain this case.

Expand Down Expand Up @@ -269,7 +269,7 @@ For storage, the formula for `valueHash` is

The above expansions are beyond what the original trie defined in [zkTrie spec] can have, where the expansion of the trie will only be up to leafnodes that are classified into `AccountTrie` or `StorageTrie`, i.e. trie-type segments. The leaf-type segments (non-trie segments) are witnesses generated <i>inside</i> the circuit (parsed from `SMTTrace`), and the trie-like structure shown above are just imaginary/virtual which only lives in the circuit. So such common constraints as key is 0 and depth is 0 for non-trie segments must be enforced in the circuit constraint system.

The `PathType` used inside the circuit is also corresponding to this expanded trie including leaf-type segments (non-trie segments). For example, in the case of insert to fill operation, `PathType` changes from `Common` to `ExtensionNew` at the empty node that is filled by a new leaf, and the path continues to the specific account/storage field. So constraints for `PathType::ExtensionNew(Old)` must discuss separately for trie and non-trie segment cases.
The `PathType` used inside the circuit is also corresponding to this expanded trie including leaf-type segments (non-trie segments). For example, in the case of insert to fill operation, `PathType` changes from `Common` to `ExtensionNew` at the empty node that is filled by a new leaf, and the path continues to the specific account/storage field. So constraints for `PathType::ExtensionNew(Old)` must be discussed separately for trie and non-trie segment cases.


### Constraints
Expand Down Expand Up @@ -300,7 +300,7 @@ on rows with `PathType::Common`:
#### PathType::ExtensionNew
on rows with `PathType::ExtensionNew`:
- `old_value==0`
- old path has `old_hash` keep unchanged on the extended path
- old path has `old_hash` kept unchanged on the extended path
- new path has `new_hash=poisedon_hash(leftchild, rightchild)`
- on trie segments (`is_trie==true`)
- In case next`SegmentType` is still trie type (`is_final_trie_segment==false` )
Expand Down