Mmp-encode
Encode a finite map into an MMP tree.
- Signature
(mmp-encode map) → (mv error? root database)
- Arguments
- map — Guard (bytelist-bytelist-mapp map).
- Returns
- error? — Type (member-eq error? '(nil :collision :rlp)).
- root — Type (byte-listp root).
- database — Type (databasep database).
This corresponds to the definition of \mathtt{TRIE} [YP:(192)].
The input is a finite map from byte arrays to byte arrays,
which we convert to a finite map from nibble arrays to byte arrays
before calling the mutually recursive encoding functions.
This is left somewhat implicit in [YP:D],
which uses the same symbol \mathfrak{I}
for both kinds of maps.
Even though \mathtt{TRIE} just returns a root (a byte array),
the encoding relies on the database.
As done for
mmp-encode-n, mmp-encode-c, and mmp-encode-u,
we explicate the database constructed to encode the map
as an additional result;
the returned root and database form the MMP tree.
We also return an error flag
with the same meaning as the one returned by those functions.
[YP:(192)] may call c with an empty map,
which, as discussed in mmp-encode-n/c,
is prohibited by the guard of mmp-encode-c,
because the maximum calculated
in the second case of the definition of c
is not well-defined if the map is empty.
Looking at [YP:(192)] and [YP:(193)],
it seems more plausible that
\mathtt{TRIE} should be defined as n(\mathfrak{I},0),
which should often be the same as \mathtt{KEC}(c(\mathfrak{I},0)),
except (critically) in the case in which the map is empty,
and except in the case in which the byte array returned by c is short
(i.e. less than 32 bytes in length).
The first paragraph of [YP:D] says that
the map is encoded as a single value that is
either a 32-byte sequence of bytes (i.e. a hash)
or the empty byte sequence.
The mention of the empty sequence contradicts
the definition of \mathtt{TRIE} as \mathtt{KEC}(\ldots)
(since \mathtt{KEC} always returns 32 bytes),
and supports our interpretation.
On the other hand, the lack of mention
of byte sequences of lengths between 1 and 31
contradicts our interpretation,
for the case in which n returns a short byte sequence.
For now we take this interpretation anyhow,
but we may revise our formal definition
once we disambiguate the definition of \mathtt{TRIE}.
We note that another possible interpretation might be
to define \mathtt{TRIE}(\mathfrak{I}) as
\mathtt{KEC}(n(\mathfrak{I},0)) (i.e. n instead of c).
But this would involve a double hash for the common case,
and would never allow the empty byte sequence.
Note that, according to our disambiguation and definition,
the root hash returned by this function
is not necessarily a Keccak-256 hash;
it may be a shorter byte sequence.
Definitions and Theorems
Function: mmp-encode
(defun mmp-encode (map)
(declare (xargs :guard (bytelist-bytelist-mapp map)))
(mmp-encode-n (bytelist-to-nibblelist-keys map)
0))
Theorem: return-type-of-mmp-encode.error?
(defthm return-type-of-mmp-encode.error?
(b* (((mv ?error? ?root ?database)
(mmp-encode map)))
(member-eq error? '(nil :collision :rlp)))
:rule-classes :rewrite)
Theorem: byte-listp-of-mmp-encode.root
(defthm byte-listp-of-mmp-encode.root
(b* (((mv ?error? ?root ?database)
(mmp-encode map)))
(byte-listp root))
:rule-classes :rewrite)
Theorem: databasep-of-mmp-encode.database
(defthm databasep-of-mmp-encode.database
(b* (((mv ?error? ?root ?database)
(mmp-encode map)))
(databasep database))
:rule-classes :rewrite)
Theorem: mmp-encode-of-bytelist-bytelist-mfix-map
(defthm mmp-encode-of-bytelist-bytelist-mfix-map
(equal (mmp-encode (bytelist-bytelist-mfix map))
(mmp-encode map)))
Theorem: mmp-encode-bytelist-bytelist-mequiv-congruence-on-map
(defthm mmp-encode-bytelist-bytelist-mequiv-congruence-on-map
(implies (bytelist-bytelist-mequiv map map-equiv)
(equal (mmp-encode map)
(mmp-encode map-equiv)))
:rule-classes :congruence)
