plebeia

Functional storage using Merkle Patricia tree
package plebeia
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library plebeia
Module Plebeia . Node
include module type of struct include Node_type end

2 Types

type hashed =
| Hashed of Hash.Prefix.t
| Not_Hashed(*

Type 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_Indexed(*

This 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.

*)
type extender_witness =
| Maybe_Extender
| Not_Extender
| Is_Extender
type node =
| Disk of Index.t * extender_witness
| View of view
| Hash of Hash.t
and view = private
| Internal of node * node * indexed * hashed
| Bud of node option * indexed * hashed
| Leaf of Value.t * indexed * hashed
| Extender of Segment.t * node * indexed * hashed

view constructors are private. Use _Internal, _Bud, _Leaf, and _Extender functions with runtime invariant checks.

type t = node

2 Constructors with invariant checks

val _Internal : (node * node * indexed * hashed) -> view
val _Bud : (node option * indexed * hashed) -> view
val _Leaf : (Value.t * indexed * hashed) -> view
val _Extender : (Segment.t * node * indexed * hashed) -> view

2 Accessors

val indexed : node -> bool
val index : node -> Index.t option
val hashed : node -> bool
val hash_available : node -> bool
val index_of_view : view -> Index.t option
val hash_prefix_of_view : view -> Hash.Prefix.t option

2 Tools to create Not_Indexed and Not_Hashed nodes

val new_internal : node -> node -> node
val new_bud : node option -> node
val new_leaf : Value.t -> node
val new_extender : Segment.t -> node -> node

2 Loading of nodes

val may_forget : node -> node option

If the node is indexed, forget the details

2 Debug

val pp : Stdlib.Format.formatter -> node -> unit

Pretty printer

2 Mapper

module Mapper : sig ... end

Mapper over a node

module Fold : sig ... end

Fold over a node

module Fold' : sig ... end

Fold over a node

val hash_of_view : view -> Hash.t option
val hash_of_node : node -> view option * Hash.t option

Random generators

val gen_leaf : t Gen.t
val gen_bud_none : t Gen.t
val gen_bud : int -> t Gen.t

gen_bud depth is a generator of Bud node with about depth sides

val gen_internal : int -> t Gen.t

gen_bud depth is a generator of Internal node with about depth sides

val gen_extender : int -> t Gen.t

gen_bud depth is a generator of Extender node with about depth sides

Node reading from a context

Obtain the view of the node. If the view is not available in the memory, it is loaded from the storage.

val compute_hash : Context.t -> Node_type.node -> Node_type.node * Hash.t

Compute the hash of the node with its view