1 Merkle Patricia tree
2 Types
type hashed = | Hashed of Hash.Prefix.t| Not_HashedType used to prove that if a node is hashed then so are its children. The type also provides the hash as a witness.
*)type indexed = | Indexed of Index.t| Not_IndexedThis rule expresses the following invariant : if a node is indexed, then its children are necessarily indexed. Less trivially, if an internal node is not indexed then at least one of its children is not yet indexed. The reason is that we never construct new nodes that just point to only existing nodes. This property guarantees that when we write internal nodes on disk, at least one of the child can be written adjacent to its parent.
*)view constructors are private. Use _Internal, _Bud, _Leaf, and _Extender functions with runtime invariant checks.
type t = node 2 Constructors with invariant checks
2 Accessors
val indexed : node -> boolval hashed : node -> boolval hash_available : node -> boolval hash_prefix_of_view : view -> Hash.Prefix.t option 2 Tools to create Not_Indexed and Not_Hashed nodes
2 Loading of nodes
2 Debug
val pp : Stdlib.Format.formatter -> node -> unitPretty printer
2 Mapper
module Mapper : sig ... endMapper over a node
module Fold : sig ... endFold over a node
module Fold' : sig ... endFold over a node
Returns the hash of the view already loaded. It returns None if the view does not have the hash.
Note that hash_of_view (Extender (_, n, _, Not_Hashed)) = None even when n has its hash loaded.
Random generators
gen_bud depth is a generator of Internal node with about depth sides