Bytelist-bytelist-map
Finite maps from byte arrays to byte arrays.
We introduce a fixtype for finite maps
from byte arrays to byte arrrays,
based on the fixtype of omaps.
An MMP tree represents a finite map from byte arrays to byte arrays,
as described by \mathfrak{I} [YP:(188)].
The type we introduce here models these finite maps.
Note that there are no constraints on the lengths of the keys or values,
because the construction of MMP trees from these finite maps
(which is described in [YP:D])
does not depend on any such length constraints.
Subtopics
- Bytelist-bytelist-mfix
- (bytelist-bytelist-mfix x) is a usual ACL2::fty omap fixing function.
- Bytelist-bytelist-mapp
- Recognizer for bytelist-bytelist-map.
- Bytelist-bytelist-mequiv
- Basic equivalence relation for bytelist-bytelist-map structures.
