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.

- Mmp-encode-n/c
- Definition of
n [YP:(193)] andc [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 ofc [YP:(194)]. - Nibblelist-bytelist-map-sup-len-key
- Natural number supremum of the lenghts 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.