🔗 Merkle_list_mli.v

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

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