Skip to main content

🔗 Merkle_list_mli.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.

Parameter max_depth : int int.

Module T.
  Record signature {t h elt path : Set} : Set := {
    
The type of a Merkle list
    t := t;
    
The type of a hash
    h := h;
    
The type of an element
    elt := elt;
    
A path, together with an element's position, is the proof of inclusion of an element in the Merkle list.
    path := path;
    
A dummy path that can be used as a placeholder when no path is actually required.
    dummy_path : path;
    pp_path : Format.formatter path unit;
    
The empty Merkle list
    nil : t;
    
The empty hash
    empty : h;
    
[root t] returns the root hash of a Merkle list.
    root_value : t h;
    
[snoc t el] adds element [el] to a Merkle list [t] and returns the new list.
    snoc : t elt t;
    
Tail recursive variant of [snoc].
    snoc_tr : t elt t;
    
[compute elems] returns the root hash of the Merkle list constructed with [elems].
    compute : list elt h;
    
Encoding of a path.
    path_encoding : Data_encoding.t path;
    
Encoding of a path, with optional bound [max_length].
    bounded_path_encoding : option int unit Data_encoding.t path;
    
[compute_path t pos] computes the path of the element in position [pos].
Can fail with [Merkle_list_invalid_position] if [pos] is negative or if it is greater than the number of elements in the list.
    compute_path : t int M? path;
    
[check_path path pos elt expected_root] checks that an [elt] with path [path] at position [pos] has the [expected_root].
Can fail with [Merkle_list_invalid_position] if [pos] is negative or if it is greater than the number of elements in the list.
    check_path : path int elt h M? bool;
    
[path_depth path] returns the depth of the tree [path] is related to.
    path_depth : path int;
    elt_bytes : elt Bytes.t;
  }.
End T.
Definition T := @T.signature.
Arguments T {_ _ _ _}.

Module S_El.
  Record signature {t : Set} : Set := {
    t := t;
    to_bytes : t bytes;
  }.
End S_El.
Definition S_El := @S_El.signature.
Arguments S_El {_}.

Parameter Make_t :
   {El_t H_t H_Set_t : Set} {H_Map_t : Set Set}
    (El : S_El (t := El_t))
    (H : S.HASH (t := H_t) (Set_t := H_Set_t) (Map_t := H_Map_t)), Set.

Parameter Make_path :
   {El_t H_t H_Set_t : Set} {H_Map_t : Set Set}
    (El : S_El (t := El_t))
    (H : S.HASH (t := H_t) (Set_t := H_Set_t) (Map_t := H_Map_t)), Set.

Parameter Make :
   {El_t H_t H_Set_t : Set} {H_Map_t : Set Set},
   (El : S_El (t := El_t)),
   (H : S.HASH (t := H_t) (Set_t := H_Set_t) (Map_t := H_Map_t)),
  T (t := Make_t El H) (h := H.(S.HASH.t)) (elt := El.(S_El.t))
    (path := Make_path El H).