Mmp-trees
Modified Merkle Patricia trees.
A Modified Merkle Patricia tree
(which we abbreviate as `MMP tree'
in the documentation of our Ethereum model)
is an Ethereum data structure
that combines characteristics of
Merkle trees and Patricia (a.k.a. radix) trees.
MMP trees are described in [YP:D] and in
Page `Patricia Tree' of [Wiki];
we reference that page of [Wiki] as `[Wiki:MMP]'.
MMP trees are not merely implementation-level entities.
Their root hashes appear
at the interface of Ethereum with the external world,
e.g. as the stateRoot component of a block [YP:4.3].
Thus, a formalization of MMP trees,
in particular of the calculation of root hashes,
belongs to a formal model of Ethereum
that covers the interface to the external world,
even if the formal model is high-level, declarative, and non-executable.
Subtopics
- Mmp-encode-n/c
- Definition of n [YP:(193)] and c [YP:(194)].
- Mmp-encode-c-max
- Value of the maximum operator
in the second case of the definition of c [YP:(194)].
- Mmp-encode
- Encode a finite map into an MMP tree.
- Mmp-write
- Write a value for a key in an MMP tree.
- Mmp-decode
- Decode an MMP tree into a finite map.
- Mmp-encode-u-map
- Submaps used to define u(0),\ldots,u(15)
in the third case of the definition of c [YP:(194)].
- Nibblelist-bytelist-map-sup-len-key
- Natural number supremum of the lengths of the keys
in a map from nibble arrays to byte arrays.
- Mmp-encode-c-forall
- Universally quantified formula
in the second case of the definition of c [YP:(194)].
- Mmp-read
- Read the value associated to a key in an MMP tree.
- Mmp-encoding-p
- Check if a root and database are an MMP encoding
of a finite map from byte arrays to byte arrays.
- Bytelist-to-nibblelist-keys
- Turn (i) a finite map from byte arrays to byte arrays
into (ii) a finite map from nibble arrays to byte arrays.
- Mmp-encode-c-exists
- Existentially quantified formula
in the second case of the definition of c [YP:(194)].
- Bytelist-bytelist-map
- Finite maps from byte arrays to byte arrays.
- Nibblelist-bytelist-map
- Finite maps from nibble arrays to byte arrays.
