123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361(*****************************************************************************)(* *)(* Open Source License *)(* Copyright (c) 2022 Nomadic Labs <contact@nomadic-labs.com> *)(* *)(* Permission is hereby granted, free of charge, to any person obtaining a *)(* copy of this software and associated documentation files (the "Software"),*)(* to deal in the Software without restriction, including without limitation *)(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)(* and/or sell copies of the Software, and to permit persons to whom the *)(* Software is furnished to do so, subject to the following conditions: *)(* *)(* The above copyright notice and this permission notice shall be included *)(* in all copies or substantial portions of the Software. *)(* *)(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*)(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*)(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)(* DEALINGS IN THE SOFTWARE. *)(* *)(*****************************************************************************)typeerror+=Merkle_list_invalid_positionletmax_depth~count_limit=(* We assume that the Merkle_tree implementation computes a tree in a
logarithmic size of the number of leaves. *)letlog2n=Z.numbits(Z.of_intn)inlog2count_limitlet()=register_error_kind`Temporary~id:"Merkle_list_invalid_position"~title:"Merkle_list_invalid_position"~description:"Merkle_list_invalid_position"~pp:(funppf()->Format.fprintfppf"%s""Merkle_list_invalid_position")Data_encoding.empty(functionMerkle_list_invalid_position->Some()|_->None)(fun()->Merkle_list_invalid_position)moduletypeT=sigtypettypehtypeelttypepathvaldummy_path:pathvalpp_path:Format.formatter->path->unitvalnil:tvalempty:hvalroot:t->hvalsnoc:t->elt->tvalsnoc_tr:t->elt->tvalof_list:eltlist->tvalcompute:eltlist->hvalpath_encoding:pathData_encoding.tvalbounded_path_encoding:?max_length:int->unit->pathData_encoding.tvalcompute_path:t->int->pathtzresultvalcheck_path:path->int->elt->h->booltzresultvalpath_depth:path->intvalelt_bytes:elt->Bytes.tmoduleInternal_for_tests:sigvalpath_to_list:path->hlistvalequal:t->t->boolvalto_list:t->hlistendendmoduleMake(El:sigtypetvalto_bytes:t->bytesend)(H:S.HASH):Twithtypeelt=El.tandtypeh=H.t=structtypeh=H.ttypeelt=El.tletelt_bytes=El.to_bytes(*
The goal of this structure is to model an append-only list.
Its internal representation is that of a binary tree whose
leaves are all at the same level (the tree's height).
To insert a new element in a full tree t, we create a new root with t
as its left subtree and a new tree t' as its right subtree. t' is just a
left-spine of the same height as t. Visually,
t = / \ t' = / snoc 4 t = / \
/\ /\ / / \ /
0 1 2 3 4 /\ /\ /
0 1 2 3 4
Then, this is a balanced tree by construction.
As the key in the tree for a given position is the position's
binary decomposition of size height(tree), the tree is dense.
For that reason, the use of extenders is not needed.
*)typetree=Empty|Leafofh|Nodeof(h*tree*tree)(* The tree has the following invariants:
A node [Node left right] if valid iff
1. [right] is Empty and [left] is not Empty, or
2. [right] is not Empty and [left] is full
Additionally:
[t.depth] is the height of [t.tree] and
[t.next_pos] is the number of leaves in [t.tree] *)typet={tree:tree;depth:int;next_pos:int}typepath=hlistletdummy_path=[]letpp_pathppf=Format.fprintfppf"%a"(Format.pp_print_list~pp_sep:(funfmt()->Format.fprintffmt";@ ")H.pp)letempty=H.zeroletroot=functionEmpty->empty|Leafh->h|Node(h,_,_)->hletnil={tree=Empty;depth=0;next_pos=0}lethash_eltel=H.hash_bytes[elt_bytesel]letleaf_ofel=Leaf(hash_eltel)lethash2h1h2=H.(hash_bytes[to_bytesh1;to_bytesh2])letnode_oft1t2=Node(hash2(roott1)(roott2),t1,t2)(* to_bin computes the [depth]-long binary representation of [pos]
(left-padding with 0s if required). This corresponds to the tree traversal
of en element at position [pos] (false = left, true = right).
Pre-condition: pos >= 0 /| pos < 2^depth
Post-condition: len(to_bin pos depth) = depth *)letto_bin~pos~depth=letrecauxaccposdepth=letpos',dir=(pos/2,posmod2)inmatchdepthwith|0->acc|d->aux(Compare.Int.(dir=1)::acc)pos'(d-1)inaux[]posdepth(* Constructs a tree of a given depth in which every right subtree is empty
* and the only leaf contains the hash of el. *)letmake_spine_withel=letrecauxleft=function|0->left|d->(aux[@tailcall])(node_ofleftEmpty)(d-1)inaux(leaf_ofel)letsnoct(el:elt)=letrectraversetreedepthkey=match(tree,key)with|Node(_,t_left,Empty),true::_key->(* The base case where the left subtree is full and we start
* the right subtree by creating a new tree the size of the remaining
* depth and placing the new element in its leftmost position. *)lett_right=make_spine_withel(depth-1)innode_oft_leftt_right|Node(_,t_left,Empty),false::key->(* Traversing left, the left subtree is not full (and thus the right
* subtree is empty). Recurse on left subtree. *)lett_left=traverset_left(depth-1)keyinnode_oft_leftEmpty|Node(_,t_left,t_right),true::key->(* Traversing right, the left subtree is full.
* Recurse on right subtree *)lett_right=traverset_right(depth-1)keyinnode_oft_leftt_right|_,_->(* Impossible by construction of the tree and of the key.
* See [tree] invariants and [to_bin]. *)assertfalseinlettree',depth'=match(t.tree,t.depth,t.next_pos)with|Empty,0,0->(node_of(leaf_ofel)Empty,1)|tree,depth,poswhenInt32.(equal(shift_left1ldepth)(of_intpos))->lett_right=make_spine_witheldepthin(node_oftreet_right,depth+1)|tree,depth,pos->letkey=to_bin~pos~depthin(traversetreedepthkey,depth)in{tree=tree';depth=depth';next_pos=t.next_pos+1}typezipper=Leftofzipper*tree|Rightoftree*zipper|Topletrecrebuild_treezt=matchzwith|Top->t|Left(z,r)->(rebuild_tree[@tailcall])z(node_oftr)|Right(l,z)->(rebuild_tree[@tailcall])z(node_oflt)letsnoc_trt(el:elt)=letrectraverse(z:zipper)treedepthkey=match(tree,key)with|Node(_,t_left,Empty),true::_key->lett_right=make_spine_withel(depth-1)inrebuild_treez(node_oft_leftt_right)|Node(_,t_left,Empty),false::key->letz=Left(z,Empty)in(traverse[@tailcall])zt_left(depth-1)key|Node(_,t_left,t_right),true::key->letz=Right(t_left,z)in(traverse[@tailcall])zt_right(depth-1)key|_,_->(* Impossible by construction of the tree and of the key.
* See [tree] invariants and [to_bin]. *)assertfalseinlettree',depth'=match(t.tree,t.depth,t.next_pos)with|Empty,0,0->(node_of(leaf_ofel)Empty,1)|tree,depth,poswhenInt32.(equal(shift_left1ldepth)(of_intpos))->lett_right=make_spine_witheldepthin(node_oftreet_right,depth+1)|tree,depth,pos->letkey=to_bin~pos~depthin(traverseToptreedepthkey,depth)in{tree=tree';depth=depth';next_pos=t.next_pos+1}letrectree_to_list=function|Empty->[]|Leafh->[h]|Node(_,t_left,t_right)->tree_to_listt_left@tree_to_listt_rightletpath_encoding=Data_encoding.(listH.encoding)letbounded_path_encoding?max_length()=matchmax_lengthwith|None->path_encoding|Somemax_length->Data_encoding.((list~max_length)H.encoding)(* The order of the path is from bottom to top *)letcompute_path{tree;depth;next_pos}pos=ifCompare.Int.(pos<0||pos>=next_pos)thenerrorMerkle_list_invalid_positionelseletkey=to_bin~pos~depthinletrecauxacctreekey=match(tree,key)with|Leaf_,[]->okacc|Node(_,l,r),b::key->ifbthenaux(rootl::acc)rkeyelseaux(rootr::acc)lkey|_->errorMerkle_list_invalid_positioninaux[]treekeyletcheck_pathpathposelexpected_root=letdepth=List.lengthpathinifCompare.Int.(pos>=0)&&Compare.Z.(Z.of_intpos<Z.shift_leftZ.onedepth)thenletkey=List.rev@@to_bin~pos~depthinletcomputed_root=List.fold_left(funacc(sibling,b)->ifbthenhash2siblingaccelsehash2accsibling)(hash_eltel)(List.combine_droppathkey)inok(H.equalcomputed_rootexpected_root)elseerrorMerkle_list_invalid_positionletpath_depthpath=List.lengthpathletbreadth_first_traversal~leaf_func~node_func~empty~resl=letrecaux~depthl=letrecpairsacc=function|[]->List.revacc|[x]->List.rev(node_funcxempty::acc)|x::y::xs->pairs(node_funcxy::acc)xsinmatchpairs[]lwith|[]->resdepthempty|[t]->resdeptht|pl->aux~depth:(depth+1)plinaux(List.mapleaf_funcl)~depth:0letcompute=breadth_first_traversal~leaf_func:hash_elt~node_func:hash2~empty~res:(fun_x->x)letof_listl=letdepth,tree=breadth_first_traversal~leaf_func:leaf_of~node_func:node_of~empty:Empty~res:(fundl->(d+1,l))lin{tree;depth;next_pos=List.lengthl}letroott=roott.treemoduleInternal_for_tests=structletpath_to_listx=xletto_listtree=tree_to_listtree.treeletequalt1t2=letreceq_treet1t2=match(t1,t2)with|Empty,Empty->true|Leafh1,Leafh2->H.equalh1h2|Node(h1,l1,r1),Node(h2,l2,r2)->H.equalh1h2&&eq_treel1l2&&eq_treer1r2|_->falseinCompare.Int.equalt1.deptht2.depth&&Compare.Int.equalt1.next_post2.next_pos&&eq_treet1.treet2.treeendend