Database
Database.
As explained in [YP:D.1] and [YP:4.1],
MMP trees
rely on a database that associates byte arrays to hashes,
where hashes are byte arrays of length 32 resulting from Keccak-256.
This is called `trie database' in [YP:D.1], and just `DB' in [Wiki:MMP].
[YP:4.1] uses the term `state database',
but it does so in the context of the world state;
indeed,
the database also contains data that is not part of the world state,
such as transactions and transaction receipts.
In the documentation of our Ethereum model, we use the term `database'.
We introduce a fixtype for finite maps
from byte arrays of length 32
to byte arrays,
based on the fixtype of omaps.
Subtopics
- Databasep
- Recognizer for database.
- Database-fix
- (database-fix x) is a usual ACL2::fty omap fixing function.
- Database-equiv
- Basic equivalence relation for database structures.
